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
28 changes: 19 additions & 9 deletions .github/workflows/witnesses.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,14 +22,17 @@ env:
GUNBC_REQUIRED_CI_CONTRACT_EPOCH: 2026-09-01.1
jobs:
emit-build:
runs-on: ubuntu-24.04-arm
runs-on: [self-hosted, linux, arm64]
timeout-minutes: 90
if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository
permissions:
contents: read
steps:
- name: Checkout
- name: Checkout the commit this lane judges
uses: actions/checkout@fbc6f3992d24b796d5a048ff273f7fcc4a7b6c09
with:
fetch-depth: 0
ref: ${{ github.event.pull_request.head.sha }}
persist-credentials: false
- name: Isolate toolchain homes
run: |-
Expand Down Expand Up @@ -75,6 +78,10 @@ jobs:
if (! '[' '-f' "$GUNBC_FLOOR_RECEIPT" ']') || '[' "$GUNBC_FLOOR_CLASS" '=' 'structural' ']' || ('[' "$GUNBC_FLOOR_CLASS" '=' 'infra' ']' && (! ('[' '-f' "$GUNBC_FLOOR_RECEIPT" ']' && 'grep' '-q' 'class=structural' "$GUNBC_FLOOR_RECEIPT"))) || ('[' "$GUNBC_FLOOR_CLASS" '=' 'none' ']' && (! ('[' '-f' "$GUNBC_FLOOR_RECEIPT" ']' && 'grep' '-q' 'class=structural' "$GUNBC_FLOOR_RECEIPT")) && (! ('[' '-f' "$GUNBC_FLOOR_RECEIPT" ']' && 'grep' '-q' 'class=infra' "$GUNBC_FLOOR_RECEIPT"))); then 'printf' 'class=%s\nsignature=%s\nexit=%s\n' "$GUNBC_FLOOR_CLASS" "$GUNBC_FLOOR_SIGNATURE" "$GUNBC_FLOOR_EXIT" > "$GUNBC_FLOOR_RECEIPT"; if '[' "$GUNBC_FLOOR_CLASS" '=' 'infra' ']'; then 'echo' '::error title=environment::floor_class='"$GUNBC_FLOOR_CLASS"' signature='"$GUNBC_FLOOR_SIGNATURE"' exit='"$GUNBC_FLOOR_EXIT"'; this is not a verdict about the diff. Attempt receipt: '"$GUNBC_FLOOR_RECEIPT"; fi; if '[' "$GUNBC_FLOOR_CLASS" '=' 'structural' ']'; then 'echo' '::error title=subject::floor_class='"$GUNBC_FLOOR_CLASS"' exit='"$GUNBC_FLOOR_EXIT"'; read the step log for the subject defect'; fi; fi
'exit' "$GUNBC_FLOOR_EXIT"

- name: Require isolated toolchain homes
run: |
if [ -z "${CARGO_HOME:-}" ] || [ -z "${RUSTUP_HOME:-}" ]; then echo "::error::ToolchainHomesNotIsolated CARGO_HOME=${CARGO_HOME:-unset} RUSTUP_HOME=${RUSTUP_HOME:-unset} -- the isolation step did not run, so this job shares a toolchain with every other runner slot on this host and a concurrent install can replace a binary mid-run" >&2; exit 1; fi
if: "!cancelled()"
- name: emit and build //gunbc/instruments:self-host
id: emit_build_self_host
run: |+
Expand Down Expand Up @@ -125,10 +132,11 @@ jobs:

