[JasonGross]

Stacked on #561: this branch contains #561's commits (the base branch lives on a fork, so GitHub cannot show the stacked diff alone). The Kami part is the last four commits, 728df75..efe4ea4; review those.

Pins deps/kami to mit-plv/kami#51, where Kami's word n is stdlib bits (Z.of_nat n) with the nat index kept, and simplifies the processor bridge accordingly: processor/src/processor/KamiWord.v shrinks from 598 to 332 lines because a Kami word 32 is now the same representation as coqutil's Naive.word 32, so the word.ok laws come from stdlib's Zmod lemmas instead of a hand-rolled bijection. The remaining edits are proof repairs in KamiRiscvStep.v (and KamiRiscv.v, End2EndPipeline.v) with unchanged statements; the last three commits follow Kami's Word.v cleanup (split1, wmsb, shifts and remainders as the stdlib operations, unused lemmas gone) and Kami's operations becoming the Zmod ones (the instance's fields are Zmod.add etc. and proofs name the stdlib lemmas; KamiRiscvStep.v keeps its simpl calls with file-local Arguments Z.pow/Z.of_nat : simpl never so the modulus stays folded) and Kami's Lt/Slt evaluating to Z.ltb (the instance's ltu/lts are Z.ltb on uwordToZ/wordToZ, and is_mmio_spec plus the eight branch cases decide that test from the riscv-side fact with one small tactic instead of change blocks); end2end/src/end2end/KamiRiscvWordProperties.v stays because it supplies word.riscv_ok for the Kami word (the division-by-zero and shift-masking conventions are unchanged). make all (compiler, processor, end2end, LiveVerif) passes; Print Assumptions end2end_lightbulb is unchanged. One caveat found on the way: with words as Zmod records, a bare lia whose Zify-translated context mentions many words can build a certificate deep enough to overflow the kernel stack at Qed (it did in End2EndPipeline.v); the offending step is now a small standalone lemma. Compile time of the processor + end2end cone is 10m09s versus 9m23s before the port (1.08x): the only real regression was a speculative eapply in prove_states_related that now failed slowly by unfolding through Zmod, fixed with simple eapply. After this port a failing eapply is much more expensive than a succeeding one, so simple eapply is the right tool wherever a hot tactic applies a lemma under try/repeat.

Depends on mit-plv/kami#51 and on #561; CI cannot fetch the pinned Kami commit until #51 merges, so this stays a draft until then.

Written by Claude Fable 5.1 and Claude Opus 5.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm

[JasonGross]

Stacked follow-up: #563 makes the Kami word instance be coqutil's Naive.word (all fields shown equal) and drops KamiRiscvWordProperties.v.

---

Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).