amadan
enginesim: the dedicated engine box and ingress (#335 plan 1)
Spec §5.9 and §5.1 "The edge is the only ingress": four rules, ports-excluded, dedicated-launch-check, dedicated-edge-refusal and ingress-precondition (a world flag), with service rows (local and remote), an engine binding its own port, ports releases and the capability pass, direct connections past the edge, and the operator removing a route. A NULL route homes its box like 1 (TestNullRouteHomesTheBox: otherwise a request admitted beside a release-less NULL route outlives a declaring launch there). INV-AV exempts proxying rows outside the group homed on their box. The dedicated-box rules mask three Task 3 witnesses alone: classify-staged app scope now needs dedicated-launch-check; minted-follow-owner's adoption witness needs both dedicated rules (a grant witness keeps it caught alone); owner-nonempty-unique's INV-AV became an INV-P witness behind dedicated-edge-refusal.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
6 files changed,
+812
−32
internal/sim/engines/dedicated_test.go+495 −0internal/sim/engines/edge_test.go+10 −0internal/sim/engines/launch_test.go+3 −0internal/sim/engines/rules_test.go+7 −0internal/sim/engines/witness_test.go+290 −31internal/sim/engines/world_test.go+7 −1
diff --git a/internal/sim/engines/dedicated_test.go b/internal/sim/engines/dedicated_test.go| new file mode 100644 |
| index 000000000..d666bb39f |
| --- /dev/null |
| +++ b/internal/sim/engines/dedicated_test.go |
| @@ -0,0 +1,495 @@ |
| +package engines |
| + |
| +import ( |
| + "fmt" |
| + "sort" |
| + "strings" |
| +) |
| + |
| +// The dedicated engine box and ingress (spec §5.9 "The engine box is |
| +// dedicated"; §5.1 "The edge is the only ingress"). |
| +// |
| +// I1 keeps a declaring build from starting before the edge refuses the |
| +// public, but the edge is not the only way to a process on its box. These |
| +// rules close the others: |
| +// |
| +// - ports-excluded: a release declaring doc_engine and ports is refused at |
| +// ship, and the box renders no ListenStream for an internal group. The |
| +// capability pass removes an existing one whenever the group's mark |
| +// closes (writeMark calls dropListeners), so it is gone before any fence |
| +// of that write completes. |
| +// - dedicated-launch-check: a declaring launch is refused on a box with a |
| +// proxying row outside its group (the gate, before it writes or waits). |
| +// - dedicated-edge-refusal: while an internal group is homed on the box, |
| +// the edge gives every proxying row outside that group the internal |
| +// refusal. |
| +// - ingress-precondition: the operator's firewall admits connections from |
| +// every source, public or private (the deployment's other boxes too), |
| +// only on the edge's ports and the ports the operator granted. It is a |
| +// world flag, not a box mechanism: the platform cannot see it. |
| +// |
| +// A proxying row is an instance or service row with a backend: the edge |
| +// proxies it to a process. Static rows (and the status host, the tunnel and |
| +// steering handlers, which the model does not have) are answered by the edge |
| +// itself. Alias rows and path maps resolve to their final row, and the edge |
| +// checks that one. |
| + |
| +// ---------- addresses ---------- |
| + |
| +// A TCP backend is on a box by its subnet, 10.0.<box>.<n>:<port>; a socket |
| +// path or 127.0.0.1 is reachable on its own box only. |
| + |
| +// boxAddr is box b's address. |
| +func boxAddr(b *box) string { return fmt.Sprintf("10.0.%d.1", b.ID) } |
| + |
| +// addrBox is the box an address backend is on, and its port; nil for a |
| +// socket path, loopback, or an address on no box. |
| +func (w *world) addrBox(backend string) (*box, string) { |
| + i := strings.LastIndex(backend, ":") |
| + if strings.HasPrefix(backend, "/") || i < 0 { |
| + return nil, "" |
| + } |
| + for _, b := range w.boxes { |
| + if strings.HasPrefix(backend[:i], fmt.Sprintf("10.0.%d.", b.ID)) { |
| + return b, backend[i+1:] |
| + } |
| + } |
| + return nil, "" |
| +} |
| + |
| +// ownPort is the port process p binds on its own, if it does (OwnPort). |
| +func ownPort(p *proc) string { return fmt.Sprint(20000 + p.ID) } |
| + |
| +// bindOwnPort is process p binding a port of its own on every interface: |
| +// the unit template allows it and the capability validator leaves high |
| +// ports to the app (spec §5.9, codex R12-1). |
| +func (w *world) bindOwnPort(b *box, p *proc) { |
| + p.OwnPort = true |
| + w.logf("box%d: process %d (%s v%d) binds port %s on every interface", b.ID, p.ID, p.Group, p.Ver, ownPort(p)) |
| +} |
| + |
| +// newest is group g's newest process on b, or nil. |
| +func (w *world) newest(b *box, g string) *proc { |
| + var p *proc |
| + for _, x := range b.Procs { |
| + if x.Group == g { |
| + p = x |
| + } |
| + } |
| + return p |
| +} |
| + |
| +// ---------- service rows ---------- |
| + |
| +// proxying: the edge proxies the row to a process. |
| +func proxying(r *row) bool { |
| + return (r.Kind == "instance" || r.Kind == "service") && r.Backend != "" |
| +} |
| + |
| +// addServiceRow is `carlos add` of a service row on box b whose upstream is |
| +// backend: a socket path or address on b, or, from box 1, box 0's address. |
| +// A service row is 0 by construction. |
| +func (w *world) addServiceRow(b *box, host, backend string) { |
| + b.Rows[host] = &row{Host: host, Kind: "service", Backend: backend, PathTo: map[string]string{}} |
| + b.Mark[host] = markPublic |
| + b.Wrote++ |
| + w.logf("box%d: registry change %d: service row %s -> %s", b.ID, b.Wrote, host, backend) |
| +} |
| + |
| +// deleteRow removes a service row. A request admitted through it keeps the |
| +// proxy it holds (the fence's business, fence-box-wide). |
| +func (w *world) deleteRow(b *box, host string) { |
| + delete(b.Rows, host) |
| + delete(b.Mark, host) |
| + b.Wrote++ |
| + w.logf("box%d: registry change %d: row %s deleted", b.ID, b.Wrote, host) |
| +} |
| + |
| +// removeGroup is the operator removing instance route g from b, as the |
| +// dedicated-box refusal's log line tells them to: its processes stop, its |
| +// rows and the rows minted from it go, and so do its listeners. The app's |
| +// staged versions stay on the box (/opt/carlos/versions is per app): any |
| +// recorded under g pass to another instance of the app. |
| +func (w *world) removeGroup(b *box, g string) { |
| + others := []string{} |
| + for _, h := range w.appGroups(b, g) { |
| + if h != g { |
| + others = append(others, h) |
| + } |
| + } |
| + if len(others) > 0 { |
| + for _, v := range b.Staged[g] { |
| + b.Staged[others[0]] = append(b.Staged[others[0]], v) |
| + } |
| + } |
| + w.stopGroup(b, g) |
| + for _, h := range hostsOf(b) { |
| + if r := b.Rows[h]; h == g || (r.Platform && r.Source == g) { |
| + delete(b.Rows, h) |
| + delete(b.Mark, h) |
| + } |
| + } |
| + for port, lg := range b.Listen { |
| + if lg == g { |
| + delete(b.Listen, port) |
| + } |
| + } |
| + delete(b.Live, g) |
| + delete(b.Good, g) |
| + delete(b.Staged, g) |
| + delete(b.SetAt, g) |
| + delete(b.PortGrant, g) |
| + b.Wrote++ |
| + w.logf("box%d: registry change %d: route %s removed with its minted rows", b.ID, b.Wrote, g) |
| +} |
| + |
| +// ---------- the dedicated box ---------- |
| + |
| +// dedicatedLaunchCheck is the launch gate's check before it writes or waits |
| +// for anything: a declaring launch in group g is refused while any proxying |
| +// row of the box's registry belongs to another group, and each such row is |
| +// named with the move or remove command. |
| +func (w *world) dedicatedLaunchCheck(b *box, g string, ver int, path string) bool { |
| + if !on("dedicated-launch-check") { |
| + return true |
| + } |
| + var outside []string |
| + for _, h := range hostsOf(b) { |
| + if r := b.Rows[h]; proxying(r) && w.group(b, h) != g { |
| + outside = append(outside, h) |
| + } |
| + } |
| + for _, h := range outside { |
| + w.logf("box%d: gate(%s) %s v%d: %s row %s proxies outside the group on the box that would home an engine; move or remove it", b.ID, path, g, ver, b.Rows[h].Kind, h) |
| + } |
| + if len(outside) > 0 { |
| + w.logf("box%d: gate(%s) %s v%d: refused: the box is not dedicated", b.ID, path, g, ver) |
| + return false |
| + } |
| + return true |
| +} |
| + |
| +// edgeHomed is every internal group homed on b, as the edge's map has it: a |
| +// group whose own route the edge serves 1 or NULL. The edge refuses NULL like |
| +// 1 (classify-null-refused), and so does this rule, release or not: a gate |
| +// writing 1 over a NULL group finds it fenced already and bumps no epoch, so |
| +// a request admitted through a row beside a NULL route would outlive a |
| +// declaring launch there (TestNullRouteHomesTheBox). The cost: a NULL route |
| +// on a shared box (an upgrade that cannot read its live manifest, a |
| +// provisioned route whose declaring first adoption the launch check refused) |
| +// takes every proxying neighbour out of service until it is classified. |
| +func (w *world) edgeHomed(b *box) map[string]bool { |
| + homed := map[string]bool{} |
| + for h, r := range b.EdgeRows { |
| + if r.Kind != "instance" || r.Platform { |
| + continue |
| + } |
| + if m := b.Serving[h]; m == markInternal || (m == markNull && on("classify-null-refused")) { |
| + homed[h] = true |
| + } |
| + } |
| + return homed |
| +} |
| + |
| +// dedicatedRefusal is the edge's refusal of final, the row a public request |
| +// resolved to: on a box that homes an internal group, a proxying row of any |
| +// other group gets the internal refusal. It returns why, or "" when the row |
| +// is served. |
| +func (w *world) dedicatedRefusal(b *box, final row) string { |
| + if !on("dedicated-edge-refusal") || !proxying(&final) { |
| + return "" |
| + } |
| + homed := w.edgeHomed(b) |
| + if len(homed) == 0 || homed[edgeGroup(b, final.Host)] { |
| + return "" |
| + } |
| + return fmt.Sprintf("%s row %s proxies outside %v, the internal group homed on the box; move or remove it", final.Kind, final.Host, sortedKeys(homed)) |
| +} |
| + |
| +func sortedKeys(m map[string]bool) []string { |
| + out := make([]string, 0, len(m)) |
| + for k := range m { |
| + out = append(out, k) |
| + } |
| + sort.Strings(out) |
| + return out |
| +} |
| + |
| +// ---------- ports ---------- |
| + |
| +// ship is `carlos ship` of build ver's release for group g, its capability |
| +// block declaring ports or not, then its adoption on b. A ports release |
| +// records the operator's grant (a port) and the capability pass runs. |
| +func (w *world) ship(b *box, g string, ver int, ports bool) bool { |
| + if ports && w.builds[ver].Declares && on("ports-excluded") { |
| + w.logf("ship %s v%d: refused: the release declares doc_engine and ports together", g, ver) |
| + return false |
| + } |
| + if !w.adopt(b, g, ver, nil) { |
| + return false |
| + } |
| + if ports && b.PortGrant[g] == "" { |
| + w.nextID++ |
| + b.PortGrant[g] = fmt.Sprint(40000 + w.nextID) |
| + w.logf("box%d: %s holds a ports grant: port %s", b.ID, g, b.PortGrant[g]) |
| + } |
| + w.capsPass(b) |
| + return true |
| +} |
| + |
| +// capsPass is the agent's capability pass: it renders each granted port's |
| +// ListenStream, except for a route of an internal group, whose listener it |
| +// removes. It fails closed: the route's own mark or any row of its group |
| +// being 1 or NULL is enough. |
| +func (w *world) capsPass(b *box) { |
| + gs := make([]string, 0, len(b.PortGrant)) |
| + for g := range b.PortGrant { |
| + gs = append(gs, g) |
| + } |
| + sort.Strings(gs) |
| + for _, g := range gs { |
| + if on("ports-excluded") && (b.Mark[g] != markPublic || w.closed(b, g)) { |
| + w.dropListeners(b, g) |
| + continue |
| + } |
| + if port := b.PortGrant[g]; b.Listen[port] != g { |
| + b.Listen[port] = g |
| + w.logf("box%d: capability pass renders ListenStream=%s for %s", b.ID, port, g) |
| + } |
| + } |
| +} |
| + |
| +// dropListeners removes group g's ListenStream sockets, stopping their |
| +// socket units, and logs the grant it is ignoring. writeMark calls it on |
| +// every write of 1 or NULL. |
| +func (w *world) dropListeners(b *box, g string) { |
| + if !on("ports-excluded") { |
| + return |
| + } |
| + ports := make([]string, 0, len(b.Listen)) |
| + for port, lg := range b.Listen { |
| + if lg == g { |
| + ports = append(ports, port) |
| + } |
| + } |
| + sort.Strings(ports) |
| + for _, port := range ports { |
| + delete(b.Listen, port) |
| + w.logf("box%d: %s is internal: ListenStream=%s removed, its ports grant ignored (revoke it with carlos caps)", b.ID, g, port) |
| + } |
| +} |
| + |
| +// ---------- ingress ---------- |
| + |
| +// directConnect is a connection to port on box b that does not go through |
| +// b's edge: from the internet, or from another box (a service row there |
| +// aimed at b's address). A ports listener takes it whatever the firewall |
| +// flag (the operator granted that port, so the firewall admits it); a stopped |
| +// unit is socket-activated from its live link. Otherwise it reaches a process |
| +// only if the ingress precondition is violated: one bound to the port on its |
| +// own, or a TCP route's backend. |
| +func (w *world) directConnect(b *box, port string, public bool) *proc { |
| + return w.connect(b, port, public, true) |
| +} |
| + |
| +// connect is directConnect, or with firewalled false the box's own traffic |
| +// (a local row's proxy to an address on its own box), which no firewall sees. |
| +func (w *world) connect(b *box, port string, public, firewalled bool) *proc { |
| + src := "private" |
| + if public { |
| + src = "public" |
| + } |
| + if g, ok := b.Listen[port]; ok { |
| + w.logf("box%d: %s connection to port %s: the ports listener of %s", b.ID, src, port, g) |
| + w.socketActivate(b, g) |
| + return w.reach(b, w.newest(b, g), public, "the ports listener on "+port) |
| + } |
| + if firewalled && on("ingress-precondition") { |
| + w.logf("box%d: %s connection to port %s: refused by the firewall (the edge's ports only)", b.ID, src, port) |
| + return nil |
| + } |
| + return w.reach(b, w.portProc(b, port), public, "port "+port) |
| +} |
| + |
| +// portProc is the process listening on port on b: one bound to it on its |
| +// own, else the newest process of the TCP route whose backend it is. |
| +func (w *world) portProc(b *box, port string) *proc { |
| + for i := len(b.Procs) - 1; i >= 0; i-- { |
| + if p := b.Procs[i]; p.OwnPort && ownPort(p) == port { |
| + return p |
| + } |
| + } |
| + for _, h := range hostsOf(b) { |
| + r := b.Rows[h] |
| + if r.Kind != "instance" || r.Platform { |
| + continue |
| + } |
| + if tb, pt := w.addrBox(r.Backend); tb == b && pt == port { |
| + return w.newest(b, w.group(b, h)) |
| + } |
| + } |
| + return nil |
| +} |
| + |
| +// reach records a connection past the edge reaching process p. INV-P, as in |
| +// deliver: a public connection never reaches a declaring build, nor a group |
| +// holding a loaded doc-engine grant. |
| +func (w *world) reach(b *box, p *proc, public bool, how string) *proc { |
| + if p == nil { |
| + w.logf("box%d: %s: nothing listens", b.ID, how) |
| + return nil |
| + } |
| + w.logf("box%d: %s reached process %d (%s v%d) past the edge", b.ID, how, p.ID, p.Group, p.Ver) |
| + if public && w.builds[p.Ver].Declares { |
| + w.fail("INV-P", "box%d: a public connection through %s reached process %d of %s running v%d, which declares doc_engine, past the edge", b.ID, how, p.ID, p.Group, p.Ver) |
| + } else if g := w.grantLoaded(b, p.Group); public && g != "" { |
| + w.fail("INV-P", "box%d: a public connection through %s reached process %d of %s running v%d, whose group holds the doc-engine grant (on %s), past the edge", b.ID, how, p.ID, p.Group, p.Ver, g) |
| + } |
| + return p |
| +} |
| + |
| +// deliverDirect is the proxy of request r on b whose backend is an address |
| +// no instance row of b carries: on another box, a direct connection there |
| +// (the firewall decides); on b itself, the process bound to that port. False |
| +// when the backend is no such address. |
| +func (w *world) deliverDirect(b *box, r *req) bool { |
| + tb, port := w.addrBox(r.Backend) |
| + if tb == nil { |
| + return false |
| + } |
| + w.logf("box%d: request %d proxies to %s, box%d's address", b.ID, r.ID, r.Backend, tb.ID) |
| + if p := w.connect(tb, port, r.Public, tb != b); p != nil { |
| + r.Reached = p.ID |
| + } |
| + return true |
| +} |
| + |
| +// ---------- INV-AV ---------- |
| + |
| +// A proxying row outside the internal group homed on its box is refused by |
| +// the dedicated-box rule on purpose (spec §5.9): INV-AV does not count it. |
| +// The row's true group decides, not the edge's resolution. |
| +func init() { |
| + avExemptions = append(avExemptions, func(w *world, b *box, host string) string { |
| + r := b.Rows[host] |
| + if r == nil || !proxying(r) { |
| + return "" |
| + } |
| + homed := w.edgeHomed(b) |
| + if len(homed) == 0 || homed[truthGroup(b, host)] { |
| + return "" |
| + } |
| + return fmt.Sprintf("a proxying row outside %v, the internal group homed on the box: refused by design (§5.9)", sortedKeys(homed)) |
| + }) |
| +} |
| + |
| +// ---------- the random walk ---------- |
| + |
| +// addressablePorts is every port on b a direct connection can name: TCP |
| +// routes' backends, ports processes bound on their own, ports listeners. |
| +func (w *world) addressablePorts(b *box) []string { |
| + set := map[string]bool{} |
| + for _, h := range hostsOf(b) { |
| + if r := b.Rows[h]; r.Kind == "instance" && !r.Platform { |
| + if tb, port := w.addrBox(r.Backend); tb == b { |
| + set[port] = true |
| + } |
| + } |
| + } |
| + for _, p := range b.Procs { |
| + if p.OwnPort { |
| + set[ownPort(p)] = true |
| + } |
| + } |
| + for port := range b.Listen { |
| + set[port] = true |
| + } |
| + return sortedKeys(set) |
| +} |
| + |
| +// localBackends is every upstream a local service row on b can name: its |
| +// instance routes' backends and the ports on b's own address. |
| +func (w *world) localBackends(b *box) []string { |
| + set := map[string]bool{"127.0.0.1:1": true} // nothing listens |
| + for _, h := range hostsOf(b) { |
| + if r := b.Rows[h]; r.Kind == "instance" && !r.Platform && r.Backend != "" { |
| + set[r.Backend] = true |
| + } |
| + } |
| + for _, port := range w.addressablePorts(b) { |
| + set[boxAddr(b)+":"+port] = true |
| + } |
| + return sortedKeys(set) |
| +} |
| + |
| +func init() { |
| + actions = append(actions, |
| + action{name: "add-service-row", weight: 2, run: func(w *world) { |
| + b := w.pickBox() |
| + if len(b.Rows) >= maxRows { |
| + return |
| + } |
| + w.nextID++ |
| + host := fmt.Sprintf("svc%d.example", w.nextID) |
| + if b.ID == 1 && w.rng.Intn(2) == 0 { |
| + // aimed at box 0's address (codex R13-1) |
| + ports := append(w.addressablePorts(w.boxes[0]), "1") |
| + w.addServiceRow(b, host, boxAddr(w.boxes[0])+":"+ports[w.rng.Intn(len(ports))]) |
| + return |
| + } |
| + bs := w.localBackends(b) |
| + w.addServiceRow(b, host, bs[w.rng.Intn(len(bs))]) |
| + }}, |
| + action{name: "delete-service-row", weight: 2, run: func(w *world) { |
| + type at struct { |
| + b *box |
| + host string |
| + } |
| + var rows []at |
| + for _, b := range w.boxes { |
| + for _, h := range hostsOf(b) { |
| + if b.Rows[h].Kind == "service" { |
| + rows = append(rows, at{b, h}) |
| + } |
| + } |
| + } |
| + if len(rows) == 0 { |
| + return |
| + } |
| + x := rows[w.rng.Intn(len(rows))] |
| + w.deleteRow(x.b, x.host) |
| + }}, |
| + action{name: "own-port", weight: 1, run: func(w *world) { |
| + b := w.pickBox() |
| + if len(b.Procs) == 0 { |
| + return |
| + } |
| + w.bindOwnPort(b, b.Procs[w.rng.Intn(len(b.Procs))]) |
| + }}, |
| + action{name: "direct-connect", weight: 2, run: func(w *world) { |
| + b := w.pickBox() |
| + ports := append(w.addressablePorts(b), "1") |
| + w.directConnect(b, ports[w.rng.Intn(len(ports))], true) |
| + }}, |
| + action{name: "ship-ports", weight: 1, run: func(w *world) { |
| + b := w.pickBox() |
| + if g := w.pickGroup(b); g != "" { |
| + w.ship(b, g, w.pickVer(), true) |
| + } |
| + }}, |
| + action{name: "caps-pass", weight: 1, run: func(w *world) { w.capsPass(w.pickBox()) }}, |
| + action{name: "remove-route", weight: 1, run: func(w *world) { |
| + // an instance route the walk added (the starting eng and shop stay) |
| + b := w.pickBox() |
| + var gs []string |
| + for _, g := range w.groups(b) { |
| + if g != eng && g != "shop" { |
| + gs = append(gs, g) |
| + } |
| + } |
| + if len(gs) > 0 { |
| + w.removeGroup(b, gs[w.rng.Intn(len(gs))]) |
| + } |
| + }}, |
| + ) |
| +} |
diff --git a/internal/sim/engines/edge_test.go b/internal/sim/engines/edge_test.go| index 0a79413a5..9145be3c5 100644 |
| --- a/internal/sim/engines/edge_test.go |
| +++ b/internal/sim/engines/edge_test.go |
| @@ -84,6 +84,9 @@ func (w *world) writeMark(b *box, g string, m mark) { |
| b.SetAt[g] = b.Wrote |
| } |
| w.logf("box%d: registry change %d: %s marked %v", b.ID, b.Wrote, g, m) |
| + if m != markPublic { |
| + w.dropListeners(b, g) // before any fence of this write (ports-excluded) |
| + } |
| } |
| // fenced: the edge's fenced counter has reached the registry change that set |
| @@ -214,6 +217,10 @@ func (w *world) admit(b *box, host, path string) (*req, string) { |
| w.logf("box%d: public %s%s: answered by the edge (%s)", b.ID, host, path, final.Host) |
| return nil, answered |
| } |
| + if why := w.dedicatedRefusal(b, final); why != "" { |
| + w.logf("box%d: public %s%s: internal refusal: %s", b.ID, host, path, why) |
| + return nil, refused |
| + } |
| w.nextID++ |
| r := &req{ID: w.nextID, Epoch: b.Epoch, Row: checked.Host, Backend: final.Backend, Public: true, Box: b.ID} |
| b.Admitted = append(b.Admitted, r) |
| @@ -261,6 +268,9 @@ func (w *world) deliver(r *req) { |
| b.Admitted = append(b.Admitted[:idx], b.Admitted[idx+1:]...) |
| r.Held = false |
| g := w.backendGroup(b, r.Backend) |
| + if g == "" && w.deliverDirect(b, r) { |
| + return |
| + } |
| var p *proc |
| for _, x := range b.Procs { |
| if x.Group == g && g != "" { |
diff --git a/internal/sim/engines/launch_test.go b/internal/sim/engines/launch_test.go| index 1ad5ce395..e8c5943f5 100644 |
| --- a/internal/sim/engines/launch_test.go |
| +++ b/internal/sim/engines/launch_test.go |
| @@ -49,6 +49,9 @@ func (w *world) gate(b *box, g string, ver int, path string) bool { |
| if !w.gateSeesDeclaring(ver) { |
| return true |
| } |
| + if !w.dedicatedLaunchCheck(b, g, ver, path) { |
| + return false |
| + } |
| wrote := false |
| if w.groupMark(b, g) != markInternal { |
| w.writeMark(b, g, markInternal) |
diff --git a/internal/sim/engines/rules_test.go b/internal/sim/engines/rules_test.go| index a022424d1..8cf130086 100644 |
| --- a/internal/sim/engines/rules_test.go |
| +++ b/internal/sim/engines/rules_test.go |
| @@ -67,4 +67,11 @@ var allRules = []string{ |
| "public-stops-group", // --public step 2: stop the whole group (R7-1, R8-2) |
| "public-holds-lock", // --public holds the adoption lock: the live link cannot move under it |
| "public-confirms-empty", // --public step 3: refuse unless every cgroup of the group is empty |
| + |
| + // Task 4: the dedicated engine box and ingress (spec §5.9; §5.1 "The |
| + // edge is the only ingress") |
| + "ports-excluded", // doc_engine with ports refused at ship; no listener for an internal group (R11-1) |
| + "dedicated-launch-check", // a declaring launch is refused on a box with a proxying row outside its group (R12-2) |
| + "dedicated-edge-refusal", // the edge refuses every proxying row outside the internal group homed on its box (R12-2) |
| + "ingress-precondition", // the operator's firewall admits only the edge's ports, from every source (R12-1, R13-1) |
| } |
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go| index a7e70bf89..562ce1142 100644 |
| --- a/internal/sim/engines/witness_test.go |
| +++ b/internal/sim/engines/witness_test.go |
| @@ -67,16 +67,18 @@ var witnesses = []witness{ |
| "R2-2: the engine runs a declaring build whose live manifest cannot be read; the upgrade leaves it NULL; an edge that serves NULL like 0 admits a public request into the engine", wClassifyNullRefused}, |
| {"classify-staged", "classify-staged", "INV-I1+INV-P", |
| "R8-1: an awake engine is repointed to a plain build without a restart, so the declaring build still runs; an upgrade that reads only the live manifest classifies the group 0, under the running engine (INV-I1) and a public request reaches it (INV-P)", wClassifyStaged}, |
| - {"classify-staged", "classify-staged", "INV-I1+INV-P", |
| - "R8-1, app scope: two instances of one app; the declaring build is staged once, by the other instance; this one runs it from that copy, is repointed to a plain build without a restart and upgraded; read per group, or without the staged clause, it classifies 0 under the running engine", wClassifyStagedApp}, |
| - {"minted-follow-owner", "minted-follow-owner", "INV-P", |
| + {"classify-staged", "classify-staged,dedicated-launch-check", "INV-I1", |
| + "R8-1, app scope: two instances of one app; the declaring build is staged once, by the other instance; this one runs it from that copy, is repointed to a plain build without a restart and upgraded; read per group, or without the staged clause, it classifies 0 under the running engine. Since Task 4 the launch check refuses the second instance's declaring adoption (another group's row on the box), so it needs that check gone too, and the edge's dedicated refusal keeps the public out (INV-I1 only)", wClassifyStagedApp}, |
| + {"minted-follow-owner", "minted-follow-owner,dedicated-launch-check,dedicated-edge-refusal", "INV-P", |
| "R5-1: an app minted a platform row while public; adoption of a declaring build marks and fences the app; a minted row that is its own group stays 0 and a public request by the minted host reaches the engine", wMintedFollowOwner}, |
| + {"minted-follow-owner", "minted-follow-owner", "INV-P", |
| + "R5-1, by the grant: --grant doc-engine on the minted row of a public app; a minted row that is its own group takes the mark alone, and a public request by the app's own host reaches the granted app", wMintedFollowOwnerGrant}, |
| {"grant-marks-group", "grant-marks-group", "INV-P", |
| "R6-1: --grant doc-engine on the minted row of a plain release; a grant that marks only when it is on the owner's own row leaves the group 0, and a public request by the minted host reaches the granted app", wGrantMarksGroup}, |
| {"static-minted-public", "static-minted-public", "INV-AV", |
| "R6-2: a static app with a minted row and a canary; an upgrade that classifies minted static rows like instance rows leaves them NULL, and they never answer (liveness)", wStaticMintedPublic}, |
| - {"owner-nonempty-unique", "owner-nonempty-unique", "INV-AV", |
| - "R7-2: two TCP instances of one app, the plain one's minted row minted before owners were recorded; a fallback that matches empty sockets puts the row in the engine's group, which marks it 1, so a public row never answers; with the rule, a match that is not unique is refused and logged, and INV-AV does not count it", wOwnerNonEmptyUnique}, |
| + {"owner-nonempty-unique", "owner-nonempty-unique,dedicated-edge-refusal", "INV-P", |
| + "R7-2: an engine instance's minted row was minted before owners were recorded; a fallback that matches empty sockets puts it in the group of a later plain instance of the app, so --public on that instance writes 0 on the engine's minted row. Since Task 4 its availability effect is gone (a misgrouped row on a box that homes a closed group is refused by design either way) and its safety effect needs the edge's dedicated refusal gone too: a public request by the minted host reaches the engine", wOwnerNonEmptyUnique}, |
| {"public-checks-live", "public-checks-live", "INV-I1+INV-P", |
| "--public on a group whose live release declares; without step 1 the clear writes 0, and systemd's socket activation starts the declaring live build ungated (INV-I1) for a public request (INV-P)", wPublicChecksLive}, |
| {"public-stops-group", "public-stops-group,public-confirms-empty", "INV-I1+INV-P", |
| @@ -85,6 +87,18 @@ var witnesses = []witness{ |
| "the clear's stop does not complete and leaves the declaring generation running; without step 3 the clear writes 0 under it (INV-I1) and a public request reaches it (INV-P)", wPublicConfirmsEmpty}, |
| {"public-holds-lock", "public-holds-lock", "INV-I1+INV-P", |
| "--public checks a plain live release; without the adoption lock, adoption repoints to a declaring build before the stop; the clear writes 0 over a declaring live link, and socket activation starts it ungated", wPublicHoldsLock}, |
| + |
| + // Task 4: the dedicated engine box and ingress |
| + {"ports-excluded", "ports-excluded", "INV-P", |
| + "R11-1: the engine route holds a port grant from a plain release, so the box renders its listener; adoption of a declaring build marks the group; a box that keeps the listener lets a public connection to the port, which the firewall admits as granted, reach the engine past the edge", wPortsExcluded}, |
| + {"dedicated-launch-check", "dedicated-launch-check,dedicated-edge-refusal", "INV-P", |
| + "R12-2: redundant alone: a service row aimed at the engine's backend exists before a declaring adoption; the launch check refuses the adoption; without it the edge's refusal still refuses the row once the group is internal; with both gone a public request through the row reaches the engine", wDedicatedLaunchCheck}, |
| + {"dedicated-edge-refusal", "dedicated-edge-refusal", "INV-P", |
| + "R12-2: a service row aimed at the engine's backend is added after the engine runs internal, where no launch check sees it; an edge that serves it lets a public request reach the engine", wDedicatedEdgeRefusal}, |
| + {"ingress-precondition", "ingress-precondition", "INV-P", |
| + "R13-1: a service row on the calling box aimed at the engine box's address; a firewall that admits it lets a public request through the calling box's edge reach the engine directly", wIngressPrivate}, |
| + {"ingress-precondition", "ingress-precondition", "INV-P", |
| + "R12-1: the engine binds a port of its own on every interface; a firewall that admits it lets a public connection reach the engine", wOwnPort}, |
| } |
| // TestWitnesses is the deterministic half of the mutation evidence. |
| @@ -592,12 +606,22 @@ func wClassifyStaged(t *testing.T, w *world) { |
| // first; tcp-b, another instance of the app, adopts the same build (staged |
| // for the app already, so recorded under tcp-a only), is repointed to a |
| // plain build without a restart, and the agent upgrades. |
| +// |
| +// Since Task 4 the launch check refuses tcp-b's declaring adoption beside |
| +// tcp-a (a proxying row of another group): the model has no era before the |
| +// upgrade in which launches pass no gate, so this scenario needs the launch |
| +// check gone too. The edge's dedicated refusal then still refuses tcp-b's |
| +// public request (tcp-a is homed internal), so it violates INV-I1 only. |
| func wClassifyStagedApp(t *testing.T, w *world) { |
| - b := w.boxes[0] |
| + b := w.engineFreeBox(t) |
| if !w.provision(b, tcpA, tcpApp, "10.0.0.7:9101", vEngine) || !w.provision(b, tcpB, tcpApp, "10.0.0.7:9102", vPlain) { |
| t.Fatalf("witness: provisioning refused: %s", w.boxesState()) |
| } |
| if !w.adopt(b, tcpB, vEngine, nil) { |
| + if on("dedicated-launch-check") { |
| + w.logf("witness: the launch check refuses %s's declaring adoption beside %s; on a dedicated box the scenario cannot arise", tcpB, tcpA) |
| + return |
| + } |
| t.Fatalf("witness: adoption of the declaring build refused: %s", w.boxesState()) |
| } |
| w.check() |
| @@ -648,22 +672,43 @@ func (w *world) tcpPublic(t *testing.T, b *box) { |
| // wMintedFollowOwner (R5-1): a public app with a minted row adopts a |
| // declaring build; a public request arrives by the minted host. |
| +// |
| +// Since Task 4 a minted row that is its own group is a proxying row of |
| +// another group: the launch check refuses the adoption beside it, and the |
| +// edge's dedicated refusal refuses it once the app is internal. The witness |
| +// needs both gone with minted-follow-owner. |
| func wMintedFollowOwner(t *testing.T, w *world) { |
| - b := w.boxes[0] |
| + b := w.engineFreeBox(t) |
| w.tcpPublic(t, b) |
| if !w.adopt(b, tcpB, vEngine, nil) { |
| - t.Fatalf("witness: adoption of the declaring build refused: %s", w.boxesState()) |
| + if on("minted-follow-owner") || !on("dedicated-launch-check") { |
| + t.Fatalf("witness: adoption of the declaring build refused: %s", w.boxesState()) |
| + } |
| + w.logf("witness: the minted row, its own group, is another group's row beside %s; the launch check refuses the adoption", tcpB) |
| + return |
| } |
| w.check() |
| w.requestBy(b, mintedB) |
| w.check() |
| } |
| +// wMintedFollowOwnerGrant (R5-1, by the grant): a public app of a plain |
| +// build with a minted row; the operator grants doc-engine on the minted row; |
| +// a public request arrives by the app's own host. |
| +func wMintedFollowOwnerGrant(t *testing.T, w *world) { |
| + b := w.engineFreeBox(t) |
| + w.tcpPublic(t, b) |
| + w.grant(b, mintedB) |
| + w.check() |
| + w.requestBy(b, tcpB) |
| + w.check() |
| +} |
| + |
| // wGrantMarksGroup (R6-1): a public app of a plain build with a minted row; |
| // the operator grants doc-engine on the minted row; a public request arrives |
| // by the minted host. |
| func wGrantMarksGroup(t *testing.T, w *world) { |
| - b := w.boxes[0] |
| + b := w.engineFreeBox(t) |
| w.tcpPublic(t, b) |
| w.grant(b, mintedB) |
| w.check() |
| @@ -684,34 +729,34 @@ func wStaticMintedPublic(t *testing.T, w *world) { |
| w.final() |
| } |
| -// wOwnerNonEmptyUnique (R7-2): app acct/tcp has TCP instances tcp-b (plain) |
| -// and, provisioned later, tcp-a (declaring); tcp-b's platform row was minted |
| -// before owners were recorded, so the edge finds its owner by backend. tcp-c |
| -// and tcp-d share one address, so tcp-c's minted row has an ambiguous owner. |
| -// At the end every public row with a findable owner must answer. |
| +// wOwnerNonEmptyUnique (R7-2): app acct/tcp's TCP instance tcp-b runs a |
| +// declaring build, internal; its platform row was minted before owners were |
| +// recorded, so the edge finds its owner by backend. tcp-a, a later plain |
| +// instance of the app, is cleared with --public. A public request arrives by |
| +// tcp-b's minted host. |
| +// |
| +// Task 3's version ended in INV-AV: tcp-b's public minted row, misgrouped |
| +// into a closed group, never answered. Since Task 4 a closed group homes its |
| +// box, so every row outside it, the misgrouped row included (its true group |
| +// is tcp-b), is refused by design and INV-AV does not count it. The safety |
| +// effect remains, behind the edge's dedicated refusal. |
| func wOwnerNonEmptyUnique(t *testing.T, w *world) { |
| - b := w.boxes[0] |
| - for _, x := range []struct { |
| - host, addr string |
| - }{{tcpB, "10.0.0.7:9102"}, {tcpC, "10.0.0.7:9103"}, {tcpD, "10.0.0.7:9103"}} { |
| - if !w.provision(b, x.host, tcpApp, x.addr, vPlain) { |
| - t.Fatalf("witness: provisioning %s refused: %s", x.host, w.boxesState()) |
| - } |
| + b := w.engineFreeBox(t) |
| + if !w.provision(b, tcpB, tcpApp, "10.0.0.7:9102", vEngine) { |
| + t.Fatalf("witness: provisioning %s refused: %s", tcpB, w.boxesState()) |
| } |
| w.mint(b, tcpB, mintedB, false) |
| - w.mint(b, tcpC, mintedC, false) |
| + w.reload(b) |
| w.check() |
| - if !w.provision(b, tcpA, tcpApp, "10.0.0.7:9101", vEngine) { |
| + if !w.provision(b, tcpA, tcpApp, "10.0.0.7:9101", vPlain) { |
| t.Fatalf("witness: provisioning %s refused: %s", tcpA, w.boxesState()) |
| } |
| - w.reload(b) |
| w.check() |
| - if on("owner-nonempty-unique") { |
| - if r := w.admitPublic(b, mintedC, "/"); r != nil { |
| - t.Fatalf("witness: a minted row with an ambiguous owner was admitted: %s", w.boxesState()) |
| - } |
| + if !w.clearPublic(b, tcpA) { |
| + t.Fatalf("witness: --public refused on %s's plain live release: %s", tcpA, w.boxesState()) |
| } |
| - w.final() |
| + w.requestBy(b, mintedB) |
| + w.check() |
| } |
| // wPublicChecksLive: the engine's live release declares; the operator runs |
| @@ -776,7 +821,7 @@ func wPublicConfirmsEmpty(t *testing.T, w *world) { |
| // the edge and refused, and no group is marked. |
| func TestGrantRefusedOnUnresolvedMintedRow(t *testing.T) { |
| w := newWitness() |
| - b := w.boxes[0] |
| + b := w.engineFreeBox(t) |
| for _, h := range []string{tcpC, tcpD} { |
| if !w.provision(b, h, tcpApp, "10.0.0.7:9103", vPlain) { |
| t.Fatalf("provisioning %s refused: %s", h, w.boxesState()) |
| @@ -828,7 +873,7 @@ func TestGrantRefusedOnUnresolvedMintedRow(t *testing.T) { |
| // --revoke returns once the edge has loaded it, and the mark is still 1. |
| func TestRevokeRunsTheBarrier(t *testing.T) { |
| w := newWitness() |
| - b := w.boxes[0] |
| + b := w.engineFreeBox(t) |
| w.tcpPublic(t, b) |
| b.ReloadFails = true |
| if w.grant(b, mintedB) { |
| @@ -979,3 +1024,217 @@ func TestI1Oracle(t *testing.T) { |
| } |
| } |
| } |
| + |
| +// ---------- Task 4: the dedicated engine box and ingress ---------- |
| + |
| +const ( |
| + svcHost = "svc.example" // a service row of the witnesses |
| + tcpE = "tcp-e" // a TCP-backed engine on box 0 |
| + tcpEAddr = "10.0.0.7:9200" |
| +) |
| + |
| +// engineFreeBox is box 0 with the engine's rows removed, the edge reloaded: |
| +// a box that homes no internal group, for scenarios that need instances of |
| +// their own (the dedicated-box rule refuses every other proxying row on a box |
| +// that homes the engine, and refuses a declaring launch beside one). |
| +func (w *world) engineFreeBox(t *testing.T) *box { |
| + b := w.boxes[0] |
| + for _, h := range []string{eng, engHost, engAlias, engSite} { |
| + delete(b.Rows, h) |
| + delete(b.Mark, h) |
| + } |
| + b.Wrote++ |
| + w.logf("witness: box0's engine rows removed (registry change %d)", b.Wrote) |
| + w.reload(b) |
| + w.check() |
| + if len(w.violations) > 0 { |
| + t.Fatalf("witness: the fixture violates: %v", w.violations) |
| + } |
| + return b |
| +} |
| + |
| +// runningEngine starts the engine group on box 0 on the declaring build, |
| +// fenced as internal (its starting mark), and returns its process. |
| +func (w *world) runningEngine(t *testing.T) (*box, *proc) { |
| + b := w.boxes[0] |
| + b.Live[eng], b.Good[eng] = vEngine, vEngine |
| + if !w.launch(b, eng, vEngine, "seed") { |
| + t.Fatalf("witness: the engine did not start under its fenced mark: %s", w.boxesState()) |
| + } |
| + w.check() |
| + if len(w.violations) > 0 { |
| + t.Fatalf("witness: the fixture violates: %v", w.violations) |
| + } |
| + return b, b.Procs[len(b.Procs)-1] |
| +} |
| + |
| +// wPortsExcluded (R11-1): the public engine route ships a plain release |
| +// declaring ports, and the box renders its listener; then adoption of a |
| +// declaring build; the capability pass runs; a public connection arrives on |
| +// the granted port. |
| +func wPortsExcluded(t *testing.T, w *world) { |
| + b := w.publicEngine(t) |
| + if !w.ship(b, eng, vPlain, true) { |
| + t.Fatalf("witness: a plain release declaring ports was refused: %s", w.boxesState()) |
| + } |
| + port := b.PortGrant[eng] |
| + if port == "" || b.Listen[port] != eng { |
| + t.Fatalf("witness: no listener rendered for the granted port: %s", w.boxesState()) |
| + } |
| + if p := w.directConnect(b, port, true); p == nil { |
| + t.Fatalf("witness: the granted port of a public route reached nothing: %s", w.boxesState()) |
| + } |
| + w.check() |
| + if !w.adopt(b, eng, vEngine, nil) { |
| + t.Fatalf("witness: adoption of the engine refused: %s", w.boxesState()) |
| + } |
| + w.check() |
| + w.capsPass(b) |
| + w.directConnect(b, port, true) |
| + w.check() |
| +} |
| + |
| +// wDedicatedLaunchCheck (R12-2): the public engine route has a service row |
| +// beside it aimed at its backend; adoption of a declaring build; a public |
| +// request arrives through the service row. |
| +func wDedicatedLaunchCheck(t *testing.T, w *world) { |
| + b := w.publicEngine(t) |
| + w.addServiceRow(b, svcHost, b.Rows[eng].Backend) |
| + w.reload(b) |
| + w.check() |
| + ok := w.adopt(b, eng, vEngine, nil) |
| + if ok && on("dedicated-launch-check") { |
| + t.Fatalf("witness: a declaring adoption passed the launch check beside a service row: %s", w.boxesState()) |
| + } |
| + w.check() |
| + w.requestBy(b, svcHost) |
| + w.check() |
| +} |
| + |
| +// wDedicatedEdgeRefusal (R12-2): the engine runs internal; a service row |
| +// aimed at its backend is added afterwards; the edge polls; a public request |
| +// arrives through the service row. |
| +func wDedicatedEdgeRefusal(t *testing.T, w *world) { |
| + b, _ := w.runningEngine(t) |
| + w.addServiceRow(b, svcHost, b.Rows[eng].Backend) |
| + w.reload(b) |
| + w.check() |
| + w.requestBy(b, svcHost) |
| + w.check() |
| +} |
| + |
| +// wIngressPrivate (R13-1): a TCP-backed engine runs internal on box 0; a |
| +// service row on box 1 is aimed at box 0's address and the engine's port; a |
| +// public request arrives at box 1's edge through it. |
| +func wIngressPrivate(t *testing.T, w *world) { |
| + b0, b1 := w.engineFreeBox(t), w.boxes[1] |
| + if !w.provision(b0, tcpE, tcpApp, tcpEAddr, vEngine) { |
| + t.Fatalf("witness: provisioning the TCP engine refused: %s", w.boxesState()) |
| + } |
| + w.check() |
| + w.addServiceRow(b1, svcHost, tcpEAddr) |
| + w.reload(b1) |
| + w.check() |
| + r := w.admitPublic(b1, svcHost, "/") |
| + if r == nil { |
| + t.Fatalf("witness: box1's edge refused its own service row: %s", w.boxesState()) |
| + } |
| + w.deliver(r) |
| + w.check() |
| +} |
| + |
| +// wOwnPort (R12-1): the engine runs internal and binds a port of its own on |
| +// every interface; a public connection arrives on that port. |
| +func wOwnPort(t *testing.T, w *world) { |
| + b, p := w.runningEngine(t) |
| + w.bindOwnPort(b, p) |
| + w.directConnect(b, ownPort(p), true) |
| + w.check() |
| +} |
| + |
| +// TestNullRouteHomesTheBox: a NULL route homes its box like a route marked |
| +// 1, whether or not it has a release. Here box 1's shop has no release, so |
| +// the upgrade leaves it NULL; a service row aimed at its backend must get the |
| +// internal refusal. Were it served, a request admitted through it and held, |
| +// with the row then deleted, would outlive a declaring `carlos run` in the |
| +// NULL group: the gate writes 1 over NULL, a group already fenced, so no |
| +// reload bumps the epoch, and the launch check finds no row to refuse. |
| +func TestNullRouteHomesTheBox(t *testing.T) { |
| + w := newWitness() |
| + b := w.boxes[1] |
| + w.upgrade(b) |
| + if m := w.groupMark(b, "shop"); m != markNull || b.Live["shop"] != 0 { |
| + t.Fatalf("fixture: shop is %v with live v%d, want NULL with no release", m, b.Live["shop"]) |
| + } |
| + w.addServiceRow(b, svcHost, b.Rows["shop"].Backend) |
| + w.reload(b) |
| + r := w.admitPublic(b, svcHost, "/") |
| + if r != nil { |
| + r.Held = true |
| + w.deleteRow(b, svcHost) |
| + w.launch(b, "shop", vEngine, "cmd") |
| + w.deliver(r) |
| + } |
| + w.check() |
| + if r != nil { |
| + t.Errorf("a service row beside a NULL route was served (request %d)", r.ID) |
| + } |
| + if len(w.violations) > 0 { |
| + t.Errorf("violations: %v", w.violations) |
| + } |
| + if t.Failed() { |
| + dump(t, w) |
| + } |
| +} |
| + |
| +// TestShipRefusesDocEngineWithPorts (spec §8): `carlos ship` refuses a |
| +// release declaring doc_engine and ports together, and nothing is adopted or |
| +// granted; a plain release declaring ports ships, and its port listens. |
| +func TestShipRefusesDocEngineWithPorts(t *testing.T) { |
| + w := newWitness() |
| + b := w.publicEngine(t) |
| + wrote := b.Wrote |
| + if w.ship(b, eng, vEngine, true) { |
| + t.Fatal("a release declaring doc_engine and ports shipped") |
| + } |
| + if b.Live[eng] != vPlain || b.PortGrant[eng] != "" || len(b.Listen) != 0 || b.Wrote != wrote { |
| + t.Fatalf("a refused ship changed the box: %s", w.boxesState()) |
| + } |
| + if !w.ship(b, eng, vPlain, true) || b.Listen[b.PortGrant[eng]] != eng { |
| + t.Fatalf("a plain release declaring ports did not ship with its listener: %s", w.boxesState()) |
| + } |
| + if len(w.violations) > 0 { |
| + t.Fatalf("violations: %v", w.violations) |
| + } |
| +} |
| + |
| +// TestEngineBoxKeepsStaticRows (spec §8): on a box homing an internal group, |
| +// a service row aimed at the engine and another app's instance get the |
| +// internal refusal, a declaring launch beside them is refused, and the |
| +// static row keeps answering. |
| +func TestEngineBoxKeepsStaticRows(t *testing.T) { |
| + w := newWitness() |
| + b, _ := w.runningEngine(t) |
| + w.addServiceRow(b, svcHost, b.Rows[eng].Backend) |
| + b.Rows["other"] = &row{Host: "other", Kind: "instance", App: "acct/other", Backend: "10.0.0.7:9300", PathTo: map[string]string{}} |
| + b.Mark["other"] = markPublic |
| + w.reload(b) |
| + for _, h := range []string{svcHost, "other"} { |
| + if _, outcome := w.admit(b, h, "/"); outcome != refused { |
| + t.Errorf("%s on the engine's box: %s, want the internal refusal", h, outcome) |
| + } |
| + } |
| + if _, outcome := w.admit(b, engSite, "/"); outcome != answered { |
| + t.Errorf("the static row %s on the engine's box: %s, want answered", engSite, outcome) |
| + } |
| + if w.launch(b, eng, vEngine, "seed") { |
| + t.Errorf("a declaring launch beside other proxying rows was not refused") |
| + } |
| + w.check() |
| + if len(w.violations) > 0 { |
| + t.Errorf("violations: %v", w.violations) |
| + } |
| + if t.Failed() { |
| + dump(t, w) |
| + } |
| +} |
diff --git a/internal/sim/engines/world_test.go b/internal/sim/engines/world_test.go| index 83c5c7a41..608bba4e0 100644 |
| --- a/internal/sim/engines/world_test.go |
| +++ b/internal/sim/engines/world_test.go |
| @@ -123,6 +123,11 @@ type box struct { |
| EdgeRows map[string]row |
| Serving map[string]mark |
| SetAt map[string]int |
| + |
| + // PortGrant is the operator's ports grant by group (the port); Listen the |
| + // ListenStream sockets the capability pass has rendered, port to group |
| + // (spec §5.1, "The edge is the only ingress"). |
| + PortGrant, Listen map[string]string |
| } |
| type world struct { |
| @@ -169,7 +174,8 @@ func newWorld(seed int64, verbose bool) *world { |
| } |
| newBox := func(id int) *box { |
| return &box{ID: id, Rows: map[string]*row{}, Mark: map[string]mark{}, Live: map[string]int{}, Good: map[string]int{}, Staged: map[string][]int{}, |
| - EdgeRows: map[string]row{}, Serving: map[string]mark{}, SetAt: map[string]int{}} |
| + EdgeRows: map[string]row{}, Serving: map[string]mark{}, SetAt: map[string]int{}, |
| + PortGrant: map[string]string{}, Listen: map[string]string{}} |
| } |
| home, calling := newBox(0), newBox(1) |
| w.boxes = []*box{home, calling} |