Skip to content

EMIT-COST-QUAL-0: qualify the production Rust emitter's copy/share behavior over a derived permutation population -- CloneMinimality x CopyRealizationCost axes, production source->emission path, sharded execution, calibration matrix falsifiers, findings blocking; no production repairs - #9781

Merged
gunbai-bot[bot] merged 30 commits into
mainfrom
session/still-swift-46
Aug 31, 2026

Conversation

@briansrls

@briansrls briansrls commented Aug 31, 2026 •

Copy link
Copy Markdown
Contributor

EMIT-COST-QUAL-0: copy/share qualification battery for the production Rust emitter (model-ahead, inert enrollment)

Authorized by the side-chat ruling of 2026-08-31 (one lane, one bounded generated population, no production repairs), narrowed by the ROOT-N division ruling of 2026-08-31: this lane authors model-ahead evidence — the battery, its falsifiers, and its workflow step — and activates nothing. Findings block the later emitter/materialization promotion chain, not main.

Exact claim (and what is NOT claimed)

For every applicable member of the named finite permutation population below, the production Rust emitter preserves behavior and satisfies the modeled minimum copy/share-cost expectation under the declared realization/toolchain/profile. No claim about all possible Dag programs; no claim about clone prevalence in the real emitted compiler closure (separate, unauthorized lane). The wet receipts are the current-emitter baseline; they are not terminal coverage — the terminal re-run waits on computation identity + demand projection + nature classification (Q1's two temporal receipts on one carrier).

The population

Grid authority: gunbc.emit_copy_qualification (dag/gunbc/emit_copy_qualification.dag).
Case identity = EmitCopyQualificationCaseId { ownership_pattern, carrier_realization, control_shape, consumer_contract, input_size_basis } — never an ordinal. Denominator = the full Cartesian product of the five closed axis rosters; every member derives CaseApplicable | CaseNotApplicable { structural_reason } (no silent filter, no hand exclusion list). The ruling's ten named shapes are covered by construction via ruling_shape_assignments (each assigned to exactly one axis; witness-counted) — the operator-approved dedup that keeps the denominator honest.
DeepCloningSequenceCarrier is on the axis (the ruling names it) and derived inapplicable: the production realization has no .dag surface type realizing to a deep-cloning Rust sequence — grounded per-run by the wet receipt reading the emitted crate root's im:: alias, not by prose.

Expectations (derived, never authored per-case)

derive_expectation = axis relations x carrier clone-realization facts; growth classes evaluated at the declared cardinalities [0, 4, 16, 64] against deterministic allocation counters (never fitted from wall time). Underivable => QualificationRefusedCostOracleUnavailable. Constant-time is not zero-cost: a redundant Rc::clone refuses on the CloneMinimality axis independently of the CopyRealizationCost axis.

Two observation arms, joined

  • Static: clippy over the pristine emitted fixture with clippy::redundant_clone armed, --message-format=json, parsed with the shared RFC 8259 reader; identity never requires an E-code (codeless diagnostics stay in the denominator). An observation, not the cost oracle. Measured instrument boundary (2026-08-31): redundant_clone does not fire on a clone-last-use shape inside a loop (isolated by a matrix repro: identical plant fires at fn top level, is silent inside nested for-loops; a custom global allocator is innocent), so the static arm under-reports loop-interior redundant clones; the calibration plants are hoisted above the case loops (repro-proven to fire inside src/bin targets), and loop-interior clone minimality remains covered by the runtime arm + derived expectations, not by this lint.
  • Runtime: generated runner (test-workspace-only counting allocator; NO counters in production runtime/emitter/interpreter/stage0) — input built before the window opens, one case per window, serial, 3 repeats with nondeterminism refusal, startup connectivity control so a disconnected counter is DETECTED (counter=disconnected => typed observation-unavailable refusal), never a rendered zero. Unobservable ObservedCopyWork dimensions are typed unavailable.
  • Join: judge_case — prerequisites (executable, behavior agrees with the interpreted driver) before cost; verdict family EmitCopyQualification exactly as ruled.

Production path

Fixtures are generated .dag source (gunbc.emit_copy_qualification_fixture_gen) traveling the real gunbc compile --entry door (source -> resolve/infer -> emit_rust), which emits a complete crate; the transport adds only the runner bin and [workspace] isolation. Interpreted comparand: a separate driver module (outside the emission closure) writing its report via Filesystem.Write. Sharded by carrier: emit once, clippy once, build once, one serial runner per shard.

Falsifiers (calibration matrix, all named modeled transformations — no hand-edited Rust)

MutantPlan: redundant share clone (static-only red), hidden deep copy (runtime-only red), redundant deep clone, disconnected counter (observation-unavailable), copied accumulator (.dag-grain, full emission path: behavior preserved, cost shape refused). Plus generation-grain discrimination witnesses.

Deliverables & consumers

  • dag/gunbc/emit_copy_qualification.dag — grid/expectations/verdicts/join (consumed by the witnesses, the transport, and the later ladder-derived emit decisions: expectations are phrased in the existing cost vocabulary so receipts stay consumable at DEMAND landing).
  • dag/gunbc/emit_copy_qualification_fixture_gen.dag — fixture/driver/runner/mutant generators.
  • dag/gunbc/instruments/emit_copy_qualification_transport.dag — the wet transaction + receipt rendering.
  • dag/test/claim/emit_copy_qualification_witness_test.dag — hermetic floor witnesses (roster totality, denominator, derivations, join arms, mutant discrimination, workflow-job closure+inertness): run on the ordinary required floor now.
  • dag/gunbc/emit_copy_qualification_wet_battery.dag — the wet battery + calibration matrix. Battery module: gunbc.emit_copy_qualification_wet_battery. Required execution entry point: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/gunbc/emit_copy_qualification_wet_battery.dag --functions <the 12 claim functions> (the exact line the workflow step runs). It is deliberately NOT a *_test.dag module yet: v2.workflow.floor_changed_witness blocks any changed witness identity without a terminal floor verdict, and these wet transactions route-gap hermetically (IsExecutable / NoMockResponse) — a wet-only witness cannot be introduced while its executing lane ships inert. Converting the battery to floor-enrolled witnesses (and enrolling its identities wherever the floor then requires) is part of ROOT-N's activation token edit (the single edit that spends the one activation slot held for Plan DESIGN placement for meaning, externalization, and quality floor #9769 -> ROOT-1 -> DEMAND-0 -> DEMAND-1 -> ROOT-2): that one edit lifts the job's if: false, deletes emit_copy_qualification_inert_standing, and converts this module to *_test.dag witnesses — so the inert standing row and the unconverted module cannot outlive each other. Until that edit, the inert job's explicit claim_batch --functions line is the module's ONLY consumer; adding another consumer before activation is the parallel-authority tell and is out of bounds.
  • Consumers: the workflow step below (on activation); Rebuild from the compiler: the v2 compiler closure as an emitted Rust crate, with go/no-go gates #9664 successor sizing (XL-2/XL-3 decomposition); the copied-accumulator and cost authorities.

Workflow step (authored INERT — the required-gate design, for merge-time review)

emit-copy-qualification-battery job in gunbc.witness_floor_workflow (an EMISSION — no hand YAML): checkout/toolchain prelude shared with the other lanes, builds gunbc + claim_batch, runs the entry above. UNCONDITIONED by design (change-conditioning without the floor's selection machinery would be a hand-rolled second path; a follow-up proposal consumes the existing affected-set machinery if the measured cost warrants). Declared budget: emit_copy_qualification_timeout_minutes (provisional until the first activated run's own receipt). Capability closure conjoined into expected_witness_floor_yml like every other job.
It ships if: false per the ROOT-N division ruling (model-ahead evidence; one activation token, held for #9769 -> ROOT-1 -> DEMAND-0 -> DEMAND-1 -> ROOT-2). The activation edit deletes the literal false and the emit_copy_qualification_inert_standing row together. Until then the job renders as permanently skipped — visible, costless, not a gate.

Merge-review checklist (ROOT-N final division standing — each item mechanically checkable)

  • (a) No required-step change in gunbc.witness_floor_workflow: the diff to dag/gunbc/witness/witness_floor_workflow.dag only ADDS the emit-copy-qualification-battery job (with if_condition: Present { value: "false" }) and its closure conjunct; the aggregate job's needs list is untouched (still exactly the three prior lanes — check the diff hunk containing needs), so the required context cannot observe the new job. Witness ecq_battery_job_is_emitted_inert_holds asserts if == "false" on the floor.
  • (b) No required claim/commit-gate roster edits: no roster file is touched anywhere in the diff (v2.workflow.floor_route_gap, floor_expected_red, gate closures and commit-gate rosters are all byte-identical to base). The only workflow-adjacent files touched are the workflow module above and its generated mirror .github/workflows/witnesses.yml (regen output, whose only delta is the new always-skipped job).
  • (c) No merge-blocking lens contract edits: no file under dag/ outside the five new emit_copy_qualification* modules and the workflow module is touched.
  • (d) No production emitter selection/behavior change: zero edits under src/ (and none under dag/ emitter authorities) — the emitter is exercised only as a built binary through gunbc compile.
  • (e) No present-tense qualification/admission standing: the wet receipts are authored as current-emitter BASELINE evidence; no Complete/Admitted standing row is written anywhere in the diff.
  • (f) No v1.compiler.ownership edits: path absent from the diff.

Baseline findings (current emitter, this battery's first full runs — BLOCKING for the promotion chain, repaired by separately authorized lanes, never here)

CI does NOT re-derive these findings. The emit-copy-qualification-battery job ships if: false per the ROOT-N division ruling and reports COMPLETED/SKIPPED on every run of this PR — a skipped battery, not a pass; green CI on this PR is evidence only that the hermetic floor witnesses and the ordinary required lanes hold, never that findings 1–4 were reproduced. The battery's execution trigger is ROOT-N's activation token edit (named under Deliverables). Until it fires, the sole producer of these findings is the battery entry point run by hand or by a wet dispatch: claim_batch --wet --source-root dag --source-root src/v2 --entry dag/gunbc/emit_copy_qualification_wet_battery.dag --functions <the 12 claim functions>; the per-shard receipts land in target/emit_copy_qual/receipts/. The clean copy-scalar shard fully qualifies (17/17) — every other clean shard refuses:

  1. Pervasive statically-redundant clones in emitted modules (CloneMinimality): clippy's redundant_clone reports ~40–50 findings per emitted fixture module on every non-scalar carrier; most non-scalar cases refuse refused_redundant_clone. The Copy-scalar column is clean, so the class is about non-Copy carrier realization, not the emission shape generally.
  2. Per-read whole-string byte copying (CopyRealizationCost): every emitted string read allocates the string's bytes again (~2 bytes/element per read at the declared cardinalities; scales with reads per case) where the derived expectation is constant share work.
  3. Quadratic copied accumulator in emitted fold+concat (the flagship class): loop_carried_accumulator__owned_string observes 12236 bytes at n=64 against a linear allowance of ~3836 — the exact v2.lens.complexity_accumulator_copy shape, now measured on the production emitter's output.
  4. Persistent-map operation costs: emitted map reads/uses allocate ~KB-scale per touch with a per-element residue (expectation now honestly LINEAR for the map carrier), and the map loop-accumulator's allocation counts are nondeterministic across in-process repeats — a typed refusal per the ruling's repeat rule.

These keep five of the six clean-shard battery claims red by construction until the emitter climbs; that is the battery doing its job as the DEMAND program's "before" baseline, not a defect of this PR.

Findings policy

Findings are blocking for the promotion chain: a real redundant clone / deep copy / copied accumulator / behavior mismatch / unobservable case is a report + a hand-back for a separately authorized serial repair lane — never an expected-red row, never battery-plus-fixes in this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC

Brian Searls and others added 28 commits August 31, 2026 00:11
…witnesses (draft)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…arse fixes

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…ure conjunct

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…; exact emitted-module clippy attribution

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…ope leading blocks only)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…ner results (drop result_is_shared)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…rse refusal)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…d, ambiguous classify_call, defaulted args

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
… (IsExecutable/NoMockResponse)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…locks inert-lane wet witnesses)

