diff --git a/.trinity/seals/policy_PolicyJsonInt53.json b/.trinity/seals/policy_PolicyJsonInt53.json new file mode 100644 index 0000000000..6746c52f6d --- /dev/null +++ b/.trinity/seals/policy_PolicyJsonInt53.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+2406a4804", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:fd7989ee2740337b1ae11b782e5fa7f1797bc995681b2a5a897c30a481838a6e", + "gen_hash_rust": "sha256:537c2c990992621f30fe6d148bc83f9bf4594519580f86d38e700ace9abab8d7", + "gen_hash_verilog": "sha256:bd97f8d585b699cf216b9a5074bc6d3e9b08135fa5ffa9363f80ac0e6cff1c26", + "gen_hash_zig": "sha256:2eeb961d994fda212a0112f22ea761a07e552d6a60d0c2cbe4ef06759f8ab3b4", + "module": "PolicyJsonInt53", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T11:34:52Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:e775f005632a89e57ceddb891bff47e33d377d957d007ee9c9cc1785629ea7ed", + "spec_path": "specs/policy/json_int53.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 16, + "total": 16, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "missing", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/docs/reports/2026-10-18-json-int53-measured.md b/docs/reports/2026-10-18-json-int53-measured.md new file mode 100644 index 0000000000..b445a1bf37 --- /dev/null +++ b/docs/reports/2026-10-18-json-int53-measured.md @@ -0,0 +1,190 @@ +# JSON integers above 2^53 - 1: measured 2026-10-18 + +Rule and scanner: [`specs/policy/json_int53.t27`](../../specs/policy/json_int53.t27) +(module `PolicyJsonInt53`). Idea taken from morluto/rea 6.6.0, which fixed the same defect for +signed 64-bit TOML integers, Android `version_code` and plist integers. + +## The defect + +A JavaScript reader (`JSON.parse`, trinity's website, the t27f wasm host) turns every JSON number +into an f64. An integer above 2^53 - 1 = 9007199254740991 is rounded to a neighbour and nothing +throws. Negative control, computed by the spec's own test +`the_negative_control_9007199254740993_reads_as_9007199254740992`: + +| written | read back | +|---|---| +| 9007199254740993 | 9007199254740992 | +| 9007199254740995 | 9007199254740996 | +| 0x7FF8000000000001 (f64 NaN payload) | 0x7FF8000000000000 | +| 446378386939836973 (`SUPPLY_NGONKA`) | not equal to itself after the round trip | + +## The rule + +A 64-bit or wider integer goes out as a decimal or 0x-hex **string**, or it carries a proof that it +is at most 2^53 - 1 (`form_of()`), and then it may stay a number. Floats are out of scope. + +## Method + +The scan covered what t27 tools write and what `t27c gen-js` prints, at `03c6be104`: + +- every `*.json` tracked in the repo, for a bare integer run above 2^53 - 1 (digits compared as + text, the way the spec's scanner compares them); +- `t27c gen-js` over the 57 specs that hold a 16-digit-or-longer integer literal, run on the + Railway lab, reading every `export const` line. + +## A. Committed JSON: 35 fields in 32 files, 2225 bare integers + +All of these sit in `conformance/vectors/` except the last row. Every one is a bare number a JS +reader rounds. Status for all: **open, writer not fixable in this PR** (see "Writers" below). + +| file | field | bare integers above 2^53 - 1 | +|---|---|---| +| binary128_conformance_v0.json | `binary128_bits_int` | 7 | +| binary256_conformance_v0.json | `binary256_bits_int` | 7 | +| binary64_conformance_v0.json | `binary64_bits_int` | 7 | +| bnf64_conformance_v0.json | `bnf64_bits_int` | 7 | +| cray_float_conformance_v0.json | `cray_float_bits_int` | 7 | +| decimal128_conformance_v0.json | `decimal128_bits_int` | 8 | +| decimal64_conformance_v0.json | `decimal64_bits_int` | 7 | +| double_double_conformance_v0.json | `double_double_bits_int` | 7 | +| gf1024_conformance_v0.json | `bias` | 1 | +| gf1024_conformance_v0.json | `bits` | 13 | +| gf128_conformance_v0.json | `bits` | 13 | +| gf256_conformance_v0.json | `bias` | 1 | +| gf256_conformance_v0.json | `bits` | 2018 | +| gf512_conformance_v0.json | `bias` | 1 | +| gf512_conformance_v0.json | `bits` | 13 | +| gf64_conformance_v0.json | `gf64_bits_int` | 7 | +| gf96_conformance_v0.json | `bits` | 13 | +| gft1024_conformance_v0.json | `bias` | 1 | +| gft128_conformance_v0.json | `bias` | 1 | +| gft256_conformance_v0.json | `bias` | 1 | +| gft512_conformance_v0.json | `bias` | 1 | +| ibm_hfp128_conformance_v0.json | `ibm_hfp128_bits_int` | 7 | +| ibm_hfp64_conformance_v0.json | `ibm_hfp64_bits_int` | 7 | +| int128_conformance_v0.json | `int128_bits_int` | 2 | +| int64_conformance_v0.json | `int64_bits_int` | 2 | +| lns64_conformance_v0.json | `lns64_bits_int` | 2 | +| ms_mbf64_conformance_v0.json | `ms_mbf64_bits_int` | 7 | +| posit64_conformance_v0.json | `posit64_bits_int` | 7 | +| quad_double_conformance_v0.json | `quad_double_bits_int` | 7 | +| takum64_conformance_v0.json | `takum64_bits_int` | 14 | +| vax_d_conformance_v0.json | `vax_d_bits_int` | 7 | +| vax_g_conformance_v0.json | `vax_g_bits_int` | 7 | +| vax_h_conformance_v0.json | `vax_h_bits_int` | 7 | +| x87_fp80_conformance_v0.json | `x87_fp80_bits_int` | 7 | +| conformance/tmem_bridge.json | `id` | 1 (the vector id 9007199254740992 = 2^53) | + +The `tmem_bridge.json` row is deliberate: it is the boundary vector next to `id = 9007199254740991` +and `id = -9007199254740991`, which sit exactly on the safe bound and pass. The bridge spec +(`specs/memory/tmem/bridge.t27`, `TMS_RPC_ID_MAX`) already states the same 2^53 - 1 limit, so that +file is the in-repo precedent for this rule; the 2^53 vector is its refusal test, and the scanner +flags it by design (an allowlist entry, not a defect). + +`gf256_conformance_v0.json` `bits` is 2018 of the 2225: one field of one file. + +Written by hand-written Python (`conformance/vectors/gen_all_formats.py`, +`conformance/gf_wide_independent_witness.py`, `conformance/gen_structural_instances.py` and the +`gen_*.py` siblings in `conformance/vectors/`). Python emits `int` as an arbitrary-precision JSON +number, so the file is exact and the reader is where the value is lost. + +## B. JSON that is already safe + +| document | why | +|---|---| +| `.trinity/seals/*.json` | hashes are hex strings; counts are small numbers | +| `t27c test-report` JSON counts (tests, pass, FAIL, asserts) | counts, far below 2^53 | +| `docs/reports/t27b_expectations.json` | counts and names; no integer run above 2^53 - 1 | +| `conformance/tmem_bridge.json` ids at +/- 9007199254740991 | exactly on the bound | + +## C. `t27c gen-js` output: 121 literals from 53 specs + +`gen-js` prints a `u64`/`i64`/wider `export const` as a bare JS number literal (hex stays a number +literal too), so the module the host imports holds the rounded value. Spec, then constants: + +| spec (under `specs/`) | constants | +|---|---| +| ternary/comb_bitnet_layer.t27 | W_P | +| tools/t27o/rust_convert.t27 | NUM_REFUSED | +| tools/t27o/rust_std.t27 | I64_MAX | +| tri/crypto/hex.t27 | NONE | +| tri/crypto/sha512.t27 | ALL | +| tri/network/payout.t27 | SPLIT_MAX, NOT_A_NUMBER, ACCOUNT_MAX, HELD_BIT, POOL_ID, ID_ACCOUNT_MAX, NO_EPOCH, ALL | +| tri/utils/args.t27 | NONE | +| tri/utils/template.t27 | NONE | +| tri/utils/random.t27 | XORSHIFT_MULTIPLIER, DEFAULT_SEED | +| tri/t27b/comptime_float.t27 | TOP64 | +| tri/t27b/source_text.t27 | I128_MAX, U64_MAX | +| tri/t27b/libm.t27 | qnan64, inf64, ones64, negzero64 (frac64 = 2^52 - 1 is safe) | +| tri/t27b/i128_plan.t27 | max64, sign64, two64, MAX128 | +| tri/t27b/type_text.t27 | LEN_NONE | +| tri/t27b/fuzz.t27 | ALL, GAMMA, MIX1, MIX2, CASE_MIX | +| tri/t27b/verilog_plan.t27 | U64_MAX | +| tri/t27b/blockers.t27 | FNV_OFFSET | +| tri/t27b/conformance/i128_arith.t27 | I128_MAX, U64_MAX, TWO_64 | +| tri/t27b/conformance/wide_int_const.t27 | WC_HALF, WC_FULL, WC_TOP, WC_MIN, WC_MAX, WC_HEX, WC_256, WC_256_TWICE | +| tri/t27b/conformance/i128_ops.t27 | I128_MAX, TWO_64, U64_MAX | +| tri/t27b/conformance/numeric_coercion.t27 | NC_TWO_60 | +| tri/misread/shapes.t27 | NO_FIELD | +| memory/tmem/bridge.t27 | TMS_BRIDGE_DOT_MAX_WIDTH (RPC_ID_MAX/MIN are on the bound and safe) | +| verified/device_dna.t27 | DNA_OBSERVED, DNA_OBSERVED_B | +| verified/payout.t27 | PRICE_OVERFLOW | +| network/usage.t27 | NO_EPOCH, ACCOUNT_MAX, HELD_BIT, POOL_ID | +| network/pool.t27 | AMOUNT_MAX, PRICE_OVERFLOW | +| network/identity.t27 | ID_ACCOUNT_MAX, ALL | +| network/quorum.t27 | LAB1_KEY_ID, LAB2_KEY_ID | +| providers/tri_gnk_pair.t27 | TOTAL_SUBSIDIES_NGONKA, SUPPLY_NGONKA (TOTAL_BURNED_NGONKA is safe) | +| network/attribution.t27 | POOL_ID, HELD_BIT, ACCOUNT_MAX | +| network/mvp.t27 | HEADROOM_OVERRUN, PRICE_OVERFLOW | +| numeric/gft128.t27 | EXP_OFFSET, OFFSET_MAX | +| numeric/paper_claims.t27 | E16, E18 | +| fpga/ddr3_head_bandwidth.t27 | LANE_SALT | +| fpga/rc_filter_ax7203.t27 | EXP_S | +| fpga/trinet_node.t27 | SIP_C0..SIP_C3, PRE_LEN_TOP, EVEN, M2, M4, M8 | +| benchmarks/gf16_bfloat16_nmse_run.t27 | SM_GAMMA, SM_MIX1, SM_MIX2, XO_FIRST_FROM_ZERO | +| hosting/credit.t27 | BALANCE_MAX | +| igla/coder/tokenizer.t27 | NONE | +| igla/coder/pipeline.t27 | PIPE_NONE, NONE | +| port/trinity/src/tri/gen_fuzz.t27 | RNG_ZERO_SEED_STATE | +| port/trios/crates/trios-igla-trainer/src/main.t27 | RNG_MULTIPLIER | +| port/trios/crates/trios-igla-trainer/src/jepa_runner.t27 | LCG_MULT, LCG_INCR | +| port/trios/crates/trios-cli/src/main.t27 | U64_MAX_DIV_10 | +| port/trios/crates/trios-chat/rings/CR-CHAT-02/src/epoch_rollover_wraparound_guard.t27 | EPRW_U64_MAX | +| port/trios/crates/trios-chat/rings/CR-CHAT-00/src/lib.t27 | CHAT_U64_MAX | +| port/conformance/witness/gf48_fp64/gf_decode_param_fp64.t27 | FP64_QNAN, FP64_POS_INF, FP64_NEG_INF | +| effects/clock_cap.t27 | CLOCK_NS_MAX | +| compiler/core/t27core.t27 | W_CONTINUE, W_INVARIA, W_UNDEFINE, W_DEFAULT_, W_VALID_IN, W_ASSERT_E, W_T27_ASSE, W_ENDMODUL | +| queen/actors_hw.t27 | HW_TAG_BITS | +| queen/actor_view.t27 | T_JOB, T_REVIEW | +| queen/actors_hw_jtag.t27 | LCG_MUL, LCG_ADD, EXPECTED_SIG | + +Safe and excluded from the 121: `W_Z`, `_Z` (6004799503160661), `TS_FOLD_MAX` (2^52), +`TMS_RPC_ID_MAX`, `TMS_RPC_ID_MIN`, `TOTAL_BURNED_NGONKA`, `t27b_libm_frac64`. + +Most of the 121 are sentinels (`u64::MAX`, `NONE`), PRNG and hash multipliers, and the 8-byte +`t27core` keyword words. They matter to a JS host only when the host reads the value and compares +or prints it: a hash seed rounded in JS no longer reproduces the t27 test's expected value. The +one that carries money-shaped meaning is `providers/tri_gnk_pair.t27`: `SUPPLY_NGONKA = +446378386939836973` is rounded by `gen-js` to a different integer. + +## D. Unknown (not measurable from this repository) + +| surface | status | +|---|---| +| t27-mcp tool results (`t27mcp`) | unknown: the server lives outside this tree; no integer field of that wire format is above 2^53 in anything checked in here, but the live responses were not sampled | +| trinity-side consumers of the conformance vectors and of `gen-js` modules | unknown: other repository (gHashTag/trinity) | +| corpus receipts written to Railway volumes | unknown: not in the tree, not read in this run | +| `t27c gen-json` IGLA board events | unknown: values go through the `gen-js` layer (`run_gen_json`), so any `u64` field above 2^53 - 1 in a board event inherits section C; no such event was captured | + +## Writers + +None of the section A or C writers can be fixed in this PR under the only-t27 rule: + +- Section A: hand-written Python. The fix is a `.t27` generator that emits the vectors with + `*_bits_int`, `bits` and `bias` as hex or decimal strings, then deleting the Python. +- Section C: `bootstrap/src/codegen_js.rs` and `codegen_ts.rs`. The fix is `gen-js` and `gen-ts` + printing a constant above 2^53 - 1 as a `BigInt` literal (`123n`) or a string; editing existing + Rust needs the `owner-approved-foreign` label. + +Both are filed as follow-ups in the linked issue. This PR lands the rule, its scanner with tests and +negative control, and this list. diff --git a/gen/c/policy/json_int53.c b/gen/c/policy/json_int53.c new file mode 100644 index 0000000000..7dcd19d77b --- /dev/null +++ b/gen/c/policy/json_int53.c @@ -0,0 +1,367 @@ +/* ============================================================================ + Generated from t27 spec: PolicyJsonInt53 + DO NOT EDIT - generated by t27c gen-c + phi^2 + 1/phi^2 = 3 | TRINITY + ============================================================================ */ + +#include +#include +#include +#include +#define t27_assert(c, m) do { if (!(c)) { __builtin_trap(); } } while (0) +#define assert_eq(a, b) do { if ((a) != (b)) { __builtin_trap(); } } while (0) + +#ifndef POLICYJSONINT53_H +#define POLICYJSONINT53_H + +/* ------------------------------------------------------- + Constants + ------------------------------------------------------- */ + +#define SAFE_MAX 9007199254740991 +#define TWO_53 9007199254740992 +static const uint8_t SAFE_MAX_DIGITS[16] = { 57, 48, 48, 55, 49, 57, 57, 50, 53, 52, 55, 52, 48, 57, 57, 49 }; +#define SAFE_MAX_LEN 16 +#define SAFE_BITS 53 +#define FORM_NUMBER 0 +#define FORM_STRING 1 +#define C_QUOTE 34 +#define C_BACKSLASH 92 +#define C_MINUS 45 +#define C_PLUS 43 +#define C_DOT 46 +#define C_E_UP 69 +#define C_E_LOW 101 +#define C_ZERO 48 +#define C_NINE 57 + +/* ------------------------------------------------------- + Function prototypes + ------------------------------------------------------- */ + +uint8_t form_of(uint32_t width, uint32_t proven_bits); +bool is_safe(uint64_t v); +uint64_t js_reads(uint64_t v); +bool is_digit(uint8_t c); +bool run_unsafe(uint8_t* buf, size_t s, size_t e); +size_t string_end(uint8_t* buf, size_t n, size_t i); +size_t number_end(uint8_t* buf, size_t n, size_t i); +bool is_integer_token(uint8_t* buf, size_t s, size_t e); +size_t next_unsafe(uint8_t* buf, size_t n, size_t from); +uint32_t unsafe_count(uint8_t* buf, size_t n); +uint32_t first_unsafe_line(uint8_t* buf, size_t n); + +/* ------------------------------------------------------- + Function implementations + ------------------------------------------------------- */ + +uint8_t form_of(uint32_t width, uint32_t proven_bits) { + if ((width <= SAFE_BITS)) { + return FORM_NUMBER; + } + if (((proven_bits != 0) && (proven_bits <= SAFE_BITS))) { + return FORM_NUMBER; + } + return FORM_STRING; +} + +bool is_safe(uint64_t v) { + return (v <= SAFE_MAX); +} + +uint64_t js_reads(uint64_t v) { + double d = ((double)(v)); + return ((uint64_t)(d)); +} + +bool is_digit(uint8_t c) { + return ((c >= C_ZERO) && (c <= C_NINE)); +} + +bool run_unsafe(uint8_t* buf, size_t s, size_t e) { + size_t a = s; + while ((((a + 1) < e) && (buf[a] == C_ZERO))) { + a = (a + 1); + } + size_t len = (e - a); + if ((len < SAFE_MAX_LEN)) { + return false; + } + if ((len > SAFE_MAX_LEN)) { + return true; + } + size_t i = 0; + while ((i < SAFE_MAX_LEN)) { + uint8_t c = buf[(a + i)]; + uint8_t m = SAFE_MAX_DIGITS[i]; + if ((c != m)) { + return (c > m); + } + i = (i + 1); + } + return false; +} + +size_t string_end(uint8_t* buf, size_t n, size_t i) { + size_t k = (i + 1); + while (((k < n) && (buf[k] != C_QUOTE))) { + if ((buf[k] == C_BACKSLASH)) { + k = (k + 2); + } else { + k = (k + 1); + } + } + if ((k >= n)) { + return n; + } + return (k + 1); +} + +size_t number_end(uint8_t* buf, size_t n, size_t i) { + size_t k = (i + 1); + while ((k < n)) { + uint8_t c = buf[k]; + if ((((((is_digit(c) || (c == C_DOT)) || (c == C_E_UP)) || (c == C_E_LOW)) || (c == C_PLUS)) || (c == C_MINUS))) { + k = (k + 1); + } else { + return k; + } + } + return n; +} + +bool is_integer_token(uint8_t* buf, size_t s, size_t e) { + size_t i = s; + while ((i < e)) { + if ((((buf[i] == C_DOT) || (buf[i] == C_E_UP)) || (buf[i] == C_E_LOW))) { + return false; + } + i = (i + 1); + } + return true; +} + +size_t next_unsafe(uint8_t* buf, size_t n, size_t from) { + size_t i = from; + while ((i < n)) { + uint8_t c = buf[i]; + if ((c == C_QUOTE)) { + i = string_end(buf, n, i); + } else if (((c == C_MINUS) || is_digit(c))) { + size_t e = number_end(buf, n, i); + if (is_integer_token(buf, i, e)) { + size_t s = i; + if ((buf[s] == C_MINUS)) { + s = (s + 1); + } + if (run_unsafe(buf, s, e)) { + return i; + } + } + i = e; + } else { + i = (i + 1); + } + } + return n; +} + +uint32_t unsafe_count(uint8_t* buf, size_t n) { + uint32_t count = 0; + size_t at = next_unsafe(buf, n, 0); + while ((at < n)) { + count = (count + 1); + at = next_unsafe(buf, n, number_end(buf, n, at)); + } + return count; +} + +uint32_t first_unsafe_line(uint8_t* buf, size_t n) { + size_t at = next_unsafe(buf, n, 0); + if ((at >= n)) { + return 0; + } + uint32_t line = 1; + size_t i = 0; + while ((i < at)) { + if ((buf[i] == 10)) { + line = (line + 1); + } + i = (i + 1); + } + return line; +} + +/* ------------------------------------------------------- + Tests + ------------------------------------------------------- */ + +void test_the_negative_control_9007199254740993_reads_as_9007199254740992(void) { + assert((js_reads(9007199254740993) == 9007199254740992)); + assert((js_reads(9007199254740993) != 9007199254740993)); + assert((js_reads(9007199254740995) == 9007199254740996)); +} + +void test_the_last_safe_integer_is_read_back_unchanged(void) { + assert((js_reads(9007199254740991) == 9007199254740991)); + assert((js_reads(9007199254740992) == 9007199254740992)); + assert((js_reads(1234567890123) == 1234567890123)); + assert(is_safe(9007199254740991)); + assert((is_safe(9007199254740992) == false)); + assert((TWO_53 == (SAFE_MAX + 1))); +} + +void test_an_f64_nan_payload_does_not_survive_a_json_number(void) { + assert((js_reads(0x7FF8000000000001) == 0x7FF8000000000000)); + assert((js_reads(0x7FF8000000000001) != 0x7FF8000000000001)); + assert((js_reads(0x7FF0000000000000) == 0x7FF0000000000000)); +} + +void test_a_u64_hash_does_not_survive_a_json_number(void) { + assert((js_reads(0x0CBF29CE484222FF) != 0x0CBF29CE484222FF)); + assert(((js_reads(0x0CBF29CE484222FF) - 0x0CBF29CE48422000) < 1024)); +} + +void test_the_measured_token_supply_is_not_a_safe_integer(void) { + assert((is_safe(446378386939836973) == false)); + assert((js_reads(446378386939836973) != 446378386939836973)); + assert(is_safe(1174606773777)); + assert(is_safe(1284341372978310)); +} + +void test_a_wide_field_is_a_string_unless_it_is_proven_small(void) { + assert((form_of(8, 0) == FORM_NUMBER)); + assert((form_of(32, 0) == FORM_NUMBER)); + assert((form_of(53, 0) == FORM_NUMBER)); + assert((form_of(64, 0) == FORM_STRING)); + assert((form_of(128, 0) == FORM_STRING)); + assert((form_of(64, 40) == FORM_NUMBER)); + assert((form_of(64, 53) == FORM_NUMBER)); + assert((form_of(64, 54) == FORM_STRING)); + assert((form_of(128, 64) == FORM_STRING)); +} + +void test_a_digit_run_is_unsafe_exactly_above_two_to_the_53_minus_1(void) { + assert((run_unsafe("9007199254740991", 0, 16) == false)); + assert(run_unsafe("9007199254740992", 0, 16)); + assert(run_unsafe("9007199254740993", 0, 16)); + assert(run_unsafe("9999999999999999", 0, 16)); + assert((run_unsafe("9007199254740990", 0, 16) == false)); + assert((run_unsafe("1000000000000000", 0, 16) == false)); + assert((run_unsafe("999999999999999", 0, 15) == false)); + assert(run_unsafe("10000000000000000", 0, 17)); + assert(run_unsafe("18446744073709551615", 0, 20)); +} + +void test_leading_zeros_and_short_runs_are_not_counted(void) { + assert((run_unsafe("0", 0, 1) == false)); + assert((run_unsafe("0009007199254740991", 0, 19) == false)); + assert(run_unsafe("0009007199254740992", 0, 19)); + assert((run_unsafe("00000000000000000000", 0, 20) == false)); + assert((run_unsafe("", 0, 0) == false)); +} + +void test_a_bare_integer_above_the_bound_is_found_with_its_line(void) { + const char* one = "{\"a\": 9007199254740993}"; + assert((unsafe_count(one, one.len) == 1)); + assert((first_unsafe_line(one, one.len) == 1)); + const char* lines = "{\n\"a\": 1,\n\"b\": 9007199254740993\n}"; + assert((first_unsafe_line(lines, lines.len) == 3)); + const char* two = "[1, 2, 18446744073709551615, -9223372036854775808, 3]"; + assert((unsafe_count(two, two.len) == 2)); +} + +void test_a_bare_integer_at_or_below_the_bound_passes(void) { + const char* ok = "{\"a\": 9007199254740991, \"b\": -9007199254740991, \"c\": 0}"; + assert((unsafe_count(ok, ok.len) == 0)); + const char* empty_list = "[]"; + assert((unsafe_count(empty_list, empty_list.len) == 0)); + assert((unsafe_count("", 0) == 0)); + const char* small = "{\"a\": 1}"; + assert((first_unsafe_line(small, small.len) == 0)); +} + +void test_a_negative_integer_is_judged_by_its_magnitude(void) { + const char* over = "[-9007199254740992]"; + assert((unsafe_count(over, over.len) == 1)); + const char* edge = "[-9007199254740991]"; + assert((unsafe_count(edge, edge.len) == 0)); +} + +void test_a_string_spelling_passes_and_a_bare_one_after_it_is_still_found(void) { + const char* dec = "{\"bits\": \"9007199254740993\"}"; + assert((unsafe_count(dec, dec.len) == 0)); + const char* hex = "{\"bits\": \"0x7FF8000000000001\"}"; + assert((unsafe_count(hex, hex.len) == 0)); + const char* esc = "{\"k\": \"a \\\" 99999999999999999999 b\"}"; + assert((unsafe_count(esc, esc.len) == 0)); + const char* esc_then_bare = "{\"k\": \"a \\\" 99999999999999999999 b\", \"z\": 99999999999999999999}"; + assert((unsafe_count(esc_then_bare, esc_then_bare.len) == 1)); + const char* unclosed = "{\"k\": \"99999999999999999999"; + assert((unsafe_count(unclosed, unclosed.len) == 0)); +} + +void test_a_float_literal_is_not_this_rules_business_and_the_bare_integer_is(void) { + const char* f1 = "[99999999999999999999.0]"; + assert((unsafe_count(f1, f1.len) == 0)); + const char* f2 = "[1e300]"; + assert((unsafe_count(f2, f2.len) == 0)); + const char* f3 = "[1.618033988749894848]"; + assert((unsafe_count(f3, f3.len) == 0)); + const char* bare = "[99999999999999999999]"; + assert((unsafe_count(bare, bare.len) == 1)); +} + +void test_the_measured_conformance_vector_line_is_found(void) { + const char* bits = "{\"binary64_bits_int\": 4607182418800017408}"; + assert((unsafe_count(bits, bits.len) == 1)); + const char* as_string = "{\"binary64_bits_int\": \"4607182418800017408\"}"; + assert((unsafe_count(as_string, as_string.len) == 0)); + const char* bias = "{\"bias\": 79228162514264337593543950335}"; + assert((unsafe_count(bias, bias.len) == 1)); +} + +void test_the_rpc_id_vectors_of_tmem_bridge_sit_exactly_on_the_bound(void) { + const char* max = "{\"id\": 9007199254740991}"; + assert((unsafe_count(max, max.len) == 0)); + const char* min = "{\"id\": -9007199254740991}"; + assert((unsafe_count(min, min.len) == 0)); + const char* over = "{\"id\": 9007199254740992}"; + assert((unsafe_count(over, over.len) == 1)); +} + +void test_every_bare_integer_is_counted_not_only_the_first(void) { + const char* many = "{\"a\": 18446744073709551615, \"b\": [9007199254740993, 5, -9223372036854775808], \"c\": \"x\", \"d\": 1}"; + assert((unsafe_count(many, many.len) == 3)); +} + + +/* ------------------------------------------------------- + Test runner (compile with -DT27_TEST_MAIN to execute) + ------------------------------------------------------- */ + +#ifdef T27_TEST_MAIN +#include +int main(void) { + test_the_negative_control_9007199254740993_reads_as_9007199254740992(); + test_the_last_safe_integer_is_read_back_unchanged(); + test_an_f64_nan_payload_does_not_survive_a_json_number(); + test_a_u64_hash_does_not_survive_a_json_number(); + test_the_measured_token_supply_is_not_a_safe_integer(); + test_a_wide_field_is_a_string_unless_it_is_proven_small(); + test_a_digit_run_is_unsafe_exactly_above_two_to_the_53_minus_1(); + test_leading_zeros_and_short_runs_are_not_counted(); + test_a_bare_integer_above_the_bound_is_found_with_its_line(); + test_a_bare_integer_at_or_below_the_bound_passes(); + test_a_negative_integer_is_judged_by_its_magnitude(); + test_a_string_spelling_passes_and_a_bare_one_after_it_is_still_found(); + test_a_float_literal_is_not_this_rules_business_and_the_bare_integer_is(); + test_the_measured_conformance_vector_line_is_found(); + test_the_rpc_id_vectors_of_tmem_bridge_sit_exactly_on_the_bound(); + test_every_bare_integer_is_counted_not_only_the_first(); + printf("All %d tests passed.\n", 16); + return 0; +} +#endif /* T27_TEST_MAIN */ + +#endif /* POLICYJSONINT53_H */ diff --git a/specs/policy/json_int53.t27 b/specs/policy/json_int53.t27 new file mode 100644 index 0000000000..9e0a6cb078 --- /dev/null +++ b/specs/policy/json_int53.t27 @@ -0,0 +1,332 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/policy/json_int53.t27 -- a 64-bit integer does not travel as a bare JSON number. +; A JSON number has no width, but the reader that matters here does: JavaScript (trinity's website, +; the t27f wasm host, the t27-mcp server) reads every JSON number into an f64. An integer above +; 2^53 - 1 comes back as the nearest multiple of 2, 4, 8, ... : 9007199254740993 is read as +; 9007199254740992 (test the_negative_control_9007199254740993_reads_as_9007199254740992), and the f64 +; bit pattern 0x7FF8000000000001 (a NaN payload) as 0x7FF8000000000000. Nothing throws; the number is +; simply another number. Idea taken from morluto/rea 6.6.0, which fixed the same defect three times +; (signed 64-bit TOML integers, Android version_code, plist integers). +; -- +; The rule, for every JSON document a t27 tool writes and every JS value `t27c gen-js` prints: +; - a 64-bit (or wider) integer goes out as a STRING, decimal or 0x-hex, never as a bare number; or +; - it carries a proof that it is <= 2^53 - 1 (a loop bound, a count, a width), and then it may stay a +; number. form_of() decides which. An unproven u64 is a string. +; - a float is a float: a decimal point or exponent makes a token a float literal, which a JS reader +; rounds the way the spec already says it is rounded. This rule is about integers only. +; -- +; The scanner finds bare integers the rule forbids. Inside a JSON string nothing is scanned, so +; "0x7FF8000000000001" and "9007199254740993" are the compliant spellings and pass. A digit run is +; unsafe when its value exceeds 2^53 - 1 = 9007199254740991; the sign does not matter (the magnitude +; is what a double cannot hold). The comparison is on the digits as text, so the scanner itself needs +; no 64-bit arithmetic, which is the point: it must not use a number type that would round. +; -- +; Measured 2026-10-18 (gHashTag/t27 @ 03c6be104, docs/reports/2026-10-18-json-int53-measured.md): +; 35 (file, field) pairs in 32 committed JSON files carry 2225 bare integers above 2^53 - 1, all in +; conformance/vectors/*.json (written by hand-written Python generators, not by t27c) except the +; one deliberate 2^53 boundary id in conformance/tmem_bridge.json; and 121 +; `export const` lines that `t27c gen-js` prints as bare number literals above 2^53 - 1, from 53 +; specs, among them the Providers token supply SUPPLY_NGONKA = 446378386939836973. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module PolicyJsonInt53; + +/// 2^53 - 1, the largest integer every double holds exactly, and 2^53, the first one that shares its +/// double with a neighbour. Number.isSafeInteger(2^53) is false for that reason. +pub const SAFE_MAX : u64 = 9007199254740991; +pub const TWO_53 : u64 = 9007199254740992; + +/// SAFE_MAX as ASCII digits (57 is the digit 9): its length is the longest digit run that can still be safe. +pub const SAFE_MAX_DIGITS : [16]u8 = [57, 48, 48, 55, 49, 57, 57, 50, 53, 52, 55, 52, 48, 57, 57, 49]; +pub const SAFE_MAX_LEN : usize = 16; + +/// Bits a bare JSON number may use: 53 value bits. Wider integers go out as strings. +pub const SAFE_BITS : u32 = 53; + +/// Verdicts of form_of(). +pub const FORM_NUMBER : u8 = 0; +pub const FORM_STRING : u8 = 1; + +/// The bytes the scanner reads, by number (t27c does not read escapes in char literals). +pub const C_QUOTE : u8 = 34; +pub const C_BACKSLASH : u8 = 92; +pub const C_MINUS : u8 = 45; +pub const C_PLUS : u8 = 43; +pub const C_DOT : u8 = 46; +pub const C_E_UP : u8 = 69; +pub const C_E_LOW : u8 = 101; +pub const C_ZERO : u8 = 48; +pub const C_NINE : u8 = 57; + +/// How a field of `width` bits, with a proven magnitude bound of `proven_bits` bits (0 = no proof), +/// goes out. A 64-bit field with no proof is a string; a 64-bit field proven to hold 40-bit values +/// may stay a number; a u32 is a number without a proof because its width is the proof. +pub fn form_of(width: u32, proven_bits: u32) -> u8 { + if (width <= SAFE_BITS) { return FORM_NUMBER; } + if (proven_bits != 0 and proven_bits <= SAFE_BITS) { return FORM_NUMBER; } + return FORM_STRING; +} + +/// Is v a value a JS reader gives back unchanged? +pub fn is_safe(v: u64) -> bool { + return v <= SAFE_MAX; +} + +/// The value a JS reader gives back for v: v rounded to the nearest double (ties to even) and back. +/// Defined for v below 2^63, where the double converts back to a u64 without overflow. +pub fn js_reads(v: u64) -> u64 { + const d : f64 = v as f64; + return d as u64; +} + +/// Is c an ASCII digit? +pub fn is_digit(c: u8) -> bool { + return c >= C_ZERO and c <= C_NINE; +} + +/// Is the digit run buf[s..e) (no sign) above 2^53 - 1? Leading zeros do not count. +pub fn run_unsafe(buf: []const u8, s: usize, e: usize) -> bool { + var a : usize = s; + while (a + 1 < e and buf[a] == C_ZERO) { a = a + 1; } + const len : usize = e - a; + if (len < SAFE_MAX_LEN) { return false; } + if (len > SAFE_MAX_LEN) { return true; } + var i : usize = 0; + while (i < SAFE_MAX_LEN) { + const c : u8 = buf[a + i]; + const m : u8 = SAFE_MAX_DIGITS[i]; + if (c != m) { return c > m; } + i = i + 1; + } + return false; +} + +/// Index just past the JSON string whose opening quote is at buf[i], or n when it is not closed. +pub fn string_end(buf: []const u8, n: usize, i: usize) -> usize { + var k : usize = i + 1; + while (k < n and buf[k] != C_QUOTE) { + if (buf[k] == C_BACKSLASH) { k = k + 2; } else { k = k + 1; } + } + if (k >= n) { return n; } + return k + 1; +} + +/// Index just past the number token that starts at buf[i] (a '-' or a digit). +pub fn number_end(buf: []const u8, n: usize, i: usize) -> usize { + var k : usize = i + 1; + while (k < n) { + const c : u8 = buf[k]; + if (is_digit(c) or c == C_DOT or c == C_E_UP or c == C_E_LOW or c == C_PLUS or c == C_MINUS) { + k = k + 1; + } else { + return k; + } + } + return n; +} + +/// Is the number token buf[s..e) an integer, with no decimal point and no exponent? +pub fn is_integer_token(buf: []const u8, s: usize, e: usize) -> bool { + var i : usize = s; + while (i < e) { + if (buf[i] == C_DOT or buf[i] == C_E_UP or buf[i] == C_E_LOW) { return false; } + i = i + 1; + } + return true; +} + +/// Offset of the first digit-or-minus of the next bare integer above 2^53 - 1 at or after `from`, +/// or n when there is none. Strings are skipped whole. +pub fn next_unsafe(buf: []const u8, n: usize, from: usize) -> usize { + var i : usize = from; + while (i < n) { + const c : u8 = buf[i]; + if (c == C_QUOTE) { + i = string_end(buf, n, i); + } else if (c == C_MINUS or is_digit(c)) { + const e : usize = number_end(buf, n, i); + if (is_integer_token(buf, i, e)) { + var s : usize = i; + if (buf[s] == C_MINUS) { s = s + 1; } + if (run_unsafe(buf, s, e)) { return i; } + } + i = e; + } else { + i = i + 1; + } + } + return n; +} + +/// How many bare integers above 2^53 - 1 buf[0..n] holds. +pub fn unsafe_count(buf: []const u8, n: usize) -> u32 { + var count : u32 = 0; + var at : usize = next_unsafe(buf, n, 0); + while (at < n) { + count = count + 1; + at = next_unsafe(buf, n, number_end(buf, n, at)); + } + return count; +} + +/// 1-based line of the first bare integer above 2^53 - 1, or 0 when there is none, so CI can print +/// path:line. +pub fn first_unsafe_line(buf: []const u8, n: usize) -> u32 { + const at : usize = next_unsafe(buf, n, 0); + if (at >= n) { return 0; } + var line : u32 = 1; + var i : usize = 0; + while (i < at) { + if (buf[i] == 10) { line = line + 1; } + i = i + 1; + } + return line; +} + +; --- The negative control: the rounding itself --------------------------------------------------------- + +test the_negative_control_9007199254740993_reads_as_9007199254740992 { + assert js_reads(9007199254740993) == 9007199254740992; + assert js_reads(9007199254740993) != 9007199254740993; + assert js_reads(9007199254740995) == 9007199254740996; +} + +test the_last_safe_integer_is_read_back_unchanged { + assert js_reads(9007199254740991) == 9007199254740991; + assert js_reads(9007199254740992) == 9007199254740992; + assert js_reads(1234567890123) == 1234567890123; + assert is_safe(9007199254740991); + assert is_safe(9007199254740992) == false; + assert TWO_53 == SAFE_MAX + 1; +} + +test an_f64_nan_payload_does_not_survive_a_json_number { + assert js_reads(0x7FF8000000000001) == 0x7FF8000000000000; + assert js_reads(0x7FF8000000000001) != 0x7FF8000000000001; + assert js_reads(0x7FF0000000000000) == 0x7FF0000000000000; +} + +test a_u64_hash_does_not_survive_a_json_number { + assert js_reads(0x0CBF29CE484222FF) != 0x0CBF29CE484222FF; + assert js_reads(0x0CBF29CE484222FF) - 0x0CBF29CE48422000 < 1024; +} + +test the_measured_token_supply_is_not_a_safe_integer { + assert is_safe(446378386939836973) == false; + assert js_reads(446378386939836973) != 446378386939836973; + assert is_safe(1174606773777); + assert is_safe(1284341372978310); +} + +; --- The form a field goes out in ---------------------------------------------------------------------- + +test a_wide_field_is_a_string_unless_it_is_proven_small { + assert form_of(8, 0) == FORM_NUMBER; + assert form_of(32, 0) == FORM_NUMBER; + assert form_of(53, 0) == FORM_NUMBER; + assert form_of(64, 0) == FORM_STRING; + assert form_of(128, 0) == FORM_STRING; + assert form_of(64, 40) == FORM_NUMBER; + assert form_of(64, 53) == FORM_NUMBER; + assert form_of(64, 54) == FORM_STRING; + assert form_of(128, 64) == FORM_STRING; +} + +; --- The digit run ---------------------------------------------------------------------------------------- + +test a_digit_run_is_unsafe_exactly_above_two_to_the_53_minus_1 { + assert run_unsafe("9007199254740991", 0, 16) == false; + assert run_unsafe("9007199254740992", 0, 16); + assert run_unsafe("9007199254740993", 0, 16); + assert run_unsafe("9999999999999999", 0, 16); + assert run_unsafe("9007199254740990", 0, 16) == false; + assert run_unsafe("1000000000000000", 0, 16) == false; + assert run_unsafe("999999999999999", 0, 15) == false; + assert run_unsafe("10000000000000000", 0, 17); + assert run_unsafe("18446744073709551615", 0, 20); +} + +test leading_zeros_and_short_runs_are_not_counted { + assert run_unsafe("0", 0, 1) == false; + assert run_unsafe("0009007199254740991", 0, 19) == false; + assert run_unsafe("0009007199254740992", 0, 19); + assert run_unsafe("00000000000000000000", 0, 20) == false; + assert run_unsafe("", 0, 0) == false; +} + +; --- The scanner ------------------------------------------------------------------------------------------ +; Each input is a const so its length comes from `.len`, not from a hand count that could cut the scan short. + +test a_bare_integer_above_the_bound_is_found_with_its_line { + const one : str = "{\"a\": 9007199254740993}"; + assert unsafe_count(one, one.len) == 1; + assert first_unsafe_line(one, one.len) == 1; + const lines : str = "{\n\"a\": 1,\n\"b\": 9007199254740993\n}"; + assert first_unsafe_line(lines, lines.len) == 3; + const two : str = "[1, 2, 18446744073709551615, -9223372036854775808, 3]"; + assert unsafe_count(two, two.len) == 2; +} + +test a_bare_integer_at_or_below_the_bound_passes { + const ok : str = "{\"a\": 9007199254740991, \"b\": -9007199254740991, \"c\": 0}"; + assert unsafe_count(ok, ok.len) == 0; + const empty_list : str = "[]"; + assert unsafe_count(empty_list, empty_list.len) == 0; + assert unsafe_count("", 0) == 0; + const small : str = "{\"a\": 1}"; + assert first_unsafe_line(small, small.len) == 0; +} + +test a_negative_integer_is_judged_by_its_magnitude { + const over : str = "[-9007199254740992]"; + assert unsafe_count(over, over.len) == 1; + const edge : str = "[-9007199254740991]"; + assert unsafe_count(edge, edge.len) == 0; +} + +test a_string_spelling_passes_and_a_bare_one_after_it_is_still_found { + const dec : str = "{\"bits\": \"9007199254740993\"}"; + assert unsafe_count(dec, dec.len) == 0; + const hex : str = "{\"bits\": \"0x7FF8000000000001\"}"; + assert unsafe_count(hex, hex.len) == 0; + const esc : str = "{\"k\": \"a \\\" 99999999999999999999 b\"}"; + assert unsafe_count(esc, esc.len) == 0; + const esc_then_bare : str = "{\"k\": \"a \\\" 99999999999999999999 b\", \"z\": 99999999999999999999}"; + assert unsafe_count(esc_then_bare, esc_then_bare.len) == 1; + const unclosed : str = "{\"k\": \"99999999999999999999"; + assert unsafe_count(unclosed, unclosed.len) == 0; +} + +test a_float_literal_is_not_this_rules_business_and_the_bare_integer_is { + const f1 : str = "[99999999999999999999.0]"; + assert unsafe_count(f1, f1.len) == 0; + const f2 : str = "[1e300]"; + assert unsafe_count(f2, f2.len) == 0; + const f3 : str = "[1.618033988749894848]"; + assert unsafe_count(f3, f3.len) == 0; + const bare : str = "[99999999999999999999]"; + assert unsafe_count(bare, bare.len) == 1; +} + +test the_measured_conformance_vector_line_is_found { + const bits : str = "{\"binary64_bits_int\": 4607182418800017408}"; + assert unsafe_count(bits, bits.len) == 1; + const as_string : str = "{\"binary64_bits_int\": \"4607182418800017408\"}"; + assert unsafe_count(as_string, as_string.len) == 0; + const bias : str = "{\"bias\": 79228162514264337593543950335}"; + assert unsafe_count(bias, bias.len) == 1; +} + +test the_rpc_id_vectors_of_tmem_bridge_sit_exactly_on_the_bound { + const max : str = "{\"id\": 9007199254740991}"; + assert unsafe_count(max, max.len) == 0; + const min : str = "{\"id\": -9007199254740991}"; + assert unsafe_count(min, min.len) == 0; + const over : str = "{\"id\": 9007199254740992}"; + assert unsafe_count(over, over.len) == 1; +} + +test every_bare_integer_is_counted_not_only_the_first { + const many : str = "{\"a\": 18446744073709551615, \"b\": [9007199254740993, 5, -9223372036854775808], \"c\": \"x\", \"d\": 1}"; + assert unsafe_count(many, many.len) == 3; +}