Skip to content

mutation-trace protocol - #238

Open
davidabram wants to merge 11 commits into
mainfrom
mutation-cursor
Open

mutation-trace protocol#238
davidabram wants to merge 11 commits into
mainfrom
mutation-cursor

Conversation

@davidabram

@davidabram davidabram commented Aug 26, 2026

Copy link
Copy Markdown
Member

No description provided.

@vercel

vercel Bot commented Aug 26, 2026 •
edited
Loading

Copy link
Copy Markdown

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated (UTC)
sce-config-json Ready Ready Preview Aug 26, 2026 2:55pm

Request Review

@davidabram @shared-context-engineering
runtime+context: Add mutation-trace protocol domain types
9a0232d 
Establish the pure, dependency-free Rust domain layer that refines the verified mutation-cursor protocol. Register the new module with opaque identity types, boundary accessors, focused tests, and context documentation while leaving transition logic and production I/O integration for later plan tasks.

Plan: mutation-cursor-protocol-kernel (T01)

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Resolve hook boundaries by scope identity
79a7e42 
Prevent callers from pairing a hook boundary with unrelated scope state by resolving its worktree through the boundary's ScopeId in a scope map. Update regression tests and protocol documentation to capture the keyed lookup and correction.

Plan: mutation-cursor-protocol-kernel T01

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
runtime: Implement mutation trace protocol transitions
3655dc2 
Add the pure mutation-trace protocol kernel's aggregate state and prepare/commit evaluation for Start, Advance, Close, and Flush boundaries, including CAS freshness, replay, taint guards, scope lifecycle, cursor/revision, and attempt state transitions. Update the mutation-trace plan and repository context to record T02 completion and the explicit observation-input design. This keeps the kernel dependency-free while leaving attribution, event materialization, and recovery for follow-up tasks.

Plan: mutation-cursor-protocol-kernel (T02)

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Implement attribution and mutation-event materialization
c7d4d60 
Refine the verified mutation-cursor protocol with pre-transition live-scope attribution and emit one MutationEvent for each accepted real tree change. Preserve Start and Close lifecycle semantics by evaluating evidence against the pre-transition state.

Plan: mutation-cursor-protocol-kernel, task T03

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Fix stale module docs after T03
8f61b1d 
mod.rs and protocol.rs's module-level rustdoc still described
attribution derivation and mutation-event materialization as not yet
implemented, and protocol.rs's refinement list omitted liveScopesOn/
attributionFor/mkMutationEvent. Update both to describe the current
module state; only taint/database-failure/abandon/recovery remain
unimplemented. Documentation only, no behavior change.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W5m3Y3Jr9eW4iof3urzeMB

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Implement snapshot and database failure taint actions
0e3ef91 
Model snapshot and database failures as guarded pure protocol transitions,
advancing snapshot-failure revisions and recording external taint without
changing unrelated worktree, scope, or mutation state.

Plan: mutation-cursor-protocol-kernel (T04)

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Fix database_failure unknown-worktree refinement gap
0786d26 
Quint's WorktreeId ranges over the finite WORKTREES universe, and init
materializes a WorktreeState for every member, so recordDatabaseFailure has
no explicit worktree-existence guard because every WorktreeId already
resolves there. That omission described a fact about Quint's closed domain,
not license for the same gap in the unbounded Rust refinement.

database_failure previously had no existence guard, so an unknown
WorktreeId could be inserted into external_taint with no corresponding
ProtocolState.worktrees entry -- a state Quint cannot represent. Add the
same worktrees.contains_key guard taint already had, keeping
external_taint subset-of ProtocolState.worktrees an invariant of every
state this module can produce.

Add unknown-worktree no-op tests for both taint and database_failure.
Document the runtime worktree materialization contract (mirroring the
existing runtime scope materialization section) in the domain context
file, correct the plan's T04 result text, note the same existence
precondition on T05/T06's abandon/recover, and fix mod.rs's stale
"not yet implemented" doc comment for taint/database-failure.

No production call site references this module; spec/mutation_cursor.qnt
and spec/mutation_cursor.md are untouched.

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Implement scope abandonment transition
ac2bc92 
Add the pure `abandon` transition that refines the verified mutation-cursor protocol for live scopes, preserving scope identity and cursor state while marking the owning worktree for rebaseline. Guard terminal, externally tainted, unknown, and unmaterialized states as no-ops, with focused Rust coverage.

