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}