Test harness for lemmas (#60)

* implement the harness

* add lemma tests

* Set Version: 0.1.51

* add CI job for lemma tests

* format

* update soroban sdk

* Fix typo

Co-authored-by: Everett Hildenbrandt <[email protected]>

* Set Version: 0.1.55

* add `EqualityProof` support

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Everett Hildenbrandt <[email protected]>

.github/workflows/test.yml

@@ -71,3 +71,29 @@ jobs:
       - name: 'Tear down Docker'
         if: always()
         run: docker stop --time=0 ${CONTAINER}
+
+  lemma-tests:
+    needs: code-quality-checks
+    name: 'Lemma Tests'
+    runs-on: [self-hosted, linux, normal]
+    env:
+      CONTAINER: komet-lemmas-${{ github.sha }}
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          fetch-depth: 0
+          submodules: recursive
+      - name: 'Set up Docker'
+        uses: ./.github/actions/with-docker
+        with:
+          container-name: ${CONTAINER}
+      - name: 'Build komet'
+        run: docker exec --user user ${CONTAINER} poetry install
+      - name: 'Build semantics'
+        run: docker exec --user user ${CONTAINER} make kdist-build
+      - name: 'Run lemma tests'
+        run: docker exec --user user ${CONTAINER} make test-lemmas
+      - name: 'Tear down Docker'
+        if: always()
+        run: docker stop --time=0 ${CONTAINER}

Makefile

@@ -44,6 +44,8 @@ test-unit: poetry-install
 test-integration: poetry-install
 	$(POETRY_RUN) pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
 
+test-lemmas: poetry-install
+	$(POETRY_RUN) pytest src/tests/lemmas --maxfail=1 --verbose --durations=0 --numprocesses=4 --dist=worksteal $(TEST_ARGS)
 
 # Coverage
 

package/version

@@ -1 +1 @@
-0.1.54
+0.1.55

pyproject.toml

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

src/komet/kasmer.py

@@ -12,6 +12,7 @@
 from pyk.cterm import CTerm, cterm_build_claim
 from pyk.kast.inner import 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
 from pyk.kore.parser import KoreParser
 from pyk.kore.syntax import EVar, SortApp
@@ -39,7 +40,7 @@
     steps_of,
     upload_wasm,
 )
-from .proof import run_claim
+from .proof import is_functional, run_claim, run_functional_claim
 from .scval import SCType
 from .utils import KSorobanError, concrete_definition
 
@@ -50,7 +51,7 @@
     from hypothesis.strategies import SearchStrategy
     from pyk.kast.inner import KInner
     from pyk.kore.syntax import Pattern
-    from pyk.proof import APRProof
+    from pyk.proof import APRProof, EqualityProof
     from pyk.utils import BugReport
     from rich.progress import TaskID
 
@@ -380,10 +381,40 @@ def deploy_and_prove(
         test_bindings = [b for b in bindings if b.name.startswith('test_') and (id is None or b.name == id)]
 
         for binding in test_bindings:
+            print(binding.name)
             proof = self.run_prove(conf, subst, binding, always_allocate, proof_dir, bug_report)
             if proof.status == ProofStatus.FAILED:
                 raise KSorobanError(proof.summary)
 
+    def prove_raw(
+        self,
+        claim_file: Path,
+        label: str | None = None,
+        proof_dir: Path | None = None,
+        bug_report: BugReport | None = None,
+    ) -> None:
+
+        modules = self.definition.kprove.parse_modules(claim_file).modules
+        claims = [
+            sent
+            for module in modules
+            for sent in module.sentences
+            if isinstance(sent, KClaim) and (label is None or sent.label == label)
+        ]
+
+        for claim in claims:
+            print('Proving:', claim.label, 'at', claim.source)
+
+            proof: EqualityProof | APRProof
+            if is_functional(claim):
+                proof = run_functional_claim(claim, proof_dir, bug_report)
+                if proof.status == ProofStatus.FAILED:
+                    raise KSorobanError(proof)
+            else:
+                proof = run_claim(claim.label, claim, proof_dir, bug_report)
+                if proof.status == ProofStatus.FAILED:
+                    raise KSorobanError(proof.summary)
+
 
 @dataclass(frozen=True)
 class ContractBinding:

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

@@ -6,6 +6,13 @@ module KSOROBAN-LEMMAS [symbolic]
   imports KWASM-LEMMAS
   imports INT-BITWISE-LEMMAS
   imports HOST-OBJECT-LEMMAS
+  imports SOROBAN
+
+  syntax InternalCmd ::= runLemma(ProofStep) | doneLemma(ProofStep)
+  syntax ProofStep ::= HostVal | ScVal | Int | Bool
+
+  rule <k> runLemma(S) => doneLemma(S) ... </k>
+
 endmodule
 
 module INT-BITWISE-LEMMAS [symbolic]
@@ -31,15 +38,18 @@ module INT-BITWISE-LEMMAS [symbolic]
   rule fullMask(I:Int) => (1 <<Int I) -Int 1 requires 0 <Int I
   rule fullMask(I:Int) => 0                  requires I <=Int 0
 
-  rule I modInt M => I &Int (M -Int 1) requires isPowerOf2(M) [simplification, concrete(M)]
+  rule [modInt-to-bit-mask]:
+      I modInt M => I &Int (M -Int 1) requires isPowerOf2(M)
+    [simplification, concrete(M)]
 
 endmodule
 
 module HOST-OBJECT-LEMMAS [symbolic]
   imports HOST-OBJECT
   imports INT-BITWISE-LEMMAS
 
-  rule (_I <<Int SHIFT |Int T) &Int MASK => T &Int MASK
+  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)]
 

