Skip to content

Commit 2245185

Browse files
arnaucubearnaucube
committed
sync spec & code
1 parent 5092149 commit 2245185

File tree

11 files changed

+71
-52
lines changed

11 files changed

+71
-52
lines changed

‎book/book.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,4 +9,4 @@ title = "POD2-docs"
99
default-theme = "light"
1010

1111
[preprocessor.katex]
12-
after = ["links"]
12+
after = ["links"]

‎book/src/SUMMARY.md‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@
2222
- [POD types](./podtypes.md)
2323
- [SignedPOD](./signedpod.md)
2424
- [MainPOD](./mainpod.md)
25-
- [MockPOD](./mockpod.md)
2625
- [Examples](./examples.md)
2726

2827
# Architecture

‎book/src/examples.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
Examples of POD2 use cases
44

55
## EthDos
6+
*Check also the [custom statement example](./customexample.md) section.*
67

78
Original in prolog https://gist.github.com/ludns/f84b379ec8c53c97b7f95630e16cc39c#file-eth_dos-pl
89

‎book/src/merklestatements.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
The front end has three compound types
44
- `Dictionary`
55
- `Array`
6-
- `Set`,
6+
- `Set`
77

88
all of which are represented as `MerkleTree` on the back end.
99

@@ -194,4 +194,4 @@ keyhash = hash(key)
194194
```ContainsValue(root, value)``` is deduced from
195195
```
196196
Contains(root, idx, value).
197-
```
197+
```

‎book/src/merkletree.md‎

Lines changed: 20 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -145,39 +145,48 @@ For the current use cases, we don't need to prove that the key exists but the va
145145

146146
```rust
147147
impl MerkleTree {
148+
/// builds a new `MerkleTree` where the leaves contain the given key-values
149+
fn new(max_depth: usize, kvs: &HashMap<Value, Value>) -> Result<Self>;
150+
148151
/// returns the root of the tree
149152
fn root(&self) -> Hash;
153+
154+
/// returns the max_depth parameter from the tree
155+
fn max_depth(&self) -> usize;
150156

151157
/// returns the value at the given key
152158
fn get(&self, key: &Value) -> Result<Value>;
153159

154160
/// returns a boolean indicating whether the key exists in the tree
155-
fn contains(&self, key: &Value) -> bool;
161+
fn contains(&self, key: &Value) -> Result<bool>;
156162

157163
/// returns a proof of existence, which proves that the given key exists in
158-
/// the tree. It returns the `MerkleProof`.
159-
fn prove(&self, key: &Value) -> Result<MerkleProof>;
160-
161-
/// returns a proof of non-existence, which proves that the given `key`
162-
/// does not exist in the tree
164+
/// the tree. It returns the `value` of the leaf at the given `key`, and the
165+
/// `MerkleProof`.
166+
fn prove(&self, key: &Value) -> Result<(Value, MerkleProof)>;
167+
168+
/// returns a proof of non-existence, which proves that the given
169+
/// `key` does not exist in the tree. The return value specifies
170+
/// the key-value pair in the leaf reached as a result of
171+
/// resolving `key` as well as a `MerkleProof`.
163172
fn prove_nonexistence(&self, key: &Value) -> Result<MerkleProof>;
164173

165174
/// verifies an inclusion proof for the given `key` and `value`
166-
fn verify(root: Hash, proof: &MerkleProof, key: &Value, value: &Value) -> Result<()>;
175+
fn verify(max_depth: usize, root: Hash, proof: &MerkleProof,
176+
key: &Value, value: &Value,) -> Result<()>;
167177

168178
/// verifies a non-inclusion proof for the given `key`, that is, the given
169179
/// `key` does not exist in the tree
170-
fn verify_nonexistence(root: Hash, proof: &MerkleProof, key: &Value) -> Result<()>;
180+
fn verify_nonexistence( max_depth: usize, root: Hash,
181+
proof: &MerkleProof, key: &Value,) -> Result<()>;
171182

172183
/// returns an iterator over the leaves of the tree
173-
fn iter(&self) -> std::collections::hash_map::Iter<Value, Value>;
184+
fn iter(&self) -> Iter;
174185
}
175186
```
176187

177188
## Development plan
178189
- short term: merkle tree as a 'precompile' in POD operations, which allows to directly verify proofs
179-
- initial version: just a wrapper on top of the existing Plonky2's MerkleTree
180-
- second iteration: implement the MerkleTree specified in this document
181190
- long term exploration:
182191
- explore feasibility of using Starky (for lookups) connected to Plonky2, which would allow doing the approach described at [https://hackmd.io/@aardvark/SkJ-wcTDJe](https://hackmd.io/@aardvark/SkJ-wcTDJe)
183192

‎book/src/mockpod.md‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎book/src/operations.md‎

Lines changed: 24 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -9,23 +9,33 @@ The following table summarises the natively-supported operations:
99
|------|-----------------------|---------------------|-----------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------|
1010
| 0 | `None` | | | `None` |
1111
| 1 | `NewEntry`[^newentry] | `(key, value)` | | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 |
12-
| 2 | `EntryEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Eq(ak1, ak2)` |
12+
| 2 | `CopyStatement` | `s` | | |
13+
| 3 | `EntryEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Eq(ak1, ak2)` |
14+
| 4 | `EntryNEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NEq(ak1, ak2)` |
15+
| 5 | `EntryGt` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2` | `Gt(ak1, ak2)` |
16+
| 6 | `EntryLEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LEq(ak1, ak2)` |
17+
| 7 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
18+
| 8 | `GtToNEq` | `s` | `s = Gt(ak1, ak2)` | `NEq(ak1, ak2)` |
19+
| 9 | `LtToNEq` | `s` | `s = Lt(ak1, ak2)` | `NEq(ak1, ak2)` |
20+
| 10 | `EntryContains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_includes(value1, value2, proof) = true` | `Contains(ak1, ak2)` |
21+
| 11 | `EntrySintains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `Sintains(ak1, ak2)` |
22+
| 12 | `RenameContains` | `s1`, `s2` | `s1 = Contains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Contains(ak4, ak2)` |
23+
| 13 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
24+
| 14 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
25+
| 15 | `MaxOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = max(value2, value3)` | `MaxOf(ak1, ak2, ak3)` |
26+
27+
<!-- NOTE: should we 'uniformalize' the names? eg. currently we have `EntryGt` and `GtToNEq` -->
28+
29+
<span style="color:red">WIP, the following ones were appearing at the docs table but not at the implementation ([src/middleware/operation.rs](https://github.com/0xPARC/pod2/blob/main/src/middleware/operation.rs#L20)):</span><br>
30+
<span style="color:red">TODO rm?</span>
31+
| Code | Identifier | Args | Condition | Output |
32+
|------|-----------------------|---------------------|-----------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------|
1333
| 3 | `SymmetricEq` | `s` | `s = Equal(ak1, ak2)` | `Eq(ak2, ak1)` |
14-
| 4 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
15-
| 5 | `EntryNEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NEq(ak1, ak2)` |
1634
| 6 | `SymmetricNEq` | `s` | `s = NotEqual(ak1, ak2)` | `NEq(ak2, ak1)` |
17-
| 7 | `GtToNEq` | `s` | `s = Gt(ak1, ak2)` | `NEq(ak1, ak2)` |
18-
| 8 | `LEqToNEq` | `s` | `s = LEq(ak1, ak2)` | `NEq(ak1, ak2)` |
19-
| 9 | `EntryGt` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2` | `Gt(ak1, ak2)` |
35+
| 16 | `RenameSintains` | `s1`, `s2` | `s1 = Sintains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Sintains(ak4, ak2)` |
36+
| 7 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
37+
| 6 | `LEqToNEq` | `s` | `s = LEq(ak1, ak2)` | `NEq(ak1, ak2)` |
2038
| 10 | `TransitiveGt` | `s1`, `s2` | `s1 = Gt(ak1, ak2)`, `s2 = Gt(ak3, ak4)`, `ak2 = ak3` | `Gt(ak1, ak4)` |
21-
| 11 | `EntryLEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LEq(ak1, ak2)` |
2239
| 12 | `TransitiveLEq` | `s1`, `s2` | `s1 = LEq(ak1, ak2)`, `s2 = LEq(ak3, ak4)`, `ak2 = ak3` | `LEq(ak1, ak4)` |
23-
| 13 | `EntryContains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_includes(value1, value2, proof) = true` | `Contains(ak1, ak2)` |
24-
| 14 | `RenameContains` | `s1`, `s2` | `s1 = Contains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Contains(ak4, ak2)` |
25-
| 15 | `EntrySintains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `Sintains(ak1, ak2)` |
26-
| 16 | `RenameSintains` | `s1`, `s2` | `s1 = Sintains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Sintains(ak4, ak2)` |
27-
| 17 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
28-
| 18 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
29-
| 19 | `MaxOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = max(value2, value3)` | `MaxOf(ak1, ak2, ak3)` |
3040

3141
[^newentry]: Since new key-value pairs are not constrained, this operation will have no arguments in-circuit.

‎book/src/statements.md‎

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -18,28 +18,29 @@ The POD system has several builtin statements. These statements are associated t
1818

1919
### Backend statements
2020

21-
<font color="red">TODO: update table of backend statements </font>
22-
2321
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.
2422

2523
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`:
2624

