-
Notifications
You must be signed in to change notification settings - Fork 3
/
Word256.thy
345 lines (216 loc) · 12.5 KB
/
Word256.thy
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
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
chapter {* Generated by Lem from word256.lem. *}
theory "Word256"
imports
Main
"Lem_pervasives"
"Lem_word"
begin
(*
Copyright 2016 Sami Mäkelä
Licensed under the Apache License, Version 2.0 (the License);
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an AS IS BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
(*open import Pervasives*)
(*open import Word*)
(*type word256 = W256 of integer*)
(* perhaps should truncate here? *)
(*val bs_to_w256 : bitSequence -> word256*)
(*let bs_to_w256 seq= W256 (integerFromBitSeq seq)*)
(*val w256_to_bs : word256 -> bitSequence*)
(*let w256_to_bs (W256 i)= bitSeqFromInteger (Just 256) i*)
(*val base : integer*)
definition base :: " int " where
" base = (( 2 :: int)^( 256 :: nat))"
(*val word256BinTest : forall 'a. (integer -> integer -> 'a) -> word256 -> word256 -> 'a*)
fun word256BinTest :: "(int \<Rightarrow> int \<Rightarrow> 'a)\<Rightarrow> 256 word \<Rightarrow> 256 word \<Rightarrow> 'a " where
" word256BinTest binop (W256 w1) (W256 w2) = ( binop (w1 mod base) (w2 mod base))"
declare word256BinTest.simps [simp del]
(*val word256BBinTest : forall 'a. (bitSequence -> bitSequence -> 'a) -> word256 -> word256 -> 'a*)
definition word256BBinTest :: "(bitSequence \<Rightarrow> bitSequence \<Rightarrow> 'a)\<Rightarrow> 256 word \<Rightarrow> 256 word \<Rightarrow> 'a " where
" word256BBinTest binop w1 w2 = ( binop ((\<lambda> w . bitSeqFromInteger (Some 256) ( (sint w))) w1) ((\<lambda> w . bitSeqFromInteger (Some 256) ( (sint w))) w2))"
(*val word256BinOp : (integer -> integer -> integer) -> word256 -> word256 -> word256*)
fun word256BinOp :: "(int \<Rightarrow> int \<Rightarrow> int)\<Rightarrow> 256 word \<Rightarrow> 256 word \<Rightarrow> 256 word " where
" word256BinOp binop (W256 w1) (W256 w2) = ( W256 (binop (w1 mod base) (w2 mod base) mod base))"
declare word256BinOp.simps [simp del]
(*val word256BBinOp : (bitSequence -> bitSequence -> bitSequence) -> word256 -> word256 -> word256*)
definition word256BBinOp :: "(bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence)\<Rightarrow> 256 word \<Rightarrow> 256 word \<Rightarrow> 256 word " where
" word256BBinOp binop w1 w2 = ( (\<lambda> w . word_of_int (integerFromBitSeq w)) (binop ((\<lambda> w . bitSeqFromInteger (Some 256) ( (sint w))) w1) ((\<lambda> w . bitSeqFromInteger (Some 256) ( (sint w))) w2)))"
(*val word256NatOp : (integer -> nat -> integer) -> word256 -> nat -> word256*)
fun word256NatOp :: "(int \<Rightarrow> nat \<Rightarrow> int)\<Rightarrow> 256 word \<Rightarrow> nat \<Rightarrow> 256 word " where
" word256NatOp binop (W256 w1) n = ( W256 (binop (w1 mod base) n mod base))"
declare word256NatOp.simps [simp del]
(*val word256BNatOp : (bitSequence -> nat -> bitSequence) -> word256 -> nat -> word256*)
definition word256BNatOp :: "(bitSequence \<Rightarrow> nat \<Rightarrow> bitSequence)\<Rightarrow> 256 word \<Rightarrow> nat \<Rightarrow> 256 word " where
" word256BNatOp binop w1 n = ( (\<lambda> w . word_of_int (integerFromBitSeq w)) (binop ((\<lambda> w . bitSeqFromInteger (Some 256) ( (sint w))) w1) n))"
(*val word256BUnaryOp : (bitSequence -> bitSequence) -> word256 -> word256*)
definition word256BUnaryOp :: "(bitSequence \<Rightarrow> bitSequence)\<Rightarrow> 256 word \<Rightarrow> 256 word " where
" word256BUnaryOp op1 w = ( (\<lambda> w . word_of_int (integerFromBitSeq w)) (op1 ((\<lambda> w . bitSeqFromInteger (Some 256) ( (sint w))) w)))"
(*val word256UnaryOp : (integer -> integer) -> word256 -> word256*)
fun word256UnaryOp :: "(int \<Rightarrow> int)\<Rightarrow> 256 word \<Rightarrow> 256 word " where
" word256UnaryOp op1 (W256 w) = ( W256 (op1 w mod base))"
declare word256UnaryOp.simps [simp del]
(*val word256ToNat : word256 -> nat*)
(*let word256ToNat w= natFromInteger (integerFromBitSeq (w256_to_bs w))*)
(*val word256ToInt : word256 -> int*)
(*let word256ToInt w= intFromInteger (integerFromBitSeq (w256_to_bs w))*)
(*val word256FromInteger : integer -> word256*)
(*let word256FromInteger i= W256 ((Instance_Num_NumRemainder_Num_integer.mod) i base)*)
(*val word256FromInt : int -> word256*)
(*let word256FromInt i= W256 ((Instance_Num_NumRemainder_Num_integer.mod) (integerFromInt i) base)*)
(*val word256FromNat : nat -> word256*)
definition word256FromNat :: " nat \<Rightarrow> 256 word " where
" word256FromNat i = ( (\<lambda> i . word_of_int ( i)) (int i))"
(*val word256FromBoollist : list bool -> word256*)
(*let word256FromBoollist lst= match bitSeqFromBoolList lst with
| Nothing -> bs_to_w256 0
| Just a -> bs_to_w256 a
end*)
(*val boolListFromWord256 : word256 -> list bool*)
(*let boolListFromWord256 w= boolListFrombitSeq 256 (w256_to_bs w)*)
(*val word256FromNumeral : numeral -> word256*)
(*let word256FromNumeral w= W256 ((Instance_Num_NumRemainder_Num_integer.mod) (integerFromNumeral w) base)*)
(*val w256Eq : word256 -> word256 -> bool*)
definition w256Eq :: " 256 word \<Rightarrow> 256 word \<Rightarrow> bool " where
" w256Eq = ( (op=))"
(*val w256Less : word256 -> word256 -> bool*)
(*let w256Less bs1 bs2= word256BinTest
(Instance_Basic_classes_Ord_Num_integer.<) bs1 bs2*)
(*val w256LessEqual : word256 -> word256 -> bool*)
(*let w256LessEqual bs1 bs2= word256BinTest
(Instance_Basic_classes_Ord_Num_integer.<=) bs1 bs2*)
(*val w256Greater : word256 -> word256 -> bool*)
(*let w256Greater bs1 bs2= word256BinTest
(Instance_Basic_classes_Ord_Num_integer.>) bs1 bs2*)
(*val w256GreaterEqual : word256 -> word256 -> bool*)
(*let w256GreaterEqual bs1 bs2= word256BinTest
(Instance_Basic_classes_Ord_Num_integer.>=) bs1 bs2*)
(*val w256Compare : word256 -> word256 -> ordering*)
(*let w256Compare bs1 bs2= word256BinTest
Instance_Basic_classes_Ord_Num_integer.compare bs1 bs2*)
definition instance_Basic_classes_Ord_Word256_word256_dict :: "( 256 word)Ord_class " where
" instance_Basic_classes_Ord_Word256_word256_dict = ((|
compare_method = (genericCompare word_sless w256Eq),
isLess_method = word_sless,
isLessEqual_method = word_sle,
isGreater_method = (\<lambda> x y. word_sless y x),
isGreaterEqual_method = (\<lambda> x y. word_sle y x)|) )"
(*val word256Negate : word256 -> word256*)
(*let word256Negate= word256UnaryOp
Instance_Num_NumNegate_Num_integer.~*)
(*val word256Succ : word256 -> word256*)
(*let word256Succ= word256UnaryOp
Instance_Num_NumSucc_Num_integer.succ*)
(*val word256Pred : word256 -> word256*)
(*let word256Pred= word256UnaryOp
Instance_Num_NumPred_Num_integer.pred*)
(*val word256Lnot : word256 -> word256*)
(*let word256Lnot= word256UnaryOp
Instance_Word_WordNot_Num_integer.lnot*)
(*val word256Add : word256 -> word256 -> word256*)
(*let word256Add= word256BinOp
(Instance_Num_NumAdd_Num_integer.+)*)
(*val word256Minus : word256 -> word256 -> word256*)
(*let word256Minus= word256BinOp
(Instance_Num_NumMinus_Num_integer.-)*)
(*val word256Mult : word256 -> word256 -> word256*)
(*let word256Mult= word256BinOp
( Instance_Num_NumMult_Num_integer.* )*)
(*val word256IntegerDivision : word256 -> word256 -> word256*)
(*let word256IntegerDivision= word256BinOp
(Instance_Num_NumDivision_Num_integer./)*)
(*val word256Division : word256 -> word256 -> word256*)
(*let word256Division= word256BinOp
Instance_Num_NumIntegerDivision_Num_integer.div*)
(*val word256Remainder : word256 -> word256 -> word256*)
(*let word256Remainder= word256BinOp
(Instance_Num_NumRemainder_Num_integer.mod)*)
(*val word256Land : word256 -> word256 -> word256*)
(*let word256Land= word256BinOp
(Instance_Word_WordAnd_Num_integer.land)*)
(*val word256Lor : word256 -> word256 -> word256*)
(*let word256Lor= word256BinOp
(Instance_Word_WordOr_Num_integer.lor)*)
(*val word256Lxor : word256 -> word256 -> word256*)
(*let word256Lxor= word256BinOp
(Instance_Word_WordXor_Num_integer.lxor)*)
(*val word256Min : word256 -> word256 -> word256*)
(*let word256Min= word256BinOp (Instance_Basic_classes_OrdMaxMin_Num_integer.min)*)
(*val word256Max : word256 -> word256 -> word256*)
(*let word256Max= word256BinOp (Instance_Basic_classes_OrdMaxMin_Num_integer.max)*)
(*val word256Power : word256 -> nat -> word256*)
(*let word256Power= word256NatOp
( Instance_Num_NumPow_Num_integer.** )*)
(*val word256Asr : word256 -> nat -> word256*)
(*let word256Asr= word256NatOp
(Instance_Word_WordAsr_Num_integer.asr)*)
(*val word256Lsr : word256 -> nat -> word256*)
(*let word256Lsr= word256NatOp
(Instance_Word_WordLsr_Num_integer.lsr)*)
(*val word256Lsl : word256 -> nat -> word256*)
(*let word256Lsl= word256NatOp
(Instance_Word_WordLsl_Num_integer.lsl)*)
definition instance_Num_NumNegate_Word256_word256_dict :: "( 256 word)NumNegate_class " where
" instance_Num_NumNegate_Word256_word256_dict = ((|
numNegate_method = (\<lambda> i. - i)|) )"
definition instance_Num_NumAdd_Word256_word256_dict :: "( 256 word)NumAdd_class " where
" instance_Num_NumAdd_Word256_word256_dict = ((|
numAdd_method = (op+)|) )"
definition instance_Num_NumMinus_Word256_word256_dict :: "( 256 word)NumMinus_class " where
" instance_Num_NumMinus_Word256_word256_dict = ((|
numMinus_method = (op-)|) )"
definition instance_Num_NumSucc_Word256_word256_dict :: "( 256 word)NumSucc_class " where
" instance_Num_NumSucc_Word256_word256_dict = ((|
succ_method = (\<lambda> n. n + 1)|) )"
definition instance_Num_NumPred_Word256_word256_dict :: "( 256 word)NumPred_class " where
" instance_Num_NumPred_Word256_word256_dict = ((|
pred_method = (\<lambda> n. n - 1)|) )"
definition instance_Num_NumMult_Word256_word256_dict :: "( 256 word)NumMult_class " where
" instance_Num_NumMult_Word256_word256_dict = ((|
numMult_method = (op*)|) )"
definition instance_Num_NumPow_Word256_word256_dict :: "( 256 word)NumPow_class " where
" instance_Num_NumPow_Word256_word256_dict = ((|
numPow_method = (op^)|) )"
definition instance_Num_NumIntegerDivision_Word256_word256_dict :: "( 256 word)NumIntegerDivision_class " where
" instance_Num_NumIntegerDivision_Word256_word256_dict = ((|
div_method = (op div)|) )"
definition instance_Num_NumDivision_Word256_word256_dict :: "( 256 word)NumDivision_class " where
" instance_Num_NumDivision_Word256_word256_dict = ((|
numDivision_method = (op div)|) )"
definition instance_Num_NumRemainder_Word256_word256_dict :: "( 256 word)NumRemainder_class " where
" instance_Num_NumRemainder_Word256_word256_dict = ((|
mod_method = (op mod)|) )"
definition instance_Basic_classes_OrdMaxMin_Word256_word256_dict :: "( 256 word)OrdMaxMin_class " where
" instance_Basic_classes_OrdMaxMin_Word256_word256_dict = ((|
max_method = max,
min_method = min |) )"
definition instance_Word_WordNot_Word256_word256_dict :: "( 256 word)WordNot_class " where
" instance_Word_WordNot_Word256_word256_dict = ((|
lnot_method = (\<lambda> w. (NOT w))|) )"
definition instance_Word_WordAnd_Word256_word256_dict :: "( 256 word)WordAnd_class " where
" instance_Word_WordAnd_Word256_word256_dict = ((|
land_method = (op AND)|) )"
definition instance_Word_WordOr_Word256_word256_dict :: "( 256 word)WordOr_class " where
" instance_Word_WordOr_Word256_word256_dict = ((|
lor_method = (op OR)|) )"
definition instance_Word_WordXor_Word256_word256_dict :: "( 256 word)WordXor_class " where
" instance_Word_WordXor_Word256_word256_dict = ((|
lxor_method = (op XOR)|) )"
definition instance_Word_WordLsl_Word256_word256_dict :: "( 256 word)WordLsl_class " where
" instance_Word_WordLsl_Word256_word256_dict = ((|
lsl_method = (op<<)|) )"
definition instance_Word_WordLsr_Word256_word256_dict :: "( 256 word)WordLsr_class " where
" instance_Word_WordLsr_Word256_word256_dict = ((|
lsr_method = (op>>)|) )"
definition instance_Word_WordAsr_Word256_word256_dict :: "( 256 word)WordAsr_class " where
" instance_Word_WordAsr_Word256_word256_dict = ((|
asr_method = (op>>>)|) )"
(*val word256UGT : word256 -> word256 -> bool*)
(*let word256UGT a b= (Instance_Basic_classes_Ord_nat.>) (word256ToNat a) (word256ToNat b)*)
end