From 80e07f1285e75fae5d1d09c4d89046f1462159ad Mon Sep 17 00:00:00 2001 From: Mihai Date: Tue, 15 Sep 2026 21:57:53 +0300 Subject: [PATCH] fix(semantics): correct i256 error type, rem_euclid domain and 256-bit object tags Three defects in the I256 support added by #127, each checked against the Soroban host rather than against the surrounding rules. - The i256 arithmetic host functions report `(Object, ArithDomain)`, not `(Value, ArithDomain)`. The 6-argument arm of `impl_bignum_host_fns!` builds its error with `ScErrorType::Object` (soroban-env-host/src/host/num.rs:39-45), and `i256_add`, `_sub`, `_mul`, `_div` and `_rem_euclid` all expand through that arm (soroban-env-host/src/host.rs:1568-1578). - `i256_rem_euclid` accepted `i256::MIN` by `-1` and returned `0`. `I256` is `ethnum::I256` (soroban-env-common/src/num.rs:10), whose `checked_rem_euclid` rejects `rhs == 0 || (self == MIN && rhs == -1)` (ethnum-1.5.2/src/int/api.rs:635-641) -- the same two pairs as `checked_div`, even though the mathematical remainder is representable. This was a silent wrong answer, not a stuck term. The comment above the rule was also wrong about `modInt`: K's `modInt` is e-division and always lands in `[0, absInt(B))` (domains.md:1262), so `absInt(B)` is redundant rather than load-bearing. Left the expression alone, corrected the claim. - `getTagWithFlag(true, _)` was missing both 256-bit types. Under `alwaysAllocate`, `addObject` tags the handle with `getTagWithFlag(AA, SCV)`; with no entry, a value that fits the small encoding fell through to `owise` and took `getTag`, so an object stored in `` was tagged `U256Small` (12) / `I256Small` (13). `isObject` is tag 64..77, so such a handle then failed `isObject` and `loadObject` took the `-small` branch, making `fromSmall` decode the object index as the value. U64, I64, U128, I128 and Symbol all carry this line for that reason; U256 and I256 were the only two small-capable types missing it. Tag numbers confirmed against `Tag` in soroban-env-common/src/val.rs (`U256Small = 12`, `U256Object = 70`, `I256Small = 13`, `I256Object = 71`). i256.wast pins the first two: the six existing error assertions move to `ErrObject`, and `i256::MIN rem_euclid -1` is added. The tag rules are only reachable with `alwaysAllocate` set, which the .wast harness does not do; they were checked by building with the cell forced to `true`, under which u256.wast, double_u256.wast and i256.wast all fail before the change and pass after. --- src/komet/kdist/soroban-semantics/data.md | 2 ++ .../kdist/soroban-semantics/host/integer.md | 24 ++++++++++--------- src/tests/integration/data/i256.wast | 22 ++++++++++++----- 3 files changed, 31 insertions(+), 17 deletions(-) diff --git a/src/komet/kdist/soroban-semantics/data.md b/src/komet/kdist/soroban-semantics/data.md index 842d0bf..0b830f6 100644 --- a/src/komet/kdist/soroban-semantics/data.md +++ b/src/komet/kdist/soroban-semantics/data.md @@ -179,6 +179,8 @@ module HOST-OBJECT rule getTagWithFlag(true, I64(_)) => 65 rule getTagWithFlag(true, U128(_)) => 68 rule getTagWithFlag(true, I128(_)) => 69 + rule getTagWithFlag(true, U256(_)) => 70 + rule getTagWithFlag(true, I256(_)) => 71 rule getTagWithFlag(true, Symbol(_)) => 74 rule getTagWithFlag(_, SCV) => getTag(SCV) [owise] diff --git a/src/komet/kdist/soroban-semantics/host/integer.md b/src/komet/kdist/soroban-semantics/host/integer.md index aca8f0e..d09397e 100644 --- a/src/komet/kdist/soroban-semantics/host/integer.md +++ b/src/komet/kdist/soroban-semantics/host/integer.md @@ -351,7 +351,7 @@ negative value is converted to its unsigned form before shifting. 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. +call with `(ErrObject, 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. @@ -367,7 +367,7 @@ arguments in reverse), so `A` is the left-hand side. requires inRangeInt(i256, Signed, A +Int B) rule [hostCallAux-i256-add-overflow]: - hostCallAux ( "i" , "v" ) => #throw(ErrValue, ArithDomain) ... + hostCallAux ( "i" , "v" ) => #throw(ErrObject, ArithDomain) ... I256(A) : I256(B) : S => S requires notBool inRangeInt(i256, Signed, A +Int B) ``` @@ -385,7 +385,7 @@ arguments in reverse), so `A` is the left-hand side. requires inRangeInt(i256, Signed, A -Int B) rule [hostCallAux-i256-sub-overflow]: - hostCallAux ( "i" , "w" ) => #throw(ErrValue, ArithDomain) ... + hostCallAux ( "i" , "w" ) => #throw(ErrObject, ArithDomain) ... I256(A) : I256(B) : S => S requires notBool inRangeInt(i256, Signed, A -Int B) ``` @@ -403,7 +403,7 @@ arguments in reverse), so `A` is the left-hand side. requires inRangeInt(i256, Signed, A *Int B) rule [hostCallAux-i256-mul-overflow]: - hostCallAux ( "i" , "x" ) => #throw(ErrValue, ArithDomain) ... + hostCallAux ( "i" , "x" ) => #throw(ErrObject, ArithDomain) ... I256(A) : I256(B) : S => S requires notBool inRangeInt(i256, Signed, A *Int B) ``` @@ -427,12 +427,12 @@ rather than range-checking `A /Int B`, so no side condition divides. [preserves-definedness] // 'A /Int B' is defined for non-zero B rule [hostCallAux-i256-div-by-zero]: - hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... + hostCallAux ( "i" , "y" ) => #throw(ErrObject, ArithDomain) ... I256(_A) : I256(B) : S => S requires B ==Int 0 rule [hostCallAux-i256-div-overflow]: - hostCallAux ( "i" , "y" ) => #throw(ErrValue, ArithDomain) ... + hostCallAux ( "i" , "y" ) => #throw(ErrObject, ArithDomain) ... I256(A) : I256(B) : S => S requires A ==Int minInt(i256, Signed) andBool B ==Int -1 ``` @@ -440,9 +440,9 @@ rather than range-checking `A /Int B`, so no side condition divides. ## 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. +operands. K's `modInt` is e-division, so it already lands in `[0, absInt(B))` +and agrees with Rust's `rem_euclid`. `checked_rem_euclid` rejects the same two +operand pairs as `checked_div`: a zero divisor, and `i256::MIN` by `-1`. ```k rule [hostCallAux-i256-rem-euclid]: @@ -453,12 +453,14 @@ zero divisor is the only failure. I256(A) : I256(B) : S => S requires B =/=Int 0 + andBool notBool (A ==Int minInt(i256, Signed) andBool B ==Int -1) [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 + hostCallAux ( "i" , "z" ) => #throw(ErrObject, ArithDomain) ... + I256(A) : I256(B) : S => S requires B ==Int 0 + orBool (A ==Int minInt(i256, Signed) andBool B ==Int -1) ``` ```k diff --git a/src/tests/integration/data/i256.wast b/src/tests/integration/data/i256.wast index c51108d..10806a5 100644 --- a/src/tests/integration/data/i256.wast +++ b/src/tests/integration/data/i256.wast @@ -268,7 +268,7 @@ callTx( Contract(b"test-sc"), "add", ListItem(I256(2 ^Int 255 -Int 1)) ListItem(I256(1)), - Error(ErrValue, ArithDomain) + Error(ErrObject, ArithDomain) ) callTx( @@ -292,7 +292,7 @@ callTx( Contract(b"test-sc"), "sub", ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(1)), - Error(ErrValue, ArithDomain) + Error(ErrObject, ArithDomain) ) callTx( @@ -317,7 +317,7 @@ callTx( Contract(b"test-sc"), "mul", ListItem(I256(2 ^Int 200)) ListItem(I256(2 ^Int 200)), - Error(ErrValue, ArithDomain) + Error(ErrObject, ArithDomain) ) ;; Division truncates toward zero. @@ -358,7 +358,7 @@ callTx( Contract(b"test-sc"), "div", ListItem(I256(1)) ListItem(I256(0)), - Error(ErrValue, ArithDomain) + Error(ErrObject, ArithDomain) ) ;; i256::MIN / -1 is the one division that overflows. @@ -367,7 +367,7 @@ callTx( Contract(b"test-sc"), "div", ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(0 -Int 1)), - Error(ErrValue, ArithDomain) + Error(ErrObject, ArithDomain) ) ;; Euclidean modulo is never negative, whatever the signs of the operands. @@ -408,7 +408,17 @@ callTx( Contract(b"test-sc"), "rem", ListItem(I256(1)) ListItem(I256(0)), - Error(ErrValue, ArithDomain) + Error(ErrObject, ArithDomain) +) + +;; `checked_rem_euclid` rejects i256::MIN % -1 as well, even though the +;; mathematical remainder (0) is representable. +callTx( + Account(b"test-caller"), + Contract(b"test-sc"), + "rem", + ListItem(I256(0 -Int 2 ^Int 255)) ListItem(I256(0 -Int 1)), + Error(ErrObject, ArithDomain) ) setExitCode(0)