fix(goal): move past a failing ledger check unless proof is required

cmd/flynn/driveopts.go

@@ -83,7 +83,8 @@ func withPlanning() driveOption {
 // It is separate from withPlanning because the two carry different risk. Planning always
 // runs the producer, so a run's items visibly flip to proven and a run's report can say
 // how many were proven by execution; this adds the refusal on top, which is the part that
-// can stop a run whose plan wrote checks no machine can run. It is staged, not optional:
+// can stop a run whose plan wrote checks no machine can run. Without it an item whose
+// check keeps failing is left unproven and the run moves on (see goal.LedgerState). It is staged, not optional:
 // the refusal is the point of keeping a ledger, and a build that never turns it on has a
 // plan that decides nothing.
 func withLedgerProof() driveOption {

cmd/flynn/ledgerline_test.go

@@ -8,6 +8,7 @@ import (
 	"testing"
 	"time"
 
+	"github.com/ionalpha/flynn/goal"
 	"github.com/ionalpha/flynn/harness"
 	"github.com/ionalpha/flynn/llm/llmtest"
 )
@@ -78,3 +79,41 @@ func TestAPlannedRunSaysWhatItsLedgerWillDo(t *testing.T) {
 		t.Fatalf("a planned run did not say its ledger proof is available and off:\n%s", out.String())
 	}
 }
+
+// TestLedgerOutcomeNamesWhatWasLeftUnproven: a run that does not require proof can finish
+// with items unproven, and the operator learns that from the run's own output, with the
+// failure that made the run move past each one, rather than from the model's answer.
+func TestLedgerOutcomeNamesWhatWasLeftUnproven(t *testing.T) {
+	ledger, err := goal.AppendItems(nil,
+		goal.LedgerItem{Item: "add the endpoint", Verify: "curl --fail localhost/health"},
+		goal.LedgerItem{Item: "write the report file", Verify: "findstr ok report.txt"},
+		goal.LedgerItem{Item: "cover it with a test", Verify: "go test ./api/..."},
+	)
+	if err != nil {
+		t.Fatal(err)
+	}
+	var st goal.Status
+	st.SyncLedger(ledger)
+	if err := st.MarkProven(ledger[0].ID, "1", time.Unix(0, 0).UTC()); err != nil {
+		t.Fatal(err)
+	}
+	st.Ledger[1].Abandoned = true
+	st.Ledger[1].AbandonedReason = "its check failed the same way on 2 consecutive runs: exit 1"
+
+	got := strings.Join(ledgerOutcomeLines(goal.Spec{Ledger: ledger}, st), "\n")
+	for _, want := range []string{
+		"1 of 3 planned item(s) proven",
+		"unproven, moved past: write the report file (its check failed the same way on 2 consecutive runs: exit 1)",
+		"unproven: cover it with a test",
+	} {
+		if !strings.Contains(got, want) {
+			t.Fatalf("outcome missing %q:\n%s", want, got)
+		}
+	}
+	if strings.Contains(got, "add the endpoint") {
+		t.Fatalf("a proven item was listed as unproven:\n%s", got)
+	}
+	if lines := ledgerOutcomeLines(goal.Spec{}, goal.Status{}); lines != nil {
+		t.Fatalf("a goal with no ledger printed %q", lines)
+	}
+}

cmd/flynn/run.go

@@ -95,6 +95,9 @@ func (r driveRequest) execute(ctx context.Context) (result, source string, trans
 	}
 
 	result, transcript, _, runErr := renderStream(w, events, r.verbose, r.cfg.observe)
+	for _, line := range r.ledgerOutcome(ctx, run.ID()) {
+		_, _ = fmt.Fprintln(w, line)
+	}
 	if r.cfg.extAgent != nil {
 		r.declareProvenance(runCtx, w, run)
 	}
@@ -104,6 +107,55 @@ func (r driveRequest) execute(ctx context.Context) (result, source string, trans
 	return result, run.ID(), transcript, runErr
 }
 
+// ledgerOutcome reads the run's goal after it settles and says how much of its plan was
+// proven. A run that does not require proof can finish with items left unproven, and the
+// model's answer is not where an operator should have to learn that: the model is told to
+// name them, and this line is what holds when it does not.
+func (r driveRequest) ledgerOutcome(ctx context.Context, id string) []string {
+	if r.rstore == nil {
+		return nil
+	}
+	rec, err := r.rstore.Get(context.WithoutCancel(ctx), goal.Kind, resource.Scope{}, id)
+	if err != nil {
+		return nil
+	}
+	spec, serr := goal.DecodeSpec(rec)
+	status, derr := goal.DecodeStatus(rec)
+	if serr != nil || derr != nil {
+		return nil
+	}
+	return ledgerOutcomeLines(spec, status)
+}
+
+// ledgerOutcomeLines renders a settled goal's ledger: how many planned items were proven,
+// then each item left unproven, with the failure that gave it up when the run moved past
+// it. A goal with no ledger says nothing.
+func ledgerOutcomeLines(spec goal.Spec, status goal.Status) []string {
+	if len(spec.Ledger) == 0 {
+		return nil
+	}
+	settled := make(map[string]goal.LedgerState, len(status.Ledger))
+	proven := 0
+	for _, st := range status.Ledger {
+		settled[st.ID] = st
+		if st.Proven {
+			proven++
+		}
+	}
+	lines := []string{fmt.Sprintf("  ledger: %d of %d planned item(s) proven", proven, len(spec.Ledger))}
+	for _, it := range spec.Ledger {
+		st := settled[it.ID]
+		switch {
+		case st.Proven:
+		case st.Abandoned:
+			lines = append(lines, fmt.Sprintf("    unproven, moved past: %s (%s)", it.Item, st.AbandonedReason))
+		default:
+			lines = append(lines, "    unproven: "+it.Item)
+		}
+	}
+	return lines
+}
+
 // assembly is the request as the governed-run assembly takes it. A caller-supplied
 // toolset, an external agent CLI, fan-out and the plain conversation each get their own
 // mode of it, and all of them record the same session and apply the same governance.
@@ -209,5 +261,5 @@ func ledgerLine(planned, proof bool) string {
 	case proof:
 		return "  ledger: each item's check runs, and an item with no passing check on the record stops the run"
 	}
-	return "  ledger: each item's check runs and is recorded; --require-proof also stops the run on an item it cannot prove"
+	return "  ledger: each item's check runs and is recorded, and an item whose check keeps failing is left unproven; --require-proof stops the run on it instead"
 }

