Skip to content
Merged
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
23 changes: 21 additions & 2 deletions dag/gunbc/instrument_targets.dag
Original file line number Diff line number Diff line change
Expand Up @@ -323,6 +323,19 @@ fn dag_emit_real_grammar_round_trips_entry() -> String {
"dag/gunbc/instruments/dag_emit_real_grammar_round_trips.dag"
}

// THE NATIVE EMISSION CONTROLS: one carrier per Rust-emitter rule, emitted, built and run by the
// NativeClaimDriver program gunbc.instruments.native_emission_controls. It is the executing evidence
// that a rule's emission is a compilable program with the right answers -- the half a textual
// witness over the emitted header cannot establish. Run by name, not a merge gate.
// `gunbc test //gunbc/instruments:native-emission-controls`.
fn native_emission_controls_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "native-emission-controls" } }
}

fn native_emission_controls_entry() -> String {
"dag/gunbc/instruments/native_emission_controls.dag"
}

// O(corpus) exact-head join of evaluation_store_address callers plus the fail-closed src/v2
// call-form scan. Not a DiscoverySelection floor witness (enrolment_bound_without_ceiling);
// not a required CI job. `gunbc test //gunbc/instruments:evaluation-store-address-exact-head`.
Expand Down Expand Up @@ -497,6 +510,10 @@ fn native_app_attest_binding() -> TargetBinding {
TargetBinding { target: native_app_attest_label() producer: NativeClaimProgramProducer { entry: native_app_attest_entry() } }
}

fn native_emission_controls_binding() -> TargetBinding {
TargetBinding { target: native_emission_controls_label() producer: NativeClaimProgramProducer { entry: native_emission_controls_entry() } }
}

fn dag_emit_real_grammar_round_trips_binding() -> TargetBinding {
TargetBinding { target: dag_emit_real_grammar_round_trips_label() producer: NativeClaimProgramProducer { entry: dag_emit_real_grammar_round_trips_entry() } }
}
Expand Down Expand Up @@ -652,7 +669,8 @@ fn instrument_targets() -> List<Label> {
required_lane_resolution_census_label(), bare_reference_channel_outcome_label(),
self_host_behavioral_equivalence_label(), dependency_demand_census_label(),
emitted_crate_workspace_label(),
native_crypto_vectors_label(), native_app_attest_label(), dag_emit_real_grammar_round_trips_label()
native_crypto_vectors_label(), native_app_attest_label(), dag_emit_real_grammar_round_trips_label(),
native_emission_controls_label()
]
}

Expand All @@ -667,7 +685,8 @@ fn instrument_bindings() -> List<TargetBinding> {
required_lane_resolution_census_binding(), bare_reference_channel_outcome_binding(),
self_host_behavioral_equivalence_binding(), dependency_demand_census_binding(),
emitted_crate_workspace_binding(),
native_crypto_vectors_binding(), native_app_attest_binding(), dag_emit_real_grammar_round_trips_binding()
native_crypto_vectors_binding(), native_app_attest_binding(), dag_emit_real_grammar_round_trips_binding(),
native_emission_controls_binding()
]
}

Expand Down
126 changes: 126 additions & 0 deletions dag/gunbc/instruments/native_emission_controls.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,126 @@
module gunbc.instruments.native_emission_controls

import std.types { Bool, List, Set, String }
import v2.std.algebra { filter }
import std.compiler_entry { CompilerEntryDriver, NativeClaimDriver, NativeClaimReport, NativeClaimTerminal, NativeClaimHeld, NativeClaimNotHeld }

// THE NATIVE EMISSION CONTROLS: one small carrier per Rust-emitter rule, EMITTED, BUILT AND RUN as a
// NativeClaimDriver entry (std.compiler_entry). `gunbc test //gunbc/instruments:native-emission-controls`
// emits this closure, builds it and runs it; nothing here is interpreted. A textual witness over the
// emitted header (test.claim.generic_item_clone_bound_witness) says what the emitter PRINTED; only
// rustc says whether what it printed is a program, and only a run says whether that program answers
// correctly. So each rule's control is a carrier whose emission did not compile before the rule and
// a set of cases over it whose answers are decided here -- a positive and a red per carrier, because
// an impl that compiled and answered `true` for everything would pass a positive alone.
//
// A CONTROL THAT STOPS COMPILING IS NO OBSERVATION FOR THE WHOLE PROGRAM, and that is the intended
// reading: every carrier in this module is one that must emit as compilable Rust, so one refusal at
// rustc is a red on the label rather than a missing row.
//
// THE ROSTER IS DECLARED, NOT DERIVED FROM THE CASES, for the reason
// gunbc.instruments.native_crypto_vectors states: the reader joins rows to this list by identity, so
// a case that was dropped is a missing row and not a smaller green.
data compiler_pipeline_entry: CompilerEntryDriver = NativeClaimDriver

