Skip to content

Commit 5d13ac3

Browse files
tideofwordsax0
tideofwords
and
ax0
authored
update docs (#242)
* Update docs: Statements, operations, syntactic sugar * Update docs: Remove low-level Merkle tree statements * Update docs: typo * Update book/src/operations.md Co-authored-by: Ahmad Afuni <root@ahmadafuni.com> * Eq -> Equal Co-authored-by: Ahmad Afuni <root@ahmadafuni.com> * Eq -> Equal, again Co-authored-by: Ahmad Afuni <root@ahmadafuni.com> * Eq -> Equal, yet again Co-authored-by: Ahmad Afuni <root@ahmadafuni.com> --------- Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>
1 parent 88a7598 commit 5d13ac3

File tree

4 files changed

+74
-81
lines changed

4 files changed

+74
-81
lines changed

‎book/src/SUMMARY.md‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@
1313
- [Signature](./signature.md)
1414
- [Deductions](./deductions.md)
1515
- [Statements](./statements.md)
16-
- [Statements involving compound types and Merkle trees](./merklestatements.md)
1716
- [Operations](./operations.md)
1817
- [Simple example](./simpleexample.md)
1918
- [Custom statements and custom operations](./custom.md)

‎book/src/merklestatements.md‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,33 @@
1+
# Copied from statements.md
2+
3+
```
4+
Branches(parent: AnchoredKey::MerkleTree, left: AnchoredKey::MerkleTree, right: AnchoredKey::MerkleTree)
5+
6+
Leaf(node: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)
7+
8+
IsNullTree(node: AnchoredKey::MerkleTree)
9+
10+
GoesLeft(key: AnchoredKey, depth: Value::Integer)
11+
12+
GoesRight(key: AnchoredKey, depth: Value::Integer)
13+
14+
Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)
15+
16+
MerkleSubtree(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree)
17+
18+
MerkleCorrectPath(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree, key: AnchoredKey, depth: Value::Integer)
19+
20+
Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)
21+
22+
NotContains(root: AnchoredKey::MerkleTree, key: AnchoredKey)
23+
24+
ContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)
25+
26+
NotContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)
27+
28+
ContainsValue(root: AnchoredKey::Array, value: AnchoredKey)
29+
```
30+
131
# Statements involving compound types and Merkle trees
232

333
The front end has three compound types

‎book/src/operations.md‎

Lines changed: 27 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -10,22 +10,33 @@ The following table summarises the natively-supported operations:
1010
| 0 | `None` | | | `None` |
1111
| 1 | `NewEntry`[^newentry] | `(key, value)` | | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 |
1212
| 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-
| 16 | `HashOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = hash(value2, value3)`| `HashOf(ak1, ak2, ak3)` |
27-
28-
<!-- NOTE: should we 'uniformize' the names? eg. currently we have `EntryGt` and `GtToNEq` -->
13+
| 3 | `EqualFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Equal(ak1, ak2)` |
14+
| 4 | `NotEqualFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NotEqual(ak1, ak2)` |
15+
| 5 | `LtEqFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LtEq(ak1, ak2)` |
16+
| 6 | `LtFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 < value2` | `Lt(ak1, ak2)` |
17+
| 7 | `TransitiveEqualFromStatements` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Equal(ak1, ak4)` |
18+
| 8 | `LtToNotEqual` | `s` | `s = Lt(ak1, ak2)` | `NotEqual(ak1, ak2)` |
19+
| 9 | `ContainsFromEntries` | `s1`, `s2`, `s3`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `merkle_includes(value1, value2, value3, proof) = true` | `Contains(ak1, ak2, ak3)` |
20+
| 10 | `NotContainsFromEntries` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `NotContains(ak1, ak2)` |
21+
| 11 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
22+
| 12 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
23+
| 13 | `MaxOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = max(value2, value3)` | `MaxOf(ak1, ak2, ak3)` |
24+
| 14 | `HashOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = hash(value2, value3)`| `HashOf(ak1, ak2, ak3)` |
25+
26+
<br><br>
27+
28+
The following table summarizes "syntactic sugar" operations. These operations are not supported by the backend. The frontend compiler is responsible for translating these operations into the operations above.
29+
30+
| Code | Identifier | Args and desugaring |
31+
|------|-----------------------|---------------------|
32+
| 1001 | DictContainsFromEntries | `DictContainsFromEntries(dict_st, key_st, value_st) -> ContainsFromEntries(dict_st, key_st, value_st)` |
33+
| 1002 | DictNotContainsFromEntries | `DictNotContainsFromEntries(dict_st, key_st, value_st) -> NotContainsFromEntries(dict_st, key_st, value_st)` |
34+
| 1003 | SetContainsFromEntries | `SetContainsFromEntries(set_st, value_st) -> ContainsFromEntries(set_st, value_st, value_st)` |
35+
| 1004 | SetNotContainsFromEntries | `SetNotContainsFromEntries(set_st, value_st) -> NotContainsFromEntries(set_st, value_st, value_st)` |
36+
| 1005 | ArrayContainsFromEntries | `ArrayContainsFromEntries(array_st, index_st, value_st) -> ContainsFromEntries(array_st, index_st, value_st)` |
37+
| 1006 | GtEqFromEntries | `GtEqFromEntries(s1, s2) -> LtEqFromEntries(s2, s1)` |
38+
| 1007 | GtFromEntries | `GtFromEntries(s1, s2) -> LtFromEntries(s2, s1)` |
39+
| 1008 | GtToNotEqual | `GtToNotEqual(s1, s2) -> LtToNotEqual(s1, s2)` |
2940

3041
<br><br>
3142

‎book/src/statements.md‎

Lines changed: 17 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -27,10 +27,10 @@ The following table summarises the natively-supported statements, where we write
2727
| 0 | `None` | | no statement, always true (useful for padding) |
2828
| 1 | `False` | | always false (useful for padding disjunctions) |
2929
| 2 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` |
30-
| 3 | `Eq` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
31-
| 4 | `NEq` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
32-
| 5 | `Gt` | `ak1`, `ak2` | `value_of(ak1) > value_of(ak2)` |
33-
| 6 | `LEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
30+
| 3 | `Equal` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
31+
| 4 | `NotEqual` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
32+
| 5 | `LtEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
33+
| 6 | `Lt` | `ak1`, `ak2` | `value_of(ak1) < value_of(ak2)` |
3434
| 7 | `Contains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
3535
| 8 | `NotContains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
3636
| 9 | `SumOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)` |
@@ -40,68 +40,25 @@ The following table summarises the natively-supported statements, where we write
4040

4141
### Frontend statements
4242

43-
<span style="color:red">TODO: Current implementation frontend Statements reuse the middleware Statements, which:</span><br>
44-
<span style="color:red">- 1: GEq & LEq don't appear in the frontend impl</span><br>
45-
<span style="color:red">- 2: frontend impl has Contains & NotContains, which don't appear at the following block</span>
46-
```
47-
ValueOf(key: AnchoredKey, value: ScalarOrVec)
48-
49-
Equal(ak1: AnchoredKey, ak2: AnchoredKey)
50-
51-
NotEqual(ak1: AnchoredKey, ak2: AnchoredKey)
52-
53-
Gt(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)
54-
55-
Lt(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)
56-
57-
GEq(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)
58-
59-
LEq(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)
60-
61-
SumOf(sum: AnchoredKey::Integer, arg1: AnchoredKey::Integer, arg2:
62-
AnchoredKey::Integer)
63-
64-
ProductOf(prod: AnchoredKey::Integer, arg1: AnchoredKey::Integer, arg2: AnchoredKey::Integer)
65-
66-
MaxOf(max: AnchoredKey::Integer, arg1: AnchoredKey::Integer, arg2: AnchoredKey::Integer)
67-
68-
HashOf(ak1: AnchoredKey::Raw, arg1: AnchoredKey::Raw, arg2: AnchoredKey::Raw)
69-
```
70-
71-
The following statements relate to Merkle trees and compound types; they are explained in detail on a [separate page](./merklestatements.md).
72-
```
73-
Branches(parent: AnchoredKey::MerkleTree, left: AnchoredKey::MerkleTree, right: AnchoredKey::MerkleTree)
43+
The frontend also exposes the following syntactic sugar predicates. These predicates are not supported by the backend. The frontend compiler is responsible for translating these predicates into the predicates above.
7444

75-
Leaf(node: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)
76-
77-
IsNullTree(node: AnchoredKey::MerkleTree)
78-
79-
GoesLeft(key: AnchoredKey, depth: Value::Integer)
80-
81-
GoesRight(key: AnchoredKey, depth: Value::Integer)
82-
83-
Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)
84-
85-
MerkleSubtree(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree)
86-
87-
MerkleCorrectPath(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree, key: AnchoredKey, depth: Value::Integer)
88-
89-
Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)
90-
91-
NotContains(root: AnchoredKey::MerkleTree, key: AnchoredKey)
92-
93-
ContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)
94-
95-
NotContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)
96-
97-
ContainsValue(root: AnchoredKey::Array, value: AnchoredKey)
98-
```
45+
| Code | Identifier | Args and desugaring |
46+
|------|---------------|---------------------|
47+
| 1000 | DictContains | `DictContains(root, key, val) -> Contains(root, key, val)` |
48+
| 1001 | DictNotContains | `DictNotContains(root, key, val) -> NotContains(root, key, val)` |
49+
| 1002 | SetContains | `SetContains(root, val) -> Contains(root, val, val)` |
50+
| 1003 | SetNotContains | `SetNotContains(root, val) -> Contains(root, val, val)` |
51+
| 1004 | ArrayContains | `ArrayContains(root, idx, val) -> Contains(root, idx, val)` |
52+
| 1005 | GtEq | `GtEq(a, b) -> LtEq(b, a)`|
53+
| 1006 | Gt | `Gt(a, b) -> Lt(b, a)` |
9954

10055

10156
In the future, we may also reserve statement IDs for "precompiles" such as:
10257
```
103-
EcdsaPrivToPubOf(A.pubkey, B.privkey)
58+
EcdsaPrivToPubOf(A.pubkey, B.privkey),
10459
```
60+
as well as for low-level operations on Merkle trees and compound types.
61+
<font color="red">NOTE</font> Merkle trees and compound types explained in a separate markdown file `./merklestatements.md` which is no longer part of these docs, but saved in the github repo in case we need to restore it in the future.
10562

10663
### Built-in statements for entries of any type
10764

@@ -143,10 +100,6 @@ poseidon_hash_of(A.hash, B.preimage) // perhaps a hash_of predicate can be param
143100
ecdsa_priv_to_pub_of(A.pubkey, B.privkey)
144101
```
145102

146-
##### Primitive Built-in Statements for Merkle Roots
147-
148-
[See separate page](./merklestatements.md).
149-
150103

151104

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

0 commit comments

Comments
 (0)