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
1 change: 1 addition & 0 deletions DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -257,5 +257,6 @@ One row per class, each carrying its recognition rule and its receipts, as a fil

- Three local checks, each named with the CI step that executes it — a check named here with no executing step is a decoration (§4b): `cargo clippy --all-targets -- -D warnings` (`gunbc.repo_self_build` `repo_self_clippy_command`, the only command that compiles the integration-test and example targets, so a red there is invisible to every other step) runs as `rust_clippy_all_targets_step` in the `required-witnesses-build` job of `gunbc.witness_floor_workflow`, which runs on every push and pull request and IS a required lane — so a clippy red blocks a merge; `cargo fmt --all --check` runs in the generated pre-commit hook (`gunbc.githooks_pre_commit_emit`). `cargo test --release -p v1-compiler --lib` (`repo_self_test_command`) IS NOT RUN BY ANY CI STEP as of the 2026-09-04 runner-capacity ruling, which deleted the `rust-unit-tests` job — it is local diligence, and its loss is a declared drop, `gunbc.rung_drop` `rust_unit_tests_off_the_merge_path`. `cargo test --workspace` is likewise local only: the test targets are compiled by the clippy step and run by nobody.
- one-time per clone: `git config core.hooksPath .githooks` — the only documented manual seed; generated pre-commit/pre-push hooks then idempotently converge `merge.generated-artifact.driver` and re-assert `core.hooksPath` via argv derived from `gunbc.repo_local_git_config` (clones that skip hooksPath degrade to vanilla text-merge for generated-artifact paths; drift gate still guards at CI). The driver REFUSES rather than answering `true`: git reaches a low-level merge driver only when both sides changed the path since the merge base — measured on a four-case matrix, one-sided and identical changes never reach it — and taking the ours side there dropped the other side's authority-derived bytes with no conflict, twice on #7836 against the stage0 seed. It now leaves the ours side in the worktree with no conflict markers, marks the path unmerged, and prints the regeneration recipe; the class is mechanically preventable, not structural, and its next-rung trigger is the commit-writer binding rows in `gunbc.commit_workflow`
- **`gunbc test <label>` is the dedicated CLI for invoking a v2 measurement, and a new one is a row rather than a flag** (operator ruling, 2026-09-16). The seam is `gunbc.target_binding` `TargetProducer` bound to a `gunbc.instrument_targets` label, and the host note says the extension shape outright: *adding one is a row in `instrument_registry` and an arm here; it is not a new route*. What that buys is not tidiness: the label carries its own refusal vocabulary, so an unknown or pattern label REFUSES with exit 2 rather than reporting a pass, and the three terminations stay distinct — 0 held, 1 an observation that did not hold, 2 no observation — which is the conflation §5 forbids, closed by construction for every instrument at once. The subject is the instrument's own fact and never a CLI option, so an invocation cannot quietly measure a different corpus while reporting the same target's standing. **What this rules out is the alternative that keeps suggesting itself:** a flag on `claim_executor`, whose ~20 flags are hand-parsed in a 2783-line `main` over 44,451 lines of `cli_run.rs` with NO `.dag` authority at all — v2 work that lands there is unmodeled by construction, and `--self-host` was withdrawn in the same change that added `//gunbc/instruments:self-host` rather than left standing beside it, because two routes to one fact is the §3 fork. `gunbc`'s own surface is modeled (`gunbc.cli_dispatch_surface` → `gunbc_cli_dispatch_generated.rs`); `claim_executor`'s is not, and the gap is the point.
- explicit actuator (CI / tooling): `gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/repo/repo_local_git_config.dag --function converge`
- **CI** is one emission, `gunbc.witness_floor_workflow` → `.github/workflows/witnesses.yml`, invoking our own binary once per LANE: `claim_executor --required-ci --source-root dag --source-root src/v2 --required-lane build` and the same with `--required-lane witnesses`, in two parallel jobs, plus an aggregating job that carries the required context and reads BOTH lane results — that last is what makes a lane block rather than merely be waited on, so read `gunbc.witness_floor_workflow` `required_lanes_roster` for the current membership rather than this sentence. **The job roster is closed to growth: adding a job needs operator sign-off, because a job is a standing claim on a paid runner on every push and every pull request** — the 2026-09-04 ruling cut three of seven on that basis (`rust-unit-tests`, `fabric-evidence`, `emit-copy-qualification-battery`), and the reasoning an author owes before proposing a lane is stated at `witness_floor_lane_jobs`. Which phases a lane owns is decided in the binary, never in the YAML — the partition is an exhaustive match, so a phase belonging to no job fails to compile. **Read the roster from the run's own announcement, not from here:** every required run prints one `phase <name>` line per phase it owns and one `ROUTED to lane <other>` line per phase it does not. Several capabilities that used to gate are currently declared rung drops — see §4b.
1 change: 1 addition & 0 deletions dag/gunbc/design_document.dag
Original file line number Diff line number Diff line change
Expand Up @@ -272,6 +272,7 @@ fn building_checks_blocks() -> List<MarkdownBlock> {
ul(items: [
li(text: "Three local checks, each named with the CI step that executes it — a check named here with no executing step is a decoration (§4b): `cargo clippy --all-targets -- -D warnings` (`gunbc.repo_self_build` `repo_self_clippy_command`, the only command that compiles the integration-test and example targets, so a red there is invisible to every other step) runs as `rust_clippy_all_targets_step` in the `required-witnesses-build` job of `gunbc.witness_floor_workflow`, which runs on every push and pull request and IS a required lane — so a clippy red blocks a merge; `cargo fmt --all --check` runs in the generated pre-commit hook (`gunbc.githooks_pre_commit_emit`). `cargo test --release -p v1-compiler --lib` (`repo_self_test_command`) IS NOT RUN BY ANY CI STEP as of the 2026-09-04 runner-capacity ruling, which deleted the `rust-unit-tests` job — it is local diligence, and its loss is a declared drop, `gunbc.rung_drop` `rust_unit_tests_off_the_merge_path`. `cargo test --workspace` is likewise local only: the test targets are compiled by the clippy step and run by nobody."),
li(text: "one-time per clone: `git config core.hooksPath .githooks` — the only documented manual seed; generated pre-commit/pre-push hooks then idempotently converge `merge.generated-artifact.driver` and re-assert `core.hooksPath` via argv derived from `gunbc.repo_local_git_config` (clones that skip hooksPath degrade to vanilla text-merge for generated-artifact paths; drift gate still guards at CI). The driver REFUSES rather than answering `true`: git reaches a low-level merge driver only when both sides changed the path since the merge base — measured on a four-case matrix, one-sided and identical changes never reach it — and taking the ours side there dropped the other side's authority-derived bytes with no conflict, twice on #7836 against the stage0 seed. It now leaves the ours side in the worktree with no conflict markers, marks the path unmerged, and prints the regeneration recipe; the class is mechanically preventable, not structural, and its next-rung trigger is the commit-writer binding rows in `gunbc.commit_workflow`"),
li(text: "**`gunbc test <label>` is the dedicated CLI for invoking a v2 measurement, and a new one is a row rather than a flag** (operator ruling, 2026-09-16). The seam is `gunbc.target_binding` `TargetProducer` bound to a `gunbc.instrument_targets` label, and the host note says the extension shape outright: *adding one is a row in `instrument_registry` and an arm here; it is not a new route*. What that buys is not tidiness: the label carries its own refusal vocabulary, so an unknown or pattern label REFUSES with exit 2 rather than reporting a pass, and the three terminations stay distinct — 0 held, 1 an observation that did not hold, 2 no observation — which is the conflation §5 forbids, closed by construction for every instrument at once. The subject is the instrument's own fact and never a CLI option, so an invocation cannot quietly measure a different corpus while reporting the same target's standing. **What this rules out is the alternative that keeps suggesting itself:** a flag on `claim_executor`, whose ~20 flags are hand-parsed in a 2783-line `main` over 44,451 lines of `cli_run.rs` with NO `.dag` authority at all — v2 work that lands there is unmodeled by construction, and `--self-host` was withdrawn in the same change that added `//gunbc/instruments:self-host` rather than left standing beside it, because two routes to one fact is the §3 fork. `gunbc`'s own surface is modeled (`gunbc.cli_dispatch_surface` → `gunbc_cli_dispatch_generated.rs`); `claim_executor`'s is not, and the gap is the point."),
li(text: "explicit actuator (CI / tooling): `gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/repo/repo_local_git_config.dag --function converge`"),
li(text: "**CI** is one emission, `gunbc.witness_floor_workflow` → `.github/workflows/witnesses.yml`, invoking our own binary once per LANE: `claim_executor --required-ci --source-root dag --source-root src/v2 --required-lane build` and the same with `--required-lane witnesses`, in two parallel jobs, plus an aggregating job that carries the required context and reads BOTH lane results — that last is what makes a lane block rather than merely be waited on, so read `gunbc.witness_floor_workflow` `required_lanes_roster` for the current membership rather than this sentence. **The job roster is closed to growth: adding a job needs operator sign-off, because a job is a standing claim on a paid runner on every push and every pull request** — the 2026-09-04 ruling cut three of seven on that basis (`rust-unit-tests`, `fabric-evidence`, `emit-copy-qualification-battery`), and the reasoning an author owes before proposing a lane is stated at `witness_floor_lane_jobs`. Which phases a lane owns is decided in the binary, never in the YAML — the partition is an exhaustive match, so a phase belonging to no job fails to compile. **Read the roster from the run's own announcement, not from here:** every required run prints one `phase <name>` line per phase it owns and one `ROUTED to lane <other>` line per phase it does not. Several capabilities that used to gate are currently declared rung drops — see §4b."),
]),
Expand Down
40 changes: 38 additions & 2 deletions dag/gunbc/instrument_targets.dag
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,27 @@ fn compile_clean_diagnostic_census_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "compile-clean-diagnostic-census" } }
}

