Skip to content

Commit 1779028

Browse files
ehildenbehildenb
committed
tests/specs/: use notMaxUInt160 alias instead of full integer in several places
1 parent cbb74f7 commit 1779028

File tree

3 files changed

+10
-12
lines changed

3 files changed

+10
-12
lines changed

‎tests/specs/benchmarks/verification.k

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ module VERIFICATION
102102
rule maxUInt256 &Int X => X requires #rangeUInt(256, X) [simplification]
103103

104104
// 2^256 - 2^160 = 0xff..ff00..00 (96 1's followed by 160 0's)
105-
rule 115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int ADDR => 0
105+
rule notMaxUInt160 &Int ADDR => 0
106106
requires #rangeAddress(ADDR)
107107
[simplification]
108108

‎tests/specs/functional/lemmas-spec.k

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -42,27 +42,27 @@ module LEMMAS-SPEC
4242
andBool #rangeUInt(256, Z) andBool Z ==Int #lookup(M, _KZ)
4343
andBool #rangeUInt(256, (X -Int Y) -Int Z)
4444

45-
claim [address-reprojection]: <k> runLemma(((maxUInt160 &Int ((368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)) modInt pow256)) modInt pow160))
45+
claim [address-reprojection]: <k> runLemma(((maxUInt160 &Int ((368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)) modInt pow256)) modInt pow160))
4646
=> doneLemma(368263281805664599098893944405654396525700029268) ... </k>
4747
requires #rangeUInt(256, X)
4848

49-
claim [address-reprojection-1]: <k> runLemma(0 <=Int (368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)))
49+
claim [address-reprojection-1]: <k> runLemma(0 <=Int (368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)))
5050
=> doneLemma(true) ... </k>
5151
requires #rangeUInt(256, X)
5252

53-
claim [address-reprojection-2]: <k> runLemma(0 <=Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int))
53+
claim [address-reprojection-2]: <k> runLemma(0 <=Int (notMaxUInt160 &Int X:Int))
5454
=> doneLemma(true) ... </k>
5555
requires #rangeUInt(256, X)
5656

57-
claim [address-reprojection-4]: <k> runLemma((368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)) <Int pow256)
57+
claim [address-reprojection-4]: <k> runLemma((368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)) <Int pow256)
5858
=> doneLemma(true) ... </k>
5959
requires #rangeUInt(256, X)
6060

61-
claim [address-reprojection-5]: <k> runLemma((115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int) <Int pow256)
61+
claim [address-reprojection-5]: <k> runLemma((notMaxUInt160 &Int X:Int) <Int pow256)
6262
=> doneLemma(true) ... </k>
6363
requires #rangeUInt(256, X)
6464

65-
claim [address-reprojection-6]: <k> runLemma(maxUInt160 &Int (368263281805664599098893944405654396525700029268 |Int (115792089237316195423570985007226406215939081747436879206741300988257197096960 &Int X:Int)))
65+
claim [address-reprojection-6]: <k> runLemma(maxUInt160 &Int (368263281805664599098893944405654396525700029268 |Int (notMaxUInt160 &Int X:Int)))
6666
=> doneLemma(368263281805664599098893944405654396525700029268) ... </k>
6767
requires #rangeUInt(256, X)
6868

‎tests/specs/mcd/word-pack.k

Lines changed: 3 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -117,16 +117,14 @@ module WORD-PACK-COMMON
117117
rule UINT48_1 |Int (maskWordPackUInt48UInt48_2 &Int UINT48_UINT48) => #WordPackUInt48UInt48( UINT48_1 , (maskWordPackUInt48UInt48_2 &Int UINT48_UINT48) /Int pow48 ) requires #rangeUInt(96, UINT48_UINT48) andBool #rangeUInt(48, UINT48_1) [simplification]
118118
rule (UINT48_2 *Int pow48) |Int (maxUInt48 &Int UINT48_UINT48) => #WordPackUInt48UInt48( maxUInt48 &Int UINT48_UINT48 , UINT48_2 ) requires #rangeUInt(96, UINT48_UINT48) andBool #rangeUInt(48, UINT48_2) [simplification]
119119

120-
syntax Int ::= "maskWordPackAddrUInt48UInt48_1" [macro] // 0xFFFFFFFFFFFFFFFFFFFFFFFF0000000000000000000000000000000000000000
121-
| "maskWordPackAddrUInt48UInt48_2" [macro] // 0xFFFFFFFFFFFF000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
120+
syntax Int ::= "maskWordPackAddrUInt48UInt48_2" [macro] // 0xFFFFFFFFFFFF000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
122121
| "maskWordPackAddrUInt48UInt48_3" [macro] // 0x000000000000FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF
123122
// -----------------------------------------------------------------------------------------------------------------------------
124-
rule maskWordPackAddrUInt48UInt48_1 => 115792089237316195423570985007226406215939081747436879206741300988257197096960
125123
rule maskWordPackAddrUInt48UInt48_2 => 115792089237315784047431654708638870748305248246218003188207458632603225030655
126124
rule maskWordPackAddrUInt48UInt48_3 => 411376139330301510538742295639337626245683966408394965837152255
127125

128-
rule (ADDR |Int (maskWordPackAddrUInt48UInt48_1 &Int ADDR_UINT48_UINT48)) /Int pow160 => ADDR_UINT48_UINT48 /Int pow160 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
129-
rule (ADDR |Int (maskWordPackAddrUInt48UInt48_1 &Int ADDR_UINT48_UINT48)) /Int pow208 => ADDR_UINT48_UINT48 /Int pow208 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
126+
rule (ADDR |Int (notMaxUInt160 &Int ADDR_UINT48_UINT48)) /Int pow160 => ADDR_UINT48_UINT48 /Int pow160 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
127+
rule (ADDR |Int (notMaxUInt160 &Int ADDR_UINT48_UINT48)) /Int pow208 => ADDR_UINT48_UINT48 /Int pow208 requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeAddress(ADDR) [simplification]
130128

131129
rule (UINT48_2 *Int pow208) |Int (maskWordPackAddrUInt48UInt48_3 &Int ADDR_UINT48_UINT48) => #WordPackAddrUInt48UInt48(maxUInt160 &Int ADDR_UINT48_UINT48, maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow160), UINT48_2) requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeUInt(48, UINT48_2) [simplification]
132130
rule (UINT48_1 *Int pow160) |Int (maskWordPackAddrUInt48UInt48_2 &Int ADDR_UINT48_UINT48) => #WordPackAddrUInt48UInt48(maxUInt160 &Int ADDR_UINT48_UINT48, UINT48_1, maxUInt48 &Int (ADDR_UINT48_UINT48 /Int pow208)) requires #rangeUInt(256, ADDR_UINT48_UINT48) andBool #rangeUInt(48, UINT48_1) [simplification]

0 commit comments

Comments
 (0)