Merge branch 'main' of github.com:mir-protocol/plonky2 into non-inv

This commit is contained in:
Dmitry Vagner 2022-11-28 14:56:41 -08:00
commit 8af4cd17f0
4 changed files with 68 additions and 42 deletions

View File

@ -21,7 +21,7 @@ global extcodehash:
%endmacro
%macro extcodesize
%stack (address) -> (address, %%after)
%stack (address) -> (address, 0, @SEGMENT_KERNEL_ACCOUNT_CODE, %%after)
%jump(load_code)
%%after:
%endmacro
@ -44,7 +44,8 @@ global extcodesize:
// Post stack: (empty)
global extcodecopy:
// stack: address, dest_offset, offset, size, retdest
%stack (address, dest_offset, offset, size, retdest) -> (address, extcodecopy_contd, size, offset, dest_offset, retdest)
%stack (address, dest_offset, offset, size, retdest)
-> (address, 0, @SEGMENT_KERNEL_ACCOUNT_CODE, extcodecopy_contd, size, offset, dest_offset, retdest)
%jump(load_code)
extcodecopy_contd:
@ -55,19 +56,22 @@ extcodecopy_contd:
// Loop copying the `code[offset]` to `memory[dest_offset]` until `i==size`.
// Each iteration increments `offset, dest_offset, i`.
// TODO: Consider implementing this with memcpy.
extcodecopy_loop:
// stack: i, size, code_length, offset, dest_offset, retdest
DUP2 DUP2 EQ
// stack: i == size, i, size, code_length, offset, dest_offset, retdest
%jumpi(extcodecopy_end)
%stack (i, size, code_length, offset, dest_offset, retdest) -> (offset, code_length, offset, code_length, dest_offset, i, size, retdest)
%stack (i, size, code_length, offset, dest_offset, retdest)
-> (offset, code_length, offset, code_length, dest_offset, i, size, retdest)
LT
// stack: offset < code_length, offset, code_length, dest_offset, i, size, retdest
DUP2
// stack: offset, offset < code_length, offset, code_length, dest_offset, i, size, retdest
%mload_current(@SEGMENT_KERNEL_ACCOUNT_CODE)
// stack: opcode, offset < code_length, offset, code_length, dest_offset, i, size, retdest
%stack (opcode, offset_lt_code_length, offset, code_length, dest_offset, i, size, retdest) -> (offset_lt_code_length, 0, opcode, offset, code_length, dest_offset, i, size, retdest)
%stack (opcode, offset_lt_code_length, offset, code_length, dest_offset, i, size, retdest)
-> (offset_lt_code_length, 0, opcode, offset, code_length, dest_offset, i, size, retdest)
// If `offset >= code_length`, use `opcode=0`. Necessary since `SEGMENT_KERNEL_ACCOUNT_CODE` might be clobbered from previous calls.
%select_bool
// stack: opcode, offset, code_length, dest_offset, i, size, retdest
@ -93,41 +97,42 @@ extcodecopy_end:
JUMP
// Loads the code at `address` in the `SEGMENT_KERNEL_ACCOUNT_CODE` at the current context and starting at offset 0.
// Loads the code at `address` into memory, at the given context and segment, starting at offset 0.
// Checks that the hash of the loaded code corresponds to the `codehash` in the state trie.
// Pre stack: address, retdest
// Pre stack: address, ctx, segment, retdest
// Post stack: code_len
global load_code:
%stack (address, retdest) -> (extcodehash, address, load_code_ctd, retdest)
%stack (address, ctx, segment, retdest) -> (extcodehash, address, load_code_ctd, ctx, segment, retdest)
JUMP
load_code_ctd:
// stack: codehash, retdest
// stack: codehash, ctx, segment, retdest
PROVER_INPUT(account_code::length)
// stack: code_length, codehash, retdest
// stack: code_length, codehash, ctx, segment, retdest
PUSH 0
// Loop non-deterministically querying `code[i]` and storing it in `SEGMENT_KERNEL_ACCOUNT_CODE` at offset `i`, until `i==code_length`.
load_code_loop:
// stack: i, code_length, codehash, retdest
// stack: i, code_length, codehash, ctx, segment, retdest
DUP2 DUP2 EQ
// stack: i == code_length, i, code_length, codehash, retdest
// stack: i == code_length, i, code_length, codehash, ctx, segment, retdest
%jumpi(load_code_check)
PROVER_INPUT(account_code::get)
// stack: opcode, i, code_length, codehash, retdest
// stack: opcode, i, code_length, codehash, ctx, segment, retdest
DUP2
// stack: i, opcode, i, code_length, codehash, retdest
%mstore_current(@SEGMENT_KERNEL_ACCOUNT_CODE)
// stack: i, code_length, codehash, retdest
// stack: i, opcode, i, code_length, codehash, ctx, segment, retdest
DUP7 // segment
DUP7 // context
MSTORE_GENERAL
// stack: i, code_length, codehash, ctx, segment, retdest
%increment
// stack: i+1, code_length, codehash, retdest
// stack: i+1, code_length, codehash, ctx, segment, retdest
%jump(load_code_loop)
// Check that the hash of the loaded code equals `codehash`.
load_code_check:
// stack: i, code_length, codehash, retdest
POP
// stack: code_length, codehash, retdest
%stack (code_length, codehash, retdest) -> (0, @SEGMENT_KERNEL_ACCOUNT_CODE, 0, code_length, codehash, retdest, code_length)
// stack: i, code_length, codehash, ctx, segment, retdest
%stack (i, code_length, codehash, ctx, segment, retdest)
-> (ctx, segment, 0, code_length, codehash, retdest, code_length)
KECCAK_GENERAL
// stack: shouldbecodehash, codehash, retdest, code_length
%assert_eq

