fix(goal): finish the plan before a claim ends the run, and seal a resume

cmd/flynn/main.go

@@ -879,7 +879,12 @@ func resumeRun(modelSpec, runID, dataDir string, verbose bool, shell governed.Sh
 	if err != nil {
 		return err
 	}
-	store, err := openDataStore(ctx, dataDir)
+	// The same best-effort signer a goal seals under, so a resumed run ends verifiable too.
+	signer, serr := runSigner(ctx, dataDir)
+	if serr != nil {
+		signer = nil
+	}
+	store, err := openDataStore(ctx, dataDir, snapshotOptions(signer)...)
 	if err != nil {
 		return err
 	}
@@ -904,6 +909,9 @@ func resumeRun(modelSpec, runID, dataDir string, verbose bool, shell governed.Sh
 		return err
 	}
 	_, _, _, err = req.execute(ctx)
+	if signer != nil {
+		sealResumed(ctx, os.Stdout, store, runID, signer, err)
+	}
 	return err
 }
 

cmd/flynn/resume_seal_test.go

@@ -0,0 +1,116 @@
+package main
+
+import (
+	"bytes"
+	"context"
+	"errors"
+	"fmt"
+	"io"
+	"strings"
+	"testing"
+
+	"github.com/ionalpha/flynn/chain"
+	"github.com/ionalpha/flynn/governed"
+	"github.com/ionalpha/flynn/harness"
+	"github.com/ionalpha/flynn/llm/llmtest"
+	"github.com/ionalpha/flynn/spine"
+	"github.com/ionalpha/flynn/storage/sqlite"
+)
+
+// unsealedRun drives a run to convergence on the plain log, as `flynn resume` does, and
+// returns its id. Nothing has sealed it.
+func unsealedRun(t *testing.T, ctx context.Context, store *sqlite.Store) string {
+	t.Helper()
+	reg, err := governed.Registry()
+	if err != nil {
+		t.Fatal(err)
+	}
+	_, runID, _, err := driveRequest{
+		out: io.Discard, model: llmtest.NewScripted(llmtest.SayText("done")), plan: harness.Plan{},
+		workdir: t.TempDir(), objective: "reply done and stop", system: defaultSystemPrompt,
+		rstore: store.Resources(reg), jq: store.Jobs(), log: store.Log(),
+	}.execute(ctx)
+	if err != nil {
+		t.Fatalf("drive: %v", err)
+	}
+	return runID
+}
+
+// TestAResumedRunIsSealed: resume drives a run whose earlier events another process wrote,
+// so it has no recorder to seal from, and before this the resumed run was left with no
+// record at all and `flynn spine verify` refused it. It is sealed from the durable stream,
+// and a run that stopped says how it ended inside the sealed chain.
+func TestAResumedRunIsSealed(t *testing.T) {
+	ctx := context.Background()
+	store, err := openStore(ctx, "")
+	if err != nil {
+		t.Fatal(err)
+	}
+	defer func() { _ = store.Close() }()
+	signer := selfCertifyingSigner(t)
+
+	for _, tc := range []struct {
+		name    string
+		runErr  error
+		outcome string
+	}{
+		{name: "converged"},
+		{name: "stalled", runErr: errors.New("goal stalled: no progress"), outcome: resultStalled},
+	} {
+		t.Run(tc.name, func(t *testing.T) {
+			runID := unsealedRun(t, ctx, store)
+			var out bytes.Buffer
+			sealResumed(ctx, &out, store, runID, signer, tc.runErr)
+			if !strings.Contains(out.String(), "run sealed") {
+				t.Fatalf("no seal reported:\n%s", out.String())
+			}
+			var report bytes.Buffer
+			if err := verifyStoredRun(ctx, &report, store, runID); err != nil {
+				t.Fatalf("verify the resumed run: %v\n%s", err, report.String())
+			}
+			if got := recordedOutcome(t, ctx, store, runID); got != tc.outcome {
+				t.Fatalf("recorded outcome = %q, want %q", got, tc.outcome)
+			}
+		})
+	}
+}
+
+// TestAnInterruptedResumeIsLeftOpen: Ctrl-C on a resume detaches, and the run can be
+// resumed again, so it is neither sealed nor marked as stopped.
+func TestAnInterruptedResumeIsLeftOpen(t *testing.T) {
+	ctx := context.Background()
+	store, err := openStore(ctx, "")
+	if err != nil {
+		t.Fatal(err)
+	}
+	defer func() { _ = store.Close() }()
+	runID := unsealedRun(t, ctx, store)
+
+	var out bytes.Buffer
+	sealResumed(ctx, &out, store, runID, selfCertifyingSigner(t), fmt.Errorf("drive: %w", context.Canceled))
+	if out.Len() != 0 {
+		t.Fatalf("an interrupted resume reported: %s", out.String())
+	}
+	if err := verifyStoredRun(ctx, io.Discard, store, runID); err == nil {
+		t.Fatal("an interrupted resume was sealed")
+	}
+	if got := recordedOutcome(t, ctx, store, runID); got != "" {
+		t.Fatalf("an interrupted resume recorded outcome %q", got)
+	}
+}
+
+// recordedOutcome is the result of the last outcome event on the run's stream, or "".
+func recordedOutcome(t *testing.T, ctx context.Context, store *sqlite.Store, runID string) string {
+	t.Helper()
+	events, err := store.Log().Read(ctx, spine.Query{Stream: runID})
+	if err != nil {
+		t.Fatal(err)
+	}
+	got := ""
+	for _, e := range events {
+		if e.Type == chain.OutcomeRecorded {
+			got, _ = e.Payload[chain.OutcomeResultKey].(string)
+		}
+	}
+	return got
+}

