Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 45 additions & 1 deletion dag/extdeps/languages/rust/derive_contracts.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,14 @@ import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Https, Uri }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import std.disposition { Disposition, Scaffold, SingleAuthority }
import std.trait_derive_shape {
ReprGroundingDeriveTrait,
ReprDeriveDebug,
ReprDeriveClone,
ReprDerivePartialEq,
ReprDeriveSerialize,
ReprDeriveDeserialize,
}

data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
Expand All @@ -12,7 +20,12 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
}
}

data im_15_1_0_vector_debug_impl_authority: ExternalAuthority = extdeps_external_authority_anchor
data im_15_1_0_vector_debug_impl_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
locator: "docs.rs/im/15.1.0/im/vector/struct.Vector.html#impl-Debug-for-Vector%3CA%3E"
}
}

data im_15_1_0_vector_clone_impl_authority: ExternalAuthority = ExternalAuthority {
uri: Uri {
Expand Down Expand Up @@ -84,6 +97,37 @@ data serde_1_0_228_hash_set_deserialize_authority: ExternalAuthority = ExternalA
}
}

data rust_vec_freemonoid_supplemental_generic_bound_rows_note: String = "SINGLE AUTHORITY for the trait -> supplemental-generic-bound facts of the FreeMonoid/Vec realization (im-15.1.0 im::Vector): deriving Debug, PartialEq, Serialize or Deserialize for an item carrying an im::Vector<P> field additionally requires P: Clone, because each of those upstream impls is conditional on A: Clone (cited per row). Clone itself is deliberately NOT a row: derive(Clone) emits a conditional impl whose own A: Clone requirement is exactly im::Vector's, so no supplemental fact exists for it (im_15_1_0_vector_clone_impl_authority documents the upstream impl, consumed by the v2 contract map's requirement-free Clone entry). This module is dag-rooted so BOTH pools read one authority: the v1 seed emitter (regen pool [src/v1, dag]) consumes these rows in v1.compiler.trait_derive_emit, and v2.extdeps.languages.rust builds its typed target_model contract map (rust_vec_supplemental_generic_bound_contracts) by folding these same rows — the mapping formerly restated there is collapsed onto this list (coordinating-session ruling, smart-ram-730 (a session, not the operator) 2026-08-19: consume, do not mint a second copy or a witness to police one)."

type RustVecSupplementalGenericBoundRow {
derive_trait: ReprGroundingDeriveTrait
required: ReprGroundingDeriveTrait
authority: ExternalAuthority
}

data rust_vec_freemonoid_supplemental_generic_bound_rows: List<RustVecSupplementalGenericBoundRow> = [
RustVecSupplementalGenericBoundRow {
derive_trait: ReprDeriveDebug
required: ReprDeriveClone
authority: im_15_1_0_vector_debug_impl_authority
},
RustVecSupplementalGenericBoundRow {
derive_trait: ReprDerivePartialEq
required: ReprDeriveClone
authority: im_15_1_0_vector_partial_eq_impl_authority
},
RustVecSupplementalGenericBoundRow {
derive_trait: ReprDeriveSerialize
required: ReprDeriveClone
authority: im_15_1_0_vector_serialize_impl_authority
},
RustVecSupplementalGenericBoundRow {
derive_trait: ReprDeriveDeserialize
required: ReprDeriveClone
authority: im_15_1_0_vector_deserialize_impl_authority
},
]

type RustSupplementalGenericBoundContractCoverageDisposition {
owner: DeclarationRef
lane: DeclarationRef
Expand Down
9 changes: 5 additions & 4 deletions dag/extdeps/languages/rust/emit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -444,11 +444,12 @@ fn rust_pair_completion_body_render(body: PairCompletionBody) -> String {
}
}