- name: Why this lane is red, and what would be a real finding
run: |-
printf '%s\n' 'emit-build is a NON-REQUIRED detector lane. A red here does NOT block your merge:'
printf '%s\n' 'the required context is `witnesses`, and this job is not an input to it.'
printf '%s\n' 'emit-build is a REQUIRED lane: a red here BLOCKS your merge, through the required context `witnesses`.'
printf '%s\n' 'No standing break is declared, so a red here is a REAL FINDING -- most likely yours.'
if: failure()
env:
MALLOC_ARENA_MAX: "2"
floor:
runs-on: [self-hosted, linux, arm64]
timeout-minutes: 90
Expand Down Expand Up @@ -565,19 +573,21 @@ jobs:
MALLOC_ARENA_MAX: "2"
witnesses:
runs-on: [self-hosted, linux, arm64]
needs: [floor, generated]
needs: [emit-build, floor, generated]
timeout-minutes: 5
if: always()
permissions:
contents: read
steps:
- name: Every required lane must have succeeded
run: |-
echo "required lanes: floor=$FLOOR generated=$GENERATED (same_repo=$SAME_REPO)"
if [ "$FLOOR" = failure ] || [ "$GENERATED" = failure ]; then echo "::error::a required lane concluded failure (floor=$FLOOR generated=$GENERATED) - open that job's log" >&2; exit 1; fi
if [ "$FLOOR" != success ]; then if [ "$SAME_REPO" = false ] && [ "$FLOOR" = skipped ]; then echo "::notice::the fleet lane is skipped for a fork pull request: no witnesses fold and no generated-artifact verdict for this head"; else echo "::error::the fleet lane produced no success (floor=$FLOOR), so this head carries no witnesses fold and no generated-artifact verdict"; exit 1; fi; fi
if [ "$GENERATED" != success ]; then if [ "$SAME_REPO" = false ] && [ "$GENERATED" = skipped ]; then echo "::notice::the generated-artifact lane is skipped for a fork pull request: no generated-artifact verdict for this head"; else echo "::error::the generated-artifact lane produced no success (generated=$GENERATED), so this head carries no witnesses fold and no generated-artifact verdict"; exit 1; fi; fi
echo "required lanes: emit-build=$EMIT_BUILD floor=$FLOOR generated=$GENERATED (same_repo=$SAME_REPO)"
if [ "$EMIT_BUILD" = failure ] || [ "$FLOOR" = failure ] || [ "$GENERATED" = failure ]; then echo "::error::a required lane concluded failure (emit-build=$EMIT_BUILD floor=$FLOOR generated=$GENERATED) - open that job's log" >&2; exit 1; fi
if [ "$EMIT_BUILD" != success ]; then if [ "$SAME_REPO" = false ] && [ "$EMIT_BUILD" = skipped ]; then echo "::notice::the emit-build lane is skipped for a fork pull request: no self-host or native-CLI emission verdict for this head"; else echo "::error::the emit-build lane produced no success (emit-build=$EMIT_BUILD), so this head carries no verdict from that lane"; exit 1; fi; fi
if [ "$FLOOR" != success ]; then if [ "$SAME_REPO" = false ] && [ "$FLOOR" = skipped ]; then echo "::notice::the fleet lane is skipped for a fork pull request: no witnesses fold and no generated-artifact verdict for this head"; else echo "::error::the fleet lane produced no success (floor=$FLOOR), so this head carries no verdict from that lane"; exit 1; fi; fi
if [ "$GENERATED" != success ]; then if [ "$SAME_REPO" = false ] && [ "$GENERATED" = skipped ]; then echo "::notice::the generated-artifact lane is skipped for a fork pull request: no generated-artifact verdict for this head"; else echo "::error::the generated-artifact lane produced no success (generated=$GENERATED), so this head carries no verdict from that lane"; exit 1; fi; fi
env:
EMIT_BUILD: ${{ needs['emit-build'].result }}
FLOOR: ${{ needs.floor.result }}
GENERATED: ${{ needs.generated.result }}
SAME_REPO: ${{ github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository }}
12 changes: 12 additions & 0 deletions dag/gunbc/instrument_targets.dag
Original file line number Diff line number Diff line change
Expand Up @@ -227,6 +227,18 @@ fn v2_native_cli_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "v2-native-cli" } }
}

// THE ENTRY EACH OF THE TWO SELF-HOST INSTRUMENTS EMITS, AS THE INSTRUMENT'S OWN FACT. Every
// reader of these entries -- the required-lane resolution census, and the seed's native lane runner
// whose constants test.claim.compiler_gate_emit_build_lane_witness_test holds against these rows --
// takes them from here, so a moved subject cannot leave a stale closure reported as covered.
fn self_host_entry() -> String {
"src/v2/compiler/00_compile.dag"
}

fn v2_native_cli_entry() -> String {
"src/v2/cli/compile_cli.dag"
}

// THE NATIVE FRONTIER INSTRUMENT: the same adjudicating run as the native route, over the whole
// v2.test.* universe, answered by gunbc.native_frontier_ratchet instead of by the lane's route
// qualification. The two are different questions. Qualification asks whether this run was a sound
Expand Down
21 changes: 19 additions & 2 deletions dag/gunbc/required_lane_resolution_census_live.dag
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,10 @@ import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }
import extdeps.github.actions { Workflow, Job }
import gunbc.compiler_gate_workflow {
compiler_gate_workflow, compiler_gate_merge_path_job_ids,
compiler_gate_floor_job_id, compiler_gate_generated_job_id, compiler_gate_aggregate_job_id,
compiler_gate_emit_build_job_id, compiler_gate_floor_job_id, compiler_gate_generated_job_id, compiler_gate_aggregate_job_id,
}
import gunbc.ci_spec { gunbc_ci_heal_verify_target }
import gunbc.instrument_targets { self_host_entry, v2_native_cli_entry }
import gunbc.ci_layer_roots { witness_layer_roots }
import gunbc.required_lane_resolution_census {
ModuleIdentityPopulation, ModuleIdentityPopulationObserved, ModuleIdentityPopulationRefused,
Expand All @@ -30,8 +31,23 @@ data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree
// roster does not is a refusal, never a job read as resolving nothing. The subject rows cite the
// same declarations the step scripts render from (gunbc.ci.ci_spec gunbc_ci_heal_verify_target
// for the drift gate's entry; the floor's nominal seeds through the compiler query).
//
// emit-build became required on 2026-10-02. Its two steps run `gunbc test` over
// //gunbc/instruments:self-host and //gunbc/instruments:v2-native-cli, whose producers
// (v1_compiler.cli_run.native_lane_runner NATIVE_COMPILE_ENTRY and V2_NATIVE_CLI_ENTRY) ingest
// and resolve the import closure of these two entries before emitting it. The entries are the
// instruments' own facts in gunbc.instrument_targets (self_host_entry, v2_native_cli_entry); the
// seed's two Rust constants cannot read a .dag row yet, so
// test.claim.compiler_gate_emit_build_lane_witness_test holds them equal to those rows and reds on drift.
fn lane_resolution_roster() -> List<LaneResolutionRow> {
[
LaneResolutionRow {
job_id: compiler_gate_emit_build_job_id,
subjects: [
RunEntryClosure { entry_path: self_host_entry() },
RunEntryClosure { entry_path: v2_native_cli_entry() },
]
},
LaneResolutionRow {
job_id: compiler_gate_floor_job_id,
subjects: [FloorNominalPreparedSubject {}]
Expand Down Expand Up @@ -73,7 +89,8 @@ fn count_of(xs: List<String>, x: String) -> Int {
// as not blocking is read by no required context, so a module only it resolves is resolved by no
// required lane, and a row for it would be the inflation this census exists to refuse. Checking
// coverage against every emitted job instead refused this census outright from the day `emit-build`
// landed announced, since that lane has no row and should not have one.
// landed announced (2026-09-22), when that lane had no row and should not have had one; it has one
// since it became required (2026-10-02).
fn required_job_ids(w: Workflow) -> List<String> {
let merge_path = compiler_gate_merge_path_job_ids()
workflow_job_ids(w: w) |> filter(j => count_of(xs: merge_path, x: j) > 0)
Expand Down
6 changes: 6 additions & 0 deletions dag/gunbc/rung_drop/v2_native_route_off_the_merge_path.dag
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,12 @@ import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable }
// change that rewrote it retired only the E0573 standing: `emit-build` stays hosted and announced,
// because a blocking lane may not run hosted (operator ruling 2026-09-28) and its fleet claim awaits
// operator sign-off. The nightly above was deleted by #12439, which rebound its own row here.
//
// HALF OF THE TRIGGER'S PRECONDITION LANDED 2026-10-02, AND THIS ROW STANDS. The operator signed off
// the fleet claim: `emit-build`'s row is LaneBlocks and the job runs on the fleet runner. The lane
// still executes only //gunbc/instruments:self-host and //gunbc/instruments:v2-native-cli, which the
// trigger names as NOT sufficient; it does not execute //gunbc/instruments:v2-native-frontier over
// the v2.test.* universe, so no run of it can fire this trigger yet. What remains is that step.

data v2_native_route_off_the_merge_path_population: List<String> = [
"gunbc.witness_v2_native_route native_route_admission — every receipt clause, on every merge candidate",
Expand Down
Loading