Skip to content

Commit 8b17c66

Browse files
virgil-serbanutavirgil-serbanuta
committed
Int simplification lemmas
1 parent 7d71631 commit 8b17c66

File tree

4 files changed

+402
-0
lines changed

4 files changed

+402
-0
lines changed

‎pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/arithmetic-normalization.md‎

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
Arithmetic normalization
2+
========================
3+
4+
The normal form of an arithmetic expression is less well defined.
5+
6+
* there are no '-' operations, `A +Int -1 *Int B` is used instead of
7+
`A -Int B
8+
* Addition is grouped to the left, i.e.,
9+
`((..((A +Int B) +Int C) +Int ...) +Int Z)`
10+
* Only the last element of an addition is concrete, i.e. `(A +Int B) +Int 7`
11+
is normal, `(A +Int 7) +Int 8` and `(A +Int 7) +Int C` are not.
12+
* Multiplication is grouped to the right, i.e.,
13+
`(Z *Int (... *Int (C *Int (A *Int B)) ...))`
14+
* Only the fist element of multiplication is concrete, i.e., `7 *Int (A *Int B)`
15+
is normal, `8 *Int (7 *Int A)` and `C *Int (7*Int B)` are not.
16+
* Multiplication with constants is always distributed, i.e.,
17+
`7 *Int A +Int 7 *Int B` is normal, `7 *Int (A +Int B)` is not.
18+
* (Not fully enforced): Constants multiplied with the same symbolic term, then
19+
added, are merged, i.e., `(7 *Int A +Int B) +Int 8 *Int A` is not normal and
20+
will be transformed to `15 *Int A +Int B`
21+
```k
22+
module WASM-INT-ARITHMETIC-NORMALIZATION
23+
imports INT
24+
25+
// The rules below complement the ones in INT-KORE
26+
27+
```
28+
-Int elimination
29+
----------------
30+
```k
31+
32+
rule X -Int Y => X +Int (-1 *Int Y) [simplification]
33+
34+
```
35+
+Int
36+
----
37+
38+
* associativity
39+
```k
40+
rule X +Int (Y +Int Z) => (X +Int Y) +Int Z [simplification]
41+
42+
```
43+
* constants
44+
```k
45+
rule I +Int X => X +Int I [simplification, symbolic(X), concrete(I)]
46+
rule (X +Int I) +Int Y => (X +Int Y) +Int I [simplification, symbolic(X, Y), concrete(I)]
47+
```
48+
*Int
49+
----
50+
51+
* associativity
52+
```k
53+
rule (X *Int Y) *Int Z => X *Int (Y *Int Z) [simplification]
54+
55+
```
56+
* constants
57+
```k
58+
rule X *Int I => I *Int X [simplification, symbolic(X), concrete(I)]
59+
rule X *Int (I *Int Y) => I *Int (X *Int Y) [simplification, symbolic(X, Y), concrete(I)]
60+
rule I1 *Int (I2 *Int X) => (I1 *Int I2) *Int X [simplification, symbolic(X), concrete(I1, I2)]
61+
62+
rule 1 *Int X => X [simplification]
63+
rule 0 *Int _ => 0 [simplification]
64+
65+
```
66+
Distributivity for *Int and +Int
67+
--------------------------------
68+
69+
* Multiplication with constants
70+
```k
71+
rule I *Int (X +Int Y) => I *Int X +Int I *Int Y
72+
[simplification, symbolic(X), concrete(I)]
73+
rule I *Int (X +Int Y) => I *Int X +Int I *Int Y
74+
[simplification, symbolic(Y), concrete(I)]
75+
```
76+
* Reverse distributivity for different-constants * same-term.
77+
```k
78+
// It would be really nice if the backend would check the equality for the
79+
// two occurrences of X by matching. The next best option is to make these
80+
// rules low-priority, so they are applied only after the formula has already
81+
// stabilized (including normalization).
82+
rule X +Int X => 2 *Int X [simplification(200)]
83+
rule X +Int I *Int X => (1 +Int I) *Int X [simplification(200), concrete(I)]
84+
rule I *Int X +Int X => (1 +Int I) *Int X [simplification(200), concrete(I)]
85+
rule I1 *Int X +Int I2 *Int X => (I1 +Int I2) *Int X [simplification(200), concrete(I1, I2)]
86+
```
87+
* Generalized reverse distributivity
88+
```k
89+
// The backends do not allow to do meta-manipulation of terms (e.g. to sort
90+
// them by some criteria), so this is an attempt to catch the most common
91+
// non-basic cases for reverse distributivity:
92+
93+
// Distance 1:
94+
rule (X +Int Y) +Int X => 2 *Int X +Int Y
95+
[simplification(200)]
96+
rule (X +Int Y) +Int I *Int X => (1 +Int I) *Int X +Int Y
97+
[simplification(200), concrete(I)]
98+
rule (I *Int X +Int Y) +Int X => (1 +Int I) *Int X +Int Y
99+
[simplification(200), concrete(I)]
100+
rule (I1 *Int X +Int Y) +Int I2 *Int X => (I1 +Int I2) *Int X +Int Y
101+
[simplification(200), symbolic(X), concrete(I1, I2)]
102+
103+
rule (Y +Int X) +Int X => Y +Int 2 *Int X
104+
[simplification(200)]
105+
rule (Y +Int X) +Int I *Int X => Y +Int (1 +Int I) *Int X
106+
[simplification(200), concrete(I)]
107+
rule (Y +Int I *Int X) +Int X => Y +Int (1 +Int I) *Int X
108+
[simplification(200), concrete(I)]
109+
rule (Y +Int I1 *Int X) +Int I2 *Int X => Y +Int (I1 +Int I2) *Int X
110+
[simplification(200), concrete(I1, I2)]
111+
112+
// Distance 2:
113+
rule ((X +Int Y) +Int Z) +Int X => (2 *Int X +Int Y) +Int Z
114+
[simplification(200)]
115+
rule ((X +Int Y) +Int Z) +Int I *Int X => ((1 +Int I) *Int X +Int Y) +Int Z
116+
[simplification(200), concrete(I)]
117+
rule ((I *Int X +Int Y) +Int Z) +Int X => ((1 +Int I) *Int X +Int Y) +Int Z
118+
[simplification(200), concrete(I)]
119+
rule ((I1 *Int X +Int Y) +Int Z) +Int I2 *Int X => ((I1 +Int I2) *Int X +Int Y) +Int Z
120+
[simplification(200), symbolic(X), concrete(I1, I2)]
121+
122+
rule ((Y +Int X) +Int Z) +Int X => (Y +Int 2 *Int X) +Int Z
123+
[simplification(200)]
124+
rule ((Y +Int X) +Int Z) +Int I *Int X => (Y +Int (1 +Int I) *Int X) +Int Z
125+
[simplification(200), concrete(I)]
126+
rule ((Y +Int I *Int X) +Int Z) +Int X => (Y +Int (1 +Int I) *Int X) +Int Z
127+
[simplification(200), concrete(I)]
128+
rule ((Y +Int I1 *Int X) +Int Z) +Int I2 *Int X => (Y +Int (I1 +Int I2) *Int X) +Int Z
129+
[simplification(200), concrete(I1, I2)]
130+
131+
// Distance 3:
132+
rule (((X +Int Y) +Int Z) +Int T) +Int X => ((2 *Int X +Int Y) +Int Z) +Int T
133+
[simplification(200)]
134+
rule (((X +Int Y) +Int Z) +Int T) +Int I *Int X => (((1 +Int I) *Int X +Int Y) +Int Z) +Int T
135+
[simplification(200), concrete(I)]
136+
rule (((I *Int X +Int Y) +Int Z) +Int T) +Int X => (((1 +Int I) *Int X +Int Y) +Int T) +Int Z
137+
[simplification(200), concrete(I)]
138+
rule (((I1 *Int X +Int Y) +Int Z) +Int T) +Int I2 *Int X => (((I1 +Int I2) *Int X +Int Y) +Int T) +Int Z
139+
[simplification(200), symbolic(X), concrete(I1, I2)]
140+
141+
rule (((Y +Int X) +Int Z) +Int T) +Int X => ((Y +Int 2 *Int X) +Int Z) +Int T
142+
[simplification(200)]
143+
rule (((Y +Int X) +Int Z) +Int T) +Int I *Int X => ((Y +Int (1 +Int I) *Int X) +Int Z) +Int T
144+
[simplification(200), concrete(I)]
145+
rule (((Y +Int I *Int X) +Int Z) +Int T) +Int X => ((Y +Int (1 +Int I) *Int X) +Int Z) +Int T
146+
[simplification(200), concrete(I)]
147+
rule (((Y +Int I1 *Int X) +Int Z) +Int T) +Int I2 *Int X => ((Y +Int (I1 +Int I2) *Int X) +Int Z) +Int T
148+
[simplification(200), concrete(I1, I2)]
149+
150+
// Distance 4:
151+
rule ((((X +Int Y) +Int Z) +Int T) +Int S) +Int X => (((2 *Int X +Int Y) +Int Z) +Int T) +Int S
152+
[simplification(200)]
153+
rule ((((X +Int Y) +Int Z) +Int T) +Int S) +Int I *Int X => ((((1 +Int I) *Int X +Int Y) +Int Z) +Int T) +Int S
154+
[simplification(200), concrete(I)]
155+
rule ((((I *Int X +Int Y) +Int Z) +Int T) +Int S) +Int X => ((((1 +Int I) *Int X +Int Y) +Int T) +Int S) +Int Z
156+
[simplification(200), concrete(I)]
157+
rule ((((I1 *Int X +Int Y) +Int Z) +Int T) +Int S) +Int I2 *Int X => ((((I1 +Int I2) *Int X +Int Y) +Int T) +Int S) +Int Z
158+
[simplification(200), symbolic(X), concrete(I1, I2)]
159+
160+
rule ((((Y +Int X) +Int Z) +Int T) +Int S) +Int X => (((Y +Int 2 *Int X) +Int Z) +Int S) +Int T
161+
[simplification(200)]
162+
rule ((((Y +Int X) +Int Z) +Int T) +Int S) +Int I *Int X => (((Y +Int (1 +Int I) *Int X) +Int Z) +Int T) +Int S
163+
[simplification(200), concrete(I)]
164+
rule ((((Y +Int I *Int X) +Int Z) +Int T) +Int S) +Int X => (((Y +Int (1 +Int I) *Int X) +Int Z) +Int T) +Int S
165+
[simplification(200), concrete(I)]
166+
rule ((((Y +Int I1 *Int X) +Int Z) +Int T) +Int S) +Int I2 *Int X => (((Y +Int (I1 +Int I2) *Int X) +Int Z) +Int T) +Int S
167+
[simplification(200), concrete(I1, I2)]
168+
endmodule
169+
170+
```

‎pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/bit-normalization.md‎

Lines changed: 196 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,196 @@
1+
Int bit normalization
2+
=====================
3+
4+
The normal form of an int expression based on bit operations is defined by:
5+
6+
```
7+
or-operand = ((non-bit-int-expression &Int mask) >>Int shift)
8+
| ((non-bit-int-expression &Int mask) <<Int shift)
9+
bit-based-expression = or-operand |Int or-operand |Int ...
10+
```
11+
12+
where any of the mask and the shift may be missing, and the int-expression
13+
may have only one or-operand.
14+
15+
In `&Int` and `|Int` expressions, the concrete operand (if any), is second.
16+
17+
Additionally, `bit-expression modInt power-of-2` is transformed to a bit expression.
18+
19+
The normalization below works properly if
20+
* In `A &Int B` and `A |Int B`, at least one of the operands is concrete
21+
* The second operand of `A >>Int B` and `A <<Int B` is concrete and less than 64
22+
23+
```k
24+
module WASM-INT-BIT-NORMALIZATION-LEMMAS [symbolic]
25+
imports CEILS-SYNTAX
26+
imports INT
27+
imports WASM-INT-COMMON
28+
29+
rule _A &Int 0 => 0
30+
rule A &Int B => A
31+
requires 0 <=Int A
32+
andBool A <=Int B
33+
andBool isFullMask(B)
34+
[simplification, concrete(B)]
35+
rule (A &Int B) => 0
36+
requires 0 <=Int A
37+
andBool (
38+
( A <=Int fullMask(8)
39+
andBool B &Int fullMask(8) ==Int 0
40+
)
41+
orBool ( A <=Int fullMask(16)
42+
andBool B &Int fullMask(16) ==Int 0
43+
)
44+
orBool ( A <=Int fullMask(32)
45+
andBool B &Int fullMask(32) ==Int 0
46+
)
47+
)
48+
[simplification]
49+
rule A &Int B => B &Int A
50+
[simplification, concrete(A), symbolic(B)]
51+
rule (A &Int B) &Int C => A &Int (B &Int C)
52+
[simplification, concrete(B, C)]
53+
rule A &Int (B &Int C) => (A &Int B) &Int C
54+
[simplification, symbolic(A, B)]
55+
56+
rule (A <<IntTotal B) &Int M
57+
=> (A &Int (M >>Int B)) <<IntTotal B
58+
requires 0 <=Int B
59+
andBool 1 <<Int B <=Int M +Int 1
60+
[simplification, concrete(M, B)]
61+
rule (_A <<IntTotal B) &Int M => 0
62+
requires 0 <=Int M
63+
andBool 0 <=Int B
64+
andBool M <Int (1 <<Int B)
65+
[simplification]
66+
rule (A >>IntTotal B) &Int M
67+
=> (A &Int (M <<Int B)) >>IntTotal B
68+
requires 0 <=Int B
69+
[simplification, concrete(M, B)]
70+
71+
rule (A <<IntTotal 0) => A
72+
[simplification]
73+
rule (A >>IntTotal 0) => A
74+
[simplification]
75+
rule (A >>IntTotal B) => 0
76+
requires 0 <=Int A andBool 0 <Int B andBool A <=Int fullMask(B)
77+
[simplification, concrete(B)]
78+
rule (A >>IntTotal B) >>IntTotal C => A >>IntTotal (B +Int C)
79+
[simplification, concrete(B, C)]
80+
rule (A <<IntTotal B) <<IntTotal C => A <<IntTotal (B +Int C)
81+
[simplification, concrete(B, C)]
82+
rule (A <<IntTotal B) >>IntTotal C => A <<IntTotal (B -Int C)
83+
requires C <=Int B
84+
[simplification, concrete(B, C)]
85+
rule (A <<IntTotal B) >>IntTotal C => A >>IntTotal (C -Int B)
86+
requires B <Int C
87+
[simplification, concrete(B, C)]
88+
rule (A >>IntTotal B) <<IntTotal C
89+
=> (A >>IntTotal (B -Int C))
90+
&Int (fullMask(64) -Int fullMask(C))
91+
requires 0 <=Int C
92+
andBool C <=Int B
93+
andBool B <=Int 64
94+
andBool 0 <=Int A
95+
andBool A <Int (1 <<Int 64)
96+
[simplification, concrete(B, C)]
97+
rule (A >>IntTotal B) <<IntTotal C
98+
=> (A <<IntTotal (C -Int B))
99+
&Int (fullMask(64) -Int fullMask(C))
100+
requires 0 <=Int B
101+
andBool B <Int C
102+
andBool C <=Int 64
103+
andBool 0 <=Int A
104+
andBool A <Int (1 <<Int (64 -Int (C -Int B)))
105+
[simplification, concrete(B, C)]
106+
107+
rule A |Int 0 => A
108+
[simplification]
109+
rule A |Int B => B |Int A
110+
[simplification, concrete(A), symbolic(B)]
111+
rule (A |Int B) |Int C => A |Int (B |Int C)
112+
[simplification, concrete(B, C)]
113+
rule A |Int (B |Int C) => (A |Int B) |Int C
114+
[simplification, symbolic(A, B)]
115+
116+
rule (A |Int B) &Int C => (A &Int C) |Int (B &Int C)
117+
[simplification]
118+
rule A &Int (B |Int C) => (A |Int C) &Int (B |Int C)
119+
[simplification, symbolic(B)]
120+
rule A &Int (B |Int C) => (A |Int C) &Int (B |Int C)
121+
[simplification, symbolic(C)]
122+
rule (A &Int B) |Int (A &Int C)
123+
=> A &Int (B |Int C)
124+
[simplification, concrete(B, C)]
125+
rule (A |Int B) >>IntTotal C => (A >>IntTotal C) |Int (B >>IntTotal C)
126+
requires 0 <=Int C
127+
[simplification]
128+
rule (A |Int B) <<IntTotal C => (A <<IntTotal C) |Int (B <<IntTotal C)
129+
requires 0 <=Int C
130+
[simplification]
131+
132+
rule (A &Int B) modIntTotal M => (A &Int B) &Int (M -Int 1)
133+
requires (0 <=Int A orBool 0 <=Int B)
134+
andBool isPowerOf2(M)
135+
[simplification]
136+
rule (A >>IntTotal B) modIntTotal M => (A >>IntTotal B) &Int (M -Int 1)
137+
requires 0 <=Int A
138+
andBool isPowerOf2(M)
139+
[simplification]
140+
rule (A <<IntTotal B) modIntTotal M => (A <<IntTotal B) &Int (M -Int 1)
141+
requires 0 <=Int A
142+
andBool isPowerOf2(M)
143+
[simplification]
144+
rule (A |Int B) modIntTotal M => (A |Int B) &Int (M -Int 1)
145+
requires 0 <=Int A
146+
andBool 0 <=Int B
147+
andBool isPowerOf2(M)
148+
[simplification]
149+
150+
rule (A modIntTotal M) &Int B => (A &Int (M -Int 1)) &Int B
151+
requires (0 <=Int A orBool 0 <=Int B)
152+
andBool isPowerOf2(M)
153+
[simplification]
154+
rule (A modIntTotal M) >>IntTotal B => (A &Int (M -Int 1)) >>IntTotal B
155+
requires 0 <=Int A
156+
andBool isPowerOf2(M)
157+
[simplification]
158+
rule (A modIntTotal M) <<IntTotal B => (A &Int (M -Int 1)) <<IntTotal B
159+
requires 0 <=Int A
160+
andBool isPowerOf2(M)
161+
[simplification]
162+
rule (A modIntTotal M) |Int B => (A &Int (M -Int 1)) |Int B
163+
requires 0 <=Int A
164+
andBool 0 <=Int B
165+
andBool isPowerOf2(M)
166+
[simplification]
167+
168+
// Rules for having saner masks.
169+
rule A &Int B => A &Int (B &Int fullMask(8))
170+
requires fullMask(8) <Int B andBool 0 <=Int A andBool A <=Int fullMask(8)
171+
[simplification, concrete(B)]
172+
rule A &Int B => A &Int (B &Int fullMask(16))
173+
requires fullMask(16) <Int B andBool 0 <=Int A andBool A <=Int fullMask(16)
174+
[simplification, concrete(B)]
175+
rule A &Int B => A &Int (B &Int fullMask(24))
176+
requires fullMask(24) <Int B andBool 0 <=Int A andBool A <=Int fullMask(24)
177+
[simplification, concrete(B)]
178+
rule A &Int B => A &Int (B &Int fullMask(32))
179+
requires fullMask(32) <Int B andBool 0 <=Int A andBool A <=Int fullMask(32)
180+
[simplification, concrete(B)]
181+
rule A &Int B => A &Int (B &Int fullMask(40))
182+
requires fullMask(40) <Int B andBool 0 <=Int A andBool A <=Int fullMask(40)
183+
[simplification, concrete(B)]
184+
rule A &Int B => A &Int (B &Int fullMask(48))
185+
requires fullMask(48) <Int B andBool 0 <=Int A andBool A <=Int fullMask(48)
186+
[simplification, concrete(B)]
187+
rule A &Int B => A &Int (B &Int fullMask(56))
188+
requires fullMask(56) <Int B andBool 0 <=Int A andBool A <=Int fullMask(56)
189+
[simplification, concrete(B)]
190+
191+
rule {0 #Equals (A &Int B) >>IntTotal C }
192+
=> { 0 #Equals A &Int B }
193+
requires B &Int fullMask(C) ==Int 0
194+
[simplification, concrete(B, C)]
195+
endmodule
196+
```

‎pykwasm/src/pykwasm/kdist/wasm-semantics/symbolic/int/common.md‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
```k
2+
module WASM-INT-COMMON
3+
imports BOOL
4+
imports INT
5+
6+
syntax Bool ::= isFullMask(Int) [function, total]
7+
rule isFullMask(I:Int) => I ==Int fullMask(log2Int(I) +Int 1)
8+
requires 0 <Int I
9+
rule isFullMask(I:Int) => false
10+
requires I <=Int 0
11+
12+
syntax Bool ::= isPowerOf2(Int) [function, total]
13+
rule isPowerOf2(I:Int) => I ==Int 1 <<Int log2Int(I)
14+
requires 0 <Int I
15+
rule isPowerOf2(I:Int) => false
16+
requires I <=Int 0
17+
18+
syntax Int ::= fullMask(Int) [function, total]
19+
rule fullMask(I:Int) => (1 <<Int I) -Int 1
20+
requires 0 <Int I
21+
rule fullMask(I:Int) => 0
22+
requires I <=Int 0
23+
endmodule
24+
```

0 commit comments

Comments
 (0)