Aard custom (#49)

* Merge changes to docs

* Fix typo

* Correct SUMMARY so it compiles; update .gitignore

* Clean up statements.md

Make syntax and notation consistent with Rust source code.

* Fix statements for Merkle trees and compound types

* First draft of custom statements and small updates to signedpod.md

* Update book/src/merkletree.md

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

* merklestatements correct typo

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

* add todo for gadget ids

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

* Separate out custom statements version 1

* More details on custom statements version 1

* new file custom2

* Partial draft of version 2

* First draft of version 2 spec, it's kind of a mess

* Another version of the custom predicates spec

* Update book/src/custom2.md

Co-authored-by: Eduard S. <eduardsanou@posteo.net>

* Simple example of deduction rule applied in circuit

* Implement Edu's comments on custom predicates

* Backend predicates must be defined in groups

* Add more examples

* Two diff statements using same constant

* Remove deprecated example

---------

Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>
Co-authored-by: Eduard S. <eduardsanou@posteo.net>

Author: 3 people

.gitignore

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

book/src/SUMMARY.md

@@ -3,6 +3,7 @@
 - [Introduction](./introduction.md)
 
 # Specification
+- [Front and back end](./front_and_back.md)
 - [The frontend structure of a POD]()
   - [Frontend POD value types](./values.md)
   - [Anchored keys](./anchoredkeys.md)
@@ -13,6 +14,11 @@
   - [Statements](./statements.md)
     - [Statements involving compound types and Merkle trees](./merklestatements.md)
   - [Operations](./operations.md)
+    - [Simple example](./simpleexample.md)
+  - [Custom statements and custom operations](./custom.md)
+    - [Version 1](./custom1.md)
+    - [Version 1, written again](./custom1b.md)
+    - [Custom statement example](./customexample.md)
 - [POD types](./podtypes.md)
   - [SignedPOD](./signedpod.md)
   - [MainPOD](./mainpod.md)

book/src/custom.md

@@ -1 +1,19 @@
 # Custom statements and custom operations
+
+Users of the POD system can introduce _custom predicates_ (previously called _custom statements_) to express complex logical relations not available in the built-in predicates.  Every custom predicate is defined as the conjunction (AND) or disjunction (OR) of a small number of other statements.
+
+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.
+
+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.  
+
+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_.
+
+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.
+
+## 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

@@ -0,0 +1,52 @@
+# Custom operations (or: how to define a custom predicate): VERSION 1
+
+(Note: At the moment, we consider a "custom operation" to be exactly the same thing as the "definition of a custom predicate.")
+
+A custom operation [^operation] is a rule that allows one to deduce a custom statement from one or more existing statements according to a logical rule, described below.
+
+> Note: Unlike built-in operations, it is not possible to perform arbitrary calculations inside a custom operation.
+
+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) |
+
+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)) |
+
+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 "compiled example", all the anchored keys have been broken down into origins 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".
+
+In order to apply the operation, the user who wants to create a POD must give acceptable values for all the arguments.  The POD prover will substitute those values for all the statements in the "Condition" and check that all substituted statements previously appear in the POD.  If this check passes, the output statement is then a valid statement.
+
+## What applying the operation looks like on the back end
+
+On the back end the "compiled example" deduction rule is converted to a sort of "template":
+
+| 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)) |
+
+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.
+
+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.
+
+[^operation]: In previous versions of these docs, "operations" were called "deduction rules".

book/src/custom1b.md

@@ -0,0 +1,36 @@
+# Custom operations (or: how to define a custom predicate), version 1, written again
+
+[All constant integers in this spec are determined by circuit size and subject to change.]
+
+On the frontend, a _custom predicate_ is defined as a combination of conjunctions and disjunctions of other custom predicates and possibly the predicate itself.
+
+On the backend, _custom predicates_ are defined in groups of up to 10.  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) 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, ....
+
+## Examples
+
+See [examples](./customexample.md)
+
+## Hashing and predicate IDs
+
+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 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 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/custom2.md

