Extend merkletree spec, init SignedPod section, add typos checker in CI (#31)

Extend merkletree spec, init SignedPod section, add typos checker in CI

- extend merkletree spec, converting old hand-drawn diagrams to drawio
  diagrams, and adding new diagrams (related: #6)
- init SignedPod section (related: #2)
- initial draft of the types dictionary, set, array (related: #26)
- add typos checker in CI (and correct the ones that were detected)

Note on drawio diagrams: each image file contains the metadata to edit the diagram in the draw.io website.

.github/workflows/typos.toml

@@ -0,0 +1,2 @@
+[default.extend-words]
+groth = "groth" # to avoid it dectecting it as 'growth'

.github/workflows/typos.yml

@@ -0,0 +1,19 @@
+name: typos
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+
+jobs:
+  typos:
+    if: github.event.pull_request.draft == false
+    name: Spell Check with Typos
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+    - name: Use typos with config file
+      uses: crate-ci/typos@master
+      with: 
+        config: .github/workflows/typos.toml
+

README.md

@@ -1,6 +1,14 @@
 # POD2
 
-Specification can be found at the [`book`](https://github.com/0xPARC/pod2/tree/main/book) directory, a live rendered version at: https://0xparc.github.io/pod2/
-
 ## Usage
 - Run tests: `cargo test --release`
+
+## Book
+The `book` contains the specification of POD2. A rendered version of the site can be found at: https://0xparc.github.io/pod2/
+
+To run it locally:
+- Requirements
+	- [mdbook](https://github.com/rust-lang/mdBook): `cargo install mdbook`
+	- [mdbook-katex](https://github.com/lzanini/mdbook-katex): `cargo install mdbook-katex`
+- Go to the book directory: `cd book`
+- Run the mdbook: `mdbook serve`

book/README.md

@@ -1,10 +0,0 @@
-# pod2-docs
-> Hackmds for sharing ideas, once there is consensus around it, move it into this repo to consolidate it. Also we can use PRs to discuss asynchronously specific ideas of the spec.
-
-## Usage
-A rendered version of the site can be found at: https://0xparc.github.io/pod2-docs/
-
-To run it locally:
-- Needs [mdbook](https://github.com/rust-lang/mdBook), to install: `cargo install mdbook`
-- Needs [mdbook-katex](https://github.com/lzanini/mdbook-katex), to install: `cargo install mdbook-katex`
-- Run locally: `mdbook serve`

book/src/SUMMARY.md

@@ -3,7 +3,7 @@
 - [Introduction](./introduction.md)
 
 # Specification
-- [Data types](./datatypes.md)
+- [Backend types](./backendtypes.md)
 	- [MerkleTree](./merkletree.md)
 - [Deductions](./deductions.md)
 	- [Statements](./statements.md)

book/src/backendtypes.md

@@ -0,0 +1 @@
+# Backend types

book/src/datatypes.md

@@ -1 +0,0 @@
-# Data types

book/src/examples.md

@@ -58,7 +58,7 @@ statement loan_check(receiver: PubKey):
          - lt(paystub.start_date, NOW_MINUS_1Y) # start_date is more than 1y old
          - gt(paystub.issue_date, NOW_MINUS_7D) # issue_date is less than 7d old
          # Annual salary is at least $20,000
-         - gt(paystub.anual_salary, 20000)
+         - gt(paystub.annual_salary, 20000)
 ```
 
 ## ZuKYC (simplified for P1)

book/src/merkletree.md

@@ -1,13 +1,26 @@
 # MerkleTree
 
-In the POD system, MerkleTrees are used to store the key-values of the POD.
+In the POD system, MerkleTrees are used to store the key-values of the POD. From the high level, we can think of it as a 'hashmap' storage, that allows us to generate proofs of inclusion and non-inclusion of the key-values stored into it.
 
-- Each leaf contains a touple of `key` and `value`
-- Leaf position is determined by the `key` content binary representation (little-endian)
 
-![](img/merkletree0.png)
+## Leaves
+Each leaf position is determined by the `key` content in binary representation (little-endian).
 
-So for example, suppose we have the following data in a POD:
+### Example 1
+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)
+
+
+### Example2
+
+Suppose we have 4 key-values, where the keys are `0000`, `0100`, `1010` and `1011`. The tree would look like:
+![](img/merkletree-example-2-a.png)
+
+To iterate this example, suppose we have the following data in a POD:
 ```js
 {
 	id: "11000...",
@@ -16,30 +29,63 @@ So for example, suppose we have the following data in a POD:
 		dateOfBirth: 1169909384,
 		userPk: 9876543210, // target user of this POD
 		_signerPk: 1234567890, // signer of the POD
-	}
+	},
+	// ...
 }
 ```
 
 The merkletree will contain the key values from the `kvs` field.
 
-Suppose that the binary representation of the key `userPk` is `1011...`. This uniquely defines the leaf position that contains the public key of the authenticated user.
+Suppose that the binary representation of the key `userPk` is `1011...`. This uniquely defines the leaf position that contains the public key of the authenticated user. Similarly for the other key-values:
 
-![](img/merkletree1.png)
+![](img/merkletree-example-2-b.png)
 
 
 ## Proofs of inclusion and non-inclusion
 Merkle proofs contain the siblings along the path from the leaf to the root, where the leaf position is determined by the key binary representation. 
 
 Since leaf positions are deterministic based on the key, the same approach is used for non-inclusion proofs, where it can be proven that a key is not in the tree, and furthermore, that a value is not in the tree (although the key exists):
-- Proving that the key does not exist in the tree is achieved by generating the merkle-proof for the specific key, and showing that the (virtual) leaf is empty - this is, showing that going down the path of the non-existing key, there is a leaf with a different key, meaning that the non-existing key has not been inserted in the tree.
-- Proving that a value is not in the tree (although the key exists) is achieved by generating the merkle-proof for the specific key, and showing that the leaf exists but it has a different value than the one being proved.
+1. Proving that the key does not exist in the tree is achieved by generating the merkle-proof for the specific key, and showing that the (virtual) leaf is empty - this is, showing that going down the path of the non-existing key, there is a leaf with a different key, meaning that the non-existing key has not been inserted in the tree.
+2. Proving that a value is not in the tree (although the key exists) is achieved by generating the merkle-proof for the specific key, and showing that the leaf exists but it has a different value than the one being proved.
 
+For the current use cases, we don't need to prove that the key exists but the value is different on that leaf, so we only use the option 1.
 
 
 ## Encoding
 > TODO: how key-values, nodes, merkle-proofs, ... are encoded.
 
-## Developement plan
+## Interface
+
+```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>;
+    
+    /// 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)>;
+    
+    /// 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>;
+}
+```
+
+## Development plan
 - short term: merkle tree as a 'precompile' in POD operations, which allows to directly verify proofs
 	- initial version: just a wrapper on top of the existing Plonky2's MerkleTree
 	- second iteration: implement the MerkleTree specified in this document

book/src/signedpod.md

@@ -1 +1,27 @@
-# SignedPOD
+# SignedPod
+
+A SignedPod consists of the following fields:
+- `mt`: key-values storage, internally it's a [MerkleTree](./merkletree.md) so that we can generate proofs on the key-values
+	- it can only contain [`ValueOf` statements](./statements.md).
+	- the Signer's public key is one of the key-values in the `kvs`.
+- `id`: the Root of the `kvs` MerkleTree
+- `signature`: a signature over the `id`
+
+<br>
+
+![](img/SignedPod.png)
+
+
+Example of SignedPod:
+```javascript
+{
+    id: "05f7a6de...",
+    kvs : {
+        _signerKey: "5e1c0b3c...",
+        idNumber: "94e328a7...",
+        dateOfBirth: 1169909384,
+        socialSecurityNum: "1111"
+    },
+    signature: "68b615f7..."
+}
+```

book/src/values.md

@@ -2,7 +2,7 @@
 From the frontend perspective, POD values may be one of three[^type] types:
 - `Integer`
 - `String`
-- `MerkleTree`
+- `Dictionary`, `array`, `set`
 
 From the backend perspective, however, these types will all be encoded as a fixed number of field elements, the number being chosen so as to accommodate the `Integer` type as well as hashes to represent the `String` and `MerkleTree` types with the appropriate level of security.
 
@@ -10,6 +10,7 @@ In the case of the Plonky2 backend with 100 bits of security, all of these types
 
 $$\texttt{HashOut<GoldilocksField>}\simeq\texttt{[GoldilocksField; 4]}.$$
 
+
 ## `Integer`
 In the frontend, this type is none other than `u64`[^i64]. In the backend, it will be appropriately embedded into the codomain of the canonical hash function.
 
@@ -19,12 +20,33 @@ with $0 \leq x_0, x_1 < 2^{32}$ and representing it as
 $$\texttt{map}\ \iota\ [x_0, x_1, 0, 0],$$
 where $\iota:\mathbb{N}\rightarrow\texttt{GoldilocksField}$ is the canonical projection.
 
+
 ## `String`
 In the frontend, this type corresponds to the usual `String`. In the backend, the string will be mapped to a sequence of field elements[^String] and hashed with the hash function employed there, thus being represented by its hash.
 
-## `MerkleTree`
-In the front end, this type encapsulates a sparse Merkle tree. In the backend, this will be represented by the root hash of the tree, which will be of the type of the output of the hash function employed.
+
+## Dictionary, array, set
+
+The array, set and dictionary types are similar types. While all of them use [a merkletree](./merkletree.md) under the hood, each of them uses it in a specific way:
+- **dictionary**: the user original keys and values are hashed to be used in the leaf.
+    - `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` 
+- **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.
+
+
+<br><br>
+
+---
+
 
 [^type]: <font color="red">TODO</font> In POD 1, there is the `cryptographic` type, which has the same type of the output of the hash function employed there. It is useful for representing arbitrary hashes. Do we want to expand our type list to include a similar type, which would correspond to the `HashOut` type in the case of Plonky2? This would not have a uniform representation in the frontend if we continue to be backend agnostic unless we fix the number of bits to e.g. 256, in which case we would actually need one more field element in the case of Plonky2.
 [^i64]: <font color="red">TODO</font> Replace this with `i64` once operational details have been worked out.
 [^String]: <font color="red">TODO</font> Adopt or recommend a particular approach, e.g. mapping the string to bytes and separating it into chunks with appropriate padding.
+

src/merkletree.rs

@@ -31,7 +31,7 @@ pub struct MerkleTree {
     // kvs are a field in the MerkleTree in order to be able to iterate over the keyvalues. This is
     // specific of the current implementation (Plonky2's tree wrapper), in the next iteration this
     // will not be needed since the tree implementation itself will offer the hashmap
-    // functionallity.
+    // functionality.
     kvs: HashMap<Hash, Value>,
 }