blob: 7b89e45447a21a0aa58ce0644768b9da82889d93 (
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
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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
|
Require Import Sail2_instr_kinds.
Require Import Sail2_values.
Require Import Sail2_operators_bitlists.
Require Import Sail2_prompt_monad.
Require Import Sail2_prompt.
Require Import Sail2_real.
Axiom slice : forall {m} (_ : mword m) (_ : Z) (n : Z) `{ArithFact (m >= 0)} `{ArithFact (n >= 0)}, mword n.
Definition length {n} (x : mword n) := length_mword x.
Hint Unfold length : sail.
Lemma Replicate_lemma1 {N M O x} :
O * M = N ->
O = Z.quot N M ->
x = Z.quot N M -> M * x = N.
intros. rewrite H1.
rewrite H0 in H.
rewrite Z.mul_comm.
assumption.
Qed.
Hint Resolve Replicate_lemma1 : sail.
Lemma Replicate_lemma2 {N M x} :
M >= 0 /\ N >= 0 ->
x = Z.quot N M ->
x >= 0.
intros; subst.
destruct M; destruct N; intros; try easy.
unfold Z.quot, Z.quotrem.
destruct (N.pos_div_eucl p0 (N.pos p)) as [x y].
case x; easy.
Qed.
Hint Resolve Replicate_lemma2 : sail.
(*
let hexchar_to_bool_list c =
if c = #'0' then Just ([false;false;false;false])
else if c = #'1' then Just ([false;false;false;true ])
else if c = #'2' then Just ([false;false;true; false])
else if c = #'3' then Just ([false;false;true; true ])
else if c = #'4' then Just ([false;true; false;false])
else if c = #'5' then Just ([false;true; false;true ])
else if c = #'6' then Just ([false;true; true; false])
else if c = #'7' then Just ([false;true; true; true ])
else if c = #'8' then Just ([true; false;false;false])
else if c = #'9' then Just ([true; false;false;true ])
else if c = #'A' then Just ([true; false;true; false])
else if c = #'a' then Just ([true; false;true; false])
else if c = #'B' then Just ([true; false;true; true ])
else if c = #'b' then Just ([true; false;true; true ])
else if c = #'C' then Just ([true; true; false;false])
else if c = #'c' then Just ([true; true; false;false])
else if c = #'D' then Just ([true; true; false;true ])
else if c = #'d' then Just ([true; true; false;true ])
else if c = #'E' then Just ([true; true; true; false])
else if c = #'e' then Just ([true; true; true; false])
else if c = #'F' then Just ([true; true; true; true ])
else if c = #'f' then Just ([true; true; true; true ])
else Nothing
let hexstring_to_bools s =
match (toCharList s) with
| z :: x :: hs ->
let str = if (z = #'0' && x = #'x') then hs else z :: x :: hs in
Maybe.map List.concat (just_list (List.map hexchar_to_bool_list str))
| _ -> Nothing
end
val hex_slice : forall 'rv 'e. string -> integer -> integer -> monad 'rv (list bitU) 'e
let hex_slice v len lo =
match hexstring_to_bools v with
| Just bs ->
let hi = len + lo - 1 in
let bs = ext_list false (len + lo) bs in
return (of_bools (subrange_list false bs hi lo))
| Nothing -> Fail "hex_slice"
end
*)
Axiom hex_slice : forall {rv e}, string -> forall n m, monad rv (mword (n - m)) e.
Definition internal_pick {rv a e} (vs : list a) : monad rv a e :=
match vs with
| (h::_) => returnm h
| _ => Fail "empty list in internal_pick"
end.
Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string.
Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt.
Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
Definition undefined_vector {rv a e} len `{ArithFact (len >= 0)} (u : a) : monad rv (vec a len) e := returnm (vec_init u len).
(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
Definition undefined_bitvector {rv e} len `{ArithFact (len >= 0)} : monad rv (mword len) e := returnm (mword_of_int 0).
(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
Definition undefined_bits {rv e} := @undefined_bitvector rv e.
Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU.
Definition undefined_real {rv e} (_:unit) : monad rv R e := returnm (realFromFrac 0 1).
Definition undefined_range {rv e} i j `{ArithFact (i <= j)} : monad rv {z : Z & ArithFact (i <= z /\ z <= j)} e := returnm (build_ex i).
Definition undefined_atom {rv e} i : monad rv Z e := returnm i.
Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii).
(*
(* Use constants for undefined values for now *)
let undefined_string () = return ""
let undefined_unit () = return ()
let undefined_int () = return (0:ii)
val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e
let undefined_vector len u = return (repeat [u] len)
val undefined_bitvector : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
let undefined_bitvector len = return (of_bools (repeat [false] len))
val undefined_bits : forall 'rv 'e. integer -> monad 'rv (list bitU) 'e
let undefined_bits = undefined_bitvector
let undefined_bit () = return B0
let undefined_real () = return (realFromFrac 0 1)
let undefined_range i j = return i
let undefined_atom i = return i
let undefined_nat () = return (0:ii)
val write_ram : forall 'rv 'e.
integer -> integer -> list bitU -> list bitU -> list bitU -> monad 'rv unit 'e*)
Definition write_ram {rv e} addrsize size (hexRAM : mword addrsize) (address : mword addrsize) (value : mword (8 * size)) : monad rv unit e :=
write_mem_ea Write_plain address size >>
write_mem_val value >>= fun _ =>
returnm tt.
(*val read_ram : forall 'rv 'e.
integer -> integer -> list bitU -> list bitU -> monad 'rv (list bitU) 'e*)
Definition read_ram {rv e} addrsize size `{ArithFact (size >= 0)} (hexRAM : mword addrsize) (address : mword addrsize) : monad rv (mword (8 * size)) e :=
read_mem Read_plain address size.
(*val elf_entry : unit -> integer*)
Definition elf_entry (_:unit) := 0.
(*declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
*)
Lemma mul_quot_8_helper : forall x, 8 * x = 8 * (Z.quot (8 * x) 8).
intro.
rewrite Z.mul_comm.
rewrite Z.quot_mul; auto with zarith.
Qed.
Hint Resolve mul_quot_8_helper : sail.
Lemma mul_quot_8_helper2 : forall x y, 8 * x = y -> 8 * x = 8 * (Z.quot y 8).
intros. subst.
apply mul_quot_8_helper.
Qed.
Hint Resolve mul_quot_8_helper2 : sail.
(* For aarch64_vector_arithmetic_binary_uniform_mul_int_dotp *)
Lemma quot4_ge {esize x} : 4 <= esize -> x = Z.quot esize 4 -> x >= 0.
intros.
apply Z.le_ge.
subst.
apply Z.quot_pos; omega.
Qed.
(* except that only proving the hard bit leads to an anomaly...
Hint Resolve quot4_ge : sail.*)
Lemma dotp_lemma {datasize esize x} :
8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
4 <= esize -> x = Z.quot esize 4 -> datasize >= 0 /\ x >= 0.
intros.
split.
* omega.
* eauto using quot4_ge.
Qed.
Hint Resolve dotp_lemma : sail.
Lemma quot4_gt {esize x} : 4 <= esize -> x = Z.quot esize 4 -> x > 0.
intros.
apply Z.lt_gt.
subst.
apply Z.quot_str_pos.
omega.
Qed.
Hint Resolve quot4_gt : sail.
Lemma vector_single_nowb_lemma {x y} : 0 <= x -> 0 <= y ->
y * x >= 0.
intros.
apply Z.le_ge.
apply Z.mul_nonneg_nonneg; auto.
Qed.
Hint Resolve vector_single_nowb_lemma : sail.
Lemma vector_single_nowb_lemma2 {x esize} : 8 * x = esize -> 8 * (Z.quot esize 8) = esize.
intro H.
rewrite <- H.
rewrite (Z.mul_comm 8 x).
rewrite Z.quot_mul; auto with zarith.
Qed.
Hint Resolve vector_single_nowb_lemma2 : sail.
Lemma simdfp_register_lemma {datasize x0} :
8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
x0 = datasize ÷ 8 ->
64 >= 0 /\ 8 * x0 >= 0.
intros.
split.
* omega.
* apply Z.le_ge.
apply Z.mul_nonneg_nonneg; auto with zarith.
subst.
apply Z.quot_pos; omega.
Qed.
Hint Resolve simdfp_register_lemma : sail.
Lemma simdfp_register_lemma2 {datasize x0} :
8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
x0 = datasize ÷ 8 ->
datasize = 8 * x0.
intros [H|[H|[H|[H|[H|[]]]]]] H'; subst;
reflexivity.
Qed.
Hint Resolve simdfp_register_lemma2 : sail.
Lemma atomicops_st_lemma {datasize} :
8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
8 * (datasize ÷ 8) > 0.
intros [H|[H|[H|[H|[H|[]]]]]]; subst;
reflexivity.
Qed.
Hint Resolve atomicops_st_lemma : sail.
Lemma atomicops_cas_pair_lemma1 {datasize x0} :
8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
x0 = 2 * datasize ÷ 8 ->
64 >= 0 /\ 8 * x0 >= 0.
intros [H|[H|[H|[H|[H|[]]]]]]; subst;
intro H; compute in H; subst; omega.
Qed.
Lemma atomicops_cas_pair_lemma2 {datasize} :
8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
2 * datasize = 8 * (2 * datasize ÷ 8).
intros [H|[H|[H|[H|[H|[]]]]]]; subst; reflexivity.
Qed.
Lemma atomicops_cas_pair_lemma3 {datasize x0} :
8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
x0 = 2 * datasize ÷ 8 ->
2 * datasize = 8 * x0.
intros [H|[H|[H|[H|[H|[]]]]]]; subst;
intro H; compute in H; subst; omega.
Qed.
Hint Resolve atomicops_cas_pair_lemma1 atomicops_cas_pair_lemma2 atomicops_cas_pair_lemma3 : sail.
|
