Add ksoroban prove command (#20)

* Add haskell backend target

* Rename

* Add module level SorobanDefinitionInfo instances

* Rename

* Make Kasmer.deploy_test unconditionally use the llvm definition

* Draft of 'ksoroban prove'

* Set Version: 0.1.16

* Lemmas

* prove view command

* More lemmas. test_adder now passes!

* Rename

* Set Version: 0.1.17

* Fix the lemmas.

I scuffed them somehow when doing some reformatting before a commit.

* Makefile: Build every soroban-semantics target

* Adjust how prove/fuzz gets selected

* Add the adder proof to the tests

* Set Version: 0.1.18

* Set Version: 0.1.18

* Set Version: 0.1.20

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Burak Bilge Yalçınkaya <[email protected]>

Makefile

@@ -23,7 +23,7 @@ poetry-install:
 # Semantics
 
 kdist-build: poetry-install
-	$(POETRY) run kdist -v build soroban-semantics.llvm
+	$(POETRY) run kdist -v build -j2 soroban-semantics.*
 
 kdist-clean: poetry-install
 	$(POETRY) run kdist clean

package/version

@@ -1 +1 @@
-0.1.19
+0.1.20

pyproject.toml

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

src/ksoroban/kasmer.py

@@ -9,17 +9,22 @@
 from typing import TYPE_CHECKING
 
 from hypothesis import strategies
+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.konvert import kast_to_kore, kore_to_kast
 from pyk.kore.parser import KoreParser
 from pyk.kore.syntax import EVar, SortApp
 from pyk.ktool.kfuzz import fuzz
 from pyk.ktool.krun import KRunOutput
+from pyk.prelude.ml import mlEqualsTrue
+from pyk.prelude.utils import token
+from pyk.proof import ProofStatus
 from pyk.utils import run_process
 from pykwasm.wasm2kast import wasm2kast
 
 from .kast.syntax import (
+    STEPS_TERMINATOR,
     account_id,
     call_tx,
     contract_id,
@@ -30,25 +35,28 @@
     steps_of,
     upload_wasm,
 )
+from .proof import run_claim
 from .scval import SCType
+from .utils import KSorobanError, concrete_definition
 
 if TYPE_CHECKING:
     from typing import Any
 
     from hypothesis.strategies import SearchStrategy
     from pyk.kast.inner import KInner
     from pyk.kore.syntax import Pattern
+    from pyk.proof import APRProof
 
-    from .utils import SorobanDefinitionInfo
+    from .utils import SorobanDefinition
 
 
 class Kasmer:
     """Reads soroban contracts, and runs tests for them."""
 
-    definition_info: SorobanDefinitionInfo
+    definition: SorobanDefinition
 
-    def __init__(self, definition_info: SorobanDefinitionInfo) -> None:
-        self.definition_info = definition_info
+    def __init__(self, definition: SorobanDefinition) -> None:
+        self.definition = definition
 
     def _which(self, cmd: str) -> Path:
         path_str = shutil.which(cmd)
@@ -121,7 +129,8 @@ def kast_from_wasm(self, wasm: Path) -> KInner:
         """Get a kast term from a wasm program."""
         return wasm2kast(open(wasm, 'rb'))
 
-    def deploy_test(self, contract: KInner) -> tuple[KInner, dict[str, KInner]]:
+    @staticmethod
+    def deploy_test(contract: KInner) -> tuple[KInner, dict[str, KInner]]:
         """Takes a wasm soroban contract as a kast term and deploys it in a fresh configuration.
 
         Returns:
@@ -140,9 +149,9 @@ def deploy_test(self, contract: KInner) -> tuple[KInner, dict[str, KInner]]:
         )
 
         # Run the steps and grab the resulting config as a starting place to call transactions
-        proc_res = self.definition_info.krun_with_kast(steps, sort=KSort('Steps'), output=KRunOutput.KORE)
+        proc_res = concrete_definition.krun_with_kast(steps, sort=KSort('Steps'), output=KRunOutput.KORE)
         kore_result = KoreParser(proc_res.stdout).pattern()
-        kast_result = kore_to_kast(self.definition_info.kdefinition, kore_result)
+        kast_result = kore_to_kast(concrete_definition.kdefinition, kore_result)
 
         conf, subst = split_config_from(kast_result)
 
@@ -162,18 +171,43 @@ def run_test(self, conf: KInner, subst: dict[str, KInner], binding: ContractBind
 
         def make_steps(*args: KInner) -> Pattern:
             steps_kast = steps_of([set_exit_code(1), call_tx(from_acct, to_acct, name, args, result), set_exit_code(0)])
-            return kast_to_kore(self.definition_info.kdefinition, steps_kast, KSort('Steps'))
+            return kast_to_kore(self.definition.kdefinition, steps_kast, KSort('Steps'))
 
         subst['PROGRAM_CELL'] = KVariable('STEPS')
         template_config = Subst(subst).apply(conf)
-        template_config_kore = kast_to_kore(
-            self.definition_info.kdefinition, template_config, KSort('GeneratedTopCell')
-        )
+        template_config_kore = kast_to_kore(self.definition.kdefinition, template_config, KSort('GeneratedTopCell'))
 
         steps_strategy = binding.strategy.map(lambda args: make_steps(*args))
         template_subst = {EVar('VarSTEPS', SortApp('SortSteps')): steps_strategy}
 
-        fuzz(self.definition_info.path, template_config_kore, template_subst, check_exit_code=True)
+        fuzz(self.definition.path, template_config_kore, template_subst, check_exit_code=True)
+
+    def run_prove(
+        self, conf: KInner, subst: dict[str, KInner], binding: ContractBinding, proof_dir: Path | None = None
+    ) -> APRProof:
+        from_acct = account_id(b'test-account')
+        to_acct = contract_id(b'test-contract')
+        name = binding.name
+        result = sc_bool(True)
+
+        def make_steps(*args: KInner) -> KInner:
+            return steps_of([set_exit_code(1), call_tx(from_acct, to_acct, name, args, result), set_exit_code(0)])
+
+        vars, ctrs = binding.symbolic_args()
+
+        lhs_subst = subst.copy()
+        lhs_subst['PROGRAM_CELL'] = make_steps(*vars)
+        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']
+        rhs = CTerm(Subst(rhs_subst).apply(conf))
+
+        claim, _ = cterm_build_claim(name, lhs, rhs)
+
+        return run_claim(name, claim, proof_dir)
 
     def deploy_and_run(self, contract_wasm: Path) -> None:
         """Run all of the tests in a soroban test contract.
@@ -194,6 +228,28 @@ def deploy_and_run(self, contract_wasm: Path) -> None:
                 continue
             self.run_test(conf, subst, binding)
 
+    def deploy_and_prove(self, contract_wasm: Path, proof_dir: Path | None = None) -> None:
+        """Prove all of the tests in a soroban test contract.
+
+        Args:
+            contract_wasm: The path to the compiled wasm contract.
+            proof_dir: The optional location to save the proof.
+
+        Raises:
+            KSorobanError if a proof fails
+        """
+        contract_kast = self.kast_from_wasm(contract_wasm)
+        conf, subst = self.deploy_test(contract_kast)
+
+        bindings = self.contract_bindings(contract_wasm)
+
+        for binding in bindings:
+            if not binding.name.startswith('test_'):
+                continue
+            proof = self.run_prove(conf, subst, binding, proof_dir)
+            if proof.status == ProofStatus.FAILED:
+                raise KSorobanError(proof.summary)
+
 
 @dataclass(frozen=True)
 class ContractBinding:
@@ -206,3 +262,12 @@ class ContractBinding:
     @cached_property
     def strategy(self) -> SearchStrategy[tuple[KInner, ...]]:
         return strategies.tuples(*(arg.strategy().map(lambda x: x.to_kast()) for arg in self.inputs))
+
+    def symbolic_args(self) -> tuple[tuple[KInner, ...], tuple[KInner, ...]]:
+        args: tuple[KInner, ...] = ()
+        constraints: tuple[KInner, ...] = ()
+        for i, arg in enumerate(self.inputs):
+            v, c = arg.as_var(f'ARG_{i}')
+            args += (v,)
+            constraints += c
+        return args, constraints

src/ksoroban/kast/syntax.py

@@ -13,9 +13,11 @@
 
     from pyk.kast.inner import KInner
 
+STEPS_TERMINATOR = KApply('.List{"kasmerSteps"}')
+
 
 def steps_of(steps: Iterable[KInner]) -> KInner:
-    return build_cons(KApply('.List{"kasmerSteps"}'), 'kasmerSteps', steps)
+    return build_cons(STEPS_TERMINATOR, 'kasmerSteps', steps)
 
 
 def account_id(acct_id: bytes) -> KApply:

src/ksoroban/kdist/plugin.py

@@ -48,6 +48,17 @@ def deps(self) -> tuple[str]:
     'source': SourceTarget(),
     'llvm': KompileTarget(
         lambda src_dir: {
+            'backend': 'llvm',
+            'main_file': src_dir / 'soroban-semantics/kasmer.md',
+            'syntax_module': 'KASMER-SYNTAX',
+            'include_dirs': [src_dir],
+            'md_selector': 'k',
+            'warnings_to_errors': True,
+        },
+    ),
+    'haskell': KompileTarget(
+        lambda src_dir: {
+            'backend': 'haskell',
             'main_file': src_dir / 'soroban-semantics/kasmer.md',
             'syntax_module': 'KASMER-SYNTAX',
             'include_dirs': [src_dir],

src/ksoroban/kdist/soroban-semantics/kasmer.md

@@ -2,6 +2,7 @@
 ```k
 requires "soroban.md"
 requires "cheatcodes.md"
+requires "ksoroban-lemmas.md"
 
 module KASMER-SYNTAX
   imports WASM-TEXT-SYNTAX
@@ -33,6 +34,7 @@ module KASMER
     imports SOROBAN
     imports CHEATCODES
     imports KASMER-SYNTAX-COMMON
+    imports KSOROBAN-LEMMAS
 
     configuration
       <kasmer>
@@ -158,4 +160,4 @@ module KASMER
         (_:HostCell => <host> <hostStack> .HostStack </hostStack> ... </host>)
 
 endmodule
-```
+```

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

@@ -0,0 +1,47 @@
+```k
+requires "wasm-semantics/kwasm-lemmas.md"
+requires "data.md"
+
+module KSOROBAN-LEMMAS [symbolic]
+  imports KWASM-LEMMAS
+  imports INT-BITWISE-LEMMAS
+  imports HOST-OBJECT-LEMMAS
+endmodule
+
+module INT-BITWISE-LEMMAS [symbolic]
+  imports INT
+  imports BOOL
+
+  rule C |Int S => S |Int C [simplification, concrete(C), symbolic(S)]
+  rule X |Int 0 => X        [simplification]
+
+  rule  A &Int  B          =>  B &Int  A          [simplification, concrete(A), symbolic(B)]
+  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]
+  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]
+  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]
+  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)]
+
+endmodule
+
+module HOST-OBJECT-LEMMAS [symbolic]
+  imports HOST-OBJECT
+  imports INT-BITWISE-LEMMAS
+
+  rule (_I <<Int SHIFT |Int T) &Int MASK => T &Int MASK
+    requires isFullMask(MASK) andBool SHIFT >=Int log2Int(MASK +Int 1)
+    [simplification, concrete(SHIFT, MASK)]
+
+endmodule
+```

src/ksoroban/ksoroban.py

@@ -12,10 +12,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.tui import APRProofViewer
+from pyk.utils import ensure_dir_path
 from pykwasm.scripts.preprocessor import preprocess
 
 from .kasmer import Kasmer
-from .utils import SorobanDefinitionInfo
+from .utils import concrete_definition, symbolic_definition
 
 if TYPE_CHECKING:
     from collections.abc import Iterator
@@ -38,6 +41,13 @@ def main() -> None:
     elif args.command == 'test':
         wasm = Path(args.wasm.name) if args.wasm is not None else None
         _exec_test(wasm=wasm)
+    elif args.command == 'prove':
+        if args.prove_command is None or args.prove_command == 'run':
+            wasm = Path(args.wasm.name) if args.wasm is not None else None
+            _exec_prove_run(wasm=wasm, proof_dir=args.proof_dir)
+        if args.prove_command == 'view':
+            assert args.proof_dir is not None
+            _exec_prove_view(proof_dir=args.proof_dir, id=args.id)
 
     raise AssertionError()
 
@@ -68,9 +78,7 @@ def _exec_test(*, wasm: Path | None) -> None:
 
     Exits successfully when all the tests pass.
     """
-    definition_dir = kdist.get('soroban-semantics.llvm')
-    definition_info = SorobanDefinitionInfo(definition_dir)
-    kasmer = Kasmer(definition_info)
+    kasmer = Kasmer(concrete_definition)
 
     if wasm is None:
         # We build the contract here, specifying where it's saved so we know where to find it.
@@ -83,6 +91,24 @@ def _exec_test(*, wasm: Path | None) -> None:
     sys.exit(0)
 
 
+def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None) -> None:
+    kasmer = Kasmer(symbolic_definition)
+
+    if wasm is None:
+        wasm = kasmer.build_soroban_contract(Path.cwd())
+
+    kasmer.deploy_and_prove(wasm, proof_dir)
+
+    sys.exit(0)
+
+
+def _exec_prove_view(*, proof_dir: Path, id: str) -> None:
+    proof = APRProof.read_proof_data(proof_dir, id)
+    viewer = APRProofViewer(proof, symbolic_definition.krun)
+    viewer.run()
+    sys.exit(0)
+
+
 @contextmanager
 def _preprocessed(program: Path) -> Iterator[Path]:
     program_text = program.read_text()
@@ -114,6 +140,18 @@ def _argument_parser() -> ArgumentParser:
     test_parser = command_parser.add_parser('test', help='Test the soroban contract in the current working directory')
     test_parser.add_argument('--wasm', type=FileType('r'), help='Test a specific contract wasm file instead')
 
+    prove_parser = command_parser.add_parser('prove', help='Test the soroban contract in the current working directory')
+    prove_parser.add_argument(
+        'prove_command',
+        default='run',
+        choices=('run', 'view'),
+        metavar='COMMAND',
+        help='Proof command to run. One of (%(choices)s)',
+    )
+    prove_parser.add_argument('--wasm', type=FileType('r'), help='Prove a specific contract wasm file instead')
+    prove_parser.add_argument('--proof-dir', type=ensure_dir_path, default=None, help='Output directory for proofs')
+    prove_parser.add_argument('--id', help='Name of the test function in the testing contract')
+
     return parser