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

update docs with no-pod-id (#403)

Browse source 
* update docs with no-pod-id

* Update book/src/anchoredkeys.md

Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>

* Update book/src/custompred.md

Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>

* Update book/src/statements.md

Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>

* Update book/src/statements.md

Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>

---------

Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>
This commit is contained in:
Eduard S. 2025-09-02 13:34:19 +02:00 • committed by GitHub
parent 511efa8d44
commit ca97d9edc4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 97 additions and 131 deletions
Download patch file Download diff file Expand all files Collapse all files

4
book/src/SUMMARY.md
View file

@ -19,9 +19,7 @@
- [Defining custom predicates](./custompred.md)
- [Custom statement example](./customexample.md)
- [How to hash a custom statement](./customhash.md)
- [POD types](./podtypes.md)
- [SignedPOD](./signedpod.md)
- [MainPOD](./mainpod.md)
- [MainPOD](./mainpod.md)
- [Introduction PODs](./introductionpods.md)
- [Examples](./examples.md)

31
book/src/anchoredkeys.md
View file

@ -1,24 +1,21 @@
# Anchored keys
Rather than dealing with just keys, we introduce the notion of an *anchored key*, which is a pair consisting of an origin specifier and a key, i.e.
Rather than dealing with just keys, we introduce the notion of an *anchored key*, which is a pair consisting of an dictionary specifier and a key, i.e.
```
type AnchoredKey = (Origin, Key)
type AnchoredKey = (Dict, Key)
type Key = String
```
FIXME: This description is incorrect. We don't have *gadget ID*. And we don't think of *origin* as a triple, we just see it as a single value that encodes the *pod ID* or SELF.
Statements can use anchored keys or literal values as arguments. Since our
system uses constructive logic, if a statement that uses an anchored key in
some of its arguments is proved, it means that a valid Merkle proof of the
value behind it exists and was used at some point to construct a `Contains`
statement that introduced that anchored key.
An *origin* is a triple consisting of a numeric identifier called the *origin ID*, a string called the *origin name* (omitted in the backend) and another numeric identifier called the *gadget ID*, which identifies the means by which the value corresponding to a given key is produced.
The origin ID is defined to be 0 for 'no origin' and 1 for 'self origin', otherwise it is the content ID[^content-id] of the POD to which it refers. The origin name is not cryptographically significant and is merely a convenience for the frontend.
The gadget ID takes on the values in the following table:
| Gadget ID | Meaning |
|-----------|-------------------------------------------------------------------------------------------|
| 0 | no gadget |
| 1 | `SignedPOD` gadget: The key-value pair was produced in the construction of a `SignedPOD`. |
| 2 | `MainPOD` gadget: The key-value pair was produced in the construction of a `MainPOD`. |
For example, a gadget ID of 1 implies that the key-value pair in question was produced in the process of constructing a `SignedPOD`.
[^content-id]: <font color="red">TODO</font> Refer to this when it is documented.
For example:
```
0: None
1: Contains(foo, bar, 42) <- ContainsFromEntries 0 0 0 mt_proof
2: Lt(foo[bar], 100) <- LtFromEntries 1 0
3: NotEqual(foo[bar], 100) <- LtToNotEqual 2
```

2
book/src/architecture.md
View file

@ -5,7 +5,7 @@ This document explains the architecture of the current implementation.
The main logic of the POD2 implementation is divided into three modules:
- frontend
- compiles user-friendly pod declarations into intermediate representations to be consumed by the backend
- internally connects to the backend to get pods built (signed / proved).
- internally connects to the backend to get pods built (proved).
- presents pods to the user
- middleware
- defines the intermediate representation of Statements, Operations and interfaces of PODs

22
book/src/custompred.md
View file

@ -11,19 +11,19 @@ The syntax of a custom operation is best explained with an example.
Original example with anchored keys, origins, and keys.
| Args | Condition | Output |
|------------|-----------------------------------------|----|
| pod: Origin, <br> good_boy_issuers: AnchoredKey::MerkleRoot, <br> receiver: AnchoredKey | ValueOf(?pod["_type"], SIGNATURE), <br> Contains(?good_boy_issuers, ?pod["_signer"]), <br> Equals(?pod["friend"], ?receiver) | GoodBoy(?receiver, ?good_boy_issuers) |
| signed_dict: Dict, <br> signer: PublicKey, <br> good_boy_issuers: AnchoredKey::MerkleRoot, <br> receiver: AnchoredKey | SignedBy(?signed_dict, ?signer), <br> Contains(?good_boy_issuers, ?signer), <br> Equals(?signed_dict["friend"], ?receiver) | GoodBoy(?receiver, ?good_boy_issuers) |
Compiled example with only origins and keys.
| Args | Condition | Output |
|------------|-----------------------------------------|----|
| pod: Origin, <br> good_boy_issuers_origin: Origin, <br> good_boy_issuers_key: Key::MerkleRoot, <br> receiver_origin: Origin, <br> receiver_key: Key | ValueOf(pod["_type"]), SIGNATURE), <br> Contains(?good_boy_issuers_origin[?good_boy_issuers_key], ?pod["_signer"]), <br> Equals(?pod["friend"], ?receiver_origin[?receiver_key]) | GoodBoy(?receiver_origin[?receiver_key]), ?good_boy_issuers_origin[?good_boy_issuers_key]) |
| signed_dict: Dict, <br> signer: PublicKey, <br> good_boy_issuers_origin: Origin, <br> good_boy_issuers_key: Key::MerkleRoot, <br> receiver_origin: Origin, <br> receiver_key: Key | SignedBy(?signed_dict, ?signer), <br> Contains(?good_boy_issuers_origin[?good_boy_issuers_key], ?signer), <br> Equals(?signed_dict["friend"], ?receiver_origin[?receiver_key]) | GoodBoy(?receiver_origin[?receiver_key]), ?good_boy_issuers_origin[?good_boy_issuers_key]) |
A custom operation accepts as input a number of statements (the `Condition`);
each statement has a number of arguments, which may be constants or anchored keys; and an [anchored key](./anchoredkeys.md) in turn can optionally be decomposed as a pair of an Origin and a Key.
each statement has a number of arguments, which may be constants or anchored keys; and an [anchored key](./anchoredkeys.md) in turn can optionally be decomposed as a pair of a Dict and a Key.
In the "original example" above, the anchored keys `good_boy_issuers` and `receiver` are not broken down, but `?pod["_type"], ?pod["_signer"], pod["friend"]` are. The purpose of breaking them down, in this case, is to force the three anchored keys to come from the same pod.
In the "original example" above, the anchored keys `good_boy_issuers` and `receiver` are not broken down, but `?signed_dict["friend"]` is. The purpose of breaking it down, in this case, is to use an entry of a dictionary that has been signed.
In the "compiled example", all the anchored keys have been broken down into origins and keys.
In the "compiled example", all the anchored keys have been broken down into dictionaries and keys.
In general, in the front-end language, the "arguments" to an operation define a list of identifiers with types. Every statement in the "condition" must have valid arguments of the correct types: either constants, or identifiers defined in the "arguments".
@ -35,18 +35,18 @@ On the back end the "compiled example" deduction rule is converted to a sort of
| Args | Condition | Output |
|------------|-----------------------------------------|----|
| ?1 (pod), <br> ?2 (good_boy_issuers_origin), <br> ?3 (good_boy_issuers_key), <br> ?4 (receiver_origin), <br> ?5 (receiver_key) | ValueOf(?1["_type"]), SIGNATURE), <br> Contains(?2[?3], ?1["_signer"]), <br> Equals(?1["friend"], ?4[?5]) | GoodBoy(?4[?5], ?2[?3]) |
| ?1 (signed_dict), <br> ?2 (signer) <br> ?3 (good_boy_issuers_origin), <br> ?4 (good_boy_issuers_key), <br> ?5 (receiver_origin), <br> ?6 (receiver_key) | SignedBy(?1, ?2), <br> Contains(?3[?4], ?2), <br> Equals(?1["friend"], ?5[?6]) | GoodBoy(?5[?6], ?3[?4]) |
If you want to apply this deduction rule to prove a `GoodBoy` statement,
you have to provide the following witnesses in-circuit.
- Copy of the deduction rule
- Values for ?1, ?2, ?3, ?4, ?5.
- Copy of the three statements in the deduction rule with ?1, ?2, ?3, ?4, ?5 filled in
- Indices of the three statements `ValueOf`, `Contains`, `Equals` in the list of previous statements.
- Values for ?1, ?2, ?3, ?4, ?5, ?6.
- Copy of the three statements in the deduction rule with ?1, ?2, ?3, ?4, ?5, ?6 filled in
- Indices of the three statements `SignedBy`, `Contains`, `Equals` in the list of previous statements.
And the circuit will verify:
- ?1, ?2, ?3, ?4, ?5 were correctly substituted into the statements
- The three statements `ValueOf`, `Contains`, `Equals` do indeed appear at the claimed indices.
- ?1, ?2, ?3, ?4, ?5, ?6 were correctly substituted into the statements
- The three statements `SignedBy`, `Contains`, `Equals` do indeed appear at the claimed indices.
[^operation]: In previous versions of these docs, "operations" were called "deduction rules".

