blob: 6a8831b1444d9a473fb0e40743356a564eb8c2c5 (
plain)
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
|
Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.NatUtil.
Require Import Bedrock.Word.
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.
|
