Merge branch 'main' into aard_custom

Author: tideofwords

.github/workflows/mdbook-check.yml

@@ -0,0 +1,35 @@
+name: Check mdbook compilation
+
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  compile:
+    if: github.event.pull_request.draft == false
+    runs-on: ubuntu-latest
+    env:
+      MDBOOK_VERSION: 0.4.40
+      MDBOOKKATEX_VERSION: 0.7.0
+    steps:
+      - uses: actions/checkout@v4
+      - name: Install mdBook
+        run: |
+          curl --proto '=https' --tlsv1.2 https://sh.rustup.rs -sSf -y | sh
+          rustup update
+          cargo install --version ${MDBOOK_VERSION} mdbook
+          cargo install --version ${MDBOOKKATEX_VERSION} mdbook-katex
+      - name: Build with mdBook
+        run: |
+          cd book
+          mdbook build
+      - name: Check build result
+        run: |
+          if [ -d "book/book" ]; then
+            echo "mdBook compilation success"
+          else
+            echo "mdBook compilation fail"
+            exit 1
+          fi

.github/workflows/mdbook.yml .github/workflows/mdbook-publish.yml.github/workflows/mdbook.yml renamed to .github/workflows/mdbook-publish.yml

@@ -0,0 +1,21 @@
+name: Rust Tests
+
+on:
+  pull_request:
+    branches: [ main ]
+  push:
+    branches: [ main ]
+
+jobs:
+  test:
+    if: github.event.pull_request.draft == false
+    name: Rust tests
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+    - name: Set up Rust
+      uses: actions-rs/toolchain@v1
+      with:
+        toolchain: stable
+    - name: Run tests
+      run: cargo test

.github/workflows/tests.yml

@@ -99,30 +99,40 @@ statement loan_check(receiver: string):
 A Good Boy Pod exposes one custom statement with one custom deduction rule.
 
 ```
-statement good_boy(receiver: PubKey, good_boy_issuers: MerkleTree):
+statement is_good_boy(user: PubKey, good_boy_issuers: MerkleTree):
    - OR():
-      - AND(pod: Pod):
-         # A good boy issuer is my friend
+      - AND(pod: Pod, age: Int):
          - eq(pod.type, SIGNATURE)
          - contains(good_boy_issuers, pod.signer)
-         - eq(pod.friend, receiver)
+         # A good boy issuer says this user is a good boy
+         - eq(pod.user, user)
+         - eq(pod.age, age)
+```
+
+A Friend Pod exposes one custom statement with one custom deduction rule.
+
+```
+statement is_friend(good_boy: PubKey, friend: PubKey, good_boy_issuers: MerkleTree):
+   - OR():
+      - AND(friend_pod: Pod):
+         - eq(pod.type, SIGNATURE)
+         # The issuer is a good boy
+         - is_good_boy(good_boy, good_boy_issuers)
+         # A good boy says this is their friend
+         - eq(pod.signer, good_boy)
+         - eq(pod.friend, friend)
 ```
 
 A Great Boy Pod exposes (in addition to the above) one new custom statement
 with one custom deduction rule.
 
 ```
-statement great_boy(receiver: PubKey, good_boy_issuers: MerkleTree):
+statement is_great_boy(great_boy: PubKey, good_boy_issuers: MerkleTree):
    - OR():
       - AND(friend_pod_0: Pod, friend_pod_1: Pod):
-         # good boy 0 is my friend
-         - eq(friend_pod_0.type, SIGNATURE)
-         - good_boy(friend_pod_0.signer, good_boy_issuers)
-         - eq(friend_pod_0.friend, receiver)
-         # good boy 1 is my friend
-         - eq(friend_pod_1.type, SIGNATURE)
-         - good_boy(friend_pod_1.signer, good_boy_issuers)
-         - eq(friend_pod_1.friend, receiver)
+         # Two good boys consider this user their friend
+         - is_friend(friend_pod_0.signer, great_boy)
+         - is_friend(friend_pod_1.signer, great_boy)
          # good boy 0 != good boy 1
          - neq(friend_pod_0.signer, friend_pod_1.signer)
 ``` 

book/src/examples.md

@@ -94,6 +94,15 @@ root = hash((L_root, R_root, 2)).
 The full `Dictionary` is then represented in the backend as `root` (four field elements in the Plonky2 backend).
 
 ### Example 2
+So for example, imagine we have 8 key-pairs, where the keys are just an enumeration from 0 to 7, then the tree leaves positions would look like:
+![](img/merkletree-example-1-a.png)
+
+Now let's change the key of the leaf `key=1`, and set it as `key=13`. Then, their respective leaf paths will be the same until they diverge in the 4-th bit:
+
+![](img/merkletree-example-1-b.png)
+
+
+### Example 3
 
 Suppose we have 4 key-values, where the first four bits of the hashes of the keys are `0000`, `0100`, `1010` and `1011`. The tree would look like:
 ![](img/merkletree-example-2-a.png)
