# Adversarial Audit of the Proposed Fork/Gather Model

## 1. Verdict

The previous proposal is **salvageable, but not correct as written**.

The strongest parts survive:

* linear token replacement is coherent;
* partial claims are useful;
* gather ports can remain local and need not serialize an originating fork;
* a lineage tree can remain the physical state-view structure;
* deterministic reducer order can be independent of scheduling;
* completed fork/gather rounds can safely loop and execute again.

Four parts need correction.

| Area               | Previous proposal                                                     | Audit result                                                                                                                |
| ------------------ | --------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------- |
| Direct fork→gather | `split()` created a child frame at the edge destination               | **Broken.** `target_port` disappears if the destination is a gather.                                                        |
| Correlation        | search all fork visits appearing anywhere in a token's claim ancestry | **Too permissive.** “Referenced by some component” is not the same as “encloses the whole token.”                           |
| Shared writes      | LCA replay; stable write IDs suggested for hard cases                 | **LCA alone demonstrably duplicates writes.** Stable contribution IDs work on the adversarial graph tested.                 |
| Checkpoint         | semantic mutations described, but no atomicity protocol               | **Not crash-safe as pseudocoded.** A crash during gather firing can leave a ready bucket whose inputs are already consumed. |

The most important conceptual correction is this:

> A control claim needs two different ancestry queries: **referenced fork visits** and **enclosing fork visits**. Re-entry safety uses the former. Gather correlation uses the latter.

That distinction was missing.

---

# 2. The adversarial graph

I used the smallest graph I found that simultaneously exercises:

1. a shared pre-fork state write,
2. direct `ForkNode -> GatherNode.port` edges,
3. cross-gathers,
4. reconvergence of the cross-gather results,
5. an order-sensitive reducer,
6. and a checkpoint while a gather is ready.

Graph:

```text
Fork r(branches = main, c, d)

r ==main==> s
r ==c=====> c
r ==d=====> d

s writes append("S")
s --ok--> Fork k(branches = x, y)

k ==x==> hx.left          # DIRECT fork -> gather edge
k ==y==> hy.left          # DIRECT fork -> gather edge

c writes append("C")
c --ok--> hx.right

d writes append("D")
d --ok--> hy.right

hx --ok--> final.left
hy --ok--> final.right

final --ok--> END
```

`==branch==>` means simultaneous fork emission. `--ok-->` means ordinary exclusive routing.

The initial committed state is:

```text
log = ["ROOT"]
```

Fresh raw state contributions are:

```text
S#1 = append("S")
C#1 = append("C")
D#1 = append("D")
```

Gather port order is always:

```text
(left, right)
```

The compiled correlation plan used by the simulation was:

```text
hx.anchor    = r
hy.anchor    = r
final.anchor = r
```

That last fact is important: **the simulation demonstrates runtime matching given this compiled plan. It does not, by itself, prove that the compiler can infer the plan for arbitrary graphs.**

---

# 3. First break: direct fork → gather was not executable

My previous pseudocode had effectively:

```python
def split(...):
    ...
    for branch in fork.branches:
        edge = branch_edge(branch)
        child_token = new_token(...)
        new_frame(
            node_id=edge.to,
            token_id=child_token.id,
        )
```

That is wrong when:

```text
k ==x==> hx.left
```

because the child frame remembers only:

```text
node_id = "hx"
token_id = ...
```

The critical:

```text
target_port = "left"
```

has been discarded.

Ordinary routing did special-case gather edges, but fork routing did not. Therefore the previous transition system could not execute the graph above without inventing another rule.

### Required correction

There should be exactly one primitive for traversing an edge:

```python
def emit_along_edge(token: ControlToken, edge: Edge) -> None:
    target = index.node(edge.to)

    if isinstance(target, GatherNode):
        if edge.target_port is None:
            raise InvalidGraph("gather edge requires target_port")

        deposit_gather_arrival(
            token=token,
            gather=target,
            port=edge.target_port,
        )
        return

    if isinstance(target, EndNode):
        attempt_owner_completion(token, target)
        return

    frame = make_frame(
        node_id=edge.to,
        token_id=token.id,
        owner_id=token.owner_id,
    )
    enqueue(frame)
```

Then fork is:

```python
for branch in fork.branches:
    edge = index.fork_branch_edge(fork.id, branch)
    child = create_branch_token(...)
    emit_along_edge(child, edge)
```

This means a direct fork→gather branch creates a token and immediately parks it in the gather bucket. It does **not** create a meaningless gather execution frame that has forgotten its port.

