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
65 changes: 62 additions & 3 deletions dag/gunbc/emit_subject_clean_frontier.dag
Original file line number Diff line number Diff line change
Expand Up @@ -802,6 +802,7 @@ type EmitRatchetVerdict
| RatchetFrontierStale { entry: String }
| RatchetNotEvaluated { entry: String, on_frontier: Bool, cause: EmitNotEvaluatedCause }
| RatchetSubjectUnmeasured { entry: String, on_frontier: Bool }
| RatchetSubjectNotSelected { entry: String, on_frontier: Bool }

fn emit_ratchet_verdict_entry(v: EmitRatchetVerdict) -> String {
match v {
Expand All @@ -811,6 +812,7 @@ fn emit_ratchet_verdict_entry(v: EmitRatchetVerdict) -> String {
RatchetFrontierStale { entry: e } => e
RatchetNotEvaluated { entry: e, on_frontier: _, cause: _ } => e
RatchetSubjectUnmeasured { entry: e, on_frontier: _ } => e
RatchetSubjectNotSelected { entry: e, on_frontier: _ } => e
}
}

Expand Down Expand Up @@ -850,6 +852,7 @@ fn emit_ratchet_verdict_standing(v: EmitRatchetVerdict) -> VerdictStanding {
RatchetFrontierStale { entry: _ } => VerdictEstablishedAndRefused
RatchetNotEvaluated { entry: _, on_frontier: _, cause: _ } => VerdictUnestablished
RatchetSubjectUnmeasured { entry: _, on_frontier: _ } => VerdictUnestablished
RatchetSubjectNotSelected { entry: _, on_frontier: _ } => VerdictUnestablished
}
}

Expand Down Expand Up @@ -891,7 +894,12 @@ fn emit_ratchet_verdict_row(v: EmitRatchetVerdict) -> String {
RatchetSubjectUnmeasured { entry: e, on_frontier: f } =>
concat(
concat(concat("UNMEASURED\t", e), concat("\ton_frontier\t", to_string(f))),
"\tthe fold was handed no measurement for this roster subject — a partial run cannot answer a closed-universe claim"
"\tthe instrument was asked about this subject and produced no reading for it — a deficit in the run, not its scope"
)
RatchetSubjectNotSelected { entry: e, on_frontier: f } =>
concat(
concat(concat("NOT-SELECTED\t", e), concat("\ton_frontier\t", to_string(f))),
"\tthis run measured a subset and never asked about this subject — scope rather than a deficit, and still not a verdict"
)
}
}
Expand Down Expand Up @@ -952,9 +960,56 @@ fn lookup_subject_reading(readings: List<EmitSubjectReading>, entry: String) ->
)
}

