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
2 changes: 1 addition & 1 deletion DESIGN.md

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion dag/gunbc/design_document.dag

Large diffs are not rendered by default.

65 changes: 59 additions & 6 deletions dag/gunbc/instrument_targets.dag
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@ import extdeps.bazel.label { Label, PackageName, PackagePath, TargetName }
import gunbc.build_target { BuildTarget, TestRule }
import gunbc.target_binding {
TargetBinding,
BehavioralReceiptPlanProducer, BehavioralReceiptCensusProducer,
BehavioralReceiptSelftestProducer,
HeadsReadingDifferentialProducer,
HeadsReadingDifferentialStanding,
HeadsReadingDifferentialCompleted,
Expand All @@ -29,10 +31,9 @@ import std.types { String, Bool }
//
// `gunbc.target_binding` declares the carriers and the witness beside it authors examples; neither
// declares an addressable target that exists in this repository. This module does, and the
// population is deliberately ONE. Landing four instruments at once would have made a first failure
// ambiguous between dispatch, subject reachability and output policy; the seam it proves is
// generic, so the remaining three are rows added here — a `BuildTarget`, a `TargetBinding`, and one
// classifier — and never an edit to `gunbc.target_invocation`.
// population began with one target so the dispatch seam could be proven independently. The three
// behavioral instruments now complete the already-modeled producer population as ordinary target
// and binding rows; `gunbc.target_invocation` remains unchanged.
//
// THE INSTRUMENTS ARE OUTSIDE `//:required` AND NOTHING HERE ADDS THEM TO IT. That is not a
// promise kept by diligence: `//:required`'s dependencies are DERIVED by
Expand All @@ -56,6 +57,18 @@ fn heads_reading_differential_label() -> Label {
}
}

fn behavioral_receipt_plan_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "behavioral-receipt-plan" } }
}

fn behavioral_receipt_census_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "behavioral-receipt-census" } }
}

fn behavioral_receipt_selftest_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "behavioral-receipt-selftest" } }
}

// THE INSTRUMENT IS A `TestRule` WITH NO DEPENDENCIES, and both halves are measurements rather
// than placeholders. It answers a test question — does the heads reading read the same grammar as
// the full reading — so it is not a `BuildRule`; and it depends on no other target in this graph,
Expand All @@ -68,13 +81,41 @@ fn heads_reading_differential_target() -> BuildTarget {
}
}

fn instrument_test_target(label: Label) -> BuildTarget {
BuildTarget { label: label kind: TestRule {} dependencies: [] }
}

fn behavioral_receipt_plan_target() -> BuildTarget {
instrument_test_target(label: behavioral_receipt_plan_label())
}

fn behavioral_receipt_census_target() -> BuildTarget {
instrument_test_target(label: behavioral_receipt_census_label())
}

fn behavioral_receipt_selftest_target() -> BuildTarget {
instrument_test_target(label: behavioral_receipt_selftest_label())
}

fn heads_reading_differential_binding() -> TargetBinding {
TargetBinding {
target: heads_reading_differential_label()
producer: HeadsReadingDifferentialProducer {}
}
}

fn behavioral_receipt_plan_binding() -> TargetBinding {
TargetBinding { target: behavioral_receipt_plan_label() producer: BehavioralReceiptPlanProducer {} }
}

fn behavioral_receipt_census_binding() -> TargetBinding {
TargetBinding { target: behavioral_receipt_census_label() producer: BehavioralReceiptCensusProducer {} }
}

fn behavioral_receipt_selftest_binding() -> TargetBinding {
TargetBinding { target: behavioral_receipt_selftest_label() producer: BehavioralReceiptSelftestProducer {} }
}

// THE SUBJECT IS THE INSTRUMENT'S OWN FACT, NOT AN ARGUMENT THE CALLER SUPPLIES.
//
// `gunbc test //gunbc/instruments:heads-reading-differential` takes no source-root option, and
Expand All @@ -87,6 +128,12 @@ fn heads_reading_differential_source_roots() -> List<String> {
["dag", "src/v2"]
}

