nx_riscv_spec_oracle_gate.nx source
↩ module page · 261 lines · 16877 B
1// nx_riscv_spec_oracle_gate.nx -- THE ORACLE ROW FOR `nishios`: corroborate the mcause exception codes
2// our kernel gates depend on against the OFFICIAL RISC-V PRIVILEGED SPECIFICATION -- a document WE DID
3// NOT WRITE.
4//
5// WHY: nx_evidence_verdict.nx clause 5 TRIANGULATION needs >=2 method classes with >=1 MECHANISTIC, and
6// defines ORACLE as agreement with external ground truth. Every nishios gate is MECH and SELF-AUTHORED,
7// so the domain carried ONE class and min_classes=2 made PROVEN unreachable. This is the second class.
8//
9// THE SUBJECT: knowledge/specs/EXTERNAL-riscv-priv-machine.adoc -- the machine-level chapter of the
10// RISC-V ISA manual, fetched 2026-08-15 from riscv/riscv-isa-manual (main) over the sovereign HTTPS
11// stack, preamble stripped, copy byte-verified. 173,346 B of CLEAN ASCIIDOC SOURCE.
12//
13// WHY NOT THE PDF -- MEASURED, AND IT IS THE WHOLE REASON THIS FILE EXISTS. The official v1.12 PDF was
14// fetched first and converted with nx_pdf_text. Its text layer is KERNED, so extraction SPLITS WORDS
15// (`Privileged Arc hitectures`, `this do cumen twas`) and drops ligatures (`simpli???ed`). Grepping THAT
16// artifact for "Environment call from U-mode" returned 0 matches, corpus_complete=1 -- while the spec
17// plainly contains it, at line 1875 of THIS file.
18// ******A DEGRADED RENDERING OF A CORRECT SOURCE PRODUCES CONFIDENT FALSE ABSENCES, AND AN ORACLE BUILT
19// ON IT WOULD ACCUSE THE ESTATE OF DEVIATING FROM A STANDARD IT ACTUALLY FOLLOWS. A FALSE RED AGAINST AN
20// EXTERNAL AUTHORITY IS THE MOST CREDIBLE WRONG ANSWER AVAILABLE. Two renderings of ONE document
21// disagreeing is what located the defect in the RENDERING rather than in the spec or in us.
22//
23// WHAT IT CHECKS, and the CEILING STATED PLAINLY. The spec's exception table is AsciiDoc: a column of
24// codes and a parallel column of descriptions. This gate does NOT claim to parse that table. It asserts
25// the STRUCTURE our gates actually depend on:
26// T1 both mcause descriptions exist in the official text at all
27// T2 U-mode precedes M-mode => mcause(U) < mcause(M), i.e. they are DISTINCT and ordered
28// T3 exactly TWO description entries sit between them (S-mode, _Reserved_)
29// => mcause(M) - mcause(U) == 3, which with the U=8 anchor pins M=11
30// That is the RELATIONSHIP _umode_gate relies on (ecall-from-U => 8, its MPP=M control => 11).
31// It pins ORDER and GAP against external text; it does not re-derive the absolute integers from the
32// table's code column. **CORROBORATION, NEVER DERIVATION** -- the same ceiling the virtio oracle carries.
33// exit: gv_verdict (0 GREEN / 1 RED / 3 SKIP) license_tier: ORIGINAL. Read-only. No hw writes (Rule 26).
34import "nx_syscalls.nx"
35import "nx_gate_verdict.nx"
36
37const RO_SPEC: *u8 = "knowledge/specs/EXTERNAL-riscv-priv-machine.adoc"
38const RO_U: *u8 = "Environment call from U-mode"
39const RO_S: *u8 = "Environment call from S-mode"
40const RO_M: *u8 = "Environment call from M-mode"
41// a description that is NOT in the RISC-V exception table. The neg-control: if this is "found", the
42// check is vacuous and the gate must go RED rather than report a clean sweep.
43const RO_BOGUS: *u8 = "Environment call from Q-mode"
44// the gap our kernel gates depend on: mcause(M) - mcause(U). 8 -> 11.
45const RO_EXPECT_GAP: i64 = 3
46// the SUPERVISOR chapter, and the satp MODE table row that names Sv39. The literal deliberately starts
47// AFTER the code column so the parser must read the row rather than match the answer it is looking for.
48// ★★★★★★A RULER WHOSE PATTERN CONTAINS THE VALUE IT REPORTS MEASURES TRANSCRIPTION, NOT THE DOCUMENT.
49const RO_SUPER: *u8 = "knowledge/specs/EXTERNAL-riscv-priv-supervisor.adoc"
50const RO_SV39ROW: *u8 = "Sv39 |Page-based 39-bit virtual addressing"
51const RO_SV39_MODE: i64 = 8
52const RO_SV48_MODE: i64 = 9
53// ★★★★★★THE SPEC LABELS ITS OWN NORMATIVE CLAIMS. The AsciiDoc source carries machine-readable
54// anchors of the form `[#norm:<id>]#<the normative sentence>#` -- so a claim can be corroborated against
55// the DOCUMENT'S OWN MARKING of what is normative, rather than against prose that merely happens to be
56// nearby. That is strictly better than substring-in-text and it was invisible in the PDF rendering.
57// **WHEN A SOURCE PUBLISHES STRUCTURE, USE THE STRUCTURE -- SEARCHING ITS PROSE INSTEAD IS THROWING AWAY
58// THE ONE THING THAT MAKES THE ANSWER UNAMBIGUOUS.
59const RO_LEVELS: *u8 = "[#norm:Sv39_levels]#three-level page table#"
60const RO_VPN: *u8 = "[#norm:Sv39_vpn_sz]#27-bit VPN#"
61const RO_PPN: *u8 = "[#norm:satp_ppn_sv39_sz]#44-bit PPN#"
62// a normative anchor that does not exist. Neg-control for the anchor teeth.
63const RO_BOGUS_NORM: *u8 = "[#norm:Sv39_qqq]#"
64// THE PTE-VALIDITY RULE _mmu_gate's bad-PTE tamper depends on. Found only after learning the spec's
65// NOTATION: it writes PTE fields in AsciiDoc italics as `_pte_._v_`, so `pte.v` and `norm:pte` BOTH
66// returned 0 matches with corpus_complete=1 and read exactly like the rule was absent.
67// ******AN ABSENCE PROOF IS ONLY AS GOOD AS THE SPELLING YOU SEARCHED FOR -- SAME CLASS AS 0x00C vs
68// 0x00c EARLIER TODAY, AND BOTH TIMES THE CONFIDENT ANSWER WAS THE WRONG ONE.
69const RO_PTEV: *u8 = "If _pte_._v_=0, or if _pte_._r_=0 and _pte_._w_=1"
70const RO_PTEFAULT: *u8 = "stop and raise a page-fault exception"
71const RO_BOGUS_PTE: *u8 = "If _pte_._z_=0"
72const RO_NL: i64 = 10
73
74func ro_p(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
75func ro_n(v: i64) -> i64 {
76 var m: i64 = v
77 if m < 0 { ro_p("-" as *u8); m = 0 - m }
78 let t: *u8 = sys_mmap(32)
79 var k: i64 = 0
80 if m == 0 { t[0] = 48 as u8; k = 1 }
81 while m > 0 { t[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
82 let o: *u8 = sys_mmap(32)
83 var i: i64 = 0
84 while i < k { o[i] = t[k - 1 - i]; i = i + 1 }
85 sys_write(1, o, k)
86 return 0
87}
88func ro_len(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
89// walk back from off to the start of its line, then return the FIRST decimal integer on that line,
90// or -1 if the line carries none. Used to read a table row's CODE column from the row itself, which
91// is a DIRECT value anchor rather than the positional one the mcause table forces.
92func ro_line_first_int(buf: *u8, off: i64) -> i64 {
93 var s: i64 = off
94 var go: i64 = 1
95 while go == 1 {
96 if s <= 0 { go = 0 } else {
97 if buf[s-1] == (RO_NL as u8) { go = 0 } else { s = s - 1 }
98 }
99 }
100 var i: i64 = s
101 var seen: i64 = 0
102 var v: i64 = 0
103 var done: i64 = 0
104 while done == 0 {
105 if i >= off { done = 1 } else {
106 let c: i64 = buf[i] as i64
107 if c >= 48 { if c <= 57 { seen = 1; v = v * 10 + (c - 48) } }
108 if seen == 1 { if c < 48 { done = 1 } }
109 if seen == 1 { if c > 57 { done = 1 } }
110 i = i + 1
111 }
112 }
113 if seen == 0 { return 0 - 1 }
114 return v
115}
116// byte offset of lit in buf[0,n), or -1. Offsets (not a boolean) because ORDER is the evidence here.
117func ro_find(buf: *u8, n: i64, lit: *u8) -> i64 {
118 let ll: i64 = ro_len(lit)
119 if ll <= 0 { return 0 - 1 }
120 var i: i64 = 0
121 while i + ll <= n {
122 var k: i64 = 0
123 var hit: i64 = 1
124 while k < ll { if buf[i+k] != lit[k] { hit = 0; k = ll } else { k = k + 1 } }
125 if hit == 1 { return i }
126 i = i + 1
127 }
128 return 0 - 1
129}
130// count newlines in buf[a,b) -- the number of table entries between two descriptions.
131func ro_lines_between(buf: *u8, a: i64, b: i64) -> i64 {
132 var c: i64 = 0
133 var i: i64 = a
134 while i < b { if buf[i] == (RO_NL as u8) { c = c + 1 } i = i + 1 }
135 return c
136}
137
138func main() -> i64 {
139 let ctr: *i64 = gv_ctr()
140 gv_head("nx_riscv_spec_oracle_gate -- the mcause codes our kernel gates rely on, vs the OFFICIAL RISC-V privileged spec (external ground truth, ORACLE class)")
141
142 let sl: *i64 = sys_mmap(16) as *i64
143 let sb: *u8 = sys_read_file(RO_SPEC, sl)
144 var have: i64 = 0
145 if (sb as i64) != 0 { if sl[0] > 0 { have = 1 } }
146 if gv_need("the official RISC-V privileged machine chapter is present (knowledge/specs/EXTERNAL-riscv-priv-machine.adoc)", have, ctr) == 0 {
147 return gv_verdict("RISCV-SPEC-ORACLE", ctr, "external corroboration")
148 }
149 let n: i64 = sl[0]
150 ro_p(" external artifact bytes=" as *u8); ro_n(n); ro_p("\n" as *u8)
151
152 // NEG-CONTROL FIRST: a fabricated exception description must be ABSENT, or a presence test that
153 // says yes to everything would score a perfect sweep.
154 var bogus_absent: i64 = 0
155 if ro_find(sb, n, RO_BOGUS) < 0 { bogus_absent = 1 }
156 gv_check("neg-control-fabricated-exception-absent: a description that is NOT in the RISC-V exception table must NOT be found in the official text", bogus_absent, ctr)
157
158 let pu: i64 = ro_find(sb, n, RO_U)
159 let ps: i64 = ro_find(sb, n, RO_S)
160 let pm: i64 = ro_find(sb, n, RO_M)
161 ro_p(" offsets: U-mode=" as *u8); ro_n(pu)
162 ro_p(" S-mode=" as *u8); ro_n(ps)
163 ro_p(" M-mode=" as *u8); ro_n(pm); ro_p("\n" as *u8)
164
165 var all_present: i64 = 0
166 if pu >= 0 { if ps >= 0 { if pm >= 0 { all_present = 1 } } }
167 gv_check("oracle-mcause-present: the official spec names 'Environment call from U-mode', '...S-mode' and '...M-mode' as exception descriptions", all_present, ctr)
168
169 // ORDER == CODE ORDER. Bound to the presence result so it cannot pass on absent offsets (-1 < -1
170 // arithmetic would otherwise let a missing entry satisfy an ordering test).
171 var ordered: i64 = 0
172 if all_present == 1 { if pu < ps { if ps < pm { ordered = 1 } } }
173 gv_check("oracle-mcause-order: U-mode precedes S-mode precedes M-mode in the exception table, so mcause(U) < mcause(S) < mcause(M) -- they are DISTINCT and ordered, which is what _umode_gate's 8-vs-11 control depends on", ordered, ctr)
174
175 // GAP: exactly two entries (S-mode, _Reserved_) sit between U-mode and M-mode => M - U == 3.
176 var gap: i64 = 0 - 1
177 if all_present == 1 { gap = ro_lines_between(sb, pu, pm) }
178 ro_p(" table entries between U-mode and M-mode=" as *u8); ro_n(gap)
179 ro_p(" expected=" as *u8); ro_n(RO_EXPECT_GAP); ro_p("\n" as *u8)
180 var gap_ok: i64 = 0
181 if gap == RO_EXPECT_GAP { gap_ok = 1 }
182 gv_check("oracle-mcause-gap: exactly 3 entries separate U-mode from M-mode (S-mode + _Reserved_ + the U row itself), so mcause(M) - mcause(U) == 3 -- with U=8 that pins M=11, the exact pair our kernel gates assert", gap_ok, ctr)
183
184 // ---- satp MODE, from the SUPERVISOR chapter. This is a DIRECT value anchor, not a positional one:
185 // the spec's satp MODE table puts the code and the name on ONE ROW
186 // |8 |Sv39 |Page-based 39-bit virtual addressing (see <<sv39>>).
187 // so reading the row's first integer answers "what MODE means Sv39" without counting anything.
188 // ★★★★★WHEN THE SOURCE OFFERS A DIRECT ANCHOR, TAKE IT -- a positional read is what you fall back to,
189 // never what you choose, because position is exactly what a reformat silently changes.
190 // drv_proto_mmu.spec programs "MODE 8 (Sv39)" and _mmu_gate/_priv_gate rely on that walk happening.
191 let ul: *i64 = sys_mmap(16) as *i64
192 let ub: *u8 = sys_read_file(RO_SUPER, ul)
193 var have_s: i64 = 0
194 if (ub as i64) != 0 { if ul[0] > 0 { have_s = 1 } }
195 if gv_need("the official RISC-V privileged SUPERVISOR chapter is present (knowledge/specs/EXTERNAL-riscv-priv-supervisor.adoc)", have_s, ctr) == 1 {
196 let un: i64 = ul[0]
197 let prow: i64 = ro_find(ub, un, RO_SV39ROW)
198 var mode: i64 = 0 - 1
199 if prow >= 0 { mode = ro_line_first_int(ub, prow) }
200 ro_p(" satp MODE row offset=" as *u8); ro_n(prow)
201 ro_p(" first-int-on-row=" as *u8); ro_n(mode)
202 ro_p(" expected=" as *u8); ro_n(RO_SV39_MODE); ro_p("\n" as *u8)
203 var mode_ok: i64 = 0
204 if mode == RO_SV39_MODE { mode_ok = 1 }
205 gv_check("oracle-satp-mode: the official satp MODE table row naming Sv39 carries the code 8 -- so MODE=8 means Sv39, exactly what drv_proto_mmu.spec programs and what _mmu_gate/_priv_gate depend on translating", mode_ok, ctr)
206 // neg-control: the SAME row must NOT report the neighbouring mode, or the parse is reading
207 // something other than the row's own code column.
208 var not_neighbour: i64 = 1
209 if mode == RO_SV48_MODE { not_neighbour = 0 }
210 gv_check("neg-control-satp-mode-not-neighbour: the Sv39 row's code is NOT 9 (Sv48's) -- a parser that returned a fixed or adjacent value would fail here", not_neighbour, ctr)
211
212 // ---- NORMATIVE-ANCHOR teeth: corroborate against the spec's OWN marking of what is normative.
213 var bogus_norm_absent: i64 = 0
214 if ro_find(ub, un, RO_BOGUS_NORM) < 0 { bogus_norm_absent = 1 }
215 gv_check("neg-control-fabricated-norm-anchor-absent: a normative anchor id that does not exist must NOT be found -- otherwise the anchor teeth below are matching something other than real anchors", bogus_norm_absent, ctr)
216
217 var lv: i64 = 0
218 if ro_find(ub, un, RO_LEVELS) >= 0 { lv = 1 }
219 gv_check("oracle-sv39-three-level: the spec's OWN normative anchor [#norm:Sv39_levels] marks 'three-level page table' -- corroborating _mmu_gate's claim that the MMU WALKED a 3-level table rather than a flat or 2-level one", lv, ctr)
220
221 var vp: i64 = 0
222 if ro_find(ub, un, RO_VPN) >= 0 { vp = 1 }
223 var pp: i64 = 0
224 if ro_find(ub, un, RO_PPN) >= 0 { pp = 1 }
225 var split_ok: i64 = 0
226 if vp == 1 { if pp == 1 { split_ok = 1 } }
227 gv_check("oracle-sv39-address-split: the normative anchors [#norm:Sv39_vpn_sz] 27-bit VPN and [#norm:satp_ppn_sv39_sz] 44-bit PPN are both present -- the address partition the walk in rv64im_min_mmu implements", split_ok, ctr)
228
229 // ---- PTE VALIDITY: the exact rule _mmu_gate's bad-PTE tamper exercises.
230 var bogus_pte_absent: i64 = 0
231 if ro_find(ub, un, RO_BOGUS_PTE) < 0 { bogus_pte_absent = 1 }
232 gv_check("neg-control-fabricated-pte-field-absent: a PTE field that does not exist (_pte_._z_) must NOT be found -- proving the tooth below matches the real rule and not any sentence shaped like it", bogus_pte_absent, ctr)
233
234 let ptev: i64 = ro_find(ub, un, RO_PTEV)
235 var pte_rule: i64 = 0
236 if ptev >= 0 {
237 // the fault clause must be on the SAME normative step, not merely somewhere in the chapter.
238 let fend: i64 = ro_find(ub, un, RO_PTEFAULT)
239 if fend > ptev { if fend - ptev < 400 { pte_rule = 1 } }
240 }
241 ro_p(" pte-validity rule offset=" as *u8); ro_n(ptev); ro_p("\n" as *u8)
242 gv_check("oracle-pte-validity: the spec's translation algorithm states that if _pte_._v_=0 the walk must STOP AND RAISE A PAGE-FAULT -- and the fault clause sits within the same normative step, not merely elsewhere in the chapter. This is exactly the rule _mmu_gate's T3 tamper exercises by clearing V on the leaf PTE and requiring the mapped VA to fault", pte_rule, ctr)
243 }
244
245 // ⚠THE CEILING IS NOW MIXED, AND SAYING SO IS THE POINT. This note originally read "NOT a
246 // re-derivation of the table's code column" -- accurate when the gate held only the mcause teeth,
247 // and FALSE the moment the satp tooth landed, because that one DOES read the code column. Two
248 // strengths now coexist and a single blanket ceiling would misdescribe one of them.
249 // ★★★★★★A CEILING WRITTEN FOR AN EARLIER VERSION OF A GATE IS A FALSE CLAIM WITH A TRUSTED BYLINE --
250 // AND THE DANGEROUS DIRECTION IS UNDERSTATEMENT, BECAUSE NOBODY AUDITS A CLAIM THAT SOUNDS MODEST.
251 // ⛔THIS NOTE DOES NOT ENUMERATE THE TEETH OR THEIR STRENGTHS, AND THAT IS DELIBERATE.
252 // It has now gone stale TWICE inside one session: written as "NOT a re-derivation of the code
253 // column" (falsified by the satp tooth), rewritten as "TWO STRENGTHS" (falsified by the normative-
254 // anchor and PTE teeth one turn later). Both times the CODE grew and the SUMMARY did not.
255 // ******A HAND-MAINTAINED SUMMARY BESIDE A GROWING TOOTH LIST IS A DUPLICATE RULER: IT WILL DRIFT,
256 // AND IT DRIFTS TOWARD UNDERSTATEMENT, WHICH NOBODY AUDITS. The fix is not a better sentence -- it is
257 // to STOP RESTATING WHAT THE TEETH ALREADY SAY. Every gv_check name below carries its own anchor
258 // strength (direct value / the spec's own norm: marker / positional order+gap), so the per-tooth
259 // output IS the summary and cannot fall out of date with itself.
260 return gv_verdict("RISCV-SPEC-ORACLE", ctr, "every constant these kernel gates rely on is corroborated against the OFFICIAL RISC-V privileged specification -- external ground truth this estate did not author. Each tooth above names the anchor strength it earned; read those, not a count. CORROBORATION IN ALL CASES, NEVER DERIVATION of our behaviour from the text")
261}