A gather execution frame, if you want one for tracing and step-budget accounting, should be created only when its bucket becomes ready.

---

# 4. Second break: “ancestor” was the wrong correlation relation

My previous runtime helper effectively computed:

```python
visit_ancestors(token.claim)
```

as the **union** of all fork visits referenced by any obligation in the token's claim.

That works on simple branch tokens. It becomes wrong immediately after a cross-gather.

After `hx`, the continuation claim is:

```text
{k#0.x, r#0.c}
```

The previous union-style ancestry calculation gives:

```text
{k#0, r#0}
```

because one part descended from `k`, and both ultimately descended from `r`.

But `k#0` does **not** enclose the whole control resource represented by this token. It encloses only the `k.x` component. The `r.c` component is outside `k`.

In the executed simulator:

```text
hx claim:
    {k#0.x, r#0.c}

union/referenced visits:
    {k#0, r#0}

common enclosing visits:
    {r#0}
```

and likewise:

```text
hy claim:
    {k#0.y, r#0.d}

referenced visits:
    {k#0, r#0}

enclosing visits:
    {r#0}
```

This distinction resolves an ambiguity that was already latent in the previous cross-gather example.

## Referenced visits

These answer:

> Does any currently outstanding component depend on this unresolved fork visit?

They are useful for recursive-reentry detection.

```python
def referenced_visits(claim) -> set[ForkVisitId]:
    result = set()

    for obligation in claim:
        if isinstance(obligation, BranchObligation):
            visit = visits[obligation.fork_visit_id]
            result.add(visit.id)
            result |= referenced_visits(visit.parent_claim)

    return result
```

For:

```text
{k.x, r.c}
```

this returns:

```text
{k, r}
```

## Enclosing visits

These answer the stronger question:

> Which unresolved fork visits enclose the **entire resource** represented by this claim?

For one branch obligation:

```python
def enclosing_visits_of_obligation(ob):
    if isinstance(ob, OwnerRoot):
        return set()

    visit = visits[ob.fork_visit_id]

    return {
        visit.id,
        *enclosing_visits(visit.parent_claim),
    }
```

For a multi-obligation claim, take the intersection:

```python
def enclosing_visits(claim):
    if not claim:
        return set()

    return intersection(
        enclosing_visits_of_obligation(ob)
        for ob in claim
    )
```

Thus:

```text
enclosers(k.x) = {k, r}
enclosers(r.c) = {r}

enclosers({k.x, r.c})
    = {k,r} ∩ {r}
    = {r}
```

### Revised gather correlation

A compiled gather anchor must be resolved against **enclosing visits**, not all referenced visits:

```python
def resolve_anchor_visit(token, plan):
    candidates = {
        visit_id
        for visit_id in enclosing_visits(token.claim)
        if visits[visit_id].fork_node_id == plan.anchor_fork_node_id
    }

    if len(candidates) != 1:
        raise CorrelationInvariantError(...)

    return only(candidates)
```

This is materially stricter.

### Revised re-entry check

Re-entry uses the opposite relation:

```python
def check_fork_reentry(token, fork):
    for visit_id in referenced_visits(token.claim):
        if visits[visit_id].fork_node_id == fork.id:
            raise UnresolvedForkReentry(...)
```

If the token contains:

```text
{old_g.left, unrelated_branch}
```

then `g` may not be a common encloser, but part of the token still owns an unresolved `g` obligation. Re-entering `g` should therefore remain illegal.

That means the two functions must not be collapsed.

---

# 5. Executed schedule 1, including checkpoint/resume

This was executed in a small Python reference simulator in this session. It is **not** an execution of the production repository.

Notation:

```text
L = live
P = parked at gather
Δ[...] = ordered raw contribution IDs visible after L0
R = OwnerRoot(O)
```

Fork visit IDs in the simulation were deterministically derived from the consumed token, hence names such as:

```text
r@T0
k@T1
```

That deterministic representation is an implementation suggestion, not required by the abstract semantics.

