Lemmas and symbolic execution improvements

package/version

@@ -1 +1 @@
-0.1.57
+0.1.58

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "komet"
-version = "0.1.57"
+version = "0.1.58"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/komet/kasmer.py

@@ -10,7 +10,7 @@
 
 from hypothesis import strategies
 from pyk.cterm import CTerm, cterm_build_claim
-from pyk.kast.inner import KSort, KVariable
+from pyk.kast.inner import KSequence, KSort, KVariable
 from pyk.kast.manip import Subst, split_config_from
 from pyk.kast.outer import KClaim
 from pyk.konvert import kast_to_kore, kore_to_kast
@@ -284,11 +284,12 @@ def make_steps(*args: KInner) -> KInner:
         lhs_subst['ALWAYSALLOCATE_CELL'] = token(always_allocate)
         lhs = CTerm(Subst(lhs_subst).apply(conf), [mlEqualsTrue(c) for c in ctrs])
 
-        rhs_subst = subst.copy()
-        rhs_subst['PROGRAM_CELL'] = STEPS_TERMINATOR
-        rhs_subst['EXITCODE_CELL'] = token(0)
-        del rhs_subst['LOGGING_CELL']
-        del rhs_subst['ALWAYSALLOCATE_CELL']
+        # Expect the root contract call to terminate successfully while allowing changes to the blockchain state
+        rhs_subst = {
+            'PROGRAM_CELL': STEPS_TERMINATOR,
+            'EXITCODE_CELL': token(0),
+            'K_CELL': KSequence(),
+        }
         rhs = CTerm(Subst(rhs_subst).apply(conf))
 
         claim, _ = cterm_build_claim(name, lhs, rhs)

src/komet/kdist/soroban-semantics/auto-allocate.md

@@ -18,10 +18,19 @@ module WASM-AUTO-ALLOCATE
 
     syntax Stmt ::= "newEmptyModule" WasmString
  // -------------------------------------------
-    rule <instrs> newEmptyModule MODNAME => .K ... </instrs>
+
+    rule [newEmptyModule-trap]:
+        <instrs> newEmptyModule _MODNAME => trap ... </instrs>
+        <nextModuleIdx> NEXT </nextModuleIdx>
+        <moduleInst> <modIdx> NEXT </modIdx> ... </moduleInst>
+      [priority(10)]
+
+    rule [newEmptyModule]:
+         <instrs> newEmptyModule MODNAME => .K ... </instrs>
          <moduleRegistry> MR => MR [ MODNAME <- NEXT ] </moduleRegistry>
          <nextModuleIdx> NEXT => NEXT +Int 1 </nextModuleIdx>
          <moduleInstances> ( .Bag => <moduleInst> <modIdx> NEXT </modIdx> ... </moduleInst>) ... </moduleInstances>
+      [preserves-definedness]
 
     syntax Stmts ::=  autoAllocModules ( ModuleDecl, Map ) [function]
                    | #autoAllocModules ( Defns     , Map ) [function]

src/komet/kdist/soroban-semantics/configuration.md

@@ -242,7 +242,7 @@ If `SCV` is a small value, `allocObject(SCV)` returns a small `HostVal` directly
         <hostStack> STACK => toSmall(SCV) : STACK </hostStack>
         <alwaysAllocate> ALWAYS_ALLOCATE </alwaysAllocate>
       requires alwaysSmall(SCV)
-        orBool ( toSmallValid(SCV) andBool notBool ALWAYS_ALLOCATE )
+        orBool ( isSmall(SCV) andBool notBool ALWAYS_ALLOCATE )
 
     // recursively allocate vector items
     rule [allocObject-vec]:

src/komet/kdist/soroban-semantics/data.md

@@ -102,40 +102,44 @@ module HOST-OBJECT
     imports HOST-OBJECT-SYNTAX
     imports WASM
 
