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
|
; Yul Library
;
; Copyright (C) 2022 Kestrel Institute (http://www.kestrel.edu)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Author: Alessandro Coglio (coglio@kestrel.edu)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "YUL")
(include-book "static-safety-checking")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defxdoc+ static-safety-checking-evm
:parents (static-semantics)
:short "Static safety checking of the EVM dialect of Yul."
:long
(xdoc::topstring
(xdoc::p
"We specialize the static safety checks for generic Yul to the EVM dialect
by defining a function table for the EVM functions
and by using that as the initial function table
to check the safety of the top-level block.")
(xdoc::p
"The EVM functions are listed at
[Solidity: Yul: Specification of Yul: EVM Dialect].
As noted in the text before the table,
they return either no or one value."))
:order-subtopics t
:default-parent t)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define evm-funtable ()
:returns (funtab funtablep)
:short "Function table for the EVM dialect of Yul."
:long
(xdoc::topstring
(xdoc::p
"This is based on the table in [Solidity],
referenced in @(see static-safety-checking-evm).")
(xdoc::p
"In order to enter the information concisely,
we introduce a macro that builds a nest of @(tsee omap::update)s."))
(evm-funtable-build "stop" 0 0
"add" 2 1
"sub" 2 1
"mul" 2 1
"div" 2 1
"sdiv" 2 1
"mod" 2 1
"smod" 2 1
"exp" 2 1
"not" 1 1
"lt" 2 1
"gt" 2 1
"slt" 2 1
"sgt" 2 1
"eq" 2 1
"iszero" 1 1
"and" 2 1
"or" 2 1
"xor" 2 1
"byte" 2 1
"shl" 2 1
"shr" 2 1
"sar" 2 1
"addmod" 3 1
"mulmod" 3 1
"signextend" 2 1
"keccak256" 2 1
"pc" 0 1
"pop" 1 0
"mload" 1 1
"mstore" 2 0
"mstore8" 2 0
"sload" 1 1
"sstore" 2 0
"msize" 0 1
"gas" 0 1
"address" 0 1
"balance" 1 1
"selfbalance" 0 1
"caller" 0 1
"callvalue" 0 1
"calldataload" 1 1
"calldatasize" 0 1
"calldatacopy" 3 0
"codesize" 0 1
"codecopy" 3 0
"extcodesize" 1 1
"extcodecopy" 4 0
"returndatasize" 0 1
"returndatacopy" 3 0
"extcodehash" 1 1
"create" 3 1
"create2" 4 1
"call" 7 1
"callcode" 7 1
"delegatecall" 6 1
"staticcall" 6 1
"return" 2 0
"revert" 2 0
"selfdestruct" 1 0
"invalid" 0 0
"log0" 2 0
"log1" 3 0
"log2" 4 0
"log3" 5 0
"log4" 6 0
"chainid" 0 1
"basefee" 0 1
"origin" 0 1
"gasprice" 0 1
"blockhash" 1 1
"coinbase" 0 1
"timestamp" 0 1
"number" 0 1
"difficulty" 0 1
"gaslimit" 0 1)
:prepwork
((defun evm-funtable-build-fn (args)
(if (endp args)
nil
`(omap::update (identifier ,(first args))
(make-funtype :in ,(second args) :out ,(third args))
,(evm-funtable-build-fn (cdddr args)))))
(defmacro evm-funtable-build (&rest args)
(evm-funtable-build-fn args))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define check-safe-top-block-evm ((block blockp))
:returns (_ reserr-optionp)
:short "Check if the top block is safe, in the EVM dialect."
:long
(xdoc::topstring
(xdoc::p
"This is like @(tsee check-safe-top-block) for generic Yul,
except that the initial function table is
the one with the EVM functions."))
(b* (((okf modes) (check-safe-block block nil (evm-funtable))))
(if (equal modes (set::insert (mode-regular) nil))
nil
(reserrf (list :top-block-mode modes))))
:hooks (:fix))
|
