[JasonGross]

Stacked on #562 (which is stacked on #561); this branch contains their commits, and the new part is the last commit, d7805a7.

Follow-up to a review question on mit-plv/coqutil#186: with Kami's word now stdlib bits, the Kami-side word instance in processor/src/processor/KamiWord.v and coqutil's Naive.word agree on all 26 fields at widths 32 and 8 (division by zero, signed overflow, shift amounts at or above the width, sextend, the mulh* family, comparisons), as lemmas. So the hand-written instance is replaced by Naive.word field for field (the rep is still spelled as Kami's nat-indexed type, because a bare alias breaks Word.word ?sz unification at every Kami use site), word 32 = Naive.word 32 holds by reflexivity, word.ok comes from Naive.ok, and end2end/src/end2end/KamiRiscvWordProperties.v is deleted: word.riscv_ok now comes from the compiler's NaiveRiscvWordProperties.v. kunsigned is Zmod.unsigned; proofs that used to cbv through the instance rewrite with a few spelling lemmas instead. No theorem statement changes; Print Assumptions end2end_lightbulb is byte-identical (the same 8 axioms).

On the reviewer's question whether Naive's adjust_too_big_shift_amount is still needed: it is, but not for the lightbulb proof specifically. An unadjusted Naive.word violates riscv_ok's slu_ignores_hibits (counterexample at y = 1, z = 32, proved in the analysis), so the adjustment is what makes Naive.word satisfy the RISC-V shift convention for the compiler theorem. Before this change the lightbulb proof used the Kami-side instance's own mod width masking; after it, it relies on Naive's adjustment like every other Naive user.

make all passes in 9m21s (KamiRiscvStep.v 7m52s, faster than before the Kami port). Depends on mit-plv/kami#51 and #562.

Written by Claude Fable 5.1.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm

[andres-erbsen]

Please include this same in the same multi-repo PR set as removing the Word interface in favor of direct use of stdlib bits.

[JasonGross]

Will do: the unification lands inside the word-removal set (the processor width is a concrete 32, so Kami's word 32 is convertible to bits 32 and this file's instance disappears with the interface); the plan is summarized on mit-plv/coqutil#186. This PR stays as is until that set replaces it.

---

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