code wiki / _hdl_build / nx_deploy_marker_gate.nx
nx_deploy_marker_gate.nx source
↩ module page · 58 lines · 3379 B
1import "nx_gate_gn.nx"
2// nx_deploy_marker_gate.nx -- hermetic gate for CAP-DEPLOY-MARKER (the self-safe deferred-restart primitive).
3// Proves: a deploy can request a restart WITHOUT restarting in-request; the supervisor consumes it EXACTLY ONCE
4// (so one request never loops); an absent marker means nothing pending; and a fresh request re-arms cleanly.
5// T1 request -> pending T2 consume -> restart-now (1) T3 second consume -> 0 (no loop) + not pending
6// T4 (NEG) no marker -> 0 T5 re-request re-arms -> consume 1 again
7// Sovereign: nx_syscalls + nx_deploy_marker. license_tier: ORIGINAL expect_exit: 0
8import "nx_syscalls.nx"
9import "nx_deploy_marker.nx"
10import "nx_gate_verdict.nx"
11
12func gp(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
13
14func main(argc: i64, argv: *i64) -> i64 {
15 gp("=== nx_deploy_marker_gate (self-safe deploy: stage+request, supervisor consumes once) ===\n" as *u8)
16 let DIR: *u8 = "/tmp" as *u8
17 let SVC: *u8 = "gate_mgmt_api" as *u8
18 let NONE: *u8 = "gate_no_such_svc_zzz" as *u8
19 var pass: i64 = 0; var fail: i64 = 0
20
21 // ensure a clean slate: consume any stale marker from a prior run
22 dm_check_and_consume(DIR, SVC)
23
24 // T1 request -> pending
25 let r1: i64 = dm_request_restart(DIR, SVC)
26 let p1: i64 = dm_is_pending(DIR, SVC)
27 if r1 == 1 { if p1 == 1 { pass=pass+1; gp(" T1 deploy requests restart -> pending PASS\n" as *u8) } else { fail=fail+1; gp(" T1 FAIL not pending\n" as *u8) } } else { fail=fail+1; gp(" T1 FAIL request\n" as *u8) }
28
29 // T2 consume -> restart now
30 let c1: i64 = dm_check_and_consume(DIR, SVC)
31 if c1 == 1 { pass=pass+1; gp(" T2 supervisor consumes -> restart-now(1) PASS\n" as *u8) } else { fail=fail+1; gp(" T2 FAIL\n" as *u8) }
32
33 // T3 second consume -> 0 (no loop) + no longer pending
34 let c2: i64 = dm_check_and_consume(DIR, SVC)
35 let p2: i64 = dm_is_pending(DIR, SVC)
36 if c2 == 0 { if p2 == 0 { pass=pass+1; gp(" T3 consumed exactly once -> 0, not pending (NO restart loop) PASS\n" as *u8) } else { fail=fail+1; gp(" T3 FAIL still pending\n" as *u8) } } else { fail=fail+1; gp(" T3 FAIL looped\n" as *u8) }
37
38 // T4 (NEG) absent marker -> 0
39 let c3: i64 = dm_check_and_consume(DIR, NONE)
40 if c3 == 0 { pass=pass+1; gp(" T4 no marker -> 0 (nothing pending) PASS\n" as *u8) } else { fail=fail+1; gp(" T4 FAIL\n" as *u8) }
41
42 // T5 re-request re-arms
43 dm_request_restart(DIR, SVC)
44 let c4: i64 = dm_check_and_consume(DIR, SVC)
45 if c4 == 1 { pass=pass+1; gp(" T5 a fresh deploy re-arms -> consume 1 again PASS\n" as *u8) } else { fail=fail+1; gp(" T5 FAIL\n" as *u8) }
46 dm_check_and_consume(DIR, SVC) // leave clean
47
48 gp("RESULT pass=" as *u8); gn(pass); gp(" fail=" as *u8); gn(fail)
49 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check
50 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled
51 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify.
52 let ctr__dry: *i64 = gv_ctr()
53 ctr__dry[0] = pass
54 ctr__dry[1] = pass + fail
55 let rc__dry: i64 = gv_verdict("DEPLOY-MARKER-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8)
56 sys_exit(rc__dry)
57 return rc__dry
58}