docs/HOST_BOUNDARY.md

@@ -170,6 +170,16 @@ run's sandbox and its verdict goes on the record. The flag adds the refusal that
 those verdicts. A run prints which of the two applies before it starts (`ledgerLine`
 in `cmd/flynn/run.go`).
 
+Without the flag the ledger is a record and never a stop. The checks are the model's own,
+written before any work, and some can never pass (a quoting mistake) or check for
+something the objective never asked for. An item whose executed check fails the same way
+on consecutive runs, or names a program the host does not have, is marked abandoned:
+still unproven on the record, with the failure that gave it up, and the run moves to the
+next item and is told to name it in its answer. A planner that finds nothing checkable
+leaves an empty ledger and the run builds. With the flag, the same item stops the run and
+an empty ledger stalls it (`TestAnAdvisoryRunMovesPastAnItemWhoseCheckKeepsFailing`,
+`TestARunThatRequiresProofStillStopsOnTheItem`).
+
 `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

@@ -70,6 +70,7 @@ Run `flynn version` afterwards; it should name a `v0.2.0-rc` release. v0.1.3 can
 - `go test`, `npm install` and `pip install` failed inside the sandbox: a confined command could not write the caches these tools keep under the home directory, on macOS it could not write its own `TMPDIR`, and on Windows its `TEMP` was the workspace, where Go ignores a `go.mod`. Each sandbox now has a private scratch directory outside the workspace, writable by its commands and deleted when the sandbox closes. The temp variables, `GOCACHE`, `GOMODCACHE`, `npm_config_cache` and `PIP_CACHE_DIR` point into it unless you set them yourself. On Linux it is under `/var/tmp`, so the caches last from one command to the next.
 - 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.
 - 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/environment_test.go

@@ -172,7 +172,9 @@ func TestAMissingProgramStopsAsAnEnvironmentProblem(t *testing.T) {
 	}
 	ev := &fakeEvidence{}
 	ver := &fakeVerifier{verdicts: []ItemVerdict{missing}}
-	h, w := producerHarness(t, ver, ev)
+	// Proof is required: an advisory run moves past the item instead (see
+	// TestAnAdvisoryRunMovesPastAnItemWhoseProgramIsMissing).
+	h, w := producerHarness(t, ver, ev, WithLedgerConvergence())
 
 	ledger := twoItemLedger(t)
 	ref := h.plannedGoal(t, "missing-program", ledger)
@@ -297,12 +299,13 @@ func TestCommandWords(t *testing.T) {
 }
 
 // runChecksTo drives EnvironmentRepeatLimit rounds of build, verify and observe against a
-// planned two-item ledger whose verifier returns the given verdict every time.
-func runChecksTo(t *testing.T, v ItemVerdict, rounds int) (Status, *fakeEvidence) {
+// planned two-item ledger whose verifier returns the given verdict every time. opts go to
+// the reconciler, as for producerHarness.
+func runChecksTo(t *testing.T, v ItemVerdict, rounds int, opts ...Option) (Status, *fakeEvidence) {
 	t.Helper()
 	ev := &fakeEvidence{}
 	ver := &fakeVerifier{verdicts: []ItemVerdict{v}}
-	h, w := producerHarness(t, ver, ev)
+	h, w := producerHarness(t, ver, ev, opts...)
 	ref := h.plannedGoal(t, "checks", twoItemLedger(t))
 	h.setStatus(t, ref, func(st *Status) { st.Planned = true })
 	for range rounds {
@@ -329,7 +332,7 @@ func TestAnAgentToolNamedInACheckStopsAsAnEnvironmentProblem(t *testing.T) {
 		Executed: true, ExitCode: 1,
 		Output: "'skill_read' is not recognized as an internal or external command,\noperable program or batch file.",
 		Detail: "exit 1: 'skill_read' is not recognized as an internal or external command",
-	}, EnvironmentRepeatLimit)
+	}, EnvironmentRepeatLimit, WithLedgerConvergence())
 
 	if len(ev.recs) == 0 || ev.recs[0].Provenance == ProvenanceExecuted {
 		t.Fatalf("recorded %+v: a check that never ran must not be on the record as executed", ev.recs)
@@ -354,7 +357,7 @@ func TestAnAgentToolNamedInACheckStopsAsAnEnvironmentProblem(t *testing.T) {
 func TestACheckThatRanAndFailedAtExitOneStillCountsAsNotConverging(t *testing.T) {
 	st, ev := runChecksTo(t, ItemVerdict{
 		Executed: true, ExitCode: 1, Output: "FAIL: TestHealth: got 500, want 200", Detail: "exit 1: FAIL",
-	}, VerdictRepeatLimit)
+	}, VerdictRepeatLimit, WithLedgerConvergence())
 
 	if len(ev.recs) == 0 || ev.recs[0].Provenance != ProvenanceExecuted {
 		t.Fatalf("recorded %+v: a check that ran must stay on the record as executed", ev.recs)

goal/ledger.go

@@ -63,6 +63,15 @@ type LedgerState struct {
 	// note instead.
 	ProvenAt *time.Time `json:"provenAt,omitempty"`
 	Evidence string     `json:"evidence,omitempty"`
+	// Abandoned marks an item the run stopped working without proving it, and
+	// AbandonedReason is the check failure that made it stop. Only a run that does not
+	// require proof abandons an item (see [Reconciler] and [WithLedgerConvergence]): its
+	// checks are the model's own guess at what done looks like, written before any work,
+	// and a check that can never pass would otherwise end a run that was told the record
+	// is only advisory. The item stays unproven, so the record still says the plan was
+	// not proven in full; the mark only moves the run on to the next item.
+	Abandoned       bool   `json:"abandoned,omitempty"`
+	AbandonedReason string `json:"abandonedReason,omitempty"`
 }
 
 // ItemID returns the content address of an item: the first ledgerIDLen hex characters of
@@ -233,25 +242,57 @@ func (s Status) Unproven() []string {
 	return out
 }
 
-// CurrentItem returns the item the run is working: the first ledger item still unproven.
-// It reports false when the ledger is empty or every item is proven.
+// CurrentItem returns the item the run is working: the first ledger item neither proven
+// nor abandoned. It reports false when the ledger is empty or every item is settled one
+// way or the other.
 //
 // The selection is derived and not stored on the status, so there is no second
 // representation of "where the run is" to drift from the record. The reconciler, the
 // executor and the producer all compute the same answer from the same two facts.
 func (s Status) CurrentItem(ledger []LedgerItem) (LedgerItem, bool) {
-	proven := make(map[string]bool, len(s.Ledger))
+	done := make(map[string]bool, len(s.Ledger))
 	for _, st := range s.Ledger {
-		proven[st.ID] = st.Proven
+		done[st.ID] = st.Proven || st.Abandoned
 	}
 	for _, it := range ledger {
-		if !proven[it.ID] {
+		if !done[it.ID] {
 			return it, true
 		}
 	}
 	return LedgerItem{}, false
 }
 
+// Abandoned returns the items the run moved past without proving, in ledger order.
+func (s Status) Abandoned() []LedgerState {
+	var out []LedgerState
+	for _, st := range s.Ledger {
+		if st.Abandoned && !st.Proven {
+			out = append(out, st)
+		}
+	}
+	return out
+}
+
+// abandonCurrent marks the current item abandoned with reason and clears every count
+// that was about its check, so the next item starts from nothing. The counts must go
+// with it: left in place, the next item's first failure would read as the abandoned
+// item's third and stop the run.
+func (s *Status) abandonCurrent(ledger []LedgerItem, reason string) {
+	item, ok := s.CurrentItem(ledger)
+	if !ok {
+		return
+	}
+	for i := range s.Ledger {
+		if s.Ledger[i].ID == item.ID {
+			s.Ledger[i].Abandoned = true
+			s.Ledger[i].AbandonedReason = reason
+		}
+	}
+	s.ItemFeedback = ""
+	s.MissingCommand, s.MissingRepeat = "", 0
+	s.LastVerdict, s.VerdictMark, s.VerdictRepeat = "", "", 0
+}
+
 // LedgerSettled reports whether the ledger has items and all of them are proven. An empty
 // ledger is not settled: a goal with nothing planned has not started.
 func (s Status) LedgerSettled() bool {

goal/ledger_test.go

@@ -46,7 +46,7 @@ type planHarness struct {
 	p *fakePlanner
 }
 
-func newPlanHarness(t *testing.T, stop StopEvaluator, planner *fakePlanner) *planHarness {
+func newPlanHarness(t *testing.T, stop StopEvaluator, planner *fakePlanner, opts ...Option) *planHarness {
 	t.Helper()
 	m := clock.NewManual(time.Date(2026, 1, 1, 0, 0, 0, 0, time.UTC))
 	reg := resource.NewRegistry()
@@ -58,7 +58,7 @@ func newPlanHarness(t *testing.T, stop StopEvaluator, planner *fakePlanner) *pla
 	}
 	store := resource.NewMemory(reg, resource.WithClock(m))
 	q := jobs.NewMemory(jobs.WithClock(m))
-	gr := NewReconciler(store, q, m, stop, WithPlanning())
+	gr := NewReconciler(store, q, m, stop, append([]Option{WithPlanning()}, opts...)...)
 	w := NewWorker(store, q, m, &fakeExec{}, WithPlanner(planner), WithLease(time.Minute))
 	h := &harness{ctx: context.Background(), store: store, jobs: q, gr: gr, clk: m}
 	return &planHarness{harness: h, w: w, p: planner}
@@ -471,11 +471,11 @@ func TestPlanningDoesNotSpendTheBuildBudget(t *testing.T) {
 	}
 }
 
-// TestAnEmptyPlanStallsTheGoal: a planner that produced nothing leaves no
-// definition of done. Building anyway is how a run claims success against a record
-// that never said what success was.
-func TestAnEmptyPlanStallsTheGoal(t *testing.T) {
-	h := newPlanHarness(t, neverStop{}, &fakePlanner{})
+// TestAnEmptyPlanStallsAGoalThatRequiresProof: a planner that produced nothing leaves
+// no definition of done. Building anyway is how a run claims success against a record
+// that never said what success was, and a run that requires proof has nothing to prove.
+func TestAnEmptyPlanStallsAGoalThatRequiresProof(t *testing.T) {
+	h := newPlanHarness(t, neverStop{}, &fakePlanner{}, WithLedgerConvergence())
 	ref := h.createGoal(t, "g", Spec{Objective: "o", StopCondition: "c"})
 
 	h.reconcile(t, ref)
@@ -493,6 +493,27 @@ func TestAnEmptyPlanStallsTheGoal(t *testing.T) {
 	}
 }
 
+// TestAnEmptyPlanBuildsAGoalThatDoesNotRequireProof: completion in such a run is the
+// model's call whatever the ledger says, and an objective whose result is only a report
+// has nothing for a check to read. Stopping it for an empty plan would stop exactly the
+// runs the planner was told to leave unplanned.
+func TestAnEmptyPlanBuildsAGoalThatDoesNotRequireProof(t *testing.T) {
+	h := newPlanHarness(t, neverStop{}, &fakePlanner{})
+	ref := h.createGoal(t, "g", Spec{Objective: "o", StopCondition: "c"})
+
+	h.reconcile(t, ref)
+	if _, err := h.w.ProcessOnce(h.ctx); err != nil {
+		t.Fatalf("worker: %v", err)
+	}
+	h.reconcile(t, ref)
+
+	st := h.status(t, ref)
+	if st.Phase == PhaseStalled {
+		t.Fatalf("an advisory run stalled on an empty plan: %q", st.Message)
+	}
+	h.completeJob(t, StepJobKind) // the next dispatch is a build step
+}
+
 // TestPlanningRunsOnce pins that the planning mark, not the ledger's emptiness, is
 // what ends the phase, and that a re-reconcile does not plan the goal again.
 func TestPlanningRunsOnce(t *testing.T) {

goal/ledgerloop.go

@@ -61,3 +61,30 @@ func (g *Reconciler) refuseCompletion(status *Status, recorded []Verification) {
 	status.stall("LedgerUnproven", fmt.Sprintf("completion reported with %d planned item(s) unproven: %s",
 		len(reasons), strings.Join(reasons, "; ")), g.clk.Now())
 }
+
+// moveOffUnprovableItem abandons the current item, in a run that does not require proof,
+// once its check has failed the same way twice or named a missing program twice. feedback
+// is the executed check failure this cycle was counted on, or "" when none ran.
+//
+// The checks are the model's own, written before any work, and some can never pass (a
+// quoting mistake) or check for a file the objective never asked for. Left to the
+// non-convergence guard, either one stops a run whose ledger the operator was told is
+// only a record. The item stays unproven, with the failure that gave it up.
+//
+// A run that requires proof stops on the item instead, and a repeated refusal with no
+// check failure in it is still the non-convergence stop.
+func (g *Reconciler) moveOffUnprovableItem(spec Spec, status *Status, feedback string) {
+	if g.ledgerConverge || !g.ledgerGated() || !status.Planned {
+		return
+	}
+	var reason string
+	switch {
+	case status.StalledForEnvironment():
+		reason = status.EnvironmentReason()
+	case feedback != "" && status.StalledForNonConvergence():
+		reason = fmt.Sprintf("its check failed the same way on %d consecutive runs: %s", status.VerdictRepeat, feedback)
+	default:
+		return
+	}
+	status.abandonCurrent(spec.Ledger, reason)
+}