nx_paper_forge_gate.nx source
↩ module page · 144 lines · 6573 B
1// nx_paper_forge_gate.nx -- KAT + neg-controls for the manuscript compiler (AS-1).
2// Proves the two refusals that make a compiled paper trustworthy:
3// REFUSE-UNCITED an unknown {ID} cannot be silently dropped or emitted bare
4// REFUSE-UNSTRUCTURED a manuscript missing a graded section is detected and named
5// plus ledger lookup, expansion shape, determinism, and NON-VACUITY (the expansion
6// really carries the ledger's value, so the gate cannot pass on an empty emitter).
7// DRY nx_gate_verdict lib (D001 migrate-on-touch).
8import "nx_paper_forge.nx"
9import "nx_gate_verdict.nx"
10
11func main() -> i64 {
12 let ctr: *i64 = gv_ctr()
13 gv_head("nx_paper_forge -- sovereign manuscript compiler (AS-1)")
14
15 // build a 2-row evidence ledger: <id>TAB<value>TAB<source>NL
16 let led: *u8 = sys_mmap(512)
17 var lo: i64 = 0
18 lo = pf_app(led, lo, "E1" as *u8); led[lo] = 9 as u8; lo = lo + 1
19 lo = pf_app(led, lo, "306" as *u8); led[lo] = 9 as u8; lo = lo + 1
20 lo = pf_app(led, lo, "drbench_scale.log" as *u8); led[lo] = 10 as u8; lo = lo + 1
21 lo = pf_app(led, lo, "E2" as *u8); led[lo] = 9 as u8; lo = lo + 1
22 lo = pf_app(led, lo, "100" as *u8); led[lo] = 9 as u8; lo = lo + 1
23 lo = pf_app(led, lo, "task_manifest.tsv" as *u8); led[lo] = 10 as u8; lo = lo + 1
24 let ledp: *i64 = sys_mmap(2 * 8) as *i64
25 ledp[0] = led as i64
26 ledp[1] = lo
27 let out: *i64 = sys_mmap(2 * 8) as *i64
28
29 // T1 lookup resolves a known id to its value field
30 var ok1: i64 = 0
31 if pf_lookup(led, lo, "E1" as *u8, 2, out) == 1 {
32 if out[1] - out[0] == 3 {
33 if led[out[0]] == (51 as u8) { ok1 = 1 }
34 }
35 }
36 gv_check("T1 ledger lookup resolves E1 -> 306", ok1, ctr)
37
38 // T2 lookup MISSES an absent id (the precondition for refusing)
39 var ok2: i64 = 0
40 if pf_lookup(led, lo, "E9" as *u8, 2, out) == 0 { ok2 = 1 }
41 gv_check("T2 lookup misses an absent id", ok2, ctr)
42
43 // T3 expansion writes "<value> [ev:ID]" -- the provenance token the ruler counts
44 let src: *u8 = "semantic recall {E1} permille" as *u8
45 var sn: i64 = 0
46 while src[sn] != (0 as u8) { sn = sn + 1 }
47 let ab: *i64 = sys_mmap(2 * 8) as *i64
48 ab[0] = 0; ab[1] = sn
49 let dst: *u8 = sys_mmap(4096)
50 let e1: i64 = pf_expand(dst, 0, src, ab, ledp)
51 var ok3: i64 = 0
52 if e1 > 0 {
53 if pb_find(dst, e1, "306 [ev:E1]" as *u8) == 1 { ok3 = 1 }
54 }
55 gv_check("T3 expansion emits value + [ev:E1] provenance token", ok3, ctr)
56
57 // T4 ***NEG-CONTROL*** REFUSE-UNCITED: an unknown id returns -1. It is NOT dropped
58 // silently and NOT emitted bare -- the manuscript simply cannot be produced.
59 let bad: *u8 = "unsupported figure {E9} appears here" as *u8
60 var bn: i64 = 0
61 while bad[bn] != (0 as u8) { bn = bn + 1 }
62 ab[0] = 0; ab[1] = bn
63 let dstbad: *u8 = sys_mmap(4096)
64 var ok4: i64 = 0
65 if pf_expand(dstbad, 0, bad, ab, ledp) < 0 { ok4 = 1 }
66 gv_check("T4 NEG-CONTROL uncited claim refuses (returns -1)", ok4, ctr)
67
68 // T5 a structurally COMPLETE manuscript passes the required-section check
69 let doc: *u8 = sys_mmap(8192)
70 var d: i64 = 0
71 d = pf_app(doc, d, "# T\n## Abstract\nx\n## Data\nd\n## Baseline\nb\n" as *u8)
72 d = pf_app(doc, d, "## Negative Controls\nc\n## Reproducibility\nr\n" as *u8)
73 d = pf_app(doc, d, "## Limitations\nl\n## References\n- x\n" as *u8)
74 let miss: *i64 = sys_mmap(6 * 8) as *i64
75 var m: i64 = 0
76 while m < 6 { miss[m] = 0; m = m + 1 }
77 var ok5: i64 = 0
78 if pf_required(doc, d, miss) == 0 { ok5 = 1 }
79 gv_check("T5 complete manuscript passes required-section check", ok5, ctr)
80
81 // T6 ***NEG-CONTROL*** REFUSE-UNSTRUCTURED: drop Limitations -> detected AND NAMED
82 let doc2: *u8 = sys_mmap(8192)
83 var d2: i64 = 0
84 d2 = pf_app(doc2, d2, "# T\n## Abstract\nx\n## Data\nd\n## Baseline\nb\n" as *u8)
85 d2 = pf_app(doc2, d2, "## Negative Controls\nc\n## Reproducibility\nr\n" as *u8)
86 d2 = pf_app(doc2, d2, "## References\n- x\n" as *u8)
87 m = 0
88 while m < 6 { miss[m] = 0; m = m + 1 }
89 var ok6: i64 = 0
90 if pf_required(doc2, d2, miss) == 1 {
91 if miss[2] == 1 { ok6 = 1 }
92 }
93 gv_check("T6 NEG-CONTROL missing Limitations detected and named", ok6, ctr)
94
95 // T7 DETERMINISM: the same (paragraph, ledger) expands to identical bytes
96 ab[0] = 0; ab[1] = sn
97 let dst2: *u8 = sys_mmap(4096)
98 let e2: i64 = pf_expand(dst2, 0, src, ab, ledp)
99 var ok7: i64 = 0
100 if e2 == e1 {
101 var k: i64 = 0
102 var same: i64 = 1
103 while k < e1 { if dst[k] != dst2[k] { same = 0; k = e1 } else { k = k + 1 } }
104 if same == 1 { ok7 = 1 }
105 }
106 gv_check("T7 expansion is byte-deterministic", ok7, ctr)
107
108 // T8 NON-VACUITY: the surrounding prose survives AND a second id resolves, so the
109 // gate cannot be satisfied by an emitter that writes nothing.
110 let two: *u8 = "over {E2} tasks recall was {E1}" as *u8
111 var tn: i64 = 0
112 while two[tn] != (0 as u8) { tn = tn + 1 }
113 ab[0] = 0; ab[1] = tn
114 let dst3: *u8 = sys_mmap(4096)
115 let e3: i64 = pf_expand(dst3, 0, two, ab, ledp)
116 var ok8: i64 = 0
117 if e3 > tn {
118 if pb_find(dst3, e3, "100 [ev:E2]" as *u8) == 1 {
119 if pb_find(dst3, e3, "306 [ev:E1]" as *u8) == 1 {
120 if pb_find(dst3, e3, "tasks recall was" as *u8) == 1 { ok8 = 1 }
121 }
122 }
123 }
124 gv_check("T8 non-vacuity: both ids resolve and prose survives", ok8, ctr)
125
126 // T9 REFUSE IS NOT ROLLBACK -- pinned deliberately. A refused expansion has already
127 // written the prose PRECEDING the bad {ID} into the caller's buffer before it could
128 // know the id was unresolvable. The engine cannot un-write it, so the CALLER's
129 // contract is "on refuse, discard the whole document" -- which is exactly what
130 // nx_paper_forge_cli does (it never opens the output file). This test exists so a
131 // future reader cannot mistake the partial bytes for a bug, or "fix" it by trusting
132 // the returned offset. Caught by T7 failing on a shared buffer during development.
133 let dstp: *u8 = sys_mmap(4096)
134 ab[0] = 0; ab[1] = bn
135 var ok9: i64 = 0
136 if pf_expand(dstp, 0, bad, ab, ledp) < 0 {
137 if pb_find(dstp, bn, "unsupported figure " as *u8) == 1 { ok9 = 1 }
138 }
139 gv_check("T9 refuse is not rollback: caller must discard, CLI does", ok9, ctr)
140
141 let rc: i64 = gv_verdict("PAPER-FORGE", ctr, "ledger lookup + provenance expansion + REFUSE-UNCITED and REFUSE-UNSTRUCTURED neg-controls + determinism + refuse-is-not-rollback")
142 sys_exit(rc)
143 return rc
144}