27-
| Code | Identifier | Args | Meaning |
28-
|------|-------------|---------------------|-------------------------------------------------------------------|
29-
| 0 | `None` | | no statement (useful for padding) |
30-
| 1 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` |
31-
| 2 | `Eq` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
32-
| 3 | `NEq` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
33-
| 4 | `Gt` | `ak1`, `ak2` | `value_of(ak1) > value_of(ak2)` |
34-
| 5 | `LEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
35-
| 6 | `Contains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
36-
| 7 | `Sintains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
37-
| 8 | `SumOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)` |
38-
| 9 | `ProductOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) * value_of(ak3)` |
39-
| 10 | `MaxOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = max(value_of(ak2), value_of(ak3))` |
25+
| Code | Identifier | Args | Meaning |
26+
|------|---------------|---------------------|-------------------------------------------------------------------|
27+
| 0 | `None` | | no statement (useful for padding) |
28+
| 1 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` |
29+
| 2 | `Eq` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
30+
| 3 | `NEq` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
31+
| 4 | `Gt` | `ak1`, `ak2` | `value_of(ak1) > value_of(ak2)` |
32+
| 5 | `LEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
33+
| 6 | `Contains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
34+
| 7 | `NotContains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
35+
| 8 | `SumOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)` |
36+
| 9 | `ProductOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) * value_of(ak3)` |
37+
| 10 | `MaxOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = max(value_of(ak2), value_of(ak3))` |
4038