fn rust_pair_completion_impl_render(row: PairCompletionOpRow) -> String {
fn rust_pair_completion_impl_render(row: PairCompletionOpRow, carrier_param_needs_clone: Bool) -> String {
match rust_pair_completion_spelling_for(row.op) {
Present { value: spelling } =>
concat(
"impl<M> ", spelling.trait_path, " for ", rust_pair_completion_carrier, "<M>",
if carrier_param_needs_clone { "impl<M: Clone> " } else { "impl<M> " },
spelling.trait_path, " for ", rust_pair_completion_carrier, "<M>",
if spelling.where_bounds == "" {
" {\n"
} else {
Expand All @@ -474,13 +475,13 @@ fn rust_pair_completion_impl_render(row: PairCompletionOpRow) -> String {
}
}

fn rust_supplemental_impls_group_completion() -> String {
fn rust_supplemental_impls_group_completion(carrier_param_needs_clone: Bool) -> String {
concat(
"\n// repr-grounding arm (b): GroupCompletion<M> carrier arithmetic, rendered from the\n",
"// pair-completion rows in std.trait_derive_shape (Add/Mul/Neg are row data; Sub/Div bodies\n",
"// remain keyed literals: only Add, Mul and Neg render from the PairCompletionSumOfProducts polynomial arms).\n",
pair_completion_op_rows()
|> map(row => rust_pair_completion_impl_render(row))
|> map(row => rust_pair_completion_impl_render(row: row, carrier_param_needs_clone: carrier_param_needs_clone))
|> join(separator: "")
)
}
Expand Down
25 changes: 25 additions & 0 deletions dag/test/claim/fn_equality_bound_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module test.claim.fn_equality_bound_witness

import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

data fn_equality_bound_witness_note: String = "Executing floor witness for the FN-level PartialEq bound trigger (v1.compiler.emit_rust v1_fn_body_equality_bound_param_names, deciding via v1.compiler.trait_bound_witness v1_equality_bound_param_name). The emitter derives Clone bounds on generic fn params ~30-48 references deep but derived NOTHING for equality, so a generic fn comparing two values of its own type param emitted bare and rustc refused with E0369 'binary operation == cannot be applied to type K'. GROUNDING FOR THE EXPECTED SPELLING, so it is not a measurement copied from this tree: quick-lynx-620 measured the requirement against rustc on the real emission -- hand-adding the bound to the emitted mirror and rebuilding the seed gave zero errors, and the required rendering is `K: Clone + PartialEq`, the equality bound COMPOSING with the separately-derived Clone bound on the same parameter rather than replacing it. THE DISCRIMINATOR IS TYPE RESOLUTION, NOT THE == SPELLING, and the two rows below exist to prove the trigger cannot be satisfied by matching on the operator. earning_comparison_bounds_its_generic_param carries BOTH comparisons in one body, exactly the shape of the real specimen: a concrete closed-enum comparison that must earn nothing, and a comparison of two K values that must earn the bound -- rustc emits exactly ONE E0369 on that real shape, at the second comparison, so the first provably compiles unbounded today. concrete_only_comparison_leaves_generic_param_bare is the sharper negative: a fn that HAS a generic param and HAS a comparison, where the comparison involves only concrete types. A predicate keyed on the presence of == bounds K there and breaks every caller instantiating K with a non-PartialEq type; the type-resolving predicate must leave it bare. That row is what makes the pair discriminating rather than two positives, and it is why the refusals below assert the bounded spelling is ABSENT rather than merely asserting some other spelling is present. Over-approximation is not free here: adding a bound TIGHTENS the emitted signature, so a spurious bound is a real break, while a missed bound only leaves the pre-existing E0369 in place."

fn earning_comparison_bounds_its_generic_param() -> Bool {
compile_dag_rust_emit_check(
"module fn_equality_witness.earning\n\ntype ShapeTag = ShapeAlpha | ShapeBeta\n\ntype CapRow<K> {\n shape: ShapeTag\n keys: List<K>\n}\n\nfn cap_row_has<K>(row: CapRow<K>, shape: ShapeTag, key: K) -> Bool {\n row.shape == shape && (row.keys |> any(k => k == key))\n}\n",
"src/fn_equality_witness_earning.rs",
["fn cap_row_has<K: Clone + PartialEq>"],
["fn cap_row_has<K>", "fn cap_row_has<K: Clone>"]
)
}

fn concrete_only_comparison_leaves_generic_param_bare() -> Bool {
compile_dag_rust_emit_check(
"module fn_equality_witness.concrete\n\ntype ShapeTag = ShapeAlpha | ShapeBeta\n\ntype CapRow<K> {\n shape: ShapeTag\n keys: List<K>\n}\n\nfn cap_row_shape_is<K>(row: CapRow<K>, shape: ShapeTag) -> Bool {\n row.shape == shape\n}\n",
"src/fn_equality_witness_concrete.rs",
["fn cap_row_shape_is"],
["K: PartialEq", "K: Clone + PartialEq"]
)
}
52 changes: 52 additions & 0 deletions dag/test/claim/generic_item_clone_bound_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -255,3 +255,55 @@ test fn fn_nested_phantom_wrapper_negative_control() -> Bool {
test fn fn_nested_value_wrapper_positive_control() -> Bool {
w_fn_nested_value_wrapper_gets_clone()
}

data freemonoid_supplemental_impl_witness_note: String = "Row 1a target shapes (FreeMonoidUniqueState<T>, ListTailResult<T> in src/v2/std/algebra.dag), exercising v1_emit_struct_from_capability_table / v1_emit_enum_supplemental_impls end to end rather than the pre-existing structural/WF fixpoint above: a struct or enum whose only Clone-requiring field is FreeMonoid<T> keeps a BARE item-level header (the derive/WF triggers above never fire for an undeclared external container), Debug and PartialEq are realized as hand-written impls instead of #[derive(..)] (v1_exclude_hand_written_freemonoid_traits drops them from the derive list), each impl header carrying the UNION of the supplemental T: Clone bound and the structural bound its own body needs (T: Clone + std::fmt::Debug for the hand-written Debug impl, T: Clone + PartialEq for the hand-written PartialEq impl). Clone and PartialEq are bare, not path-qualified, because both are prelude traits (std::prelude::v1 re-exports std::clone::Clone and std::cmp::PartialEq by their trait names -- confirmed against doc.rust-lang.org/std/prelude/index.html's prelude-contents listing). Debug is NOT: that page's listing has no std::fmt::Debug entry at all, and the only `Debug` the prelude brings into scope is the derive macro std::prelude::v1::Debug -- a distinct namespace citizen from the trait. 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`, on every hand-written Debug impl this mechanism emits -- independent of and prior to any emitter's behavior. The bound is path-qualified (T: Clone + std::fmt::Debug) for exactly this reason, matching the `for` clause's existing std::fmt::Debug qualification rather than leaving the bound and the `for` position spelled two different ways for the same trait. Serialize/Deserialize stay #[derive(..)] with a #[serde(bound(..))] override naming every item generic param against the fully-qualified serde::Serialize / serde::Deserialize<'de> paths (serde's traits are not in the emitted module's scope by bare name either, so an unqualified bound string would fail to resolve). The struct row's derive list carries Clone but never Copy: FreeMonoid<T> is a shared type and realizes as Rc<Vec<T>> (v1_emit_struct_derives selects the heap roster over the copy roster on exactly that membership), and std::rc::Rc<T> does not implement Copy for any T regardless of T's own bounds -- confirmed against doc.rust-lang.org/std/rc/struct.Rc.html's trait-implementation list (Clone present, Copy absent) and doc.rust-lang.org/std/marker/trait.Copy.html's field requirement (every field's type must implement Copy). #[derive(Copy)] on a type with an Rc field is therefore not a spelling choice but rustc E0277/E0204 (\"the trait Copy cannot be implemented for this type\", naming the Rc-realized field) on every instantiation of T, independent of and prior to any emitter's behavior -- the corrected list is the ONLY one a correct implementation of the mechanism under test could produce. w_freemonoid_supplemental_struct_hand_written_impls and w_freemonoid_supplemental_enum_hand_written_impls assert all four facts positively (bare item header, hand-written impl headers carrying the full bound union with Debug path-qualified in the bound, fully-qualified serde bound attr) and negatively (no bounded item header, no naive #[derive(Debug...)] reintroducing the excluded traits, no bare-Debug-in-bound spelling that would resolve to the derive macro, no Copy in the struct's derive list). The struct witness additionally asserts both impl BODIES, not only their headers: correct headers over an empty or wrong body would otherwise satisfy every other assertion here -- a PartialEq whose body is literally `true` passes a header-only witness, and the enum witness's body assertions would catch that only by being the more thorough of the pair, which is luck rather than coverage wherever the struct and enum emission paths can diverge. The body spellings are grounded independently of this emitter: the `&self.<field>` access form and the `fn eq(&self, other: &Self) -> bool` signature come from the pre-existing NonEmptyVec hand-written impls the runtime prelude already emits . That same precedent independently corroborates the two impl HEADERS asserted above, which is worth stating separately because it was not the reason the precedent was consulted: the runtime prelude emits `impl<T: Clone + std::fmt::Debug> std::fmt::Debug for NonEmptyVec<T>`, character-for-character the shape of the third include here, authored before this change existed and by a different mechanism -- so those two header assertions are precedent-backed rather than author-chosen, which matters because every other assertion in this witness was authored by the same session that authored the emitter under test. And `debug_struct(..).field(..).finish()` is the std::fmt::Formatter builder documented for named-field structs, the named-field counterpart of the debug_tuple form NonEmptyVec uses for its tuple field. If this emitter disagrees with those spellings the emitter is what changes, not these strings. Two known limits of this witness, recorded so neither is mistaken for coverage: the include assertions are SPELLING-sensitive, so a semantically identical `impl<T> Debug for X<T> where T: Clone + Debug` would fail include 3 -- normal for a golden, but it means a red here is not by itself evidence of a semantic defect; and the `#[derive(Debug` exclude matches anywhere in the emitted file, which is safe only because this fixture declares a single type -- a future fixture carrying two types would silently weaken it to a file-wide rather than per-item assertion. Finally, on this row's own representation: the bulk of it is CITATIONS, which section 4c places in a typed carrier rather than in prose, so its eventual destination is not a leading // block either -- a comment is exactly as unreadable to a machine as this String, and both are the same deferral in different syntax. It is left as-is deliberately: converting this row alone, while the other rows in this file and the rest of the corpus keep the String form, would author a third representation rather than remove one."

fn w_freemonoid_supplemental_struct_hand_written_impls() -> Bool {
compile_dag_rust_emit_check(
"module generic_item_witness.freemonoid_supplemental_struct\nimport std.algebra { FreeMonoid }\n\ntype FreeMonoidSupplementalStruct<T> {\n seen: FreeMonoid<T>\n unique: Bool\n}\n",
"src/generic_item_witness_freemonoid_supplemental_struct.rs",
[
"struct FreeMonoidSupplementalStruct<T>",
"#[derive(Clone, serde::Serialize, serde::Deserialize)]\n#[serde(bound(serialize = \"T: Clone + serde::Serialize\", deserialize = \"T: Clone + serde::Deserialize<'de>\"))]",
"impl<T: Clone + std::fmt::Debug> std::fmt::Debug for FreeMonoidSupplementalStruct<T>",
"impl<T: Clone + PartialEq> PartialEq for FreeMonoidSupplementalStruct<T>",
"f.debug_struct(\"FreeMonoidSupplementalStruct\").field(\"seen\", &self.seen).field(\"unique\", &self.unique).finish()",
"self.seen == other.seen && self.unique == other.unique"
],
[
"struct FreeMonoidSupplementalStruct<T: Clone>",
"#[derive(Debug",
"derive(Clone, Copy, PartialEq",
"#[derive(Clone, Copy, serde::Serialize, serde::Deserialize)]",
"impl<T: Clone + Debug> std::fmt::Debug for FreeMonoidSupplementalStruct<T>"
]
)
}

fn w_freemonoid_supplemental_enum_hand_written_impls() -> Bool {
compile_dag_rust_emit_check(
"module generic_item_witness.freemonoid_supplemental_enum\nimport std.algebra { FreeMonoid }\n\ntype ListTailResultLike<T>\n = TailFound { tail: FreeMonoid<T> }\n | TailAbsent\n",
"src/generic_item_witness_freemonoid_supplemental_enum.rs",
[
"enum ListTailResultLike<T>",
"#[derive(Clone, serde::Serialize, serde::Deserialize)]\n#[serde(bound(serialize = \"T: Clone + serde::Serialize\", deserialize = \"T: Clone + serde::Deserialize<'de>\"))]",
"impl<T: Clone + std::fmt::Debug> std::fmt::Debug for ListTailResultLike<T>",
"impl<T: Clone + PartialEq> PartialEq for ListTailResultLike<T>",
"Self::TailFound { tail } => f.debug_struct(\"TailFound\").field(\"tail\", tail).finish(),",
"(Self::TailFound { tail: a_tail }, Self::TailFound { tail: b_tail }) => a_tail == b_tail,"
],
[
"enum ListTailResultLike<T: Clone>",
"#[derive(Debug",
"impl<T: Clone + Debug> std::fmt::Debug for ListTailResultLike<T>"
]
)
}

test fn freemonoid_supplemental_struct_hand_written_impls() -> Bool {
w_freemonoid_supplemental_struct_hand_written_impls()
}

test fn freemonoid_supplemental_enum_hand_written_impls() -> Bool {
w_freemonoid_supplemental_enum_hand_written_impls()
}
Loading
Loading