cmd/flynn/spine.go

@@ -205,6 +205,37 @@ func sealStopped(ctx context.Context, out io.Writer, store *sqlite.Store, rec *c
 	sealReported(ctx, out, store, rec, runID, signer)
 }
 
+// sealResumed seals a run that `flynn resume` drove, from its durable stream: the events
+// before the resume were written by an earlier process, so no recorder in this one holds
+// them. A run that stopped records how it ended first, as [sealStopped] does. An
+// interrupt is left unsealed, because Ctrl-C on a resume detaches and the run can be
+// resumed again; a stopped outcome on its stream would then sit inside a run that went on.
+func sealResumed(ctx context.Context, out io.Writer, store *sqlite.Store, runID string, signer chain.RootSigner, runErr error) {
+	if errors.Is(runErr, context.Canceled) {
+		return
+	}
+	ctx, cancel := context.WithTimeout(context.WithoutCancel(ctx), 30*time.Second)
+	defer cancel()
+	if runErr != nil {
+		if _, err := store.Log().Append(ctx, spine.AppendInput{
+			Stream: runID,
+			Type:   chain.OutcomeRecorded,
+			Actor:  spine.ActorSystem,
+			Payload: map[string]any{
+				chain.OutcomeResultKey: stoppedOutcome(runErr),
+				outcomeReasonKey:       runErr.Error(),
+			},
+		}); err != nil {
+			_, _ = fmt.Fprintf(out, "  (outcome not recorded: %v)\n", err)
+		}
+	}
+	if err := sealRunFromStore(ctx, store, runID, signer); err != nil {
+		_, _ = fmt.Fprintf(out, "  (run not sealed: %v)\n", err)
+		return
+	}
+	_, _ = fmt.Fprintf(out, "  run sealed; verify with: flynn spine verify %s\n", runID)
+}
+
 // sealRunFromStore seals a run's current durable stream into a signed record stored on
 // the stream, without a live recorder. It reads the run's events, folds every one
 // except a prior seal into a fresh record builder, signs the Merkle head, and appends

docs/HOST_BOUNDARY.md

@@ -180,6 +180,13 @@ leaves an empty ledger and the run builds. With the flag, the same item stops th
 an empty ledger stalls it (`TestAnAdvisoryRunMovesPastAnItemWhoseCheckKeepsFailing`,
 `TestARunThatRequiresProofStillStopsOnTheItem`).
 
