ed255/pod2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

update docs (#242)

Browse source 
* 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>
This commit is contained in:
tideofwords 2025-06-02 17:49:33 -07:00 • committed by GitHub
parent 88a75986b8
commit 5d13ac32ce
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 73 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

1
book/src/SUMMARY.md
View file

@ -13,7 +13,6 @@
- [Signature](./signature.md) - [Signature](./signature.md)
- [Deductions](./deductions.md) - [Deductions](./deductions.md)
- [Statements](./statements.md) - [Statements](./statements.md)
- [Statements involving compound types and Merkle trees](./merklestatements.md)
- [Operations](./operations.md) - [Operations](./operations.md)
- [Simple example](./simpleexample.md) - [Simple example](./simpleexample.md)
- [Custom statements and custom operations](./custom.md) - [Custom statements and custom operations](./custom.md)

30
book/src/merklestatements.md
View file

@ -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 # Statements involving compound types and Merkle trees
The front end has three compound types The front end has three compound types

41
book/src/operations.md
View file

@ -10,22 +10,33 @@ The following table summarises the natively-supported operations:
| 0 | `None` | | | `None` | | 0 | `None` | | | `None` |
| 1 | `NewEntry`[^newentry] | `(key, value)` | | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 | | 1 | `NewEntry`[^newentry] | `(key, value)` | | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 |
| 2 | `CopyStatement` | `s` | | | | 2 | `CopyStatement` | `s` | | |
| 3 | `EntryEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Eq(ak1, ak2)` | | 3 | `EqualFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = value2` | `Equal(ak1, ak2)` |
| 4 | `EntryNEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NEq(ak1, ak2)` | | 4 | `NotEqualFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 != value2` | `NotEqual(ak1, ak2)` |
| 5 | `EntryGt` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 > value2` | `Gt(ak1, ak2)` | | 5 | `LtEqFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LtEq(ak1, ak2)` |
| 6 | `EntryLEq` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 <= value2` | `LEq(ak1, ak2)` | | 6 | `LtFromEntries` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 < value2` | `Lt(ak1, ak2)` |
| 7 | `TransitiveEq` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Eq(ak1, ak4)` | | 7 | `TransitiveEqualFromStatements` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Equal(ak1, ak4)` |
| 8 | `GtToNEq` | `s` | `s = Gt(ak1, ak2)` | `NEq(ak1, ak2)` | | 8 | `LtToNotEqual` | `s` | `s = Lt(ak1, ak2)` | `NotEqual(ak1, ak2)` |
| 9 | `LtToNEq` | `s` | `s = Lt(ak1, ak2)` | `NEq(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 | `EntryContains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_includes(value1, value2, proof) = true` | `Contains(ak1, ak2)` | | 10 | `NotContainsFromEntries` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `NotContains(ak1, ak2)` |
| 11 | `EntrySintains` | `s1`, `s2`, `proof` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `merkle_excludes(value1, value2, proof) = true` | `Sintains(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 | `RenameContains` | `s1`, `s2` | `s1 = Contains(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak1 = ak3` | `Contains(ak4, ak2)` | | 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 | `SumOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 + value3` | `SumOf(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 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `s3 = ValueOf(ak3, value3)`, `value1 = value2 * value3` | `ProductOf(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)` |
| 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` --> <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> <br><br>

81
book/src/statements.md
View file

@ -27,10 +27,10 @@ The following table summarises the natively-supported statements, where we write
| 0 | `None` | | no statement, always true (useful for padding) | | 0 | `None` | | no statement, always true (useful for padding) |
| 1 | `False` | | always false (useful for padding disjunctions) | | 1 | `False` | | always false (useful for padding disjunctions) |
| 2 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` | | 2 | `ValueOf` | `ak`, `value` | `value_of(ak) = value` |
| 3 | `Eq` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` | | 3 | `Equal` | `ak1`, `ak2` | `value_of(ak1) = value_of(ak2)` |
| 4 | `NEq` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` | | 4 | `NotEqual` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
| 5 | `Gt` | `ak1`, `ak2` | `value_of(ak1) > value_of(ak2)` | | 5 | `LtEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
| 6 | `LEq` | `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) | | 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) | | 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)` | | 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
### Frontend statements ### Frontend statements
<span style="color:red">TODO: Current implementation frontend Statements reuse the middleware Statements, which:</span><br> 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.
<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) | Code | Identifier | Args and desugaring |
|------|---------------|---------------------|
NotEqual(ak1: AnchoredKey, ak2: AnchoredKey) | 1000 | DictContains | `DictContains(root, key, val) -> Contains(root, key, val)` |
| 1001 | DictNotContains | `DictNotContains(root, key, val) -> NotContains(root, key, val)` |
Gt(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer) | 1002 | SetContains | `SetContains(root, val) -> Contains(root, val, val)` |
| 1003 | SetNotContains | `SetNotContains(root, val) -> Contains(root, val, val)` |
Lt(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer) | 1004 | ArrayContains | `ArrayContains(root, idx, val) -> Contains(root, idx, val)` |
| 1005 | GtEq | `GtEq(a, b) -> LtEq(b, a)`|
GEq(ak1: AnchoredKey::Integer, ak2: AnchoredKey::Integer) | 1006 | Gt | `Gt(a, b) -> Lt(b, a)` |
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)
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)
```
In the future, we may also reserve statement IDs for "precompiles" such as: 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 ### Built-in statements for entries of any type
@ -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) 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. [^builtin]: <font color="red">TODO</font> List of built-in statements is not yet complete.