-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
**Trace generation** - Expand `StepRecord` to support multiple accesses to registers and memory (beyond standard instructions). - Introduce a module for syscall witness generation. See `fn handle_syscall(…)` - Witness generation for Keccak-f. Same format as sp1. - Runtime wrapper function `syscall_keccak_permute`. - Test program using Keccak-f and concrete values. **Circuit part** ([standalone diff here](https://github.com/Inversed-Tech/ceno/pull/1/files)) There is a placeholder for upcoming precompile circuits. The real implementation must have the same effects as this one (same memory writes, etc). - `LargeEcallDummy` is an extension of the dummy circuit to support precompiles. - Support any number of registers and memory accesses. - New testing technique using the real trace generator instead of artificial StepRecord’s. See `keccak_step`. --------- Co-authored-by: Aurélien Nicolas <[email protected]>
- Loading branch information
Showing
22 changed files
with
598 additions
and
45 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,64 @@ | ||
use crate::{RegIdx, Tracer, VMState, Word, WordAddr, WriteOp}; | ||
use anyhow::Result; | ||
|
||
pub mod keccak_permute; | ||
|
||
// Using the same function codes as sp1: | ||
// https://github.com/succinctlabs/sp1/blob/013c24ea2fa15a0e7ed94f7d11a7ada4baa39ab9/crates/core/executor/src/syscalls/code.rs | ||
|
||
pub const KECCAK_PERMUTE: u32 = 0x00_01_01_09; | ||
|
||
/// Trace the inputs and effects of a syscall. | ||
pub fn handle_syscall(vm: &VMState, function_code: u32) -> Result<SyscallEffects> { | ||
match function_code { | ||
KECCAK_PERMUTE => Ok(keccak_permute::keccak_permute(vm)), | ||
// TODO: introduce error types. | ||
_ => Err(anyhow::anyhow!("Unknown syscall: {}", function_code)), | ||
} | ||
} | ||
|
||
/// A syscall event, available to the circuit witness generators. | ||
#[derive(Clone, Debug, Default, PartialEq, Eq)] | ||
pub struct SyscallWitness { | ||
pub mem_ops: Vec<WriteOp>, | ||
pub reg_ops: Vec<WriteOp>, | ||
} | ||
|
||
/// The effects of a syscall to apply on the VM. | ||
#[derive(Clone, Debug, Default, PartialEq, Eq)] | ||
pub struct SyscallEffects { | ||
/// The witness being built. Get it with `finalize`. | ||
witness: SyscallWitness, | ||
|
||
/// The next PC after the syscall. Defaults to the next instruction. | ||
pub next_pc: Option<u32>, | ||
} | ||
|
||
impl SyscallEffects { | ||
/// Iterate over the register values after the syscall. | ||
pub fn iter_reg_values(&self) -> impl Iterator<Item = (RegIdx, Word)> + '_ { | ||
self.witness | ||
.reg_ops | ||
.iter() | ||
.map(|op| (op.register_index(), op.value.after)) | ||
} | ||
|
||
/// Iterate over the memory values after the syscall. | ||
pub fn iter_mem_values(&self) -> impl Iterator<Item = (WordAddr, Word)> + '_ { | ||
self.witness | ||
.mem_ops | ||
.iter() | ||
.map(|op| (op.addr, op.value.after)) | ||
} | ||
|
||
/// Keep track of the cycles of registers and memory accesses. | ||
pub fn finalize(mut self, tracer: &mut Tracer) -> SyscallWitness { | ||
for op in &mut self.witness.reg_ops { | ||
op.previous_cycle = tracer.track_access(op.addr, Tracer::SUBCYCLE_RD); | ||
} | ||
for op in &mut self.witness.mem_ops { | ||
op.previous_cycle = tracer.track_access(op.addr, Tracer::SUBCYCLE_MEM); | ||
} | ||
self.witness | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,65 @@ | ||
use itertools::{Itertools, izip}; | ||
use tiny_keccak::keccakf; | ||
|
||
use crate::{Change, EmuContext, Platform, VMState, WORD_SIZE, WordAddr, WriteOp}; | ||
|
||
use super::{SyscallEffects, SyscallWitness}; | ||
|
||
const KECCAK_CELLS: usize = 25; // u64 cells | ||
pub const KECCAK_WORDS: usize = KECCAK_CELLS * 2; // u32 words | ||
|
||
/// Trace the execution of a Keccak permutation. | ||
/// | ||
/// Compatible with: | ||
/// https://github.com/succinctlabs/sp1/blob/013c24ea2fa15a0e7ed94f7d11a7ada4baa39ab9/crates/core/executor/src/syscalls/precompiles/keccak256/permute.rs | ||
/// | ||
/// TODO: test compatibility. | ||
pub fn keccak_permute(vm: &VMState) -> SyscallEffects { | ||
let state_ptr = vm.peek_register(Platform::reg_arg0()); | ||
|
||
// Read the argument `state_ptr`. | ||
let reg_ops = vec![WriteOp::new_register_op( | ||
Platform::reg_arg0(), | ||
Change::new(state_ptr, state_ptr), | ||
0, // Cycle set later in finalize(). | ||
)]; | ||
|
||
let addrs = (state_ptr..) | ||
.step_by(WORD_SIZE) | ||
.take(KECCAK_WORDS) | ||
.map(WordAddr::from) | ||
.collect_vec(); | ||
|
||
// Read Keccak state. | ||
let input = addrs | ||
.iter() | ||
.map(|&addr| vm.peek_memory(addr)) | ||
.collect::<Vec<_>>(); | ||
|
||
// Compute Keccak permutation. | ||
let output = { | ||
let mut state = [0_u64; KECCAK_CELLS]; | ||
for (cell, (&lo, &hi)) in izip!(&mut state, input.iter().tuples()) { | ||
*cell = lo as u64 | (hi as u64) << 32; | ||
} | ||
|
||
keccakf(&mut state); | ||
|
||
state.into_iter().flat_map(|c| [c as u32, (c >> 32) as u32]) | ||
}; | ||
|
||
// Write permuted state. | ||
let mem_ops = izip!(addrs, input, output) | ||
.map(|(addr, before, after)| WriteOp { | ||
addr, | ||
value: Change { before, after }, | ||
previous_cycle: 0, // Cycle set later in finalize(). | ||
}) | ||
.collect_vec(); | ||
|
||
assert_eq!(mem_ops.len(), KECCAK_WORDS); | ||
SyscallEffects { | ||
witness: SyscallWitness { mem_ops, reg_ops }, | ||
next_pc: None, | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
use crate::{ | ||
CENO_PLATFORM, InsnKind, Instruction, Platform, Program, StepRecord, VMState, encode_rv32, | ||
encode_rv32u, syscalls::KECCAK_PERMUTE, | ||
}; | ||
use anyhow::Result; | ||
|
||
pub fn keccak_step() -> (StepRecord, Vec<Instruction>) { | ||
let instructions = vec![ | ||
// Call Keccak-f. | ||
load_immediate(Platform::reg_arg0() as u32, CENO_PLATFORM.heap.start), | ||
load_immediate(Platform::reg_ecall() as u32, KECCAK_PERMUTE), | ||
encode_rv32(InsnKind::ECALL, 0, 0, 0, 0), | ||
// Halt. | ||
load_immediate(Platform::reg_ecall() as u32, Platform::ecall_halt()), | ||
encode_rv32(InsnKind::ECALL, 0, 0, 0, 0), | ||
]; | ||
|
||
let pc = CENO_PLATFORM.pc_base(); | ||
let program = Program::new(pc, pc, instructions.clone(), Default::default()); | ||
let mut vm = VMState::new(CENO_PLATFORM, program.into()); | ||
let steps = vm.iter_until_halt().collect::<Result<Vec<_>>>().unwrap(); | ||
|
||
(steps[2].clone(), instructions) | ||
} | ||
|
||
const fn load_immediate(rd: u32, imm: u32) -> Instruction { | ||
encode_rv32u(InsnKind::ADDI, 0, 0, rd, imm) | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.