fn emit_ratchet_verdict_for(entry: String, on_frontier: Bool, readings: List<EmitSubjectReading>) -> EmitRatchetVerdict {
// ---------------------------------------------------------------------------------------------
// THE SELECTION, WHICH IS WHY "NO VERDICT" IS TWO FACTS AND NOT ONE.
//
// A roster subject can arrive at the fold with no reading for two reasons that share nothing but
// their silence. Either the run ASKED about it and the instrument produced nothing -- a deficit in
// the run -- or the run never asked, because `entries` named a subset. The owners are opposite:
// the first is an instrument to fix, the second is a run to widen, and a reader handed one
// UNMEASURED count cannot tell which they are looking at.
//
// This module already draws exactly this distinction correctly one axis over: an admission row
// naming a subject the roster lacks is reported as an ORPHAN rather than as a missing measurement,
// because the two have opposite owners. The selection axis is the same shape and did not get the
// same treatment, so it is given one here.
//
// THE CARRIER IS A COPRODUCT AND NOT A LIST, deliberately. A bare `List<String>` would make the
// empty list mean both a subset naming nothing and no subsetting at all -- the state-space
// conflation this type exists to remove, reintroduced in the type that removes it.
type SubjectSelection
= SelectionWholeRoster
| SelectionSubset { entries: List<String> }

fn subject_was_selected(selection: SubjectSelection, entry: String) -> Bool {
match selection {
SelectionWholeRoster => true
SelectionSubset { entries: es } => string_list_contains(xs: es, wanted: entry)
}
}

// The subjects an instrument should be invoked over, which is the SAME value the classification
// above reads. A caller deriving this list independently of the selection is how the two drift.
fn subject_selection_entries(selection: SubjectSelection, roster: List<String>) -> List<String> {
match selection {
SelectionWholeRoster => roster
SelectionSubset { entries: es } => es
}
}

fn emit_ratchet_verdict_for(
entry: String,
on_frontier: Bool,
selection: SubjectSelection,
readings: List<EmitSubjectReading>
) -> EmitRatchetVerdict {
match lookup_subject_reading(readings: readings, entry: entry) {
SubjectReadingAbsent => RatchetSubjectUnmeasured { entry: entry, on_frontier: on_frontier }
SubjectReadingAbsent =>
if subject_was_selected(selection: selection, entry: entry) {
RatchetSubjectUnmeasured { entry: entry, on_frontier: on_frontier }
} else {
RatchetSubjectNotSelected { entry: entry, on_frontier: on_frontier }
}
SubjectReadingFound { reading: reading } =>
emit_ratchet_verdict_of_outcome(
entry: entry,
Expand Down Expand Up @@ -982,6 +1037,7 @@ type EmitSubjectCleanRatchet {
fn fold_emit_subject_clean_ratchet_over_readings(
universe: RatchetUniverse,
admissions: List<EmitDebtAdmission>,
selection: SubjectSelection,
readings: List<EmitSubjectReading>
) -> EmitSubjectCleanRatchet {
let keys = map(admissions, a => emit_debt_admission_entry(admission: a))
Expand All @@ -995,6 +1051,7 @@ fn fold_emit_subject_clean_ratchet_over_readings(
emit_ratchet_verdict_for(
entry: entry,
on_frontier: string_list_contains(xs: keys, wanted: entry),
selection: selection,
readings: all_readings
)
),
Expand All @@ -1020,11 +1077,13 @@ fn fold_emit_subject_clean_ratchet_over_readings(
fn fold_emit_subject_clean_ratchet(
universe: RatchetUniverse,
admissions: List<EmitDebtAdmission>,
selection: SubjectSelection,
measurements: List<EmissionMeasurement>
) -> EmitSubjectCleanRatchet {
fold_emit_subject_clean_ratchet_over_readings(
universe: universe,
admissions: admissions,
selection: selection,
readings: map(measurements, m => emit_subject_reading(m: m))
)
}
Expand Down
62 changes: 60 additions & 2 deletions dag/test/claim/emit_subject_clean_frontier_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -57,6 +57,7 @@ fn fixture_fold_of(
fold_emit_subject_clean_ratchet_over_readings(
universe: IndexOnlyUniverse { policy: fixture_policy(), entries: roster },
admissions: admissions,
selection: SelectionWholeRoster,
readings: readings
)
}
Expand Down Expand Up @@ -105,6 +106,7 @@ fn fixture_dual_fold(
inventory: inventory
},
admissions: [],
selection: SelectionWholeRoster,
readings: readings
)
}
Expand Down Expand Up @@ -269,7 +271,7 @@ test fn a_partial_run_refuses_and_names_the_subjects_it_did_not_measure() -> Boo
let readings = [fixture_reading(entry: fixture_alpha, outcome: EmitSubjectClean)]
!fixture_standing_holds(roster: fixture_roster, admissions: [], readings: readings)
&& fixture_failing_rows(roster: fixture_roster, admissions: [], readings: readings)
== ["UNMEASURED\tdag/fixture/beta.dag\ton_frontier\tfalse\tthe fold was handed no measurement for this roster subject — a partial run cannot answer a closed-universe claim"]
== ["UNMEASURED\tdag/fixture/beta.dag\ton_frontier\tfalse\tthe instrument was asked about this subject and produced no reading for it — a deficit in the run, not its scope"]
}

// RED: an admission row naming a subject the discovered roster does not contain is a row to delete,
Expand Down Expand Up @@ -451,6 +453,7 @@ test fn a_measurement_cannot_overwrite_an_unclassified_files_classification() ->
inventory: [fixture_alpha, fixture_beta, hidden]
},
admissions: [],
selection: SelectionWholeRoster,
readings: concat(fixture_both_clean(), [fixture_reading(entry: hidden, outcome: EmitSubjectClean)])
)
count(
Expand Down Expand Up @@ -495,6 +498,7 @@ fn fixture_empty_dual_fold() -> EmitSubjectCleanRatchet {
fold_emit_subject_clean_ratchet_over_readings(
universe: DualUniverse { policy: fixture_policy(), entries: [], inventory: [] },
admissions: [],
selection: SelectionWholeRoster,
readings: []
)
}
Expand Down Expand Up @@ -767,13 +771,67 @@ test fn the_ratchet_runner_has_no_executing_consumer_today() -> Bool {
// by measuring them against each other, which is exactly how it came up in review. Routing both
// through `emit_ratchet_verdict_standing` makes the divergence a named class, and this claim pins
// the two properties that make the split load-bearing rather than decorative.

// ---------------------------------------------------------------------------------------------
// THE SELECTION SPLIT: ONE SILENCE, TWO OWNERS.
//
// A roster subject with no reading used to render as UNMEASURED whether the run had asked about it
// or not. The two facts have opposite remedies -- fix the instrument, or widen the run -- so a
// reader handed one count could not tell which they were looking at. The pair below is the whole
// evidence for the split, and it is a ONE-FIELD control: the roster, the admissions and the
// readings are IDENTICAL across both claims and only the selection differs. A green that survived
// collapsing the two arms would therefore have to be an accident of the selection alone.
// ---------------------------------------------------------------------------------------------

fn fixture_beta_verdict_under(selection: SubjectSelection) -> List<EmitRatchetVerdict> {
filter(
fold_emit_subject_clean_ratchet_over_readings(
universe: IndexOnlyUniverse { policy: fixture_policy(), entries: fixture_roster },
admissions: [],
selection: selection,
readings: [fixture_reading(entry: fixture_alpha, outcome: EmitSubjectClean)]
).verdicts,
v => emit_ratchet_verdict_entry(v: v) == fixture_beta
)
}

// RED: a subject the run never asked about must not be reported as one the instrument failed on.
// If the classifier stops consulting the selection, this arm collapses into the one below.
test fn a_subject_the_run_never_selected_is_scope_rather_than_a_deficit() -> Bool {
fixture_beta_verdict_under(selection: SelectionSubset { entries: [fixture_alpha] })
== [RatchetSubjectNotSelected { entry: fixture_beta, on_frontier: false }]
}

// RED: the same silence, from a run that DID ask, is a deficit and keeps its old name. This is the
// control that makes the claim above discriminating rather than a rename.
test fn a_subject_the_run_selected_and_could_not_measure_is_still_a_deficit() -> Bool {
fixture_beta_verdict_under(selection: SelectionWholeRoster)
== [RatchetSubjectUnmeasured { entry: fixture_beta, on_frontier: false }]
}

// NEITHER IS A VERDICT. The split names two owners; it does not promote scope into evidence, and a
// gate must still refuse over both. If the new arm were ever classified as established, a subset
// run would start answering a closed-universe question it never asked.
test fn neither_silence_establishes_a_verdict() -> Bool {
count(
filter(
[
RatchetSubjectNotSelected { entry: fixture_beta, on_frontier: false },
RatchetSubjectUnmeasured { entry: fixture_beta, on_frontier: false }
],
v => emit_ratchet_verdict_evaluated(v: v) || emit_ratchet_verdict_holds(v: v)
)
) == 0
}

data every_verdict_shape: List<EmitRatchetVerdict> = [
RatchetCleanHeld { entry: fixture_alpha },
RatchetDebtHeld { entry: fixture_alpha, cause: BlockingDiagnostics { blocking: 1 } },
RatchetRegressed { entry: fixture_alpha, cause: BlockingDiagnostics { blocking: 1 } },
RatchetFrontierStale { entry: fixture_alpha },
RatchetNotEvaluated { entry: fixture_alpha, on_frontier: false, cause: ExtentUnestablished },
RatchetSubjectUnmeasured { entry: fixture_alpha, on_frontier: false }
RatchetSubjectUnmeasured { entry: fixture_alpha, on_frontier: false },
RatchetSubjectNotSelected { entry: fixture_alpha, on_frontier: false }
]

// A HELD VERDICT IS ALWAYS AN EVALUATED ONE -- the ratchet cannot hold over a subject nobody
Expand Down
28 changes: 20 additions & 8 deletions dag/tools/emit_subject_clean_ratchet.dag
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,10 @@ import gunbc.emit_subject_clean_frontier {
ObservationNotTaken,
RosterDiscoveryPolicy,
DeclarationIndexUnderRoots,
SubjectSelection,
SelectionWholeRoster,
SelectionSubset,
subject_selection_entries,
emit_subject_clean_admissions,
emit_ratchet_report_text,
emit_ratchet_standing,
Expand Down Expand Up @@ -138,35 +142,43 @@ fn module_inventory(roots: List<String>) -> ModuleInventoryRead {
)
}

fn selected_entries(entries: String, roster: List<String>) -> List<String> {
// An empty `entries` is WHOLE-ROSTER and not an empty subset. That is the one place the two could
// have been conflated, and the coproduct is what keeps them apart all the way to the report.
fn subject_selection(entries: String, roster: List<String>) -> SubjectSelection {
if entries == "" {
roster
SelectionWholeRoster
} else {
fold(
split(s: entries, delimiter: ","),
init: [],
f: (acc, e) => if e == "" { acc } else { concat(acc, [e]) }
)
SelectionSubset {
entries: filter(split(s: entries, delimiter: ","), e => e != "")
}
}
}

fn measure_selected(selection: List<String>) -> List<EmissionMeasurement> {
map(selection, entry => measure_entry_emission(entry: entry))
}

// ONE SELECTION, READ TWICE. The list the instrument is invoked over and the selection the fold
// classifies against are derived from the same value rather than computed twice from `entries` --
// two derivations could disagree, and a disagreement here would render as an UNMEASURED subject
// the run had in fact measured, which is the precise confusion the selection carrier removes.
fn run_emit_subject_clean_ratchet(
entries: String,
roster: List<String>,
inventory: List<String>
) -> EmitSubjectCleanRatchet {
let selection = subject_selection(entries: entries, roster: roster)
fold_emit_subject_clean_ratchet(
universe: DualUniverse {
policy: emit_subject_clean_roster_policy,
entries: roster,
inventory: inventory
},
admissions: emit_subject_clean_admissions,
measurements: measure_selected(selection: selected_entries(entries: entries, roster: roster))
selection: selection,
measurements: measure_selected(
selection: subject_selection_entries(selection: selection, roster: roster)
)
)
}

Expand Down
Loading