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
52 changes: 50 additions & 2 deletions dag/gunbc/namespace/namespace_step0_canary_v2.dag
Original file line number Diff line number Diff line change
Expand Up @@ -206,14 +206,62 @@ fn step0_import_dependence_not_judged() -> Step0ImportDependenceStanding {
// the rewrite -- and a raw byte span is not that identity, because deleting an import shifts every
// later offset in the file. That join is Step 0 evidence work with its own owner; it is deliberately
// not pulled in here to make two red totals sound cleaner than they are.
// THE DIFFERENCED POPULATION IS A TYPED FIELD OF THE DIFFERENTIAL, because the headline and the
// differential do NOT range over the same rows and nothing said so. step0_blocking_measure filters
// to row.blocking; step0_histogram_differential is handed the FULL census. Both figures were
// arithmetically correct and were printed side by side, and a reader who differenced the blocking
// occurrences could not reconcile the result with gross_increases -- the LABELLING was the defect.
// A caption cannot carry that fact: a caption is prose the substrate cannot read (DESIGN 4c), and
// the reader who needs it is reading a value. So the domain travels INSIDE the value, and every
// renderer of a delta prints it from there.
type Step0DifferentialDomain
= EveryCensusRow
| BlockingCensusRowsOnly

fn step0_differential_domain_label(domain: Step0DifferentialDomain) -> NonEmptyStr {
match domain {
EveryCensusRow => "every census row, blocking and advisory alike" as NonEmptyStr
BlockingCensusRowsOnly => "only census rows whose blocking flag is set" as NonEmptyStr
}
}

// FOUR PRIMITIVE OCCURRENCE MOVEMENTS, NOT TWO GROSS ONES, and the split is what makes a
// conservation identity WRITABLE at all. The prior model folded a post-only bucket's whole count
// into gross_increases, so shared-bucket growth and wholly-new buckets were one number: no identity
// could be stated over them, and therefore nothing could catch a domain mismatch between the
// headline and the delta -- precisely the class this receipt exists to refuse. gross_increases and
// gross_decreases survive as DERIVED projections rather than stored fields (DESIGN section 2), so
// the two views cannot disagree.
type Step0HistogramDifferential {
gross_increases: Int
gross_decreases: Int
domain: Step0DifferentialDomain
pre_occurrences: Int
post_occurrences: Int
shared_increases: Int
shared_decreases: Int
pre_only_occurrences: Int
post_only_occurrences: Int
unchanged_buckets: Int
pre_only_buckets: Int
post_only_buckets: Int
}

fn step0_differential_gross_increases(differential: Step0HistogramDifferential) -> Int {
differential.shared_increases + differential.post_only_occurrences
}

fn step0_differential_gross_decreases(differential: Step0HistogramDifferential) -> Int {
differential.shared_decreases + differential.pre_only_occurrences
}

// THE CONSERVATION IDENTITY, AND IT IS A JOIN BETWEEN TWO PRODUCERS RATHER THAN measure() ==
// measure(). The left side is each arm's own occurrence total, summed over the row lists directly.
// The right side is the bucket-by-bucket fold's four movements. They are computed by different
// walks over the same rows, so a delta whose domain does not match the totals it is differenced
// against cannot satisfy it. A violation is a refusal, never a printed number.
fn step0_differential_conserves(differential: Step0HistogramDifferential) -> Bool {
(differential.post_occurrences - differential.pre_occurrences) == ((differential.shared_increases + differential.post_only_occurrences) - (differential.shared_decreases + differential.pre_only_occurrences))
}

type Step0DifferentialStanding
= HistogramsIdentical
| HistogramBucketsChanged { differential: Step0HistogramDifferential }
Expand Down
124 changes: 102 additions & 22 deletions dag/gunbc/namespace/namespace_step0_candidate_run.dag
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,9 @@ import gunbc.namespace_step0_canary_v2 {
CompileAttemptedAndRefused,
CompileAttemptedAndCompleted,
Step0HistogramDifferential,
Step0DifferentialDomain,
EveryCensusRow,
BlockingCensusRowsOnly,
Step0DifferentialStanding,
HistogramsIdentical,
HistogramBucketsChanged,
Expand All @@ -78,6 +81,10 @@ import gunbc.namespace_step0_canary_v2 {
OrderInvarianceHeld,
OrderInvarianceViolated,
OrderInvarianceNotMeasured,
step0_differential_conserves,
step0_differential_domain_label,
step0_differential_gross_decreases,
step0_differential_gross_increases,
step0_v2_entered_prefix_for,
admit_namespace_step0_v2_receipt,
namespace_step0_canary_v2_contract,
Expand Down Expand Up @@ -316,33 +323,53 @@ fn step0_differential_left_step(
) -> Step0HistogramDifferential {
match map_get(post_index, step0_row_key(row: row)) {
Absent => Step0HistogramDifferential {
gross_increases: acc.gross_increases,
gross_decreases: acc.gross_decreases + row.count,
domain: acc.domain,
pre_occurrences: acc.pre_occurrences,
post_occurrences: acc.post_occurrences,
shared_increases: acc.shared_increases,
shared_decreases: acc.shared_decreases,
pre_only_occurrences: acc.pre_only_occurrences + row.count,
post_only_occurrences: acc.post_only_occurrences,
unchanged_buckets: acc.unchanged_buckets,
pre_only_buckets: acc.pre_only_buckets + 1,
post_only_buckets: acc.post_only_buckets
}
Present { value: other } =>
if other > row.count {
Step0HistogramDifferential {
gross_increases: acc.gross_increases + (other - row.count),
gross_decreases: acc.gross_decreases,
domain: acc.domain,
pre_occurrences: acc.pre_occurrences,
post_occurrences: acc.post_occurrences,
shared_increases: acc.shared_increases + (other - row.count),
shared_decreases: acc.shared_decreases,
pre_only_occurrences: acc.pre_only_occurrences,
post_only_occurrences: acc.post_only_occurrences,
unchanged_buckets: acc.unchanged_buckets,
pre_only_buckets: acc.pre_only_buckets,
post_only_buckets: acc.post_only_buckets
}
} else if row.count > other {
Step0HistogramDifferential {
gross_increases: acc.gross_increases,
gross_decreases: acc.gross_decreases + (row.count - other),
domain: acc.domain,
pre_occurrences: acc.pre_occurrences,
post_occurrences: acc.post_occurrences,
shared_increases: acc.shared_increases,
shared_decreases: acc.shared_decreases + (row.count - other),
pre_only_occurrences: acc.pre_only_occurrences,
post_only_occurrences: acc.post_only_occurrences,
unchanged_buckets: acc.unchanged_buckets,
pre_only_buckets: acc.pre_only_buckets,
post_only_buckets: acc.post_only_buckets
}
} else {
Step0HistogramDifferential {
gross_increases: acc.gross_increases,
gross_decreases: acc.gross_decreases,
domain: acc.domain,
pre_occurrences: acc.pre_occurrences,
post_occurrences: acc.post_occurrences,
shared_increases: acc.shared_increases,
shared_decreases: acc.shared_decreases,
pre_only_occurrences: acc.pre_only_occurrences,
post_only_occurrences: acc.post_only_occurrences,
unchanged_buckets: acc.unchanged_buckets + 1,
pre_only_buckets: acc.pre_only_buckets,
post_only_buckets: acc.post_only_buckets
Expand All @@ -359,15 +386,28 @@ fn step0_differential_right_step(
match map_get(pre_index, step0_row_key(row: row)) {
Present { value: _ } => acc
Absent => Step0HistogramDifferential {
gross_increases: acc.gross_increases + row.count,
gross_decreases: acc.gross_decreases,
domain: acc.domain,
pre_occurrences: acc.pre_occurrences,
post_occurrences: acc.post_occurrences,
shared_increases: acc.shared_increases,
shared_decreases: acc.shared_decreases,
pre_only_occurrences: acc.pre_only_occurrences,
post_only_occurrences: acc.post_only_occurrences + row.count,
unchanged_buckets: acc.unchanged_buckets,
pre_only_buckets: acc.pre_only_buckets,
post_only_buckets: acc.post_only_buckets + 1
}
}
}

// THE OCCURRENCE TOTAL OF A ROW LIST, walked directly rather than accumulated by the bucket fold.
// That independence is the whole value of it: the conservation identity below joins this walk's
// answer to the fold's four movements, so the two cannot be the same measurement compared with
// itself.
fn step0_census_occurrences(rows: List<CompileDiagnosticCensusRow>) -> Int {
fold(rows, init: 0, f: fn(acc, row) { acc + row.count })
}

type Step0DifferentialOutcome
= Step0DifferentialUndefined { cause: NonEmptyStr }
| Step0DifferentialComputed { differential: Step0HistogramDifferential }
Expand All @@ -386,19 +426,35 @@ fn step0_histogram_differential(
}
HistogramIndexed { index: post_index } => {
let left = fold(pre, init: Step0HistogramDifferential {
gross_increases: 0, gross_decreases: 0, unchanged_buckets: 0, pre_only_buckets: 0, post_only_buckets: 0
domain: EveryCensusRow,
pre_occurrences: step0_census_occurrences(rows: pre),
post_occurrences: step0_census_occurrences(rows: post),
shared_increases: 0, shared_decreases: 0,
pre_only_occurrences: 0, post_only_occurrences: 0,
unchanged_buckets: 0, pre_only_buckets: 0, post_only_buckets: 0
}, f: fn(acc, row) { step0_differential_left_step(acc: acc, post_index: post_index, row: row) })
Step0DifferentialComputed {
differential: fold(post, init: left, f: fn(acc, row) { step0_differential_right_step(acc: acc, pre_index: pre_index, row: row) })
let differential = fold(post, init: left, f: fn(acc, row) { step0_differential_right_step(acc: acc, pre_index: pre_index, row: row) })
if step0_differential_conserves(differential: differential) {
Step0DifferentialComputed { differential: differential }
} else {
Step0DifferentialUndefined {
cause: concat(
concat("the bucket movements do not conserve the differenced population (", step0_differential_domain_label(domain: differential.domain) as String),
concat(
concat("): pre_occurrences=", to_string(differential.pre_occurrences)),
concat(" post_occurrences=", to_string(differential.post_occurrences))
)
) as NonEmptyStr
}
}
}
}
}
}

fn step0_differential_is_identity(differential: Step0HistogramDifferential) -> Bool {
differential.gross_increases == 0
&& differential.gross_decreases == 0
step0_differential_gross_increases(differential: differential) == 0
&& step0_differential_gross_decreases(differential: differential) == 0
&& differential.pre_only_buckets == 0
&& differential.post_only_buckets == 0
}
Expand Down Expand Up @@ -722,8 +778,11 @@ fn run_current_step0_candidate() -> Step0CandidateRun {
// make impossible, and "blocking rows" and "blocking occurrences" are different measurements.
fn step0_blocking_line(measure: Step0BlockingMeasure) -> String {
concat(
concat("blocking_rows=", to_string(measure.histogram_rows)),
concat(" blocking_occurrences=", to_string(measure.occurrences))
concat("blocking_domain=", step0_differential_domain_label(domain: BlockingCensusRowsOnly) as String),
concat(
concat(" blocking_rows=", to_string(measure.histogram_rows)),
concat(" blocking_occurrences=", to_string(measure.occurrences))
)
)
}

Expand All @@ -747,14 +806,35 @@ fn step0_differential_line(standing: Step0DifferentialStanding) -> String {
OccurrenceJoinUnavailable { cause: cause } => concat("differential=unavailable cause=", cause as String)
HistogramBucketsChanged { differential: d } =>
concat(
concat("differential=buckets-changed gross_increases=", to_string(d.gross_increases)),
concat("differential=buckets-changed domain=", step0_differential_domain_label(domain: d.domain) as String),
concat(
concat(" gross_decreases=", to_string(d.gross_decreases)),
concat(
concat(" unchanged_buckets=", to_string(d.unchanged_buckets)),
concat(" pre_occurrences=", to_string(d.pre_occurrences)),
concat(" post_occurrences=", to_string(d.post_occurrences))
),
concat(
concat(
concat(" shared_increases=", to_string(d.shared_increases)),
concat(" shared_decreases=", to_string(d.shared_decreases))
),
concat(
concat(" pre_only_buckets=", to_string(d.pre_only_buckets)),
concat(" post_only_buckets=", to_string(d.post_only_buckets))
concat(
concat(" pre_only_occurrences=", to_string(d.pre_only_occurrences)),
concat(" post_only_occurrences=", to_string(d.post_only_occurrences))
),
concat(
concat(
concat(" gross_increases=", to_string(step0_differential_gross_increases(differential: d))),
concat(" gross_decreases=", to_string(step0_differential_gross_decreases(differential: d)))
),
concat(
concat(" unchanged_buckets=", to_string(d.unchanged_buckets)),
concat(
concat(" pre_only_buckets=", to_string(d.pre_only_buckets)),
concat(" post_only_buckets=", to_string(d.post_only_buckets))
)
)
)
)
)
)
Expand Down
Loading
Loading