Resolve https://github.com/0xPARC/pod2/issues/466
Now batches are identified by the root of a merkle tree that contains all the predicates (using sequential indices as keys). This means that the format to identify a custom predicate reference is still a hash + index, but the calculation of the hash is different.
The MainPod circuit now isn't limited by number of batches but instead number of custom predicates; and for each one we verify a merkle proof to verify the batch id.
I've removed a bunch of tests from lang that were testing splitting into multiple batches because there's no longer any need for that. In a future PR we'll remove the code that handles batch splitting.
Each custom predicate needs 148.2 gates (which is very close to my estimate of 142.7 in https://github.com/0xPARC/pod2/issues/466#issuecomment-3823531286 where I actually made a mistake and considered 5 predicates per batch instead of 4 in the previous Params).
I thought it would be nice to have a Predicate for the typed value so that the developer can work with predicates as values comfortably. Then I noticed that hashing a predicate required `Params` which would have been annoying for converting a `TypedValue::Predicate` to `RawValue` and this led to a small refactor over how `Params` work.
We already had some fields in the `Params` struct that determine compatibility between encoded data. They can be seen as determining a kind of ABI compatibility. In general it's better if those parameters don't change so that different circuit configurations can still verify proofs from each other. So I decided to force those parameters to be constant in the code base and not allow the user of our library to change them. Many field element serialization/deserialization functions in our code depended on those parameters, and since now they are constant many functions get rid of the `Params` argument, which simplifies the code. This includes the serialization of a `Predicate` which was required to calculate its hash.
Implement support for first order predicates in the backend.
Now a statement template can have a predicate hash or a wildcard.
## predicate <-> predicate hash constraints
To build the custom predicate table we need to calculate the custom predicate batch id, which uses the serialization of the statement templates before normalization. This serialization uses the predicate hash when the template uses a predicate (instead of a wildcard). Then in normalization we recalculate the predicate hash if it was a Batch Self.
This means that the relation between hash and predicate must be checked before and after normalization when the template is not using a wildcard. How this is achieved:
- Before normalization: the constructor of StatementTmplTarget forces that if we keep a predicate, it's hash must be equal to the pred_hash when the template has a predicate (and not a wildcard)
- After normalization: the predicate hash is calculated in the normalization and replaced in the case of the template using a predicate and it being a BatchSelf. If it was a predicate but not batch self, the old value was used which was constrained via the constructor.
See `CircuitBuilder::add_virtual_statement_tmpl` and `normalize_st_tmpl_circuit`
## Wildcard predicate resolution
It is done via `make_predicate_from_template_circuit` and is fairly simple as it's contains similar logic to `make_statement_arg_from_template_circuit` but simpler.
Resolve#448
Previously a predicate was 6 elements. Now it grows to 8 elements; and the hash is 4 elements.
Some parts of the circuit require only require equality checks with the predicate: that works with the predicate hash. Other parts require inspecting or working with particular elements in the predicate, those need the preimage of the predicate hash.
Both `StatementTarget` and `StatementTmplTarget` have been updated to include the predicate hash and optionally the predicate. When the predicate is included, constraints are automatically generated for `pred_hash = hash(pred)`. We only include the predicate when needed.
This simplifies the MerkleTree (and container) API.
Defer the max depth check when assigning the witness (merkle proof siblings) to the merkle tree circuit.
In this implementation the native Merkle Tree branches grow as much as they needed. There are no checks of max depth in the merkle tree. All keys are 256 bits (I added a debug_assert for this); so in the worst case a path will have depth 256. It can't have a longer depth because the `insert` method calls `prove_nonexistence` which errors if the key already exists; another one may exist which must be different and thus require a path <= 256 depth.
Resolve#436
This is useful for a verifier that wants to verify a MainPod that
contains a custom predicate in a public statement without
knowledge of how the custom predicate is defined.
- 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
This PR is a continuation of the work done in #276
- Fix PodType in MainPod (we were using `MockMain` instead of `Main`)
- Update anchored keys in statement template arguments to only support wildcards in the origin and literal keys as the key.
- Update the pest grammar accordingly
- Update the parser accordingly
- Rewrite the eth_dos example in a recursive manner so that we use one recursive pod for every distance increment of 1.
- I've also used the podlang to define the eth_dos custom predicates. Currently all predicates are in a single batch (previously `eth_friend` was in a different batch). With #286 we could define `eth_friend` in a different batch again.
- I was feeling a bit creative and used a format macro to pass `Value`s from rust to the podlang code.
- The eth_dos is now written using literals. This resolves https://github.com/0xPARC/pod2/issues/255
- Remove `StatementArg::WildcardValue` in favor of `StatementArg::Literal`. The `WildcardValue` was just a way to have some kind of typing for values that would be used as arguments in custom predicates. Now that we can have literals in any statement this value can be anything, so I just removed the `WildcardValue` and use `Literal` instead. On the backend it was already the case that both cases were treated the same way (after all, `WildcardValue` and `Literal` were 4 fields in the backend).
- Added a new type for Value: `PodId` so that we can use it for custom predicates that take a pod id to be used in a wildcard
- Add a mock vd_set that is empty for tests that don't use plonky2; this allows running those tests individually without paying for the expensive work of calculating the vd for various circuits.
- rename StatementTmplArg::WildcardValue to StatementTmplArg::Wildcard
* Initial commit for Podlog language
* Spell-checker thinks that 'lits' is a bad abbreviation for 'literals'
* Enable SetContains/SetNotContains
* Update language based on review feedback
* Typo/comment fix
* Make native predicates case-sensitive
* Enforce max batch size in CustomPredicateBatchBuilder
* Remove some unnecessary checks for things handled by the grammar
* Clean up more unnecessary error-checking
* Typo
* Simplify hex processing
* Replace various errors with unreachable!()
* Translate from big-endian hex string to little-endian RawValue
* Update hex en/decoding functions
* migrate from anyhow to thiserror (#190). pending polish error msgs
* Add backtrace and compartmentalize errors
- Include backtraces in the errors we generate. To get this we can't
just return a literal enum, because the backtrace requires a call.
- Related to the previous point: add methods to create errors so
we can include the backtrace conveniently without changing too much
the syntax. So instead of `Err(Error::KeyNotFound(key))` (literal
enum) it will be `Err(Error::key_not_found(key))` (method call)
- Each error should be local to its scope, and each scope should
only return its own error.
- The merkle tree should return `TreeError` and not Error
- The middleware should return `MiddlewareError` and not Error
- With a global Error we can't easily include backend/frontend types in
the error fields, so declare a `BackendError` and a `FrontendError`
and follow the pattern from the previous point
- The Pod traits should be able to return backend errors and will be
used in the frontend; for that we change them to use trait object
Error: `dyn std::error::Error`
* fix error
* apply suggestions from @arnaucube
* rename XError and XResult to Error and Result
* reorg signature
* make frontend custom error more ergonomic
* remove unnecessary feature
---------
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
* Serialization tests now pass again
* Tidy up and test more edge-cases
* Use attributes rather than custom serializer for arrays
* Add JSON Schema support
* Tests for JSON Schema generation and validation
* Add comments
* Support custom predicates
* Clippy fixes
* Make deserialization/constructor functions pub(crate)
* unify fe/be NativeOp and NativePred
* remove Origin in favour of PodId
* Combine string and hash in Key
* use middleware::AnchoredKey in frontend
* merge frontend/middleware types
* refactor custom predicates
* clean up a bit
* fix middleware custom tests
* clean up
* clean up 2
* add acronyms in typos list
* limit the number of StatementTmpl in CustomPredicate:
- add constructor method for CustomPredicate
- make size checks at the CustomPredicate creation, so that once instantiated we can assume that contains valid data
This resolves#79
* Update tests to use new interface
---------
Co-authored-by: Ahmad <root@ahmadafuni.com>
At the middleware we were defining some types that actually are dependant on the
backend no matter how we define them in the middleware.
For example, we were hardcoding the `Hash` and `Value` types and their related
behaviour (eg. `.to_fields()`) to be based on the length of 4 field elements,
but that's not a choice of the middleware, and in fact this is determined by the
backend itself. On the same time, those types and related methods do not belong
to the backend, since conceptually they are part of the middleware reasoning.
The intention of this PR is not to prematurely abstract the library, but to
avoid inconsistencies where a type or parameter is defined in the middleware to
have certain carachteristic and later in the backend it gets used differently.
The idea is that those types and parameters (eg. lengths) have a single source
of truth in the code; and in the case of the "base types" (hash, value, etc)
this is determined by the backend being used under the hood, not by a choice of
the middleware parameters.
The idea with this approach, is that the frontend & middleware should not need
to import the proving library used by the backend (eg. plonky2, plonky3, etc).
As mentioned earlier, the `Hash` and `Value` types are types belonging at the
middleware, and is the middleware who reasons about them, but depending on the
backend being used, the `Hash` and `Value` types will have different sizes. So
it's the backend being used who actually defines their nature under the hood.
For example with a plonky2 backend, these types will have a length of 4 field
elements, whereas with a plonky3 backend they will have a length of 8 field
eleements.
Note that his approach does not introduce new traits or abstract code, just
makes use of rust features to define 'base types' that are being used in the
middleware.
* Print pods from SignedPodBuilder
* Add additional print to test printing SignedPodBuilder
* Mock-prove and print MainPod
* Implement ToFields for custom predicates and dependencies
* Test: print serialization of a recursive batch
* Rearrange serialization of CustomPredicate so args_len is always in the same position
* Serialize predicates with first entry nonzero to avoid collision with padding
* Off by one error in ethdos test BatchSelf(2)
* cargo fmt
* not a typo
* Typos, trying again
* add comments detailing logic, migrate middleware::custom::tests to frontend::custom
* simplify custom predicate's frontend interfaces, making it less verbose to define Statement Template arguments
The main idea is that when defining the arguments at a statement
template, it can be done from 3 different inputs:
i. `(&str, literal)`: this is to set a POD and a field, ie. `(POD, literal("field")`)
ii. `(&str, &str)`: this is to define a origin-key wildcard pair, ie. `(src_origin, src_dest)`
iii. `Value`: this is to define a literal value, ie. `0`
