nx_ecomat_trend_gate.nx source

1// nx_ecomat_trend_gate.nx -- executable proof for the advancement/expansion decomposition. 2// 3// NON-VACUITY IS THE POINT. T7 and T8 run the SAME code path over two fixtures that differ only in 4// whether the domain count moved. If the instrument were stuck reporting RISING (the flattering 5// answer) T8 fails; if it were stuck reporting FLAT, T7 fails. A gauge that cannot return both 6// answers is not measuring anything, so the pair is the neg-control, not decoration. 7// 8// Fixtures are in-memory string literals: the core is pure, so this gate touches no filesystem and 9// cannot pass by reading a stale artifact it wrote itself. 10// Inherits the nx_gate_verdict base class (D001 DRY: gv_ctr/gv_head/gv_check/gv_verdict). 11// license_tier: ORIGINAL No hw writes (Rule 26). 12import "nx_ecomat_trend_lib.nx" 13import "nx_gate_verdict.nx" 14 15func tg_eq(a: i64, b: i64) -> i64 { if a == b { return 1 } return 0 } 16 17func main(argc: i64, argv: *i64) -> i64 { 18 let ctr: *i64 = gv_ctr() 19 gv_head("nx_ecomat_trend -- advancement (real rungs) vs expansion (new declarations)" as *u8) 20 21 let out: *i64 = sys_mmap(TR_OUT_SLOTS * TR_I64) as *i64 22 23 let one: *u8 = "ECOMAT epoch=100 domains=5 overall_permil=400 sum_cur=20 sum_bar=50 verdict=GREEN\n" as *u8 24 let one_n: i64 = el_len(one) 25 gv_check("T1 tr_field reads a mid-line field" as *u8, tg_eq(tr_field(one, 0, one_n, "sum_cur=" as *u8), 20), ctr) 26 gv_check("T2 tr_field returns -1 for an absent field" as *u8, tg_eq(tr_field(one, 0, one_n, "autonomy_permil=" as *u8), 0 - 1), ctr) 27 gv_check("T3 tr_field does not confuse a prefix-sharing field" as *u8, tg_eq(tr_field(one, 0, one_n, "overall_permil=" as *u8), 400), ctr) 28 29 let two: *u8 = "ECOMAT epoch=100 domains=5 src=beat verdict=GREEN\nECOMAT epoch=200 domains=5 sum_cur=23 sum_bar=50 verdict=GREEN\n" as *u8 30 var l1end: i64 = 0 31 while (two[l1end] as i64) != TR_NL { l1end = l1end + 1 } 32 gv_check("T4 tr_field is line-scoped (cannot read the next row's value)" as *u8, tg_eq(tr_field(two, 0, l1end, "sum_cur=" as *u8), 0 - 1), ctr) 33 34 gv_check("T5 empty ledger REFUSES (no-log, not a silent zero)" as *u8, tg_eq(em_trend_buf(one, 0, out), TR_ERR_NOLOG), ctr) 35 gv_check("T6 single row REFUSES (nothing to difference)" as *u8, tg_eq(em_trend_buf(one, one_n, out), TR_ERR_THIN), ctr) 36 37 let rise: *u8 = "ECOMAT epoch=100 domains=5 overall_permil=400 sum_cur=20 sum_bar=50 verdict=GREEN\nECOMAT epoch=200 domains=5 overall_permil=460 sum_cur=23 sum_bar=50 verdict=GREEN\n" as *u8 38 let rc_r: i64 = em_trend_buf(rise, el_len(rise), out) 39 var t7: i64 = 0 40 if rc_r == 0 { if tg_eq(out[TRO_ADVANCE], 3) == 1 { if tg_eq(tr_finding(out), TR_RISING) == 1 { t7 = 1 } } } 41 gv_check("T7 stable cohort + climbing numerator => finding=RISING, advance=3 EXACT" as *u8, t7, ctr) 42 43 let flat: *u8 = "ECOMAT epoch=100 domains=5 overall_permil=400 sum_cur=20 sum_bar=50 verdict=GREEN\nECOMAT epoch=150 domains=5 overall_permil=400 sum_cur=20 sum_bar=50 verdict=GREEN\nECOMAT epoch=200 domains=6 overall_permil=366 sum_cur=22 sum_bar=60 verdict=GREEN\n" as *u8 44 let rc_f: i64 = em_trend_buf(flat, el_len(flat), out) 45 var t8: i64 = 0 46 if rc_f == 0 { if tg_eq(out[TRO_ADVANCE], 0) == 1 { if tg_eq(tr_finding(out), TR_FLAT) == 1 { t8 = 1 } } } 47 gv_check("T8 NEG-CONTROL expansion-only => finding=FLAT, advance=0 (gauge can return the unflattering answer)" as *u8, t8, ctr) 48 49 var t9: i64 = 0 50 if out[TRO_LAST_PERMIL] < out[TRO_FIRST_PERMIL] { if out[TRO_LAST_CUR] > out[TRO_FIRST_CUR] { t9 = 1 } } 51 gv_check("T9 headline FALLS while levels earned RISE (the dilution defect, reproduced)" as *u8, t9, ctr) 52 gv_check("T10 expansion bar attributed to the new domain (+10)" as *u8, tg_eq(out[TRO_EXPAND_BAR], 10), ctr) 53 gv_check("T11 unattributable movement is declared AMBIGUOUS, not folded into advancement" as *u8, tg_eq(out[TRO_AMBIG_CUR], 2), ctr) 54 var t12: i64 = 0 55 if out[TRO_DECOMP_PERMIL] < TR_PERMIL { t12 = 1 } 56 gv_check("T12 decomposable coverage reported BELOW 1000 when attribution is incomplete" as *u8, t12, ctr) 57 58 let beat: *u8 = "ECOMAT epoch=100 domains=5 overall_permil=400 sum_cur=20 sum_bar=50 verdict=GREEN\nECOMAT epoch=150 domains=5 overall_permil=400 autonomy_permil=328 src=beat verdict=GREEN\nECOMAT epoch=200 domains=5 overall_permil=460 sum_cur=23 sum_bar=50 verdict=GREEN\n" as *u8 59 let rc_b: i64 = em_trend_buf(beat, el_len(beat), out) 60 var t13: i64 = 0 61 if rc_b == 0 { if tg_eq(out[TRO_ROWS], 2) == 1 { if tg_eq(out[TRO_SCANNED], 3) == 1 { if tg_eq(out[TRO_ADVANCE], 3) == 1 { t13 = 1 } } } } 62 gv_check("T13 cadence src=beat rows are skipped, not scored as a regression to zero" as *u8, t13, ctr) 63 64 let fall: *u8 = "ECOMAT epoch=100 domains=5 overall_permil=400 sum_cur=20 sum_bar=50 verdict=GREEN\nECOMAT epoch=200 domains=5 overall_permil=360 sum_cur=18 sum_bar=50 verdict=GREEN\n" as *u8 65 let rc_d: i64 = em_trend_buf(fall, el_len(fall), out) 66 var t14: i64 = 0 67 if rc_d == 0 { if tg_eq(out[TRO_ADVANCE], 0 - 2) == 1 { if tg_eq(tr_finding(out), TR_FALLING) == 1 { t14 = 1 } } } 68 gv_check("T14 a real regression reports FALLING with a signed advance (-2)" as *u8, t14, ctr) 69 70 let grow: *u8 = "ECOMAT epoch=100 domains=5 overall_permil=400 sum_cur=20 sum_bar=50 verdict=GREEN\nECOMAT epoch=200 domains=6 overall_permil=366 sum_cur=22 sum_bar=60 verdict=GREEN\n" as *u8 71 let rc_g: i64 = em_trend_buf(grow, el_len(grow), out) 72 var t15: i64 = 0 73 if rc_g == 0 { if tg_eq(out[TRO_STABLE_SPANS], 0) == 1 { if tg_eq(tr_finding(out), TR_UNDECIDABLE) == 1 { t15 = 1 } } } 74 gv_check("T15 zero stable spans => UNDECIDABLE (refuses to call it FLAT on no evidence)" as *u8, t15, ctr) 75 76 let rc: i64 = gv_verdict("ECOMAT-TREND-GATE" as *u8, ctr, "advancement separated from expansion; neg-control proves both answers reachable" as *u8) 77 sys_exit(rc) 78 return rc 79}