Document the implemented protocol slice and cite the completed mutation-cursor-protocol-kernel plan task T05.

Co-authored-by: SCE <sce@crocoder.dev>
davidabram and others added 2 commits August 26, 2026 16:11
@davidabram @shared-context-engineering
mutation-trace: Implement recovery with observed-tree rebaselining
a10300d 
Add the pure recovery transition to complete the mutation-trace protocol action set. Rebaseline the cursor from an explicit observed tree, clear failure state and external taint, and abandon live scopes after taint recovery while preserving scopes for needs-rebaseline-only recovery.

Add focused recovery tests and synchronize the protocol context and plan records. Plan: mutation-cursor-protocol-kernel (T06)

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Add cross-action protocol coverage and refinement matrix
f4d110d 
Complete the mutation-cursor protocol kernel's remaining T07 coverage so the pure transition module is tested across real multi-action sequences, not only isolated states.

Add cross-action and invariant-focused tests for attribution, taint and recovery, scope terminality, CAS rejection, replay, and mutation evidence. Document the Quint-to-Rust refinement matrix and distinguish verification instrumentation from production-semantic guarantees. Keep the module dependency-free and unwired to hooks, commands, or database call sites.

Plan: mutation-cursor-protocol-kernel (T07)

Co-authored-by: SCE <sce@crocoder.dev>
@davidabram @shared-context-engineering
mutation-trace: Fix T07 refinement-matrix misclassifications and guar…
33cc2aa 
…d revision overflow

PR review of T07 found three defects in the module's refinement matrix and one
unbounded-integer refinement gap:

- `AbandonCreatesRebaselineRequirement`, `MutationEventsMatchCursorHistory`, and
  `MutationEventsCrossOnlyTrustworthyProtocolStates` were classified
  verification-only because Quint states them via history/checkpoint variables,
  conflating the proof mechanism (verification-only) with the property it
  proves (production-semantic). Moved into the semantic-properties table, with
  a new regression test,
  `needs_rebaseline_suppresses_mutation_event_even_when_commit_observes_a_real_tree_change`,
  backing the third (no existing test drove `commit` through
  `accepted && observes && observed_change` against a `needs_rebaseline`
  worktree to prove `changed` still comes out false).
- `AiExclusiveRequiresExactlyOneActiveScope` was classified "enforced by Rust
  type", which is false: `Attribution::AiExclusive(ScopeId)` does not itself
  make an inconsistent scope count unrepresentable. Corrected to "implemented
  directly + preserved by transition tests", backed by `attribution_for`'s own
  `live.len() == 1` branch.
- Every revision-advancing action (`commit`, `taint`, `abandon`, `recover`)
  used a raw `worktree_state.revision + 1`, assuming a Rust `u64` can always
  refine Quint's unbounded `revision: int`. At `revision == u64::MAX` this
  would wrap to 0 in release mode.

Added a private `next_revision(revision: u64) -> Option<u64>` helper
(`checked_add(1)`) in `protocol.rs` and routed all four actions through it.
`commit`'s `accepted` gate folds in the headroom check unconditionally, before
`apply` touches any state, so an overflowing attempt is rejected exactly like a
stale one (no cursor movement, scope transition, processed-EventKey insertion,
or MutationEvent); `taint`/`abandon`/`recover` treat it as an additional
guarded no-op. Four new tests
(`commit_does_not_wrap_revision_at_u64_max`,
`taint_does_not_wrap_revision_at_u64_max`,
`abandon_does_not_wrap_revision_at_u64_max`,
`recover_does_not_wrap_revision_at_u64_max`) each start from
`revision: u64::MAX` and prove a no-op/rejection rather than a wrap.

Documented the refinement in a new `context/cli/mutation-trace-revision-refinement.md`
domain file, linked from `context/cli/mutation-trace-protocol.md` and
`context/context-map.md`.

74/74 mutation_trace tests pass (69 + 5 new); clippy and fmt clean;
spec/mutation_cursor.qnt is untouched and its own typecheck/test still pass.
No behavior changes to any previously-accepted transition.

mutation-cursor-protocol-kernel plan, T07 post-review correction.

Co-authored-by: SCE <sce@crocoder.dev>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@davidabram