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
|
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.
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 *)
Local Infix "++" := combine.
Definition keeplow n {b} {H:n <= b} (w:word b) : word b :=
wand (cast_word( wones n ++ wzero (b-n) )) w.
Definition clearlow n {b} {H:n <= b} (w:word b) : word b :=
wand (cast_word( wzero n ++ wones (b-n) )) w.
Definition setbit n {b} {H:n < b} (w:word b) : word b :=
wor (cast_word( wzero n ++ wones 1 ++ wzero (b-n-1) )) w.
Definition clearbit n {b} {H:n < b} (w:word b) : word b :=
wand (cast_word( wones n ++ wzero 1 ++ wones (b-n-1) )) w.
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 wordToNnat_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.
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.
|
