Updating prover

kmir/k-src/mir.md

@@ -45,7 +45,6 @@ If we are, then we stop execution and enter the finalization phase. Otherwise, i
        <callStack> ListItem(Fn(main)) => .List </callStack>
        <phase> Execution => Finalization </phase>
        <returncode> _ => 0 </returncode>
-
   rule <k> #return(FUNCTION_KEY, _) => .K ... </k>
        <callStack> ListItem(FUNCTION_KEY) XS => XS </callStack>
     requires FUNCTION_KEY =/=K Fn(main)
@@ -61,16 +60,17 @@ The `#halt` construct is used to signify the end of execution. Any remaining ite
 endmodule
 ```
 
-
 `MIR-SYMBOLIC` is a stub module to be used with the Haskell backend in the future. It does not import `MIR-AMBIGUITIES`, since `amb` productions are not supported by the Haskell backend. We may need to consult the C semantics team when we start working on symbolic execution.
 
 ```k
 module MIR-SYMBOLIC
-  imports MIR-CONFIGURATION
-  imports MIR-INITIALIZATION
-  imports MIR-EXECUTION
-  imports MIR-FINALIZATION
+  imports MIR
+
+    syntax KItem ::= runLemma ( Step ) | doneLemma ( Step )
+    // -------------------------------------------------------
+    rule <k> runLemma(S) => doneLemma(S) ... </k>
 
