| 1 | package engines |
| 2 | |
| 3 | import ( |
| 4 | "os" |
| 5 | "strings" |
| 6 | ) |
| 7 | |
| 8 | // Every protocol rule the model enforces has a name here. The mutation |
| 9 | // harness runs one prebuilt test binary with ENGINESIM_MUTATE set to one |
| 10 | // rule name (or a comma-separated combination), and requires at least one |
| 11 | // seed to fail. A rule whose mutation no seed catches is either redundant or |
| 12 | // untested, and the run says which. |
| 13 | // |
| 14 | // Never edit `mutated` in place; the harness sets ENGINESIM_MUTATE. |
| 15 | var mutated = "" |
| 16 | |
| 17 | // ENGINESIM_MUTATE sets `mutated` for one run of a prebuilt test binary, so |
| 18 | // the mutation harness never edits or copies the source (mutate.sh). |
| 19 | func init() { |
| 20 | if v := os.Getenv("ENGINESIM_MUTATE"); v != "" { |
| 21 | mutated = v |
| 22 | } |
| 23 | } |
| 24 | |
| 25 | // on reports whether a rule is enforced: false only when the mutation set |
| 26 | // names it. |
| 27 | func on(rule string) bool { |
| 28 | for _, m := range strings.Split(mutated, ",") { |
| 29 | if m == rule { |
| 30 | return false |
| 31 | } |
| 32 | } |
| 33 | return true |
| 34 | } |
| 35 | |
| 36 | // allRules is the mutation list. Each task appends its rules, in spec order, |
| 37 | // with a comment naming the spec section each answers. |
| 38 | var allRules = []string{ |
| 39 | // Task 2: the fence and the launch gate, I1 (spec §5.1 "The invariant", |
| 40 | // "Setting the mark: the serving barrier", "What the edge does with it", |
| 41 | // "Starts systemd makes on its own"; §5.9 the box-wide fence; §6.3) |
| 42 | "set-before-repoint", // adoption gates before it repoints the live link (R2-1) |
| 43 | "fence-needs-reload", // a failed reload advances nothing (R10-1) |
| 44 | "fence-drains-admitted", // the fence cancels public requests admitted before the swap (R3-1) |
| 45 | "fence-box-wide", // ... on every row of the box, deleted rows included (§5.9, R13-2) |
| 46 | "gate-adopt", // the gate on adoption's restart |
| 47 | "gate-swap", // ... on a swap's incoming generation (R7-1) |
| 48 | "gate-fallback", // ... on a wake plan's fallback build (R9-1) |
| 49 | "gate-recovery", // ... on a wake plan's recovery build (R9-1) |
| 50 | "gate-seed", // ... on a seed |
| 51 | "gate-cmd", // ... on a carlos run command |
| 52 | "gate-waits-when-written", // the gate waits for the fence when 1 is already written (R10-1) |
| 53 | "unreadable-declares", // an unreadable manifest is treated as declaring |
| 54 | "live-link-only-adoption", // nothing but adoption (and --public) moves a live link (R11) |
| 55 | "mark-on-final-upstream", // the edge checks the final resolved upstream's row (R1-2) |
| 56 | |
| 57 | // Task 3: classification, minted groups, the operator clear (spec §5.1 |
| 58 | // "The column", "Platform-minted rows", "Becoming public is never |
| 59 | // automatic", "Classification before serving"; §6.3) |
| 60 | "classify-null-refused", // the edge refuses NULL like 1 (R2-2) |
| 61 | "classify-staged", // the upgrade classifies 1 if any staged version declares (R8-1) |
| 62 | "minted-follow-owner", // a minted instance row is in its owner's group: one mark, one barrier (R5-1) |
| 63 | "grant-marks-group", // a grant on any row of the group marks the group (R6-1) |
| 64 | "static-minted-public", // a minted static row is 0 by construction, never classified (R6-2) |
| 65 | "owner-nonempty-unique", // the owner fallback matches only non-empty backends, and only uniquely (R7-2) |
| 66 | "public-checks-live", // --public step 1: the live manifest is readable and does not declare |
| 67 | "public-stops-group", // --public step 2: stop the whole group (R7-1, R8-2) |
| 68 | "public-holds-lock", // --public holds the group's lock: adoption cannot move the live link under it |
| 69 | "public-confirms-empty", // --public step 3: refuse unless every cgroup of the group is empty |
| 70 | |
| 71 | // Task 4: the dedicated engine box and ingress (spec §5.9; §5.1 "The |
| 72 | // edge is the only ingress") |
| 73 | "ports-excluded", // doc_engine with ports refused at ship; no listener for an internal group (R11-1) |
| 74 | "dedicated-launch-check", // a declaring launch is refused on a box with a proxying row outside its group (R12-2) |
| 75 | "dedicated-edge-refusal", // the edge refuses every proxying row outside the internal group homed on its box (R12-2) |
| 76 | "ingress-precondition", // the operator's firewall admits only the edge's ports, from every source (R12-1, R13-1) |
| 77 | |
| 78 | // Task 5: calls, identity, grants and arming (spec §5.2 the signed |
| 79 | // record; §5.3 the grant mirror; §5.4 the call path; §6.1, §6.2, §6.4) |
| 80 | "cgroup-identity", // the engine socket admits only a process in its own instance's slice (R1-1) |
| 81 | "door-uid", // the door makes an engine call only for a uid other than carlos (R2-3) |
| 82 | "hop-caller-signed", // the engine box takes the caller only from a MAC-verified hop; the header is stripped elsewhere |
| 83 | "engine-box-recheck", // the engine box checks its own grant table, whatever the calling box admitted (G4) |
| 84 | "exact-route-engine", // an engine call reaches only the engine hostname's own route, never through a path map (R4-2) |
| 85 | "floor-persisted", // the mirror's revision floor and record survive a restart (R1-4) |
| 86 | "stale-clears-grants", // a stale, expired or never-read table grants nothing (§5.3, §6.4) |
| 87 | "armed-refuses-unisolated", // an armed box refuses flat, foreign and worker launches before they start (R3-2, R4-1) |
| 88 | "arm-checks-box", // arming refuses a box with an unisolated route or a non-empty carlos-exec@ cgroup (R5-2) |
| 89 | |
| 90 | // Final review (spec §5.1 "The invariant", "Becoming public is never |
| 91 | // automatic"; §5.2, §5.3 the freshness bound, ruling R5) |
| 92 | "new-group-fenced", // a new or unseen row's NULL is never fenced: a first declaring launch writes 1 and waits for the fence |
| 93 | "clear-launch-lock", // the launch gate takes the group's lock, which --public holds for its whole run |
| 94 | "grant-freshness-bound", // a record signed ten minutes ago or more is stale: the mirror refuses it and the table is empty |
| 95 | } |
| 96 | |
amadan