299 lines
15 KiB
Markdown
299 lines
15 KiB
Markdown
# Fork/Gather Reference Verification Implementation Plan
|
|
|
|
> **For agentic workers:** Use `subagent-driven-development` or
|
|
> `executing-plans` to implement this plan task-by-task. OpenCode should use
|
|
> one fresh implementer per task, sequentially, with separate spec and quality
|
|
> reviews before proceeding. Do not launch production implementation.
|
|
|
|
**Goal:** Close two reproduced reference-model defects and deliver executable
|
|
evidence for the next fork/gather design decision.
|
|
|
|
**Architecture:** Copy the archived reference into an isolated experimental
|
|
directory. Preserve the original evidence, repair occurrence tracking, and
|
|
exercise compiler/runtime agreement. This produces a verification prototype,
|
|
not a new production runtime or approval of the entire graph model.
|
|
|
|
**Tech Stack:** Repository Python 3.14, standard-library `unittest`, existing
|
|
Ruff tooling, Markdown lint. No new dependencies or lockfile changes.
|
|
|
|
**Spec:** [Draft fork/gather contract](../specs/2026-09-06-fork-gather-design.md).
|
|
Only its reference-verification gates are implemented here. Production owner
|
|
integration, step-budget dispatch, and merge-policy selection remain open.
|
|
|
|
## Global constraints
|
|
|
|
- Do not modify `src/`, production tests, public APIs, or dependencies.
|
|
- Do not modify `docs/historical/research/2026-09-06-fork-gather/imported/`.
|
|
- Do not choose strict precedence or final-port order as product policy.
|
|
- Do not add a transition journal, external-effect guarantees, or compatibility
|
|
for this throwaway prototype's old checkpoints.
|
|
- New writes get new occurrence identities; merges retain original identities.
|
|
- One gather firing per owner/gather/anchor visit; resolved rounds may repeat.
|
|
- Report analysis bounds as inability to prove, never acceptance.
|
|
- Work in an isolated worktree; no main-worktree edits, merge, push, or squash.
|
|
- Do not remove untracked files or reset somebody else's changes.
|
|
|
|
## Handoff preflight
|
|
|
|
The planning inputs may still be uncommitted in the primary workspace. A new
|
|
worktree does not inherit those files automatically. Before dispatching a
|
|
worker, copy the following planning inputs from the primary workspace into the
|
|
isolated worktree if they are absent or differ from the clean branch baseline:
|
|
|
|
- `CONTEXT.md`, `docs/README.md`, and `docs/current_roadmap.md`;
|
|
- `docs/adr/0006-explicit-fork-and-topology-driven-gather.md`;
|
|
- `docs/superpowers/specs/2026-09-06-fork-gather-design.md`;
|
|
- this plan;
|
|
- `docs/historical/research/2026-09-06-fork-gather/` in full.
|
|
|
|
Use read-only access to the primary workspace and copy, never move. Verify
|
|
SHA-256 equality before starting work. Do not overwrite unrelated dirty files
|
|
in the destination; stop on a conflict or if the primary source cannot be
|
|
identified. Commit transferred inputs separately on the isolated branch and
|
|
record the resulting task base. Do not substitute older docs from branch HEAD.
|
|
|
|
Record the worktree path, branch, initial commit, and initial dirty-file list.
|
|
Read root `AGENTS.md`, `docs/AGENTS.md`, the spec, and the archive README. The
|
|
archive README is enough to understand the prior findings; reading both long
|
|
reports is optional unless resolving a specific discrepancy.
|
|
|
|
## File ownership
|
|
|
|
Create `experiments/fork_gather/` with these files:
|
|
|
|
- `fork_gather_reference.py`: editable copy of the reference simulator/analyzer.
|
|
- `test_fork_gather_reference.py`: copy of the original 25 tests.
|
|
- `test_occurrences.py`: repeated writes, gather firings, recovery regressions.
|
|
- `test_agreement.py`: bounded schedules, inference agreement, merge evidence.
|
|
- `README.md`: commands, supported grammar, experimental status, limitations.
|
|
- `VERIFICATION.md`: actual commands/results, counterexamples, decision report.
|
|
|
|
The copied flat module is an explicitly disposable research artifact, not a
|
|
production package-design precedent. Avoid a gratuitous module split in this
|
|
verification wave; document non-obvious changes near their implementation.
|
|
|
|
## Task 1: Distinguish write executions from token identity
|
|
|
|
**Files:** Create the experimental directory, copy the two Python files above,
|
|
create `test_occurrences.py` and `README.md`. Edit only the experimental copies.
|
|
|
|
**Consumes:** Archived `Graph`, `Runtime`, `RuntimeState`, `_write`, `_atomic`,
|
|
`checkpoint`, and `recover` interfaces.
|
|
|
|
**Produces:** Existing public interfaces unchanged; persisted per-token
|
|
execution counters in `RuntimeState`. Write identity includes the node-execution
|
|
occurrence, not only the static node and token.
|
|
|
|
- [ ] Copy the two Python sources with `Copy-Item`, not move. Record SHA-256
|
|
hashes of the originals before starting. Run the copied 25-test baseline:
|
|
|
|
```powershell
|
|
Push-Location experiments/fork_gather
|
|
try { python -B -m unittest -v test_fork_gather_reference.py }
|
|
finally { Pop-Location }
|
|
```
|
|
|
|
- [ ] Add this graph and a regression that executes two writes, then ends:
|
|
|
|
```python
|
|
graph = Graph("w", {
|
|
"w": WriteNode("w", "X"),
|
|
"pick": ChoiceNode("pick", ("again", "done")),
|
|
"end": EndNode("end"),
|
|
}, (
|
|
Edge("w", "ok", "pick"),
|
|
Edge("pick", "again", "w"),
|
|
Edge("pick", "done", "end"),
|
|
))
|
|
rt = Runtime(graph, {})
|
|
rt.step_token("T0")
|
|
rt.step_token("T0", outcome="again")
|
|
rt.step_token("T0")
|
|
rt.step_token("T0", outcome="done")
|
|
rt.step_token("T0")
|
|
assert rt.state.committed_values == ["ROOT", "X", "X"]
|
|
assert len(rt.state.contributions) == 2
|
|
```
|
|
|
|
- [ ] Run `python -B -m unittest -v test_occurrences.py` from the experimental
|
|
directory. Confirm failure is `duplicate semantic contribution w@T0`.
|
|
- [ ] Add `execution_counts: dict[str, int]` with a default factory to
|
|
`RuntimeState`. Increment only inside the candidate-state transaction for a
|
|
valid node dispatch; use the token-local count in each fresh write ID:
|
|
|
|
```python
|
|
occurrence = s.execution_counts.get(token.id, 0) + 1
|
|
s.execution_counts[token.id] = occurrence
|
|
# _write reads this count after _step_token_impl admits the execution.
|
|
contribution_id = f"{node.id}@{token.id}:execution:{occurrence}:write:0"
|
|
```
|
|
|
|
The reference has one write per WriteNode execution. Document that limitation;
|
|
do not invent multi-write capabilities. Failed candidate transitions must
|
|
leave the published counter unchanged. Do not use a global scheduling counter
|
|
that changes contribution IDs when sibling execution order changes.
|
|
- [ ] Add checkpoint coverage after the first write and before the second.
|
|
Continue both original and recovered states through the same choices. Assert
|
|
equal contribution ID sets and two final X values. Keep shared-history
|
|
deduplication tests passing so fresh IDs are not minted during a merge.
|
|
- [ ] Run the baseline and occurrence suites. Document commands and the identity
|
|
rule in the experiment README. Commit only Task 1 files, then obtain separate
|
|
spec and quality reviews. Close concrete findings before Task 2.
|
|
|
|
## Task 2: Track fired gathers through unresolved activations
|
|
|
|
**Files:** Modify the experimental reference and `test_occurrences.py`.
|
|
|
|
**Consumes:** Existing `SActivation`, `SToken`, claim normalization/enclosure,
|
|
`SymbolicAnalyzer.analyze()`, and runtime gather transitions.
|
|
|
|
**Produces:** Same `AnalysisResult` interface, with a structured diagnostic
|
|
string prefix `repeated_gather:` for the forbidden repeated occurrence.
|
|
Runtime raises `RepeatedGatherError`, not incidental duplicate-lineage errors.
|
|
|
|
- [ ] Add the following fixture to `test_occurrences.py`:
|
|
|
|
```python
|
|
def repeated_gather_graph():
|
|
nodes = (
|
|
ForkNode("g", ("a", "b")),
|
|
GatherNode("h", ("only",)),
|
|
ChoiceNode("pick", ("again", "done")),
|
|
GatherNode("final", ("left", "right")), EndNode("end"),
|
|
)
|
|
edges = (
|
|
Edge("g", "a", "h", "only"),
|
|
Edge("g", "b", "final", "right"),
|
|
Edge("h", "ok", "pick"),
|
|
Edge("pick", "again", "h", "only"),
|
|
Edge("pick", "done", "final", "left"),
|
|
Edge("final", "ok", "end"),
|
|
)
|
|
return Graph("g", {n.id: n for n in nodes}, edges)
|
|
```
|
|
|
|
Assert analysis rejects with `repeated_gather:`. Independently supply runtime
|
|
anchors `{"h": "g", "final": "g"}` to exercise runtime defense despite
|
|
invalid authoring. Fire `h`, checkpoint, recover, choose `again`; assert
|
|
`RepeatedGatherError` and unchanged published state. It is acceptable to
|
|
reject on deposit before the second firing; test that explicit boundary.
|
|
- [ ] Confirm the rejection test fails against the Task 1 analyzer, which
|
|
incorrectly accepts. Do not make it pass by banning one-port gathers.
|
|
- [ ] Introduce immutable symbolic marking state:
|
|
|
|
```python
|
|
@dataclass(frozen=True)
|
|
class SMarking:
|
|
tokens: tuple[SToken, ...]
|
|
fired: frozenset[tuple[str, SActivation]] = frozenset()
|
|
```
|
|
|
|
Preserve the canonical token ordering from `_marking`. Queue and visited
|
|
membership must include `fired`. An inferred firing key is `(gather_id,
|
|
anchor_activation)`. If already present, record `repeated_gather:` and do not
|
|
explore that invalid transition. Otherwise insert it before continuation.
|
|
- [ ] Keep firing keys only while their anchor remains referenced by at least
|
|
one token in the resulting marking, including references through saved parent
|
|
claims. Add a helper returning symbolic activation objects, not merely static
|
|
fork IDs. This garbage collection lets fully resolved rounds reach the same
|
|
abstract state again. Test retention through partial claims and cleanup only
|
|
after complete discharge. Do not drop markers based on enclosure alone.
|
|
- [ ] Add runtime `fired_gathers: set[tuple[str, str]]` to `RuntimeState`, using
|
|
the existing single-owner `(gather_id, dynamic_anchor_id)` keys. Add
|
|
`RepeatedGatherError(RuntimeError)`. Check before deposit and firing mutation;
|
|
insert the marker within the successful candidate transition before routing
|
|
its continuation. Persist the set in reference checkpoints. Distinct dynamic
|
|
visits must remain distinct; this is not a serialized production format.
|
|
- [ ] Verify the completed-round loop remains accepted within a fixed bound
|
|
(100 markings for the supplied tiny graph). Execute two complete rounds in
|
|
the runtime and assert distinct visit and continuation IDs. Force a tiny
|
|
`max_markings` bound and assert rejection with `analysis_limit_exceeded:`.
|
|
- [ ] Run all copied and new tests. Explain the revised finite-state argument,
|
|
including token multiplicity and retained markers, without claiming general
|
|
workflow soundness. If the argument fails, report a counterexample and stop
|
|
that claim; do not waive it because the sample tests pass. Commit Task 2 and
|
|
obtain separate spec and quality reviews before Task 3.
|
|
|
|
## Task 3: Adversarial agreement and decision handoff
|
|
|
|
**Files:** Create `test_agreement.py` and `VERIFICATION.md`; update experiment
|
|
README and only evidence-backed reference gates in the live spec.
|
|
|
|
**Consumes:** Repaired occurrence tracking and existing graph fixtures,
|
|
`AnalysisResult.unique_anchor_plan()`, runtime transitions, and both merge
|
|
policies. **Produces:** Executable bounded agreement tests and a short report;
|
|
no selected production policy and no production implementation plan.
|
|
|
|
- [ ] For the supplied basic, direct, partial, cross, conditional, and ordering
|
|
graph fixtures, derive plans through the analyzer. Do not hardcode anchors
|
|
in happy-path tests. Execute accepted acyclic examples to completion under
|
|
all schedules within an explicit per-fixture bound, branching over ready
|
|
token/gather actions and declared choices. Fail the test if the bound is
|
|
exceeded rather than silently omitting paths. Keep loops in separate bounded
|
|
tests so this is not a termination test.
|
|
- [ ] Use semantic comparisons, not trace order or counts alone:
|
|
|
|
```python
|
|
semantic_result = (
|
|
tuple(rt.state.committed_values),
|
|
frozenset(rt.state.committed_contribution_ids),
|
|
rt.state.completed,
|
|
)
|
|
assert not rt.live_token_ids()
|
|
assert not rt.parked_token_ids()
|
|
assert not rt.state.gather_buckets
|
|
```
|
|
|
|
For choice fixtures compare schedules for the same outcome choices. Treat
|
|
deliberate strict-policy merge conflicts as expected results, not completion.
|
|
Report schedule counts and bounds by fixture.
|
|
- [ ] Exercise the two new occurrence regressions alongside simultaneous
|
|
duplicate ports, unresolved re-entry, and sibling-same-static-fork ambiguity.
|
|
Record conservative unsupported cases separately from invalid runtime state.
|
|
Add a missing-arrival/deadlock probe and report what the analyzer does; do
|
|
not relabel `accepted` as complete workflow soundness.
|
|
- [ ] Preserve the A/B opposite-history and three-history precedence-cycle
|
|
tests under both policies. Show the concrete final values or merge error.
|
|
Add a pure contribution-replay example with numeric addition to demonstrate
|
|
that deduplication is distinct from append ordering. This is evidence for
|
|
one more reducer, not proof of generic state-path merge semantics.
|
|
- [ ] For a ready-gather snapshot, resume and compare semantic results with
|
|
uninterrupted execution. For a failing strict-order transition, compare the
|
|
complete published dataclass state (not only `snapshot_dict`, which omits
|
|
fields) before/after; include occurrence counters and fired markers.
|
|
- [ ] Run `python -B -m unittest discover -v` inside the experimental directory.
|
|
Run Ruff check and format-check on the exact changed experimental Python
|
|
files. Document inherited diagnostics before fixing; keep formatting changes
|
|
confined to editable copies. Lint the exact changed Markdown files and run
|
|
`git diff --check`. Recheck archived hashes and forbidden-path diffs.
|
|
- [ ] Write `VERIFICATION.md` with the exact base/HEAD, commands, pass/fail
|
|
counts, explored-state/schedule counts, unsupported cases, and new findings.
|
|
Include a short user-facing choice: preserve previous merge orders and fail
|
|
on cycles, or let final-port order define the local merged view. Recommend
|
|
one with tradeoffs, but leave the spec's policy undecided.
|
|
- [ ] Update only closed spec gates. Leave ordering selection, owner integration,
|
|
and production-validator selection open. Once this plan's work is complete,
|
|
move it under `docs/historical/superpowers/plans/` and repair its relative
|
|
links and live references per `docs/AGENTS.md`. Commit Task 3 and obtain a
|
|
final whole-branch review. Stop without merging or pushing.
|
|
|
|
## Controller and review contract
|
|
|
|
The controller owns scope, baseline, integration, and verdict triage; it should
|
|
not implement tasks behind its reviewers. Use a fresh implementer per task and
|
|
separate spec/quality reviewers. Give each worker exact file ownership and the
|
|
preceding commit. Do not run concurrent writers against the same files.
|
|
|
|
Reviewers must execute the two regression cases and inspect occurrence state,
|
|
not merely repeat the implementer's test counts. Distinguish a demonstrated
|
|
bug, a conservative limitation, and a policy preference. Reproduce findings
|
|
before fixing; commission focused fix waves without expanding into production.
|
|
|
|
If subagents are unavailable, report that fact and request a workflow decision;
|
|
do not invent review verdicts. The model-coordination guide is optional context,
|
|
not a dependency on its ignored filesystem path or its model availability claims.
|
|
|
|
Final handoff: branch/worktree, commits, verification evidence, outstanding
|
|
findings, and the one merge-order policy choice in plain language. Do not label
|
|
fork/gather implemented or production-ready because this plan is complete.
|