Start developing property testing

.gitignore

@@ -4,10 +4,13 @@
 ## Get latest from https://github.com/github/gitignore/blob/master/VisualStudio.gitignore
 
 .build
+.kbuild
 .kprove-*
-.kore-repl-history
+.kore-repl-*
 .sessionCommands
 tmp
+kore-exec.tar.gz
+bug-report.tar
 
 # User-specific files
 *.rsuser

deps/k_release

@@ -1 +1 @@
-v5.5.110
+v6.0.57

kmxwasm/Makefile

@@ -90,9 +90,8 @@ kbuild-%: k-src/elrond-semantics/deps/wasm-semantics/blockchain-k-plugin/krypto.
 			--backend $* \
 			--md-selector k \
 			--emit-json \
-			-I k-src/elrond-semantics \
-			-I k-src/elrond-semantics/deps/wasm-semantics \
-			-I k-src/summaries \
+			-I k-src \
+			-I k-src/elrond-semantics/deps \
 			--directory ../.build/defn/haskell \
 			--main-module ELROND-WASM \
 			--syntax-module ELROND-WASM-SYNTAX \

kmxwasm/k-src/ceils.k

@@ -305,4 +305,12 @@ module CEILS
         [symbolic(Key), simplification]
 
 
+    // -----------------------------------
+
+    rule #Ceil(#signed(@T:IValType, @N:Int))
+        => {0 <=Int @N andBool @N <Int #pow(@T) #Equals true}
+          #And #Ceil(@T)
+          #And #Ceil(@N)
+          [simplification]
+
 endmodule

kmxwasm/k-src/elrond-lemmas.md

@@ -7,6 +7,7 @@ module ELROND-LEMMAS
   imports public ELROND
   imports public INT-KORE
   imports public SET
+  imports public WASM-TEXT
 
   rule size(_:List) >=Int 0 => true  [simplification, smt-lemma]
 

kmxwasm/k-src/elrond-wasm.md

@@ -1,16 +1,17 @@
 ```k
 require "elrond-lemmas.md"
-require "elrond-wasm-configuration.md"
-require "kwasm-lemmas.md"
+require "wasm-semantics/kwasm-lemmas.md"
 require "proof-extensions.md"
+require "elrond-semantics/foundry.md"
 
 module ELROND-WASM-SYNTAX
   imports WASM-TEXT-SYNTAX
+  imports FOUNDRY-SYNTAX
 endmodule
 
 module ELROND-WASM
   imports ELROND-LEMMAS
-  imports ELROND-WASM-CONFIGURATION
+  imports FOUNDRY
   imports KWASM-LEMMAS
   imports MAP-KORE-SYMBOLIC
   imports PROOF-EXTENSIONS

kmxwasm/k-src/kbuild.toml

@@ -0,0 +1,15 @@
+[project]
+name = "kmxwasm-semantics"
+version = "0.1.0"
+source = "."
+
+[dependencies]
+elrond-semantics={ path = "elrond-semantics" }
+
+[targets.llvm]
+main-file = 'elrond-wasm.md'
+backend='llvm'
+
+[targets.haskell]
+main-file = 'elrond-wasm.md'
+backend='haskell'

kmxwasm/k-src/proof-extensions.md

@@ -1,8 +1,9 @@
 ```k
-require "elrond.md"
+require "elrond-semantics/elrond.md"
 
 module PROOF-EXTENSIONS
   imports ELROND
+  imports WASM
 
   syntax Instr ::= "infiniteLoop"  [symbol, klabel(infiniteLoop)]
   rule <instrs> (infiniteLoop ~> _:KItem => infiniteLoop) ... </instrs>

kmxwasm/src/kmxwasm/ast/collections.py

@@ -0,0 +1,44 @@
+from typing import Iterable
+
+from pyk.kast.inner import KApply, KInner, KLabel
+
+# TODO: Move these to the pyk repository.
+
+
+def simple_list(concat_label: str | KLabel, empty_label: str | KLabel, items: Iterable[KInner]) -> KInner:
+    tail = KApply(empty_label)
+    for item in reversed(list(items)):
+        tail = KApply(concat_label, [item, tail])
+    return tail
+
+
+def full_list(
+    concat_label: str | KLabel, item_label: str | KLabel, empty_label: str | KLabel, items: Iterable[KInner]
+) -> KInner:
+    items_ast = [KApply(item_label, item) for item in items]
+    return simple_list(concat_label=concat_label, empty_label=empty_label, items=items_ast)
+
+
+def k_map(
+    concat_label: str | KLabel, item_label: str | KLabel, empty_label: str | KLabel, items: dict[KInner, KInner]
+) -> KInner:
+    if not items:
+        return KApply(empty_label)
+    items_ast = [KApply(item_label, key, value) for key, value in items.items()]
+    result = items_ast.pop()
+    for item in reversed(items):
+        result = KApply(concat_label, [item, result])
+    return result
+
+
+def cell_map(name: str, items: Iterable[KInner]) -> KInner:
+    items_dict: dict[KInner, KInner] = {}
+    for item in items:
+        if not isinstance(item, KApply):
+            raise ValueError(f'Expected a list of KApply, one item is of type {type(item)}.')
+        if item.arity < 2:
+            raise ValueError(
+                f'Expected a list of KApply with at least two arguments each, one has {item.arity} arguments.'
+            )
+        items_dict[item.args[0]] = item
+    return k_map(concat_label=f'_{name}_', item_label=f'{name}Item', empty_label=f'.{name}', items=items_dict)

kmxwasm/src/kmxwasm/ast/elrond.py

@@ -0,0 +1,24 @@
+from typing import Iterable
+
+from pyk.kast.inner import KInner
+
+from .collections import cell_map, full_list, k_map, simple_list
+
+
+# TODO: Move these to the elrond-semantics repository.
+def listBytes(items: Iterable[KInner]) -> KInner:  # noqa: N802
+    return full_list(concat_label='_ListBytes_', item_label='ListBytesItem', empty_label='.ListBytes', items=items)
+
+
+def mapIntToBytes(int_to_bytes: dict[KInner, KInner]) -> KInner:  # noqa: N802
+    return k_map(
+        concat_label='_MapIntToBytes_', item_label='_Int2Bytes|->_', empty_label='.MapIntToBytes', items=int_to_bytes
+    )
+
+
+def bytesStack(items: Iterable[KInner]) -> KInner:  # noqa: N802
+    return simple_list(concat_label='bytesStackList', empty_label='.List{"bytesStackList"}_BytesStack', items=items)
+
+
+def accountCellMap(accounts: Iterable[KInner]) -> KInner:  # noqa: N802
+    return cell_map(name='AccountCellMap', items=accounts)

kmxwasm/src/kmxwasm/ast/wasm.py

@@ -0,0 +1,35 @@
+from typing import Iterable
+
+from pyk.kast.inner import KApply, KInner
+
+from .collections import cell_map, simple_list
+
+# TODO: Move these to the wasm-semantics repository
+
+
+def funcDefCellMap(func_defs: Iterable[KInner]) -> KInner:  # noqa: N802
+    return cell_map(name='FuncDefCellMap', items=func_defs)
+
+
+def moduleInstCellMap(module_insts: Iterable[KInner]) -> KInner:  # noqa: N802
+    return cell_map(name='ModuleInstCellMap', items=module_insts)
+
+
+def tabInstCellMap(tab_insts: Iterable[KInner]) -> KInner:  # noqa: N802
+    return cell_map(name='TabInstCellMap', items=tab_insts)
+
+
+def memInstCellMap(mem_insts: Iterable[KInner]) -> KInner:  # noqa: N802
+    return cell_map(name='MemInstCellMap', items=mem_insts)
+
+
+def globalInstCellMap(global_insts: Iterable[KInner]) -> KInner:  # noqa: N802
+    return cell_map(name='GlobalInstCellMap', items=global_insts)
+
+
+def valStack(items: Iterable[KInner]) -> KInner:  # noqa: N802
+    return simple_list(concat_label='concatValStack', empty_label='.ValStack', items=items)
+
+
+def optionalInt_empty() -> KInner:  # noqa: N802
+    return KApply('.Int')

kmxwasm/src/kmxwasm/build.py

@@ -0,0 +1,13 @@
+from pathlib import Path
+
+from pyk.kbuild.kbuild import KBuild
+from pyk.kbuild.package import Package
+
+from .tools import Tools
+
+
+def kbuild_semantics(kbuild_dir: Path, ml_file: Path) -> Tools:
+    kbuild = KBuild(kbuild_dir)
+    package = Package.create(ml_file)
+    kbuild.kompile(package, 'haskell')
+    return Tools(kbuild.definition_dir(package, 'haskell'))

kmxwasm/src/kmxwasm/execution.py

@@ -3,6 +3,7 @@
 
 from pyk.kast.inner import KApply, KInner, KSequence, KToken, KVariable
 from pyk.kcfg import KCFG
+from pyk.kcfg.kcfg import NodeIdLike
 from pyk.prelude.k import K
 
 from .functions import Functions
@@ -51,7 +52,7 @@ def __init__(self, functions: Functions, loop_whitelist: Set[str]) -> None:
         self.__executing_addr = -1
         self.__loop_whitelist = loop_whitelist
 
-    def decide_configuration(self, kcfg: KCFG, node_id: int) -> Decision:
+    def decide_configuration(self, kcfg: KCFG, node_id: NodeIdLike) -> Decision:
         node = kcfg.node(node_id)
         instrs = get_instrs_child(node.cterm.config)
 

kmxwasm/src/kmxwasm/paths.py

@@ -0,0 +1,6 @@
+import subprocess
+from pathlib import Path
+
+ROOT = Path(subprocess.check_output(['git', 'rev-parse', '--show-toplevel']).decode().strip())
+KBUILD_DIR = ROOT / '.kbuild'
+KBUILD_ML_PATH = ROOT / 'kmxwasm/k-src/kbuild.toml'

kmxwasm/src/kmxwasm/proofs.py

@@ -75,7 +75,11 @@ def __init__(
         extra_unparsing_modules: Iterable[KFlatModule] = (),
     ) -> None:
         super().__init__(
-            definition_dir, use_directory, bug_report, extra_unparsing_modules, MyKPrint._my_patch_symbol_table
+            definition_dir,
+            use_directory,
+            bug_report,
+            extra_unparsing_modules,
+            patch_symbol_table=MyKPrint._my_patch_symbol_table,
         )
 
     @classmethod
@@ -84,8 +88,39 @@ def _my_patch_symbol_table(cls, symbol_table: SymbolTable) -> None:
         symbol_table['_Map_'] = lambda c1, c2: f'({c1} {c2})'
         symbol_table['_Int2Bytes|->_'] = lambda c1, c2: f'({c1} Int2Bytes|-> {c2})'
         symbol_table['_MapIntwToBytesw_'] = lambda c1, c2: f'({c1} {c2})'
+        symbol_table['_MapIntwToBytesw_'] = lambda c1, c2: f'({c1} {c2})'
+        symbol_table['MapIntswToBytesw:curly_update'] = lambda c1, c2, c3: f'({c1}){{ {c2} <- {c3} }}'
+        symbol_table['_Bytes2Bytes|->_'] = lambda c1, c2: f'({c1} Bytes2Bytes|-> {c2})'
+        symbol_table['_MapByteswToBytesw_'] = lambda c1, c2: f'({c1} {c2})'
+        symbol_table['MapByteswToBytesw:curly_update'] = lambda c1, c2, c3: f'({c1}){{ {c2} <- {c3} }}'
+        symbol_table['_Int2Int|->_'] = lambda c1, c2: f'({c1} Int2Int|-> {c2})'
+        symbol_table['_MapIntwToIntw_'] = lambda c1, c2: f'({c1} {c2})'
+        symbol_table['MapIntwToIntw:curly_update'] = lambda c1, c2, c3: f'({c1}){{ {c2} <- {c3} }}'
         symbol_table['.TabInstCellMap'] = lambda: '.Bag'
+
         symbol_table['notBool_'] = lambda c1: f'notBool ({c1})'
+        symbol_table['_andBool_'] = lambda c1, c2: f'({c1}) andBool ({c2})'
+        symbol_table['_orBool_'] = lambda c1, c2: f'({c1}) orBool ({c2})'
+        symbol_table['_andThenBool_'] = lambda c1, c2: f'({c1}) andThenBool ({c2})'
+        symbol_table['_xorBool_'] = lambda c1, c2: f'({c1}) xorBool ({c2})'
+        symbol_table['_orElseBool_'] = lambda c1, c2: f'({c1}) orElseBool ({c2})'
+        symbol_table['_impliesBool_'] = lambda c1, c2: f'({c1}) impliesBool ({c2})'
+
+        symbol_table['~Int_'] = lambda c1: f'~Int ({c1})'
+        symbol_table['_modInt_'] = lambda c1, c2: f'({c1}) modInt ({c2})'
+        symbol_table['_modIntTotal_'] = lambda c1, c2: f'({c1}) modIntTotal ({c2})'
+        symbol_table['_*Int_'] = lambda c1, c2: f'({c1}) *Int ({c2})'
+        symbol_table['_/Int_'] = lambda c1, c2: f'({c1}) /Int ({c2})'
+        symbol_table['_%Int_'] = lambda c1, c2: f'({c1}) %Int ({c2})'
+        symbol_table['_^Int_'] = lambda c1, c2: f'({c1}) ^Int ({c2})'
+        symbol_table['_^%Int_'] = lambda c1, c2: f'({c1}) ^%Int ({c2})'
+        symbol_table['_+Int_'] = lambda c1, c2: f'({c1}) +Int ({c2})'
+        symbol_table['_-Int_'] = lambda c1, c2: f'({c1}) -Int ({c2})'
+        symbol_table['_>>Int_'] = lambda c1, c2: f'({c1}) >>Int ({c2})'
+        symbol_table['_<<Int_'] = lambda c1, c2: f'({c1}) <<Int ({c2})'
+        symbol_table['_&Int_'] = lambda c1, c2: f'({c1}) &Int ({c2})'
+        symbol_table['_xorInt_'] = lambda c1, c2: f'({c1}) xorInt ({c2})'
+        symbol_table['_|Int_'] = lambda c1, c2: f'({c1}) |Int ({c2})'
 
 
 def filter_bytes(term: KToken) -> KInner:

kmxwasm/src/kmxwasm/property.py

@@ -0,0 +1,30 @@
+#!/usr/bin/env python3
+
+import sys
+from pathlib import Path
+
+from .build import kbuild_semantics
+from .paths import KBUILD_DIR, KBUILD_ML_PATH
+from .running import run_claim
+
+
+def main(args: list[str]) -> None:
+    if len(args) != 1:
+        print('Usage:')
+        print('  python3 -m kmxwasm.property <claim-file>')
+        sys.exit(-1)
+    claim_path = Path(args[0])
+    if not claim_path.exists():
+        print(f'Input file ({claim_path}) does not exist.')
+        sys.exit(-1)
+    definition = kbuild_semantics(KBUILD_DIR, KBUILD_ML_PATH)
+    claims = definition.kprove.get_claims(claim_path)
+    if len(claims) != 1:
+        print(f'Expected exactly one claim in {claim_path}, found {len(claims)}.')
+        sys.exit(-1)
+    claim = claims[0]
+    run_claim(definition, claim)
+
+
+if __name__ == '__main__':
+    main(sys.argv[1:])

kmxwasm/src/kmxwasm/rules.py

@@ -4,6 +4,7 @@
 from pyk.kast.manip import ml_pred_to_bool
 from pyk.kast.outer import KAtt, KRule
 from pyk.kcfg import KCFG
+from pyk.kcfg.kcfg import NodeIdLike
 from pyk.prelude.kbool import TRUE, andBool
 
 from .kast import (
@@ -23,7 +24,7 @@ def __init__(self, priority: int) -> None:
         self.__rules: List[KRule] = []
         self.__priority = priority
 
-    def add_rule(self, lhs_id: int, rhs_id: int, kcfg: KCFG) -> None:
+    def add_rule(self, lhs_id: NodeIdLike, rhs_id: NodeIdLike, kcfg: KCFG) -> None:
         lhs_cterm = kcfg.node(lhs_id).cterm
         rhs_cterm = kcfg.node(rhs_id).cterm