nx_gated_edit_multi_gate.nx source

1// nx_gated_edit_multi_gate.nx -- GATE for nx_gated_edit_multi (atomic multi-edit applier). 5 teeth incl the 2// KEY ATOMICITY proof (T4: edit1 valid + edit2 NOMATCH -> NEITHER applied, no partial write). PREREQ (staged 3// by build): ./nx_gated_edit_multi.elf + ./nx_ge_mockcat.elf. mock verify = cat(argv1). Verdict 0 iff 5/5. 4// license_tier: ORIGINAL No hw writes (Rule 26). 5import "nx_seat_drive_lib.nx" 6import "nx_seg_store.nx" 7import "nx_deploy_lib.nx" 8import "nx_ag_lib.nx" 9import "nx_syscalls.nx" 10 11func gm_run(src: *u8, man: *u8, velf: *u8, varg: *u8, outp: *u8) -> i64 { 12 let av: *i64 = sys_mmap(64) as *i64 13 av[0] = src as i64 14 av[1] = man as i64 15 av[2] = velf as i64 16 av[3] = varg as i64 17 return dep_run_capture("./nx_gated_edit_multi.elf" as *u8, av, 4, outp) 18} 19 20func main(argc: i64, argv: *i64) -> i64 { 21 var stage: i64 = 1 22 var pass: i64 = 0 23 if argc >= 2 { let ss1: *u8 = argv[1] as *u8; stage = ag_atoi(ss1) } 24 if argc >= 3 { let ps: *u8 = argv[2] as *u8; pass = ag_atoi(ps) } 25 if stage < 1 { stage = 1 } 26 27 ss_writefile("/tmp/gm_o1" as *u8, "AAA" as *u8, ag_len("AAA" as *u8)) 28 ss_writefile("/tmp/gm_n1" as *u8, "BBB" as *u8, ag_len("BBB" as *u8)) 29 ss_writefile("/tmp/gm_o2" as *u8, "CCC" as *u8, ag_len("CCC" as *u8)) 30 ss_writefile("/tmp/gm_n2" as *u8, "DDD" as *u8, ag_len("DDD" as *u8)) 31 ss_writefile("/tmp/gm_fixed" as *u8, "constant\n" as *u8, ag_len("constant\n" as *u8)) 32 ss_writefile("/tmp/gm_man2" as *u8, "/tmp/gm_o1\t/tmp/gm_n1\n/tmp/gm_o2\t/tmp/gm_n2\n" as *u8, ag_len("/tmp/gm_o1\t/tmp/gm_n1\n/tmp/gm_o2\t/tmp/gm_n2\n" as *u8)) 33 ss_writefile("/tmp/gm_manbad" as *u8, "/tmp/gm_o1\t/tmp/gm_n1\n/tmp/gm_ozz\t/tmp/gm_n2\n" as *u8, ag_len("/tmp/gm_o1\t/tmp/gm_n1\n/tmp/gm_ozz\t/tmp/gm_n2\n" as *u8)) 34 ss_writefile("/tmp/gm_man1" as *u8, "/tmp/gm_o1\t/tmp/gm_n1\n" as *u8, ag_len("/tmp/gm_o1\t/tmp/gm_n1\n" as *u8)) 35 36 if stage == 1 { 37 ss_writefile("/tmp/gm_src1" as *u8, "hello AAA and CCC\n" as *u8, ag_len("hello AAA and CCC\n" as *u8)) 38 let rc: i64 = gm_run("/tmp/gm_src1" as *u8, "/tmp/gm_man2" as *u8, "./nx_ge_mockcat.elf" as *u8, "/tmp/gm_fixed" as *u8, "/tmp/gm_t1.out" as *u8) 39 let sb: *u8 = sys_mmap(4096) 40 let m: i64 = ag_read("/tmp/gm_src1" as *u8, sb, 4096) 41 var ok: i64 = 0 42 if rc == 0 { if sd_count(sb, m, "BBB" as *u8) == 1 { if sd_count(sb, m, "DDD" as *u8) == 1 { if sd_count(sb, m, "AAA" as *u8) == 0 { ok = 1 } } } } 43 if ok == 1 { sd_w("T1 multi-consolidated PASS\n" as *u8); pass = pass + 1 } else { sd_w("T1 multi-consolidated FAIL\n" as *u8) } 44 } 45 if stage == 2 { 46 ss_writefile("/tmp/gm_src2" as *u8, "hello AAA and CCC\n" as *u8, ag_len("hello AAA and CCC\n" as *u8)) 47 let rc: i64 = gm_run("/tmp/gm_src2" as *u8, "/tmp/gm_man2" as *u8, "./nx_ge_mockcat.elf" as *u8, "/tmp/gm_src2" as *u8, "/tmp/gm_t2.out" as *u8) 48 let ob: *u8 = sys_mmap(4096) 49 let n: i64 = dp_read("/tmp/gm_t2.out" as *u8, ob, 4096) 50 let sb: *u8 = sys_mmap(4096) 51 let m: i64 = ag_read("/tmp/gm_src2" as *u8, sb, 4096) 52 var ok: i64 = 0 53 if rc == 1 { if sd_count(ob, n, "verdict=REFUSED" as *u8) == 1 { if sd_count(sb, m, "AAA" as *u8) == 1 { if sd_count(sb, m, "BBB" as *u8) == 0 { ok = 1 } } } } 54 if ok == 1 { sd_w("T2 neg-revert-all PASS\n" as *u8); pass = pass + 1 } else { sd_w("T2 neg-revert-all FAIL\n" as *u8) } 55 } 56 if stage == 3 { 57 let sb: *u8 = sys_mmap(4096) 58 let m: i64 = ag_read("/tmp/gm_src2" as *u8, sb, 4096) 59 let orig: *u8 = "hello AAA and CCC\n" as *u8 60 var ok: i64 = 0 61 if m == ag_len(orig) { 62 var same: i64 = 1 63 var i: i64 = 0 64 while i < m { if sb[i] != orig[i] { same = 0; i = m } else { i = i + 1 } } 65 if same == 1 { ok = 1 } 66 } 67 if ok == 1 { sd_w("T3 restore-byte-exact PASS\n" as *u8); pass = pass + 1 } else { sd_w("T3 restore-byte-exact FAIL\n" as *u8) } 68 } 69 if stage == 4 { 70 ss_writefile("/tmp/gm_src4" as *u8, "hello AAA and CCC\n" as *u8, ag_len("hello AAA and CCC\n" as *u8)) 71 let rc: i64 = gm_run("/tmp/gm_src4" as *u8, "/tmp/gm_manbad" as *u8, "./nx_ge_mockcat.elf" as *u8, "/tmp/gm_fixed" as *u8, "/tmp/gm_t4.out" as *u8) 72 let sb: *u8 = sys_mmap(4096) 73 let m: i64 = ag_read("/tmp/gm_src4" as *u8, sb, 4096) 74 var ok: i64 = 0 75 if rc == 2 { if sd_count(sb, m, "AAA" as *u8) == 1 { if sd_count(sb, m, "BBB" as *u8) == 0 { ok = 1 } } } 76 if ok == 1 { sd_w("T4 atomic-nomatch-no-partial PASS\n" as *u8); pass = pass + 1 } else { sd_w("T4 atomic-nomatch-no-partial FAIL\n" as *u8) } 77 } 78 if stage == 5 { 79 ss_writefile("/tmp/gm_src5" as *u8, "AAA AAA CCC\n" as *u8, ag_len("AAA AAA CCC\n" as *u8)) 80 let rc: i64 = gm_run("/tmp/gm_src5" as *u8, "/tmp/gm_man1" as *u8, "./nx_ge_mockcat.elf" as *u8, "/tmp/gm_fixed" as *u8, "/tmp/gm_t5.out" as *u8) 81 let sb: *u8 = sys_mmap(4096) 82 let m: i64 = ag_read("/tmp/gm_src5" as *u8, sb, 4096) 83 var ok: i64 = 0 84 if rc == 2 { if sd_count(sb, m, "BBB" as *u8) == 0 { if sd_count(sb, m, "AAA" as *u8) == 2 { ok = 1 } } } 85 if ok == 1 { sd_w("T5 ambiguous-untouched PASS\n" as *u8); pass = pass + 1 } else { sd_w("T5 ambiguous-untouched FAIL\n" as *u8) } 86 } 87 88 if stage >= 5 { 89 sd_w("NX-GEM-GATE pass=" as *u8) 90 let pb: *u8 = sys_mmap(8) 91 pb[0] = (48 + pass) as u8 92 pb[1] = 0 as u8 93 sd_w(pb) 94 if pass == 5 { sd_w("/5 verdict=GREEN\n" as *u8); sys_exit(0); return 0 } 95 sd_w("/5 verdict=RED\n" as *u8) 96 sys_exit(1) 97 return 1 98 } 99 100 let self: *u8 = argv[0] as *u8 101 let sb2: *u8 = sys_mmap(24) 102 ag_itoa(sb2, stage + 1) 103 let pb2: *u8 = sys_mmap(24) 104 ag_itoa(pb2, pass) 105 let nav: *i64 = sys_mmap(40) as *i64 106 nav[0] = self as i64 107 nav[1] = sb2 as i64 108 nav[2] = pb2 as i64 109 nav[3] = 0 110 let envp: *i64 = sys_mmap(16) as *i64 111 envp[0] = 0 112 sys_execve(self, nav, envp) 113 sd_w("GM-EXEC-FAIL\n" as *u8) 114 sys_exit(1) 115 return 1 116}