nx_assets_gate.nx source

1// nx_assets_gate.nx -- GATE for the foreign-asset reader (nx_assets_lib), driven IN-PROCESS on planted rows: a clean 2// run-path row, a candidate with unmeasured bytes, an oracle and an unavailable row with no lift, a run-path asset 3// with NO replacement rung (the defect this ledger exists to expose), a rung the plan does not declare, a lift 4// whose P10 exceeds its P50, a priced row with no lift, a cross-board rung, an unknown kind, an unknown state and a 5// short row; both partitions sum to the rows, the run-path bytes and the three-point aggregates are exact, and the 6// NORUNG detector is bite-proven against an oracle row that legitimately has none. 7// license_tier: ORIGINAL No hw writes (Rule 26). 8import "nx_syscalls.nx" 9import "nx_costest_lib.nx" 10import "nx_assets_lib.nx" 11import "nx_gate_verdict.nx" 12 13const G_I64: i64 = 8 14const G_FX: *u8 = "# planted assets\nasset|a1|runpath|weights|MiniLM|apache-2.0|90870598|runtime/x.nx:f|R1|6|9|16|components|note\nasset|a2|candidate|weights|Diver|apache-2.0|-|none|R2|2|4|8|b|n\nasset|a3|oracle|dataset|BRIGHT|cc-by-4.0|465489179|harness|-|-|-|-|b|n\nasset|a4|unavailable|weights|MQR-A1|apache-2.0|0|none|-|-|-|-|b|n\nasset|a5|runpath|font|Liberation|OFL|410712|renderer|-|1|2|3|b|n\nasset|a6|runpath|weights|X|lic|1|used|R9|1|2|3|b|n\nasset|a7|candidate|weights|Y|lic|1|used|R1|5|3|9|b|n\nasset|a8|candidate|weights|Z|lic|1|used|R1|-|-|-|b|n\nasset|a9|runpath|weights|W|lic|1|used|llm:LM9|1|2|3|b|n\nasset|a10|runpath|gizmo|V|lic|1|used|R1|1|2|3|b|n\nasset|a11|maybe|weights|U|lic|1|used|R1|1|2|3|b|n\nasset|a12|runpath|weights|T|lic|1|used|R1|1|2\n" 15const G_PLAN: *u8 = "rung|R1|one|s1|d|Organ|1|-\nrung|R2|two|s2|d|Organ|2|R1\n" 16const G_CLEAN: *u8 = "asset|a1|runpath|weights|MiniLM|apache-2.0|90870598|runtime/x.nx:f|R1|6|9|16|components|note\nasset|a3|oracle|dataset|BRIGHT|cc-by-4.0|465489179|harness|-|-|-|-|b|n\n" 17const G_ROWS: i64 = 12 18const G_RUNPATH: i64 = 6 19const G_CANDIDATE: i64 = 3 20const G_ORACLE: i64 = 1 21const G_UNAVAIL: i64 = 1 22const G_BADSTATE: i64 = 1 23const G_OK: i64 = 5 24const G_DEFECTS: i64 = 7 25const G_XBOARD: i64 = 1 26const G_MISSING: i64 = 1 27const G_RP_BYTES: i64 = 91281314 28const G_RP_PRICED: i64 = 5 29const G_RP_P10: i64 = 134 // 170 - isqrt(30*30 + 4*10*10) 30const G_RP_P50: i64 = 170 31const G_RP_P90: i64 = 242 // 170 + isqrt(70*70 + 4*10*10) 32const G_RP_SUM10: i64 = 100 33const G_RP_SUM90: i64 = 280 34const G_CA_PRICED: i64 = 1 35const G_CA_P50: i64 = 40 36const G_ROW_A5: i64 = 4 // a5 is the fifth asset row (0-based 4) 37const G_ROW_A3: i64 = 2 38 39func g_lit(s: *u8, dst: *u8) -> i64 { 40 let n: i64 = ces_slen(s) 41 var i: i64 = 0 42 while i < n { dst[i] = s[i]; i = i + 1 } 43 dst[n] = 0 as u8 44 return n 45} 46 47func main(argc: i64, argv: *i64) -> i64 { 48 let c: *i64 = gv_ctr() 49 gv_head("nx_assets_gate -- the foreign-asset reader: states, kinds, lifts, rungs, partitions and aggregates on planted rows" as *u8) 50 let buf: *u8 = sys_mmap(ces_slen(G_FX) + 1) 51 let n: i64 = g_lit(G_FX, buf) 52 let plan: *u8 = sys_mmap(ces_slen(G_PLAN) + 1) 53 let pn: i64 = g_lit(G_PLAN, plan) 54 let cap: i64 = fas_cap(n) 55 gv_check("fixture-reached-the-condition: the capacity derived from the bytes holds the twelve rows" as *u8, (cap >= G_ROWS) as i64, c) 56 let tab: *i64 = sys_mmap(cap * FAS_STRIDE * G_I64) as *i64 57 let rows: i64 = fas_load(buf, n, tab, cap) 58 gv_check_eq("rows-parsed-twelve (the header comment is not a row)" as *u8, rows, G_ROWS, c) 59 let missing: i64 = fas_judge_rungs(tab, rows, buf, plan, pn) 60 gv_check_eq("rung-absent-from-the-plan-counted-once" as *u8, missing, G_MISSING, c) 61 let t: *i64 = sys_mmap(FAS_T_SLOTS * G_I64) as *i64 62 fas_totals(tab, rows, t) 63 gv_check_eq("state-runpath" as *u8, t[FAS_T_ST0 + FAS_ST_RUNPATH], G_RUNPATH, c) 64 gv_check_eq("state-candidate" as *u8, t[FAS_T_ST0 + FAS_ST_CANDIDATE], G_CANDIDATE, c) 65 gv_check_eq("state-oracle" as *u8, t[FAS_T_ST0 + FAS_ST_ORACLE], G_ORACLE, c) 66 gv_check_eq("state-unavailable" as *u8, t[FAS_T_ST0 + FAS_ST_UNAVAILABLE], G_UNAVAIL, c) 67 gv_check_eq("state-bad" as *u8, t[FAS_T_ST0 + FAS_ST_BAD], G_BADSTATE, c) 68 gv_check_eq("state-partition-sums-to-rows" as *u8, fas_state_sum(t), rows, c) 69 gv_check_eq("verdict-ok-five" as *u8, t[FAS_T_V0 + FAS_V_OK], G_OK, c) 70 gv_check_eq("verdict-fields-one (the short row)" as *u8, t[FAS_T_V0 + FAS_V_FIELDS], 1, c) 71 gv_check_eq("verdict-badstate-one" as *u8, t[FAS_T_V0 + FAS_V_BADSTATE], 1, c) 72 gv_check_eq("verdict-badkind-one" as *u8, t[FAS_T_V0 + FAS_V_BADKIND], 1, c) 73 gv_check_eq("verdict-badlift-one (P10 above P50)" as *u8, t[FAS_T_V0 + FAS_V_BADLIFT], 1, c) 74 gv_check_eq("verdict-lift-missing-one (a priced row with dashes)" as *u8, t[FAS_T_V0 + FAS_V_LIFTMISSING], 1, c) 75 gv_check_eq("verdict-norung-one (a run-path asset with no path to replacing it)" as *u8, t[FAS_T_V0 + FAS_V_NORUNG], 1, c) 76 gv_check_eq("verdict-badrung-one (a rung the plan never declared)" as *u8, t[FAS_T_V0 + FAS_V_BADRUNG], 1, c) 77 gv_check_eq("verdict-partition-sums-to-rows" as *u8, fas_verdict_sum(t), rows, c) 78 gv_check_eq("defects-seven" as *u8, t[FAS_T_DEFECTS], G_DEFECTS, c) 79 gv_check_eq("cross-board-rung-counted-not-judged" as *u8, t[FAS_T_XBOARD], G_XBOARD, c) 80 gv_check_eq("runpath-bytes-sum-of-measured-sizes" as *u8, t[FAS_T_RP_BYTES], G_RP_BYTES, c) 81 gv_check_eq("runpath-bytes-unknown-zero (the unmeasured row is a candidate)" as *u8, t[FAS_T_RP_UNKNOWN], 0, c) 82 gv_check_eq("runpath-priced-rows-five (the short row carries no P90)" as *u8, t[FAS_T_RP_PRICED], G_RP_PRICED, c) 83 gv_check_eq("runpath-lift-p50-sum-of-medians" as *u8, t[FAS_T_RP_AGG + CES_A_P50], G_RP_P50, c) 84 gv_check_eq("runpath-lift-p10-rss-band" as *u8, t[FAS_T_RP_AGG + CES_A_P10], G_RP_P10, c) 85 gv_check_eq("runpath-lift-p90-rss-band" as *u8, t[FAS_T_RP_AGG + CES_A_P90], G_RP_P90, c) 86 gv_check_eq("runpath-lift-correlated-sum10" as *u8, t[FAS_T_RP_AGG + CES_A_SUM10], G_RP_SUM10, c) 87 gv_check_eq("runpath-lift-correlated-sum90" as *u8, t[FAS_T_RP_AGG + CES_A_SUM90], G_RP_SUM90, c) 88 gv_check_eq("candidate-priced-rows-one (the badlift and the missing lift are excluded)" as *u8, t[FAS_T_CA_PRICED], G_CA_PRICED, c) 89 gv_check_eq("candidate-lift-p50" as *u8, t[FAS_T_CA_AGG + CES_A_P50], G_CA_P50, c) 90 // the NORUNG detector: fires on the run-path font with no rung, silent on the oracle with none 91 let bad: i64 = (tab[G_ROW_A5 * FAS_STRIDE + FAS_VERDICT] == FAS_V_NORUNG) as i64 92 let good: i64 = (tab[G_ROW_A3 * FAS_STRIDE + FAS_VERDICT] == FAS_V_NORUNG) as i64 93 gv_bite("neg-control-norung-fires-on-the-runpath-row-and-not-on-the-oracle-row" as *u8, bad, good, c) 94 gv_check_eq("a5-rung-state-none" as *u8, tab[G_ROW_A5 * FAS_STRIDE + FAS_RUNGST], FAS_R_NONE, c) 95 gv_check_eq("a2-bytes-unmeasured-is-NONE-not-zero" as *u8, tab[1 * FAS_STRIDE + FAS_BYTES], CES_NONE, c) 96 gv_check_eq("a4-bytes-zero-is-a-measurement" as *u8, tab[3 * FAS_STRIDE + FAS_BYTES], 0, c) 97 // a clean file has no defects 98 let cb: *u8 = sys_mmap(ces_slen(G_CLEAN) + 1) 99 let cn: i64 = g_lit(G_CLEAN, cb) 100 let ctab: *i64 = sys_mmap(fas_cap(cn) * FAS_STRIDE * G_I64) as *i64 101 let crows: i64 = fas_load(cb, cn, ctab, fas_cap(cn)) 102 fas_judge_rungs(ctab, crows, cb, plan, pn) 103 let ct: *i64 = sys_mmap(FAS_T_SLOTS * G_I64) as *i64 104 fas_totals(ctab, crows, ct) 105 gv_check_eq("neg-control-clean-file-two-rows" as *u8, crows, 2, c) 106 gv_check_eq("neg-control-clean-file-zero-defects" as *u8, ct[FAS_T_DEFECTS], 0, c) 107 gv_values_head() 108 gv_kv("rows" as *u8, rows) 109 gv_kv("defects" as *u8, t[FAS_T_DEFECTS]) 110 gv_kv("runpath_bytes" as *u8, t[FAS_T_RP_BYTES]) 111 gv_kv("runpath_lift_p10_deciu" as *u8, t[FAS_T_RP_AGG + CES_A_P10]) 112 gv_kv("runpath_lift_p50_deciu" as *u8, t[FAS_T_RP_AGG + CES_A_P50]) 113 gv_kv("runpath_lift_p90_deciu" as *u8, t[FAS_T_RP_AGG + CES_A_P90]) 114 gv_kv("runpath_lift_sum90_deciu" as *u8, t[FAS_T_RP_AGG + CES_A_SUM90]) 115 return gv_verdict("nx_assets_gate" as *u8, c, "the foreign-asset reader proven on planted rows: every state and kind is classified, a lift is refused when malformed or inverted and named missing when a priced row carries none, a run-path asset with no replacement rung is a NORUNG defect while an oracle without one is not (bite-proven), a rung the plan never declared is BADRUNG, a cross-board rung is counted and not judged here, both partitions sum to the rows, the run-path bytes are the sum of measured sizes with unmeasured counted apart, and the three-point aggregates match the hand-derived band inside the correlated sum" as *u8) 116}