+Without the flag the model's claim of completion ends the run, but only once no item is
+open: a claim made while an item is neither proven nor abandoned is held, and the run goes
+on to that item. An item whose check the host could not run at all is abandoned when the
+claim arrives, since rerunning a refused check teaches the run nothing
+(`TestAClaimWaitsForAnItemNobodyTried`, `TestAClaimMovesPastAnItemWhoseCheckCannotRun`,
+`TestAClaimUnderProofStillStops`).
+
 `goal.Cleaner`: a nil cleaner means there is nothing external to tear down, which is
 true of the standalone binary. Child goals are removed through owner references. A
 delete with no cleaner completes instead of waiting on a finalizer

docs/releases/v0.2.0.md

@@ -71,6 +71,8 @@ Run `flynn version` afterwards; it should name a `v0.2.0-rc` release. v0.1.3 can
 - On Windows a command the agent ran had no memory cap unless you passed `--max-memory`, and its process cap (4096) did not bound memory. A command that kept starting copies of itself, here a `go` shim on `PATH` that resolved back to itself, used all of a 95 GB machine's memory at a few hundred processes. With no `--max-memory`, a command and everything it starts may now commit at most half the machine's physical memory, in `flynn goal`, the interactive session, `flynn serve` and the MCP server. Pass `--max-memory` to set another cap. Local model servers are not affected.
 - `flynn resume` rebuilt a run without the guards it was started with. A planned goal resumed after a crash or kill then stalled at its first item check with `goal_no_verifier`, and a resumed run had no `--max-cost` or `--max-tokens` cap, no `--require-approval` gate, no `--irreversible` gate and no `--require-proof`. A resume now reads how the run was first assembled from its record and wires the same guards, with the spend already recorded still counted against the cap. A run driven by an external agent CLI is refused, since resume drives a native model.
 - Without `--require-proof` a goal still stopped when a check it wrote for itself kept failing, though the ledger is documented as a record in that mode. A wrong check (a quoting mistake, or a check for a file the objective never asked for) ended the run after two cycles, and the model spent those cycles reshaping the work to fit the check. Such an item is now left unproven on the record with the failure that gave it up, the run moves to the next item, and the model is told to name it in its answer and not to bend the work to a check it thinks is wrong. An objective with nothing checkable, such as "run this and report", is no longer planned with invented checks, and an empty plan no longer stops the run. With `--require-proof` both still stop the run. A planned goal now ends by printing how many of its items were proven and naming each one that was not.
+- Without `--require-proof` a planned goal ended as soon as the model said it was done, even with items in its plan that it had never attempted. The model is briefed on one item at a time, so a run resumed after a kill redid its first item, said "Done" and stopped with the rest of the plan untouched. A claim of completion now waits until every item is proven or has been moved past; an item whose check the host cannot run at all is moved past when the model claims completion, so a run on such a host still finishes. `--require-proof` is unchanged.
+- A run continued with `flynn resume` was never sealed, so `flynn spine verify` refused it with "has no signed record". A resumed run is now sealed when it ends, with how it ended on the record if it stopped. A resume interrupted with Ctrl-C is left open, since it can be resumed again.
 - A confined signer on Windows can read its sealed key.
 - The interactive session could hang reading input when a multi-byte character arrived with no room left for it in the read buffer.
 - Markdown in the terminal could render a line one cell wider than the screen, so it wrapped.

goal/ledgerloop.go

@@ -50,6 +50,51 @@ func (g *Reconciler) holdsClaimAgainstLedger(spec Spec, status Status) bool {
 		status.Planned && len(spec.Ledger) > 0 && !status.LedgerSettled()
 }
 