| Transition            | Every live/parked token                                                                  | Pending gathers                                 | Unresolved fork visits | Committed      |
| --------------------- | ---------------------------------------------------------------------------------------- | ----------------------------------------------- | ---------------------- | -------------- |
| 0 start               | `T0 L@r {R} Δ[]`                                                                         | —                                               | —                      | `[ROOT]`       |
| 1 `r` splits          | `T1 L@s {r.main} Δ[]`; `T2 L@c {r.c} Δ[]`; `T3 L@d {r.d} Δ[]`                            | —                                               | `r`                    | `[ROOT]`       |
| 2 `s` writes S        | `T1 L@k {r.main} Δ[S#1]`; T2, T3 unchanged                                               | —                                               | `r`                    | `[ROOT]`       |
| 3 `k` splits          | `T2 L@c {r.c}`; `T3 L@d {r.d}`; `T4 P@hx.left {k.x} Δ[S#1]`; `T5 P@hy.left {k.y} Δ[S#1]` | `hx{left=T4}`; `hy{left=T5}`                    | `r,k`                  | `[ROOT]`       |
| 4 c writes C          | `T2 P@hx.right {r.c} Δ[C#1]`; `T3 L@d`; T4/T5 parked                                     | `hx{left=T4,right=T2}=READY`; `hy{left=T5}`     | `r,k`                  | `[ROOT]`       |
| 5 checkpoint + reload | **identical to transition 4**                                                            | identical                                       | identical              | `[ROOT]`       |
| 6 fire hx             | `T3 L@d {r.d}`; `T5 P@hy.left {k.y} Δ[S#1]`; `THX P@final.left {k.x,r.c} Δ[S#1,C#1]`     | `hy{left=T5}`; `final{left=THX}`                | `r,k`                  | `[ROOT]`       |
| 7 d writes D          | `T3 P@hy.right {r.d} Δ[D#1]`; T5; THX                                                    | `hy{left=T5,right=T3}=READY`; `final{left=THX}` | `r,k`                  | `[ROOT]`       |
| 8 fire hy             | `THX P@final.left {k.x,r.c} Δ[S#1,C#1]`; `THY P@final.right {k.y,r.d} Δ[S#1,D#1]`        | `final{left=THX,right=THY}=READY`               | `r,k`                  | `[ROOT]`       |
| 9 fire final          | `TF L@END {R} Δ[S#1,C#1,D#1]`                                                            | —                                               | —                      | `[ROOT]`       |
| 10 END commit         | —                                                                                        | —                                               | —                      | `[ROOT,S,C,D]` |

The control normalization at transition 9 is:

```text
{k.x, r.c} + {k.y, r.d}

= {k.x, k.y, r.c, r.d}

k.x + k.y
    -> k.parent_claim
    -> {r.main}

therefore:

{r.main, r.c, r.d}
    -> r.parent_claim
    -> {R}
```

No parent branch obligation is simultaneously live while its refinement is live. `r.main` is restored only when both `k` branches are consumed.

The checkpoint after transition 4 reconstructed:

```text
T2 parked in hx.right
T4 parked in hx.left
T5 parked in hy.left
T3 live at d
hx READY
hy collecting
r and k open
S#1 and C#1 pending
committed state = [ROOT]
```

Resume created no new fork visit, no new arrival, and no repeated contribution.

That clean semantic checkpoint passed.

---

# 6. Executed schedule 2

I then changed both branch scheduling and gather firing order.

Execution:

```text
r split
d first
c second
main/S third
k split last

=> hx and hy become READY together

fire hy before hx
fire hx second
fire final
```

State trace:

| Transition | Live/parked control state                                  | Gather state                   | Committed      |
| ---------- | ---------------------------------------------------------- | ------------------------------ | -------------- |
| 0          | `T0 {R}`                                                   | —                              | `[ROOT]`       |
| 1 `r`      | `T1 {r.main}`, `T2 {r.c}`, `T3 {r.d}`                      | —                              | `[ROOT]`       |
| 2 d        | `T3 P@hy.right Δ[D#1]`; T1/T2 live                         | `hy{right=T3}`                 | `[ROOT]`       |
| 3 c        | `T2 P@hx.right Δ[C#1]`; T3 parked; T1 live                 | `hx{right=T2}`, `hy{right=T3}` | `[ROOT]`       |
| 4 S        | `T1 L@k Δ[S#1]`; T2/T3 parked                              | unchanged                      | `[ROOT]`       |
| 5 `k`      | `T4 P@hx.left Δ[S#1]`; `T5 P@hy.left Δ[S#1]`; T2/T3 parked | **hx and hy READY**            | `[ROOT]`       |
| 6 fire hy  | `THY P@final.right {k.y,r.d} Δ[S#1,D#1]`; hx inputs parked | `hx READY`; `final{right=THY}` | `[ROOT]`       |
| 7 fire hx  | `THX P@final.left Δ[S#1,C#1]`; THY parked                  | `final READY`                  | `[ROOT]`       |
| 8 final    | `TF L@END {R} Δ[S#1,C#1,D#1]`                              | —                              | `[ROOT]`       |
| 9 END      | —                                                          | —                              | `[ROOT,S,C,D]` |

