fix(semantics): correct i256 error type, rem_euclid domain and 256-bit object tags

[mihaieremia]

Follow up fix to #127, not a feature.

This branch was opened as "add I256 support" against 089b3aa. #127 landed that support first, so the original diff is obsolete, and merging it would have regressed master: it had no i256_sub, its smaller i256.wast would have replaced yours, and it carried a stale json-utils.md reverting the ValMap2JSON rename from #126. Rebased onto a078e29 and reduced to the three defects the comparison exposed in #127's rules.

Fixes

Citations are rs-soroban-env at a7e15b43, which is the current tip of main. Re-checked against the v28.0.2 tag as well; every cited line is identical there.

1. Wrong error type, 7 sites. i256_add, i256_sub, i256_mul, i256_div and i256_rem_euclid all expand through the 6 argument arm of impl_bignum_host_fns! (host.rs:1568-1579), which raises ScErrorType::Object (host/num.rs:39-45). The rules threw ErrValue. Now ErrObject.

2. i256_rem_euclid accepted i256::MIN by -1. I256 is ethnum::I256, whose checked_rem_euclid rejects a zero divisor and MIN / -1 alike (ethnum 1.5.3, src/int/api.rs:635-641). The rule guarded only B =/=Int 0. Run against the unfixed build it returned I256(0) with exitCode 0, so this was a silent wrong answer rather than a stuck term.

The comment above the rule was also wrong: K's modInt is e-division (domains.md:1262), so absInt(B) is redundant rather than load bearing. Expression left alone, claim corrected.

3. getTagWithFlag(true, _) missing for both 256 bit types. Under alwaysAllocate, addObject tags a handle with getTagWithFlag(AA, SCV) (configuration.md:324). With no entry for the type, a small range value falls through to owise and takes getTag, so an object in <hostObjects> gets tag 12 or 13. isObject is 64..77 (data.md:123), so the handle fails it, loadObject takes its -small branch, and fromSmall decodes the object index as the value.

U64, I64, U128, I128 and Symbol already carry this line. U256 and I256 were the only remaining small capable types missing it, so both are added. Timepoint and Duration have no ScVal constructor in komet (data.md:53-70) and cannot reach the rule.

Verification

K v7.1.313 on macOS/arm64.

kdist build 'soroban-semantics.*'	exit 0, four backends, --warnings-to-errors
pytest -k "test_run or tracing_smoke"	72 passed, 32 deselected
make check, make test-unit	exit 0, 15 passed
krun over all 36 .wast	PASS=36 FAIL=0

Arithmetic, both directions executed: master semantics with this branch's i256.wast gives krun exit 1, stuck at the first expectResult(Error(ErrObject, 0)). This branch gives exit 0.

Tags: no committed test reaches these rules, because the .wast harness runs with alwaysAllocate = false. Forcing the cell true in a local build, which is not part of this PR, u256.wast, double_u256.wast and i256.wast all fail on master's data.md and all pass with both rules. Reading the U256(123) handle out of <locals> at the same step in each build:

data.md	HostVal	body	tag
master	12884901900	50331648	12, U256Small
this branch	12884901958	50331648	70, U256Object

Same handle, tag differing by 58. Unfixed, the run ends with U256(50331648) on the host stack where U256(246) is expected. Both runs print <alwaysAllocate> in their own output configuration, so the mode is self attested rather than asserted.

Constants were re-read from source rather than recall: the four tags (val.rs), every host function letter for module "i" (env.json, all already correct), ScValTypeOrd(I256) = 12, and the /Int and modInt division semantics (domains.md:1255,1262).

Not included

The soroban-sdk 22 to 27 bump from the original diff is dropped. 22.0.11 already has every I256 method the tests use, and dropping it removes a 419 line Cargo.lock diff.

The comparison also surfaced five pre-existing gaps unrelated to I256, mostly missing error rules that leave a term stuck where the host errors. Out of scope here, happy to file them separately.

Limits

CI has not run. gh pr checks 128 reports no checks, since the integration jobs need a maintainer to approve the workflow for a fork PR. Everything above is local.

No symbolic proof was run. The Haskell backend compiles, but only the concrete and tracing definitions were executed, and fix 3 was reached by forcing the configuration cell rather than through komet prove --always-allocate. make test-integration was not run in full, because test_komet needs the CI Docker image.