Skip to content

witness: freemonoid supplemental Clone-bound impls (row 1a, expected red) - #8525

Closed
briansrls wants to merge 4 commits into
mainfrom
witness/freemonoid-supplemental-clone-bound
Closed

briansrls wants to merge 4 commits into
mainfrom
witness/freemonoid-supplemental-clone-bound

Conversation

@briansrls

@briansrls briansrls commented Aug 19, 2026 •

Copy link
Copy Markdown
Contributor

What this PR is

Witness-only addition for row 1a of the CommutativeSemiring serde-bound E0277 effort (node adhoc-09c47958-545). Adds exactly two new rows to the existing, already-enrolled file dag/test/claim/generic_item_clone_bound_witness_test.dag:

  • freemonoid_supplemental_struct_hand_written_impls
  • freemonoid_supplemental_enum_hand_written_impls

These exercise the row-1a target shapes directly — a struct and an enum whose only Clone-requiring field is FreeMonoid<T> (repr-grounds to Rc<im::Vector<T>>), matching FreeMonoidUniqueState<T> / ListTailResult<T> in src/v2/std/algebra.dag — through v1_emit_struct_from_capability_table / v1_emit_enum_supplemental_impls end to end, rather than the pre-existing structural/WF fixpoint checks above them in the same file.

No emitter files are touched. Neither forbidden file (src/v1/05_emit_rust.dag, src/v1/trait_derive_emit.dag) is touched. No repair code lands here.

Expected status: BOTH NEW ROWS ARE RED, ON PURPOSE

Both freemonoid_supplemental_struct_hand_written_impls and freemonoid_supplemental_enum_hand_written_impls are EXPECTED RED until the row-1a repair lands. compile.emit succeeds (the emitter does not refuse); the assertions fail because today's emission still puts a blanket T: Clone bound on the item-level header instead of the target shape (bare header + hand-written Debug/PartialEq with a supplemental T: Clone bound scoped to just that impl + #[derive(Serialize, Deserialize)] with #[serde(bound(...))]). This is the discriminating RED the packet cites as evidence the target shape is not yet produced.

Re-verified from a clean instrument (fresh detached worktree at origin/main, zero working-tree diff outside this file, local build) immediately before opening this PR:

  • freemonoid_supplemental_struct_hand_written_impls: FAIL (red for cause; compile.emit succeeds)
  • freemonoid_supplemental_enum_hand_written_impls: FAIL (red for cause; compile.emit succeeds)
  • unbounded_declared_container_negative_control: PASS

Why the pre-existing negative control still passes, and is not superseded

unbounded_declared_container_negative_control (pre-existing row, unmodified here) asserts only item-level header bareness on an unrelated fixture (type FreeMonoidOnly<T> { ancestors: FreeMonoid<T> }) — that the header stays struct FreeMonoidOnly<T>, never struct FreeMonoidOnly<T: Clone>. The row-1a repair this witness targets never touches item-header bareness; it only changes which trait impls are hand-written vs. derived, and adds a #[serde(bound(...))] attribute. So this control's subject is disjoint from the new rows' subject, it keeps passing both before and after the eventual repair, and it needs no retirement receipt.

Enrollment route (confirmed, not assumed)

CI's only witness mechanism is claim_executor --required-floor --source-root dag --source-root src/v2 (gunbc.witness_floor_workflow → .github/workflows/witnesses.yml), which discovers every test fn in every .dag file under the dag and src/v2 roots via run_required_floor (src/v1/stage0/src/cli_run.rs:39590) and folds them through one prepared subject — no plan entry, no selection flag, no manual roster edit required.

This file (dag/test/claim/generic_item_clone_bound_witness_test.dag) is already discovered and already executing its pre-existing rows today. Its module identity (test.claim.generic_item_clone_bound_witness_test) does not match any long_home_prefixes exclusion (test.claim.long., v2.test.long., v2.test.claim.long.), so it is not routed to the excluded long-home lane. The two new test fn declarations are therefore picked up automatically by the existing directory-scan discovery the next time the required-floor fold runs — no additional wiring needed.

This PR was opened in draft (auto-attached by the dashboard); flipping to ready now since the addition is complete and self-contained.

…d emission (row 1a)

