`fx_gate.nx` source

↩ module page · 108 lines · 5222 B
1// fx_gate.nx -- the gate for the Q16.16 fixed-point math 49 modules import.
2// WHY: nx_gensota gen-3 worklist. This module exists for ONE reason -- bit-identical simulation
3// across machines (rollback netcode); IEEE-754 cannot deliver it. Its header numbers four
4// invariants FX1-FX4, and an invariant nothing checks is a wish.
5// ★SCOPE DECLARED HONESTLY: determinism has an IN-PROCESS half (same input -> same bits, every
6// call) and a CROSS-MACHINE half (same bits on every target). T9 proves the first. The second
7// CANNOT be proven from one host and is NOT claimed here -- it would need the same vectors run
8// on a second architecture and compared. Saying so beats a gate that implies coverage it lacks.
9// ⚠OPEN QUESTION FILED, NOT GUESSED (see debt): FX2 says fx_mul and fx_div "round toward zero
10// (arithmetic shift)" -- but an arithmetic right shift rounds toward NEGATIVE INFINITY on
11// negatives while integer division truncates toward ZERO, so the two may DISAGREE on negative
12// operands. Rather than pin a guessed direction, T5 asserts the property that is true either
13// way and matters to callers: the result is within ONE ULP of the exact product.
14// license_tier: ORIGINAL  expect_exit: 0  No hw writes (Rule 26).
15import "nx_syscalls.nx"
16import "nx_gate_verdict.nx"
17import "fx.nx"
18
19func fxg_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v }
20
21func main() -> i64 {
22    let ctr: *i64 = gv_ctr()
23    gv_head("FX-GATE -- the Q16.16 determinism contract 49 modules import" as *u8)
24
25    var t1: i64 = 1
26    if FX_ONE != (1 << FX_SHIFT) { t1 = 0 }
27    if FX_HALF * 2 != FX_ONE { t1 = 0 }
28    if FX_FRAC_MASK != FX_ONE - 1 { t1 = 0 }
29    gv_check("T1 scale constants are mutually CONSISTENT (ONE, HALF, FRAC_MASK)" as *u8, t1, ctr)
30
31    var t2: i64 = 1
32    if fx_to_int(fx_from_int(0)) != 0 { t2 = 0 }
33    if fx_to_int(fx_from_int(7)) != 7 { t2 = 0 }
34    if fx_to_int(fx_from_int(32000)) != 32000 { t2 = 0 }
35    if fx_to_int(fx_from_int(0 - 7)) != (0 - 7) { t2 = 0 }
36    gv_check("T2 from_int/to_int ROUND-TRIPS incl. negative and near-range" as *u8, t2, ctr)
37
38    var t3: i64 = 1
39    if fx_mul(FX_ONE, FX_ONE) != FX_ONE { t3 = 0 }
40    if fx_mul(fx_from_int(5), FX_ONE) != fx_from_int(5) { t3 = 0 }
41    if fx_mul(fx_from_int(0 - 5), FX_ONE) != fx_from_int(0 - 5) { t3 = 0 }
42    if fx_mul(FX_HALF, fx_from_int(4)) != fx_from_int(2) { t3 = 0 }
43    gv_check("T3 mul: ONE is the identity (both signs); half x 4 == 2 exactly" as *u8, t3, ctr)
44
45    var t4: i64 = 1
46    if fx_div(FX_ONE, FX_ONE) != FX_ONE { t4 = 0 }
47    if fx_div(fx_from_int(9), FX_ONE) != fx_from_int(9) { t4 = 0 }
48    if fx_div(fx_from_int(0 - 9), FX_ONE) != fx_from_int(0 - 9) { t4 = 0 }
49    if fx_div(fx_from_int(6), fx_from_int(2)) != fx_from_int(3) { t4 = 0 }
50    gv_check("T4 div: ONE is the identity (both signs); 6/2 == 3 exactly" as *u8, t4, ctr)
51
52    // FX2 without guessing the rounding DIRECTION -- see header.
53    var t5: i64 = 1
54    var probe: i64 = 0 - 3
55    var iters: i64 = 0
56    while iters < 5 {
57        let a: i64 = probe
58        let b: i64 = FX_HALF + 7
59        let got: i64 = fx_mul(a, b)
60        let exact_num: i64 = a * b
61        let lo: i64 = got << FX_SHIFT
62        if fxg_abs(exact_num - lo) >= FX_ONE { t5 = 0 }
63        probe = probe * 11 + 13
64        iters = iters + 1
65    }
66    gv_check("T5 FX2: mul is within ONE ULP of the exact product (true for either rounding rule)" as *u8, t5, ctr)
67
68    var t6: i64 = 1
69    if fx_from_frac(1, 2) != FX_HALF { t6 = 0 }
70    if fx_from_frac(3, 1) != fx_from_int(3) { t6 = 0 }
71    if fx_from_frac(1, 4) != FX_HALF / 2 { t6 = 0 }
72    gv_check("T6 from_frac builds EXACT rationals (1/2, 3/1, 1/4)" as *u8, t6, ctr)
73
74    // the module's own stated exactness claim
75    var t7: i64 = 1
76    if fx_log2(FX_ONE) != 0 { t7 = 0 }
77    if fx_log2(FX_ONE << 1) != FX_ONE { t7 = 0 }
78    if fx_log2(FX_ONE << 3) != 3 * FX_ONE { t7 = 0 }
79    if fx_log2(FX_ONE << 10) != 10 * FX_ONE { t7 = 0 }
80    gv_check("T7 STATED CLAIM: log2 is EXACT on powers of two (2^0,2^1,2^3,2^10)" as *u8, t7, ctr)
81
82    // documented defensive boundary (Rule 12)
83    var t8: i64 = 1
84    if fx_log2(0) != 0 { t8 = 0 }
85    if fx_log2(0 - 5) != 0 { t8 = 0 }
86    gv_check("T8 log2 domain guard: <=0 returns 0, never a garbage value or a hang" as *u8, t8, ctr)
87
88    // FX1/FX3 raison d'etre: same input -> same bits, every call (IN-PROCESS half)
89    var t9: i64 = 1
90    var k: i64 = 0
91    while k < 4 {
92        let x: i64 = FX_ONE + k * 7919
93        if fx_log2(x) != fx_log2(x) { t9 = 0 }
94        if fx_mul(x, x) != fx_mul(x, x) { t9 = 0 }
95        if fx_div(x, FX_HALF) != fx_div(x, FX_HALF) { t9 = 0 }
96        k = k + 1
97    }
98    gv_check("T9 DETERMINISM (in-process): identical inputs give identical bits, 4 values" as *u8, t9, ctr)
99
100    // NEG-CONTROL: the comparators must be capable of failing.
101    var t10: i64 = 0
102    if fx_log2(FX_ONE << 1) != 3 * FX_ONE { if fx_mul(FX_ONE, FX_ONE) != 0 { if fx_from_int(1) != 1 { t10 = 1 } } }
103    gv_check("T10 NEG-CONTROL: wrong log2, wrong product and raw-int confusion all REJECT" as *u8, t10, ctr)
104
105    let rc: i64 = gv_verdict("FX-GATE" as *u8, ctr, "Q16.16 invariants checked; cross-machine half declared out of scope" as *u8)
106    sys_exit(rc)
107    return rc
108}
fx_gate.nx source

`fx_gate.nx` source
