Skip to content
3 changes: 3 additions & 0 deletions dag/extdeps/languages/rust/emit.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import std.trait_derive_shape {
ReprDeriveEq,
ReprDerivePartialOrd,
ReprDeriveOrd,
ReprDeriveHash,
ReprDeriveSerialize,
ReprDeriveDeserialize,
ReprDeriveAdd,
Expand Down Expand Up @@ -118,6 +119,7 @@ fn rust_trait_derive_spelling(derive_trait: ReprGroundingDeriveTrait) -> String
ReprDeriveEq => "Eq"
ReprDerivePartialOrd => "PartialOrd"
ReprDeriveOrd => "Ord"
ReprDeriveHash => "std::hash::Hash"
ReprDeriveSerialize => "serde::Serialize"
ReprDeriveDeserialize => "serde::Deserialize"
ReprDeriveAdd => "std::ops::Add"
Expand Down Expand Up @@ -345,6 +347,7 @@ fn rust_pair_completion_op_key(op: ReprGroundingDeriveTrait) -> String {
ReprDeriveEq => "eq"
ReprDerivePartialOrd => "partial_ord"
ReprDeriveOrd => "ord"
ReprDeriveHash => "hash"
ReprDeriveSerialize => "serialize"
ReprDeriveDeserialize => "deserialize"
}
Expand Down
100 changes: 100 additions & 0 deletions dag/std/trait_derive_shape.dag
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ type ReprGroundingDeriveTrait
| ReprDeriveEq
| ReprDerivePartialOrd
| ReprDeriveOrd
| ReprDeriveHash
| ReprDeriveSerialize
| ReprDeriveDeserialize
| ReprDeriveAdd
Expand Down Expand Up @@ -50,6 +51,7 @@ fn repr_grounding_derive_shape_has_trait(
ReprDeriveEq => true
ReprDerivePartialOrd => true
ReprDeriveOrd => true
ReprDeriveHash => true
ReprDeriveSerialize => true
ReprDeriveDeserialize => true
_ => false
Expand All @@ -63,6 +65,7 @@ fn repr_grounding_derive_shape_has_trait(
ReprDeriveEq => true
ReprDerivePartialOrd => true
ReprDeriveOrd => true
ReprDeriveHash => true
ReprDeriveSerialize => true
ReprDeriveDeserialize => true
ReprDeriveAdd => true
Expand All @@ -81,6 +84,7 @@ fn repr_grounding_derive_shape_has_trait(
ReprDeriveEq => true
ReprDerivePartialOrd => true
ReprDeriveOrd => true
ReprDeriveHash => true
ReprDeriveSerialize => true
ReprDeriveDeserialize => true
_ => false
Expand All @@ -94,6 +98,7 @@ fn repr_grounding_derive_shape_has_trait(
ReprDeriveEq => true
ReprDerivePartialOrd => true
ReprDeriveOrd => true
ReprDeriveHash => true
ReprDeriveSerialize => true
ReprDeriveDeserialize => true
_ => false
Expand All @@ -107,6 +112,7 @@ fn repr_grounding_derive_shape_has_trait(
ReprDeriveEq => true
ReprDerivePartialOrd => true
ReprDeriveOrd => true
ReprDeriveHash => true
ReprDeriveSerialize => true
ReprDeriveDeserialize => true
_ => false
Expand All @@ -119,6 +125,7 @@ fn repr_grounding_derive_shape_has_trait(
ReprDeriveEq => true
ReprDerivePartialOrd => true
ReprDeriveOrd => true
ReprDeriveHash => true
ReprDeriveSerialize => true
ReprDeriveDeserialize => true
_ => false
Expand All @@ -128,6 +135,8 @@ fn repr_grounding_derive_shape_has_trait(
ReprDeriveDebug => true
ReprDeriveClone => true
ReprDerivePartialEq => true
ReprDeriveEq => true
ReprDeriveHash => true
ReprDeriveSerialize => true
ReprDeriveDeserialize => true
_ => false
Expand All @@ -136,6 +145,20 @@ fn repr_grounding_derive_shape_has_trait(
}
}

// Eq and Hash on a payload coproduct are CAPABILITY rows, not roster rows, and the distinction is why
// they read false until the usage-derived requirement needed them. The capability table answers what a
// shape CAN derive; the roster answers what it DOES. Rust derives Eq and Hash on an enum with payloads
// exactly as it derives PartialEq — the macro emits an impl bounded by the payload types, so the
// capability is the payload types' problem and not the enum shape's, and PartialEq was already true
// here for that same reason. Setting these false conflated the two questions: it said the shape cannot
// support the trait when the fact was only that payload_coproduct_derive_traits does not ask for it.
// The rows change no existing emission, because the completeness predicate is evaluated against the
// roster actually chosen and that roster is unchanged; what they unblock is a payload coproduct
// reaching a map-key position, which before this refused with compile_error! at a shape that could
// have carried the derive. Where a payload genuinely is not Eq or Hash — a Float, a callable field —
// the emitted impl fails at rustc with a located E0277 against the offending payload, which is a
// better refusal than one against the enum, because it names the field that cannot hold rather than
// the shape that could.
fn repr_grounding_derive_completeness_predicate(
required: List<ReprGroundingDeriveTrait>,
shape: ReprGroundingDeriveElemShape
Expand Down Expand Up @@ -251,6 +274,83 @@ fn payload_coproduct_derive_traits() -> List<ReprGroundingDeriveTrait> {
}
}

// USAGE-DERIVED half of the roster, distinct from the SHAPE-derived rosters above and additive to
// them. The rosters above answer what a type's own structure can support; they cannot answer what a
// type's USE demands, so a record reaching a keyed-collection key position carries a requirement no
// shape classification produces. map_key_required_derive_traits names that requirement once: a keyed
// collection realized as a hash map bounds its key parameter by Hash + Eq (im 15.1.0 HashMap<K, V>
// declares K: Hash + Eq, matching std::collections::HashMap), so the key type must derive both. The
// requirement is target-agnostic here and spelled per target in extdeps.languages.rust.emit. Union is
// append-only and idempotent (derive_traits_union), so a type that already earns a trait from its
// shape roster gains nothing and its emitted bytes do not move — the asymmetry a fixed wider roster
// cannot express: a Symbol-wrapped ord carrier already derives Eq and needs only Hash, while a plain
// record needs both. NOT the same axis as the Ord requirement BTreeSet elements carry
// (rust_btree_set_element_ord_eligible), which is answered today by refusing at the use site rather
// than by propagating to the declaration; unifying the two on this fn is the named next step and
// deliberately not taken here.
fn phantom_opaque_carrier_derive_traits() -> List<ReprGroundingDeriveTrait> {
Cons {
head: ReprDeriveDebug,
tail: Cons {
head: ReprDeriveClone,
tail: Cons {
head: ReprDeriveCopy,
tail: Cons {
head: ReprDerivePartialEq,
tail: Cons {
head: ReprDeriveEq,
tail: Cons {
head: ReprDeriveSerialize,
tail: Cons { head: ReprDeriveDeserialize, tail: Empty }
}
}
}
}
}
}
}

fn map_key_required_derive_traits() -> List<ReprGroundingDeriveTrait> {
Cons { head: ReprDeriveEq, tail: Cons { head: ReprDeriveHash, tail: Empty } }
}

fn repr_grounding_derive_trait_rank(derive_trait: ReprGroundingDeriveTrait) -> Int {
match derive_trait {
ReprDeriveDebug => 0
ReprDeriveClone => 1
ReprDeriveCopy => 2
ReprDerivePartialEq => 3
ReprDeriveEq => 4
ReprDerivePartialOrd => 5
ReprDeriveOrd => 6
ReprDeriveHash => 7
ReprDeriveSerialize => 8
ReprDeriveDeserialize => 9
ReprDeriveAdd => 10
ReprDeriveSub => 11
ReprDeriveMul => 12
ReprDeriveDiv => 13
ReprDeriveRem => 14
ReprDeriveNeg => 15
}
}

fn derive_traits_contain(
traits: List<ReprGroundingDeriveTrait>,
derive_trait: ReprGroundingDeriveTrait
) -> Bool {
traits |> any(t => repr_grounding_derive_trait_rank(t) == repr_grounding_derive_trait_rank(derive_trait))
}

fn derive_traits_union(
base: List<ReprGroundingDeriveTrait>,
extra: List<ReprGroundingDeriveTrait>
) -> List<ReprGroundingDeriveTrait> {
extra |> fold(init: base, f: (acc, t) =>
if derive_traits_contain(traits: acc, derive_trait: t) { acc } else { concat(acc, [t]) }
)
}

fn kernel_int_arithmetic_traits() -> List<ReprGroundingDeriveTrait> {
Cons {
head: ReprDeriveAdd,
Expand Down
120 changes: 120 additions & 0 deletions dag/test/claim/map_key_derive_requirement_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
module test.claim.map_key_derive_requirement_witness

import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// Executing floor witness for the USAGE-DERIVED half of v1.compiler.trait_derive_emit derive selection
// (v1.compiler.trait_derive_emit v1_with_map_key_requirement). compile_dag_rust_emit_check is the
// enrolled consumer: it
// compiles an inline fixture through the real emit path and asserts emitted Rust spellings, so a claim
// here is green by execution rather than by declaration. THE SUBJECT: a type that reaches a keyed-
// collection key position must derive Eq + Hash, because the container Map lowers to im::HashMap whose
// key parameter is bounded K: Hash + Eq — a fact about the type's USE that no shape classification
// produces. Every positive row is paired with a control that must stay silent, because the failure
// mode this mechanism can have is not missing the requirement (rustc refuses loudly) but fabricating
// it on a type no one keys by, which nothing downstream would ever report.
// w_non_key_record_derives_no_hash is that control at record grain and
// w_map_value_position_does_not_seed is the sharper one: it puts the SAME type in the VALUE position
// of the same container, so a rule that keyed on 'mentioned by a Map' rather than 'occupies the key
// slot' goes red on it while every other row here stays green.
// w_map_key_requirement_propagates_to_field_types pins the fixpoint rather than a one-hop read, and
// w_nullary_coproduct_key_gains_only_hash pins the union's idempotence — a nullary coproduct already
// deriving Eq and Ord from its shape roster must gain Hash alone, which is the asymmetry a wider
// constant roster cannot express and the reason the union is append-only.
// w_fn_field_record_as_map_key_refuses pins the fail-closed arm: Rc<dyn Fn> is neither Eq nor Hash, so
// a callable-field record in a key position is refused with compile_error! rather than emitted with a
// derive that cannot hold.
fn w_map_key_record_earns_eq_and_hash() -> Bool {
compile_dag_rust_emit_check(
"module map_key_witness.keyed\n\ntype PositionKey {\n position: Int\n}\n\ntype MemoTable {\n entries: Map<PositionKey, Int>\n}\n",
"src/map_key_witness_keyed.rs",
["Eq, std::hash::Hash)]\npub struct PositionKey"],
[]
)
}

fn w_non_key_record_derives_no_hash() -> Bool {
compile_dag_rust_emit_check(
"module map_key_witness.unkeyed\n\ntype PlainRecord {\n position: Int\n}\n\ntype PlainHolder {\n held: PlainRecord\n}\n",
"src/map_key_witness_unkeyed.rs",
["pub struct PlainRecord"],
["std::hash::Hash"]
)
}

fn w_map_value_position_does_not_seed() -> Bool {
compile_dag_rust_emit_check(
"module map_key_witness.valued\n\ntype ValueOnly {\n payload: Int\n}\n\ntype ValueTable {\n entries: Map<String, ValueOnly>\n}\n",
"src/map_key_witness_valued.rs",
["pub struct ValueOnly"],
["std::hash::Hash"]
)
}

fn w_map_key_requirement_propagates_to_field_types() -> Bool {
compile_dag_rust_emit_check(
"module map_key_witness.propagate\n\ntype InnerLeaf {\n tag: Int\n}\n\ntype OuterKey {\n inner: InnerLeaf\n}\n\ntype PropagateTable {\n entries: Map<OuterKey, Int>\n}\n",
"src/map_key_witness_propagate.rs",
[
"Eq, std::hash::Hash)]\npub struct InnerLeaf",
"Eq, std::hash::Hash)]\npub struct OuterKey"
],
[]
)
}

fn w_fn_return_type_seeds_the_requirement() -> Bool {
compile_dag_rust_emit_check(
"module map_key_witness.returned\n\ntype ReturnedKey {\n tag: Int\n}\n\nfn empty_returned_table() -> Map<ReturnedKey, Int> {\n empty_map()\n}\n",
"src/map_key_witness_returned.rs",
["Eq, std::hash::Hash)]\npub struct ReturnedKey"],
[]
)
}

fn w_nullary_coproduct_key_gains_only_hash() -> Bool {
compile_dag_rust_emit_check(
"module map_key_witness.nullary_key\n\ntype ChoiceKey\n = ChoiceLeft\n | ChoiceRight\n\ntype ChoiceTable {\n entries: Map<ChoiceKey, Int>\n}\n",
"src/map_key_witness_nullary_key.rs",
["pub enum ChoiceKey", "Ord, serde::Serialize, serde::Deserialize, std::hash::Hash)]"],
["serde::Deserialize, Eq"]
)
}

fn w_fn_field_record_as_map_key_refuses() -> Bool {
compile_dag_rust_emit_check(
"module map_key_witness.callable\n\ntype CallableKey {\n step: fn(Int) -> Int\n}\n\ntype CallableTable {\n entries: Map<CallableKey, Int>\n}\n",
"src/map_key_witness_callable.rs",
["compile_error!"],
["std::hash::Hash)]\npub struct CallableKey"]
)
}

test fn map_key_record_earns_eq_and_hash() -> Bool {
w_map_key_record_earns_eq_and_hash()
}

test fn non_key_record_derives_no_hash() -> Bool {
w_non_key_record_derives_no_hash()
}

test fn map_value_position_does_not_seed() -> Bool {
w_map_value_position_does_not_seed()
}

test fn map_key_requirement_propagates_to_field_types() -> Bool {
w_map_key_requirement_propagates_to_field_types()
}

test fn fn_return_type_seeds_the_requirement() -> Bool {
w_fn_return_type_seeds_the_requirement()
}

test fn nullary_coproduct_key_gains_only_hash() -> Bool {
w_nullary_coproduct_key_gains_only_hash()
}

test fn fn_field_record_as_map_key_refuses() -> Bool {
w_fn_field_record_as_map_key_refuses()
}
4 changes: 4 additions & 0 deletions src/v1/04_emit_info.dag
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ type EmitGraphInfo {
read_only_params: Set<String>

clone_bounded_type_params: Map<String, Set<String>>
map_key_required_type_names: Set<String>
clone_impl_required_type_params: Map<String, Set<String>>

corpus_repr: RustCorpusRepr
Expand Down Expand Up @@ -122,6 +123,7 @@ fn empty_emit_graph_info() -> EmitGraphInfo {
read_only_params_index: empty_map(),
read_only_params: empty_set(),
clone_bounded_type_params: empty_map(),
map_key_required_type_names: empty_set(),
clone_impl_required_type_params: empty_map(),

corpus_repr: FaithfulFreeMonoid,
Expand All @@ -146,6 +148,7 @@ fn emit_info_with_fn_type_context(emit_info: EmitGraphInfo, generic_param_names:
read_only_params_index: emit_info.read_only_params_index,
read_only_params: emit_info.read_only_params,
clone_bounded_type_params: emit_info.clone_bounded_type_params,
map_key_required_type_names: emit_info.map_key_required_type_names,
clone_impl_required_type_params: emit_info.clone_impl_required_type_params,
corpus_repr: emit_info.corpus_repr,
fn_generic_param_names: generic_param_names,
Expand All @@ -169,6 +172,7 @@ fn emit_info_with_fn_return(emit_info: EmitGraphInfo, fn_return_type: Node?) ->
read_only_params_index: emit_info.read_only_params_index,
read_only_params: emit_info.read_only_params,
clone_bounded_type_params: emit_info.clone_bounded_type_params,
map_key_required_type_names: emit_info.map_key_required_type_names,
clone_impl_required_type_params: emit_info.clone_impl_required_type_params,
corpus_repr: emit_info.corpus_repr,
fn_generic_param_names: emit_info.fn_generic_param_names,
Expand Down
1 change: 1 addition & 0 deletions src/v1/04_infer.dag
Original file line number Diff line number Diff line change
Expand Up @@ -9572,6 +9572,7 @@ fn build_emit_graph_info(modules: List<TypedModule>, has_v1_seed: Bool) -> EmitG
read_only_params_index: empty_map(),
read_only_params: empty_set(),
clone_bounded_type_params: empty_map(),
map_key_required_type_names: empty_set(),
clone_impl_required_type_params: empty_map(),
corpus_repr: rust_corpus_repr(has_v1_seed: has_v1_seed),
fn_generic_param_names: [],
Expand Down
Loading
Loading