Implement Edu's comments on custom predicates

Author: tideofwords

.gitignore

@@ -2,3 +2,4 @@
 Cargo.lock
 .DS_Store
 aardnotes.md
+notes

book/src/custom.md

@@ -4,14 +4,15 @@ Users of the POD system can introduce _custom predicates_ (previously called _cu
 
 When a custom predicate is introduced in a MainPod, it becomes available for use in that POD and all PODs that inherit[^inherit] from it.
 
-A custom predicate can be defined either _nonrecursively_ or _recursively_ (as part of a "batch"). A nonrecursive custom predicate is defined in terms of previously defined predicates (whether custom or native).  A "batch" of custom predicates can be defined _recursively_: the definition of any custom predicate in the batch can use both previously defined predicates and all the predicates in the batch.
+On the frontend, a custom predicate is defined as a collection of conjunctions and disjunctions of statements.  The definition can be recursive: the definition of a predicate can involve the predicate itself, or the definitions of several predicates can depend on each other.  
 
-## Custom predicates and their IDs
+At the backend level, every definition of a predicate is either a conjunction or a disjunction of statements.  To convert a frontend custom predicate to the backend, the middleware may need to introduce _sub-predicates_.
 
-A custom predicate, like a built-in predicate, is identified by a _name_ on the front end and an _identifier_ on the back end.  In the non-recursive case, the back-end identifier is defined as a hash of the definition of the custom predicate.
+On the backend, custom predicates are defined in _groups_.  A group can contain one or more custom predicates and their associated sub-predicates.  Recursive definition is only possible within a group: the definition of a predicate in a group can only depend on previously existing predicates, itself, and other predicates in the same group.
 
-### Recursively defined custom predicates
+## Custom predicates and their IDs
 
+A custom predicate, like a built-in predicate, is identified by a _name_ on the front end and an _identifier_ on the back end.  The identifier is a cryptographic hash of the definition of the group.
 
 
 [^inherit]: What to call this?  One POD "inherits" from another?

book/src/custom1.md

@@ -41,7 +41,7 @@ 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.  (*1, *2, *4 should be OriginIDs for the three origins; *3 and *5 should be key names.)
+- 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.
 

book/src/custom1b.md

@@ -5,37 +5,33 @@
 A _custom predicate_ can be defined in one of two ways:
 
 - Directly, as either the AND or OR of two pre-existing predicates, or
-- Recursively, in a _batch_ of up to 10 custom predicates.  Each custom predicate in the batch is either the AND or OR of five predicates which are either pre-existing, or defined in the same batch.
+- Recursively, in a _group_ of up to 10 custom predicates.  Each custom predicate in the group is either the AND or OR of five predicates which are either pre-existing, or defined in the same group.
 
 [Note: We could potentially allow the AND or OR of, say, two predicates instead of five.  To make this work, we might need to have access to pod ID as a virtual key, see github issue #60]
 
 ## Arguments of custom predicates
 
-The definition of a custom predicate might also be called an _operation_ or _deduction rule_.  It includes two (or, potentially, say, five) input statements.  The arguments to the input statements are decomposed as (origin, key) pairs: if statements are allowed to have arity at most 4, then the input statements 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 input statement 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
 
 See [examples](./customexample.md)
 
 ## Hashing and predicate IDs
 
-Each custom predicate is assigned a cryptographic ID as follows:
-
-If it is defined directly: its ID is simply a zk-friendly hash of its definition.  The definition is serialized as it will appear in circuit (see below) and hashed.
-
-If it is defined in a batch: The definitions of all statements in the batch are laid out consecutively (see [examples](./customexample.md)) and hashed.
+Each custom predicate is defined as part of a _group_ of predicates. The definitions of all statements in the group are laid out consecutively (see [examples](./customexample.md)) and hashed.
 
 ## How to prove an application of an operation
 
 A POD contains a "tabular proof", in which each row includes a "statement" and a "reason".  The "reason" is everything the circuit needs as a witness to verify the statement.
 
 For a custom statement, the "reason" includes the following witnesses and verifications:
 - the definition of the statement, serialized (see [examples](./customexample.md))
-  - if the statement is part of a batch, the definition of the full batch, 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
-- the definition will have some number of "wildcards" (*1, *2, ...) as arguments to input statements; 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 statements (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

book/src/customexample.md

@@ -1,7 +1,8 @@
 
-# Ethdos custom predicate, using binary AND and OR: example of a direct definition and a recursive batch
+# Ethdos custom predicate, using binary AND and OR: example of a direct definition and a recursive group
 
 ## Direct definition
+(DEPRECATED: All predicates must be defined as part of a group.)
 ```
 eth_friend(src_or, src_key, dst_or, dst_key) = and<
     // there is an attestation pod that's a SIGNATURE POD
@@ -30,7 +31,7 @@ This backend definition is then hashed in the obvious way.
 
 ```
 
-## Recursive batch definition
+## Recursive group definition
 
 ```
 eth_dos_distance(src_or, src_key, dst_or, dst_key, distance_or, distance_key) = or<
@@ -56,7 +57,7 @@ eth_dos_distance_ind_0(src_or, src_key, dst_or, dst_key, distance_or, distance_k
    >
 ```
 
-This batch includes three statements.
+This group includes three statements.
 
 When the definition is serialized for hashing, the statements are renamed to SELF.1, SELF.2, SELF.3.
 
@@ -69,11 +70,11 @@ SELF.1( *1, *2, *3, *4, *5, *6 ) = or<
 ```
 and similarly for the other two definitions.
 
-The above definition is serialized in-circuit and hashed with a zk-friendly hash to generate the "batch hash", a unique cryptographic identifier for the batch.
+The above definition is serialized in-circuit and hashed with a zk-friendly hash to generate the "group hash", a unique cryptographic identifier for the group.
 
-Then the individual statements in the batch are identified as:
+Then the individual statements in the group are identified as:
 ```
-eth_dos_distance = BATCHHASH.1
-eth_dos_distance_base = BATCHHASH.2
-eth_dos_distance_ind = BATCHHASH.3
+eth_dos_distance = groupHASH.1
+eth_dos_distance_base = groupHASH.2
+eth_dos_distance_ind = groupHASH.3
 ```

book/src/examples.md

@@ -136,3 +136,21 @@ statement is_great_boy(great_boy: PubKey, good_boy_issuers: MerkleTree):
          # good boy 0 != good boy 1
          - neq(friend_pod_0.signer, friend_pod_1.signer)
 ``` 
+
+## Attested GreatBoy
+
+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):
+   - OR():
+      - AND(friend_pod_0: Pod, friend_pod_1: Pod):
+         # Two good boys consider this user their friend
+         - is_friend(friend_pod_0.signer, great_boy)
+         - is_friend(friend_pod_1.signer, great_boy)
+         # good boy 0 != good boy 1
+         - neq(friend_pod_0.signer, friend_pod_1.signer)
+         # publicize signer names
+         - value_of(friend_pod_0.name, friend0)
+         - value_of(friend_pod_1.name, friend1)
+```