nx_fx_gate.nx source
↩ module page · 116 lines · 5672 B
1// nx_fx_gate.nx -- F984 INDEPENDENT GATE: exact multi-currency conversion.
2// Proves the SOTA property that a currency conversion loses NO value -- the remainder is accounted and
3// the source amount reconstructs EXACTLY -- plus fail-closed on a bad rate and provenance-gated pricing.
4// license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
5
6import "nx_fx_lib.nx"
7
8func fg_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
9func fg_putn(v: i64) -> i64 {
10 let t: *u8 = sys_mmap(32)
11 var o: i64 = 0
12 var m: i64 = v
13 if m < 0 { t[o] = 45 as u8; o = o + 1; m = 0 - m }
14 let d: *u8 = sys_mmap(32)
15 var k: i64 = 0
16 if m == 0 { d[0] = 48 as u8; k = 1 }
17 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
18 var i: i64 = 0
19 while i < k { t[o] = d[k - 1 - i]; o = o + 1; i = i + 1 }
20 sys_write(1, t, o)
21 return 0
22}
23func fg_ck(cnt: *i64, name: *u8, got: i64, want: i64) -> i64 {
24 if got == want {
25 cnt[0] = cnt[0] + 1
26 fg_puts(" PASS " as *u8); fg_puts(name); fg_puts(" = " as *u8); fg_putn(got); fg_puts("\n" as *u8)
27 return 1
28 }
29 cnt[1] = cnt[1] + 1
30 fg_puts(" FAIL " as *u8); fg_puts(name); fg_puts(" got " as *u8); fg_putn(got)
31 fg_puts(" want " as *u8); fg_putn(want); fg_puts("\n" as *u8)
32 return 0
33}
34func fg_id(tag: *u8, nonce: i64, out: *u8) -> i64 {
35 var o: i64 = mt_catcopy(out, 0, tag)
36 o = mt_catn(out, o, nonce)
37 out[o] = 0 as u8
38 return o
39}
40
41func main(argc: i64, argv: *i64) -> i64 {
42 // FIXTURE MOVED OUT OF THE SWEPT STORE (2026-08-07). knowledge/store/ is walked every 600s by
43 // the nx_segguard beat; this gate's fixture is one of TEN measured as actually folded by it. A
44 // fold landing mid-run rewrites the manifest under the code being measured, so a RED could not
45 // be attributed. Proven on the sibling defect: the SAME code went RED on a knowledge/store
46 // fixture and GREEN 24/24 on a /tmp one -- the RED tracked the FIXTURE, not the code.
47 // Created at SETUP, not teardown: a teardown does not run when a run crashes.
48 sys_mkdir("/tmp/fxgate\x00" as *u8, 0x1ed)
49 let pfx: *u8 = "/tmp/fxgate/fxgate-" as *u8
50 let nonce: i64 = sys_now_us()
51 let cnt: *i64 = sys_mmap(16) as *i64
52 cnt[0] = 0
53 cnt[1] = 0
54 let rem: *i64 = sys_mmap(16) as *i64
55
56 fg_puts("NISHI-FX-GATE (F984 exact multi-currency: conversion loses no value)\n" as *u8)
57
58 // ---- X1: clean conversion. $100.00 (10000c) at 0.85 EUR/USD (rate 85/100) -> 8500c, remainder 0 ----
59 fg_ck(cnt, "X1 $100.00 at 0.85 -> 8500 minor units" as *u8, fx_convert(10000, 85, 100, rem), 8500)
60 fg_ck(cnt, "X1a exact, zero remainder" as *u8, rem[0], 0)
61
62 // ---- X2: a conversion WITH a remainder -- 100 at 1/3 -> 33, remainder 1 (NOT silently dropped) ----
63 fg_ck(cnt, "X2 100 at 1/3 -> 33 minor units" as *u8, fx_convert(100, 1, 3, rem), 33)
64 fg_ck(cnt, "X2a remainder = 1 is accounted, not dropped" as *u8, rem[0], 1)
65
66 // ---- X3: THE SOTA PROPERTY. reconstruct the source EXACTLY from converted + remainder ----
67 let b: i64 = fx_convert(100, 1, 3, rem)
68 fg_ck(cnt, "X3 reconstruct(33, rem=1, 1/3) == original 100 (no value lost)" as *u8,
69 fx_reconstruct(b, rem[0], 1, 3), 100)
70
71 // ---- X4: reconstruction holds for a messy rate and a messy amount ----
72 let b2: i64 = fx_convert(987654, 1732, 1000, rem) // ~1.732 rate
73 fg_ck(cnt, "X4 messy conversion reconstructs exactly" as *u8,
74 fx_reconstruct(b2, rem[0], 1732, 1000), 987654)
75
76 // ---- X5: FAIL-CLOSED on a zero denominator (no divide-by-zero, no NaN) ----
77 fg_ck(cnt, "X5 zero-denominator rate REFUSED (-1)" as *u8, fx_convert(10000, 85, 0, rem), FX_BAD_RATE)
78 fg_ck(cnt, "X5a and remainder cleared to 0 on refusal" as *u8, rem[0], 0)
79
80 // ---- X6: PROVENANCE round-trip -- a stored, sourced rate loads back exactly ----
81 let pair: *u8 = sys_mmap(64)
82 fg_id("USD-EUR-" as *u8, nonce, pair)
83 fx_rate_put(pfx, pair, 85, 100, "ECB-2026-07-24" as *u8)
84 let num: *i64 = sys_mmap(16) as *i64
85 let den: *i64 = sys_mmap(16) as *i64
86 fg_ck(cnt, "X6 stored rate loads (1=found)" as *u8, fx_rate_get(pfx, pair, num, den), 1)
87 fg_ck(cnt, "X6a rate numerator round-trips" as *u8, num[0], 85)
88 fg_ck(cnt, "X6b rate denominator round-trips" as *u8, den[0], 100)
89
90 // ---- X7: provenance-gated conversion uses the stored rate ----
91 fg_ck(cnt, "X7 priced conversion uses the cited rate: $250.00 -> 21250" as *u8,
92 fx_convert_priced(pfx, pair, 25000, rem), 21250)
93
94 // ---- X8: NO CONVERSION WITHOUT A CITED RATE -- an unpriced pair refuses ----
95 let unpriced: *u8 = sys_mmap(64)
96 fg_id("XYZ-QQQ-" as *u8, nonce, unpriced)
97 fg_ck(cnt, "X8 unpriced pair REFUSES (no cited rate, no conversion)" as *u8,
98 fx_convert_priced(pfx, unpriced, 10000, rem), FX_BAD_RATE)
99
100 // ---- X9: value conservation across a ROUND TRIP through a stored rate + its inverse remainder ----
101 // convert then reconstruct via the same stored rate
102 let conv: i64 = fx_convert_priced(pfx, pair, 33333, rem)
103 fg_ck(cnt, "X9 priced round-trip reconstructs the source exactly" as *u8,
104 fx_reconstruct(conv, rem[0], 85, 100), 33333)
105
106 fg_puts("nx_fx_gate: pass=" as *u8); fg_putn(cnt[0])
107 fg_puts(" fail=" as *u8); fg_putn(cnt[1]); fg_puts("\n" as *u8)
108 if cnt[1] == 0 {
109 fg_puts("F984 nx_fx: VERDICT=GREEN (exact conversion, remainder accounted, source reconstructs, provenance-gated)\n" as *u8)
110 sys_exit(0)
111 return 0
112 }
113 fg_puts("F984 nx_fx: VERDICT=RED\n" as *u8)
114 sys_exit(1)
115 return 1
116}