Skip to content

Commit cd2e87a

Browse files
PetarMaxrv-auditorpalinatolmachehildenbtothtamas28
authored
Lemmas on Boolean reasoning, set reasoning, map lookup (#2037)
* lemmas on Boolean reasoning, set reasoning, map lookup, and keccak * Set Version: 1.0.277 * removing keccak lemmas that should not be upstreamed * addressing comments * Set Version: 1.0.278 * Set Version: 1.0.278 * corrections * removing ==Bool from expected files * Set Version: 1.0.279 * Set Version: 1.0.279 * Set Version: 1.0.309 * Set Version: 1.0.311 * updating expected outputs * Set Version: 1.0.312 * Set Version: 1.0.330 * Set Version: 1.0.334 * revisiting set simplifications * --amend * --amend * --amend * streamlining lookup simplifications * streamlining set simplifications * removing set reasoning entirely * Set Version: 1.0.336 * concretising set simplifications: * streamlining set simplifications * Set Version: 1.0.337 * even more concrete set simplifications * bringing old simplifications back * Set Version: 1.0.340 * resolving parsing ambiguities * --amend * --amend * Set Version: 1.0.341 * Set Version: 1.0.342 * Set Version: 1.0.343 * correction * syntax * --amend * Set Version: 1.0.349 * Set Version: 1.0.355 * Set Version: 1.0.356 * Set Version: 1.0.357 * Correctly ordered arguments in `typed_args` (#2174) * Correctly ordered arguments in `typed_args` * Set Version: 1.0.357 --------- Co-authored-by: devops <[email protected]> * Inject `ccopts` directly into `kevm_kompile` and fix some tests (#2164) * Makefile: make sure evm-optimizations-spec is rebuilt on changes to optimizations.md * kproj/optimizations: remove symbolic attribute on evm-optimizations-lemmas * tests/specs/examples/sum-to-n-foundry-spec: correct imports for LLVM backend * tests/specs/functional/infinite-gas-spec.k: allow import of main module in symbolic module for LLVM * kevm-pyk/__main__, Makefile, VERIFICATION: rename kevm {kompile => kompile-spec} for more accurate usage * README: update documentation * kevm-pyk/: all builds require plugin_dir, compute it directly * kevm-pyk/: move calculation of plugin_dir out of run_kompile, pass in ccopts directly * kevm-pyk/__main__: adjust acceptable values for kevm kompile-spec * VERIFICATION: update documentation * Makefile: bring back --target argument * Set Version: 1.0.343 * test_prove: only add ccopts if were using the booster * Set Version: 1.0.355 * package/test-package: add previously failing test of using booster due to plugin_dir being missing * kevm-pyk/__main__: use correct target for kompile-spec * Set Version: 1.0.356 * Set Version: 1.0.356 * kevm-pyk/plugin: correction from code review * kevm-pyk/kdist/plugin: hardcode plugin as dependency for other targets * kevm-pyk/: factor out generic run_kompile from kevm_kompile * kevm_pyk/kompile: rename lib_ccopts => _lib_ccopts * Set Version: 1.0.357 * kevm-pyk/kdist/plugin: make sure all KEVMTarget have plugin as depenndency * Set Version: 1.0.357 * kdist/plugin: drop self._deps * Set Version: 1.0.358 * Set Version: 1.0.358 --------- Co-authored-by: devops <[email protected]> * Fix circular import (#2179) * Fix circular import * Set Version: 1.0.359 --------- Co-authored-by: devops <[email protected]> * Move `--port` arguments to `rpc_args` (#2178) * Move `--port` arguments to `rpc_args` * Set Version: 1.0.359 * Set Version: 1.0.360 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> * Update dependency: deps/pyk_release (#2175) * deps/pyk_release: Set Version v0.1.501 * Set Version: 1.0.357 * kevm-pyk/: sync poetry files pyk version v0.1.501 * deps/k_release: sync release file version 6.1.14 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.359 * kevm-pyk/: sync poetry files pyk version v0.1.501 * Set Version: 1.0.361 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> * Update dependency: deps/pyk_release (#2181) * deps/pyk_release: Set Version v0.1.505 * kevm-pyk/: sync poetry files pyk version v0.1.505 * deps/k_release: sync release file version 6.1.20 * flake.{nix,lock}: update Nix derivations * Set Version: 1.0.362 --------- Co-authored-by: devops <[email protected]> * Set Version: 1.0.364 * Set Version: 1.0.364 * Set Version: 1.0.365 * Set Version: 1.0.372 * Set Version: 1.0.379 * adding tests * Set Version: 1.0.381 * normalising comparisons, adding keccak * reverting normalisation * removing equality simplification * Set Version: 1.0.382 * Set Version: 1.0.382 * bringing back comparison (but not equality) normalisation * bringing back equality normalisation * Set Version: 1.0.394 * Set Version: 1.0.396 * Set Version: 1.0.398 * removing unsound keccak simplifying assumptions * Set Version: 1.0.399 * Set Version: 1.0.400 * Set Version: 1.0.406 * Set Version: 1.0.407 * adding tests for comparison normalisation, removing keccak * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md Co-authored-by: Everett Hildenbrandt <[email protected]> * ----- alignment * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]> Co-authored-by: Tamás Tóth <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent b70fd06 commit cd2e87a

File tree

8 files changed

+155
-41
lines changed

8 files changed

+155
-41
lines changed

‎kevm-pyk/pyproject.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "kevm-pyk"
7-
version = "1.0.406"
7+
version = "1.0.407"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

‎kevm-pyk/src/kevm_pyk/__init__.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,4 @@
66
from typing import Final
77

88

9-
VERSION: Final = '1.0.406'
9+
VERSION: Final = '1.0.407'

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,11 @@ module BYTES-SIMPLIFICATION [symbolic]
5454
requires lengthBytes(B) <=Int 32
5555
andBool #rangeUInt(256, X) [simplification, concrete(B), comm]
5656

57+
rule [buf-as-int-ml]:
58+
{ B:Bytes #Equals #buf(32, X:Int) } => { X #Equals #asInteger(B) }
59+
requires lengthBytes(B) <=Int 32
60+
andBool #rangeUInt(256, X) [simplification, concrete(B), comm]
61+
5762
rule [buf-asWord-invert]:
5863
#buf (W:Int , #asWord(B:Bytes)) => #buf(W -Int lengthBytes(B), 0) +Bytes B
5964
requires lengthBytes(B) <=Int W andBool W <=Int 32

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k‎

Lines changed: 58 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -13,35 +13,77 @@ module INT-SIMPLIFICATION-HASKELL [symbolic, kore]
1313

1414
// associativity normalization
1515

16-
rule A +Int B => B +Int A [concrete(A), symbolic(B), simplification(40)]
17-
18-
rule A +Int (B +Int C) => (A +Int B) +Int C [symbolic(A, B), simplification(40)]
19-
rule A +Int (B -Int C) => (A +Int B) -Int C [symbolic(A, B), simplification(40)]
20-
rule A -Int (B +Int C) => (A -Int B) -Int C [symbolic(A, B), simplification(40)]
21-
rule A -Int (B -Int C) => (A -Int B) +Int C [symbolic(A, B), simplification(40)]
16+
rule A +Int (B +Int C) => (A +Int B) +Int C [symbolic(A, B), concrete(C), simplification(40)]
17+
rule A +Int (B -Int C) => (A +Int B) -Int C [symbolic(A, B), concrete(C), simplification(40)]
18+
rule A -Int (B +Int C) => (A -Int B) -Int C [symbolic(A, B), concrete(C), simplification(40)]
19+
rule A -Int (B -Int C) => (A -Int B) +Int C [symbolic(A, B), concrete(C), simplification(40)]
2220

2321
rule A +Int (B -Int C) => (A -Int C) +Int B [symbolic(A, C), concrete(B), simplification(40)]
2422
rule A -Int (B -Int C) => (A +Int C) -Int B [symbolic(A, C), concrete(B), simplification(40)]
2523

26-
rule (A +Int B) +Int C => (A +Int C) +Int B [concrete(B), symbolic(C), simplification(40)]
27-
rule (A +Int B) -Int C => (A -Int C) +Int B [concrete(B), symbolic(C), simplification(40)]
28-
rule (A -Int B) +Int C => (A +Int C) -Int B [concrete(B), symbolic(C), simplification(40)]
29-
rule (A -Int B) -Int C => (A -Int C) -Int B [concrete(B), symbolic(C), simplification(40)]
24+
rule (A +Int B) +Int C => (A +Int C) +Int B [concrete(B), symbolic(A, C), simplification(40)]
25+
rule (A +Int B) -Int C => (A -Int C) +Int B [concrete(B), symbolic(A, C), simplification(40)]
26+
rule (A -Int B) +Int C => (A +Int C) -Int B [concrete(B), symbolic(A, C), simplification(40)]
27+
rule (A -Int B) -Int C => (A -Int C) -Int B [concrete(B), symbolic(A, C), simplification(40)]
3028

3129
rule (A +Int B) +Int C => A +Int (B +Int C) [concrete(B, C), symbolic(A), simplification(40)]
3230
rule (A +Int B) -Int C => A +Int (B -Int C) [concrete(B, C), symbolic(A), simplification(40)]
3331
rule (A -Int B) +Int C => A +Int (C -Int B) [concrete(B, C), symbolic(A), simplification(40)]
3432
rule (A -Int B) -Int C => A -Int (B +Int C) [concrete(B, C), symbolic(A), simplification(40)]
3533

3634
// ###########################################################################
37-
// inequality
35+
// comparison normalization
3836
// ###########################################################################
3937

40-
rule A +Int B <Int C => A <Int C -Int B [concrete(B), simplification(40)]
41-
rule A <Int B +Int C => A -Int C <Int B [concrete(A, C), simplification(40)]
42-
rule A <=Int B +Int C => A -Int C <=Int B [concrete(A, C), simplification(40)]
43-
rule A -Int B <Int C => A -Int C <Int B [concrete(A, C), simplification(40)]
44-
rule A <=Int B -Int C => C <=Int B -Int A [concrete(A, B), simplification(40)]
38+
rule A +Int B <Int C => A <Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
39+
rule A +Int B <=Int C => A <=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
40+
rule A +Int B >Int C => A >Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
41+
rule A +Int B >=Int C => A >=Int C -Int B [concrete(B, C), symbolic(A), simplification(45)]
42+
43+
rule A +Int B <Int C => B <Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
44+
rule A +Int B <=Int C => B <=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
45+
rule A +Int B >Int C => B >Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
46+
rule A +Int B >=Int C => B >=Int C -Int A [concrete(A, C), symbolic(B), simplification(45)]
47+
48+
rule A -Int B <Int C => A <Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
49+
rule A -Int B <=Int C => A <=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
50+
rule A -Int B >Int C => A >Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
51+
rule A -Int B >=Int C => A >=Int C +Int B [concrete(B, C), symbolic(A), simplification(45)]
52+
53+
rule A -Int B <Int C => A -Int C <Int B [concrete(A, C), symbolic(B), simplification(45)]
54+
rule A -Int B <=Int C => A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)]
55+
rule A -Int B >Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45)]
56+
rule A -Int B >=Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)]
57+
58+
rule A <Int B +Int C => A -Int B <Int C [concrete(A, B), symbolic(C), simplification(45)]
59+
rule A <=Int B +Int C => A -Int B <=Int C [concrete(A, B), symbolic(C), simplification(45)]
60+
rule A >Int B +Int C => A -Int B >Int C [concrete(A, B), symbolic(C), simplification(45)]
61+
rule A >=Int B +Int C => A -Int B >=Int C [concrete(A, B), symbolic(C), simplification(45)]
62+
63+
rule A <Int B +Int C => A -Int C <Int B [concrete(A, C), symbolic(B), simplification(45)]
64+
rule A <=Int B +Int C => A -Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)]
65+
rule A >Int B +Int C => A -Int C >Int B [concrete(A, C), symbolic(B), simplification(45)]
66+
rule A >=Int B +Int C => A -Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)]
67+
68+
rule A <Int B -Int C => C <Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
69+
rule A <=Int B -Int C => C <=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
70+
rule A >Int B -Int C => C >Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
71+
rule A >=Int B -Int C => C >=Int B -Int A [concrete(A, B), symbolic(C), simplification(45)]
72+
73+
rule A <Int B -Int C => A +Int C <Int B [concrete(A, C), symbolic(B), simplification(45)]
74+
rule A <=Int B -Int C => A +Int C <=Int B [concrete(A, C), symbolic(B), simplification(45)]
75+
rule A >Int B -Int C => A +Int C >Int B [concrete(A, C), symbolic(B), simplification(45)]
76+
rule A >=Int B -Int C => A +Int C >=Int B [concrete(A, C), symbolic(B), simplification(45)]
77+
78+
rule A +Int B ==Int C => A ==Int C -Int B [concrete(B, C), symbolic(A), simplification(45), comm]
79+
rule A +Int B ==Int C => B ==Int C -Int A [concrete(A, C), symbolic(B), simplification(45), comm]
80+
rule A -Int B ==Int C => A ==Int C +Int B [concrete(B, C), symbolic(A), simplification(45), comm]
81+
rule A -Int B ==Int C => A -Int C ==Int B [concrete(A, C), symbolic(B), simplification(45), comm]
82+
83+
rule { A +Int B #Equals C } => { A #Equals C -Int B } [concrete(B, C), symbolic(A), simplification(45), comm]
84+
rule { A +Int B #Equals C } => { B #Equals C -Int A } [concrete(A, C), symbolic(B), simplification(45), comm]
85+
rule { A -Int B #Equals C } => { A #Equals C +Int B } [concrete(B, C), symbolic(A), simplification(45), comm]
86+
rule { A -Int B #Equals C } => { A -Int C #Equals B } [concrete(A, C), symbolic(B), simplification(45), comm]
4587

4688
endmodule
4789

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ module LEMMAS [symbolic]
2828
rule chop(_V) <Int pow256 => true [simplification]
2929

3030
rule X *Int Y <Int pow256 => true requires Y <=Int maxUInt256 /Int X [simplification]
31-
rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]
31+
rule #if B #then C +Int C1 #else C +Int C2 #fi => C +Int #if B #then C1 #else C2 #fi [simplification]
3232

3333
// ########################
3434
// Set Reasoning
@@ -37,6 +37,9 @@ module LEMMAS [symbolic]
3737
rule X in (SetItem(Y) _ ) => true requires X ==Int Y [simplification]
3838
rule X in (SetItem(Y) REST) => X in REST requires X =/=Int Y [simplification]
3939

40+
rule ( S:Set |Set SetItem ( X ) ) |Set SetItem( X ) => ( S:Set |Set SetItem ( X ) ) [simplification]
41+
rule ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) |Set SetItem( X ) => ( ( S:Set |Set SetItem ( X ) ) |Set SetItem ( Y ) ) [simplification]
42+
4043
// ########################
4144
// Word Reasoning
4245
// ########################
@@ -56,8 +59,6 @@ module LEMMAS [symbolic]
5659
rule bool2Word(_B) |Int 1 => 1 [simplification]
5760
rule bool2Word( B) &Int 1 => bool2Word(B) [simplification]
5861

59-
rule notBool notBool B => B [simplification]
60-
6162
// #newAddr range
6263
rule 0 <=Int #newAddr(_,_) => true [simplification]
6364
rule #newAddr(_,_) <Int pow160 => true [simplification]
@@ -72,20 +73,21 @@ module LEMMAS [symbolic]
7273
// Keccak
7374
// ########################
7475

75-
//Required for #Ceil(#buf)
76+
// Required for #Ceil(#buf)
7677
rule 0 <=Int keccak( _ ) => true [simplification]
7778
rule keccak( _ ) <Int pow256 => true [simplification]
7879

7980
// ########################
8081
// Map Reasoning
8182
// ########################
8283

83-
rule #lookup ( _M:Map [ K1 <- V1 ] , K2 ) => #lookup ( K1 |-> V1 , K1 ) requires K1 ==Int K2 [simplification]
84-
rule #lookup ( M:Map [ K1 <- _ ] , K2 ) => #lookup ( M , K2 ) requires K1 =/=Int K2 [simplification]
85-
8684
rule 0 <=Int #lookup( _M:Map , _ ) => true [simplification, smt-lemma]
8785
rule #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
8886

87+
rule #lookup ( _M:Map [ K1 <- V1 ] , K2 ) => #lookup ( K1 |-> V1 , K1 ) requires K1 ==Int K2 [simplification]
88+
rule #lookup ( M:Map [ K1 <- _ ] , K2 ) => #lookup ( M , K2 ) requires K1 =/=Int K2 [simplification]
89+
rule #lookup ( (K1:Int |-> _) M:Map, K2:Int) => #lookup ( M , K2 ) requires K1 =/=Int K2 [simplification]
90+
8991
rule M:Map [ I1:Int <- V1:Int ] [ I2:Int <- V2:Int ] ==K M:Map [ I2 <- V2 ] [ I1 <- V1 ] => true
9092
requires I1 =/=Int I2
9193
[simplification]
@@ -217,6 +219,11 @@ module LEMMAS-HASKELL [symbolic, kore]
217219
// Boolean Logic
218220
// ########################
219221

220-
rule B ==Bool false => notBool B [simplification]
222+
rule B ==Bool true => B [simplification, comm]
223+
rule B ==Bool false => notBool B [simplification, comm]
224+
225+
rule notBool notBool B => B [simplification]
226+
221227
rule (notBool (A andBool B)) andBool A => (notBool B) andBool A [simplification]
228+
222229
endmodule

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ Address/Hash Helpers
2222

2323
```k
2424
syntax Int ::= keccak ( Bytes ) [function, total, smtlib(smt_keccak)]
25-
// -------------------------------------------------------------------------
25+
// ---------------------------------------------------------------------
2626
rule [keccak]: keccak(WS) => #parseHexWord(Keccak256bytes(WS)) [concrete]
2727
```
2828

@@ -37,7 +37,7 @@ Address/Hash Helpers
3737
syntax Bytes ::= ECDSARecoverbytes ( Bytes , Int , Bytes , Bytes ) [function, total]
3838
syntax String ::= ECDSASignbytes ( Bytes, Bytes ) [function, total]
3939
| ECDSAPubKeybytes ( Bytes ) [function, total]
40-
// -------------------------------------------------------------------------
40+
// ------------------------------------------------------------------------------------
4141
rule Keccak256bytes(BS) => Keccak256(Bytes2String(BS)) [concrete]
4242
rule Sha256bytes(BS) => Sha256(Bytes2String(BS)) [concrete]
4343
rule RipEmd160bytes(BS) => RipEmd160(Bytes2String(BS)) [concrete]

‎package/version‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
1.0.406
1+
1.0.407

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

Lines changed: 72 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -73,6 +73,64 @@ module LEMMAS-SPEC
7373
=> doneLemma(368263281805664599098893944405654396525700029268) ... </k>
7474
requires #lookup(ACCT_STORAGE, 8) <Int pow160
7575

76+
// Comparisons
77+
// -----------
78+
79+
claim [comp-norm-01]:
80+
<k> runLemma (
81+
( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 <=Int 7
82+
) =>
83+
doneLemma (
84+
1 <=Int X
85+
) ...
86+
</k>
87+
88+
claim [comp-norm-02]:
89+
<k> runLemma (
90+
( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 <Int 7
91+
) =>
92+
doneLemma (
93+
1 <Int X
94+
) ...
95+
</k>
96+
97+
claim [comp-norm-03]:
98+
<k> runLemma (
99+
( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 >Int 7
100+
) =>
101+
doneLemma (
102+
1 >Int X
103+
) ...
104+
</k>
105+
106+
claim [comp-norm-04]:
107+
<k> runLemma (
108+
( ( 20 -Int ( 10 +Int X:Int ) ) -Int 5 ) +Int 3 >=Int 7
109+
) =>
110+
doneLemma (
111+
1 >=Int X
112+
) ...
113+
</k>
114+
115+
116+
// Sets
117+
// ----
118+
119+
claim [set-union-01]:
120+
<k> runLemma (
121+
notBool ( ( ((((S:Set |Set SetItem(X)) |Set SetItem (X)) |Set SetItem(Y)) |Set SetItem(X))
122+
==K
123+
((S:Set |Set SetItem(X)) |Set SetItem (Y))
124+
) ==Bool false
125+
) ==Bool true
126+
) =>
127+
doneLemma (
128+
true
129+
) ...
130+
</k>
131+
requires X =/=K Y
132+
133+
76134
// Buffer write simplifications
77135
// ----------------------------
78136

@@ -113,6 +171,8 @@ module LEMMAS-SPEC
113171
claim <k> runLemma ( #lookup( _M:Map [ KEY <- 33 ] [ KEY' <- 728 ] [ KEY'' <- (pow256 +Int 5) ] [ KEY''' <- "hello" ] , KEY'' ) ) => doneLemma ( 5 ) ... </k> requires KEY =/=Int KEY' andBool KEY =/=Int KEY'' andBool KEY =/=Int KEY''' andBool KEY' =/=Int KEY'' andBool KEY' =/=Int KEY''' andBool KEY'' =/=Int KEY'''
114172
claim <k> runLemma ( #lookup( _M:Map [ KEY <- 33 ] [ KEY' <- 728 ] [ KEY'' <- (pow256 +Int 5) ] [ KEY''' <- "hello" ] , KEY''' ) ) => doneLemma ( 0 ) ... </k> requires KEY =/=Int KEY' andBool KEY =/=Int KEY'' andBool KEY =/=Int KEY''' andBool KEY' =/=Int KEY'' andBool KEY' =/=Int KEY''' andBool KEY'' =/=Int KEY'''
115173

174+
claim [lookup-key-neq]: <k> runLemma ( #lookup( ( (3 |-> 3) (5 |-> 5) (7 |-> 7) M:Map ) [ 9 <- 9 ] [ 11 <- 11 ] [ 13 <- 13 ], KEY ) ) => doneLemma ( #lookup (M, KEY) ) ... </k> requires 15 <=Int KEY
175+
116176
// #range selection operation
117177
// --------------------------
118178

@@ -422,18 +482,18 @@ module LEMMAS-SPEC
422482
claim <k> runLemma ( notMaxUInt240 &Int ( X <<Int 240 ) ) => doneLemma( X <<Int 240 ) ... </k> requires #rangeUInt ( 16 , X )
423483
claim <k> runLemma ( notMaxUInt248 &Int ( X <<Int 248 ) ) => doneLemma( X <<Int 248 ) ... </k> requires #rangeUInt ( 8 , X )
424484

425-
claim <k> runLemma ( maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 8 , X )
426-
claim <k> runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 16 , X )
427-
claim <k> runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 32 , X )
428-
claim <k> runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 64 , X )
429-
claim <k> runLemma ( maxUInt96 &Int ( X |Int ( notMaxUInt96 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 96 , X )
430-
claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
431-
claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
432-
claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
433-
claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
434-
claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
435-
claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
436-
claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int Y ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )
485+
claim <k> runLemma ( maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 8 , X )
486+
claim <k> runLemma ( maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 16 , X )
487+
claim <k> runLemma ( maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 32 , X )
488+
claim <k> runLemma ( maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 64 , X )
489+
claim <k> runLemma ( maxUInt96 &Int ( X |Int ( notMaxUInt96 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 96 , X )
490+
claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
491+
claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
492+
claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
493+
claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
494+
claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
495+
claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
496+
claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )
437497

438498
claim <k> runLemma ( #buf ( 32 , #asWord ( X ) ) ) => doneLemma( X ) </k> requires lengthBytes(X) ==Int 32
439499
claim <k> runLemma ( #buf ( 32 , X <<Int 248 ) ) => doneLemma( #buf ( 1 , X ) +Bytes #buf ( 31 , 0 ) ) ... </k> requires #rangeUInt ( 8 , X )

0 commit comments

Comments
 (0)