amadan

carlos / platform Public

enginesim: an expiry keeps a revoke's age; a residual covers only its own breaches (#335 plan 1)

newestGrants used the newest record's expiry for every key, so a grant
revoked long before that expiry looked newly absent and INV-G gave a
cached grant another 60 ticks. Expiry now counts only for keys the
expired record granted.

failProc filed every breach of a process tagged with the
unwritten-manifest residual as that residual. Now only a breach by a
path the upgrade's 0 opened (I1, the edge, a ports listener for a
public group) counts, and only while the group stays open; the tag is
cleared the first time the group closes again.

Regressions: TestExpiryKeepsRevokeAge, TestResidualCoversOnlyItsOwnBreaches.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 4648305e01b8da95a18db97a2bc360617a103ec6 parent 3a2169f
5 files changed, +163 −18
  • internal/sim/engines/calls_test.go +11 −7
  • internal/sim/engines/dedicated_test.go +5 −2
  • internal/sim/engines/edge_test.go +2 −2
  • internal/sim/engines/invariants_test.go +41 −7
  • internal/sim/engines/witness_test.go +104 −0
diff --git a/internal/sim/engines/calls_test.go b/internal/sim/engines/calls_test.go
index 8042d03af..504442d69 100644
--- a/internal/sim/engines/calls_test.go
+++ b/internal/sim/engines/calls_test.go
@@ -155,15 +155,17 @@ func (w *world) setBucketDown(down bool) {
}
// newestGrants is the oracle's truth for key: whether the newest record the
-// console published grants it, and if not, since when. An expired newest
-// record grants nothing from its expiry (a console down for 72 hours drops
-// every grant, §6.4). A key no record ever granted has never been granted.
+// console published grants it, and if not, since when. A key the newest
+// record grants stops being granted at its expiry (a console down for 72
+// hours drops every grant, §6.4). A key it does not grant keeps the age of
+// its revoke, whatever the record's expiry: an expiry never makes an old
+// revoke young again. A key no record ever granted has never been granted.
func (w *world) newestGrants(key string) (bool, int) {
rec := w.console.Records[w.console.Rev]
- if w.now() >= rec.Expires {
- return false, rec.Expires
- }
if rec.Grants[key] {
+ if w.now() >= rec.Expires {
+ return false, rec.Expires
+ }
return true, 0
}
if t, ok := w.console.RevokedAt[key]; ok {
@@ -564,7 +566,9 @@ func (w *world) maybeForged() *caller {
// every edge that has a floor has read the newest revision, so a floor
// refuses it everywhere but on a box with no floor. A replay before an edge
// has read the newest revision withholds that revision from it, which no
-// floor can refuse; see the Task 5 report (an unstated residual).
+// floor can refuse: by the controller's ruling a stated residual (a bucket
+// writer within the 72-hour expiry), excluded from the walk, not a
+// violation.
func (w *world) replayable() bool {
if w.console.Rev < 2 {
return false
diff --git a/internal/sim/engines/dedicated_test.go b/internal/sim/engines/dedicated_test.go
index e4c890aca..47c4e9062 100644
--- a/internal/sim/engines/dedicated_test.go
+++ b/internal/sim/engines/dedicated_test.go
@@ -340,10 +340,13 @@ func (w *world) reach(b *box, p *proc, public bool, how string) *proc {
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)
+ // a ports listener exists only because the group is public: a path the
+ // upgrade's 0 opens; any other way past the edge is the ingress rule's
+ listener := strings.HasPrefix(how, "the ports listener")
if public && w.builds[p.Ver].Declares {
- w.failProc(p, "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)
+ w.failProc(b, p, "INV-P", listener, "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.failProc(p, "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)
+ w.failProc(b, p, "INV-P", listener, "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
}
diff --git a/internal/sim/engines/edge_test.go b/internal/sim/engines/edge_test.go
index 36b26f297..e619f82d8 100644
--- a/internal/sim/engines/edge_test.go
+++ b/internal/sim/engines/edge_test.go
@@ -284,9 +284,9 @@ func (w *world) deliver(r *req) {
r.Reached = p.ID
w.logf("box%d: request %d delivered to process %d (%s v%d)", b.ID, r.ID, p.ID, p.Group, p.Ver)
if r.Public && w.builds[p.Ver].Declares {
- w.failProc(p, "INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, which declares doc_engine", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver)
+ w.failProc(b, p, "INV-P", true, "box%d: public request %d (row %s) delivered to process %d of %s running v%d, which declares doc_engine", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver)
} else if r.Public && w.grantLoaded(b, g) != "" {
- w.failProc(p, "INV-P", "box%d: public request %d (row %s) delivered to process %d of %s running v%d, whose group holds the doc-engine grant (on %s)", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver, w.grantLoaded(b, g))
+ w.failProc(b, p, "INV-P", true, "box%d: public request %d (row %s) delivered to process %d of %s running v%d, whose group holds the doc-engine grant (on %s)", b.ID, r.ID, r.Row, p.ID, p.Group, p.Ver, w.grantLoaded(b, g))
}
if p.Ver == b.Live[g] {
b.Good[g] = p.Ver // the live build answered: it is the good version now
diff --git a/internal/sim/engines/invariants_test.go b/internal/sim/engines/invariants_test.go
index 5067236ab..d3746b984 100644
--- a/internal/sim/engines/invariants_test.go
+++ b/internal/sim/engines/invariants_test.go
@@ -67,7 +67,7 @@ func (w *world) i1Broken(b *box, p *proc) string {
// checkStart is I1 at the moment process p starts.
func (w *world) checkStart(b *box, p *proc) {
if why := w.i1Broken(b, p); why != "" {
- w.failProc(p, "INV-I1", "box%d: process %d of %s started v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
+ w.failProc(b, p, "INV-I1", true, "box%d: process %d of %s started v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
}
}
@@ -76,10 +76,11 @@ func (w *world) checkStart(b *box, p *proc) {
// Task 5 adds INV-ARM (checkArm); its event invariants INV-ID and INV-G are
// recorded when an engine call reaches a process (checkCall).
func (w *world) check() {
+ w.endResidualWindows()
for _, b := range w.boxes {
for _, p := range b.Procs {
if why := w.i1Broken(b, p); why != "" {
- w.failProc(p, "INV-I1", "box%d: process %d of %s runs v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
+ w.failProc(b, p, "INV-I1", true, "box%d: process %d of %s runs v%d, which declares doc_engine: %s", b.ID, p.ID, p.Group, p.Ver, why)
}
}
}
@@ -223,7 +224,7 @@ func (w *world) checkArm() {
}
for _, p := range b.Procs {
if p.Unisolated {
- w.failProc(p, "INV-ARM", "box%d: engine sockets are open (armed %v) while process %d runs unisolated in %s", b.ID, b.Armed, p.ID, p.Slice)
+ w.fail("INV-ARM", "box%d: engine sockets are open (armed %v) while process %d runs unisolated in %s", b.ID, b.Armed, p.ID, p.Slice)
}
}
}
@@ -240,12 +241,45 @@ func (w *world) residual(name, format string, args ...any) {
w.logf("residual:%s recorded", name)
}
-// failProc is fail for a breach process p causes: a process a stated
-// residual covers records the residual instead.
-func (w *world) failProc(p *proc, inv, format string, args ...any) {
- if p != nil && p.Residual != "" {
+// failProc is fail for a breach process p on b causes. It records the stated
+// residual p belongs to instead only when the breach is the residual's own:
+// viaClassification says the breach came by a path the upgrade's 0 opened
+// (I1 itself, the edge serving the group, a ports listener rendered for a
+// public group), and the residual's window still holds (residualHolds). Any
+// other breach of a tagged process is a violation.
+func (w *world) failProc(b *box, p *proc, inv string, viaClassification bool, format string, args ...any) {
+ if viaClassification && w.residualHolds(b, p) {
w.residual(p.Residual, inv+": "+format, args...)
return
}
w.fail(inv, format, args...)
}
+
+// residualHolds: p is tagged with the unwritten-manifest residual and its
+// group is still open, as the upgrade classified it. The window ends for good
+// the first time the group is closed again (a grant, a gate's 1): the tag is
+// cleared, so a later 0 (another rule's failure) is never misfiled as the
+// upgrade's.
+func (w *world) residualHolds(b *box, p *proc) bool {
+ if p == nil || p.Residual == "" {
+ return false
+ }
+ if w.closed(b, p.Group) {
+ w.logf("box%d: %s is closed again: process %d's residual window (%s) ends", b.ID, p.Group, p.ID, p.Residual)
+ p.Residual = ""
+ return false
+ }
+ return true
+}
+
+// endResidualWindows runs residualHolds on every tagged process, so a window
+// ends when its group closes even if nothing breaches meanwhile.
+func (w *world) endResidualWindows() {
+ for _, b := range w.boxes {
+ for _, p := range b.Procs {
+ if p.Residual != "" {
+ w.residualHolds(b, p)
+ }
+ }
+ }
+}
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go
index 019e7bd09..91604595a 100644
--- a/internal/sim/engines/witness_test.go
+++ b/internal/sim/engines/witness_test.go
@@ -1633,3 +1633,107 @@ func TestArmRefusesAndAdmits(t *testing.T) {
dump(t, w)
}
}
+
+// withMutation runs f with the mutation set m, restoring the previous set.
+func withMutation(m string, f func()) {
+ saved := mutated
+ mutated = m
+ defer func() { mutated = saved }()
+ f()
+}
+
+// TestExpiryKeepsRevokeAge: with stale-clears-grants off, the edges keep a
+// cached grant past the newest record's expiry. A key revoked long before
+// that expiry is a violation the moment a call reaches the engine, not 60
+// ticks after the expiry; a key the expired record granted is within the
+// bound for 60 ticks after the expiry, then a violation.
+func TestExpiryKeepsRevokeAge(t *testing.T) {
+ withMutation("stale-clears-grants", func() {
+ w := newWitness()
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ w.setBucketDown(true)
+ w.consoleRevoke(shopEng) // tick 0; revision 2, never read
+ w.advance(lifetimeTicks) // revision 2 expires now
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-G" || !strings.Contains(w.violations[0], "since tick 0") {
+ t.Errorf("a key revoked at tick 0, called across the record's expiry: want INV-G since tick 0, got %v", w.violations)
+ dump(t, w)
+ }
+
+ w = newWitness()
+ w.runningEngine(t)
+ shop = w.armedShop(t)
+ w.setBucketDown(true)
+ w.advance(lifetimeTicks) // revision 1, which grants shop, expires now
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ if len(w.violations) != 0 {
+ t.Errorf("a granted key at its record's expiry is within the bound: got %v", w.violations)
+ }
+ w.advance(staleTicks)
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ if len(w.violations) != 1 || !strings.Contains(w.violations[0], "since tick 25920") {
+ t.Errorf("a granted key 60 ticks past its record's expiry: want INV-G since tick 25920, got %v", w.violations)
+ dump(t, w)
+ }
+ })
+}
+
+// upgradeResidualFixture is residualUnwrittenManifest up to the upgrade,
+// with the flag on: the residual is recorded and nothing violates. It
+// returns the engine's box and the tagged process.
+func upgradeResidualFixture(t *testing.T) (*world, *box, *proc) {
+ w := newWitness()
+ w.unwrittenManifestAcrossUpgrade = true
+ b := w.boxes[0]
+ b.Live[eng], b.Good[eng] = vUnreadable, vUnreadable
+ w.launch(b, eng, vUnreadable, "seed")
+ p := w.newest(b, eng)
+ w.repointAwake(b, eng, vPlain)
+ w.upgrade(b)
+ w.check()
+ if len(w.residuals) == 0 || len(w.violations) > 0 || p.Residual == "" {
+ t.Fatalf("fixture: want the upgrade residual recorded on process %d, got residuals %v violations %v", p.ID, w.residuals, w.violations)
+ }
+ return w, b, p
+}
+
+// TestResidualCoversOnlyItsOwnBreaches: a process tagged with the
+// unwritten-manifest residual is not a licence. While its group is still
+// open, a breach by a path the upgrade's 0 did not open (a public connection
+// to a port the engine bound itself, through a broken firewall) is a
+// violation. Once the group is closed again the window has ended: a later 0
+// written by a broken --public, under that same process, is a violation.
+func TestResidualCoversOnlyItsOwnBreaches(t *testing.T) {
+ t.Run("another path", func(t *testing.T) {
+ w, b, p := upgradeResidualFixture(t)
+ withMutation("ingress-precondition", func() {
+ w.bindOwnPort(b, p)
+ w.directConnect(b, ownPort(p), true)
+ })
+ w.check()
+ if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-P" {
+ t.Errorf("want INV-P through the broken firewall, got violations %v residuals %v", w.violations, w.residuals)
+ dump(t, w)
+ }
+ })
+ t.Run("after the window", func(t *testing.T) {
+ w, b, p := upgradeResidualFixture(t)
+ w.writeMark(b, eng, markInternal) // a gate's 1: the group is closed again
+ w.reload(b)
+ w.check()
+ if p.Residual != "" || len(w.violations) > 0 {
+ t.Fatalf("closing the group: want the window ended and no violation, got tag %q violations %v", p.Residual, w.violations)
+ }
+ withMutation("public-confirms-empty", func() {
+ w.clearStopMisses = true
+ w.operatorPublic(b, eng) // the stop misses process p; step 3 is gone
+ w.reload(b)
+ w.check()
+ })
+ if len(w.violations) == 0 || invariantOf(w.violations[0]) != "INV-I1" {
+ t.Errorf("a broken --public under the formerly tagged process: want INV-I1, got violations %v residuals %v", w.violations, w.residuals)
+ dump(t, w)
+ }
+ })
+}