Skip to content

Commit 3bca8d7

Browse files
virgil-serbanutavirgil-serbanuta
committed
Use total versions of operators.
1 parent 204e055 commit 3bca8d7

File tree

1 file changed

+34
-33
lines changed

1 file changed

+34
-33
lines changed

‎pykwasm/src/pykwasm/kdist/wasm-semantics/kwasm-lemmas.md‎

Lines changed: 34 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ module KWASM-LEMMAS-SYMBOLIC [symbolic]
1818
imports BYTES-KORE
1919
imports INT-SYMBOLIC
2020
imports MAP-SYMBOLIC
21+
imports CEILS-SYNTAX
2122
```
2223

2324
Basic logic
@@ -54,14 +55,14 @@ These are given in pure modulus form, and in form with `#wrap`, which is modulus
5455
andBool X <Int (1 <<Int (N *Int 8))
5556
[simplification]
5657
57-
rule _X modInt 1 => 0
58+
rule _X modIntTotal 1 => 0
5859
[simplification]
5960
```
6061

6162
`modInt` selects the least non-negative representative of a congruence class modulo `N`.
6263

6364
```k
64-
rule (X modInt M) modInt N => X modInt M
65+
rule (X modIntTotal M) modIntTotal N => X modInt M
6566
requires M >Int 0
6667
andBool M <=Int N
6768
[simplification]
@@ -78,7 +79,7 @@ Since 0 <= x mod m < m <= n, (x mod m) mod n = x mod m
7879
```
7980

8081
```k
81-
rule (X modInt M) modInt N => X modInt N
82+
rule (X modIntTotal M) modIntTotal N => X modInt N
8283
requires M >Int 0
8384
andBool N >Int 0
8485
andBool M modInt N ==Int 0
@@ -104,24 +105,24 @@ x = m * q + r, for a unique q and r s.t. 0 <= r < m
104105
#### Modulus Over Addition
105106

106107
```k
107-
rule (_X *Int M +Int Y) modInt N => Y modInt N
108+
rule (_X *Int M +Int Y) modIntTotal N => Y modInt N
108109
requires M >Int 0
109110
andBool N >Int 0
110111
andBool M modInt N ==Int 0
111112
[simplification]
112113
113-
rule (Y +Int _X *Int M) modInt N => Y modInt N
114+
rule (Y +Int _X *Int M) modIntTotal N => Y modInt N
114115
requires M >Int 0
115116
andBool N >Int 0
116117
andBool M modInt N ==Int 0
117118
[simplification]
118119
119-
rule #wrap(N, (_X <<Int M) +Int Y) => #wrap(N, Y)
120+
rule #wrap(N, (_X <<IntTotal M) +Int Y) => #wrap(N, Y)
120121
requires 0 <=Int M
121122
andBool (N *Int 8) <=Int M
122123
[simplification]
123124
124-
rule #wrap(N, Y +Int (_X <<Int M)) => #wrap(N, Y)
125+
rule #wrap(N, Y +Int (_X <<IntTotal M)) => #wrap(N, Y)
125126
requires 0 <=Int M
126127
andBool (N *Int 8) <=Int M
127128
[simplification]
@@ -135,13 +136,13 @@ x * m + y mod n = x * (k * n) + y mod n = y mod n
135136
```
136137

