amadan

carlos / platform Public

enginesim: the R5 freshness bound; expiry, staleness and revoke age apart; residuals from independent facts (#335 plan 1, final review)

Finding 3 (ruling R5): every record carries signed_at; the console
re-signs every 12 ticks while up (a console-down toggle stops it) and on
every change; an edge refuses a record signed 60 ticks ago or more and
empties its table on one (new rule grant-freshness-bound, witness
wGrantFreshnessBound, boundary test TestReplayBoundedBySignedAt). The
replayable exclusion is gone: the walk's bucket writer replays any older
record at any time and keeps it in place over the console's publishes for
a while. The fresh-box replay residual, its flag and its case are gone;
INV-G covers it.

Finding 4: INV-G's grant clauses read only facts no rule changes: the
newest record's expiry (at once), the revoke's age (over 60 ticks plus one
poll), each admitting table's own freshness (never read, expired, no good
read for 60 ticks, signed 60 ticks ago), and a revoke a box has read stays
in force there (§6.4; what keeps floor-persisted and engine-box-recheck
caught alone). TestExpiryKeepsRevokeAge now checks expiry at once and a
stale read with no revoke at all.

Finding 5: the flat-era residual covers only a call by the compromised
instance's own process in its own slice whose recorded caller is that
instance; TestFlatEraTamperKeepsUnrelatedViolations combines it with
cgroup-identity and hop-caller-signed off (INV-ID stays a violation).

stale-clears-grants is now caught only with grant-freshness-bound: a
table's record was signed no later than its last good read.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 04637acc900b57f83b4c38960388ec4076f31943 parent 1d72325
6 files changed, +449 −188
  • internal/sim/engines/calls_test.go +160 −109
  • internal/sim/engines/expected-outcomes.txt +1 −0
  • internal/sim/engines/invariants_test.go +89 −19
  • internal/sim/engines/rules_test.go +4 −3
  • internal/sim/engines/witness_test.go +181 −44
  • internal/sim/engines/world_test.go +14 −13