@@ -136,28 +145,30 @@ For the current use cases, we don't need to prove that the key exists but the va
 
 ```rust
 impl MerkleTree {
-    /// builds a new `MerkleTree` where the leaves contain the given key-values
-    fn new(kvs: HashMap<Value, Value>) -> Self;
-    
     /// returns the root of the tree
-    fn root(&self) -> Result<Hash>;
+    fn root(&self) -> Hash;
+
+    /// returns the value at the given key
+    fn get(&self, key: &Value) -> Result<Value>;
 
+    /// returns a boolean indicating whether the key exists in the tree
+    fn contains(&self, key: &Value) -> bool;
+
     /// returns a proof of existence, which proves that the given key exists in
-    /// the tree. It returns the `value` of the leaf at the given `key`, and
-    /// the `MerkleProof`.
-    fn prove(&self, key: &Value) -> Result<(Value, MerkleProof)>;
-    
+    /// the tree. It returns the `MerkleProof`.
+    fn prove(&self, key: &Value) -> Result<MerkleProof>;
+
     /// returns a proof of non-existence, which proves that the given `key`
     /// does not exist in the tree
     fn prove_nonexistence(&self, key: &Value) -> Result<MerkleProof>;
-    
+
     /// verifies an inclusion proof for the given `key` and `value`
     fn verify(root: Hash, proof: &MerkleProof, key: &Value, value: &Value) -> Result<()>;
-    
+
     /// verifies a non-inclusion proof for the given `key`, that is, the given
     /// `key` does not exist in the tree
     fn verify_nonexistence(root: Hash, proof: &MerkleProof, key: &Value) -> Result<()>;
-    
+
     /// returns an iterator over the leaves of the tree
     fn iter(&self) -> std::collections::hash_map::Iter<Value, Value>;
 }

book/src/merkletree.md

@@ -16,6 +16,30 @@ On the back end, a statement is identified by a unique numerical _identifier_.
 
 The POD system has several builtin statements. These statements are associated to a reserved set of statement IDs.
 
+### Backend statements
+
+<font color="red">TODO: update table of backend statements </font>
+
+A statement is a code (or, in the frontend, string identifier) followed by 0 or more arguments. These arguments may consist of up to three anchored keys and up to one POD value.
+
+The following table summarises the natively-supported statements, where we write `value_of(ak)` for 'the value anchored key `ak` maps to', which is of type `PODValue`, and `key_of(ak)` for the key part of `ak`:
+
+| Code | Identifier  | Args                | Meaning                                                           |
+|------|-------------|---------------------|-------------------------------------------------------------------|
+| 0    | `None`      |                     | no statement (useful for padding)                                 |
+| 1    | `ValueOf`   | `ak`, `value`       | `value_of(ak) = value`                                            |
+| 2    | `Eq`        | `ak1`, `ak2`        | `value_of(ak1) = value_of(ak2)`                                   |
+| 3    | `NEq`       | `ak1`, `ak2`        | `value_of(ak1) != value_of(ak2)`                                  |
+| 4    | `Gt`        | `ak1`, `ak2`        | `value_of(ak1) > value_of(ak2)`                                   |
+| 5    | `LEq`       | `ak1`, `ak2`        | `value_of(ak1) <= value_of(ak2)`                                  |
+| 6    | `Contains`  | `ak1`, `ak2`        | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
+| 7    | `Sintains`  | `ak1`, `ak2`        | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
+| 8    | `SumOf`     | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)`                   |
+| 9    | `ProductOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) * value_of(ak3)`                   |
+| 10   | `MaxOf`     | `ak1`, `ak2`, `ak3` | `value_of(ak1) = max(value_of(ak2), value_of(ak3))`               |
+
+### Frontend statements
+
 ```
 ValueOf(key: AnchoredKey, value: ScalarOrVec)
 

book/src/statements.md

@@ -51,14 +51,15 @@ The array, set and dictionary types are similar types. While all of them use [a
     - `leaf.key=hash(original_key)`
     - `leaf.value=hash(original_value)`
 - **array**: the elements are placed at the value field of each leaf, and the key field is just the array index (integer)
-    - `leaf.value=original_value` 
     - `leaf.key=i` 
+    - `leaf.value=original_value` 
 - **set**: the value field of the leaf is unused, and the key contains the hash of the element
     -  `leaf.key=hash(original_value)`
     - `leaf.value=0`
 
 In the three types, the merkletree under the hood allows to prove inclusion & non-inclusion of the particular entry of the {dictionary/array/set} element.
 
+A concrete implementation of dictionary, array, set can be found at [pod2/src/middleware/containers.rs](https://github.com/0xPARC/pod2/blob/main/src/middleware/containers.rs).
 
 <br><br>