nx_ship_fleet_gate.nx source
↩ module page · 59 lines · 4116 B
1// nx_ship_fleet_gate.nx -- bite-proves the PURE adaptive-concurrency core in nx_shipfleet_lib.nx: the AIMD
2// cap state machine (additive-increase +1 on progress, multiplicative-decrease halve on a storm, ceilinged
3// by the polite budget, floored at 1) and the effective-width gate (pause on serve-first or admission-deny,
4// else min(budget,cap)). The DRIVER's fork/wait4 pool is I/O and cannot be unit-tested here; the load-bearing
5// DECISIONS are pure and are all tested. Every tooth is an equality on a pure function, so a mutant that
6// (a) grows on a storm, (b) ignores the ceiling, (c) drops below 1, or (d) launches while serving/refused
7// is KILLED. license_tier: ORIGINAL
8// evidence -> stdout + verdict line (exit code carries the verdict via gv_verdict).
9import "nx_syscalls.nx"
10import "nx_gate_verdict.nx"
11import "nx_shipfleet_lib.nx"
12
13func main() -> i64 {
14 let c: *i64 = gv_ctr()
15
16 // ---- AIMD additive increase -------------------------------------------------------------------
17 gv_check("aimd-OK-grows-by-one" as *u8, sf_aimd_next(1, 8, SF_OK) == 2, c)
18 gv_check("aimd-OK-caps-at-ceiling" as *u8, sf_aimd_next(8, 8, SF_OK) == 8, c)
19 gv_check("aimd-OK-never-exceeds-ceiling" as *u8, sf_aimd_next(7, 8, SF_OK) == 8, c)
20
21 // ---- AIMD multiplicative decrease -------------------------------------------------------------
22 gv_check("aimd-storm-halves" as *u8, sf_aimd_next(8, 8, SF_STORM) == 4, c)
23 gv_check("aimd-storm-floors-at-one" as *u8, sf_aimd_next(1, 8, SF_STORM) == 1, c)
24 gv_check("aimd-storm-of-3-floors-to-1" as *u8, sf_aimd_next(3, 8, SF_STORM) == 1, c) // 3/2=1
25
26 // ---- AIMD hold / ceiling clamp ---------------------------------------------------------------
27 gv_check("aimd-hold-keeps-cap" as *u8, sf_aimd_next(4, 8, SF_HOLD) == 4, c)
28 gv_check("aimd-hold-clamps-over-ceiling" as *u8, sf_aimd_next(10, 8, SF_HOLD) == 8, c)
29
30 // ---- effective width: PAUSE conditions -------------------------------------------------------
31 gv_check("width-pauses-on-serve-first" as *u8, sf_effective_width(8, 4, 1, 1) == 0, c)
32 gv_check("width-pauses-on-admit-deny" as *u8, sf_effective_width(8, 4, 0, 0) == 0, c)
33 gv_check("width-serve-first-dominates-grant" as *u8, sf_effective_width(8, 4, 1, 1) == 0, c)
34
35 // ---- effective width: the min(budget, cap) --------------------------------------------------
36 gv_check("width-cap-binds" as *u8, sf_effective_width(8, 3, 1, 0) == 3, c)
37 gv_check("width-budget-binds" as *u8, sf_effective_width(2, 5, 1, 0) == 2, c)
38
39 // ---- launch slots ---------------------------------------------------------------------------
40 gv_check("slots-are-width-minus-inflight" as *u8, sf_launch_slots(5, 2) == 3, c)
41 gv_check("slots-never-negative" as *u8, sf_launch_slots(2, 5) == 0, c)
42
43 // ---- END-TO-END trajectory (anti-vacuity: both behaviours in one run) ------------------------
44 // start at 1, drive OK to the ceiling, then one storm must HALVE it -- the whole point of the fleet.
45 var cap: i64 = 1
46 var i: i64 = 0
47 while i < 20 { cap = sf_aimd_next(cap, 8, SF_OK); i = i + 1 }
48 gv_check("trajectory-converges-to-ceiling" as *u8, cap == 8, c)
49 let after_storm: i64 = sf_aimd_next(cap, 8, SF_STORM)
50 gv_check("trajectory-storm-halves-from-ceiling" as *u8, after_storm == 4, c)
51
52 // ---- NEGATIVE CONTROLS: a storm must NEVER grow the cap, and the ceiling must never be exceeded.
53 // A mutant that treated SF_STORM as SF_OK would grow the cap -> these teeth fail. A mutant that
54 // dropped the ceiling clamp would let OK exceed it -> the caps teeth fail.
55 gv_check("neg-control-storm-must-not-grow" as *u8, sf_aimd_next(4, 8, SF_STORM) <= 4, c)
56 gv_check("neg-control-storm-strictly-shrinks-when-above-1" as *u8, sf_aimd_next(6, 8, SF_STORM) < 6, c)
57
58 return gv_verdict("SHIP-FLEET-GATE" as *u8, c, "adaptive-concurrency AIMD core: +1 on progress, halve on storm, ceiling=polite budget, floor=1, pause on serve-first/admit-deny" as *u8)
59}