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

update docs to use pod lang v1 (#268)

Browse source
This commit is contained in:
Eduard S. 2025-06-10 15:08:45 +02:00 • committed by GitHub
parent 6feff2ae69
commit 6258e52e1a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 185 additions and 177 deletions
Download patch file Download diff file Expand all files Collapse all files

4
book/src/custom.md
View file

@ -14,7 +14,7 @@ On the backend, custom predicates are defined in _groups_. A group can contain
The definition of a custom predicate might also be called an _operation_ or _deduction rule_. It includes two (or, potentially, say, five) statement templates as conditions. The arguments to the statement templates are decomposed as (origin, key) pairs: if statements are allowed to have arity at most 4, then the statement templates in a deduction rule will have at most 8 arguments (4 origins and 4 keys). The same holds for the output statement. The definition of a custom predicate might also be called an _operation_ or _deduction rule_. It includes two (or, potentially, say, five) statement templates as conditions. The arguments to the statement templates are decomposed as (origin, key) pairs: if statements are allowed to have arity at most 4, then the statement templates in a deduction rule will have at most 8 arguments (4 origins and 4 keys). The same holds for the output statement.
Each argument (origin or key) to an statement template is either a wildcard or a literal. In the backend, the wildcard arguments will be identified as *1, *2, *3, .... Each argument (origin or key) to an statement template is either a wildcard or a literal. In the backend, the wildcard arguments will be identified as ?1, ?2, ?3, ....
## Examples ## Examples
@ -32,7 +32,7 @@ For a custom statement, the "reason" includes the following witnesses and verifi
- the definition of the statement, serialized (see [examples](./customexample.md)) - the definition of the statement, serialized (see [examples](./customexample.md))
- if the statement is part of a group, the definition of the full group, serialized - if the statement is part of a group, the definition of the full group, serialized
- verify that the hash of the definition is the statement ID - verify that the hash of the definition is the statement ID
- the definition will have some number of "wildcards" (*1, *2, ...) as arguments to statement templates; a value for each wildcard must be provided as a witness (each will be either an origin ID or key) - the definition will have some number of "wildcards" (?1, ?2, ...) as arguments to statement templates; a value for each wildcard must be provided as a witness (each will be either an origin ID or key)
- the circuit must substitute the claimed values for the wildcards, and the resulting statements (true statements with origins and keys) will appear as witnesses - the circuit must substitute the claimed values for the wildcards, and the resulting statements (true statements with origins and keys) will appear as witnesses
- the circuit must verify that all the input statement templates (with origins and keys) appear in the previous statements (in higher rows of the table) - the circuit must verify that all the input statement templates (with origins and keys) appear in the previous statements (in higher rows of the table)
- the circuit also substitutes the claimed values for the wildcards in the output statement, and verifies that it matches the claimed output statement - the circuit also substitutes the claimed values for the wildcards in the output statement, and verifies that it matches the claimed output statement

41
book/src/customexample.md
View file

@ -2,27 +2,26 @@
# Ethdos custom predicate, using binary AND and OR: example of a recursive group # Ethdos custom predicate, using binary AND and OR: example of a recursive group
``` ```
eth_dos_distance(src_or, src_key, dst_or, dst_key, distance_or, distance_key) = or< eth_dos_distance(src_or, src_key, dst_or, dst_key, distance_or, distance_key) = OR(
eth_dos_distance_ind_0(src_or, src_key, dst_or, dst_key, distance_or, distance_key), eth_dos_distance_ind_0(?src_or, ?src_key, ?dst_or, ?dst_key, ?distance_or, ?distance_key),
eth_dos_distance_base(src_or, src_key, dst_or, dst_key, distance_or, distance_key) eth_dos_distance_base(?src_or, ?src_key, ?dst_or, ?dst_key, ?distance_or, ?distance_key)
> )
eth_dos_distance_base(src_or, src_key, dst_or, dst_key, distance_or, distance_key) = and< eth_dos_distance_base(src_or, src_key, dst_or, dst_key, distance_or, distance_key) = AND(
eq(src_or, src_key, dst_or, dst_key), Equal(?src_or[?src_key], ?dst_or[?dst_key]),
ValueOf(distance_or, distance_key, 0) ValueOf(?distance_or[?distance_key], 0)
> )
eth_dos_distance_ind_0(src_or, src_key, dst_or, dst_key, distance_or, distance_key, private: intermed_or, intermed_key, shorter_distance_or, shorter_distance_key, one_or, one_key) = AND(
eth_dos_distance(?src_or, ?src_key, ?intermed_or, ?intermed_key, ?shorter_distance_or, ?shorter_distance_key)
eth_dos_distance_ind_0(src_or, src_key, dst_or, dst_key, distance_or, distance_key) = and< // distance == shorter_distance + 1
eth_dos_distance(src_or, src_key, intermed_or, intermed_key, shorter_distance_or, shorter_distance_key) ValueOf(?one_or[?one_key], 1)
SumOf(?distance_or[?distance_key], ?shorter_distance_or[?shorter_distance_key], ?one_or[?one_key])
// distance == shorter_distance + 1 // intermed is a friend of dst
ValueOf(one_or, one_key, 1) eth_friend(?intermed_or, ?intermed_key, ?dst_or, ?dst_key)
SumOf(distance_or, distance_key, shorter_distance_or, shorter_distance_key, one_or, one_key) )
// intermed is a friend of dst
eth_friend(intermed_or, intermed_key, dst_or, dst_key)
>
``` ```
This group includes three statements. This group includes three statements.
@ -31,10 +30,10 @@ When the definition is serialized for hashing, the statements are renamed to SEL
With this renaming and the wildcards, the first of the three definitions becomes: With this renaming and the wildcards, the first of the three definitions becomes:
``` ```
SELF.1( *1, *2, *3, *4, *5, *6 ) = or< SELF.1(?1, ?2, ?3, ?4, ?5, ?6) = OR(
SELF.2( *1, *2, *3, *4, *5, *6 ) , SELF.2(?1, ?2, ?3, ?4, ?5, ?6)
SELF.3( *1, *2, *3, *4, *5, *6 ) SELF.3(?1, ?2, ?3, ?4, ?5, ?6)
> )
``` ```
and similarly for the other two definitions. and similarly for the other two definitions.

14
book/src/custompred.md
View file

@ -11,17 +11,17 @@ The syntax of a custom operation is best explained with an example.
Original example with anchored keys, origins, and keys. Original example with anchored keys, origins, and keys.
| Args | Condition | Output | | Args | Condition | Output |
|------------|-----------------------------------------|----| |------------|-----------------------------------------|----|
| pod: Origin, <br> good_boy_issuers: AnchoredKey::MerkleRoot, <br> receiver: AnchoredKey | ValueOf(AK(pod, "_type"), SIGNATURE), <br> Contains(good_boy_issuers, AK(pod,"_signer")), <br> Equals(AK(pod, "friend"), receiver) | GoodBoy(receiver, good_boy_issuers) | | 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) |
Compiled example with only origins and keys. Compiled example with only origins and keys.
| Args | Condition | Output | | 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(AK(pod, "_type"), SIGNATURE), <br> Contains(AK(good_boy_issuers_origin, good_boy_issuers_key), AK(pod,"_signer")), <br> Equals(AK(pod, "friend"), AK(receiver_origin, receiver_key)) | GoodBoy(AK(receiver_origin, receiver_key), AK(good_boy_issuers_origin, good_boy_issuers_key)) | | 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]) |
A custom operation accepts as input a number of statements (the `Condition`); 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 an Origin and a Key.
In the "original example" above, the anchored keys `good_boy_issuers` and `receiver` are not broken down, but `AK(pod, "_type"), AK(pod, "_signer"), AK(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 `?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 "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 origins and keys.
@ -35,18 +35,18 @@ On the back end the "compiled example" deduction rule is converted to a sort of
| Args | Condition | Output | | 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(AK(*1, "_type"), SIGNATURE), <br> Contains(AK(*2, *3), AK(*1,"_signer")), <br> Equals(AK(*1, "friend"), AK(*4, *5)) | GoodBoy(AK(*4, *5), AK(*2, *3)) | | ?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]) |
If you want to apply this deduction rule to prove a `GoodBoy` statement, If you want to apply this deduction rule to prove a `GoodBoy` statement,
you have to provide the following witnesses in-circuit. you have to provide the following witnesses in-circuit.
- Copy of the deduction rule - Copy of the deduction rule
- Values for *1, *2, *3, *4, *5. - Values for ?1, ?2, ?3, ?4, ?5.
- Copy of the three statements in the deduction rule with *1, *2, *3, *4, *5 filled in - 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. - Indices of the three statements `ValueOf`, `Contains`, `Equals` in the list of previous statements.
And the circuit will verify: And the circuit will verify:
- *1, *2, *3, *4, *5 were correctly substituted into the statements - ?1, ?2, ?3, ?4, ?5 were correctly substituted into the statements
- The three statements `ValueOf`, `Contains`, `Equals` do indeed appear at the claimed indices. - The three statements `ValueOf`, `Contains`, `Equals` do indeed appear at the claimed indices.
[^operation]: In previous versions of these docs, "operations" were called "deduction rules". [^operation]: In previous versions of these docs, "operations" were called "deduction rules".

