Repository navigation
Word: represent Kami words as stdlib bits (Zmod), keeping the nat index - #51
Conversation
|
CI note: this PR comes from a fork, so the workflow needs a maintainer's approval to run here. Reproduced the docker job locally on a clean copy of de19289 in Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
|
bedrock2 side: mit-plv/bedrock2#562 (thin KamiWord bridge, pins this branch; stacked on mit-plv/bedrock2#561). Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
|
Follow-up on the bedrock2 side: mit-plv/bedrock2#563 unifies the Kami word instance with coqutil's Naive.word. Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
| - injection e; intros; subst; exact x. | ||
| - injection e; intros; subst; exact x. | ||
| Defined. | ||
| (* [word] is no longer an inductive type, so the head bit and the tail are |
There was a problem hiding this comment.
Comments describing the change should not be added to the code but rather to the commit description
There was a problem hiding this comment.
Done: the change-describing comments are removed across the whole diff (Semantics.v, Word.v, the Divider, Multiplier and Fifo examples) and their substance is in the commit messages; the diff against the previous tip is comments only, so the build is unchanged.
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
| intros. replace (p - z) with (- z + 1 * p) by lia. rewrite Z.mod_add; lia. | ||
| Qed. | ||
|
|
||
| Lemma Zplus_pminus_mod : forall a b p, p <> 0 -> (a + (p - b)) mod p = (a - b) mod p. |
There was a problem hiding this comment.
This file is a grab-bag of generated lemmas. Could we consider an alternative PR where Zmod is used more directly instead of re-proving a bunch of operations using the nat-indexed view? It's possible that the downstream proofs are even messier to fix that way, but a comparison would be valuable.
There was a problem hiding this comment.
Done as #52, with the comparison in #51 (comment). Short version: 5.6x smaller Word.v and a 2.7x faster Kami build, but about ten public statements change shape, the Multiplier and Divider proofs get messier because the modulus is spelled several ways after simpl, and it needs global simpl never on stdlib's Zmod constants for every importer. Recommendation is to keep this PR's design and take the cheap wins (stdlib lemmas at use sites, Lt/Slt as Z.ltb, of_Z-based sext/zext/extz).
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
Replace the inductive two-constructor word with `word n := bits (Z.of_nat n)` from the standard library's Zmod, so that a Kami word is the same type as the words used by coqutil and bedrock2 and stdlib's Zmod lemmas apply to it. Every Kami operation is a named `simpl never` wrapper around a `Zmod.of_Z` of its integer specification; `WO` and `WS` are ordinary definitions that build the value bit by bit; `weq`/`wlt_dec`/... decide via `Zmod.eqb` and `Z` comparisons. Facts are proved by moving to `Zmod.unsigned` with `word_to_Z` and reasoning in `Z`. The nat-stated legacy lemmas are kept, with `Z_scope` closed again before them, and are reproved that way. `isWcst` no longer puts the word in `hnf` before matching: `WO`/`WS` are definitions and would unfold. Kami/Tactics.v's `is_not_const_word` learns the fully explicit `@WS` spelling. Kami/Lib/Word.v does not yet compile at this commit; the next commit repairs the remaining legacy proofs. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
Word.v is now `word n := bits (Z.of_nat n)`; this fixes the ~30 legacy lemmas whose proofs did not survive the change, teaches `word_to_Z` how `pow2` (a nat function) relates to `2 ^ Z.of_nat _`, restores the `Local Open Scope nat` that the rewrite had dropped, and removes a forward reference to `wordToZ_size'` from `wordToZ_ZToWord'`. Also rewrites `evalVec` in Kami/Semantics.v: it used to match on the `WO`/`WS` constructors of the inductive `word`; it now takes the head bit and the tail with `whd`/`wtl`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
Both were proved by `word_mod_simpl; mod_args_unify; lia`, which made `lia`/`nia` search for tens of minutes on a cold proof cache. Case split on the sign of the difference and rewrite the two moduli directly instead. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
- Kami/Semantics.v: evalVec no longer matches on WO/WS.
- Kami/Ex/{,Simple}FifoCorrect.v: `$0~1` and `$1` are no longer
definitionally equal, so spell the constant one way; `inv e` can no
longer refute `$1 = $0` (word is not inductive), compare wordToNat;
one `replace ... by reflexivity` now needs WS_true_natToWord_0.
- Kami/Lib/Word.v: add WS_true_natToWord_0 / WS_false_natToWord_0.
Everything except Kami/Ex/{Multiplier,Divider}{32,64}.v builds.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
Define `sext`/`zext`/`extz` as `combine w (wones/wzero _)` and `combine (wzero n) w`, exactly as with the inductive word, rather than as a single `Zmod.of_Z`: the Kami examples rely on those definitional equalities. Their `unsigned_*` lemmas are proved instead of being instances of `unsigned_of_Z`. Add the eliminator `word_rect`/`word_ind`/`word_rec` and the `word_destruct` tactic, which take over from `dependent induction` and `dependent destruction` on the former inductive, plus `whd_WS`, `wtl_WS`, `whd_split1`, `wtl_split1`, `wordToNat_wtl`, `wordToZ_one`, `wordToZ_succ` and `shatter_word_1/2/3`. Multiplier32/64: the Booth encodings are written with `whd`/`wtl` instead of constructor matching, and `rtrunc1`/`rtrunc2` are `wtl`/`wtl (wtl _)`. Divider32/64 and Multiplier32/64: `DivNumPhases`/`MultNumPhases` were `wordToNat (wones k) + 1`, which the inductive word evaluated by computation; `wordToNat` is `simpl never` now, so spell the same number as `pow2 k` so that the width arithmetic still reduces. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
The Booth-step invariant proof `set`s the initial accumulator as the associated `combine (combine $0 a) $0` rather than `extz (combine a $0) 1`: the two are no longer definitionally equal, and the former is the shape that `boothStepInv_init` produces. `split1`/`split2` do not reduce structurally any more, so the `simpl; rewrite wtl_combine` step becomes a rewrite with the new Word.v lemma `split2_split1_combine1`. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
`pn2binBitwise` recurses on the width and reads bits with `whd`/`wtl` instead of matching on the `WO`/`WS` constructors. Its facts are derived from two `Z`-valued characterizations, `pn2binBitwise_eqn` and `pn2binE_wordToZ`, instead of by induction on the word. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
The `Arguments ... : simpl never` block spelled the size argument `{_}`,
which makes it maximally inserted; `Set Implicit Arguments` (what the
inductive-word Word.v used) makes it non-maximal, so 48 operations
changed insertion mode and partial applications stopped typechecking:
Definition apply2 (f : forall sz, word sz -> word sz -> word sz) := f.
Check apply2 wplus.
Spell them `[_]` instead. The three Zmod lines keep stdlib's own modes,
so their only effect stays `simpl never`.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
…ide effect
`Arguments` outside a section is global, so
Arguments Zmod.unsigned {_} _ : simpl never.
Arguments Zmod.signed {_} _ : simpl never.
Arguments Zmod.of_Z _ _ : simpl never.
disabled cbn/simpl on stdlib's Zmod for every importer of Kami.Lib.Word,
bedrock2 included: after the import, cbn no longer reduced
`Zmod.unsigned (Zmod.of_Z 8 5)` to 5. Delete them. No proof needed a
replacement: every Kami operation is itself a `simpl never` wrapper, so
Zmod.* only appears in a goal where a proof deliberately unfolds one and
reduction is wanted there.
Also note in the header that requiring ZifyNat/ZifyN registers those
Zify instances globally for importers.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
de19289 to
aff07cc
Compare
|
Comparison of this PR (
Statement changes on the alternate: Where the alternate is cleaner: the Fifo proofs (25 sites like Where it is messier: the Multiplier "product halves" step goes from 13 lines in the signed view to a proof through Recommendation: keep this PR's design, and take from the alternate what is cheap and clearly better: stdlib lemmas at downstream use sites where they apply syntactically, Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
evalBinBitBool (Lt n) a b is now Z.ltb (uwordToZ a) (uwordToZ b) and (Slt n) is Z.ltb (wordToZ a) (wordToZ b), instead of a match on the sumbool deciders wlt_dec/wslt_dec. evalBinBit (Mul n _) is wmult, i.e. Zmod.mul, for all three signedness flags: the signed products wmultZ/wmultZsu compute the same residue, so nothing observable changes, and the Multiplier32/64 correctness proofs close by comparing residues (unsigned_inj + Zmod.mod_signed) instead of unfolding wmultZ. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
sext w n is of_Z (signed w), zext w n is of_Z (unsigned w) and extz w n is of_Z (2 ^ n * unsigned w), so unsigned_sext/zext/extz are instances of unsigned_of_Z instead of case analyses over combine. The combine spellings survive as the lemmas extz_combine and the new split1_zext; the Divider proofs that unfolded zext to reach split1_combine rewrite with split1_zext instead. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
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
|
Applied the cheap wins from the #52 comparison as three commits on top of aff07cc (tip 29c7e87): Turning Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
|
Hmm, |
wplus, wminus, wmult, wneg, wand, wor, wxor, wnot, weqb, wzero, wone, ZToWord, uwordToZ and wordToZ are notations for Zmod.add, Zmod.sub, Zmod.mul, Zmod.opp, Zmod.and, Zmod.or, Zmod.xor, Zmod.not, Zmod.eqb, Zmod.zero, Zmod.one, Zmod.of_Z (2 ^ Z.of_nat sz), Zmod.unsigned and Zmod.signed, so every Zmod lemma applies to Kami words as it is; word n stays bits (Z.of_nat n). The 8-bit ring and the ring morphism are stated with Zmod.ring_theory and the Zmod operations, and the tactics that match the type of a word accept every spelling of it (word_width), since the type of wzero sz is now Zmod (2 ^ Z.of_nat sz). The notations expose the modulus 2 ^ Z.of_nat sz as an argument, and simpl/cbn normalize it (to Z.pow_pos 2 (Pos.of_succ_nat _) or to a literal) although they never unfold the operation itself; the lemmas over word sz are keyed on 2 ^ Z.of_nat ?sz and stop rewriting after that. The six example files whose simpl calls hit words (FifoCorrect, SimpleFifoCorrect, Divider32/64, Multiplier32/64) declare #[local] Arguments Z.pow / Z.of_nat : simpl never; with that, none of their 338 simpl/cbn calls needed a change (those calls unfold Kami's evaluation functions and fixpoints and compute nat widths, which the two declarations leave intact). No Arguments Zmod.<op> : simpl never is declared: measured unnecessary (the tree builds without). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
wplus_comm, wplus_assoc, wmult_comm, wmult_assoc, wmult_plus_distr, wminus_def, wminus_inv, weqb_true_iff, weqb_sound, weqb_eq, wneg_idempotent, wplus_wzero_1, wplus_wzero_2, wzero_wplus, ZToWord_0, ZToWord_1, ZToWord_plus, ZToWord_mult, ZToWord_minus, ZToWord_opp_wneg, ZToWord_wordToZ, unsigned_wplus, unsigned_wminus, unsigned_wmult, unsigned_wneg, unsigned_wor, unsigned_wand, unsigned_wxor, unsigned_ZToWord, unsigned_wzero, unsigned_wone and uwordToZ_ZToWord are Zmod.add_comm, Zmod.add_assoc, Zmod.mul_comm, Zmod.mul_assoc, Zmod.mul_add_l, Zmod.add_opp_r (mirrored), Zmod.add_opp_same_r, Zmod.eqb_eq (three times), Zmod.opp_opp, Zmod.add_0_r, Zmod.add_0_l (twice), Zmod.of_Z_0, Zmod.of_Z_1, Zmod.of_Z_add, Zmod.of_Z_mul, Zmod.of_Z_sub, Zmod.of_Z_opp, Zmod.of_Z_signed, Zmod.unsigned_add, Zmod.unsigned_sub, Zmod.unsigned_mul, Zmod.unsigned_opp, bits.unsigned_or, bits.unsigned_and, bits.unsigned_xor, Zmod.unsigned_of_Z, Zmod.unsigned_0, Zmod.unsigned_1 and Zmod.unsigned_of_Z_small; the use sites (Word.v, WordSupport.v and the examples) name the stdlib lemma, and Word.v exports Zmod so that they can. Kept: the lemmas about natToWord sz 0/1 ($0/$1 is of_Z (Z.of_nat 0), not Zmod.zero), unsigned_range (no 0 <= n hypothesis), and the bitwise algebra (or/and/xor units, commutativity, associativity), which the stdlib does not have for Zmod. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
| (a ^* b) ^% n = ((a ^% n) ^* (b ^% n)) ^% n. | ||
| Lemma wmsb_wlshift_sext: | ||
| forall sz (w: word sz) n, | ||
| wmsb (sext w n) false = wmsb (wlshift (sext w n) n) false. |
There was a problem hiding this comment.
Could this lemma have an easier proof using the definition of wmsb in terms of <? sign of the argument?
There was a problem hiding this comment.
Yes: after wmsb_S both sides are sign tests; the shifted side's signed is Z.smodulo of its unsigned value (bits.smod_unsigned, Zmod.unsigned_slu, unsigned_sext), which Z.smod_pow2_small turns into signed w * 2 ^ n, and Z.ltb_spec with 2 ^ n > 0 finishes. The testbit/split1 detour is gone; the proof is about the same length only because the empty-word case still needs its own three lines (f3d7334).
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
| Definition wminus sz (x y : word sz) : word sz := wplus x (wneg y). | ||
| Definition wnegN sz (x : word sz) : word sz := | ||
| natToWord sz (pow2 sz - wordToNat x). | ||
| Notation wneg := Zmod.opp. |
There was a problem hiding this comment.
When using Notation for abbreviations, always use (only parsing). However, here we don't need abbreviations at all -- just replace uses of these functions with uses of corresponding stdlib functions.
There was a problem hiding this comment.
Done (58c39ca): the abbreviations are gone and every use site names the stdlib function (Zmod.add, Zmod.eqb, bits.of_Z, ...). Kami's infix syntax (^+, ^-, ^*, ^~, ^|, ^&, ^/, ^%, ^<<, ^>>) and the $/# literal forms stay as notations bound directly to the stdlib operations; the two remaining local abbreviations are (only parsing). bedrock2's bridge (#562/#563) is adapted to the new spellings.
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
| Definition sext (sz : nat) (w : word sz) (sz' : nat) : word (sz + sz') := | ||
| if wmsb w false then | ||
| combine w (wones sz') | ||
| else | ||
| combine w (wzero sz'). | ||
| ofZ _ (Zmod.signed w). | ||
|
|
||
| Definition zext (sz : nat) (w : word sz) (sz' : nat) : word (sz + sz') := | ||
| combine w (wzero sz'). | ||
| ofZ _ (unsigned w). |
There was a problem hiding this comment.
Do we have enough use for theory about zext and sext to keep definitions for them, or should they be inlined instead?
There was a problem hiding this comment.
Kept: zext/sext have 24 lemmas and 118 use sites across Kami and bedrock2's processor, so inlining Zmod.of_Z _ (Zmod.unsigned w) / Zmod.of_Z _ (Zmod.signed w) everywhere would lose more than it saves; the definitions are exactly those terms, so the stdlib lemmas apply after one unfold.
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
|
The code proposed in this PR still does not read like idiomatic Zmod/bits usage -- it's clear that the stdlib functions were adapted in place of a different design. Consider alternatives, improvements, and simpifications that would lead to a more conventional usage of Zmod. If nothing works better, we can stick to what's here now. |
wmsb w a is (Zmod.signed w <? 0) for a nonempty word (and a for the empty one), which wmsb_S states; wmsb_sext and wmsb_wlshift_sext go through it and the sign of the value (sext_wordToZ, and Z.smodulo for the shifted word) instead of the unsigned-value case analysis. split1 sz1 sz2 w is Zmod.firstn (Z.of_nat sz1) w; wlshift, wrshift and wrshifta are notations for Zmod.slu, Zmod.sru and Zmod.srs at Z.of_nat n; wmod is Zmod.umod and wremZ is Zmod.srem, which agree with Kami at a zero divisor (x mod 0 = x); wdiv and wdivZ keep Kami's x / 0 = 0 over Zmod.udiv and Zmod.squot, which give -1 there; ZToWord is bits.of_Z. wtl, combine, split2, WS and extz stay of_Z of their value: bits.skipn, bits.app and a one-bit app produce the moduli 2 ^ (Z.of_nat (S n) - 1), 2 ^ (Z.of_nat a + Z.of_nat b) and 2 ^ (1 + Z.of_nat n), which are not convertible to the nat-indexed 2 ^ Z.of_nat n, 2 ^ Z.of_nat (a + b) and 2 ^ Z.of_nat (S n). Semantics.v spells Rem as wremZ. Duplicates merged: wordToNat_natToWord_idempotent' into wordToNat_natToWord_2 and shatter_word_0 into word0; wordToZ_inj is Zmod.signed_inj, Npow2_Z is NatLib.Z_of_N_Npow2 and unsigned_wmod is Zmod.unsigned_umod. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
pow2_normalize is two autorewrite databases (word_pow2, then word_inj, in that order: rewriting Z.of_nat (a + b) before 2 ^ Z.of_nat (a + b) leaves 2 ^ (Z.of_nat a + Z.of_nat b), which nothing else matches). The mod/div rules stay an ordered chain: as a database, each rule applied exhaustively in list order, the normal forms differ and wlshift_sext_extz stops closing. word_lia_Z ends in lia; word_nia_Z is the variant ending in nia, used by split2_split1_combine1 only; the zify; Z.div_mod_to_equations; nia branch is gone, nothing needs it. Measured alternative for the unsigned_word pass: rewrite_strat (topdown (hints unsigned_word)) on the goal and each hypothesis takes the same time as autorewrite on the 1254 lines it gets through (5.7 s both) and then produces a normal form on which neither wneg_zero's proof nor word_nia_Z closes; rewrite_strat also has no `in *`. autorewrite stays. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
KamiRiscv.v uses it as `rewrite 2wordToZ_ZToWord'' in HX`; the use count behind the previous commit did not see a name preceded by a digit. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
dbba41f to
f3d7334
Compare
wplus, wminus, wmult, wneg, wand, wor, wxor, wnot, weqb, wzero, wone, ZToWord, uwordToZ, wordToZ, wmod, wremZ, wlshift, wrshift and wrshifta were abbreviations of Zmod.add, sub, mul, opp, and, or, xor, not, eqb, zero, one, bits.of_Z (Z.of_nat sz), Zmod.unsigned, Zmod.signed, umod, srem, slu, sru and srs (the shifts at Z.of_nat n); every use site in Word.v, Semantics.v, Syntax.v and the examples spells the stdlib name. The infix notations ^+ ^- ^* ^~ ^| ^& ^/ ^% ^<< ^>> stay, bound to the stdlib operations: they are syntax used at hundreds of sites and the examples open kami_expr_scope, whose + and * would clash with Zmod_scope's. The two local abbreviations of Word.v are only parsing. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
| | xH => WS true (wzero' sz') | ||
| end | ||
| end. | ||
| Definition wzero' (sz : nat) : word sz := ofZ _ 0. |
There was a problem hiding this comment.
Can we get rid of this definition in favor of Zmod.zero? Are there any other similarly redundant definitions?
There was a problem hiding this comment.
Deleted (51a6a0f): it was Zmod.zero under another name, and its lemmas were Zmod.unsigned_0/Zmod.signed_0. The same pass made wones the stdlib's -1 (Zmod.opp Zmod.one) and wlt plain Z.lt on Zmod.unsigned; every remaining definition was checked against the stdlib's Zmod/bits modules and none is a stdlib value under another name (30 definitions are left, from 61).
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
…alues gone wones sz is Zmod.opp Zmod.one (unsigned_wones through Zmod.unsigned_m1); wlt l r is Z.lt (Zmod.unsigned l) (Zmod.unsigned r) and wlt_dec is Z_lt_dec on them (the N detour and the opacity note for a deleted test are gone); wzero' was Zmod.zero and wordToNat' was wordToNat, so their lemmas are Zmod.unsigned_0/Zmod.signed_0 and the use sites say so. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
| | WS b w1' => fun w2 => WS (f b (whd w2)) (bitwp f w1' (wtl w2)) | ||
| (** [bitwp f] applies [f] bit by bit; it is only used to state facts about | ||
| the bitwise operators below, which are the [Zmod] ones. *) | ||
| Fixpoint bitwp (f : bool -> bool -> bool) (sz : nat) : word sz -> word sz -> word sz := |
There was a problem hiding this comment.
Can we get rid of this definition? are there any other ultimately unused definitions?
There was a problem hiding this comment.
Deleted (a84d229), together with everything else the unused-content sweep found on the current tip: bitwp and its lemma chain, wones, wlsb, posToWord, wdiv, wordBinN, wslt, wlt_dec, the unused infix notations (^%, ^|, ^&, ^<<, ^>>, the <s family), and WO is now an only-parsing abbreviation of Zmod.zero. The sweep is transitive over Kami, bedrock2's processor and end2end, coqutil, fiat-crypto and rupicola (the last three do not use Kami); Word.v is now 1864 lines, 182 lemmas, 21 definitions (from 5147/582/61 when this review started), each with at least one user.
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
|
Please prepare a follow-up PR for the BlueSpec extraction pipeline; also add a CI target that tests it. |
|
Follow-up prepared as #53 (stacked on this PR): it fixes the extraction ( Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
|
Done what pays for itself (51a6a0f): What is still Kami-shaped, and why it was left:
If any of 1 to 3 is wanted, it is a separate PR with statement changes in the examples. Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
WO is an only-parsing abbreviation of Zmod.zero at width 0 (the base of the 4221 bit literals WO~0~1... in the examples; the cast keeps the ConstBit coercion); wones sz was Zmod.opp Zmod.one, wlsb was whd, wordBinN only served wdivN/wremN, posToWord had no user, wslt and wdiv with their notations >s >s= <s <s= ^/ had no user, and neither had the infix ^% ^| ^& ^<< ^>>: all gone, use sites spell the stdlib term. unsigned_WO, unsigned_posToWord, unsigned_wdiv, wnot_zero and wnot_ones were Zmod.unsigned_0, nothing, nothing, bits.not_0 and bits.not_m1; unsigned_wones is unsigned_opp_one. With wnot_zero/wnot_ones gone the bit-by-bit machinery (bitwp, bitwp_0, bitwp_S, testbit_*, word_bits*, unsigned_wnot_ldiff, unsigned_wone_S) and wlt_dec, wmsb_sext and wmsb_testbit have no user left and are gone too. The signed comparisons of kami_expr_scope carry their own level now that Word.v no longer declares one. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
| Definition wdivN sz (x y : word sz) : word sz := natToWord sz (wordToNat x / wordToNat y). | ||
| Definition wremN sz (x y : word sz) : word sz := natToWord sz (wordToNat x mod wordToNat y). |
There was a problem hiding this comment.
Would it work the define these in terms of Zmod unsigned division and modulo operations?
There was a problem hiding this comment.
Yes (227155a): Div/Rem now evaluate to Zmod.udiv/squot and Zmod.umod/srem directly, and wdivN/wremN/wdivZ are gone. The remainders agree with the old definitions everywhere; the quotients differ only at a zero divisor (-1, the RISC-V convention, instead of 0), which no Kami program reaches (the divider spec and implementation assert d != $0, and IsaRv32 has no division). The divider's final-restoring lemma is stated with Zmod.udiv/umod under its d <> 0 hypothesis and proved through unsigned_udiv_nonneg/unsigned_umod instead of the nat round trip.
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
There was a problem hiding this comment.
Does the BlueSpec backend need a particlular value for division by zero to be accurate?
There was a problem hiding this comment.
No. The backend prints Div/Rem as divide_{unsigned,signed}/remainder_{unsigned,signed} from Kami's own MulDiv.bsv, which are Bluespec's / and % on UInt/Int with no zero check, and bsc turns those into the plain Verilog operators: with a zero divisor the simulated Verilog yields x (checked with bsc 2026.01 + iverilog: xx for all four of udiv/urem/sdiv/srem) and Bluesim aborts with SIGFPE, so no Kami-side value is accurate there and none is inaccurate either. Nothing that reaches the backend divides anyway: the extracted rv32i processor's Proc.bsv has no divide_/remainder_ call, and the Divider examples that use Div/Rem assume a nonzero divisor. So the choice is free to follow the least surprising convention for proofs; the stdlib's udiv/squot value (-1, all ones, RISC-V's DIV result) is the one a hardware reader expects, and the transliteration needs no change either way.
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
|
|
||
| Notation "l ^| r" := (@wor _ l%word r%word) (at level 50, left associativity). | ||
| Notation "l ^& r" := (@wand _ l%word r%word) (at level 40, left associativity). | ||
|
|
||
| (** * Conversion to and from [Z] *) |
There was a problem hiding this comment.
Remove stray headers
There was a problem hiding this comment.
Removed (e2507eb): the file has no header without content under it any more (the five empty headers and the no-op scope pairs left by the deletions are gone).
Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm).
wdivN, wremN and wdivZ are gone: evalBinBit (Div n false) is Zmod.udiv, (Div n true) is Zmod.squot, (Rem n false) is Zmod.umod and (Rem n true) is Zmod.srem. The remainders agree with the old nat/Z definitions everywhere (x mod 0 = x); the quotients differ only at a zero divisor, where the stdlib gives -1 (the RISC-V convention) and Kami gave 0. No Kami program divides by zero: dividerSpec and nrDividerImpl assert d != $0 before every Div/Rem, IsaRv32 has no division, and the processor's ISA is rv32i. Divider32/64's final-restoring lemma is stated with Zmod.udiv/umod under its d <> 0 hypothesis and proved through Zmod.unsigned_udiv_nonneg/unsigned_umod instead of the nat round trip; Z_of_nat_wordToNat is the bridge. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
wmsb no longer takes a default answer for the empty word and no longer matches on the width: it is Zmod.signed w <? 0, which is false at width 0. wmsb_S is now the definition and wmsb_eqn_gen is gone; every lemma and use site (Divider32/64, Multiplier32/64) drops the extra argument. No use site passed anything but false. word_split_bools iterates until no boolean test is left, since signed_eqn now exposes nested tests inside the hypotheses it creates. Remove the empty section headers left behind by earlier deletions and a no-op Close/Open Scope pair. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
|
Both ports are up: mit-plv/quartz#2 (stdlib bits, with the backend tests per observable difference) and mit-plv/granite#1 (pins quartz#2's tip; 60 files, no admits, same axiom for Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
bedrock2's processor proofs meet Kami's word through wordToN, split1, split2, combine, eq_rect and weq, and carried the lemmas relating those spellings to the unsigned characterization in its own KamiWord.v. They belong with the library they are about, so bedrock2 can drop that file: Z_of_N_wordToN, wordToN_split1, wordToN_split2, wordToN_eq_rect, split1_wplus_silent, if_weq_eqb and Z_of_N_wordToN_combine. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
|
Added 2777a72: seven transport lemmas about Written by Claude Fable 5.1 via Claude Code (session https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm). |
Kami's word type is now stdlib
bits:word n := bits (Z.of_nat n)(that is,Zmod (2^(Z.of_nat n))from rocq-stdlib >= 9.1), with thenatindex kept soBit nand the rest of Kami's syntax are unchanged.Kami/Lib/Word.vgoes from 7326 to 1864 lines (only what Kami, bedrock2's processor and end2end use survives, re-proved over the new representation;split1,wmsb, the shifts and the remainders are the stdlib operations,combine/split2/extzstayof_Z-based becausebits.app/skipngive non-convertible widths); every name that Kami, or bedrock2's processor/end2end, uses from it keeps its name and statement, with these exceptions taken from the #52 comparison:Lt/Sltevaluate toZ.ltbonuwordToZ/wordToZand everyMultoZmod.mul(provably, not convertibly, equal to the oldwlt_dec/wmultZforms);sext/zext/extzareof_Zof their value (thecombinespellings are lemmas); and the lemmas that were stdlib lemmas modulo the notations are gone in favour of theZmod.*/bits.*names. No theorem statement of Kami's examples changes meaning. The operations the stdlib has are used by their stdlib names at every site (Zmod.add,Zmod.eqb,bits.of_Z, ...; Kami's infix^+/^-/... syntax is bound directly to them), so stdlib lemmas apply directly and the Word.v lemmas that restated them are deleted; the operations whose shape differs (natToWord,wordToNat, shifts,combine/split,sext/zext/extz, ...) aresimpl neverdefinitions over them. Sincesimpl/cbnnormalize the modulus argument2 ^ Z.of_nat szeven under asimpl neverhead, the six example files whose proofs rewrite with word lemmas after asimpldeclare#[local] Arguments Z.pow : simpl neverand the same forZ.of_nat; no globalsimpl neveranywhere.Semantics.v(evalVec,wordVecDec'),Tactics.vand the Multiplier, Divider and Fifo examples are adapted; the whole tree builds in about 100 s at -j144 (Word.v alone in about 2 minutes). No new axioms; the pre-existingAxiom cheatinCommonTactics.vis untouched.MultNumPhases/DivNumPhasesreadpow2 kinstead ofwordToNat (wones k) + 1(same value; the latter no longer reduces undercbn).Not done here:
Kami/Ext/Ocaml/PP.mlstill pattern-matches on the extractedWO/WSconstructors, so the Bluespec extraction pipeline needs a follow-up; no Coq file depends on it.This requires rocq-stdlib >= 9.1 (Kami's CI already tests only Rocq dev). It is the Kami side of the wider move of coqutil's
Word.Naive(mit-plv/coqutil#186) and fiat-crypto'sF(mit-plv/fiat-crypto#2434) onto stdlibZmod/bits; the bedrock2 bridge simplification that pins this commit will be linked in a comment once open.Written by Claude Fable 5.1 and Claude Opus 5.
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm