nx_logadd_gate.nx source
↩ module page · 84 lines · 6064 B
1// nx_logadd_gate.nx -- GATE for the fixed-point log-domain library (nx_logadd_lib), driven IN-PROCESS with no fixture:
2// its subject is arithmetic, so every tooth is a known-answer test against values derived by hand from ln 2, e and
3// ln 3 (S = 1024 units per nat), plus the structural laws a log-sum-exp must obey (identity with minus infinity,
4// symmetry, bounds, monotone tables, a three-way partition that sums to one, determinism across two inits) and one
5// neg-control (a positive argument to the probability reader is clamped AND counted, never silently accepted).
6// license_tier: ORIGINAL No hw writes (Rule 26).
7import "nx_syscalls.nx"
8import "nx_logadd_lib.nx"
9import "nx_gate_verdict.nx"
10
11const G_LN2_Q10: i64 = 710 // 1024 * ln 2 = 709.78
12const G_LN3_Q10: i64 = 1125 // 1024 * ln 3 = 1125.03
13const G_SOFTPLUS_1: i64 = 321 // 1024 * ln(1 + e^-1) = 320.78
14const G_INV_E_Q10: i64 = 377 // 1024 / e = 376.71
15const G_INV_E2_Q10: i64 = 139 // 1024 / e^2 = 138.58
16const G_TOL: i64 = 1 // one Q10 unit: the table's own quantisation
17const G_TOL_SUM: i64 = 3 // a three-way partition may lose one unit per rounding
18const G_THIRD_Q10: i64 = 341 // 1024 / 3 = 341.33
19const G_FAR: i64 = 0 - 20000 // well past the horizon
20const G_EXP_UNIT_Q30: i64 = 1072693760 // 2^30 * e^(-1/1024) = 1,072,693,759.83
21
22func main() -> i64 {
23 gv_head("=== nx_logadd_gate -- fixed-point log-sum-exp and exp against hand-derived known answers ===" as *u8)
24 let c: *i64 = gv_ctr()
25 gv_check_eq("init-returns-one" as *u8, la_init(), 1, c)
26 gv_check_eq("taylor-constant-e^(-1/S)-in-Q30-matches-the-hand-value" as *u8, la_exp_unit_q30(), G_EXP_UNIT_Q30, c)
27 let h: i64 = la_horizon()
28 gv_check("horizon-is-derived-inside-the-table (0 < h < cap)" as *u8, ((h > 0) & (h < LA_TABLE_CAP)) as i64, c)
29 // known answers
30 gv_check_near("lse(0,0) = S*ln2" as *u8, la_lse(0, 0), G_LN2_Q10, G_TOL, c)
31 gv_check_near("lse(S,0) = S + S*ln(1+e^-1)" as *u8, la_lse(LA_S, 0), LA_S + G_SOFTPLUS_1, G_TOL, c)
32 gv_check_eq("lse(x,-inf) = x" as *u8, la_lse(4321, LA_NEG_INF), 4321, c)
33 gv_check_eq("lse(-inf,x) = x" as *u8, la_lse(LA_NEG_INF, 0 - 77), 0 - 77, c)
34 gv_check_eq("lse(-inf,-inf) = -inf" as *u8, la_lse(LA_NEG_INF, LA_NEG_INF), LA_NEG_INF, c)
35 gv_check_eq("lse-is-symmetric" as *u8, la_lse(300, 0 - 1200), la_lse(0 - 1200, 300), c)
36 gv_check("lse-bounded-below-by-the-max-and-above-by-max-plus-ln2" as *u8, ((la_lse(500, 400) >= 500) & (la_lse(500, 400) <= 500 + G_LN2_Q10)) as i64, c)
37 gv_check_eq("lse-past-the-horizon-returns-the-max-exactly" as *u8, la_lse(0, 0 - h), 0, c)
38 gv_check("lse-just-inside-the-horizon-adds-at-least-one-unit" as *u8, (la_lse(0, 1 - h) >= 1) as i64, c)
39 gv_check_eq("exp_neg(0) = S" as *u8, la_exp_neg(0), LA_S, c)
40 gv_check_near("exp_neg(-S*ln2) = S/2" as *u8, la_exp_neg(0 - G_LN2_Q10), LA_S / 2, G_TOL, c)
41 gv_check_near("exp_neg(-S) = S/e" as *u8, la_exp_neg(0 - LA_S), G_INV_E_Q10, G_TOL, c)
42 gv_check_near("exp_neg(-2S) = S/e^2" as *u8, la_exp_neg(0 - 2 * LA_S), G_INV_E2_Q10, G_TOL, c)
43 gv_check_eq("exp_neg-far-below-the-table-is-zero" as *u8, la_exp_neg(G_FAR), 0, c)
44 gv_check_eq("exp_neg_q30(0) = Q30" as *u8, la_exp_neg_q30(0), LA_Q30, c)
45 // a three-way partition: three equal scores normalise to a third each and sum to one
46 let z: i64 = la_lse(la_lse(0, 0), 0)
47 gv_check_near("three-equal-scores-partition-is-S*ln3" as *u8, z, G_LN3_Q10, G_TOL, c)
48 let p: i64 = la_exp_neg(0 - z)
49 gv_check_near("each-share-is-a-third" as *u8, p, G_THIRD_Q10, G_TOL, c)
50 gv_check_near("the-three-shares-sum-to-one" as *u8, 3 * p, LA_S, G_TOL_SUM, c)
51 // associativity within rounding: (a+b)+c vs a+(b+c)
52 let l1: i64 = la_lse(la_lse(2000, 0 - 500), 900)
53 let l2: i64 = la_lse(2000, la_lse(0 - 500, 900))
54 gv_check_near("lse-is-associative-within-rounding" as *u8, l1, l2, G_TOL_SUM, c)
55 // table monotonicity over the WHOLE table (a bound tied to its denominator: every entry examined)
56 var mono_exp: i64 = 1
57 var mono_sp: i64 = 1
58 var examined: i64 = 0
59 var d: i64 = 1
60 while d < LA_TABLE_CAP {
61 if la_exp_neg_q30(0 - d) > la_exp_neg_q30(1 - d) { mono_exp = 0 }
62 if la_lse(0, 0 - d) > la_lse(0, 1 - d) { mono_sp = 0 }
63 examined = examined + 1
64 d = d + 1
65 }
66 gv_check_eq("every-table-entry-examined" as *u8, examined, LA_TABLE_CAP - 1, c)
67 gv_check_eq("exp-table-is-non-increasing-over-the-whole-table" as *u8, mono_exp, 1, c)
68 gv_check_eq("softplus-table-is-non-increasing-over-the-whole-table" as *u8, mono_sp, 1, c)
69 // neg-control: a positive argument (a caller's rounding drift) clamps to S and is COUNTED
70 let before: i64 = la_clamp_count()
71 gv_check_eq("neg-control-exp_neg-of-a-positive-clamps-to-S" as *u8, la_exp_neg(5), LA_S, c)
72 gv_check_eq("neg-control-the-clamp-is-counted-not-hidden" as *u8, la_clamp_count(), before + 1, c)
73 // determinism: a second init is a no-op and the values agree
74 gv_check_eq("second-init-is-idempotent" as *u8, la_init(), 1, c)
75 gv_check_eq("values-agree-after-the-second-init" as *u8, la_lse(LA_S, 0), LA_S + la_lse(0, 0 - LA_S), c)
76 gv_values_head()
77 gv_kv("horizon" as *u8, h)
78 gv_kv("exp_unit_q30" as *u8, la_exp_unit_q30())
79 gv_kv("lse_0_0" as *u8, la_lse(0, 0))
80 gv_kv("ln3_q10" as *u8, z)
81 gv_kv("third_q10" as *u8, p)
82 gv_kv("exp_neg_minus_s" as *u8, la_exp_neg(0 - LA_S))
83 return gv_verdict("nx_logadd_gate" as *u8, c, "the fixed-point log-domain library proven against hand-derived known answers (ln 2, ln 3, softplus(1), 1/e, 1/e^2, the Taylor constant) and the laws a log-sum-exp must obey: identity with minus infinity, symmetry, max-plus-ln2 bounds, a derived horizon past which it returns the max exactly, whole-table monotonicity, a three-way partition summing to one, associativity within rounding, an idempotent init; a positive argument to the probability reader clamps and is counted" as *u8)
84}