Skip to content
Merged
Show file tree
Hide file tree
Changes from 3 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
27 changes: 25 additions & 2 deletions dag/gunbc/instrument_targets.dag
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,23 @@ fn dag_emit_real_grammar_round_trips_entry() -> String {
"dag/gunbc/instruments/dag_emit_real_grammar_round_trips.dag"
}

// THE MATERIALIZATION STORE CLOSURE, EMITTED, BUILT UNDER CARGO AND RUN: the NativeClaimDriver
// program gunbc.instruments.native_materialization_store_closure, whose closure contains
// extdeps.realization.materialization_store_local. It is the executing control for three classes of
// accepted source that emitted Rust rustc refused -- item bounds missing from hand-written impl and
// fn headers, an optional-returning lambda unwrapped inside its own body, and five kernel-String
// values at structural-text parameters (specimens of gunbc.rung_drop text_boundary_identity_wall)
// -- so the BUILD is a verdict here, not only the cases: a regression in any of them is a red
// emitted-crate build before a single case runs. Run by name, not a merge gate.
// `gunbc test //gunbc/instruments:native-materialization-store-closure`.
fn native_materialization_store_closure_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "native-materialization-store-closure" } }
}

fn native_materialization_store_closure_entry() -> String {
"dag/gunbc/instruments/native_materialization_store_closure.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 @@ -470,6 +487,10 @@ 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() } }
}

fn native_materialization_store_closure_binding() -> TargetBinding {
TargetBinding { target: native_materialization_store_closure_label() producer: NativeClaimProgramProducer { entry: native_materialization_store_closure_entry() } }
}

fn v2_native_frontier_binding() -> TargetBinding {
TargetBinding { target: v2_native_frontier_label() producer: V2NativeFrontierProducer {} }
}
Expand Down Expand Up @@ -617,7 +638,8 @@ fn instrument_targets() -> List<Label> {
required_lane_resolution_census_label(), bare_reference_channel_outcome_label(),
self_host_behavioral_equivalence_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_materialization_store_closure_label()
]
}

Expand All @@ -632,7 +654,8 @@ fn instrument_bindings() -> List<TargetBinding> {
required_lane_resolution_census_binding(), bare_reference_channel_outcome_binding(),
self_host_behavioral_equivalence_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_materialization_store_closure_binding()
]
}

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

import std.types { List, String, Bool }
import std.compiler_entry { CompilerEntryDriver, NativeClaimDriver, NativeClaimReport, NativeClaimTerminal, NativeClaimHeld, NativeClaimNotHeld }
import std.authorization_profile { UniversalAudience, EnumeratedAudience, audience_subset, audience_join }
import std.effect_grant { namespace_tree_of_label, namespace_tree_label }
import std.materialization_object { store_object_line, store_object_line_malformed_text }
import extdeps.realization.materialization_store_local { store_path }
import v2.compiler.self_host.generation {
SourceClosureMember, SourceClosureRoster, source_closure_axis_digest,
SourceClosureAxisDigest, SourceClosureAxisRefused,
RosterCanonicallyOrdered, RosterNotAscending, RosterDuplicateMember, RosterMemberIdentityEmpty,
}
import v2.std.node { symbol_identity_digest }

// THE MATERIALIZATION STORE CLOSURE, EMITTED, BUILT AND RUN. `gunbc test
// //gunbc/instruments:native-materialization-store-closure` emits the closure this entry reaches --
// which contains extdeps.realization.materialization_store_local and everything it imports -- builds
// the emitted crate under cargo, and runs it. The build is the first half of the evidence and the
// reason this is a program rather than a string witness: the three defect classes it stands over
// were each ACCEPTED source that emitted Rust rustc refused, and two of them sat under a
// compile_dag_rust_emit_check row that was green the whole time, one of them asserting the
// ill-formed text verbatim. A substring oracle cannot refuse Rust that does not compile; cargo can.
//
// The cases are the second half: one natively executed case per repaired site, each on the exact
// function the defect sat in, each with a discriminating RED beside it.
// audience_* std.authorization_profile audience_subset / audience_join -- generic fns
// over a Set element, which emitted `P: Clone` and no `P: Ord`, beside
// hand-written Debug/PartialEq impls whose headers omitted the item header's
// own Clone bound.
// tree_label_* std.effect_grant namespace_tree_of_label -- the four kernel-String values
// that were passed to v2.std.algebra length (gunbc.rung_drop
// text_boundary_identity_wall, specimens of 2026-10-03). The prefix-only
// label is the RED for that exact comparison.
// roster_* v2.compiler.self_host.generation roster_scan_step -- the fifth specimen,
// where emptiness is now tested on the kernel value the member holds.
// malformed_text_* std.materialization_object store_object_line_malformed_text -- an
// optional-returning lambda passed to a `fn(..) -> T` parameter, which the
// emitter unwrapped inside the closure body.
// store_path_* extdeps.realization.materialization_store_local itself, so the store module
// is in the closure by a reference this program executes rather than by an
// import nothing calls.
//
// WHAT THIS DOES NOT ESTABLISH. It runs no filesystem operation: a NativeClaimDriver main reads no
// file (std.compiler_entry), so the store's effectful half -- open, lookup, commit -- is built here
// and executed elsewhere. And it is run by name; it is not a merge gate.
data compiler_pipeline_entry: CompilerEntryDriver = NativeClaimDriver

type StoreClosureCase {
identity: String
held: Bool
observed: String
}

fn bool_text(b: Bool) -> String {
if b { "true" } else { "false" }
}