137138
```k
138-
rule ((X modInt M) +Int Y) modInt N => (X +Int Y) modInt N
139+
rule ((X modIntTotal M) +Int Y) modIntTotal N => (X +Int Y) modInt N
139140
requires M >Int 0
140141
andBool N >Int 0
141142
andBool M modInt N ==Int 0
142143
[simplification]
143144
144-
rule (X +Int (Y modInt M)) modInt N => (X +Int Y) modInt N
145+
rule (X +Int (Y modIntTotal M)) modIntTotal N => (X +Int Y) modInt N
145146
requires M >Int 0
146147
andBool N >Int 0
147148
andBool M modInt N ==Int 0
@@ -177,45 +178,45 @@ We want K to understand what a bit-shift is.
177178
// According to domains.md, shifting by negative amounts is #False, so
178179
// all simplification rules must take that into account.
179180
180-
rule (_X <<Int N) modInt M => 0
181+
rule (_X <<IntTotal N) modIntTotal M => 0
181182
requires 0 <=Int N andBool (2 ^Int N) modInt M ==Int 0
182183
[simplification]
183184
184-
rule #wrap(M, _X <<Int N) => 0
185+
rule #wrap(M, _X <<IntTotal N) => 0
185186
requires 0 <=Int N andBool (M *Int 8) <=Int N
186187
[simplification]
187188
188-
rule (X >>Int N) => 0
189+
rule (X >>IntTotal N) => 0
189190
requires 0 <=Int N
190191
andBool 0 <=Int X
191192
andBool X <Int 2 ^Int N
192193
[simplification]
193-
rule (_X <<Int N) modInt M => 0
194+
rule (_X <<IntTotal N) modIntTotal M => 0
194195
requires 0 <=Int N
195196
andBool M <Int 2 ^Int N
196197
[simplification]
197198
198-
rule (X >>Int N) >>Int M => X >>Int (N +Int M)
199+
rule (X >>IntTotal N) >>IntTotal M => X >>Int (N +Int M)
199200
requires 0 <=Int N andBool 0 <=Int M
200201
[simplification]
201-
rule (X <<Int N) <<Int M => X <<Int (N +Int M)
202+
rule (X <<IntTotal N) <<IntTotal M => X <<Int (N +Int M)
202203
requires 0 <=Int N andBool 0 <=Int M
203204
[simplification]
204205
205-
rule (X <<Int N) >>Int M => X <<Int (N -Int M)
206+
rule (X <<IntTotal N) >>IntTotal M => X <<Int (N -Int M)
206207
requires 0 <=Int M andBool M <=Int N
207208
[simplification]
208-
rule (X <<Int N) >>Int M => X >>Int (M -Int N)
209+
rule (X <<IntTotal N) >>IntTotal M => X >>Int (M -Int N)
209210
requires 0 <=Int N andBool notBool (N >=Int M)
210211
[simplification]
211212
```
212213

213214
```k
214-
rule ((X <<Int M) +Int Y) >>Int N => (X <<Int (M -Int N)) +Int (Y >>Int N)
215+
rule ((X <<IntTotal M) +Int Y) >>IntTotal N => (X <<Int (M -Int N)) +Int (Y >>Int N)
215216
requires M >=Int N andBool N >=Int 0
216217
andBool 0 <=Int X andBool 0 <=Int Y
217218
[simplification]
218-
rule (Y +Int (X <<Int M)) >>Int N => (X <<Int (M -Int N)) +Int (Y >>Int N)
219+
rule (Y +Int (X <<IntTotal M)) >>IntTotal N => (X <<Int (M -Int N)) +Int (Y >>Int N)
219220
requires M >=Int N andBool N >=Int 0
220221
andBool 0 <=Int X andBool 0 <=Int Y
221222
[simplification]
@@ -240,14 +241,14 @@ Let x' = x << m
240241
The following rules decrease the modulus by rearranging it around a shift.
241242

242243
```k
243-
rule (X modInt POW) >>Int N => (X >>Int N) modInt (POW /Int (2 ^Int N))
244+
rule (X modIntTotal POW) >>IntTotal N => (X >>Int N) modInt (POW /Int (2 ^Int N))
244245
requires N >=Int 0
245246
andBool POW >Int 0
246247
andBool POW modInt (2 ^Int N) ==Int 0
247248
andBool 0 <=Int X
248249
[simplification]
249250
250-
rule (X <<Int N) modInt POW => (X modInt (POW /Int (2 ^Int N))) <<Int N
251+
rule (X <<IntTotal N) modIntTotal POW => (X modInt (POW /Int (2 ^Int N))) <<Int N
251252
requires N >=Int 0
252253
andBool POW >Int 0
253254
andBool POW modInt (2 ^Int N) ==Int 0
@@ -260,13 +261,13 @@ Therefore, we may as well shift first and then take the modulus, only we need to
260261
The argument for the left shift is similar.
261262

262263
```k
263-
rule (X +Int (_Y <<Int N)) modInt POW => X modInt POW
264+
rule (X +Int (_Y <<IntTotal N)) modIntTotal POW => X modInt POW
264265
requires N >=Int 0
265266
andBool POW >Int 0
266267
andBool (2 ^Int N) modInt POW ==Int 0
267268
[simplification]
268269
269-
rule ((_Y <<Int N) +Int X) modInt POW => X modInt POW
270+
rule ((_Y <<IntTotal N) +Int X) modIntTotal POW => X modInt POW
270271
requires N >=Int 0
271272
andBool POW >Int 0
272273
andBool (2 ^Int N) modInt POW ==Int 0
@@ -281,7 +282,7 @@ When reasoning about `#chop`, it's often the case that the precondition to the p
281282
In this case, it's simpler (and safe) to simply discard the `#chop`, instead of evaluating it.
282283

