-
Notifications
You must be signed in to change notification settings - Fork 3
/
Word160.thy
345 lines (216 loc) · 12.5 KB
/
Word160.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 word160.lem. *}
theory "Word160"
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 word160 = W160 of integer*)
(* perhaps should truncate here? *)
(*val bs_to_w160 : bitSequence -> word160*)
(*let bs_to_w160 seq= W160 (integerFromBitSeq seq)*)
(*val w160_to_bs : word160 -> bitSequence*)
(*let w160_to_bs (W160 i)= bitSeqFromInteger (Just 160) i*)
(*val base : integer*)
definition base :: " int " where
" base = (( 2 :: int)^( 160 :: nat))"
(*val word160BinTest : forall 'a. (integer -> integer -> 'a) -> word160 -> word160 -> 'a*)
fun word160BinTest :: "(int \<Rightarrow> int \<Rightarrow> 'a)\<Rightarrow> 160 word \<Rightarrow> 160 word \<Rightarrow> 'a " where
" word160BinTest binop (W160 w1) (W160 w2) = ( binop (w1 mod base) (w2 mod base))"
declare word160BinTest.simps [simp del]
(*val word160BBinTest : forall 'a. (bitSequence -> bitSequence -> 'a) -> word160 -> word160 -> 'a*)
definition word160BBinTest :: "(bitSequence \<Rightarrow> bitSequence \<Rightarrow> 'a)\<Rightarrow> 160 word \<Rightarrow> 160 word \<Rightarrow> 'a " where
" word160BBinTest binop w1 w2 = ( binop ((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w1) ((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w2))"
(*val word160BinOp : (integer -> integer -> integer) -> word160 -> word160 -> word160*)
fun word160BinOp :: "(int \<Rightarrow> int \<Rightarrow> int)\<Rightarrow> 160 word \<Rightarrow> 160 word \<Rightarrow> 160 word " where
" word160BinOp binop (W160 w1) (W160 w2) = ( W160 (binop (w1 mod base) (w2 mod base) mod base))"
declare word160BinOp.simps [simp del]
(*val word160BBinOp : (bitSequence -> bitSequence -> bitSequence) -> word160 -> word160 -> word160*)
definition word160BBinOp :: "(bitSequence \<Rightarrow> bitSequence \<Rightarrow> bitSequence)\<Rightarrow> 160 word \<Rightarrow> 160 word \<Rightarrow> 160 word " where
" word160BBinOp binop w1 w2 = ( (\<lambda> w . word_of_int (integerFromBitSeq w)) (binop ((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w1) ((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w2)))"
(*val word160NatOp : (integer -> nat -> integer) -> word160 -> nat -> word160*)
fun word160NatOp :: "(int \<Rightarrow> nat \<Rightarrow> int)\<Rightarrow> 160 word \<Rightarrow> nat \<Rightarrow> 160 word " where
" word160NatOp binop (W160 w1) n = ( W160 (binop (w1 mod base) n mod base))"
declare word160NatOp.simps [simp del]
(*val word160BNatOp : (bitSequence -> nat -> bitSequence) -> word160 -> nat -> word160*)
definition word160BNatOp :: "(bitSequence \<Rightarrow> nat \<Rightarrow> bitSequence)\<Rightarrow> 160 word \<Rightarrow> nat \<Rightarrow> 160 word " where
" word160BNatOp binop w1 n = ( (\<lambda> w . word_of_int (integerFromBitSeq w)) (binop ((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w1) n))"
(*val word160BUnaryOp : (bitSequence -> bitSequence) -> word160 -> word160*)
definition word160BUnaryOp :: "(bitSequence \<Rightarrow> bitSequence)\<Rightarrow> 160 word \<Rightarrow> 160 word " where
" word160BUnaryOp op1 w = ( (\<lambda> w . word_of_int (integerFromBitSeq w)) (op1 ((\<lambda> w . bitSeqFromInteger (Some 160) ( (sint w))) w)))"
(*val word160UnaryOp : (integer -> integer) -> word160 -> word160*)
fun word160UnaryOp :: "(int \<Rightarrow> int)\<Rightarrow> 160 word \<Rightarrow> 160 word " where
" word160UnaryOp op1 (W160 w) = ( W160 (op1 w mod base))"
declare word160UnaryOp.simps [simp del]
(*val word160ToNat : word160 -> nat*)
(*let word160ToNat w= natFromInteger (integerFromBitSeq (w160_to_bs w))*)
(*val word160ToInt : word160 -> int*)
(*let word160ToInt w= intFromInteger (integerFromBitSeq (w160_to_bs w))*)
(*val word160FromInteger : integer -> word160*)
(*let word160FromInteger i= W160 ((Instance_Num_NumRemainder_Num_integer.mod) i base)*)
(*val word160FromInt : int -> word160*)
(*let word160FromInt i= W160 ((Instance_Num_NumRemainder_Num_integer.mod) (integerFromInt i) base)*)
(*val word160FromNat : nat -> word160*)
definition word160FromNat :: " nat \<Rightarrow> 160 word " where
" word160FromNat i = ( (\<lambda> i . word_of_int ( i)) (int i))"
(*val word160FromBoollist : list bool -> word160*)
(*let word160FromBoollist lst= match bitSeqFromBoolList lst with
| Nothing -> bs_to_w160 0
| Just a -> bs_to_w160 a
end*)
(*val boolListFromWord160 : word160 -> list bool*)
(*let boolListFromWord160 w= boolListFrombitSeq 160 (w160_to_bs w)*)
(*val word160FromNumeral : numeral -> word160*)
(*let word160FromNumeral w= W160 ((Instance_Num_NumRemainder_Num_integer.mod) (integerFromNumeral w) base)*)
(*val w160Eq : word160 -> word160 -> bool*)
definition w160Eq :: " 160 word \<Rightarrow> 160 word \<Rightarrow> bool " where
" w160Eq = ( (op=))"
(*val w160Less : word160 -> word160 -> bool*)
(*let w160Less bs1 bs2= word160BinTest
(Instance_Basic_classes_Ord_Num_integer.<) bs1 bs2*)
(*val w160LessEqual : word160 -> word160 -> bool*)
(*let w160LessEqual bs1 bs2= word160BinTest
(Instance_Basic_classes_Ord_Num_integer.<=) bs1 bs2*)
(*val w160Greater : word160 -> word160 -> bool*)
(*let w160Greater bs1 bs2= word160BinTest
(Instance_Basic_classes_Ord_Num_integer.>) bs1 bs2*)
(*val w160GreaterEqual : word160 -> word160 -> bool*)
(*let w160GreaterEqual bs1 bs2= word160BinTest
(Instance_Basic_classes_Ord_Num_integer.>=) bs1 bs2*)
(*val w160Compare : word160 -> word160 -> ordering*)
(*let w160Compare bs1 bs2= word160BinTest
Instance_Basic_classes_Ord_Num_integer.compare bs1 bs2*)
definition instance_Basic_classes_Ord_Word160_word160_dict :: "( 160 word)Ord_class " where
" instance_Basic_classes_Ord_Word160_word160_dict = ((|
compare_method = (genericCompare word_sless w160Eq),
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 word160Negate : word160 -> word160*)
(*let word160Negate= word160UnaryOp
Instance_Num_NumNegate_Num_integer.~*)
(*val word160Succ : word160 -> word160*)
(*let word160Succ= word160UnaryOp
Instance_Num_NumSucc_Num_integer.succ*)
(*val word160Pred : word160 -> word160*)
(*let word160Pred= word160UnaryOp
Instance_Num_NumPred_Num_integer.pred*)
(*val word160Lnot : word160 -> word160*)
(*let word160Lnot= word160UnaryOp
Instance_Word_WordNot_Num_integer.lnot*)
(*val word160Add : word160 -> word160 -> word160*)
(*let word160Add= word160BinOp
(Instance_Num_NumAdd_Num_integer.+)*)
(*val word160Minus : word160 -> word160 -> word160*)
(*let word160Minus= word160BinOp
(Instance_Num_NumMinus_Num_integer.-)*)
(*val word160Mult : word160 -> word160 -> word160*)
(*let word160Mult= word160BinOp
( Instance_Num_NumMult_Num_integer.* )*)
(*val word160IntegerDivision : word160 -> word160 -> word160*)
(*let word160IntegerDivision= word160BinOp
(Instance_Num_NumDivision_Num_integer./)*)
(*val word160Division : word160 -> word160 -> word160*)
(*let word160Division= word160BinOp
Instance_Num_NumIntegerDivision_Num_integer.div*)
(*val word160Remainder : word160 -> word160 -> word160*)
(*let word160Remainder= word160BinOp
(Instance_Num_NumRemainder_Num_integer.mod)*)
(*val word160Land : word160 -> word160 -> word160*)
(*let word160Land= word160BinOp
(Instance_Word_WordAnd_Num_integer.land)*)
(*val word160Lor : word160 -> word160 -> word160*)
(*let word160Lor= word160BinOp
(Instance_Word_WordOr_Num_integer.lor)*)
(*val word160Lxor : word160 -> word160 -> word160*)
(*let word160Lxor= word160BinOp
(Instance_Word_WordXor_Num_integer.lxor)*)
(*val word160Min : word160 -> word160 -> word160*)
(*let word160Min= word160BinOp (Instance_Basic_classes_OrdMaxMin_Num_integer.min)*)
(*val word160Max : word160 -> word160 -> word160*)
(*let word160Max= word160BinOp (Instance_Basic_classes_OrdMaxMin_Num_integer.max)*)
(*val word160Power : word160 -> nat -> word160*)
(*let word160Power= word160NatOp
( Instance_Num_NumPow_Num_integer.** )*)
(*val word160Asr : word160 -> nat -> word160*)
(*let word160Asr= word160NatOp
(Instance_Word_WordAsr_Num_integer.asr)*)
(*val word160Lsr : word160 -> nat -> word160*)
(*let word160Lsr= word160NatOp
(Instance_Word_WordLsr_Num_integer.lsr)*)
(*val word160Lsl : word160 -> nat -> word160*)
(*let word160Lsl= word160NatOp
(Instance_Word_WordLsl_Num_integer.lsl)*)
definition instance_Num_NumNegate_Word160_word160_dict :: "( 160 word)NumNegate_class " where
" instance_Num_NumNegate_Word160_word160_dict = ((|
numNegate_method = (\<lambda> i. - i)|) )"
definition instance_Num_NumAdd_Word160_word160_dict :: "( 160 word)NumAdd_class " where
" instance_Num_NumAdd_Word160_word160_dict = ((|
numAdd_method = (op+)|) )"
definition instance_Num_NumMinus_Word160_word160_dict :: "( 160 word)NumMinus_class " where
" instance_Num_NumMinus_Word160_word160_dict = ((|
numMinus_method = (op-)|) )"
definition instance_Num_NumSucc_Word160_word160_dict :: "( 160 word)NumSucc_class " where
" instance_Num_NumSucc_Word160_word160_dict = ((|
succ_method = (\<lambda> n. n + 1)|) )"
definition instance_Num_NumPred_Word160_word160_dict :: "( 160 word)NumPred_class " where
" instance_Num_NumPred_Word160_word160_dict = ((|
pred_method = (\<lambda> n. n - 1)|) )"
definition instance_Num_NumMult_Word160_word160_dict :: "( 160 word)NumMult_class " where
" instance_Num_NumMult_Word160_word160_dict = ((|
numMult_method = (op*)|) )"
definition instance_Num_NumPow_Word160_word160_dict :: "( 160 word)NumPow_class " where
" instance_Num_NumPow_Word160_word160_dict = ((|
numPow_method = (op^)|) )"
definition instance_Num_NumIntegerDivision_Word160_word160_dict :: "( 160 word)NumIntegerDivision_class " where
" instance_Num_NumIntegerDivision_Word160_word160_dict = ((|
div_method = (op div)|) )"
definition instance_Num_NumDivision_Word160_word160_dict :: "( 160 word)NumDivision_class " where
" instance_Num_NumDivision_Word160_word160_dict = ((|
numDivision_method = (op div)|) )"
definition instance_Num_NumRemainder_Word160_word160_dict :: "( 160 word)NumRemainder_class " where
" instance_Num_NumRemainder_Word160_word160_dict = ((|
mod_method = (op mod)|) )"
definition instance_Basic_classes_OrdMaxMin_Word160_word160_dict :: "( 160 word)OrdMaxMin_class " where
" instance_Basic_classes_OrdMaxMin_Word160_word160_dict = ((|
max_method = max,
min_method = min |) )"
definition instance_Word_WordNot_Word160_word160_dict :: "( 160 word)WordNot_class " where
" instance_Word_WordNot_Word160_word160_dict = ((|
lnot_method = (\<lambda> w. (NOT w))|) )"
definition instance_Word_WordAnd_Word160_word160_dict :: "( 160 word)WordAnd_class " where
" instance_Word_WordAnd_Word160_word160_dict = ((|
land_method = (op AND)|) )"
definition instance_Word_WordOr_Word160_word160_dict :: "( 160 word)WordOr_class " where
" instance_Word_WordOr_Word160_word160_dict = ((|
lor_method = (op OR)|) )"
definition instance_Word_WordXor_Word160_word160_dict :: "( 160 word)WordXor_class " where
" instance_Word_WordXor_Word160_word160_dict = ((|
lxor_method = (op XOR)|) )"
definition instance_Word_WordLsl_Word160_word160_dict :: "( 160 word)WordLsl_class " where
" instance_Word_WordLsl_Word160_word160_dict = ((|
lsl_method = (op<<)|) )"
definition instance_Word_WordLsr_Word160_word160_dict :: "( 160 word)WordLsr_class " where
" instance_Word_WordLsr_Word160_word160_dict = ((|
lsr_method = (op>>)|) )"
definition instance_Word_WordAsr_Word160_word160_dict :: "( 160 word)WordAsr_class " where
" instance_Word_WordAsr_Word160_word160_dict = ((|
asr_method = (op>>>)|) )"
(*val word160UGT : word160 -> word160 -> bool*)
(*let word160UGT a b= (Instance_Basic_classes_Ord_nat.>) (word160ToNat a) (word160ToNat b)*)
end