Skip to content

Floor cost repair: one producer, not three witnesses — the compile-phase frontier standing crosses the 500ms CPU ceiling and makes the required floor a coin flip #10133

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
briansrls merged 1 commit into from
Sep 2, 2026
Merged

Floor cost repair: one producer, not three witnesses — the compile-phase frontier standing crosses the 500ms CPU ceiling and makes the required floor a coin flip #10133

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
112 changes: 96 additions & 16 deletions dag/gunbc/self_host_compile_phase_frontier.dag
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -823,7 +823,8 @@ fn phase_ratchet(previous: RustcPhaseBoard, current: RustcPhaseBoard) -> PhaseRa
PhaseRatchetHeld => match board_row(board: current, phase: old.phase) {
Absent => PhaseRatchetRefused { phase: old.phase, identities: [], reason: "current board omitted a phase" as NonEmptyStr }
Present { value: now } => {
let added = now.identities |> filter(identity => !any(old.identities, prior => prior == identity))
let prior = identity_membership_index(identities: old.identities)
let added = now.identities |> filter(identity => !map_contains_key(prior, identity))
if phase_closed_at_zero(row: old) && phase_reached_with_diagnostics(row: now) {
PhaseRatchetRefused { phase: old.phase, identities: now.identities, reason: "a closed phase regained diagnostic identities" as NonEmptyStr }
} else if rustc_phase_order(phase: old.phase) == rustc_phase_order(phase: previous.furthest_phase_reached) && phase_count_increased(old: old, now: now) {
Expand All @@ -843,9 +844,25 @@ type RegressionTransitionVerdict
= RegressionTransitionHeld { open_unadmitted: List<OpenUnadmittedRegression> }
| RegressionTransitionMalformed { reason: NonEmptyStr }

// MEMBERSHIP IS ASKED ONCE PER ROW OF THE OTHER POPULATION, SO IT IS INDEXED ONCE RATHER THAN
// SCANNED PER ROW. Both differences here used to answer each membership question with `any` over
// the other board's whole identity list, which makes the comparison count the PRODUCT of two
// populations that only grow with every receipt -- the quadratic fold DESIGN section 6 fixes
// regardless of the realized n. A board is a census at identity grain (the note on
// `deduplicate_identities` above states why encounter order is not semantic), so an
// identity-keyed index is the same fact in the representation the question actually asks for,
// never a second authority over it.
fn identity_membership_index(identities: List<String>) -> Map<String, Bool> {
fold(identities, init: {}, f: (seen, identity) => map_insert(seen, identity, true))
}

fn board_identity_index(board: RustcPhaseBoard) -> Map<String, Bool> {
identity_membership_index(identities: board_all_identities(board: board))
}

fn board_added_identities(previous: RustcPhaseBoard, current: RustcPhaseBoard) -> List<String> {
board_all_identities(board: current)
|> filter(identity => !any(board_all_identities(board: previous), prior => prior == identity))
let prior = board_identity_index(board: previous)
board_all_identities(board: current) |> filter(identity => !map_contains_key(prior, identity))
}

fn diagnostic_identity_file(identity: String) -> String {
Expand All @@ -859,8 +876,8 @@ fn diagnostic_semantic_key(identity: String) -> String {
}

fn board_removed_identities(previous: RustcPhaseBoard, current: RustcPhaseBoard) -> List<String> {
board_all_identities(board: previous)
|> filter(identity => !any(board_all_identities(board: current), now => now == identity))
let now = board_identity_index(board: current)
board_all_identities(board: previous) |> filter(identity => !map_contains_key(now, identity))
}

type RegressionComparisonPredecessor
Expand Down Expand Up @@ -893,14 +910,34 @@ fn regression_comparison_predecessor(
}
}

// THE SEMANTIC KEYS OF ONE TRANSITION'S ADDED AND REMOVED POPULATIONS, DERIVED ONCE.
//
// The hop test below is asked once per added identity and each answer needs the key of EVERY row
// in both populations. Deriving those keys inside the test made the count of `diagnostic_semantic_key`
// calls the PRODUCT of the two populations rather than their sum -- a quadratic fold over a
// population that only grows, which DESIGN section 6 fixes on sight rather than on the realized n.
// The keys depend on the transition and not on the identity being tested, so this is exactly the
// demand DESIGN section 2 says to satisfy at the least common ancestor: `apply_regression_transition`
// builds one index and every test reads it.
type HopRelocationIndex {
added_keys: List<String>
removed_keys: List<String>
}

fn hop_relocation_index(added: List<String>, removed: List<String>) -> HopRelocationIndex {
HopRelocationIndex {
added_keys: added |> map(row => diagnostic_semantic_key(identity: row)),
removed_keys: removed |> map(row => diagnostic_semantic_key(identity: row))
}
}

fn identity_is_hop_relocation(
identity: String,
added: List<String>,
removed: List<String>
index: HopRelocationIndex
) -> Bool {
let key = diagnostic_semantic_key(identity: identity)
let added_same = added |> filter(row => diagnostic_semantic_key(identity: row) == key) |> count
let removed_same = removed |> filter(row => diagnostic_semantic_key(identity: row) == key) |> count
let added_same = index.added_keys |> filter(row => row == key) |> count
let removed_same = index.removed_keys |> filter(row => row == key) |> count
removed_same > 0 && added_same <= removed_same
}

Expand Down Expand Up @@ -974,6 +1011,7 @@ fn apply_regression_transition(
RegressionComparisonAvailable { board: comparable_previous } => {
let added = board_added_identities(previous: comparable_previous, current: current.board)
let removed = board_removed_identities(previous: comparable_previous, current: current.board)
let hop_index = hop_relocation_index(added: added, removed: removed)
let admitted = added |> filter(identity => newly_exposed_identity_admitted(
previous: comparable_previous,
current: current.board,
Expand All @@ -982,7 +1020,7 @@ fn apply_regression_transition(
))
let unadmitted = added |> filter(identity =>
!any(admitted, row => row == identity)
&& !identity_is_hop_relocation(identity: identity, added: added, removed: removed)
&& !identity_is_hop_relocation(identity: identity, index: hop_index)
)
let ratchet_recoverable = match phase_ratchet_with_dispositions(
previous: comparable_previous,
Expand All @@ -994,7 +1032,7 @@ fn apply_regression_transition(
count(ids) > 0 && all(ids, identity =>
any(unadmitted, row => row == identity)
|| any(admitted, row => row == identity)
|| identity_is_hop_relocation(identity: identity, added: added, removed: removed)
|| identity_is_hop_relocation(identity: identity, index: hop_index)
)
}
if !ratchet_recoverable {
Expand All @@ -1018,13 +1056,17 @@ fn board_all_identities(board: RustcPhaseBoard) -> List<String> {
board.rows |> flat_map(r => r.identities)
}

fn newly_exposed_identity_admitted(
// WHETHER ONE DISPOSITION'S CAUSE ADMITS ONE IDENTITY. Split out of
// `newly_exposed_identity_admitted` below so the SELECTION of the disposition row happens before
// this derivation is demanded at all; the two halves are stated separately because only the
// selection half is cheap.
fn newly_exposed_cause_admits(
previous: RustcPhaseBoard,
current: RustcPhaseBoard,
dispositions: List<NewlyExposedDiagnostic>,
identity: String
identity: String,
cause: NewlyExposedCause
) -> Bool {
any(dispositions, row => row.identity == identity && match row.cause {
match cause {
ExposedByRemovedMaskingIdentity { removed_identity: masking } =>
any(board_all_identities(board: previous), prior => prior == masking)
&& !any(board_all_identities(board: current), now => now == masking)
Expand All @@ -1035,7 +1077,45 @@ fn newly_exposed_identity_admitted(
ExposedByNewEmittedModule { module: file } =>
diagnostic_identity_file(identity: identity) == file
&& !any(board_all_identities(board: previous), prior => diagnostic_identity_file(identity: prior) == file)
})
}
}

// THE FILTER IS THE WHOLE POINT AND IT IS NOT A STYLE CHOICE. This read as
// `any(dispositions, row => row.identity == identity && <cause derivation>)`, and `&&` in this
// substrate EVALUATES BOTH OPERANDS: `v1_interpreter` `eval_expr_inner` evaluates the left and the
// right of an `ExprBinOp` before it applies the operator, so a cheap guard conjoined ahead of an
// expensive derivation guards NOTHING at evaluation time -- it only narrows the result. The
// short-circuit an author carries over from Rust or C is not a property of this language, and the
// emitted Rust for the same expression DOES short-circuit, so the two differ in what they evaluate
// while agreeing on what they answer. So the cause derivation ran once per (added identity x disposition row)
// pair rather than once per row that actually names the identity, and two of its three arms scan
// the whole previous board, one of them re-splitting every identity on it. Selecting the rows
// first makes the demand graph match the question being asked (DESIGN section 2: minimize the
// demand graph before materializing its answers), and it is EXACTLY equivalent rather than merely
// close: for boolean p and q, `any(xs, p && q)` and `any(filter(xs, p), q)` agree on every input,
// including the empty and the multiple-matching-rows cases.
//
// MEASURED, because "n is small here" is the claim DESIGN section 6 refuses. This function was the
// single largest term in `compile_phase_frontier_standing`, which is the whole cost of three
// required-floor witness modules -- gunbc.self_host_compile_phase_live_gate's witness,
// this module's own witness, and test.claim.compiler_frontend_program_status_witness through
// `gunbc.compiler_frontend_program_status` `milestone_status`. The instrument is
// `claim_batch --entry <the witness> --functions <its rows>`; the figures are not transcribed here.
fn newly_exposed_identity_admitted(
previous: RustcPhaseBoard,
current: RustcPhaseBoard,
dispositions: List<NewlyExposedDiagnostic>,
identity: String
) -> Bool {
any(
dispositions |> filter(row => row.identity == identity),
row => newly_exposed_cause_admits(
previous: previous,
current: current,
identity: identity,
cause: row.cause
)
)
}

fn phase_ratchet_with_dispositions(
Expand Down
Loading