// RULE: a hand-written impl header carries the item header's bounds (v1.compiler.trait_derive_emit
// v1_set_impl_type_params / v1_freemonoid_impl_type_params). ControlContext<C, P> is the shape of
// std.authorization_profile PublicationContext: P reaches a Set only through ControlAudience<P>, so
// Debug and PartialEq leave the derive list and are written by hand with `P: Ord`, while the bare
// `context: C` field earns `C: Clone` on the struct header. The hand-written headers used to print
// `impl<C: PartialEq, P: Ord + PartialEq>`, which rustc refuses at `ControlContext<C, P>` (E0277:
// `C: Clone` is not satisfied). ControlDisclosure adds the List<F> field of DisclosureRequest, whose
// `==` needs `F: Clone` for the same reason.
type ControlAudience<P>
= ControlEveryone
| ControlListed { members: Set<P> }

type ControlContext<C, P> {
audience: ControlAudience<P>
context: C
}

type ControlDisclosure<P, F, C> {
principal: P
fields: List<F>
audience: ControlAudience<P>
context: C
}

type NativeEmissionCase {
identity: String
held: Bool
}

fn control_listed(names: List<String>) -> ControlAudience<String> {
ControlListed { members: names |> fold(init: empty_set(), f: (acc, n) => set_insert(acc, n)) }
}

fn control_context(names: List<String>, context: String) -> ControlContext<String, String> {
ControlContext { audience: control_listed(names: names), context: context }
}

fn control_disclosure(fields: List<String>, names: List<String>) -> ControlDisclosure<String, String, String> {
ControlDisclosure { principal: "p", fields: fields, audience: control_listed(names: names), context: "c" }
}

fn header_bound_cases() -> List<NativeEmissionCase> {
[
NativeEmissionCase {
identity: "set_struct_eq_same_members_in_another_order",
held: control_context(names: ["a", "b"], context: "x") == control_context(names: ["b", "a"], context: "x")
},
NativeEmissionCase {
identity: "set_struct_eq_red_bare_field_differs",
held: !(control_context(names: ["a", "b"], context: "x") == control_context(names: ["a", "b"], context: "y"))
},
NativeEmissionCase {
identity: "set_struct_eq_red_set_member_differs",
held: !(control_context(names: ["a", "b"], context: "x") == control_context(names: ["a", "c"], context: "x"))
},
NativeEmissionCase {
identity: "set_struct_eq_red_everyone_is_not_a_listing",
held: !(ControlContext { audience: ControlEveryone, context: "x" } == control_context(names: [], context: "x"))
},
NativeEmissionCase {
identity: "set_and_list_struct_eq_same_fields",
held: control_disclosure(fields: ["f", "g"], names: ["a"]) == control_disclosure(fields: ["f", "g"], names: ["a"])
},
NativeEmissionCase {
identity: "set_and_list_struct_eq_red_list_order_differs",
held: !(control_disclosure(fields: ["f", "g"], names: ["a"]) == control_disclosure(fields: ["g", "f"], names: ["a"]))
}
]
}

data native_emission_expected_identities: List<String> = [
"set_struct_eq_same_members_in_another_order",
"set_struct_eq_red_bare_field_differs",
"set_struct_eq_red_set_member_differs",
"set_struct_eq_red_everyone_is_not_a_listing",
"set_and_list_struct_eq_same_fields",
"set_and_list_struct_eq_red_list_order_differs"
]

fn native_emission_cases() -> List<NativeEmissionCase> {
header_bound_cases()
}

fn case_row(c: NativeEmissionCase) -> String {
concat("case ", concat(c.identity, concat(if c.held { " held" } else { " not_held" }, concat(" observed=", concat(if c.held { "as_decided" } else { "other_answer" }, "\n")))))
}

fn native_claim_report() -> NativeClaimReport {
let cases = native_emission_cases()
let roster = concat("roster ", concat(native_emission_expected_identities |> join(separator: ","), "\n"))
let failed = cases |> filter(c => !c.held) |> map(c => c.identity)
let terminal = if (failed |> count) == 0 { held_terminal() } else { not_held_terminal(reason: concat("not held: ", failed |> join(separator: ","))) }
NativeClaimReport { stdout: concat(roster, cases |> map(c => case_row(c: c)) |> join(separator: "")), terminal: terminal }
}

fn held_terminal() -> NativeClaimTerminal {
NativeClaimHeld
}

