nx_model_lane_gate.nx source
↩ module page · 79 lines · 4141 B
1// nx_model_lane_gate.nx -- gate for the sovereign model-lane lease. Deterministic, tiny-RAM,
2// test lease path only (never touches the real lane). Proves:
3// T1 claim -> free -> re-claim (lifecycle; pid=1 init = always alive)
4// T2 second claimant REFUSED while held (rc=10) -- the anti-OOM tooth
5// T3 stale holder (dead pid) is REAPED and the lane re-claimed (crash recovery)
6// T4 NEG headroom: absurd est_mb DENIED (rc=11) even though the lane is FREE
7// T5 NEG corrupt lease: garbage bytes -> claim REFUSES rc=14 (fail-loud, never steals)
8// T6 NEG free-by-non-holder REFUSED (rc=13)
9// license_tier: ORIGINAL expect_exit: 0
10import "nx_model_lane_core.nx"
11import "nx_gate_verdict.nx"
12
13func mg_write_raw(path: *u8, s: *u8) -> i64 {
14 let fd: i64 = sys_openat_wr(path, 420)
15 if fd < 0 { return 0 - 1 }
16 let n: i64 = std_slen(s)
17 sys_write(fd, s, n)
18 sys_close(fd)
19 return 0
20}
21
22func main(argc: i64, argv: *i64) -> i64 {
23 let lease: *u8 = "/tmp/mlane_gate.lease" as *u8
24 let ga: *u8 = "gateA" as *u8
25 let gb: *u8 = "gateB" as *u8
26 let gz: *u8 = "gateZ" as *u8
27 std_putln("MODEL-LANE-GATE: sovereign lease vs the shared-VM OOM collision class" as *u8)
28 ml_unlink(lease)
29 var pass: i64 = 0
30 // T1 lifecycle
31 let r1a: i64 = ml_claim(lease, ga, 100, 1, 3600, 0)
32 let r1b: i64 = ml_free(lease, ga)
33 let r1c: i64 = ml_claim(lease, ga, 100, 1, 3600, 0)
34 let r1d: i64 = ml_free(lease, ga)
35 if r1a == 0 && r1b == 0 && r1c == 0 && r1d == 0 { pass = pass + 1; std_putln("T1 PASS lifecycle" as *u8) }
36 if r1a != 0 || r1b != 0 || r1c != 0 || r1d != 0 { std_putln("T1 FAIL" as *u8) }
37 // T2 held -> second claimant refused
38 let r2a: i64 = ml_claim(lease, ga, 100, 1, 3600, 0)
39 let r2b: i64 = ml_claim(lease, gb, 100, 1, 3600, 0)
40 if r2a == 0 && r2b == 10 { pass = pass + 1; std_putln("T2 PASS second-claimant refused (anti-OOM tooth)" as *u8) }
41 if r2a != 0 || r2b != 10 { std_putln("T2 FAIL" as *u8) }
42 let r2c: i64 = ml_free(lease, ga)
43 if r2c != 0 { std_putln("T2 cleanup-warn" as *u8) }
44 // T3 stale dead-pid reap
45 let r3a: i64 = ml_claim(lease, ga, 100, 99999999, 3600, 0)
46 let r3b: i64 = ml_claim(lease, gb, 100, 1, 3600, 0)
47 if r3a == 0 && r3b == 0 { pass = pass + 1; std_putln("T3 PASS stale holder reaped, lane recovered" as *u8) }
48 if r3a != 0 || r3b != 0 { std_putln("T3 FAIL" as *u8) }
49 let r3c: i64 = ml_free(lease, gb)
50 if r3c != 0 { std_putln("T3 cleanup-warn" as *u8) }
51 // T4 NEG headroom denied on a FREE lane
52 let r4: i64 = ml_claim(lease, ga, 999999999, 1, 3600, 0)
53 if r4 == 11 { pass = pass + 1; std_putln("T4 PASS NEG headroom denied" as *u8) }
54 if r4 != 11 { std_puts("T4 FAIL rc=" as *u8); std_pdec(r4); std_puts("\n" as *u8) }
55 // T5 NEG corrupt lease refuses (never steals)
56 mg_write_raw(lease, "not a lease record at all\n" as *u8)
57 let r5: i64 = ml_claim(lease, gb, 100, 1, 3600, 0)
58 if r5 == 14 { pass = pass + 1; std_putln("T5 PASS NEG corrupt lease fail-loud" as *u8) }
59 if r5 != 14 { std_puts("T5 FAIL rc=" as *u8); std_pdec(r5); std_puts("\n" as *u8) }
60 ml_unlink(lease)
61 // T6 NEG free by non-holder refused
62 let r6a: i64 = ml_claim(lease, ga, 100, 1, 3600, 0)
63 let r6b: i64 = ml_free(lease, gz)
64 let r6c: i64 = ml_free(lease, ga)
65 if r6a == 0 && r6b == 13 && r6c == 0 { pass = pass + 1; std_putln("T6 PASS NEG non-holder free refused" as *u8) }
66 if r6a != 0 || r6b != 13 || r6c != 0 { std_putln("T6 FAIL" as *u8) }
67 ml_unlink(lease)
68 std_puts("MODEL-LANE-GATE pass=" as *u8)
69 std_pdec(pass)
70 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
71 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
72 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
73 let ctr__dry: *i64 = gv_ctr()
74 ctr__dry[0] = pass
75 ctr__dry[1] = 6
76 let rc__dry: i64 = gv_verdict("MODEL-LANE-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
77 sys_exit(rc__dry)
78 return rc__dry
79}