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
7 changes: 3 additions & 4 deletions dag/gunbc/compiler_frontend_program_status.dag
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,7 @@ import gunbc.self_host_compile_phase_frontier {
CompilePhaseFrontierEmpty,
CompilePhaseFrontierValidated,
CompilePhaseFrontierInvalid,
compile_phase_frontier_standing,
self_host_compile_phase_frontier_receipts,
current_compile_phase_frontier_standing,
self_host_compile_phase_ratchet_enrolment,
}
import v2.compiler.self_host.stage0_crate_layout { emitter_produced_divergent_registrations }
Expand Down Expand Up @@ -424,7 +423,7 @@ fn stage_subject_outstanding(stage: NamespaceCutStage) -> List<String> {
fn milestone_status(m: ProgramMilestone) -> MilestoneStanding {
match m {
SelfHostWholeCorpusPopulationDerived =>
match compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts) {
match current_compile_phase_frontier_standing() {
CompilePhaseFrontierValidated { latest } => standing_from_evidence(e: observe_outstanding(
subject: "self-host S2: whole-corpus compile-phase population derived from the latest validated frontier receipt" as NonEmptyStr,
outstanding: if latest.board.partition_complete { [] } else { latest.unplaced_identities }
Expand Down Expand Up @@ -497,7 +496,7 @@ fn milestone_status(m: ProgramMilestone) -> MilestoneStanding {
)
)
SelfHostCorpusEmitsCleanly =>
match compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts) {
match current_compile_phase_frontier_standing() {
CompilePhaseFrontierValidated { latest } => standing_from_evidence(e: observe_outstanding(
subject: "self-host: error diagnostics in the latest validated whole-corpus compile-phase receipt (coded and codeless)" as NonEmptyStr,
outstanding: latest.raw_error_diagnostic_identities
Expand Down
5 changes: 2 additions & 3 deletions dag/gunbc/design_ledgers.dag
Original file line number Diff line number Diff line change
Expand Up @@ -80,9 +80,8 @@ import gunbc.self_host_compile_phase_frontier {
CompilePhaseFrontierEmpty,
CompilePhaseFrontierValidated,
CompilePhaseFrontierInvalid,
compile_phase_frontier_standing,
current_compile_phase_frontier_standing,
render_phase_board,
self_host_compile_phase_frontier_receipts,
}

fn h1(text: String) -> MarkdownBlock { HeadingBlock { level: H1, inlines: [TextInline { text: text }] } }
Expand Down Expand Up @@ -138,7 +137,7 @@ fn failure_mode_document() -> MarkdownDocument {
}

fn compile_phase_frontier_blocks() -> List<MarkdownBlock> {
match compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts) {
match current_compile_phase_frontier_standing() {
CompilePhaseFrontierEmpty => [
h3(text: "Whole-corpus compile-phase frontier receipts"),
p(text: "No complete instrument observation has been appended; the next valid row must be the typed genesis receipt."),
Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/instruments/compile_phase_frontier_live_gate.dag
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ import extdeps.cargo_build
import gunbc.self_host_compile_phase_frontier {
TargetPinnedOnInvocation,
CompilePhaseInvocation,
self_host_compile_phase_frontier_receipts
current_compile_phase_frontier_standing
}
import extdeps.languages.rust.compiler_phases { rustc_phase_classification_policy_digest }
import gunbc.self_host_compile_phase_live_gate {
Expand Down Expand Up @@ -142,7 +142,7 @@ fn write_gate_report(report: String, m: EmissionMeasurement, verdict_text: Strin
// only other constructor for an observation does not exist.
fn adjudicate(report: String, m: EmissionMeasurement, reading: LiveToolchainReading) -> ProcessExit {
let verdict = live_tree_verdict_for_measurement(
series: self_host_compile_phase_frontier_receipts,
standing: current_compile_phase_frontier_standing(),
m: m,
toolchain: reading
)
Expand Down
29 changes: 29 additions & 0 deletions dag/gunbc/self_host_compile_phase_frontier.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1283,6 +1283,35 @@ fn compile_phase_frontier_standing(series: List<CompilePhaseFrontierReceipt>) ->
}
}

// THE STANDING OF THE PERSISTED SERIES -- one authority for the question five call sites were
// each spelling out.
//
// WHY IT EXISTS AS A DECLARATION RATHER THAN AS A REPEATED ARGUMENT. `compile_phase_frontier_standing`
// is general in its series: it judges ANY series of receipts, which is what its own witnesses
// exercise with perturbed fixtures. But there is only ONE persisted series in this repository, and
// "the standing of THAT series" is a distinct, singular fact that this module owns. Spelling the
// pairing at every consumer made the fact positional -- five sites each re-asserting the join --
// and DESIGN section 3 puts one fact in one place. Consumers that judge a HYPOTHETICAL series keep
// calling the general function directly; that distinction is the whole reason both spellings stay.
//
// THE COST CONSEQUENCE IS A CONSEQUENCE AND NOT THE REASON, but it is why the rewire happened now.
// The required floor builds a fresh evaluation frame per claim, so the eval-frame memo dies at
// every claim boundary and each claim re-derived this standing from scratch. Measured on main run
// 33664768371's `required_floor_cross_claim_demand.tsv`: 22 claims, 36 evaluations, 6508ms
// inclusive-of-callees, with `phase_board_series_ratchet` (23/23) and `apply_regression_transition`
// (23/23) nested underneath it. Being NULLARY, this declaration is preparation-forceable, so
// `v2.workflow.floor_pure_producer_share` can serve it as a WARM row with an empty argument row --
// no per-serve argument reification of the receipt series at all, which is the cost shape that
// disqualified earlier candidates from that roster. THAT IS A PROPERTY OF THIS DECLARATION AND NOT
// A CLAIM THAT A ROW EXISTS: no roster row is enrolled here, and the enrolment is held pending a
// present-vs-absent measurement on a tree that includes gunbc#10133, which made the recompute side
// of that comparison cheaper and so moved the denominator the earlier receipt was measured against.
// The census figures above predate it for the same reason. Re-derive with the instruments the
// roster names, never from these sentences.
fn current_compile_phase_frontier_standing() -> CompilePhaseFrontierStanding {
compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts)
}

// THE RATCHET ABOVE JUDGES RECEIPTS AGAINST EACH OTHER, AND NOTHING IN IT LOOKS AT THE TREE BEING
// MERGED. compile_phase_frontier_standing answers Validated{latest} from the persisted series
// alone, so its verdict is a claim about the TREE THE LATEST RECEIPT NAMES -- a past tree by
Expand Down
25 changes: 21 additions & 4 deletions dag/gunbc/self_host_compile_phase_live_gate.dag
Original file line number Diff line number Diff line change
Expand Up @@ -256,14 +256,14 @@ fn live_observation_from_measurement(
// The verdict for a measurement, which is the only entry point a consumer should use: it cannot be
// handed an observation that no measurement produced.
fn live_tree_verdict_for_measurement(
series: List<CompilePhaseFrontierReceipt>,
standing: CompilePhaseFrontierStanding,
m: EmissionMeasurement,
toolchain: LiveToolchainReading
) -> LiveFrontierVerdict {
match live_observation_from_measurement(m: m, toolchain: toolchain) {
LiveObservationNotTaken { cause: why } => LiveFrontierUnmeasured { reason: why }
LiveObservationTaken { observation: observation } =>
live_tree_frontier_verdict(series: series, observation: observation)
live_tree_frontier_verdict(standing: standing, observation: observation)
}
}

Expand All @@ -279,11 +279,28 @@ fn live_phase_board(observation: LiveCompilePhaseObservation) -> PersistedPhaseB
// board; a live tree carries no such authored disposition, so any identity the live board holds
// and the latest receipt does not refuses here. The remedy is to append a receipt -- to make the
// exposure a declared, checked fact -- and not to teach this gate to guess a cause.
// THE PARAMETER IS THE STANDING AND NOT THE SERIES, and the distinction is the difference between
// a parameter the body consumes and a parameter it merely passes through. Every use of `series`
// below was one call to `compile_phase_frontier_standing`; nothing else in this fold ever looked at
// a receipt list. Taking the series therefore declared a dependency wider than the body has, and
// the width was not free: it forced the fold to be RE-DERIVED at every call even when every caller
// meant the same persisted series, because the shared value was one level inside the parameter
// rather than being the parameter.
//
// TAKING THE STANDING KEEPS EVERY CALLER HONEST IN BOTH DIRECTIONS. A caller judging the live tree
// against THE persisted frontier passes `current_compile_phase_frontier_standing()`, which names
// that subject exactly and is servable across claim frames. A caller judging a PERTURBED series --
// which is what this module's witnesses exist to do -- passes
// `compile_phase_frontier_standing(series: <perturbed>)` and gets a genuine re-derivation, because
// its subject genuinely differs. Neither spelling can be mistaken for the other at a call site,
// which the old signature could not say: `series: self_host_compile_phase_frontier_receipts` and
// `series: self_host_compile_phase_frontier_receipts |> skip(n: 1)` are one character apart and
// mean entirely different subjects.
fn live_tree_frontier_verdict(
series: List<CompilePhaseFrontierReceipt>,
standing: CompilePhaseFrontierStanding,
observation: LiveCompilePhaseObservation
) -> LiveFrontierVerdict {
match compile_phase_frontier_standing(series: series) {
match standing {
CompilePhaseFrontierInvalid { reason: why } => LiveFrontierRefused {
identities: [],
reason: concat(
Expand Down
61 changes: 56 additions & 5 deletions dag/test/claim/self_host_compile_phase_frontier_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,6 @@ import gunbc.self_host_compile_phase_frontier {
PhaseBoardSeriesRefused,
ExposedByPhaseAdvance,
PhaseBoardSeriesHeld,
phase_board_series_ratchet,
self_host_compile_phase_frontier_receipts,
PersistedPhaseBoardFold,
phase_board_from_census_identities,
Expand All @@ -53,6 +52,7 @@ import gunbc.self_host_compile_phase_frontier {
board_row,
CompilePhaseFrontierValidated,
compile_phase_frontier_standing,
current_compile_phase_frontier_standing,
CompilePhaseFrontierCoverage,
FrontierCoversSubjectTree,
FrontierReceiptTreeStale,
Expand Down Expand Up @@ -180,10 +180,41 @@ fn fixture_board(resolve_ids: List<String>, typeck_ids: List<String>) -> RustcPh
// The required witness executes over the persisted series, not a fixture or a copied count. The
// genesis is the only row today; once a successor is appended this same call validates the link and
// applies the phase/identity ratchet to the latest validated pair.
// ASKED THROUGH THE STANDING RATHER THAN THROUGH THE RATCHET, and the two are not the same
// question by a hair: `CompilePhaseFrontierValidated` is `PhaseBoardSeriesHeld` AND a latest
// receipt existing, so this asserts strictly MORE than it did. The extra conjunct cannot go green
// where the old one went red -- a held series with no latest would now refuse here, which is the
// fail-closed direction.
//
// IT ALSO STOPS BEING THE MOST EXPENSIVE ROW IN THE CORPUS. Asking the ratchet directly re-derived
// the whole fold in this claim's own frame; asking the standing reads the value
// `v2.workflow.floor_pure_producer_share` already holds. Measured on this branch: 427ms on the
// absent arm and 461ms with the share enrolled but this row still folding for itself -- the single
// highest row in a 3499-row corpus at 92% of the 500ms ceiling.
//
// WHAT THIS ROW NOW TRUSTS, STATED PRECISELY, BECAUSE AN EARLIER REVISION OF THIS COMMENT OVERCLAIMED
// IT. It said this row's safety rested on
// `the_persisted_standing_accessor_agrees_with_the_general_fold_on_the_named_series` acting as the
// corpus's cache cross-check, which would make the share tier's correctness depend on one test in
// one module. That is the wrong home for that fact and it is not where it lives.
//
// THE SERVE IS THE TIER'S OWN GUARANTEE. `v2.workflow.floor_pure_producer_share` keys every entry on
// FN-NODE IDENTITY plus a content hash of the full argument row and serves only after the stored
// argument row verifies structurally equal in portable form, a hash collision degrading to
// recompute rather than to a wrong value. For a NULLARY producer the argument row is empty, so a
// wrong serve would mean one declaration's value returned under another declaration's node
// identity. That invariant is the tier's, it carries the tier's own evidence, and re-asserting it
// here would be a second authority for it.
//
// SO THE WITNESS BELOW GUARDS A DIFFERENT HAZARD, AND THE TWO WERE CONFLATED. Its subject is
// AUTHORING: whether `current_compile_phase_frontier_standing` names the series its name claims.
// That is decidable without the cache and is not a statement about serving at all. Its removal is
// an ordinary loss of a discriminating red -- which is a real loss -- and not a silent conversion of
// a verified share into an unverified one.
test fn current_persisted_compile_phase_frontier_holds() -> Bool {
match phase_board_series_ratchet(series: self_host_compile_phase_frontier_receipts) {
PhaseBoardSeriesHeld => true
verdict => false
match current_compile_phase_frontier_standing() {
CompilePhaseFrontierValidated { latest: _ } => true
standing => false
}
}

Expand Down Expand Up @@ -413,7 +444,7 @@ test fn the_persisted_genesis_census_is_fully_attributed_to_its_phases() -> Bool
// the document renders may not say the emitted compiler clears typeck or borrowck while the latest
// validated receipt's census says otherwise.
test fn the_published_frontier_standing_does_not_claim_typeck_or_borrowck_passed() -> Bool {
match compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts) {
match current_compile_phase_frontier_standing() {
CompilePhaseFrontierValidated { latest: latest } => {
let rendered = render_phase_board(board: latest.board)
!string_contains(s: rendered, pattern: "typeck PASSES")
Expand Down Expand Up @@ -787,3 +818,23 @@ test fn an_empty_series_refuses_coverage_rather_than_reporting_none_needed() ->
_ => false
}
}

// THE CONSOLIDATED ACCESSOR NAMES THE SAME SUBJECT AS THE SPELLING IT REPLACED.
//
// gunbc.self_host_compile_phase_frontier current_compile_phase_frontier_standing exists so that
// "the standing of THE persisted series" has one home instead of being re-spelled at five call
// sites. That consolidation has exactly one way to go wrong and it goes wrong SILENTLY: the
// accessor binds a DIFFERENT series -- a truncated one, a fixture one, a second data declaration
// added later -- and every consumer keeps compiling and keeps answering, about the wrong subject.
// No existing claim in either consuming closure would notice, because they all read the accessor
// and would agree with each other about the wrong thing.
//
// So this asserts the identity the rewire assumed, against the general function it delegates to,
// applied to the series by name. It is not a restatement of the delegation: it is authored one
// layer above it and it is the only executing place the two spellings are compared. Rebind the
// accessor to `self_host_compile_phase_frontier_receipts |> skip(n: 1)` -- the perturbation this
// module's sibling live-gate witnesses already use -- and this reds while nothing else does.
test fn the_persisted_standing_accessor_agrees_with_the_general_fold_on_the_named_series() -> Bool {
current_compile_phase_frontier_standing()
== compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts)
}
21 changes: 11 additions & 10 deletions dag/test/claim/self_host_compile_phase_live_gate_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ import gunbc.self_host_compile_phase_frontier {
CompilePhaseFrontierStanding,
CompilePhaseFrontierValidated,
compile_phase_frontier_standing,
current_compile_phase_frontier_standing,
self_host_compile_phase_frontier_receipts,
ParseReached,
CompilePhaseInvocation
Expand Down Expand Up @@ -47,7 +48,7 @@ import gunbc.self_host_compile_phase_live_gate {
data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

fn latest_receipt() -> CompilePhaseFrontierReceipt? {
match compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts) {
match current_compile_phase_frontier_standing() {
CompilePhaseFrontierValidated { latest: latest } => Present { value: latest }
standing => none
}
Expand Down Expand Up @@ -81,7 +82,7 @@ test fn a_live_census_equal_to_the_latest_receipt_holds() -> Bool {
Absent => false
Present { value: latest } =>
match live_tree_frontier_verdict(
series: self_host_compile_phase_frontier_receipts,
standing: current_compile_phase_frontier_standing(),
observation: observation_of(receipt: latest, identities: latest.raw_error_diagnostic_identities)
) {
LiveFrontierHeld { live_identity_count: n } => n == count(latest.raw_error_diagnostic_identities)
Expand All @@ -101,7 +102,7 @@ test fn a_live_tree_that_gained_an_identity_refuses_and_names_it() -> Bool {
Absent => false
Present { value: latest } =>
match live_tree_frontier_verdict(
series: self_host_compile_phase_frontier_receipts,
standing: current_compile_phase_frontier_standing(),
observation: observation_of(
receipt: latest,
identities: concat(latest.raw_error_diagnostic_identities, [planted_live_regression_identity])
Expand All @@ -122,7 +123,7 @@ test fn a_live_tree_that_swapped_an_identity_at_equal_cardinality_refuses() -> B
Absent => false
Present { value: latest } =>
match live_tree_frontier_verdict(
series: self_host_compile_phase_frontier_receipts,
standing: current_compile_phase_frontier_standing(),
observation: observation_of(
receipt: latest,
identities: concat(
Expand All @@ -146,7 +147,7 @@ test fn a_live_tree_that_removed_an_identity_holds() -> Bool {
Absent => false
Present { value: latest } =>
match live_tree_frontier_verdict(
series: self_host_compile_phase_frontier_receipts,
standing: current_compile_phase_frontier_standing(),
observation: observation_of(
receipt: latest,
identities: latest.raw_error_diagnostic_identities |> skip(n: 1)
Expand Down Expand Up @@ -181,7 +182,7 @@ test fn a_live_observation_from_another_host_target_is_unmeasured_not_held() ->
classification_policy_digest: latest.subject.classification_policy_digest
}
}
match live_tree_frontier_verdict(series: self_host_compile_phase_frontier_receipts, observation: foreign) {
match live_tree_frontier_verdict(standing: current_compile_phase_frontier_standing(), observation: foreign) {
LiveFrontierUnmeasured { reason: why } => string_contains(s: why as String, pattern: "host target")
verdict => false
}
Expand Down Expand Up @@ -245,7 +246,7 @@ test fn an_empty_receipt_series_leaves_the_live_tree_unmeasured_rather_than_held
Absent => false
Present { value: latest } =>
match live_tree_frontier_verdict(
series: [],
standing: compile_phase_frontier_standing(series: []),
observation: observation_of(receipt: latest, identities: latest.raw_error_diagnostic_identities)
) {
LiveFrontierUnmeasured { reason: why } => string_contains(s: why as String, pattern: "empty")
Expand All @@ -263,7 +264,7 @@ test fn a_non_validating_receipt_series_refuses_the_live_tree() -> Bool {
Absent => false
Present { value: latest } =>
match live_tree_frontier_verdict(
series: self_host_compile_phase_frontier_receipts |> skip(n: 1),
standing: compile_phase_frontier_standing(series: self_host_compile_phase_frontier_receipts |> skip(n: 1)),
observation: observation_of(receipt: latest, identities: latest.raw_error_diagnostic_identities)
) {
LiveFrontierRefused { identities: _, reason: why } =>
Expand Down Expand Up @@ -323,7 +324,7 @@ test fn a_measurement_that_never_reached_cargo_is_unmeasured_and_never_held() ->
Absent => false
Present { value: latest } =>
match live_tree_verdict_for_measurement(
series: self_host_compile_phase_frontier_receipts,
standing: current_compile_phase_frontier_standing(),
m: unreached_measurement,
toolchain: toolchain_of(receipt: latest)
) {
Expand Down Expand Up @@ -361,7 +362,7 @@ test fn an_empty_census_from_a_completed_measurement_still_holds() -> Bool {
Absent => false
Present { value: latest } =>
match live_tree_frontier_verdict(
series: self_host_compile_phase_frontier_receipts,
standing: current_compile_phase_frontier_standing(),
observation: observation_of(receipt: latest, identities: [])
) {
LiveFrontierHeld { live_identity_count: n } => n == 0
Expand Down
Loading