Implement i64 and i128 Types and Host Functions

package/version

@@ -1 +1 @@
-0.1.41
+0.1.42

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. <[email protected]>",

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)

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<HostVal>
         | ScMap(Map)                               [symbol(SCVal:Map)]      // Map<ScVal, HostVal>
         | 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
 ```

src/komet/kdist/soroban-semantics/host/integer.md

@@ -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))
@@ -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
 ```

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)
 

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)