Shard-A: compile-gate partition totality + cross-shard seam preservation proof

[briansrls]

Worker attestation

• Title describes the change (not the session id or branch).
• PR body summarises what and why.
• Tests run: named below, all confirmed green by real execution.
• No Closes #N — this is an ad-hoc shard-A work item, not a GitHub issue.
• No commits on this branch are surprises (only a merge of origin/main plus my own commits; verified git diff --stat origin/main shows only the 7 files below).
• No secrets / credentials / large binaries staged.

Summary

Builds on #6118's partition/verdict-compose algebra (dag/tools/dag_compile_clean_partition.dag, reused not duplicated) with two by-execution proofs for the compile-gate shard partition:

1. Partition totality (dag_compile_clean_shard_roster.dag, dag_compile_clean_shard_totality*.dag) — proves every module in the live dag/ corpus (885 files) is claimed by exactly one shard: no orphan, no double-claim. The roster is built from the real host builtin module_declaration_facts (bypassing the currently-broken v2.lens.module_graph.dag, which Affected-set Step 3: module-grain frontier equivalence receipts #6274 is fixing separately — not a dependency here, per the brief). Ground truth is an independent find dag -name '*.dag' | sort run via shell.Exec.Run, not just a re-derivation from the same source — the two are compared and any orphan/dup/glob-failure fails closed to a typed, located PartitionOrphan/PartitionDuplicateClaim/PartitionGlobUnavailable verdict, never silence.

2. Cross-shard seam preservation (dag_compile_clean_seam*.dag) — deliberately breaks a real cross-shard import edge (dag/std/bit.dag imports Classical from dag/std/logic.dag) by renaming only the type declaration in a scratch copy of the tree, leaving logic.dag's own usages of the old name untouched. This proves by execution that: (i) shard Y (logic.dag) reds with a located diagnostic, (ii) shard X (bit.dag, the importer) also reds — the seam's consequence is not silently lost — and the composed verdict (via compile-clean shard A: partition boundary, one-shard receipt, compose proof #6118's compose_compile_clean_shard_verdicts) reds and names the cause, and (iii) the full monolith compile run as a control emits the same diagnostic class (Classical) as both shards, confirming no diagnostic class is uniquely available to the monolith and missing from the sharded path.

Both witnesses run against the real 885-module dag/ tree (not synthetic fixtures) via shell.Exec.Run; synthetic-input algebra witnesses are included too as fast unit-style checks, but are not a substitute for the live-tree proof.

Explicitly out of scope

Wiring this partition into ci_floor_plan is not part of this PR. Floor wiring is gated on the in-process shard resolve pool (M2) — re-landing per-PR floor wiring before that lands regressed CI by 30.9x (see the #6127/#6156 receipt trail). This PR is proof-of-partition only.

Test plan

Locally built gunbc in-tree (ctrl-build --local -- cargo build -p v1-compiler --release --bin gunbc) — a pre-installed binary resolves workspace_root() against a different checkout and silently returns wrong (not errored) results, so all witnesses below ran against that local binary:

• compile_clean_shard_roster_is_well_formed → true
• compile_clean_shard_totality_transport_serializes_find_sort → true
• compile_clean_shard_totality_algebra_holds → true
• compile_clean_shard_totality_holds_on_live_tree → true (real find dag -name '*.dag' | sort executed via shell.Exec.Run, compared against the live 885-module roster)
• cross_shard_seam_transport_serializes_expected_shape → true
• cross_shard_seam_algebra_holds → true (synthetic-receipt algebra, including two fail-closed negative cases)
• cross_shard_seam_preservation_holds_on_live_tree → true, run twice (pre- and post- merging latest origin/main): whole-dag/-tree scratch copy, single-line perturbation of logic.dag, three real gunbc compile invocations (shard Y alone, shard X alone, full monolith control) with captured stdout/stderr/exit codes

All via gunbc run --claim-run against the real worktree, not gunbc compile's typecheck-only path.

[gunbai-bot]

Addressing review 35760:

Finding 1 (partition totality one-sided, dag_compile_clean_shard_totality.dag:45-50) — valid, fixed in 3b337f0.
Added a PartitionSurplusClaim { surplus_paths } variant computed symmetrically to the existing orphan check (roster_paths entries absent from the live glob output), wired into compile_clean_partition_totality_verdict_from's priority chain and compile_clean_partition_totality_is_total's exhaustive match, plus a new synthetic witness witness_totality_reds_on_synthetic_surplus (paralleling the existing orphan/double-claim witnesses) proving the arm reds on a phantom roster path. Re-ran both compile_clean_shard_totality_algebra_holds and the live-tree compile_clean_shard_totality_holds_on_live_tree witnesses by execution — both still green.

Finding 2 (fragile substring exit-code parsing, dag_compile_clean_seam.dag:27-28) — not reproducible, no change.
seam_exit_nonzero/seam_field_zero search for the literal substring field + "=0" (e.g. "Y_EXIT=0") in the raw SEAM_RESULT ... line. For this to false-match on a nonzero value, that value's string form would need to start with the digit 0 — but neither bash's $? nor grep -c's count ever render with a leading zero, so a two-digit (or longer) value never collides with the single-0 pattern. Concretely, "Y_EXIT=10" does not contain "Y_EXIT=0" as a substring: the character immediately after = is 1, not 0, at every possible alignment. Verified by execution with a throwaway synthetic receipt built from SEAM_RESULT Y_EXIT=10 X_EXIT=1 M_EXIT=1 Y_HAS=2 X_HAS=1 M_HAS=1 — seam_field_zero(field: "Y_EXIT") returns false and seam_exit_nonzero(field: "Y_EXIT") returns true, i.e. the two-digit case is classified correctly. No field name is a prefix/suffix of another in this line's fixed vocabulary (Y_EXIT/X_EXIT/M_EXIT/Y_HAS/X_HAS/M_HAS), so there's no cross-field collision either. Leaving as-is; happy to revisit with a concrete counterexample if one exists.

— sent from jolly-ram-333

[gunbai-bot]

Addressing review 35752:

Finding A (RawLine medium-as-string scaffold missing typed Disposition, dag_compile_clean_seam_transport.dag) — valid, fixed.
Added a cross_shard_seam_transport_invocation_substring_witness_disposition: Disposition = Scaffold { dissolves_to: RealizationDispatch, bind: ... } typed carrier (matching the established dag_compile_clean_shard_transport.dag precedent), registered the file in medium_structure_exception_roster (baseline bumped 52→54, see below), and appended a "retire medium_structure_exception_roster entry for dag/tools/dag_compile_clean_seam_transport.dag" clause to the existing dissolution note.

Finding B (missing realization_vocab_exception_roster entries) — valid, fixed.
Added both new bash-program-importing transport files (dag_compile_clean_seam_transport.dag, dag_compile_clean_shard_totality_transport.dag) to realization_vocab_exception_roster. Re-running realization_vocab_clean_tree_holds by execution surfaced that bash_program_importer_count_baseline also needed correcting — the true live importer count (scanning src/v2+dag) is 37, not the stale 33/35 I'd first assumed; bumped to 37 and confirmed by execution. medium_structure_clean_tree_holds also independently caught that dag_compile_clean_shard_totality_transport.dag's test function has the same emit→check serialize_bash/string_contains shape, so it needed the same roster entry (baseline 53→54).

All of the above pre-existing debt uncovered along the way (3 files in medium_structure, 2 files in realization_vocab, main's own stale importer-count baseline) predates this PR — confirmed via git show origin/main:... — and is left untouched as out of scope; none of it is enrolled in the CI witness roster.

— sent from jolly-ram-333

[gunbai-bot]

Addressing review 35762:

Finding (missing Disposition scaffold on dag_compile_clean_shard_totality_transport.dag) — valid, fixed in 8fd294e.
Added the same Disposition = Scaffold { dissolves_to: RealizationDispatch, bind: DeclarationRef { module_path: "v2.lens.medium_structure_containment", decl_name: "medium_structure_containment_holds", field: WholeDeclaration } } carrier used by the sibling transports (dag_compile_clean_shard_transport.dag, dag_compile_clean_seam_transport.dag), so the dissolution mark lives on the scaffold itself rather than only in the lens roster entry. Re-ran both compile_clean_shard_totality_transport_serializes_find_sort and compile_clean_shard_totality_algebra_holds by execution — both green.

— sent from jolly-ram-333

[gunbai-bot]

Re: CI FAILING @ 126d318.

Investigated both failing jobs — this is the pre-existing tree-wide infra outage, not a regression from this PR's diff:

• ci timed out after 15 min at the very first step, "Build release bins (claim_executor + gunbc)" — before any .dag witness in this PR (or anywhere) even runs.
• rust_tests timed out after 15 min at the equivalent first step, "v1 rust gate (fmt + clippy + nextest)".

Cross-checked main's own recent CI history: ci has failed on every one of the last several main commits (28746406899, 28746397430, 28746342868, 28745228439, ...), and rust_tests is flaking the same way (28745228439 failed with the identical "v1 rust gate ... timed out after 15 minutes" signature and a sccache/fleet-pressure $HOME differs from euid runner error visible in the log). This is shared-runner/sccache capacity pressure unrelated to any PR's content — the timeout fires before this PR's added .dag files are ever reached, and those files aren't wired into ci_floor_plan (out of scope per the original brief).

No fix pushed since there's nothing in this diff to fix; this branch merges origin/main at 126d318, so it inherits main's current infra state. Will keep watching for the check to go green on retry.

— sent from jolly-ram-333