amadan

carlos / platform Public

provision: pin the class rule across its two gates; state the far-copy cost

Review fixes.

The class rule lives in two hand-maintained functions — everywhereClass
over a record (the mint gate) and everywhereRoute over a row (the removal
gate, asked when the record is gone and the row is all that is left).
Nothing held the copies together: a rule added to one alone recreates the
immortality bug the pair was written to close, silently, with every other
test green. TestEverywhereClassAgreesAcrossRecordAndRow locks the property
routeFor gives them for free — everywhereClass(rec) ==
everywhereRoute(routeFor(rec, ...)) across fourteen shapes, each first
checked to be one ValidateShape would actually admit. Mutation-proven: a
rule added to the record side alone fails it on the exact fixture.

And everywhereRoute's comment now states what the Backing/Tunnel/Caps
refusal really costs, which is more than the "stale row" it claimed: an
operator running `carlos route -grant` against a FAR box's copy takes that
copy out of removal scope permanently, so deleting the record retires the
route on its home box and leaves the far box still SERVING the retired
site with its grants intact — `carlos remove` stops being fleet-wide the
moment anyone touches a far copy. The conservative gate stands (the
alternative hands an unattended record deletion the grant purge
registry.Delete documents as human-gated); the gap is bookkeeping.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Paul Campbell pushed by paul@keymail.dev af006be76a68f4a8086da9525c0b9608ea0cd3ed parent 7bb1c76
2 files changed, +92 −5
  • internal/provision/reconcile.go +19 −5
  • internal/provision/reconcile_test.go +73 −0
