2023-02-21 21:12:03 -05:00
use core ::mem ::{ self , MaybeUninit } ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use std ::collections ::BTreeMap ;
use std ::ops ::Range ;
2023-08-23 23:29:58 +01:00
use eth_trie_utils ::partial_trie ::{ HashedPartialTrie , Node , PartialTrie } ;
2023-03-31 18:12:38 -04:00
use hashbrown ::HashMap ;
2023-05-11 02:59:02 +10:00
use itertools ::{ zip_eq , Itertools } ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use plonky2 ::field ::extension ::Extendable ;
2023-01-15 00:06:08 -08:00
use plonky2 ::fri ::FriParams ;
2023-07-06 16:25:45 -04:00
use plonky2 ::gates ::constant ::ConstantGate ;
2023-01-03 15:46:59 -08:00
use plonky2 ::gates ::noop ::NoopGate ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use plonky2 ::hash ::hash_types ::RichField ;
use plonky2 ::iop ::challenger ::RecursiveChallenger ;
2023-01-03 15:46:59 -08:00
use plonky2 ::iop ::target ::{ BoolTarget , Target } ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use plonky2 ::iop ::witness ::{ PartialWitness , WitnessWrite } ;
use plonky2 ::plonk ::circuit_builder ::CircuitBuilder ;
2023-01-15 00:06:08 -08:00
use plonky2 ::plonk ::circuit_data ::{
2023-11-28 12:23:20 -05:00
CircuitConfig , CircuitData , CommonCircuitData , VerifierCircuitData , VerifierCircuitTarget ,
2023-01-15 00:06:08 -08:00
} ;
2023-05-11 02:59:02 +10:00
use plonky2 ::plonk ::config ::{ AlgebraicHasher , GenericConfig } ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use plonky2 ::plonk ::proof ::{ ProofWithPublicInputs , ProofWithPublicInputsTarget } ;
2023-01-03 15:46:59 -08:00
use plonky2 ::recursion ::cyclic_recursion ::check_cyclic_proof_verifier_data ;
2023-03-31 18:12:38 -04:00
use plonky2 ::recursion ::dummy_circuit ::cyclic_base_proof ;
2023-04-04 15:23:19 -04:00
use plonky2 ::util ::serialization ::{
Buffer , GateSerializer , IoResult , Read , WitnessGeneratorSerializer , Write ,
} ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use plonky2 ::util ::timing ::TimingTree ;
2023-01-03 15:46:59 -08:00
use plonky2_util ::log2_ceil ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use crate ::all_stark ::{ all_cross_table_lookups , AllStark , Table , NUM_TABLES } ;
use crate ::config ::StarkConfig ;
2023-02-13 15:58:26 +01:00
use crate ::cross_table_lookup ::{
get_grand_product_challenge_set_target , verify_cross_table_lookups_circuit , CrossTableLookup ,
GrandProductChallengeSet ,
} ;
2023-06-23 11:06:51 -04:00
use crate ::generation ::GenerationInputs ;
2023-08-18 18:59:58 -04:00
use crate ::get_challenges ::observe_public_values_target ;
2023-08-07 21:00:32 +02:00
use crate ::proof ::{
2023-11-15 14:51:35 -05:00
BlockHashesTarget , BlockMetadataTarget , ExtraBlockData , ExtraBlockDataTarget , PublicValues ,
PublicValuesTarget , StarkProofWithMetadata , TrieRootsTarget ,
2023-08-07 21:00:32 +02:00
} ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
use crate ::prover ::prove ;
use crate ::recursive_verifier ::{
2023-08-19 10:46:01 -04:00
add_common_recursion_gates , add_virtual_public_values ,
2023-09-12 19:23:16 -04:00
get_memory_extra_looking_products_circuit , recursive_stark_circuit , set_public_value_targets ,
PlonkWrapperCircuit , PublicInputs , StarkWrapperCircuit ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
} ;
use crate ::stark ::Stark ;
2023-09-05 14:20:45 +01:00
use crate ::util ::h256_limbs ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
/// The recursion threshold. We end a chain of recursive proofs once we reach this size.
const THRESHOLD_DEGREE_BITS : usize = 13 ;
/// Contains all recursive circuits used in the system. For each STARK and each initial
/// `degree_bits`, this contains a chain of recursive circuits for shrinking that STARK from
/// `degree_bits` to a constant `THRESHOLD_DEGREE_BITS`. It also contains a special root circuit
/// for combining each STARK's shrunk wrapper proof into a single proof.
2023-02-21 21:12:03 -05:00
#[ derive(Eq, PartialEq, Debug) ]
2023-04-01 09:34:13 -04:00
pub struct AllRecursiveCircuits < F , C , const D : usize >
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
2023-05-11 02:59:02 +10:00
C ::Hasher : AlgebraicHasher < F > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
{
2023-01-03 15:46:59 -08:00
/// The EVM root circuit, which aggregates the (shrunk) per-table recursive proofs.
2023-04-01 09:34:13 -04:00
pub root : RootCircuitData < F , C , D > ,
pub aggregation : AggregationCircuitData < F , C , D > ,
2023-01-15 00:06:08 -08:00
/// The block circuit, which verifies an aggregation root proof and a previous block proof.
2023-04-01 09:34:13 -04:00
pub block : BlockCircuitData < F , C , D > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
/// Holds chains of circuits for each table and for each initial `degree_bits`.
2023-04-01 09:34:13 -04:00
by_table : [ RecursiveCircuitsForTable < F , C , D > ; NUM_TABLES ] ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
2023-01-03 15:46:59 -08:00
/// Data for the EVM root circuit, which is used to combine each STARK's shrunk wrapper proof
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
/// into a single proof.
2023-02-21 21:12:03 -05:00
#[ derive(Eq, PartialEq, Debug) ]
2023-04-01 09:34:13 -04:00
pub struct RootCircuitData < F , C , const D : usize >
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
{
2023-02-21 21:12:03 -05:00
pub circuit : CircuitData < F , C , D > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
proof_with_pis : [ ProofWithPublicInputsTarget < D > ; NUM_TABLES ] ,
/// For each table, various inner circuits may be used depending on the initial table size.
/// This target holds the index of the circuit (within `final_circuits()`) that was used.
index_verifier_data : [ Target ; NUM_TABLES ] ,
2023-06-21 20:05:39 +02:00
/// Public inputs containing public values.
public_values : PublicValuesTarget ,
2023-01-03 15:46:59 -08:00
/// Public inputs used for cyclic verification. These aren't actually used for EVM root
/// proofs; the circuit has them just to match the structure of aggregation proofs.
cyclic_vk : VerifierCircuitTarget ,
}
2023-02-21 21:12:03 -05:00
impl < F , C , const D : usize > RootCircuitData < F , C , D >
where
F : RichField + Extendable < D > ,
C : GenericConfig < D , F = F > ,
{
2023-11-13 09:26:56 -05:00
fn to_buffer (
2023-02-21 21:12:03 -05:00
& self ,
buffer : & mut Vec < u8 > ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < ( ) > {
buffer . write_circuit_data ( & self . circuit , gate_serializer , generator_serializer ) ? ;
for proof in & self . proof_with_pis {
buffer . write_target_proof_with_public_inputs ( proof ) ? ;
}
for index in self . index_verifier_data {
buffer . write_target ( index ) ? ;
}
2023-06-21 20:05:39 +02:00
self . public_values . to_buffer ( buffer ) ? ;
2023-02-21 21:12:03 -05:00
buffer . write_target_verifier_circuit ( & self . cyclic_vk ) ? ;
Ok ( ( ) )
}
2023-11-13 09:26:56 -05:00
fn from_buffer (
2023-02-21 21:12:03 -05:00
buffer : & mut Buffer ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < Self > {
let circuit = buffer . read_circuit_data ( gate_serializer , generator_serializer ) ? ;
let mut proof_with_pis = Vec ::with_capacity ( NUM_TABLES ) ;
for _ in 0 .. NUM_TABLES {
proof_with_pis . push ( buffer . read_target_proof_with_public_inputs ( ) ? ) ;
}
let mut index_verifier_data = Vec ::with_capacity ( NUM_TABLES ) ;
for _ in 0 .. NUM_TABLES {
index_verifier_data . push ( buffer . read_target ( ) ? ) ;
}
2023-06-21 20:05:39 +02:00
let public_values = PublicValuesTarget ::from_buffer ( buffer ) ? ;
2023-02-21 21:12:03 -05:00
let cyclic_vk = buffer . read_target_verifier_circuit ( ) ? ;
Ok ( Self {
circuit ,
proof_with_pis : proof_with_pis . try_into ( ) . unwrap ( ) ,
index_verifier_data : index_verifier_data . try_into ( ) . unwrap ( ) ,
2023-06-21 20:05:39 +02:00
public_values ,
2023-02-21 21:12:03 -05:00
cyclic_vk ,
} )
}
}
2023-01-03 15:46:59 -08:00
/// Data for the aggregation circuit, which is used to compress two proofs into one. Each inner
/// proof can be either an EVM root proof or another aggregation proof.
2023-02-21 21:12:03 -05:00
#[ derive(Eq, PartialEq, Debug) ]
2023-04-01 09:34:13 -04:00
pub struct AggregationCircuitData < F , C , const D : usize >
2023-01-03 15:46:59 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
2023-01-03 15:46:59 -08:00
{
2023-02-21 21:12:03 -05:00
pub circuit : CircuitData < F , C , D > ,
2023-01-03 15:46:59 -08:00
lhs : AggregationChildTarget < D > ,
rhs : AggregationChildTarget < D > ,
2023-06-21 20:05:39 +02:00
public_values : PublicValuesTarget ,
2023-01-03 15:46:59 -08:00
cyclic_vk : VerifierCircuitTarget ,
}
2023-02-21 21:12:03 -05:00
impl < F , C , const D : usize > AggregationCircuitData < F , C , D >
where
F : RichField + Extendable < D > ,
C : GenericConfig < D , F = F > ,
{
2023-11-13 09:26:56 -05:00
fn to_buffer (
2023-02-21 21:12:03 -05:00
& self ,
buffer : & mut Vec < u8 > ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < ( ) > {
buffer . write_circuit_data ( & self . circuit , gate_serializer , generator_serializer ) ? ;
buffer . write_target_verifier_circuit ( & self . cyclic_vk ) ? ;
2023-06-21 20:05:39 +02:00
self . public_values . to_buffer ( buffer ) ? ;
2023-02-21 21:12:03 -05:00
self . lhs . to_buffer ( buffer ) ? ;
self . rhs . to_buffer ( buffer ) ? ;
Ok ( ( ) )
}
2023-11-13 09:26:56 -05:00
fn from_buffer (
2023-02-21 21:12:03 -05:00
buffer : & mut Buffer ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < Self > {
let circuit = buffer . read_circuit_data ( gate_serializer , generator_serializer ) ? ;
let cyclic_vk = buffer . read_target_verifier_circuit ( ) ? ;
2023-06-21 20:05:39 +02:00
let public_values = PublicValuesTarget ::from_buffer ( buffer ) ? ;
2023-02-21 21:12:03 -05:00
let lhs = AggregationChildTarget ::from_buffer ( buffer ) ? ;
let rhs = AggregationChildTarget ::from_buffer ( buffer ) ? ;
Ok ( Self {
circuit ,
lhs ,
rhs ,
2023-06-21 20:05:39 +02:00
public_values ,
2023-02-21 21:12:03 -05:00
cyclic_vk ,
} )
}
}
#[ derive(Eq, PartialEq, Debug) ]
2023-11-13 09:26:56 -05:00
struct AggregationChildTarget < const D : usize > {
2023-01-03 15:46:59 -08:00
is_agg : BoolTarget ,
agg_proof : ProofWithPublicInputsTarget < D > ,
evm_proof : ProofWithPublicInputsTarget < D > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
2023-02-21 21:12:03 -05:00
impl < const D : usize > AggregationChildTarget < D > {
2023-11-13 09:26:56 -05:00
fn to_buffer ( & self , buffer : & mut Vec < u8 > ) -> IoResult < ( ) > {
2023-02-21 21:12:03 -05:00
buffer . write_target_bool ( self . is_agg ) ? ;
buffer . write_target_proof_with_public_inputs ( & self . agg_proof ) ? ;
buffer . write_target_proof_with_public_inputs ( & self . evm_proof ) ? ;
Ok ( ( ) )
}
2023-11-13 09:26:56 -05:00
fn from_buffer ( buffer : & mut Buffer ) -> IoResult < Self > {
2023-02-21 21:12:03 -05:00
let is_agg = buffer . read_target_bool ( ) ? ;
let agg_proof = buffer . read_target_proof_with_public_inputs ( ) ? ;
let evm_proof = buffer . read_target_proof_with_public_inputs ( ) ? ;
Ok ( Self {
is_agg ,
agg_proof ,
evm_proof ,
} )
}
2023-08-07 21:00:32 +02:00
2023-11-13 09:26:56 -05:00
fn public_values < F : RichField + Extendable < D > > (
2023-08-07 21:00:32 +02:00
& self ,
builder : & mut CircuitBuilder < F , D > ,
) -> PublicValuesTarget {
let agg_pv = PublicValuesTarget ::from_public_inputs ( & self . agg_proof . public_inputs ) ;
let evm_pv = PublicValuesTarget ::from_public_inputs ( & self . evm_proof . public_inputs ) ;
PublicValuesTarget ::select ( builder , self . is_agg , agg_pv , evm_pv )
}
2023-02-21 21:12:03 -05:00
}
#[ derive(Eq, PartialEq, Debug) ]
2023-04-01 09:34:13 -04:00
pub struct BlockCircuitData < F , C , const D : usize >
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
2023-01-15 00:06:08 -08:00
{
2023-02-21 21:12:03 -05:00
pub circuit : CircuitData < F , C , D > ,
2023-01-15 00:06:08 -08:00
has_parent_block : BoolTarget ,
parent_block_proof : ProofWithPublicInputsTarget < D > ,
agg_root_proof : ProofWithPublicInputsTarget < D > ,
2023-06-21 20:05:39 +02:00
public_values : PublicValuesTarget ,
2023-01-15 00:06:08 -08:00
cyclic_vk : VerifierCircuitTarget ,
}
2023-02-21 21:12:03 -05:00
impl < F , C , const D : usize > BlockCircuitData < F , C , D >
where
F : RichField + Extendable < D > ,
C : GenericConfig < D , F = F > ,
{
2023-11-13 09:26:56 -05:00
fn to_buffer (
2023-02-21 21:12:03 -05:00
& self ,
buffer : & mut Vec < u8 > ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < ( ) > {
buffer . write_circuit_data ( & self . circuit , gate_serializer , generator_serializer ) ? ;
buffer . write_target_bool ( self . has_parent_block ) ? ;
buffer . write_target_proof_with_public_inputs ( & self . parent_block_proof ) ? ;
buffer . write_target_proof_with_public_inputs ( & self . agg_root_proof ) ? ;
2023-06-21 20:05:39 +02:00
self . public_values . to_buffer ( buffer ) ? ;
2023-02-21 21:12:03 -05:00
buffer . write_target_verifier_circuit ( & self . cyclic_vk ) ? ;
Ok ( ( ) )
}
2023-11-13 09:26:56 -05:00
fn from_buffer (
2023-02-21 21:12:03 -05:00
buffer : & mut Buffer ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < Self > {
let circuit = buffer . read_circuit_data ( gate_serializer , generator_serializer ) ? ;
let has_parent_block = buffer . read_target_bool ( ) ? ;
let parent_block_proof = buffer . read_target_proof_with_public_inputs ( ) ? ;
let agg_root_proof = buffer . read_target_proof_with_public_inputs ( ) ? ;
2023-06-21 20:05:39 +02:00
let public_values = PublicValuesTarget ::from_buffer ( buffer ) ? ;
2023-02-21 21:12:03 -05:00
let cyclic_vk = buffer . read_target_verifier_circuit ( ) ? ;
Ok ( Self {
circuit ,
has_parent_block ,
parent_block_proof ,
agg_root_proof ,
2023-06-21 20:05:39 +02:00
public_values ,
2023-02-21 21:12:03 -05:00
cyclic_vk ,
} )
}
}
2023-04-01 09:34:13 -04:00
impl < F , C , const D : usize > AllRecursiveCircuits < F , C , D >
2023-01-15 00:06:08 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > + 'static ,
2023-05-11 02:59:02 +10:00
C ::Hasher : AlgebraicHasher < F > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
{
2023-02-21 21:12:03 -05:00
pub fn to_bytes (
& self ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < Vec < u8 > > {
// TODO: would be better to initialize it dynamically based on the supported max degree.
let mut buffer = Vec ::with_capacity ( 1 < < 34 ) ;
self . root
. to_buffer ( & mut buffer , gate_serializer , generator_serializer ) ? ;
self . aggregation
. to_buffer ( & mut buffer , gate_serializer , generator_serializer ) ? ;
self . block
. to_buffer ( & mut buffer , gate_serializer , generator_serializer ) ? ;
for table in & self . by_table {
table . to_buffer ( & mut buffer , gate_serializer , generator_serializer ) ? ;
}
Ok ( buffer )
}
pub fn from_bytes (
bytes : & [ u8 ] ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < Self > {
2023-06-24 18:25:49 -04:00
let mut buffer = Buffer ::new ( bytes ) ;
2023-02-21 21:12:03 -05:00
let root =
RootCircuitData ::from_buffer ( & mut buffer , gate_serializer , generator_serializer ) ? ;
let aggregation = AggregationCircuitData ::from_buffer (
& mut buffer ,
gate_serializer ,
generator_serializer ,
) ? ;
let block =
BlockCircuitData ::from_buffer ( & mut buffer , gate_serializer , generator_serializer ) ? ;
// Tricky use of MaybeUninit to remove the need for implementing Debug
// for all underlying types, necessary to convert a by_table Vec to an array.
let by_table = {
let mut by_table : [ MaybeUninit < RecursiveCircuitsForTable < F , C , D > > ; NUM_TABLES ] =
unsafe { MaybeUninit ::uninit ( ) . assume_init ( ) } ;
for table in & mut by_table [ .. ] {
let value = RecursiveCircuitsForTable ::from_buffer (
& mut buffer ,
gate_serializer ,
generator_serializer ,
) ? ;
* table = MaybeUninit ::new ( value ) ;
}
unsafe {
mem ::transmute ::< _ , [ RecursiveCircuitsForTable < F , C , D > ; NUM_TABLES ] > ( by_table )
}
} ;
Ok ( Self {
root ,
aggregation ,
block ,
by_table ,
} )
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
/// Preprocess all recursive circuits used by the system.
pub fn new (
all_stark : & AllStark < F , D > ,
2023-04-02 11:35:54 -04:00
degree_bits_ranges : & [ Range < usize > ; NUM_TABLES ] ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
stark_config : & StarkConfig ,
) -> Self {
Cross-table lookup for arithmetic stark (#905)
* First draft of linking arithmetic Stark into the CTL mechanism.
* Handle {ADD,SUB,MUL}FP254 operations explicitly in `modular.rs`.
* Adjust argument order; add tests.
* Add CTLs for ADD, MUL, SUB, LT and GT.
* Add CTLs for {ADD,MUL,SUB}MOD, DIV and MOD.
* Add CTLs for {ADD,MUL,SUB}FP254 operations.
* Refactor the CPU/arithmetic CTL mapping; add some documentation.
* Minor comment fixes.
* Combine addcy CTLs at the expense of repeated constraint evaluation.
* Combine addcy CTLs at the expense of repeated constraint evaluation.
* Merge `*FP254` CTL into main CTL; rename some registers.
* Connect extra argument from CPU in binary ops to facilitate combining with ternary ops.
* Merge modular ops CTL into main CTL.
* Refactor DIV and MOD code into its own module.
* Merge DIV and MOD into arithmetic CTL.
* Clippy.
* Fixes related to merge.
* Simplify register naming.
* Generate u16 BN254 modulus limbs at compile time.
* Clippy.
* Add degree bits ranges for Arithmetic table.
2023-05-11 03:29:06 +10:00
let arithmetic = RecursiveCircuitsForTable ::new (
Table ::Arithmetic ,
& all_stark . arithmetic_stark ,
2023-09-19 18:38:40 -04:00
degree_bits_ranges [ Table ::Arithmetic as usize ] . clone ( ) ,
Cross-table lookup for arithmetic stark (#905)
* First draft of linking arithmetic Stark into the CTL mechanism.
* Handle {ADD,SUB,MUL}FP254 operations explicitly in `modular.rs`.
* Adjust argument order; add tests.
* Add CTLs for ADD, MUL, SUB, LT and GT.
* Add CTLs for {ADD,MUL,SUB}MOD, DIV and MOD.
* Add CTLs for {ADD,MUL,SUB}FP254 operations.
* Refactor the CPU/arithmetic CTL mapping; add some documentation.
* Minor comment fixes.
* Combine addcy CTLs at the expense of repeated constraint evaluation.
* Combine addcy CTLs at the expense of repeated constraint evaluation.
* Merge `*FP254` CTL into main CTL; rename some registers.
* Connect extra argument from CPU in binary ops to facilitate combining with ternary ops.
* Merge modular ops CTL into main CTL.
* Refactor DIV and MOD code into its own module.
* Merge DIV and MOD into arithmetic CTL.
* Clippy.
* Fixes related to merge.
* Simplify register naming.
* Generate u16 BN254 modulus limbs at compile time.
* Clippy.
* Add degree bits ranges for Arithmetic table.
2023-05-11 03:29:06 +10:00
& all_stark . cross_table_lookups ,
stark_config ,
) ;
2023-09-12 14:45:37 -04:00
let byte_packing = RecursiveCircuitsForTable ::new (
Table ::BytePacking ,
& all_stark . byte_packing_stark ,
2023-09-19 18:38:40 -04:00
degree_bits_ranges [ Table ::BytePacking as usize ] . clone ( ) ,
Cross-table lookup for arithmetic stark (#905)
* First draft of linking arithmetic Stark into the CTL mechanism.
* Handle {ADD,SUB,MUL}FP254 operations explicitly in `modular.rs`.
* Adjust argument order; add tests.
* Add CTLs for ADD, MUL, SUB, LT and GT.
* Add CTLs for {ADD,MUL,SUB}MOD, DIV and MOD.
* Add CTLs for {ADD,MUL,SUB}FP254 operations.
* Refactor the CPU/arithmetic CTL mapping; add some documentation.
* Minor comment fixes.
* Combine addcy CTLs at the expense of repeated constraint evaluation.
* Combine addcy CTLs at the expense of repeated constraint evaluation.
* Merge `*FP254` CTL into main CTL; rename some registers.
* Connect extra argument from CPU in binary ops to facilitate combining with ternary ops.
* Merge modular ops CTL into main CTL.
* Refactor DIV and MOD code into its own module.
* Merge DIV and MOD into arithmetic CTL.
* Clippy.
* Fixes related to merge.
* Simplify register naming.
* Generate u16 BN254 modulus limbs at compile time.
* Clippy.
* Add degree bits ranges for Arithmetic table.
2023-05-11 03:29:06 +10:00
& all_stark . cross_table_lookups ,
stark_config ,
) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let cpu = RecursiveCircuitsForTable ::new (
Table ::Cpu ,
& all_stark . cpu_stark ,
2023-09-19 18:38:40 -04:00
degree_bits_ranges [ Table ::Cpu as usize ] . clone ( ) ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
& all_stark . cross_table_lookups ,
stark_config ,
) ;
let keccak = RecursiveCircuitsForTable ::new (
Table ::Keccak ,
& all_stark . keccak_stark ,
2023-09-19 18:38:40 -04:00
degree_bits_ranges [ Table ::Keccak as usize ] . clone ( ) ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
& all_stark . cross_table_lookups ,
stark_config ,
) ;
let keccak_sponge = RecursiveCircuitsForTable ::new (
Table ::KeccakSponge ,
& all_stark . keccak_sponge_stark ,
2023-09-19 18:38:40 -04:00
degree_bits_ranges [ Table ::KeccakSponge as usize ] . clone ( ) ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
& all_stark . cross_table_lookups ,
stark_config ,
) ;
let logic = RecursiveCircuitsForTable ::new (
Table ::Logic ,
& all_stark . logic_stark ,
2023-09-19 18:38:40 -04:00
degree_bits_ranges [ Table ::Logic as usize ] . clone ( ) ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
& all_stark . cross_table_lookups ,
stark_config ,
) ;
let memory = RecursiveCircuitsForTable ::new (
Table ::Memory ,
& all_stark . memory_stark ,
2023-09-19 18:38:40 -04:00
degree_bits_ranges [ Table ::Memory as usize ] . clone ( ) ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
& all_stark . cross_table_lookups ,
stark_config ,
) ;
2023-09-12 14:45:37 -04:00
let by_table = [
arithmetic ,
byte_packing ,
cpu ,
keccak ,
keccak_sponge ,
logic ,
memory ,
] ;
2023-06-21 20:05:39 +02:00
let root = Self ::create_root_circuit ( & by_table , stark_config ) ;
2023-01-03 15:46:59 -08:00
let aggregation = Self ::create_aggregation_circuit ( & root ) ;
2023-01-15 00:06:08 -08:00
let block = Self ::create_block_circuit ( & aggregation ) ;
2023-01-03 15:46:59 -08:00
Self {
root ,
aggregation ,
2023-01-15 00:06:08 -08:00
block ,
2023-01-03 15:46:59 -08:00
by_table ,
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
2023-11-28 12:23:20 -05:00
/// Expand the preprocessed STARK table circuits with the provided ranges.
///
/// If a range for a given table is contained within the current one, this will be a no-op.
/// Otherwise, it will add the circuits for the missing table sizes, and regenerate the upper circuits.
pub fn expand (
& mut self ,
all_stark : & AllStark < F , D > ,
degree_bits_ranges : & [ Range < usize > ; NUM_TABLES ] ,
stark_config : & StarkConfig ,
) {
self . by_table [ Table ::Arithmetic as usize ] . expand (
Table ::Arithmetic ,
& all_stark . arithmetic_stark ,
degree_bits_ranges [ Table ::Arithmetic as usize ] . clone ( ) ,
& all_stark . cross_table_lookups ,
stark_config ,
) ;
self . by_table [ Table ::BytePacking as usize ] . expand (
Table ::BytePacking ,
& all_stark . byte_packing_stark ,
degree_bits_ranges [ Table ::BytePacking as usize ] . clone ( ) ,
& all_stark . cross_table_lookups ,
stark_config ,
) ;
self . by_table [ Table ::Cpu as usize ] . expand (
Table ::Cpu ,
& all_stark . cpu_stark ,
degree_bits_ranges [ Table ::Cpu as usize ] . clone ( ) ,
& all_stark . cross_table_lookups ,
stark_config ,
) ;
self . by_table [ Table ::Keccak as usize ] . expand (
Table ::Keccak ,
& all_stark . keccak_stark ,
degree_bits_ranges [ Table ::Keccak as usize ] . clone ( ) ,
& all_stark . cross_table_lookups ,
stark_config ,
) ;
self . by_table [ Table ::KeccakSponge as usize ] . expand (
Table ::KeccakSponge ,
& all_stark . keccak_sponge_stark ,
degree_bits_ranges [ Table ::KeccakSponge as usize ] . clone ( ) ,
& all_stark . cross_table_lookups ,
stark_config ,
) ;
self . by_table [ Table ::Logic as usize ] . expand (
Table ::Logic ,
& all_stark . logic_stark ,
degree_bits_ranges [ Table ::Logic as usize ] . clone ( ) ,
& all_stark . cross_table_lookups ,
stark_config ,
) ;
self . by_table [ Table ::Memory as usize ] . expand (
Table ::Memory ,
& all_stark . memory_stark ,
degree_bits_ranges [ Table ::Memory as usize ] . clone ( ) ,
& all_stark . cross_table_lookups ,
stark_config ,
) ;
// Regenerate the upper circuits.
self . root = Self ::create_root_circuit ( & self . by_table , stark_config ) ;
self . aggregation = Self ::create_aggregation_circuit ( & self . root ) ;
self . block = Self ::create_block_circuit ( & self . aggregation ) ;
}
/// Outputs the `VerifierCircuitData` needed to verify any block proof
/// generated by an honest prover.
pub fn final_verifier_data ( & self ) -> VerifierCircuitData < F , C , D > {
self . block . circuit . verifier_data ( )
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
fn create_root_circuit (
2023-04-01 09:34:13 -04:00
by_table : & [ RecursiveCircuitsForTable < F , C , D > ; NUM_TABLES ] ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
stark_config : & StarkConfig ,
2023-04-01 09:34:13 -04:00
) -> RootCircuitData < F , C , D > {
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let inner_common_data : [ _ ; NUM_TABLES ] =
2023-01-30 08:51:33 -08:00
core ::array ::from_fn ( | i | & by_table [ i ] . final_circuits ( ) [ 0 ] . common ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let mut builder = CircuitBuilder ::new ( CircuitConfig ::standard_recursion_config ( ) ) ;
2023-04-14 21:55:44 +08:00
2023-06-21 20:05:39 +02:00
let public_values = add_virtual_public_values ( & mut builder ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let recursive_proofs =
2023-02-25 08:55:55 -08:00
core ::array ::from_fn ( | i | builder . add_virtual_proof_with_pis ( inner_common_data [ i ] ) ) ;
2023-01-30 08:51:33 -08:00
let pis : [ _ ; NUM_TABLES ] = core ::array ::from_fn ( | i | {
2023-05-11 02:59:02 +10:00
PublicInputs ::< Target , < C ::Hasher as AlgebraicHasher < F > > ::AlgebraicPermutation > ::from_vec (
2023-04-01 09:34:13 -04:00
& recursive_proofs [ i ] . public_inputs ,
stark_config ,
)
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
} ) ;
2023-01-30 08:51:33 -08:00
let index_verifier_data = core ::array ::from_fn ( | _i | builder . add_virtual_target ( ) ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
2023-05-11 02:59:02 +10:00
let mut challenger = RecursiveChallenger ::< F , C ::Hasher , D > ::new ( & mut builder ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
for pi in & pis {
for h in & pi . trace_cap {
challenger . observe_elements ( h ) ;
}
}
2023-08-18 18:59:58 -04:00
observe_public_values_target ::< F , C , D > ( & mut challenger , & public_values ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let ctl_challenges = get_grand_product_challenge_set_target (
& mut builder ,
& mut challenger ,
stark_config . num_challenges ,
) ;
// Check that the correct CTL challenges are used in every proof.
for pi in & pis {
for i in 0 .. stark_config . num_challenges {
builder . connect (
ctl_challenges . challenges [ i ] . beta ,
pi . ctl_challenges . challenges [ i ] . beta ,
) ;
builder . connect (
ctl_challenges . challenges [ i ] . gamma ,
pi . ctl_challenges . challenges [ i ] . gamma ,
) ;
}
}
let state = challenger . compact ( & mut builder ) ;
2023-05-11 02:59:02 +10:00
for ( & before , & s ) in zip_eq ( state . as_ref ( ) , pis [ 0 ] . challenger_state_before . as_ref ( ) ) {
builder . connect ( before , s ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
// Check that the challenger state is consistent between proofs.
for i in 1 .. NUM_TABLES {
2023-05-11 02:59:02 +10:00
for ( & before , & after ) in zip_eq (
pis [ i ] . challenger_state_before . as_ref ( ) ,
pis [ i - 1 ] . challenger_state_after . as_ref ( ) ,
) {
builder . connect ( before , after ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
}
2023-09-12 14:45:37 -04:00
// Extra products to add to the looked last value.
// Only necessary for the Memory values.
2023-05-10 17:35:28 -04:00
let mut extra_looking_products =
2023-09-12 14:45:37 -04:00
vec! [ vec! [ builder . one ( ) ; stark_config . num_challenges ] ; NUM_TABLES ] ;
2023-04-14 21:55:44 +08:00
// Memory
2023-09-12 14:45:37 -04:00
extra_looking_products [ Table ::Memory as usize ] = ( 0 .. stark_config . num_challenges )
2023-08-10 08:52:21 -04:00
. map ( | c | {
2023-08-19 10:46:01 -04:00
get_memory_extra_looking_products_circuit (
2023-05-10 15:37:05 -04:00
& mut builder ,
2023-06-21 20:05:39 +02:00
& public_values ,
2023-05-10 15:37:05 -04:00
ctl_challenges . challenges [ c ] ,
2023-08-10 08:52:21 -04:00
)
} )
. collect_vec ( ) ;
2023-04-14 21:55:44 +08:00
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
// Verify the CTL checks.
2023-02-10 21:47:51 -08:00
verify_cross_table_lookups_circuit ::< F , D > (
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
& mut builder ,
all_cross_table_lookups ( ) ,
2023-09-11 14:11:13 -04:00
pis . map ( | p | p . ctl_zs_first ) ,
2023-04-14 21:55:44 +08:00
extra_looking_products ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
stark_config ,
) ;
for ( i , table_circuits ) in by_table . iter ( ) . enumerate ( ) {
let final_circuits = table_circuits . final_circuits ( ) ;
for final_circuit in & final_circuits {
assert_eq! (
& final_circuit . common , inner_common_data [ i ] ,
" common_data mismatch "
) ;
}
let mut possible_vks = final_circuits
. into_iter ( )
. map ( | c | builder . constant_verifier_data ( & c . verifier_only ) )
. collect_vec ( ) ;
// random_access_verifier_data expects a vector whose length is a power of two.
// To satisfy this, we will just add some duplicates of the first VK.
while ! possible_vks . len ( ) . is_power_of_two ( ) {
possible_vks . push ( possible_vks [ 0 ] . clone ( ) ) ;
}
let inner_verifier_data =
builder . random_access_verifier_data ( index_verifier_data [ i ] , possible_vks ) ;
2023-04-01 09:34:13 -04:00
builder . verify_proof ::< C > (
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
& recursive_proofs [ i ] ,
& inner_verifier_data ,
inner_common_data [ i ] ,
) ;
}
2023-01-03 15:46:59 -08:00
// We want EVM root proofs to have the exact same structure as aggregation proofs, so we add
// public inputs for cyclic verification, even though they'll be ignored.
let cyclic_vk = builder . add_verifier_data_public_inputs ( ) ;
2023-07-06 16:25:45 -04:00
builder . add_gate (
ConstantGate ::new ( inner_common_data [ 0 ] . config . num_constants ) ,
vec! [ ] ,
) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
RootCircuitData {
2023-04-01 09:34:13 -04:00
circuit : builder . build ::< C > ( ) ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
proof_with_pis : recursive_proofs ,
index_verifier_data ,
2023-06-21 20:05:39 +02:00
public_values ,
2023-01-03 15:46:59 -08:00
cyclic_vk ,
}
}
fn create_aggregation_circuit (
2023-04-01 09:34:13 -04:00
root : & RootCircuitData < F , C , D > ,
) -> AggregationCircuitData < F , C , D > {
2023-01-03 15:46:59 -08:00
let mut builder = CircuitBuilder ::< F , D > ::new ( root . circuit . common . config . clone ( ) ) ;
2023-06-21 20:05:39 +02:00
let public_values = add_virtual_public_values ( & mut builder ) ;
2023-01-03 15:46:59 -08:00
let cyclic_vk = builder . add_verifier_data_public_inputs ( ) ;
let lhs = Self ::add_agg_child ( & mut builder , root ) ;
let rhs = Self ::add_agg_child ( & mut builder , root ) ;
2023-08-07 21:00:32 +02:00
let lhs_public_values = lhs . public_values ( & mut builder ) ;
let rhs_public_values = rhs . public_values ( & mut builder ) ;
2023-08-21 23:32:53 +01:00
// Connect all block hash values
BlockHashesTarget ::connect (
& mut builder ,
public_values . block_hashes ,
lhs_public_values . block_hashes ,
) ;
BlockHashesTarget ::connect (
& mut builder ,
public_values . block_hashes ,
rhs_public_values . block_hashes ,
) ;
2023-08-07 21:00:32 +02:00
// Connect all block metadata values.
BlockMetadataTarget ::connect (
& mut builder ,
public_values . block_metadata ,
lhs_public_values . block_metadata ,
) ;
BlockMetadataTarget ::connect (
& mut builder ,
public_values . block_metadata ,
rhs_public_values . block_metadata ,
) ;
// Connect aggregation `trie_roots_before` with lhs `trie_roots_before`.
TrieRootsTarget ::connect (
& mut builder ,
public_values . trie_roots_before ,
lhs_public_values . trie_roots_before ,
) ;
// Connect aggregation `trie_roots_after` with rhs `trie_roots_after`.
TrieRootsTarget ::connect (
& mut builder ,
public_values . trie_roots_after ,
rhs_public_values . trie_roots_after ,
) ;
// Connect lhs `trie_roots_after` with rhs `trie_roots_before`.
TrieRootsTarget ::connect (
& mut builder ,
lhs_public_values . trie_roots_after ,
rhs_public_values . trie_roots_before ,
) ;
2023-08-23 23:29:58 +01:00
Self ::connect_extra_public_values (
& mut builder ,
& public_values . extra_block_data ,
& lhs_public_values . extra_block_data ,
& rhs_public_values . extra_block_data ,
) ;
2023-01-03 15:46:59 -08:00
// Pad to match the root circuit's degree.
while log2_ceil ( builder . num_gates ( ) ) < root . circuit . common . degree_bits ( ) {
builder . add_gate ( NoopGate , vec! [ ] ) ;
}
2023-04-01 09:34:13 -04:00
let circuit = builder . build ::< C > ( ) ;
2023-01-03 15:46:59 -08:00
AggregationCircuitData {
circuit ,
lhs ,
rhs ,
2023-06-21 20:05:39 +02:00
public_values ,
2023-01-03 15:46:59 -08:00
cyclic_vk ,
}
}
2023-08-23 23:29:58 +01:00
fn connect_extra_public_values (
builder : & mut CircuitBuilder < F , D > ,
pvs : & ExtraBlockDataTarget ,
lhs : & ExtraBlockDataTarget ,
rhs : & ExtraBlockDataTarget ,
) {
2023-09-11 15:47:33 +01:00
// Connect genesis state root values.
2023-10-03 17:47:10 +02:00
for ( & limb0 , & limb1 ) in pvs
. genesis_state_trie_root
. iter ( )
. zip ( & rhs . genesis_state_trie_root )
{
2023-09-11 15:47:33 +01:00
builder . connect ( limb0 , limb1 ) ;
}
2023-10-03 17:47:10 +02:00
for ( & limb0 , & limb1 ) in pvs
. genesis_state_trie_root
. iter ( )
. zip ( & lhs . genesis_state_trie_root )
{
2023-09-26 12:21:29 -04:00
builder . connect ( limb0 , limb1 ) ;
}
2023-09-11 15:47:33 +01:00
2023-08-23 23:29:58 +01:00
// Connect the transaction number in public values to the lhs and rhs values correctly.
builder . connect ( pvs . txn_number_before , lhs . txn_number_before ) ;
builder . connect ( pvs . txn_number_after , rhs . txn_number_after ) ;
2023-11-27 10:24:11 -05:00
// Connect lhs `txn_number_after` with rhs `txn_number_before`.
2023-08-23 23:29:58 +01:00
builder . connect ( lhs . txn_number_after , rhs . txn_number_before ) ;
// Connect the gas used in public values to the lhs and rhs values correctly.
2023-11-17 10:01:26 -05:00
builder . connect ( pvs . gas_used_before , lhs . gas_used_before ) ;
builder . connect ( pvs . gas_used_after , rhs . gas_used_after ) ;
2023-08-23 23:29:58 +01:00
2023-11-27 10:24:11 -05:00
// Connect lhs `gas_used_after` with rhs `gas_used_before`.
2023-11-17 10:01:26 -05:00
builder . connect ( lhs . gas_used_after , rhs . gas_used_before ) ;
2023-08-23 23:29:58 +01:00
// Connect the `block_bloom` in public values to the lhs and rhs values correctly.
for ( & limb0 , & limb1 ) in pvs . block_bloom_after . iter ( ) . zip ( & rhs . block_bloom_after ) {
builder . connect ( limb0 , limb1 ) ;
}
for ( & limb0 , & limb1 ) in pvs . block_bloom_before . iter ( ) . zip ( & lhs . block_bloom_before ) {
builder . connect ( limb0 , limb1 ) ;
}
2023-11-27 10:24:11 -05:00
// Connect lhs `block_bloom_after` with rhs `block_bloom_before`.
2023-08-23 23:29:58 +01:00
for ( & limb0 , & limb1 ) in lhs . block_bloom_after . iter ( ) . zip ( & rhs . block_bloom_before ) {
builder . connect ( limb0 , limb1 ) ;
}
}
2023-01-03 15:46:59 -08:00
fn add_agg_child (
builder : & mut CircuitBuilder < F , D > ,
2023-04-01 09:34:13 -04:00
root : & RootCircuitData < F , C , D > ,
2023-01-03 15:46:59 -08:00
) -> AggregationChildTarget < D > {
let common = & root . circuit . common ;
let root_vk = builder . constant_verifier_data ( & root . circuit . verifier_only ) ;
let is_agg = builder . add_virtual_bool_target_safe ( ) ;
2023-02-25 08:55:55 -08:00
let agg_proof = builder . add_virtual_proof_with_pis ( common ) ;
let evm_proof = builder . add_virtual_proof_with_pis ( common ) ;
2023-01-03 15:46:59 -08:00
builder
2023-04-01 09:34:13 -04:00
. conditionally_verify_cyclic_proof ::< C > (
2023-01-03 15:46:59 -08:00
is_agg , & agg_proof , & evm_proof , & root_vk , common ,
)
. expect ( " Failed to build cyclic recursion circuit " ) ;
AggregationChildTarget {
is_agg ,
agg_proof ,
evm_proof ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
}
2023-04-01 09:34:13 -04:00
fn create_block_circuit ( agg : & AggregationCircuitData < F , C , D > ) -> BlockCircuitData < F , C , D > {
2023-01-15 00:06:08 -08:00
// The block circuit is similar to the agg circuit; both verify two inner proofs.
// We need to adjust a few things, but it's easier than making a new CommonCircuitData.
let expected_common_data = CommonCircuitData {
fri_params : FriParams {
degree_bits : 14 ,
.. agg . circuit . common . fri_params . clone ( )
} ,
.. agg . circuit . common . clone ( )
} ;
let mut builder = CircuitBuilder ::< F , D > ::new ( CircuitConfig ::standard_recursion_config ( ) ) ;
2023-06-21 20:05:39 +02:00
let public_values = add_virtual_public_values ( & mut builder ) ;
2023-01-15 00:06:08 -08:00
let has_parent_block = builder . add_virtual_bool_target_safe ( ) ;
2023-02-25 08:55:55 -08:00
let parent_block_proof = builder . add_virtual_proof_with_pis ( & expected_common_data ) ;
let agg_root_proof = builder . add_virtual_proof_with_pis ( & agg . circuit . common ) ;
2023-01-15 00:06:08 -08:00
2023-08-21 23:32:53 +01:00
// Connect block hashes
Self ::connect_block_hashes ( & mut builder , & parent_block_proof , & agg_root_proof ) ;
2023-08-23 23:29:58 +01:00
let parent_pv = PublicValuesTarget ::from_public_inputs ( & parent_block_proof . public_inputs ) ;
let agg_pv = PublicValuesTarget ::from_public_inputs ( & agg_root_proof . public_inputs ) ;
// Make connections between block proofs, and check initial and final block values.
2023-09-05 14:20:45 +01:00
Self ::connect_block_proof ( & mut builder , has_parent_block , & parent_pv , & agg_pv ) ;
2023-08-23 23:29:58 +01:00
2023-01-15 00:06:08 -08:00
let cyclic_vk = builder . add_verifier_data_public_inputs ( ) ;
builder
2023-04-01 09:34:13 -04:00
. conditionally_verify_cyclic_proof_or_dummy ::< C > (
2023-01-15 00:06:08 -08:00
has_parent_block ,
& parent_block_proof ,
& expected_common_data ,
)
. expect ( " Failed to build cyclic recursion circuit " ) ;
let agg_verifier_data = builder . constant_verifier_data ( & agg . circuit . verifier_only ) ;
2023-04-01 09:34:13 -04:00
builder . verify_proof ::< C > ( & agg_root_proof , & agg_verifier_data , & agg . circuit . common ) ;
2023-01-15 00:06:08 -08:00
2023-04-01 09:34:13 -04:00
let circuit = builder . build ::< C > ( ) ;
2023-01-15 00:06:08 -08:00
BlockCircuitData {
circuit ,
has_parent_block ,
parent_block_proof ,
agg_root_proof ,
2023-06-21 20:05:39 +02:00
public_values ,
2023-01-15 00:06:08 -08:00
cyclic_vk ,
}
}
2023-08-21 23:32:53 +01:00
/// Connect the 256 block hashes between two blocks
2023-11-13 09:26:56 -05:00
fn connect_block_hashes (
2023-08-21 23:32:53 +01:00
builder : & mut CircuitBuilder < F , D > ,
lhs : & ProofWithPublicInputsTarget < D > ,
rhs : & ProofWithPublicInputsTarget < D > ,
) {
let lhs_public_values = PublicValuesTarget ::from_public_inputs ( & lhs . public_inputs ) ;
let rhs_public_values = PublicValuesTarget ::from_public_inputs ( & rhs . public_inputs ) ;
for i in 0 .. 255 {
for j in 0 .. 8 {
builder . connect (
lhs_public_values . block_hashes . prev_hashes [ 8 * ( i + 1 ) + j ] ,
rhs_public_values . block_hashes . prev_hashes [ 8 * i + j ] ,
) ;
}
}
let expected_hash = lhs_public_values . block_hashes . cur_hash ;
let prev_block_hash = & rhs_public_values . block_hashes . prev_hashes [ 255 * 8 .. 256 * 8 ] ;
for i in 0 .. expected_hash . len ( ) {
builder . connect ( expected_hash [ i ] , prev_block_hash [ i ] ) ;
}
}
2023-08-23 23:29:58 +01:00
fn connect_block_proof (
builder : & mut CircuitBuilder < F , D > ,
2023-09-05 14:20:45 +01:00
has_parent_block : BoolTarget ,
2023-08-23 23:29:58 +01:00
lhs : & PublicValuesTarget ,
rhs : & PublicValuesTarget ,
) {
// Between blocks, we only connect state tries.
for ( & limb0 , limb1 ) in lhs
. trie_roots_after
. state_root
. iter ( )
. zip ( rhs . trie_roots_before . state_root )
{
builder . connect ( limb0 , limb1 ) ;
}
2023-09-11 15:47:33 +01:00
// Between blocks, the genesis state trie remains unchanged.
for ( & limb0 , limb1 ) in lhs
. extra_block_data
2023-10-03 17:47:10 +02:00
. genesis_state_trie_root
2023-09-11 15:47:33 +01:00
. iter ( )
2023-10-03 17:47:10 +02:00
. zip ( rhs . extra_block_data . genesis_state_trie_root )
2023-09-11 15:47:33 +01:00
{
builder . connect ( limb0 , limb1 ) ;
}
2023-08-23 23:29:58 +01:00
// Connect block numbers.
let one = builder . one ( ) ;
let prev_block_nb = builder . sub ( rhs . block_metadata . block_number , one ) ;
builder . connect ( lhs . block_metadata . block_number , prev_block_nb ) ;
// Check initial block values.
Self ::connect_initial_values_block ( builder , rhs ) ;
2023-09-05 14:20:45 +01:00
// Connect intermediary values for gas_used and bloom filters to the block's final values. We only plug on the right, so there is no need to check the left-handside block.
2023-08-23 23:29:58 +01:00
Self ::connect_final_block_values_to_intermediary ( builder , rhs ) ;
2023-09-05 14:20:45 +01:00
let has_not_parent_block = builder . sub ( one , has_parent_block . target ) ;
2023-09-25 10:35:38 -04:00
2023-09-26 12:21:29 -04:00
// Check that the genesis block number is 0.
2023-11-27 10:24:11 -05:00
let gen_block_constr = builder . mul ( has_not_parent_block , lhs . block_metadata . block_number ) ;
2023-10-16 08:53:59 -04:00
builder . assert_zero ( gen_block_constr ) ;
2023-09-05 14:20:45 +01:00
2023-09-25 10:35:38 -04:00
// Check that the genesis block has the predetermined state trie root in `ExtraBlockData`.
Self ::connect_genesis_block ( builder , rhs , has_not_parent_block ) ;
}
fn connect_genesis_block (
builder : & mut CircuitBuilder < F , D > ,
x : & PublicValuesTarget ,
has_not_parent_block : Target ,
) where
F : RichField + Extendable < D > ,
{
for ( & limb0 , limb1 ) in x
2023-09-11 15:47:33 +01:00
. trie_roots_before
. state_root
. iter ( )
2023-10-03 17:47:10 +02:00
. zip ( x . extra_block_data . genesis_state_trie_root )
2023-09-11 15:47:33 +01:00
{
let mut constr = builder . sub ( limb0 , limb1 ) ;
constr = builder . mul ( has_not_parent_block , constr ) ;
2023-10-16 08:53:59 -04:00
builder . assert_zero ( constr ) ;
2023-09-11 15:47:33 +01:00
}
2023-08-23 23:29:58 +01:00
}
fn connect_final_block_values_to_intermediary (
builder : & mut CircuitBuilder < F , D > ,
x : & PublicValuesTarget ,
) where
F : RichField + Extendable < D > ,
{
builder . connect (
2023-11-17 10:01:26 -05:00
x . block_metadata . block_gas_used ,
x . extra_block_data . gas_used_after ,
2023-08-23 23:29:58 +01:00
) ;
for ( & limb0 , & limb1 ) in x
. block_metadata
. block_bloom
. iter ( )
. zip ( & x . extra_block_data . block_bloom_after )
{
builder . connect ( limb0 , limb1 ) ;
}
}
fn connect_initial_values_block ( builder : & mut CircuitBuilder < F , D > , x : & PublicValuesTarget )
where
F : RichField + Extendable < D > ,
{
// The initial number of transactions is 0.
2023-10-16 08:53:59 -04:00
builder . assert_zero ( x . extra_block_data . txn_number_before ) ;
2023-09-29 14:47:23 -04:00
// The initial gas used is 0.
2023-11-17 10:01:26 -05:00
builder . assert_zero ( x . extra_block_data . gas_used_before ) ;
2023-08-23 23:29:58 +01:00
// The initial bloom filter is all zeroes.
2023-09-05 14:20:45 +01:00
for t in x . extra_block_data . block_bloom_before {
2023-10-16 08:53:59 -04:00
builder . assert_zero ( t ) ;
2023-08-23 23:29:58 +01:00
}
// The transactions and receipts tries are empty at the beginning of the block.
let initial_trie = HashedPartialTrie ::from ( Node ::Empty ) . hash ( ) ;
2023-09-05 14:20:45 +01:00
for ( i , limb ) in h256_limbs ::< F > ( initial_trie ) . into_iter ( ) . enumerate ( ) {
let limb_target = builder . constant ( limb ) ;
builder . connect ( x . trie_roots_before . transactions_root [ i ] , limb_target ) ;
builder . connect ( x . trie_roots_before . receipts_root [ i ] , limb_target ) ;
2023-08-23 23:29:58 +01:00
}
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
/// Create a proof for each STARK, then combine them, eventually culminating in a root proof.
pub fn prove_root (
& self ,
all_stark : & AllStark < F , D > ,
config : & StarkConfig ,
generation_inputs : GenerationInputs ,
timing : & mut TimingTree ,
2023-06-21 20:05:39 +02:00
) -> anyhow ::Result < ( ProofWithPublicInputs < F , C , D > , PublicValues ) > {
2023-04-01 09:34:13 -04:00
let all_proof = prove ::< F , C , D > ( all_stark , config , generation_inputs , timing ) ? ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let mut root_inputs = PartialWitness ::new ( ) ;
2023-01-03 15:46:59 -08:00
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
for table in 0 .. NUM_TABLES {
let stark_proof = & all_proof . stark_proofs [ table ] ;
let original_degree_bits = stark_proof . proof . recover_degree_bits ( config ) ;
let table_circuits = & self . by_table [ table ] ;
2023-08-07 11:42:03 -04:00
let shrunk_proof = table_circuits
. by_stark_size
. get ( & original_degree_bits )
. ok_or_else ( | | {
anyhow ::Error ::msg ( format! (
" Missing preprocessed circuits for {:?} table with size {}. " ,
Table ::all ( ) [ table ] ,
original_degree_bits ,
) )
} ) ?
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
. shrink ( stark_proof , & all_proof . ctl_challenges ) ? ;
let index_verifier_data = table_circuits
. by_stark_size
. keys ( )
. position ( | & size | size = = original_degree_bits )
. unwrap ( ) ;
root_inputs . set_target (
self . root . index_verifier_data [ table ] ,
F ::from_canonical_usize ( index_verifier_data ) ,
) ;
root_inputs . set_proof_with_pis_target ( & self . root . proof_with_pis [ table ] , & shrunk_proof ) ;
}
2023-01-03 15:46:59 -08:00
2023-01-03 17:45:47 -08:00
root_inputs . set_verifier_data_target (
& self . root . cyclic_vk ,
& self . aggregation . circuit . verifier_only ,
) ;
2023-01-03 15:46:59 -08:00
2023-08-01 16:43:27 -04:00
set_public_value_targets (
2023-06-21 20:05:39 +02:00
& mut root_inputs ,
2023-08-01 16:43:27 -04:00
& self . root . public_values ,
& all_proof . public_values ,
2023-09-12 19:23:16 -04:00
)
2023-09-18 09:59:48 -04:00
. map_err ( | _ | {
anyhow ::Error ::msg ( " Invalid conversion when setting public values targets. " )
} ) ? ;
2023-06-21 20:05:39 +02:00
let root_proof = self . root . circuit . prove ( root_inputs ) ? ;
Ok ( ( root_proof , all_proof . public_values ) )
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
2023-01-03 15:46:59 -08:00
2023-04-01 09:34:13 -04:00
pub fn verify_root ( & self , agg_proof : ProofWithPublicInputs < F , C , D > ) -> anyhow ::Result < ( ) > {
2023-01-04 14:50:15 -08:00
self . root . circuit . verify ( agg_proof )
2023-01-03 15:46:59 -08:00
}
pub fn prove_aggregation (
& self ,
lhs_is_agg : bool ,
2023-04-01 09:34:13 -04:00
lhs_proof : & ProofWithPublicInputs < F , C , D > ,
2023-11-15 14:51:35 -05:00
lhs_public_values : PublicValues ,
2023-01-03 15:46:59 -08:00
rhs_is_agg : bool ,
2023-04-01 09:34:13 -04:00
rhs_proof : & ProofWithPublicInputs < F , C , D > ,
2023-11-15 14:51:35 -05:00
rhs_public_values : PublicValues ,
2023-06-21 20:05:39 +02:00
) -> anyhow ::Result < ( ProofWithPublicInputs < F , C , D > , PublicValues ) > {
2023-01-03 15:46:59 -08:00
let mut agg_inputs = PartialWitness ::new ( ) ;
agg_inputs . set_bool_target ( self . aggregation . lhs . is_agg , lhs_is_agg ) ;
agg_inputs . set_proof_with_pis_target ( & self . aggregation . lhs . agg_proof , lhs_proof ) ;
agg_inputs . set_proof_with_pis_target ( & self . aggregation . lhs . evm_proof , lhs_proof ) ;
agg_inputs . set_bool_target ( self . aggregation . rhs . is_agg , rhs_is_agg ) ;
agg_inputs . set_proof_with_pis_target ( & self . aggregation . rhs . agg_proof , rhs_proof ) ;
agg_inputs . set_proof_with_pis_target ( & self . aggregation . rhs . evm_proof , rhs_proof ) ;
agg_inputs . set_verifier_data_target (
& self . aggregation . cyclic_vk ,
& self . aggregation . circuit . verifier_only ,
) ;
2023-01-04 14:50:15 -08:00
2023-11-15 14:51:35 -05:00
// Aggregates both `PublicValues` from the provided proofs into a single one.
let agg_public_values = PublicValues {
trie_roots_before : lhs_public_values . trie_roots_before ,
trie_roots_after : rhs_public_values . trie_roots_after ,
extra_block_data : ExtraBlockData {
genesis_state_trie_root : lhs_public_values . extra_block_data . genesis_state_trie_root ,
txn_number_before : lhs_public_values . extra_block_data . txn_number_before ,
txn_number_after : rhs_public_values . extra_block_data . txn_number_after ,
gas_used_before : lhs_public_values . extra_block_data . gas_used_before ,
gas_used_after : rhs_public_values . extra_block_data . gas_used_after ,
block_bloom_before : lhs_public_values . extra_block_data . block_bloom_before ,
block_bloom_after : rhs_public_values . extra_block_data . block_bloom_after ,
} ,
block_metadata : rhs_public_values . block_metadata ,
block_hashes : rhs_public_values . block_hashes ,
} ;
2023-09-12 19:23:16 -04:00
set_public_value_targets (
2023-06-21 20:05:39 +02:00
& mut agg_inputs ,
2023-09-12 19:23:16 -04:00
& self . aggregation . public_values ,
2023-11-15 14:51:35 -05:00
& agg_public_values ,
2023-09-12 19:23:16 -04:00
)
2023-09-18 09:59:48 -04:00
. map_err ( | _ | {
anyhow ::Error ::msg ( " Invalid conversion when setting public values targets. " )
} ) ? ;
2023-06-21 20:05:39 +02:00
let aggregation_proof = self . aggregation . circuit . prove ( agg_inputs ) ? ;
2023-11-15 14:51:35 -05:00
Ok ( ( aggregation_proof , agg_public_values ) )
2023-01-03 15:46:59 -08:00
}
pub fn verify_aggregation (
& self ,
2023-04-01 09:34:13 -04:00
agg_proof : & ProofWithPublicInputs < F , C , D > ,
2023-01-03 15:46:59 -08:00
) -> anyhow ::Result < ( ) > {
self . aggregation . circuit . verify ( agg_proof . clone ( ) ) ? ;
check_cyclic_proof_verifier_data (
agg_proof ,
& self . aggregation . circuit . verifier_only ,
& self . aggregation . circuit . common ,
)
}
2023-01-15 00:06:08 -08:00
pub fn prove_block (
& self ,
2023-04-01 09:34:13 -04:00
opt_parent_block_proof : Option < & ProofWithPublicInputs < F , C , D > > ,
agg_root_proof : & ProofWithPublicInputs < F , C , D > ,
2023-06-21 20:05:39 +02:00
public_values : PublicValues ,
) -> anyhow ::Result < ( ProofWithPublicInputs < F , C , D > , PublicValues ) > {
2023-01-15 00:06:08 -08:00
let mut block_inputs = PartialWitness ::new ( ) ;
block_inputs . set_bool_target (
self . block . has_parent_block ,
opt_parent_block_proof . is_some ( ) ,
) ;
if let Some ( parent_block_proof ) = opt_parent_block_proof {
block_inputs
. set_proof_with_pis_target ( & self . block . parent_block_proof , parent_block_proof ) ;
2023-03-31 18:12:38 -04:00
} else {
2023-11-27 10:24:11 -05:00
// Initialize genesis_state_trie, state_root_after, and the previous block hashes for correct connection between blocks.
// Block number does not need to be initialized as genesis block is constrained to have number 0.
if public_values . trie_roots_before . state_root
! = public_values . extra_block_data . genesis_state_trie_root
{
return Err ( anyhow ::Error ::msg ( format! (
" Inconsistent pre-state for first block {:?} with genesis state {:?}. " ,
public_values . trie_roots_before . state_root ,
public_values . extra_block_data . genesis_state_trie_root ,
) ) ) ;
}
2023-09-11 15:47:33 +01:00
// Initialize `state_root_after`.
2023-11-22 13:30:52 -05:00
let state_trie_root_after_keys =
TrieRootsTarget ::SIZE .. TrieRootsTarget ::SIZE + TrieRootsTarget ::HASH_SIZE ;
2023-08-23 23:29:58 +01:00
let mut nonzero_pis = HashMap ::new ( ) ;
2023-09-11 15:47:33 +01:00
for ( key , & value ) in state_trie_root_after_keys
2023-09-05 14:20:45 +01:00
. zip_eq ( & h256_limbs ::< F > ( public_values . trie_roots_before . state_root ) )
{
2023-08-23 23:29:58 +01:00
nonzero_pis . insert ( key , value ) ;
}
2023-09-11 15:47:33 +01:00
// Initialize the genesis state trie digest.
let genesis_state_trie_keys = TrieRootsTarget ::SIZE * 2
+ BlockMetadataTarget ::SIZE
+ BlockHashesTarget ::BLOCK_HASHES_SIZE
.. TrieRootsTarget ::SIZE * 2
+ BlockMetadataTarget ::SIZE
+ BlockHashesTarget ::BLOCK_HASHES_SIZE
+ 8 ;
for ( key , & value ) in genesis_state_trie_keys . zip_eq ( & h256_limbs ::< F > (
2023-10-03 17:47:10 +02:00
public_values . extra_block_data . genesis_state_trie_root ,
2023-09-11 15:47:33 +01:00
) ) {
nonzero_pis . insert ( key , value ) ;
}
2023-11-22 13:30:52 -05:00
// Initialize block hashes.
let block_hashes_keys = TrieRootsTarget ::SIZE * 2 + BlockMetadataTarget ::SIZE
.. TrieRootsTarget ::SIZE * 2
+ BlockMetadataTarget ::SIZE
+ BlockHashesTarget ::BLOCK_HASHES_SIZE
- 8 ;
for i in 0 .. public_values . block_hashes . prev_hashes . len ( ) - 1 {
let targets = h256_limbs ::< F > ( public_values . block_hashes . prev_hashes [ i ] ) ;
for j in 0 .. 8 {
nonzero_pis . insert ( block_hashes_keys . start + 8 * ( i + 1 ) + j , targets [ j ] ) ;
}
}
2023-11-27 10:24:11 -05:00
let block_hashes_current_start = TrieRootsTarget ::SIZE * 2
+ BlockMetadataTarget ::SIZE
+ BlockHashesTarget ::BLOCK_HASHES_SIZE
- 8 ;
2023-11-22 13:30:52 -05:00
let cur_targets = h256_limbs ::< F > ( public_values . block_hashes . prev_hashes [ 255 ] ) ;
for i in 0 .. 8 {
2023-11-27 10:24:11 -05:00
nonzero_pis . insert ( block_hashes_current_start + i , cur_targets [ i ] ) ;
2023-11-22 13:30:52 -05:00
}
2023-03-31 18:12:38 -04:00
block_inputs . set_proof_with_pis_target (
& self . block . parent_block_proof ,
& cyclic_base_proof (
& self . block . circuit . common ,
& self . block . circuit . verifier_only ,
2023-08-23 23:29:58 +01:00
nonzero_pis ,
2023-03-31 18:12:38 -04:00
) ,
) ;
2023-01-15 00:06:08 -08:00
}
block_inputs . set_proof_with_pis_target ( & self . block . agg_root_proof , agg_root_proof ) ;
block_inputs
. set_verifier_data_target ( & self . block . cyclic_vk , & self . block . circuit . verifier_only ) ;
2023-09-12 19:23:16 -04:00
set_public_value_targets ( & mut block_inputs , & self . block . public_values , & public_values )
. map_err ( | _ | {
2023-09-18 09:59:48 -04:00
anyhow ::Error ::msg ( " Invalid conversion when setting public values targets. " )
2023-09-12 19:23:16 -04:00
} ) ? ;
2023-06-21 20:05:39 +02:00
let block_proof = self . block . circuit . prove ( block_inputs ) ? ;
Ok ( ( block_proof , public_values ) )
2023-01-15 00:06:08 -08:00
}
2023-04-01 09:34:13 -04:00
pub fn verify_block ( & self , block_proof : & ProofWithPublicInputs < F , C , D > ) -> anyhow ::Result < ( ) > {
2023-01-15 00:06:08 -08:00
self . block . circuit . verify ( block_proof . clone ( ) ) ? ;
check_cyclic_proof_verifier_data (
block_proof ,
& self . block . circuit . verifier_only ,
& self . block . circuit . common ,
)
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
2023-02-21 21:12:03 -05:00
#[ derive(Eq, PartialEq, Debug) ]
pub struct RecursiveCircuitsForTable < F , C , const D : usize >
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
2023-05-11 02:59:02 +10:00
C ::Hasher : AlgebraicHasher < F > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
{
/// A map from `log_2(height)` to a chain of shrinking recursion circuits starting at that
/// height.
2023-04-01 09:34:13 -04:00
by_stark_size : BTreeMap < usize , RecursiveCircuitsForTableSize < F , C , D > > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
2023-04-01 09:34:13 -04:00
impl < F , C , const D : usize > RecursiveCircuitsForTable < F , C , D >
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
2023-05-11 02:59:02 +10:00
C ::Hasher : AlgebraicHasher < F > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
{
2023-11-13 09:26:56 -05:00
fn to_buffer (
2023-02-21 21:12:03 -05:00
& self ,
buffer : & mut Vec < u8 > ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < ( ) > {
buffer . write_usize ( self . by_stark_size . len ( ) ) ? ;
for ( & size , table ) in & self . by_stark_size {
buffer . write_usize ( size ) ? ;
table . to_buffer ( buffer , gate_serializer , generator_serializer ) ? ;
}
Ok ( ( ) )
}
2023-11-13 09:26:56 -05:00
fn from_buffer (
2023-02-21 21:12:03 -05:00
buffer : & mut Buffer ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < Self > {
let length = buffer . read_usize ( ) ? ;
let mut by_stark_size = BTreeMap ::new ( ) ;
for _ in 0 .. length {
let key = buffer . read_usize ( ) ? ;
let table = RecursiveCircuitsForTableSize ::from_buffer (
buffer ,
gate_serializer ,
generator_serializer ,
) ? ;
by_stark_size . insert ( key , table ) ;
}
Ok ( Self { by_stark_size } )
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
fn new < S : Stark < F , D > > (
table : Table ,
stark : & S ,
degree_bits_range : Range < usize > ,
all_ctls : & [ CrossTableLookup < F > ] ,
stark_config : & StarkConfig ,
2023-09-22 09:19:13 -04:00
) -> Self {
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let by_stark_size = degree_bits_range
. map ( | degree_bits | {
(
degree_bits ,
RecursiveCircuitsForTableSize ::new ::< S > (
table ,
stark ,
degree_bits ,
all_ctls ,
stark_config ,
) ,
)
} )
. collect ( ) ;
Self { by_stark_size }
}
2023-11-28 12:23:20 -05:00
fn expand < S : Stark < F , D > > (
& mut self ,
table : Table ,
stark : & S ,
degree_bits_range : Range < usize > ,
all_ctls : & [ CrossTableLookup < F > ] ,
stark_config : & StarkConfig ,
) {
let new_ranges = degree_bits_range
. filter ( | degree_bits | ! self . by_stark_size . contains_key ( degree_bits ) )
. collect_vec ( ) ;
for degree_bits in new_ranges {
self . by_stark_size . insert (
degree_bits ,
RecursiveCircuitsForTableSize ::new ::< S > (
table ,
stark ,
degree_bits ,
all_ctls ,
stark_config ,
) ,
) ;
}
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
/// For each initial `degree_bits`, get the final circuit at the end of that shrinking chain.
/// Each of these final circuits should have degree `THRESHOLD_DEGREE_BITS`.
2023-04-01 09:34:13 -04:00
fn final_circuits ( & self ) -> Vec < & CircuitData < F , C , D > > {
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
self . by_stark_size
. values ( )
. map ( | chain | {
chain
. shrinking_wrappers
. last ( )
. map ( | wrapper | & wrapper . circuit )
. unwrap_or ( & chain . initial_wrapper . circuit )
} )
. collect ( )
}
}
/// A chain of shrinking wrapper circuits, ending with a final circuit with `degree_bits`
/// `THRESHOLD_DEGREE_BITS`.
2023-02-21 21:12:03 -05:00
#[ derive(Eq, PartialEq, Debug) ]
2023-04-01 09:34:13 -04:00
struct RecursiveCircuitsForTableSize < F , C , const D : usize >
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
2023-05-11 02:59:02 +10:00
C ::Hasher : AlgebraicHasher < F > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
{
2023-04-01 09:34:13 -04:00
initial_wrapper : StarkWrapperCircuit < F , C , D > ,
shrinking_wrappers : Vec < PlonkWrapperCircuit < F , C , D > > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
}
2023-04-01 09:34:13 -04:00
impl < F , C , const D : usize > RecursiveCircuitsForTableSize < F , C , D >
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
where
F : RichField + Extendable < D > ,
2023-04-01 09:34:13 -04:00
C : GenericConfig < D , F = F > ,
2023-05-11 02:59:02 +10:00
C ::Hasher : AlgebraicHasher < F > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
{
2023-11-13 09:26:56 -05:00
fn to_buffer (
2023-02-21 21:12:03 -05:00
& self ,
buffer : & mut Vec < u8 > ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < ( ) > {
buffer . write_usize ( self . shrinking_wrappers . len ( ) ) ? ;
if ! self . shrinking_wrappers . is_empty ( ) {
buffer . write_common_circuit_data (
& self . shrinking_wrappers [ 0 ] . circuit . common ,
gate_serializer ,
) ? ;
}
for wrapper in & self . shrinking_wrappers {
buffer . write_prover_only_circuit_data (
& wrapper . circuit . prover_only ,
generator_serializer ,
2023-06-28 08:38:02 -04:00
& wrapper . circuit . common ,
2023-02-21 21:12:03 -05:00
) ? ;
buffer . write_verifier_only_circuit_data ( & wrapper . circuit . verifier_only ) ? ;
buffer . write_target_proof_with_public_inputs ( & wrapper . proof_with_pis_target ) ? ;
}
self . initial_wrapper
. to_buffer ( buffer , gate_serializer , generator_serializer ) ? ;
Ok ( ( ) )
}
2023-11-13 09:26:56 -05:00
fn from_buffer (
2023-02-21 21:12:03 -05:00
buffer : & mut Buffer ,
gate_serializer : & dyn GateSerializer < F , D > ,
generator_serializer : & dyn WitnessGeneratorSerializer < F , D > ,
) -> IoResult < Self > {
let length = buffer . read_usize ( ) ? ;
let mut shrinking_wrappers = Vec ::with_capacity ( length ) ;
if length ! = 0 {
let common = buffer . read_common_circuit_data ( gate_serializer ) ? ;
for _ in 0 .. length {
let prover_only =
buffer . read_prover_only_circuit_data ( generator_serializer , & common ) ? ;
let verifier_only = buffer . read_verifier_only_circuit_data ( ) ? ;
let proof_with_pis_target = buffer . read_target_proof_with_public_inputs ( ) ? ;
shrinking_wrappers . push ( PlonkWrapperCircuit {
circuit : CircuitData {
common : common . clone ( ) ,
prover_only ,
verifier_only ,
} ,
proof_with_pis_target ,
} )
}
} ;
let initial_wrapper =
StarkWrapperCircuit ::from_buffer ( buffer , gate_serializer , generator_serializer ) ? ;
Ok ( Self {
initial_wrapper ,
shrinking_wrappers ,
} )
}
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
fn new < S : Stark < F , D > > (
table : Table ,
stark : & S ,
degree_bits : usize ,
all_ctls : & [ CrossTableLookup < F > ] ,
stark_config : & StarkConfig ,
2023-09-22 09:19:13 -04:00
) -> Self {
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let initial_wrapper = recursive_stark_circuit (
table ,
stark ,
degree_bits ,
all_ctls ,
stark_config ,
& shrinking_config ( ) ,
THRESHOLD_DEGREE_BITS ,
) ;
let mut shrinking_wrappers = vec! [ ] ;
// Shrinking recursion loop.
loop {
let last = shrinking_wrappers
. last ( )
2023-04-01 09:34:13 -04:00
. map ( | wrapper : & PlonkWrapperCircuit < F , C , D > | & wrapper . circuit )
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
. unwrap_or ( & initial_wrapper . circuit ) ;
let last_degree_bits = last . common . degree_bits ( ) ;
assert! ( last_degree_bits > = THRESHOLD_DEGREE_BITS ) ;
if last_degree_bits = = THRESHOLD_DEGREE_BITS {
break ;
}
let mut builder = CircuitBuilder ::new ( shrinking_config ( ) ) ;
2023-02-25 08:55:55 -08:00
let proof_with_pis_target = builder . add_virtual_proof_with_pis ( & last . common ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let last_vk = builder . constant_verifier_data ( & last . verifier_only ) ;
2023-04-01 09:34:13 -04:00
builder . verify_proof ::< C > ( & proof_with_pis_target , & last_vk , & last . common ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
builder . register_public_inputs ( & proof_with_pis_target . public_inputs ) ; // carry PIs forward
add_common_recursion_gates ( & mut builder ) ;
2023-04-01 09:34:13 -04:00
let circuit = builder . build ::< C > ( ) ;
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
assert! (
circuit . common . degree_bits ( ) < last_degree_bits ,
" Couldn't shrink to expected recursion threshold of 2^{}; stalled at 2^{} " ,
THRESHOLD_DEGREE_BITS ,
circuit . common . degree_bits ( )
) ;
shrinking_wrappers . push ( PlonkWrapperCircuit {
circuit ,
proof_with_pis_target ,
} ) ;
}
Self {
initial_wrapper ,
shrinking_wrappers ,
}
}
fn shrink (
& self ,
2023-04-01 09:34:13 -04:00
stark_proof_with_metadata : & StarkProofWithMetadata < F , C , D > ,
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
ctl_challenges : & GrandProductChallengeSet < F > ,
2023-04-01 09:34:13 -04:00
) -> anyhow ::Result < ProofWithPublicInputs < F , C , D > > {
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
let mut proof = self
. initial_wrapper
. prove ( stark_proof_with_metadata , ctl_challenges ) ? ;
for wrapper_circuit in & self . shrinking_wrappers {
proof = wrapper_circuit . prove ( & proof ) ? ;
}
Ok ( proof )
}
}
2023-01-03 11:23:28 -08:00
/// Our usual recursion threshold is 2^12 gates, but for these shrinking circuits, we use a few more
/// gates for a constant inner VK and for public inputs. This pushes us over the threshold to 2^13.
/// As long as we're at 2^13 gates, we might as well use a narrower witness.
Shrink STARK proofs to a constant degree
The goal here is to end up with a single "root" circuit representing any EVM proof. I.e. it must verify each STARK, but be general enough to work with any combination of STARK sizes (within some range of sizes that we chose to support). This root circuit can then be plugged into our aggregation circuit.
In particular, for each STARK, and for each initial `degree_bits` (within a range that we choose to support), this adds a "shrinking chain" of circuits. Such a chain shrinks a STARK proof from that initial `degree_bits` down to a constant, `THRESHOLD_DEGREE_BITS`.
The root circuit then combines these shrunk-to-constant proofs for each table. It's similar to `RecursiveAllProof::verify_circuit`; I adapted the code from there and I think we can remove it after. The main difference is that now instead of having one verification key per STARK, we have several possible VKs, one per initial `degree_bits`. We bake the list of possible VKs into the root circuit, and have the prover indicate the index of the VK they're actually using.
This also partially removes the default feature of CTLs. So far we've used filters instead of defaults. Until now it was easy to keep supporting defaults just in case, but here maintaining support would require some more work. E.g. we couldn't use `exp_u64` any more, since the size delta is now dynamic, it can't be hardcoded. If there are no concerns, I'll fully remove the feature after.
2022-12-27 18:15:18 -08:00
fn shrinking_config ( ) -> CircuitConfig {
CircuitConfig {
num_routed_wires : 40 ,
.. CircuitConfig ::standard_recursion_config ( )
}
}