-
Notifications
You must be signed in to change notification settings - Fork 3
/
EvmAuxiliary.thy
62 lines (44 loc) · 1.88 KB
/
EvmAuxiliary.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
chapter {* Generated by Lem from evm.lem. *}
theory "EvmAuxiliary"
imports
Main "~~/src/HOL/Library/Code_Target_Numeral"
"Lem_pervasives"
"Lem_word"
"Word256"
"Word160"
"Word8"
"Evm"
begin
(****************************************************)
(* *)
(* Termination Proofs *)
(* *)
(****************************************************)
termination store_byte_list_memory by lexicographic_order
(****************************************************)
(* *)
(* Lemmata *)
(* *)
(****************************************************)
lemma uint_to_address_def_lemma:
" ((\<forall> w. word160FromNat (unat w) = Word.ucast w)) "
(* Theorem: uint_to_address_def_lemma*)(* try *) by auto
lemma address_to_uint_def_lemma:
" ((\<forall> w. word256FromNat (unat w) = Word.ucast w)) "
(* Theorem: address_to_uint_def_lemma*)(* try *) by auto
lemma uint_to_byte_def_lemma:
" ((\<forall> w. word8FromNat (unat w) = Word.ucast w)) "
(* Theorem: uint_to_byte_def_lemma*)(* try *) by auto
lemma byte_to_uint_def_lemma:
" ((\<forall> w. word256FromNat (unat w) = Word.ucast w)) "
(* Theorem: byte_to_uint_def_lemma*)(* try *) by auto
lemma word_rsplit_def_lemma:
" ((\<forall> w. word_rsplit_aux (to_bl w) (( 32 :: nat)) = word_rsplit w)) "
(* Theorem: word_rsplit_def_lemma*)(* try *) by auto
lemma address_to_bytes_def_lemma:
" ((\<forall> w. word_rsplit_aux (to_bl w) (( 20 :: nat)) = word_rsplit w)) "
(* Theorem: address_to_bytes_def_lemma*)(* try *) by auto
lemma word_of_bytes_def_lemma:
" ((\<forall> lst. of_bl (List.concat (List.map to_bl lst)) = word_rcat lst)) "
(* Theorem: word_of_bytes_def_lemma*)(* try *) by auto
end