@@ -0,0 +1,130 @@
+# Custom operations (or: how to define a custom predicate): VERSION 2
+
+# DO NOT USE THIS DOC
+# SAVING IN THE GITHUB JUST SO WE HAVE A COPY
+# WE ARE NOT USING THIS SPEC
+# DO NOT USE
+
+## The local variable requirement
+
+This spec differs from the main spec in that there are no anchored keys.  However, there are still types `Origin` and `Key`.
+
+An `Origin` refers to an input POD; in-circuit, the `Origin` is the pod ID of the pod.
+
+A `Key` refers to a value within a POD.
+
+With the exception of the special statement `ValueFromPodKey`, a key always refers to a value within the POD _self.  In other words, a statement (except for `ValueFromPodKey`) cannot refer to a value from a previous POD, only to a value in the "namespace" of the current POD.
+
+Roughly speaking, the statement
+```
+ValueFromPodKey(local_key, origin_id, key)
+```
+means that the value of `local_key` on the current POD (_self) is the same as the value of `key` on the POD `origin_id` -- in other words, it is basically the same as 
+```
+Equals(AnchoredKey(_SELF, local_key), AnchoredKey(origin_id, key)).
+```
+
+I say "basically the same" because, in this spec, it is possible to refer to both keys and origin IDs by reference.
+
+## Referencing
+
+Recall that in the front-end, a `Key` is a string that functions as an identifier (like a variable name in other languages), and a `Value` is the value of that variable -- an `Integer`, `String`, or compound value.
+
+In the back-end, a `Key` is four field elements (computed as a hash of the front-end key); and a `Value` is again four field elements.  Again, each `Key` has a unique `Value`.
+
+A `Reference` statement allows a key to be reinterpreted as a value; it is analogous to a pointer in C.
+
+The statement
+```
+Reference(reference_key, key)
+```
+means that `reference_key` is a key, whose associated value is the same as the key `key`.
+
+## ValueFromPodKey, precisely this time
+
+```
+ValueFromPodKey(local_key: KeyOrLiteral::String, origin_id: KeyOrLiteral::OriginID, key: KeyOrLiteral::String).
+```
+
+means that the _values_ of `local_key` and `key` are _keys_, the _value_ of `origin_id` is an _origin ID_, and the value assigned to the key `local_key` on the present POD is the same as the value assigned to the key `key` on the pod `origin_ID`.
+
+An example with literals:
+```
+ValueFromPodKey("local_ssn", 0x4030, "ssn")
+```
+means that the pod `0x4030` has a key called `ssn`, the local pod has a key `local_ssn`, and they have the same value.
+
+An example with keys, that expresses the same semantic meaning:
+```
+ValueOf(local_varname, "local_ssn")
+ValueOf(remote_varname, "ssn")
+ValueOf(gov_id_pod_id, 0x4030)
+ValueFromPodKey(local_varname, gov_id_pod_id, remote_varname)
+```
+
+## Summary of additional statements in this spec
+
+```
+ValueFromPodKey(local_key: KeyOrLiteral::String, origin_id: KeyOrLiteral::OriginID, key: KeyOrLiteral::String).
+```
+
+
+In addition to the built-in statements in the [main spec](./statements.md):
+
+There is one additional front-end type: `OriginID`.  As the name suggests, it contains the "origin ID" of a POD.
+
+There are two additional built-in statements:
+```
+Reference(reference_key: Key::String, key: Key)
+
+ValueFromPodKey(local_key: KeyOrLiteral::String, origin_id: KeyOrLiteral::OriginID, key: KeyOrLiteral::String).
+```
+
+```
+Reference(reference_key, key)
+```
+means that the *value* of `reference key` is the *key name* of `key`.
+
+```
+ValueFromPodKey(local_key, origin_id, key)
+```
+means that the key `local_key` in the local scope has the same value as the key `key` in the scope of the pod `origin_id`.
+
+## How to work with the local variable requirement
+
+To make a statement about an inherited value (a value introduced in an ancestor POD), the value must be copied to a local value:
+
+The statements below assert that "name" on pod1 and "friend" on pod2 are assigned the same value.
+```
+ValueFromPodKey(name_from_pod1, pod1, "name")
+ValueFromPodKey(friend_from_pod2, pod2, "friend")
+Equal(name_from_pod1, friend_from_pod2)
+```
+
+## How to inherit local variables from a previous POD
+
+In this design, an additional complication arises when you
+carry a value from one POD to another,
+and you want to keep track of the origin POD on which it originated.
+
+To allow this operation, we introduce an additional deduction rule
+```
+InheritValueFromPodKey,
+```
+which works as follows.
+
+Suppose "self" is the current POD and "parent_id" is the POD id of one of the input PODs to "self".
+
+Suppose "parent" has, among its public statements, the statement
+```
+ValueFromPodKey(parent_name, origin, original_name)
+```
+and "self" has the statement (public or private)
+```
+ValueFromPodKey(self_name, parent_id, parent_name).
+```
+
+Then ```InheritValueFromPodKey``` allows you to generate the following statement on "self":
+```
+ValueFromPodKey(self_name, origin, original_name).
+```

book/src/customexample.md

@@ -0,0 +1,48 @@
+
+# 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)
+   >
+```
+
+This group includes three statements.
+
+When the definition is serialized for hashing, the statements are renamed to SELF.1, SELF.2, SELF.3.
+
+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 ) 
+   >
+```
+and similarly for the other two definitions.
+
+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 group are identified as:
+```
+eth_dos_distance = groupHASH.1
+eth_dos_distance_base = groupHASH.2
+eth_dos_distance_ind = groupHASH.3
+```