// One modeled subject shared by the three behavioral producers. The host leaf receives this
// population; it does not decide it.
fn behavioral_receipt_source_roots() -> List<String> {
["dag", "src/v2"]
}

// WHAT AN INVOCATION OF THIS INSTRUMENT DOES NOT ESTABLISH, STATED HERE RATHER THAN ASSUMED SAFE.
//
// The producer reads an UNPINNED LIVE WORKING TREE. Nothing binds the bytes it consumed to the
Expand All @@ -103,11 +150,17 @@ fn heads_reading_differential_source_roots() -> List<String> {
// standing was about source X". Direct invocation and its immediate rendering are what this seam
// claims, and they need none of them.
fn instrument_targets() -> List<Label> {
[heads_reading_differential_label()]
[
heads_reading_differential_label(), behavioral_receipt_plan_label(),
behavioral_receipt_census_label(), behavioral_receipt_selftest_label()
]
}

fn instrument_bindings() -> List<TargetBinding> {
[heads_reading_differential_binding()]
[
heads_reading_differential_binding(), behavioral_receipt_plan_binding(),
behavioral_receipt_census_binding(), behavioral_receipt_selftest_binding()
]
}

// THE PRODUCTION ENTRY: the generic route, bound to the live population, in one place. Every
Expand Down
1 change: 1 addition & 0 deletions dag/gunbc/stage0_crate_layout_generated.dag
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ data generated_stage0_filenames: List<String> = [
"cssl_seed_linked_closure_assembly.rs",
"required_regen_host.rs",
"target_invocation_host.rs",
"behavioral_receipt_host.rs",
"partition_crate_boundary_host.rs",
"emitted_closure_compile_host.rs",
"v2_compiler_compile.rs",
Expand Down
29 changes: 27 additions & 2 deletions dag/gunbc/target_invocation_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -103,10 +103,35 @@ data target_invocation_seed_growth_justification: SeedGrowthJustification = Seed
module_path: "v1_compiler.target_invocation_host",
decl_name: "test_verb",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.behavioral_receipt_host",
decl_name: "BehavioralHostTermination",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.behavioral_receipt_host",
decl_name: "BehavioralHostOutcome",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.behavioral_receipt_host",
decl_name: "run_census",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.behavioral_receipt_host",
decl_name: "run_selftest",
field: WholeDeclaration
},
DeclarationRef {
module_path: "v1_compiler.behavioral_receipt_host",
decl_name: "run_plan",
field: WholeDeclaration
}
],
reason: "The verb's leaf producer is host Rust because its subject is a filesystem walk the hermetic floor refuses; the route around that leaf is hand-mirrored because none of the three modeled modules is in the v1 seed's emitted closure, and the two alternatives are worse -- routing through the interpreter makes it load-bearing for a NEW capability while two lanes delete it, and growing the emitter's closure to reach extdeps.bazel.label is a larger seed change than the verb it serves. What the growth buys is that the repository's instruments become addressable by label at all: before it, no target in this repository could be run by name.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete all 19 when the seam is EMITTED rather than authored -- when gunbc.target_invocation and gunbc.instrument_targets are in the emitted closure of whatever renders gunbc's CLI, the route, the registry and the termination vocabulary come from the model and only the producer leaf stays behind. A PARTIAL migration is admissible and is the expected shape: the label admission dissolves the moment extdeps.bazel.label is emitted, independently of the producer, because it is a pure function of a string. What does NOT dissolve them is moving them to another host file, and what does NOT dissolve them is a witness asserting the mirror agrees with the model -- that would raise the rung without removing the duplicate.",
current_boundary: "src/v1/stage0/src/target_invocation_host.rs; src/v1/stage0/src/cli_run.rs (one #[path] mod line); src/v1/stage0/src/main.rs (one Commands variant and its arm); dag/gunbc/target_invocation_seed_growth.dag"
trigger: "Discharge each declaration when its modeled realization is emitted rather than authored. The target_invocation_host subset deletes when gunbc.target_invocation and gunbc.instrument_targets enter the emitted closure of whatever renders gunbc's CLI; the behavioral_receipt_host subset deletes when the three already-modeled behavioral producers gain emitted native realization. A PARTIAL migration is admissible and expected: label admission dissolves when extdeps.bazel.label is emitted, independently of either producer family. Moving a declaration to another host file or adding a parity witness does not discharge it -- both leave the hand-authored declaration standing.",
current_boundary: "src/v1/stage0/src/target_invocation_host.rs; src/v1/stage0/src/behavioral_receipt_host.rs (native realization of the already-modeled behavioral producers, relocated from claim_executor); src/v1/stage0/src/cli_run.rs (two #[path] mod lines); src/v1/stage0/src/main.rs (one Commands variant and its arm); dag/gunbc/target_invocation_seed_growth.dag"
}
26 changes: 24 additions & 2 deletions dag/test/claim/target_invocation_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import gunbc.target_binding {
TargetBindingIndexBuild, TargetBindingIndexReady, TargetBindingIndexRefused,
build_target_binding_index,
TargetProducer, HeadsReadingDifferentialProducer, BehavioralReceiptPlanProducer,
BehavioralReceiptCensusProducer, BehavioralReceiptSelftestProducer,
HeadsReadingDifferentialStanding,
HeadsReadingDifferentialCompleted, HeadsReadingDifferentialSubjectUnreached,
HeadsReadingDifferentialRefused,
Expand All @@ -34,6 +35,8 @@ import gunbc.instrument_targets {
heads_reading_differential_label,
heads_reading_differential_target,
heads_reading_differential_binding,
behavioral_receipt_plan_label, behavioral_receipt_census_label,
behavioral_receipt_selftest_label,
instrument_targets, instrument_bindings,
invoke_target,
heads_reading_differential_termination,
Expand Down Expand Up @@ -88,6 +91,25 @@ test fn the_acceptance_operand_routes_to_the_real_differential_producer() -> Boo
}
}