+// claimOverOpenItem reports whether a completion claim in a run that does not require
+// proof has to wait for the ledger: an item is still neither proven nor moved past. Such a
+// run's completion is the model's call once every item has been tried, never before. A
+// model briefed on one item says it is done when that item is, and accepting that would
+// end the run with the rest of the plan never attempted. Each open item is still bounded:
+// a check that keeps failing the same way moves the run past it (moveOffUnprovableItem),
+// and the step budget bounds the rest.
+func (g *Reconciler) claimOverOpenItem(spec Spec, status Status) bool {
+	if g.ledgerConverge || !g.ledgerGated() || !status.Planned {
+		return false
+	}
+	_, open := status.CurrentItem(spec.Ledger)
+	return open
+}
+
+// moveOffUnrunnableItem abandons the current item when the run has claimed completion and
+// the item's latest check, taken after its last build, could not be run at all (the
+// sandbox refused it, or there was no check). Holding the claim for such an item teaches
+// the run nothing: the host refuses the same check the same way every time, and a check
+// that never ran is never counted as a repeat, so the run would spin until the no-progress
+// guard stalled it. Only a claim reaches here, so an item the model is still working on
+// keeps its chance. recorded is the run's verifications in recorded order.
+func (g *Reconciler) moveOffUnrunnableItem(spec Spec, status *Status, recorded []Verification) {
+	if status.VerifyPending {
+		return // the latest check predates the last build; it says nothing about the work now
+	}
+	item, ok := status.CurrentItem(spec.Ledger)
+	if !ok {
+		return
+	}
+	for i := len(recorded) - 1; i >= 0; i-- {
+		if recorded[i].Item != item.ID {
+			continue
+		}
+		if recorded[i].Provenance != ProvenanceExecuted {
+			detail := status.ItemFeedback
+			if detail == "" {
+				detail = recorded[i].Reason
+			}
+			status.abandonCurrent(spec.Ledger, "its check could not be run: "+strings.TrimSpace(detail))
+		}
+		return
+	}
+}
+
 // refuseCompletion settles a goal whose model reported success over an unproven ledger,
 // naming each unproven item and the reason the gate would refuse it.
 //

goal/ledgerloop_producer_test.go