// THE SELF-HOST INSTRUMENT: THE GENERATION THIS REPOSITORY CAN PERFORM, ASKED AS ONE QUESTION.
//
// The seed emits v2's compiler closure, assembles it as a crate, and builds it. Pass or fail is
// the whole verdict and WHERE IT STOPS IS THE STATUS, so there is no roster of known-good entries
// beside it: a roster is a second representation of what this instrument demonstrates by running
// (DESIGN sections 2 and 3), and it drifts exactly when nobody updates it.
// `required_v2_emission_entries` has changed once in repository history and that change was a
// directory move.
//
// WHAT A GREEN DOES NOT ESTABLISH, named so it is not cited for more than it carries. It is
// EMISSION AND COMPILATION, not behavioural equivalence -- DESIGN section 7 asks that the emitted
// module also behave as the seed does on a discriminating corpus, and that half lives in the three
// behavioral-receipt instruments beside this one. Nor is it the second generation: the BUILT binary
// emitting the same closure is the v2 -> v2 boundary, and it refuses today because
// `v2.compiler.compile` declares `SourceRootEvalDriver`, whose rendered main answers `census` and
// `adjudicate` and has no compile mode at all. That refusal is the honest next position and belongs
// in this instrument when a driver can reach it.
fn self_host_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "self-host" } }
}

