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](sandbox:/mnt/data/fork_gather_reference_artifacts.zip) Individual files: [simulator + analyzer](sandbox:/mnt/data/fork_gather_reference.py), [25-test suite](sandbox:/mnt/data/test_fork_gather_reference.py), [README / commands](sandbox:/mnt/data/README_fork_gather_reference.md), and [captured test output](sandbox:/mnt/data/verification_test_results.txt). Run them with: ```bash 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: ```text 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: ```text 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: ```text hx = [ A@r@T0/a, B@r@T0/b, ] hy = [ B@r@T0/b, A@r@T0/a, ] ``` or by labels: ```text 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: ```text r.a -> A -> fa r.b -> B -> fb ``` `A` and `B` are concurrent sibling writes. There is no causal dependency: ```text A -> B ``` or: ```text B -> A ``` `hx` later imposes: ```text A < B ``` because its ports are `(left,right)`. `hy` independently imposes: ```text 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: ```text hx: A, B => A < B hy: B, A => B < A ``` At `final`, their union contains a cycle: ```text A < B < A ``` The actual simulator result is: ```text 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: ```text merge-order conflict ``` not corruption. ## Global cycle detection is necessary Checking histories pairwise is insufficient. I executed: ```text H1 = [A, B] H2 = [B, C] H3 = [C, A] ``` A straightforward pairwise shared-subsequence agreement predicate returns: ```text True ``` because each pair shares only one contribution: ```text H1 ∩ H2 = {B} H2 ∩ H3 = {C} H3 ∩ H1 = {A} ``` There is no pairwise disagreement to observe. But their combined constraints are: ```text A < B B < C C < A ``` and the implemented global precedence check produces: ```text 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: ```text [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: ```text final.left = hx = [A, B] final.right = hy = [B, A] ``` the scan is: ```text left: A -> retain B -> retain right: B -> already present A -> already present ``` so: ```text final = [A, B] ``` The actual simulator commits: ```text ["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: ```text ROOT, B, A ``` while the final continuation observes: ```text 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: ```python SActivation( fork_id, parent_claim, ) ``` A branch obligation is: ```python SBranch( activation, branch, ) ``` So two sibling activations of the same static fork are distinguishable. For example: ```text p.left -> g p.right -> g ``` produces abstract activations equivalent to: ```text g<[p.left]> g<[p.right]> ``` rather than merely: ```text g g ``` A marking is a multiset of symbolic tokens located either: ```text at node N ``` or: ```text parked at gather H.port ``` with their complete current control claims. ## Fork transfer Executing `g` with claim `C` creates: ```text activation = g ``` and emits: ```text g.x g.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: ```text 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: ```text 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: ```text 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: ```text 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: ```text 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: ```text g<[p.l]>.x g<[p.l]>.y g<[p.r]>.x g<[p.r]>.y ``` There are sensible same-activation combinations: ```text 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: ```text g<[p.l]>.x + g<[p.r]>.y ``` whose deepest common encloser is: ```text p ``` and similarly for the opposite cross-pair. The executed analyzer therefore observes: ```text h anchors = {g, p} ``` and rejects: ```text 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: ```text (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: ```python 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: ```text 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: ```text S, C, D ``` rather than: ```text 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: ```text 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: ```text 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.