The two schedules therefore produced exactly the same semantic result:

```text
normalized control claim = {R}

pending reducer sequence =
    [S#1, C#1, D#1]

final state =
    ["ROOT", "S", "C", "D"]
```

The fact that `hy` fired first did not move `D` before `C`, because arrival/firing order does not define reducer order. `final` has:

```text
ports = (left, right)

left  = hx = [S#1, C#1]
right = hy = [S#1, D#1]
```

and merge order follows that declaration.

---

# 7. Shared-write deduplication: LCA alone definitely fails

I also executed the same graph with contribution deduplication disabled at the final gather.

Result:

```text
hx delta = [S, C]
hy delta = [S, D]

LCA = L0

naive final replay =
    [S, C, S, D]
```

So the resulting append state would be:

```text
["ROOT", "S", "C", "S", "D"]
```

This is not hypothetical. The simulator produced:

```text
['S', 'C', 'S', 'D']
```

for the final delta.

Therefore:

> **A lineage tree plus LCA is insufficient once the same pending semantic history has been materialized into two different merged descendants.**

The LCA is still useful as the physical state base. It is not the proof of semantic uniqueness.

## Stable contribution identity fixes this example

With:

```text
hx = [S#1, C#1]
hy = [S#1, D#1]
```

the merge algorithm is an ordered stable union:

```python
seen = contributions_already_in(base)

for port in gather.ports:
    for contribution in delta_since(base, arrival[port].lineage):
        if contribution.id in seen:
            continue

        seen.add(contribution.id)
        output.append(contribution)
```

Result:

```text
port left:
    S#1
    C#1

port right:
    S#1   # already seen: skip
    D#1

=> [S#1, C#1, D#1]
```

This is schedule-independent.

### Stronger requirement than “give writes IDs”

The ID must identify the **original semantic contribution**.

When a gather carries `S#1` into a new merged lineage, it must retain:

```text
S#1
```

It must not clone it as:

```text
S#27
```

merely because it now resides in another lineage.

A fresh node write gets a fresh ID. A merge copies/references existing contribution IDs.

A good shape is approximately:

```python
@dataclass(frozen=True)
class StateContribution:
    id: ContributionId
    path: StatePath
    incoming_value: JsonValue
```

with an ID derived from a durable node-execution occurrence plus write ordinal:

```text
(step_execution_id, write_index)
```

rather than generated afresh while replaying a merge.

### Additional invariant

If two input histories contain the same contribution IDs, their relative ordering of the shared IDs should agree.

For example, this should be treated as corruption:

```text
left  = [A#1, B#2]
right = [B#2, A#1]
```

A first-port-wins union would conceal the contradiction.

For histories that genuinely share a causal ancestor, common contributions should form order-consistent subsequences.

---

# 8. Third break: gather firing was not crash-safe

The clean checkpoint above passed because it occurred between semantic transitions.

I then injected a crash **inside** the previous `fire_gather()` ordering.

The previous pseudocode did approximately:

```text
1. create merged lineage
2. normalize claims
3. consume input tokens
4. mark resolved fork visits
5. create continuation token
6. mark bucket fired
7. enqueue continuation
```

I crashed after step 5 but before step 6.

Persisted state was:

```text
hx bucket:
    status = READY
    left  = T4
    right = T2

T4.status = CONSUMED
T2.status = CONSUMED

continuation token exists:
    claim = {k.x, r.c}
    delta = [S#1, C#1]
```

The previous `fire_gather()` begins by asserting that all bucket input tokens are still parked.

On recovery that precondition is false:

```text
left  = CONSUMED
right = CONSUMED
```

So the transition cannot be replayed.

If that precondition is relaxed and the whole operation is blindly rerun, a second continuation can instead be created.

Therefore the old pseudocode gives a choice between:

```text
stuck recovery
```

and:

```text
duplicate continuation
```

depending on implementation details.

Neither is acceptable.

## Required durability rule

You need one of two explicit guarantees.

### Option 1: semantic transitions are atomically persisted

If the persistence layer guarantees:

> `fire_gather` mutates a private run state and the completed RunState is atomically persisted as one unit,

then no intermediate state above is ever durable.

That is sufficient and simpler.

But it must be an actual runtime guarantee, not an assumption hidden inside the algorithm.

### Option 2: persistent transition journal

If internal transition phases may be checkpointed, gather firing needs a recoverable state machine.

For example:

