From 180cf4f9058b83eacc160512edbbc80a2cd6c288 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 24 Mar 2020 17:26:04 +0000 Subject: [PATCH 01/22] Add #wrap rules corresponding to modInt Rules --- kwasm-lemmas.md | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 143b98ef6..253f81e78 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -35,14 +35,23 @@ Not however that K defines `X modInt N ==Int X modInt (-N)`. #### Rules for Expressions With Only Modulus +These are given in pure modulus form, and in form with `#wrap`, which is modulus with a power of 2. + ```k rule X modInt N => X requires 0 <=Int X andBool X X + requires 0 <=Int X + andBool X 0 [simplification] + + rule #wrap(0, _) => 0 + [simplification] ``` `modInt` selects the least non-negative representative of a congruence class modulo `N`. @@ -52,6 +61,10 @@ Not however that K defines `X modInt N ==Int X modInt (-N)`. requires M >Int 0 andBool M <=Int N [simplification] + + rule #wrap(N, #wrap(M, X)) => #wrap(M, X) + requires M <=Int N + [simplification] ``` Proof: @@ -66,6 +79,10 @@ Since 0 <= x mod m < m <= n, (x mod m) mod n = x mod m andBool N >Int 0 andBool M modInt N ==Int 0 [simplification] + + rule #wrap(N, #wrap(M, X)) => #wrap(N, X) + requires notBool (M <=Int N) + [simplification] ``` Proof: @@ -94,6 +111,14 @@ x = m * q + r, for a unique q and r s.t. 0 <= r < m andBool N >Int 0 andBool M modInt N ==Int 0 [simplification] + + rule #wrap(N, (X < #wrap(N, Y) + requires N <=Int M + [simplification] + + rule #wrap(N, Y +Int (X < #wrap(N, Y) + requires N <=Int M + [simplification] ``` Proof: @@ -115,6 +140,14 @@ x * m + y mod n = x * (k * n) + y mod n = y mod n andBool N >Int 0 andBool M modInt N ==Int 0 [simplification] + + rule #wrap(N, #wrap(M, X) +Int Y) => #wrap(N, X +Int Y) + requires N <=Int M + [simplification] + + rule #wrap(N, Y +Int #wrap(M, X)) => #wrap(N, X +Int Y) + requires N <=Int M + [simplification] ``` Proof: From af904923c1966f0cf3c28b70416ed8167b2871f1 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 24 Mar 2020 17:26:19 +0000 Subject: [PATCH 02/22] Fix existential variable --- tests/proofs/memory-symbolic-type-spec.k | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/proofs/memory-symbolic-type-spec.k b/tests/proofs/memory-symbolic-type-spec.k index edad99f04..42097d839 100644 --- a/tests/proofs/memory-symbolic-type-spec.k +++ b/tests/proofs/memory-symbolic-type-spec.k @@ -16,8 +16,8 @@ module MEMORY-SYMBOLIC-TYPE-SPEC BM ... - requires #chop( ADDR) ==K EA - andBool EA +Int #numBytes(ITYPE) <=Int SIZE *Int #pageSize() + requires #chop( ADDR) ==K ?EA + andBool ?EA +Int #numBytes(ITYPE) <=Int SIZE *Int #pageSize() andBool #isByteMap(BM) endmodule From 645ef9eec6feb7198e05c70bb63a64dabfc9b25b Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 24 Mar 2020 21:10:39 +0000 Subject: [PATCH 03/22] More wrapping rules --- kwasm-lemmas.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 253f81e78..2be04db37 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -334,6 +334,11 @@ They are non-trivial in their implementation, but the following should obviously andBool #isByteMap(BM) [simplification] + rule #wrap(8, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR) + requires notBool (WIDTH ==Int 0) + andBool #isByteMap(BM) + [simplification] + rule #getRange(BM, ADDR, WIDTH) => #get(BM, ADDR) requires WIDTH ==Int 1 [simplification] @@ -384,13 +389,16 @@ module WRC20-LEMMAS This conversion turns out to be helpful in this particular proof, but we don't want to apply it on all KWasm proofs. ```k - rule X /Int 256 => X >>Int 8 + rule X /Int 256 => X >>Int 8 [simplification] ``` TODO: The two `#get` theorems below theorems handle special cases in this proof, but we should be able to use some more general theorems to prove them. ```k rule (#get(BM, ADDR) +Int (X +Int Y)) modInt 256 => (#get(BM, ADDR) +Int ((X +Int Y) modInt 256)) modInt 256 [simplification] + + rule #wrap(8, #get(BM, ADDR) +Int (X +Int Y)) => #wrap(8, #get(BM, ADDR) +Int #wrap(8, X +Int Y)) [simplification] + rule (#get(BM, ADDR) +Int X) >>Int 8 => X >>Int 8 requires X modInt 256 ==Int 0 andBool #isByteMap(BM) [simplification] ``` @@ -421,6 +429,13 @@ Perhaps using `requires N ==Int 2 ^Int log2Int(N)`? andBool X =Int 8 [simplification] + + rule #wrap(N, (X +Int (Y < X +Int (#wrap(N, Y <=Int 8 + andBool 0 <=Int X + andBool X =Int 8 + [simplification] ``` TODO: The following theorem should be proven, and moved to the set of general lemmas. From ae5e70f5f9ec7a331a339dabec8a4c5dbce00192 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 24 Mar 2020 21:19:28 +0000 Subject: [PATCH 04/22] WIP: Add speed-up lemma Causes infinite loop, it seems, not actually a speed up. Not worth investigating, I think, at least for now. --- kwasm-lemmas.md | 67 +++++++++++++++++++++------------------ tests/proofs/wrc20-spec.k | 13 ++++++++ 2 files changed, 49 insertions(+), 31 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 2be04db37..d9d34487a 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -469,7 +469,8 @@ A module of shorthand commands for the WRC20 module. syntax Defns ::= "#wrc20Functions" syntax Defns ::= "#wrc20ReverseBytes" syntax TypeDecls ::= "#wrc20ReverseBytesTypeDecls" - // -------------------------------------------------- + syntax Instr ::= "#reverseLoop" + // ----------------------------------- rule #wrc20 => ( module #wrc20Body ) .EmptyStmts [macro] rule #wrc20Body => #wrc20Imports ++Defns #wrc20Functions [macro] @@ -648,36 +649,7 @@ A module of shorthand commands for the WRC20 module. rule #wrc20ReverseBytes => (func String2Identifier("$i64.reverse_bytes") #wrc20ReverseBytesTypeDecls local i64 i64 .ValTypes .LocalDecls block .TypeDecls - loop .TypeDecls - local.get 1 - i64.const 8 - i64.ge_u - br_if 1 - local.get 0 - i64.const 56 - local.get 1 - i64.const 8 - i64.mul - i64.sub - i64.shl - i64.const 56 - i64.shr_u - i64.const 56 - i64.const 8 - local.get 1 - i64.mul - i64.sub - i64.shl - local.get 2 - i64.add - local.set 2 - local.get 1 - i64.const 1 - i64.add - local.set 1 - br 0 - .EmptyStmts - end + #reverseLoop .EmptyStmts end local.get 2 @@ -686,6 +658,39 @@ A module of shorthand commands for the WRC20 module. .Defns [macro] + rule #reverseLoop + => loop .TypeDecls + local.get 1 + i64.const 8 + i64.ge_u + br_if 1 + local.get 0 + i64.const 56 + local.get 1 + i64.const 8 + i64.mul + i64.sub + i64.shl + i64.const 56 + i64.shr_u + i64.const 56 + i64.const 8 + local.get 1 + i64.mul + i64.sub + i64.shl + local.get 2 + i64.add + local.set 2 + local.get 1 + i64.const 1 + i64.add + local.set 1 + br 0 + .EmptyStmts + end + [macro] + syntax Defns ::= Defns "++Defns" Defns [function, functional] // ------------------------------------------------------------- rule .Defns ++Defns DS' => DS' diff --git a/tests/proofs/wrc20-spec.k b/tests/proofs/wrc20-spec.k index 77ed78a7c..08c559b49 100644 --- a/tests/proofs/wrc20-spec.k +++ b/tests/proofs/wrc20-spec.k @@ -55,4 +55,17 @@ module WRC20-SPEC andBool #get(BM, ADDR +Int 6) ==Int #get(?BM', ADDR +Int 1 ) andBool #get(BM, ADDR +Int 7) ==Int #get(?BM', ADDR +Int 0 ) + // This lemma speeds things up, by reducing the number of iterations we do through the loop. + rule #reverseLoop => br 0 ~> label [ .ValTypes ] { #reverseLoop } .ValStack ... + .ValStack + + (0 |-> ORIGINAL) + (1 |-> (X => X +Int 1)) + (2 |-> (SUM => #wrap(64, (#wrap(8, ORIGINAL >>Int (X *Int 8)) < + LD => LD +Int 1 + requires 0 <=Int X + andBool X Date: Wed, 1 Apr 2020 17:34:38 +0000 Subject: [PATCH 05/22] Clean up general lemmas --- kwasm-lemmas.md | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 7e92ea2a3..ee8fd09f7 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -35,7 +35,7 @@ Not however that K defines `X modInt N ==Int X modInt (-N)`. #### Rules for Expressions With Only Modulus -These are given in pure modulus form, and in form with `#wrap`, which is modulus with a power of 2. +These are given in pure modulus form, and in form with `#wrap`, which is modulus with a power of 2 for positive `N`. ```k rule X modInt N => X @@ -51,9 +51,6 @@ These are given in pure modulus form, and in form with `#wrap`, which is modulus rule X modInt 1 => 0 [simplification] - - rule #wrap(0, _) => 0 - [simplification] ``` `modInt` selects the least non-negative representative of a congruence class modulo `N`. @@ -115,12 +112,12 @@ x = m * q + r, for a unique q and r s.t. 0 <= r < m [simplification] rule #wrap(N, (X < #wrap(N, Y) - requires 0 <=Int N + requires 0 <=Int M andBool N <=Int M [simplification] rule #wrap(N, Y +Int (X < #wrap(N, Y) - requires 0 <=Int N + requires 0 <=Int M andBool N <=Int M [simplification] ``` @@ -149,7 +146,7 @@ x * m + y mod n = x * (k * n) + y mod n = y mod n requires N <=Int M [simplification] - rule #wrap(N, Y +Int #wrap(M, X)) => #wrap(N, X +Int Y) + rule #wrap(N, X +Int #wrap(M, Y)) => #wrap(N, X +Int Y) requires N <=Int M [simplification] ``` @@ -351,8 +348,9 @@ They are non-trivial in their implementation, but the following should obviously andBool #isByteMap(BM) [simplification] - rule #wrap(8, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR) - requires notBool (WIDTH ==Int 0) + rule #wrap(N, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR) + requires N ==Int 8 + andBool notBool (WIDTH ==Int 0) andBool #isByteMap(BM) [simplification] From 872f368a727a5d714913bd0af583aeb188e3cd90 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 1 Apr 2020 17:35:41 +0000 Subject: [PATCH 06/22] Start moving exact values in simplifications to side conditions --- kwasm-lemmas.md | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index ee8fd09f7..58f653bc4 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -423,16 +423,27 @@ This conversion turns out to be helpful in this particular proof, but we don't w TODO: The two `#get` theorems below theorems handle special cases in this proof, but we should be able to use some more general theorems to prove them. ```k - rule (#get(BM, ADDR) +Int (X +Int Y)) modInt 256 => (#get(BM, ADDR) +Int ((X +Int Y) modInt 256)) modInt 256 [simplification] + rule (#get(BM, ADDR) +Int (X +Int Y)) modInt N => (#get(BM, ADDR) +Int ((X +Int Y) modInt 256)) modInt 256 + requires N ==Int 256 + [simplification] - rule #wrap(8, #get(BM, ADDR) +Int (X +Int Y)) => #wrap(8, #get(BM, ADDR) +Int #wrap(8, X +Int Y)) [simplification] + rule #wrap(N, #get(BM, ADDR) +Int (X +Int Y)) => #wrap(8, #get(BM, ADDR) +Int #wrap(8, X +Int Y)) + requires N ==Int 8 + [simplification] - rule (#get(BM, ADDR) +Int X) >>Int 8 => X >>Int 8 requires X modInt 256 ==Int 0 andBool #isByteMap(BM) [simplification] + rule (#get(BM, ADDR) +Int X) >>Int N => X >>Int 8 + requires N ==Int 8 + andBool X modInt 256 ==Int 0 + andBool #isByteMap(BM) + [simplification] ``` TODO: The following theorems should be generalized and proven, and moved to the set of general lemmas. Perhaps using `requires N ==Int 2 ^Int log2Int(N)`? +TODO: Some of these have concrete integers on the LHS. +It's better to use a symbolic value and a side condition, e.g. `rule N => foo requires N ==Int 8`, because simplifications only apply when the LHS matches exactly. + ```k rule X *Int 256 >>Int N => (X >>Int (N -Int 8)) requires N >=Int 8 [simplification] From fc838b49f147699c277046fc94f2df32efe34c66 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 1 Apr 2020 17:35:54 +0000 Subject: [PATCH 07/22] Simplify modInts to #wraps --- kwasm-lemmas.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 58f653bc4..e21b9817d 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -414,10 +414,17 @@ module WRC20-LEMMAS imports KWASM-LEMMAS ``` -This conversion turns out to be helpful in this particular proof, but we don't want to apply it on all KWasm proofs. +TODO: Remove anything that uses `modInt 2^N` where `N` is 8, 16, 32 or 64 -- we simplify those. + +These conversions turns out to be helpful in this particular proof, but we don't want to apply it on all KWasm proofs. ```k - rule X /Int 256 => X >>Int 8 [simplification] + rule X modInt N => #wrap( 8, X) requires N ==Int 256 [simplification] + rule X modInt N => #wrap(16, X) requires N ==Int 65536 [simplification] + rule X modInt N => #wrap(32, X) requires N ==Int #pow(i32) [simplification] + rule X modInt N => #wrap(64, X) requires N ==Int #pow(i64) [simplification] + + rule X /Int N => X >>Int 8 requires N ==Int 256 [simplification] ``` TODO: The two `#get` theorems below theorems handle special cases in this proof, but we should be able to use some more general theorems to prove them. From 319b6f1368e573e38ec237b0af8020bd766422c2 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 2 Apr 2020 14:30:58 +0000 Subject: [PATCH 08/22] Bugfix: missing syntax production --- kwasm-lemmas.md | 1 + 1 file changed, 1 insertion(+) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index e21b9817d..324cc5e26 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -514,6 +514,7 @@ A module of shorthand commands for the WRC20 module. syntax Defns ::= "#wrc20Imports" syntax Defns ::= "#wrc20Functions_fastBalance" syntax Defns ::= "#wrc20ReverseBytes" + syntax Instr ::= "#reverseLoop" syntax TypeDecls ::= "#wrc20ReverseBytesTypeDecls" // --------------------------------------------------- rule #wrc20 => ( module #wrc20Body ) [macro] From 9088ebb54b767ef478dee6eb116b485f377683cb Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 2 Apr 2020 14:31:13 +0000 Subject: [PATCH 09/22] Make setRange total --- data.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/data.md b/data.md index 84edc81d8..504cb0426 100644 --- a/data.md +++ b/data.md @@ -502,8 +502,8 @@ However, `ByteMap` is just a wrapper around regular `Map`s. `#setRange(BM, START, VAL, WIDTH)` writes the integer `I` to memory as bytes (little-endian), starting at index `N`. ```k - syntax ByteMap ::= #setRange(ByteMap, Int, Int, Int) [function] - // --------------------------------------------------------------- + syntax ByteMap ::= #setRange(ByteMap, Int, Int, Int) [function, functional, smtlib(setRange)] + // --------------------------------------------------------------------------------------------- rule #setRange(BM, _, _, WIDTH) => BM requires notBool (WIDTH >Int 0) rule #setRange(BM, IDX, VAL, WIDTH) => #setRange(#set(BM, IDX, VAL modInt 256), IDX +Int 1, VAL /Int 256, WIDTH -Int 1) From eae41fabe1f23612c3c192372e2e0010e5ad01a7 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 2 Apr 2020 14:31:42 +0000 Subject: [PATCH 10/22] New #getRange lemmas --- kwasm-lemmas.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 324cc5e26..6b517ea26 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -348,6 +348,10 @@ They are non-trivial in their implementation, but the following should obviously andBool #isByteMap(BM) [simplification] + rule #getRange(BM, ADDR, WIDTH) => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) + requires #get(BM, ADDR) ==Int 0 + andBool WIDTH >Int 0 + rule #wrap(N, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR) requires N ==Int 8 andBool notBool (WIDTH ==Int 0) @@ -359,6 +363,21 @@ They are non-trivial in their implementation, but the following should obviously [simplification] ``` +`#getRange` over `#setRange` + +```k + rule #getRange(#setRange(BM, EA, VALUE, SET_WIDTH), EA, GET_WIDTH) + => #wrap(GET_WIDTH *Int 8, VALUE) + requires GET_WIDTH <=Int SET_WIDTH + [simplification] + + rule #getRange(#setRange(BM, EA, VALUE, SET_WIDTH), EA, GET_WIDTH) + => #wrap(SET_WIDTH *Int 8, VALUE) + +Int (#getRange(BM, EA +Int SET_WIDTH, GET_WIDTH -Int SET_WIDTH) < Date: Thu, 9 Apr 2020 16:12:27 +0000 Subject: [PATCH 11/22] Formatting --- kwasm-lemmas.md | 6 ++---- tests/proofs/wrc20-spec.k | 6 ------ 2 files changed, 2 insertions(+), 10 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 6b517ea26..c7581296d 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -433,13 +433,11 @@ module WRC20-LEMMAS imports KWASM-LEMMAS ``` -TODO: Remove anything that uses `modInt 2^N` where `N` is 8, 16, 32 or 64 -- we simplify those. - These conversions turns out to be helpful in this particular proof, but we don't want to apply it on all KWasm proofs. ```k - rule X modInt N => #wrap( 8, X) requires N ==Int 256 [simplification] - rule X modInt N => #wrap(16, X) requires N ==Int 65536 [simplification] + rule X modInt N => #wrap( 8, X) requires N ==Int 256 [simplification] + rule X modInt N => #wrap(16, X) requires N ==Int 65536 [simplification] rule X modInt N => #wrap(32, X) requires N ==Int #pow(i32) [simplification] rule X modInt N => #wrap(64, X) requires N ==Int #pow(i64) [simplification] diff --git a/tests/proofs/wrc20-spec.k b/tests/proofs/wrc20-spec.k index 08c559b49..6262c93c0 100644 --- a/tests/proofs/wrc20-spec.k +++ b/tests/proofs/wrc20-spec.k @@ -5,11 +5,6 @@ requires "kwasm-lemmas.k" module WRC20-SPEC imports WRC20-LEMMAS - // Main spec. - // There is no specified behavior yet, so this claim is commented out. - // - // rule #wrc20 - // Reverse bytes spec. rule #wrc20ReverseBytes // TODO: Have this pre-loaded in the store. @@ -44,7 +39,6 @@ module WRC20-SPEC requires notBool unnameFuncType(asFuncType(#wrc20ReverseBytesTypeDecls)) in values(TYPES) andBool ADDR +Int #numBytes(i64) <=Int SIZE *Int #pageSize() andBool #isByteMap(BM) -// andBool #inUnsignedRange(i64, X) X is not bound in the LHS andBool #inUnsignedRange(i32, ADDR) ensures #get(BM, ADDR +Int 0) ==Int #get(?BM', ADDR +Int 7 ) andBool #get(BM, ADDR +Int 1) ==Int #get(?BM', ADDR +Int 6 ) From 5d9b041c0e3fe77c07a3c49240c9b555f5cd4db2 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 9 Apr 2020 16:12:44 +0000 Subject: [PATCH 12/22] Remove the loop-lemma, not giving any speed-up --- kwasm-lemmas.md | 65 ++++++++++++++++++--------------------- tests/proofs/wrc20-spec.k | 13 -------- 2 files changed, 30 insertions(+), 48 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index c7581296d..e8827a361 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -531,7 +531,6 @@ A module of shorthand commands for the WRC20 module. syntax Defns ::= "#wrc20Imports" syntax Defns ::= "#wrc20Functions_fastBalance" syntax Defns ::= "#wrc20ReverseBytes" - syntax Instr ::= "#reverseLoop" syntax TypeDecls ::= "#wrc20ReverseBytesTypeDecls" // --------------------------------------------------- rule #wrc20 => ( module #wrc20Body ) [macro] @@ -711,7 +710,36 @@ A module of shorthand commands for the WRC20 module. rule #wrc20ReverseBytes => (func String2Identifier("$i64.reverse_bytes") #wrc20ReverseBytesTypeDecls local i64 i64 .ValTypes .LocalDecls block .TypeDecls - #reverseLoop + loop .TypeDecls + local.get 1 + i64.const 8 + i64.ge_u + br_if 1 + local.get 0 + i64.const 56 + local.get 1 + i64.const 8 + i64.mul + i64.sub + i64.shl + i64.const 56 + i64.shr_u + i64.const 56 + i64.const 8 + local.get 1 + i64.mul + i64.sub + i64.shl + local.get 2 + i64.add + local.set 2 + local.get 1 + i64.const 1 + i64.add + local.set 1 + br 0 + .EmptyStmts + end .EmptyStmts end local.get 2 @@ -720,39 +748,6 @@ A module of shorthand commands for the WRC20 module. .Defns [macro] - rule #reverseLoop - => loop .TypeDecls - local.get 1 - i64.const 8 - i64.ge_u - br_if 1 - local.get 0 - i64.const 56 - local.get 1 - i64.const 8 - i64.mul - i64.sub - i64.shl - i64.const 56 - i64.shr_u - i64.const 56 - i64.const 8 - local.get 1 - i64.mul - i64.sub - i64.shl - local.get 2 - i64.add - local.set 2 - local.get 1 - i64.const 1 - i64.add - local.set 1 - br 0 - .EmptyStmts - end - [macro] - syntax Defns ::= Defns "++Defns" Defns [function, functional] // ------------------------------------------------------------- rule .Defns ++Defns DS' => DS' diff --git a/tests/proofs/wrc20-spec.k b/tests/proofs/wrc20-spec.k index 6262c93c0..e7199bccc 100644 --- a/tests/proofs/wrc20-spec.k +++ b/tests/proofs/wrc20-spec.k @@ -49,17 +49,4 @@ module WRC20-SPEC andBool #get(BM, ADDR +Int 6) ==Int #get(?BM', ADDR +Int 1 ) andBool #get(BM, ADDR +Int 7) ==Int #get(?BM', ADDR +Int 0 ) - // This lemma speeds things up, by reducing the number of iterations we do through the loop. - rule #reverseLoop => br 0 ~> label [ .ValTypes ] { #reverseLoop } .ValStack ... - .ValStack - - (0 |-> ORIGINAL) - (1 |-> (X => X +Int 1)) - (2 |-> (SUM => #wrap(64, (#wrap(8, ORIGINAL >>Int (X *Int 8)) < - LD => LD +Int 1 - requires 0 <=Int X - andBool X Date: Thu, 9 Apr 2020 16:29:56 +0000 Subject: [PATCH 13/22] Formatting --- data.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/data.md b/data.md index 504cb0426..08733f5bf 100644 --- a/data.md +++ b/data.md @@ -270,7 +270,7 @@ The `#wrap` function wraps an integer to a given bit width. ```k syntax IVal ::= #chop ( IVal ) [function, functional] - // ----------------------------------------- + // ----------------------------------------------------- rule #chop(< ITYPE > N) => < ITYPE > (N modInt #pow(ITYPE)) syntax Int ::= #wrap(Int, Int) [function, functional] From 5b31383c18b38e2365a873b8dd899491fd6135ac Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 15 Apr 2020 15:36:51 +0000 Subject: [PATCH 14/22] Documentation update --- kwasm-lemmas.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index e8827a361..1ddeaed0b 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -464,9 +464,8 @@ TODO: The two `#get` theorems below theorems handle special cases in this proof, TODO: The following theorems should be generalized and proven, and moved to the set of general lemmas. Perhaps using `requires N ==Int 2 ^Int log2Int(N)`? - -TODO: Some of these have concrete integers on the LHS. -It's better to use a symbolic value and a side condition, e.g. `rule N => foo requires N ==Int 8`, because simplifications only apply when the LHS matches exactly. +Also, some of these have concrete integers on the LHS. +It may be better to use a symbolic value as a side condition, e.g. `rule N => foo requires N ==Int 8`, because simplifications rely on exact matching of the LHS. ```k rule X *Int 256 >>Int N => (X >>Int (N -Int 8)) requires N >=Int 8 [simplification] From 53032a459e33d836f221553b5d98becc3f1349a3 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 15 Apr 2020 18:36:37 +0000 Subject: [PATCH 15/22] Remove unused and bad lemma, caused branching --- kwasm-lemmas.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 1ddeaed0b..d66a78465 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -348,9 +348,9 @@ They are non-trivial in their implementation, but the following should obviously andBool #isByteMap(BM) [simplification] - rule #getRange(BM, ADDR, WIDTH) => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) - requires #get(BM, ADDR) ==Int 0 - andBool WIDTH >Int 0 +// rule #getRange(BM, ADDR, WIDTH) => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) +// requires #get(BM, ADDR) ==Int 0 +// andBool WIDTH >Int 0 rule #wrap(N, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR) requires N ==Int 8 From cf5772245d82fede84b77d7d79f634a1ecf6c2b0 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Wed, 15 Apr 2020 18:36:57 +0000 Subject: [PATCH 16/22] Nits --- kwasm-lemmas.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index d66a78465..8e108569e 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -343,8 +343,9 @@ They are non-trivial in their implementation, but the following should obviously requires WIDTH ==Int 1 [simplification] - rule #getRange(BM, ADDR, WIDTH) modInt 256 => #get(BM, ADDR) - requires notBool (WIDTH ==Int 0) + rule #getRange(BM, ADDR, WIDTH) modInt BYTE_SIZE => #get(BM, ADDR) + requires BYTE_SIZE ==Int 256 + andBool notBool (WIDTH ==Int 0) andBool #isByteMap(BM) [simplification] @@ -459,7 +460,7 @@ TODO: The two `#get` theorems below theorems handle special cases in this proof, requires N ==Int 8 andBool X modInt 256 ==Int 0 andBool #isByteMap(BM) - [simplification] + [simplification] ``` TODO: The following theorems should be generalized and proven, and moved to the set of general lemmas. From 9e584abfe6c043596e03039d38a5de042fbda926 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 11:29:13 +0000 Subject: [PATCH 17/22] Update lemmas --- kwasm-lemmas.md | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 8e108569e..57d684baa 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -169,10 +169,14 @@ x mod m + y = r + y We want K to understand what a bit-shift is. ```k - rule (X < true + rule (X < 0 requires M modInt (2 ^Int N) ==Int 0 [simplification] + rule #wrap(M, X < 0 + requires M <=Int N + [simplification] + rule (X >>Int N) => 0 requires X 0 requires M #wrap( 8, X) requires N ==Int 256 [simplification] - rule X modInt N => #wrap(16, X) requires N ==Int 65536 [simplification] - rule X modInt N => #wrap(32, X) requires N ==Int #pow(i32) [simplification] - rule X modInt N => #wrap(64, X) requires N ==Int #pow(i64) [simplification] - rule X /Int N => X >>Int 8 requires N ==Int 256 [simplification] ``` From 03cfb324087ec9376fde7f8c8ea850ca4ad8f0f5 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 13:05:47 +0000 Subject: [PATCH 18/22] Fix side condition --- kwasm-lemmas.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 57d684baa..327d93f35 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -170,7 +170,7 @@ We want K to understand what a bit-shift is. ```k rule (X < 0 - requires M modInt (2 ^Int N) ==Int 0 + requires (2 ^Int N) modInt M ==Int 0 [simplification] rule #wrap(M, X < 0 From 013e6c48d96fff8e0fb34059814d274ac511114b Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Thu, 16 Apr 2020 15:49:24 +0000 Subject: [PATCH 19/22] Remove commented out lemma --- kwasm-lemmas.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 327d93f35..38608dd19 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -353,10 +353,6 @@ They are non-trivial in their implementation, but the following should obviously andBool #isByteMap(BM) [simplification] -// rule #getRange(BM, ADDR, WIDTH) => #getRange(BM, ADDR +Int 1, WIDTH -Int 1) -// requires #get(BM, ADDR) ==Int 0 -// andBool WIDTH >Int 0 - rule #wrap(N, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR) requires N ==Int 8 andBool notBool (WIDTH ==Int 0) From 3172a96f3891fbdf2d3fe23cdbe31d2906206b7d Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 21 Apr 2020 14:32:23 +0000 Subject: [PATCH 20/22] Specilalize #getRange lemma --- kwasm-lemmas.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 38608dd19..57d89fa33 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -374,9 +374,11 @@ They are non-trivial in their implementation, but the following should obviously rule #getRange(#setRange(BM, EA, VALUE, SET_WIDTH), EA, GET_WIDTH) => #wrap(SET_WIDTH *Int 8, VALUE) - +Int (#getRange(BM, EA +Int SET_WIDTH, GET_WIDTH -Int SET_WIDTH) <, _, _) => 0 [simplification] ``` `#get` over `#setRange`. From 62a6c3ad0fd8f76c7d447507e909b7100c2fc0fa Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 21 Apr 2020 14:44:10 +0000 Subject: [PATCH 21/22] Fix getRange side conditions for when WIDTH <= 0 --- kwasm-lemmas.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 57d89fa33..ff7d38bcd 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -349,13 +349,13 @@ They are non-trivial in their implementation, but the following should obviously rule #getRange(BM, ADDR, WIDTH) modInt BYTE_SIZE => #get(BM, ADDR) requires BYTE_SIZE ==Int 256 - andBool notBool (WIDTH ==Int 0) + andBool notBool (WIDTH <=Int 0) andBool #isByteMap(BM) [simplification] rule #wrap(N, #getRange(BM, ADDR, WIDTH)) => #get(BM, ADDR) requires N ==Int 8 - andBool notBool (WIDTH ==Int 0) + andBool notBool (WIDTH <=Int 0) andBool #isByteMap(BM) [simplification] From e9e90b78c741370c1cbd22eb22be7b4f3d728fc0 Mon Sep 17 00:00:00 2001 From: hjorthjort Date: Tue, 21 Apr 2020 15:21:58 +0000 Subject: [PATCH 22/22] Typo in annotation --- kwasm-lemmas.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kwasm-lemmas.md b/kwasm-lemmas.md index 7248bebbf..ef3dd3a70 100644 --- a/kwasm-lemmas.md +++ b/kwasm-lemmas.md @@ -375,7 +375,7 @@ They are non-trivial in their implementation, but the following should obviously => #wrap(SET_WIDTH *Int 8, VALUE) requires (notBool GET_WIDTH <=Int SET_WIDTH) andBool #getRange(BM, EA +Int SET_WIDTH, GET_WIDTH -Int SET_WIDTH) ==Int 0 - [simplificaton] + [simplification] rule #getRange(ByteMap <| .Map |>, _, _) => 0 [simplification] ```