src/komet/komet.py

@@ -14,11 +14,13 @@
 from pyk.kdist import kdist
 from pyk.ktool.kprint import KAstOutput, _kast
 from pyk.ktool.krun import _krun
-from pyk.proof.reachability import APRProof
+from pyk.proof import APRProof, EqualityProof
 from pyk.proof.tui import APRProofViewer
 from pyk.utils import abs_or_rel_to, ensure_dir_path
 from pykwasm.scripts.preprocessor import preprocess
 
+from komet.proof import simplify
+
 from .kasmer import Kasmer
 from .utils import KSorobanError, concrete_definition, symbolic_definition
 
@@ -65,6 +67,12 @@ def main() -> None:
             assert args.proof_dir is not None
             _exec_prove_view(proof_dir=args.proof_dir, id=args.id)
 
+    elif args.command == 'prove-raw':
+        assert args.claim_file is not None
+        _exec_prove_raw(
+            claim_file=args.claim_file, label=args.label, proof_dir=args.proof_dir, bug_report=args.bug_report
+        )
+
     raise AssertionError()
 
 
@@ -77,6 +85,37 @@ def _exec_run(*, program: Path, backend: Backend) -> None:
     _exit_with_output(proc_res)
 
 
+def _exec_prove_raw(
+    *,
+    claim_file: Path,
+    label: str | None,
+    proof_dir: Path | None,
+    bug_report: BugReport | None = None,
+) -> None:
+    kasmer = Kasmer(symbolic_definition)
+    try:
+        kasmer.prove_raw(claim_file, label, proof_dir, bug_report)
+        exit(0)
+    except KSorobanError as e:
+        if isinstance(e.args[0], EqualityProof):
+            proof: EqualityProof = e.args[0]
+
+            # Simplify the LHS and RHS of the equality separately to show why the proof failed.
+            # We do not use proof.simplified_equality because for a failed proof, it is usually #Bottom and provides no additional insight.
+            lhs = simplify(proof.lhs_body)
+            rhs = simplify(proof.rhs_body)
+            constraints = [simplify(c) for c in proof.constraints]
+
+            print('LHS:', kasmer.definition.krun.pretty_print(lhs), file=sys.stderr)
+            print('RHS:', kasmer.definition.krun.pretty_print(rhs), file=sys.stderr)
+
+            print('Constraints:', file=sys.stderr)
+            for c in constraints:
+                print('    ', kasmer.definition.krun.pretty_print(c), file=sys.stderr)
+
+        exit(1)
+
+
 def _exec_kast(*, program: Path, backend: Backend, output: KAstOutput | None) -> None:
     definition_dir = kdist.get(f'soroban-semantics.{backend.value}')
 
@@ -212,6 +251,17 @@ def _argument_parser() -> ArgumentParser:
     prove_parser.add_argument('--bug-report', type=bug_report_arg, default=None, help='Bug report directory for proofs')
     _add_common_test_arguments(prove_parser)
 
+    prove_raw_parser = command_parser.add_parser(
+        'prove-raw',
+        help='Prove K claims directly from a file, bypassing the usual test contract structure; intended for development and advanced users.',
+    )
+    prove_raw_parser.add_argument('claim_file', metavar='CLAIM_FILE', type=file_path, help='path to claim file')
+    prove_raw_parser.add_argument('--proof-dir', type=ensure_dir_path, default=None, help='Output directory for proofs')
+    prove_raw_parser.add_argument(
+        '--bug-report', type=bug_report_arg, default=None, help='Bug report directory for proofs'
+    )
+    prove_raw_parser.add_argument('--label', help='Label of the K claim in the file')
+
     return parser
 
 

src/komet/proof.py

@@ -4,16 +4,20 @@
 from typing import TYPE_CHECKING
 
 from pyk.cterm import cterm_symbolic
+from pyk.kast.outer import KApply, KRewrite
 from pyk.kcfg import KCFGExplore
 from pyk.kcfg.semantics import DefaultSemantics
+from pyk.konvert import kast_to_kore, kore_to_kast
 from pyk.proof import APRProof, APRProver
