Merge pull request #134 from valida-xyz/morgan/issue/133

Static data chip

Cargo.toml

@@ -14,6 +14,7 @@ members = [
     "output",
     "program",
     "range",
+    "static_data",
     "util",
     "verifier"
 ]

basic/Cargo.toml

@@ -31,6 +31,7 @@ valida-opcodes = { path = "../opcodes" }
 valida-output = { path = "../output" }
 valida-program = { path = "../program" }
 valida-range = { path = "../range" }
+valida-static-data = { path = "../static_data" }
 p3-baby-bear = { workspace = true }
 p3-field = { workspace = true }
 p3-maybe-rayon = { workspace = true }

basic/src/bin/test_prover.rs

@@ -2,18 +2,16 @@ extern crate core;
 
 use p3_baby_bear::BabyBear;
 use p3_fri::{TwoAdicFriPcs, TwoAdicFriPcsConfig};
-use valida_alu_u32::add::{Add32Instruction, MachineWithAdd32Chip};
+use valida_alu_u32::add::Add32Instruction;
 use valida_basic::BasicMachine;
 use valida_cpu::{
     BeqInstruction, BneInstruction, Imm32Instruction, JalInstruction, JalvInstruction,
     MachineWithCpuChip, StopInstruction,
 };
 use valida_machine::{
     FixedAdviceProvider, Instruction, InstructionWord, Machine, MachineProof, Operands, ProgramROM,
-    Word,
 };
 
-use valida_memory::MachineWithMemoryChip;
 use valida_opcodes::BYTES_PER_INSTR;
 use valida_program::MachineWithProgramChip;
 

basic/src/lib.rs

@@ -47,6 +47,7 @@ use valida_memory::{MachineWithMemoryChip, MemoryChip};
 use valida_output::{MachineWithOutputChip, OutputChip, WriteInstruction};
 use valida_program::{MachineWithProgramChip, ProgramChip};
 use valida_range::{MachineWithRangeChip, RangeCheckerChip};
+use valida_static_data::{MachineWithStaticDataChip, StaticDataChip};
 
 use p3_maybe_rayon::prelude::*;
 use valida_machine::StarkConfig;
@@ -180,6 +181,10 @@ pub struct BasicMachine<F: PrimeField32 + TwoAdicField> {
     #[chip]
     range: RangeCheckerChip<256>,
 
+    #[chip]
+    #[static_data_chip]
+    static_data: StaticDataChip,
+
     _phantom_sc: PhantomData<fn() -> F>,
 }
 
@@ -335,3 +340,13 @@ impl<F: PrimeField32 + TwoAdicField> MachineWithRangeChip<F, 256> for BasicMachi
         &mut self.range
     }
 }
+
+impl<F: PrimeField32 + TwoAdicField> MachineWithStaticDataChip<F> for BasicMachine<F> {
+    fn static_data(&self) -> &StaticDataChip {
+        &self.static_data
+    }
+
+    fn static_data_mut(&mut self) -> &mut StaticDataChip {
+        &mut self.static_data
+    }
+}

basic/tests/test_static_data.rs