@@ -8,6 +8,7 @@ package goal
 import (
 	"encoding/json"
 	"errors"
+	"strings"
 	"testing"
 	"time"
 
@@ -177,8 +178,9 @@ func TestConsumptionSurvivesARestart(t *testing.T) {
 // TestTheProducerRunsBeforeTheRefusalDoes is the staging the rollout depends on: with the
 // loop wired but the refusal not yet turned on, items still flip to proven from the record
 // (so a build can be observed actually proving things) while a completion claim is still
-// the model's to make. Without this split the refusal would have to be switched on ahead of
-// any evidence that the producer works, which is what stalls every goal.
+// the model's to make once the plan has been worked through. Without this split the refusal
+// would have to be switched on ahead of any evidence that the producer works, which is what
+// stalls every goal.
 func TestTheProducerRunsBeforeTheRefusalDoes(t *testing.T) {
 	ev := &fakeEvidence{}
 	h := newHarness(t, alwaysMet{}, WithLedgerGate(ev, newGate(t, RequireExecuted())))
@@ -187,6 +189,8 @@ func TestTheProducerRunsBeforeTheRefusalDoes(t *testing.T) {
 	if _, err := ev.Record(h.ctx, resource.Resource{}, ledger[0].ID, ItemVerdict{Passed: true, Executed: true}); err != nil {
 		t.Fatal(err)
 	}
+	// The second item was tried and given up on, so nothing in the plan is still open.
+	h.setStatus(t, ref, func(st *Status) { st.Ledger[1].Abandoned = true })
 
 	h.reconcile(t, ref)
 
@@ -199,6 +203,83 @@ func TestTheProducerRunsBeforeTheRefusalDoes(t *testing.T) {
 	}
 }
 
+// TestAClaimWaitsForAnItemNobodyTried is the resumed run that ended after its first item:
+// the model, briefed on one item, says it is done when that item is. Without proof
+// required the claim is still the model's, but not while an item it never attempted is
+// open, so the run goes on to build that item instead of converging over it.
+func TestAClaimWaitsForAnItemNobodyTried(t *testing.T) {
+	ev := &fakeEvidence{}
+	h := newHarness(t, alwaysMet{}, WithLedgerGate(ev, newGate(t, RequireExecuted())))
+	ledger := twoItemLedger(t)
+	ref := h.plannedGoal(t, "open-item", ledger)
+	if _, err := ev.Record(h.ctx, resource.Resource{}, ledger[0].ID, ItemVerdict{Passed: true, Executed: true}); err != nil {
+		t.Fatal(err)
+	}
+
+	h.reconcile(t, ref)
+
+	st := h.status(t, ref)
+	if st.Phase == PhaseConverged {
+		t.Fatalf("the run converged with %q never attempted", ledger[1].Item)
+	}
+	if st.Phase == PhaseStalled {
+		t.Fatalf("the run stalled instead of building the open item: %s", st.Message)
+	}
+	if st.InFlight == nil || st.InFlight.Kind != StepJobKind {
+		t.Fatalf("in flight = %+v, want a build step for the open item", st.InFlight)
+	}
+}
+
+// TestAClaimMovesPastAnItemWhoseCheckCannotRun: on a host that refuses the check outright
+// the item can never be proven, and a check that did not run is not counted as a repeat,
+// so holding the claim for it would spin until the no-progress guard stalled the run. The
+// claim instead moves the run past the item, which stays unproven with the reason.
+func TestAClaimMovesPastAnItemWhoseCheckCannotRun(t *testing.T) {
+	ev := &fakeEvidence{}
+	h := newHarness(t, alwaysMet{}, WithLedgerGate(ev, newGate(t, RequireExecuted())))
+	ledger := twoItemLedger(t)
+	ref := h.plannedGoal(t, "unrunnable", ledger)
+	for _, it := range ledger {
+		if _, err := ev.Record(h.ctx, resource.Resource{}, it.ID, ItemVerdict{Detail: "the check could not run: refused"}); err != nil {
+			t.Fatal(err)
+		}
+	}
+
+	// One item per claim: the second has a refused check on the record too, so the next
+	// claim moves past it and the plan is worked through.
+	h.reconcile(t, ref)
+	h.setStatus(t, ref, func(st *Status) { st.InFlight = nil })
+	h.reconcile(t, ref)
+
+	st := h.status(t, ref)
+	if st.Phase != PhaseConverged {
+		t.Fatalf("phase = %q, want the claim honoured once no item can be worked: %s", st.Phase, st.Message)
+	}
+	for i, ls := range st.Ledger {
+		if ls.Proven || !ls.Abandoned || !strings.Contains(ls.AbandonedReason, "could not be run") {
+			t.Errorf("item %d = %+v, want it left unproven because its check could not run", i, ls)
+		}
+	}
+}
+
+// TestAClaimUnderProofStillStops: the require-proof refusal is the line that must not be
+// softened, so an open item there still settles the run as stalled rather than going on.
+func TestAClaimUnderProofStillStops(t *testing.T) {
+	ev := &fakeEvidence{}
+	h := newHarness(t, alwaysMet{}, WithLedgerGate(ev, newGate(t, RequireExecuted())), WithLedgerConvergence())
+	ledger := twoItemLedger(t)
+	ref := h.plannedGoal(t, "proof", ledger)
+	if _, err := ev.Record(h.ctx, resource.Resource{}, ledger[0].ID, ItemVerdict{Passed: true, Executed: true}); err != nil {
+		t.Fatal(err)
+	}
+
+	h.reconcile(t, ref)
+
+	if st := h.status(t, ref); st.Phase != PhaseStalled {
+		t.Fatalf("phase = %q, want the unproven item to stop a run that requires proof", st.Phase)
+	}
+}
+
 // TestAProofSurvivesTheDispatchWrite: the ledger has two writers, so the dispatch write
 // merges rather than adopting one side. Taking the worker's copy wholesale would drop the
 // proof this very pass admitted, and the item would be re-verified forever.

goal/reconciler.go

@@ -352,6 +352,16 @@ func (g *Reconciler) judgeOrStep(ctx context.Context, r resource.Resource, spec
 			return g.terminal(ctx, r, *status, specHash)
 		}
 	}
+	// Without proof required the claim is accepted, but only once the plan has been worked
+	// through. The claim's wording is dropped with it, so the non-convergence count below
+	// compares the open item's check output and not the model's varying account of being
+	// done.
+	if met && g.claimOverOpenItem(spec, *status) {
+		g.moveOffUnrunnableItem(spec, status, recorded)
+		if g.claimOverOpenItem(spec, *status) {
+			met, reason = false, ""
+		}
+	}
 	// Fold this cycle's refusal into the non-convergence count. It sits here because this
 	// is the first point where both halves of the refusal are current: the evaluator has
 	// just spoken, and under the ledger gate the item's check has just been settled, so