Alternate: Kami word directly on stdlib Zmod (comparison with #51) - #52
Closed
JasonGross wants to merge 1 commit into
Closed
JasonGross wants to merge 1 commit into
JasonGross wants to merge 1 commit into
Conversation
Make `word n` the standard library's `Zmod (Zpow2 n)` (with `Zpow2 n := 2 ^ Z.of_nat n`, so `word n` is `bits (Z.of_nat n)`) and make Kami's operations the Zmod operations themselves: `wplus` is `Zmod.add`, `wneg` is `Zmod.opp`, `wzero sz` is `Zmod.zero`, `wordToZ` is `Zmod.signed`, `wlt` is `Z.lt` on `Zmod.unsigned`, and so on, as notations. Only the operations whose shape the standard library does not have are definitions of their own: the nat/N conversions (`natToWord`, `wordToNat`, ...), the width-changing operations (`WS`, `wtl`, `combine`, `split1/2`, `sext`, `zext`, `extz`), the nat-indexed shifts, `wmsb`, `weq`, and the divisions with Kami's zero-divisor convention (`wdivN`, `wremN`, `wdivZ`, `wremZ`). The nat-indexed lemma library of Word.v is dropped rather than reproved. Word.v keeps the `unsigned_*` characterizations of its own definitions, a rewrite database that combines them with the standard library's `unsigned_add`/`unsigned_sub`/`unsigned_opp`/`unsigned_of_Z`/..., the `word_to_Z`/`word_lia_Z` tactics that move a word goal to `Z`, the `word_rect` eliminator, and the handful of nat-view facts the core needs. WordDerived.v holds the facts the examples (Fifo, Multiplier, Divider) need and the standard library lacks: 96 lemmas, almost all one `word_lia_Z` line. `Zpow2` is a named constant declared `simpl never` because Kami's tactics `simpl` freely and `simpl` computes inside an implicit modulus: `2 ^ Z.of_nat (S n)` becomes `Z.pow_pos 2 (Pos.of_succ_nat n)`, which no lemma matches. For the same reason the standard library's Zmod operations are declared `simpl never` for every importer of Word.v (reducing through `Zmod.of_Z` duplicates the specification at every nesting level), and so are the definitions above. Syntax.v spells the `ConstBit` constructor's argument as `Zmod (Zpow2 n)` so that the coercion into `ConstT` has source class `Zmod` and applies both to terms typed `word n` and to bare Zmod terms such as `Zmod.add x y`. Semantics.v evaluates `Mul` (all signednesses) as `Zmod.mul`, the shifts as `Zmod.slu/sru/srs` by `Zmod.unsigned` of the amount, and `Lt`/`Slt` as `Z.ltb`; `evalVec` reads bits with `whd`/`wtl`. Downstream proofs that chained the legacy lemmas (`wplus_comm`, `wminus_def`, `wminus_inv`, ...) are one `word_lia_Z` call each; the processor and tutorial proofs use `Zmod.add_assoc`, `Zmod.mul_comm`, `Zmod.mul_add_l` and `natToWord_S` directly. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
JasonGross
added a commit
to JasonGross/kami
that referenced
this pull request
Sep 14, 2026
unsigned_inj, unsigned_ofZ, unsigned_ofZ_small and ofZ_unsigned were Zmod.unsigned_inj, Zmod.unsigned_of_Z, Zmod.unsigned_of_Z_small and Zmod.of_Z_unsigned at modulus 2 ^ Z.of_nat sz; use sites name the stdlib lemma. The operation-level duplicates (wplus_comm for Zmod.add_comm, ...) stay, because turning wplus, wminus, wmult, wneg, wor, wand, wxor, wnot, weqb, wzero, wone, ZToWord, uwordToZ and wordToZ into notations for the stdlib operations was measured and is not cheap here: with word n := bits (Z.of_nat n) the notations expose the modulus 2 ^ Z.of_nat sz as an argument, and every simpl/cbn in a proof normalizes it (to Z.pow_pos 2 (Pos.of_succ_nat _) or to a literal), after which no lemma stated over word sz rewrites any more. Six example files fail at their first such site (FifoCorrect.v:46, SimpleFifoCorrect.v:45, Divider32.v:663, Divider64.v:664, Multiplier32.v:1270, Multiplier64.v:1270), identically with and without a global `Arguments Zmod.<op> : simpl never` for the 14 constants involved, since simpl never does not stop argument normalization; those files contain 338 simpl/cbn and 936 rewrite lines. The fix is a simpl-never modulus constant in the definition of word (the mit-plv#52 design), which touches the 194 occurrences of 2 ^ Z.of_nat in this file, the pow2 facts of the lia hammer and the bedrock2 processor proofs. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Comparison branch requested in the review of #51. Instead of keeping Kami's nat-indexed lemma library and re-proving it over
bits, this makes Kami's word operations the stdlibZmodoperations themselves (wplusisZmod.add,wordToZisZmod.signed,ZToWordisZmod.of_Z, ...), drops the legacy lemma library, and proves the examples with stdlib lemmas plus a small derived set (Kami/Lib/WordDerived.v) and alia-based hammer. One commit onrv32i, same base as #51.Against #51:
Word.vis 953 lines instead of 5352 (plus 645 inWordDerived.v), 75 lemmas instead of 616; the whole tree builds in 102 s instead of 277 s at -j144; about ten public statements change shape (wlt/wsltareZ.ltonunsigned/signed,Lt/Sltevaluate toZ.ltb,MultoZmod.mul,wordToZisZmod.signed,sext/zext/extzareof_Zof their value). bedrock2's processor adapts in 5 files (+95/-146, branchfable/kami-zmod-directon the JasonGross fork) and end2end builds unchanged. The full comparison is in a comment on #51.Recommendation: keep #51's design and take the cheap wins from here (stdlib lemmas at the use sites where they apply syntactically,
Lt/SltasZ.ltb). The costs here are structural:simplcomputes inside implicit moduli, so a named modulus constant and refolding are needed and goals show the same modulus in several spellings; the sext/extz/wmsb facts that the Multiplier and Divider proofs use are needed either way (the derived file is the old grab-bag at an eighth of the size); and it needs globalsimpl neveron stdlib'sZmodconstants for every Kami importer. Draft, not meant to merge as is.Written by Claude Fable 5.1.
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm