- middleware:
- Add `Statement::Intro`
- Add `SignedBy` native predicate and operation. The signature is auxiliary data to the operation
- Rename `PodSigner` to `Signer` with a new API (just for signing `RawValue`)
- Removed `NewEntry` operation. Use `ContainsFromEntries` instead
- Remove `KEY_SIGNER` and `KEY_TYPE` which are no longer used
- Merge `RecursivePod` and `Pod` traits
- Change the `Pod::deserialize_data` method to use `Self` instead of `Box<dyn Pod>`
- Extend `Pod` trait with these methods:
- `is_main`: when the pod is Main, in a (recursive) verification its vk will be checked to exist in the vd_set but not if it's intro pod
- `is_mock`: skip some verifications in the recursive mock MainPod verification
- `verifier_data_hash`
- `pod_id` renamed to `statements_hash`
- AnchoredKeys are now a pair of dictionary root and key
- Entry statements are now defined as Contains with literal arguments
- Operations that take Entries now use Contains statements with literal arguments
- frontend:
- Rename `SignedPod` to `SignedDict` (which now contains the dict, public key and signature, and can still `verify(self)`ed)
- The `SignedDict` keeps the method `get_statement` for convenience but now it returns a `Contains` statement that proves the existence of the key in the dict
- The `MainPodBuilder` automatically inserts a `Contains` statement when an operation is added that uses an entry as argument that was not yet "opened".
- Removed the `literal` methods from the `MainPodBuilder` that were loading literals to anchored keys: that was no longer needed after we introduced literal arguments
- backend
- Only verify inclusion of the verifying key into the vd_set if the pod is MainPod. A pod is not MainPod if the first statement is Intro.
- Reject intro pods that have non-intro statements
- Empty pod now returns an intro statement
- Don't insert a type statement automatically in MainPod and MockMainPod. We get rid of the type entry.
- Implement `SignedBy` operation, which uses the muxed table to store signature verifications
- Rename `PodId` to `statements_hash` or `sts_hash` for short. Now this is only used as a hash of the statements for the circuits public inputs.
- Refactor normalization of `self` statements:
- Before: replace values that contain `SELF` by the given pod_id
- After: place the verifying key hash into the Intro predicates
* wrote some initial code
* added way to input private key into circuit
* TypedValue::SecretKey hashed as 10 32-bit limbs
* Check PublicKeyOf in Frontend and Middleware
* Diff review
* PR review
* Finish utest
* Fix bounds check
* added giving secret key witness to circuit
* Test & doc improvements
* added private key comparison to circuit and added test cases
* cargo fmt
* Add frontend tests for PublicKeyOf
* Add public_key_of and hash_of to op! macro
* Add ownership check to ticket example
* Group order checking in tests
* More negative test cases at circuit level
* Cleanups after self review
* clippy fixes
* Fixes after merge. Temporarily remove plonky2 commit hash
* Add a nullifier to the ticket test example
* Test PublicKeyOf with a real prover (not mock)
* plonky-u32 dependency
* feat: optimize operation checks
Skip the circuits that verify operation checks other than None, Copy or
NewEntry for the public statements. This works because public
statements are created by copying private statements, so we never use
the other operation checks in those slots.
---------
Co-authored-by: Andrew Twyman <artwyman@gmail.com>
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
In this commit I remove all `*Gadget` types and instead implement the naming convention defined here https://github.com/0xPARC/pod2/issues/181#issuecomment-3051954321
The biggest changes can be summarized by:
- a) Removal of `*Gadget` types and their `eval_*` methods in favour of `verb_object_circuit` functions.
- b) The above functions don't create targets that need to be witness-assigned later. Instead they receive those as arguments. This clearly shows what's the circuit input and output.
I'm specially happy about the changes from b), I think they make the flow of data in the circuit more clear.
Missing things that I did not address in this PR
- The RecursiveCircuit still uses some old naming conventions like `build`.
- We have some `*Target` types that have methods that define constraints. I think we can keep those as they are convenient and I don't see them as strongly breaking the new convention: I see them as the object-oriented way to apply the convention. In those cases the `object` can be omitted from the method when it's implied by the type name, and the `_circuit` suffix doesn't appear because it's implied by the fact that the type is a `*Target`. Examples are: `SignatureTarget::verify -> BoolTarget`, `StatementTarget::has_native_type -> BoolTarget` or `OperationTypeTarget::as_custom -> (BoolTarget, HashOutTarget, Target)`.
* expose some interfaces for external usage (from introduction-pods)
* add From<MainPod> for OperationArg, add copy op!
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
---------
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
* merkletree: add keypath circuit
* merkletree-circuit: implement proof of existence verification in-circuit
* parametrize max_depth at the tree circuit
* Constrain selectors in-circuit
* implement merketree nonexistence proof circuit, and add edgecase tests
* add non-existence proofs documentation in the mdbook, mv EMPTY->EMPTY_VALUE & NULL->EMPTY_HASH, dependency clean and public exposure methods
* review comments, some extra polishing and add a test that expects wrong proofs to fail
* Add circuit to check only merkleproofs-of-existence
With this, the merkletree_circuit module offers two different circuits:
- `MerkleProofCircuit`: allows to verify both proofs of existence and proofs
non-existence with the same circuit.
- `MerkleProofExistenceCircuit`: allows to verify proofs of existence only.
In this way, if only proofs of existence are needed,
`MerkleProofExistenceCircuit` should be used, which requires less amount
of constraints than `MerkleProofCircuit`.
* Code review
---------
Co-authored-by: Ahmad <root@ahmadafuni.com>
* sync spec & code
* move primitives (merkletree) into the backend
* comment on the ops spec and link to issue #108
* typo
* fix github-ci mdbook-publish pages
* Organize docs: front and back end; custom predicates.
* Whoops forgot to hit save before git commit last time -- delete stuff moved out of values.md
* Update book/src/values.md
---------
Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>
* 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>
* Implement Containers (Dictionary,Set,Array) on top of MerkleTree. And restructure the code.
- Reorganize the code grouping backends, middleware, frontend, (crypto) primitives.
- Add types Dictionary,Set,Array at the middleware layer, so that
it can be used both by the backend and frontend. The Dictionary, Set,
Array use the merkletree differently as specified at
f2575d1524/book/src/values.md (dictionary-array-set)
- The containers introduce the trait Container, which has the
method 'cm()'. At the current version this uses a merkletree
under the hood, and the method 'cm' returns the merkle root.
- Ideally neither frontend nor backend use the MerkleTree type, and they
use the wrappers {Dictionary,Set,Array}. Note that the current commit
the MerkleTree is used at the mock-backend to check internal values, but
not at the struct types.
- updated the spec's merkletree section updating the defined interface
- add github ci to run the tests
---------
Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
* Progress towards mock MainPod verification
* add MockMainPod.pub_statements logic so that when originid==SELF it is replaced by self.id()
* Basic op checking for mock MainPOD
* More op checking
* wip
* feat: add great boy example
* feat: put examples under cfg(test)
---------
Co-authored-by: Ahmad <root@ahmadafuni.com>
Co-authored-by: arnaucube <git@arnaucube.com>
* 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>
* Remove custom statements, will do on separate branch
* Restore Merkle examples and statements table
---------
Co-authored-by: Ahmad Afuni <root@ahmadafuni.com>
Extend merkletree spec, init SignedPod section, add typos checker in CI
- extend merkletree spec, converting old hand-drawn diagrams to drawio
diagrams, and adding new diagrams (related: #6)
- init SignedPod section (related: #2)
- initial draft of the types dictionary, set, array (related: #26)
- add typos checker in CI (and correct the ones that were detected)
Note on drawio diagrams: each image file contains the metadata to edit the diagram in the draw.io website.
Add initial MerkleTree implementation, which is a wrapper on top of
Plonky2's MerkleTree, with the idea that the future iteration will
replace it by the MerkleTree specified at
https://0xparc.github.io/pod2/merkletree.html .