@@ -0,0 +1,113 @@
+extern crate core;
+
+use p3_baby_bear::BabyBear;
+use p3_fri::{TwoAdicFriPcs, TwoAdicFriPcsConfig};
+use valida_basic::BasicMachine;
+use valida_cpu::{
+    BneInstruction, Imm32Instruction, Load32Instruction, MachineWithCpuChip, StopInstruction,
+};
+use valida_machine::{
+    FixedAdviceProvider, Instruction, InstructionWord, Machine, Operands, ProgramROM, Word,
+};
+
+use valida_program::MachineWithProgramChip;
+use valida_static_data::MachineWithStaticDataChip;
+
+use p3_challenger::DuplexChallenger;
+use p3_dft::Radix2Bowers;
+use p3_field::extension::BinomialExtensionField;
+use p3_field::Field;
+use p3_fri::FriConfig;
+use p3_keccak::Keccak256Hash;
+use p3_mds::coset_mds::CosetMds;
+use p3_merkle_tree::FieldMerkleTreeMmcs;
+use p3_poseidon::Poseidon;
+use p3_symmetric::{CompressionFunctionFromHasher, SerializingHasher32};
+use rand::thread_rng;
+use valida_machine::StarkConfigImpl;
+use valida_machine::__internal::p3_commit::ExtensionMmcs;
+
+#[test]
+fn prove_static_data() {
+    // _start:
+    //  imm32 0(fp), 0, 0, 0, 0x10
+    //  load32 -4(fp), 0(fp), 0, 0, 0
+    //  bnei _start, 0(fp), 0x25, 0, 1        // infinite loop unless static value is loaded
+    //  stop
+    let program = vec![
+        InstructionWord {
+            opcode: <Imm32Instruction as Instruction<BasicMachine<Val>, Val>>::OPCODE,
+            operands: Operands([0, 0, 0, 0, 0x10]),
+        },
+        InstructionWord {
+            opcode: <Load32Instruction as Instruction<BasicMachine<Val>, Val>>::OPCODE,
+            operands: Operands([-4, 0, 0, 0, 0]),
+        },
+        InstructionWord {
+            opcode: <BneInstruction as Instruction<BasicMachine<Val>, Val>>::OPCODE,
+            operands: Operands([0, -4, 0x25, 0, 1]),
+        },
+        InstructionWord {
+            opcode: <StopInstruction as Instruction<BasicMachine<Val>, Val>>::OPCODE,
+            operands: Operands::default(),
+        },
+    ];
+
+    let mut machine = BasicMachine::<Val>::default();
+    let rom = ProgramROM::new(program);
+    machine.static_data_mut().write(0x10, Word([0, 0, 0, 0x25]));
+    machine.static_data_mut().write(0x14, Word([0, 0, 0, 0x32]));
+    machine.program_mut().set_program_rom(&rom);
+    machine.cpu_mut().fp = 0x1000;
+    machine.cpu_mut().save_register_state(); // TODO: Initial register state should be saved
+                                             // automatically by the machine, not manually here
+
+    machine.run(&rom, &mut FixedAdviceProvider::empty());
+
+    type Val = BabyBear;
+    type Challenge = BinomialExtensionField<Val, 5>;
+    type PackedChallenge = BinomialExtensionField<<Val as Field>::Packing, 5>;
+
+    type Mds16 = CosetMds<Val, 16>;
+    let mds16 = Mds16::default();
+
+    type Perm16 = Poseidon<Val, Mds16, 16, 5>;
+    let perm16 = Perm16::new_from_rng(4, 22, mds16, &mut thread_rng()); // TODO: Use deterministic RNG
+
+    type MyHash = SerializingHasher32<Keccak256Hash>;
+    let hash = MyHash::new(Keccak256Hash {});
+
+    type MyCompress = CompressionFunctionFromHasher<Val, MyHash, 2, 8>;
+    let compress = MyCompress::new(hash);
+
+    type ValMmcs = FieldMerkleTreeMmcs<Val, MyHash, MyCompress, 8>;
+    let val_mmcs = ValMmcs::new(hash, compress);
+
+    type ChallengeMmcs = ExtensionMmcs<Val, Challenge, ValMmcs>;
+    let challenge_mmcs = ChallengeMmcs::new(val_mmcs.clone());
+
+    type Dft = Radix2Bowers;
+    let dft = Dft::default();
+
+    type Challenger = DuplexChallenger<Val, Perm16, 16>;
+
+    type MyFriConfig = TwoAdicFriPcsConfig<Val, Challenge, Challenger, Dft, ValMmcs, ChallengeMmcs>;
+    let fri_config = FriConfig {
+        log_blowup: 1,
+        num_queries: 40,
+        proof_of_work_bits: 8,
+        mmcs: challenge_mmcs,
+    };
+
+    type Pcs = TwoAdicFriPcs<MyFriConfig>;
+    type MyConfig = StarkConfigImpl<Val, Challenge, PackedChallenge, Pcs, Challenger>;
+
+    let pcs = Pcs::new(fri_config, dft, val_mmcs);
+
+    let challenger = Challenger::new(perm16);
+    let config = MyConfig::new(pcs, challenger);
+    let proof = machine.prove(&config);
+    machine
+        .verify(&config, &proof)
+        .expect("verification failed");
+}

