blob: dea937ac1cc621af236fd7d725b086f248b3bb21 (
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
|
Require Import ZArith NArith NPeano.
Require Import QhasmCommon.
Require Export Bedrock.Word.
Module Util.
Inductive Either A B := | xleft: A -> Either A B | xright: B -> Either A B.
Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i.
Coercion indexToNat : Index >-> nat.
(* Magical Bitwise Manipulations *)
(* Force w to be m bits long, by truncation or zero-extension *)
Definition trunc {n} (m: nat) (w: word n): word m.
destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s].
- replace m with (n + (m - n)) by abstract intuition.
refine (zext w (m - n)).
- rewrite <- s; assumption.
- replace n with (m + (n - m)) in w by abstract intuition.
refine (split1 m (n-m) w).
Defined.
(* Get the index-th m-bit block of w *)
Definition getIndex {n} (w: word n) (m index: nat): word m.
replace n with
((min n (m * index)) + (n - (min n (m * index))))%nat
in w by abstract (
assert ((min n (m * index)) <= n)%nat
by apply Nat.le_min_l;
intuition).
refine
(trunc m
(split2 (min n (m * index)) (n - min n (m * index)) w)).
Defined.
(* set the index-th m-bit block of w to s *)
Definition setInPlace {n m} (w: word n) (s: word m) (index: nat): word n :=
(w ^& (wnot (trunc n (combine (wones m) (wzero (index * m)%nat)))))
^| (trunc n (combine s (wzero (index * m)%nat))).
(* Iterating Stack Operations *)
Lemma getStackWords_spec: forall {n} (x: Stack n), n = 32 * (getStackWords x).
Proof. intros; destruct x; simpl; intuition. Qed.
Definition segmentStackWord {n} (x: Stack n) (w: word n): word (32 * (getStackWords x)).
intros; destruct x; simpl; intuition.
Defined.
Definition desegmentStackWord {n} (x: Stack n) (w: word (32 * (getStackWords x))): word n.
intros; destruct x; simpl; intuition.
Defined.
End Util.
|
