Bluespec extraction pipeline on the Zmod word, with a CI test - #54
Draft
JasonGross wants to merge 30 commits into
Draft
JasonGross wants to merge 30 commits into
JasonGross wants to merge 30 commits into
Conversation
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
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
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
415 of the 704 named items of Word.v and WordSupport.v (379 lemmas, 20 definitions, 13 tactics, 1 fixpoint, 1 tactic notation, 1 instance) are referenced nowhere, transitively, in Kami, in bedrock2's processor and end2end, or in coqutil, fiat-crypto and rupicola (the last three do not use Kami at all); they are gone. WordSupport.v restated pre_word_lia and wordToN_to_nat from Word.v and nothing required it; it is gone too. The Zify instance for Npow2 stays: lia uses it through the registration, not by name. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
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
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
…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
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
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
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
Kami's word is now the standard library's Zmod record, so the extracted OCaml no longer has the WO/WS constructors that PP.ml walked to read a constant's value. Kami's own wordToNat already computes Z.to_nat of the unsigned value, so extract it alongside targetB and let PP.ml call it; PP.ml then needs no knowledge of how Z or the record are represented. The Is_true proof field of the record is a Prop and is erased by extraction, so nothing else changes on the OCaml side. ppWord had no users and is gone. Zmod's operations go through Z.compare, which drags the comparison type into the extracted code. Its Eq and Lt constructors would then shadow Kami's expression constructors of the same names, which extraction renames to Eq0 and Lt0 and which PP.ml matches on. Extracting comparison to an OCaml int keeps the Kami names stable. The Bluespec output for the rv32i four-stage processor is byte-identical to the output before the word change. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
The transliterator uses only the OCaml standard library, so ocamlbuild and ocamlfind buy nothing; a direct ocamlopt invocation needs only the compiler that every Rocq installation already has (the rocq-prover docker image ships ocamlfind, dune and zarith but not ocamlbuild). The Batteries requirement in the README was stale for the same reason. `make Proc.bsv` in Kami/Ext/Ocaml runs the transliterator on the extracted processor; `make bluespec` at the root runs the Rocq build, which performs the extraction, first. The .gitignore line that hid all of Kami/Ext gave way to the specific generated files, so that source files can be added under Kami/Ext. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
Kami/Ext/BluespecFrontEnd/verilog/Top.bsv wraps the extracted processor as `Empty proc <- mkProc(...)`, and the connectal front end does the same. The transliterator, however, prints the module's interface with the name given by -top (default Top), a type nobody declares, so bsc rejected its output. The generated top module has no methods (every external call is a module parameter), so its interface is Empty, and the default module name is again mkProc; -top still renames it. SimpleBRAM.bsv, which Header.bsv imports and the verilog Makefile depends on, was never committed. This one is reconstructed from the checked-in build/mkBramInst.v: a register file with a one-cycle read latency, synthesized as mkBramInst. It uses mkRegFileFull rather than the load-from-file variant so simulations do not report a missing file.hex. The verilog Makefile now copies Proc.bsv from the transliterator and puts everything bsc generates under gen/, keeping the 2020 Verilog in build/ (used by bedrock2's FPGA flow) untouched. `make verilog` at the root extracts, transliterates and compiles in one go. With bsc 2026.01 the generated mkTop.v has the same rules and submodule instances as build/mkTopB10.v. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm
The Bluespec pipeline broke silently when word changed representation because nothing built the extracted OCaml. Run `make verilog` after the Rocq build, so extraction, the transliterator and bsc's acceptance of its output are checked on every push. bsc comes from its release tarball for Debian 12, which the rocq-prover docker image is based on; its checksum is pinned. 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
Contributor
Author
|
Continuation of #53 (auto-closed when its head branch was briefly deleted during a force-push): same commits, rebased onto #51's merge commit, ending in a merge commit as requested for submodule PRs. Written by Claude Fable 5.1 via Claude Code (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
1 participant
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.
Follow-up to #51 (stacked on it: the last three commits are this PR). With Kami's word being the standard library's Zmod record, the Bluespec transliterator in Kami/Ext/Ocaml could no longer compile against the extracted code. This restores the pipeline by extracting Kami's
wordToNatfor the pretty-printer and mappingcomparisonto an OCamlintso Kami'sEq/Ltconstructors keep their names; the generated Proc.bsv for the rv32i processor is byte-identical to what rv32i produced. It also addsmake bluespec(extract and build the transliterator with plainocamlopt) andmake verilog(compile the extracted processor with bsc; this fixes the transliterator's top-module interface, broken since 2020, and reconstructs the never-committed SimpleBRAM.bsv from the checked-in mkBramInst.v), and CI compiles the processor with bsc after the build. The simulation of the regenerated processor lives in bedrock2 (mit-plv/bedrock2#564).Written by Claude Fable 5.1.
🤖 Generated with Claude Code
https://claude.ai/code/session_01YJbiRBkJtM7x6PvYV6hmEm