Skip to content

Phase 0: harden completion semantics and terminal integrity - #48

Merged
SollanSystems merged 1 commit into
mainfrom
phase0/correctness-kernel
Jul 13, 2026
Merged

SollanSystems merged 1 commit into
mainfrom
phase0/correctness-kernel

Conversation

@SollanSystems

Copy link
Copy Markdown
Owner

Phase 0: harden completion semantics and terminal integrity

Summary

Establishes a single deterministic definition of success across the writer API,
runtime adapters, validator, schemas, templates, and normative documentation.

Succeeded now means what the public contract already says it means: every
declared acceptance criterion is proven true, evidence is present, and the run
is not flagged as false completion.

Terminal records become immutable, and the concurrent check-then-overwrite race
in loop.emit.terminate() is closed.

Why

The previous implementation allowed Succeeded when only one entry in
criteria_met was true — in three independent places (loop/emit.py,
loop/integrations.py, and the doctor's G1 check in loop/contract.py). A
terminal like this passed both write-time and validation gates:

{
  "state": "Succeeded",
  "criteria_met": {
    "tests_pass": true,
    "security_review": false,
    "deployment_verified": false
  }
}

That contradicted the normative contract's success model
(reference/repo-os-contract.md prose already declared iteration_id | int
and terminal_state.json "written exactly once" with no force clause) and
created a direct false-completion path.

force=True also meant a terminal record was not actually an immutable audit
decision, and the separate existence-check/replace operations let concurrent
writers race (TOCTOU).

Changes

Shared completion policy

  • New loop/completion.py: normalize_completion_policy,
    criteria_satisfy_completion, unmet_required_criteria.
  • First explicit policy: {"mode": "all_required"}. Nonempty criteria map,
    exact boolean true for every entry (truthy 1 does not count).
  • Legacy terminal@1 records without the field are read as all_required.
  • Unsupported modes and undeclared policy fields are rejected.
  • One evaluator, three call sites: emit.terminate,
    integrations.to_terminal_state, and contract G1 (both validation modes) —
    the write path, projection path, and read/validate path can no longer drift.

Writer hardening (loop/emit.py)

  • Refuses partial, empty, evidence-free, or false-completion success claims.
  • Rejects blank or duplicate evidence entries.
  • Rejects malformed criteria and noncanonical iteration ids; iteration ids are
    stored as canonical non-negative integers.
  • Terminal creation is atomic and create-once via os.link (fsync'd temp file
    • hard-link claim) — two simultaneous terminators produce exactly one
      terminal decision; the loser gets a clean EmitError.
  • Legacy force=True calls now always raise with an actionable message; the
    original record is never replaced.

Runtime-neutral projection hardening (loop/integrations.py)

  • Same completion-policy evaluator; green gate with incomplete criteria →
    FailedUnverifiable; unsupported/malformed completion spec →
    FailedSpecGap; blank/duplicate evidence → FailedUnverifiable.
  • Existing safety → human → blocked → budget → spec-gap → gate precedence is
    preserved.

Contract and schema updates

  • All-required success checks run in both structural and JSON Schema
    validation modes.
  • completion_policy added to terminal@1 as an additive optional field
    (records without it still validate — conformance rule D2 holds).
  • Tightened criteria key shape, evidence non-blank/uniqueness, and terminal
    iteration ids. These constraints encode what the normative spec prose
    already required; the schemas had been deliberately loosened below the spec
    and are now realigned with it.
  • New state@1 writers emit canonical integers; canonical decimal strings
    ("0", "7") remain read-compatible for legacy records.
  • templates/state.json.tmpl renders iteration_id unquoted.
  • reference/repo-os-contract.md §8 field table + example + §14 B2 updated to
    the all-required wording; README force/writer sentences updated.

Architecture decision

  • ADR 0001 (docs/adr/0001-proof-kernel-and-runtime.md): separate the
    portable proof kernel from the first-party execution runtime. Governing
    rule: agents propose; the kernel disposes. Next persistence milestone:
    SQLite/WAL-backed immutable EventStore.

Provenance and verification

The core migration was authored externally (GPT-5.5 deep-review lane) against
f2e9347 and applied here after independent verification:

  • Premise check: the any-true bug confirmed at loop/emit.py:221,
    loop/integrations.py:119, loop/contract.py:222; docs/spec confirmed to
    say "all"/"every"/"written exactly once".
  • Bundle security review: no network/exec/eval surface; hard-coded target
    paths; manifest hashes verified 14/14.
  • Applied via the bundle's own fail-closed staged transforms for code/schemas;
    reference/repo-os-contract.md and README.md were hand-edited (the
    bundle's doc anchors assumed a non-table format).
  • One deviation: the G1 doctor message names criteria_met
    (pre-existing scripts/test_loop_contract_core.py pins the field name).
  • os.link semantics smoke-tested on WSL2/DrvFS (create + FileExistsError
    on second link both correct).

An independent adversarial review of the applied diff then found five issues
(1 HIGH, 2 MEDIUM, 2 LOW), all fixed here with pinning tests:

  • R-001 (HIGH) — removing force=True eliminated the only recovery path
    for the pre-existing split-write window between terminal_state.json and
    state.json, and scripts/runtime_monitor.py (which read only
    state.json) recommended replan for an already-terminated loop. Fixed
    three ways: new narrow repair op emit.sync_state_to_terminal() (stamps
    state.json from an existing terminal record, never touches the terminal
    file); runtime_monitor._terminal_disposition now treats an existing
    terminal_state.json as authoritative; and a failed post-link state write
    raises EmitError naming the repair op instead of a raw OSError.
  • R-002 (MEDIUM) — explicit "completion_policy": null was doctor-clean
    in structural-fallback mode but a schema violation in jsonschema mode;
    terminal@1 now types the field ["object", "null"] and a test pins
    cross-mode agreement.
  • R-003 (MEDIUM) — non-FileExistsError OSErrors from the os.link
    claim (filesystems without hard-link support) now raise EmitError like
    every other refusal path.
  • R-004 (LOW)loop/completion.py criteria hints narrowed to
    Mapping[str, object] (the invariant every call site enforces).
  • R-005 (LOW) — reference-doc compat callout: pre-migration Succeeded
    records with mixed criteria now fail doctor and need re-verification.

Gates (all green, after review fixes):

Gate Result Prior baseline
Focused suite (completion/emit/integrations) 51 passed
Full suite (jsonschema+langgraph+temporalio) 455 passed / 9 skipped 433 / 9
Structural fallback (pyyaml-only) 438 passed / 24 skipped 417 / 23
validate_frontmatter / self_eval 9/9 · 13/13 clean
py_compile loop/*.py scripts/*.py + schema JSON parse OK

Test coverage strictly grows (17→21 emit tests, 14→18 integration tests, +6
policy tests); no existing assertion weakened — every changed assertion tracks
an intentional semantics change (string→int iteration id, force-overwrite→
force-refusal).

Compatibility

Additive for valid historical records: missing completion_policy means
all_required; canonical legacy state id strings remain readable; new writers
emit the stricter canonical forms. Behavior intentionally changes for
dishonest or ambiguous records: partial success, terminal overwrite, malformed
evidence, malformed criteria, and noncanonical ids now fail closed.

Follow-up

  • EventStore + SQLite/WAL so terminal creation, state reduction, receipts,
    and runlog projections derive from one transactional immutable event stream
    (removes the remaining split-write boundary between terminal_state.json
    and state.json; sync_state_to_terminal is the interim repair).
  • Consider a doctor warning for the desynced window (terminal record present,
    state.json unstamped) so the crash residue is surfaced, not just tolerated.

…anonical iteration ids

Succeeded now requires EVERY declared criterion true under an explicit
completion_policy ({"mode": "all_required"}, the compatibility default for
legacy records), enforced by one shared evaluator (loop/completion.py) across
emit.terminate, integrations.to_terminal_state, and the contract doctor G1
check in both validation modes. Previously all three independently accepted
any single true criterion — a direct false-completion path contradicting the
normative spec.

terminal_state.json is now immutable: atomic create-once via a hard-link
claim (two concurrent terminators produce exactly one record), force=True
always raises, and the new emit.sync_state_to_terminal() is the narrow
repair for the terminal/state split-write window (runtime_monitor now also
treats an existing terminal record as authoritative). Iteration ids are
canonical non-negative integers (legacy decimal strings stay read-compatible
in state@1); terminal@1 gains additive completion_policy and encodes the
spec's existing evidence/criteria constraints.

Provenance: core migration authored externally (GPT-5.5 lane) against
f2e9347, applied after independent verification (premise check, security
review, manifest hashes), then hardened per an adversarial review (5
findings fixed: split-write recovery, cross-mode null policy agreement,
os.link OSError wrapping, hint narrowing, compat callout).

Full suite 455 passed / 9 skipped (was 433/9); pyyaml-only fallback 438/24
(was 417/23); self_eval 13/13; frontmatter 9/9.
Copilot AI review requested due to automatic review settings July 13, 2026 14:22
@SollanSystems
SollanSystems merged commit 03c6673 into main Jul 13, 2026
11 checks passed
@SollanSystems
SollanSystems deleted the phase0/correctness-kernel branch July 13, 2026 14:23

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c48f775311

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread loop/integrations.py
"evidence": list(outcome.artifacts),
"criteria_met": {key: value is True for key, value in canonical_criteria.items()},
"completion_policy": normalized_policy,
"evidence": list(artifacts),

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Validate evidence before returning failure bodies

When a higher-precedence failure is returned first (for example external_error, human_abort, or FailedSafety) and outcome.artifacts contains a blank entry or duplicates, this helper still copies those raw artifacts into evidence and never reaches the later evidence_error branch. Since emit.terminate now rejects blank/duplicate evidence for every terminal state, the adapter can produce a FailedBlocked/FailedSafety body that cannot be persisted instead of a valid failure record.

Useful? React with 👍 / 👎.

terminal = state.get("terminal_state")
if terminal:
return terminal
terminal_path = paths.loop_dir / "terminal_state.json"

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Use the resolved terminal path for orphan records

When terminal_state.json is in the root-level legacy location that resolve_loop_paths already supports, and state.json was never stamped, this hard-coded .loop path ignores the resolved paths.terminal. In that context the monitor falls through to stall/budget detection and can recommend replan or continue for an already terminal loop, so the new orphan-terminal handling should read the resolver-selected path.

Useful? React with 👍 / 👎.

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR hardens “Succeeded” semantics and terminal-record integrity by centralizing completion-policy evaluation, enforcing all-required criteria for success across writer/projection/validation paths, and making terminal records immutable and concurrency-safe.

Changes:

  • Introduces a shared completion-policy module and applies it consistently in emit, integrations, and contract validation.
  • Makes terminal writes create-once/immutable (closing overwrite and concurrency race paths) and adds a narrow state-stamp repair helper.
  • Updates schemas, templates, docs, and tests to reflect canonical integer iteration IDs and all-required success semantics.

Reviewed changes

Copilot reviewed 15 out of 15 changed files in this pull request and generated 3 comments.

Show a summary per file
File Description
templates/state.json.tmpl Emit iteration_id as an unquoted value to support canonical integer IDs.
scripts/test_runtime_monitor.py Adds regression coverage for “terminal exists but state.json not stamped” monitoring behavior.
scripts/test_integrations.py Expands projection tests to pin all-required completion, policy failures, and evidence validation.
scripts/test_emit.py Expands writer tests for stricter success semantics, immutability, concurrency, and repair path.
scripts/test_completion_policy.py New tests pinning shared policy semantics and cross-validation-mode agreement.
scripts/runtime_monitor.py Treats terminal_state.json as authoritative even when state.json lacks terminal_state.
schemas/terminal.schema.json Adds completion_policy, tightens evidence/criteria shapes, and documents legacy interpretation.
schemas/state.schema.json Tightens iteration_id to non-negative int or canonical decimal string for legacy compatibility.
reference/repo-os-contract.md Updates normative contract to specify all-required completion via completion_policy.
README.md Updates user-facing contract description to reflect immutable terminal records and stricter success rules.
loop/integrations.py Uses shared policy evaluator; fails closed on partial/malformed criteria and invalid evidence/policy.
loop/emit.py Enforces stricter success rules; implements atomic create-once terminal writes and adds sync repair helper.
loop/contract.py Applies shared completion semantics in both validation modes; tightens structural checks.
loop/completion.py New shared, deterministic completion-policy implementation (default all_required).
docs/adr/0001-proof-kernel-and-runtime.md Adds ADR formalizing kernel-vs-runtime split and immutability/policy rules.
Comments suppressed due to low confidence (1)

loop/emit.py:88

  • _atomic_write_text() tries to delete the temp file but only ignores FileNotFoundError. If unlink fails for any other reason (e.g., permission/transient Windows file-lock), that exception will mask the original failure and/or change the error surfaced to callers.
    except BaseException:
        try:
            os.unlink(tmp_name)
        except FileNotFoundError:
            pass

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread loop/completion.py
Comment on lines +71 to +73
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))
Comment thread loop/emit.py
Comment on lines +106 to +110
finally:
try:
os.unlink(tmp_name)
except FileNotFoundError:
pass
Comment on lines +181 to +183
if isinstance(record, dict) and record.get("state"):
return str(record["state"])
return "terminal"
SollanSystems added a commit that referenced this pull request Jul 17, 2026
…en .loop/events.db exists (#77)

loop doctor now incorporates event-store consistency (ADR 0001 consequence #4,
PR #48 follow-up): doctor_report composes validate_contract with a new appended
loop/runtime.py event_consistency_issues() that calls the status/replay verbs
unchanged as black boxes. Absent store stays byte-stable plus one additive
event_store report key; unreadable stores (corrupt_store / empty_store /
ambiguous_run_id) become typed doctor failures, never skips; ok only narrows
True->False, issues only append. reference/repo-os-contract.md gains section 22
and the corrected section-16 scope boundary. 11 new tests (933/16 extras,
864/85 pyyaml-only, exact).
SollanSystems added a commit that referenced this pull request Jul 17, 2026
Version 0.8.0 -> 0.9.0 across pyproject.toml, plugin.json, README
(badge, action example, schema list 4 -> 10, event-sourced runtime
bullet, Status), CHANGELOG 0.9.0 entry covering #41-#48 and #59-#77,
and the version-pin test.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants