code wiki / _hdl_build / _coopsched_gate.nx
_coopsched_gate.nx source
↩ module page · 105 lines · 5610 B
1// _coopsched_gate.nx -- gate for the COOPERATIVE (yield-syscall) scheduler.
2// NO mocks: runs the REAL nx_coopsched_emit, RUNS the image on the SOVEREIGN rv64 emu, asserts the
3// serial CONTAINS the table-computed byte-exact golden "ABABABABABAB" (each task emitted then yielded
4// via ecall -> deterministic alternation) + clean finisher halt. TAMPER: corrupt task B's emit char
5// -> the alternation breaks ("ARAR.." not "ABAB..") -> golden absent -> RED (proves the yield really
6// switched to task B). Evidence -> knowledge/status/coopsched.log. license_tier: ORIGINAL
7import "nx_syscalls.nx"
8
9func 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 }
10func 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 }
11func g_fn(fd: i64, v: i64) -> i64 { let bb: *u8=sys_mmap(28); var m: i64=v; if m<0{m=0-m}; 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 }
12
13func g_run1(prog: *u8, arg1: *u8, outpath: *u8) -> i64 {
14 let pid: i64 = sys_fork()
15 if pid == 0 {
16 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) } }
17 else { let dn: i64 = sys_openat_wr("/dev/null" as *u8, 0x1a4); if dn >= 0 { sys_dup3(dn, 1, 0) } }
18 let argv: *i64 = sys_mmap(32) as *i64
19 argv[0] = prog as i64
20 if arg1 != (0 as *u8) { argv[1] = arg1 as i64; argv[2] = 0 } else { argv[1] = 0 }
21 let envp: *i64 = sys_mmap(16) as *i64
22 envp[0] = "PATH=/usr/bin:/bin" as *u8 as i64; envp[1] = 0
23 sys_execve(prog, argv, envp)
24 sys_exit(127)
25 }
26 let st: *i64 = sys_mmap(16) as *i64
27 sys_wait4(pid, st, 0)
28 return st[0]
29}
30
31func g_read(path: *u8, buf: *u8, cap: i64) -> i64 {
32 let fd: i64 = sys_openat_rd(path)
33 if fd < 0 { return 0 }
34 var n: i64 = 0
35 var go: i64 = 1
36 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 } }
37 sys_close(fd)
38 return n
39}
40
41func g_buf_has(buf: *u8, n: i64, pat: *u8, pl: i64) -> i64 {
42 if pl <= 0 { return 0 }
43 var i: i64 = 0
44 while i + pl <= n {
45 var k: i64 = 0
46 var hit: i64 = 1
47 while k < pl { if buf[i+k] != pat[k] { hit = 0; k = pl } else { k = k + 1 } }
48 if hit == 1 { return 1 }
49 i = i + 1
50 }
51 return 0
52}
53
54func main() -> i64 {
55 let binpath: *u8 = "runtime/_hdl_build/_coopsched_virt.bin" as *u8
56 let goldpath: *u8 = "runtime/_hdl_build/_coopsched_virt.bin.gold" as *u8
57 let tamper_bin: *u8 = "/tmp/_coopgate_tamper.bin" as *u8
58 let sov_serial: *u8 = "/tmp/_coopgate_sov.txt" as *u8
59 let sov_tamper: *u8 = "/tmp/_coopgate_tamper.txt" as *u8
60 g_p("=== cooperative-yield-scheduler gate (ecall-driven context switch: SOVEREIGN rv64 emu + tamper) ===\n" as *u8)
61 let lfd: i64 = sys_openat_append("knowledge/status/coopsched.log" as *u8, 0x1a4)
62
63 let est: i64 = g_run1("/tmp/nx_coopsched_emit.sov.elf" as *u8, 0 as *u8, 0 as *u8)
64 if est != 0 { g_p("COOPSCHEDGATE verdict=RED reason=emit-failed\n" as *u8); if lfd>=0 { g_fp(lfd,"COOPSCHEDGATE verdict=RED reason=emit-failed\n" as *u8); sys_close(lfd) } sys_exit(1); return 1 }
65 let gold: *u8 = sys_mmap(64)
66 let gn: i64 = g_read(goldpath, gold, 64)
67
68 let sst: i64 = g_run1("_offc/nx_boot_run_sov.elf" as *u8, binpath, sov_serial)
69 let sbuf: *u8 = sys_mmap(65536)
70 let sbn: i64 = g_read(sov_serial, sbuf, 65536)
71 let trans_ok: i64 = g_buf_has(sbuf, sbn, gold, gn)
72 let halt_ok: i64 = g_buf_has(sbuf, sbn, "BOOTSOV verdict=GREEN" as *u8, 21)
73 var sov_ok: i64 = 0
74 if sst == 0 { if trans_ok == 1 { if halt_ok == 1 { sov_ok = 1 } } }
75
76 // TAMPER: corrupt task B's emit char (addi t1,x0,'B' at byte 100; imm byte 103).
77 let ibuf: *u8 = sys_mmap(8192)
78 let ibn: i64 = g_read(binpath, ibuf, 8192)
79 ibuf[100 + 3] = (ibuf[100 + 3] + 1) as u8
80 let tfd: i64 = sys_openat_wr(tamper_bin, 0x1a4)
81 if tfd >= 0 { sys_write(tfd, ibuf, ibn); sys_close(tfd) }
82 let tst: i64 = g_run1("_offc/nx_boot_run_sov.elf" as *u8, tamper_bin, sov_tamper)
83 let tbuf: *u8 = sys_mmap(65536)
84 let tbn: i64 = g_read(sov_tamper, tbuf, 65536)
85 let tamper_trans: i64 = g_buf_has(tbuf, tbn, gold, gn)
86 var tamper_bites: i64 = 0
87 if tamper_trans == 0 { tamper_bites = 1 }
88
89 g_p(" sovereign_emu=" as *u8)
90 if sov_ok == 1 { g_p("GREEN(serial-contains-ABAB+clean-halt)" as *u8) } else { g_p("RED" as *u8) }
91 g_p(" tamper_bites=" as *u8)
92 if tamper_bites == 1 { g_p("yes\n" as *u8) } else { g_p("no\n" as *u8) }
93
94 var pass: i64 = 0
95 if sov_ok == 1 { if tamper_bites == 1 { pass = 1 } }
96 if pass == 1 {
97 g_p("COOPSCHEDGATE verdict=GREEN (sovereign rv64 emu: ecall-driven cooperative yield, deterministic ABAB round-robin; tamper REJECTED)\n" as *u8)
98 if lfd >= 0 { g_fp(lfd, "COOPSCHEDGATE verdict=GREEN runtime=sovereign-emu sched=cooperative-yield mechanism=ecall-yield-csrrw-mepc-swap tasks=2 tamper=rejected epoch=" as *u8); g_fn(lfd, sys_now_realtime_sec()); g_fp(lfd, "\n" as *u8); sys_close(lfd) }
99 sys_exit(0); return 0
100 }
101 g_p("COOPSCHEDGATE verdict=RED (sov_ok/tamper not both green)\n" as *u8)
102 if lfd >= 0 { g_fp(lfd, "COOPSCHEDGATE verdict=RED sov_ok=" as *u8); g_fn(lfd, sov_ok); g_fp(lfd, " tamper_bites=" as *u8); g_fn(lfd, tamper_bites); g_fp(lfd, "\n" as *u8); sys_close(lfd) }
103 sys_exit(1)
104 return 1
105}