diff --git a/dag/test/claim/legacy_binding_delta_witness_test.dag b/dag/test/claim/legacy_binding_delta_witness_test.dag new file mode 100644 index 00000000000..de835e056ea --- /dev/null +++ b/dag/test/claim/legacy_binding_delta_witness_test.dag @@ -0,0 +1,527 @@ +module test.claim.legacy_binding_delta_witness + +import std.types { String, Bool, Int, List } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.content_hash { Fnv1a64Structural, structural_content_hash } +import std.decl_ref { DeclarationRef, decl_ref } +import std.occurrence_identity { OccurrenceId } +import std.content_hash { Fnv1a64Structural, structural_content_hash } +import v2.workflow.legacy_binding_observation { + LegacyBindingObservation, + LegacyBindingObservationRow, + LegacyBindingObservationSubject, + SubjectOccurrenceRef, + ImportScopedPolicy, + NamespaceOnlyPolicy, + CompleteLegacyObservation, + LegacyObservationAdmission, + ObservationAdmitted, + ObservationRefused, + LegacyObservationCompleteness, + LegacyObservationMissingExpected, + LegacyObservationForeignObserved, + LegacyObservationRepeatedObserved, + admit_complete_observation, + legacy_subject_identity +} +import v2.workflow.legacy_binding_delta { + ProjectionProvenance, + ProjectionProvenanceEntry, + ProjectedFromSource, + ProjectedAsInsertion, + ProvenanceTotality, + ProvenanceTotal, + ProvenanceSourceMissing, + ProvenanceSourceRepeated, + ProvenanceTargetMissing, + ProvenanceForeignOccurrence, + ProvenanceTargetRepeated, + ProvenanceRefOutOfSubjectScope, + LegacyBindingDelta, + DeltaProvenanceRefused, + CorrespondenceAdmitted, + provenance_totality, + legacy_binding_delta +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE DELTA HAS NO KEY, SO EVERY ONE OF ITS LAWS IS ABOUT THE PROVENANCE THE PROJECTOR EMITTED. +// +// There is no admissible cross-compile occurrence key: OccurrenceId is a traversal ordinal, and the +// projection's inserted qualifier tokens are exactly what shifts it. So the correspondence arrives +// as the projector's output and this file's whole subject is whether that output ACCOUNTS FOR BOTH +// DENOMINATORS. The outcome type parameters are instantiated with a one-arm test vocabulary +// because the delta's laws never read an outcome -- which is itself the claim that the envelope +// and the producer are separable. +// +// THE FIXTURES ARE ALL SIZE-PRESERVING WHERE THEY CAN BE. Each refusal fixture carries a +// provenance whose entry count is the same as the passing one's wherever the law permits, so no arm +// is reachable by comparing sizes. That is the operator's oracle rule applied to the fixtures +// rather than only to the laws they exercise. +type LbdTestOutcome + = LbdObserved + | LbdUnobserved + +fn lbd_subject() -> LegacyBindingObservationSubject { + LegacyBindingObservationSubject { + semantic_source_digest: structural_content_hash(digest: "1111111111111111"), + source_set_digest: structural_content_hash(digest: "2222222222222222"), + compiler_artifact_digest: structural_content_hash(digest: "3333333333333333"), + resolver_identity: decl_ref(module_path: "v1.compiler.infer_env", decl_name: "lookup_binding_by_name"), + resolver_policy: ImportScopedPolicy, + occurrence_transport_digest: structural_content_hash(digest: "4444444444444444"), + declaration_index_digest: structural_content_hash(digest: "5555555555555555") + } +} + +fn lbd_projected_subject() -> LegacyBindingObservationSubject { + LegacyBindingObservationSubject { + semantic_source_digest: structural_content_hash(digest: "9999999999999999"), + source_set_digest: structural_content_hash(digest: "2222222222222222"), + compiler_artifact_digest: structural_content_hash(digest: "3333333333333333"), + resolver_identity: decl_ref(module_path: "v1.compiler.infer_env", decl_name: "lookup_binding_by_name"), + resolver_policy: NamespaceOnlyPolicy, + occurrence_transport_digest: structural_content_hash(digest: "4444444444444444"), + declaration_index_digest: structural_content_hash(digest: "5555555555555555") + } +} + +fn lbd_observation_of(subject: LegacyBindingObservationSubject, ids: List) -> LegacyBindingObservation { + LegacyBindingObservation { + subject: subject, + rows: ids |> map(id => LegacyBindingObservationRow { + occurrence: OccurrenceId { value: id }, + outcome: LbdObserved + }) + } +} + +fn lbd_base_ref(id: Int) -> SubjectOccurrenceRef { + SubjectOccurrenceRef { + subject_identity: legacy_subject_identity(subject: lbd_subject()), + occurrence: OccurrenceId { value: id } + } +} + +fn lbd_projected_ref(id: Int) -> SubjectOccurrenceRef { + SubjectOccurrenceRef { + subject_identity: legacy_subject_identity(subject: lbd_projected_subject()), + occurrence: OccurrenceId { value: id } + } +} + +fn lbd_pair(source: Int, target: Int) -> ProjectionProvenanceEntry { + ProjectedFromSource { source: lbd_base_ref(id: source), target: lbd_projected_ref(id: target) } +} + +fn lbd_insertion(target: Int, caused_by: Int) -> ProjectionProvenanceEntry { + ProjectedAsInsertion { target: lbd_projected_ref(id: target), caused_by: lbd_base_ref(id: caused_by) } +} + +// THE FIXTURE CANNOT FABRICATE AN ADMITTED OBSERVATION, AND THAT IS THE WALL WORKING RATHER THAN +// AN INCONVENIENCE. CompleteLegacyObservation is sole_constructor, so this file has no way to hand +// the delta a carrier whose completeness was never established -- an earlier revision of the helper +// below simply built the observation and passed it, which is precisely the hole review 56328 found. +// The consequence is that every arm must now carry an admission-refused branch, and that branch is +// not decoration: rendering an admission refusal as a totality verdict would be the unmade +// comparison reading as a made one, one level above where the delta's own vocabulary prevents it. +type LbdTotalityOutcome + = TotalityComputed { totality: ProvenanceTotality } + | AdmissionRefusedBeforeTotality { completeness: LegacyObservationCompleteness } + +fn lbd_admit(subject: LegacyBindingObservationSubject, ids: List, expected: List) -> LegacyObservationAdmission { + admit_complete_observation( + observation: lbd_observation_of(subject: subject, ids: ids), + expected: expected + ) +} + +fn lbd_totality_expecting( + base: List, + projected: List, + base_expected: List, + projected_expected: List, + entries: List +) -> LbdTotalityOutcome { + match lbd_admit(subject: lbd_subject(), ids: base, expected: base_expected) { + ObservationRefused { completeness: c } => AdmissionRefusedBeforeTotality { completeness: c } + ObservationAdmitted { admitted: b } => match lbd_admit(subject: lbd_projected_subject(), ids: projected, expected: projected_expected) { + ObservationRefused { completeness: c } => AdmissionRefusedBeforeTotality { completeness: c } + ObservationAdmitted { admitted: pr } => TotalityComputed { + totality: provenance_totality( + base_admitted: b, + projected_admitted: pr, + provenance: ProjectionProvenance { entries: entries } + ) + } + } + } +} + +// EVERY LAW FIXTURE BELOW OBSERVES ITS OWN WHOLE EXPECTED POPULATION, so admission always succeeds +// and each arm exercises the totality law it names rather than the admission boundary. The two arms +// that exercise the boundary itself pass a DIFFERENT expected population deliberately. +fn lbd_delta(base: List, projected: List, entries: List) -> LbdDeltaOutcome { + match lbd_admit(subject: lbd_subject(), ids: base, expected: base) { + ObservationRefused { completeness: c } => DeltaAdmissionRefused { completeness: c } + ObservationAdmitted { admitted: b } => match lbd_admit(subject: lbd_projected_subject(), ids: projected, expected: projected) { + ObservationRefused { completeness: c } => DeltaAdmissionRefused { completeness: c } + ObservationAdmitted { admitted: pr } => DeltaComputedOutcome { + delta: legacy_binding_delta( + base_admitted: b, + projected_admitted: pr, + provenance: ProjectionProvenance { entries: entries } + ) + } + } + } +} + +type LbdDeltaOutcome + = DeltaComputedOutcome { delta: LegacyBindingDelta } + | DeltaAdmissionRefused { completeness: LegacyObservationCompleteness } + +fn lbd_totality(base: List, projected: List, entries: List) -> LbdTotalityOutcome { + lbd_totality_expecting( + base: base, + projected: projected, + base_expected: base, + projected_expected: projected, + entries: entries + ) +} + +// THE PASSING SHAPE, AND IT IS THE ONE THE REAL PROJECTION PRODUCES: the base's three occurrences +// map to three targets whose ordinals have ALL SHIFTED, plus one inserted target with no source. +// The shifted ordinals are the point -- if any law here accidentally compared ids across the two +// sides rather than reading the provenance, this arm would refuse. +test fn a_provenance_accounting_for_both_denominators_is_total() -> Bool { + match lbd_totality( + base: [10, 20, 30], + projected: [11, 21, 31, 41], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21), lbd_pair(source: 30, target: 31), lbd_insertion(target: 41, caused_by: 10)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceTotal => true + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// AN INSERTION IS NOT A MISSING SOURCE, and this arm is why the two are separate constructors. A +// schema that required every target to carry a source would refuse the projection for doing the one +// thing it exists to do. +test fn a_projection_with_no_insertions_is_also_total() -> Bool { + match lbd_totality( + base: [10, 20], + projected: [11, 21], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceTotal => true + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// A DROPPED BASE OCCURRENCE IS A SITE THE MIGRATION SILENTLY DECLINED TO CONSIDER. The entry count +// is unchanged -- an insertion stands where the third pair was -- so this arm is not reachable by +// counting. +test fn a_base_occurrence_with_no_provenance_source_refuses() -> Bool { + match lbd_totality( + base: [10, 20, 30], + projected: [11, 21, 41], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21), lbd_insertion(target: 41, caused_by: 10)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceSourceMissing { occurrences: missing } => (missing |> count) == 1 + ProvenanceTotal => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// ONE BASE OCCURRENCE PROJECTED TO TWO TARGETS IS A FORK THE DELTA CANNOT INTERPRET, and it is a +// distinct failure from a drop: here nothing is missing and the totals are complete in both +// directions. Only multiplicity distinguishes it, which is why the law reads multiplicity rather +// than membership. +test fn a_base_occurrence_projected_twice_refuses() -> Bool { + match lbd_totality( + base: [10, 20], + projected: [11, 21], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 10, target: 21), lbd_pair(source: 20, target: 11)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceSourceRepeated { occurrences: repeated } => (repeated |> count) == 1 + ProvenanceTotal => false + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// A TARGET THE PROVENANCE WILL NOT ACCOUNT FOR is the projection producing something it declines to +// explain -- neither derived nor declared as inserted. +test fn a_projected_occurrence_with_no_provenance_entry_refuses() -> Bool { + match lbd_totality( + base: [10, 20], + projected: [11, 21, 31], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceTargetMissing { occurrences: missing } => (missing |> count) == 1 + ProvenanceTotal => false + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// THE ARM THAT READS AS SUCCESS IF IT IS NOT CHECKED: a provenance about some other pair of +// compiles. Every base occurrence is carried, every target is accounted for exactly once, nothing is +// out of scope -- and one entry names an occurrence neither observation contains. This is the +// count-equality trap in its own habitat, and it is why the foreign check exists on both sides. +// +// THE FOREIGN REF IS A CAUSE RATHER THAN A CARRIED SOURCE, and the reason is worth recording: the +// first version of this fixture added a third PAIR claiming an already-claimed target, so once the +// target-multiplicity law landed it refused as ProvenanceTargetRepeated instead -- a fixture whose +// intended arm was shadowed by a stronger law firing first. The laws are ordered, so a fixture must +// violate exactly one of them or it is testing the ordering rather than the law it names. +test fn a_provenance_naming_an_occurrence_outside_either_denominator_refuses() -> Bool { + match lbd_totality( + base: [10, 20], + projected: [11, 21, 31], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21), lbd_insertion(target: 31, caused_by: 99)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceForeignOccurrence { occurrences: foreign } => (foreign |> count) == 1 + ProvenanceTotal => false + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// THE DELTA REFUSES BEFORE IT COMPARES, and the two verdicts must not render alike: a comparison +// that could not be made is not a comparison that agreed. +test fn the_delta_refuses_rather_than_comparing_over_an_incomplete_provenance() -> Bool { + match lbd_delta( + base: [10, 20, 30], + projected: [11, 21], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21)] + ) { + DeltaAdmissionRefused { completeness: _ } => false + DeltaComputedOutcome { delta: d } => match d { + DeltaProvenanceRefused { totality: _ } => true + CorrespondenceAdmitted { pairs: _ } => false + } + } +} + +test fn the_delta_computes_over_a_total_provenance() -> Bool { + match lbd_delta( + base: [10, 20], + projected: [11, 21, 41], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21), lbd_insertion(target: 41, caused_by: 10)] + ) { + DeltaAdmissionRefused { completeness: _ } => false + DeltaComputedOutcome { delta: d } => match d { + CorrespondenceAdmitted { pairs: pairs } => (pairs |> count) == 3 + DeltaProvenanceRefused { totality: _ } => false + } + } +} + +// THE SCOPE LAW, WHICH IS WHAT MAKES THE RELATION INDEXABLE RATHER THAN MERELY LISTED. +// +// The two subjects here differ (different semantic-source digest, different resolution policy), so +// their content addresses differ, and a ref minted in one allocator domain cannot be silently +// looked up in the other. This fixture hands the base side a ref carrying the PROJECTED subject's +// address at an ordinal the base observation genuinely contains -- so every other law is satisfied +// and only the scope check separates it. Without that check the accidental equality of two +// independently-allocated ordinals is indistinguishable from a real correspondence, which is the +// shared-allocator trap arriving through the index instead of through the key. +test fn a_ref_bearing_the_wrong_subject_address_refuses() -> Bool { + match lbd_totality( + base: [10, 20], + projected: [11, 21], + entries: [ + ProjectedFromSource { source: lbd_projected_ref(id: 10), target: lbd_projected_ref(id: 11) }, + lbd_pair(source: 20, target: 21) + ] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceRefOutOfSubjectScope { occurrences: out } => (out |> count) == 1 + ProvenanceTotal => false + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + } + } +} + +// QUALIFYING A REFERENCE IS NOT A FORK. An insertion names the reference it acts for, and that +// cause is a base-side ref -- so a law that counted every base-side ref toward the +// one-source-per-occurrence rule would report a fork every time the projector did its job. This +// arm holds an occurrence that is both carried forward AND named as the cause of an insertion, and +// requires that it pass. +test fn a_reference_that_is_carried_forward_and_also_causes_an_insertion_is_not_a_fork() -> Bool { + match lbd_totality( + base: [10, 20], + projected: [11, 21, 41], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21), lbd_insertion(target: 41, caused_by: 10)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceTotal => true + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// A CAUSE IS NOT COVERAGE, AND NO EXISTING ARM COULD SEE IT. +// +// Every insertion in the arms above names a cause that is ALSO carried forward, so none of them +// separates the two populations. This one drops occurrence 30 entirely and has the insertion name +// 30 as its cause: under a source law reading every base-side ref, 30 is present, nothing else +// fires, and a DROPPED OCCURRENCE READS AS A COMPLETE CORRESPONDENCE -- the exact lie the +// source-missing law exists to catch, defeated by the arm added to carry more information. +// +// A caused_by is evidence that an insertion acts ON BEHALF OF a reference. It is not evidence that +// the reference survived. It still counts for SCOPE, because a cause is a base-side ref and must +// have been minted in the base's allocator domain -- which is why this fixture reaches the source +// law at all rather than being refused earlier. +test fn an_insertion_naming_a_dropped_occurrence_does_not_cover_it() -> Bool { + match lbd_totality( + base: [10, 20, 30], + projected: [11, 21, 41], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 21), lbd_insertion(target: 41, caused_by: 30)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceSourceMissing { occurrences: missing } => (missing |> count) == 1 + ProvenanceTotal => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// TWO SOURCES CLAIMING ONE TARGET IS AMBIGUOUS PROVENANCE, and membership alone admits it: every +// source occurs exactly once, every target appears, nothing is foreign, nothing is out of scope. +// Only target multiplicity separates it -- the mirror of the fork law, and it was missing while its +// twin was present, which is why the pair is stated as one law per direction per property rather +// than as "totality". +test fn two_sources_claiming_one_target_refuses() -> Bool { + match lbd_totality( + base: [10, 20], + projected: [11, 21], + entries: [lbd_pair(source: 10, target: 11), lbd_pair(source: 20, target: 11), lbd_insertion(target: 21, caused_by: 10)] + ) { + AdmissionRefusedBeforeTotality { completeness: _ } => false + TotalityComputed { totality: t } => match t { + ProvenanceTargetRepeated { occurrences: repeated } => (repeated |> count) == 1 + ProvenanceTotal => false + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + } +} + +// THE SPECIMEN REVIEW 56328 NAMED, AND IT IS THE ONE ARM WHOSE RED WAS REACHABLE BEFORE THE FIX. +// +// Two observations carrying NO rows, against provenance carrying no entries, satisfy every totality +// law below vacuously: there is no source to be missing, no target to be repeated, nothing out of +// scope. Under the old signature that returned an admitted correspondence -- a verdict about a +// population the function never examined. What makes it a defect rather than a degenerate case is +// the EXPECTED populations: both subjects' transports name three references each, so "no rows" is +// not an empty world, it is an observation that answered for none of it. The admission boundary +// refuses here, and it refuses BEFORE any law runs, which is why the outcome is the admission arm +// and not a totality arm. +test fn two_row_less_observations_over_nonempty_expected_populations_refuse_before_any_law_runs() -> Bool { + match lbd_totality_expecting( + base: [], + projected: [], + base_expected: [10, 20, 30], + projected_expected: [11, 21, 31], + entries: [] + ) { + AdmissionRefusedBeforeTotality { completeness: c } => match c { + LegacyObservationMissingExpected { occurrences: missing } => (missing |> count) == 3 + LegacyObservationForeignObserved { occurrences: _ } => false + LegacyObservationRepeatedObserved { occurrences: _ } => false + LegacyObservationComplete => false + } + TotalityComputed { totality: _ } => false + } +} + +// AND THE CONTROL, WITHOUT WHICH THE ARM ABOVE IS SATISFIED BY REFUSING EMPTINESS AS SUCH. An +// observation of a genuinely empty expected population is COMPLETE -- it answered for all zero of +// it -- so the correspondence is admitted and the delta is vacuous in the honest sense. The +// distinction the pair establishes is that the boundary reads the expected population, never the +// row count: same zero rows, opposite verdicts, and the only thing that moved is what was expected. +test fn a_row_less_observation_over_a_genuinely_empty_expected_population_is_admitted() -> Bool { + match lbd_totality_expecting( + base: [], + projected: [], + base_expected: [], + projected_expected: [], + entries: [] + ) { + TotalityComputed { totality: t } => match t { + ProvenanceTotal => true + ProvenanceSourceMissing { occurrences: _ } => false + ProvenanceSourceRepeated { occurrences: _ } => false + ProvenanceTargetMissing { occurrences: _ } => false + ProvenanceForeignOccurrence { occurrences: _ } => false + ProvenanceTargetRepeated { occurrences: _ } => false + ProvenanceRefOutOfSubjectScope { occurrences: _ } => false + } + AdmissionRefusedBeforeTotality { completeness: _ } => false + } +} diff --git a/dag/test/claim/legacy_binding_observation_witness_test.dag b/dag/test/claim/legacy_binding_observation_witness_test.dag new file mode 100644 index 00000000000..f21365bd065 --- /dev/null +++ b/dag/test/claim/legacy_binding_observation_witness_test.dag @@ -0,0 +1,488 @@ +module test.claim.legacy_binding_observation_witness + +import std.types { String, Bool, Int, List, NonEmptyStr } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.content_hash { Fnv1a64Structural, structural_content_hash } +import std.decl_ref { DeclarationRef, WholeDeclaration, NamedField, decl_ref, decl_field_ref } +import std.occurrence_identity { OccurrenceId } +import v2.workflow.legacy_binding_observation { + LegacyResolutionPolicy, + LegacyBindingObservation, + LegacyBindingObservationRow, + LegacyBindingObservationSubject, + LegacyResolutionPolicy, + ImportScopedPolicy, + NamespaceOnlyPolicy, + LegacyObservationCompleteness, + LegacyObservationComplete, + LegacyObservationMissingExpected, + LegacyObservationForeignObserved, + LegacyObservationRepeatedObserved, + LegacySubjectApplicability, + LegacySubjectApplicable, + LegacySubjectDiverged, + legacy_subject_applicability, + legacy_observation_completeness, + legacy_subject_identity, + decl_field_label +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE APPLICABILITY WALL, EXERCISED FIELD BY FIELD. +// +// An observation is evidence about the base it was taken on. The wall that says so is only a wall +// if EVERY identity field can move it -- a subject comparison that checked six of eight fields +// would answer "applicable" across a base that differs in the seventh, and the whole point of a +// content-addressed subject is that no such gap exists. +// +// SO THE EXERCISES ARE PER FIELD, NOT ONE REPRESENTATIVE. A single "some field differs" arm is +// satisfiable by a comparison that only reads that one field, which is exactly the failure being +// guarded against; eight arms, each moving one field and holding the rest fixed, cannot be +// satisfied by anything less than a total comparison. The RED is reachable for every one of them: +// deleting any branch from legacy_subject_applicability turns its arm green-to-applicable, which +// is the wrong answer rather than a missing one. +// +// THESE ARE SUBSTRATE INPUTS ONLY, and that is the honest declaration rather than a convenience. +// Every subject here is hand-constructed and the function under test is a pure fold over it. +// Nothing calls a producer, because there is no producer yet: the tap that observes X's decisions +// is a separate authority under a separate owner, and standing a stub in for it here would be a +// second, lying authority for the one fact this module deliberately does not own. +fn lbo_digest(label: String) -> Fnv1a64Structural { + structural_content_hash(digest: label) +} + +// THE FIXTURE'S RESOLVER REFERENCE NAMES A RECORD TYPE RATHER THAN THE RESOLVER FUNCTION, and that +// is a deliberate choice about the arms below rather than a claim about what X actually is. Every +// divergence arm must perturb EXACTLY ONE axis of the compared identity, and the reason is stronger +// than picking the wrong population: a two-axis perturbation cannot discriminate WHICH axis the +// comparison reads, so its green is the same green whether the second axis is folded into the +// identity or not. It is permanently green by construction -- the decoration DESIGN section 4b calls +// worse than absent, reached from the multiplicity direction rather than the unauthorable-RED one. +// The general rule, which outlives this fixture: ANY divergence arm perturbing more than one axis of +// a compared identity is uninformative by construction. +// +// So a single-axis module move needs one declared name living in two modules, and a single-axis +// field move needs one of those declarations to carry a field. `OccurrenceId` satisfies both: +// `std.occurrence_identity` and `std.observation` each declare it and the former carries `value`. +// NO UNIQUENESS IS CLAIMED FOR IT, and an earlier revision of this annotation claimed exactly that +// -- "the only pair in the corpus" -- which was false when written: a census over `dag`, `src/v1` +// and `src/v2` at `90bfcfad293` found 47 names declared in two or more modules with at least one +// declaration carrying a field. The first measurement that produced the claim searched two roots +// and compared only adjacent rows of a sort, so it was a property of the search, not of the corpus. +// 47 against 1 is not a near miss, it is the signature of a census whose denominator was its own +// search, and the adjacent-rows filter names the mechanism: it can only ever surface PAIRS, never a +// name declared three or more times, so it was blind by construction to the widest members of the +// very population it was counting. A claim false at authorship is also worse than one that rotted, +// because a rotted claim has a moment in the tree that justified it and a re-measurement disagrees +// cleanly; this one has no such moment anywhere, so re-measuring it looks like a regression someone +// introduced and the next reader spends their time hunting for the change that broke it. +// The claim is not repaired by bounding it to a SHA, because the fixture never needed it: what the +// arms need is that THIS pair holds, and that is self-checking rather than censused -- the citation +// wall refuses this module if either declaration or the field stops existing, so the arms cannot go +// quietly green over a reference that has rotted. A second qualifying pair appearing changes +// nothing here. +// +// The resolver identity the production subject carries is a decision surface such as +// `v1.compiler.infer_env` `lookup_binding_by_name`; nothing in the envelope depends on which. +fn lbo_resolver() -> DeclarationRef { + decl_ref(module_path: "std.occurrence_identity", decl_name: "OccurrenceId") +} + +fn lbo_base_subject() -> LegacyBindingObservationSubject { + LegacyBindingObservationSubject { + semantic_source_digest: lbo_digest(label: "1111111111111111"), + source_set_digest: lbo_digest(label: "2222222222222222"), + compiler_artifact_digest: lbo_digest(label: "3333333333333333"), + resolver_identity: lbo_resolver(), + resolver_policy: ImportScopedPolicy, + occurrence_transport_digest: lbo_digest(label: "4444444444444444"), + declaration_index_digest: lbo_digest(label: "5555555555555555") + } +} + +fn lbo_diverged_field(other: LegacyBindingObservationSubject) -> String { + match legacy_subject_applicability(left: lbo_base_subject(), right: other) { + LegacySubjectDiverged { field: f } => f + LegacySubjectApplicable => "" + } +} + +// THE POSITIVE CONTROL, AND IT IS NOT DECORATION. Without it every arm below is satisfied by a +// comparison that refuses unconditionally, which would be a wall that admits nothing -- useless in +// the opposite direction and just as wrong. +test fn an_identical_subject_is_applicable_to_itself() -> Bool { + match legacy_subject_applicability(left: lbo_base_subject(), right: lbo_base_subject()) { + LegacySubjectApplicable => true + LegacySubjectDiverged { field: _ } => false + } +} + +test fn a_moved_semantic_source_digest_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: lbo_digest(label: "aaaaaaaaaaaaaaaa"), + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: base.resolver_identity, + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + }) == "semantic_source_digest" +} + +test fn a_moved_source_set_digest_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: lbo_digest(label: "bbbbbbbbbbbbbbbb"), + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: base.resolver_identity, + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + }) == "source_set_digest" +} + +test fn a_moved_compiler_artifact_digest_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: lbo_digest(label: "cccccccccccccccc"), + resolver_identity: base.resolver_identity, + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + }) == "compiler_artifact_digest" +} + +// THE RESOLVER IDENTITY IS THE FIELD MOST LIKELY TO BE THOUGHT REDUNDANT WITH THE ARTIFACT DIGEST, +// and it is not: one binary contains several decision surfaces, so an observation of one of them is +// not evidence about another even though both were compiled from the same bytes. All three axes of +// the reference move it, which is why there are three arms. +test fn a_moved_resolver_module_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: decl_ref(module_path: "std.observation", decl_name: "OccurrenceId"), + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + }) == "resolver_identity.module_path" +} + +test fn a_moved_resolver_declaration_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: decl_ref(module_path: "std.occurrence_identity", decl_name: "OccurrenceIdAllocator"), + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + }) == "resolver_identity.decl_name" +} + +// THE POLICY ARM IS THE ONE THIS ENVELOPE CANNOT DERIVE, which is exactly why it must be able to +// refuse over it: the gate is a host thread-local no substrate program can read, so the producer +// states it and this comparison is the only thing standing between an ImportScoped observation and +// a NamespaceOnly one being treated as the same evidence. Same bytes, same sources, same resolver, +// different answers. +test fn a_moved_resolution_policy_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: base.resolver_identity, + resolver_policy: NamespaceOnlyPolicy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + }) == "resolver_policy" +} + +test fn a_moved_occurrence_transport_digest_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: base.resolver_identity, + resolver_policy: base.resolver_policy, + occurrence_transport_digest: lbo_digest(label: "dddddddddddddddd"), + declaration_index_digest: base.declaration_index_digest + }) == "occurrence_transport_digest" +} + +test fn a_moved_declaration_index_digest_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: base.resolver_identity, + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: lbo_digest(label: "eeeeeeeeeeeeeeee") + }) == "declaration_index_digest" +} + +// COMPLETENESS, EXERCISED IN BOTH DIRECTIONS BECAUSE ONE DIRECTION IS NOT A LAW. +// +// The outcome vocabulary here is a two-arm test type, not X's. That is the type parameter earning +// its keep: the join is about WHICH occurrences were answered for, never about what the answer +// said, so it can be proven without the producer existing and without a stub pretending to be one. +// +// WHY BOTH ARMS ARE NECESSARY. A join that only checked for missing rows passes an observation +// that answers for occurrences belonging to some other subject -- right count, wrong identities, +// and it reads as success. A join that only checked for foreign rows passes an observation that +// silently drops the occurrences the producer found inconvenient, which is the failure the whole +// denominator discipline exists to prevent. Each arm below goes green only if its own direction is +// checked, and neither is reachable by a comparison of counts: the missing and foreign fixtures +// both carry exactly as many rows as the expected list has entries. +type LboTestOutcome + = LboTestAnswered + | LboTestRefused + +fn lbo_row(id: Int) -> LegacyBindingObservationRow { + LegacyBindingObservationRow { occurrence: OccurrenceId { value: id }, outcome: LboTestRefused } +} + +fn lbo_observation(ids: List) -> LegacyBindingObservation { + LegacyBindingObservation { subject: lbo_base_subject(), rows: ids |> map(id => lbo_row(id: id)) } +} + +fn lbo_expected() -> List { + [11, 22, 33] +} + +test fn an_observation_answering_exactly_the_expected_occurrences_is_complete() -> Bool { + match legacy_observation_completeness(observation: lbo_observation(ids: [11, 22, 33]), expected: lbo_expected()) { + LegacyObservationComplete => true + LegacyObservationMissingExpected { occurrences: _ } => false + LegacyObservationForeignObserved { occurrences: _ } => false + LegacyObservationRepeatedObserved { occurrences: _ } => false + } +} + +// THE ROW COUNT IS THREE ON BOTH SIDES AND THE JOIN STILL REFUSES. That is the whole difference +// between an identity join and a count equality, stated as a fixture rather than as a claim. +test fn an_observation_missing_one_expected_occurrence_refuses() -> Bool { + match legacy_observation_completeness(observation: lbo_observation(ids: [11, 22, 99]), expected: lbo_expected()) { + LegacyObservationMissingExpected { occurrences: missing } => (missing |> count) == 1 + LegacyObservationComplete => false + LegacyObservationForeignObserved { occurrences: _ } => false + LegacyObservationRepeatedObserved { occurrences: _ } => false + } +} + +test fn an_observation_answering_for_a_non_subject_occurrence_refuses() -> Bool { + match legacy_observation_completeness(observation: lbo_observation(ids: [11, 22, 33, 44]), expected: lbo_expected()) { + LegacyObservationForeignObserved { occurrences: foreign } => (foreign |> count) == 1 + LegacyObservationComplete => false + LegacyObservationMissingExpected { occurrences: _ } => false + LegacyObservationRepeatedObserved { occurrences: _ } => false + } +} + +// A WHOLLY-REFUSED OBSERVATION IS COMPLETE, AND THIS ARM IS WHY THAT IS NOT A CRISIS. +// +// Both sides of the completeness law come from the DENOMINATOR -- the expected list and the row +// keys -- and neither comes from the producer. So an observation whose every row is a production +// refusal is complete, applicable and true, which is exactly what a correct O_X(B) contains on +// today's legacy resolver: measured, X carries zero exact declaration identities to its decision, +// so every row is absent-at-decision. The next reader of an all-refused artifact will assume it is +// broken; this arm is the standing answer that it is not. +test fn an_observation_whose_every_row_is_refused_is_still_complete() -> Bool { + match legacy_observation_completeness(observation: lbo_observation(ids: [11, 22, 33]), expected: lbo_expected()) { + LegacyObservationComplete => true + LegacyObservationMissingExpected { occurrences: _ } => false + LegacyObservationForeignObserved { occurrences: _ } => false + LegacyObservationRepeatedObserved { occurrences: _ } => false + } +} + +// ONE OCCURRENCE, ONE OUTCOME -- AND MEMBERSHIP ALONE DOES NOT SAY SO. +// +// This fixture has every expected occurrence present and no foreign one, so a two-direction +// membership check calls it complete while the artifact carries two outcomes for occurrence 11. +// That is the grain confusion the row type warns about arriving through the completeness law: an +// unreconciled producer hands over attempt-grain rows and, without this arm, they pass. Found by +// review 56288 on the first cut of this module. +test fn an_observation_answering_twice_for_one_occurrence_refuses() -> Bool { + match legacy_observation_completeness(observation: lbo_observation(ids: [11, 11, 22, 33]), expected: lbo_expected()) { + LegacyObservationRepeatedObserved { occurrences: repeated } => (repeated |> count) == 1 + LegacyObservationComplete => false + LegacyObservationMissingExpected { occurrences: _ } => false + LegacyObservationForeignObserved { occurrences: _ } => false + } +} + +// THE FIELD HALF OF THE RESOLVER REFERENCE MOVES THE COMPARISON, and it must also move the content +// address -- review 56288 and review 56285 both found the asymmetry, from opposite ends. The arm +// below is the comparison half; legacy_subject_identity now folds the field, so the two cannot +// disagree about whether these are the same base. +test fn a_moved_resolver_field_refuses() -> Bool { + let base = lbo_base_subject() + lbo_diverged_field(other: LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: decl_field_ref(module_path: "std.occurrence_identity", decl_name: "OccurrenceId", field_name: "value"), + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + }) == "resolver_identity.field" +} + +// AND THE ADDRESS MOVES WITH IT. This is the arm that would have caught the original defect: two +// subjects differing only in the resolver reference's field are refused by the comparison AND carry +// different content addresses. Either alone is satisfiable by the asymmetry the reviews found. +test fn a_moved_resolver_field_also_moves_the_content_address() -> Bool { + let base = lbo_base_subject() + let other = LegacyBindingObservationSubject { + semantic_source_digest: base.semantic_source_digest, + source_set_digest: base.source_set_digest, + compiler_artifact_digest: base.compiler_artifact_digest, + resolver_identity: decl_field_ref(module_path: "std.occurrence_identity", decl_name: "OccurrenceId", field_name: "value"), + resolver_policy: base.resolver_policy, + occurrence_transport_digest: base.occurrence_transport_digest, + declaration_index_digest: base.declaration_index_digest + } + legacy_subject_identity(subject: base).digest != legacy_subject_identity(subject: other).digest +} + +// THE INJECTIVITY WITNESS, PER FIELD OVER ALL NINE INPUTS. +// +// The applicability arms are per-field on the stated grounds that a comparison reading eight of nine +// fields must be impossible to write. That argument applies with equal force to the ADDRESS, and on +// the first cut of this module it was not applied: the fold read seven of the nine inputs, and +// nothing here would have noticed. Two reviews found it from opposite ends within minutes of each +// other -- which is the honest reason these arms exist, and the reason a covered function's sibling +// being uncovered is worth treating as a defect rather than as missing polish. +// +// NINE INPUTS, NOT EIGHT: the resolver reference contributes three (module path, declaration name, +// field), so the identity fold has one more input than the subject has fields. +fn lbo_address_moves(other: LegacyBindingObservationSubject) -> Bool { + legacy_subject_identity(subject: lbo_base_subject()).digest != legacy_subject_identity(subject: other).digest +} + +fn lbo_with_semantic_source(d: Fnv1a64Structural) -> LegacyBindingObservationSubject { + let b = lbo_base_subject() + LegacyBindingObservationSubject { + semantic_source_digest: d, + source_set_digest: b.source_set_digest, + compiler_artifact_digest: b.compiler_artifact_digest, + resolver_identity: b.resolver_identity, + resolver_policy: b.resolver_policy, + occurrence_transport_digest: b.occurrence_transport_digest, + declaration_index_digest: b.declaration_index_digest + } +} + +fn lbo_with_source_set(d: Fnv1a64Structural) -> LegacyBindingObservationSubject { + let b = lbo_base_subject() + LegacyBindingObservationSubject { + semantic_source_digest: b.semantic_source_digest, + source_set_digest: d, + compiler_artifact_digest: b.compiler_artifact_digest, + resolver_identity: b.resolver_identity, + resolver_policy: b.resolver_policy, + occurrence_transport_digest: b.occurrence_transport_digest, + declaration_index_digest: b.declaration_index_digest + } +} + +fn lbo_with_artifact(d: Fnv1a64Structural) -> LegacyBindingObservationSubject { + let b = lbo_base_subject() + LegacyBindingObservationSubject { + semantic_source_digest: b.semantic_source_digest, + source_set_digest: b.source_set_digest, + compiler_artifact_digest: d, + resolver_identity: b.resolver_identity, + resolver_policy: b.resolver_policy, + occurrence_transport_digest: b.occurrence_transport_digest, + declaration_index_digest: b.declaration_index_digest + } +} + +fn lbo_with_transport(d: Fnv1a64Structural) -> LegacyBindingObservationSubject { + let b = lbo_base_subject() + LegacyBindingObservationSubject { + semantic_source_digest: b.semantic_source_digest, + source_set_digest: b.source_set_digest, + compiler_artifact_digest: b.compiler_artifact_digest, + resolver_identity: b.resolver_identity, + resolver_policy: b.resolver_policy, + occurrence_transport_digest: d, + declaration_index_digest: b.declaration_index_digest + } +} + +fn lbo_with_decl_index(d: Fnv1a64Structural) -> LegacyBindingObservationSubject { + let b = lbo_base_subject() + LegacyBindingObservationSubject { + semantic_source_digest: b.semantic_source_digest, + source_set_digest: b.source_set_digest, + compiler_artifact_digest: b.compiler_artifact_digest, + resolver_identity: b.resolver_identity, + resolver_policy: b.resolver_policy, + occurrence_transport_digest: b.occurrence_transport_digest, + declaration_index_digest: d + } +} + +fn lbo_with_resolver(reference: DeclarationRef) -> LegacyBindingObservationSubject { + let b = lbo_base_subject() + LegacyBindingObservationSubject { + semantic_source_digest: b.semantic_source_digest, + source_set_digest: b.source_set_digest, + compiler_artifact_digest: b.compiler_artifact_digest, + resolver_identity: reference, + resolver_policy: b.resolver_policy, + occurrence_transport_digest: b.occurrence_transport_digest, + declaration_index_digest: b.declaration_index_digest + } +} + +fn lbo_with_policy(policy: LegacyResolutionPolicy) -> LegacyBindingObservationSubject { + let b = lbo_base_subject() + LegacyBindingObservationSubject { + semantic_source_digest: b.semantic_source_digest, + source_set_digest: b.source_set_digest, + compiler_artifact_digest: b.compiler_artifact_digest, + resolver_identity: b.resolver_identity, + resolver_policy: policy, + occurrence_transport_digest: b.occurrence_transport_digest, + declaration_index_digest: b.declaration_index_digest + } +} + +test fn the_content_address_is_stable_for_an_unchanged_subject() -> Bool { + legacy_subject_identity(subject: lbo_base_subject()).digest == legacy_subject_identity(subject: lbo_base_subject()).digest +} + +test fn every_identity_input_moves_the_content_address() -> Bool { + lbo_address_moves(other: lbo_with_semantic_source(d: lbo_digest(label: "aaaaaaaaaaaaaaaa"))) + && lbo_address_moves(other: lbo_with_source_set(d: lbo_digest(label: "bbbbbbbbbbbbbbbb"))) + && lbo_address_moves(other: lbo_with_artifact(d: lbo_digest(label: "cccccccccccccccc"))) + && lbo_address_moves(other: lbo_with_transport(d: lbo_digest(label: "dddddddddddddddd"))) + && lbo_address_moves(other: lbo_with_decl_index(d: lbo_digest(label: "eeeeeeeeeeeeeeee"))) + && lbo_address_moves(other: lbo_with_resolver(reference: decl_ref(module_path: "std.observation", decl_name: "OccurrenceId"))) + && lbo_address_moves(other: lbo_with_resolver(reference: decl_ref(module_path: "std.occurrence_identity", decl_name: "OccurrenceIdAllocator"))) + && lbo_address_moves(other: lbo_with_resolver(reference: decl_field_ref(module_path: "std.occurrence_identity", decl_name: "OccurrenceId", field_name: "value"))) + && lbo_address_moves(other: lbo_with_policy(policy: NamespaceOnlyPolicy)) +} + +// THE COLLISION THE OTHER NINE ARMS CANNOT SEE, because it needs two subjects differing only in the +// DeclField ARM with the payload chosen to impersonate the nullary arm's label. Everything else +// about these two subjects is identical, and decl_field_eq reports them different, so an address +// that collided here would be the comparison and the address disagreeing -- the same defect the +// field fold was added to fix, one level down inside the fix. +test fn a_field_name_cannot_impersonate_the_whole_declaration_arm() -> Bool { + decl_field_label(field: WholeDeclaration) != decl_field_label(field: NamedField { field_name: "whole_declaration" as NonEmptyStr }) +} diff --git a/src/v2/workflow/legacy_binding_delta.dag b/src/v2/workflow/legacy_binding_delta.dag new file mode 100644 index 00000000000..b97fa7b6a0d --- /dev/null +++ b/src/v2/workflow/legacy_binding_delta.dag @@ -0,0 +1,254 @@ +module v2.workflow.legacy_binding_delta + +import std.types { String, Bool, Int, List } +import std.content_hash { Fnv1a64Structural } +import std.occurrence_identity { OccurrenceId } +import v2.workflow.legacy_binding_observation { + CompleteLegacyObservation, + LegacyBindingObservationSubject, + SubjectOccurrenceRef, + observed_occurrence_ids, + legacy_subject_identity +} + +// THE CORRESPONDENCE IS THE PROJECTOR'S OUTPUT, NOT A JOIN KEY. THIS MODULE CONSUMES IT AND +// REFUSES TO RECONSTRUCT IT. +// +// The delta between what the legacy resolver X selected over base B and what the strict resolver Y +// selects over the projection P(B) is a comparison BETWEEN TWO COMPILES, and there is no admissible +// key for one. std.occurrence_identity's scope law forbids filename, SourceSpan, authored name, +// structural Node equality, content hash and module-local allocator reset as identity inputs, and +// OccurrenceId is not a stable cross-compile name either -- alloc_occurrence_id is a monotone +// counter consumed in DFS order, so an id ENCODES POSITION IN THE WALK. P(B) differs from B by +// INSERTED QUALIFIER TOKENS, which is precisely the edit that shifts every id allocated after it. +// +// SO THE DICHOTOMY IS CLOSED, NOT MERELY UNSOLVED. Every property computable from a finished tree +// in isolation is positional or content-derived; the law names both classes; and a cross-compile +// key must by definition be computed from each tree separately and then joined. What escapes is +// not a better key -- it is a relation the TRANSFORMATION EMITS, because a function knows which +// output came from which input. That is a fact the projector had in hand, not an inference about +// the trees. +// +// THE TRAP THIS MODULE EXISTS TO NOT FALL INTO, recorded because it is the natural first idea: +// threading one allocator across both parses. It is roughly one line and it is what the scope law +// says a production source graph does. IT ESTABLISHES NOTHING. B's occurrence and its P(B) +// counterpart still get different ordinals; what the shared allocator buys is that they are +// GUARANTEED-DISTINCT rather than ACCIDENTALLY-EQUAL, so a correspondence keyed on it goes from +// noisily wrong to silently and totally wrong. Worse, it makes the ordinal look MORE trustworthy: +// globally unique, totally ordered, reproducible run to run -- everything a reader checks comes +// back clean, and the one property it lacks is the only one anyone wanted. +// +// THE GENERAL TELL, which is the absorbing fallback one level up: IF YOUR JOIN ALWAYS CLOSES, IT +// IS NOT A JOIN. A correspondence that cannot fail has its deficit frequency zeroed by +// construction, so it never ranks for repair, and it gets cited as coverage. + +// AND NOTHING HERE MAY READ AN ORDINAL AS AN ORDER, WHICH IS A SEPARATE PROHIBITION FROM THE ONE +// ABOVE AND ARRIVES FROM THE OTHER END OF THE SAME FACT. +// +// The prohibition above is about comparing ordinals ACROSS compiles. This one is about reading them +// as a SEQUENCE WITHIN one. Once identity is minted at parser construction rather than by a later +// traversal, children are often constructed before their parents, so a parent's ordinal may be +// numerically GREATER than its child's -- and adding an unrelated earlier construction renumbers +// later ids without changing a single binding, closure, diagnostic or emitted byte. +// +// So no law in this module sorts, ranges over, or compares the magnitude of an occurrence ordinal. +// Every one of them is set membership or multiplicity, both of which are order-free by +// construction, and containment is the explicit ancestor relation rather than an inequality between +// ids. Stated here rather than left implicit because the tempting use is exactly the plausible one: +// a projector comparing two projections would naturally want a stable traversal order, and the +// ordinals look like one. + +// A PROJECTION PAIR RELATES ONE TARGET OCCURRENCE TO ITS SOURCE, AND THE ABSENT SOURCE IS A +// FIRST-CLASS ARM RATHER THAN AN EXCEPTION. +// +// A projection that inserts qualifier tokens produces target occurrences with no source. That is +// the projector DOING ITS JOB, not a gap in its provenance, and a schema requiring every target to +// carry a source would refuse P(B) for succeeding -- the not-applicable-rendered-as-malformed +// shape. So insertion is its own constructor, and a reader can tell "this target came from +// nowhere, by design" from "this target's source is missing", which have opposite owners. +// AN INSERTED SEGMENT CARRIES ITS CAUSE RATHER THAN BEING SOURCELESS, and the difference is not +// cosmetic. "No source" and "caused by the reference being qualified" have the same first-class +// status but not the same information: the first leaves a reader concluding that inserted syntax is +// unattributable, and the second names the occurrence on whose behalf the segment exists. A +// projection that inserts a qualifier is acting FOR some reference, and it knows which. +type ProjectionProvenanceEntry + = ProjectedFromSource { source: SubjectOccurrenceRef, target: SubjectOccurrenceRef } + | ProjectedAsInsertion { target: SubjectOccurrenceRef, caused_by: SubjectOccurrenceRef } + +type ProjectionProvenance { + entries: List +} + +fn provenance_source_refs(provenance: ProjectionProvenance) -> List { + provenance.entries |> flat_map(entry => match entry { + ProjectedFromSource { source: s, target: _ } => [s] + ProjectedAsInsertion { target: _, caused_by: c } => [c] + }) +} + +fn provenance_target_refs(provenance: ProjectionProvenance) -> List { + provenance.entries |> map(entry => match entry { + ProjectedFromSource { source: _, target: t } => t + ProjectedAsInsertion { target: t, caused_by: _ } => t + }) +} + +// AN INSERTION'S CAUSE IS A BASE-SIDE REFERENCE AND IS THEREFORE A SOURCE FOR SCOPE PURPOSES, which +// is why provenance_source_refs collects it -- but it is NOT a carried-forward source, so counting +// it toward the one-source-per-base-occurrence law would make qualifying a reference look like a +// fork. The two questions are separated: scope membership reads every base-side ref, multiplicity +// reads only the carried-forward ones. +fn provenance_carried_source_ids(provenance: ProjectionProvenance) -> List { + provenance.entries |> flat_map(entry => match entry { + ProjectedFromSource { source: s, target: _ } => [s.occurrence.value] + ProjectedAsInsertion { target: _, caused_by: _ } => [] + }) +} + +fn refs_in_scope(refs: List, identity: Fnv1a64Structural) -> List { + refs |> filter(r => r.subject_identity.digest == identity.digest) |> map(r => r.occurrence.value) +} + +fn refs_out_of_scope(refs: List, identity: Fnv1a64Structural) -> List { + refs |> filter(r => r.subject_identity.digest != identity.digest) |> map(r => r.occurrence.value) +} + +// PROVENANCE TOTALITY IS SIX LAWS, AND EACH ONE FAILS A DIFFERENT LIE. +// +// EVERY LAW NAMES ITS DENOMINATOR BESIDE IT, AND THAT DISCIPLINE IS THE RESIDUE OF THREE REVIEW +// FINDINGS RATHER THAN A PREFERENCE. Three defects in two modules had one shape: the prose stated +// the law correctly and the filter ran it over the wrong set. Membership checked without +// cardinality (a repeated observed occurrence read as complete); presence checked over a population +// wider than its subject (an insertion's caused_by discharging a dropped occurrence's obligation); +// and totality checked without target cardinality. Each passed every arm that existed. So the laws +// below state WHICH SET and WHICH MULTIPLICITY explicitly: +// +// scope -- every ref, both sides, against its own subject's address +// source missing -- base denominator against CARRIED sources only +// source repeat -- base denominator against CARRIED sources, multiplicity +// target missing -- projected denominator against ALL targets +// target repeat -- projected denominator against ALL targets, multiplicity +// foreign -- in-scope refs, both sides, against their denominators +// +// THE CARRIED-VERSUS-ALL SPLIT IS THE ONE THAT BIT. A caused_by is evidence that an insertion acts +// ON BEHALF OF a reference; it is NOT evidence that the reference survived the projection. Reading +// it as coverage lets a dropped base occurrence read as a complete correspondence, which is the +// exact lie the source-missing law exists to catch. It still counts for SCOPE, because a cause is a +// base-side ref and must have been minted in the base's allocator domain. +// +// A source left out means the projection dropped an occurrence the base carried -- a site the +// migration silently declined to consider. A carried source appearing twice means one base +// occurrence was projected to two targets, which is a fork the delta cannot interpret. A target +// left out means the projection produced something it will not account for. A ref scoped to +// NEITHER subject means the provenance is about some other pair of compiles entirely, and that is +// the failure that reads as success -- exactly the count-equality trap, since such a provenance can +// have the right size. +// +// THE SCOPE LAW IS WHAT MAKES AN INDEXABLE RELATION SOUND. An ordinal names an occurrence only +// inside the allocator that minted it, so a ref carries the subject whose allocator that was, and +// a ref bearing the wrong subject address is refused rather than silently looked up in the wrong +// domain. Without it the accidental equality of two independently-allocated ordinals would be +// indistinguishable from a real correspondence -- the shared-allocator trap arriving through the +// index instead of through the key. +// +// NOTE WHAT IS NOT A LAW: a target that is an insertion is admitted, because insertion is the +// point. The asymmetry between the source and target laws is deliberate and is the one place a +// reader should expect the two directions NOT to mirror each other. +type ProvenanceTotality + = ProvenanceTotal + | ProvenanceSourceMissing { occurrences: List } + | ProvenanceSourceRepeated { occurrences: List } + | ProvenanceTargetMissing { occurrences: List } + | ProvenanceForeignOccurrence { occurrences: List } + | ProvenanceTargetRepeated { occurrences: List } + | ProvenanceRefOutOfSubjectScope { occurrences: List } + +fn occurrence_multiplicity(ids: List, id: Int) -> Int { + ids |> filter(other => other == id) |> count +} + +// THE DENOMINATORS ARE THE OBSERVATIONS' OWN ROW KEYS, AND COMPLETENESS IS CARRIED IN THE +// PARAMETER TYPE RATHER THAN REQUESTED OF THE CALLER. An earlier revision took raw observations +// and stated the ordering obligation in this annotation. Review 56328 was right that the comment +// could not enforce it, and right about the specimen: two row-less observations against row-less +// provenance satisfy every law below VACUOUSLY, so the delta admitted a correspondence over a +// population it never examined -- an unmade comparison rendered as agreement, which is the exact +// failure the verdict vocabulary further down exists to prevent. CompleteLegacyObservation is +// `sole_constructor` and admit_complete_observation is its only mint, so a caller that skipped the +// completeness join now fails to typecheck instead of being asked not to. +// +// Taking the transports again HERE would still be wrong, and that half of the old note survives: +// it would re-derive a fact the admitted carrier already establishes and let two derivations of one +// fact disagree. The repair is to make the established fact reach this function, not to establish +// it twice. +fn provenance_totality( + base_admitted: CompleteLegacyObservation, + projected_admitted: CompleteLegacyObservation

, + provenance: ProjectionProvenance +) -> ProvenanceTotality { + let base_observation = base_admitted.observation + let projected_observation = projected_admitted.observation + let base_identity = legacy_subject_identity(subject: base_observation.subject) + let projected_identity = legacy_subject_identity(subject: projected_observation.subject) + let base_ids = observed_occurrence_ids(observation: base_observation) + let projected_ids = observed_occurrence_ids(observation: projected_observation) + let source_refs = provenance_source_refs(provenance: provenance) + let target_refs = provenance_target_refs(provenance: provenance) + let out_of_scope = concat( + refs_out_of_scope(refs: source_refs, identity: base_identity), + refs_out_of_scope(refs: target_refs, identity: projected_identity) + ) + let sources = refs_in_scope(refs: source_refs, identity: base_identity) + let targets = refs_in_scope(refs: target_refs, identity: projected_identity) + let carried = provenance_carried_source_ids(provenance: provenance) + let source_missing = base_ids |> filter(id => !(carried |> any(s => s == id))) + let source_repeated = base_ids |> filter(id => occurrence_multiplicity(ids: carried, id: id) > 1) + let target_missing = projected_ids |> filter(id => !(targets |> any(t => t == id))) + let target_repeated = projected_ids |> filter(id => occurrence_multiplicity(ids: targets, id: id) > 1) + let foreign_sources = sources |> filter(id => !(base_ids |> any(b => b == id))) + let foreign_targets = targets |> filter(id => !(projected_ids |> any(p => p == id))) + let foreign = concat(foreign_sources, foreign_targets) + if (out_of_scope |> count) > 0 { ProvenanceRefOutOfSubjectScope { occurrences: out_of_scope } } + else if (source_missing |> count) > 0 { ProvenanceSourceMissing { occurrences: source_missing } } + else if (source_repeated |> count) > 0 { ProvenanceSourceRepeated { occurrences: source_repeated } } + else if (target_missing |> count) > 0 { ProvenanceTargetMissing { occurrences: target_missing } } + else if (target_repeated |> count) > 0 { ProvenanceTargetRepeated { occurrences: target_repeated } } + else if (foreign |> count) > 0 { ProvenanceForeignOccurrence { occurrences: foreign } } + else { ProvenanceTotal } +} + +// THE DELTA TAKES THREE INPUTS AND NO KEY, AND REFUSES BEFORE IT COMPARES. +// +// Its verdict vocabulary keeps two failures apart that a single arm would conflate: a provenance +// that does not account for both denominators, and a genuine disagreement between what X selected +// and what Y selects. The first says the comparison could not be made; the second says it was made +// and diverged. Rendering them alike would let an unmade comparison read as agreement, which is +// the execution-provenance failure at this artifact's own surface. +// THE ADMITTING ARM IS NAMED FOR WHAT IT HOLDS, NOT FOR WHAT A READER WILL WANT IT TO HOLD. It was +// DeltaComputed, and it returns its input verbatim -- nothing here compares X's outcomes against +// Y's, and nothing in this slice can. The name promised a comparison the module deliberately does +// not make, which is a name covering a superset of its own population. CorrespondenceAdmitted says +// the correspondence is total and admissible, which is exactly the fact established. +type LegacyBindingDelta + = DeltaProvenanceRefused { totality: ProvenanceTotality } + | CorrespondenceAdmitted { pairs: List } + +fn legacy_binding_delta( + base_admitted: CompleteLegacyObservation, + projected_admitted: CompleteLegacyObservation