// 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 Down Expand Up @@ -133,6 +154,14 @@ fn compile_clean_diagnostic_census_target() -> BuildTarget {
instrument_test_target(label: compile_clean_diagnostic_census_label())
}

fn self_host_target() -> BuildTarget {
instrument_test_target(label: self_host_label())
}

fn self_host_binding() -> TargetBinding {
TargetBinding { target: self_host_label() producer: SelfHostProducer {} }
}

fn heads_reading_differential_binding() -> TargetBinding {
TargetBinding {
target: heads_reading_differential_label()
Expand Down Expand Up @@ -168,6 +197,13 @@ fn heads_reading_differential_source_roots() -> List<String> {
["dag", "src/v2"]
}

// The self-host instrument's own subject, on the same rule its siblings follow: which corpus the
// seed emits v2 FROM is a property of this instrument, not a CLI option, so an invocation cannot
// quietly build a different closure while reporting this target's standing.
fn self_host_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> {
Expand Down Expand Up @@ -201,15 +237,15 @@ fn instrument_targets() -> List<Label> {
[
heads_reading_differential_label(), behavioral_receipt_plan_label(),
behavioral_receipt_census_label(), behavioral_receipt_selftest_label(),
compile_clean_diagnostic_census_label()
compile_clean_diagnostic_census_label(), self_host_label()
]
}

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

Expand Down
3 changes: 2 additions & 1 deletion dag/gunbc/target_binding.dag
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@ import std.integer { Int }
// particular, no command line, function name, or execution closure is carried here: selecting a
// transport belongs to the later realization layer, not to either side of this model relation.
type TargetProducer
= RequiredFloorProducer
= SelfHostProducer
| RequiredFloorProducer
| BazelProducer
| BehavioralReceiptPlanProducer
| BehavioralReceiptCensusProducer
Expand Down
71 changes: 71 additions & 0 deletions dag/test/claim/self_host_instrument_binding_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
module test.claim.self_host_instrument_binding_witness

import extdeps.bazel.label { Label, label_eq }
import gunbc.target_binding {
TargetProducer,
SelfHostProducer,
HeadsReadingDifferentialProducer,
CompileCleanDiagnosticCensusProducer
}
import gunbc.instrument_targets {
invoke_target,
instrument_targets,
instrument_bindings,
self_host_label,
self_host_source_roots
}
import gunbc.target_invocation {
TargetInvocationRoute,
TargetInvocationRouted,
TargetInvocationRouteRefused
}
import v2.std.logic { Bool }
import v2.std.text { String }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import v2.std.algebra { fold_list, length }
import std.algebra { Cons, Empty }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// THE SELF-HOST INSTRUMENT IS REACHABLE BY THE OPERAND A SHELL WOULD HAND THE VERB, and that is
// the whole claim these rows make. `gunbc test //gunbc/instruments:self-host` is the modeled route
// to the v1 -> v2 generation, so the operand must end at this instrument's own producer through
// the LIVE registry -- not through a population authored here, which would pass while the
// repository's roster had lost the row.
//
// WHY THE SECOND ROW IS NOT REDUNDANT WITH THE FIRST. Routing to A producer is not routing to the
// RIGHT one: a binding that names the wrong producer routes successfully and then measures
// something else while reporting this target's standing. So the arm is asserted, not merely the
// absence of a refusal.
//
// THE THIRD ROW IS THE STANDING RED AND IT DOES NOT RETIRE. The subject is the instrument's own
// fact -- `gunbc test` takes no source-root option -- so if these roots ever became an invocation
// argument, one fact would have two homes and an invocation could quietly build a different
// closure while reporting this target's standing. That is the same rule its five siblings follow
// and the reason none of them accepts a corpus option either.

fn routed_producer_is_self_host(route: TargetInvocationRoute) -> Bool {
match route {
TargetInvocationRouted { binding: b } =>
label_eq(a: b.target, b: self_host_label())
&& (b.producer == SelfHostProducer {})
TargetInvocationRouteRefused { cause: _ } => false
}
}

test fn the_self_host_operand_routes_through_the_live_registry_holds() -> Bool {
routed_producer_is_self_host(route: invoke_target(operand: "//gunbc/instruments:self-host"))
}

// A LOST ROW REDS HERE RATHER THAN SILENTLY SHRINKING THE ROSTER. The two lists are built from the
// same rows the CLI routes against, so a label added without its binding -- or a binding added
// without its label -- is a length disagreement rather than a target that refuses at invocation
// time in someone else's session.
test fn every_rostered_label_carries_a_binding_holds() -> Bool {
length(xs: instrument_targets()) == length(xs: instrument_bindings())
}

// THE SUBJECT IS THE INSTRUMENT'S OWN FACT, NOT AN INVOCATION OPTION.
test fn the_self_host_subject_is_the_instruments_own_fact_holds() -> Bool {
length(xs: self_host_source_roots()) == 2
}
2 changes: 1 addition & 1 deletion src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ mod required_floor_runner;
mod required_lane_roster;
pub mod rostered_row_join;
mod serve_budget_refusal;
pub use native_lane_runner::run_required_v2_native;
pub use native_lane_runner::{run_required_v2_native, run_self_host, SelfHostHeld};
pub(crate) use required_floor_runner::*;
pub use required_floor_runner::{
floor_discovery_path_excluded, make_eval_context, make_eval_context_with_runtime_options,
Expand Down
Loading