The 12 wet transactions route-gap hermetically (IsExecutable/NoMockResponse) and
v2.workflow.floor_changed_witness rightly blocks changed witness identities without
a terminal verdict — so the battery moves out of *_test.dag discovery into
gunbc.emit_copy_qualification_wet_battery, run by the inert job via explicit
claim_batch --functions; converting it to floor-enrolled witnesses is part of the
activation edit. Reverts the route-gap chunk_05 enrollment (identities no longer
declared witnesses; enrolled-but-not-executed would red the floor).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…nding row (parent conditions)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…g block named no subject)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8yC
…n-deep-copy wrapper, pre-window clone planting, emitted lib path

- hidden-deep-copy wrapper skips loop cases (subject arg is the element list, not the String)
- redundant-clone mutants plant 'let input = input.clone();' BEFORE the window: a clone inside
  the capturing closure clones a borrowed value and is not statically redundant, so clippy was
  right to stay quiet; the pre-window shadowing clone kills the original unused
- grounding receipt reads out/src/lib.rs (the compile door emits a full crate under src/)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…qualification_case accessor

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…fication-battery job renders

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…ThenMutate linear on structural share, per-shard target dir (diagnostic-replay hazard), window-line clone planting, static-arm debug receipt

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…nondeterministic behavior cause, static-arm receipt survives the sweep, clippy --all-targets

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…oves to the fully-qualifying sequence carrier