freemonoid_supplemental_struct_hand_written_impls and
freemonoid_supplemental_enum_hand_written_impls assert the target repair
shape for FreeMonoidUniqueState<T>/ListTailResult<T>-like items whose only
Clone-requiring field is std.algebra.FreeMonoid<T>: a bare item-level
header, hand-written Debug/PartialEq impls carrying a supplemental
T: Clone bound, and #[serde(bound(...))] on the still-derived
Serialize/Deserialize. Both are EXPECTED RED until the row-1a repair
lands — verified by execution on a clean origin/main build
(compile.emit succeeds; the includes/excludes assertions fail because
today's emission is item-level-unbounded, not per-impl-bounded).

unbounded_declared_container_negative_control is unaffected and still
passes: it locks in header bareness for an unbounded external
container, which the row-1a repair does not touch (only impl blocks
and the serde bound attribute change).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title E0277: 16 per-derived-impl bound rows (CommutativeSemiring<Magnitude> serde obligations) — largest unowned population blocking the first compiling module witness: freemonoid supplemental Clone-bound impls (row 1a, expected red) Aug 19, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 19, 2026 06:31
Brian Searls and others added 2 commits August 19, 2026 07:19
Two independently-derived corrections to the FreeMonoid supplemental
Clone-bound witnesses, sourced from im 15.1.0's actual Vector<A> trait
impls (raw source + rustdoc) and serde's documented #[serde(bound(..))]
splice scoping, never from the target emitter's current output:

- Hand-written Debug/PartialEq impl headers must carry the union of the
  supplemental T: Clone bound and the structural bound their own body
  needs (T: Clone + Debug, T: Clone + PartialEq) -- bare, since Clone/
  Debug/PartialEq are Rust prelude traits already in scope.
- serde bound strings must spell fully-qualified serde::Serialize /
  serde::Deserialize<'de> -- these are not prelude traits and the bound
  string resolves in the emitted module's own (import-free) scope.
- im_15_1_0_vector_debug_impl_authority gets its own dedicated,
  symbol-anchored rustdoc citation instead of aliasing the generic
  extdeps_external_authority_anchor placeholder.

Re-verified wet on a clean remote build: both corrected witnesses
remain FAIL (red for cause, documenting the as-yet-unimplemented
emitter capability) and the negative control still PASSes.
…e list

FreeMonoid<T> is a shared type and realizes as Rc<Vec<T>>; std::rc::Rc<T>
never implements Copy for any T (doc.rust-lang.org/std/rc/struct.Rc.html
lists Clone but not Copy), and Copy derive requires every field's type to
implement Copy (doc.rust-lang.org/std/marker/trait.Copy.html). #[derive(Copy)]
on a type with an Rc-realized field is therefore uncompilable Rust — rustc
E0277/E0204 on every instantiation of T — independent of and prior to any
emitter's current behavior. The struct row's must-contain derive string now
omits Copy, and a must-not-contain entry pins the old (wrong) spelling so it
cannot silently reappear. Re-verified wet: both row-1a witnesses still FAIL
as expected (the hand-written Debug/PartialEq capability under test remains
unimplemented), so this correction does not accidentally turn the row green.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as draft August 19, 2026 10:07
…Debug, not bare)

std::fmt::Debug is not a prelude trait. doc.rust-lang.org/std/prelude/index.html's
prelude-contents listing has no std::fmt::Debug entry; the only `Debug` the prelude
brings into scope is the derive macro std::prelude::v1::Debug, a distinct namespace
citizen. A bare `T: Debug` bound in a module with no explicit `use std::fmt::Debug;`
therefore resolves the name to the macro, and rustc refuses with
error[E0404]: expected trait, found derive macro `Debug`.

Clone and PartialEq are unaffected: the same prelude page lists std::clone::Clone
and std::cmp::PartialEq as re-exported trait names, so the bare bound spelling for
those two is correct as-is.

Fixed both row-1a witnesses' hand-written-Debug-impl bound assertions
(FreeMonoidSupplementalStruct and ListTailResultLike) from
`impl<T: Clone + Debug> std::fmt::Debug for ...` to
`impl<T: Clone + std::fmt::Debug> std::fmt::Debug for ...`, matching the qualification
already present in the `for` clause. Added must-not-contain pins on the old bare-bound
spelling so it cannot silently regress. Updated the rationale note with the same
independent basis. Re-verified wet: both witnesses still FAIL as expected -- the
hand-written Debug/PartialEq-excluded-from-derive capability under test remains
unimplemented in the emitter.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

CI failure on this check is expected and by design, not a defect -- no fix is being pushed.

The witnesses job fails on exactly the two witnesses this PR adds:
required-floor: FAIL test.claim.generic_item_clone_bound_witness.freemonoid_supplemental_struct_hand_written_impls returned Bool(false)
required-floor: FAIL test.claim.generic_item_clone_bound_witness.freemonoid_supplemental_enum_hand_written_impls returned Bool(false)

Both are row-1a "expected red" oracles: they assert the hand-written Debug/PartialEq-impl shape the emitter is supposed to produce for FreeMonoid-containing generic types, and that capability does not exist in the emitter yet. A green result here would mean the fixture stopped testing the real behavior, not that anything improved.

Per smart-ram-730's standing ruling, this PR is deliberately parked as draft and must never merge standalone -- merging it alone would land two knowingly-red witnesses on main with no mechanism to satisfy them, which is exactly what this failing check reflects. It lands atomically via cherry-pick into the row-1a mechanism PR (swift-moth-294's lane) once that capability is implemented, at which point these two witnesses are expected to flip to PASS with zero fixture changes.

No action needed here until that mechanism PR is ready.

@gunbai-bot

gunbai-bot Bot commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

Retiring this PR unmerged. Row 1a was dropped from #8534 (swift-moth-294, by parent ruling) -- it lands as Row 3 only, and E0277/E0369 are already zero on main via #8539's Clone-bound call-forwarding work with no FreeMonoid supplemental-bound mechanism present. The open question that sank row 1a was whether #8539's approach generalizes to the FreeMonoid supplemental case; that question is undecided today and gets settled by execution whenever a real FreeMonoid-field closure next appears, not by landing an untested mechanism now.

That leaves this oracle asserting behavior no mechanism on main implements or is scheduled to implement. Per DESIGN.md's evidence-retirement rule (S3/S4b: a witness whose only subject is behavior the tree doesn't carry is retired with a receipt, never left standing -- otherwise it becomes enrolled-but-can-never-pass, exactly the required-floor CI failure this branch has been showing), the correct disposition is retire, not merge-as-red and not indefinite-draft-park.

What this closes with, for the record: the oracle was verified correct by execution against swift-moth-294's mechanism commits (fce0b6d, 80aea09, 709e72e) before those were dropped from #8534 -- all three rows passed, including the negative control. Four independently-sourced corrections landed on this branch (Copy-on-Rc-field via rustc/std::rc::Rc docs, Debug-prelude/E0404 via doc.rust-lang.org/std/prelude), none copied from emitter output. This branch (witness/freemonoid-supplemental-clone-bound) and its commit history remain as quarry: the discriminating fixture and its derivation trail are here, cheap to resurrect, if/when a real FreeMonoid supplemental-bound site makes the row 1a question decidable again.

Closing without merge.

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