diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md index c9b7f34..bedc54a 100644 --- a/book/src/SUMMARY.md +++ b/book/src/SUMMARY.md @@ -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) diff --git a/book/src/anchoredkeys.md b/book/src/anchoredkeys.md index fcdbb4f..d2fd38d 100644 --- a/book/src/anchoredkeys.md +++ b/book/src/anchoredkeys.md @@ -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]: TODO 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 +``` diff --git a/book/src/architecture.md b/book/src/architecture.md index bb5e8f3..58da789 100644 --- a/book/src/architecture.md +++ b/book/src/architecture.md @@ -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 diff --git a/book/src/custompred.md b/book/src/custompred.md index 4af5c9c..6459f97 100644 --- a/book/src/custompred.md +++ b/book/src/custompred.md @@ -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,
good_boy_issuers: AnchoredKey::MerkleRoot,
receiver: AnchoredKey | ValueOf(?pod["_type"], SIGNATURE),
Contains(?good_boy_issuers, ?pod["_signer"]),
Equals(?pod["friend"], ?receiver) | GoodBoy(?receiver, ?good_boy_issuers) | +| signed_dict: Dict,
signer: PublicKey,
good_boy_issuers: AnchoredKey::MerkleRoot,
receiver: AnchoredKey | SignedBy(?signed_dict, ?signer),
Contains(?good_boy_issuers, ?signer),
Equals(?signed_dict["friend"], ?receiver) | GoodBoy(?receiver, ?good_boy_issuers) | Compiled example with only origins and keys. | Args | Condition | Output | |------------|-----------------------------------------|----| -| pod: Origin,
good_boy_issuers_origin: Origin,
good_boy_issuers_key: Key::MerkleRoot,
receiver_origin: Origin,
receiver_key: Key | ValueOf(pod["_type"]), SIGNATURE),
Contains(?good_boy_issuers_origin[?good_boy_issuers_key], ?pod["_signer"]),
Equals(?pod["friend"], ?receiver_origin[?receiver_key]) | GoodBoy(?receiver_origin[?receiver_key]), ?good_boy_issuers_origin[?good_boy_issuers_key]) | +| signed_dict: Dict,
signer: PublicKey,
good_boy_issuers_origin: Origin,
good_boy_issuers_key: Key::MerkleRoot,
receiver_origin: Origin,
receiver_key: Key | SignedBy(?signed_dict, ?signer),
Contains(?good_boy_issuers_origin[?good_boy_issuers_key], ?signer),
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),
?2 (good_boy_issuers_origin),
?3 (good_boy_issuers_key),
?4 (receiver_origin),
?5 (receiver_key) | ValueOf(?1["_type"]), SIGNATURE),
Contains(?2[?3], ?1["_signer"]),
Equals(?1["friend"], ?4[?5]) | GoodBoy(?4[?5], ?2[?3]) | +| ?1 (signed_dict),
?2 (signer)
?3 (good_boy_issuers_origin),
?4 (good_boy_issuers_key),
?5 (receiver_origin),
?6 (receiver_key) | SignedBy(?1, ?2),
Contains(?3[?4], ?2),
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". diff --git a/book/src/introductionpods.md b/book/src/introductionpods.md index e0f97e8..215652c 100644 --- a/book/src/introductionpods.md +++ b/book/src/introductionpods.md @@ -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`. diff --git a/book/src/operations.md b/book/src/operations.md index 91fa62a..77d5522 100644 --- a/book/src/operations.md +++ b/book/src/operations.md @@ -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)` |

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

@@ -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. diff --git a/book/src/podtypes.md b/book/src/podtypes.md deleted file mode 100644 index cac7ff1..0000000 --- a/book/src/podtypes.md +++ /dev/null @@ -1,4 +0,0 @@ -# POD types - -- SignedPod -- MainPod diff --git a/book/src/signedpod.md b/book/src/signedpod.md deleted file mode 100644 index e32f541..0000000 --- a/book/src/signedpod.md +++ /dev/null @@ -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` - -
- -![](img/SignedPod.png) - - -Example of SignedPod: -```javascript -{ - id: "05f7a6de...", - kvs : { - _signerKey: "5e1c0b3c...", - idNumber: "94e328a7...", - dateOfBirth: 1169909384, - socialSecurityNum: "1111" - }, - signature: "68b615f7..." -} -``` diff --git a/book/src/simpleexample.md b/book/src/simpleexample.md index ee25230..840823d 100644 --- a/book/src/simpleexample.md +++ b/book/src/simpleexample.md @@ -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]) diff --git a/book/src/statements.md b/book/src/statements.md index e9003ef..d52c00e 100644 --- a/book/src/statements.md +++ b/book/src/statements.md @@ -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. -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 -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]: TODO List of built-in statements is not yet complete. - -[^fillsum]: TODO Does sum mean x+y = z or x = y+z?