```python
class GatherBucket:
    ...
    phase: Literal[
        "collecting",
        "ready",
        "firing",
        "fired",
        "cancelled",
    ]

    fire_transition_id: str | None
    output_lineage_id: str | None
    continuation_token_id: str | None
```

Prepare:

```text
READY
  |
  | persist:
  | - deterministic transition ID
  | - exact input token IDs
  | - output lineage ID
  | - ordered contribution IDs
  | - normalized output claim
  | - continuation token ID, initially PREPARED
  v
FIRING
```

Commit/recovery:

```text
FIRING
  |
  | idempotently:
  | - consume exact inputs
  | - resolve recorded visits
  | - activate exact continuation
  | - mark bucket FIRED
  | - enqueue exact continuation frame once
  v
FIRED
```

I executed that version with a simulated crash after `FIRING` was persisted.

Recovery produced:

```text
bucket = FIRED

inputs:
    left  = CONSUMED
    right = CONSUMED

continuation:
    status = LIVE
    delta  = [S#1, C#1]
```

without a second continuation.

The same durability question applies to `ForkNode`.

A checkpoint must not expose:

```text
parent token consumed
branch x emitted
branch y not yet created
```

as an apparently complete fork.

Either fork splitting is atomic at the RunState persistence boundary, or a fork visit needs a `splitting -> open` recovery state.

---

# 9. Deterministic IDs are more useful than I gave them credit for

A `ForkVisitId` is conceptually distinct from `TokenId`, but its stored representation need not be an independently allocated UUID.

Because fork is a linear transition:

```text
one input token is consumed exactly once
```

a visit can be deterministically identified by:

```python
ForkVisitKey = (input_token_id, fork_node_id)
```

The branch tokens can similarly be:

```text
(fork_visit_key, branch_name)
```

For the simulation:

```text
r@T0
k@T1
```

were sufficient.

Repeated completed rounds do not collide because the next round starts from a newly created continuation token:

```text
g@T0
...
gather -> T7
...
g@T7
```

Conceptually they remain distinct visits even if no random ID is allocated.

Likewise, under the V1 restriction of at most one gather firing per:

```text
(owner, gather, anchor_visit)
```

you can derive:

```text
GatherKey =
    (owner_id, gather_node_id, anchor_visit_id)

GatherTransitionId =
    ("gather", GatherKey)

ContinuationTokenId =
    ("gather-output", GatherKey)

MergedLineageId =
    ("gather-lineage", GatherKey)
```

This greatly simplifies idempotent recovery.

---

# 10. Correlation inference is still the largest unproven part

The executed schedules demonstrate:

> Given the correct compiled anchor `r`, runtime matching is deterministic.

They do **not** demonstrate:

> The compiler can infer the correct anchor for every graph we intend to accept.

My previous phrase “deepest common unresolved region” was insufficiently precise.

The new `enclosing_visits` distinction makes a precise inference strategy possible.

## Example: direct inner join

For:

```text
g ==left==> ...
g ==right=> ...
             \ /
              h
```

both arrivals have:

```text
enclosers = [g, outer...]
```

The innermost common encloser is `g`.

## Example: cross-gather

Our `hx` inputs have:

```text
k.x:
    enclosers = [k, r]

r.c:
    enclosers = [r]
```

Intersection:

```text
[r]
```

so `r` is unambiguous.

## Example: result of the cross-gather

The `hx` continuation claim is:

```text
{k.x, r.c}
```

Its entire claim is enclosed only by:

```text
r
```

not by `k`.

That gives `final` an unambiguous `r` correlation as well.

This is better than union ancestry.

### Proposed compiler rule

For every reachable co-enabled combination of arrivals to gather `h`:

1. compute the enclosing-fork chain of each arrival's abstract claim;
2. intersect the chains;
3. choose the innermost common encloser;
4. require that it exists;
5. require that every reachable firing shape for this static gather chooses the same static anchor;
6. require at most one simultaneously compatible arrival per port for one dynamic anchor occurrence.

Steps 5 and 6 are where this becomes actual activation analysis rather than graph degree checking.

I have **not executed a general implementation of that compiler analysis**. That remains a proposal.

---

# 11. The unresolved-same-fork rule is necessary but not sufficient

The proposed rule:

```text
reject entering static fork g
if an unresolved g visit is already referenced by the token
```

is useful and should remain.

But it does not by itself guarantee gather correlation.

Consider:

```text
Fork p ==left==>  g
       ==right==> g
```

Two sibling tokens can each activate the same static `g`.

Neither incoming token has `g` in its own ancestry before executing it, so the recursive-reentry rule permits both.

You can now obtain:

```text
g#A.x
g#A.y
g#B.x
g#B.y
```

If a downstream gather is locally correlated to `g`, these can form two deterministic buckets:

```text
(gather, g#A)
(gather, g#B)
```

That is potentially valid.

But if downstream topology expects the outer `p` activation to correlate them, one port can receive more than one token under:

```text
(gather, p#0)
```

Ports and ancestry alone do not say which one should win.

Therefore V1 additionally needs a **port-cardinality invariant**:

> For one `(OwnerId, GatherNode, AnchorVisit, Port)`, the accepted graph must produce at most one compatible live arrival.

Multiple producer edges remain legal when they are proven alternatives.

For example:

```text
decision --d--> d --ok--> h.right
         --e--> e --ok--> h.right
```

is fine because `d` and `e` are mutually exclusive.

Two simultaneously emitted branches targeting `h.right` are not.

The runtime duplicate-port check remains mandatory even when static analysis claims this cannot happen.

---

# 12. Loops create a second cardinality problem

Even if a static inner fork completely converges before being entered again, an **outer unresolved anchor** can remain open.

For example:

```text
outer fork
  |
  +-- loop branch:
  |      g -> local_gather -> repeat
  |
  +-- slow sibling
```

Repeated completed `g` rounds are individually coherent.

But if every round emits an arrival to:

```text
H.left
```

while `H` is correlated to the still-open outer fork, the second round produces:

```text
a second H.left for the same outer activation
```

before `H.right` necessarily arrives.

So:

> “No same unresolved fork re-entry” does not imply “one gather arrival per port per correlation occurrence.”

Those are different validation properties.

Completed rounds after **full relevant convergence** remain valid. Repeated rounds underneath another still-open synchronization domain require cardinality analysis.

---

# 13. Static validator audit

I executed a small finite worklist checker specifically for the unresolved-fork re-entry property.

This checker assumes that the compiler has already determined which gathers fully discharge which forks. It is **not** the full gather soundness validator.

Its abstract state is:

```python
(node_id, frozenset[open_static_fork_ids])
```

Transfer:

```python
if node is Fork(g):
    if g in open:
        reject
    open += {g}

if node is a gather proven to fully discharge g:
    open -= {g}

propagate to successors
```

Because the abstract domain is finite:

```text
|Nodes| × 2^|ForkNodes|
```

a visited-state worklist reaches a fixed point even when the concrete graph contains ordinary cycles.

### Executed results

| Graph                                                     |       Result | Abstract states examined |
| --------------------------------------------------------- | -----------: | -----------------------: |
| Ordinary cycle with no forks                              | **accepted** |                        4 |
| `g -> branches -> h -> repeat g` where h fully resolves g | **accepted** |                        7 |
| recursive unresolved case `g.left -> ... -> g` before h   | **rejected** |                        7 |

For the recursive case the rejection state was exactly:

```text
entering g
open_forks = {g}
```

So the checker does not need termination analysis of the workflow.

It merely asks whether a particular finite abstract control state is reachable.

## Why completed rounds are not rejected

For:

```text
g
==left==> a -> h.left
==right=> b -> h.right

h -> decide

decide --repeat--> g
       --finish--> END
```

the abstract states are:

```text
before g:
    {}

after g:
    {g}

at both branches:
    {g}

after full h:
    {}

repeat backedge:
    {}

enter g again:
    legal
```

The second concrete visit may be:

```text
g#1
```

rather than:

```text
g#0
```

but the static fixed point intentionally collapses completed rounds onto the same abstract state.

## Recursive unresolved case

For:

```text
g ==left==> a
g ==right=> b -> h.right

a --recurse--> g
a --finish---> h.left
```

the recurse edge carries:

```text
open = {g}
```

into `g`.

Therefore it is rejected without unrolling:

```text
g#0, g#1, g#2, ...
```

at all.

That is the correct static abstraction for this restriction.

### What this result does not prove

It does not prove:

* that every gather can eventually fire;
* that every port's alternatives are co-enabled correctly;
* that a gather receives at most one token per port;
* that the inferred correlation anchor is always correct;
* workflow termination;
* absence of synchronization deadlocks.

Those require a stronger abstract marking/token analysis.

---

# 14. Revised correlation model

The audit leaves me with this smaller and more precise runtime model.

