amadan

carlos / platform Public

moves: the start check over the three markers and the claim (§5.1, INV-4)

StartCheck and PreparedCheck over genselect.Marker, .files-gen JSON and the
plain .gen name (H11); spec §5.1 amended for .gen; copy rows MV-N184 to 186.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 118031d03a04b30f4ce89e7c28be67ce21087b5c parent 81d0cc6
5 files changed, +336 −4
  • approved_moves_copy_test.go +2 −1
  • docs/superpowers/plans/2026-10-06-moves-phase1-copy.md +3 −0
  • docs/superpowers/specs/2026-10-02-move-any-app-design.md +4 −3
  • internal/moves/startcheck.go +136 −0
  • internal/moves/startcheck_test.go +191 −0
diff --git a/approved_moves_copy_test.go b/approved_moves_copy_test.go
index ef0477bd0..3ff23c842 100644
--- a/approved_moves_copy_test.go
+++ b/approved_moves_copy_test.go
@@ -70,7 +70,7 @@ var movesCopyIDs = []string{
"MV-N163", "MV-N164", "MV-N165", "MV-N166", "MV-N167", "MV-N168",
"MV-N169", "MV-N170", "MV-N171", "MV-N172", "MV-N173", "MV-N174",
"MV-N175", "MV-N176", "MV-N177", "MV-N178", "MV-N179", "MV-N180", "MV-N181",
- "MV-N182", "MV-N183",
+ "MV-N182", "MV-N183", "MV-N184", "MV-N185", "MV-N186",
}
// copyRow is one row of the record. The File cell is the file the sentence is
@@ -627,6 +627,7 @@ var movesScanFiles = []string{
"internal/moves/sealedclient.go",
"internal/moves/source.go",
"internal/moves/staging.go",
+ "internal/moves/startcheck.go",
"internal/moves/switch.go",
"internal/moves/timers.go",
"internal/provision/provision.go",
diff --git a/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md b/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md
index 40607c9e1..0baaab1e0 100644
--- a/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md
+++ b/docs/superpowers/plans/2026-10-06-moves-phase1-copy.md
@@ -237,6 +237,9 @@ Columns: id, file, text, status.
|---|---|---|---|
| MV-N182 | internal/provision/provision.go | the probe ran out of attempts | pending |
| MV-N183 | internal/provision/provision.go | the commit came after the deadline | pending |
+| MV-N184 | internal/moves/startcheck.go | this box holds another generation of the instance | pending |
+| MV-N185 | internal/moves/startcheck.go | the instance's files belong to another generation | pending |
+| MV-N186 | internal/moves/startcheck.go | the instance's database belongs to another generation | pending |
## Plan 4
diff --git a/docs/superpowers/specs/2026-10-02-move-any-app-design.md b/docs/superpowers/specs/2026-10-02-move-any-app-design.md
index 36c92b479..77562a013 100644
--- a/docs/superpowers/specs/2026-10-02-move-any-app-design.md
+++ b/docs/superpowers/specs/2026-10-02-move-any-app-design.md
@@ -1838,7 +1838,7 @@ field.
| marker | where | written | content |
|---|---|---|---|
| `generation.json` | `<location>generation.json`, beside `lock.json` | **last**, after the install manifest is complete and verified (§7.6); **conditionally**: If-Match the marker it supersedes, or If-None-Match when there is none (model 29) | `{"op","incarnation","host","box","installed_at","manifest_sha256","snapshot_key","snapshot_version","snapshot_txid","snapshot_crc64"}`: the pinned root, the install's snapshot identity and the floor a successor snapshot must clear (R3-1, R4-1, R5-3) |
-| `<dbPath>.gen` | beside the local database | after a restore completes | `{"op","incarnation","location"}` |
+| `<dbPath>.gen` | beside the local database | after a restore completes | the generation's name as plain text, one line: the format main already writes (`hostbox.WriteGenerationMarker`). It carries no incarnation and no location; the claim's holder vouches for both (Paul's ruling, moves Phase 1 Plan 3) |
| `.files-gen` | inside the files directory | **last**, after files, `<host>.env`, timers and the carried registry columns are all durable (§7.6) | `{"op","incarnation"}` |
`generation.json` is the one reused key a generation writes: everything
@@ -1890,8 +1890,9 @@ is the region of the holder's current installation:
holder's;
2. `.files-gen`, when the files directory exists, to name the same
generation and incarnation;
-3. `<dbPath>.gen` to name the same generation and location. A warm
- database that does not is from an earlier stay on this box: the
+3. `<dbPath>.gen` to name the same generation, exactly: the plain name
+ carries no location, which the claim's `holder.location` vouches for.
+ A warm database that does not is from an earlier stay on this box: the
activator parks it (§6.3) and restores cold.
Rev 5's check compared the three markers with each other only. Astra
diff --git a/internal/moves/startcheck.go b/internal/moves/startcheck.go
new file mode 100644
index 000000000..a569c53da
--- /dev/null
+++ b/internal/moves/startcheck.go
@@ -0,0 +1,136 @@
+package moves
+
+import (
+ "errors"
+
+ "github.com/carlosframework/platform/internal/genselect"
+ "github.com/carlosframework/platform/internal/hostclaim"
+)
+
+// The start check (spec §5.1, INV-4, J2-R2-8): before every spawn the three
+// markers a generation leaves on a box are compared with the host claim. A
+// marker that merely exists proves nothing; the claim says which generation
+// this box may run.
+//
+// The three markers have three formats (Paul's ruling on H11):
+//
+// - generation.json is genselect.Marker, read from the box's own location;
+// absent is the origin.
+// - .files-gen is the JSON {op, incarnation} (FilesGen); absent is "no
+// files directory yet".
+// - <dbPath>.gen is the plain generation name hostbox.WriteGenerationMarker
+// writes and ColdRestore rewrites; "" is absent. It carries no incarnation
+// and no location: the claim's holder and the restore vouch for those.
+//
+// Refusals are typed and carry member-safe reasons, never marker contents.
+var (
+ // ErrStartMarker: generation.json does not name a generation the claim
+ // expects, or names another incarnation.
+ ErrStartMarker = errors.New("this box holds another generation of the instance")
+ // ErrStartFiles: .files-gen does not name a generation and incarnation
+ // the claim expects.
+ ErrStartFiles = errors.New("the instance's files belong to another generation")
+ // ErrStartDB: the database's marker does not name the claim's generation.
+ ErrStartDB = errors.New("the instance's database belongs to another generation")
+)
+
+// FilesGen is the .files-gen body (§5.1): the op and the incarnation.
+type FilesGen struct {
+ Op string `json:"op"`
+ Incarnation string `json:"incarnation"`
+}
+
+// originOr names the origin generation the way the claim's admissions do.
+func originOr(g string) string {
+ if g == "" {
+ return hostclaim.RootGeneration
+ }
+ return g
+}
+
+// expectedGenerations is the set of generations a marker may name for this
+// holder: holder.generation, as the admission's CAS left it, and the lagging
+// ones. A marker is published once per admission, at Replicate, so after a
+// restarted attempt (a fresh generation restored from the prepared one) or a
+// run of admissions that published nothing, the marker still names an
+// earlier generation. Walking holder.admissions from the newest, each
+// admission whose generation is already accepted adds its predecessor. The
+// origin is hostclaim.RootGeneration here.
+func expectedGenerations(h *hostclaim.Holder) map[string]bool {
+ cur := originOr(h.Generation)
+ ok := map[string]bool{cur: true}
+ for {
+ var next string
+ found := false
+ for i := len(h.Admissions) - 1; i >= 0; i-- {
+ if originOr(h.Admissions[i].Generation) == cur {
+ next, found = originOr(h.Admissions[i].Predecessor), true
+ break
+ }
+ }
+ if !found || ok[next] {
+ return ok
+ }
+ ok[next] = true
+ cur = next
+ }
+}
+
+// StartCheck is the §5.1 start check against the claim, run after the
+// admission CAS and before every spawn.
+//
+// 1. marker (generation.json; nil is the origin) names a generation the
+// claim expects (holder.generation or, lagging, an earlier link of the
+// admission chain) and the holder's incarnation.
+// 2. filesGen, when present, names an expected generation (the same chain:
+// a restarted attempt's files still name the prepared generation) and
+// the holder's incarnation.
+// 3. dbGen, when not "", is exactly holder.generation: the restore rewrites
+// it, so it is current after every restore. A warm database that fails
+// here is from an earlier stay; the caller parks it and restores cold.
+//
+// A claim with no holder expects no generation, so every start is refused
+// with ErrStartMarker.
+func StartCheck(c *hostclaim.Claim, marker *genselect.Marker, filesGen *FilesGen, dbGen string) error {
+ if c == nil || c.Holder == nil {
+ return ErrStartMarker
+ }
+ h := c.Holder
+ want := expectedGenerations(h)
+ if marker == nil {
+ if !want[hostclaim.RootGeneration] {
+ return ErrStartMarker
+ }
+ } else if marker.Op == "" || marker.Op == hostclaim.RootGeneration ||
+ !want[marker.Op] || marker.Incarnation != h.Incarnation {
+ return ErrStartMarker
+ }
+ if filesGen != nil {
+ if filesGen.Op == "" || filesGen.Op == hostclaim.RootGeneration ||
+ !want[filesGen.Op] || filesGen.Incarnation != h.Incarnation {
+ return ErrStartFiles
+ }
+ }
+ if dbGen != "" && dbGen != h.Generation {
+ return ErrStartDB
+ }
+ return nil
+}
+
+// PreparedCheck validates a landing probe's inputs before admission (Plan 3
+// Task 5 step 3): the files marker and the database marker both exist and
+// name the prepared generation (the move id), and the files marker names the
+// holder's incarnation. The database marker is the plain name (H11); the
+// location is vouched for by the holder.
+func PreparedCheck(prepared string, holder hostclaim.Holder, filesGen *FilesGen, dbGen string) error {
+ if prepared == "" || prepared == hostclaim.RootGeneration {
+ return ErrStartFiles
+ }
+ if filesGen == nil || filesGen.Op != prepared || filesGen.Incarnation != holder.Incarnation {
+ return ErrStartFiles
+ }
+ if dbGen != prepared {
+ return ErrStartDB
+ }
+ return nil
+}
diff --git a/internal/moves/startcheck_test.go b/internal/moves/startcheck_test.go
new file mode 100644
index 000000000..bddf1c4bf
--- /dev/null
+++ b/internal/moves/startcheck_test.go
@@ -0,0 +1,191 @@
+package moves
+
+import (
+ "errors"
+ "testing"
+
+ "github.com/carlosframework/platform/internal/genselect"
+ "github.com/carlosframework/platform/internal/hostclaim"
+)
+
+func startClaim(gen string, adm ...hostclaim.AdmissionRecord) *hostclaim.Claim {
+ return &hostclaim.Claim{Holder: &hostclaim.Holder{
+ Incarnation: "inc-1", Location: "loc/", Generation: gen, Admissions: adm,
+ }}
+}
+
+func startMarker(op string) *genselect.Marker {
+ return &genselect.Marker{Op: op, Incarnation: "inc-1"}
+}
+
+func TestStartCheckOriginEverywhere(t *testing.T) {
+ if err := StartCheck(startClaim(""), nil, nil, ""); err != nil {
+ t.Fatalf("origin everywhere: %v", err)
+ }
+}
+
+func TestStartCheckMarkerNamesTheHoldersGeneration(t *testing.T) {
+ c := startClaim("g2", hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"})
+ fg := &FilesGen{Op: "g2", Incarnation: "inc-1"}
+ if err := StartCheck(c, startMarker("g2"), fg, "g2"); err != nil {
+ t.Fatalf("all three name the holder's generation: %v", err)
+ }
+}
+
+func TestStartCheckLaggingMarker(t *testing.T) {
+ // The latest admission replaced g1 with g2 and has published nothing.
+ c := startClaim("g2", hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"})
+ if err := StartCheck(c, startMarker("g1"), nil, ""); err != nil {
+ t.Fatalf("marker naming the latest admission's predecessor: %v", err)
+ }
+ // A restarted probe: the fresh generation F restored from the prepared M;
+ // the files still name M.
+ c = startClaim("F", hostclaim.AdmissionRecord{Generation: "M", Predecessor: "g0"},
+ hostclaim.AdmissionRecord{Generation: "F", Predecessor: "M"})
+ fg := &FilesGen{Op: "M", Incarnation: "inc-1"}
+ if err := StartCheck(c, startMarker("M"), fg, "F"); err != nil {
+ t.Fatalf("restarted attempt: %v", err)
+ }
+}
+
+func TestStartCheckChainOfAdmissionsWithoutMarkers(t *testing.T) {
+ c := startClaim("g3",
+ hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"},
+ hostclaim.AdmissionRecord{Generation: "g3", Predecessor: "g2"})
+ for _, op := range []string{"g3", "g2", "g1"} {
+ if err := StartCheck(c, startMarker(op), nil, ""); err != nil {
+ t.Errorf("marker %s through the chain: %v", op, err)
+ }
+ }
+ if err := StartCheck(c, startMarker("g0"), nil, ""); !errors.Is(err, ErrStartMarker) {
+ t.Errorf("marker beyond the chain = %v, want ErrStartMarker", err)
+ }
+ // The chain is by predecessor link, not by position: an admission whose
+ // generation the chain never reaches adds nothing.
+ c = startClaim("g3",
+ hostclaim.AdmissionRecord{Generation: "x2", Predecessor: "x1"},
+ hostclaim.AdmissionRecord{Generation: "g3", Predecessor: "g2"})
+ if err := StartCheck(c, startMarker("x1"), nil, ""); !errors.Is(err, ErrStartMarker) {
+ t.Errorf("marker off the chain = %v, want ErrStartMarker", err)
+ }
+}
+
+func TestStartCheckChainTerminatesOnACycle(t *testing.T) {
+ // A damaged record whose predecessors loop must still end.
+ c := startClaim("g2",
+ hostclaim.AdmissionRecord{Generation: "g1", Predecessor: "g2"},
+ hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"})
+ if err := StartCheck(c, startMarker("g1"), nil, ""); err != nil {
+ t.Errorf("marker in the cycle: %v", err)
+ }
+ if err := StartCheck(c, startMarker("g9"), nil, ""); !errors.Is(err, ErrStartMarker) {
+ t.Errorf("marker outside the cycle = %v, want ErrStartMarker", err)
+ }
+}
+
+func TestStartCheckOriginAfterAFirstAdmission(t *testing.T) {
+ // The first admission left the origin: its predecessor is the origin, so
+ // an absent marker is lagging, not wrong.
+ c := startClaim("g1", hostclaim.AdmissionRecord{Generation: "g1"})
+ if err := StartCheck(c, nil, nil, ""); err != nil {
+ t.Fatalf("absent marker, predecessor the origin: %v", err)
+ }
+ // With no admission reaching the origin, absent is refused.
+ c = startClaim("g2", hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"})
+ if err := StartCheck(c, nil, nil, ""); !errors.Is(err, ErrStartMarker) {
+ t.Errorf("absent marker with a published generation = %v, want ErrStartMarker", err)
+ }
+}
+
+func TestStartCheckMarkerRefusals(t *testing.T) {
+ c := startClaim("g2", hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"})
+ for name, m := range map[string]*genselect.Marker{
+ "unrelated generation": startMarker("other"),
+ "another incarnation": {Op: "g2", Incarnation: "inc-2"},
+ "empty op": {Incarnation: "inc-1"},
+ "root as an op": startMarker(hostclaim.RootGeneration),
+ } {
+ if err := StartCheck(c, m, nil, ""); !errors.Is(err, ErrStartMarker) {
+ t.Errorf("%s = %v, want ErrStartMarker", name, err)
+ }
+ }
+ if err := StartCheck(&hostclaim.Claim{}, nil, nil, ""); !errors.Is(err, ErrStartMarker) {
+ t.Errorf("no holder = %v, want ErrStartMarker", err)
+ }
+ if err := StartCheck(nil, nil, nil, ""); !errors.Is(err, ErrStartMarker) {
+ t.Errorf("nil claim = %v, want ErrStartMarker", err)
+ }
+}
+
+func TestStartCheckFilesGen(t *testing.T) {
+ c := startClaim("g2", hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"})
+ m := startMarker("g2")
+ for name, fg := range map[string]*FilesGen{
+ "another op": {Op: "other", Incarnation: "inc-1"},
+ "another incarnation": {Op: "g2", Incarnation: "inc-2"},
+ "empty": {},
+ } {
+ if err := StartCheck(c, m, fg, ""); !errors.Is(err, ErrStartFiles) {
+ t.Errorf("%s = %v, want ErrStartFiles", name, err)
+ }
+ }
+ // The origin's own files carry no .files-gen, and a stray one is refused.
+ if err := StartCheck(startClaim(""), nil, &FilesGen{Op: "g1", Incarnation: "inc-1"}, ""); !errors.Is(err, ErrStartFiles) {
+ t.Errorf("files-gen on an origin claim = %v, want ErrStartFiles", err)
+ }
+}
+
+func TestStartCheckDBGen(t *testing.T) {
+ c := startClaim("g2", hostclaim.AdmissionRecord{Generation: "g2", Predecessor: "g1"})
+ m := startMarker("g2")
+ // The .gen is plain and exact: a lagging name is a warm database from an
+ // earlier stay, even though the chain would admit it elsewhere.
+ for _, g := range []string{"other", "g1", hostclaim.RootGeneration} {
+ if err := StartCheck(c, m, nil, g); !errors.Is(err, ErrStartDB) {
+ t.Errorf(".gen %q = %v, want ErrStartDB", g, err)
+ }
+ }
+ if err := StartCheck(c, m, nil, "g2"); err != nil {
+ t.Errorf(".gen g2: %v", err)
+ }
+ if err := StartCheck(startClaim(""), nil, nil, "g1"); !errors.Is(err, ErrStartDB) {
+ t.Errorf(".gen on an origin claim = %v, want ErrStartDB", err)
+ }
+}
+
+func TestStartCheckReportsTheFirstFailingMarker(t *testing.T) {
+ c := startClaim("g2")
+ err := StartCheck(c, startMarker("other"), &FilesGen{Op: "other", Incarnation: "inc-1"}, "other")
+ if !errors.Is(err, ErrStartMarker) || errors.Is(err, ErrStartFiles) || errors.Is(err, ErrStartDB) {
+ t.Errorf("err = %v, want only ErrStartMarker", err)
+ }
+}
+
+func TestPreparedCheck(t *testing.T) {
+ h := hostclaim.Holder{Incarnation: "inc-1", Location: "loc/", Generation: "g1"}
+ ok := &FilesGen{Op: "mv-1", Incarnation: "inc-1"}
+ if err := PreparedCheck("mv-1", h, ok, "mv-1"); err != nil {
+ t.Fatalf("both name the prepared generation: %v", err)
+ }
+ cases := []struct {
+ name string
+ prepared string
+ fg *FilesGen
+ db string
+ want error
+ }{
+ {"files-gen absent", "mv-1", nil, "mv-1", ErrStartFiles},
+ {"files-gen another op", "mv-1", &FilesGen{Op: "mv-2", Incarnation: "inc-1"}, "mv-1", ErrStartFiles},
+ {"files-gen another incarnation", "mv-1", &FilesGen{Op: "mv-1", Incarnation: "inc-2"}, "mv-1", ErrStartFiles},
+ {"gen absent", "mv-1", ok, "", ErrStartDB},
+ {"gen another op", "mv-1", ok, "mv-2", ErrStartDB},
+ {"gen the holder's generation", "mv-1", ok, "g1", ErrStartDB},
+ {"no prepared generation", "", &FilesGen{}, "", ErrStartFiles},
+ {"root as prepared", hostclaim.RootGeneration, &FilesGen{Op: hostclaim.RootGeneration, Incarnation: "inc-1"}, hostclaim.RootGeneration, ErrStartFiles},
+ }
+ for _, tc := range cases {
+ if err := PreparedCheck(tc.prepared, h, tc.fg, tc.db); !errors.Is(err, tc.want) {
+ t.Errorf("%s = %v, want %v", tc.name, err, tc.want)
+ }
+ }
+}