cpu/src/lib.rs

@@ -96,9 +96,10 @@ where
             let is_read = VirtualPairCol::single_main(channel.is_read);
             let clk = VirtualPairCol::single_main(CPU_COL_MAP.clk);
             let addr = VirtualPairCol::single_main(channel.addr);
+            let is_static_initial = VirtualPairCol::constant(SC::Val::zero());
             let value = channel.value.0.map(VirtualPairCol::single_main);
 
-            let mut fields = vec![is_read, clk, addr];
+            let mut fields = vec![is_read, clk, addr, is_static_initial];
             fields.extend(value);
 
             Interaction {
@@ -296,6 +297,7 @@ impl CpuChip {
         let len = values.len();
         let n_real_rows = values.len() / NUM_CPU_COLS;
 
+        debug_assert!(len > 0);
         let last_row = &values[len - NUM_CPU_COLS..];
         let pc = last_row[CPU_COL_MAP.pc];
         let fp = last_row[CPU_COL_MAP.fp];

derive/src/lib.rs

@@ -26,7 +26,10 @@ impl Parse for MachineFields {
     }
 }
 
-#[proc_macro_derive(Machine, attributes(machine_fields, bus, chip, instruction))]
+#[proc_macro_derive(
+    Machine,
+    attributes(machine_fields, bus, chip, static_data_chip, instruction)
+)]
 pub fn machine_derive(input: TokenStream) -> TokenStream {
     let ast = syn::parse(input).unwrap();
     impl_machine(&ast)
@@ -61,8 +64,18 @@ fn impl_machine(machine: &syn::DeriveInput) -> TokenStream {
             .expect("Invalid machine_fields attribute, expected #[machine_fields(<Val>)]");
         let val = &machine_fields.val;
 
+        let static_data_chip: Option<Ident> = chips
+            .iter()
+            .filter(|f| f.attrs.iter().any(|a| a.path.is_ident("static_data_chip")))
+            .map(|f| {
+                f.ident
+                    .clone()
+                    .expect("static data chip requires an identifier")
+            })
+            .next();
+
         let name = &machine.ident;
-        let run = run_method(machine, &instructions, &val);
+        let run = run_method(machine, &instructions, &val, &static_data_chip);
         let prove = prove_method(&chips);
         let verify = verify_method(&chips);
 
@@ -127,7 +140,12 @@ fn chip_methods(chip: &Field) -> TokenStream2 {
     }
 }
 
-fn run_method(machine: &syn::DeriveInput, instructions: &[&Field], val: &Ident) -> TokenStream2 {
+fn run_method(
+    machine: &syn::DeriveInput,
+    instructions: &[&Field],
+    val: &Ident,
+    static_data_chip: &Option<Ident>,
+) -> TokenStream2 {
     let name = &machine.ident;
     let (_, ty_generics, _) = machine.generics.split_for_impl();
 
@@ -143,8 +161,17 @@ fn run_method(machine: &syn::DeriveInput, instructions: &[&Field], val: &Ident)
         })
         .collect::<TokenStream2>();
 
+    let init_static_data: TokenStream2 = match static_data_chip {
+        Some(_static_data_chip) => quote! {
+            self.initialize_memory();
+        },
+        None => quote! {},
+    };
+
     quote! {
         fn run<Adv: ::valida_machine::AdviceProvider>(&mut self, program: &ProgramROM<i32>, advice: &mut Adv) {
+            #init_static_data
+
             loop {
                 // Fetch
                 let pc = self.cpu().pc;

memory/src/columns.rs

@@ -4,7 +4,7 @@ use valida_derive::AlignedBorrow;
 use valida_machine::Word;
 use valida_util::indices_arr;
 
-#[derive(AlignedBorrow, Default)]
+#[derive(AlignedBorrow, Default, Debug)]
 pub struct MemoryCols<T> {
     /// Memory address
     pub addr: T,
@@ -15,6 +15,9 @@ pub struct MemoryCols<T> {
     /// Main CPU clock cycle
     pub clk: T,
 
+    /// Flag indicating if this is an initial static data value or not
+    pub is_static_initial: T,
+
     /// Whether memory operation is a read
     pub is_read: T,