carlos / platform Public

host: the seal's coverage fails closed; a missing database is uncovered unless the checkpoint journalled it covered (Task 5 fix round 1, ruling 3)

covered started true and was only lowered when a database was there to
compare, so a cut whose disk vanished before the final checkpoint sealed
FromDB false, SrcCovered true: coverage with no evidence, and the loss
declaration it would have forced suppressed. Now the checkpoint decides
coverage with the database present (its position against N) and journals
it; the final round starts from uncovered and takes the journalled answer
only for the same N. regularFile distinguishes absence from every other
filesystem answer, which is an error, never absence.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude agent, operated by paul@keymail.dev 2d9d3ea9568628cfb1570171096cd937ad26777b parent d3fc219
2 files changed, +153 −6
  • internal/host/movescut.go +63 −6
  • internal/host/movescut_test.go +90 −0
diff --git a/internal/host/movescut.go b/internal/host/movescut.go
index 2d7bde6cb..6c62b013c 100644
--- a/internal/host/movescut.go
+++ b/internal/host/movescut.go
@@ -65,10 +65,18 @@ const cutStepsPerPass = 8
// Op journal steps the cut writes (moves.Journal).
const (
cutStepEvidence = "evidence" // §5.3 steps 1 to 4, the StoppedReport JSON
+ cutStepCoverage = "coverage" // cutCoverage: the stopped database's position against N
cutStepArchive = "archive" // the cut archive's identity, before any PUT
cutStepRevertBound = "revert_bound" // the revert's staging park evidence_at
)
+// cutCoverage is the journalled coverage decision (ruling 3): whether the
+// stopped database's own position equalled N after the final checkpoint.
+type cutCoverage struct {
+ N uint64 `json:"n"`
+ Covered bool `json:"covered"`
+}
+
// cutRun is one pass's state for one cutting record.
type cutRun struct {
w *movesWorker
@@ -531,7 +539,10 @@ func (c *cutRun) giveUpExecution(ctx context.Context, obs hostclaim.Observed, st
}
prefix, keep := moves.ReplicaSource(holder)
dbPath := c.dbPath()
- fromDB := regularFile(dbPath)
+ fromDB, err := regularFile(dbPath)
+ if err != nil {
+ return moves.StoppedReport{}, err
+ }
if fromDB {
if cfg.FinalCheckpoint == nil {
return moves.StoppedReport{}, errors.New("no final checkpoint on this box")
@@ -553,6 +564,26 @@ func (c *cutRun) giveUpExecution(ctx context.Context, obs hostclaim.Observed, st
if dbSHA, err = fileSHA256(dbPath); err != nil {
return moves.StoppedReport{}, fmt.Errorf("digest the stopped database: %w", err)
}
+ // Coverage (ruling 3): the stopped database's own position against
+ // N, decided here, with the database present after its checkpoint,
+ // and journalled so the seal can still state it if the disk is lost
+ // before the final round. Without a database nothing is journalled
+ // and the seal says uncovered.
+ if cfg.LocalPosition == nil {
+ return moves.StoppedReport{}, errors.New("no local position on this box")
+ }
+ pos, err := cfg.LocalPosition(dbPath)
+ if err != nil {
+ return moves.StoppedReport{}, fmt.Errorf("read the stopped database's position: %w", err)
+ }
+ body, err := json.Marshal(cutCoverage{N: n, Covered: pos == n})
+ if err != nil {
+ return moves.StoppedReport{}, err
+ }
+ j.Mark(cutStepCoverage, string(body))
+ if err := j.Write(cfg.DataDir); err != nil {
+ return moves.StoppedReport{}, err
+ }
}
timersSHA, err := c.snapshotTimers(ctx, own, vs)
if err != nil {
@@ -910,8 +941,14 @@ func (c *cutRun) finalRound(ctx context.Context, holder hostclaim.Holder, report
}
replica = append(replica, moves.SealedObject{Key: dstPrefix + rel, VersionID: ver, Size: o.Size})
}
- fromDB := regularFile(c.dbPath())
- covered := true
+ // Coverage starts false (ruling 3): a database still here is asked for
+ // its position against N; one that is gone is covered only if the
+ // checkpoint journalled that it was, at this N (giveUpExecution).
+ fromDB, err := regularFile(c.dbPath())
+ if err != nil {
+ return false, err
+ }
+ covered := false
if fromDB {
if cfg.LocalPosition == nil {
return false, errors.New("no local position on this box")
@@ -921,6 +958,13 @@ func (c *cutRun) finalRound(ctx context.Context, holder hostclaim.Holder, report
return false, fmt.Errorf("read the stopped database's position: %w", err)
}
covered = pos == report.FinalTXID
+ } else if j, err := c.journal(); err != nil {
+ return false, err
+ } else if raw, ok := j.Steps[cutStepCoverage]; ok {
+ var cov cutCoverage
+ if json.Unmarshal([]byte(raw), &cov) == nil && cov.N == report.FinalTXID {
+ covered = cov.Covered
+ }
}
now := cfg.Now().UTC()
seal := moves.Seal{V: moves.SealVersion, N: report.FinalTXID, Replica: replica,
@@ -1429,10 +1473,23 @@ func obligationID() string {
return hex.EncodeToString(b[:])
}
-// regularFile reports whether path is a regular file.
-func regularFile(path string) bool {
+// regularFile reports whether path is a regular file. Absence (ENOENT) is
+// false with no error; any other answer from the filesystem, an error or
+// something there that is not a regular file, is an error, never absence
+// (ruling 3): the cut decides coverage on it, so it must not read a
+// transient fault as "the database is gone".
+func regularFile(path string) (bool, error) {
st, err := os.Lstat(path)
- return err == nil && st.Mode().IsRegular()
+ if errors.Is(err, os.ErrNotExist) {
+ return false, nil
+ }
+ if err != nil {
+ return false, fmt.Errorf("stat %s: %w", path, err)
+ }
+ if !st.Mode().IsRegular() {
+ return false, fmt.Errorf("%s is not a regular file (%s)", path, st.Mode())
+ }
+ return true, nil
}
// fileSHA256 is "sha256:<hex>" of the file at path.
diff --git a/internal/host/movescut_test.go b/internal/host/movescut_test.go
index 934d806c2..0a72af438 100644
--- a/internal/host/movescut_test.go
+++ b/internal/host/movescut_test.go
@@ -1126,3 +1126,93 @@ func TestLocalLTXPosition(t *testing.T) {
t.Fatalf("position %d, %v; want 10", n, err)
}
}
+
+// Ruling 3: coverage is never assumed. A database that is gone before the
+// final checkpoint leaves the seal FromDB false and SrcCovered false, since
+// nothing proved the replica holds its last write; one that was there
+// through the checkpoint, with its position journalled equal to N, keeps
+// SrcCovered true if the disk is lost afterwards; one still present but
+// behind its replica is not covered.
+func TestMissingDatabaseIsNotCovered(t *testing.T) {
+ t.Run("lost before the checkpoint", func(t *testing.T) {
+ h := newCutHarness(t)
+ h.ready(t)
+ h.crashAt = "after-evidence"
+ h.cut(t)
+ h.crashPass(t)
+ if m := h.move(t); m.CutPhase != provision.CutStopping {
+ t.Fatalf("after the crash: %+v", m)
+ }
+ if err := os.Remove(h.route.DBPath); err != nil {
+ t.Fatal(err)
+ }
+ h.freshWorker()
+ h.pass(t)
+ m := h.move(t)
+ if m.State != provision.MoveLanding || h.checkpoints != 0 {
+ t.Fatalf("the cut without a database: %+v (%d checkpoints)", m, h.checkpoints)
+ }
+ if m.Source.FinalTXID != 2 || m.Source.DBSHA256 != "" {
+ t.Fatalf("source baselines: %+v", m.Source)
+ }
+ seal := h.seal(t)
+ if seal.FromDB || seal.SrcCovered || seal.N != 2 {
+ t.Fatalf("seal claims coverage with no database: %+v", seal)
+ }
+ })
+ t.Run("lost after the checkpoint journalled coverage", func(t *testing.T) {
+ h := newCutHarness(t)
+ h.ready(t)
+ h.crashAt = "after-exec-none"
+ h.cut(t)
+ h.crashPass(t)
+ if err := os.Remove(h.route.DBPath); err != nil {
+ t.Fatal(err)
+ }
+ h.freshWorker()
+ h.pass(t)
+ if m := h.move(t); m.State != provision.MoveLanding {
+ t.Fatalf("the replay: %+v", m)
+ }
+ seal := h.seal(t)
+ if seal.FromDB || !seal.SrcCovered || seal.N != 3 {
+ t.Fatalf("seal: %+v", seal)
+ }
+ })
+ t.Run("present but behind its replica", func(t *testing.T) {
+ h := newCutHarness(t)
+ h.ready(t)
+ h.localPos = 2
+ h.cut(t)
+ h.pass(t)
+ if m := h.move(t); m.State != provision.MoveLanding {
+ t.Fatalf("the cut: %+v", m)
+ }
+ if seal := h.seal(t); !seal.FromDB || seal.SrcCovered {
+ t.Fatalf("seal: %+v", seal)
+ }
+ })
+}
+
+// regularFile: a regular file is one; an absent path is not and no error;
+// anything else (a path under a file, a directory where a file should be)
+// is an error, never absence.
+func TestRegularFileDistinguishesAbsence(t *testing.T) {
+ dir := t.TempDir()
+ file := filepath.Join(dir, "a.db")
+ if err := os.WriteFile(file, []byte("x"), 0o600); err != nil {
+ t.Fatal(err)
+ }
+ if ok, err := regularFile(file); !ok || err != nil {
+ t.Fatalf("a file: %v %v", ok, err)
+ }
+ if ok, err := regularFile(filepath.Join(dir, "absent.db")); ok || err != nil {
+ t.Fatalf("absent: %v %v", ok, err)
+ }
+ if ok, err := regularFile(filepath.Join(file, "under-a-file.db")); ok || err == nil {
+ t.Fatalf("a path under a file: %v %v", ok, err)
+ }
+ if ok, err := regularFile(dir); ok || err == nil {
+ t.Fatalf("a directory: %v %v", ok, err)
+ }
+}