From 5d13ac32ceaa5a9373767ca1b4a0354d9c34b899 Mon Sep 17 00:00:00 2001 From: tideofwords Date: Mon, 2 Jun 2025 17:49:33 -0700 Subject: [PATCH] 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 * Eq -> Equal Co-authored-by: Ahmad Afuni * Eq -> Equal, again Co-authored-by: Ahmad Afuni * Eq -> Equal, yet again Co-authored-by: Ahmad Afuni --------- Co-authored-by: Ahmad Afuni --- book/src/SUMMARY.md | 1 - book/src/merklestatements.md | 30 +++++++++++++ book/src/operations.md | 41 +++++++++++------- book/src/statements.md | 81 ++++++++---------------------------- 4 files changed, 73 insertions(+), 80 deletions(-) diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index 6d0360d..52291ae 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -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) diff --git a/book/src/merklestatements.md b/book/src/merklestatements.md index 9cce717..5329702 100644 --- a/book/src/merklestatements.md +++ b/book/src/merklestatements.md @@ -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 diff --git a/book/src/operations.md b/book/src/operations.md index 6faa16e..78149ce 100644 --- a/book/src/operations.md +++ b/book/src/operations.md @@ -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)` | +| 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)` | - +

+ +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)` |

diff --git a/book/src/statements.md b/book/src/statements.md index db09873..9b9252c 100644 --- a/book/src/statements.md +++ b/book/src/statements.md @@ -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)` | @@ -40,68 +40,25 @@ The following table summarises the natively-supported statements, where we write ### Frontend statements -TODO: Current implementation frontend Statements reuse the middleware Statements, which:
-- 1: GEq & LEq don't appear in the frontend impl
-- 2: frontend impl has Contains & NotContains, which don't appear at the following block -``` -ValueOf(key: AnchoredKey, value: ScalarOrVec) +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. -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) - -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. +NOTE 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 @@ -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]: TODO List of built-in statements is not yet complete.