283284
```k
284-
rule X modInt #pow(ITYPE) => #unsigned(ITYPE, X)
285+
rule X modIntTotal #pow(ITYPE) => #unsigned(ITYPE, X)
285286
requires #inSignedRange (ITYPE, X)
286287
[simplification]
287288
@@ -309,16 +310,16 @@ Memory
309310
Bounds on `#getRange`:
310311

311312
```k
312-
rule 0 <=Int #getRange(_, _, _) => true [simplification]
313-
rule 0 <=Int VAL <<Int SHIFT => true requires 0 <=Int VAL andBool 0 <=Int SHIFT [simplification]
314-
rule 0 <=Int VAL1 +Int VAL2 => true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification]
313+
rule 0 <=Int #getRange(_, _, _) => true [simplification]
314+
rule 0 <=Int VAL <<IntTotal SHIFT => true requires 0 <=Int VAL andBool 0 <=Int SHIFT [simplification]
315+
rule 0 <=Int VAL1 +Int VAL2 => true requires 0 <=Int VAL1 andBool 0 <=Int VAL2 [simplification]
315316
316-
rule #getRange(_, _, WIDTH) <Int MAX => true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification]
317-
rule #getRange(_, _, WIDTH) <<Int SHIFT <Int MAX => true
317+
rule #getRange(_, _, WIDTH) <Int MAX => true requires 2 ^Int (8 *Int WIDTH) <=Int MAX [simplification]
318+
rule #getRange(_, _, WIDTH) <<IntTotal SHIFT <Int MAX => true
318319
requires 2 ^Int ((8 *Int WIDTH) +Int SHIFT) <=Int MAX
319320
andBool 0 <=Int SHIFT
320321
[simplification]
321-
rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) <<Int SHIFT) #as VAL2) <Int MAX => true
322+
rule (#getRange(_, _, WIDTH1) #as VAL1) +Int ((#getRange(_, _, WIDTH2) <<IntTotal SHIFT) #as VAL2) <Int MAX => true
322323
requires VAL1 <Int MAX
323324
andBool VAL2 <Int MAX
324325
andBool 0 <=Int SHIFT
@@ -338,13 +339,13 @@ Bounds on `#getRange`:
338339
Arithmetic over `#getRange`:
339340

340341
```k
341-
rule #getRange(BM, ADDR, WIDTH) >>Int SHIFT => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) >>Int (SHIFT -Int 8)
342+
rule #getRange(BM, ADDR, WIDTH) >>IntTotal SHIFT => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) >>Int (SHIFT -Int 8)
342343
requires 0 <=Int ADDR
343344
andBool 0 <Int WIDTH
344345
andBool 8 <=Int SHIFT
345346
[simplification]
346347
347-
rule #getRange(BM, ADDR, WIDTH) modInt MAX => #getRange(BM, ADDR, WIDTH -Int 1) modInt MAX
348+
rule #getRange(BM, ADDR, WIDTH) modIntTotal MAX => #getRange(BM, ADDR, WIDTH -Int 1) modInt MAX
348349
requires 0 <Int MAX andBool 0 <Int WIDTH
349350
andBool 2 ^Int (8 *Int (WIDTH -Int 1)) modInt MAX ==Int 0
350351
[simplification]
@@ -368,7 +369,7 @@ Arithmetic over `#getRange`:
368369

369370
```k
370371
rule #setRange(BM, ADDR, #getRange(BM, ADDR, WIDTH), WIDTH) => BM [simplification]
371-
rule #setRange(BM, ADDR, (#getRange(_, _, WIDTH1) #as VAL1) +Int (VAL2 <<Int SHIFT), WIDTH)
372+
rule #setRange(BM, ADDR, (#getRange(_, _, WIDTH1) #as VAL1) +Int (VAL2 <<IntTotal SHIFT), WIDTH)
372373
=> #setRange(#setRange(BM, ADDR, VAL1, minInt(WIDTH1, WIDTH)), ADDR +Int WIDTH1, VAL2, WIDTH -Int WIDTH1)
373374
requires 0 <=Int ADDR
374375
andBool 0 <=Int SHIFT

0 commit comments

Comments
 (0)