Skip to content

Commit 1cb93fe

Browse files
committed
completed range check implementation
1 parent d2d1d72 commit 1cb93fe

File tree

16 files changed

+991
-31
lines changed

16 files changed

+991
-31
lines changed

Cargo.lock

Lines changed: 1 addition & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

crates/lean_compiler/Cargo.toml

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -29,3 +29,6 @@ p3-poseidon2-air.workspace = true
2929
lookup.workspace = true
3030
lean_vm.workspace = true
3131
multilinear-toolkit.workspace = true
32+
33+
[dev-dependencies]
34+
rand_chacha = "0.9.0"

crates/lean_compiler/src/a_simplify_lang.rs

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -148,6 +148,10 @@ pub enum SimpleLine {
148148
LocationReport {
149149
location: SourceLineNumber,
150150
},
151+
RangeCheck {
152+
value: SimpleExpr,
153+
max: ConstExpression,
154+
},
151155
}
152156

153157
pub fn simplify_program(mut program: Program) -> SimpleProgram {
@@ -690,6 +694,14 @@ fn simplify_lines(
690694
location: *location,
691695
});
692696
}
697+
Line::RangeCheck { value, max } => {
698+
let simplified_value =
699+
simplify_expr(value, &mut res, counters, array_manager, const_malloc);
700+
res.push(SimpleLine::RangeCheck {
701+
value: simplified_value,
702+
max: max.clone(),
703+
});
704+
}
693705
}
694706
}
695707

@@ -898,7 +910,7 @@ pub fn find_variable_usage(lines: &[Line]) -> (BTreeSet<Var>, BTreeSet<Var>) {
898910
on_new_expr(index, &internal_vars, &mut external_vars);
899911
on_new_expr(value, &internal_vars, &mut external_vars);
900912
}
901-
Line::Panic | Line::Break | Line::LocationReport { .. } => {}
913+
Line::Panic | Line::Break | Line::LocationReport { .. } | Line::RangeCheck { .. } => {}
902914
}
903915
}
904916

@@ -1062,7 +1074,7 @@ pub fn inline_lines(
10621074
inline_expr(index, args, inlining_count);
10631075
inline_expr(value, args, inlining_count);
10641076
}
1065-
Line::Panic | Line::Break | Line::LocationReport { .. } => {}
1077+
Line::Panic | Line::Break | Line::LocationReport { .. } | Line::RangeCheck { .. } => {}
10661078
}
10671079
}
10681080
for (i, new_lines) in lines_to_replace.into_iter().rev() {
@@ -1531,7 +1543,7 @@ fn replace_vars_for_unroll(
15311543
Line::CounterHint { var } => {
15321544
*var = format!("@unrolled_{unroll_index}_{iterator_value}_{var}");
15331545
}
1534-
Line::Break | Line::Panic | Line::LocationReport { .. } => {}
1546+
Line::Break | Line::Panic | Line::LocationReport { .. } | Line::RangeCheck { .. } => {}
15351547
}
15361548
}
15371549
}
@@ -1921,7 +1933,8 @@ fn get_function_called(lines: &[Line], function_called: &mut Vec<String>) {
19211933
| Line::MAlloc { .. }
19221934
| Line::Panic
19231935
| Line::Break
1924-
| Line::LocationReport { .. } => {}
1936+
| Line::LocationReport { .. }
1937+
| Line::RangeCheck { .. } => {}
19251938
}
19261939
}
19271940
}
@@ -2025,7 +2038,7 @@ fn replace_vars_by_const_in_lines(lines: &mut [Line], map: &BTreeMap<Var, F>) {
20252038
assert!(!map.contains_key(var), "Variable {var} is a constant");
20262039
replace_vars_by_const_in_expr(size, map);
20272040
}
2028-
Line::Panic | Line::Break | Line::LocationReport { .. } => {}
2041+
Line::Panic | Line::Break | Line::LocationReport { .. } | Line::RangeCheck { .. } => {}
20292042
}
20302043
}
20312044
}
@@ -2213,6 +2226,9 @@ impl SimpleLine {
22132226
}
22142227
Self::Panic => "panic".to_string(),
22152228
Self::LocationReport { .. } => Default::default(),
2229+
Self::RangeCheck { value, max } => {
2230+
format!("range_check({value}, {max})")
2231+
}
22162232
};
22172233
format!("{spaces}{line_str}")
22182234
}

