nx_langspec_gate.nx source

1// nx_langspec_gate.nx -- THE REFEREE for lang.plan rung LR5 (written specification plus conformance 2// suite, watch symbol spec_conformance_run). 3// 4// THE ROW NAMES ONE TOOTH AND THIS GATE IS BUILT AROUND IT: "a planted deviation goes RED". A 5// conformance runner that cannot fail is a certification costume, so the load-bearing question is not 6// whether the suite passes -- it is whether the runner would NOTICE if the compiler stopped obeying 7// the specification. That is asserted here by PLANTING a divergence between a written clause and the 8// shipped compiler and requiring the runner to report DEVIATION and name the case. 9// 10// FIXTURES ARE ASSEMBLED AT RUNTIME into /tmp/nx_langspec_gate/, never committed beside the organ: 11// a gate that shares a fixture with a production beat measures the fixture, and a detector that scans 12// source finds its own fixture. The fixture spec, its three suites and its OWN conf are written here 13// by this gate on every run, so the gate carries its own thresholds and never has to lower the live 14// coverage ratchet to make its fixtures pass -- lowering the production floor to fit a test is 15// editing the detector to flatter the measurement. 16// 17// WHY A SEPARATE CONF FIXTURE MATTERS. The production ratchet stands at full coverage. A fixture spec 18// deliberately carries one clause NO case exercises, because the unexercised list is the rung's real 19// deliverable and a list that is always empty cannot be shown to work. Its own conf sets a floor the 20// fixture meets, so the two facts stay independent. 21// 22// SUBJECT: the SHIPPED runner (nx_langspec.elf, resolved from the cwd or from _offc/), driving the 23// SHIPPED compiler. Nothing here simulates either. The absent-compiler control proves it: point the 24// runner at a compiler that does not exist and it must ABSTAIN, not acquit and not convict. 25// 26// exit: gv_verdict (0 GREEN / 1 RED / 3 SKIP). license_tier: ORIGINAL. No hw writes (Rule 26). 27import "nx_syscalls.nx" 28import "nx_gate_verdict.nx" 29import "nx_ccgate_lib.nx" 30 31const LG_DIR: *u8 = "/tmp/nx_langspec_gate\x00" 32const LG_CC: *u8 = "_offc/nx_cc_sovereign.elf\x00" 33const LG_CC_ABSENT: *u8 = "_offc/nx_cc_this_compiler_does_not_exist.elf\x00" 34const LG_PROD_SPEC: *u8 = "knowledge/specs/nishilang.spec\x00" 35const LG_PROD_SUITE: *u8 = "knowledge/specs/nishilang.suite\x00" 36const LG_PROD_CONF: *u8 = "knowledge/specs/nishilang_conformance.conf\x00" 37const LG_ARGV_SLOTS: i64 = 8 38const LG_EXIT_CONFORMANT: i64 = 0 39const LG_EXIT_DEVIATION: i64 = 1 40const LG_EXIT_UNOBSERVABLE: i64 = 3 41const LG_EXIT_EMPTY: i64 = 4 42 43func lg_have(p: *u8) -> i64 { 44 let fd: i64 = sys_openat_rd(p) 45 if fd < 0 { return 0 } 46 sys_close(fd) 47 return 1 48} 49 50func lg_put(path: *u8, body: *u8) -> i64 { 51 var n: i64 = 0 52 while body[n] != (0 as u8) { n = n + 1 } 53 let fd: i64 = sys_openat_wr(path, CCG_MODE_RW) 54 if fd < 0 { return 0 - 1 } 55 sys_write(fd, body, n) 56 sys_close(fd) 57 return 0 58} 59 60// Fork the shipped runner with the full argument vector and capture BOTH streams into one file. 61// Returns the runner's EXIT CODE -- which is the whole contract: a conformance runner whose verdict 62// is only readable in its prose cannot be consumed by anything. 63func lg_run(elf: *u8, verb: *u8, spec: *u8, suite: *u8, cc: *u8, conf: *u8, out: *u8) -> i64 { 64 let a: *i64 = sys_mmap(LG_ARGV_SLOTS * 8) as *i64 65 a[0] = elf as i64 66 a[1] = verb as i64 67 a[2] = spec as i64 68 a[3] = suite as i64 69 a[4] = cc as i64 70 a[5] = conf as i64 71 a[6] = 0 72 let ofd: i64 = sys_openat_wr(out, CCG_MODE_RW) 73 let st: i64 = ccg_run(elf, a, ofd, ofd) 74 sys_close(ofd) 75 return wait_status_rc(st) 76} 77 78func main(argc: i64, argv: *i64) -> i64 { 79 let ctr: *i64 = gv_ctr() 80 gv_head("=== nx_langspec_gate -- LR5 written specification plus conformance suite: the runner drives the SHIPPED compiler, a PLANTED deviation goes RED, an empty suite is not success, and every unexercised clause is counted AND named ===" as *u8) 81 82 // ---- subject resolution: I could not look is not it is broken ------------------------------- 83 var elf: *u8 = "nx_langspec.elf\x00" 84 if argc >= 2 { elf = argv[1] as *u8 } 85 if lg_have(elf) == 0 { elf = "_offc/nx_langspec.elf\x00" } 86 var have_runner: i64 = lg_have(elf) 87 if gv_need("the shipped conformance runner is present (nx_langspec.elf from this cwd or from _offc/)" as *u8, have_runner, ctr) == 0 { 88 return gv_verdict("LANGSPEC-LR5" as *u8, ctr, "subject absent" as *u8) 89 } 90 var have_cc: i64 = lg_have("buildroot/_offc/nx_cc_sovereign.elf\x00" as *u8) 91 if have_cc == 0 { have_cc = lg_have(LG_CC) } 92 if gv_need("the shipped sovereign compiler is present (the runner anchors into buildroot and forks it)" as *u8, have_cc, ctr) == 0 { 93 return gv_verdict("LANGSPEC-LR5" as *u8, ctr, "compiler absent" as *u8) 94 } 95 96 // ---- fixtures, assembled at RUNTIME --------------------------------------------------------- 97 sys_mkdir(LG_DIR, CCG_MODE_X) 98 let f_spec: *u8 = "/tmp/nx_langspec_gate/gx.spec\x00" 99 let f_conf: *u8 = "/tmp/nx_langspec_gate/gx.conf\x00" 100 let f_good: *u8 = "/tmp/nx_langspec_gate/gx_good.suite\x00" 101 let f_plant: *u8 = "/tmp/nx_langspec_gate/gx_planted.suite\x00" 102 let f_wrong: *u8 = "/tmp/nx_langspec_gate/gx_wrongreason.suite\x00" 103 let f_empty: *u8 = "/tmp/nx_langspec_gate/gx_empty.suite\x00" 104 let f_unres: *u8 = "/tmp/nx_langspec_gate/gx_unresolved.suite\x00" 105 let o_good: *u8 = "/tmp/nx_langspec_gate/o_good.txt\x00" 106 let o_plant: *u8 = "/tmp/nx_langspec_gate/o_planted.txt\x00" 107 let o_wrong: *u8 = "/tmp/nx_langspec_gate/o_wrong.txt\x00" 108 let o_empty: *u8 = "/tmp/nx_langspec_gate/o_empty.txt\x00" 109 let o_unres: *u8 = "/tmp/nx_langspec_gate/o_unres.txt\x00" 110 let o_nocc: *u8 = "/tmp/nx_langspec_gate/o_nocc.txt\x00" 111 let o_prod: *u8 = "/tmp/nx_langspec_gate/o_prod.txt\x00" 112 113 lg_put(f_conf, "max_clauses=64\nmax_cases=64\nfail_capture_head_bytes=256\nmin_clause_coverage_permil=600\ncompiler_elf=_offc/nx_cc_sovereign.elf\n" as *u8) 114 lg_put(f_spec, "clause|GX-A|SYN|A minimal program is accepted|A function returning a constant compiles and emits assembly.\nclause|GX-B|REF|A constant shift out of range is refused|A shift whose count is a constant outside the width of the result is refused at compile time.\nclause|GX-C|EXE|Deliberately unexercised|No case cites this clause, so the coverage report must count it and name it.\n" as *u8) 115 lg_put(f_good, "case|GX-1|GX-A|ACCEPT|-|.att_syntax|-|INLINE\nfunc main() -> i64 { return 0 }\nendcase\ncase|GX-2|GX-B|REFUSE|-|capability=shift-count-range|exit=2|INLINE\nfunc main() -> i64 {\n let x: i64 = 1 << 70\n return x\n}\nendcase\n" as *u8) 116 // THE PLANT: clause GX-B still says the out-of-range shift is refused, but the case now asserts 117 // the compiler ACCEPTS it. That is a divergence between the written specification and the shipped 118 // implementation -- precisely what a conformance suite exists to catch -- and the runner must say 119 // so rather than pass. 120 lg_put(f_plant, "case|GX-1|GX-A|ACCEPT|-|.att_syntax|-|INLINE\nfunc main() -> i64 { return 0 }\nendcase\ncase|GX-2|GX-B|ACCEPT|-|.att_syntax|-|INLINE\nfunc main() -> i64 {\n let x: i64 = 1 << 70\n return x\n}\nendcase\n" as *u8) 121 // THE SECOND PLANT, the other direction: the program IS refused, but for a reason the clause does 122 // not name. A suite that only asks whether something was refused passes this; this one must not. 123 lg_put(f_wrong, "case|GX-1|GX-A|ACCEPT|-|.att_syntax|-|INLINE\nfunc main() -> i64 { return 0 }\nendcase\ncase|GX-2|GX-B|REFUSE|-|capability=a-rule-this-compiler-never-prints|-|INLINE\nfunc main() -> i64 {\n let x: i64 = 1 << 70\n return x\n}\nendcase\n" as *u8) 124 lg_put(f_empty, "a suite file that declares no cases at all\n" as *u8) 125 lg_put(f_unres, "case|GX-1|GX-A|ACCEPT|-|.att_syntax|-|INLINE\nfunc main() -> i64 { return 0 }\nendcase\ncase|GX-9|GX-NO-SUCH-CLAUSE|ACCEPT|-|.att_syntax|-|INLINE\nfunc main() -> i64 { return 0 }\nendcase\n" as *u8) 126 127 let run_verb: *u8 = "run\x00" 128 let rc_good: i64 = lg_run(elf, run_verb, f_spec, f_good, LG_CC, f_conf, o_good) 129 let rc_plant: i64 = lg_run(elf, run_verb, f_spec, f_plant, LG_CC, f_conf, o_plant) 130 let rc_wrong: i64 = lg_run(elf, run_verb, f_spec, f_wrong, LG_CC, f_conf, o_wrong) 131 let rc_empty: i64 = lg_run(elf, run_verb, f_spec, f_empty, LG_CC, f_conf, o_empty) 132 let rc_unres: i64 = lg_run(elf, run_verb, f_spec, f_unres, LG_CC, f_conf, o_unres) 133 let rc_nocc: i64 = lg_run(elf, run_verb, f_spec, f_good, LG_CC_ABSENT, f_conf, o_nocc) 134 let rc_prod: i64 = lg_run(elf, run_verb, LG_PROD_SPEC, LG_PROD_SUITE, LG_CC, LG_PROD_CONF, o_prod) 135 136 ccg_val("good_exit" as *u8, rc_good) 137 ccg_val("planted_exit" as *u8, rc_plant) 138 ccg_val("wrongreason_exit" as *u8, rc_wrong) 139 ccg_val("emptysuite_exit" as *u8, rc_empty) 140 ccg_val("unresolved_exit" as *u8, rc_unres) 141 ccg_val("absentcompiler_exit" as *u8, rc_nocc) 142 ccg_val("production_exit" as *u8, rc_prod) 143 144 // ---- the good run: the discrimination control ----------------------------------------------- 145 var t: i64 = 0 146 if rc_good == LG_EXIT_CONFORMANT { t = 1 } 147 gv_check("T1 good-fixture-suite-is-CONFORMANT-exit0 (without this every refusal tooth below would be satisfied by a runner that failed everything)" as *u8, t, ctr) 148 gv_check("T2 good-run-drove-the-shipped-compiler-and-found-it (compiler_present=1 and drives_compiler=1 both on the record)" as *u8, ccg_file_has(o_good, "compiler_present=1\x00" as *u8), ctr) 149 gv_check("T3 good-run-declares-it-actually-compiled (drives_compiler=1, so a coverage-only pass cannot wear a full run's clothes)" as *u8, ccg_file_has(o_good, "drives_compiler=1\x00" as *u8), ctr) 150 gv_check("T4 good-run-passes-both-cases (cases_pass=2 -- binds the verdict to its denominator, so a zero-case run cannot produce this green)" as *u8, ccg_file_has(o_good, "cases_pass=2\x00" as *u8), ctr) 151 gv_check("T5 good-run-has-no-failures (cases_fail=0)" as *u8, ccg_file_has(o_good, "cases_fail=0\x00" as *u8), ctr) 152 gv_check("T6 good-run-has-no-abstentions (cases_unobservable=0, so T1's CONFORMANT rests on cases actually judged)" as *u8, ccg_file_has(o_good, "cases_unobservable=0\x00" as *u8), ctr) 153 gv_check("T7 good-run-case-partition-reconciles (pass plus fail plus unobservable equals cases admitted)" as *u8, ccg_file_has(o_good, "case_partition_reconciles=1\x00" as *u8), ctr) 154 gv_check("T8 good-run-reports-complete-coverage-of-what-it-observed (coverage_complete=1)" as *u8, ccg_file_has(o_good, "coverage_complete=1\x00" as *u8), ctr) 155 156 // ---- THE LOAD-BEARING TOOTH: a planted deviation goes RED ------------------------------------- 157 var t9: i64 = 0 158 if rc_plant == LG_EXIT_DEVIATION { t9 = 1 } 159 gv_check("T9 PLANTED-DEVIATION-GOES-RED (a clause and the shipped compiler made to disagree: the runner must exit DEVIATION(1), the rung's named done-rule)" as *u8, t9, ctr) 160 gv_check("T10 planted-deviation-says-so-in-its-verdict-line (verdict=DEVIATION, readable from outside without parsing prose)" as *u8, ccg_file_has(o_plant, "verdict=DEVIATION\x00" as *u8), ctr) 161 gv_check("T11 planted-deviation-NAMES-the-failing-case (a count without a worklist is not actionable)" as *u8, ccg_file_has(o_plant, "CASE id=GX-2 kind=ACCEPT verdict=FAIL\x00" as *u8), ctr) 162 gv_check("T12 planted-deviation-names-WHY-it-failed (the reason field distinguishes a refused-legal-program from a missing marker)" as *u8, ccg_file_has(o_plant, "reason=compiler-refused-a-program-the-spec-says-is-legal\x00" as *u8), ctr) 163 gv_check("T13 planted-deviation-still-passes-the-untouched-case (cases_pass=1: the plant is attributable to ONE case, not a suite-wide collapse)" as *u8, ccg_file_has(o_plant, "cases_pass=1\x00" as *u8), ctr) 164 165 // ---- the second plant: a refusal for the WRONG reason is not a pass --------------------------- 166 var t14: i64 = 0 167 if rc_wrong == LG_EXIT_DEVIATION { t14 = 1 } 168 gv_check("T14 neg-control-refusal-for-the-wrong-reason-is-a-DEVIATION (the program IS refused, but not by the clause under test -- a suite that only asks whether it was refused passes here and this one must not)" as *u8, t14, ctr) 169 gv_check("T15 neg-control-wrong-reason-is-named-as-such" as *u8, ccg_file_has(o_wrong, "reason=refused-but-not-for-the-clause-under-test\x00" as *u8), ctr) 170 171 // ---- the empty set -------------------------------------------------------------------------- 172 var t16: i64 = 0 173 if rc_empty == LG_EXIT_EMPTY { t16 = 1 } 174 gv_check("T16 neg-control-empty-suite-is-EMPTY-not-success (exit 4: a conformance runner that certifies the empty set is the vacuous-test defect wearing a certification costume)" as *u8, t16, ctr) 175 var t17: i64 = 1 176 if rc_empty == LG_EXIT_CONFORMANT { t17 = 0 } 177 gv_check("T17 neg-control-empty-suite-is-NEVER-exit0 (stated separately from T16 so a future exit-code change cannot quietly make the empty set succeed)" as *u8, t17, ctr) 178 179 // ---- traceability integrity ------------------------------------------------------------------ 180 var t18: i64 = 0 181 if rc_unres == LG_EXIT_DEVIATION { t18 = 1 } 182 gv_check("T18 neg-control-citation-to-a-clause-that-does-not-exist-is-a-DEVIATION (a broken requirements-to-tests link is the defect this rung exists to prevent, so it may not be dropped quietly)" as *u8, t18, ctr) 183 gv_check("T19 unresolved-citation-is-NAMED-with-its-case-and-its-clause" as *u8, ccg_file_has(o_unres, "UNRESOLVED-MARK case=GX-9 clause=GX-NO-SUCH-CLAUSE\x00" as *u8), ctr) 184 185 // ---- the rung's actual deliverable: which clauses nothing exercises --------------------------- 186 gv_check("T20 clause-population-is-counted (clauses_total=3 over the fixture spec)" as *u8, ccg_file_has(o_good, "clauses_total=3\x00" as *u8), ctr) 187 gv_check("T21 unexercised-clauses-are-COUNTED (clauses_unexercised=1)" as *u8, ccg_file_has(o_good, "clauses_unexercised=1\x00" as *u8), ctr) 188 gv_check("T22 unexercised-clauses-are-NAMED-individually (UNEXERCISED clause=GX-C: the coverage number is worthless without the worklist behind it)" as *u8, ccg_file_has(o_good, "UNEXERCISED clause=GX-C\x00" as *u8), ctr) 189 gv_check("T23 clause-partition-sums-to-the-population (exercised plus unexercised equals total)" as *u8, ccg_file_has(o_good, "clause_partition_sum=3\x00" as *u8), ctr) 190 gv_check("T24 exercised-count-is-not-saturated (clauses_exercised=2 of 3: a coverage metric that answered ALL for every input would discriminate nothing)" as *u8, ccg_file_has(o_good, "clauses_exercised=2\x00" as *u8), ctr) 191 192 // ---- it really executes the compiler ---------------------------------------------------------- 193 var t25: i64 = 0 194 if rc_nocc == LG_EXIT_UNOBSERVABLE { t25 = 1 } 195 gv_check("T25 neg-control-absent-compiler-ABSTAINS-rather-than-acquitting-or-convicting (exit 3: proves the runner genuinely forks the compiler, since a simulation would be unaffected by its absence)" as *u8, t25, ctr) 196 gv_check("T26 absent-compiler-says-which-artifact-it-could-not-find" as *u8, ccg_file_has(o_nocc, "COMPILER-ABSENT\x00" as *u8), ctr) 197 var t27: i64 = 1 198 if rc_nocc == LG_EXIT_CONFORMANT { t27 = 0 } 199 if rc_nocc == LG_EXIT_DEVIATION { t27 = 0 } 200 gv_check("T27 absent-compiler-is-neither-CONFORMANT-nor-DEVIATION (an axis that cannot see must not vote in either direction)" as *u8, t27, ctr) 201 202 // ---- the production suite --------------------------------------------------------------------- 203 var t28: i64 = 0 204 if rc_prod == LG_EXIT_CONFORMANT { t28 = 1 } 205 gv_check("T28 production-specification-and-suite-run-CONFORMANT-against-the-shipped-compiler" as *u8, t28, ctr) 206 var t29: i64 = 1 207 if ccg_file_has(o_prod, "COVERAGE-BELOW-FLOOR\x00" as *u8) == 1 { t29 = 0 } 208 gv_check("T29 production-clause-coverage-is-at-or-above-the-declared-ratchet" as *u8, t29, ctr) 209 var t30: i64 = 1 210 if ccg_file_has(o_prod, "unresolved_marks=0\x00" as *u8) == 0 { t30 = 0 } 211 gv_check("T30 production-requirements-to-tests-links-all-resolve (every clause a case cites exists)" as *u8, t30, ctr) 212 213 return gv_verdict("LANGSPEC-LR5" as *u8, ctr, "spec_conformance_run over the shipped compiler" as *u8) 214}