```python
@dataclass(frozen=True)
class OwnerRoot:
    owner_id: OwnerId


@dataclass(frozen=True)
class BranchObligation:
    fork_visit_id: ForkVisitId
    branch: str


ControlClaim = frozenset[OwnerRoot | BranchObligation]


@dataclass
class ControlToken:
    id: TokenId
    owner_id: OwnerId
    scope_id: ScopeId
    claim: ControlClaim
    lineage_id: LineageId
    status: TokenStatus


@dataclass
class ForkVisit:
    id: ForkVisitId
    fork_node_id: str
    parent_claim: ControlClaim
    branches: tuple[str, ...]
    status: Literal["splitting", "open", "resolved", "cancelled"]


@dataclass(frozen=True)
class GatherKey:
    owner_id: OwnerId
    gather_node_id: str
    anchor_visit_id: ForkVisitId
```

The crucial operations are now:

```text
referenced_visits(claim)
    all unresolved forks on which any component depends

enclosing_visits(claim)
    unresolved forks enclosing every component of the claim

normalize(claim)
    replace complete branch sets with their saved parent claims
```

Use them as follows:

| Question                                              | Operation                                                                  |
| ----------------------------------------------------- | -------------------------------------------------------------------------- |
| Can this token execute Fork `g`?                      | `g ∉ referenced_visits(claim)`                                             |
| Can this token participate in gather anchored by `g`? | unique `g` in `enclosing_visits(claim)`                                    |
| Does combining tokens resolve a fork?                 | `normalize(union(claims))`                                                 |
| Are two arrivals in same occurrence?                  | same owner + scope + resolved anchor visit                                 |
| Has all owner control converged?                      | normalized claim is `{OwnerRoot(owner)}` plus no other live/parked control |

That separation is much stronger than my first version.

---

# 15. Revised state-merge rule

A physical lineage tree still works for this graph.

But its meaning changes slightly:

> The lineage tree determines state-view ancestry and provides a convenient merge base. Contribution IDs determine semantic exactly-once replay.

A gather should effectively compute:

```python
base = deepest_common_tree_ancestor(input_lineages)

base_ids = contribution_ids_visible_at(base)

output_delta = ordered_stable_union(
    base_ids=base_ids,
    inputs=[
        delta_since(base, arrival[port].lineage_id)
        for port in gather.ports
    ],
)

output_lineage = Lineage(
    parent=base,
    contributions=output_delta,
)
```

The output contains **references to contribution identities**, not copied anonymous writes.

For the adversarial graph:

```text
hx:
    parent L0
    local refs [S#1, C#1]

hy:
    parent L0
    local refs [S#1, D#1]

final:
    parent L0
    local refs [S#1, C#1, D#1]
```

The LCA remains `L0`.

The correctness comes from the IDs.

---

# 16. One more checkpoint boundary: owner commit

My simulation used:

```text
all fork-region writes remain pending
until the final `{R}` token reaches END,
then the ordered final delta is committed.
```

That gives:

```text
before END:
    committed = [ROOT]
    continuation visible state = [ROOT,S,C,D]

after END:
    committed = [ROOT,S,C,D]
```

This is a proposed completion rule, not something established by the previous pseudocode.

The actual implementation must also make this commit crash-safe.

Otherwise an append reducer can suffer:

```text
apply [S,C,D] to committed state
CRASH
resume still thinks owner is uncommitted
apply [S,C,D] again
```

and produce:

```text
ROOT,S,C,D,S,C,D
```

So exactly-once contribution identity does not help if the final **commit transition itself** is not durable/idempotent.

Again, either:

```text
RunState mutation + persisted completion is atomic
```

or committed contribution IDs / a commit journal must make recovery idempotent.

---

# 17. Demonstrated versus still assumed

### Demonstrated by executed reference simulations

| Property                                                        | Result                      |
| --------------------------------------------------------------- | --------------------------- |
| Direct fork→gather works after routing correction               | yes                         |
| Two substantially different schedules correlate the same tokens | yes                         |
| Gather firing order does not determine reducer order            | yes                         |
| Stable contribution IDs prevent duplicated `S`                  | yes                         |
| LCA-only replay duplicates `S`                                  | **yes, failure reproduced** |
| Clean checkpoint with a ready gather resumes correctly          | yes                         |
| Previous mid-gather-fire ordering is not recoverable            | **yes, failure reproduced** |
| Journaled gather firing survives prepare/fire checkpoint        | yes                         |
| Union ancestry differs from whole-claim enclosure               | yes                         |
| Finite re-entry worklist terminates on ordinary cycles          | yes                         |
| Completed-round loop is accepted                                | yes                         |
| unresolved recursive re-entry is rejected                       | yes                         |

### Assumptions/proposals not yet demonstrated

The following are still unproven:

