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

Open

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
fix(cpu): enforce JALR bit-0 clearing in constraints and trace
eason
committed

Commits on May 21, 2026

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

Commits on May 22, 2026

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

Commits on May 31, 2026

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

Commits on Jun 4, 2026

Commits on Jun 5, 2026

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