Skip to content

Commit 3dff033

Browse files
author
jagdeep sidhu
committed
Update dump_shrink_verify_constraints.rs
1 parent 9dba80c commit 3dff033

File tree

1 file changed

+49
-1
lines changed

1 file changed

+49
-1
lines changed

crates/prover/src/bin/dump_shrink_verify_constraints.rs

Lines changed: 49 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -482,6 +482,51 @@ fn fix_input_public_values_digest(
482482
}
483483
}
484484

485+
fn report_runtime_error(
486+
err: &sp1_recursion_core::RuntimeError<BabyBear, <InnerSC as StarkGenericConfig>::Challenge>,
487+
runtime: &sp1_recursion_core::Runtime<
488+
BabyBear,
489+
<InnerSC as StarkGenericConfig>::Challenge,
490+
DiffusionMatrixBabyBear,
491+
>,
492+
asm: &sp1_recursion_compiler::circuit::AsmCompiler<InnerConfig>,
493+
) {
494+
use sp1_recursion_core::{Address, BaseAluInstr, BaseAluOpcode};
495+
496+
if let sp1_recursion_core::RuntimeError::DivFOutOfDomain { in1, in2, instr, .. } = err {
497+
let BaseAluInstr { opcode, addrs, .. } = instr;
498+
let BaseAluOpcode::DivF = opcode else { return };
499+
let addr_in1 = addrs.in1.as_usize();
500+
let addr_in2 = addrs.in2.as_usize();
501+
let addr_out = addrs.out.as_usize();
502+
503+
let vaddr_in1 = find_vaddr_for_phys(asm, addrs.in1);
504+
let vaddr_in2 = find_vaddr_for_phys(asm, addrs.in2);
505+
let vaddr_out = find_vaddr_for_phys(asm, addrs.out);
506+
507+
eprintln!("DivFOutOfDomain at runtime:");
508+
eprintln!(" in1={in1:?} (phys={addr_in1}, vaddr={vaddr_in1:?})");
509+
eprintln!(" in2={in2:?} (phys={addr_in2}, vaddr={vaddr_in2:?})");
510+
eprintln!(" out phys={addr_out}, vaddr={vaddr_out:?}");
511+
512+
let mem = &runtime.memory;
513+
let read_val = |addr: Address<BabyBear>| mem.mr(addr).map(|entry| entry.val[0]);
514+
eprintln!(" mem[in1]={:?}", read_val(addrs.in1));
515+
eprintln!(" mem[in2]={:?}", read_val(addrs.in2));
516+
eprintln!(" mem[out]={:?}", read_val(addrs.out));
517+
}
518+
}
519+
520+
fn find_vaddr_for_phys(
521+
asm: &sp1_recursion_compiler::circuit::AsmCompiler<InnerConfig>,
522+
addr: sp1_recursion_core::Address<BabyBear>,
523+
) -> Option<usize> {
524+
let target = addr.as_usize();
525+
asm.virtual_to_physical
526+
.iter()
527+
.find_map(|(vaddr, phys)| if phys.as_usize() == target { Some(vaddr) } else { None })
528+
}
529+
485530
/// Audit that the lifted LF-targeted R1CS cannot exploit modulus wraparound when proven in Frog64
486531
/// under the current SP1/Frog64 boundedness regime (currently `decomp_b=12, k=8` in LF+).
487532
///
@@ -868,7 +913,10 @@ fn main() {
868913
Witnessable::<InnerConfig>::write(input_with_merkle, &mut witness_blocks);
869914
let witness_blocks_for_fill = witness_blocks.clone();
870915
runtime.witness_stream = witness_blocks.into();
871-
runtime.run().unwrap();
916+
if let Err(err) = runtime.run() {
917+
report_runtime_error(&err, &runtime, &asm);
918+
panic!("runtime error during witness fill: {err:?}");
919+
}
872920

873921
// Compile to R1CS **and** generate the full witness in one pass.
874922
//

0 commit comments

Comments
 (0)