The emitted modules THEMSELVES carry 40-50 clippy redundant-clone findings per shard (the
battery's flagship static finding), so an absolute no-redundant baseline tested the emitter,
not the instrument.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…s at n=64)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…made before the static-debug write; merge main (stale XL-0N admission dissolved by #9797)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…ed-module clones); refusal carries emitted_item

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…nal into a sink fn, no closure)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
…amily clones)

Measured on the share shard: clean and mutant produced byte-equal finding
counts (122/46) because the planted clone was carrier-typed (Rc-realized) and
clippy's redundant_clone, being MIR-based, deliberately skips Rc-family clones.
A minimal src/bin repro with a String clone fires (2 hits, clippy 0.1.93), so
the plant is now a pre-window String-typed redundant clone — carrier-independent,
runtime-arm-neutral — and the boundary is documented at the plant and in the
battery comments.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
… loop-blind)

Matrix repro isolated the suppressor: the identical String clone-last-use shape
fires at fn top level (TOP_CASE=2) and with a custom global allocator
(ALLOC_CASE=2) but is silent inside nested for-loops (LOOP_CASE=0). The prior
commit's Rc-blindness attribution was a hypothesis, not a measurement — loop
suppression alone explains every observation; comments and the boundary note
now state only what the matrix measured.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 31, 2026 13:03
AllocObservationRow.allocated_bytes, ConsecutivePairScan.prev_bytes, and the
observed_bytes/allowed_bytes pairs on GrowthExceeds and
QualificationRefusedExcessCopy are now ByteSize, compared through measure_le
(byte_size_gt/byte_size_ne helpers) and summed with measure_add. The one
Int -> ByteSize crossing for allocator readings is allocated_byte_size, with the
Nat hop at a return position per std.checked_arithmetic. The linear bound stays
Int deliberately: it is a rate (bytes/element), lifted into ByteSize only when
multiplied by a cardinality delta at its single consuming site.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01JE2ZWLWkrsHvbnb8wMJ7yC
@gunbai-bot

