Phase 0: harden completion semantics and terminal integrity

README.md

@@ -216,7 +216,7 @@ terminal outcome:
   .loop/
     manifest.yaml        # contract metadata
     state.json           # live FSM cursor
-    terminal_state.json  # final exit record; written once — emit refuses overwrite without force=True
+    terminal_state.json  # final exit record; immutable once written
     artifacts/           # evidence bundles and intermediate outputs
     approvals/           # approval requests and resolutions
     checkpoints/         # recoverable snapshots
@@ -301,7 +301,8 @@ otherwise, the stop is blocked with the exact doctor issues. No-op without
 **Any Python runtime** — `loop.emit` is a pure-stdlib writer for foreign
 orchestrators (LangGraph, or anything that can call four functions):
 `open_contract`, `append_iteration`, `append_receipt`, `terminate`. The writer
-refuses an evidence-free `Succeeded` at write time. Recipe:
+refuses `Succeeded` unless every declared criterion is true and evidence is
+present. Recipe:
 [docs/integrations/langgraph.md](docs/integrations/langgraph.md).
 
 **CI** — one workflow step validates the contract and publishes a scorecard:

docs/adr/0001-proof-kernel-and-runtime.md

@@ -0,0 +1,104 @@
+# ADR 0001: Separate the proof kernel from the execution runtime
+
+- **Status:** Accepted
+- **Date:** 2026-07-12
+- **Decision owners:** Loop Engineer maintainers
+
+## Context
+
+Loop Engineer began as a portable contract and proof layer. Its current core is
+valuable because it defines typed terminal states, evidence-gated completion,
+anti-cheat checks, bounded repair, and repo-native state without binding those
+concepts to a particular orchestration framework.
+
+The product goal is broader: a user should be able to provide a complex goal,
+receive a reviewable loop design, execute it through interchangeable agents and
+tools, pause for approvals, recover from failure, and obtain an independently
+verified terminal result.
+
+Keeping execution out of the project would preserve a small scope, but it would
+also leave the most important invariants as instructions that a host agent may
+ignore. Folding every concern into one package would create the opposite
+problem: provider-specific execution details would contaminate the portable
+proof protocol.
+
+## Decision
+
+Loop Engineer will have two first-party layers with a strict dependency
+direction.
+
+### 1. Proof kernel
+
+The proof kernel is the stable, runtime-neutral protocol. It owns:
+
+- contract and schema versions;
+- deterministic completion-policy evaluation;
+- legal state and terminal-state projection;
+- evidence and provenance rules;
+- verifier and anti-cheat interfaces;
+- policy validation and conformance tests;
+- event reduction and replay semantics.
+
+The kernel must not import model providers, agent frameworks, or workflow
+engines. It may be embedded by foreign runtimes.
+
+### 2. Execution runtime
+
+The execution runtime interprets a validated Loop Plan and owns:
+
+- planning and task scheduling;
+- worker leases and attempt numbers;
+- agent and tool dispatch;
+- budgets, retries, timeouts, pause, resume, and cancellation;
+- approvals and side-effect policy;
+- checkpointing and crash recovery;
+- persistence of immutable events and artifacts.
+
+The runtime depends on the kernel. The kernel never depends on the runtime.
+
+## Governing rule
+
+**Agents propose; the kernel disposes.**
+
+An agent may propose a command, patch, transition, or completion claim. Only the
+kernel may validate and commit a state transition or terminal result.
+
+## Immediate consequences
+
+1. `Succeeded` uses an explicit completion policy. The first supported policy is
+   `all_required`; every declared criterion must be proven true.
+2. Terminal records are immutable. Corrections will be represented by separate,
+   auditable administrative events rather than file replacement.
+3. New state writers use canonical integer iteration identifiers. Legacy
+   numeric strings remain a read-compatibility concern until a versioned state
+   migration removes them.
+4. The next persistence milestone will introduce an `EventStore` protocol and a
+   SQLite/WAL implementation. JSON and Markdown files become projections rather
+   than the sole authoritative state.
+5. Provider and model selection will be capability-based, not encoded in the
+   portable contract as vendor model names.
+
+## Non-goals of this decision
+
+This ADR does not select a distributed scheduler, hosted control plane, web UI,
+or model provider. It also does not make structural evidence equivalent to
+cryptographic attestation. Those require separate decisions.
+
+## Rejected alternatives
+
+### Remain contract-only
+
+Rejected because the desired product must execute and govern loops end to end.
+A prose-only state machine cannot reliably enforce concurrency, approvals,
+budgets, or immutable terminal decisions.
+
+### Build a monolithic provider-specific agent framework
+
+Rejected because it would erase the strongest differentiation: a portable proof
+contract that can sit above multiple runtimes.
+
+### Permit terminal overwrite for operator convenience
+
+Rejected because an overwritten terminal record destroys audit history and
+creates a race in which a later writer can launder an earlier result. A future
+supersession event can preserve both the original decision and the correction.

