-
Notifications
You must be signed in to change notification settings - Fork 3
/
Rlp.thy
155 lines (125 loc) · 5.25 KB
/
Rlp.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
chapter {* Generated by Lem from rlp.lem. *}
theory "Rlp"
imports
Main
"Lem_pervasives"
"Lem_word"
"Word256"
"Word160"
"Word8"
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*)
(*open import Word256*)
(*open import Word160*)
(*open import Word8*)
type_synonym byte =" 8 word "
datatype tree =
Leaf " byte list "
| Node " tree list "
(*val BE_rev : nat -> list byte*)
function (sequential,domintros) BE_rev :: " nat \<Rightarrow>( 8 word)list " where
" BE_rev 0 = ( [])"
|" BE_rev n = ( if n <( 256 :: nat) then [word8FromNat n] else
(word8FromNat (n mod( 256 :: nat)) # BE_rev (n div( 256 :: nat))))"
by pat_completeness auto
(*val BE : nat -> list byte*)
definition BE :: " nat \<Rightarrow>( 8 word)list " where
" BE n = ( List.rev (BE_rev n))"
(*val BD_rev : list byte -> nat*)
function (sequential,domintros) BD_rev :: "( 8 word)list \<Rightarrow> nat " where
" BD_rev ([]) = (( 0 :: nat))"
|" BD_rev (h # t) = ((( 256 :: nat) * BD_rev t) + unat h )"
by pat_completeness auto
(*val BD : list byte -> nat*)
definition BD :: "( 8 word)list \<Rightarrow> nat " where
" BD lst = ( BD_rev (List.rev lst))"
(*val r_b : list byte -> list byte*)
fun r_b :: "( 8 word)list \<Rightarrow>( 8 word)list " where
" r_b ([]) = ( [((word_of_int 128) :: 8 word)])"
|" r_b ([k]) = ( if word_sless k(((word_of_int 128) :: 8 word)) then [k] else [((word_of_int 129) :: 8 word), k])"
|" r_b lst = (
if List.length lst <( 56 :: nat) then word8FromNat (( 128 :: nat) + List.length lst) # lst
else word8FromNat (( 183 :: nat) + List.length (BE (List.length lst))) # (BE (List.length lst) @ lst))"
declare r_b.simps [simp del]
(*val read_n_bytes : nat -> list byte -> maybe (list byte * list byte)*)
definition read_n_bytes :: " nat \<Rightarrow>( 8 word)list \<Rightarrow>(( 8 word)list*( 8 word)list)option " where
" read_n_bytes n lst = (
if List.length lst \<ge> n then Some (List.take n lst, List.drop n lst)
else None )"
(*val de_r_b : list byte -> maybe (list byte * list byte)*)
fun de_r_b :: "( 8 word)list \<Rightarrow>(( 8 word)list*( 8 word)list)option " where
" de_r_b ([]) = ( None )"
|" de_r_b (k # lst) = (
if k =((word_of_int 128) :: 8 word) then Some ([], lst)
else if word_sless k(((word_of_int 128) :: 8 word)) then Some ([k], lst)
else if word_sless k(((word_of_int 184) :: 8 word)) then
((let len = (unat k -( 128 :: nat)) in
(if List.length lst \<ge> len then Some (List.take len lst, List.drop len lst)
else None)))
else if word_sle k(((word_of_int 192) :: 8 word)) then
(case read_n_bytes (unat k -( 183 :: nat)) lst of
None => None
| Some (be_bytes, x_and_rest) =>
read_n_bytes (BD be_bytes) x_and_rest
)
else None )"
declare de_r_b.simps [simp del]
(*val RLP : tree -> list byte*)
function (sequential,domintros) RLP :: " tree \<Rightarrow>(byte)list " where
" RLP (Leaf l) = ( r_b l )"
|" RLP (Node lst) = (
(let s = (List.concat (List.map RLP lst)) in
(let len_s = (List.length s) in
if len_s <( 56 :: nat) then word8FromNat (( 192 :: nat) + len_s) # s
else word8FromNat (( 247 :: nat) + List.length (BE len_s)) # (BE len_s @ s))))"
by pat_completeness auto
(*val RLP_nat : nat -> list byte*)
definition RLP_nat :: " nat \<Rightarrow>(byte)list " where
" RLP_nat i = ( RLP (Leaf (BE i)))"
(*val decode : list byte -> maybe (tree * list byte)*)
(*val decode_n : nat -> list byte -> maybe (list tree * list byte)*)
function (sequential,domintros) decode_n :: " nat \<Rightarrow>(byte)list \<Rightarrow>((tree)list*(byte)list)option "
and decode :: "( 8 word)list \<Rightarrow>(tree*(byte)list)option " where
" decode ([]) = ( None )"
|" decode (k # lst) = (
if word_sless (((word_of_int 247) :: 8 word)) k then
(case read_n_bytes (unat k -( 247 :: nat)) lst of
None => None
| Some (be_bytes, rest) =>
(let list_len = (BD be_bytes) in
(case decode_n list_len rest of
None => None
| Some (lst, rest) => Some (Node lst, rest)
))
)
else if word_sless (((word_of_int 192) :: 8 word)) k then
(let list_len = (unat k -( 192 :: nat)) in
(case decode_n list_len lst of
None => None
| Some (lst, rest) => Some (Node lst, rest)
))
else None )" |" decode_n 0 lst = ( Some ([], lst))"
|" decode_n ((Suc n)) lst = (
(case decode lst of
None => None
| Some (t, left) =>
(case decode_n n left of
None => None
| Some (lst, left) => Some ((t # lst), left)
)
))"
by pat_completeness auto
end