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

Aard custom (#49)

Browse source 
* 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>
This commit is contained in:
tideofwords 2025-02-24 09:05:30 -08:00 • committed by GitHub
parent c101d94530
commit d3bc892906
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 543 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

52
book/src/custom1.md Normal file
View file

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