Implement missing host calls

package/version

@@ -1 +1 @@
-0.1.86
+0.1.89

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "komet"
-version = "0.1.88"
+version = "0.1.89"
 description = "K tooling for the Soroban platform"
 requires-python = "~=3.10"
 dependencies = [

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

@@ -61,6 +61,7 @@ various contexts:
         | U128(Int)                                [symbol(SCVal:U128)]
         | I128(Int)                                [symbol(SCVal:I128)]
         | U256(Int)                                [symbol(SCVal:U256)]
+        | I256(Int)                                [symbol(SCVal:I256)]
         | ScVec(List)                              [symbol(SCVal:Vec)]      // List<HostVal> or List<ScVal>
         | ScMap(Map)                               [symbol(SCVal:Map)]      // Map<ScVal, HostVal> or Map<ScVal, ScVal>
         | ScAddress(Address)                       [symbol(SCVal:Address)]
@@ -162,6 +163,8 @@ module HOST-OBJECT
     rule getTag(I128(I))       => 69    requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small )
     rule getTag(U256(I))       => 12    requires          I <=Int #maxU64small
     rule getTag(U256(I))       => 70    requires notBool( I <=Int #maxU64small ) // U64small and U128small have the same width
+    rule getTag(I256(I))       => 13    requires          #minI64small <=Int I andBool I <=Int #maxI64small
+    rule getTag(I256(I))       => 71    requires notBool( #minI64small <=Int I andBool I <=Int #maxI64small )
     rule getTag(ScVec(_))      => 75
     rule getTag(ScMap(_))      => 76
     rule getTag(ScAddress(_))  => 77
@@ -285,6 +288,10 @@ module HOST-OBJECT
 
     rule fromSmall(VAL) => U256(getBody(VAL))      requires getTag(VAL) ==Int 12
 
+    rule fromSmall(VAL) => I256(#signed(i56, getBody(VAL)))
+      requires getTag(VAL) ==Int 13
+       andBool definedSigned(i56, getBody(VAL))
+
     rule fromSmall(VAL) => Symbol(decode6bit(getBody(VAL)))
                                                    requires getTag(VAL) ==Int 14
 
@@ -315,6 +322,9 @@ module HOST-OBJECT
       requires #minI64small <=Int I andBool I <=Int #maxI64small
        andBool definedUnsigned(i56, I)
     rule toSmall(U256(I))       => fromBodyAndTag(I, 12)              requires I <=Int #maxU64small
+    rule toSmall(I256(I))       => fromBodyAndTag(#unsigned(i56, I), 13)
+      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]
 
@@ -449,6 +459,7 @@ For scalar types the comparison is straightforward.
     rule compare(U128(A), U128(B)) => compareInt(A, B)
     rule compare(I128(A), I128(B)) => compareInt(A, B)
     rule compare(U256(A), U256(B)) => compareInt(A, B)
+    rule compare(I256(A), I256(B)) => compareInt(A, B)
     rule compare(ScAddress(A), ScAddress(B)) => compareAddress(A, B)
     rule compare(Symbol(A), Symbol(B))       => compareString(A, B)
     rule compare(ScBytes(A), ScBytes(B))     => compareBytes(A, B)
@@ -570,6 +581,7 @@ corresponding values.
     rule ScValTypeOrd(U128(_))       => 9
     rule ScValTypeOrd(I128(_))       => 10
     rule ScValTypeOrd(U256(_))       => 11
+    rule ScValTypeOrd(I256(_))       => 12
     rule ScValTypeOrd(ScBytes(_))    => 13
     rule ScValTypeOrd(ScString(_))   => 14
     rule ScValTypeOrd(Symbol(_))     => 15

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

@@ -242,6 +242,225 @@ Convert a 32-byte `Bytes` object to `U256`.
       requires 0 =/=Int B
 ```
 
+## obj_from_i256_pieces
+
+The four words are the two's-complement representation of the value, most
+significant first, so they are reassembled as an unsigned 256-bit number and
+then reinterpreted as signed.
+
+```k
+    rule [hostfun-obj-from-i256-pieces]:
+        <instrs> hostCall ( "i" , "g" , [ i64 i64 i64  i64  .ValTypes ] -> [ i64  .ValTypes ] )
+              => allocObject( I256( #signed(i256,
+                       (HI_HI <<Int 192)
+                  |Int (HI_LO <<Int 128)
+                  |Int (LO_HI <<Int 64)
+                  |Int  LO_LO
+                )))
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <locals>
+          0 |-> < i64 > HI_HI
+          1 |-> < i64 > HI_LO
+          2 |-> < i64 > LO_HI
+          3 |-> < i64 > LO_LO
+        </locals>
+      requires definedSigned(i256,
+                   (HI_HI <<Int 192)
+              |Int (HI_LO <<Int 128)
+              |Int (LO_HI <<Int 64)
+              |Int  LO_LO
+             )
+```
+
+## i256_val_from_be_bytes
+
+Convert a 32-byte `Bytes` object to `I256`, sign-extending from the high bit.
+
+```k
+    rule [hostCallAux-i256-val-from-be-bytes]:
+        <instrs> hostCallAux ( "i" , "h" )
+              => allocObject( I256( Bytes2Int(BS, BE, Signed) ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> ScBytes(BS) : S => S </hostStack>
+      requires lengthBytes(BS) ==Int 32
+```
+
+## i256_val_to_be_bytes
+
+```k
+    rule [hostCallAux-i256-val-to-be-bytes]:
+        <instrs> hostCallAux ( "i" , "i" )
+              => allocObject( ScBytes( Int2Bytes(32, #unsigned(i256, I), BE) ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> I256(I) : S => S </hostStack>
+      requires definedUnsigned(i256, I)
+      [preserves-definedness] // definedness of '#unsigned(,)' is checked
+```
+
+## obj_to_i256_hi_hi
+
+The extractors return the words of the two's-complement representation, so a
+negative value is converted to its unsigned form before shifting.
+(`i64.const N` chops `N` to 64 bits, so the lower words need no masking.)
+
+```k
+    rule [hostCallAux-obj-to-i256-hi-hi]:
+        <instrs> hostCallAux ( "i" , "j" ) => i64.const (#unsigned(i256, I) >>Int 192) ... </instrs>
+        <hostStack> I256(I) : S => S </hostStack>
+      requires definedUnsigned(i256, I)
+      [preserves-definedness]
+```
+
+## obj_to_i256_hi_lo
+
+```k
+    rule [hostCallAux-obj-to-i256-hi-lo]:
+        <instrs> hostCallAux ( "i" , "k" ) => i64.const (#unsigned(i256, I) >>Int 128) ... </instrs>
+        <hostStack> I256(I) : S => S </hostStack>
+      requires definedUnsigned(i256, I)
+      [preserves-definedness]
+```
+
+## obj_to_i256_lo_hi
+
+```k
+    rule [hostCallAux-obj-to-i256-lo-hi]:
+        <instrs> hostCallAux ( "i" , "l" ) => i64.const (#unsigned(i256, I) >>Int 64) ... </instrs>
+        <hostStack> I256(I) : S => S </hostStack>
+      requires definedUnsigned(i256, I)
+      [preserves-definedness]
+```
+
+## obj_to_i256_lo_lo
+
+```k
+    rule [hostCallAux-obj-to-i256-lo-lo]:
+        <instrs> hostCallAux ( "i" , "m" ) => i64.const (#unsigned(i256, I)) ... </instrs>
+        <hostStack> I256(I) : S => S </hostStack>
+      requires definedUnsigned(i256, I)
+      [preserves-definedness]
+```
+
+## i256_add
+
+The i256 arithmetic host functions are *checked*: the result must be
+representable, and the divisor must be non-zero. Otherwise the host fails the
+call with `(ErrValue, ArithDomain)` rather than wrapping around.
+
+The first Wasm argument is on top of the host stack (`loadArgs` pushes the
+arguments in reverse), so `A` is the left-hand side.
+
+```k
+    rule [hostCallAux-i256-add]:
+        <instrs> hostCallAux ( "i" , "v" )
+              => allocObject( I256( A +Int B ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires inRangeInt(i256, Signed, A +Int B)
+
+    rule [hostCallAux-i256-add-overflow]:
+        <instrs> hostCallAux ( "i" , "v" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires notBool inRangeInt(i256, Signed, A +Int B)
+```
+
+## i256_sub
+
+```k
+    rule [hostCallAux-i256-sub]:
+        <instrs> hostCallAux ( "i" , "w" )
+              => allocObject( I256( A -Int B ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires inRangeInt(i256, Signed, A -Int B)
+
+    rule [hostCallAux-i256-sub-overflow]:
+        <instrs> hostCallAux ( "i" , "w" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires notBool inRangeInt(i256, Signed, A -Int B)
+```
+
+## i256_mul
+
+```k
+    rule [hostCallAux-i256-mul]:
+        <instrs> hostCallAux ( "i" , "x" )
+              => allocObject( I256( A *Int B ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires inRangeInt(i256, Signed, A *Int B)
+
+    rule [hostCallAux-i256-mul-overflow]:
+        <instrs> hostCallAux ( "i" , "x" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires notBool inRangeInt(i256, Signed, A *Int B)
+```
+
+## i256_div
+
+Division truncates toward zero (K's `/Int`), matching Rust's `i256` division.
+`i256::MIN / -1` is the one quotient that leaves the range; it is named directly
+rather than range-checking `A /Int B`, so no side condition divides.
+
+```k
+    rule [hostCallAux-i256-div]:
+        <instrs> hostCallAux ( "i" , "y" )
+              => allocObject( I256( A /Int B ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires B =/=Int 0
+       andBool notBool (A ==Int minInt(i256, Signed) andBool B ==Int -1)
+      [preserves-definedness] // 'A /Int B' is defined for non-zero B
+
+    rule [hostCallAux-i256-div-by-zero]:
+        <instrs> hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <hostStack> I256(_A) : I256(B) : S => S </hostStack>
+      requires B ==Int 0
+
+    rule [hostCallAux-i256-div-overflow]:
+        <instrs> hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires A ==Int minInt(i256, Signed) andBool B ==Int -1
+```
+
+## i256_rem_euclid
+
+Euclidean modulo: the result is always non-negative, whatever the signs of the
+operands. K's `modInt` takes the sign of its divisor, so dividing by `absInt(B)`
+gives exactly Rust's `rem_euclid`. The quotient never leaves the range, so a
+zero divisor is the only failure.
+
+```k
+    rule [hostCallAux-i256-rem-euclid]:
+        <instrs> hostCallAux ( "i" , "z" )
+              => allocObject( I256( A modInt absInt(B) ) )
+              ~> returnHostVal
+                 ...
+        </instrs>
+        <hostStack> I256(A) : I256(B) : S => S </hostStack>
+      requires B =/=Int 0
+      [preserves-definedness] // 'A modInt absInt(B)' is defined for non-zero B
+
+    rule [hostCallAux-i256-rem-euclid-error]:
+        <instrs> hostCallAux ( "i" , "z" ) => #throw(ErrValue, ArithDomain) ... </instrs>
+        <hostStack> I256(_A) : I256(B) : S => S </hostStack>
+      requires B ==Int 0
+```
+
 ```k
 endmodule
 ```

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

@@ -294,6 +294,15 @@ module HOST-LEDGER
       requires THRESHOLD <=Int EXTEND_TO   // input is valid
        andBool SEQ <=Int LIVE_UNTIL        // entry is still alive
 
+  // An invalid threshold or an expired instance leaves nothing to extend. Fail
+  // the host call the way `extendContractDataTtl-err` fails the data-entry case,
+  // rather than getting stuck: a stuck interpreter surfaces as an opaque node
+  // error with no position, while a thrown error is a debuggable host trap.
+    rule [extendContractTtl-err]:
+        <instrs> extendContractTtl(_CONTRACT) => #throw(ErrStorage, InvalidAction) ... </instrs>
+        <hostStack> U32(_THRESHOLD) : U32(_EXTEND_TO) : S => S </hostStack>
+      [owise]
+
     syntax Int ::= extendedLiveUntil(Int, Int, Int, Int)    [function, total]
  // -----------------------------------------------------------------------------------
     rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO)
@@ -332,6 +341,27 @@ module HOST-LEDGER
       requires THRESHOLD <=Int EXTEND_TO   // input is valid
        andBool SEQ <=Int LIVE_UNTIL        // entry is still alive
 
+    rule [extendCodeTtl-err]:
+        <instrs> extendCodeTtl(_HASH) => #throw(ErrStorage, InvalidAction) ... </instrs>
+        <hostStack> U32(_THRESHOLD) : U32(_EXTEND_TO) : S => S </hostStack>
+      [owise]
+
+```
+
+## get_max_live_until_ledger
+
+The last ledger an entry created now can live to, inclusive. This is a context
+host function (`x.8`), but it lives here with the other TTL rules because that
+is where `maxLiveUntil` and the max-entry-TTL constant are defined.
+
+```k
+    rule [hostfun-get-max-live-until-ledger]:
+        <instrs> hostCall ( "x" , "8" , [ .ValTypes ] -> [ i64  .ValTypes ] )
+              => toSmall(U32(maxLiveUntil(SEQ_NUM)))
+                 ...
+        </instrs>
+        <locals> .Map </locals>
+        <ledgerSequenceNumber> SEQ_NUM </ledgerSequenceNumber>
 ```
 
 ## Helpers

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

@@ -242,6 +242,43 @@ Returns a slice of the `Vec` object from the given start index (inclusive) to th
        andBool END   <=Int size(VEC)
 ```
 
+## vec_first_index_of
+
+Returns the `U32` index of the first element equal to `X`, or `Void` when there
+is none.
+
+The vector's items are `HostVal`s, so an element that holds an object and an
+equal needle allocated separately have different handles: the elements have to
+be resolved to `ScVal`s and compared by value, which is what `compare` does
+(the same ordering `obj_cmp` exposes to contracts). `X` is resolved too, since
+`loadArgs` only decodes the outermost level of a container.
+
+```k
+    rule [hostCallAux-vec-first-index-of]:
+        <instrs> hostCallAux ( "v" , "d" )
+              => toSmall(firstIndexOf(VEC, HostVal2ScValRec(X, OBJS, RELS), OBJS, RELS, 0))
+                 ...
+        </instrs>
+        <hostStack> ScVec(VEC) : X : S => S </hostStack>
+        <hostObjects>     OBJS </hostObjects>
+        <relativeObjects> RELS </relativeObjects>
+
+    syntax ScVal ::= firstIndexOf(List, ScVal, objs: List, rels: List, idx: Int)
+        [function, total, symbol(firstIndexOf)]
+ // -------------------------------------------------------------------------------
+    rule firstIndexOf(ListItem(V:HostVal) _REST, X, OBJS, RELS, IDX) => U32(IDX)
+      requires compare(HostVal2ScVal(V, OBJS, RELS), X) ==K Equal
+
+    rule firstIndexOf(ListItem(V:ScVal)  _REST, X, OBJS, RELS, IDX) => U32(IDX)
+      requires compare(HostVal2ScValRec(V, OBJS, RELS), X) ==K Equal
+
+    rule firstIndexOf(ListItem(_) REST, X, OBJS, RELS, IDX)
+      => firstIndexOf(REST, X, OBJS, RELS, IDX +Int 1)
+      [owise]
+
+    rule firstIndexOf(.List, _, _, _, _) => Void
+```
+
 ## vec_unpack_to_linear_memory
 
 ```k

src/komet/kdist/soroban-semantics/json-utils.md

@@ -323,6 +323,7 @@ Bytes are encoded with the builtin `Bytes2Hex` hook, which is the inverse of `He
     rule ScVal2JSON(U128(I))            => {"type" : "u128",    "value" : I}
     rule ScVal2JSON(I128(I))            => {"type" : "i128",    "value" : I}
     rule ScVal2JSON(U256(I))            => {"type" : "u256",    "value" : I}
+    rule ScVal2JSON(I256(I))            => {"type" : "i256",    "value" : I}
     rule ScVal2JSON(Symbol(S))          => {"type" : "symbol",  "value" : S}
     rule ScVal2JSON(ScString(S))        => {"type" : "string",  "value" : S}
     rule ScVal2JSON(ScBytes(B))         => {"type" : "bytes",   "value" : Bytes2Hex(B)}