View File

@ -70,7 +70,7 @@ impl<F: Field> GenerationState<F> {
match input_fn.0[1].as_str() {
"length" => {
// Return length of code.
// stack: codehash
// stack: codehash, ...
let codehash = stack.last().expect("Empty stack");
self.inputs.contract_code[&H256::from_uint(codehash)]
.len()
@ -78,7 +78,7 @@ impl<F: Field> GenerationState<F> {
}
"get" => {
// Return `code[i]`.
// stack: i, code_length, codehash
// stack: i, code_length, codehash, ...
let stacklen = stack.len();
let i = stack[stacklen - 1].as_usize();
let codehash = stack[stacklen - 3];

View File

@ -40,7 +40,7 @@ use crate::plonk::circuit_data::{
CircuitConfig, CircuitData, CommonCircuitData, ProverCircuitData, ProverOnlyCircuitData,
VerifierCircuitData, VerifierCircuitTarget, VerifierOnlyCircuitData,
};
use crate::plonk::config::{GenericConfig, Hasher};
use crate::plonk::config::{GenericConfig, GenericHashOut, Hasher};
use crate::plonk::copy_constraint::CopyConstraint;
use crate::plonk::permutation_argument::Forest;
use crate::plonk::plonk_common::PlonkOracle;
@ -53,6 +53,11 @@ use crate::util::{log2_ceil, log2_strict, transpose, transpose_poly_values};
pub struct CircuitBuilder<F: RichField + Extendable<D>, const D: usize> {
pub config: CircuitConfig,
/// A domain separator, which is included in the initial Fiat-Shamir seed. This is generally not
/// needed, but can be used to ensure that proofs for one application are not valid for another.
/// Defaults to the empty vector.
domain_separator: Option<Vec<F>>,
/// The types of gates used in this circuit.
gates: HashSet<GateRef<F, D>>,
@ -102,6 +107,7 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
pub fn new(config: CircuitConfig) -> Self {
let builder = CircuitBuilder {
config,
domain_separator: None,
gates: HashSet::new(),
gate_instances: Vec::new(),
public_inputs: Vec::new(),
@ -145,6 +151,11 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
);
}
pub fn set_domain_separator(&mut self, separator: Vec<F>) {
assert!(self.domain_separator.is_none());
self.domain_separator = Some(separator);
}
pub fn num_gates(&self) -> usize {
self.gate_instances.len()
}
@ -849,9 +860,12 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
num_partial_products(self.config.num_routed_wires, quotient_degree_factor);
let constants_sigmas_cap = constants_sigmas_commitment.merkle_tree.cap.clone();
let domain_separator = self.domain_separator.unwrap_or_default();
let domain_separator_digest = C::Hasher::hash_pad(&domain_separator);
// TODO: This should also include an encoding of gate constraints.
let circuit_digest_parts = [
constants_sigmas_cap.flatten(),
domain_separator_digest.to_vec(),
vec![
F::from_canonical_usize(degree_bits),
/* Add other circuit data here */

View File

@ -35,7 +35,7 @@ pub struct CyclicRecursionTarget<const D: usize> {
pub verifier_data: VerifierCircuitTarget,
pub dummy_proof: ProofWithPublicInputsTarget<D>,
pub dummy_verifier_data: VerifierCircuitTarget,
pub base_case: BoolTarget,
pub condition: BoolTarget,
}
impl<C: GenericConfig<D>, const D: usize> VerifierOnlyCircuitData<C, D> {
@ -91,12 +91,22 @@ impl VerifierCircuitTarget {
}
impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
/// Cyclic recursion gadget.
/// If `condition` is true, recursively verify a proof for the same circuit as the one we're
/// currently building.
///
/// For a typical IVC use case, `condition` will be false for the very first proof in a chain,
/// i.e. the base case.
///
/// Note that this does not enforce that the inner circuit uses the correct verification key.
/// This is not possible to check in this recursive circuit, since we do not know the
/// verification key until after we build it. Verifiers must separately call
/// `check_cyclic_proof_verifier_data`, in addition to verifying a recursive proof, to check
/// that the verification key matches.
///
/// WARNING: Do not register any public input after calling this! TODO: relax this
pub fn cyclic_recursion<C: GenericConfig<D, F = F>>(
&mut self,
// Flag set to true for the base case of the cycle where we verify a dummy proof to bootstrap the cycle. Set to false otherwise.
base_case: BoolTarget,
condition: BoolTarget,
previous_virtual_public_inputs: &[Target],
common_data: &mut CommonCircuitData<F, D>,
) -> Result<CyclicRecursionTarget<D>>
@ -137,13 +147,13 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
self.connect(*x, *y);
}
// Verify the dummy proof if `base_case` is set to true, otherwise verify the "real" proof.
// Verify the real proof if `condition` is set to true, otherwise verify the dummy proof.
self.conditionally_verify_proof::<C>(
base_case,
&dummy_proof,
&dummy_verifier_data,
condition,
&proof,
&verifier_data,
&dummy_proof,
&dummy_verifier_data,
common_data,
);
@ -161,7 +171,7 @@ impl<F: RichField + Extendable<D>, const D: usize> CircuitBuilder<F, D> {
verifier_data: verifier_data.clone(),
dummy_proof,
dummy_verifier_data,
base_case,
condition,
})
}
}
@ -182,7 +192,7 @@ where
C::Hasher: AlgebraicHasher<F>,
{
if let Some(proof) = cyclic_recursion_data.proof {
pw.set_bool_target(cyclic_recursion_data_target.base_case, false);
pw.set_bool_target(cyclic_recursion_data_target.condition, true);
pw.set_proof_with_pis_target(&cyclic_recursion_data_target.proof, proof);
pw.set_verifier_data_target(
&cyclic_recursion_data_target.verifier_data,
@ -195,7 +205,7 @@ where
);
} else {
let (dummy_proof, dummy_data) = dummy_proof::<F, C, D>(cyclic_recursion_data.common_data)?;
pw.set_bool_target(cyclic_recursion_data_target.base_case, true);
pw.set_bool_target(cyclic_recursion_data_target.condition, false);
let mut proof = dummy_proof.clone();
proof.public_inputs[0..public_inputs.len()].copy_from_slice(public_inputs);
let pis_len = proof.public_inputs.len();
@ -231,8 +241,7 @@ where
}
/// Additional checks to be performed on a cyclic recursive proof in addition to verifying the proof.
/// Checks that the `base_case` flag is boolean and that the purported verifier data in the public inputs
/// match the real verifier data.
/// Checks that the purported verifier data in the public inputs match the real verifier data.
pub fn check_cyclic_proof_verifier_data<
F: RichField + Extendable<D>,
C: GenericConfig<D, F = F>,
@ -328,7 +337,6 @@ mod tests {
builder.register_public_inputs(&h.elements);
// Previous counter.
let old_counter = builder.add_virtual_target();
let one = builder.one();
let new_counter = builder.add_virtual_public_input();
let old_pis = [
initial_hash.elements.as_slice(),
@ -339,16 +347,15 @@ mod tests {
let mut common_data = common_data_for_recursion::<F, C, D>();
let base_case = builder.add_virtual_bool_target_safe();
let condition = builder.add_virtual_bool_target_safe();
// Add cyclic recursion gadget.
let cyclic_data_target =
builder.cyclic_recursion::<C>(base_case, &old_pis, &mut common_data)?;
builder.cyclic_recursion::<C>(condition, &old_pis, &mut common_data)?;
let input_hash_bis =
builder.select_hash(cyclic_data_target.base_case, initial_hash, old_hash);
builder.select_hash(cyclic_data_target.condition, old_hash, initial_hash);
builder.connect_hashes(input_hash, input_hash_bis);
let not_base_case = builder.sub(one, cyclic_data_target.base_case.target);
// New counter is the previous counter +1 if the previous proof wasn't a base case.
let new_counter_bis = builder.add(old_counter, not_base_case);
let new_counter_bis = builder.add(old_counter, condition.target);
builder.connect(new_counter, new_counter_bis);
let cyclic_circuit_data = builder.build::<C>();