1. A practical compiler analysis can infer a unique anchor for every topology you want to accept.
2. The proposed bounded token-state analysis remains acceptably cheap on realistic large graphs.
3. Stable contribution-ID union is sufficient for every reducer/state topology you eventually want, rather than merely the cases tested.
4. Your actual persistence layer provides the atomic semantic-transition boundary assumed by the simpler implementation.
5. Port cardinality can always be proven cheaply enough without excessive false rejection.
6. Failure cleanup under arbitrary cross-gathers can be reduced further than owner-wide cancellation safely.

I would not treat any of these as established yet.

---

# 18. Updated acceptance restrictions

I would tighten V1 to the following.

**Accept a gather only when the compiler can establish:**

```text
1. every incoming edge specifies a declared destination port;

2. every reachable firing has one statically unique correlation anchor;

3. runtime anchor matching uses whole-claim enclosure, not union ancestry;

4. at most one compatible token can satisfy each port for one
   (owner, gather, dynamic anchor) occurrence;

5. alternatives targeting the same port are mutually exclusive;

6. the gather fires at most once for each GatherKey;

7. no branch can reach owner completion while unresolved control remains;

8. executing Fork g is impossible while any component of the incoming
   token still references an unresolved visit of g;

9. reducer conflicts are deterministic and schedule-independent;

10. if shared pending histories can reconverge, stable contribution
    identity is enabled; otherwise that graph class is rejected.
```

This is stricter than the previous proposal, but the restrictions correspond to actual failure modes uncovered by the audit.

---

# 19. Tests I would add before implementation expands further

The most valuable tests now are:

```python
test_direct_fork_branch_to_gather_preserves_target_port()

test_cross_gather_uses_common_encloser_not_any_referenced_visit()

test_cross_gather_mixed_claim_enclosers()
# {k.x, r.c}: referenced={k,r}, enclosing={r}

test_append_shared_history_no_duplicate_schedule_a()

test_append_shared_history_no_duplicate_schedule_b()

test_lca_only_reference_model_demonstrates_duplicate()
# expected deliberately-bad delta: S,C,S,D

test_checkpoint_ready_bucket_round_trip()

test_crash_after_gather_prepare_recovers_one_continuation()

test_crash_after_continuation_before_fired_never_duplicates()

test_fork_split_checkpoint_never_exposes_partial_branch_set()

test_owner_commit_append_is_idempotent_across_crash()

test_completed_fork_round_loop_is_valid()

test_unresolved_same_fork_reentry_is_invalid()

test_partial_cross_claim_reentry_detects_referenced_fork()

test_two_simultaneous_arrivals_same_port_rejected()

test_alternative_arrivals_same_port_allowed()

test_inner_completed_loop_cannot_emit_second_outer_port_arrival()

test_gather_anchor_inference_same_under_all_reachable_alternatives()
```

For every concurrency test, compare semantic state rather than trace order:

```python
assert (
    normalized_claim,
    gather_keys,
    unresolved_visits,
    ordered_contribution_ids,
    committed_state,
) == expected
```

---

# 20. Revised conclusion

The audit changes my recommendation in two important ways.

First, **activation IDs and provenance are still not the main abstraction**. The more exact primitive is:

```text
linear control obligations
+ whole-claim enclosure
+ static correlation planning
```

Historical/reference ancestry and correlation ancestry are different relations.

Second, stable state-write identity is no longer merely an observability enhancement if you want arbitrary:

```text
merge
-> re-fork
-> cross-gather
-> reconverge
```

with order-sensitive reducers.

For that topology, it is a correctness requirement.

If you do **not** need that topology in V1, rejecting it remains the smaller choice.

The smallest defensible V1 therefore remains fairly constrained:

```text
explicit fork
fixed gather ports
direct fork->gather supported
linear token replacement
unique compiled correlation anchor
whole-claim enclosure matching
one arrival per port per anchor occurrence
one gather firing per GatherKey
no unresolved same-fork re-entry
no premature END
atomic/journaled semantic transitions
deterministic reducer order
```

Then choose exactly one of:

```text
A. reject shared-history cross/reconvergence
```

or:

```text
B. introduce stable StateContribution IDs before accepting it
```

I would now make another implementation-order change as well:

> **Consolidate durable transition identity before implementing fork/gather, not merely owner/activation identity.**

Fork visits, branch tokens, gather buckets, merge lineages, continuation tokens, contribution writes, and final commits all need a coherent answer to “is this the same semantic transition being recovered, or a new execution?”

Without that, the graph semantics can be correct in memory and still be wrong after a crash.