lda-wf/docs/historical/research/2026-09-06-fork-gather/imported/audit-2.md

The exact scratch code behind my previous audit was not persisted and is no longer accessible. The artifacts below are a reconstruction of those semantics, written and executed in this verification round. They do not import or implement against the production repository.

Runnable artifacts

Download the complete artifact bundle

Individual files: simulator + analyzer, 25-test suite, README / commands, and captured test output.

Run them with:

python -m unittest -v test_fork_gather_reference.py

python fork_gather_reference.py ordering-strict
python fork_gather_reference.py ordering-port
python fork_gather_reference.py checkpoint
python fork_gather_reference.py analysis

I executed all four code paths represented by the tests/demos. The final suite result was:

Ran 25 tests in 0.024s

OK

Those are actual executions of the reconstructed reference implementation. Nothing below relies on the earlier claimed execution.

1. The ordering counterexample breaks one conclusion from the prior audit

Your graph is accepted by the reconstructed control analyzer.

It derives:

hx    anchor = r
hy    anchor = r
final anchor = r

hx discharges:    {}
hy discharges:    {}
final discharges: {fa, fb, r}

After the two inner gathers, the actual stable contribution IDs were:

hx = [
    A@r@T0/a,
    B@r@T0/b,
]

hy = [
    B@r@T0/b,
    A@r@T0/a,
]

or by labels:

hx = [A, B]
hy = [B, A]

There is no existing control rule in the reconstructed model that rejects this. Every branch obligation is consumed exactly once, and the final normalization restores the owner root.

So my previous statement that opposite histories imply "corruption" was wrong.

The correct classification is:

This is a legitimate authored control graph that produces incompatible merge-order constraints under one possible definition of merge-history preservation.

The metadata itself is not malformed.

Causal order versus gather-imposed order

This distinction matters.

In your graph:

r.a -> A -> fa
r.b -> B -> fb

A and B are concurrent sibling writes. There is no causal dependency:

A -> B

or:

B -> A

hx later imposes:

A < B

because its ports are (left,right).

hy independently imposes:

B < A

because its left input happens to originate from B.

Those are merge serialization orders, not original happens-before dependencies.

The architectural question is therefore whether an earlier gather's serialization order becomes a permanent constraint on later reconvergence.

That is a policy decision, not a provenance-integrity invariant.

---

2. Policy A: preserve previous merge orders, error on cycles

The implemented STRICT_PRECEDENCE policy treats each materialized history as an ordering constraint.

Thus:

hx: A, B    => A < B
hy: B, A    => B < A

At final, their union contains a cycle:

A < B < A

The actual simulator result is:

MergeOrderConflict:
incompatible contribution-order constraints;
cycle involves A@r@T0/a, B@r@T0/b

Importantly, hx and hy both succeed. Only final fails.

This policy preserves:

• exactly-once contribution identity;
• every previously established ordering when merging succeeds;
• schedule independence;
• order-sensitive reducer semantics as a coherent accumulated history;
• the property that a later merge never silently reverses an order already visible in an earlier merged lineage.

It sacrifices composability: a completely legitimate control graph can reach a deterministic merge conflict because independently serialized concurrent histories are incompatible.

Given your existing preference conflicts="error", I think this is the cleaner first policy. The error should be called something like:

merge-order conflict

not corruption.

Global cycle detection is necessary

Checking histories pairwise is insufficient.

I executed:

H1 = [A, B]
H2 = [B, C]
H3 = [C, A]

A straightforward pairwise shared-subsequence agreement predicate returns:

True

because each pair shares only one contribution:

H1 ∩ H2 = {B}
H2 ∩ H3 = {C}
H3 ∩ H1 = {A}

There is no pairwise disagreement to observe.

But their combined constraints are:

A < B
B < C
C < A

and the implemented global precedence check produces:

MergeOrderConflict:
cycle involves A, B, C

Therefore:

Pairwise agreement on shared IDs is not sufficient. Strict preservation requires building the union precedence graph and checking it globally for cycles.

The implementation uses adjacent sequence pairs:

[A,B,C] -> A→B, B→C

rather than every ordered pair. Transitivity supplies the rest. It then performs deterministic topological sorting.

---

3. Policy B: final gather port order wins

The implemented FINAL_PORT_ORDER policy performs stable first-occurrence deduplication in the declared final port order.

For:

final.left  = hx = [A, B]
final.right = hy = [B, A]

the scan is:

left:
    A -> retain
    B -> retain

right:
    B -> already present
    A -> already present

so:

final = [A, B]

The actual simulator commits:

["ROOT", "A", "B"]

Reversing the histories supplied to the same primitive produces [B,A], as expected.

This policy preserves:

• one occurrence per contribution ID;
• deterministic behavior;
• schedule independence;
• declared current gather port precedence;
• very simple runtime semantics.

It sacrifices a stronger property:

An ordering already observable in an earlier merged state is not necessarily preserved after later reconvergence.

A node downstream of hy could have observed:

ROOT, B, A

while the final continuation observes:

ROOT, A, B

That is not a causal contradiction—A and B were originally concurrent—but it means a lineage history is no longer interpretable as a monotonically accumulated global ordering.

For an order-sensitive reducer such as append, that is a substantial semantic choice.

Recommendation between A and B

For the prototype, I would choose A: strict precedence + deterministic merge error.

That matches conflicts="error" without confusing a legitimate authored conflict with malformed metadata. It also avoids making partial-gather ordering retroactively disposable.

If later experience shows that gather order should be a purely local projection rather than historical ordering, policy B can be introduced explicitly. I would not make that interpretation implicit.

---

4. Correlation inference is now independently executable

The reconstructed SymbolicAnalyzer does not receive manually supplied gather anchors or fork-discharge tables.

Its supported graph class is intentionally narrow:

• finite flat graph;
• one initial owner token;
• concurrency arises only from explicit ForkNode;
• a fork simultaneously emits all declared branches;
• ordinary outcomes have exactly one successor;
• ChoiceNode alternatives are explored nondeterministically;
• gathers have fixed statically declared ports;
• each gather firing consumes exactly one arrival per port;
• no unresolved re-entry of the same static fork along a token's referenced ancestry;
• no foreach/subgraph/failure/interrupt semantics in this verifier.

That is enough to test the correlation issue in isolation.

Abstract state

A symbolic activation is:

SActivation(
    fork_id,
    parent_claim,
)

A branch obligation is:

SBranch(
    activation,
    branch,
)

So two sibling activations of the same static fork are distinguishable.

For example:

p.left  -> g
p.right -> g

produces abstract activations equivalent to:

g<[p.left]>
g<[p.right]>

rather than merely:

g
g

A marking is a multiset of symbolic tokens located either:

at node N

or:

parked at gather H.port

with their complete current control claims.

Fork transfer

Executing g with claim C creates:

activation = g<C>

and emits:

g<C>.x
g<C>.y
...

Before doing so, the analyzer recursively examines the incoming claim. If static g already occurs in any referenced unresolved obligation, that transition is rejected as:

unresolved_reentry:g

It does not unroll another g.

Gather inference

When one arrival exists for every port, the analyzer enumerates complete port combinations.

For each combination it computes the deepest common enclosing symbolic activation.

That dynamically observed activation is the candidate correlation anchor.

The analyzer does not need to know in advance what the gather discharges.

It then unions the input claims and repeatedly performs:

all branches of activation X present
    ->
replace them with X.parent_claim

The activations removed by that normalization are the observed discharges for this firing.

Only after exploring all reachable markings does it require that each static gather have one static anchor fork across every possible firing.

That avoids the previous circular construction:

need anchor to infer firing
need firing to infer discharge
need discharge to infer anchor

For this supported class, firing combinations are enumerated from the actual symbolic marking first; anchor and discharge are observations of each combination.

---

5. Actual analyzer results

Graph	Result	Derived anchor(s)	Observed discharge
Ordinary g -> a,b -> h	accept	h → g	h: {g}
Direct g -> h.left,h.right	accept	h → g	h: {g}
Partial a+b, then result+c	accept	both → g	partial {}, final {g}
Sibling nested cross-gathers	accept	h1,h2,final → r	final {fa,fd,r}
Your A/B ordering graph	accept	hx,hy,final → r	final {fa,fb,r}
Conditional d OR e → h.right	accept	h → g	{g}
Simultaneous two arrivals to h.right	reject	h → g observed	duplicate compatible arrival
Completed round g→h→repeat→g	accept	h → g	{g}
Unresolved g...→g recursion	reject	—	unresolved re-entry
Two sibling activations of same static g feeding same h	reject	both g and p observed	ambiguous correlation

The completed-round analysis reached a fixed point after 8 symbolic markings. The unresolved-recursion graph rejected after 9.

The separate simpler (node, open_static_forks) re-entry checker examined six states in each of its two executed cases:

completed round:
    accepted
    6 states

unresolved recursion:
    rejected: unresolved_reentry:g
    6 states

---

6. The two-sibling-same-static-fork case reveals the real conservative boundary

Consider:

Fork p(branches=l,r)

p.l -> g
p.r -> g

Fork g(branches=x,y)

g.x -> h.left
g.y -> h.right

The symbolic state contains:

g<[p.l]>.x
g<[p.l]>.y

g<[p.r]>.x
g<[p.r]>.y

There are sensible same-activation combinations:

g<[p.l]>.x + g<[p.l]>.y
    anchor = g<[p.l]>

g<[p.r]>.x + g<[p.r]>.y
    anchor = g<[p.r]>

But ports alone also permit:

g<[p.l]>.x + g<[p.r]>.y

whose deepest common encloser is:

p

and similarly for the opposite cross-pair.

The executed analyzer therefore observes:

h anchors = {g, p}

and rejects:

non_unique_static_anchor:h:['g', 'p']

It also observes duplicate compatible arrivals under the p interpretation.

This is a useful result because it demonstrates that:

Static port identity + provenance + deepest-common-encloser does not solve general correlation.

For this prototype grammar, the exact restriction is:

A gather is accepted only if every reachable complete port combination yields the same static anchor fork, and each dynamic anchor can have at most one compatible arrival per port.

An explicit correlation declaration could make more graphs expressible later. The prototype does not need one yet.

---

7. Why the symbolic analysis terminates

This is a demonstrated property of the implemented restricted analysis, not a claim about unrestricted workflow graphs.

An activation is recursively:

(static fork ID, parent claim)

and unresolved re-entry of an already referenced static fork is rejected.

Therefore a single obligation ancestry cannot contain the same static fork twice, so nesting depth is bounded by the finite number of fork nodes.

Branch sets and static node positions are finite. Forking can create exponentially many combinations, but without same-fork unresolved recursion it cannot create an unbounded activation ancestry. Ordinary cycles eventually revisit an existing marking. Fully converged rounds similarly restore their parent claim, so another round produces the same symbolic abstract state and hits the visited set.

Thus the state space is finite for this supported class.

The practical cost is still poor in the worst case: explicit concurrent marking exploration is combinatorial. The implementation has a max_markings guard. I would treat this as a correctness prototype, not the intended production validator algorithm.

---

8. Durability correction: no journal is justified by the stated contract

My previous recommendation overreached here.

The current persistence contract you supplied is:

externally stopped states are persisted: interrupted, completed, failed.

It does not promise that arbitrary internal fork/gather mutations are individually durable.

Under that contract, a gather transition journal is not required merely because an internal transition has several logical substeps.

The reconstructed runtime instead models:

candidate = deepcopy(stable_state)

perform_complete_semantic_transition(candidate)
validate(candidate)

# publish only after successful completion
stable_state = candidate

checkpoint() serializes only stable_state.

That is deliberately illustrative rather than a production implementation prescription.

What was actually tested

The 25-test run includes:

Checkpoint round trip. A complete state containing live tokens, a ready gather, fork visits, lineages, contributions, and gather buckets was serialized and reconstructed exactly. This is actually stronger than your currently promised checkpoint surface because the reference test snapshots an internally runnable state.

Recovery from last durable checkpoint. The simulator checkpointed, performed additional uncheckpointed gather/write progress, discarded that process state, reconstructed the old checkpoint, re-executed from there, and completed as:

ROOT, S, C, D

Exception isolation. Under strict ordering, final raises MergeOrderConflict. Because it executes against a candidate copy, the published runtime state after the exception is byte-for-semantic-state identical to the state immediately before attempting the merge.

Shared-write recovery. After checkpoint/recovery, reconvergence still produced:

S, C, D

rather than:

S, C, S, D

because stable contribution IDs survived the checkpoint.

Four durability questions should remain separate

Problem	Required here?	Mechanism
Consistent supported checkpoint	Yes	snapshot only a stable semantic state
Process crash after uncheckpointed progress	Yes	recover last durable state; later work may rerun
Recovery from half-persisted internal gather mutation	No, given stated contract	don't persist such states; use atomic snapshot storage
Exactly-once external side effect	Not solved here	requires idempotency/dedup/activity semantics at effect boundary

There is one implementation consequence worth retaining.

If an operational exception causes the runtime to persist a failed stopped run, that failed snapshot should be derived from:

last stable pre-transition state
+ structured failure information

not from an in-place RunState that may have been partially mutated before the exception.

That can be achieved with a transition patch, copy-on-write, rollback, or another commit boundary. It does not imply a durable transition journal.

Exactly-once external effects are different. If:

checkpoint
-> call payment API
-> process crashes before next checkpoint

recovery can invoke the API again. Fork/gather contribution IDs cannot undo or intrinsically deduplicate that external effect.

---

9. What the artifacts now demonstrate—and what they don't

Demonstrated by execution:

• direct fork→gather preserves destination ports;
• partial gathers can retain unresolved obligations and later complete them;
• cross-gathers can be correlated for the tested sibling-nested topology;
• your ordering graph is control-valid;
• [A,B] and [B,A] are legitimate intermediate histories;
• strict precedence rejects their final reconvergence;
• final-port-order deterministically accepts it;
• global precedence cycles can exist despite pairwise agreement;
• stable contribution IDs deduplicate shared history;
• two alternate schedules of the shared-write adversarial graph both commit ROOT,S,C,D;
• checkpoint/recovery preserves tokens, gathers, lineages, contributions and correlation state;
• unresolved same-static-fork re-entry can be rejected with a terminating finite analysis;
• completed rounds are not falsely rejected;
• two sibling activations of one static fork expose a real correlation ambiguity.

Still assumptions or intentionally unsupported:

• scalability of explicit marking exploration;
• foreach/subgraph owner correlation;
• interrupts and cancellation;
• operational failures during concurrent branches;
• correlation for graphs outside the stated grammar;
• general workflow soundness or termination;
• exactly-once external effects;
• whether earlier gather serialization should semantically constrain all later reconvergences.

---

10. Narrow recommendation for the next prototype

I would prototype exactly this much:

1. Keep explicit forks, destination gather ports, and token replacement.
2. Represent symbolic/runtime fork activations by fork identity plus the consumed parent control claim; don't use static fork ID alone for correlation.
3. Initially accept a gather only when finite analysis proves one static deepest-common-encloser across all reachable firing combinations and at most one compatible arrival per port.
4. Reject unresolved same-static-fork re-entry. Permit loops after normalization fully discharges that fork.
5. Treat the two-sibling-same-static-fork/shared-gather topology as unsupported rather than inventing a correlation heuristic.
6. If shared pending histories can reconverge, retain stable contribution identities.
7. For noncommutative reducers, prototype strict global precedence checking and report cycles as ordinary merge conflicts.
8. Keep persistence at atomic, consistent externally supported stop boundaries. Do not add a transition journal for fork/gather at this stage.
9. Keep exactly-once external effect semantics out of this prototype.

The principal remaining semantic decision is now much narrower than before: does a partial gather's deterministic ordering become durable history, or is it merely that continuation's local state view? Policy A and B correspond almost exactly to those two interpretations. The control/correlation model no longer needs to answer that question for you.