, + provenance: ProjectionProvenance +) -> LegacyBindingDelta { + match provenance_totality( + base_admitted: base_admitted, + projected_admitted: projected_admitted, + provenance: provenance + ) { + ProvenanceTotal => CorrespondenceAdmitted { pairs: provenance.entries } + ProvenanceSourceMissing { occurrences: o } => DeltaProvenanceRefused { totality: ProvenanceSourceMissing { occurrences: o } } + ProvenanceSourceRepeated { occurrences: o } => DeltaProvenanceRefused { totality: ProvenanceSourceRepeated { occurrences: o } } + ProvenanceTargetMissing { occurrences: o } => DeltaProvenanceRefused { totality: ProvenanceTargetMissing { occurrences: o } } + ProvenanceForeignOccurrence { occurrences: o } => DeltaProvenanceRefused { totality: ProvenanceForeignOccurrence { occurrences: o } } + ProvenanceTargetRepeated { occurrences: o } => DeltaProvenanceRefused { totality: ProvenanceTargetRepeated { occurrences: o } } + ProvenanceRefOutOfSubjectScope { occurrences: o } => DeltaProvenanceRefused { totality: ProvenanceRefOutOfSubjectScope { occurrences: o } } + } +} diff --git a/src/v2/workflow/legacy_binding_observation.dag b/src/v2/workflow/legacy_binding_observation.dag new file mode 100644 index 00000000000..ad35dd77f0a --- /dev/null +++ b/src/v2/workflow/legacy_binding_observation.dag @@ -0,0 +1,332 @@ +module v2.workflow.legacy_binding_observation + +import std.types { String, Bool, Int, List, Map, NonEmptyStr } +import std.content_hash { Fnv1a64Structural, content_hash_atom, content_hash_combine_structural } +import std.decl_ref { DeclarationRef, DeclField, WholeDeclaration, NamedField, decl_field_eq } +import std.occurrence_identity { + OccurrenceId, + ReferenceOccurrence, + ValidatedOccurrenceTransport +} + +// WHAT THIS OBSERVES, AND WHY IT IS AN OBSERVATION RATHER THAN A RESOLVER. +// +// The legacy resolver X decides, today, what a bare name binds to. A migration that changes how +// names are spelled has to know what X ACTUALLY SELECTED before it changes anything, and it has to +// know it about ONE EXACT BASE -- not about "the tree", which moves under any measurement long +// enough to be useful. O_X(B) is that record: a complete, content-addressed, past-tense statement +// of X's selections over one exact subject B. +// +// THE ENVELOPE IS NOT THE PRODUCER, AND THE SEPARATION IS THE POINT. Everything here is about +// WHICH occurrences must be answered for, WHETHER the answer set is complete, and WHETHER an +// observation may be compared to a later one. NOTHING here decides what X would choose -- that +// judgment arrives through the outcome type parameter, from the tap that sits inside X's own +// decision functions. If this module ever needed to know what X would have selected, it would be +// reconstructing X from the outside, which is authority substitution wearing a completeness claim. + +// WHY THE OUTCOME IS A TYPE PARAMETER RATHER THAN A COPRODUCT DECLARED HERE. +// +// X's decision vocabulary belongs to the tap that observes X, not to the envelope that counts +// rows. Declaring it here would fork it: the tap would either import a vocabulary written by +// someone who cannot see X's decision sites, or mint its own beside it, and DESIGN section 3 says +// what happens next. Parameterising leaves exactly one authority for what X answered and exactly +// one for whether the answering is complete, which are genuinely two facts. +// +// It also means this module is buildable and testable BEFORE the tap exists, without a stub +// standing in for a producer -- a stub would be a second, lying authority for the same fact, and +// the fixtures below instantiate the parameter with an ordinary test vocabulary instead. +// THE ROW GRAIN IS ONE OUTCOME PER REFERENCE OCCURRENCE, AND THE SEAM HAS TO AGREE ON IT. +// +// X is queried more than once per authored reference -- the same occurrence is asked about across +// inference stages, and some of those calls are the compiler's internal questions rather than +// decisions about an authored reference at all. So a producer's natural unit is an ATTEMPT, and +// this envelope's unit is an OCCURRENCE. Those are different denominators. +// +// THE CONSEQUENCE IS NOT ABSTRACT: attempt-grain rows handed to the completeness join fail it, and +// they fail it looking like a defect in the join. Repeated attempts must be reconciled BEFORE they +// reach here -- one outcome per occurrence, emitted only when the attempts agree, and disagreement +// surfaced as a typed conflict rather than as a last-writer-wins pick. That reconciliation is the +// producer's, because only the producer can see the attempts; the refusal to guess is this +// module's, because a row it cannot check is a row it must not accept. +type LegacyBindingObservationRow { + occurrence: OccurrenceId + outcome: O +} + +// THE SUBJECT IS THE WHOLE OF WHAT MAKES TWO OBSERVATIONS COMPARABLE, and every field is here +// because changing it alone changes what X answers. +// +// Semantic source and source set are two facts, not one: the same semantic content can be reached +// through a different source-root set, and the reachable declarations differ even though every +// byte the compiler read is identical. Compiler artifact and resolver identity are likewise two: +// the artifact fixes the whole binary, the resolver identity fixes WHICH decision surface inside +// it was tapped, and an observation of one resolver is not evidence about another. Occurrence +// transport and declaration index are the two populations the answer ranges over -- the questions +// asked and the answers available. +// +// RESOLVER POLICY IS CARRIED, NOT OBSERVED, AND THAT IS DELIBERATE. The policy gate is a host +// thread-local; dag/test/retirement/model.dag records that a substrate program has no handle to +// read or flip it. So this envelope cannot derive the field and must not invent it: it is required +// with no default, and the producer -- which runs where the gate is readable -- states it. A field +// this module could not check is the one field it must refuse to guess. +type LegacyResolutionPolicy + = ImportScopedPolicy + | NamespaceOnlyPolicy + +// WHY NOTHING HERE TYPES THE ANSWER AS A DeclarationRef, stated because it is the schema mistake +// this envelope is one edit away from at all times. +// +// Not every binding X selects is an authored declaration. A LEXICAL BINDER may have no declaration +// reference to project to at all, and kernel and synthetic bindings differ again -- which is the +// same fact that makes occurrence grain mandatory, seen from the answer side rather than the +// question side. An answer schema that stored a DeclarationRef would therefore be wrong for three +// of its four cases, and wrong in the direction that looks complete. +// +// The outcome type parameter is what keeps that decision out of this module: the closed target +// domain belongs beside the producer that can tell the cases apart, and a DeclarationRef is +// DERIVED from the authored case rather than stored beside it, so the two cannot disagree. +type LegacyBindingObservationSubject { + semantic_source_digest: Fnv1a64Structural + source_set_digest: Fnv1a64Structural + compiler_artifact_digest: Fnv1a64Structural + resolver_identity: DeclarationRef + resolver_policy: LegacyResolutionPolicy + occurrence_transport_digest: Fnv1a64Structural + declaration_index_digest: Fnv1a64Structural +} + +type LegacyBindingObservation { + subject: LegacyBindingObservationSubject + rows: List> +} + +// THE DENOMINATOR IS DERIVED FROM THE SUBJECT'S OWN TRANSPORTS AND FROM NOTHING ELSE. +// +// Every reference occurrence the validated transport carries is a question this observation owes +// an answer for. NOT the names a grep finds, NOT the modules in the widest entry, NOT a hand-kept +// roster, and above all NOT the occurrences for which the producer happened to return a convenient +// answer -- that last one is the failure this whole envelope exists to prevent, because an +// observation that defines its denominator as "whatever I could answer" is complete by +// construction and says nothing. +fn expected_reference_occurrence_ids(transport: ValidatedOccurrenceTransport) -> List { + map_keys(transport.references_by_id) +} + +fn observed_occurrence_ids(observation: LegacyBindingObservation) -> List { + observation.rows |> map(row => row.occurrence.value) +} + +// COMPLETENESS IS AN IDENTITY JOIN, NOT A COUNT EQUALITY, and the two refusals below are why. +// +// A count equality passes when an observation answers for N occurrences that are not the subject's +// -- the exact oracle failure DESIGN section 5 forbids, and it fails in the direction that reads +// as success. So the law is stated twice, once in each direction: nothing expected may be missing, +// and nothing observed may be foreign. Either alone is satisfiable by a wrong answer set of the +// right size. +// AND ONE OCCURRENCE MAY BE ANSWERED FOR ONCE, which membership alone does not say. +// +// Rows [11, 11, 22, 33] against expected [11, 22, 33] have every expected occurrence present and no +// foreign one, so a two-direction MEMBERSHIP check calls them complete -- while the artifact carries +// two, possibly conflicting, outcomes for occurrence 11. That is the one-outcome-per-occurrence +// grain this module declares, admitted as a writable state by the very law that was supposed to +// enforce it. It is also precisely the attempt-versus-occurrence grain confusion the row type warns +// about: an unreconciled producer hands over attempt rows, and without this arm they pass. +type LegacyObservationCompleteness + = LegacyObservationComplete + | LegacyObservationMissingExpected { occurrences: List } + | LegacyObservationForeignObserved { occurrences: List } + | LegacyObservationRepeatedObserved { occurrences: List } + +// THE JOIN TAKES THE DERIVED LIST, NOT THE TRANSPORT, AND THE SPLIT IS DELIBERATE. Two facts sit +// here: WHAT the subject's questions are (a derivation, above) and WHETHER an answer set matches +// them exactly (a join). Folding the derivation into the join would leave the join untestable +// except through a hand-built transport -- which is the named-scenario fixture this program +// already refuses -- and would let a change to either half hide behind the other. +fn legacy_observation_completeness( + observation: LegacyBindingObservation, + expected: List +) -> LegacyObservationCompleteness { + let observed = observed_occurrence_ids(observation: observation) + let missing = expected |> filter(id => !(observed |> any(o => o == id))) + let foreign = observed |> filter(id => !(expected |> any(e => e == id))) + let repeated = expected |> filter(id => (observed |> filter(o => o == id) |> count) > 1) + if (missing |> count) > 0 { LegacyObservationMissingExpected { occurrences: missing } } + else if (foreign |> count) > 0 { LegacyObservationForeignObserved { occurrences: foreign } } + else if (repeated |> count) > 0 { LegacyObservationRepeatedObserved { occurrences: repeated } } + else { LegacyObservationComplete } +} + +// THE ADMITTED CARRIER, AND WHY THE PROSE OBLIGATION IT REPLACES WAS NOT ENOUGH. +// +// legacy_observation_completeness ANSWERS a question; nothing downstream could previously be made +// to depend on the answer. The delta consumed raw observations and stated its ordering obligation +// in an annotation -- callers must establish completeness first -- which is validation asked for in +// prose, the weakest form there is: no `Accepted` program can read a comment, so the obligation was +// unenforceable by construction. The failure it admitted is not hypothetical and it is the worst +// available shape: two observations carrying no rows, with provenance carrying no rows, satisfy +// every totality law VACUOUSLY, so the delta returned an admitted correspondence over a population +// it never looked at. An unmade comparison rendered as agreement -- exactly the execution-provenance +// loss the delta's own verdict vocabulary exists to prevent, sitting one level above the vocabulary. +// +// So the fact flows forward in a carrier instead. CompleteLegacyObservation is `sole_constructor`, +// which makes admit_complete_observation the only route to one, and the delta's parameter type is +// then the evidence rather than a request that someone check. The refusal keeps its cause: this is +// a typed admission answering WHY, never an Option that would collapse every completeness arm into +// one absent. +// +// RUNG, HONESTLY. This is `mechanically preventable`, not structural impossibility, and two +// separate facts bound it. `sole_constructor`'s record-literal refusal executes on the v1 seed +// infer path only (v2.compiler.04_infer carries no sole_constructor handling), so the wall is a +// property of the compiling PATH and not of the type. And confinement establishes WHO may +// construct, never WHAT was proven -- here the mint's predicate is fixed and module-owned rather +// than caller-supplied, which is the stronger of the two shapes, but it is still a mint and not an +// unrepresentable state. NEXT-RUNG TRIGGER: v2's own infer path carrying the construction wall. +type CompleteLegacyObservation sole_constructor { + observation: LegacyBindingObservation +} + +type LegacyObservationAdmission + = ObservationAdmitted { admitted: CompleteLegacyObservation } + | ObservationRefused { completeness: LegacyObservationCompleteness } + +fn admit_complete_observation( + observation: LegacyBindingObservation, + expected: List +) -> LegacyObservationAdmission { + match legacy_observation_completeness(observation: observation, expected: expected) { + LegacyObservationComplete => ObservationAdmitted { + admitted: CompleteLegacyObservation { observation: observation } + } + LegacyObservationMissingExpected { occurrences: o } => ObservationRefused { completeness: LegacyObservationMissingExpected { occurrences: o } } + LegacyObservationForeignObserved { occurrences: o } => ObservationRefused { completeness: LegacyObservationForeignObserved { occurrences: o } } + LegacyObservationRepeatedObserved { occurrences: o } => ObservationRefused { completeness: LegacyObservationRepeatedObserved { occurrences: o } } + } +} + +// APPLICABILITY IS A REFUSAL, NOT A COMPARISON RESULT. +// +// An observation is evidence about the base it was taken on and about no other. Comparing two +// observations whose subjects differ in ANY field is not a weaker comparison, it is a category +// error, so it answers with the field that diverged rather than with a verdict. Naming the field +// is what makes the refusal actionable: "these are different bases" sends a reader looking, while +// "the source-set digest differs" tells them what moved. +type LegacySubjectApplicability + = LegacySubjectApplicable + | LegacySubjectDiverged { field: String } + +// THE FIELD ARM CONSUMES std.decl_ref's OWN EQUALITY RATHER THAN A BARE `!=`, and the reason is a +// question a reviewer asked rather than a preference. DeclField's authority module ships +// decl_field_eq; if a bare coproduct `!=` were structurally correct here then that helper would be +// redundant and its own module would have the problem, and if it is not then this arm would have +// been wrong. Either way, two answers to one question existed and only one of them lives beside the +// type. LegacyResolutionPolicy is different and stays a bare comparison: this module declares it, +// so there is no second authority to consume. +fn legacy_subject_applicability( + left: LegacyBindingObservationSubject, + right: LegacyBindingObservationSubject +) -> LegacySubjectApplicability { + if left.semantic_source_digest.digest != right.semantic_source_digest.digest { + LegacySubjectDiverged { field: "semantic_source_digest" } + } else if left.source_set_digest.digest != right.source_set_digest.digest { + LegacySubjectDiverged { field: "source_set_digest" } + } else if left.compiler_artifact_digest.digest != right.compiler_artifact_digest.digest { + LegacySubjectDiverged { field: "compiler_artifact_digest" } + } else if left.resolver_identity.module_path != right.resolver_identity.module_path { + LegacySubjectDiverged { field: "resolver_identity.module_path" } + } else if left.resolver_identity.decl_name != right.resolver_identity.decl_name { + LegacySubjectDiverged { field: "resolver_identity.decl_name" } + } else if !decl_field_eq(a: left.resolver_identity.field, b: right.resolver_identity.field) { + LegacySubjectDiverged { field: "resolver_identity.field" } + } else if left.resolver_policy != right.resolver_policy { + LegacySubjectDiverged { field: "resolver_policy" } + } else if left.occurrence_transport_digest.digest != right.occurrence_transport_digest.digest { + LegacySubjectDiverged { field: "occurrence_transport_digest" } + } else if left.declaration_index_digest.digest != right.declaration_index_digest.digest { + LegacySubjectDiverged { field: "declaration_index_digest" } + } else { + LegacySubjectApplicable + } +} + +// THE SUBJECT'S CONTENT ADDRESS, AND WHY IT IS DERIVED RATHER THAN STORED. +// +// A stored digest beside the seven fields would be a second representation of the same fact, free +// to disagree with them -- and the disagreement would be undetectable, because nothing would +// recompute it. So the identity is a fold over the fields themselves: change any field and the +// address changes, by construction rather than by anyone remembering to update it. +// +// THE TWO NON-DIGEST FIELDS ARE FOLDED THROUGH THEIR RENDERINGS, which is a projection and not a +// second authority: the policy coproduct and the resolver reference are named by their own +// declarations, and this function reads those names rather than re-deciding what they mean. The +// renderings are total matches, so a new policy arm or a changed reference shape fails to compile +// here rather than silently hashing to the same address as before. +fn legacy_resolution_policy_label(policy: LegacyResolutionPolicy) -> String { + match policy { + ImportScopedPolicy => "import_scoped" + NamespaceOnlyPolicy => "namespace_only" + } +} + +// THE FIELD IS FOLDED BECAUSE APPLICABILITY DIVERGES ON IT, and the two must not be able to +// disagree. A pair of subjects that applicability refuses and the content address cannot tell apart +// would be exactly the stored-versus-derived split this function exists to avoid -- one authority +// saying "different bases" and another saying "same base", with nothing to adjudicate. So the rule +// is mechanical rather than a matter of taste: every field the comparison reads, the address folds. +// Caught by review on the first cut of this module, where the address folded six of the eight +// fields the comparison reads. +// AND THE LABELLING MUST BE INJECTIVE, WHICH TOTALITY DOES NOT GIVE. A total match guarantees +// every arm is considered; a hash fold needs the arms to map to DISTINCT values, which is a +// property of the codomain rather than of the match. The first cut of this function returned the +// field name bare, so NamedField { field_name: "whole_declaration" } and WholeDeclaration folded to +// the same address while decl_field_eq correctly reported them different -- the comparison and the +// address disagreeing about what a subject is, reproduced INSIDE the repair for that exact defect. +// The arm tag makes a payload unable to impersonate the nullary arm, because ":" cannot appear +// before it in a bare field name. +// +// legacy_resolution_policy_label needs no such tag and it is worth saying why rather than leaving +// the asymmetry unexplained: both of its arms are nullary with distinct literals, so nothing can +// collide. DeclField is the only labelled type here carrying a payload, which is why it is the only +// one exposed to this class. +fn decl_field_label(field: DeclField) -> String { + match field { + WholeDeclaration => "whole_declaration" + NamedField { field_name: n } => concat("named_field:", n) + } +} + +fn legacy_subject_identity(subject: LegacyBindingObservationSubject) -> Fnv1a64Structural { + let resolver = content_hash_combine_structural( + left: content_hash_combine_structural( + left: content_hash_atom(value: subject.resolver_identity.module_path), + right: content_hash_atom(value: subject.resolver_identity.decl_name) + ), + right: content_hash_atom(value: decl_field_label(field: subject.resolver_identity.field) as NonEmptyStr) + ) + let policy = content_hash_atom(value: legacy_resolution_policy_label(policy: subject.resolver_policy) as NonEmptyStr) + let sources = content_hash_combine_structural( + left: subject.semantic_source_digest, + right: subject.source_set_digest + ) + let build = content_hash_combine_structural(left: subject.compiler_artifact_digest, right: resolver) + let populations = content_hash_combine_structural( + left: subject.occurrence_transport_digest, + right: subject.declaration_index_digest + ) + content_hash_combine_structural( + left: content_hash_combine_structural(left: sources, right: build), + right: content_hash_combine_structural(left: policy, right: populations) + ) +} + +// AN OCCURRENCE ID IS LAWFUL AS AN IDENTITY INSIDE ONE SUBJECT AND UNLAWFUL ACROSS TWO, so a +// reference that travels between subjects carries the scope it was minted in. +// +// The allocator is a monotone counter consumed in traversal order, so an ordinal names an +// occurrence exactly within the compile that allocated it. Pairing it with the subject's content +// address does not derive the occurrence's identity -- the parser minted that -- it SCOPES THE +// ALLOCATOR DOMAIN, which is applicability rather than identity. That distinction is what makes an +// indexable relation admissible where a cross-compile key is not. +type SubjectOccurrenceRef { + subject_identity: Fnv1a64Structural + occurrence: OccurrenceId +}