diff --git a/internal/sim/engines/calls_test.go b/internal/sim/engines/calls_test.go
index 504442d69..78221e170 100644
--- a/internal/sim/engines/calls_test.go
+++ b/internal/sim/engines/calls_test.go
@@ -10,9 +10,11 @@ import (
// freshness).
//
// The console publishes the grant set as one signed record with a strictly
-// increasing revision and a 72-hour expiry; every edge mirrors it, keeps a
+// increasing revision, its signing time and a 72-hour expiry, and re-signs it
+// every two minutes and on every change; every edge mirrors it, keeps a
// durable revision floor, and treats a stale, expired or never-read table as
-// empty. A nested instance calls an engine through its engine socket, which
+// empty. Stale is either no good read for ten minutes or a record signed more
+// than ten minutes ago (ruling R5). A nested instance calls an engine through its engine socket, which
// is open only on an armed box; a host-app process calls through the door.
// The calling box proves the caller (the peer's cgroup, or a door key from a
// uid other than carlos), checks its own table and hops to the engine's home
@@ -25,7 +27,8 @@ import (
// Time: one tick is 10 s.
const (
pollTicks = 3 // the mirror polls every 30 s
- staleTicks = 60 // no good read for ten minutes: stale
+ staleTicks = 60 // no good read, or a record signed, ten minutes ago: stale (R5)
+ resignTicks = 12 // the console re-signs every two minutes while it is up (R5)
lifetimeTicks = 25920 // a record expires 72 hours after it is signed
)
@@ -41,11 +44,11 @@ func (w *world) advance(n int) {
// ---------- the console's record (spec §5.2) ----------
-// record is one signed control/engines.json: its revision, its expiry (in
-// ticks), and its grants by account/app/engine.
+// record is one signed control/engines.json: its revision, its signed_at and
+// expiry (in ticks), and its grants by account/app/engine.
type record struct {
- Rev, Expires int
- Grants map[string]bool
+ Rev, SignedAt, Expires int
+ Grants map[string]bool
}
// mirror is an edge's grant mirror (§5.3): the record it holds, its revision
@@ -60,15 +63,25 @@ type mirror struct {
// engConsole is the console's side: its database (Grants, the authority),
// every record it has signed, the newest revision, and the object in the
-// bucket. RevokedAt is the oracle's: the tick of the publish that stopped
-// granting a key. BucketDown: the edges cannot read the bucket.
+// bucket. RevokedAt and RevokedRev are the oracle's: the tick and revision of
+// the publish that stopped granting a key. BucketDown: the edges cannot read
+// the bucket. Down: the console is down, so it neither re-signs nor takes a
+// grant or revoke.
+//
+// Pinned is a bucket writer's replay: an older signed record it keeps in the
+// bucket, overwriting each record the console publishes, until tick
+// PinnedUntil.
type engConsole struct {
- Rev int
- Records map[int]*record
- Grants map[string]bool
- RevokedAt map[string]int
- Bucket *record
- BucketDown bool
+ Rev int
+ Records map[int]*record
+ Grants map[string]bool
+ RevokedAt map[string]int
+ RevokedRev map[string]int
+ Bucket *record
+ BucketDown bool
+ Down bool
+ Pinned *record
+ PinnedUntil int
}
// The engines the operator has named (carlos engines add): name to its
@@ -91,22 +104,23 @@ func (c caller) key() string { return c.app() + "/" + c.Engine }
// initEngines is the starting world: the console's first record grants shop
// the engine eng, and every edge has read it.
func (w *world) initEngines() {
- w.console = engConsole{Records: map[int]*record{}, Grants: map[string]bool{"acct/shop/eng": true}, RevokedAt: map[string]int{}}
+ w.console = engConsole{Records: map[int]*record{}, Grants: map[string]bool{"acct/shop/eng": true}, RevokedAt: map[string]int{}, RevokedRev: map[string]int{}}
w.publish(1)
for _, b := range w.boxes {
w.mirrorTick(b)
}
}
-// publish is the console signing its grant set as revision rev, expiring 72
-// hours out, and writing it to the bucket. A revision is strictly increasing;
-// a re-sign with the same grants is a new revision.
+// publish is the console signing its grant set as revision rev, signed now
+// and expiring 72 hours out, and writing it to the bucket (where a pinned
+// replay overwrites it at once). A revision is strictly increasing; a re-sign
+// with the same grants is a new revision.
func (w *world) publish(rev int) {
c := &w.console
if rev <= c.Rev {
panic(fmt.Sprintf("publish: revision %d after %d", rev, c.Rev))
}
- rec := &record{Rev: rev, Expires: w.now() + lifetimeTicks, Grants: map[string]bool{}}
+ rec := &record{Rev: rev, SignedAt: w.now(), Expires: w.now() + lifetimeTicks, Grants: map[string]bool{}}
for k, v := range c.Grants {
if v {
rec.Grants[k] = true
@@ -115,38 +129,66 @@ func (w *world) publish(rev int) {
if prev := c.Records[c.Rev]; prev != nil {
for _, k := range sortedKeys(prev.Grants) {
if !rec.Grants[k] {
- c.RevokedAt[k] = w.now()
+ c.RevokedAt[k], c.RevokedRev[k] = w.now(), rev
}
}
}
for k := range rec.Grants {
delete(c.RevokedAt, k)
+ delete(c.RevokedRev, k)
}
c.Records[rev], c.Rev, c.Bucket = rec, rev, rec
- w.logf("console: publishes revision %d, expiring at %d, grants %v", rev, rec.Expires, sortedKeys(rec.Grants))
+ w.logf("console: publishes revision %d, signed at %d, expiring at %d, grants %v", rev, rec.SignedAt, rec.Expires, sortedKeys(rec.Grants))
+ if c.Pinned != nil {
+ c.Bucket = c.Pinned
+ w.logf("bucket writer: overwrites it with revision %d", c.Pinned.Rev)
+ }
}
// consoleGrant and consoleRevoke are carlos engines grant/revoke: the
-// database changes and the console publishes the next revision.
-func (w *world) consoleGrant(key string) {
+// database changes and the console publishes the next revision. A console
+// that is down takes neither (false).
+func (w *world) consoleGrant(key string) bool {
+ if w.console.Down {
+ w.logf("console: down; carlos engines grant %s fails", key)
+ return false
+ }
w.console.Grants[key] = true
w.publish(w.console.Rev + 1)
+ return true
}
-func (w *world) consoleRevoke(key string) {
+func (w *world) consoleRevoke(key string) bool {
+ if w.console.Down {
+ w.logf("console: down; carlos engines revoke %s fails", key)
+ return false
+ }
delete(w.console.Grants, key)
w.publish(w.console.Rev + 1)
+ return true
}
-// replay is a bucket writer restoring an older signed record: validly signed,
-// and unexpired unless 72 hours have passed.
-func (w *world) replay(rev int) {
+// replay is a bucket writer restoring an older signed record (validly signed,
+// and unexpired unless 72 hours have passed) and keeping it in the bucket
+// over everything the console publishes, until it stops (unpin).
+func (w *world) replay(rev int) { w.replayUntil(rev, 1<<62) }
+
+// replayUntil is replay for a writer who stops at tick until.
+func (w *world) replayUntil(rev, until int) {
rec := w.console.Records[rev]
if rec == nil {
panic(fmt.Sprintf("replay: no revision %d", rev))
}
- w.console.Bucket = rec
- w.logf("bucket writer: replays revision %d (newest %d) into the bucket", rev, w.console.Rev)
+ w.console.Bucket, w.console.Pinned, w.console.PinnedUntil = rec, rec, until
+ w.logf("bucket writer: replays revision %d (signed at %d; newest %d) into the bucket, until tick %d", rev, rec.SignedAt, w.console.Rev, until)
+}
+
+// unpin is the bucket writer stopping: the newest record is in the bucket
+// again.
+func (w *world) unpin() {
+ c := &w.console
+ c.Pinned, c.Bucket = nil, c.Records[c.Rev]
+ w.logf("bucket writer: stops; the bucket holds revision %d again", c.Rev)
}
func (w *world) setBucketDown(down bool) {
@@ -154,33 +196,14 @@ func (w *world) setBucketDown(down bool) {
w.logf("the bucket is unreachable = %v", down)
}
-// newestGrants is the oracle's truth for key: whether the newest record the
-// 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 rec.Grants[key] {
- if w.now() >= rec.Expires {
- return false, rec.Expires
- }
- return true, 0
- }
- if t, ok := w.console.RevokedAt[key]; ok {
- return false, t
- }
- return false, -1 << 30
-}
-
// ---------- the grant mirror (spec §5.3) ----------
// mirrorTick is one poll of b's mirror. It verifies the record's expiry and
-// refuses a revision below its floor (an equal revision is the same signed
-// bytes: the model's records are immutable per revision). A good read
-// replaces the record, raises the floor, and persists both before either is
-// used (floor-persisted).
+// its signed_at (a record signed more than ten minutes ago is stale, like an
+// expired one, grant-freshness-bound) and refuses a revision below its floor
+// (an equal revision is the same signed bytes: the model's records are
+// immutable per revision). A good read replaces the record, raises the floor,
+// and persists both before either is used (floor-persisted).
func (w *world) mirrorTick(b *box) {
m := &b.Mirror
c := &w.console
@@ -194,18 +217,26 @@ func (w *world) mirrorTick(b *box) {
}
return
}
+ if now-rec.SignedAt >= staleTicks && on("grant-freshness-bound") {
+ if m.Rec != rec {
+ w.logf("box%d: mirror refuses revision %d: signed at %d, ten minutes ago or more", b.ID, rec.Rev, rec.SignedAt)
+ }
+ return
+ }
if rec.Rev < m.Floor {
w.logf("box%d: mirror refuses revision %d: below the floor %d", b.ID, rec.Rev, m.Floor)
return
}
if rec.Rev > m.Floor || m.Rec == nil {
- b.FreshRead = m.Floor == 0 && b.Rebuilt
w.logf("box%d: mirror reads revision %d (floor %d -> %d)", b.ID, rec.Rev, m.Floor, rec.Rev)
}
m.Rec, m.ReadAt = rec, now
if rec.Rev > m.Floor {
m.Floor = rec.Rev
}
+ if rec.Rev > b.ReadRev {
+ b.ReadRev = rec.Rev
+ }
if on("floor-persisted") {
m.Persisted, m.PersistedFloor = m.Rec, m.Floor
}
@@ -225,16 +256,18 @@ func (w *world) restartEdge(b *box) {
}
// rebuild is a new or rebuilt box: its edge's data directory is gone, so it
-// has no floor and no record until its first read (the fresh-box residual,
-// §5.3).
+// has no floor and no record until its first read, and may admit any validly
+// signed record a bucket writer replays, until ten minutes after its signing
+// (§5.3). The oracle forgets what the box had read (ReadRev).
func (w *world) rebuild(b *box) {
b.Mirror = mirror{}
- b.Rebuilt, b.FreshRead = true, false
+ b.ReadRev = 0
w.logf("box%d: rebuilt: the edge has no persisted floor", b.ID)
}
-// tableGrants is b's grant table on key. Stale (no good read for ten
-// minutes), expired, or never read: empty (stale-clears-grants).
+// tableGrants is b's grant table on key. Never read: empty. No good read for
+// ten minutes, or expired: empty (stale-clears-grants). A record signed more
+// than ten minutes ago: empty (grant-freshness-bound, R5).
func (w *world) tableGrants(b *box, key string) bool {
m := b.Mirror
if m.Rec == nil {
@@ -243,6 +276,9 @@ func (w *world) tableGrants(b *box, key string) bool {
if on("stale-clears-grants") && (w.now()-m.ReadAt >= staleTicks || w.now() >= m.Rec.Expires) {
return false
}
+ if on("grant-freshness-bound") && w.now()-m.Rec.SignedAt >= staleTicks {
+ return false
+ }
return m.Rec.Grants[key]
}
@@ -365,7 +401,7 @@ func (w *world) placeCall(c call) bool {
seen = *c.forged
}
}
- return w.engineAdmit(home, b, seen, hostname, c.path, w.realApp(b, c.p), c.p)
+ return w.engineAdmit(home, b, seen, hostname, c.path, c.host, w.realApp(b, c.p), c.p)
}
// clientHop is a public client sending b's edge a request for hostname that
@@ -381,7 +417,7 @@ func (w *world) clientHop(b *box, hostname, path string, forged caller) bool {
}
return false
}
- return w.engineAdmit(b, b, forged, hostname, path, "", nil)
+ return w.engineAdmit(b, b, forged, hostname, path, "", "", nil)
}
// homeOf is the box whose registry has hostname (the edge's home map).
@@ -410,8 +446,10 @@ func (w *world) exactRoute(b *box, hostname string) (row, bool) {
// the hostname for the mark's engine and grant it to the mark's app
// (engine-box-recheck), and the route must be the hostname's own
// (exact-route-engine). Then the activator's dispatch, which may wake the
-// engine. real is the calling process's real app; p the process.
-func (w *world) engineAdmit(home, from *box, mark caller, hostname, path, real string, p *proc) bool {
+// engine. via is the instance whose engine socket or door key the call came
+// through ("" for a client's hop); real is the calling process's real app;
+// p the process.
+func (w *world) engineAdmit(home, from *box, mark caller, hostname, path, via, real string, p *proc) bool {
final, ok := w.exactRoute(home, hostname)
if !ok {
w.logf("box%d: engine call to %s: unknown host", home.ID, hostname)
@@ -446,7 +484,7 @@ func (w *world) engineAdmit(home, from *box, mark caller, hostname, path, real s
return false
}
w.logf("box%d: engine call reaches process %d (%s v%d); the access log records caller %s", home.ID, q.ID, q.Group, q.Ver, mark.app())
- w.checkCall(home, from, mark, real, p, q)
+ w.checkCall(home, from, mark, via, real, p, q)
return true
}
@@ -562,44 +600,39 @@ func (w *world) maybeForged() *caller {
return &c
}
-// replayable: a bucket writer's replay in the default world lands only once
-// 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: 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
- }
- for _, b := range w.boxes {
- if b.Mirror.Floor > 0 && b.Mirror.Floor < w.console.Rev {
- return false
- }
- }
- return true
-}
-
// pickReplay is the revision a bucket writer replays: one that grants a key
-// the console has since revoked, if any (the damaging choice), else any
-// older one.
+// the console has since revoked, if any (the damaging choice: half the time
+// the newest such, signed most recently, else any), else any older one.
func (w *world) pickReplay() int {
+ newest := w.console.Records[w.console.Rev]
var damaging []int
for r := 1; r < w.console.Rev; r++ {
for k := range w.console.Records[r].Grants {
- if g, _ := w.newestGrants(k); !g {
+ if !newest.Grants[k] {
damaging = append(damaging, r)
break
}
}
}
if len(damaging) > 0 {
+ if w.rng.Intn(2) == 0 {
+ return damaging[len(damaging)-1]
+ }
return damaging[w.rng.Intn(len(damaging))]
}
return 1 + w.rng.Intn(w.console.Rev-1)
}
+// walkReplay is the walk's bucket writer: it replays an older record and
+// keeps it in place for up to twenty minutes.
+func (w *world) walkReplay() bool {
+ if w.console.Rev < 2 {
+ return false
+ }
+ w.replayUntil(w.pickReplay(), w.now()+1+w.rng.Intn(2*staleTicks))
+ return true
+}
+
// callers are the nested instance groups on b with an engine socket open.
func (w *world) callers(b *box) []string {
var out []string
@@ -612,14 +645,26 @@ func (w *world) callers(b *box) []string {
}
func init() {
- // the mirror polls every 30 s, whatever the walk does
- stepHooks = append(stepHooks, func(w *world) {
- if w.now()%pollTicks == 0 {
- for _, b := range w.boxes {
- w.mirrorTick(b)
+ stepHooks = append(stepHooks,
+ // a bucket writer whose time is up stops; the console, while up,
+ // re-signs every two minutes (R5)
+ func(w *world) {
+ c := &w.console
+ if c.Pinned != nil && w.now() >= c.PinnedUntil {
+ w.unpin()
}
- }
- })
+ if !c.Down && w.now()-c.Records[c.Rev].SignedAt >= resignTicks {
+ w.publish(c.Rev + 1)
+ }
+ },
+ // the mirror polls every 30 s, whatever the walk does
+ func(w *world) {
+ if w.now()%pollTicks == 0 {
+ for _, b := range w.boxes {
+ w.mirrorTick(b)
+ }
+ }
+ })
actions = append(actions,
action{name: "engine-call", weight: 4, run: func(w *world) {
b := w.pickBox()
@@ -669,7 +714,15 @@ func init() {
w.consoleRevoke(keys[w.rng.Intn(len(keys))])
}
}},
- action{name: "console-resign", weight: 1, run: func(w *world) { w.publish(w.console.Rev + 1) }},
+ action{name: "console-resign", weight: 1, run: func(w *world) {
+ if !w.console.Down {
+ w.publish(w.console.Rev + 1)
+ }
+ }},
+ action{name: "console-down", weight: 1, run: func(w *world) {
+ w.console.Down = !w.console.Down && !w.calm()
+ w.logf("console: down = %v", w.console.Down)
+ }},
action{name: "bucket-down", weight: 1, run: func(w *world) {
w.setBucketDown(!w.console.BucketDown && !w.calm())
}},
@@ -678,15 +731,17 @@ func init() {
return
}
if w.rng.Intn(8) == 0 {
+ w.console.Down = true
+ w.logf("console: down = true")
w.advance(lifetimeTicks + staleTicks) // the console is down for three days
return
}
w.advance(staleTicks) // ten minutes with no poll
}},
+ // any older signed record, at any time: the freshness bound, not the
+ // walk, limits what a replay can do (R5)
action{name: "replay", weight: 1, run: func(w *world) {
- if w.replayable() {
- w.replay(w.pickReplay())
- }
+ w.walkReplay()
}},
action{name: "restart-edge", weight: 2, run: func(w *world) {
switch w.rng.Intn(3) {
@@ -697,15 +752,11 @@ func init() {
case 1:
w.restartEdge(w.pickBox())
default:
- // a rebuilt box: the calling box, or under freshBoxReplay any
- // box (the engine's home too); a bucket writer may replay at once
- b := w.boxes[1]
- if w.freshBoxReplay {
- b = w.pickBox()
- }
- w.rebuild(b)
- if w.rng.Intn(2) == 0 && w.replayable() {
- w.replay(w.pickReplay())
+ // a rebuilt box, the engine's home included; a bucket writer
+ // may replay at once
+ w.rebuild(w.pickBox())
+ if w.rng.Intn(2) == 0 {
+ w.walkReplay()
}
}
}},
@@ -759,14 +810,14 @@ func init() {
// mirrorsState is a one-line summary of the console and every mirror, for a
// failing witness.
func (w *world) mirrorsState() string {
- out := []string{fmt.Sprintf("console{rev %d bucket %d down %v now %d}", w.console.Rev, w.console.Bucket.Rev, w.console.BucketDown, w.now())}
+ out := []string{fmt.Sprintf("console{rev %d bucket %d bucketDown %v down %v pinned %v now %d}", w.console.Rev, w.console.Bucket.Rev, w.console.BucketDown, w.console.Down, w.console.Pinned != nil, w.now())}
for _, b := range w.boxes {
m := b.Mirror
rev := 0
if m.Rec != nil {
rev = m.Rec.Rev
}
- out = append(out, fmt.Sprintf("box%d{rec %d floor %d readAt %d persisted %d armed %v sockets %v rebuilt %v}", b.ID, rev, m.Floor, m.ReadAt, m.PersistedFloor, b.Armed, b.Sockets, b.Rebuilt))
+ out = append(out, fmt.Sprintf("box%d{rec %d floor %d readAt %d persisted %d readRev %d armed %v sockets %v}", b.ID, rev, m.Floor, m.ReadAt, m.PersistedFloor, b.ReadRev, b.Armed, b.Sockets))
}
return strings.Join(out, " ")
}
diff --git a/internal/sim/engines/expected-outcomes.txt b/internal/sim/engines/expected-outcomes.txt
index ba3bd6bf0..03c910d34 100644
--- a/internal/sim/engines/expected-outcomes.txt
+++ b/internal/sim/engines/expected-outcomes.txt
@@ -9,3 +9,4 @@
gate-adopt missed caught with set-before-repoint (witness): adoption's set-before is the same gate reached earlier, so with it in place the restart's gate always finds the group already fenced
public-stops-group missed caught with public-confirms-empty (witness): without the stop, --public step 3 finds the declaring generation still serving and refuses, so the clear never writes 0 under it
dedicated-launch-check missed caught with dedicated-edge-refusal (witness): without the launch check a declaring adoption beside a proxying row goes ahead, but the edge's refusal then refuses that row once the group is internal, so no public request reaches the engine
+stale-clears-grants missed caught with grant-freshness-bound (witness): a table's record was signed no later than its last good read, and expires long after it goes stale by its signing, so the signed_at bound (R5) empties a stale or expired table first; with both gone the stale table serves a revoked grant
diff --git a/internal/sim/engines/invariants_test.go b/internal/sim/engines/invariants_test.go
index 8e921eed8..d0dbe5fc1 100644
--- a/internal/sim/engines/invariants_test.go
+++ b/internal/sim/engines/invariants_test.go
@@ -174,19 +174,18 @@ func (w *world) avExempt(b *box, host string) string {
// ---------- Task 5: INV-ID, INV-G, INV-ARM (calls_test.go) ----------
// checkCall is INV-ID and INV-G for an engine call that reached process q on
-// home, sent by process p (nil: a public client) on box from.
+// home, sent by process p (nil: a public client) on box from through the
+// engine socket or door key of instance via.
//
// - INV-ID: the caller the engine box records is the app whose code made
-// the call.
-// - INV-G: the call reaches the engine's exact route, and the newest record
-// the console published grants it, unless the revoke is younger than the
-// freshness bound (§6.4: within ten minutes of the last good read a box
-// may still grant; both boxes' bounds run from the same revoke, so a call
-// past it got through two tables that should both have dropped it).
-func (w *world) checkCall(home, from *box, mark caller, real string, p, q *proc) {
+// the call. The flat-era residual covers only a call whose recorded
+// caller is the compromised instance itself (compromisedItself).
+// - INV-G: the call reaches the engine's exact route, and grantBreach finds
+// no breach of the grant's freshness.
+func (w *world) checkCall(home, from *box, mark caller, via, real string, p, q *proc) {
if mark.app() != real {
msg := fmt.Sprintf("box%d: the engine box records caller %s for a call made by %q (process %v)", home.ID, mark.app(), real, procID(p))
- if w.flatEraTamper && p != nil && p.Code != "" && !p.Unisolated {
+ if w.flatEraTamper && w.compromisedItself(from, mark, via, p) {
w.residual("flatEraTamper", "%s: code planted before the box was armed", msg)
} else {
w.fail("INV-ID", "%s", msg)
@@ -196,20 +195,91 @@ func (w *world) checkCall(home, from *box, mark caller, real string, p, q *proc)
if want := truthGroup(home, exact.Host); q.Group != want {
w.fail("INV-G", "box%d: an engine call for %s reached process %d of %s, not the engine's exact route %s", home.ID, mark.key(), q.ID, q.Group, want)
}
- if granted, since := w.newestGrants(mark.key()); !granted && w.now()-since >= staleTicks {
- msg := fmt.Sprintf("box%d: an engine call for %s reached process %d of %s; the newest record (revision %d) has not granted it since tick %d, now %d", home.ID, mark.key(), q.ID, q.Group, w.console.Rev, since, w.now())
- if w.freshBoxReplay && w.freshGrant(from, mark.key()) && w.freshGrant(home, mark.key()) {
- w.residual("freshBoxReplay", "%s: both boxes hold a replayed record with no floor", msg)
- } else {
- w.fail("INV-G", "%s", msg)
+ if why := w.grantBreach(home, from, mark.key()); why != "" {
+ w.fail("INV-G", "box%d: an engine call for %s reached process %d of %s; %s", home.ID, mark.key(), q.ID, q.Group, why)
+ }
+}
+
+// compromisedItself: the flat-era residual's own case, from facts no rule
+// changes. Process p is the instance via's own process, in via's own slice,
+// running the code planted in via's directory, and the caller recorded is
+// via's own app. Planted code that borrows another instance's socket or
+// forges a hop caller is a violation like any other.
+func (w *world) compromisedItself(from *box, mark caller, via string, p *proc) bool {
+ if p == nil || p.Code == "" || p.Unisolated || via == "" {
+ return false
+ }
+ r := from.Rows[via]
+ return r != nil && p.Group == via && p.Slice == "inst:"+via && from.Tampered[via] == p.Code && mark.app() == r.App
+}
+
+// grantBreach is INV-G's grant clauses for key on a call admitted by the
+// tables of from and home, each from facts no rule changes (spec §5.3, §6.4,
+// ruling R5). It returns the first breach, or "".
+//
+// 1. Expiry: a key the newest record grants is granted by no table once that
+// record has expired (every older record expired first), at once.
+// 2. Revoke age: a key the newest record does not grant is granted by no
+// table more than ten minutes plus one poll after the revoke, whatever
+// was replayed (every record that grants it was signed before the
+// revoke, and is stale ten minutes after its signing). A key no record
+// ever granted is never granted.
+// 3. The admitting tables: neither box admits on a table that was never
+// read, holds an expired record, has had no good read for ten minutes, or
+// holds a record signed ten minutes ago or more, whatever the key's
+// revoke (from always checks its table; home is the engine box, whose
+// table must be empty too).
+// 4. A revoke a box has read stays in force there (§6.4: the floor refuses
+// every older record).
+func (w *world) grantBreach(home, from *box, key string) string {
+ c := &w.console
+ now := w.now()
+ newest := c.Records[c.Rev]
+ if newest.Grants[key] && now >= newest.Expires {
+ return fmt.Sprintf("the newest record (revision %d), which grants it, expired at %d, now %d", newest.Rev, newest.Expires, now)
+ }
+ if !newest.Grants[key] {
+ since, ok := c.RevokedAt[key]
+ if !ok {
+ return fmt.Sprintf("no record has granted it (newest revision %d)", newest.Rev)
+ }
+ if now-since > staleTicks+pollTicks {
+ return fmt.Sprintf("the newest record (revision %d) has not granted it since tick %d, now %d", newest.Rev, since, now)
+ }
+ }
+ boxes := []*box{from}
+ if home != from {
+ boxes = append(boxes, home)
+ }
+ for _, b := range boxes {
+ if why := w.tableStale(b); why != "" {
+ return fmt.Sprintf("box%d admitted it on a table that %s", b.ID, why)
+ }
+ }
+ if rr, ok := c.RevokedRev[key]; ok && !newest.Grants[key] {
+ for _, b := range boxes {
+ if b.ReadRev >= rr {
+ return fmt.Sprintf("box%d had read revision %d, which revoked it (read %d)", b.ID, rr, b.ReadRev)
+ }
}
}
+ return ""
}
-// freshGrant: b's table grants key from a record b accepted with no floor
-// after it was rebuilt (the fresh-box residual).
-func (w *world) freshGrant(b *box, key string) bool {
- return b.FreshRead && w.tableGrants(b, key)
+// tableStale says why b's table must be empty, or "".
+func (w *world) tableStale(b *box) string {
+ m, now := b.Mirror, w.now()
+ switch {
+ case m.Rec == nil:
+ return "was never read"
+ case now >= m.Rec.Expires:
+ return fmt.Sprintf("holds revision %d, expired at %d, now %d", m.Rec.Rev, m.Rec.Expires, now)
+ case now-m.ReadAt >= staleTicks:
+ return fmt.Sprintf("has had no good read for %d ticks", now-m.ReadAt)
+ case now-m.Rec.SignedAt >= staleTicks:
+ return fmt.Sprintf("holds revision %d, signed at %d, %d ticks ago", m.Rec.Rev, m.Rec.SignedAt, now-m.Rec.SignedAt)
+ }
+ return ""
}
func procID(p *proc) any {
diff --git a/internal/sim/engines/rules_test.go b/internal/sim/engines/rules_test.go
index b4e8b8b22..d988036f5 100644
--- a/internal/sim/engines/rules_test.go
+++ b/internal/sim/engines/rules_test.go
@@ -88,7 +88,8 @@ var allRules = []string{
"arm-checks-box", // arming refuses a box with an unisolated route or a non-empty carlos-exec@ cgroup (R5-2)
// Final review (spec §5.1 "The invariant", "Becoming public is never
- // automatic")
- "new-group-fenced", // a new or unseen row's NULL is never fenced: a first declaring launch writes 1 and waits for the fence
- "clear-launch-lock", // the launch gate takes the group's lock, which --public holds for its whole run
+ // automatic"; §5.2, §5.3 the freshness bound, ruling R5)
+ "new-group-fenced", // a new or unseen row's NULL is never fenced: a first declaring launch writes 1 and waits for the fence
+ "clear-launch-lock", // the launch gate takes the group's lock, which --public holds for its whole run
+ "grant-freshness-bound", // a record signed ten minutes ago or more is stale: the mirror refuses it and the table is empty
}
diff --git a/internal/sim/engines/witness_test.go b/internal/sim/engines/witness_test.go
index c463bc041..1fa64571f 100644
--- a/internal/sim/engines/witness_test.go
+++ b/internal/sim/engines/witness_test.go
@@ -108,13 +108,13 @@ var witnesses = []witness{
{"hop-caller-signed", "hop-caller-signed", "INV-ID",
"a public client sends the engine box a request carrying X-Carlos-Hop-Caller naming a granted app; an engine box that takes the caller from the header rather than a verified hop records that app as the caller", wHopCallerSigned},
{"engine-box-recheck", "engine-box-recheck", "INV-G",
- "G4: the calling box is rebuilt (no floor) and a bucket writer replays the record revoked ten minutes ago; the calling box admits on its superseded table; an engine box that trusts the calling box's admission serves the revoked app", wEngineBoxRecheck},
+ "G4: a revoke is read everywhere; the calling box is rebuilt (no floor) and a bucket writer at once replays the record the revoke superseded, still inside its ten minutes; the calling box admits on it; an engine box that trusts the calling box's admission serves the revoked app although it has read the revoke", wEngineBoxRecheck},
{"exact-route-engine", "exact-route-engine", "INV-G",
"R4-2: an app holds engine A's grant only; A's hostname is a static row whose path map points at engine B's route; an engine call resolved through the path map reaches B", wExactRouteEngine},
{"floor-persisted", "floor-persisted", "INV-G",
- "R1-4: a grant is revoked and read everywhere; a bucket writer replays the older record, which the floor refuses; both edges restart; a floor not persisted admits the replay and the revoked grant serves past the freshness bound", wFloorPersisted},
- {"stale-clears-grants", "stale-clears-grants", "INV-G",
- "§6.4: the bucket is unreachable when a revoke is published; ten minutes pass with no good read; a stale table that still grants serves the revoked app past the bound", wStaleClearsGrants},
+ "R1-4: a grant is revoked and read everywhere; a bucket writer at once replays the older record, still inside its ten minutes, which the floor refuses; both edges restart; a floor not persisted admits the replay, and the revoke both boxes had read is no longer in force", wFloorPersisted},
+ {"stale-clears-grants", "stale-clears-grants,grant-freshness-bound", "INV-G",
+ "§6.4: redundant alone: a table's record was signed no later than its last good read, so the signed_at bound empties a stale table first. The bucket is unreachable when a revoke is published; ten minutes pass with no good read; with both checks gone the stale table still grants and serves the revoked app", wStaleClearsGrants},
{"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
"R3-2/R4-1: on an armed box with engine sockets open, a foreign instance starts and a worker spawns; a box that does not refuse them runs unisolated tenant code beside open sockets", wArmedRefusesUnisolated},
{"armed-refuses-unisolated", "armed-refuses-unisolated", "INV-ARM",
@@ -127,6 +127,8 @@ var witnesses = []witness{
// Final review
{"new-group-fenced", "new-group-fenced", "INV-I1+INV-P",
"a public request is admitted through a service row aimed at address X and held; the row is deleted; a declaring instance is provisioned at X; a new row's NULL taken as fenced lets its first launch skip the reload, so the held request is never drained and reaches the engine", wNewGroupFenced},
+ {"grant-freshness-bound", "grant-freshness-bound", "INV-G",
+ "R5: the console re-signs (revision 2) and both edges read it; it revokes shop (revision 3) and a bucket writer puts revision 2 back before any edge reads 3; the floor admits it (equal revision); a mirror with no signed_at bound keeps the revoked grant until revision 2 expires, so a call ten minutes and one poll later reaches the engine", wGrantFreshnessBound},
{"clear-launch-lock", "clear-launch-lock", "INV-I1+INV-P",
"--public on an internal group whose live release is plain; after its empty check and before its write of 0, a carlos run command of a declaring build passes the gate (the group is still fenced as internal); a launch that ignores the group's lock starts it, and --public writes 0 under it", wClearLaunchLock},
}
@@ -1326,6 +1328,62 @@ func wClearLaunchLock(t *testing.T, w *world) {
w.check()
}
+// wGrantFreshnessBound (final review, finding 3; ruling R5): thirty ticks in,
+// the console re-signs (revision 2, granting shop) and both edges read it;
+// the console revokes shop (revision 3) and a bucket writer puts revision 2
+// back before any edge reads 3. Each edge reads revision 2 again (equal to
+// its floor: the same signed bytes). Shop calls at once (within the bound),
+// then again ten minutes and one poll after the revoke.
+func wGrantFreshnessBound(t *testing.T, w *world) {
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ w.advance(30)
+ w.publish(w.console.Rev + 1) // the periodic re-sign: revision 2, signed at 30
+ w.pollAll()
+ w.consoleRevoke(shopEng) // revision 3, at 30
+ w.replay(2)
+ w.pollAll()
+ w.check()
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ w.check()
+ w.advance(staleTicks + pollTicks + 1)
+ w.pollAll()
+ w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
+ w.check()
+}
+
+// TestReplayBoundedBySignedAt (ruling R5): wGrantFreshnessBound's replay, with
+// every rule in place, keeps the revoked grant on both edges until the
+// replayed record's signed_at plus ten minutes, and not one tick longer.
+func TestReplayBoundedBySignedAt(t *testing.T) {
+ w := newWitness()
+ w.runningEngine(t)
+ shop := w.armedShop(t)
+ w.advance(30)
+ w.publish(w.console.Rev + 1)
+ signed := w.now()
+ w.pollAll()
+ w.consoleRevoke(shopEng)
+ w.replay(2)
+ w.advance(staleTicks - 1) // 59 ticks after revision 2 was signed
+ w.pollAll()
+ if !w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/") {
+ t.Errorf("at signed_at+%d the replayed record should still grant (the bound is not tighter than R5): %s", w.now()-signed, w.mirrorsState())
+ }
+ w.advance(1)
+ w.pollAll()
+ if w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/") {
+ t.Errorf("at signed_at+%d the replayed record still grants: %s", w.now()-signed, w.mirrorsState())
+ }
+ w.check()
+ if len(w.violations) > 0 || len(w.residuals) > 0 {
+ t.Errorf("violations %v residuals %v", w.violations, w.residuals)
+ }
+ if t.Failed() {
+ dump(t, w)
+ }
+}
+
// ---------- Task 5: calls, identity, grants and arming ----------
// shopEng is the grant every Task 5 world starts with: shop may call eng.
@@ -1396,8 +1454,8 @@ func wHopCallerSigned(t *testing.T, w *world) {
// wEngineBoxRecheck (G4): shop's grant is revoked and read everywhere; box
// 1's data directory is lost (a rebuilt box: no floor), and a bucket writer
-// replays revision 1; box 1 accepts it, box 0's floor refuses it; ten
-// minutes pass; shop calls eng.
+// at once replays revision 1, signed moments ago; box 1 accepts it, box 0's
+// floor refuses it; shop calls eng.
func wEngineBoxRecheck(t *testing.T, w *world) {
w.runningEngine(t)
shop := w.armedShop(t)
@@ -1407,8 +1465,6 @@ func wEngineBoxRecheck(t *testing.T, w *world) {
w.rebuild(b1)
w.replay(1)
w.pollAll()
- w.advance(staleTicks)
- w.pollAll()
w.check()
if !w.tableGrants(b1, shopEng) {
t.Fatalf("witness: the rebuilt calling box does not hold the replayed grant: %s", w.mirrorsState())
@@ -1431,15 +1487,14 @@ func wExactRouteEngine(t *testing.T, w *world) {
w.check()
}
-// wFloorPersisted (R1-4): shop's grant is revoked and read everywhere; ten
-// minutes pass; a bucket writer replays revision 1, which both floors
-// refuse; both edges restart; each polls; shop calls eng.
+// wFloorPersisted (R1-4): shop's grant is revoked and read everywhere; a
+// bucket writer at once replays revision 1 (signed moments ago), which both
+// floors refuse; both edges restart; each polls; shop calls eng.
func wFloorPersisted(t *testing.T, w *world) {
w.runningEngine(t)
shop := w.armedShop(t)
w.consoleRevoke(shopEng)
w.pollAll()
- w.advance(staleTicks)
w.replay(1)
w.pollAll()
for _, b := range w.boxes {
@@ -1502,8 +1557,8 @@ func wArmChecksBox(t *testing.T, w *world) {
w.check()
}
-// TestResidualsAreCountedNotFailed: each of the spec's three stated
-// residuals, as a fixed scenario. With its flag off the scenario is a
+// TestResidualsAreCountedNotFailed: each of the spec's two stated residuals,
+// as a fixed scenario. With its flag off the scenario is a
// violation (the sequence really breaks the invariant the residual
// concedes); with the flag on the world records residual:<name> and no
// violation. The default world never sets a flag (TestEngines asserts the
@@ -1514,7 +1569,6 @@ func TestResidualsAreCountedNotFailed(t *testing.T) {
set func(w *world)
run func(t *testing.T, w *world)
}{
- {"freshBoxReplay", func(w *world) { w.freshBoxReplay = true }, residualFreshBoxReplay},
{"unwrittenManifestAcrossUpgrade", func(w *world) { w.unwrittenManifestAcrossUpgrade = true }, residualUnwrittenManifest},
{"flatEraTamper", func(w *world) { w.flatEraTamper = true }, residualFlatEraTamper},
}
@@ -1542,25 +1596,6 @@ func TestResidualsAreCountedNotFailed(t *testing.T) {
}
}
-// residualFreshBoxReplay (§5.3): shop's grant is revoked and read
-// everywhere; both boxes are rebuilt (no floor anywhere); a bucket writer
-// replays revision 1; both accept it; ten minutes pass; shop calls eng.
-func residualFreshBoxReplay(t *testing.T, w *world) {
- w.runningEngine(t)
- shop := w.armedShop(t)
- w.consoleRevoke(shopEng)
- w.pollAll()
- for _, b := range w.boxes {
- w.rebuild(b)
- }
- w.replay(1)
- w.pollAll()
- w.advance(staleTicks)
- w.pollAll()
- w.engineCall(w.boxes[1], shop, false, "carlos", "shop", eng, "/")
- w.check()
-}
-
// residualUnwrittenManifest (§5.1 "Classification before serving"): the
// engine runs a declaring build whose staged manifest was never written;
// an awake repoint moves its live link to a plain build without a restart;
@@ -1705,13 +1740,19 @@ func withMutation(m string, f func()) {
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.
+// TestExpiryKeepsRevokeAge: the grant oracle keeps expiry, staleness and
+// revoke age apart (final review, finding 4). With the table's own checks off
+// (stale-clears-grants and grant-freshness-bound), the edges keep serving a
+// cached grant, and the oracle alone decides:
+// - a key revoked long before the newest record expires is a violation by
+// its revoke's age, whatever the expiry;
+// - a key the newest record grants is a violation the moment that record
+// expires: an expired record admits nothing, with no grace;
+// - a key nobody revoked is a violation once the admitting box has had no
+// good read for ten minutes, whatever the revoke's age (there is none),
+// and not a tick earlier.
func TestExpiryKeepsRevokeAge(t *testing.T) {
- withMutation("stale-clears-grants", func() {
+ withMutation("stale-clears-grants,grant-freshness-bound", func() {
w := newWitness()
w.runningEngine(t)
shop := w.armedShop(t)
@@ -1730,13 +1771,25 @@ func TestExpiryKeepsRevokeAge(t *testing.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) != 1 || invariantOf(w.violations[0]) != "INV-G" || !strings.Contains(w.violations[0], "expired at 25920") {
+ t.Errorf("a granted key at its record's expiry: want INV-G at once, naming the expiry, got %v", w.violations)
+ dump(t, w)
+ }
+
+ w = newWitness()
+ w.runningEngine(t)
+ shop = w.armedShop(t)
+ w.setBucketDown(true)
+ w.advance(staleTicks - 1) // no good read for 59 ticks; shop still granted
+ 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)
+ t.Errorf("a granted key 59 ticks after the last good read is within the bound: got %v", w.violations)
+ dump(t, w)
}
- w.advance(staleTicks)
+ w.advance(1)
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)
+ if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-G" || !strings.Contains(w.violations[0], "no good read") {
+ t.Errorf("a granted key ten minutes after the last good read: want INV-G for the stale read, got %v", w.violations)
dump(t, w)
}
})
@@ -1801,6 +1854,90 @@ func TestResidualCoversOnlyItsOwnBreaches(t *testing.T) {
})
}
+// flatEraFixture is residualFlatEraTamper's setup with the flag on, the
+// tamper planted in group target's instance directory instead of shop's: a
+// flat tenant on unarmed box 1 plants it, its route moves off, the box is
+// armed, and shop and other (a sibling instance) start. It returns box 1.
+func flatEraFixture(t *testing.T, target string) (*world, *box) {
+ w := newWitness()
+ w.flatEraTamper = true
+ w.runningEngine(t)
+ b := w.boxes[1]
+ if !w.provision(b, "other", "acct/other", "127.0.0.1:9002", vPlain) {
+ t.Fatalf("fixture: provisioning other refused: %s", w.boxesState())
+ }
+ b.Live["shop"], b.Good["shop"] = vPlain, vPlain
+ if !w.launchUnisolated(b, "flat") {
+ t.Fatalf("fixture: a flat start on an unarmed box refused: %s", w.boxesState())
+ }
+ w.tamper(b, w.newest(b, "flat"), target)
+ w.moveToNested(b, "flat")
+ if !w.arm(b) {
+ t.Fatalf("fixture: arming refused after the flat route moved: %s", w.boxesState())
+ }
+ for _, g := range []string{"shop", "other"} {
+ w.stopGroup(b, g)
+ if !w.launch(b, g, vPlain, "seed") {
+ t.Fatalf("fixture: %s did not start: %s", g, w.boxesState())
+ }
+ }
+ w.check()
+ if len(w.violations) > 0 {
+ t.Fatalf("fixture: violations %v", w.violations)
+ }
+ return w, b
+}
+
+// TestFlatEraTamperKeepsUnrelatedViolations: the flat-era residual covers a
+// call whose recorded caller is the compromised instance itself, made by its
+// own process in its own slice (final review, finding 5). Combined with an
+// unrelated mutation, the unrelated breach stays a violation:
+// - cgroup-identity off: planted code in other borrows shop's engine
+// socket; the engine box records shop, which is not the compromised
+// instance;
+// - hop-caller-signed off: planted code in shop sends its own socket's call
+// with an X-Carlos-Hop-Caller naming another granted app, which the
+// engine box takes.
+//
+// And the positive control: planted code in shop calling through shop's own
+// socket is the residual, not a violation.
+func TestFlatEraTamperKeepsUnrelatedViolations(t *testing.T) {
+ t.Run("own socket: the residual", func(t *testing.T) {
+ w, b := flatEraFixture(t, "shop")
+ w.engineCall(b, w.newest(b, "shop"), false, "carlos", "shop", eng, "/")
+ w.check()
+ if len(w.violations) > 0 || len(w.residuals) != 1 || !strings.HasPrefix(w.residuals[0], "residual:flatEraTamper:") {
+ t.Errorf("want residual:flatEraTamper and no violation, got violations %v residuals %v", w.violations, w.residuals)
+ dump(t, w)
+ }
+ })
+ t.Run("cgroup-identity off: a borrowed socket", func(t *testing.T) {
+ w, b := flatEraFixture(t, "other")
+ withMutation("cgroup-identity", func() {
+ w.engineCall(b, w.newest(b, "other"), false, "carlos", "shop", eng, "/")
+ })
+ w.check()
+ if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-ID" || len(w.residuals) > 0 {
+ t.Errorf("want INV-ID and no residual, got violations %v residuals %v", w.violations, w.residuals)
+ dump(t, w)
+ }
+ })
+ t.Run("hop-caller-signed off: a forged hop caller", func(t *testing.T) {
+ w, b := flatEraFixture(t, "shop")
+ w.consoleGrant("acct/tcp/" + eng)
+ w.pollAll()
+ forged := callerOf("acct/tcp", eng)
+ withMutation("hop-caller-signed", func() {
+ w.placeCall(call{from: b, p: w.newest(b, "shop"), uid: "carlos", host: "shop", engine: eng, path: "/", forged: &forged})
+ })
+ w.check()
+ if len(w.violations) != 1 || invariantOf(w.violations[0]) != "INV-ID" || len(w.residuals) > 0 {
+ t.Errorf("want INV-ID and no residual, got violations %v residuals %v", w.violations, w.residuals)
+ dump(t, w)
+ }
+ })
+}
+
// TestWitnessesHoldUnmutated: every witness holds with every rule in place.
// A witness that violates unmutated is a model bug, and a witness that
// passes under its mutation for the wrong reason starts here (Review Focus 1).
diff --git a/internal/sim/engines/world_test.go b/internal/sim/engines/world_test.go
index 8955bec69..f3d8196d4 100644
--- a/internal/sim/engines/world_test.go
+++ b/internal/sim/engines/world_test.go
@@ -143,14 +143,14 @@ type box struct {
// kind (flat, foreign, worker). Tampered is a nested group's instance
// directory written by an unisolated tenant: the planter's app.
//
- // Rebuilt and FreshRead are the oracle's, not the protocol's: the box was
- // rebuilt (its data directory lost), and its table holds a record it
- // accepted with no floor since then (the fresh-box residual, §5.3).
- Mirror mirror
- Sockets bool
- Unisolated map[string]bool
- Tampered map[string]string
- Rebuilt, FreshRead bool
+ // ReadRev is the oracle's, not the protocol's: the highest revision the
+ // box's mirror has read since it was last rebuilt (a restart keeps it), so
+ // INV-G can hold a revoke the box has read in force (§6.4).
+ Mirror mirror
+ Sockets bool
+ Unisolated map[string]bool
+ Tampered map[string]string
+ ReadRev int
}
type world struct {
@@ -181,11 +181,12 @@ type world struct {
console engConsole
skew int
- // The spec's three stated residuals. Off by default and set only by
- // tests: with one on, the walk may generate its sequence, and the breach
- // it causes is recorded in residuals as residual:<name>, never in
- // violations.
- freshBoxReplay, unwrittenManifestAcrossUpgrade, flatEraTamper bool
+ // The spec's two stated residuals. Off by default and set only by tests:
+ // with one on, the walk may generate its sequence, and the breach it
+ // causes is recorded in residuals as residual:<name>, never in
+ // violations. (A fresh box's replay was a third until ruling R5 bounded
+ // it by the freshness bound; INV-G now covers it.)
+ unwrittenManifestAcrossUpgrade, flatEraTamper bool
verbose bool
}