loop/completion.py

@@ -0,0 +1,73 @@
+"""Deterministic completion-policy evaluation.
+
+The first portable policy is intentionally narrow: every declared acceptance
+criterion is required.  Keeping the evaluator in a small, side-effect-free
+module lets emitters, runtime adapters, and contract validation share exactly
+the same success semantics.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Mapping
+from typing import Final, Literal, TypeAlias, cast
+
+CompletionMode: TypeAlias = Literal["all_required"]
+DEFAULT_COMPLETION_MODE: Final[CompletionMode] = "all_required"
+SUPPORTED_COMPLETION_MODES: Final[tuple[CompletionMode, ...]] = (DEFAULT_COMPLETION_MODE,)
+
+
+class CompletionPolicyError(ValueError):
+    """The requested completion policy is malformed or unsupported."""
+
+
+def normalize_completion_policy(policy: object | None = None) -> dict[str, CompletionMode]:
+    """Return the canonical JSON form of a supported completion policy.
+
+    ``None`` is the compatibility default for terminal@1 records created before
+    the policy field existed.  New writers should always persist the returned
+    object explicitly.
+    """
+    if policy is None:
+        mode: object = DEFAULT_COMPLETION_MODE
+    elif isinstance(policy, str):
+        mode = policy
+    elif isinstance(policy, Mapping):
+        unexpected = sorted(str(key) for key in policy if key != "mode")
+        if unexpected:
+            raise CompletionPolicyError(
+                "completion_policy contains unsupported fields: " + ", ".join(unexpected)
+            )
+        if "mode" not in policy:
+            raise CompletionPolicyError("completion_policy.mode is required")
+        mode = policy.get("mode")
+    else:
+        raise CompletionPolicyError(
+            "completion_policy must be null, a mode string, or an object with a mode field"
+        )
+
+    if mode not in SUPPORTED_COMPLETION_MODES:
+        supported = ", ".join(SUPPORTED_COMPLETION_MODES)
+        raise CompletionPolicyError(
+            f"unsupported completion policy mode {mode!r}; expected one of: {supported}"
+        )
+    return {"mode": cast(CompletionMode, mode)}
+
+
+def criteria_satisfy_completion(
+    criteria_met: Mapping[str, object],
+    policy: object | None = None,
+) -> bool:
+    """Return whether a criteria map satisfies the declared policy.
+
+    An empty map never proves completion.  Values must be the boolean singleton
+    ``True``; truthy substitutes such as ``1`` are deliberately rejected.
+    """
+    normalized = normalize_completion_policy(policy)
+    if normalized["mode"] == "all_required":
+        return bool(criteria_met) and all(value is True for value in criteria_met.values())
+    raise AssertionError(f"unhandled completion policy: {normalized!r}")
+
+
+def unmet_required_criteria(criteria_met: Mapping[str, object]) -> tuple[str, ...]:
+    """Return stable string identifiers for criteria not proven true."""
+    return tuple(sorted(key for key, value in criteria_met.items() if value is not True))