test fn every_behavioral_instrument_operand_routes_to_its_own_producer() -> Bool {
let plan = invoke_target(operand: "//gunbc/instruments:behavioral-receipt-plan")
let census = invoke_target(operand: "//gunbc/instruments:behavioral-receipt-census")
let selftest = invoke_target(operand: "//gunbc/instruments:behavioral-receipt-selftest")
match plan {
TargetInvocationRouted { binding: p } => match census {
TargetInvocationRouted { binding: c } => match selftest {
TargetInvocationRouted { binding: s } =>
(p.producer == BehavioralReceiptPlanProducer {})
&& (c.producer == BehavioralReceiptCensusProducer {})
&& (s.producer == BehavioralReceiptSelftestProducer {})
TargetInvocationRouteRefused { cause: _ } => false
}
TargetInvocationRouteRefused { cause: _ } => false
}
TargetInvocationRouteRefused { cause: _ } => false
}
}

// THE DISCRIMINATING RED FOR THE ROUTE ITSELF. A label of the same SHAPE that names no registered
// target must refuse rather than reach a producer -- without this, the assertion above is
// satisfied by any function that returns the one binding it knows.
Expand Down Expand Up @@ -269,8 +291,8 @@ test fn the_instrument_target_and_its_binding_are_the_same_identity() -> Bool {
LabelNonCanonical { cause: _ } => false
})
&& (render_label(l: t.label) == differential_operand())
&& ((instrument_targets() |> count) == 1)
&& ((instrument_bindings() |> count) == 1)
&& ((instrument_targets() |> count) == 4)
&& ((instrument_bindings() |> count) == 4)
}

// THE ABSENCE PROOF, MEASURED OVER THE DERIVED POPULATION RATHER THAN ASSERTED IN PROSE.
Expand Down
Loading
Loading