+    syntax Int ::= unwrap(HostVal)    [function, total, symbol(HostVal:unwrap)]
+ // ---------------------------------------------------
+    rule unwrap(HostVal(I)) => I
+
     syntax Int ::= getMajor(HostVal)        [function, total, symbol(getMajor)]
                  | getMinor(HostVal)        [function, total, symbol(getMinor)]
                  | getTag(HostVal)          [function, total, symbol(getTag)]
                  | getBody(HostVal)         [function, total, symbol(getBody)]
  // -----------------------------------------------------------------------
-    rule getMajor(HostVal(I)) => I >>Int 32
-    rule getMinor(HostVal(I)) => (I &Int (#pow(i32) -Int 1)) >>Int 8
-    rule getTag(HostVal(I))   => I &Int 255
-    rule getBody(HostVal(I))  => I >>Int 8
+    rule getMajor(HostVal(I)) => I >>Int 32                            [concrete]
+    rule getMinor(HostVal(I)) => (I &Int (#pow(i32) -Int 1)) >>Int 8   [concrete]
+    rule getTag(HostVal(I))   => I &Int 255                            [concrete]
+    rule getBody(HostVal(I))  => I >>Int 8                             [concrete]
 
     syntax Bool ::= isObject(HostVal)                   [function, total, symbol(isObject)]
                   | isObjectTag(Int)                    [function, total, symbol(isObjectTag)]
                   | isRelativeObjectHandle(HostVal)     [function, total, symbol(isRelativeObjectHandle)]
  // --------------------------------------------------------------------------------
     rule isObject(V)               => isObjectTag(getTag(V))
-    rule isObjectTag(TAG)          => 64 <=Int TAG andBool TAG <=Int 77
+    rule isObjectTag(TAG)          => 64 <=Int TAG andBool TAG <=Int 77    [concrete]
     rule isRelativeObjectHandle(V) => getMajor(V) &Int 1 ==Int 0
 
     syntax Int ::= indexToHandle(Int, Bool)       [function, total, symbol(indexToHandle)]
  // --------------------------------------------------------------------------------
-    rule indexToHandle(I, false) => (I <<Int 1) |Int 1
-    rule indexToHandle(I, true)  =>  I <<Int 1
+    rule indexToHandle(I, false) => (I <<Int 1) |Int 1             [concrete]
+    rule indexToHandle(I, true)  =>  I <<Int 1                     [concrete]
 
     syntax Int ::= getIndex(HostVal)   [function, total, symbol(getIndex)]
  // ----------------------------------------------------------------------------
-    rule getIndex(V) => getMajor(V) >>Int 1
+    rule getIndex(V) => getMajor(V) >>Int 1                     [concrete]
 
     syntax HostVal ::= fromHandleAndTag(Int, Int)                [function, total, symbol(fromHandleAndTag)]
                      | fromMajorMinorAndTag(Int, Int, Int)       [function, total, symbol(fromMajorMinorAndTag)]
                      | fromBodyAndTag(Int, Int)                  [function, total, symbol(fromBodyAndTag)]
  // --------------------------------------------------------------------------------
     rule fromHandleAndTag(H, T)              => fromMajorMinorAndTag(H, 0, T)
-    rule fromMajorMinorAndTag(MAJ, MIN, TAG) => fromBodyAndTag((MAJ <<Int 24) |Int MIN, TAG)
-    rule fromBodyAndTag(BODY, TAG)           => HostVal((BODY <<Int 8) |Int TAG)
+    rule fromMajorMinorAndTag(MAJ, MIN, TAG) => fromBodyAndTag((MAJ <<Int 24) |Int MIN, TAG)    [concrete]
+    rule fromBodyAndTag(BODY, TAG)           => HostVal((BODY <<Int 8) |Int TAG)                [concrete]
 
     syntax WasmStringToken ::= #unparseWasmString ( String )         [function, total, hook(STRING.string2token)]
                              | #quoteUnparseWasmString ( String )   [function, total]
@@ -144,26 +148,26 @@ module HOST-OBJECT
   // https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#tag-values
     syntax Int ::= getTag(ScVal)   [function, total]
  // -----------------------------------------------------
-    rule getTag(SCBool(false)) => 0
-    rule getTag(SCBool(true))  => 1
-    rule getTag(Void)          => 2
-    rule getTag(Error(_,_))    => 3
-    rule getTag(U32(_))        => 4
-    rule getTag(I32(_))        => 5
-    rule getTag(U64(I))        => 6     requires          I <=Int #maxU64small
-    rule getTag(U64(I))        => 64    requires notBool( I <=Int #maxU64small )
-    rule getTag(I64(I))        => 7     requires          #minI64small <=Int I andBool I <=Int #maxI64small
-    rule getTag(I64(I))        => 65    requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small )
-    rule getTag(U128(I))       => 10    requires          I <=Int #maxU64small
-    rule getTag(U128(I))       => 68    requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width
-    rule getTag(I128(I))       => 11    requires          #minI64small <=Int I andBool I <=Int #maxI64small
-    rule getTag(I128(I))       => 69    requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small )
-    rule getTag(ScVec(_))      => 75
-    rule getTag(ScMap(_))      => 76
-    rule getTag(ScAddress(_))  => 77
-    rule getTag(Symbol(BS))    => 14    requires lengthString(BS) <=Int 9
-    rule getTag(Symbol(BS))    => 74    requires lengthString(BS) >Int  9
-    rule getTag(ScBytes(_))    => 72
+    rule getTag(SCBool(false))   => 0
+    rule getTag(SCBool(true))    => 1
+    rule getTag(Void)            => 2
+    rule getTag(Error(_,_))      => 3
+    rule getTag(U32(_))          => 4
+    rule getTag(I32(_))          => 5
+    rule getTag(U64(_)  #as X)   => 6     requires         isSmall(X)
+    rule getTag(U64(_)  #as X)   => 64    requires notBool isSmall(X)
+    rule getTag(I64(_)  #as X)   => 7     requires         isSmall(X)
+    rule getTag(I64(_)  #as X)   => 65    requires notBool isSmall(X)
+    rule getTag(U128(_) #as X)   => 10    requires         isSmall(X)
+    rule getTag(U128(_) #as X)   => 68    requires notBool isSmall(X)
+    rule getTag(I128(_) #as X)   => 11    requires         isSmall(X)
+    rule getTag(I128(_) #as X)   => 69    requires notBool isSmall(X)
+    rule getTag(ScVec(_))        => 75
+    rule getTag(ScMap(_))        => 76
+    rule getTag(ScAddress(_))    => 77
+    rule getTag(Symbol(_) #as X) => 14    requires         isSmall(X)
+    rule getTag(Symbol(_) #as X) => 74    requires notBool isSmall(X)
+    rule getTag(ScBytes(_))      => 72
 
     syntax Int ::= getTagWithFlag(alwaysAllocate: Bool, ScVal)   [function, total]
  // -------------------------------------------------------------------------------
@@ -173,7 +177,7 @@ module HOST-OBJECT
     rule getTagWithFlag(true, I128(_))   => 69
     rule getTagWithFlag(true, Symbol(_)) => 74
     rule getTagWithFlag(_,    SCV)       => getTag(SCV)      [owise]
-   
+
     // 64-bit integers that fit in 56 bits
     syntax Int ::= "#maxU64small"     [macro]
                  | "#maxI64small"     [macro]
@@ -273,28 +277,38 @@ module HOST-OBJECT
 
     syntax HostVal ::= toSmall(ScVal)      [function, total, symbol(toSmall)]
  // ---------------------------------------------------------------------------------
-    rule toSmall(SCBool(false)) => fromMajorMinorAndTag(0, 0, 0)
-    rule toSmall(SCBool(true))  => fromMajorMinorAndTag(0, 0, 1)
-    rule toSmall(Void)          => fromMajorMinorAndTag(0, 0, 2)
-    rule toSmall(Error(TYP, I)) => fromMajorMinorAndTag(I, ErrorType2Int(TYP), 3)
-    rule toSmall(U32(I))        => fromMajorMinorAndTag(I, 0, 4)
-    rule toSmall(I32(I))        => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5)
+    rule toSmall(SCBool(false))   => fromMajorMinorAndTag(0, 0, 0)
+    rule toSmall(SCBool(true))    => fromMajorMinorAndTag(0, 0, 1)
+    rule toSmall(Void)            => fromMajorMinorAndTag(0, 0, 2)
+    rule toSmall(Error(TYP, I))   => fromMajorMinorAndTag(I, ErrorType2Int(TYP), 3)
+    rule toSmall(U32(I))          => fromMajorMinorAndTag(I, 0, 4)
+    rule toSmall(I32(I))          => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5)
       requires definedUnsigned(i32, I)
-    rule toSmall(U64(I))        => fromBodyAndTag(I, 6)               requires I <=Int #maxU64small
-    rule toSmall(I64(I))        => fromBodyAndTag(#unsigned(i56, I), 7)
-      requires #minI64small <=Int I andBool I <=Int #maxI64small
-       andBool definedUnsigned(i56, I)
-    rule toSmall(U128(I))       => fromBodyAndTag(I, 10)              requires I <=Int #maxU64small
-    rule toSmall(I128(I))       => fromBodyAndTag(#unsigned(i56, I), 11)
-      requires #minI64small <=Int I andBool I <=Int #maxI64small
-       andBool definedUnsigned(i56, I)
-    rule toSmall(Symbol(S))     => fromBodyAndTag(encode6bit(S), 14)  requires lengthString(S) <=Int 9
-    rule toSmall(_)             => HostVal(-1)                        [owise]
-
-    syntax Bool ::= toSmallValid(ScVal)
-        [function, total, symbol(toSmallValid)]
- // ---------------------------------------------------------------------------------
-    rule toSmallValid(VAL) => toSmall(VAL) =/=K HostVal(-1)
+    rule toSmall(U64(I) #as X)    => fromBodyAndTag(I, 6)                  requires isSmall(X)
+    rule toSmall(I64(I) #as X)    => fromBodyAndTag(#unsigned(i56, I), 7)  requires isSmall(X)
+    rule toSmall(U128(I) #as X)   => fromBodyAndTag(I, 10)                 requires isSmall(X)
+    rule toSmall(I128(I) #as X)   => fromBodyAndTag(#unsigned(i56, I), 11) requires isSmall(X)
+    rule toSmall(Symbol(S) #as X) => fromBodyAndTag(encode6bit(S), 14)     requires isSmall(X)
+    rule toSmall(_)               => HostVal(-1)                           [owise]
+
+    syntax Bool ::= isSmall(ScVal)       [function, total, symbol(isSmall)]
+ // -----------------------------------------------------------------------
+    rule isSmall(SCBool(_))   => true
+    rule isSmall(Void)        => true
+    rule isSmall(Error(_, _)) => true
+    rule isSmall(U32(_))      => true
+    rule isSmall(I32(_))      => true
+    rule isSmall(U64(I))      => isSmallInt(Unsigned, I)
+    rule isSmall(I64(I))      => isSmallInt(Signed, I)
+    rule isSmall(U128(I))     => isSmallInt(Unsigned, I)
+    rule isSmall(I128(I))     => isSmallInt(Signed, I)
+    rule isSmall(Symbol(S))   => lengthString(S) <=Int 9
+    rule isSmall(_)           => false                        [owise]
+
+    syntax Bool ::= isSmallInt(Signedness, Int)    [function, total, symbol(isSmallInt)]
+ // ------------------------------------------------------------------------
+    rule isSmallInt(Unsigned, I) => 0 <=Int I andBool I <Int #pow(i56)
+    rule isSmallInt(Signed,   I) => 0 -Int #pow1(i56) <=Int I andBool I <Int #pow1(i56)
 
     syntax Bool ::= alwaysSmall(ScVal)
         [function, total, symbol(alwaysSmall)]

src/komet/kdist/soroban-semantics/host/integer.md

@@ -20,8 +20,8 @@ module HOST-INTEGER
       [preserves-definedness] // definedness of '#unsigned(,)' is checked
 
     rule [returnHostVal]:
-        <instrs> returnHostVal => i64.const I ... </instrs>
-        <hostStack> HostVal(I) : S => S </hostStack>
+        <instrs> returnHostVal => HV ... </instrs>
+        <hostStack> HV:HostVal : S => S </hostStack>
 
     rule [hostfun-obj-to-u64]:
         <instrs> hostCall ( "i" , "0" , [ i64  .ValTypes ] -> [ i64  .ValTypes ] )

src/komet/kdist/soroban-semantics/komet-lemmas.md

@@ -7,9 +7,10 @@ module KSOROBAN-LEMMAS [symbolic]
   imports INT-BITWISE-LEMMAS
   imports HOST-OBJECT-LEMMAS
   imports SOROBAN
+  imports MAP-SYMBOLIC
 
   syntax InternalCmd ::= runLemma(ProofStep) | doneLemma(ProofStep)
-  syntax ProofStep ::= HostVal | ScVal | Int | Bool
+  syntax ProofStep ::= HostVal | ScVal | Int | Bool | Val
 
   rule <k> runLemma(S) => doneLemma(S) ... </k>
 
@@ -26,35 +27,48 @@ module INT-BITWISE-LEMMAS [symbolic]
   rule (A &Int  B) &Int C  =>  A &Int (B  &Int C) [simplification, concrete(B, C)]
   rule  A &Int (B  &Int C) => (A &Int  B) &Int C  [simplification, symbolic(A, B)]
 
-  syntax Bool ::= isPowerOf2(Int)  [function, total]
+  syntax Bool ::= isPowerOf2(Int)  [function, total, symbol(isPowerOf2)]
   rule isPowerOf2(I:Int) => I ==Int 1 <<Int log2Int(I) requires 0 <Int I
   rule isPowerOf2(I:Int) => false                      requires I <=Int 0
 
-  syntax Bool ::= isFullMask(Int)  [function, total]
+  syntax Bool ::= isFullMask(Int)  [function, total, symbol(isFullMask)]
   rule isFullMask(I:Int) => I ==Int fullMask(log2Int(I) +Int 1) requires 0 <Int I
   rule isFullMask(I:Int) => false                               requires I <=Int 0
 
-  syntax Int ::= fullMask(Int) [function, total]
+  syntax Int ::= fullMask(Int) [function, total, symbol(fullMask)]
   rule fullMask(I:Int) => (1 <<Int I) -Int 1 requires 0 <Int I
   rule fullMask(I:Int) => 0                  requires I <=Int 0
 
   rule [modInt-to-bit-mask]:
-      I modInt M => I &Int (M -Int 1) requires isPowerOf2(M)
-    [simplification, concrete(M)]
+      I modInt M => I &Int (M -Int 1) requires isPowerOf2(M) andBool 0 <=Int I
+    [simplification, concrete(M), preserves-definedness]
 
 endmodule
 
-module HOST-OBJECT-LEMMAS [symbolic]
+module HOST-OBJECT-LEMMA-HELPERS [symbolic]
   imports HOST-OBJECT
   imports INT-BITWISE-LEMMAS
 
+  syntax Bool ::= isTag(Int)      [function, total, symbol(isTag)]
+                | isPayload(Int)  [function, total, symbol(isPayload)]
+//-----------------------------------------------------------------
+  rule isTag(TAG)   => 0 <=Int TAG andBool TAG <=Int 255
+  // A payload is a 64-bit unsigned integer
+  rule isPayload(P) => 0 <=Int P   andBool P <Int #pow(i64)     [concrete]
+
+endmodule
+
+module HOST-OBJECT-LEMMAS [symbolic]
+  imports HOST-OBJECT-LEMMA-HELPERS
+
   rule [bitwise-mk-hostval-then-mask]:
       (_I <<Int SHIFT |Int T) &Int MASK => T &Int MASK
     requires isFullMask(MASK) andBool SHIFT >=Int log2Int(MASK +Int 1)
     [simplification, concrete(SHIFT, MASK)]
 
-  // #getRange(_,_,8)'s result always fits in 64-bit
-  rule #getRange(SB, ADDR, 8) &Int 18446744073709551615 => #getRange(SB, ADDR, 8)
+  rule [64bit-fullmask-of-payload]:
+      X &Int 18446744073709551615 => X
+    requires isPayload(X)
     [simplification]
 
 
@@ -66,5 +80,75 @@ module HOST-OBJECT-LEMMAS [symbolic]
      andBool WIDTH' <=Int WIDTH
     [simplification]
 
+  rule [shrs-to-getBody]:
+      i64 . shr_s unwrap(HV:HostVal) 8 => <i64> getBody(HV)
+    [simplification]
+
+  rule [shift-to-getBody]:
+      unwrap(HV) >>Int 8 => getBody(HV)
+      [simplification]
+
+  rule [defined-unsigned-is-non-negative]:
+        0 <=Int #unsigned(T, I) => true
+    requires definedUnsigned(T, I)
+    [simplification, preserves-definedness]
+
+  rule [and-255-of-unwrap]:
+    unwrap(HV:HostVal) &Int 255 => getTag(HV)    [simplification]
+
+  rule [getTag-of-fromMajorMinorAndTag]:
+      getTag(fromMajorMinorAndTag(MAJ, MIN, TAG)) => TAG
+    requires 0 <=Int MAJ
+     andBool 0 <=Int MIN
+     andBool isTag(TAG)
+    [simplification]
+
+  rule [getBody-of-fromBodyAndTag]:
+      getBody(fromBodyAndTag(BODY, TAG)) => BODY
+    requires 0 <=Int BODY
+     andBool isTag(TAG)
+      [simplification]
+
+  rule [getTag-of-fromBodyAndTag]:
+      getTag(fromBodyAndTag(BODY, TAG)) => TAG
+    requires 0 <=Int BODY
+     andBool isTag(TAG)
+      [simplification]
+
+  rule [unwrap-is-payload]:
+      isPayload(unwrap(_:HostVal)) => true
+    [simplification]
+
+  rule [unwrap-is-non-negative]:
+      0 <=Int unwrap(_:HostVal) => true
+    [simplification]
+
+  // #getRange(_,_,8)'s result always fits in 64-bit
+  rule [getRange-8-is-payload]: 
+      isPayload(#getRange(_, _, 8)) => true
+    [simplification]
+
+
+  rule [getBody-of-unwrapped-small-i64]:
+      #signed(
+        i64,
+        unwrap(
+          fromBodyAndTag( #unsigned ( i56 , I:Int ) , 7 )
+        )
+      ) >>Int 8
+      => I
+    requires isSmallInt(Signed, I)
+    [simplification]
+
+  rule [shift-of-nonneg-is-nonneg]:
+      0 <=Int I <<Int S => true
+    requires 0 <=Int I andBool 0 <=Int S
+    [simplification]
+
+  rule [or-of-nonnegs-is-nonneg]:
+      0 <=Int X |Int Y => true
+    requires 0 <=Int X andBool 0 <=Int Y
+    [simplification]
+
 endmodule
 ```