From 947cadfab527829f8e42a896339a0fa6c2e81ad9 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Mon, 17 Aug 2026 14:56:46 +0200 Subject: test: lectionary properties, golden pins, and the blast radius Layers 2 and 5 for the reading citations, which until now had coverage from layers 3 and 4 only -- both oracle-bounded, at 2050 and 2027. test_validate.ml said so in its own words ("No fixture here exercises citations") and test_golden.ml's describe pinned twelve fields, none of them a citation. 358 tests -> 369, and 370 under the sweep. Layer 2 as two Validate checks rather than standalone QCheck properties, so they ride the existing prop_invariants and the exhaustive sweep instead of duplicating that machinery. "citations" asserts a day's parts, sorted, are exactly [First; Gospel] -- one condition carrying three invariants: zero or two but never one, nothing outside First and Gospel since the chants are deliberately unbuilt, and no part twice, which a bare cardinality test would miss. "citations-unresolved" is the separate coverage half: the chain fell through every step. Both are gated on the rite producing some citation somewhere, so a rite whose lectionary is not built is held to neither and the synthetic fixtures stay unaffected. The result over the whole domain: every day of every liturgical year 1583-9999 resolves exactly one Epistle and one Gospel. Mutation-proved live rather than merely silent -- treating a well-formed pair as malformed reddens the suite with real days showing [first,gospel]. citations-unresolved has no live witness at all, which is why test_validate.ml gains five fixtures driving both checks through a new ?readings override, including the gate itself. Layer 5 as six pins, one per chain step, so a regression names the step that broke. Every literal was read out of the scans before being compared with colitur, per that file's standing rule; scan lines are in each pin's comment. Two of the six cover step 4, and the plan's own dates for steps 1 and 4 were wrong: 2030-01-13 is a temporal day (Holy Family on the generic Sunday slug) and would not have exercised step 1, while 2038-03-08 is John of God, who has a full proper Mass and never routes through a Common -- so he becomes the step-1 pin instead. A separate formatter rather than widening describe: widening would invalidate all thirty existing literals at once and the only practical way back would be pasting in whatever colitur printed, which is what the file's header forbids. Restoring them honestly means hand-verifying thirty more Masses against the scans, a task of its own. Stated rather than hidden, and defensible because layer 2 now checks the shape of every day in every year, which is the breadth that widening would have bought. Two pins earned their keep immediately. Lent I Monday failed on "Ezek" against colitur's "Ezech" -- notation only, and colitur matches the Missal's own abbreviation; layer 3 normalises this away and cannot see it. The displaced-Sunday feria pins M26 shape 2(b)'s known-wrong walkback deliberately, labelled as such so a future fix fails loudly, and established two things M26 had not recorded: both parts come from the displacing feast, not only the Gospel it cites, and the reference carries a stray trailing period inherited through the bootstrap. Blast radius: zero. The CLI never calls Validate, no data file changed, and 20 years spanning 1583-9998 produce 7301 byte-identical lines between the pre-change binary and HEAD. Step 4's blind spot is now measured rather than argued. Corrupting the Common of Non-Virgins I's Epistle leaves layer 3 (16801 days) and layer 4 (730 days) both green, reddening only one unit test and one new pin. Both step-4 pins matched the scans on the first attempt -- the first independent confirmation that route has ever had. It narrows the gap without closing it: two of five Common-routed saints are witnessed, isidore-of-seville is not, and gregory-the-great and patrick are unreachable in any year 2005-2050. Register: section 6.7 addendum. validate.mli documents both new labels; liturgical_day.mli's "always empty until Plan 4" was outlived by the lectionary and is corrected. --- lib/kernel/liturgical_day.mli | 9 ++++++- lib/kernel/validate.ml | 60 ++++++++++++++++++++++++++++++++++++++++++- lib/kernel/validate.mli | 23 +++++++++++++++++ 3 files changed, 90 insertions(+), 2 deletions(-) (limited to 'lib') diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli index a109251..f0ea3d9 100644 --- a/lib/kernel/liturgical_day.mli +++ b/lib/kernel/liturgical_day.mli @@ -20,6 +20,13 @@ type ('s, 'r) t = { omitted : ('r Celebration.t * string) list; (** with the reason, never silent -- Task 12's no-celebration-lost invariant reads this *) - citations : Citation.t list; (** always empty until Plan 4 *) + citations : Citation.t list; + (** The day's reading references, resolved by the rite's own + {!Rite.readings}. Empty for a rite whose lectionary is not built; + for EF, exactly one [First] and one [Gospel] on every day of every + year 1583..9999 -- asserted, not assumed, by {!Validate}'s own + ["citations"] / ["citations-unresolved"] checks. (This said "always + empty until Plan 4" until Task 10; the lectionary landed before + Plan 4 did, and the comment outlived its truth.) *) } [@@deriving sexp] diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index ffeb89e..1a0248b 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -388,5 +388,63 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = "admit is not a fixed point on this day's own commemorations: re-offering %d \ admitted %d back" (List.length offered) (List.length readmitted))) - resolved); + resolved; + (* ---- Citation invariants (the lectionary, Plan 4) ---- + + RITE-AGNOSTIC BY CONSTRUCTION, and this gating is the whole reason + these can live in the kernel beside the temporal checks rather than + in EF's own tests: a rite whose lectionary is not built yet returns + [] from {!Rite.readings} on every day, so [year_has_citations] is + false and not one of these fires. A rite that computes readings AT + ALL is held to all of them, on every day of its year. That is also + why test_validate.ml's own synthetic rite ([readings] a constant + [], "a harmless placeholder" in its own words) stays unaffected -- + checked, not assumed: its negative-path fixtures would otherwise + fail on every day of the year rather than on the one invariant each + is built to violate. + + The single [match] below expresses THREE invariants at once, which + is why it is a match on the sorted part list rather than three + separate tests: + + - zero or two, never one -- an Epistle without a Gospel, or the + reverse, is a malformed Mass, not a partial one; + - only [First] and [Gospel] ever appear -- the chants (Psalm, + Second, Tract, Alleluia, Sequence) are deliberately unbuilt, + with no source and no oracle, so a citation carrying one is a + defect and not a feature arriving early; + - no part appears twice -- two Epistles and no Gospel has length + two and would slip past a bare cardinality test. + + [Citation.part]'s own constructor order puts [First] before + [Gospel], so the sorted well-formed list is literally + [[First; Gospel]] and nothing else. *) + let year_has_citations = + Array.exists + (fun (d : ('s, 'r) Liturgical_day.t) -> d.Liturgical_day.citations <> []) + resolved + in + if year_has_citations then + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + let date = d.Liturgical_day.date in + let parts = + List.map (fun (c : Citation.t) -> c.Citation.part) d.Liturgical_day.citations + in + match List.sort compare parts with + | [ Citation.First; Citation.Gospel ] -> () + | [] -> + (* Separate check name from the malformed case below on + purpose: this is the lectionary chain falling through + every one of its steps and resolving nothing, a COVERAGE + gap, where the other is a WELL-FORMEDNESS one. They want + different fixes and should be countable apart. *) + fail date "citations-unresolved" + "no reading citations resolved for this day: the lectionary chain fell through \ + every step" + | sorted -> + fail date "citations" + (Printf.sprintf "expected exactly one First and one Gospel, got [%s]" + (String.concat "," (List.map Citation.part_to_string sorted)))) + resolved); List.rev !failures diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index b46ca30..385e111 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -78,6 +78,29 @@ val failure_to_string : failure -> string was not exceeded" available without embedding a rite's specific numeric caps (RG 111's, for EF) into kernel code. + Two further labels (Task 10) check the day's reading {!Citation.t}s. Both + are GATED on the rite producing at least one citation somewhere in the + year: a rite whose lectionary is not built returns [[]] from + {!Rite.readings} on every day and is held to neither, so this stays a + check on rites that HAVE readings rather than a demand that every rite + have them. + - ["citations"]: well-formedness. A day's citation parts, sorted, are + exactly [[First; Gospel]]. This single condition carries three + invariants at once: zero or two but never one (an Epistle without a + Gospel, or the reverse, is a malformed Mass rather than a partial one); + no part outside [First]/[Gospel] (the chants -- Psalm, Second, Tract, + Alleluia, Sequence -- are deliberately unbuilt, so one appearing is a + defect, not a feature arriving early); and no part twice (two Epistles + and no Gospel has length two and would pass a bare cardinality test). + - ["citations-unresolved"]: coverage. A day resolved NO citations at all, + i.e. the rite's own lookup chain fell through every one of its steps. + Deliberately a separate label from ["citations"] above: a coverage gap + and a well-formedness fault want different fixes and should be + countable apart. On the EF data as it stands this label has no live + witness -- every day of every year 1583..9999 resolves exactly one + Epistle and one Gospel -- which is precisely why test_validate.ml + carries a synthetic fixture proving it can fire at all. + Total over the whole 1583..9999 domain, including [year] = 9999: the liturgical year opening there continues into out-of-domain civil year 10000, so the walk is clamped to 31 December 9999 and the checks run -- cgit v1.3