235
book/src/examples.md
View file

@ -11,16 +11,25 @@ An EthDos Pod exposes a single custom statement with two custom deduction
rules, the inductive case and the base case. rules, the inductive case and the base case.
``` ```
statement eth_dos_distance(src: PubKey, dst: PubKey, distance: Int): // src, dst: PubKey, attetation_pod: Pod
- OR(): eth_dos_friend(src, dst, private: attestation_pod) = AND(
- AND(attestation_pod: Pod, intermediate: PubKey, n: int): ValueOf(?attestation_pod[KEY_TYPE], SIGNATURE)
- eq(attetation_pod.attestation, dst) Equal(?attestation_pod[KEY_SIGNER], src)
- eq(attetation_pod.type, SIGNATURE) Equal(?attestation_pod["attestation"], dst)
- sum_of(distance, 1, n) )
- eth_dos_distance(src, attetation_pod.signer, n)
- AND(): // src, intermed, dst: PubKey, distance, shorter_distance: Int
- eq(src, dst) eth_dos_distance(src, dst, distance, private: shorter_distance, intermed) = OR(
- eq(distance, 0) AND(
eth_dos_distance(?src, ?intermed, ?shorter)
SumOf(?distance, ?shorter_distance, 1)
eth_friend(?intermed, ?dst)
)
AND(
Equal(?src, ?dst)
Equal(?distance, 0)
)
)
``` ```
## ZuKYC (classic) ## ZuKYC (classic)
@ -31,7 +40,7 @@ Authority public keys:
- `ZOO_GOV`: PubKey, issues IDs - `ZOO_GOV`: PubKey, issues IDs
- `ZOO_DEEL`: PubKey, issues bank statements - `ZOO_DEEL`: PubKey, issues bank statements
Authority lists: Authority lists:
- `SANCTION_LIST`: Hash, Merkle Tree Root of set of sanctioned public keys - `SANCTION_LIST`: Set, Merkle Tree Root of set of sanctioned public keys
- values: `["G2345678", "G1987654", "G1657678"]` - values: `["G2345678", "G1987654", "G1657678"]`
Date values: Date values:
- `NOW_MINUS_18Y`: Int, 18 years ago - `NOW_MINUS_18Y`: Int, 18 years ago
@ -41,29 +50,32 @@ Date values:
A ZuKYC Pod exposes a single custom statement with one custom deduction rule. A ZuKYC Pod exposes a single custom statement with one custom deduction rule.
``` ```
statement loan_check(receiver: PubKey): // receiver: PubKey, gov_id, paystub, sk_pok: Pod, nullifier, sk: Raw
- OR(): loan_check(receiver, private: gov_id, paystub, nullifier, sk, sk_pok) = AND(
- AND(gov_id: Pod, paystub: Pod): Equal(?gov_id["pk"], receiver)
- eq(gov_id.pk, receiver) // Not in the sanction list
# Not in the sanction list SetNotContains(SANCTION_LIST, receiver)
- does_not_contain(SANCTION_LIST, gov_id.pk) // Valid government-issued ID
# Valid government-issued ID Equal(?gov_id[KEY_SIGNER], ZOO_GOV)
- eq(gov_id.signer, ZOO_GOV) Equal(?gov_id[KEY_TYPE], SIGNATURE)
- eq(gov_id.type, SIGNATURE) // At least 18 years old
# At least 18 years old Lt(?gov_id.date_of_birth, NOW_MINUS_18Y) # date_of_birdth is more than 18y old
- lt(gov_id.date_of_birth, NOW_MINUS_18Y) # date_of_birdth is more than 18y old Equal(?paystub[KEY_SIGNER], ZOO_DEEL)
- eq(paystub.signer, ZOO_DEEL) Equal(?paystub[KEY_TYPE], SIGNATURE)
- eq(paystub.type, SIGNATURE) Equal(?paystub[ssn], ?gov_id.ssn)
- eq(paystub.ssn, gov_id.ssn) // At least one year of consistent employment with your current employer
# At least one year of consistent employment with your current employer Lt(?paystub["start_date"], NOW_MINUS_1Y) # start_date is more than 1y old
- lt(paystub.start_date, NOW_MINUS_1Y) # start_date is more than 1y old Gt(?paystub["issue_date"], NOW_MINUS_7D) # issue_date is less than 7d old
- gt(paystub.issue_date, NOW_MINUS_7D) # issue_date is less than 7d old // Annual salary is at least $20,000
# Annual salary is at least $20,000 Gt(?paystub["annual_salary"], 20000)
- gt(paystub.annual_salary, 20000) // Private key knowledge
# Private key knowledge Equal(?sk_pok[KEY_SIGNER], receiver)
- hash(0, sk, gov_id.pk) Equal(?sk_pok[KEY_TYPE], SIGNATURE)
# Nullifier Equal(?sk_pok["auth"], "ZUKYC_V1_AUTH")
- hash("ZooKyc", sk, nullifier) HashOf(, 0, ?sk)
// Nullifier
HashOf(nullifier, "ZUKYC_V1_NULLIFIER", ?sk)
)
``` ```
## ZuKYC (simplified for P1) ## ZuKYC (simplified for P1)
@ -72,7 +84,7 @@ This simplified version uses less statements but requires a very similar set of
features. features.
Authority lists: Authority lists:
- `SANCTION_LIST`: Hash, Merkle Tree Root of set of sanctioned public keys - `SANCTION_LIST`: Set, Merkle Tree Root of set of sanctioned public keys
- values: `["G2345678", "G1987654", "G1657678"]` - values: `["G2345678", "G1987654", "G1657678"]`
Date values: Date values:
- `NOW_MINUS_18Y`: Int, 18 years ago - `NOW_MINUS_18Y`: Int, 18 years ago
@ -81,22 +93,22 @@ Date values:
A ZuKYC Pod exposes a single custom statement with one custom deduction rule. A ZuKYC Pod exposes a single custom statement with one custom deduction rule.
``` ```
statement loan_check(receiver: string): // receiver: String, gov_pk, paystub_pk: PubKey, gov_id, paystub: Pod
- OR(): loan_check(receiver, gov_pk, paystub_pk, private: gov_id, paystub) = AND(
- AND(gov_id: Pod, paystub: Pod): Equal(?gov_id["id_number"], ?receiver)
- eq(gov_id.id_number, receiver) // Not in the sanction list
# Not in the sanction list SetNotContains(SANCTION_LIST, ?gov_id["id_number"])
- does_not_contain(SANCTION_LIST, gov_id.id_number) // Valid government-issued ID
# Valid government-issued ID ValueOf(?gov_id[KEY_SIGNER], ?gov_pk)
- reveal(gov_id.signer) Equal(?gov_id[KEY_TYPE], SIGNATURE)
- eq(gov_id.type, SIGNATURE) // At least 18 years old
# At least 18 years old Lt(?gov_id["date_of_birth"], NOW_MINUS_18Y) # date_of_birdth is more than 18y old
- lt(gov_id.date_of_birth, NOW_MINUS_18Y) # date_of_birdth is more than 18y old ValueOf(?paystub[KEY_SIGNER], ?paystub_pk)
- reveal(paystub.signer) Equal(?paystub[KEY_TYPE], SIGNATURE)
- eq(paystub.type, SIGNATURE) Equal(?paystub["ssn"], ?gov_id["ssn"])
- eq(paystub.ssn, gov_id.ssn) // At least one year of consistent employment with your current employer
# At least one year of consistent employment with your current employer Lt(?paystub["start_date"], NOW_MINUS_1Y) # start_date is more than 1y old
- lt(paystub.start_date, NOW_MINUS_1Y) # start_date is more than 1y old )
``` ```
## GreatBoy ## GreatBoy
@ -104,42 +116,41 @@ statement loan_check(receiver: string):
A Good Boy Pod exposes one custom statement with one custom deduction rule. A Good Boy Pod exposes one custom statement with one custom deduction rule.
``` ```
statement is_good_boy(user: PubKey, good_boy_issuers: MerkleTree): // user: PubKey, good_boy_issuers: Set, pod: Pod, age: Int
- OR(): is_good_boy(user, good_boy_issuers, private: pod, age) = AND(
- AND(pod: Pod, age: Int): Equal(?pod[KEY_TYPE], SIGNATURE)
- eq(pod.type, SIGNATURE) SetContains(?good_boy_issuers, ?pod[KEY_SIGNER])
- contains(good_boy_issuers, pod.signer) // A good boy issuer says this user is a good boy
# A good boy issuer says this user is a good boy Equal(?pod["user"], ?user)
- eq(pod.user, user) Equal(?pod["age"], ?age)
- eq(pod.age, age) )
``` ```
A Friend Pod exposes one custom statement with one custom deduction rule. A Friend Pod exposes one custom statement with one custom deduction rule.
``` ```
statement is_friend(good_boy: PubKey, friend: PubKey, good_boy_issuers: MerkleTree): // good_boy, friend: PubKey, good_boy_issuers: Set, friend_pod: Pod
- OR(): is_friend(good_boy, friend, good_boy_issuers, friend_pod) = AND(
- AND(friend_pod: Pod): Equal(?pod[KEY_TYPE], SIGNATURE)
- eq(pod.type, SIGNATURE) // The issuer is a good boy
# The issuer is a good boy is_good_boy(?good_boy, ?good_boy_issuers)
- is_good_boy(good_boy, good_boy_issuers) // A good boy says this is their friend
# A good boy says this is their friend Equal(?pod[KEY_SIGNER], ?good_boy)
- eq(pod.signer, good_boy) Equal(?pod["friend"], ?friend)
- eq(pod.friend, friend) )
``` ```
A Great Boy Pod exposes (in addition to the above) one new custom statement A Great Boy Pod exposes (in addition to the above) one new custom statement
with one custom deduction rule. with one custom deduction rule.
``` ```
statement is_great_boy(great_boy: PubKey, good_boy_issuers: MerkleTree): great_boy: PubKey, good_boy_issuers: Set, friend_pod_0, friend_pod_1: Pod
- OR(): is_great_boy(great_boy, good_boy_issuers, private: friend_pod_0, friend_pod_1) = AND
- AND(friend_pod_0: Pod, friend_pod_1: Pod): // Two good boys consider this user their friend
# Two good boys consider this user their friend is_friend(?friend_pod_0[KEY_SIGNER], ?great_boy)
- is_friend(friend_pod_0.signer, great_boy) is_friend(?friend_pod_1[KEY_SIGNER], ?great_boy)
- is_friend(friend_pod_1.signer, great_boy) // good boy 0 != good boy 1
# good boy 0 != good boy 1 NotEqual(?friend_pod_0[KEY_SIGNER], ?friend_pod_1[KEY_SIGNER])
- neq(friend_pod_0.signer, friend_pod_1.signer)
``` ```
## Attested GreatBoy ## Attested GreatBoy
@ -147,17 +158,16 @@ statement is_great_boy(great_boy: PubKey, good_boy_issuers: MerkleTree):
An Attested Great Boy Pod is like a Great Boy Pod, but the names of the signers are revealed. An Attested Great Boy Pod is like a Great Boy Pod, but the names of the signers are revealed.
``` ```
statement is_great_boy(great_boy: PubKey, friend0: String, friend1: String, good_boy_issuers: MerkleTree): // great_boy: PubKey, friend0, friend1: String, good_boy_issuers: Set, friend_pod_0, friend_pod_1: Pod
- OR(): is_great_boy(great_boy, friend0, friend1, good_boy_issuers, private: friend_pod_0, friend_pod_1) = AND
- AND(friend_pod_0: Pod, friend_pod_1: Pod): // Two good boys consider this user their friend
# Two good boys consider this user their friend is_friend(?friend_pod_0[KEY_SIGNER], ?great_boy)
- is_friend(friend_pod_0.signer, great_boy) is_friend(?friend_pod_1[KEY_SIGNER], ?great_boy)
- is_friend(friend_pod_1.signer, great_boy) // good boy 0 != good boy 1
# good boy 0 != good boy 1 NotEqual(?friend_pod_0[KEY_SIGNER], ?friend_pod_1[KEY_SIGNER])
- neq(friend_pod_0.signer, friend_pod_1.signer) // publicize signer names
# publicize signer names ValueOf(?friend_pod_0["name"], ?friend0)
- value_of(friend_pod_0.name, friend0) ValueOf(?friend_pod_1["name"], ?friend1)
- value_of(friend_pod_1.name, friend1)
``` ```
To produce a Great Boy Pod, you need two Friend Pods, `friend_pod0` and `friend_pod1`, each of which reveals its `signer`. To produce a Great Boy Pod, you need two Friend Pods, `friend_pod0` and `friend_pod1`, each of which reveals its `signer`.
@ -185,52 +195,51 @@ timestamp: Int
A post is popular if it has at least two comments from different signers. A post is popular if it has at least two comments from different signers.
``` ```
statement is_popular(post: PodID): // post, comment1, comment2: Pod
- AND(): statement is_popular(post, private: comment1, comment2) = AND(
- IsEqual(comment1.referenced_post, post) IsEqual(?comment1["referenced_post"], ?post)
- IsEqual(comment2.referenced_post, post) IsEqual(?comment2["referenced_post"], ?post)
- NotEqual(comment1.signer, comment2.signer) NotEqual(?comment1[KEY_SIGNER], ?comment2[KEY_SIGNER])
)
``` ```
## Multiple people over 18 ## Multiple people over 18
Suppose I want to prove that two different people are over 18, and a third person is under 18, using the custom predicates `over_18` and `under_18`. Suppose I want to prove that two different people are over 18, and a third person is under 18, using the custom predicates `over_18` and `under_18`.
``` ```
statement over_18(age): // age: Int
- AND(): over_18(age) = AND(
- ValueOf(eighteen, 18) GtEq(?age, 18)
- GEq(age, eighteen) )
``` ```
``` ```
statement under_18(age): // age: Int
- AND(): under_18(age) = AND(
- ValueOf(eighteen, 18) Lt(age, 18)
- Lt(age, eighteen) )
``` ```
With wildcards: With wildcards:
``` ```
statement over_18(*1, *2): over_18(?1) = AND(
- AND(): GtEq(?1, 18)
- ValueOf(*3, *4, 18) )
- GEq(*1, *2, *3, *4)
``` ```
Maybe I have two input pods `gov_id1` and `gov_id2`, and I want to prove that these pods refer to two different people, both of whom are over 18; and a third pods `gov_id3` refers to someone under 18. So in my public output statements, I want to have: Maybe I have two input pods `gov_id1` and `gov_id2`, and I want to prove that these pods refer to two different people, both of whom are over 18; and a third pods `gov_id3` refers to someone under 18. So in my public output statements, I want to have:
``` ```
IsUnequal(gov_id1.name, gov_id2.name) NotEqual(?gov_id1["name"], ?gov_id2["name"])
over_18(gov_id1.age) over_18(?gov_id1["age"])
over_18(gov_id2.age) over_18(?gov_id2["age"])
under_18(gov_id3.age). under_18(?gov_id3["age"]).
``` ```
I would prove this with the following sequence of deductions: I would prove this with the following sequence of deductions:
| Statement | Reason | | Statement | Reason |
| --- | --- | | --- | --- |
| ValueOf(local_eighteen, 18) | (new entry) | | over_18(gov_id1["age"]) | over_18, <br> ?1 = gov_id1["age"] |
| over_18(gov_id1.age) | over_18, <br> *1 = _SELF, <br> *2 = "local_eighteen", <br> *3 = gov_id1, <br> *4 = "age" | | over_18(gov_id2["age"]) | over_18, <br> ?1 = gov_id2["age"] |
| over_18(gov_id2.age) | over_18, <br> *1 = _SELF, <br> *2 = "local_eighteen", <br> *3 = gov_id2, <br> *4 = "age" | | under_18(gov_id3["age"]) | under_18, <br> ?1 = gov_id3["age"] |
| under_18(gov_id3.age) | under_18, <br> *1 = _SELF, <br> *2 = "local_eighteen", <br> *3 = gov_id3, <br> *4 = "age" | | NotEqual(gov_id1["name"], gov_id2["name"]) | (not equal from entries) |
| IsUnequal(gov_id1.name, gov_id2.name) | (is unequal from entries) |

54
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: Example:
``` ```
STATEMENT1 = Equals(oldpod, "name", otherpod, "field") STATEMENT1 = Equals(oldpod["name"], otherpod["field"])
STATEMENT2 = Equals(otherpod, "field", newpod, "result") STATEMENT2 = Equals(otherpod["field"], newpod["result"])
STATEMENT3 = Equals(oldpod, "name", newpod, "result") STATEMENT3 = Equals(oldpod["name"], newpod["result"])
``` ```
The reasons in human-readable simplified format: The reasons in human-readable simplified format:
@ -59,19 +59,19 @@ 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 (key, origin) pairs. This is the frontend description of the deduction rule.
``` ```
IF IF
Equals(a_or, a_key, b_or, b_key) Equals(a_or[a_key], b_or[b_key)
AND AND
Equals(b_or, b_key, c_or, c_key) Equals(b_or[b_key], c_or[c_key])
THEN THEN
Equals(a_or, a_key, c_or, c_key) Equals(a_or[a_key], c_or[c_key])
``` ```
In-circuit, all these identifiers are replaced with wildcards, which come in numerical order (because they will be used as array indices). So the backend representation is: In-circuit, all these identifiers are replaced with wildcards, which come in numerical order (because they will be used as array indices). So the backend representation is:
``` ```
IF IF
Equals( *1, *2, *3, *4 ) and Equals ( *3, *4, *5, *6 ) Equals( ?1[?2], ?3[?4] ) and Equals ( ?3[?4], ?5[?6] )
THEN THEN
Equals( *1, *2, *5, *6 ) Equals( ?1[?2], ?5[?6] )
``` ```
@ -80,24 +80,24 @@ Equals( *1, *2, *5, *6 )
- Repeat deduction rule - Repeat deduction rule
``` ```
IF IF
Equals( *1, *2, *3, *4 ) and Equals ( *3, *4, *5, *6 ) Equals( ?1[?2], ?3[?4] ) and Equals ( ?3[?4], ?5[?6] )
THEN THEN
Equals( *1, *2, *5, *6 ) Equals( ?1[?2], ?5[?6] )
``` ```
- Say what the wildcards are - Say what the wildcards are
``` ```
*1 -- oldpod ?1 -- oldpod
*2 -- "name" ?2 -- "name"
*3 -- otherpod ?3 -- otherpod
... ...
``` ```
- Substitute the wildcards into the deduction rule - Substitute the wildcards into the deduction rule
``` ```
IF IF
Equals( oldpod, "name", ... ) ... Equals( oldpod["name"], ... ) ...
Equals( otherpod, "value") Equals( otherpod["value"])
THEN THEN
Equals( oldpod, "name", newpod, ... ) Equals( oldpod["name"] newpod[...] )
... ...
``` ```
- Say where to find the previous statements (indices in the list), and check that they are above this one. - Say where to find the previous statements (indices in the list), and check that they are above this one.
@ -118,13 +118,13 @@ The wildcard system handles this very naturally, since origin ID and key are two
``` ```
eth_friend(src_or, src_key, dst_or, dst_key) = and< eth_friend(src_or, src_key, dst_or, dst_key) = and<
// there is an attestation pod that's a SIGNATURE POD // there is an attestation pod that's a SIGNATURE POD
ValueOf(attestation_pod, "type", SIGNATURE) ValueOf(?attestation_pod["type"], SIGNATURE)
// the attestation pod is signed by (src_or, src_key) // the attestation pod is signed by (src_or, src_key)
Equal((attestation_pod, "signer"), (src_or, src_key)) Equal(?attestation_pod["signer"], ?src_or[?src_key])
// that same attestation pod has an "attestation" // that same attestation pod has an "attestation"
Equal((attestation_pod, "attestation"), (dst_or, dst_key)) Equal(?attestation_pod["attestation"], ?dst_or[?dst_key])
> >
``` ```
@ -132,9 +132,9 @@ In terms of anchored keys, it would be a little more complicated. five anchored
``` ```
AK1 = src AK1 = src
AK2 = dst AK2 = dst
AK3 = (attestation_pod, "type") AK3 = attestation_pod["type"]
AK4 = (attestation_pod, "signer") AK4 = attestation_pod["signer"]
AK5 = (attestation_pod, "attestation") AK5 = attestation_pod["attestation"]
``` ```
and we need to force AK3, AK4, AK5 to come from the same origin. and we need to force AK3, AK4, AK5 to come from the same origin.
@ -142,14 +142,14 @@ and we need to force AK3, AK4, AK5 to come from the same origin.
WILDCARD matching takes care of it. WILDCARD matching takes care of it.
``` ```
eth_friend(*1, *2, *3, *4) = and< eth_friend(?1, ?2, ?3, ?4) = and<
// there is an attestation pod that's a SIGNATURE POD // there is an attestation pod that's a SIGNATURE POD
ValueOf(*5, "type", SIGNATURE) ValueOf(?5["type"], SIGNATURE)
// the attestation pod is signed by (src_or, src_key) // the attestation pod is signed by ?src_or[?src_key]
Equal((*5, "signer"), (*1, *2)) Equal(?5["signer"], ?1[?2])
// that same attestation pod has an "attestation" // that same attestation pod has an "attestation"
Equal((*5, "attestation"), (*3, *4)) Equal(?5["attestation"], ?3[?4])
> >
``` ```

14
book/src/statements.md
View file

@ -55,7 +55,7 @@ The frontend also exposes the following syntactic sugar predicates. These predi
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. 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. <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.
@ -64,12 +64,12 @@ as well as for low-level operations on Merkle trees and compound types.
A ```ValueOf``` statement asserts that an entry has a certain value. A ```ValueOf``` statement asserts that an entry has a certain value.
``` ```
ValueOf(A.name, "Arthur") ValueOf(A["name"], "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.) 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.)
``` ```
Equal(A.name, B.name) Equal(A["name"], B["name"])
``` ```
An ```NotEqual``` statement asserts that two entries have different values. An ```NotEqual``` statement asserts that two entries have different values.
@ -81,8 +81,8 @@ NotEqual (for arbitrary types)
An ```Gt(x, y)``` statement asserts that ```x``` is an entry of type ```Integer```, ```y``` is an entry or constant of type ```Integer```, and ```x > y```. An ```Gt(x, y)``` statement asserts that ```x``` is an entry of type ```Integer```, ```y``` is an entry or constant of type ```Integer```, and ```x > y```.
``` ```
Gt (for numerical types only) Gt (for numerical types only)
Gt(A.price, 100) Gt(A["price"], 100)
Gt(A.price, B.balance) Gt(A["price"], B["balance"])
``` ```
The statements ```Lt```, ```GEq```, ```Leq``` are defined analogously. The statements ```Lt```, ```GEq```, ```Leq``` are defined analogously.
@ -93,11 +93,11 @@ The statements ```Lt```, ```GEq```, ```Leq``` are defined analogously.
The two items below may be added in the future: The two items below may be added in the future:
``` ```
poseidon_hash_of(A.hash, B.preimage) // perhaps a hash_of predicate can be parametrized by an enum representing the hash scheme; rather than having a bunch of specific things like SHA256_hash_of and poseidon_hash_of etc. poseidon_hash_of(A["hash"], B["preimage"]) // perhaps a hash_of predicate can be parametrized by an enum representing the hash scheme; rather than having a bunch of specific things like SHA256_hash_of and poseidon_hash_of etc.
``` ```
``` ```
ecdsa_priv_to_pub_of(A.pubkey, B.privkey) ecdsa_priv_to_pub_of(A["pubkey"], B["privkey"])
``` ```