1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
|
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.NatUtil.
Require Import Crypto.Util.Tactics.
Require Import Bedrock.Word.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Program.Program.
Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
Require Import Coq.micromega.Psatz.
Local Open Scope nat_scope.
Lemma pow2_id : forall n, pow2 n = 2 ^ n.
Proof.
induction n; intros; simpl; auto.
Qed.
Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)).
Proof.
induction n; intros; auto.
simpl pow2.
rewrite Nat2Z.inj_succ.
rewrite Z.pow_succ_r by apply Zle_0_nat.
rewrite untimes2.
rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
rewrite <- IHn.
auto.
Qed.
Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
wordToN (NToWord sz n) = n.
Proof.
intros.
rewrite wordToN_nat, NToWord_nat.
rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
Qed.
Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
Proof.
intros.
rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
apply natToWord_wordToNat.
Qed.
Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N.
Proof.
intros x n bound_nat.
rewrite <- Nnat.N2Nat.id, Npow2_nat.
replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
apply (Nat2N_inj_lt _ (pow2 n)).
rewrite pow2_id; assumption.
Qed.
Lemma weqb_false_iff : forall sz (x y : word sz), weqb x y = false <-> x <> y.
Proof.
split; intros.
+ intro eq_xy; apply weqb_true_iff in eq_xy; congruence.
+ case_eq (weqb x y); intros weqb_xy; auto.
apply weqb_true_iff in weqb_xy.
congruence.
Qed.
Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
| eq_refl => w
end)); abstract omega. Defined.
Lemma combine_eq_iff {a b} (A:word a) (B:word b) C :
combine A B = C <-> A = split1 a b C /\ B = split2 a b C.
Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed.
Class wordsize_eq (x y : nat) := wordsize_eq_to_eq : x = y.
Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m :=
match n, m return wordsize_eq n m -> word n -> word m with
| O, O => fun _ _ => WO
| S n', S m' => fun _ w => WS (whd w) (@cast_word _ _ _ (wtl w))
| _, _ => fun _ _ => !
end.
Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *)
Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
Proof. induction w; simpl; auto using f_equal. Qed.
Lemma wordToNat_cast_word {n} (w:word n) m pf :
wordToNat (@cast_word n m pf w) = wordToNat w.
Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
Lemma wordToN_cast_word {n} (w:word n) m pf :
wordToN (@cast_word n m pf w) = wordToN w.
Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
Import NPeano Nat.
Local Infix "++" := combine.
Definition zext_ge n {m} {pf:m <= n} (w:word m) : word n :=
cast_word (w ++ wzero (n - m)).
Definition keeplow {b} n (w:word b) : word b :=
wand (cast_word( wones (min b n) ++ wzero (b-n) )) w.
Definition clearlow {b} n (w:word b) : word b :=
wand (cast_word( wzero (min b n) ++ wones (b-n) )) w.
Definition setbit {b} n {H:n < b} (w:word b) : word b :=
wor (cast_word( wzero n ++ wones 1 ++ wzero (b-n-1) )) w.
Definition clearbit {b} n {H:n < b} (w:word b) : word b :=
wand (cast_word( wones n ++ wzero 1 ++ wones (b-n-1) )) w.
Lemma wordToNat_wzero {n} : wordToNat (wzero n) = 0.
Proof.
unfold wzero; induction n; simpl; try rewrite_hyp!*; omega.
Qed.
Lemma wordToNat_combine : forall {a} (wa:word a) {b} (wb:word b),
wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb.
Proof.
induction wa; intros; simpl; rewrite ?IHwa; break_match; nia.
Qed.
Lemma wordToNat_zext_ge {n m pf} (w:word m) : wordToNat (@zext_ge n m pf w) = wordToNat w.
Proof.
unfold zext_ge.
rewrite wordToNat_cast_word, wordToNat_combine, wordToNat_wzero; nia.
Qed.
Lemma wordToNat_clearlow {b} (c : nat) (x : Word.word b) :
wordToNat (clearlow c x) = wordToNat x - (wordToNat x) mod (2^c).
Admitted.
Lemma wordToNat_keeplow {b} (c : nat) (x : Word.word b) :
wordToNat (keeplow c x) = (wordToNat x) mod (2^c).
Admitted.
Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a).
Admitted.
Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a).
Admitted.
Lemma wordeqb_Zeqb {sz} (x y : word sz) : (Z.of_N (wordToN x) =? Z.of_N (wordToN y))%Z = weqb x y.
Proof.
match goal with |- ?LHS = ?RHS => destruct LHS eqn:HL, RHS eqn:HR end;
repeat match goal with
| _ => reflexivity
| _ => progress unfold not in *
| [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H
| [ |- Z.eqb _ _ = true ] => apply Z.eqb_eq
| [ H : context[Z.of_N _ = Z.of_N _] |- _ ] => rewrite N2Z.inj_iff in H
| [ H : wordToN _ = wordToN _ |- _ ] => apply wordToN_inj in H
| [ H : x = y :> word _ |- _ ] => apply weqb_true_iff in H
| [ H : ?x = false |- _ ] => progress rewrite <- H; clear H
| _ => congruence
| [ H : weqb _ _ = true |- _ ] => apply weqb_true_iff in H; subst
end.
Qed.
|
