Merge branch 'master' into fxdao-test

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

deps/k_release

@@ -1 +1 @@
-7.1.93
+7.1.103

deps/kwasm_release

@@ -1 +1 @@
-0.1.97
+0.1.98

package/version

@@ -1 +1 @@
-0.1.17
+0.1.20

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "ksoroban"
-version = "0.1.17"
+version = "0.1.20"
 description = "K tooling for the Soroban platform"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
@@ -18,7 +18,7 @@ soroban-semantics = "ksoroban.kdist.plugin"
 
 [tool.poetry.dependencies]
 python = "^3.10"
-pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.97", subdirectory = "pykwasm" }
+pykwasm = { git = "https://github.com/runtimeverification/wasm-semantics.git", tag = "v0.1.98", subdirectory = "pykwasm" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

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/configuration.md

@@ -45,6 +45,12 @@ module CONFIG
 
 ```k
             <instanceStorage> .Map </instanceStorage> // Map of ScVal to ScVal
+```
+
+- `contractLiveUntil`: The ledger sequence number until which the contract instance will live.
+
+```k
+            <contractLiveUntil> 0 </contractLiveUntil>
           </contract>
         </contracts>
         <accounts>
@@ -60,7 +66,13 @@ module CONFIG
 
 ```k
         <contractData> .Map </contractData> // Map of StorageKey to ScVal
-        <contractCodes> .Map </contractCodes>
+        <contractCodes>
+          <contractCode multiplicity="*" type="Map">
+            <codeHash>      .Bytes         </codeHash>
+            <codeLiveUntil> 0              </codeLiveUntil>
+            <codeWasm>      #emptyModule() </codeWasm> 
+          </contractCode>
+        </contractCodes>
 ```
 
 - `ledgerSequenceNumber`: The current block (or "ledger" in Stellar) number.

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

@@ -3,13 +3,16 @@
 [Documentation - Host Value Type](https://github.com/stellar/stellar-protocol/blob/master/core/cap-0046-01.md#host-value-type)
 
 ```k
+requires "errors.md"
+
 module HOST-OBJECT-SYNTAX
     imports BOOL-SYNTAX
     imports INT-SYNTAX
     imports BYTES-SYNTAX
     imports STRING-SYNTAX
     imports LIST
     imports MAP
+    imports ERRORS
 ```
 
 ## ScVal
@@ -48,8 +51,9 @@ various contexts:
 
 ```k
     syntax ScVal
-     ::= SCBool(Bool)                              [symbol(SCVal:Bool)]
+      ::= SCBool(Bool)                             [symbol(SCVal:Bool)]
         | "Void"                                   [symbol(SCVal:Void)]
+        | Error(ErrorType, Int)                  [symbol(SCVal:Error)]
         | U32(Int)                                 [symbol(SCVal:U32)]
         | I32(Int)                                 [symbol(SCVal:I32)]
         | U64(Int)                                 [symbol(SCVal:U64)]
@@ -97,10 +101,12 @@ module HOST-OBJECT
     imports WASM
 
     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
 
@@ -139,6 +145,7 @@ module HOST-OBJECT
     rule getTag(SCBool(true))  => 0
     rule getTag(SCBool(false)) => 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
@@ -204,6 +211,10 @@ module HOST-OBJECT
 
     rule fromSmall(VAL) => Void                    requires getTag(VAL) ==Int 2
 
+    rule fromSmall(VAL) => Error(Int2ErrorType(getMinor(VAL)), getMajor(VAL))
+                                                   requires getTag(VAL) ==Int 3
+                                                    andBool Int2ErrorTypeValid(getMinor(VAL))
+
     rule fromSmall(VAL) => U32(getMajor(VAL))      requires getTag(VAL) ==Int 4
 
     rule fromSmall(VAL) => I32(#signed(i32, getMajor(VAL)))
@@ -232,6 +243,7 @@ module HOST-OBJECT
     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)