177192087 · carlos/platform

diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go

index 642f71695..cf45639e0 100644

--- a/internal/sim/hostlife/background_test.go

+++ b/internal/sim/hostlife/background_test.go

@@ -163,7 +163,7 @@ func (w *world) adopt() bool {

if w.claim != nil || w.rec == nil {

return false

}

- eb := w.regionBox(w.rec.Region)

+ eb := w.adoptionOwner(w.rec.Region) // exactly one proven owner (claim P5-D2)

if eb == nil {

return false

}

@@ -468,7 +468,7 @@ func (w *world) fault() {

func (w *world) replaceDestroyed() {

for r := 0; r < nRegions; r++ {

- if w.regionBox(r) == nil {

+ for len(w.regionBoxes(r)) < w.perRegion { // the region's minimum (H5): the group launches replacements

w.nextID++

nb := &box{ID: 100 + w.nextID, Region: r, HasKey: true}

nb.forget()

diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go

index c85851365..10cad9a39 100644

--- a/internal/sim/hostlife/console_test.go

+++ b/internal/sim/hostlife/console_test.go

@@ -237,7 +237,9 @@ func (w *world) createSteps(p *consolePlan) bool {

}

return abandon()

}

- b := w.regionBox(p.Region)

+ // the executor, chosen once and recorded in the intent (region HA

+ // §5.2, H12, L8; claim P5-D6 selected_executor)

+ b := w.chooseBox(p.Region, p.App)

if b == nil || (c != nil && contains(c.Lost, b.ID)) {

return abandon()

}

@@ -253,7 +255,7 @@ func (w *world) createSteps(p *consolePlan) bool {

w.violate("INV-20: create %s claimed the host while %d obligation(s) were outstanding (%s %s)", p.OpID, len(n.Obl), n.Obl[0].Kind, n.Obl[0].Prefix)

}

n.Holder = &holder{Inc: p.Inc, App: p.App, Serial: w.serial, Location: locationFor(p.Inc, false), WriterBox: -1} // no writer yet

- n.Op = opState{Kind: "creating", ID: p.OpID, Exec: -1, NewInc: p.Inc, NewApp: p.App, NewRegion: p.Region, ReqAt: w.now}

+ n.Op = opState{Kind: "creating", ID: p.OpID, Exec: -1, NewInc: p.Inc, NewApp: p.App, NewRegion: p.Region, NewBox: b.ID, ReqAt: w.now}

n.Regions, n.Boxes, n.Complete, n.Obl = []int{p.Region}, []int{b.ID}, true, nil

return true

}) {

@@ -315,7 +317,7 @@ func (w *world) createSteps(p *consolePlan) bool {

}

return false

}

- b := w.regionBox(c.Op.NewRegion)

+ b := w.createExecutor(c)

if b == nil {

return false

}

@@ -383,6 +385,25 @@ func (w *world) userMove() {

// moveTo requests a move of the serving host to region r. A witness calls

// it directly (witness_test.go).

+// createExecutor is the box a create's step 4 hands op.exec to: the one

+// its intent named, never another (region HA §5.2, claim P5-D2: recovery

+// never substitutes a newly available box); nil while that box is gone.

+// The mutation of create-choice-once chooses again, as rev 7.22's

+// region-wide pick did.

+func (w *world) createExecutor(c *claim) *box {

+ if w.perRegion <= 1 {

+ return w.regionBox(c.Op.NewRegion) // the one-box shape: today's region-wide pick, unchanged (spec §4; rev 4, Astra R1-1)

+ }

+ if !on("create-choice-once") {

+ return w.chooseBox(c.Op.NewRegion, c.Holder.App)

+ }

+ b := w.boxByID(c.Op.NewBox)

+ if b == nil || b.Destroyed {

+ return nil

+ }

+ return b

+}

+

func (w *world) moveTo(r int) {

c := w.claim

if c == nil || c.Holder == nil || c.Op.Kind != "serving" {

@@ -395,7 +416,7 @@ func (w *world) moveTo(r int) {

if r == src.Region {

return

}

- tgt := w.regionBox(r)

+ tgt := w.chooseBox(r, c.Holder.App) // the target box, chosen in the start CAS (region HA L15)

if tgt == nil || contains(c.Lost, tgt.ID) || tgt.Old {

return

}

@@ -1058,8 +1079,30 @@ func (w *world) recoveryPass() {

return

}

if w.rec != nil && w.rec.Inc == c.Holder.Inc {

- b := w.regionBox(c.Op.NewRegion)

+ b := w.createExecutor(c)

if b == nil {

+ if nb := w.boxByID(c.Op.NewBox); w.perRegion > 1 && on("create-choice-once") && (nb == nil || nb.Destroyed) {

+ // the chosen box cannot complete the create (the two-box

+ // shape only; the one-box shape waits for its region's

+ // box, as the baseline does): recovery cancels it (claim

+ // §5.1 step 5, P5-D6), retiring the

+ // incarnation; the record is an orphan the cleanup removes

+ inc, app, id := c.Holder.Inc, c.Holder.App, c.Op.ID

+ if w.cas(c, func(n *claim) bool {

+ if !sameOp(n.Op.ID, id) {

+ return false

+ }

+ n.Holder, n.Op = nil, opState{}

+ n.Regions, n.Boxes = nil, nil

+ n.Retired = retire(n.Retired, inc)

+ n.Cancelled = append(n.Cancelled, cancelledCreate{Inc: inc, Until: w.now + 4*horizonH})

+ return true

+ }) {

+ delete(w.admit[app].Reg, id)

+ w.stats["create cancelled: its box is gone"]++

+ w.logf("recovery: cancelled create %s inc %d, its chosen box %d is gone", id, inc, c.Op.NewBox)

+ }

return

}

if w.cas(c, func(n *claim) bool {

diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go

index 6e5ae501f..d547b8de9 100644

--- a/internal/sim/hostlife/moves_test.go

+++ b/internal/sim/hostlife/moves_test.go

@@ -34,7 +34,7 @@ func (w *world) workerMode(b *box, obl bool) {

return

}

for _, o := range c.Obl {

- if w.ownerOf(o) == b {

+ if w.ownsObligation(o, b) {

w.doObligation(b, c, o)

return

}

diff --git a/internal/sim/hostlife/onebox_identity_test.go b/internal/sim/hostlife/onebox_identity_test.go

new file mode 100644

index 000000000..a35af4a66

--- /dev/null

+++ b/internal/sim/hostlife/onebox_identity_test.go

@@ -0,0 +1,71 @@

+package hostlife

+

+import (

+ "crypto/sha256"

+ "fmt"

+ "os"

+ "regexp"

+ "strings"

+ "testing"

+)

+

+// TestOneBoxCreateInterruptionTrace is a deterministic trace of the

+// interruptions a one-box create recovers from (two-box plan rev 4,

+// Astra round 1 finding 1): the create's record persists, then its

+// selected box stops, then recovery runs for longer than its 15-step

+// wait; the box starts again (stopped) or the region's group replaces

+// it (destroyed). It writes the whole trace to $HOSTLIFE_TRACE_OUT when

+// set, so the trace at the baseline and after each task can be compared

+// byte for byte; the one-box shape must not change it.

+func TestOneBoxCreateInterruptionTrace(t *testing.T) {

+ var out []string

+ for _, how := range []string{"restarted", "replaced"} {

+ w := newWitness()

+ w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0})

+ w.admit[app0].Reg[w.console[0].OpID] = regEntry{Until: w.now + 1000}

+ w.drive(60, func() bool { return w.rec != nil && w.claim != nil && w.claim.Op.Kind == "creating" }, w.runConsole)

+ b := w.boxes[0]

+ b.Destroyed, b.Procs = true, nil

+ w.logf("trace: box %d stopped after the record persisted", b.ID)

+ w.drive(40, func() bool { return false }, w.runConsole, w.recoveryPass)

+ if how == "restarted" {

+ b.Destroyed = false

+ b.forget()

+ } else {

+ w.replaceDestroyed()

+ }

+ w.logf("trace: box %s", how)

+ w.drive(200, func() bool { return w.claim != nil && w.claim.Op.Kind == "serving" }, w.runConsole, w.recoveryPass, w.actAll())

+ out = append(out, "== "+how)

+ out = append(out, w.trace...)

+ c := w.claim

+ out = append(out, fmt.Sprintf("final: op=%s/%s exec=%d holder=%+v rec=%+v lost=%v obl=%d", c.Op.Kind, c.Op.ID, c.Op.Exec, c.Holder, w.rec, c.Lost, len(c.Obl)))

+ }

+ if p := os.Getenv("HOSTLIFE_TRACE_OUT"); p != "" {

+ if err := os.WriteFile(p, []byte(strings.Join(out, "\n")+"\n"), 0o644); err != nil {

+ t.Fatal(err)

+ }

+}

+

+// TestOneBoxSeedTraces writes one line per seed of the one-box sweep,

+// the SHA-256 of its whole trace, to $HOSTLIFE_TRACE_OUT_SEEDS (and is

+// skipped without it): the per-seed evidence that a task leaves every

+// one-box trace as the baseline's, beyond the aggregate COUNTERS line.

+// Map-ordered fields in state dumps are masked.

+func TestOneBoxSeedTraces(t *testing.T) {

+ p := os.Getenv("HOSTLIFE_TRACE_OUT_SEEDS")

+ if p == "" {

+ t.Skip("HOSTLIFE_TRACE_OUT_SEEDS is not set")

+ }

+ mask := regexp.MustCompile(`admission=\[[^\]]*\]`)

+ var out []string

+ for seed := int64(1); seed <= int64(seedsFromEnv(300)); seed++ { // the gate's seeds, 1..n (rev 11, Astra round 8)

+ w := runSeed(seed, true)

+ sum := sha256.Sum256([]byte(mask.ReplaceAllString(strings.Join(w.trace, "\n"), "admission=[masked]")))

+ out = append(out, fmt.Sprintf("%d %x %d", seed, sum[:8], len(w.trace)))

+ }

+ if err := os.WriteFile(p, []byte(strings.Join(out, "\n")+"\n"), 0o644); err != nil {

+ t.Fatal(err)

+ }

+}

diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go

index 803320fad..b6fd9268f 100644

--- a/internal/sim/hostlife/rules_test.go

+++ b/internal/sim/hostlife/rules_test.go

@@ -144,4 +144,7 @@ var allRules = []string{

"files-carried", // §8 (the kpmg outage)

"config-before-probe", // L3 (the kpmg outage)

"recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs

+

+ // region HA (two boxes per region, L18)

+ "create-choice-once", // region HA §5.2, claim P5-D2/P5-D6: the create's executor is chosen once and recorded in the intent; recovery never substitutes, it cancels a create whose box is gone

}

diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go

index 1cac18606..fbe5f8e62 100644

--- a/internal/sim/hostlife/sim_test.go

+++ b/internal/sim/hostlife/sim_test.go

@@ -16,7 +16,7 @@ const (

)

func newWorld(seed int64, verbose bool) *world {

- w := &world{seed: seed, rng: &counting{r: rand.New(rand.NewSource(seed))}, verbose: verbose,

+ w := &world{seed: seed, rng: &counting{r: rand.New(rand.NewSource(seed))}, verbose: verbose, perRegion: boxesPerRegion,

stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{},

control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, txs: map[int]tx{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, markerAlerted: map[string]bool{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}

for r := 0; r < nRegions; r++ {

@@ -45,6 +45,23 @@ func newWorld(seed int64, verbose bool) *world {

} else if w.fail["retention"] {

w.retentionStart()

}

+ // the two-box shape (region HA L18): a second enrolled box in every

+ // region, drawn after every one-box draw of this world, so the one-box

+ // stream is untouched; id nRegions+r, as addBox gives a witness

+ for r := 0; r < nRegions && w.perRegion > 1; r++ {

+ b := &box{ID: nRegions + r, Region: r, HasKey: w.rng.Intn(4) != 0, Skew: w.rng.Intn(3) - 1, Nested: w.rng.Intn(2) == 0}

+ if w.rng.Intn(4) == 0 {

+ b.FailApp = true

+ }

+ if w.rng.Intn(10) == 0 {

+ b.FailArchive = true

+ }

+ if w.rng.Intn(2) == 0 {

+ b.FailSettle = true

+ }

+ b.forget()

+ w.boxes = append(w.boxes, b)

+ }

return w

}

@@ -896,8 +913,27 @@ func seedsFromEnv(def int) int {

// TestHostLifecycle runs the joint model. HOSTLIFE_SEEDS sets the seed

// count (the gate's default is short); HOSTLIFE_SEED=n runs one seed and

-// prints its trace.

+// prints its trace; HOSTLIFE_BOXES=2 runs the two-box shape (region HA

+// L18) in place of the one-box one.

func TestHostLifecycle(t *testing.T) {

+ sweep(t)

+}

+

+// TestHostLifecycleTwoBox runs the joint model with two boxes per region

+// (region HA L18) beside the one-box sweep, so the gate covers both

+// shapes. With HOSTLIFE_BOXES set, TestHostLifecycle runs that shape and

+// this test stands aside.

+func TestHostLifecycleTwoBox(t *testing.T) {

+ if os.Getenv("HOSTLIFE_BOXES") != "" {

+ t.Skip("HOSTLIFE_BOXES is set: TestHostLifecycle runs that shape")

+ }

+ saved := boxesPerRegion

+ boxesPerRegion = 2

+ defer func() { boxesPerRegion = saved }()

+ sweep(t)

+}

+

+func sweep(t *testing.T) {

if s := os.Getenv("HOSTLIFE_SEED"); s != "" {

seed, _ := strconv.ParseInt(s, 10, 64)

w := runSeed(seed, true)

@@ -931,7 +967,7 @@ func TestHostLifecycle(t *testing.T) {

}

- t.Logf("%d seeds, %d failed, %d completed operations; mutated=%q", n, failed, ops, mutated)

+ t.Logf("%d seeds, %d failed, %d completed operations; mutated=%q boxes=%d", n, failed, ops, mutated, boxesPerRegion)

t.Logf("outcomes: %v", stats)

if js, err := json.Marshal(stats); err == nil {

t.Logf("COUNTERS %s", js) // structured, for the spec's generator (R10-9)

diff --git a/internal/sim/hostlife/twobox_test.go b/internal/sim/hostlife/twobox_test.go

new file mode 100644

index 000000000..5b6de6032

--- /dev/null

+++ b/internal/sim/hostlife/twobox_test.go

@@ -0,0 +1,154 @@

+package hostlife

+

+import (

+ "fmt"

+ "hash/fnv"

+ "os"

+)

+

+// Two boxes per region (region HA spec 1 §9 L18; claim rev 6.30 §11).

+//

+// boxesPerRegion is the world's shape: one box per region, today's model,

+// where every seed is byte-identical to the one-box baseline (spec §4: a

+// region with one box behaves exactly as today); or two, where every

+// region starts with a second enrolled box and the placement, relocation

+// and termination rules below apply. HOSTLIFE_BOXES=2 selects the two-box

+// shape for a sweep (mutate.sh inherits it); TestHostLifecycleTwoBox sets

+// it for its own run. A two-box world draws its extra random values only

+// after the one-box draws of the same step, so the one-box stream is

+// untouched.

+var boxesPerRegion = 1

+

+func init() {

+ if os.Getenv("HOSTLIFE_BOXES") == "2" {

+ boxesPerRegion = 2

+ }

+}

+

+// regionBoxes is every live box of region r, by id.

+func (w *world) regionBoxes(r int) []*box {

+ var out []*box

+ for _, b := range w.boxes {

+ if b.Region == r && !b.Destroyed {

+ out = append(out, b)

+ }

+ return out

+}

+

+// addBox enrolls a second box in region r of a witness world: the secrets

+// key held, no faults, id nRegions+r (the sweep's second boxes carry the

+// same ids; replacements are 100 and up).

+func (w *world) addBox(r int) *box {

+ b := &box{ID: nRegions + r, Region: r, HasKey: true}

+ b.forget()

+ w.boxes = append(w.boxes, b)

+ w.logf("witness: box %d enrolled in region %d", b.ID, r)

+ return b

+}

+

+// tieHash is the model's stand-in for claim P5-D2's SHA-256 of

+// host + "\x00" + box reference: a fixed function of the reference, never

+// a draw, so the choice is the same on every replay.

+func tieHash(id int) uint32 {

+ h := fnv.New32a()

+ h.Write([]byte(fmt.Sprintf("%s\x00%d", host, id)))

+ return h.Sum32()

+}

+

+// hostsOn counts the instances of app placed on b (app "" counts every

+// app): the claimed host on its executor, or on the box its create or

+// move named.

+func (w *world) hostsOn(b *box, app string) int {

+ c := w.claim

+ if c == nil || c.Holder == nil || (app != "" && c.Holder.App != app) {

+ return 0

+ }

+ switch {

+ case c.Op.Kind == "creating" && c.Op.NewBox == b.ID:

+ return 1

+ case c.Op.Exec == b.ID:

+ return 1

+ }

+ return 0

+}

+

+// owesLocal: an open park-local chore names b.

+func (w *world) owesLocal(c *claim, b *box) bool {

+ if c == nil {

+ return false

+ }

+ for _, o := range c.Obl {

+ if o.Kind == "park-local" && o.Box == b.ID {

+ return true

+ }

+ return false

+}

+

+// chooseBox is region HA §5.2's choose() (H12, L8; a move's target under

+// L15): among the eligible boxes of region r (§2: live, running the

+// claim's executable, holding the secrets key, not on lost, not owing a

+// park-local for the host), prefer one running no instance of app, then

+// the fewest hosts, then the greatest tieHash. With one box in the region

+// it is that box, as today (spec §4). It is a pure function of the world;

+// the caller records the choice in the claim's intent and never

+// substitutes (rule create-choice-once).

+func (w *world) chooseBox(r int, app string) *box {

+ bs := w.regionBoxes(r)

+ if len(bs) <= 1 {

+ if len(bs) == 0 {

+ return nil

+ }

+ return bs[0]

+ }

+ c := w.claim

+ var best *box

+ var bestKey [3]int

+ for _, b := range bs {

+ if b.Old || !b.HasKey || (c != nil && contains(c.Lost, b.ID)) || w.owesLocal(c, b) {

+ continue

+ }

+ key := [3]int{w.hostsOn(b, app), w.hostsOn(b, ""), -int(tieHash(b.ID))}

+ if best == nil || key[0] < bestKey[0] || key[0] == bestKey[0] && (key[1] < bestKey[1] || key[1] == bestKey[1] && key[2] < bestKey[2]) {

+ best, bestKey = b, key

+ }

+ return best

+}

+

+// adoptionOwner is the box adoption runs on (claim P5-D2, region HA §9 K5):

+// with one live box in the record's region it is that box, as today; with

+// more, exactly one box must hold the legacy host's local state (its row

+// or database), and zero or several refuse adoption.

+func (w *world) adoptionOwner(r int) *box {

+ bs := w.regionBoxes(r)

+ if len(bs) <= 1 {

+ if len(bs) == 0 {

+ return nil

+ }

+ return bs[0]

+ }

+ var owner *box

+ for _, b := range bs {

+ holds := b.Row != nil && b.Row.Inc == w.rec.Inc || b.DB != nil && b.DB.Inc == w.rec.Inc

+ if !holds {

+ continue

+ }

+ if owner != nil {

+ return nil // several proven owners: refused

+ }

+ owner = b

+ }

+ return owner

+}

+

+// ownsObligation: b may run chore o. A park-local is its box's alone; a

+// regional chore is any live box of its region's (claim P6-D5: regional

+// workers), as it was the region's one box's.

+func (w *world) ownsObligation(o obligation, b *box) bool {

+ if o.Kind == "park-local" {

+ return w.ownerOf(o) == b

+ }

+ return b.Region == o.Region && !b.Destroyed

+}

diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go

index 9600d7fd0..94a4f5c7c 100644

--- a/internal/sim/hostlife/witness_test.go

+++ b/internal/sim/hostlife/witness_test.go

@@ -345,7 +345,7 @@ func dump(t *testing.T, w *world) {

// newWitness is a clean world: three boxes with the secrets key, no faults

// armed, no legacy host, the quiet RNG, and the trace kept.

func newWitness() *world {

- w := &world{seed: -1, rng: quiet{}, verbose: true, now: 100,

+ w := &world{seed: -1, rng: quiet{}, verbose: true, now: 100, perRegion: 1,

stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{},

control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, txs: map[int]tx{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, markerAlerted: map[string]bool{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}

for r := 0; r < nRegions; r++ {

diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go

index d0a6813e1..ef69ba791 100644

--- a/internal/sim/hostlife/world_test.go

+++ b/internal/sim/hostlife/world_test.go

@@ -780,6 +780,7 @@ type opState struct {

NewApp string

NewRegion int

NewSerial int

+ NewBox int // the executor a create named once (region HA §5.2, H12): never substituted

// journal

ReportAt int

@@ -958,9 +959,10 @@ type ack struct {

type intner interface{ Intn(n int) int }

type world struct {

- t testingT

- seed int64

- rng intner

+ perRegion int // boxes per region at the start (region HA L18): 1, today's model, or 2

+ t testingT

+ seed int64

+ rng intner

// hold, when set, is a witness's hand on S3: a request it answers true

// for is accepted and completes only when the witness says so

// (witness_test.go). The random sweep never sets it.

carlos / platform Public

sim: one or two boxes per region (region HA L18): HOSTLIFE_BOXES and TestHostLifecycleTwoBox, choose() for creates and move targets recorded once, adoption's one proven owner, regional chores for any box of the region, replacements to the region's minimum; the one-box sweep is byte-identical