gunbai-bot Bot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Addressed review 57849 (unit-modeling REQUEST_CHANGES) in 3ce9827: AllocObservationRow.allocated_bytes, ConsecutivePairScan.prev_bytes, and the observed_bytes/allowed_bytes pairs on both GrowthExceeds and QualificationRefusedExcessCopy now ride std.measure's ByteSize, compared via measure_le (module-local byte_size_gt/byte_size_ne) and summed with measure_add — no bare-Int byte field survives on the substrate rows, the verdict surface, or the growth judgment. The one Int→ByteSize crossing for allocator readings is allocated_byte_size, with the Int→Nat hop at a return position per std.checked_arithmetic's documented crossing.

One deliberate residue: linear_alloc_growth_bound_bytes_per_element stays Int because it is a RATE (bytes per element of cardinality delta), not a byte quantity — it is lifted into ByteSize only when multiplied by a delta at its single consuming site in judge_alloc_growth; typing the rate itself as ByteSize would be the opposite unit fork (a per-element denomination wearing an absolute-bytes carrier). Comment at the declaration records this.

Validated by execution: the three runtime-sensitive calibrations (copied-accumulator, hidden-deep-copy, redundant-share-clone) PASS over the refactored judge path and receipt rendering.

@gunbai-bot

gunbai-bot Bot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Handover from the closed duplicate (#9834), recorded here because a delivered message is not a handover.

#9834 was dispatched from the same work-item brief as this PR and independently ADDed the same two paths (dag/gunbc/emit_copy_qualification.dag, dag/test/claim/emit_copy_qualification_witness_test.dag), neither of which is on main. I ruled that this PR owns the module — it is the fuller construction, and on both findings codex raised against #9834 it is the stronger one. #9834 is now closed. The duplication was a dispatch defect on my side, not either lane's.

Two items are genuinely additive and were handed over. They are reasoning, not evidence, and the second is a measured instrument defect. Recording them here so they survive independently of message delivery — @still-swift-46 has not acknowledged the DM.

1. CloneNecessityUnjudgeable has a second, structural ground. As written it is grounded only in StaticObservationUnavailable — the observation did not run. On the CopyScalarControl carrier there is a different fact: the observation runs and is uninformative, because rustc performs an implicit bitwise copy whether or not the clone is written, so a delete-and-rebuild arm returns the same answer for a necessary and a redundant clone. Available-but-non-discriminating is not the same state as unavailable, and collapsing them lets a Copy-carrier clone read as CloneNecessary off a silent lint. That is a §4b rung-honesty distinction — the reported rung would exceed what the executed evidence establishes — and it is worth splitting whether or not the axis ever grows. (This is state_space_conflation's "not-applicable rendered as malformed" shape: two causes with opposite owners and opposite repairs under one reason symbol.)

2. A cost-axis probe spelled as a bare Rc< is a correct answer about the wrong subject. Measured in the other lane: the returned-closure cell realizes the closure as Rc<dyn Fn...>, so a bare Rc< assertion reported a shared handle on a receiver that is a bare i64, producing a false shard failure until every assertion was bound to its parameter (w: i64 / w: Rc<). This PR's sink-bound spelling — ecq_sink(planted.clone()) with a paired negative — already avoids it; the note is so a future axis addition does not reintroduce it.

Figures cited in item 2 were executed (the 3×3 clone matrix and the three receiver realizations w: Rc<Widget>, w: Rc<FreeMonoid...>, w: i64). Item 1 is reasoning and is flagged as such.

Separately, and blocking merge here: this branch's base is ~30 commits behind main and the diff includes .github/workflows/witnesses.yml and dag/gunbc/witness/witness_floor_workflow.dag — required-lane decision authority against an intervening delta that moved witness tests and floor machinery. No delta exclusion is granted over that intersection; re-integrate and re-run.

@gunbai-bot

gunbai-bot Bot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Additional base note, same cause as the re-integration already asked for above: #9814 landed as 5e8e55add4 and adds a FIFTH variant to the closed required-phase vocabulary — GeneratedArtifactPhase on the build lane — so the required set is now parse, namespace-wave-admission, regen, generated-artifact, floor. Any green measured before 5e8e55add4 is a receipt about a weaker acceptance than the one now in force. Re-run after re-integrating so the generated-artifact phase actually executes on your head.

…cessityUnjudgeable's two grounds

witnesses.yml is the driver-refused path: regenerated via
gunbc.instruments.generated_artifact_gate main_wet from the MERGED authority tree
(remote, since the baked interpreter refuses this corpus). The result equals main's
current projection plus exactly this lane's 37-line inert emit-copy-qualification-battery
job -- main's fabric-evidence removal from the required aggregate is preserved, nothing
of the other side's authority-derived bytes was dropped.

CloneNecessityUnjudgeable carried ONE ground where there are two. A clean redundant_clone
report is uninformative on a Copy-eligible receiver -- rustc emits the same bitwise copy
whether or not the clone is written -- so NoRedundantCloneReported => CloneNecessary was
rung inflation on the CopyScalarControl cell, the one carrier where nothing was
established. The ground is now typed (StaticObservationDidNotRun vs
StaticObservationNonDiscriminating), derived per carrier from carrier_clone_realization,
with three executing witnesses: the two grounds separately and
ecq_lint_discrimination_splits_the_carriers_holds.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011KGsgroSxMJMAENEUKh8BB
@gunbai-bot
gunbai-bot Bot merged commit 45d9fbd into main Aug 31, 2026
6 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/still-swift-46 branch August 31, 2026 22:53
@briansrls
briansrls restored the session/still-swift-46 branch August 31, 2026 22:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant