fix(bug): soundness and constraints for formal verification - #101

Closed

eason1981 wants to merge 12 commits into

mainfrom

formal-verification-fixes

Commits on May 20, 2026

fix(alu): address Nethermind soundness bugs in LT, SR, SLL constraints
eason
committed
f4cdc89
fix(cpu): enforce JALR bit-0 clearing in constraints and trace
eason
committed
64dcf10

Commits on May 21, 2026

fix(alu): enforce remainder < divisor in divrem constraints
eason
committed
0786b8b

Commits on May 22, 2026

fix(alu): bind quot_msb to quotient bit-31 in divrem word constraints
eason
committed
ddd0d96
fix(alu): enforce sign/zero extension of c upper limbs in divrem word constraints
eason
committed
f35b17d
fix(alu): enforce sign/zero extension of b upper limbs in divrem word constraints
eason
committed
b6f2de0

Commits on May 31, 2026

fix(alu): close two soundness gaps in ShiftRight chip constraints
eason
committed
0bacdaf

Commits on Jun 4, 2026

fix(memory): remove addr_aligned free witness, compute inline in eval_memory_access
eason
committed
db682d9
fix(memory): pin op_a to zero when rd = x0 in load instructions
eason
committed
7860af1
fix(memory): range-check high byte of selected_limb for LB/LBU
eason
committed
fc197c0
refactor(memory): replace op_b_access/op_c_access MemoryReadCols with Word
eason
committed
0ecd943

Commits on Jun 5, 2026

Revert "fix(memory): pin op_a to zero when rd = x0 in load instructions"
eason
committed
e128062