Skip to content

Word: represent Kami words as stdlib bits (Zmod), keeping the nat index #51

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
andres-erbsen merged 25 commits into from
Sep 17, 2026
Merged

Word: represent Kami words as stdlib bits (Zmod), keeping the nat index #51

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
25 commits
Select commit Hold shift + click to select a range
a86f174
Kami/Lib/Word.v: define word as stdlib's bits (Z.of_nat n)
JasonGross Sep 12, 2026
b1bf79b
Kami/Lib/Word.v: repair legacy proofs for the Zmod-based word
JasonGross Sep 12, 2026
58c629c
Kami/Lib/Word.v: cut the cold-cache cost of wminus_WS_pos{,'}
JasonGross Sep 12, 2026
8c46cea
Kami core + Fifo examples: adapt to the non-inductive word
JasonGross Sep 12, 2026
756af10
Word.v: keep sext/zext/extz as combines; add word_rect and helpers
JasonGross Sep 12, 2026
3963459
Kami/Ex/Multiplier{32,64}.v: build against the Zmod-based word
JasonGross Sep 12, 2026
54518ba
Kami/Ex/Divider{32,64}.v: build against the Zmod-based word
JasonGross Sep 12, 2026
1d4511d
Word.v: restore non-maximal implicit insertion for the size argument
JasonGross Sep 12, 2026
aff07cc
Word.v: stop declaring stdlib's Zmod simpl never; document the Zify s…
JasonGross Sep 12, 2026
bf23d89
Semantics: evaluate Lt/Slt to Z.ltb and every Mul to Zmod.mul
JasonGross Sep 13, 2026
c6fd2ce
Word.v: define sext/zext/extz as of_Z of their integer value
JasonGross Sep 13, 2026
29c7e87
Word.v: use the stdlib lemmas about unsigned/of_Z directly
JasonGross Sep 13, 2026
0836dbb
Word.v: the operations the stdlib has are notations for the Zmod ones
JasonGross Sep 14, 2026
c0f853a
Word.v: delete the lemmas that are stdlib lemmas modulo the notations
JasonGross Sep 14, 2026
6664a85
Word.v: delete what nothing uses
JasonGross Sep 14, 2026
fc21bf4
Word.v: wmsb, split1, shifts and division on the stdlib operations
JasonGross Sep 14, 2026
6d0f58d
Word.v: hammer rewriting as hint databases, word_lia_Z without nia
JasonGross Sep 14, 2026
f3d7334
Word.v: keep wordToZ_ZToWord'', which bedrock2 rewrites with
JasonGross Sep 14, 2026
58c39ca
Word.v: no abbreviations for the stdlib operations; use sites name them
JasonGross Sep 15, 2026
51a6a0f
Word.v: wones is -1, wlt is Z.lt on unsigned, two aliases of stdlib v…
JasonGross Sep 15, 2026
a84d229
Word.v: no definition for a stdlib value, nothing unused
JasonGross Sep 15, 2026
227155a
Semantics: Div and Rem are Zmod.udiv/squot and Zmod.umod/srem
JasonGross Sep 15, 2026
e2507eb
Word: wmsb is the sign test at every width; drop stray headers
JasonGross Sep 15, 2026
2777a72
Word: wordToN, split, combine and weq transport lemmas
JasonGross Sep 16, 2026
9217329
Merge branch 'fable/word-on-bits'
JasonGross Sep 16, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
330 changes: 157 additions & 173 deletions Kami/Ex/Divider32.v
View file
Open in desktop

Large diffs are not rendered by default.

323 changes: 153 additions & 170 deletions Kami/Ex/Divider64.v
View file
Open in desktop

Large diffs are not rendered by default.

162 changes: 83 additions & 79 deletions Kami/Ex/FifoCorrect.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,8 @@ Require Import Ex.Fifo Ex.NativeFifo Lia.

Import ListNotations.

#[local] Arguments Stdlib.ZArith.BinInt.Z.pow : simpl never.
#[local] Arguments Stdlib.ZArith.BinInt.Z.of_nat : simpl never.
Set Implicit Arguments.
Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
Expand Down Expand Up @@ -43,7 +45,7 @@ Section ToNative.
forall eltv x, fifo_nfifo_elt_not_full eltv (x ^+ $1) 1 = [eltv x].
Proof.
intros; simpl; repeat f_equal.
rewrite wminus_def, <-wplus_assoc, wminus_inv, wplus_comm.
rewrite <-Zmod.add_opp_r, <-Zmod.add_assoc, Zmod.add_opp_same_r, Zmod.add_comm.
apply wplus_unit.
Qed.

Expand All @@ -59,7 +61,7 @@ Section ToNative.

Lemma fifo_nfifo_elt_not_full_enq:
forall eltv enqPv elt edSub,
(edSub <= wordToNat (wones rsz))%nat ->
(edSub <= wordToNat ((@Zmod.opp (Z.pow 2 (Z.of_nat rsz)) Zmod.one)))%nat ->
fifo_nfifo_elt_not_full eltv enqPv edSub ++ [elt] =
fifo_nfifo_elt_not_full (fun w => if weq w enqPv then elt else eltv w)
(enqPv ^+ $1) (S edSub).
Expand All @@ -68,8 +70,8 @@ Section ToNative.
- simpl; f_equal.
destruct (weq _ _); auto.
elim n; clear n.
rewrite wminus_def, <-wplus_assoc, wminus_inv.
rewrite wplus_comm, wplus_unit.
rewrite <-Zmod.add_opp_r, <-Zmod.add_assoc, Zmod.add_opp_same_r.
rewrite Zmod.add_comm, wplus_unit.
reflexivity.
- unfold fifo_nfifo_elt_not_full in *.
fold fifo_nfifo_elt_not_full in *.
Expand All @@ -79,28 +81,28 @@ Section ToNative.
+ exfalso.
rewrite natToWord_S with (n:= S edSub) in e.
rewrite wminus_plus_distr in e.
rewrite !wminus_def in e.
rewrite <-wplus_assoc with (x:= enqPv) in e.
rewrite wminus_inv in e.
rewrite wplus_comm with (x:= enqPv), wplus_unit in e.
rewrite wplus_comm in e.
rewrite <-!Zmod.add_opp_r in e.
rewrite <-Zmod.add_assoc with (a:= enqPv) in e.
rewrite Zmod.add_opp_same_r in e.
rewrite Zmod.add_comm with (a:= enqPv), wplus_unit in e.
rewrite Zmod.add_comm in e.
rewrite <-wplus_unit with (x:= enqPv) in e at 2.
apply wplus_cancel in e.
apply wneg_zero in e.
apply natToWord_inj in e.
* inv e.
* pose proof (wordToNat_bound (wones rsz)); lia.
* pose proof (wordToNat_bound ((@Zmod.opp (Z.pow 2 (Z.of_nat rsz)) Zmod.one))); lia.
* apply pow2_zero.
+ f_equal.
do 2 rewrite wminus_def.
rewrite <-wplus_assoc.
do 2 rewrite <-Zmod.add_opp_r.
rewrite <-Zmod.add_assoc.
f_equal.
rewrite natToWord_S with (n:= S edSub).
apply wplus_cancel with (c:= $1 ^+ $ (S edSub)).
rewrite <-wplus_assoc, wplus_comm with (x:= ^~ ($1 ^+ $ (S edSub))).
rewrite wminus_inv.
rewrite wplus_comm with (x:= ^~ $ (S edSub)).
rewrite <-wplus_assoc, wminus_inv.
rewrite <-Zmod.add_assoc, Zmod.add_comm with (a:= ^~ ($1 ^+ $ (S edSub))).
rewrite Zmod.add_opp_same_r.
rewrite Zmod.add_comm with (a:= ^~ $ (S edSub)).
rewrite <-Zmod.add_assoc, Zmod.add_opp_same_r.
reflexivity.
Qed.

Expand All @@ -126,7 +128,7 @@ Section ToNative.
refine (Some (existT _ (listEltK dType type) _)).
destruct (weq enqPv deqPv).
- refine (if fullv then _ else _).
+ exact ((eltv deqPv) :: (fifo_nfifo_elt_not_full eltv enqPv (wordToNat (wones rsz)))).
+ exact ((eltv deqPv) :: (fifo_nfifo_elt_not_full eltv enqPv (wordToNat ((@Zmod.opp (Z.pow 2 (Z.of_nat rsz)) Zmod.one))))).
+ exact nil.
- exact (fifo_nfifo_elt_not_full eltv enqPv (wordToNat (enqPv ^- deqPv))).
Defined.
Expand Down Expand Up @@ -232,7 +234,7 @@ Section ToNative.
{ destruct (weq _ _); auto.
exfalso; eapply wplus_one_neq; eauto.
}
* destruct (weq x6 (x5 ^+ $0~1)).
* destruct (weq x6 (x5 ^+ $1)).
{ or3_snd; repeat split.
destruct (weq _ _); auto.
}
Expand All @@ -248,7 +250,7 @@ Section ToNative.
{ destruct (weq _ _); auto.
exfalso; eapply wplus_one_neq; eauto.
}
* destruct (weq x5 (x6 ^+ $0~1)).
* destruct (weq x5 (x6 ^+ $1)).
{ or3_fst; auto. }
{ or3_thd; auto. }
+ simpl in *; kinv_magic_light_with kinv_or3.
Expand Down Expand Up @@ -298,10 +300,10 @@ Section ToNative.
{ rewrite fifo_nfifo_elt_not_full_prop_1.
destruct (weq x6 x6); intuition idtac.
}
{ rewrite wminus_def, <-wplus_assoc.
rewrite wplus_comm with (x:= $0~1), wplus_assoc.
rewrite wminus_inv, wplus_unit.
simpl; rewrite roundTrip_0; reflexivity.
{ rewrite <-Zmod.add_opp_r, <-Zmod.add_assoc.
rewrite Zmod.add_comm with (a:= $1), Zmod.add_assoc.
rewrite Zmod.add_opp_same_r, wplus_unit.
rewrite ?roundTrip_0, ?roundTrip_1; reflexivity.
}
}
{ exfalso; generalize e0; apply wplus_one_neq. }
Expand All @@ -316,52 +318,53 @@ Section ToNative.
{ exfalso.
rewrite natToWord_S with (n:= wordToNat _) in e.
rewrite !wminus_plus_distr in e.
rewrite !wminus_def in e.
rewrite <-wplus_assoc with (x:= x5) in e.
rewrite !wminus_inv in e.
rewrite wplus_comm with (x:= x5) in e.
rewrite <-!Zmod.add_opp_r in e.
rewrite <-Zmod.add_assoc with (a:= x5) in e.
rewrite !Zmod.add_opp_same_r in e.
rewrite Zmod.add_comm with (a:= x5) in e.
rewrite !wplus_unit in e.
rewrite wplus_comm in e.
rewrite Zmod.add_comm in e.
rewrite <-wplus_unit in e.
apply wplus_cancel in e.
apply wneg_zero in e.
rewrite natToWord_wordToNat in e.
apply wneg_zero in e.
inv e.
apply (f_equal (@wordToNat _)) in e;
rewrite roundTrip_0, roundTrip_1 in e; discriminate.
}
{ f_equal.
rewrite wminus_plus_distr.
rewrite !wminus_def.
rewrite wminus_inv, wplus_unit.
rewrite <-wplus_assoc; f_equal.
rewrite <-!Zmod.add_opp_r.
rewrite Zmod.add_opp_same_r, wplus_unit.
rewrite <-Zmod.add_assoc; f_equal.
rewrite natToWord_S with (n:= wordToNat _).
rewrite <-wminus_def.
rewrite Zmod.add_opp_r.
rewrite wminus_plus_distr.
rewrite !wminus_def.
rewrite wminus_inv, wplus_unit.
rewrite <-!Zmod.add_opp_r.
rewrite Zmod.add_opp_same_r, wplus_unit.
rewrite natToWord_wordToNat.
rewrite wneg_idempotent.
rewrite Zmod.opp_opp.
reflexivity.
}
}
{ rewrite wones_wneg_one.
apply wplus_cancel with (c:= x5 ^+ $0~1).
rewrite wminus_def, <-wplus_assoc.
rewrite wplus_comm with (y:= x5 ^+ $0~1).
rewrite wminus_inv.
rewrite wplus_comm with (x:= ^~ $1), <-wplus_assoc.
rewrite wminus_inv.
apply wplus_cancel with (c:= x5 ^+ $1).
rewrite <-Zmod.add_opp_r, <-Zmod.add_assoc.
rewrite Zmod.add_comm with (b:= x5 ^+ $1).
rewrite Zmod.add_opp_same_r.
rewrite Zmod.add_comm with (a:= ^~ $1), <-Zmod.add_assoc.
rewrite Zmod.add_opp_same_r.
reflexivity.
}
}
{ replace (x5 ^- (x5 ^+ $0~1)) with (wones rsz).
{ replace (x5 ^- (x5 ^+ $1)) with ((@Zmod.opp (Z.pow 2 (Z.of_nat rsz)) Zmod.one)).
{ apply Nat.le_refl. }
{ rewrite wones_wneg_one.
apply wplus_cancel with (c:= x5 ^+ $0~1).
rewrite wplus_comm, <-wplus_assoc, wminus_inv.
rewrite wminus_def, <-wplus_assoc.
rewrite wplus_comm with (y:= x5 ^+ $0~1).
rewrite wminus_inv.
apply wplus_cancel with (c:= x5 ^+ $1).
rewrite Zmod.add_comm, <-Zmod.add_assoc, Zmod.add_opp_same_r.
rewrite <-Zmod.add_opp_r, <-Zmod.add_assoc.
rewrite Zmod.add_comm with (b:= x5 ^+ $1).
rewrite Zmod.add_opp_same_r.
reflexivity.
}
}
Expand All @@ -372,8 +375,8 @@ Section ToNative.
apply natToWord_inj with (sz:= S sz).
{ rewrite natToWord_S.
rewrite !natToWord_wordToNat.
rewrite !wminus_def.
rewrite wplus_assoc, wplus_comm with (x:= $1).
rewrite <-!Zmod.add_opp_r.
rewrite Zmod.add_assoc, Zmod.add_comm with (a:= $1).
reflexivity.
}
{ pose proof (wordToNat_bound (x5 ^- x6)).
Expand All @@ -385,14 +388,14 @@ Section ToNative.
intro Hx.
apply pow2_minus_one_wones in Hx.
elim n0.
apply wplus_cancel with (c:= ^~ $0~1).
rewrite <-wplus_assoc, wminus_inv.
rewrite wplus_comm, wplus_unit.
rewrite wplus_comm.
apply wplus_cancel with (c:= ^~ $1).
rewrite <-Zmod.add_assoc, Zmod.add_opp_same_r.
rewrite Zmod.add_comm, wplus_unit.
rewrite Zmod.add_comm.
apply wplus_cancel with (c:= ^~ x6).
rewrite <-wplus_assoc, wminus_inv.
rewrite wplus_comm with (y:= wzero _), wplus_unit.
rewrite <-wminus_def; rewrite Hx.
rewrite <-Zmod.add_assoc, Zmod.add_opp_same_r.
rewrite Zmod.add_comm with (b:= Zmod.zero), wplus_unit.
rewrite Zmod.add_opp_r; rewrite Hx.
rewrite wones_wneg_one.
reflexivity.
}
Expand Down Expand Up @@ -432,16 +435,17 @@ Section ToNative.
{ intros; inv H1. }
{ kregmap_red; kregmap_clear; meq.
{ exfalso; eapply wplus_one_neq; eauto. }
{ replace (x6 ^- (x6 ^+ $0~1)) with (wones (S sz)); auto.
apply wplus_cancel with (c:= x6 ^+ $0~1).
rewrite wminus_def, <-wplus_assoc.
rewrite wplus_comm with (x:= ^~ (x6 ^+ _)).
rewrite wminus_inv, wplus_comm with (y:= $0~1).
rewrite wplus_assoc.
replace ((natToWord sz 0)~1) with (natToWord rsz 1) by reflexivity.
{ replace (x6 ^- (x6 ^+ $1)) with ((@Zmod.opp (Z.pow 2 (Z.of_nat (S sz))) Zmod.one)); auto.
apply wplus_cancel with (c:= x6 ^+ $1).
rewrite <-Zmod.add_opp_r, <-Zmod.add_assoc.
rewrite Zmod.add_comm with (a:= ^~ (x6 ^+ _)).
rewrite Zmod.add_opp_same_r, Zmod.add_comm with (b:= $1).
rewrite Zmod.add_assoc.
replace ((natToWord sz 0)~1) with (natToWord rsz 1)
by (rewrite WS_true_natToWord_0; reflexivity).
rewrite wones_wneg_one.
rewrite wplus_comm with (y:= $1), wminus_inv.
apply wplus_comm.
rewrite Zmod.add_comm with (b:= $1), Zmod.add_opp_same_r.
apply Zmod.add_comm.
}
}
}
Expand Down Expand Up @@ -485,11 +489,11 @@ Section ToNative.

rewrite natToWord_wordToNat.
apply wplus_cancel with (c:= x5 ^- x6).
rewrite wminus_def with (y:= x5 ^- x6), <-wplus_assoc.
rewrite wplus_comm with (x:= ^~ (x5 ^- x6)).
rewrite wminus_inv, wminus_def, wplus_comm with (y:= ^~ x6).
rewrite wplus_assoc, wminus_inv.
apply wplus_comm.
rewrite <-Zmod.add_opp_r with (b:= x5 ^- x6), <-Zmod.add_assoc.
rewrite Zmod.add_comm with (a:= ^~ (x5 ^- x6)).
rewrite Zmod.add_opp_same_r, <-Zmod.add_opp_r, Zmod.add_comm with (b:= ^~ x6).
rewrite Zmod.add_assoc, Zmod.add_opp_same_r.
apply Zmod.add_comm.
}
}
{ repeat split.
Expand All @@ -499,9 +503,9 @@ Section ToNative.
{ simpl; repeat f_equal.
replace (wordToNat _) with 1.
{ rewrite fifo_nfifo_elt_not_full_prop_1; reflexivity. }
{ rewrite wminus_def, <-wplus_assoc, wplus_comm.
rewrite <-wplus_assoc, wplus_comm with (y:= x6), wminus_inv.
rewrite wplus_comm, wplus_unit.
{ rewrite <-Zmod.add_opp_r, <-Zmod.add_assoc, Zmod.add_comm.
rewrite <-Zmod.add_assoc, Zmod.add_comm with (b:= x6), Zmod.add_opp_same_r.
rewrite Zmod.add_comm, wplus_unit.
rewrite roundTrip_1; auto.
}
}
Expand Down Expand Up @@ -565,11 +569,11 @@ Section ToNative.
rewrite natToWord_wordToNat.
simpl; f_equal.
apply wplus_cancel with (c:= x4 ^- x5).
rewrite wminus_def with (y:= x4 ^- x5), <-wplus_assoc.
rewrite wplus_comm with (x:= ^~ (x4 ^- x5)).
rewrite wminus_inv, wminus_def, wplus_comm with (y:= ^~ x5).
rewrite wplus_assoc, wminus_inv.
apply wplus_comm.
rewrite <-Zmod.add_opp_r with (b:= x4 ^- x5), <-Zmod.add_assoc.
rewrite Zmod.add_comm with (a:= ^~ (x4 ^- x5)).
rewrite Zmod.add_opp_same_r, <-Zmod.add_opp_r, Zmod.add_comm with (b:= ^~ x5).
rewrite Zmod.add_assoc, Zmod.add_opp_same_r.
apply Zmod.add_comm.
}
}
* repeat split; auto.
Expand Down
6 changes: 3 additions & 3 deletions Kami/Ex/InDepthTutorial.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -548,10 +548,10 @@ Lemma next_f_consistent:
f123 (next123 w1) = f123 (next123 w2).
Proof.
unfold f123, next123; intros.
rewrite 2! wmult_comm with (x:= $2).
repeat rewrite wmult_plus_distr.
rewrite 2! Zmod.mul_comm with (a:= $2).
repeat rewrite Zmod.mul_add_l.
f_equal.
rewrite 2! wmult_comm with (y:= $2).
rewrite 2! Zmod.mul_comm with (b:= $2).
auto.
Qed.
#[local] Hint Immediate next_f_consistent.
Expand Down
2 changes: 1 addition & 1 deletion Kami/Ex/IsaRv32Pgm.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ Section RV32Struct.
| BLTZ rs1 ofs => SBtypeToRaw opcode_BRANCH rs1 x0 funct3_BLT ofs
| BGTZ rs1 ofs => SBtypeToRaw opcode_BRANCH x0 rs1 funct3_BLT ofs
| J ofs => UJtypeToRaw opcode_JAL x0 ofs
| NOP => ItypeToRaw opcode_OP_IMM x0 x0 funct3_ADDI (wzero _)
| NOP => ItypeToRaw opcode_OP_IMM x0 x0 funct3_ADDI (Zmod.zero)
end.

End RV32Struct.
Expand Down
Loading
Loading