Skip to content

Commit

Permalink
Implement i64 and i128 Types and Host Functions (#45)
Browse files Browse the repository at this point in the history 
* implement `i64`

* implement `i128`

* add komet tests for i128 operations

* `test_adder`: add `i64` and `i128` tests

* Set Version: 0.1.38

* Set Version: 0.1.39

* enable `--id` argument in `komet prove`

* update `test_prove_adder` to use `--id` argument to skip new properties

* Set Version: 0.1.42

---------

Co-authored-by: devops <[email protected]>
  • Loading branch information
@bbyalcinkaya
bbyalcinkaya and devops authored Nov 19, 2024
1 parent 50117c0 commit f689855
Show file tree
Hide file tree
Showing 13 changed files with 429 additions and 10 deletions.
2 changes: 1 addition & 1 deletion package/version
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.41
0.1.42
2 changes: 1 addition & 1 deletion pyproject.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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. <[email protected]>",
Expand Down
7 changes: 4 additions & 3 deletions src/komet/kasmer.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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)
Expand Down
33 changes: 32 additions & 1 deletion src/komet/kdist/soroban-semantics/data.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<HostVal>
| ScMap(Map) [symbol(SCVal:Map)] // Map<ScVal, HostVal>
| ScAddress(Address) [symbol(SCVal:Address)]
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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
```
57 changes: 57 additions & 0 deletions src/komet/kdist/soroban-semantics/host/integer.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,17 @@ module HOST-INTEGER
</locals>
<k> (.K => allocObject(U64(I))) ... </k>
rule [hostfun-obj-from-i64]:
<instrs> hostCall ( "i" , "1" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> allocObject(I64(#signed(i64, VAL)))
~> returnHostVal
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
requires definedSigned(i64, VAL)
rule [hostfun-obj-to-i64]:
<instrs> hostCall ( "i" , "2" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
Expand Down Expand Up @@ -99,5 +110,51 @@ module HOST-INTEGER
<hostStack> U128(I) : S => S </hostStack>
[preserves-definedness] // 'X >>Int K' is defined for positive K
rule [hostfun-obj-from-i128-pieces]:
<instrs> hostCall ( "i" , "6" , [ i64 i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> allocObject(I128(#signed(i128, (HIGH <<Int 64) |Int LOW )))
~> returnHostVal
...
</instrs>
<locals>
0 |-> < i64 > HIGH
1 |-> < i64 > LOW
</locals>
requires definedSigned(i128, (HIGH <<Int 64) |Int LOW )
rule [hostfun-obj-to-i128-lo64]:
<instrs> hostCall ( "i" , "7" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
~> i128lo64
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
syntax InternalInstr ::= "i128lo64" [symbol(i128lo64)]
// --------------------------------------------------------
rule [i128lo64]:
<instrs> i128lo64 => i64.const (#unsigned(i128, I)) ... </instrs>
<hostStack> I128(I) : S => S </hostStack>
requires definedUnsigned(i128, I)
[preserves-definedness]
rule [hostfun-obj-to-i128-hi64]:
<instrs> hostCall ( "i" , "8" , [ i64 .ValTypes ] -> [ i64 .ValTypes ] )
=> loadObject(HostVal(VAL))
~> i128hi64
...
</instrs>
<locals>
0 |-> < i64 > VAL
</locals>
syntax InternalInstr ::= "i128hi64" [symbol(i128hi64)]
// --------------------------------------------------------
rule [i128hi64]:
<instrs> i128hi64 => i64.const (I >>Int 64) ... </instrs>
<hostStack> I128(I) : S => S </hostStack>
endmodule
```
8 changes: 5 additions & 3 deletions src/komet/komet.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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, ...] = ()
Expand All @@ -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)

Expand Down
150 changes: 150 additions & 0 deletions src/tests/integration/data/i128.wast
View file
Original file line number Diff line number Diff line change
@@ -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)
Loading

0 comments on commit f689855

Please sign in to comment.