forked from runtimeverification/verified-smart-contracts
-
Notifications
You must be signed in to change notification settings - Fork 0
/
lemmas.k
570 lines (395 loc) · 24.3 KB
/
lemmas.k
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
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
requires "edsl.k"
// NOTE: This module includes all lemmas (except assosiativity ones) in both lemmas.md and evm-data-map-symbolic.k
module LEMMAS
imports K-REFLECTION
imports EDSL
//////////////////////////
// Macros
//////////////////////////
syntax Int ::= "pow24"
| "pow32"
| "pow40"
| "pow48"
| "pow56"
| "pow64"
rule pow24 => 16777216 [macro]
rule pow32 => 4294967296 [macro]
rule pow40 => 1099511627776 [macro]
rule pow48 => 281474976710656 [macro]
rule pow56 => 72057594037927936 [macro]
rule pow64 => 18446744073709551616 [macro]
syntax Bool ::= #regularAddress(Schedule, Int)
rule #regularAddress(SCHEDULE, X) => X >Int 0 andBool (notBool X in #precompiledAccounts(SCHEDULE)) [macro]
// normalization
rule X <=Int maxUInt256 => X <Int pow256
rule X <=Int maxUInt160 => X <Int pow160
rule X <=Int 255 => X <Int 256
rule X >Int Y => Y <Int X
rule X >=Int Y => Y <=Int X
rule notBool (X <Int Y) => Y <=Int X
rule notBool (X <=Int Y) => Y <Int X
//orienting symbolic term to be first, converting -Int to +Int for concrete values.
rule I +Int B => B +Int I when #isConcrete(I) andBool notBool #isConcrete(B)
rule A -Int I => A +Int (0 -Int I) when notBool #isConcrete(A) andBool #isConcrete(I)
// eDSL
rule #hashedLocation("Array", BASE, OFFSET OFFSETS) => #hashedLocation("Array", keccakIntList(BASE) +Word OFFSET, OFFSETS)
//////////////////////////
// Range Predicates
//////////////////////////
rule 0 <=Int (X modInt Y) => true
rule (X modInt Y) <Int Y => true requires Y >Int 0
rule 0 <=Int 2 ^Int X => true
rule 2 ^Int X <Int pow256 => true requires X <Int 256
rule 0 <=Int X &Int Y => true requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
rule X &Int Y <Int pow256 => true requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
rule 0 <=Int X |Int Y => true requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
rule X |Int Y <Int pow256 => true requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
rule 0 <=Int #blockhash(_, _, _, _) => true
rule #blockhash(_, _, _, _) <Int pow256 => true
rule 0 <=Int #bufElm(_, _) => true
rule #bufElm(_, _) <Int 256 => true
rule #bufElm(_, _) <Int pow256 => true
rule 0 <=Int bool2Word(_) => true
rule bool2Word(_) <Int 2 => true
rule bool2Word(_) <Int 256 => true
rule bool2Word(_) <Int pow256 => true
rule 0 <=Int X xorInt maxUInt256 => true requires #rangeUInt(256, X)
rule X xorInt maxUInt256 <Int pow256 => true requires #rangeUInt(256, X)
rule 0 <=Int #asWord(WS) => true
rule #asWord(WS) <Int pow256 => true
rule 0 <=Int chop(V) => true
rule chop(V) <Int pow256 => true
rule 0 <=Int keccak(V) => true
rule keccak(V) <Int pow256 => true
rule 0 <=Int keccakIntList(_) => true
rule keccakIntList(_) <Int pow256 => true
rule 0 <=Int #sha256(_) => true
rule #sha256(_) <Int pow256 => true
syntax Bool ::= isStorage(Map) [function]
rule 0 <=Int select(M, _) => true requires isStorage(M)
rule select(M, _) <Int pow256 => true requires isStorage(M)
//////////////////////////
// Arithmetic
//////////////////////////
// TODO: move to builtin
rule N +Int 0 => N
rule N -Int 0 => N
rule N -Int N => 0
rule 1 *Int N => N
rule N *Int 1 => N
rule 0 *Int _ => 0
rule _ *Int 0 => 0
rule N /Int 1 => N
rule 0 |Int N => N
rule N |Int 0 => N
rule N |Int N => N
rule 0 &Int N => 0
rule N &Int 0 => 0
rule N &Int N => N
rule (A +Int I2) +Int I3 => A +Int (I2 +Int I3) when notBool #isConcrete(A) andBool #isConcrete(I2) andBool #isConcrete(I3)
rule A +Int (I -Int A) => I when notBool #isConcrete(A) andBool #isConcrete(I)
rule 0 <=Int X +Int Y => true requires 0 <=Int X andBool 0 <=Int Y
//
// nonlinear
//
rule chop(I) => I requires 0 <=Int I andBool I <Int pow256
// safeMath mul check c / a == b where c == a * b
rule (X *Int Y) /Int X => Y requires X =/=Int 0
rule chop(X *Int Y) /Int X ==K Y => false requires X =/=Int 0 andBool pow256 <=Int X *Int Y
rule chop((ADDR &Int maxUInt160) modInt pow160) => ADDR
requires #rangeAddress(ADDR)
rule 2 ^%Int X pow256 => 2 ^Int X
requires 0 <=Int X andBool X <Int 256
rule X modInt Y => X
requires 0 <=Int X andBool X <Int Y
rule ((X *Int Y) /Int Z) /Int Y => X /Int Z
requires Y =/=Int 0
rule (X /Int 32) *Int 32 => X requires X modInt 32 ==Int 0
rule #ceil32(X) => X requires X modInt 32 ==Int 0
rule X <=Int #ceil32(X) => true
requires X >=Int 0
rule (X +Int 31) /Int 32 *Int 32 => #ceil32(X)
rule (31 +Int X) /Int 32 *Int 32 => #ceil32(X)
//
// bitwise
//
// 0xffff...f &Int N = N
rule MASK &Int N => N requires MASK ==Int (2 ^Int (log2Int(MASK) +Int 1)) -Int 1 // MASK = 0xffff...f
andBool 0 <=Int N andBool N <=Int MASK
// N &Int 0xffff...f = N
rule N &Int MASK => N requires MASK ==Int (2 ^Int (log2Int(MASK) +Int 1)) -Int 1 // MASK = 0xffff...f
andBool 0 <=Int N andBool N <=Int MASK
// 0xff..ff00..00 (16 1's followed by 240 0's)
rule 115790322390251417039241401711187164934754157181743688420499462401711837020160 &Int #asWord(WS1 ++ WS2)
=> #asWord(WS1 ++ #buf(30, 0))
requires #sizeWordStack(WS1) ==Int 2
andBool #sizeWordStack(WS2) ==Int 30
// x &Int (NOT 31)
rule X &Int 115792089237316195423570985008687907853269984665640564039457584007913129639904 => (X /Int 32) *Int 32 requires 0 <=Int X
// 2^256 - 2^160 = 0xff..ff00..00 (96 1's followed by 160 0's)
rule 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int ADDR => 0
requires #rangeAddress(ADDR)
rule #asWord(WS) &Int maxUInt256 => #asWord(WS)
//
// boolean
//
rule bool2Word(A) |Int bool2Word(B) => bool2Word(A orBool B)
rule bool2Word(A) &Int bool2Word(B) => bool2Word(A andBool B)
rule 1 |Int bool2Word(B) => 1
rule 1 &Int bool2Word(B) => bool2Word(B)
rule bool2Word(B) |Int 1 => 1
rule bool2Word(B) &Int 1 => bool2Word(B)
rule bool2Word(A) ==K 0 => notBool(A)
rule bool2Word(A) ==K 1 => A
rule bool2Word(A) =/=K 0 => A
rule bool2Word(A) =/=K 1 => notBool(A)
rule chop(bool2Word(B)) => bool2Word(B)
//////////////////////////
// Buffer Abstraction
//////////////////////////
syntax WordStack ::= #bufSeg ( WordStack , Int , Int ) [function, smtlib(bufSeg)] // BUFFER, START, WIDTH
syntax Int ::= #bufElm ( WordStack , Int ) [function] // BUFFER, INDEX
syntax Bool ::= #isBuf ( WordStack ) [function]
rule #isBuf(#buf(_,_)) => true
rule #isBuf(#bufSeg(_,_,_)) => true
syntax Bool ::= #isTake ( WordStack ) [function]
rule #isTake(#take(_,_)) => true
rule #isTake(#takeAux(_,_,_)) => true
rule #asWord(#buf(SIZE, DATA)) => DATA requires SIZE <=Int 32 andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) andBool #isConcrete(SIZE)
rule #buf(SIZE, _) => .WordStack requires SIZE ==Int 0
rule #bufSeg(_, _, WIDTH) => .WordStack requires WIDTH ==Int 0
rule #bufSeg(WS, START, WIDTH) => WS requires START ==Int 0 andBool WIDTH ==Int #sizeWordStack(WS)
rule #bufSeg(#bufSeg(BUF, START0, WIDTH0), START, WIDTH)
=> #bufSeg(BUF, START0 +Int START, WIDTH)
requires 0 <=Int START andBool START +Int WIDTH <=Int WIDTH0
rule #bufElm(#bufSeg(BUF, START0, WIDTH0), INDEX)
=> #bufElm(BUF, START0 +Int INDEX)
requires 0 <=Int INDEX andBool INDEX <Int WIDTH0
// Auxiliary function to make rules compatible with simplification `rule WS ++ .WordStack => WS`
syntax WordStack ::= #takeAux ( Int , WordStack , WordStack ) [function]
// ------------------------------------------------------------------------
rule #take(N, BUF ) => #takeAux(N, BUF, .WordStack) requires #isBuf(BUF)
rule #take(N, BUF ++ WS) => #takeAux(N, BUF, WS) requires #isBuf(BUF)
rule #takeAux(N, BUF, WS) => #bufSeg(BUF, 0, N) requires 0 <=Int N andBool N <=Int #sizeBuffer(BUF)
rule #takeAux(N, BUF, WS) => BUF ++ #take(N -Int #sizeBuffer(BUF), WS) requires N >Int #sizeBuffer(BUF)
rule #take(N, .WordStack) => #buf(N, 0) requires notBool #isConcrete(N)
syntax WordStack ::= #dropAux ( Int , WordStack , WordStack ) [function]
// ------------------------------------------------------------------------
rule #drop(N, BUF ) => #dropAux(N, BUF, .WordStack) requires #isBuf(BUF)
rule #drop(N, BUF ++ WS) => #dropAux(N, BUF, WS) requires #isBuf(BUF)
rule #dropAux(N, BUF, WS) => #bufSeg(BUF, N, #sizeBuffer(BUF) -Int N) ++ WS requires 0 <=Int N andBool N <=Int #sizeBuffer(BUF)
rule #dropAux(N, BUF, WS) => #drop(N -Int #sizeBuffer(BUF), WS) requires N >=Int #sizeBuffer(BUF)
syntax Int ::= #getElmAux ( WordStack , WordStack , Int ) [function]
// --------------------------------------------------------------------
rule (BUF ) [ N ] => #getElmAux(BUF, .WordStack, N) requires #isBuf(BUF)
rule (BUF ++ WS) [ N ] => #getElmAux(BUF, WS, N) requires #isBuf(BUF)
rule #getElmAux(BUF, WS, N) => #bufElm(BUF, N) requires 0 <=Int N andBool N <Int #sizeBuffer(BUF)
rule #getElmAux(BUF, WS, N) => WS [ N -Int #sizeBuffer(BUF) ] requires N >=Int #sizeBuffer(BUF)
rule #sizeWordStack ( BUF ++ WS, SIZE ) => #sizeWordStack(WS, SIZE +Int #sizeBuffer(BUF)) requires #isBuf(BUF) orBool #isTake(BUF)
rule #sizeWordStack ( BUF , SIZE ) => SIZE +Int #sizeBuffer(BUF) requires #isBuf(BUF) orBool #isTake(BUF)
syntax Int ::= #sizeBuffer ( WordStack ) [function]
// ---------------------------------------------------
rule #sizeBuffer ( #buf(N,_) ) => N
rule #sizeBuffer ( #bufSeg(_,_,N) ) => N
rule #sizeBuffer ( #take(N,_) ) => N
rule #sizeBuffer ( #takeAux(N,_,_) ) => N
//
// simplification
//
rule ( WS1 ++ WS2 ) ++ WS3 => WS1 ++ ( WS2 ++ WS3 )
rule WS ++ .WordStack => WS
// rule #asWord( 0 : W1 : WS => W1 : WS )
rule #asWord( 0 : WS => WS )
rule #padToWidth(32, #asByteStack(V)) => #buf(32, V)
requires 0 <=Int V andBool V <Int pow256
rule #buf(N, #asWord(WS)) => WS
requires #noOverflow(WS) andBool N ==Int #sizeWordStack(WS)
rule #buf(32, #asWord(WS)) => WS requires #sizeWordStack(WS) ==Int 32
rule #buf(32, #asWord(#bufSeg(BUF, START, WIDTH))) => #bufSeg(BUF, START +Int WIDTH -Int 32, 32) requires WIDTH >=Int 32
rule #asWord(#bufSeg(BUF, START, WIDTH)) &Int 255 => #asWord(#bufSeg(BUF, START +Int WIDTH -Int 1, 1)) requires WIDTH >=Int 1
rule 255 &Int #asWord(#bufSeg(BUF, START, WIDTH)) => #asWord(#bufSeg(BUF, START +Int WIDTH -Int 1, 1)) requires WIDTH >=Int 1
rule #bufSeg(BUF, START, 1) => #bufElm(BUF, START) : .WordStack
rule #asWord(#bufElm(BUF, INDEX) : .WordStack) => #bufElm(BUF, INDEX)
rule #buf(SIZE, DATA) => #padToWidth(SIZE, #asByteStack(DATA)) requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) [concrete]
rule #asWord(WS0 ++ #buf(MASKWIDTH0, 0)) |Int #asWord(#buf(MASKWIDHT1, 0) ++ WS1)
=> #asWord(WS0 ++ WS1)
requires #sizeWordStack(WS0) +Int MASKWIDTH0 ==Int 32
andBool #sizeWordStack(WS0) ==Int MASKWIDHT1
andBool MASKWIDTH0 ==Int #sizeWordStack(WS1)
rule #noOverflowAux(BUF) => true requires #isBuf(BUF) orBool #isTake(BUF)
rule #noOverflowAux(WS1 ++ WS2) => #noOverflowAux(WS1) andBool #noOverflowAux(WS2)
rule #bufSeg(BUF, S0, W0) ++ #bufSeg(BUF, S1, W1) => #bufSeg(BUF, S0, W0 +Int W1)
requires S1 ==Int S0 +Int W0
rule #bufSeg(BUF, S0, W0) ++ (#bufSeg(BUF, S1, W1) ++ WS) => #bufSeg(BUF, S0, W0 +Int W1) ++ WS
requires S1 ==Int S0 +Int W0
rule 0 <=Int #sizeWordStack ( _ , _ ) => true [smt-lemma]
rule #sizeWordStack(WS, N) <Int SIZE => #sizeWordStack(WS, 0) +Int N <Int SIZE requires N =/=Int 0
rule SIZELIMIT <Int #sizeWordStack(WS, N) +Int DELTA => SIZELIMIT <Int (#sizeWordStack(WS, 0) +Int N) +Int DELTA requires N =/=Int 0
rule SIZELIMIT <Int #sizeWordStack(WS, N) => SIZELIMIT <Int #sizeWordStack(WS, 0) +Int N requires N =/=Int 0
rule #sizeWordStack(WS, N) <=Int SIZE => #sizeWordStack(WS, 0) +Int N <=Int SIZE requires N =/=Int 0
rule #sizeWordStack(selectRange(_, _, WIDTH), SIZE) => SIZE +Int WIDTH
rule #take(#sizeWordStack(WS, 0), WS) => WS
rule #bufSeg(BUF, N, WIDTH) => BUF requires WIDTH ==Int #sizeBuffer(BUF)
rule selectRange(storeRange(M, START1, WIDTH1, BUF), START2, WIDTH2) => BUF
requires START1 ==Int START2 andBool WIDTH1 ==Int WIDTH2
/*
// Merge
rule storeRange(storeRange(M, MS0, MW0, #bufSeg(BUF, BS0, BW0)), MS1, MW1, #bufSeg(BUF, BS1, BW1))
=> storeRange(M, MS0, MW0 +Int MW1, #bufSeg(BUF, BS0, MW0 +Int MW1))
requires #isBuf(BUF) andBool MW0 ==Int BW0 andBool MW1 ==Int BW1
andBool MS1 ==Int MS0 +Int MW0 andBool BS1 ==Int BS0 +Int BW0
*/
syntax Bool ::= #noOverflow ( WordStack ) [function]
| #noOverflowAux ( WordStack ) [function]
// -------------------------------------------------------
rule #noOverflow(WS) => #sizeWordStack(WS) <=Int 32 andBool #noOverflowAux(WS)
rule #noOverflowAux(W : WS) => 0 <=Int W andBool W <Int 256 andBool #noOverflowAux(WS)
rule #noOverflowAux(.WordStack) => true
//////////////////////////
// Map
//////////////////////////
syntax Map ::= store ( Map , Int , Int ) [function, smtlib(storeInt) ]
syntax Int ::= select ( Map , Int ) [function, smtlib(selectInt)]
// -----------------------------------------------------------------------
rule select(store(M, K0, V), K) => V requires K0 ==Int K
rule select(store(M, K0, V), K) => select(M, K) requires K0 =/=Int K
syntax Map ::= storeRange ( Map , Int , Int , WordStack ) [function, smtlib(storeRange) ]
syntax WordStack ::= selectRange ( Map , Int , Int ) [function, smtlib(selectRange)]
// ------------------------------------------------------------------------------------------------
rule select(storeRange(M, START, WIDTH, WS), K) => WS[K -Int START] requires START <=Int K andBool K <Int START +Int WIDTH
rule select(storeRange(M, START, WIDTH, WS), K) => select(M, K) requires notBool (START <=Int K andBool K <Int START +Int WIDTH)
rule selectRange(store(M, K0, V), START, WIDTH) => selectRange(M, START, WIDTH) requires ( K0 <Int START orBool START +Int WIDTH <=Int K0 ) // no overlap
// included: [START0..[START..END]..END0]
rule selectRange(storeRange(M, START0, WIDTH0, WS), START, WIDTH) => WS [ START -Int START0 .. WIDTH ]
requires START0 <=Int START andBool START +Int WIDTH <=Int START0 +Int WIDTH0
// no overlap: [START..END]..[START0..END0] or [START0..END0]..[START..END]
rule selectRange(storeRange(M, START0, WIDTH0, WS), START, WIDTH) => selectRange(M, START, WIDTH)
requires ( (START +Int WIDTH) <=Int START0 orBool (START0 +Int WIDTH0) <=Int START )
// left margin: [START..(START0..END]..END0) or [START..(START0..END0)..END]
rule selectRange(storeRange(M, START0, WIDTH0, WS), START, WIDTH) => selectRange(M, START, START0 -Int START)
++ selectRange(storeRange(M, START0, WIDTH0, WS), START0, (START +Int WIDTH) -Int START0)
requires START <Int START0 andBool START0 <Int START +Int WIDTH
andBool WIDTH0 >=Int 1 // to avoid unnecessary split
// right margin: (START0..[START..END0)..END] or [START..(START0..END0)..END]
rule selectRange(storeRange(M, START0, WIDTH0, WS), START, WIDTH) => selectRange(storeRange(M, START0, WIDTH0, WS), START, (START0 +Int WIDTH0) -Int START)
++ selectRange(M, START0 +Int WIDTH0, (START +Int WIDTH) -Int (START0 +Int WIDTH0))
requires START <Int START0 +Int WIDTH0 andBool START0 +Int WIDTH0 <Int START +Int WIDTH
andBool WIDTH0 >=Int 1 // to avoid unnecessary split
// simplification
rule store(M, K, select(M, K)) => M
// TODO: check validity: i.e., WS ==K .WordStack
rule storeRange(M, _, WIDTH, _) => M requires WIDTH ==Int 0
rule selectRange(M, _, WIDTH) => .WordStack requires WIDTH ==Int 0
// lifting
rule #lookup(M, K:Int) => select(M, K) requires notBool (#isConcrete(M) andBool #isConcrete(K))
rule M:Map [ K:Int <- V:Int ] => store(M, K, V) requires notBool (#isConcrete(M) andBool #isConcrete(K) andBool #isConcrete(V))
rule #range(M, START, WIDTH) => selectRange(M, START, WIDTH) requires notBool (#isConcrete(M) andBool #isConcrete(START) andBool #isConcrete(WIDTH))
rule M [ START := WS ] => storeRange(M, START, #sizeWordStack(WS), WS) requires notBool (#isConcrete(M) andBool #isConcrete(START) andBool #isConcrete(WS))
// once it gets down to the concrete map, return to the corresponding function
// shouldn't have the infinite rule application
rule select(M, K) => #lookup(M, K) [concrete]
rule selectRange(M, START, WIDTH) => #range(M, START, WIDTH) [concrete]
// equalities
syntax Bool ::= Map "==IMap" Map [function, smtlib(=)]
syntax Bool ::= Map "==IMap" Map "except" Set [function]
// --------------------------------------------------------
rule store(M1, K, _) ==IMap M2 except Ks
=> M1 ==IMap M2 except Ks
requires K in Ks
rule M1 ==IMap store(M2, K, _) except Ks
=> M1 ==IMap M2 except Ks
requires K in Ks
rule M1 ==IMap M2 except _ => true
requires M1 ==K M2 // structural equality
syntax Set ::= keys(Map) [function]
rule K1 in keys(store(M, K2, _)) => true requires K1 ==Int K2
rule K1 in keys(store(M, K2, _)) => K1 in keys(M) requires K1 =/=Int K2
// in-place update
// store
rule store(store(M, K0, V0), K1, V1) => store(M, K0, V1)
requires K0 ==Int K1
rule store(store(M, K0, V0), K1, V1) => store(store(M, K1, V1), K0, V0)
requires K0 =/=Int K1 andBool K1 in keys(M)
// storeRange
rule storeRange(storeRange(M, K0, W0, V0), K1, W1, V1) => storeRange(M, K0, W0, V1)
requires range(K0, W0) ==Range range(K1, W1)
rule storeRange(storeRange(M, K0, W0, V0), K1, W1, V1) => storeRange(storeRange(M, K1, W1, V1), K0, W0, V0)
requires range(K0, W0) <>Range range(K1, W1)
andBool range(K1, W1) in keys(M)
rule storeRange(store(M, K0, V0), K1, W1, V1) => store(storeRange(M, K1, W1, V1), K0, V0)
requires range(K0, 1) <>Range range(K1, W1) andBool range(K1, W1) in keys(M)
rule store(storeRange(M, K0, W0, V0), K1, V1) => storeRange(store(M, K1, V1), K0, W0, V0)
requires range(K0, W0) <>Range range(K1, 1) andBool K1 in keys(M)
syntax Range ::= range(Int, Int)
rule range(K1, W1) in keys(storeRange(M, K2, W2, _)) => true requires range(K1, W1) ==Range range(K2, W2)
rule range(K1, W1) in keys(storeRange(M, K2, W2, _)) => range(K1, W1) in keys(M) requires range(K1, W1) <>Range range(K2, W2)
rule range(K1, W1) in keys(store (M, K2, _)) => range(K1, W1) in keys(M) requires range(K1, W1) <>Range range(K2, 1)
rule K1 in keys(storeRange(M, K2, W2, _)) => K1 in keys(M) requires range(K1, 1) <>Range range(K2, W2)
syntax Bool ::= Range "==Range" Range [function]
| Range "<>Range" Range [function]
rule range(K1, W1) ==Range range(K2, W2) => K1 ==Int K2 andBool W1 ==Int W2
rule range(K1, W1) <>Range range(K2, W2) => K1 +Int W1 <=Int K2 orBool K2 +Int W2 <=Int K1
//////////////////////////
// Hash Abstraction
//////////////////////////
// sha256
syntax Int ::= #sha256 ( WordStack ) [function, smtlib(sha256)]
rule #sha256(DATA) => #asWord(#parseHexBytes(Sha256(#unparseByteStack(DATA)))) [concrete]
//////////////////////////
// Gas Abstraction
//////////////////////////
// see also abstract-semantics.k
syntax Int ::= #symGas(Int, Int, Int, List, Int) [function]
syntax Int ::= #symMem(Int, Set) [function]
/* Definition
rule #symGas(INIT, LB, UB, S, MU) => INIT - [LB, UB] - sum(S) - MU
rule #symMem(N, S) => maxInt(N, maxIntSet(S)) up/Int 32
*/
syntax Int ::= Int "-Gas" Int [function]
syntax Int ::= Int "+Gas" Int [function]
// interval abstraction -- both bounds must be concrete
syntax Int ::= #itv(Int, Int) [function]
syntax Int ::= #makeItv(Int, Int) [function]
rule #makeItv(X1, X2) => #itv(X1, X2) requires X1 <Int X2 andBool #isConcrete(X1) andBool #isConcrete(X2)
rule #makeItv(X1, X2) => X1 requires X1 ==Int X2 andBool #isConcrete(X1) andBool #isConcrete(X2)
// #memoryUsageUpdate
rule #memoryUsageUpdate(#symMem(MU, MUS), START, WIDTH) => #symMem(maxInt(MU, START +Int WIDTH), MUS)
requires #isConcrete(MU) andBool #isConcrete(START) andBool #isConcrete(WIDTH)
rule #memoryUsageUpdate(#symMem(MU, MUS), START, WIDTH) => #symMem(MU, SetItem(START +Int WIDTH) MUS)
requires notBool (#isConcrete(START) andBool #isConcrete(WIDTH))
rule #memoryUsageUpdate( MU, START, WIDTH) => #symMem(MU, SetItem(START +Int WIDTH) .Set)
requires #isConcrete(MU) andBool notBool (#isConcrete(START) andBool #isConcrete(WIDTH))
// deductGas
rule #symGas(I, LB, UB, S, CMEM) -Gas G => #symGas(I, LB +Int G, UB +Int G, S, CMEM)
requires #isConcrete(G)
rule #symGas(I, LB, UB, S, CMEM) -Gas #itv(LB', UB') => #symGas(I, LB +Int LB', UB +Int UB', S, CMEM)
rule #symGas(I, LB, UB, S, CMEM) -Gas G => #symGas(I, LB, UB, ListItem(G) S, CMEM)
requires (notBool #isConcrete(G)) andBool #getKLabelString(G) =/=String "#itv" andBool #getKLabelString(G) =/=String "_+Int_"
rule G -Gas (G1 +Int G2) => (G -Gas G1) -Gas G2
// refund
rule #symGas(X, LB, UB, ListItem(C) S, CMEM) +Gas #symGas(CGASCAP, LB', UB', S', CMEM')
=> #symGas(X, LB +Int LB', UB +Int UB', S' S, CMEM) -Gas CMEM'
requires C ==K CGASCAP
andBool isPositiveGas(#symGas(CGASCAP, LB', UB', S', CMEM'))
rule #symGas(X, LB, UB, ListItem(C) S, CMEM) +Gas #symGas(CGASCAP +Int CCALLSTIPEND, LB', UB', S', CMEM')
=> #symGas(X +Int CCALLSTIPEND, LB +Int LB', UB +Int UB', S' S, CMEM) -Gas CMEM'
requires C ==K CGASCAP
andBool isPositiveGas(#symGas(CGASCAP +Int CCALLSTIPEND, LB', UB', S', CMEM'))
syntax Bool ::= isPositiveGas(Int) [function]
syntax Bool ::= isInitGas(Int) [function]
// call with constant gas (particularly for precompiled contract calls)
rule isPositiveGas(#symGas(Cgascap(_, G, #symGas(IG, _, _, _, _), _), _, UB, .List, 0)) => G >=Int UB
requires isInitGas(IG) andBool #isConcrete(G) andBool #isConcrete(UB)
rule isPositiveGas(#symGas(Cgascap(_, G, #symGas(IG, _, _, _, _), _) +Int CCALLSTIPEND, _, UB, .List, 0)) => G +Int CCALLSTIPEND >=Int UB
requires isInitGas(IG) andBool #isConcrete(G) andBool #isConcrete(UB) andBool #isConcrete(CCALLSTIPEND)
// call with all available gas
rule isPositiveGas(#symGas(Cgascap(_, #symGas(IG, _, _, _, _), _, _), _, _, _, _)) => true
requires isInitGas(IG)
rule isPositiveGas(#symGas(Cgascap(_, #symGas(IG, _, _, _, _), _, _) +Int _, _, _, _, _)) => true
requires isInitGas(IG)
// Cs*
rule Csstore(SCHED, NEW, CURR, ORIG) => #makeItv(Gsstorereset < SCHED >, Gsstoreset < SCHED >)
requires #isConcrete(SCHED)
andBool notBool ( #isConcrete(NEW) andBool #isConcrete(CURR) )
andBool notBool Ghasdirtysstore << SCHED >>
endmodule