497 Start of a lemma library

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.101"
+version = "0.3.102"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.101'
+VERSION: Final = '0.3.102'

kmir/src/kmir/kdist/mir-semantics/kmir.md

@@ -3,6 +3,7 @@
 ```k
 requires "kmir-ast.md"
 requires "rt/data.md"
+requires "lemmas/kmir-lemmas.md"
 ```
 
 ## Syntax of MIR in K
@@ -86,7 +87,7 @@ endmodule
 ### Execution Control Flow
 
 ```k
-module KMIR
+module KMIR-CONTROL-FLOW
   imports KMIR-SYNTAX
   imports KMIR-CONFIGURATION
   imports MONO
@@ -618,3 +619,14 @@ Otherwise the provided message is passed to a `panic!` call, ending the program
 ```k
 endmodule
 ```
+
+## Top-level Module
+
+The top-level module `KMIR` includes both the control flow constructs (and transitively all modules related to runtime operations and AST) and a collection of simplification lemmas required for symbolic execution of MIR programs.
+
+```k
+module KMIR
+  imports KMIR-CONTROL-FLOW
+  imports KMIR-LEMMAS
+
+endmodule

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

@@ -0,0 +1,57 @@
+# Lemmas for MIR symbolic execution
+
+This file contains basic lemmas required for symbolic execution of MIR programs using `kmir`.
+
+Lemmas are simpliciations of symbolic function application that aims to confirm conditions for rewrite rules to avoid spurious branching on symbolic program parts.
+
+Some of the lemmas relate to the control flow implementation in `kmir.md` and will be needed in various proofs (for instance the simplification of list size for partially-symbolic lists of locals or stack frames).  
+Others are related to helper functions used for integer arithmetic.
+
+```k
+requires "../rt/data.md"
+requires "../kmir.md"
+
+module KMIR-LEMMAS
+  imports RT-DATA-HIGH
+
+  imports LIST
+  imports INT-SYMBOLIC
+  imports BOOL
+```
+## Simplifications for lists to avoid spurious branching on error cases in control flow
+
+Rewrite rules that look up locals or stack frames require that an index into the respective `List`s in the configuration be within the bounds of the locals list/stack. Therefore, the `size` function on lists needs to be computed. The following simplifications allow for locals and stacks to have concrete values in the beginning but a symbolic rest (of unknown size).  
+The lists used in the semantics are cons-lists, so only rules with a head element match are required.
+
+```k
+  rule N <Int size(_LIST:List) => true
+    requires N <Int 0
+    [simplification, symbolic(_LIST)]
+
+  rule N <Int size(ListItem(_) REST:List) => N -Int 1 <Int size(REST)
+    requires 0 <Int N
+    [simplification, symbolic(REST)]
+```
+
+## Simplifications related to the `truncate` function
+
+The `truncate` function is used in various overflow checks in integer arithmetic.
+Therefore, its value range should be simplified for symbolic input asserted to be in range.
+
+```k
+  rule truncate(VAL, WIDTH, Unsigned) => VAL
+    requires VAL <Int (1 <<Int WIDTH)
+     andBool 0 <=Int VAL
+     [simplification]
+
+  rule truncate(VAL, WIDTH, Signed) => VAL
+    requires VAL <Int (1 <<Int (WIDTH -Int 1))
+     andBool 0 -Int (1 <<Int (WIDTH -Int 1)) <=Int VAL
+     [simplification]
+
+```
+
+
+```k
+endmodule
+```

kmir/src/kmir/kmir.py

@@ -36,7 +36,7 @@ def __init__(
         self.llvm_library_dir = llvm_library_dir
 
     class Symbols:
-        END_PROGRAM: Final = KApply('#EndProgram_KMIR_KItem')
+        END_PROGRAM: Final = KApply('#EndProgram_KMIR-CONTROL-FLOW_KItem')
 
     @contextmanager
     def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:

package/version

@@ -1 +1 @@
-0.3.101
+0.3.102