+    syntax Step ::= Bool | Int | MIRValue
 endmodule
 ```
 

kmir/src/kmir/__main__.py

@@ -5,6 +5,7 @@
 from pathlib import Path
 from typing import Any, Final
 
+from pyk.cterm import CTerm
 from pyk.kast.outer import KApply, KClaim, KRewrite
 from pyk.kcfg import KCFG
 from pyk.ktool.kprint import KAstInput, KAstOutput
@@ -104,13 +105,16 @@ def exec_prove(
     definition_dir: str,
     haskell_dir: str,
     spec_file: str,
+    *,
+    use_booster: bool = False,
     bug_report: bool = False,
     save_directory: Path | None = None,
     reinit: bool = False,
     depth: int | None = None,
     smt_timeout: int | None = None,
     smt_retry_limit: int | None = None,
     trace_rewrites: bool = False,
+    kore_rpc_command: str | Iterable[str] | None = None,
     **kwargs: Any,
 ) -> None:
     if spec_file is None:
@@ -134,6 +138,11 @@ def exec_prove(
     if not claims:
         raise ValueError(f'No claims found in file {spec_file}')
 
+    if kore_rpc_command is None:
+        kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',)
+    elif isinstance(kore_rpc_command, str):
+        kore_rpc_command = kore_rpc_command.split()
+
     def is_functional(claim: KClaim) -> bool:
         claim_lhs = claim.body
         if type(claim_lhs) is KRewrite:
@@ -145,12 +154,13 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
             kprove,
             kcfg_semantics=KMIRSemantics(),
             id=claim.label,
+            llvm_definition_dir=kmir.llvm_dir if use_booster else None,
             bug_report=br,
+            kore_rpc_command=kore_rpc_command,
             smt_timeout=smt_timeout,
             smt_retry_limit=smt_retry_limit,
             trace_rewrites=trace_rewrites,
         ) as kcfg_explore:
-            # TODO: simplfy_init
             proof_problem: Proof
             if is_functional(claim):
                 if (
@@ -175,6 +185,14 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]:
                     _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}')
                     new_init = kcfg_explore.cterm_assume_defined(new_init)
 
+                    _LOGGER.info(f'Simplifying initial and target node: {claim.label}')
+                    new_init, _ = kcfg_explore.cterm_simplify(new_init)
+                    new_target, _ = kcfg_explore.cterm_simplify(new_target)
+                    if CTerm._is_bottom(new_init.kast):
+                        raise ValueError('Simplifying initial node led to #Bottom, are you sure your LHS is defined?')
+                    if CTerm._is_top(new_target.kast):
+                        raise ValueError('Simplifying target node led to #Bottom, are you sure your RHS is defined?')
+
                     kcfg.replace_node(init_node_id, new_init)
                     kcfg.replace_node(target_node_id, new_target)
 

kmir/src/kmir/cli.py

@@ -157,6 +157,18 @@ def create_argument_parser() -> ArgumentParser:
         default=False,
         help='Reinitialise a proof.',
     )
+    prove_subparser.add_argument(
+        '--use-booster',
+        action='store_true',
+        default=False,
+        help='Use the booster backend instead of the haskell backend',
+    )
+    prove_subparser.add_argument(
+        '--kore-rpc-command',
+        type=str,
+        default=None,
+        help='Custom command to start RPC server',
+    )
 
     kmir_cli_args = KMIRCLIArgs()
 

kmir/src/kmir/utils.py

@@ -197,12 +197,8 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore, counterexample_i
                 simplified_node, _ = kcfg_explore.cterm_simplify(node.cterm)
                 simplified_target, _ = kcfg_explore.cterm_simplify(target.cterm)
 
-                # TODO: Remove the ignore annotations, unsure why mypy couldn't infer type here
-                node_cterm = CTerm.from_kast(simplified_node)  # type: ignore
-                target_cterm = CTerm.from_kast(simplified_target)  # type: ignore
-
                 res_lines.append('  Failure reason:')
-                _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm)
+                _, reason = kcfg_explore.implication_failure_reason(simplified_node, simplified_target)
                 res_lines += [f'    {line}' for line in reason.split('\n')]
 
                 res_lines.append('  Path condition:')

kmir/src/tests/integration/proofs/empty-program.k

@@ -0,0 +1,30 @@
+requires "../../../../k-src/mir.md"
+
+module VERIFICATION
+    imports K-EQUAL
+    imports BASIC-K
+    imports MIR-SYMBOLIC
+
+    // LocalTokens will have parsing error if they are not enumerated here 
+    syntax LocalToken ::= "_1" [token]
+    syntax LocalToken ::= "_2" [token]
+    syntax LocalToken ::= "_3" [token]
+    syntax LocalToken ::= "_4" [token]
+
+    syntax BBId ::= "bb0" [token]
+endmodule
+
+module EMPTY-PROGRAM
+    imports VERIFICATION
+
+    claim 
+      <k>
+        fn main :: .FunctionPath ( .ParameterList ) -> ( ) { .DebugList let mut _0 : ( ) ;  .BindingList .ScopeList bb0  : { .Statements return ; }  .BasicBlockList }  .Mir ~> .
+        =>
+        #halt ~> .
+      </k>
+      <callStack> .List </callStack>
+      <returncode> 4 => 0 </returncode> 
+      <phase> Initialization => Finalization </phase> 
+      <functions> .Bag => ?_ </functions>
+endmodule

kmir/src/tests/integration/proofs/empty-program.mir

@@ -0,0 +1,9 @@
+// WARNING: This output format is intended for human consumers only
+// and is subject to change without notice. Knock yourself out.
+fn main() -> () {
+    let mut _0: ();
+
+    bb0: {
+        return;
+    }
+}

kmir/src/tests/integration/proofs/empty-program.rs

@@ -0,0 +1,3 @@
+fn main() {
+     42;
+}

kmir/src/tests/integration/proofs/lemmas.k

@@ -0,0 +1,21 @@
+requires "../../../../k-src/mir.md"
+
+module VERIFICATION
+    imports K-EQUAL
+    imports BASIC-K
+    imports MIR-SYMBOLIC
+
+    // LocalTokens will have parsing error if they are not enumerated here
+    syntax LocalToken ::= "_1" [token]
+    syntax LocalToken ::= "_2" [token]
+    syntax LocalToken ::= "_3" [token]
+    syntax LocalToken ::= "_4" [token]
+endmodule
+
+module LEMMAS
+    imports VERIFICATION
+
+    // For testing
+    claim <k> runLemma(isRValueResult(_:RValueResult)) => doneLemma(true) ...</k>
+    claim <k> runLemma(isRValueResult(_:MIRValue))     => doneLemma(true) ...</k>
+endmodule

kmir/src/tests/integration/proofs/simple-spec.k

@@ -15,7 +15,7 @@ endmodule
 module SIMPLE-SPEC
     imports VERIFICATION
 
-    claim <k> #executeStatement(_3 = const 5_usize) => .K ...</k>
+    claim [statement.1]: <k> #executeStatement(_3 = const 5_usize) => .K ...</k>
           <callStack> ListItem(FN_KEY) ... </callStack>
           <function>
             <fnKey> FN_KEY </fnKey>
@@ -27,7 +27,7 @@ module SIMPLE-SPEC
               ...
           </function>
 
-    claim <k> #executeStatement(PLACE:Local = const 5_usize) => .K ...</k>
+    claim [statement.2]: <k> #executeStatement(PLACE:Local = const 5_usize) => .K ...</k>
           <callStack> ListItem(FN_KEY) ... </callStack>
           <function>
             <fnKey> FN_KEY </fnKey>
@@ -40,7 +40,7 @@ module SIMPLE-SPEC
           </function>
     requires INDEX ==Int Local2Int(PLACE)
 
-    claim <k> #executeStatement(PLACE:Local = Add(const 3_i32, const 5_i32)) => .K ...</k>
+    claim [statement.3]: <k> #executeStatement(PLACE:Local = Add(const 3_i32, const 5_i32)) => .K ...</k>
           <callStack> ListItem(FN_KEY) ... </callStack>
           <function>
             <fnKey> FN_KEY </fnKey>
@@ -53,7 +53,24 @@ module SIMPLE-SPEC
           </function>
     requires INDEX ==Int Local2Int(PLACE)
 
-    claim <k> #executeStatements(PLACE1:Local = Add(const 3_i32, const 5_i32); PLACE2:Local = Add(const 3_i32, const 6_i32);) => .K ...</k>
+    claim [statement.4]: <k> #executeStatement(_1:Local = move _2) => .K ...</k>
+          <callStack> ListItem(FN_KEY) ... </callStack>
+          <function>
+            <fnKey> FN_KEY </fnKey>
+              <localDecl>
+                <index> 1 </index>
+                <value> _ => 42 </value>
+                ...
+              </localDecl>
+              <localDecl>
+                <index> 2 </index>
+                <value> 42 </value>
+                ...
+              </localDecl>
+              ...
+          </function>
+
+    claim [statements.1]: <k> #executeStatements(PLACE1:Local = Add(const 3_i32, const 5_i32); PLACE2:Local = Add(const 3_i32, const 6_i32);) => .K ...</k>
           <callStack> ListItem(FN_KEY) ... </callStack>
           <function>
             <fnKey> FN_KEY </fnKey>
@@ -71,7 +88,7 @@ module SIMPLE-SPEC
           </function>
     requires INDEX1 ==Int Local2Int(PLACE1) andBool INDEX2 ==Int Local2Int(PLACE2) andBool INDEX1 =/=Int INDEX2
 
-    claim <k> #executeStatements(PLACE:Local = Add(const 3_i32, const 5_i32); PLACE:Local = Add(const 3_i32, const 6_i32);) => .K ...</k>
+    claim [statements.2]: <k> #executeStatements(PLACE:Local = Add(const 3_i32, const 5_i32); PLACE:Local = Add(const 3_i32, const 6_i32);) => .K ...</k>
           <callStack> ListItem(FN_KEY) ... </callStack>
           <function>
             <fnKey> FN_KEY </fnKey>
@@ -83,21 +100,4 @@ module SIMPLE-SPEC
               ...
           </function>
     requires INDEX ==Int Local2Int(PLACE)
-
-    // claim <k> #executeStatement(_1:Local = move _2) => .K ...</k>
-    //       <callStack> ListItem(FN_KEY) ... </callStack>
-    //       <function>
-    //         <fnKey> FN_KEY </fnKey>
-    //           <localDecl>
-    //             <index> 1 </index>
-    //             <value> _ => 42 </value>
-    //             ...
-    //           </localDecl>
-    //           <localDecl>
-    //             <index> 2 </index>
-    //             <value> 42 </value>
-    //             ...
-    //           </localDecl>
-    //           ...
-    //       </function>
 endmodule

kmir/src/tests/integration/test_prove.py

@@ -19,8 +19,9 @@
 TEST_DIR: Final = REPO_ROOT / 'kmir/src/tests'
 SYMBOLIC_TEST_DIR: Final = TEST_DIR / 'integration/proofs'
 INITIAL_SPECS: Final = SYMBOLIC_TEST_DIR / 'simple-spec.k'
+EMPTY_PROGRAM: Final = SYMBOLIC_TEST_DIR / 'empty-program.k'
 
-ALL_TESTS: Final = [INITIAL_SPECS]
+ALL_TESTS: Final = [INITIAL_SPECS, EMPTY_PROGRAM]
 
 
 def exclude_list(exclude_file: Path) -> list[Path]:
@@ -40,7 +41,7 @@ def exclude_list(exclude_file: Path) -> list[Path]:
 @pytest.mark.parametrize(
     'spec_file',
     ALL_TESTS,
-    ids=[str(spec_file.relative_to(INITIAL_SPECS)) for spec_file in ALL_TESTS],
+    ids=[str(spec_file.relative_to(SYMBOLIC_TEST_DIR)) for spec_file in ALL_TESTS],
 )
 def test_pyk_prove(
     llvm_dir: str,