12
book/src/introductionpods.md
View file

@ -23,11 +23,15 @@ a GitHub account).
### Interface
The interface of a `IntroductionPod` is just the one of the
[RecursivePod](https://github.com/0xPARC/pod2/tree/3ea0d5be71ce98971305076b220079a1b2b7a8d0/src/middleware/mod.rs#L823)
trait, together with matching the expected `vds_root` of the used `VDSet` in the
`MainPod`, and using the same circuit configuration for the proof verification.
[Pod](https://github.com/0xPARC/pod2/blob/511efa8d4477a0d936bd898a484e3b41454b1991/src/middleware/mod.rs#L901)
trait, and by definition the `IntroductionPod` is expected to only output
Introduction statements (or None statements for padding).
This means that as long as we fit into the `RecursivePod` interface, the
An Introduction Statement is a Statement that uses an Introduction predicate
which embeds the verifying key of the circuit that generates it. This way the
statements generated by an `IntroductionPod` are self-describing.
This means that as long as we fit into the `Pod` interface, the
`IntroductionPod` will fit into the recursive verification chain of the
`MainPods`.

52
book/src/operations.md
View file

@ -8,21 +8,24 @@ The following table summarises the natively-supported operations:
| Code | Identifier | Args | Condition | Output |
|------|-----------------------|---------------------|-----------------------------------------------------------------------------------------------------------------------|----------------------------------------------------------------|
| 0 | `None` | | | `None` |
| 1 | `NewEntry`[^newentry] | `(key, value)` | | `ValueOf(ak, value)`, where `ak` has key `key` and origin ID 1 |
| 2 | `CopyStatement` | `s` | | |
| 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)` |
| 15 | `PublicKeyOf` | `s1`, `s2` | `s1 = ValueOf(ak1, value1)`, `s2 = ValueOf(ak2, value2)`, `value1 = derive_public_key(value2)` | `PublicKeyOf(ak1, ak2)` |
| 1 | `CopyStatement` | `s` | | |
| 2 | `EqualFromEntries` | `s1`, `s2` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `value1 = value2` | `Equal(ak1, ak2)` |
| 3 | `NotEqualFromEntries` | `s1`, `s2` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `value1 != value2` | `NotEqual(ak1, ak2)` |
| 4 | `LtEqFromEntries` | `s1`, `s2` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `value1 <= value2` | `LtEq(ak1, ak2)` |
| 5 | `LtFromEntries` | `s1`, `s2` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `value1 < value2` | `Lt(ak1, ak2)` |
| 6 | `TransitiveEqualFromStatements` | `s1`, `s2` | `s1 = Equal(ak1, ak2)`, `s2 = Equal(ak3, ak4)`, `ak2 = ak3` | `Equal(ak1, ak4)` |
| 7 | `LtToNotEqual` | `s` | `s = Lt(ak1, ak2)` | `NotEqual(ak1, ak2)` |
| 8 | `ContainsFromEntries` | `s1`, `s2`, `s3`, `proof` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `merkle_includes(value1, value2, value3, proof) = true` | `Contains(ak1, ak2, ak3)` |
| 9 | `NotContainsFromEntries` | `s1`, `s2`, `proof` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `merkle_excludes(value1, value2, proof) = true` | `NotContains(ak1, ak2)` |
| 10 | `SumOf` | `s1`, `s2`, `s3` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `value1 = value2 + value3` | `SumOf(ak1, ak2, ak3)` |
| 11 | `ProductOf` | `s1`, `s2`, `s3` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `value1 = value2 * value3` | `ProductOf(ak1, ak2, ak3)` |
| 12 | `MaxOf` | `s1`, `s2`, `s3` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `value1 = max(value2, value3)` | `MaxOf(ak1, ak2, ak3)` |
| 13 | `HashOf` | `s1`, `s2`, `s3` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `value1 = hash(value2, value3)`| `HashOf(ak1, ak2, ak3)` |
| 14 | `PublicKeyOf` | `s1`, `s2` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `value1 = derive_public_key(value2)` | `PublicKeyOf(ak1, ak2)` |
| 15 | `SignedBy` | `s1`, `s2`, `sig` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `verify_signature(msg: value1, pk: value2, sig) = true` | `SignedBy(ak1, ak2)` |
| 16 | `ContainerInsertFromEntries` | `s1`, `s2`, `s3`, `s4`, `proof` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `s4 = Contains(ak4..., value4)`, `merkle_insert(value1, value2, value3, value4, proof) = true` | `ContainerInsert(ak1, ak2, ak3, ak4)` |
| 17 | `ContainerUpdateFromEntries` | `s1`, `s2`, `s3`, `s4`, `proof` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `s4 = Contains(ak4..., value4)`, `merkle_update(value1, value2, value3, value4, proof) = true` | `ContainerUpdate(ak1, ak2, ak3, ak4)` |
| 18 | `ContainerDeleteFromEntries` | `s1`, `s2`, `s3`, `proof` | `s1 = Contains(ak1..., value1)`, `s2 = Contains(ak2..., value2)`, `s3 = Contains(ak3..., value3)`, `merkle_delete(value1, value2, value3, proof) = true` | `ContainerDelete(ak1, ak2, ak3, ak4)` |
<br><br>
@ -30,14 +33,20 @@ The following table summarizes "syntactic sugar" operations. These operations a
| 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)` |
| 1001 | DictContainsFromEntries | `DictContainsFromEntries(dict_st, key_st, value_st, proof_st) -> ContainsFromEntries(dict_st, key_st, value_st, proof_st)` |
| 1002 | DictNotContainsFromEntries | `DictNotContainsFromEntries(dict_st, key_st, value_st, proof_st) -> NotContainsFromEntries(dict_st, key_st, value_st, proof_st)` |
| 1003 | SetContainsFromEntries | `SetContainsFromEntries(set_st, value_st, proof_st) -> ContainsFromEntries(set_st, value_st, value_st, proof_st)` |
| 1004 | SetNotContainsFromEntries | `SetNotContainsFromEntries(set_st, value_st, proof_st) -> NotContainsFromEntries(set_st, value_st, value_st, proof_st)` |
| 1005 | ArrayContainsFromEntries | `ArrayContainsFromEntries(array_st, index_st, value_st, proof_st) -> ContainsFromEntries(array_st, index_st, value_st, proof_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)` |
| 1009 | DictInsertFromEntries | `DictInsertFromEntries(new_dict_st, old_dict_st, key_st, value_st, proof) -> ContainerInsertFromEntries(new_dict_st, old_dict_st, key_st, value_st, proof)` |
| 1010 | DictUpdateFromEntries | `DictInsertUpdateEntries(new_dict_st, old_dict_st, key_st, value_st, proof) -> ContainerUpdateFromEntries(new_dict_st, old_dict_st, key_st, value_st, proof)` |
| 1011 | DictDeleteFromEntries | `DictInsertDeleteEntries(new_dict_st, old_dict_st, key_st, proof) -> ContainerDeleteFromEntries(new_dict_st, old_dict_st, key_st, value_st, proof)` |
| 1009 | SetInsertFromEntries | `SetInsertFromEntries(new_set_st, old_set_st, value_st, proof) -> ContainerInsertFromEntries(new_set_st, old_set_st, value_st, value_st, proof)` |
| 1011 | SetDeleteFromEntries | `SetInsertDeleteEntries(new_set_st, old_set_st, value_st, proof) -> ContainerDeleteFromEntries(new_set_st, old_set_st, value_st, value_st, proof)` |
| 1010 | ArrayUpdateFromEntries | `ArrayInsertUpdateEntries(new_array_st, old_array_st, index_st, value_st, proof) -> ContainerUpdateFromEntries(new_array_st, old_array_st, index_st, value_st, proof)` |
<br><br>
@ -53,6 +62,3 @@ Issue keeping track of the operations: [#108](https://github.com/0xPARC/pod2/iss
| | `TransitiveGt` | `s1`, `s2` | `s1 = Gt(ak1, ak2)`, `s2 = Gt(ak3, ak4)`, `ak2 = ak3` | `Gt(ak1, ak4)` |
| | `TransitiveLEq` | `s1`, `s2` | `s1 = LEq(ak1, ak2)`, `s2 = LEq(ak3, ak4)`, `ak2 = ak3` | `LEq(ak1, ak4)` |
| | `LEqToNEq` | `s` | `s = LEq(ak1, ak2)` | `NEq(ak1, ak2)` |
[^newentry]: Since new key-value pairs are not constrained, this operation will have no arguments in-circuit.

4
book/src/podtypes.md
View file

@ -1,4 +0,0 @@
# POD types
- SignedPod
- MainPod

29
book/src/signedpod.md
View file

@ -1,29 +0,0 @@
# SignedPod
A SignedPod consists of the following fields:
- `mt`: key-values storage, internally it's a [MerkleTree](./merkletree.md) so that we can generate proofs on the key-values
- it can only contain [`ValueOf` statements](./statements.md).
- the Signer's public key is one of the key-values in the `kvs`.
- `id`: the Root of the `kvs` MerkleTree
- `signature`: a [signature](./signature.md) over the `id`
- `signer`: the public key attached to the digital signature `signature`
- `type`: the constant `SIGNATURE`
<br>
![](img/SignedPod.png)
Example of SignedPod:
```javascript
{
id: "05f7a6de...",
kvs : {
_signerKey: "5e1c0b3c...",
idNumber: "94e328a7...",
dateOfBirth: 1169909384,
socialSecurityNum: "1111"
},
signature: "68b615f7..."
}
```

42
book/src/simpleexample.md
View file

@ -23,11 +23,11 @@ The reason is everything the circuit needs to verify that the statement is true.
Example:
```
STATEMENT1 = Equals(oldpod["name"], otherpod["field"])
STATEMENT1 = Equals(olddict["name"], otherdict["field"])
STATEMENT2 = Equals(otherpod["field"], newpod["result"])
STATEMENT2 = Equals(otherdict["field"], newdict["result"])
STATEMENT3 = Equals(oldpod["name"], newpod["result"])
STATEMENT3 = Equals(olddict["name"], newdict["result"])
```
The reasons in human-readable simplified format:
@ -56,7 +56,7 @@ then
Equals(a, c)
```
First, we need to decompose all the anchored keys as (key, origin) pairs. This is the frontend description of the deduction rule.
First, we need to decompose all the anchored keys as (dict, key) pairs. This is the frontend description of the deduction rule.
```
IF
Equals(a_or[a_key], b_or[b_key)
@ -86,18 +86,18 @@ Equals( ?1[?2], ?5[?6] )
```
- Say what the wildcards are
```
?1 -- oldpod
?1 -- olddict
?2 -- "name"
?3 -- otherpod
?3 -- otherdict
...
```
- Substitute the wildcards into the deduction rule
```
IF
Equals( oldpod["name"], ... ) ...
Equals( otherpod["value"])
Equals( olddict["name"], ... ) ...
Equals( otherdict["value"])
THEN
Equals( oldpod["name"] newpod[...] )
Equals( olddict["name"] newdict[...] )
...
```
- Say where to find the previous statements (indices in the list), and check that they are above this one.
@ -111,20 +111,17 @@ Statement2
## Decomposing anchored keys
Sometimes a deduction rule requires different anchored keys to come from the same POD. Here's an example from Ethdos.
Sometimes a deduction rule requires different anchored keys to come from the same dictionary. Here's an example from Ethdos.
The wildcard system handles this very naturally, since origin ID and key are two separate wildcards.
The wildcard system handles this very naturally, since the dict of the anchored key can use its own wildcard.
```
eth_friend(src_or, src_key, dst_or, dst_key) = and<
// there is an attestation pod that's a SIGNATURE POD
ValueOf(?attestation_pod["type"], SIGNATURE)
// the attestation pod is signed by (src_or, src_key)
Equal(?attestation_pod["signer"], ?src_or[?src_key])
// the attestation dict is signed by (src_or, src_key)
SignedBy(?attestation_dict, ?src_or[?src_key])
// that same attestation pod has an "attestation"
Equal(?attestation_pod["attestation"], ?dst_or[?dst_key])
Equal(?attestation_dict["attestation"], ?dst_or[?dst_key])
>
```
@ -132,9 +129,7 @@ In terms of anchored keys, it would be a little more complicated. five anchored
```
AK1 = src
AK2 = dst
AK3 = attestation_pod["type"]
AK4 = attestation_pod["signer"]
AK5 = attestation_pod["attestation"]
AK3 = attestation_dict["attestation"]
```
and we need to force AK3, AK4, AK5 to come from the same origin.
@ -143,11 +138,8 @@ WILDCARD matching takes care of it.
```
eth_friend(?1, ?2, ?3, ?4) = and<
// there is an attestation pod that's a SIGNATURE POD
ValueOf(?5["type"], SIGNATURE)
// the attestation pod is signed by ?src_or[?src_key]
Equal(?5["signer"], ?1[?2])
// the attestation dict is signed by (src_or, src_key)
SignedBy(?5, ?1[?2])
// that same attestation pod has an "attestation"
Equal(?5["attestation"], ?3[?4])

30
book/src/statements.md
View file

@ -30,13 +30,17 @@ The following table summarises the natively-supported statements, where we write
| 3 | `NotEqual` | `ak1`, `ak2` | `value_of(ak1) != value_of(ak2)` |
| 4 | `LtEq` | `ak1`, `ak2` | `value_of(ak1) <= value_of(ak2)` |
| 5 | `Lt` | `ak1`, `ak2` | `value_of(ak1) < value_of(ak2)` |
| 6 | `Contains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∈ value_of(ak1)` (Merkle inclusion) |
| 7 | `NotContains` | `ak1`, `ak2` | `(key_of(ak2), value_of(ak2)) ∉ value_of(ak1)` (Merkle exclusion) |
| 6 | `Contains` | `ak1`, `ak2`, `ak3` | `(value_of(ak2), value_of(ak3)) ∈ value_of(ak1)` (Merkle inclusion) |
| 7 | `NotContains` | `ak1`, `ak2` | `(value_of(ak2), _) ∉ value_of(ak1)` (Merkle exclusion) |
| 8 | `SumOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) + value_of(ak3)` |
| 9 | `ProductOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = value_of(ak2) * value_of(ak3)` |
| 10 | `MaxOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = max(value_of(ak2), value_of(ak3))` |
| 11 | `HashOf` | `ak1`, `ak2`, `ak3` | `value_of(ak1) = hash(value_of(ak2), value_of(ak3))` |
| 12 | `PublicKeyOf` | `ak1`, `ak2` | `value_of(ak1) = derive_public_key(value_of(ak2))` |
| 13 | `SignedBy` | `ak1`, `ak2` | `value_of(ak1)` is signed by `value_of(ak2)` |
| 14 | `ContainerInsert` | `ak1`, `ak2`, `ak3`, `ak4` | `(value_of(ak3), _) ∉ value_of(ak2) ∧ value_of(ak1) = value_of(ak2) ∪ {(value_of(ak3), value_of(ak4))}` (Merkle insert) |
| 15 | `ContainerUpdate` | `ak1`, `ak2`, `ak3`, `ak4` | `(value_of(ak3), v) ∈ value_of(ak2) ∧ value_of(ak1) = (value_of(ak2) - {(value_of(ak3), v)}) ∪ {(value_of(ak3), value_of(ak4))}` (Merkle update) |
| 16 | `ContainerDelete` | `ak1`, `ak2`, `ak3` | `(value_of(ak3), v) ∈ value_of(ak2) ∧ value_of(ak1) = value_of(ak2) - {(value_of(ak3), v)}` (Merkle delete) |
### Frontend statements
@ -51,21 +55,21 @@ The frontend also exposes the following syntactic sugar predicates. These predi
| 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)` |
| 1009 | DictInsert | `DictInsert(new_root, old_root, key, val) -> ContainerInsert(new_root, old_root, key, val)` |
| 1010 | DictUpdate | `DictUpdate(new_root, old_root, key, val) -> ContainerUpdate(new_root, old_root, key, val)` |
| 1011 | DictDelete | `DictDelete(new_root, old_root, key) -> ContainerDelete(new_root, old_root, key)` |
| 1012 | SetInsert | `SetInsert(new_root, old_root, val) -> ContainerInsert(new_root, old_root, val, val)` |
| 1013 | SetDelete | `SetDelete(new_root, old_root, val) -> ContainerDelete(new_root, old_root, val)` |
| 1014 | ArrayUpdate | `ArrayUpdate(new_root, old_root, idx, val) -> ContainerUpdate(new_root, old_root, idx, val)` |
In the future, we may also reserve statement IDs for "precompiles" such as:
```
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
A ```ValueOf``` statement asserts that an entry has a certain value.
A ```DictContains``` statement asserts that an entry has a certain value.
```
ValueOf(A["name"], "Arthur")
DictContains(A, "name", "Arthur")
```
Implies that the entry `A["name"]` exists with the value `"Arthur"`.
An ```Equal``` statement asserts that two entries have the same value. (Technical note: The circuit only proves equality of field elements; no type checking is performed. For strings or Merkle roots, collision-resistance of the hash gives a cryptographic guarantee of equality. However, note both Arrays and Sets are implemented as dictionaries in the backend; the backend cannot type-check, so it is possible to prove an equality between an Array or Set and a Dictionary.)
```
@ -87,7 +91,7 @@ Gt(A["price"], B["balance"])
The statements ```Lt```, ```GEq```, ```Leq``` are defined analogously.
```SumOf(x, y, z)``` asserts that ```x```, ```y```, ```z``` are entries of type ```Integer```, and [^fillsum]
```SumOf(x, y, z)``` asserts that ```x```, ```y```, ```z``` are entries of type ```Integer```, and ```x = y + z```
```ProductOf``` and ```MaxOf``` are defined analogously.
@ -103,5 +107,3 @@ ecdsa_priv_to_pub_of(A["pubkey"], B["privkey"])
[^builtin]: <font color="red">TODO</font> List of built-in statements is not yet complete.
[^fillsum]: <font color="red">TODO</font> Does sum mean x+y = z or x = y+z?