nx_fx_gate.nx source
↩ module page · 109 lines · 5060 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 let pfx: *u8 = "knowledge/store/fxgate-" as *u8
43 let nonce: i64 = sys_now_us()
44 let cnt: *i64 = sys_mmap(16) as *i64
45 cnt[0] = 0
46 cnt[1] = 0
47 let rem: *i64 = sys_mmap(16) as *i64
48
49 fg_puts("NISHI-FX-GATE (F984 exact multi-currency: conversion loses no value)\n" as *u8)
50
51 // ---- X1: clean conversion. $100.00 (10000c) at 0.85 EUR/USD (rate 85/100) -> 8500c, remainder 0 ----
52 fg_ck(cnt, "X1 $100.00 at 0.85 -> 8500 minor units" as *u8, fx_convert(10000, 85, 100, rem), 8500)
53 fg_ck(cnt, "X1a exact, zero remainder" as *u8, rem[0], 0)
54
55 // ---- X2: a conversion WITH a remainder -- 100 at 1/3 -> 33, remainder 1 (NOT silently dropped) ----
56 fg_ck(cnt, "X2 100 at 1/3 -> 33 minor units" as *u8, fx_convert(100, 1, 3, rem), 33)
57 fg_ck(cnt, "X2a remainder = 1 is accounted, not dropped" as *u8, rem[0], 1)
58
59 // ---- X3: THE SOTA PROPERTY. reconstruct the source EXACTLY from converted + remainder ----
60 let b: i64 = fx_convert(100, 1, 3, rem)
61 fg_ck(cnt, "X3 reconstruct(33, rem=1, 1/3) == original 100 (no value lost)" as *u8,
62 fx_reconstruct(b, rem[0], 1, 3), 100)
63
64 // ---- X4: reconstruction holds for a messy rate and a messy amount ----
65 let b2: i64 = fx_convert(987654, 1732, 1000, rem) // ~1.732 rate
66 fg_ck(cnt, "X4 messy conversion reconstructs exactly" as *u8,
67 fx_reconstruct(b2, rem[0], 1732, 1000), 987654)
68
69 // ---- X5: FAIL-CLOSED on a zero denominator (no divide-by-zero, no NaN) ----
70 fg_ck(cnt, "X5 zero-denominator rate REFUSED (-1)" as *u8, fx_convert(10000, 85, 0, rem), FX_BAD_RATE)
71 fg_ck(cnt, "X5a and remainder cleared to 0 on refusal" as *u8, rem[0], 0)
72
73 // ---- X6: PROVENANCE round-trip -- a stored, sourced rate loads back exactly ----
74 let pair: *u8 = sys_mmap(64)
75 fg_id("USD-EUR-" as *u8, nonce, pair)
76 fx_rate_put(pfx, pair, 85, 100, "ECB-2026-07-24" as *u8)
77 let num: *i64 = sys_mmap(16) as *i64
78 let den: *i64 = sys_mmap(16) as *i64
79 fg_ck(cnt, "X6 stored rate loads (1=found)" as *u8, fx_rate_get(pfx, pair, num, den), 1)
80 fg_ck(cnt, "X6a rate numerator round-trips" as *u8, num[0], 85)
81 fg_ck(cnt, "X6b rate denominator round-trips" as *u8, den[0], 100)
82
83 // ---- X7: provenance-gated conversion uses the stored rate ----
84 fg_ck(cnt, "X7 priced conversion uses the cited rate: $250.00 -> 21250" as *u8,
85 fx_convert_priced(pfx, pair, 25000, rem), 21250)
86
87 // ---- X8: NO CONVERSION WITHOUT A CITED RATE -- an unpriced pair refuses ----
88 let unpriced: *u8 = sys_mmap(64)
89 fg_id("XYZ-QQQ-" as *u8, nonce, unpriced)
90 fg_ck(cnt, "X8 unpriced pair REFUSES (no cited rate, no conversion)" as *u8,
91 fx_convert_priced(pfx, unpriced, 10000, rem), FX_BAD_RATE)
92
93 // ---- X9: value conservation across a ROUND TRIP through a stored rate + its inverse remainder ----
94 // convert then reconstruct via the same stored rate
95 let conv: i64 = fx_convert_priced(pfx, pair, 33333, rem)
96 fg_ck(cnt, "X9 priced round-trip reconstructs the source exactly" as *u8,
97 fx_reconstruct(conv, rem[0], 85, 100), 33333)
98
99 fg_puts("nx_fx_gate: pass=" as *u8); fg_putn(cnt[0])
100 fg_puts(" fail=" as *u8); fg_putn(cnt[1]); fg_puts("\n" as *u8)
101 if cnt[1] == 0 {
102 fg_puts("F984 nx_fx: VERDICT=GREEN (exact conversion, remainder accounted, source reconstructs, provenance-gated)\n" as *u8)
103 sys_exit(0)
104 return 0
105 }
106 fg_puts("F984 nx_fx: VERDICT=RED\n" as *u8)
107 sys_exit(1)
108 return 1
109}