crates/lean_compiler/src/b_compile_intermediate.rs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -597,6 +597,12 @@ fn compile_lines(
597597
location: *location,
598598
});
599599
}
600+
SimpleLine::RangeCheck { value, max } => {
601+
instructions.push(IntermediateInstruction::RangeCheck {
602+
value: IntermediateValue::from_simple_expr(value, compiler),
603+
max: max.clone(),
604+
});
605+
}
600606
}
601607
}
602608

@@ -795,7 +801,8 @@ fn find_internal_vars(lines: &[SimpleLine]) -> BTreeSet<Var> {
795801
| SimpleLine::Print { .. }
796802
| SimpleLine::FunctionRet { .. }
797803
| SimpleLine::Precompile { .. }
798-
| SimpleLine::LocationReport { .. } => {}
804+
| SimpleLine::LocationReport { .. }
805+
| SimpleLine::RangeCheck { .. } => {}
799806
}
800807
}
801808
internal_vars

crates/lean_compiler/src/c_compile_final.rs renamed to crates/lean_compiler/src/c_compile_to_low_level_bytecode.rs

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ impl IntermediateInstruction {
1313
| Self::DecomposeCustom { .. }
1414
| Self::CounterHint { .. }
1515
| Self::Inverse { .. }
16-
| Self::LocationReport { .. } => true,
16+
| Self::LocationReport { .. }
17+
| Self::RangeCheck { .. } => true,
1718
Self::Computation { .. }
1819
| Self::Panic
1920
| Self::Deref { .. }
@@ -307,6 +308,14 @@ fn compile_block(
307308
n_vars: eval_const_expression_usize(&n_vars, compiler),
308309
});
309310
}
311+
IntermediateInstruction::RangeCheck { value, max } => {
312+
let hint = Hint::RangeCheck {
313+
value: value.try_into_mem_or_fp(compiler).unwrap(),
314+
// TODO: support max being an IntermediateValue
315+
max: MemOrConstant::Constant(eval_const_expression(&max, compiler)),
316+
};
317+
hints.entry(pc).or_default().push(hint);
318+
}
310319
IntermediateInstruction::DecomposeBits {
311320
res_offset,
312321
to_decompose,
Lines changed: 248 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,248 @@
1+
use lean_vm::*;
2+
use p3_field::PrimeCharacteristicRing;
3+
use std::collections::{BTreeMap, BTreeSet};
4+
use utils::ToUsize;
5+
6+
#[derive(Debug, Clone)]
7+
pub struct RangeCheckInfo {
8+
pub hint_fp: usize,
9+
pub v_pos: usize,
10+
pub v: usize,
11+
pub t: usize,
12+
pub q: usize, // t - 1 - v
13+
}
14+
15+
fn find_next_zero_cell(memory: &Memory, start_offset: usize) -> Option<usize> {
16+
if start_offset >= memory.0.len() {
17+
return None;
18+
}
19+
let mut z = start_offset;
20+
21+
loop {
22+
if z >= memory.0.len() {
23+
break;
24+
}
25+
let m_fp_z = &memory.get(z);
26+
if !m_fp_z.is_err() && m_fp_z.clone().unwrap() == F::ZERO {
27+
return Some(z);
28+
}
29+
z += 1;
30+
}
31+
None
32+
}
33+
34+
fn find_next_undefined_cell_from_mem(
35+
mem: &Memory,
36+
conflicts: &BTreeSet<usize>,
37+
pos: usize,
38+
) -> usize {
39+
let mut z = pos;
40+
41+
while !matches!(mem.get(z), Err(RunnerError::UndefinedMemory)) {
42+
z += 1;
43+
}
44+
45+
loop {
46+
if conflicts.contains(&z) {
47+
z = find_next_undefined_cell_from_mem(mem, conflicts, z + 1);
48+
} else {
49+
break;
50+
}
51+
}
52+
z
53+
}
54+
55+
pub fn is_undef(mem: &Memory, pos: usize) -> bool {
56+
matches!(mem.get(pos), Err(RunnerError::UndefinedMemory))
57+
}
58+
59+
pub fn compile_range_checks(
60+
first_exec: &ExecutionResult,
61+
bytecode: &Bytecode,
62+
) -> Result<Bytecode, RunnerError> {
63+
// Early return if no range checks exist
64+
if !bytecode
65+
.hints
66+
.values()
67+
.any(|hints| hints.iter().any(|h| matches!(h, Hint::RangeCheck { .. })))
68+
{
69+
return Ok(bytecode.clone());
70+
}
71+
72+
// Convenience mapping: instr_idx -> RangeCheckInfo
73+
let mut rcs: BTreeMap<(usize, usize), RangeCheckInfo> = BTreeMap::new();
74+
75+
// Validate that the last fp is 0
76+
let last_fp = first_exec.fps.last().ok_or(RunnerError::PCOutOfBounds)?; // Using existing error type
77+
if *last_fp != 0 {
78+
return Err(RunnerError::PCOutOfBounds); // Using existing error type for now
79+
}
80+
81+
// Find the penultimate instruction
82+
let pen_instr = bytecode.instructions[first_exec.pcs[first_exec.pcs.len() - 2]].clone();
83+
84+
// Assume that the penultimate instruction is a JUMP
85+
assert!(matches!(pen_instr, Instruction::Jump { .. }));
86+
87+
// Assume that the destination of the penultimate jump is the last instruction
88+
match pen_instr {
89+
Instruction::Jump { dest, .. } => match dest {
90+
MemOrConstant::Constant(c) => {
91+
assert_eq!(c.to_usize(), first_exec.pcs[first_exec.pcs.len() - 1]);
92+
}
93+
MemOrConstant::MemoryAfterFp { .. } => {
94+
unreachable!();
95+
}
96+
},
97+
_ => {}
98+
}
99+
100+
// Keep track of memory locations we will write to
101+
let mut conflicts: BTreeSet<usize> = BTreeSet::new();
102+
103+
for (pc, hints) in &bytecode.hints {
104+
for (hint_idx, hint) in hints.iter().enumerate() {
105+
match hint {
106+
Hint::RangeCheck { value, max } => {
107+
let v_off = match value {
108+
MemOrFp::MemoryAfterFp { offset } => *offset,
109+
MemOrFp::Fp => 0, // fp is at offset 0
110+
};
111+
let execution_step = first_exec.pcs.iter().position(|&p| p == *pc).unwrap();
112+
let hint_fp = first_exec.fps[execution_step];
113+
let v_pos = hint_fp + v_off;
114+
let v = first_exec.memory.get(v_pos).unwrap().to_usize();
115+
let t = match max {
116+
MemOrConstant::MemoryAfterFp { .. } => {
117+
unreachable!();
118+
}
119+
MemOrConstant::Constant(c) => c.to_usize(),
120+
};
121+
122+
// q = t - 1 - v in the field
123+
let q = (F::from_usize(t) - F::ONE - F::from_usize(v)).to_usize();
124+
125+
rcs.insert(
126+
(*pc, hint_idx),
127+
RangeCheckInfo {
128+
hint_fp,
129+
v_pos,
130+
v,
131+
t,
132+
q,
133+
},
134+
);
135+
136+
conflicts.insert(v);
137+
conflicts.insert(t);
138+
}
139+
_ => {}
140+
}
141+
}
142+
}
143+
144+
// Since the range check vals are referenced by offset, our fp must be the smallest possible
145+
// value: 0.
146+
let fp = 0;
147+
148+
let mut instrs_to_insert: Vec<Instruction> = vec![];
149+
150+
// Look for any 0 cells past fp, or create one
151+
let z_pos = find_next_zero_cell(&first_exec.memory, fp).unwrap_or_else(|| {
152+
let z_pos = find_next_undefined_cell_from_mem(&first_exec.memory, &conflicts, fp);
153+
if first_exec.memory.get(z_pos).is_err() {
154+
let z_instr = Instruction::Computation {
155+
operation: Operation::Add,
156+
arg_a: MemOrConstant::Constant(F::ZERO),
157+
arg_c: MemOrFp::MemoryAfterFp { offset: z_pos - fp },
158+
res: MemOrConstant::Constant(F::ZERO),
159+
};
160+
instrs_to_insert.push(z_instr);
161+
}
162+
z_pos
163+
});
164+
165+
conflicts.insert(z_pos);
166+
167+
for ((_pc, _hint_idx), rc_info) in &rcs {
168+
// Step 1: DEREF m[m[fp + x]] == m[fp + i]
169+
let i = if is_undef(&first_exec.memory, rc_info.v) {
170+
// if m[v] is undefined, use z
171+
z_pos
172+
} else {
173+
// if m[v] is defined, then search for an i where m[fp + i] is undefined
174+
find_next_undefined_cell_from_mem(&first_exec.memory, &conflicts, fp)
175+
};
176+
let step_1 = Instruction::Deref {
177+
shift_0: rc_info.v_pos - fp,
178+
shift_1: 0,
179+
res: MemOrFpOrConstant::MemoryAfterFp { offset: i - fp },
180+
};
181+
182+
// Since the step 1 deref writes to m[i], add i to conflicts
183+
conflicts.insert(i);
184+
185+
// Step 2: ADD m[fp + j] = t - 1 - v
186+
let j = find_next_undefined_cell_from_mem(&first_exec.memory, &conflicts, i);
187+
let step_2 = Instruction::Computation {
188+
operation: Operation::Add,
189+
arg_a: MemOrConstant::Constant(F::ZERO), // 0
190+
arg_c: MemOrFp::MemoryAfterFp { offset: j - fp }, // Unknown; solves to t - 1 - v
191+
res: MemOrConstant::Constant(F::from_usize(rc_info.q)), // t - 1 - v
192+
};
193+
194+
// Since the step 2 add writes to m[j], add j to conflicts
195+
conflicts.insert(j);
196+
197+
// Step 3: DEREF m[fp + k] = m[m[fp + j]]
198+
let k = if is_undef(&first_exec.memory, rc_info.q) && !conflicts.contains(&rc_info.q) {
199+
// if m[q] is undefined, use z
200+
z_pos
201+
} else {
202+
// if m[q] is defined, then search for an k where m[fp + k] is undefined
203+
find_next_undefined_cell_from_mem(&first_exec.memory, &conflicts, j)
204+
};
205+
206+
let step_3 = Instruction::Deref {
207+
shift_0: j - fp,
208+
shift_1: 0,
209+
res: MemOrFpOrConstant::MemoryAfterFp { offset: k - fp },
210+
};
211+
212+
// Since the step 3 deref may write to m[k] or m[q], add q and k to conflicts
213+
conflicts.insert(k);
214+
conflicts.insert(rc_info.q);
215+
216+
instrs_to_insert.push(step_1);
217+
instrs_to_insert.push(step_2);
218+
instrs_to_insert.push(step_3);
219+
}
220+
221+
// Create the updated bytecode with range check instructions appended at the end
222+
let mut updated_bytecode = bytecode.clone();
223+
224+
// Find the index of the penultimate instruction in the instruction list
225+
let penultimate_pc = first_exec.pcs[first_exec.pcs.len() - 2];
226+
227+
// Append the range check instructions to the end
228+
let first_range_check_pc = updated_bytecode.instructions.len();
229+
updated_bytecode.instructions.extend(instrs_to_insert);
230+
231+
// Add a final jump that terminates execution
232+
updated_bytecode.instructions.push(Instruction::Jump {
233+
condition: MemOrConstant::Constant(F::ZERO), // Never jump - terminates execution
234+
dest: MemOrConstant::Constant(F::ZERO), // Doesn't matter since condition is false
235+
updated_fp: MemOrFp::Fp,
236+
label: Label::custom("termination_jump".to_string()),
237+
});
238+
239+
// Update the penultimate jump to point to the first range check instruction
240+
if let Instruction::Jump { dest, .. } = &mut updated_bytecode.instructions[penultimate_pc] {
241+
*dest = MemOrConstant::Constant(F::from_usize(first_range_check_pc));
242+
}
243+
244+
// Update ending_pc to point after the final jump
245+
updated_bytecode.ending_pc = updated_bytecode.instructions.len();
246+
247+
Ok(updated_bytecode)
248+
}

0 commit comments

Comments
 (0)