diff --git a/ceno_zkvm/examples/riscv_opcodes.rs b/ceno_zkvm/examples/riscv_opcodes.rs index 9aa7631d6..55c2b8d07 100644 --- a/ceno_zkvm/examples/riscv_opcodes.rs +++ b/ceno_zkvm/examples/riscv_opcodes.rs @@ -10,10 +10,11 @@ use const_env::from_env; use ceno_emul::{ ByteAddr, - InsnKind::{ADD, BLT}, + InsnKind::{ADD, BLT, EANY}, StepRecord, VMState, CENO_PLATFORM, }; use ceno_zkvm::{ + instructions::riscv::ecall::HaltInstruction, scheme::{constants::MAX_NUM_VARIABLES, verifier::ZKVMVerifier}, structs::{ZKVMConstraintSystem, ZKVMFixedTraces, ZKVMWitnesses}, tables::{AndTableCircuit, LtuTableCircuit, U16TableCircuit}, @@ -104,6 +105,7 @@ fn main() { // opcode circuits let add_config = zkvm_cs.register_opcode_circuit::>(); let blt_config = zkvm_cs.register_opcode_circuit::(); + let halt_config = zkvm_cs.register_opcode_circuit::>(); // tables let u16_range_config = zkvm_cs.register_table_circuit::>(); // let u1_range_config = zkvm_cs.register_table_circuit::>(); @@ -120,6 +122,7 @@ fn main() { let mut zkvm_fixed_traces = ZKVMFixedTraces::default(); zkvm_fixed_traces.register_opcode_circuit::>(&zkvm_cs); zkvm_fixed_traces.register_opcode_circuit::(&zkvm_cs); + zkvm_fixed_traces.register_opcode_circuit::>(&zkvm_cs); zkvm_fixed_traces.register_table_circuit::>( &zkvm_cs, @@ -179,12 +182,18 @@ fn main() { .collect::>(); let mut add_records = Vec::new(); let mut blt_records = Vec::new(); - all_records.iter().for_each(|record| { + let mut halt_records = Vec::new(); + all_records.into_iter().for_each(|record| { let kind = record.insn().kind().1; - if kind == ADD { - add_records.push(record.clone()); - } else if kind == BLT { - blt_records.push(record.clone()); + match kind { + ADD => add_records.push(record), + BLT => blt_records.push(record), + EANY => { + if record.rs1().unwrap().value == CENO_PLATFORM.ecall_halt() { + halt_records.push(record); + } + } + _ => {} } }); @@ -202,6 +211,10 @@ fn main() { zkvm_witness .assign_opcode_circuit::(&zkvm_cs, &blt_config, blt_records) .unwrap(); + zkvm_witness + .assign_opcode_circuit::>(&zkvm_cs, &halt_config, halt_records) + .unwrap(); + zkvm_witness.finalize_lk_multiplicities(); // assign table circuits zkvm_witness diff --git a/ceno_zkvm/src/instructions/riscv/ecall.rs b/ceno_zkvm/src/instructions/riscv/ecall.rs index 0c75fc9e0..76c1c04e6 100644 --- a/ceno_zkvm/src/instructions/riscv/ecall.rs +++ b/ceno_zkvm/src/instructions/riscv/ecall.rs @@ -1 +1,3 @@ mod halt; + +pub use halt::HaltInstruction; diff --git a/ceno_zkvm/src/instructions/riscv/ecall/halt.rs b/ceno_zkvm/src/instructions/riscv/ecall/halt.rs index 0d39e2378..bb1d15cce 100644 --- a/ceno_zkvm/src/instructions/riscv/ecall/halt.rs +++ b/ceno_zkvm/src/instructions/riscv/ecall/halt.rs @@ -26,9 +26,9 @@ pub struct HaltConfig { lt_x10_cfg: ExprLtConfig, } -pub struct HaltCircuit(PhantomData); +pub struct HaltInstruction(PhantomData); -impl Instruction for HaltCircuit { +impl Instruction for HaltInstruction { type InstructionConfig = HaltConfig; fn name() -> String {