`_mmu_gate.nx` source

↩ module page · 204 lines · 11540 B
1// _mmu_gate.nx -- gate for the Sv39 PAGE-TABLE-WALK device (virtual-memory-paging-mmu).  NO mocks.
2//
3//   (1) WALK WORKS -- emits the MMU driver (via nx_drv_proto_emit) + runs it on the sovereign emu:
4//       it lays a Sv39 gigapage page table, programs satp, and the device WALKS the table -> the
5//       mapped VA 0xC0009000 translates to PA 0x80009000 ("MAP") and an unmapped VA faults ("FLT").
6//       Serial must contain "MAPFLT" + a clean halt.
7//   (2) TAMPER device-base -- bump the device-base lui imm (byte 7): the MMU regs are missed, the
8//       walk never runs, "MAP" drops (the driver really talks to the MMU device).
9//   (3) TAMPER bad-PTE -- run the variant whose leaf PTE has V=0: the mapped VA walk FAULTS, the
10//       PADDR verify fails, "MAP" drops -> the Sv39 walk genuinely reads + validates the page table
11//       (translation is not a rubber stamp).
12//
13// Evidence -> knowledge/status/mmu.log (MMUGATE row).  Sovereign.  license_tier: ORIGINAL
14import "nx_syscalls.nx"
15import "nx_gate_verdict.nx"
16
17const M_EMIT: *u8 = "_offc/nx_drv_proto_emit.elf"
18const M_SOV:  *u8 = "_offc/nx_boot_run_sov.elf"
19const M_SPEC: *u8 = "knowledge/specs/drv_proto_mmu.spec"
20const M_BIN:  *u8 = "runtime/_hdl_build/_drv_proto_mmu.bin"
21const M_BADSPEC: *u8 = "knowledge/specs/drv_proto_mmu_badpte.spec"
22const M_BADBIN:  *u8 = "runtime/_hdl_build/_drv_proto_mmu_badpte.bin"
23
24func g_p(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
25func g_fp(fd: i64, s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(fd,s,n); return 0 }
26func g_fn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m;sys_write(fd,"-" as *u8,1)}; let t: *u8=sys_mmap(28); var k: i64=0; if m==0{t[0]=48;k=1}; while m>0{t[k]=(48+(m%10)) as u8;m=m/10;k=k+1}; var i: i64=0; while i<k{bb[i]=t[k-1-i];i=i+1}; sys_write(fd,bb,k); return 0 }
27
28func g_run(prog: *u8, a1: *u8, outpath: *u8) -> i64 {
29    let pid: i64 = sys_fork()
30    if pid == 0 {
31        if outpath != (0 as *u8) { let ofd: i64 = sys_openat_wr(outpath, 0x1a4); if ofd >= 0 { sys_dup3(ofd, 1, 0); sys_dup3(ofd, 2, 0) } }
32        let argv: *i64 = sys_mmap(32) as *i64
33        argv[0] = prog as i64
34        var k: i64 = 1
35        if a1 != (0 as *u8) { argv[k] = a1 as i64; k = k + 1 }
36        argv[k] = 0
37        let envp: *i64 = sys_mmap(16) as *i64
38        envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0
39        sys_execve(prog, argv, envp)
40        sys_exit(127)
41    }
42    let st: *i64 = sys_mmap(16) as *i64
43    sys_wait4(pid, st, 0)
44    let sg: i64 = st[0] & 0x7f
45    if sg != 0 { return 128 + sg }
46    return (st[0] >> 8) & 0xff
47}
48
49func g_read(path: *u8, buf: *u8, cap: i64) -> i64 {
50    let fd: i64 = sys_openat_rd(path)
51    if fd < 0 { return 0 }
52    var n: i64 = 0
53    var go: i64 = 1
54    while go == 1 { let r: i64 = sys_read(fd, (buf as i64 + n) as *u8, cap - 1 - n); if r <= 0 { go = 0 } else { n = n + r } if n >= cap - 1 { go = 0 } }
55    sys_close(fd)
56    return n
57}
58
59func g_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 {
60    if pl <= 0 { return 0 }
61    var i: i64 = 0
62    while i + pl <= n { var k: i64=0; var hit: i64=1; while k<pl { if buf[i+k]!=pat[k]{hit=0;k=pl}else{k=k+1} } if hit==1 { return 1 } i=i+1 }
63    return 0
64}
65
66func g_emit_run(spec: *u8, bin: *u8, serial: *u8) -> i64 {
67    if g_run(M_EMIT, spec, "/tmp/_mmu_emit.out" as *u8) != 0 { return 0 }
68    g_run(M_SOV, bin, serial)
69    let sb: *u8 = sys_mmap(65536); let sn: i64 = g_read(serial, sb, 65536)
70    let halt: i64 = g_has(sb, sn, "BOOTSOV verdict=GREEN" as *u8, 21)
71    let mapflt: i64 = g_has(sb, sn, "MAPFLT" as *u8, 6)
72    if halt == 1 { if mapflt == 1 { return 1 } }
73    return 0
74}
75
76// Scan ONLY the emulator's serial line for `pat`.  Returns 1=present, 0=absent, -1=NO SERIAL LINE.
77//
78// ★FIXED 2026-08-07.  This used to grep the WHOLE captured file.  That is unsafe by construction:
79// on a transcript mismatch nx_boot_run_sov prints the EXPECTED GOLDEN INLINE --
80//     BOOTSOV verdict=RED reason=transcript-mismatch ... expected=[MAPFLT] got=[]
81// -- so a whole-file search for "MAP" finds the EMULATOR'S OWN DIAGNOSTIC and an absence tooth
82// INVERTS.  MEASURED: tooth 3 (bad-PTE) read FAIL for exactly this reason while the driver was
83// behaving perfectly -- the serial really was empty, and the word MAP the tooth found was the
84// runner quoting what it had hoped to see.
85// A DETECTOR THAT GREPS A WHOLE LOG FOR A TOKEN BREAKS THE DAY THE LOG STARTS QUOTING THAT TOKEN.
86//
87// -1 is deliberately DISTINCT from 0: "I could not find the serial line" is not "the token was
88// absent".  Every caller below tests `== 0`, so a -1 never silently credits an absence tooth.
89func g_serial_has(serial: *u8, pat: *u8, pl: i64) -> i64 {
90    if pl <= 0 { return 0 - 1 }
91    let sb: *u8 = sys_mmap(65536); let sn: i64 = g_read(serial, sb, 65536)
92    let key: *u8 = "SOVEREIGN-EMU serial: " as *u8
93    var kl: i64 = 0
94    while key[kl] != (0 as u8) { kl = kl + 1 }
95    var i: i64 = 0
96    var start: i64 = 0 - 1
97    var scan: i64 = 1
98    while scan == 1 {
99        if i + kl > sn { scan = 0 } else {
100            var k: i64 = 0
101            var hit: i64 = 1
102            while k < kl { if sb[i+k] != key[k] { hit = 0; k = kl } else { k = k + 1 } }
103            if hit == 1 { start = i + kl; scan = 0 } else { i = i + 1 }
104        }
105    }
106    if start < 0 { return 0 - 1 }
107    var e: i64 = start
108    var go: i64 = 1
109    while go == 1 {
110        if e >= sn { go = 0 } else {
111            if sb[e] == (10 as u8) { go = 0 } else { e = e + 1 }
112        }
113    }
114    var j: i64 = start
115    while j + pl <= e {
116        var k2: i64 = 0
117        var h2: i64 = 1
118        while k2 < pl { if sb[j+k2] != pat[k2] { h2 = 0; k2 = pl } else { k2 = k2 + 1 } }
119        if h2 == 1 { return 1 }
120        j = j + 1
121    }
122    return 0
123}
124
125func g_has_map(serial: *u8) -> i64 {
126    return g_serial_has(serial, "MAP" as *u8, 3)
127}
128
129func main() -> i64 {
130    g_p("=== Sv39 page-table-walk gate (virtual-memory-paging-mmu) ===\n" as *u8)
131    let lfd: i64 = sys_openat_append("knowledge/status/mmu.log" as *u8, 0x1a4)
132
133    // (1) walk works: mapped VA translates (MAP) + unmapped faults (FLT)
134    let walk_ok: i64 = g_emit_run(M_SPEC, M_BIN, "/tmp/_mmu_main.txt" as *u8)
135
136    // (2) tamper device base (byte 7): MMU regs missed -> MAP drops
137    let ib: *u8 = sys_mmap(16384); let ibn: i64 = g_read(M_BIN, ib, 16384)
138    var t1: i64 = 0
139    if ibn > 7 {
140        ib[7] = (ib[7] + 1) as u8
141        let tfd: i64 = sys_openat_wr("/tmp/_mmu_t1.bin" as *u8, 0x1a4)
142        if tfd >= 0 { sys_write(tfd, ib, ibn); sys_close(tfd) }
143        g_run(M_SOV, "/tmp/_mmu_t1.bin" as *u8, "/tmp/_mmu_t1.txt" as *u8)
144        // ANTI-VACUITY 2026-08-06 (see the longer note on tooth 3): a tooth that asserts an ABSENCE
145        // passes loudest when nothing ran. Only credit a disappearance we can prove we CAUSED: the
146        // baseline must have worked, and this tamper run must have produced a serial transcript.
147        let t1b: *u8 = sys_mmap(65536)
148        let t1n: i64 = g_read("/tmp/_mmu_t1.txt" as *u8, t1b, 65536)
149        if walk_ok == 1 { if t1n > 0 { if g_has_map("/tmp/_mmu_t1.txt" as *u8) == 0 { t1 = 1 } } }
150    }
151
152    // (3) tamper bad-PTE variant: leaf PTE V=0 -> mapped VA faults -> MAP drops
153    let bad_emit: i64 = g_run(M_EMIT, M_BADSPEC, "/tmp/_mmu_bad_emit.out" as *u8)
154    g_run(M_SOV, M_BADBIN, "/tmp/_mmu_bad.txt" as *u8)
155    var t2: i64 = 0
156    // ANTI-VACUITY 2026-08-06. This tooth asserts an ABSENCE -- "MAP is gone" -- so it scores PASS
157    // MAXIMALLY when nothing executed at all. MEASURED: knowledge/specs/drv_proto_mmu_badpte.spec and
158    // drv_proto_mmu.spec are BOTH ABSENT, so the emit fails, _drv_proto_mmu_badpte.bin is never built,
159    // /tmp/_mmu_bad.txt is never written -- and the old form read that empty nothing, found no "MAP",
160    // and reported PASS. The gate therefore scored 1/3 while its true state was 0/3-cannot-run, and the
161    // one tooth it credited was the one that had proven the least.
162    // A TOOTH THAT ASSERTS AN ABSENCE PASSES LOUDEST WHEN NOTHING RAN AT ALL. It may only credit a
163    // disappearance it can prove it CAUSED: the baseline worked, the emit succeeded, and this run
164    // actually produced a transcript.
165    var bad_ran: i64 = 0
166    let bb2: *u8 = sys_mmap(65536)
167    let bn2: i64 = g_read("/tmp/_mmu_bad.txt" as *u8, bb2, 65536)
168    if bad_emit == 0 { if bn2 > 0 { bad_ran = 1 } }
169    if walk_ok == 1 { if bad_ran == 1 { if g_has_map("/tmp/_mmu_bad.txt" as *u8) == 0 { t2 = 1 } } }
170
171    g_p("  walk_works=" as *u8); if walk_ok==1 { g_p("GREEN(MAP=mapped-VA->PA, FLT=unmapped-faults)" as *u8) } else { g_p("RED" as *u8) }
172    g_p(" tamper_base=" as *u8); g_fn(1, t1); g_p(" tamper_badpte=" as *u8); g_fn(1, t2); g_p("\n" as *u8)
173
174    // ---- D001 MIGRATION 2026-08-06 -- IDIOM G: BOOLEAN CONJUNCTION, NO COUNTER --------------------
175    // This gate scored a boolean AND-chain into ONE flag and printed its own verdict, so nx_gate_green
176    // could not judge it, it recorded no harness frame, and /api/promote refused it -- which in turn
177    // stranded its registry row on an unpromoted .sov.elf.new (the stagedref class).
178    // nx_gate_dry_apply SKIPS this shape with "counter idiom not recognised", and the reason is
179    // STRUCTURAL: idioms A-F all assume a pass/total COUNTER PAIR to map onto ctr[0]/ctr[1], and this
180    // gate HAS NO COUNTER AT ALL. Measured 2026-08-06: 8 of 8 D001-blocked gates skip -- 6 for exactly
181    // this reason -- so "migrate it" was a remedy with no automated path for this whole family.
182    // THE FAITHFUL MAPPING IS ONE gv_check PER CONJUNCT: that CREATES the counter, and gv_verdict is
183    // GREEN iff pass==total, which is precisely the old `walk_ok && t1 && t2`. The three teeth below are
184    // the SAME three conditions computed above -- NO test logic changed, only who reports the verdict.
185    let ctr: *i64 = gv_ctr()
186    gv_check("T1 Sv39 walk works (mapped VA 0xC0009000 -> PA 0x80009000 [MAP]; unmapped VA FAULTS [FLT])" as *u8, walk_ok, ctr)
187    gv_check("T2 tamper device-base REJECTED (bumped lui imm -> MMU regs missed -> MAP drops)" as *u8, t1, ctr)
188    gv_check("T3 tamper bad-PTE REJECTED (leaf PTE V=0 -> mapped VA faults -> MAP drops)" as *u8, t2, ctr)
189    let rc: i64 = gv_verdict("MMUGATE" as *u8, ctr, "sovereign Sv39 page-table walk: programmed satp + a gigapage page table in guest RAM; the MMU WALKED the 3-level table, translated the mapped VA 0xC0009000 -> PA 0x80009000 [MAP] and FAULTED an unmapped VA [FLT]; device-base and bad-PTE[V=0] tampers both drop MAP, so the walk genuinely reads+validates the page table. probe=virtual-memory-paging" as *u8)
190    // The knowledge/status/mmu.log evidence row is PRESERVED in both branches, byte-for-byte with the
191    // pre-migration text. The rollup reads that file; a migration that quietly stopped writing it would
192    // have traded a D001 refusal for an INVISIBLE gate, which is a strictly worse outcome.
193    if lfd >= 0 {
194        if rc == 0 {
195            g_fp(lfd, "MMUGATE verdict=GREEN keystone=virtual-memory-paging probe=mmu_paging sv39-walk=3-level mapped=0xC0009000->0x80009000 fault=unmapped tamper=rejected(base+badpte) epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8)
196        }
197        if rc != 0 {
198            g_fp(lfd, "MMUGATE verdict=RED walk=" as *u8); g_fn(lfd, walk_ok); g_fp(lfd, " t1=" as *u8); g_fn(lfd, t1); g_fp(lfd, " t2=" as *u8); g_fn(lfd, t2); g_fp(lfd, "\n" as *u8)
199        }
200        sys_close(lfd)
201    }
202    sys_exit(rc)
203    return rc
204}
_mmu_gate.nx source

`_mmu_gate.nx` source