+from pyk.proof.implies import EqualityProof, ImpliesProver
 
 from .utils import library_definition, symbolic_definition
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
     from pathlib import Path
 
+    from pyk.kast.inner import KInner
     from pyk.kast.outer import KClaim
     from pyk.utils import BugReport
 
@@ -45,3 +49,33 @@ def run_claim(id: str, claim: KClaim, proof_dir: Path | None = None, bug_report:
 
     proof.write_proof_data()
     return proof
+
+
+def is_functional(claim: KClaim) -> bool:
+    claim_lhs = claim.body
+    if type(claim_lhs) is KRewrite:
+        claim_lhs = claim_lhs.lhs
+    return not (type(claim_lhs) is KApply and claim_lhs.label.name == '<generatedTop>')
+
+
+def run_functional_claim(
+    claim: KClaim, proof_dir: Path | None = None, bug_report: BugReport | None = None
+) -> EqualityProof:
+    if proof_dir is not None and EqualityProof.proof_exists(claim.label, proof_dir):
+        proof = EqualityProof.read_proof_data(proof_dir, claim.label)
+    else:
+        proof = EqualityProof.from_claim(claim, symbolic_definition.kdefinition, proof_dir=proof_dir)
+
+    with _explore_context(claim.label, bug_report) as kcfg_explore:
+        prover = ImpliesProver(proof, kcfg_explore=kcfg_explore)
+        prover.advance_proof(proof)
+
+    proof.write_proof_data()
+    return proof
+
+
+def simplify(kast: KInner, bug_report: BugReport | None = None) -> KInner:
+    pat = kast_to_kore(symbolic_definition.kdefinition, kast)
+    with _explore_context('', bug_report=bug_report) as kcfg_explore:
+        simplified, _ = kcfg_explore.cterm_symbolic._kore_client.simplify(pat)
+        return kore_to_kast(symbolic_definition.kdefinition, simplified)

src/komet/utils.py

@@ -7,6 +7,7 @@
 from pyk.kdist import kdist
 from pyk.konvert import kast_to_kore
 from pyk.ktool.kompile import DefinitionInfo
+from pyk.ktool.kprove import KProve
 from pyk.ktool.krun import KRun
 
 if TYPE_CHECKING:
@@ -46,6 +47,10 @@ def kdefinition(self) -> KDefinition:
     def krun(self) -> KRun:
         return KRun(self.path)
 
+    @cached_property
+    def kprove(self) -> KProve:
+        return KProve(self.path)
+
     def krun_with_kast(self, pgm: KInner, sort: KSort | None = None, **kwargs: Any) -> CompletedProcess:
         """Run the semantics on a kast term.
 

src/tests/lemmas/specs/int-bitwise-spec.k

@@ -0,0 +1,12 @@
+module INT-BITWISE-SPEC
+    imports KASMER
+
+    // Tested lemmas:
+    // - modInt-to-bit-mask
+    claim [test-modInt-to-andInt]:
+        ( (I <<Int 32) |Int 4) modInt 256
+          =>
+        ( (I <<Int 32) |Int 4) &Int 255 
+      requires 0 <=Int I
+
+endmodule

src/tests/lemmas/specs/test-spec.k

@@ -0,0 +1,12 @@
+module TEST-SPEC
+    imports KASMER
+
+    // Tested lemmas:
+    // - bitwise-mk-hostval-then-mask
+    claim [test-bitwise-mk-hostval-then-mask]:
+        ( (I <<Int 32) |Int 4) &Int 255
+          =>
+        4
+      requires 0 <=Int I
+
+endmodule

src/tests/lemmas/test_lemmas.py

@@ -0,0 +1,30 @@
+from pathlib import Path
+
+import pytest
+from pyk.kast.outer import KClaim
+from pyk.kdist import kdist
+from pyk.ktool.kprove import KProve
+
+from komet.kasmer import Kasmer
+from komet.utils import symbolic_definition
+
+SYMBOLIC_DEFINITION_DIR = kdist.get('soroban-semantics.haskell')
+
+
+def parse_kclaims(claim_path: Path) -> list[KClaim]:
+    modules = KProve(SYMBOLIC_DEFINITION_DIR).parse_modules(claim_path).modules
+    return [sent for module in modules for sent in module.sentences if isinstance(sent, KClaim)]
+
+
+SPEC_DATA = (Path(__file__).parent / 'specs').resolve(strict=True)
+SPEC_FILES = SPEC_DATA.glob('*.k')
+
+
+@pytest.fixture
+def symbolic_kasmer() -> Kasmer:
+    return Kasmer(symbolic_definition)
+
+
+@pytest.mark.parametrize('claim_file', SPEC_FILES, ids=str)
+def test_run(claim_file: Path, tmp_path: Path, symbolic_kasmer: Kasmer) -> None:
+    symbolic_kasmer.prove_raw(claim_file=claim_file, proof_dir=tmp_path)