* Dedupe statements during POD-building
* Fix failure to assume existence of Contains statement
* Remove possible source of non-determinism
* Faster ILP backend
* Formatting
Adds nicer errors for Podlang code, using the `annotate_snippets` crate, the same crate used by the Rust compiler to generate contextual errors. This prints a short snippet of the code containing the error within the error message, highlighting the part that needs to be fixed.
It also includes a change to the `load_module` function, changing a `Vec` function argument to a slice.
* First pass at removing batch splitting
* Refactor to separate module loading from request parsing
* Consolidate module functionality
* Tidy up comments
* Use array of modules instead of HashMap
* Formatting
* Use module hashes when importing modules
- Export MultiPodBuilder Error
- Redefine MultiPodBuilder error to wrap the frontend Error (this way we get better formatting instead of an embedded string)
- handle initial wildcard values in `MultiPodBuilder.op` just like the `MainPodBuilder` does
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.
* Remove CopyStatement constraints
* Use a constant objective, since the iterative approach already finds the minimum number of PODs
* Make solving/proving consume the builder
* Remove use of cached builder
* Create multiple PODs where resource limits for a single POD are exceeded
* HashSet -> BTreeSet determinism fix
* Fixed incorrect assignment of input PODs and added test
* Ensure only a single output POD
* Return error when reveal() called with unknown statement
* Use unreachable! for presumed-impossible cases
* Use assert_eq! rather than debug_assert_eq
* Use FIFO for topological sort
* Simplify bounds calculation
* Some more simplifications/comments
* Enforce dep_idx < idx invariant
* Incrementally solve rather than estimating slack
* Fix tests to correctly test dependencies between private and public statements
* More tidying
* Note possible optimisation of MainPodBuilder cloning of input PODs
* Fix tracking of total input POD count
* Refactor tests
* Formatting
* Small optimisation: use Vec in place of BTreeSet
* Account for automatically-inserted Contains statements
* Formatting
* Fix possible issue with copied statements
* Simplify result type given only a single result MainPod
* Remove unnecessary POD count estimate functionality
* Simplify dependency ordering and tracking
* Remove notion of multiple output PODs from solver
* Minor simplifications
* Use add_constraint instead of with
* Remove unnecessary check following assertion
* Fix handling of anchored keys given that Contains statements are not auto-inserted if they already exist
* Fix confusing dependency graph test
* Remove prove_order
* Fix deduplication and possible double-counting of public but not copied statements
* Reorder so that the output POD is the final POD
* Add more detailed tests
* Remove redundant tests
* Simplify POD counting
* More docs
* Flag more branches as unreachable
* Formatting
* Fix for changed custom batch parsing
* Multi-batch splitting
* Invoke split predicates by name, passing in full argument list
* Reorder batches to prevent failure of forward references where possible
* Rename APIs for clarity
* Simplify example
* Add more docs
* Review updates
* Remove duplicate code
* Comment topological sort algorithm
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.
The MainPodBuilder automatically adds contains statements for operations
that are created from entries. But if the contains statement was
already added manually there will be duplicates. We now track manually
added contains statements so that we don't generate duplicates when
adding statements from entries that use them.
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
* Basic frontend AST and semantic validation
* Intro statement support
* Simplify validator lifetime
* Fix arity validation
* Lowering and splitting
* Remove legacy processor and use frontend AST by default
* Use builders instead of creating middleware types directly
* Typos/formatting
* Improve error messages when overflowing a batch due to splitting
* Add FromStr implementation for NativePredicate
* Remove 'raw' fields, and switch HashHex representation to byte vector rather than string
* Simpler wrapper types for batch and intro predicate hashes
* Parse secret and public keys to their respective data structures earlier
* More detail around string escape validity
* Simplify native predicate arity handling and move method to NativePredicate impl
* Store hashes using middleware::Hash, and simplify lowering by using pre-parsed values
* Simplify predicate building
* Formatting
* Better error messages/suggestions for cases where predicate splitting fails
* Formatting
* Clippy fix
* Return error if we get a too-large int
- 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
Changed the middleware to only allow comparison of integers and to
use the implementation of Ord for i64. This matches the backend
behavior.
Also fixed a separate bug where LtEqFromEntries was producing a
NotEquals statement.
* Add container update ops
* Update src/middleware/operation.rs
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
* Update src/backends/plonky2/mainpod/mod.rs
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
* Code review
---------
Co-authored-by: Eduard S. <eduardsanou@posteo.net>
* 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>
- Bump rust version to `nightly-2025-07-02` because some of the nightly features we were using have been stabilized.
- Introduce feature `disk_cache` which enables caching to disk. Each time an artifact is retrieved from the cache it will be read and deserialized. On a cache miss the artifact will be created, serialized and stored to disk.
- Introduce feature `mem_cache` which enables caching to memory. All cached artifacts are kept in memory after they are created. The mem cache implementation avoids cloning of artifacts by extending their lifetime to `'static`. This is `unsafe` code, but I argue that this usage is safe.
- Add a `build.rs`
- When the feature `disk_cache` is enabled, the `build.rs` will inject env variables to the process with the git commit information, which is used to index the cached artifacts
- Replace all previous cached artifacts from `LazyStatic` methods that call the cache API
- Derive `Serialize, Deserialize` for all `*Target` types so that they can be serialized for caching to disk
- Add finer level of caching: now we cache the `CircuitData` and `VerifierData` independently. The reason for this is that `CircuitData` is a very big artifact which is not needed for verification. So by only accessing `VerifierData` in verification we don't pay a big overhead for reading from disk and deserializing
- Add missing artifacts to the cache: like the `CircuitData` for the `MainPod` indexed by `Params`
- Add helper types to serialize and deserialize `CircuitData`, `CommonData` and `VerifierData` with the set of gates and generators used in the recursive MainPod circuit
- Tweak the ids of our custom gates so that they remain unique when their generic parameters change
- Bugfix: several tests were using the standard `vd_set` but were using MainPod circuits with non-default parameters. This was working before because there was a bug: the MainPod circuit was reporting that the used verifier data was the standard one instead of picking the one corresponding to it's own Params.
Summary of breaking changes:
- One and only one of the features `mem_cache` or `disk_cache` need to be enabled. By default it's `mem_cache`
- To enable the `disk_cache` you need to disable the default features like this: `--no-default-features --features=backend_plonky2,zk,disk_cache`
- Removed `DEFAULT_PARAMS`, instead use `Params::default()`
- Removed `STANDARD_REC_MAIN_POD_CIRCUIT_DATA`, instead use `cache_get_standard_rec_main_pod_common_circuit_data`
- The library is now using `nightly-2025-07-02`. Some rust language features are unstable in previous versions.
The PodSigner trait was taking `&mut self` in the `sign` method, but the
signer doesn't need mutation in the Shcnorr implementation. Remove the
`mut`.
Previously the PodProver trait was also taking `&mut self` in the
`prove` method, and we had many tests creating a `mut Prover/mut
MockProver`. Remove all those `mut`.
Breaking change: `PodSigner` trait method `sign` replaces `&mut self` by
`&self`
The examples show:
- Building a Signed Pod with different types of values
- Building a MainPod
- Input SignedPod to MainPod
- Input MainPod to MainPod
- Using MainPod or MockMainPod
- Using custom predicates
- Update the `RecursivePod` trait to return `vd_set` instead of `vds_root`
- A native verifier requires the entire set to reason about the circuits that have been used in the recursive tree
- Implement serialization/deserialization for `VDSet`
- Remove `DynError` and use `BackendError` instead for middleware functions that wrap or define trait functions implemented in the backend. This is based on the fact that we will only have a single backend enabled at a time, so there's no need for a `dyn Error`
- Move the implementations of `_verify` functions to `verify` and similarly for `_prove`
- Complete the verification of a MockMainPod: the verification of input pods was missing. The inclusion of these input pods in the serialization was also missing. With this change a `MockMainPod` will grow after each recursion. This was expected from the design but was not the case because of the missing recursive native verification implementation.
* apply feedback from @arnaucube
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
* containers: add method to create new {Dict,Set,Array} with custom max_depth
* add vds_tree computation, update tree circuit interface
* add VDTree struct, add DEFAULT_VD_TREE, integrate it with MainPod,EmptyPod,frontend,etc.
* adapt frontend/serialization tests to new containers field (max_depth)
* adapt interfaces to allow using custom vd_tree in frontend & backend constructors
* rename VDTree to VDSet (and derivate namings too)
* containers 'new' always with param 'max_depth', use params.max_depth_mt_containers instead of the global constant MAX_DEPTH
* adapt after rebasing the branch to main latest changes
* apply review suggestions from @ed255
* use emptypod vd_mt_proofs (using vd_set as circuit input), merge the two existing set_targets methods of MainPodVerifyTarget
* document VDSet & vds_root
