Skip to content

Commit dc2e22b

Browse files
emarzionemarzion
committed
updating regressions + goldens
1 parent 571268d commit dc2e22b

10 files changed

+35755
-16260
lines changed

‎test/regression-evm-semantics-39dd1e5/generate.sh

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,4 +46,5 @@ done
4646
kollect test-sum-to-n \
4747
./kevm prove --backend haskell \
4848
tests/specs/examples/sum-to-n-spec.k \
49-
--format-failures --def-module VERIFICATION
49+
VERIFICATION \
50+
--format-failures

‎test/regression-evm-semantics-39dd1e5/test-add0.sh.out.golden

Lines changed: 1 addition & 232 deletions
Original file line numberDiff line numberDiff line change
@@ -1,232 +1 @@
1-
/* Fl Fn D Sfa Cl */
2-
Lbl'-LT-'generatedTop'-GT-'{}(
3-
/* Fl Fn D Sfa Cl */
4-
Lbl'-LT-'kevm'-GT-'{}(
5-
/* Fl Fn D Sfa Cl */ Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
6-
/* Fl Fn D Sfa Cl */
7-
Lbl'-LT-'exit-code'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")),
8-
/* Fl Fn D Sfa Cl */
9-
Lbl'-LT-'mode'-GT-'{}(
10-
/* Fl Fn D Sfa Cl */
11-
LblSUCCESS'Unds'ETHEREUM-SIMULATION'Unds'Mode{}()
12-
),
13-
/* Fl Fn D Sfa Cl */
14-
Lbl'-LT-'schedule'-GT-'{}(/* Fl Fn D Sfa Cl */ LblDEFAULT'Unds'EVM{}()),
15-
/* Fl Fn D Sfa Cl */
16-
Lbl'-LT-'ethereum'-GT-'{}(
17-
/* Fl Fn D Sfa Cl */
18-
Lbl'-LT-'evm'-GT-'{}(
19-
/* Fl Fn D Sfa Cl */
20-
Lbl'-LT-'output'-GT-'{}(
21-
/* Fl Fn D Sfa Cl */ \dv{SortBytes{}}("")
22-
),
23-
/* Fl Fn D Sfa Cl */
24-
Lbl'-LT-'statusCode'-GT-'{}(
25-
/* Fl Fn D Sfa Cl */
26-
Lbl'Stop'StatusCode'Unds'NETWORK'Unds'StatusCode{}()
27-
),
28-
/* Fl Fn D Sfa Cl */
29-
Lbl'-LT-'callStack'-GT-'{}(
30-
/* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Stop'List{}()
31-
),
32-
/* Fl Fn D Sfa Cl */
33-
Lbl'-LT-'interimStates'-GT-'{}(
34-
/* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Stop'List{}()
35-
),
36-
/* Fl Fn D Sfa Cl */
37-
Lbl'-LT-'touchedAccounts'-GT-'{}(
38-
/* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Stop'Set{}()
39-
),
40-
/* Fl Fn D Sfa Cl */
41-
Lbl'-LT-'callState'-GT-'{}(
42-
/* Fl Fn D Sfa Cl */
43-
Lbl'-LT-'program'-GT-'{}(
44-
/* Fl Fn D Sfa Cl */ \dv{SortBytes{}}("")
45-
),
46-
/* Fl Fn D Sfa Cl */
47-
Lbl'-LT-'jumpDests'-GT-'{}(
48-
/* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Stop'Set{}()
49-
),
50-
/* Fl Fn D Sfa Cl */
51-
Lbl'-LT-'id'-GT-'{}(
52-
/* Fl Fn D Sfa Cl */
53-
Lbl'Stop'Account'Unds'EVM-TYPES'Unds'Account{}()
54-
),
55-
/* Fl Fn D Sfa Cl */
56-
Lbl'-LT-'caller'-GT-'{}(
57-
/* Fl Fn D Sfa Cl */
58-
Lbl'Stop'Account'Unds'EVM-TYPES'Unds'Account{}()
59-
),
60-
/* Fl Fn D Sfa Cl */
61-
Lbl'-LT-'callData'-GT-'{}(
62-
/* Fl Fn D Sfa Cl */ \dv{SortBytes{}}("")
63-
),
64-
/* Fl Fn D Sfa Cl */
65-
Lbl'-LT-'callValue'-GT-'{}(
66-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
67-
),
68-
/* Fl Fn D Sfa Cl */
69-
Lbl'-LT-'wordStack'-GT-'{}(
70-
/* Fl Fn D Sfa Cl */
71-
Lbl'Stop'WordStack'Unds'EVM-TYPES'Unds'WordStack{}()
72-
),
73-
/* Fl Fn D Sfa Cl */
74-
Lbl'-LT-'localMem'-GT-'{}(
75-
/* Fl Fn D Sfa Cl */ /* InternalMap: */ Lbl'Stop'Map{}()
76-
),
77-
/* Fl Fn D Sfa Cl */
78-
Lbl'-LT-'pc'-GT-'{}(
79-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
80-
),
81-
/* Fl Fn D Sfa Cl */
82-
Lbl'-LT-'gas'-GT-'{}(
83-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
84-
),
85-
/* Fl Fn D Sfa Cl */
86-
Lbl'-LT-'memoryUsed'-GT-'{}(
87-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
88-
),
89-
/* Fl Fn D Sfa Cl */
90-
Lbl'-LT-'callGas'-GT-'{}(
91-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
92-
),
93-
/* Fl Fn D Sfa Cl */
94-
Lbl'-LT-'static'-GT-'{}(
95-
/* Fl Fn D Sfa Cl */ \dv{SortBool{}}("false")
96-
),
97-
/* Fl Fn D Sfa Cl */
98-
Lbl'-LT-'callDepth'-GT-'{}(
99-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
100-
)
101-
),
102-
/* Fl Fn D Sfa Cl */
103-
Lbl'-LT-'substate'-GT-'{}(
104-
/* Fl Fn D Sfa Cl */
105-
Lbl'-LT-'selfDestruct'-GT-'{}(
106-
/* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Stop'Set{}()
107-
),
108-
/* Fl Fn D Sfa Cl */
109-
Lbl'-LT-'log'-GT-'{}(
110-
/* Fl Fn D Sfa Cl */
111-
/* InternalList: */ Lbl'Stop'List{}()
112-
),
113-
/* Fl Fn D Sfa Cl */
114-
Lbl'-LT-'refund'-GT-'{}(
115-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
116-
)
117-
),
118-
/* Fl Fn D Sfa Cl */
119-
Lbl'-LT-'gasPrice'-GT-'{}(
120-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
121-
),
122-
/* Fl Fn D Sfa Cl */
123-
Lbl'-LT-'origin'-GT-'{}(
124-
/* Fl Fn D Sfa Cl */
125-
Lbl'Stop'Account'Unds'EVM-TYPES'Unds'Account{}()
126-
),
127-
/* Fl Fn D Sfa Cl */
128-
Lbl'-LT-'blockhashes'-GT-'{}(
129-
/* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Stop'List{}()
130-
),
131-
/* Fl Fn D Sfa Cl */
132-
Lbl'-LT-'block'-GT-'{}(
133-
/* Fl Fn D Sfa Cl */
134-
Lbl'-LT-'previousHash'-GT-'{}(
135-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
136-
),
137-
/* Fl Fn D Sfa Cl */
138-
Lbl'-LT-'ommersHash'-GT-'{}(
139-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
140-
),
141-
/* Fl Fn D Sfa Cl */
142-
Lbl'-LT-'coinbase'-GT-'{}(
143-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
144-
),
145-
/* Fl Fn D Sfa Cl */
146-
Lbl'-LT-'stateRoot'-GT-'{}(
147-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
148-
),
149-
/* Fl Fn D Sfa Cl */
150-
Lbl'-LT-'transactionsRoot'-GT-'{}(
151-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
152-
),
153-
/* Fl Fn D Sfa Cl */
154-
Lbl'-LT-'receiptsRoot'-GT-'{}(
155-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
156-
),
157-
/* Fl Fn D Sfa Cl */
158-
Lbl'-LT-'logsBloom'-GT-'{}(
159-
/* Fl Fn D Sfa Cl */ \dv{SortBytes{}}("")
160-
),
161-
/* Fl Fn D Sfa Cl */
162-
Lbl'-LT-'difficulty'-GT-'{}(
163-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
164-
),
165-
/* Fl Fn D Sfa Cl */
166-
Lbl'-LT-'number'-GT-'{}(
167-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
168-
),
169-
/* Fl Fn D Sfa Cl */
170-
Lbl'-LT-'gasLimit'-GT-'{}(
171-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
172-
),
173-
/* Fl Fn D Sfa Cl */
174-
Lbl'-LT-'gasUsed'-GT-'{}(
175-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
176-
),
177-
/* Fl Fn D Sfa Cl */
178-
Lbl'-LT-'timestamp'-GT-'{}(
179-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
180-
),
181-
/* Fl Fn D Sfa Cl */
182-
Lbl'-LT-'extraData'-GT-'{}(
183-
/* Fl Fn D Sfa Cl */ \dv{SortBytes{}}("")
184-
),
185-
/* Fl Fn D Sfa Cl */
186-
Lbl'-LT-'mixHash'-GT-'{}(
187-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
188-
),
189-
/* Fl Fn D Sfa Cl */
190-
Lbl'-LT-'blockNonce'-GT-'{}(
191-
/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0")
192-
),
193-
/* Fl Fn D Sfa Cl */
194-
Lbl'-LT-'ommerBlockHeaders'-GT-'{}(
195-
/* Fl Fn D Sfa Cl */
196-
LblJSONList{}(
197-
/* Fl Fn D Sfa Cl */
198-
Lbl'Stop'List'LBraQuot'JSONs'QuotRBraUnds'JSONs{}()
199-
)
200-
)
201-
)
202-
),
203-
/* Fl Fn D Sfa Cl */
204-
Lbl'-LT-'network'-GT-'{}(
205-
/* Fl Fn D Sfa Cl */
206-
Lbl'-LT-'activeAccounts'-GT-'{}(
207-
/* Fl Fn D Sfa Cl */ /* InternalSet: */ Lbl'Stop'Set{}()
208-
),
209-
/* Fl Fn D Sfa Cl */
210-
Lbl'-LT-'accounts'-GT-'{}(
211-
/* Fl Fn D Sfa Cl */
212-
/* InternalMap: */ Lbl'Stop'AccountCellMap{}()
213-
),
214-
/* Fl Fn D Sfa Cl */
215-
Lbl'-LT-'txOrder'-GT-'{}(
216-
/* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Stop'List{}()
217-
),
218-
/* Fl Fn D Sfa Cl */
219-
Lbl'-LT-'txPending'-GT-'{}(
220-
/* Fl Fn D Sfa Cl */ /* InternalList: */ Lbl'Stop'List{}()
221-
),
222-
/* Fl Fn D Sfa Cl */
223-
Lbl'-LT-'messages'-GT-'{}(
224-
/* Fl Fn D Sfa Cl */
225-
/* InternalMap: */ Lbl'Stop'MessageCellMap{}()
226-
)
227-
)
228-
)
229-
),
230-
/* Fl Fn D Sfa Cl */
231-
Lbl'-LT-'generatedCounter'-GT-'{}(/* Fl Fn D Sfa Cl */ \dv{SortInt{}}("0"))
232-
)
1+
/* Fn Sfa */ \bottom{SortGeneratedTopCell{}}()

0 commit comments

Comments
 (0)