Branch for fixing the self-writing bug with overlapping non-identical addresses - #18

Open

kristinas wants to merge 17 commits into

mainfrom

kristina-fix-self-writing-bug

Commits on Sep 9, 2026

Remove dead code from ISA module

kristinas
and
claude
committed
75bfd0c
Regenerate stack.yaml.lock to fix stale GitHub archive hashes

kristinas
and
claude
committed
94b0770
reorder conditions for stall
kristinas
committed
a4c2284
Halting moved from memory to writeback
kristinas
committed
a937320
Fixed address overlap bug
kristinas
committed
18a3598

Commits on Sep 10, 2026

Functional correctness
kristinas
committed
2340cdf
Put the SMT obligations behind a flag so CI can build without a solver

kristinas
and
claude
committed
2952242
Merge main into kristina-fix-self-writing-bug (PR #18)
windtf
committed
965dcb0

Commits on Sep 14, 2026

Quantify the architectural PC in the inductive steps

kristinas
and
claude
committed
805367e
Export KState to silence a spurious unused-constructor warning

kristinas
and
claude
committed
523afac
Read the pointwise invariant off the real flush instead of hand copies

kristinas
and
claude
committed
f9ef8a9
Bind the next architectural state before stating each conclusion

kristinas
and
claude
committed
925a72b
Import only the ISA names each module uses

kristinas
and
claude
committed
8e16e34
State the reset hop as the base case instead of a startup invariant case

kristinas
and
claude
committed
484d39d
Refer to Syscall unqualified in the halted cases, like EBreak

kristinas
and
claude
committed
7e1d5f9
Remove isArithOrJumpInstr, which only one test used

kristinas
and
claude
committed
fcf63b2
Say in package.yaml that CI now discharges the proof with bitwuzla

kristinas
and
claude
committed
9d7c066