diff --git a/internal/provision/reconcile.go b/internal/provision/reconcile.go
index 56b0b32c0..8b532196a 100644
--- a/internal/provision/reconcile.go
+++ b/internal/provision/reconcile.go
@@ -128,11 +128,25 @@ func everywhereClass(rec Record) bool {
//
// The two must agree, or the widened mint gate leaves immortal routes: a far
// box that mints an everywhere-class route and then cannot see it as one is a
-// box serving a retired site forever. They are separate functions rather than
-// one over a shared shape because the row carries columns no record can state
-// (Backing, Tunnel, Caps) — and a row that has GROWN one of those since it was
-// minted is deliberately read as home-boxed here, which costs a stale row on a
-// far box and never a surprise deletion.
+// box serving a retired site forever. They agree by construction today because
+// routeFor is the one renderer between them, and
+// TestEverywhereClassAgreesAcrossRecordAndRow locks that: a class rule added to
+// one of these functions alone recreates exactly the immortality bug this pair
+// was written to close, with every other test still green.
+//
+// They are separate functions rather than one over a shared shape because the
+// row carries columns no record can state (Backing, Tunnel, Caps), and a row
+// that has GROWN one of those since it was minted is deliberately read as
+// home-boxed here. State that cost honestly, because it is bigger than a stale
+// row: an operator who runs `carlos route -grant` (or -backing/-tunnel) against
+// the FAR box's copy takes that copy out of removal scope permanently. Deleting
+// the record then retires the route on its home box and leaves the far box
+// still SERVING the retired site, grants intact, with no record left anywhere
+// to explain it — so `carlos remove` stops being fleet-wide the moment anyone
+// touches a far copy. The alternative (removing rows carrying operator columns)
+// hands an unattended bucket-record deletion the grant purge registry.Delete
+// documents as human-gated, which is worse. The conservative gate stands; the
+// gap is tracked in the bookkeeping issue, not papered over here.
func everywhereRoute(rt registry.Route) bool {
if rt.Unit != "" || rt.Hibernate || rt.Backing != "" || rt.Tunnel != "" || rt.Caps != "" {
return false
diff --git a/internal/provision/reconcile_test.go b/internal/provision/reconcile_test.go
index 9048d09d4..039ba4b19 100644
--- a/internal/provision/reconcile_test.go
+++ b/internal/provision/reconcile_test.go
@@ -2039,6 +2039,79 @@ func TestReconcileRemovesEverywhereRouteWhenItsRecordGoes(t *testing.T) {
}
}
+// TestEverywhereClassAgreesAcrossRecordAndRow is the drift pin between the two
+// halves of the class rule: everywhereClass reads a RECORD (the mint gate) and
+// everywhereRoute reads a ROW (the removal gate, asked when the record is gone
+// and the row is all that is left). routeFor is the one renderer between them,
+// so the property holds by construction today — and it is exactly what a class
+// rule added to one function alone would break, silently, with every other test
+// in this file still green. That divergence is the immortality bug the pair was
+// written to close: a far box that mints an everywhere-class route and then
+// cannot see it as one serves a retired site forever.
+//
+// The fixture set is every shape the file already exercises, plus the two
+// directions a new rule would most plausibly be written into one side only (a
+// probe config, an explicitly non-hibernating addr record).
+func TestEverywhereClassAgreesAcrossRecordAndRow(t *testing.T) {
+ off := false
+ on := true
+ base := func(host string) Record {
+ return Record{Schema: 1, Host: host, Slug: "s", App: "tito", Account: "bac",
+ Pool: "tito", Region: "ie", Channel: "stable"}
+ }
+ with := func(host string, mut func(*Record)) Record {
+ rec := base(host)
+ mut(&rec)
+ return rec
+ }
+ fixtures := []struct {
+ name string
+ rec Record
+ }{
+ {"socket instance (no kind, no addr)", base("exec.go.tito.io")},
+ {"static", with("site.go.tito.io", func(r *Record) { r.Kind = "static" })},
+ {"static, status-named", with("named-site.go.tito.io", func(r *Record) { r.Kind, r.StatusNamed = "static", &on })},
+ {"public single addr", with("pub.go.tito.io", func(r *Record) { r.Kind, r.Addr = "service", "203.0.113.10:443" })},
+ {"public addrs set", with("pubs.go.tito.io", func(r *Record) {
+ r.Kind, r.Addrs = "service", []string{"203.0.113.11:443", "198.51.100.7:443"}
+ })},
+ {"public addrs with an explicit probe", with("probed.go.tito.io", func(r *Record) {
+ r.Kind, r.Addrs, r.Health = "service", []string{"203.0.113.12:443", "198.51.100.8:443"}, &Health{Path: "/healthz"}
+ })},
+ {"public addr, explicitly never hibernating", with("awake.go.tito.io", func(r *Record) {
+ r.Kind, r.Addr, r.Hibernate = "service", "203.0.113.13:443", &off
+ })},
+ {"loopback addr", with("loop.go.tito.io", func(r *Record) { r.Kind, r.Addr = "service", "127.0.0.1:8090" })},
+ {"private addrs", with("priv.go.tito.io", func(r *Record) { r.Kind, r.Addrs = "service", []string{"10.0.0.5:3000"} })},
+ {"mixed public and private addrs", with("mixed.go.tito.io", func(r *Record) {
+ r.Kind, r.Addrs = "service", []string{"203.0.113.14:443", "192.168.1.9:3000"}
+ })},
+ {"name-based addr", with("named.go.tito.io", func(r *Record) { r.Kind, r.Addr = "service", "backend.example.com:443" })},
+ {"unit-owned public addr", with("unit.go.tito.io", func(r *Record) {
+ r.Addr, r.Unit = "203.0.113.20:8090", "console.service"
+ })},
+ {"environment-bound static", with("env-site.go.tito.io", func(r *Record) { r.Kind, r.Environment = "static", "staging" })},
+ {"fleet-placed static", with("pisite.go.tito.io", func(r *Record) { r.Kind, r.Region = "static", "fleet/pi" })},
+ }
+ for _, f := range fixtures {
+ t.Run(f.name, func(t *testing.T) {
+ // Every fixture must be one the pass would actually materialize —
+ // a shape ValidateShape refuses never reaches either gate, so a
+ // property proved on one would prove nothing.
+ if err := ValidateShape(f.rec); err != nil {
+ t.Fatalf("fixture is not a shape this pass would ever see: %v", err)
+ }
+ fromRecord := everywhereClass(f.rec)
+ fromRow := everywhereRoute(routeFor(f.rec, "/data", `["seed"]`))
+ if fromRecord != fromRow {
+ t.Fatalf("class disagrees across the mint and removal gates: everywhereClass = %v, "+
+ "everywhereRoute(routeFor(...)) = %v — a record this box mints must be a row it can retire",
+ fromRecord, fromRow)
+ }
+ })
+ }
+}
+
// TestRouteForCarriesAddrsAndHealth is Task 3's mint-side proof: a record
// with an explicit multi-upstream Addrs set mints a route whose Addrs is the
// comma-joined string and whose Health carries a fully-materialized default