4139
### Frontend statements
4240

41+
<span style="color:red">TODO: Current implementation frontend Statements reuse the middleware Statements, which:</span><br>
42+
<span style="color:red">- 1: GEq & LEq don't appear in the frontend impl</span><br>
43+
<span style="color:red">- 2: frontend impl has Contains & NotCointains, which don't appear at the following block</span>
4344
```
4445
ValueOf(key: AnchoredKey, value: ScalarOrVec)
4546
@@ -150,4 +151,4 @@ ecdsa_priv_to_pub_of(A.pubkey, B.privkey)
150151

151152
[^builtin]: <font color="red">TODO</font> List of built-in statements is not yet complete.
152153

153-
[^fillsum]: <font color="red">TODO</font> Does sum mean x+y = z or x = y+z?
154+
[^fillsum]: <font color="red">TODO</font> Does sum mean x+y = z or x = y+z?

‎book/src/values.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ In the frontend, this is a simple bool. In the backend, it will have the same e
2727
In the frontend, this type corresponds to the usual `String`. In the backend, the string will be mapped to a sequence of field elements and hashed with the hash function employed there, thus being represented by its hash.
2828

2929
## `Raw`
30-
"Raw" is short for "raw value". A `Raw` exposes a backend value on the frontend.
30+
"Raw" is short for "raw value". A `Raw` exposes a [backend `Value`](./backendtypes.md) on the frontend.
3131

3232
With the plonky2 backend, a `Raw` is a tuple of 4 elements of the Goldilocks field.
3333

‎src/frontend/mod.rs‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -578,13 +578,12 @@ pub mod tests {
578578
let sanction_list = sanction_list.sign(&mut signer).unwrap();
579579
println!("{}", sanction_list);
580580

581-
let kyc = zu_kyc_pod_builder(&params, &gov_id, &pay_stub, &sanction_list)?;
582-
println!("{}", kyc);
581+
let kyc_builder = zu_kyc_pod_builder(&params, &gov_id, &pay_stub, &sanction_list)?;
582+
println!("{}", kyc_builder);
583583

584584
let mut prover = MockProver {};
585-
let kyc = kyc.prove(&mut prover, &params)?;
585+
let kyc = kyc_builder.prove(&mut prover, &params)?;
586586

587-
// TODO: prove kyc with MockProver and print it
588587
println!("{}", kyc);
589588

590589
Ok(())
@@ -595,7 +594,7 @@ pub mod tests {
595594
let great_boy = great_boy_pod_full_flow()?;
596595
println!("{}", great_boy);
597596

598-
// TODO: prove kyc with MockProver and print it
597+
// TODO: prove great_boy with MockProver and print it
599598

600599
Ok(())
601600
}

0 commit comments

Comments
 (0)