nx_virtio_spec_oracle_gate.nx source
↩ module page · 194 lines · 10980 B
1// nx_virtio_spec_oracle_gate.nx -- THE ORACLE ROW FOR `smallos`: corroborate OUR declared virtio-MMIO
2// register map against the PUBLISHED OASIS SPECIFICATION -- a document WE DID NOT WRITE.
3//
4// WHY THIS EXISTS (and why it is not just another self-test). nx_evidence_verdict.nx clause 5
5// TRIANGULATION requires >=2 distinct method classes with >=1 MECHANISTIC, and defines the ORACLE class
6// as agreement with an INDEPENDENT implementation or external ground truth -- explicitly "something WE
7// DID NOT WRITE". Every other gate in this lane is MECH and SELF-AUTHORED: I wrote the questions AND the
8// answers. MEASURED 2026-08-15: smallos therefore carried exactly ONE method class, min_classes=2 binds,
9// and the domain COULD NOT REACH PROVEN no matter how many of its own gates went green.
10// ******A DOMAIN THAT CAN ONLY EVER CITE ITSELF HAS A CEILING NO AMOUNT OF GREEN CAN RAISE.
11//
12// WHAT I REFUSED, recorded so nobody quietly does it: this estate has TWO rv64 simulators
13// (rv64im_min_sim, nx_rv64_fast) and a differential between them LOOKS like clause 5's
14// "second-implementation cross-check". It does not qualify -- BOTH ARE OURS. **A CROSS-CHECK BETWEEN TWO
15// THINGS YOU WROTE MEASURES YOUR CONSISTENCY, NOT YOUR CORRECTNESS.**
16//
17// THE SUBJECT: knowledge/specs/EXTERNAL-virtio-v1.2-oasis.html, fetched 2026-08-15 over the sovereign
18// HTTPS stack from docs.oasis-open.org (2,678,562 B, byte-verified on copy). It is the ONLY external
19// virtio ground truth in the corpus -- before the fetch there was NONE (`virtio-v1` across knowledge/ =
20// 0 matches, corpus_complete=1 over 176,785 files).
21//
22// THE CHECK, and its CEILING STATED PLAINLY: for every register offset and identity constant OUR spec
23// DECLARES, assert the literal appears in the OASIS document. This is PRESENCE-IN-THE-NORMATIVE-TEXT,
24// which is WEAKER than parsing the register table: a literal could in principle occur in unrelated prose.
25// It is corroboration, NOT derivation, and it must never be quoted as more. What makes it worth having
26// anyway is the NEG-CONTROL below: a FABRICATED offset must be ABSENT, which proves the check can
27// discriminate rather than saying yes to everything. *A PRESENCE TEST WITHOUT AN ABSENCE CONTROL IS A
28// FUNCTION THAT RETURNS TRUE.
29//
30// DATA-DRIVEN (rule 11): the constants are READ OUT OF OUR SPEC at runtime, never retyped here, so the
31// gate cannot drift from the thing it certifies. Adding a register to the spec extends this gate for free.
32// exit: gv_verdict (0 GREEN / 1 RED / 3 SKIP) license_tier: ORIGINAL. Read-only. No hw writes (Rule 26).
33import "nx_syscalls.nx"
34import "nx_gate_verdict.nx"
35
36const VO_SPEC_EXT: *u8 = "knowledge/specs/EXTERNAL-virtio-v1.2-oasis.html"
37const VO_SPEC_OURS: *u8 = "knowledge/specs/virtio_blk_sector_virt.spec"
38// a value that is NOT a virtio-MMIO register offset. The neg-control: if THIS is "found", the check is
39// vacuous and the gate must go RED rather than report a clean sweep.
40const VO_BOGUS: *u8 = "0x0AB7"
41const VO_NL: i64 = 10
42const VO_SP: i64 = 32
43
44func vo_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
45func vo_n(v: i64) -> i64 {
46 var m: i64 = v
47 if m < 0 { vo_p("-" as *u8); m = 0 - m }
48 let t: *u8 = sys_mmap(32)
49 var k: i64 = 0
50 if m == 0 { t[0] = 48 as u8; k = 1 }
51 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
52 let o: *u8 = sys_mmap(32)
53 var i: i64 = 0
54 while i < k { o[i] = t[k - 1 - i]; i = i + 1 }
55 sys_write(1, o, k)
56 return 0
57}
58func vo_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
59// ASCII lower-case fold. HEX IS CASE-INSENSITIVE AND THE TWO CASES ARE TWO STRINGS TO EVERY SCANNER:
60// our spec writes 0x00C / 0x03C, the OASIS document writes 0x00c / 0x03c, and a case-sensitive compare
61// reported BOTH as absent from the standard -- a false accusation against a register that is in fact
62// specified. *THE SAME CONSTANT IN TWO SPELLINGS IS TWO CONSTANTS UNLESS THE COMPARATOR SAYS OTHERWISE.
63func vo_lc(c: i64) -> i64 { if c >= 65 { if c <= 90 { return c + 32 } } return c }
64// does buf[0,n) contain the NUL-terminated literal lit, case-insensitively? 1/0
65func vo_has(buf: *u8, n: i64, lit: *u8) -> i64 {
66 let ll: i64 = vo_len(lit)
67 if ll <= 0 { return 0 }
68 var i: i64 = 0
69 while i + ll <= n {
70 var k: i64 = 0
71 var hit: i64 = 1
72 while k < ll { if vo_lc(buf[i+k] as i64) != vo_lc(lit[k] as i64) { hit = 0; k = ll } else { k = k + 1 } }
73 if hit == 1 { return 1 }
74 i = i + 1
75 }
76 return 0
77}
78// is this a SOVEREIGN INSTRUMENT register rather than a standard virtio one? 1/0
79// The *Peek registers (QueueDescPeek/QueueUsedIdxPeek/QueueStatPeek/QueueSectPeek) are OUR additions --
80// RO result registers the real device does not expose, which our own specs already say in those words.
81// Their ABSENCE from the OASIS document is the CORRECT answer, not a violation, so they must be counted
82// as EXTENSIONS and never as failures -- and equally never as corroborations.
83// ******A GATE THAT FLAGS YOUR DELIBERATE EXTENSIONS AS SPEC VIOLATIONS IS A FALSE-POSITIVE MACHINE, AND
84// ONE THAT COUNTS THEM AS CORROBORATED IS WORSE -- MEASURED HERE: off_queueusedidxpeek 0x064 scored as
85// CORROBORATED because the literal 0x064 happens to occur elsewhere in a 2.6 MB document. That is the
86// exact ceiling this gate's header declares (presence-in-text, not table parsing) catching itself.
87func vo_is_sovereign(buf: *u8, ls: i64, le: i64) -> i64 {
88 var i: i64 = ls
89 while i + 4 <= le {
90 if buf[i] == (112 as u8) { if buf[i+1] == (101 as u8) { if buf[i+2] == (101 as u8) { if buf[i+3] == (107 as u8) { return 1 } } } }
91 i = i + 1
92 }
93 return 0
94}
95// does the line [ls,le) start with the literal pfx? 1/0
96func vo_starts(buf: *u8, ls: i64, le: i64, pfx: *u8) -> i64 {
97 let pl: i64 = vo_len(pfx)
98 if ls + pl > le { return 0 }
99 var k: i64 = 0
100 while k < pl { if buf[ls+k] != pfx[k] { return 0 } k = k + 1 }
101 return 1
102}
103// copy the LAST whitespace-separated field of [ls,le) into out (NUL-terminated); return its length.
104// Separate cursor + explicit flag, never a sentinel written into the cursor itself -- a loop that exits
105// by clobbering its own cursor cannot also report where it stopped.
106func vo_lastfield_tail(buf: *u8, ls: i64, le: i64, out: *u8) -> i64 {
107 var s: i64 = le
108 var go: i64 = 1
109 while go == 1 {
110 if s <= ls { go = 0 } else {
111 if buf[s-1] == (VO_SP as u8) { go = 0 } else { s = s - 1 }
112 }
113 }
114 var o: i64 = 0
115 var i: i64 = s
116 while i < le { out[o] = buf[i]; o = o + 1; i = i + 1 }
117 out[o] = 0 as u8
118 return o
119}
120
121func main() -> i64 {
122 let ctr: *i64 = gv_ctr()
123 gv_head("nx_virtio_spec_oracle_gate -- OUR declared virtio register map vs the PUBLISHED OASIS spec (external ground truth, ORACLE class)")
124
125 let el: *i64 = sys_mmap(16) as *i64
126 let eb: *u8 = sys_read_file(VO_SPEC_EXT, el)
127 let ol: *i64 = sys_mmap(16) as *i64
128 let ob: *u8 = sys_read_file(VO_SPEC_OURS, ol)
129
130 // PRECONDITIONS: both artifacts must be readable. "I could not look" is not "it disagrees".
131 var have_ext: i64 = 0
132 if (eb as i64) != 0 { if el[0] > 0 { have_ext = 1 } }
133 var have_ours: i64 = 0
134 if (ob as i64) != 0 { if ol[0] > 0 { have_ours = 1 } }
135 if gv_need("the OASIS virtio specification artifact is present (knowledge/specs/EXTERNAL-virtio-v1.2-oasis.html)", have_ext, ctr) == 0 {
136 return gv_verdict("VIRTIO-SPEC-ORACLE", ctr, "external corroboration")
137 }
138 if gv_need("our own declared register map is readable", have_ours, ctr) == 0 {
139 return gv_verdict("VIRTIO-SPEC-ORACLE", ctr, "external corroboration")
140 }
141 let en: i64 = el[0]
142 let on: i64 = ol[0]
143 vo_p(" external artifact bytes=" as *u8); vo_n(en)
144 vo_p(" our spec bytes=" as *u8); vo_n(on); vo_p("\n" as *u8)
145
146 // NEG-CONTROL FIRST, so a vacuous run cannot reach the real teeth and look clean.
147 let bogus_absent: i64 = 1 - vo_has(eb, en, VO_BOGUS)
148 gv_check("neg-control-fabricated-offset-absent: a value that is NOT a virtio register offset must NOT be found in the OASIS document (without this, a presence test that always says yes would score a perfect sweep)", bogus_absent, ctr)
149
150 // POSITIVE ANCHOR: the identity magic the spec states the device MUST return.
151 gv_check("oracle-magic: our declared MagicValue 0x74726976 appears in the OASIS specification text", vo_has(eb, en, "0x74726976" as *u8), ctr)
152
153 // DATA-DRIVEN SWEEP: every `off_*` row OUR spec declares must have its offset literal in the doc.
154 let val: *u8 = sys_mmap(64)
155 var checked: i64 = 0
156 var found: i64 = 0
157 var sovereign: i64 = 0
158 var ls: i64 = 0
159 while ls < on {
160 var le: i64 = ls
161 var go: i64 = 1
162 while go == 1 { if le >= on { go = 0 } else { if ob[le] == (VO_NL as u8) { go = 0 } else { le = le + 1 } } }
163 if le > ls {
164 if vo_starts(ob, ls, le, "off_" as *u8) == 1 {
165 if vo_lastfield_tail(ob, ls, le, val) > 0 {
166 if vo_is_sovereign(ob, ls, le) == 1 {
167 sovereign = sovereign + 1
168 vo_p(" SOVEREIGN-EXTENSION (correctly absent from the standard, not judged): " as *u8)
169 sys_write(1, (ob as i64 + ls) as *u8, le - ls); vo_p("\n" as *u8)
170 } else {
171 checked = checked + 1
172 if vo_has(eb, en, val) == 1 { found = found + 1 } else {
173 vo_p(" NOT-IN-SPEC: " as *u8); sys_write(1, (ob as i64 + ls) as *u8, le - ls); vo_p("\n" as *u8)
174 }
175 }
176 }
177 }
178 }
179 ls = le + 1
180 }
181 // PARTITION, PRINTED AND RECONCILED: standard-judged + sovereign-extension must account for EVERY
182 // off_ row our spec declares. A census whose parts do not sum is a census somebody plans against.
183 vo_p(" standard_offsets=" as *u8); vo_n(checked)
184 vo_p(" corroborated=" as *u8); vo_n(found)
185 vo_p(" sovereign_extensions=" as *u8); vo_n(sovereign)
186 vo_p(" total_declared=" as *u8); vo_n(checked + sovereign); vo_p("\n" as *u8)
187
188 // BIND THE ASSERTION TO ITS DENOMINATOR: a sweep that examined ZERO rows must NEVER pass.
189 var all_corroborated: i64 = 0
190 if checked > 0 { if found == checked { all_corroborated = 1 } }
191 gv_check("oracle-offsets: EVERY register offset our spec declares is corroborated by the OASIS document, over a NON-EMPTY set of declared offsets (a tooth that passes on the empty set is not a tooth)", all_corroborated, ctr)
192
193 return gv_verdict("VIRTIO-SPEC-ORACLE", ctr, "our declared virtio-MMIO register map is corroborated against the PUBLISHED OASIS virtio specification -- external ground truth this estate did not author. CEILING: presence-in-normative-text, not table parsing; corroboration, never derivation")
194}