fn not_held_terminal(reason: String) -> NativeClaimTerminal {
NativeClaimNotHeld { reason: reason }
}
60 changes: 59 additions & 1 deletion dag/test/claim/generic_item_clone_bound_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ test fn unbounded_declared_container_negative_control() -> Bool {
// proving the WF trigger does not widen to every fn touching a declared type.
// w_impl_accessor_inherits_item_bound_once locks in the already-correct IMPL-side behavior
// (accessor impl blocks read the struct's own item-level clone_bounded_type_params via
// emit_item_type_params_with_clone_bounds, not a fn-grain re-derivation) by asserting the accessor
// emit_type_params_from_clone_param_names, not a fn-grain re-derivation) by asserting the accessor
// impl header carries the bound exactly once, with doubled-spelling refusals mirroring
// both_triggers_render_single_bound above.

Expand Down Expand Up @@ -407,3 +407,61 @@ test fn freemonoid_supplemental_struct_hand_written_impls() -> Bool {
test fn freemonoid_supplemental_enum_hand_written_impls() -> Bool {
w_freemonoid_supplemental_enum_hand_written_impls()
}

// A HAND-WRITTEN IMPL HEADER CARRIES ITS ITEM HEADER'S BOUNDS. The Set route removes Debug and
// PartialEq from the derive list and writes them by hand, with the trait's own requirement on each
// parameter. A derive would also have copied the DECLARATION's bounds onto the impl; the hand-written
// header did not, so an item whose header earns `C: Clone` from a bare field emitted
// `impl<C: std::fmt::Debug, P: Ord + std::fmt::Debug> std::fmt::Debug for HdrCtx<C, P>`, which rustc
// refuses at the `for` type (E0277, `C: Clone` not satisfied) -- the std.authorization_profile
// PublicationContext shape. The header list is taken from the same decision the struct line printed,
// so the two are asserted TOGETHER here: the struct header and both impl headers in one emission.
//
// THE CONVERSE ARM IS WHAT KEEPS THIS FROM BEING "PUT Clone ON EVERYTHING". The coproduct in the
// same fixture declares a BARE header (a Set field earns no declaration bound), so its hand-written
// impls must stay exactly `P: Ord + ..` -- a rule that unioned Clone onto every hand-written impl
// would pass the positive arm and over-bound this one. And P on the struct stays without Clone for
// the same reason: the struct header does not bound it. The native half -- that the emission is a
// program rustc accepts and that `==` answers correctly over it -- is
// gunbc.instruments.native_emission_controls.
fn w_set_struct_hand_written_impls_carry_header_bounds() -> Bool {
compile_dag_rust_emit_check(
"module probe_hdr_set\n\nimport std.types { Set }\n\ntype HdrAud<P>\n = HdrEveryone\n | HdrListed { members: Set<P> }\n\ntype HdrCtx<C, P> {\n audience: HdrAud<P>\n context: C\n}\n",
"src/probe_hdr_set.rs",
[
"pub struct HdrCtx<C: Clone, P>",
"impl<C: Clone + std::fmt::Debug, P: Ord + std::fmt::Debug> std::fmt::Debug for HdrCtx<C, P>",
"impl<C: Clone + PartialEq, P: Ord + PartialEq> PartialEq for HdrCtx<C, P>"
],
[
"impl<C: std::fmt::Debug, P: Ord + std::fmt::Debug> std::fmt::Debug for HdrCtx<C, P>",
"impl<C: PartialEq, P: Ord + PartialEq> PartialEq for HdrCtx<C, P>",
"compile_error"
]
)
}

fn w_set_coproduct_hand_written_impls_stay_at_the_bare_header() -> Bool {
compile_dag_rust_emit_check(
"module probe_hdr_set_bare\n\nimport std.types { Set }\n\ntype HdrAud<P>\n = HdrEveryone\n | HdrListed { members: Set<P> }\n\ntype HdrCtx<C, P> {\n audience: HdrAud<P>\n context: C\n}\n",
"src/probe_hdr_set_bare.rs",
[
"pub enum HdrAud<P>",
"impl<P: Ord + std::fmt::Debug> std::fmt::Debug for HdrAud<P>",
"impl<P: Ord + PartialEq> PartialEq for HdrAud<P>"
],
[
"impl<P: Clone + Ord + std::fmt::Debug> std::fmt::Debug for HdrAud<P>",
"P: Clone + Ord + std::fmt::Debug> std::fmt::Debug for HdrCtx<C, P>",
"compile_error"
]
)
}

test fn set_struct_hand_written_impls_carry_header_bounds() -> Bool {
w_set_struct_hand_written_impls_carry_header_bounds()
}

test fn set_coproduct_hand_written_impls_stay_at_the_bare_header() -> Bool {
w_set_coproduct_hand_written_impls_stay_at_the_bare_header()
}
Loading