Skip to content

update docs #242

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ax0 merged 7 commits into from
Jun 3, 2025
Merged

update docs #242

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
c6bd4d6
Update docs: Statements, operations, syntactic sugar
tideofwords May 23, 2025
0f0249e
Update docs: Remove low-level Merkle tree statements
tideofwords May 23, 2025
b313573
Update docs: typo
tideofwords May 23, 2025
a1f487c
Update book/src/operations.md
tideofwords May 28, 2025
4580148
Eq -> Equal
tideofwords May 28, 2025
7f7e38d
Eq -> Equal, again
tideofwords May 28, 2025
9fa8394
Eq -> Equal, yet again
tideofwords May 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion book/src/SUMMARY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@
- [Signature](./signature.md)
- [Deductions](./deductions.md)
- [Statements](./statements.md)
- [Statements involving compound types and Merkle trees](./merklestatements.md)
- [Operations](./operations.md)
- [Simple example](./simpleexample.md)
- [Custom statements and custom operations](./custom.md)
Expand Down
30 changes: 30 additions & 0 deletions book/src/merklestatements.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,33 @@
# Copied from statements.md

```
Branches(parent: AnchoredKey::MerkleTree, left: AnchoredKey::MerkleTree, right: AnchoredKey::MerkleTree)

Leaf(node: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)

IsNullTree(node: AnchoredKey::MerkleTree)

GoesLeft(key: AnchoredKey, depth: Value::Integer)

GoesRight(key: AnchoredKey, depth: Value::Integer)

Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)

MerkleSubtree(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree)

MerkleCorrectPath(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree, key: AnchoredKey, depth: Value::Integer)

Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)

NotContains(root: AnchoredKey::MerkleTree, key: AnchoredKey)

ContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)

NotContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)

ContainsValue(root: AnchoredKey::Array, value: AnchoredKey)
```

# Statements involving compound types and Merkle trees

The front end has three compound types
Expand Down
43 changes: 27 additions & 16 deletions book/src/operations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,22 +10,33 @@ The following table summarises the natively-supported operations:
| 0 | `None` | | | `None` |
| 1 | `NewEntry`[^newentry] | `(key, value)` | | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 |
| 2 | `CopyStatement` | `s` | | |
| 3 | `EntryEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Eq(ak1, ak2)` |
| 4 | `EntryNEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NEq(ak1, ak2)` |
| 5 | `EntryGt` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2` | `Gt(ak1, ak2)` |
| 6 | `EntryLEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LEq(ak1, ak2)` |
| 7 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` |
| 8 | `GtToNEq` | `s` | `s = Gt(ak1, ak2)` | `NEq(ak1, ak2)` |
| 9 | `LtToNEq` | `s` | `s = Lt(ak1, ak2)` | `NEq(ak1, ak2)` |
| 10 | `EntryContains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_includes(value1, value2, proof) = true` | `Contains(ak1, ak2)` |
| 11 | `EntrySintains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `Sintains(ak1, ak2)` |
| 12 | `RenameContains` | `s1`, `s2` | `s1 = Contains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Contains(ak4, ak2)` |
| 13 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
| 14 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
| 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)` |
| 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)` |

<!-- NOTE: should we 'uniformize' the names? eg. currently we have `EntryGt` and `GtToNEq` -->
| 3 | `EqualFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Equal(ak1, ak2)` |
| 4 | `NotEqualFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NotEqual(ak1, ak2)` |
| 5 | `LtEqFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LtEq(ak1, ak2)` |
| 6 | `LtFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 < value2` | `Lt(ak1, ak2)` |
| 7 | `TransitiveEqualFromStatements` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Equal(ak1, ak4)` |
| 8 | `LtToNotEqual` | `s` | `s = Lt(ak1, ak2)` | `NotEqual(ak1, ak2)` |
| 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)` |
| 10 | `NotContainsFromEntries` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `NotContains(ak1, ak2)` |
| 11 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
| 12 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
| 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)` |
| 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)` |

<br><br>

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.

| Code | Identifier | Args and desugaring |
|------|-----------------------|---------------------|
| 1001 | DictContainsFromEntries | `DictContainsFromEntries(dict_st, key_st, value_st) -> ContainsFromEntries(dict_st, key_st, value_st)` |
| 1002 | DictNotContainsFromEntries | `DictNotContainsFromEntries(dict_st, key_st, value_st) -> NotContainsFromEntries(dict_st, key_st, value_st)` |
| 1003 | SetContainsFromEntries | `SetContainsFromEntries(set_st, value_st) -> ContainsFromEntries(set_st, value_st, value_st)` |
| 1004 | SetNotContainsFromEntries | `SetNotContainsFromEntries(set_st, value_st) -> NotContainsFromEntries(set_st, value_st, value_st)` |
| 1005 | ArrayContainsFromEntries | `ArrayContainsFromEntries(array_st, index_st, value_st) -> ContainsFromEntries(array_st, index_st, value_st)` |
| 1006 | GtEqFromEntries | `GtEqFromEntries(s1, s2) -> LtEqFromEntries(s2, s1)` |
| 1007 | GtFromEntries | `GtFromEntries(s1, s2) -> LtFromEntries(s2, s1)` |
| 1008 | GtToNotEqual | `GtToNotEqual(s1, s2) -> LtToNotEqual(s1, s2)` |

<br><br>

Expand Down
81 changes: 17 additions & 64 deletions book/src/statements.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,10 @@ The following table summarises the natively-supported statements, where we write
| 0 | `None` | | no statement, always true (useful for padding) |
| 1 | `False` | | always false (useful for padding disjunctions) |
| 2 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` |
| 3 | `Eq` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
| 4 | `NEq` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
| 5 | `Gt` | `ak1`, `ak2` | `value_of(ak1) > value_of(ak2)` |
| 6 | `LEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
| 3 | `Equal` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
| 4 | `NotEqual` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
| 5 | `LtEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
| 6 | `Lt` | `ak1`, `ak2` | `value_of(ak1) < value_of(ak2)` |
| 7 | `Contains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
| 8 | `NotContains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
| 9 | `SumOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)` |
Expand All @@ -40,68 +40,25 @@ The following table summarises the natively-supported statements, where we write

### Frontend statements

<span style="color:red">TODO: Current implementation frontend Statements reuse the middleware Statements, which:</span><br>
<span style="color:red">- 1: GEq & LEq don't appear in the frontend impl</span><br>
<span style="color:red">- 2: frontend impl has Contains & NotContains, which don't appear at the following block</span>
```
ValueOf(key: AnchoredKey, value: ScalarOrVec)

Equal(ak1: AnchoredKey, ak2: AnchoredKey)

NotEqual(ak1: AnchoredKey, ak2: AnchoredKey)

Gt(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)

Lt(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)

GEq(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)

LEq(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer)

SumOf(sum: AnchoredKey::Integer, arg1: AnchoredKey::Integer, arg2:
AnchoredKey::Integer)

ProductOf(prod: AnchoredKey::Integer, arg1: AnchoredKey::Integer, arg2: AnchoredKey::Integer)

MaxOf(max: AnchoredKey::Integer, arg1: AnchoredKey::Integer, arg2: AnchoredKey::Integer)

HashOf(ak1: AnchoredKey::Raw, arg1: AnchoredKey::Raw, arg2: AnchoredKey::Raw)
```

The following statements relate to Merkle trees and compound types; they are explained in detail on a [separate page](./merklestatements.md).
```
Branches(parent: AnchoredKey::MerkleTree, left: AnchoredKey::MerkleTree, right: AnchoredKey::MerkleTree)
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.

Leaf(node: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)

IsNullTree(node: AnchoredKey::MerkleTree)

GoesLeft(key: AnchoredKey, depth: Value::Integer)

GoesRight(key: AnchoredKey, depth: Value::Integer)

Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)

MerkleSubtree(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree)

MerkleCorrectPath(root: AnchoredKey::MerkleTree, node: AnchoredKey::MerkleTree, key: AnchoredKey, depth: Value::Integer)

Contains(root: AnchoredKey::MerkleTree, key: AnchoredKey, value: AnchoredKey)

NotContains(root: AnchoredKey::MerkleTree, key: AnchoredKey)

ContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)

NotContainsHashedKey(root: AnchoredKey::DictOrSet, key: AnchoredKey)

ContainsValue(root: AnchoredKey::Array, value: AnchoredKey)
```
| Code | Identifier | Args and desugaring |
|------|---------------|---------------------|
| 1000 | DictContains | `DictContains(root, key, val) -> Contains(root, key, val)` |
| 1001 | DictNotContains | `DictNotContains(root, key, val) -> NotContains(root, key, val)` |
| 1002 | SetContains | `SetContains(root, val) -> Contains(root, val, val)` |
| 1003 | SetNotContains | `SetNotContains(root, val) -> Contains(root, val, val)` |
| 1004 | ArrayContains | `ArrayContains(root, idx, val) -> Contains(root, idx, val)` |
| 1005 | GtEq | `GtEq(a, b) -> LtEq(b, a)`|
| 1006 | Gt | `Gt(a, b) -> Lt(b, a)` |


In the future, we may also reserve statement IDs for "precompiles" such as:
```
EcdsaPrivToPubOf(A.pubkey, B.privkey)
EcdsaPrivToPubOf(A.pubkey, B.privkey),
```
as well as for low-level operations on Merkle trees and compound types.
<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.

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

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

##### Primitive Built-in Statements for Merkle Roots

[See separate page](./merklestatements.md).



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