blob: acf2b5c315c3d55288a437ce44fcf8515a288e22 (
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
Require Import ZArith NArith NPeano.
Require Import QhasmCommon.
Require Export Bedrock.Word.
Delimit Scope nword_scope with w.
Local Open Scope nword_scope.
Notation "& x" := (wordToN x) (at level 30) : nword_scope.
Notation "** x" := (NToWord _ x) (at level 30) : nword_scope.
Section Util.
Definition convS {A B: Set} (x: A) (H: A = B): B :=
eq_rect A (fun B0 : Set => B0) x B H.
Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
refine (split1 k (n - k) (convS w _)).
abstract (replace n with (k + (n - k)) by omega; intuition).
Defined.
Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
refine (split2 (n - k) k (convS w _)).
abstract (replace n with (k + (n - k)) by omega; intuition).
Defined.
Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n.
refine (convS (zext w (n - k)) _).
abstract (replace (k + (n - k)) with n by omega; intuition).
Defined.
Definition shiftr {n} (w: word n) (k: nat): word n :=
match (le_dec k n) with
| left p => extend p (high p w)
| right _ => wzero n
end.
Definition mask {n} (k: nat) (w: word n): word n :=
match (le_dec k n) with
| left p => extend p (low p w)
| right _ => w
end.
Definition overflows (n: nat) (x: N) :
{(x >= Npow2 n)%N} + {(x < Npow2 n)%N}.
refine (
let c := (x ?= Npow2 n)%N in
match c as c' return c = c' -> _ with
| Lt => fun _ => right _
| _ => fun _ => left _
end eq_refl); abstract (
unfold c in *; unfold N.lt, N.ge;
repeat match goal with
| [ H: (_ ?= _)%N = _ |- _] =>
rewrite H; intuition; try inversion H
| [ H: Eq = _ |- _] => inversion H
| [ H: Gt = _ |- _] => inversion H
| [ H: Lt = _ |- _] => inversion H
end).
Defined.
Definition break {n} (m: nat) (x: word n): word m * word (n - m).
refine match (le_dec m n) with
| left p => (extend _ (low p x), extend _ (@high (n - m) n _ x))
| right p => (extend _ x, _)
end; try abstract intuition.
replace (n - m) with O by abstract omega; exact WO.
Defined.
Definition addWithCarry {n} (x y: word n) (c: bool): word n :=
x ^+ y ^+ (natToWord _ (if c then 1 else 0)).
Definition omap {A B} (x: option A) (f: A -> option B) :=
match x with | Some y => f y | _ => None end.
Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
End Util.
Close Scope nword_scope.
|