fn held_as(identity: String, observed: String, expected: String) -> StoreClosureCase {
StoreClosureCase { identity: identity, held: observed == expected, observed: observed }
}

fn string_set(a: String, b: String) -> Set<String> {
set_insert(set_insert(empty_set(), a), b)
}

fn audience_cases() -> List<StoreClosureCase> {
let narrow = EnumeratedAudience { members: set_insert(empty_set(), "alice") }
let wide = EnumeratedAudience { members: string_set(a: "alice", b: "bob") }
let other = EnumeratedAudience { members: string_set(a: "bob", b: "carol") }
let joined = match audience_join(left: wide, right: other) {
EnumeratedAudience { members: members } => members == set_insert(string_set(a: "alice", b: "bob"), "carol")
UniversalAudience => false
}
[
held_as(identity: "audience_subset_admits_a_contained_set", observed: bool_text(b: audience_subset(left: narrow, right: wide)), expected: "true"),
held_as(identity: "audience_subset_red_a_wider_set_is_not_contained", observed: bool_text(b: audience_subset(left: wide, right: narrow)), expected: "false"),
held_as(identity: "audience_subset_red_overlapping_sets_are_incomparable", observed: bool_text(b: audience_subset(left: wide, right: other)), expected: "false"),
held_as(identity: "audience_join_is_the_union", observed: bool_text(b: joined), expected: "true")
]
}

fn tree_label_round_trip(label: String) -> String {
match namespace_tree_of_label(label: label) {
Present { value: tree } => namespace_tree_label(tree: tree)
Absent => "refused"
}
}

fn tree_label_cases() -> List<StoreClosureCase> {
[
held_as(identity: "tree_label_service_round_trips", observed: tree_label_round_trip(label: "service:fs"), expected: "service:fs"),
held_as(identity: "tree_label_red_service_prefix_naming_no_service_refuses", observed: tree_label_round_trip(label: "service:"), expected: "refused"),
held_as(identity: "tree_label_parameterless_tree_round_trips", observed: tree_label_round_trip(label: "filesystem"), expected: "filesystem")
]
}

fn roster_member(identity: String) -> SourceClosureMember {
SourceClosureMember { identity: identity, content: symbol_identity_digest(sym: "content") }
}

fn roster_verdict_text(roster: SourceClosureRoster) -> String {
match source_closure_axis_digest(roster: roster) {
SourceClosureAxisDigest { digest: _ } => "digest"
SourceClosureAxisRefused { verdict: v } =>
match v {
RosterMemberIdentityEmpty => "identity_empty"
RosterCanonicallyOrdered => "ordered"
RosterNotAscending { at_member: _ } => "not_ascending"
RosterDuplicateMember { at_member: _ } => "duplicate"
}
}
}

fn roster_cases() -> List<StoreClosureCase> {
[
held_as(identity: "roster_ascending_members_fold_to_a_digest", observed: roster_verdict_text(roster: SourceClosureRoster { members: [roster_member(identity: "a_module"), roster_member(identity: "b_module")] }), expected: "digest"),
held_as(identity: "roster_red_an_empty_member_identity_refuses", observed: roster_verdict_text(roster: SourceClosureRoster { members: [roster_member(identity: "")] }), expected: "identity_empty")
]
}

fn malformed_text(line: String) -> String {
match store_object_line_malformed_text(l: store_object_line(line: line)) {
Present { value: text } => concat("malformed:", text)
Absent => "well_formed"
}
}

fn malformed_text_cases() -> List<StoreClosureCase> {
[
held_as(identity: "malformed_text_carries_the_malformed_line", observed: malformed_text(line: "neither a part nor a payload"), expected: "malformed:neither a part nor a payload"),
held_as(identity: "malformed_text_red_a_well_formed_line_carries_none", observed: malformed_text(line: "end"), expected: "well_formed")
]
}

fn store_path_cases() -> List<StoreClosureCase> {
[
held_as(identity: "store_path_joins_root_and_name", observed: store_path(root_path: "/store", name: "object"), expected: "/store/object"),
held_as(identity: "store_path_does_not_double_a_trailing_separator", observed: store_path(root_path: "/store/", name: "object"), expected: "/store/object")
]
}

fn store_closure_cases() -> List<StoreClosureCase> {
concat(
concat(audience_cases(), tree_label_cases()),
concat(concat(roster_cases(), malformed_text_cases()), store_path_cases())
)
}

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

// THE EXPECTED IDENTITIES, DECLARED RATHER THAN DERIVED FROM THE CASES, on the rule
// gunbc.instruments.native_crypto_vectors states: the reader joins the printed rows against this
// roster, so a case function deleted or filtered away leaves its identity here with no row and the
// run is NO OBSERVATION rather than a smaller green.
data store_closure_expected_identities: List<String> = [
"audience_subset_admits_a_contained_set",
"audience_subset_red_a_wider_set_is_not_contained",
"audience_subset_red_overlapping_sets_are_incomparable",
"audience_join_is_the_union",
"tree_label_service_round_trips",
"tree_label_red_service_prefix_naming_no_service_refuses",
"tree_label_parameterless_tree_round_trips",
"roster_ascending_members_fold_to_a_digest",
"roster_red_an_empty_member_identity_refuses",
"malformed_text_carries_the_malformed_line",
"malformed_text_red_a_well_formed_line_carries_none",
"store_path_joins_root_and_name",
"store_path_does_not_double_a_trailing_separator"
]

fn native_claim_report() -> NativeClaimReport {
let cases = store_closure_cases()
let roster = concat("roster ", concat(store_closure_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 }
}
Loading