Merge branch 'main' into feat/dummy-signed-pod

Author: ed255

book/src/custom.md

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

book/src/customexample.md

@@ -2,27 +2,26 @@
 # 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_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) = and<
-   eq(src_or, src_key, dst_or, dst_key),
-   ValueOf(distance_or, distance_key, 0)
-   >
-
-
-eth_dos_distance_ind_0(src_or, src_key, dst_or, dst_key, distance_or, distance_key) = and<
-   eth_dos_distance(src_or, src_key, intermed_or, intermed_key, shorter_distance_or, shorter_distance_key)
-
-   // distance == shorter_distance + 1
-   ValueOf(one_or, one_key, 1)
-   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)
-   >
+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_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(
+    Equal(?src_or[?src_key], ?dst_or[?dst_key]),
+    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)
+
+    // distance == shorter_distance + 1
+    ValueOf(?one_or[?one_key], 1)
+    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.
@@ -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:
 ```
-SELF.1( *1, *2, *3, *4, *5, *6 ) = or<
-   SELF.2( *1, *2, *3, *4, *5, *6 ) ,
-   SELF.3( *1, *2, *3, *4, *5, *6 ) 
-   >
+SELF.1(?1, ?2, ?3, ?4, ?5, ?6) = OR( 
+    SELF.2(?1, ?2, ?3, ?4, ?5, ?6)
+    SELF.3(?1, ?2, ?3, ?4, ?5, ?6) 
+) 
 ```
 and similarly for the other two definitions.
 

book/src/custompred.md

@@ -11,17 +11,17 @@ 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(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.
 | 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`); 
 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.
 
@@ -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(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,
 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
+- 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.
 
 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.
 
 [^operation]: In previous versions of these docs, "operations" were called "deduction rules".