diff --git a/package/version b/package/version index 37f868fb..4a3e97d0 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.41 +0.1.42 diff --git a/pyproject.toml b/pyproject.toml index 21c083f1..f1879430 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.41" +version = "0.1.42" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ", diff --git a/src/komet/kasmer.py b/src/komet/kasmer.py index 0507724f..a33617b7 100644 --- a/src/komet/kasmer.py +++ b/src/komet/kasmer.py @@ -270,6 +270,7 @@ def deploy_and_prove( self, contract_wasm: Path, child_wasms: tuple[Path, ...], + id: str | None = None, proof_dir: Path | None = None, bug_report: BugReport | None = None, ) -> None: @@ -290,9 +291,9 @@ def deploy_and_prove( conf, subst = self.deploy_test(contract_kast, child_kasts, has_init) - for binding in bindings: - if not binding.name.startswith('test_'): - continue + 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: proof = self.run_prove(conf, subst, binding, proof_dir, bug_report) if proof.status == ProofStatus.FAILED: raise KSorobanError(proof.summary) diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index b33b5c68..1df7297a 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -59,6 +59,7 @@ various contexts: | U64(Int) [symbol(SCVal:U64)] | I64(Int) [symbol(SCVal:I64)] | U128(Int) [symbol(SCVal:U128)] + | I128(Int) [symbol(SCVal:I128)] | ScVec(List) [symbol(SCVal:Vec)] // List | ScMap(Map) [symbol(SCVal:Map)] // Map | ScAddress(Address) [symbol(SCVal:Address)] @@ -151,9 +152,12 @@ module HOST-OBJECT rule getTag(I32(_)) => 5 rule getTag(U64(I)) => 6 requires I <=Int #maxU64small rule getTag(U64(I)) => 64 requires notBool( I <=Int #maxU64small ) - rule getTag(I64(_)) => 65 // I64small is not implemented + rule getTag(I64(I)) => 7 requires #minI64small <=Int I andBool I <=Int #maxI64small + rule getTag(I64(I)) => 65 requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small ) rule getTag(U128(I)) => 10 requires I <=Int #maxU64small rule getTag(U128(I)) => 68 requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width + rule getTag(I128(I)) => 11 requires #minI64small <=Int I andBool I <=Int #maxI64small + rule getTag(I128(I)) => 69 requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small ) rule getTag(ScVec(_)) => 75 rule getTag(ScMap(_)) => 76 rule getTag(ScAddress(_)) => 77 @@ -225,8 +229,16 @@ module HOST-OBJECT rule fromSmall(VAL) => U64(getBody(VAL)) requires getTag(VAL) ==Int 6 + rule fromSmall(VAL) => I64(#signed(i56, getBody(VAL))) + requires getTag(VAL) ==Int 7 + andBool definedSigned(i56, getBody(VAL)) + rule fromSmall(VAL) => U128(getBody(VAL)) requires getTag(VAL) ==Int 10 + rule fromSmall(VAL) => I128(#signed(i56, getBody(VAL))) + requires getTag(VAL) ==Int 11 + andBool definedSigned(i56, getBody(VAL)) + rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL))) requires getTag(VAL) ==Int 14 @@ -249,7 +261,13 @@ module HOST-OBJECT rule toSmall(I32(I)) => fromMajorMinorAndTag(#unsigned(i32, I), 0, 5) requires definedUnsigned(i32, I) rule toSmall(U64(I)) => fromBodyAndTag(I, 6) requires I <=Int #maxU64small + rule toSmall(I64(I)) => fromBodyAndTag(#unsigned(i56, I), 7) + requires #minI64small <=Int I andBool I <=Int #maxI64small + andBool definedUnsigned(i56, I) rule toSmall(U128(I)) => fromBodyAndTag(I, 10) requires I <=Int #maxU64small + rule toSmall(I128(I)) => fromBodyAndTag(#unsigned(i56, I), 11) + requires #minI64small <=Int I andBool I <=Int #maxI64small + andBool definedUnsigned(i56, I) rule toSmall(Symbol(S)) => fromBodyAndTag(encode6bit(S), 14) requires lengthString(S) <=Int 9 rule toSmall(_) => HostVal(-1) [owise] @@ -307,5 +325,18 @@ module HOST-OBJECT rule tail(S) => "" requires lengthString(S) <=Int 0 rule tail(S) => substrString(S, 1, lengthString(S)) requires lengthString(S) >Int 0 + // 56-bit integers for small values + syntax IWidth ::= "i56" + // ------------------------------------ + rule #width(i56) => 56 + rule #pow(i56) => 72057594037927936 + rule #pow1(i56) => 36028797018963968 + + syntax IWidth ::= "i128" + // ------------------------------------ + rule #width(i128) => 128 + rule #pow(i128) => 340282366920938463463374607431768211456 + rule #pow1(i128) => 170141183460469231731687303715884105728 + endmodule ``` diff --git a/src/komet/kdist/soroban-semantics/host/integer.md b/src/komet/kdist/soroban-semantics/host/integer.md index de1bcb98..959b5a03 100644 --- a/src/komet/kdist/soroban-semantics/host/integer.md +++ b/src/komet/kdist/soroban-semantics/host/integer.md @@ -44,6 +44,17 @@ module HOST-INTEGER (.K => allocObject(U64(I))) ... + rule [hostfun-obj-from-i64]: + hostCall ( "i" , "1" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => allocObject(I64(#signed(i64, VAL))) + ~> returnHostVal + ... + + + 0 |-> < i64 > VAL + + requires definedSigned(i64, VAL) + rule [hostfun-obj-to-i64]: hostCall ( "i" , "2" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) => loadObject(HostVal(VAL)) @@ -99,5 +110,51 @@ module HOST-INTEGER U128(I) : S => S [preserves-definedness] // 'X >>Int K' is defined for positive K + rule [hostfun-obj-from-i128-pieces]: + hostCall ( "i" , "6" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => allocObject(I128(#signed(i128, (HIGH < returnHostVal + ... + + + 0 |-> < i64 > HIGH + 1 |-> < i64 > LOW + + requires definedSigned(i128, (HIGH < hostCall ( "i" , "7" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VAL)) + ~> i128lo64 + ... + + + 0 |-> < i64 > VAL + + + syntax InternalInstr ::= "i128lo64" [symbol(i128lo64)] + // -------------------------------------------------------- + rule [i128lo64]: + i128lo64 => i64.const (#unsigned(i128, I)) ... + I128(I) : S => S + requires definedUnsigned(i128, I) + [preserves-definedness] + + rule [hostfun-obj-to-i128-hi64]: + hostCall ( "i" , "8" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => loadObject(HostVal(VAL)) + ~> i128hi64 + ... + + + 0 |-> < i64 > VAL + + + syntax InternalInstr ::= "i128hi64" [symbol(i128hi64)] + // -------------------------------------------------------- + rule [i128hi64]: + i128hi64 => i64.const (I >>Int 64) ... + I128(I) : S => S + endmodule ``` \ No newline at end of file diff --git a/src/komet/komet.py b/src/komet/komet.py index fd1fc6dd..b00d0dc6 100644 --- a/src/komet/komet.py +++ b/src/komet/komet.py @@ -51,7 +51,7 @@ def main() -> None: 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, bug_report=args.bug_report) + _exec_prove_run(wasm=wasm, id=args.id, proof_dir=args.proof_dir, bug_report=args.bug_report) if args.prove_command == 'view': assert args.proof_dir is not None _exec_prove_view(proof_dir=args.proof_dir, id=args.id) @@ -101,7 +101,9 @@ def _exec_test(*, wasm: Path | None) -> None: sys.exit(0) -def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None, bug_report: BugReport | None = None) -> None: +def _exec_prove_run( + *, wasm: Path | None, id: str | None, proof_dir: Path | None, bug_report: BugReport | None = None +) -> None: kasmer = Kasmer(symbolic_definition) child_wasms: tuple[Path, ...] = () @@ -110,7 +112,7 @@ def _exec_prove_run(*, wasm: Path | None, proof_dir: Path | None, bug_report: Bu wasm = kasmer.build_soroban_contract(Path.cwd()) child_wasms = _read_config_file() - kasmer.deploy_and_prove(wasm, child_wasms, proof_dir, bug_report) + kasmer.deploy_and_prove(wasm, child_wasms, id, proof_dir, bug_report) sys.exit(0) diff --git a/src/tests/integration/data/i128.wast b/src/tests/integration/data/i128.wast new file mode 100644 index 00000000..39676035 --- /dev/null +++ b/src/tests/integration/data/i128.wast @@ -0,0 +1,150 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $test_wasm + (import "i" "_" (func $obj_from_u64 (param i64) (result i64))) + (import "i" "1" (func $obj_from_i64 (param i64) (result i64))) + (import "i" "6" (func $obj_from_i128_pieces (param i64 i64) (result i64))) + (import "i" "7" (func $obj_to_i128_lo64 (param i64) (result i64))) + (import "i" "8" (func $obj_to_i128_hi64 (param i64) (result i64))) + (func $lo (param i64) (result i64) + local.get 0 + call $obj_to_i128_lo64 + call $obj_from_u64 + ) + (func $hi (param i64) (result i64) + local.get 0 + call $obj_to_i128_hi64 + call $obj_from_i64 + ) + (func $roundtrip (param i64) (result i64) + (call $obj_from_i128_pieces + (call $obj_to_i128_hi64 (local.get 0)) + (call $obj_to_i128_lo64 (local.get 0)) + ) + ) + (export "lo" (func $lo)) + (export "hi" (func $hi)) + (export "roundtrip" (func $roundtrip)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ;; i128::MAX + ListItem(I128(2 ^Int 127 -Int 1)), + U64(2 ^Int 64 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ListItem(I128(0 -Int 2 ^Int 127)), ;; i128::MIN + U64(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ListItem(I128(0)), + U64(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "lo", + ListItem(I128(-1)), + U64(2 ^Int 64 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ;; 2^127-1 (i128::MAX) + ListItem(I128(2 ^Int 127 -Int 1)), + I64(9223372036854775807) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(0 -Int 2 ^Int 127)), ;; i128::MIN + I64(0 -Int 2 ^Int 63) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(0)), + I64(0) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(-1)), + I64(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hi", + ListItem(I128(-2)), + I64(-1) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(0)), + I128(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(170141183460469231731687303715884105727)), + I128(170141183460469231731687303715884105727) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(-1)), + I128(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I128(-170141183460469231731687303715884105727)), + I128(-170141183460469231731687303715884105727) +) + + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/i64.wast b/src/tests/integration/data/i64.wast new file mode 100644 index 00000000..78c95652 --- /dev/null +++ b/src/tests/integration/data/i64.wast @@ -0,0 +1,66 @@ + +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $test_wasm + (import "i" "1" (func $obj_from_i64 (param i64) (result i64))) + (import "i" "2" (func $obj_to_i64 (param i64) (result i64))) + (func $roundtrip (param i64) (result i64) + (call $obj_from_i64 + (call $obj_to_i64 (local.get 0)) + ) + ) + (export "roundtrip" (func $roundtrip)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(1)), + I64(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(0)), + I64(0) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(-1)), + I64(-1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(2 ^Int 63 -Int 1)), + I64(2 ^Int 63 -Int 1) +) + + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I64(0 -Int 2 ^Int 63)), + I64(0 -Int 2 ^Int 63) +) + +setExitCode(0) \ No newline at end of file diff --git a/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs index 45cf218e..297b52cf 100644 --- a/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_adder/src/lib.rs @@ -10,10 +10,36 @@ impl AdderContract { first as u64 + second as u64 } + + pub fn add_i64(env: Env, first: i64, second: i64) -> i128 { + first as i128 + second as i128 + } + + pub fn increment_i128(env: Env, x: i128) -> i128 { + x + 1 + } + + ///////////////////////////////////////////////////////////////////// + /// Properties + /// + pub fn test_add(env: Env, num: u32) -> bool { let sum = Self::add(env, num, 5); sum == num as u64 + 5 } + + + pub fn test_add_i64_comm(env: Env, first: i64, second: i64) -> bool { + let a = Self::add_i64(env.clone(), first, second); + let b = Self::add_i64(env, second, first); + + a == b + } + + pub fn test_increment_i128(env: Env, x: i128) -> bool { + x == i128::MAX || x == Self::increment_i128(env, x) - 1 + } + } mod test; diff --git a/src/tests/integration/data/soroban/contracts/test_integers/Cargo.toml b/src/tests/integration/data/soroban/contracts/test_integers/Cargo.toml new file mode 100644 index 00000000..fdee533e --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_integers/Cargo.toml @@ -0,0 +1,15 @@ +[package] +name = "test_integers" +version = "0.0.0" +edition = "2021" +publish = false + +[lib] +crate-type = ["cdylib"] +doctest = false + +[dependencies] +soroban-sdk = { workspace = true } + +[dev-dependencies] +soroban-sdk = { workspace = true, features = ["testutils"] } diff --git a/src/tests/integration/data/soroban/contracts/test_integers/README.md b/src/tests/integration/data/soroban/contracts/test_integers/README.md new file mode 100644 index 00000000..10424c19 --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_integers/README.md @@ -0,0 +1,18 @@ +A quick example of a contract that can be ran with `komet test` + +You will need to have the stellar cli utils installed: +https://developers.stellar.org/docs/build/smart-contracts/getting-started/setup + +And the soroban semantics kompiled: +``` +kdist build soroban-semantics.llvm +``` + +And then (from this directory): + +```sh +soroban contract build --out-dir output +komet test output/test_integers.wasm +``` + +`komet test` should exit successfully diff --git a/src/tests/integration/data/soroban/contracts/test_integers/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_integers/src/lib.rs new file mode 100644 index 00000000..7359423a --- /dev/null +++ b/src/tests/integration/data/soroban/contracts/test_integers/src/lib.rs @@ -0,0 +1,53 @@ +#![no_std] +use soroban_sdk::{contract, contractimpl, xdr::{int128_helpers::{i128_from_pieces, i128_hi, i128_lo}, FromXdr, ScVal}, Env, Val}; + +#[contract] +pub struct TestIntegersContract; + +#[contractimpl] +impl TestIntegersContract { + + pub fn i128_hi(_env: Env, x: i128) -> i64 { + i128_hi(x) + } + + pub fn i128_lo(_env: Env, x: i128) -> u64 { + i128_lo(x) + } + + pub fn i128_from_pieces(_env: Env, hi: i64, lo: u64) -> i128 { + i128_from_pieces(hi, lo) + } + + ///////////////////////////////////////////////////////////////////// + /// Properties + /// + + pub fn test_i128_roundtrip(env: Env, x: i128) -> bool { + let hi = Self::i128_hi(env.clone(), x); + let lo = Self::i128_lo(env.clone(), x); + let y = Self::i128_from_pieces(env, hi, lo); + + x == y + } + + pub fn test_i128_roundtrip_2(env: Env, hi: i64, lo: u64) -> bool { + let x = Self::i128_from_pieces(env.clone(), hi, lo); + let hi2 = Self::i128_hi(env.clone(), x); + let lo2 = Self::i128_lo(env, x); + + hi == hi2 && lo == lo2 + } + + // hi < 0 iff x < 0 + pub fn test_i128_hi_negativity(env: Env, x: i128) -> bool { + let hi = Self::i128_hi(env, x); + (x < 0) == (hi < 0) + } + + // hi < 0 iff x < 0 + pub fn test_i128_hi_negativity_2(env: Env, hi: i64, lo: u64) -> bool { + let x = Self::i128_from_pieces(env, hi, lo); + (x < 0) == (hi < 0) + } +} diff --git a/src/tests/integration/test_integration.py b/src/tests/integration/test_integration.py index 35826f55..e0ac2233 100644 --- a/src/tests/integration/test_integration.py +++ b/src/tests/integration/test_integration.py @@ -51,7 +51,7 @@ def test_prove_adder(tmp_path: Path, symbolic_kasmer: Kasmer) -> None: contract_wasm = symbolic_kasmer.build_soroban_contract(SOROBAN_CONTRACTS_DIR / 'test_adder', tmp_path) # Then - symbolic_kasmer.deploy_and_prove(contract_wasm, (), tmp_path) + symbolic_kasmer.deploy_and_prove(contract_wasm, (), 'test_add', tmp_path) def test_bindings(tmp_path: Path, concrete_kasmer: Kasmer) -> None: