Prove Flow Choice predicate disjointness

[srinji-kaggss]

Based on main at 14c572a3. Closes #71.

This replaces Flow Choice target-uniqueness theatre with a bounded, versioned proof that predicates cannot overlap, then binds planning to the immutable snapshot that made the choice.

The gap

Choice admission previously treated distinct target node IDs as if they proved distinct predicates. They do not: two arms can both be true and point at different targets. Planning also did not select a Choice target from the actual snapshot, so the verifier and planner did not share a complete semantic contract.

The fix

• Add disjointness fragment v0 with public Disjoint, Overlap(counterexample), and typed Unknown results.
• Cover constants, equality/inequality, numeric ordering, Boolean composition, De Morgan normalization, and completion atoms.
• Reject overlap with stable Choice/arm/target identity plus a deterministic witness.
• Fail closed on unsupported relations and on predicate node, depth, normal-form, atom, per-pair, and aggregate-work ceilings.
• Preflight every pair and aggregate work before normal-form/solver allocation.
• Evaluate every Choice arm against the immutable snapshot during planning; select exactly one proven arm, use otherwise when none prove, and defer the entire Choice if any arm is unknown.
• Bind the selected target and full next-step identity into the Plan CID.

The rejected alternative was an unbounded SAT/SMT dependency or a first-match rule. The former adds a second operational dependency and non-portable proof surface; the latter silently turns ambiguous graphs into order-dependent behavior. This bounded fragment is deterministic, no_std + alloc, and refuses what it cannot prove.

The real user path

These are the public verifier/planner paths, not private helper-only tests:

$ cargo test -p braid-flow-verify --test disjointness demonstrably_disjoint_choice_is_admitted --locked
test demonstrably_disjoint_choice_is_admitted ... ok
test result: ok. 1 passed; 0 failed; 11 filtered out
exit 0

$ cargo test -p braid-flow-verify --test disjointness mutation_removing_pair_checks_cannot_hide_identical_predicates --locked
test mutation_removing_pair_checks_cannot_hide_identical_predicates ... ok
test result: ok. 1 passed; 0 failed; 11 filtered out
exit 0

$ cargo test -p braid-flow-verify --test disjointness mutation_treating_unknown_as_disjoint_cannot_admit --locked
test mutation_treating_unknown_as_disjoint_cannot_admit ... ok
test result: ok. 1 passed; 0 failed; 11 filtered out
exit 0

$ cargo test -p braid-flow-plan --test plan_invariants mutation_removing_snapshot_binding_changes_choice_plan_cid --locked
test mutation_removing_snapshot_binding_changes_choice_plan_cid ... ok
test result: ok. 1 passed; 0 failed; 11 filtered out
exit 0

The refusal cases are asserted through the public library APIs: an overlapping or unknown Choice is rejected by verify, while an unknown runtime predicate defers plan. A shell exit 1 would test a wrapper rather than the contract this repository exposes.

Regressions

• Property-test the solver against exhaustive finite-domain evaluation.
• Admit provably disjoint numeric/equality predicates and reject overlaps with witnesses.
• Normalize De Morgan and operand order to the same deterministic witness.
• Cover the four-state completion domain.
• Preserve operand types for reflexive relations.
• Refuse unsupported cross-reference relations as typed Unknown.
• Exercise predicate-node, depth, normal-form clause, and aggregate all-pairs work ceilings.
• Prove Choice target selection, otherwise, unknown deferral, snapshot binding, and stale planner-version refusal.

Proof of teeth

Mutation	Test that kills it
Delete the all-pairs loop	mutation_removing_pair_checks_cannot_hide_identical_predicates
Convert Unknown to Disjoint	mutation_treating_unknown_as_disjoint_cannot_admit
Remove the snapshot from Plan identity	mutation_removing_snapshot_binding_changes_choice_plan_cid
Remove aggregate pair-work preflight	aggregate_pair_work_budget_blocks_large_choices
Treat an unknown arm as false	unknown_choice_arm_defers_instead_of_falling_through

Plan identity had to move to version 1

Choice planning now changes Plan CID bytes by including the full next-step node, kind, capsule CID, and selected Choice target. Keeping planner version 0 would silently reinterpret old identities. PLANNER_VERSION is therefore 1; version 0 caller contexts are rejected and must recompute rather than alias the new scheme.

Debt-on-touch

File	Before	After
Cargo.lock	Verifier lacked property-test support	Lockfile records the verifier dev dependency
crates/braid-flow-plan/src/lib.rs	Planner version was implicit to callers	Exports planner version 1
crates/braid-flow-plan/src/plan.rs	Choice did not bind an evaluated target	Snapshot-evaluated target selection and version refusal
crates/braid-flow-plan/tests/plan_invariants.rs	No Choice planning contract	Target, fallback, deferral, CID, and version regressions
crates/braid-flow-verify/Cargo.toml	No finite-domain property harness	Adds test-only proptest
crates/braid-flow-verify/src/disjoint.rs	No predicate disjointness solver	Bounded fragment, normalization, witnesses, and ceilings
crates/braid-flow-verify/src/error.rs	Choice errors could not report semantic overlap	Typed overlap, unknown, budget, and duplicate-target errors
crates/braid-flow-verify/src/lib.rs	Solver contract was not public	Exports the versioned disjointness API and ceilings
crates/braid-flow-verify/src/verify.rs	Distinct targets passed without predicate proof	Two-pass all-pairs preflight and fail-closed verification
crates/braid-flow-verify/tests/disjointness.rs	No semantic or mutation coverage	Twelve solver/admission/property/mutation tests
docs/CRATE-OWNERSHIP.md	Ownership omitted disjointness	Assigns the solver to braid-flow-verify
docs/STRATEGIC-VISION.md	Choice semantics were underspecified	Records bounded proof and fail-closed behavior
docs/adr-099-braid-frontier-flow.md	Flow ADR allowed target-level ambiguity	Requires predicate disjointness and snapshot planning
docs/adr-101-root-admission-triad-and-token-plan.md	Plan identity did not cover Choice target	Records planner v1 migration and recomputation
spec/braid/DECISIONS.md	No closed disjointness-fragment decision	Records v0 fragment, public ceilings, and unknown policy

Full CI, run locally at ae01e77b739d

bash .wwfd/local-ci.sh completed all 27 lanes and wrote /Users/srinji/wwfd/state/local-ci-receipt.json for this exact Jujutsu subject.

Lanes	Result
01 swallow budget	pass
02 format	pass
03 locked metadata	pass
04 build all targets	pass
05 workspace tests	pass
06 doc tests	pass
07 clippy with warnings denied	pass
08–14 lgwks-std feature matrix	pass
15–22 MSRV feature/gate checks	pass
23 contract drift	pass
24 package smoke	pass
25–27 consumption contract	pass

Receipt:

{"repo_root":"/Users/srinji/Braid","branch":"fix/flow-choice-predicate-disjointness","head_sha":"ae01e77b739d","attested_at":1788066777,"ci_script":"bash .wwfd/local-ci.sh"}

GitHub Actions

Braid CI run 33294327212 completed successfully at ae01e77b739d729a8140ce65fc77e8d019290163: 14/14 checks passed, including Stack, Scope, Build, Tier 0 test, Tier 0 clippy, and Cleanup.

What is still not done

• Relations between distinct references that require relational solving return typed Unknown; this patch does not add an SMT backend.
• The counterexample is a deterministic bounded-fragment witness, not a transported external proof certificate.
• The PR remains open; this receipt does not claim it is merged.
• Remaining roadmap issues, including [P0.1 AMENDMENT] Collapse v0 interop to Read | Write; keep Justified as a loud future gate #63, are outside this issue's contract.