From 254d854ad571e16aca5d3617796039d30e76c6e0 Mon Sep 17 00:00:00 2001 From: Raoul Date: Tue, 18 Aug 2026 08:21:33 +0000 Subject: [PATCH 1/3] Implement missing host calls --- src/komet/kdist/soroban-semantics/data.md | 12 + .../kdist/soroban-semantics/host/integer.md | 219 +++++++++ .../kdist/soroban-semantics/host/ledger.md | 16 + .../kdist/soroban-semantics/host/vector.md | 37 ++ .../kdist/soroban-semantics/json-utils.md | 1 + src/tests/integration/data/i256.wast | 414 ++++++++++++++++++ .../data/max_live_until_ledger.wast | 55 +++ .../integration/data/vec_first_index_of.wast | 131 ++++++ 8 files changed, 885 insertions(+) create mode 100644 src/tests/integration/data/i256.wast create mode 100644 src/tests/integration/data/max_live_until_ledger.wast create mode 100644 src/tests/integration/data/vec_first_index_of.wast diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index 7bde93e5..842d0bfc 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/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 or List | ScMap(Map) [symbol(SCVal:Map)] // Map or Map | 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 diff --git a/src/komet/kdist/soroban-semantics/host/integer.md b/src/komet/kdist/soroban-semantics/host/integer.md index e0d8bc76..aca8f0e6 100644 --- a/src/komet/kdist/soroban-semantics/host/integer.md +++ b/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]: + hostCall ( "i" , "g" , [ i64 i64 i64 i64 .ValTypes ] -> [ i64 .ValTypes ] ) + => allocObject( I256( #signed(i256, + (HI_HI < returnHostVal + ... + + + 0 |-> < i64 > HI_HI + 1 |-> < i64 > HI_LO + 2 |-> < i64 > LO_HI + 3 |-> < i64 > LO_LO + + requires definedSigned(i256, + (HI_HI < hostCallAux ( "i" , "h" ) + => allocObject( I256( Bytes2Int(BS, BE, Signed) ) ) + ~> returnHostVal + ... + + ScBytes(BS) : S => S + requires lengthBytes(BS) ==Int 32 +``` + +## i256_val_to_be_bytes + +```k + rule [hostCallAux-i256-val-to-be-bytes]: + hostCallAux ( "i" , "i" ) + => allocObject( ScBytes( Int2Bytes(32, #unsigned(i256, I), BE) ) ) + ~> returnHostVal + ... + + I256(I) : S => S + 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]: + hostCallAux ( "i" , "j" ) => i64.const (#unsigned(i256, I) >>Int 192) ... + I256(I) : S => S + requires definedUnsigned(i256, I) + [preserves-definedness] +``` + +## obj_to_i256_hi_lo + +```k + rule [hostCallAux-obj-to-i256-hi-lo]: + hostCallAux ( "i" , "k" ) => i64.const (#unsigned(i256, I) >>Int 128) ... + I256(I) : S => S + requires definedUnsigned(i256, I) + [preserves-definedness] +``` + +## obj_to_i256_lo_hi + +```k + rule [hostCallAux-obj-to-i256-lo-hi]: + hostCallAux ( "i" , "l" ) => i64.const (#unsigned(i256, I) >>Int 64) ... + I256(I) : S => S + requires definedUnsigned(i256, I) + [preserves-definedness] +``` + +## obj_to_i256_lo_lo + +```k + rule [hostCallAux-obj-to-i256-lo-lo]: + hostCallAux ( "i" , "m" ) => i64.const (#unsigned(i256, I)) ... + I256(I) : S => S + 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]: + hostCallAux ( "i" , "v" ) + => allocObject( I256( A +Int B ) ) + ~> returnHostVal + ... + + I256(A) : I256(B) : S => S + requires inRangeInt(i256, Signed, A +Int B) + + rule [hostCallAux-i256-add-overflow]: + hostCallAux ( "i" , "v" ) => #throw(ErrValue, ArithDomain) ... + I256(A) : I256(B) : S => S + requires notBool inRangeInt(i256, Signed, A +Int B) +``` + +## i256_sub + +```k + rule [hostCallAux-i256-sub]: + hostCallAux ( "i" , "w" ) + => allocObject( I256( A -Int B ) ) + ~> returnHostVal + ... + + I256(A) : I256(B) : S => S + requires inRangeInt(i256, Signed, A -Int B) + + rule [hostCallAux-i256-sub-overflow]: + hostCallAux ( "i" , "w" ) => #throw(ErrValue, ArithDomain) ... + I256(A) : I256(B) : S => S + requires notBool inRangeInt(i256, Signed, A -Int B) +``` + +## i256_mul + +```k + rule [hostCallAux-i256-mul]: + hostCallAux ( "i" , "x" ) + => allocObject( I256( A *Int B ) ) + ~> returnHostVal + ... + + I256(A) : I256(B) : S => S + requires inRangeInt(i256, Signed, A *Int B) + + rule [hostCallAux-i256-mul-overflow]: + hostCallAux ( "i" , "x" ) => #throw(ErrValue, ArithDomain) ... + I256(A) : I256(B) : S => S + 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]: + hostCallAux ( "i" , "y" ) + => allocObject( I256( A /Int B ) ) + ~> returnHostVal + ... + + I256(A) : I256(B) : S => S + 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]: + hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... + I256(_A) : I256(B) : S => S + requires B ==Int 0 + + rule [hostCallAux-i256-div-overflow]: + hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... + I256(A) : I256(B) : S => S + 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]: + hostCallAux ( "i" , "z" ) + => allocObject( I256( A modInt absInt(B) ) ) + ~> returnHostVal + ... + + I256(A) : I256(B) : S => S + requires B =/=Int 0 + [preserves-definedness] // 'A modInt absInt(B)' is defined for non-zero B + + rule [hostCallAux-i256-rem-euclid-error]: + hostCallAux ( "i" , "z" ) => #throw(ErrValue, ArithDomain) ... + I256(_A) : I256(B) : S => S + requires B ==Int 0 +``` + ```k endmodule ``` \ No newline at end of file diff --git a/src/komet/kdist/soroban-semantics/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md index 1e635dd0..6defbfa9 100644 --- a/src/komet/kdist/soroban-semantics/host/ledger.md +++ b/src/komet/kdist/soroban-semantics/host/ledger.md @@ -334,6 +334,22 @@ module HOST-LEDGER ``` +## 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]: + hostCall ( "x" , "8" , [ .ValTypes ] -> [ i64 .ValTypes ] ) + => toSmall(U32(maxLiveUntil(SEQ_NUM))) + ... + + .Map + SEQ_NUM +``` + ## Helpers ```k diff --git a/src/komet/kdist/soroban-semantics/host/vector.md b/src/komet/kdist/soroban-semantics/host/vector.md index c8a7b27f..b65f0852 100644 --- a/src/komet/kdist/soroban-semantics/host/vector.md +++ b/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]: + hostCallAux ( "v" , "d" ) + => toSmall(firstIndexOf(VEC, HostVal2ScValRec(X, OBJS, RELS), OBJS, RELS, 0)) + ... + + ScVec(VEC) : X : S => S + OBJS + RELS + + 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 diff --git a/src/komet/kdist/soroban-semantics/json-utils.md b/src/komet/kdist/soroban-semantics/json-utils.md index 2997301c..810c6deb 100644 --- a/src/komet/kdist/soroban-semantics/json-utils.md +++ b/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)} diff --git a/src/tests/integration/data/i256.wast b/src/tests/integration/data/i256.wast new file mode 100644 index 00000000..c51108d7 --- /dev/null +++ b/src/tests/integration/data/i256.wast @@ -0,0 +1,414 @@ +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $test_wasm + (import "i" "g" (func $obj_from_i256_pieces (param i64 i64 i64 i64) (result i64))) + (import "i" "h" (func $i256_val_from_be_bytes (param i64) (result i64))) + (import "i" "i" (func $i256_val_to_be_bytes (param i64) (result i64))) + (import "i" "j" (func $obj_to_i256_hi_hi (param i64) (result i64))) + (import "i" "k" (func $obj_to_i256_hi_lo (param i64) (result i64))) + (import "i" "l" (func $obj_to_i256_lo_hi (param i64) (result i64))) + (import "i" "m" (func $obj_to_i256_lo_lo (param i64) (result i64))) + (import "i" "v" (func $i256_add (param i64 i64) (result i64))) + (import "i" "w" (func $i256_sub (param i64 i64) (result i64))) + (import "i" "x" (func $i256_mul (param i64 i64) (result i64))) + (import "i" "y" (func $i256_div (param i64 i64) (result i64))) + (import "i" "z" (func $i256_rem_euclid (param i64 i64) (result i64))) + + ;; Split a value into its four 64-bit words and reassemble it. + (func $roundtrip (param i64) (result i64) + (call $obj_from_i256_pieces + (call $obj_to_i256_hi_hi (local.get 0)) + (call $obj_to_i256_hi_lo (local.get 0)) + (call $obj_to_i256_lo_hi (local.get 0)) + (call $obj_to_i256_lo_lo (local.get 0)) + ) + ) + (func $roundtripBytes (param i64) (result i64) + (call $i256_val_from_be_bytes + (call $i256_val_to_be_bytes (local.get 0)) + ) + ) + (func $roundtripBytesInv (param i64) (result i64) + (call $i256_val_to_be_bytes + (call $i256_val_from_be_bytes (local.get 0)) + ) + ) + ;; The four extractors on their own, widened to i256 so the result is checkable. + (func $hiHi (param i64) (result i64) + (call $obj_from_i256_pieces + (i64.const 0) (i64.const 0) (i64.const 0) + (call $obj_to_i256_hi_hi (local.get 0)) + ) + ) + (func $loLo (param i64) (result i64) + (call $obj_from_i256_pieces + (i64.const 0) (i64.const 0) (i64.const 0) + (call $obj_to_i256_lo_lo (local.get 0)) + ) + ) + (func $add (param i64 i64) (result i64) (call $i256_add (local.get 0) (local.get 1))) + (func $sub (param i64 i64) (result i64) (call $i256_sub (local.get 0) (local.get 1))) + (func $mul (param i64 i64) (result i64) (call $i256_mul (local.get 0) (local.get 1))) + (func $div (param i64 i64) (result i64) (call $i256_div (local.get 0) (local.get 1))) + (func $rem (param i64 i64) (result i64) (call $i256_rem_euclid (local.get 0) (local.get 1))) + + (export "roundtrip" (func $roundtrip)) + (export "roundtripBytes" (func $roundtripBytes)) + (export "roundtripBytesInv" (func $roundtripBytesInv)) + (export "hiHi" (func $hiHi)) + (export "loLo" (func $loLo)) + (export "add" (func $add)) + (export "sub" (func $sub)) + (export "mul" (func $mul)) + (export "div" (func $div)) + (export "rem" (func $rem)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +;; --------------------------------------------------------------------------- +;; obj_from_i256_pieces / obj_to_i256_* (i.g, i.j, i.k, i.l, i.m) +;; +;; 0, 1 and -1 are small values (|x| < 2^55, tag 13); the rest are I256 objects +;; (tag 71), so both HostVal representations are covered. +;; --------------------------------------------------------------------------- + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I256(0)), + I256(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I256(1)), + I256(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I256(0 -Int 1)), + I256(0 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I256(1000000000000000000)), ;; 1e18: a Wad price, as the oracle path uses + I256(1000000000000000000) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I256(0 -Int 12345678901234567890123456789)), + I256(0 -Int 12345678901234567890123456789) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I256(2 ^Int 255 -Int 1)), ;; i256::MAX + I256(2 ^Int 255 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtrip", + ListItem(I256(0 -Int 2 ^Int 255)), ;; i256::MIN + I256(0 -Int 2 ^Int 255) +) + +;; The words are the two's-complement representation: -1 is all ones. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hiHi", + ListItem(I256(0 -Int 1)), + I256(2 ^Int 64 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "loLo", + ListItem(I256(0 -Int 1)), + I256(2 ^Int 64 -Int 1) +) + +;; i256::MIN is 1 followed by 255 zeros. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "hiHi", + ListItem(I256(0 -Int 2 ^Int 255)), + I256(2 ^Int 63) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "loLo", + ListItem(I256(0 -Int 2 ^Int 255)), + I256(0) +) + +;; --------------------------------------------------------------------------- +;; i256_val_from_be_bytes / i256_val_to_be_bytes (i.h, i.i) +;; --------------------------------------------------------------------------- + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtripBytes", + ListItem(I256(0)), + I256(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtripBytes", + ListItem(I256(0 -Int 1)), + I256(0 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtripBytes", + ListItem(I256(100000000)), + I256(100000000) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtripBytes", + ListItem(I256(2 ^Int 255 -Int 1)), ;; i256::MAX + I256(2 ^Int 255 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtripBytes", + ListItem(I256(0 -Int 2 ^Int 255)), ;; i256::MIN + I256(0 -Int 2 ^Int 255) +) + +;; A negative value's big-endian bytes are its two's complement: -1 is 32 0xff. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtripBytesInv", + ListItem(ScBytes(b"\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff")), + ScBytes(b"\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff") +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "roundtripBytesInv", + ListItem(ScBytes(b"abcdefghabcdefghabcdefghabcdefgh")), ;; 32 bytes + ScBytes(b"abcdefghabcdefghabcdefghabcdefgh") +) + +;; --------------------------------------------------------------------------- +;; Arithmetic (i.v, i.w, i.x, i.y, i.z) +;; +;; The argument order matters for the non-commutative ops: the first Wasm +;; argument is the left-hand side. +;; --------------------------------------------------------------------------- + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "add", + ListItem(I256(1)) ListItem(I256(2)), + I256(3) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "add", + ListItem(I256(0 -Int 5)) ListItem(I256(3)), + I256(0 -Int 2) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "add", + ListItem(I256(2 ^Int 255 -Int 2)) ListItem(I256(1)), + I256(2 ^Int 255 -Int 1) +) + +;; Overflow past i256::MAX is a checked failure, not a wrap. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "add", + ListItem(I256(2 ^Int 255 -Int 1)) ListItem(I256(1)), + Error(ErrValue, ArithDomain) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "sub", + ListItem(I256(1)) ListItem(I256(2)), + I256(0 -Int 1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "sub", + ListItem(I256(0 -Int 2 ^Int 255 +Int 1)) ListItem(I256(1)), + I256(0 -Int 2 ^Int 255) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "sub", + ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(1)), + Error(ErrValue, ArithDomain) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "mul", + ListItem(I256(0 -Int 3)) ListItem(I256(4)), + I256(0 -Int 12) +) + +;; 1e18 * 1e27: the product `mul_div` forms before dividing. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "mul", + ListItem(I256(1000000000000000000)) ListItem(I256(1000000000000000000000000000)), + I256(1000000000000000000000000000000000000000000000) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "mul", + ListItem(I256(2 ^Int 200)) ListItem(I256(2 ^Int 200)), + Error(ErrValue, ArithDomain) +) + +;; Division truncates toward zero. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "div", + ListItem(I256(7)) ListItem(I256(2)), + I256(3) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "div", + ListItem(I256(0 -Int 7)) ListItem(I256(2)), + I256(0 -Int 3) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "div", + ListItem(I256(7)) ListItem(I256(0 -Int 2)), + I256(0 -Int 3) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "div", + ListItem(I256(0 -Int 7)) ListItem(I256(0 -Int 2)), + I256(3) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "div", + ListItem(I256(1)) ListItem(I256(0)), + Error(ErrValue, ArithDomain) +) + +;; i256::MIN / -1 is the one division that overflows. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "div", + ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(0 -Int 1)), + Error(ErrValue, ArithDomain) +) + +;; Euclidean modulo is never negative, whatever the signs of the operands. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "rem", + ListItem(I256(7)) ListItem(I256(3)), + I256(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "rem", + ListItem(I256(0 -Int 7)) ListItem(I256(3)), + I256(2) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "rem", + ListItem(I256(7)) ListItem(I256(0 -Int 3)), + I256(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "rem", + ListItem(I256(0 -Int 7)) ListItem(I256(0 -Int 3)), + I256(2) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "rem", + ListItem(I256(1)) ListItem(I256(0)), + Error(ErrValue, ArithDomain) +) + +setExitCode(0) diff --git a/src/tests/integration/data/max_live_until_ledger.wast b/src/tests/integration/data/max_live_until_ledger.wast new file mode 100644 index 00000000..7743236c --- /dev/null +++ b/src/tests/integration/data/max_live_until_ledger.wast @@ -0,0 +1,55 @@ +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $test_wasm + ;; The cheatcode takes a U32 HostVal payload and returns nothing; see + ;; ledger_sequence_get_set.wast for the Rust side of this declaration. + (import "env" "kasmer_set_ledger_sequence" (func $kasmer_set_ledger_sequence (param i64))) + (import "x" "8" (func $get_max_live_until_ledger (result i64))) + (func $max_live (result i64) + (call $get_max_live_until_ledger) + ) + (func $max_live_at (param i64) (result i64) + (call $kasmer_set_ledger_sequence (local.get 0)) + (call $get_max_live_until_ledger) + ) + (export "max_live" (func $max_live)) + (export "max_live_at" (func $max_live_at)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +;; The max entry TTL is 6312000 ledgers and the bound is inclusive, so at +;; ledger 0 an entry can live until ledger 6311999. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "max_live", + .List, + U32(6311999) +) + +;; It tracks the current ledger, rather than being a constant. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "max_live_at", + ListItem(U32(100)), + U32(6312099) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "max_live_at", + ListItem(U32(987654321)), + U32(993966320) +) + +setExitCode(0) diff --git a/src/tests/integration/data/vec_first_index_of.wast b/src/tests/integration/data/vec_first_index_of.wast new file mode 100644 index 00000000..222ed9ef --- /dev/null +++ b/src/tests/integration/data/vec_first_index_of.wast @@ -0,0 +1,131 @@ +setExitCode(1) + +uploadWasm( b"test-wasm", +(module $test_wasm + (import "v" "d" (func $vec_first_index_of (param i64 i64) (result i64))) + (func $first_index_of (param i64 i64) (result i64) + (call $vec_first_index_of (local.get 0) (local.get 1)) + ) + (export "first_index_of" (func $first_index_of)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +;; Present: the index of the match. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(U32(10)) ListItem(U32(20)) ListItem(U32(30)))) + ListItem(U32(20)), + U32(1) +) + +;; The first element and the last element. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(U32(10)) ListItem(U32(20)) ListItem(U32(30)))) + ListItem(U32(10)), + U32(0) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(U32(10)) ListItem(U32(20)) ListItem(U32(30)))) + ListItem(U32(30)), + U32(2) +) + +;; Duplicates: the FIRST occurrence. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(U32(7)) ListItem(U32(7)) ListItem(U32(7)))) + ListItem(U32(7)), + U32(0) +) + +;; Absent, and absent from an empty vector: Void. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(U32(10)) ListItem(U32(20)))) + ListItem(U32(99)), + Void +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(.List)) + ListItem(U32(1)), + Void +) + +;; Equality is typed: U64(1) is not U32(1). +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(U64(1)))) + ListItem(U32(1)), + Void +) + +;; Object-valued elements: each I128 is a separately allocated host object, so +;; a match can only be found by comparing values, not object handles. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(I128(2 ^Int 100)) ListItem(I128(0 -Int 2 ^Int 100)))) + ListItem(I128(0 -Int 2 ^Int 100)), + U32(1) +) + +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(I128(2 ^Int 100)))) + ListItem(I128(2 ^Int 100 +Int 1)), + Void +) + +;; Nested containers are compared element by element. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec( + ListItem(ScVec(ListItem(U32(1)))) + ListItem(ScVec(ListItem(U32(1)) ListItem(U32(2)))) + )) + ListItem(ScVec(ListItem(U32(1)) ListItem(U32(2)))), + U32(1) +) + +;; Symbols long enough to become host objects rather than small values. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "first_index_of", + ListItem(ScVec(ListItem(Symbol(str("short"))) ListItem(Symbol(str("a_long_symbol_name"))))) + ListItem(Symbol(str("a_long_symbol_name"))), + U32(1) +) + +setExitCode(0) From 0ae23812e66e02c8b864db9a86e5380c3e9444ed Mon Sep 17 00:00:00 2001 From: Raoul Date: Tue, 18 Aug 2026 13:47:43 +0000 Subject: [PATCH 2/3] Fix TTL for contract code and deployments --- .../kdist/soroban-semantics/host/ledger.md | 14 +++++ src/komet/kdist/soroban-semantics/kasmer.md | 11 ++++ .../data/extend_ttl_past_ledger_zero.wast | 62 +++++++++++++++++++ .../soroban/contracts/test_ttl/src/lib.rs | 30 +++++---- 4 files changed, 106 insertions(+), 11 deletions(-) create mode 100644 src/tests/integration/data/extend_ttl_past_ledger_zero.wast diff --git a/src/komet/kdist/soroban-semantics/host/ledger.md b/src/komet/kdist/soroban-semantics/host/ledger.md index 6defbfa9..fefcb510 100644 --- a/src/komet/kdist/soroban-semantics/host/ledger.md +++ b/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]: + extendContractTtl(_CONTRACT) => #throw(ErrStorage, InvalidAction) ... + U32(_THRESHOLD) : U32(_EXTEND_TO) : S => S + [owise] + syntax Int ::= extendedLiveUntil(Int, Int, Int, Int) [function, total] // ----------------------------------------------------------------------------------- rule extendedLiveUntil(SEQ, LIVE_UNTIL, THRESHOLD, EXTEND_TO) @@ -332,6 +341,11 @@ module HOST-LEDGER requires THRESHOLD <=Int EXTEND_TO // input is valid andBool SEQ <=Int LIVE_UNTIL // entry is still alive + rule [extendCodeTtl-err]: + extendCodeTtl(_HASH) => #throw(ErrStorage, InvalidAction) ... + U32(_THRESHOLD) : U32(_EXTEND_TO) : S => S + [owise] + ``` ## get_max_live_until_ledger diff --git a/src/komet/kdist/soroban-semantics/kasmer.md b/src/komet/kdist/soroban-semantics/kasmer.md index 876b185a..f2b0a451 100644 --- a/src/komet/kdist/soroban-semantics/kasmer.md +++ b/src/komet/kdist/soroban-semantics/kasmer.md @@ -106,13 +106,20 @@ module KASMER uploadWasm(HASH, _MOD) => .K ... HASH + // Contract code is a persistent ledger entry, so an upload starts it with the + // minimum persistent TTL, exactly as `putContractData` does for a new + // persistent entry. Leaving `codeLiveUntil` at its 0 default would mark the + // entry expired at every ledger past 0, and + // `extend_current_contract_instance_and_code_ttl` only extends a live entry. rule [uploadWasm]: uploadWasm(HASH, MOD) => .K ... (.Bag => HASH + minLiveUntil(#persistent, SEQ) MOD ... ) + SEQ [priority(51)] // ----------------------------------------------------------------------------------------------------------------------- @@ -126,15 +133,19 @@ module KASMER syntax HostCell + // The contract instance is a persistent entry too (and `` + // shares its TTL), so it starts at the minimum persistent TTL as well. rule [deployContract]: deployContract(_OWNER, ADDR, WASM_HASH) => .K ... ( .Bag => ADDR WASM_HASH + minLiveUntil(#persistent, SEQ) ... ) + SEQ [priority(55)] syntax InternalCmd ::= callContractFromStack(Address, ContractId, WasmString) [symbol(callContractFromStack)] diff --git a/src/tests/integration/data/extend_ttl_past_ledger_zero.wast b/src/tests/integration/data/extend_ttl_past_ledger_zero.wast new file mode 100644 index 00000000..96269424 --- /dev/null +++ b/src/tests/integration/data/extend_ttl_past_ledger_zero.wast @@ -0,0 +1,62 @@ +setExitCode(1) + +;; `extend_ttl.wast` covers the host call at ledger 0, where a contract deployed +;; with `contractLiveUntil = 0` still counts as alive. This file covers the same +;; host call at a LATER ledger: an upload/deploy must start the code and instance +;; entries at the minimum persistent TTL, otherwise every extension past ledger 0 +;; sees an expired entry. +uploadWasm( b"test-wasm", +(module $test_wasm + ;; The cheatcode takes a U32 HostVal payload and returns nothing; see + ;; ledger_sequence_get_set.wast for the Rust side of this declaration. + (import "env" "kasmer_set_ledger_sequence" (func $kasmer_set_ledger_sequence (param i64))) + (import "l" "8" (func $extend_current_contract_instance_and_code_ttl (param i64 i64) (result i64))) + ;; extend_at(seq, threshold, extend_to): move the ledger to `seq`, then extend + ;; this contract's instance and code TTL. Returns the host call's Void. + (func $extend_at (param i64 i64 i64) (result i64) + (call $kasmer_set_ledger_sequence (local.get 0)) + (call $extend_current_contract_instance_and_code_ttl (local.get 1) (local.get 2)) + ) + (export "extend_at" (func $extend_at)) +)) + +setAccount(Account(b"test-account"), 9876543210) + +deployContract( + Account(b"test-account"), + Contract(b"test-sc"), + b"test-wasm" +) + +;; Deployed at ledger 0, so both entries live until 4095 (minimum persistent TTL +;; of 4096, inclusive bound). At ledger 100 they are alive, and the current TTL +;; (3995) already exceeds the threshold, so this is a successful no-op. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "extend_at", + ListItem(U32(100)) ListItem(U32(50)) ListItem(U32(200)), + Void +) + +;; At ledger 4090 the remaining TTL (5) is below the threshold, so the entries +;; are extended to ledger 4290. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "extend_at", + ListItem(U32(4090)) ListItem(U32(50)) ListItem(U32(200)), + Void +) + +;; Past that, the entries have expired: there is nothing to extend, and the host +;; call fails rather than leaving the interpreter stuck. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "extend_at", + ListItem(U32(5000)) ListItem(U32(50)) ListItem(U32(200)), + Error(ErrStorage, InvalidAction) +) + +setExitCode(0) diff --git a/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs b/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs index 27c3c5a3..89f80c2c 100644 --- a/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs +++ b/src/tests/integration/data/soroban/contracts/test_ttl/src/lib.rs @@ -26,6 +26,9 @@ fn set_ledger_timestamp(env: &Env, x: u64) { } const MAX_ENTRY_TTL: u32 = 6312000; +// A freshly deployed contract instance (and its code) is a persistent entry, so +// it already carries the minimum persistent TTL before anything extends it. +const MIN_PERSISTENT_ENTRY_TTL: u32 = 4096; #[contractimpl] impl TtlContract { @@ -43,19 +46,24 @@ impl TtlContract { return true; } - // Set the initial TTL and ledger sequence number - env.storage().instance().extend_ttl(threshold, ttl); - let init_ttl = u32::min(ttl, MAX_ENTRY_TTL); + // Track where the entry's live-until bound stands, mirroring the host: + // it starts at the minimum persistent TTL, and an extension applies only + // while the remaining TTL is at or below the threshold, never reaching + // past the maximum entry TTL. let init_seq = env.ledger().sequence(); - let init_live_until = init_seq.checked_add(init_ttl - 1); // the sequence number at the beginning is 0 - + let mut live_until = init_seq.saturating_add(MIN_PERSISTENT_ENTRY_TTL - 1); + let requested = init_seq.saturating_add(ttl); + if live_until - init_seq <= threshold && live_until < requested { + live_until = u32::min(requested, init_seq.saturating_add(MAX_ENTRY_TTL - 1)); + } + env.storage().instance().extend_ttl(threshold, ttl); + set_ledger_sequence(seq); - - if let Some(live_until) = init_live_until { - // If the contract is still alive extend the instance ttl - if seq <= live_until { - env.storage().instance().extend_ttl(threshold, extend_to); - } + + // Extending an entry that has already expired is an error, so only + // extend while the contract is still alive. + if seq <= live_until { + env.storage().instance().extend_ttl(threshold, extend_to); } // Since there is no getter function for the TTL value, we cannot verify From 6abf9640de8bde65dd55fbbbabddf4cead38f3b9 Mon Sep 17 00:00:00 2001 From: Raoul Date: Wed, 19 Aug 2026 17:05:47 +0000 Subject: [PATCH 3/3] Set Version: 0.1.89 --- package/version | 2 +- pyproject.toml | 2 +- uv.lock | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 93c6c476..5096aa31 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.86 +0.1.89 diff --git a/pyproject.toml b/pyproject.toml index 747cf870..49d16251 100644 --- a/pyproject.toml +++ b/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 = [ diff --git a/uv.lock b/uv.lock index d9596b5f..f1462614 100644 --- a/uv.lock +++ b/uv.lock @@ -679,7 +679,7 @@ wheels = [ [[package]] name = "komet" -version = "0.1.88" +version = "0.1.89" source = { editable = "." } dependencies = [ { name = "pykwasm" },