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. --- test/test_validate.ml | 108 +++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 103 insertions(+), 5 deletions(-) (limited to 'test/test_validate.ml') diff --git a/test/test_validate.ml b/test/test_validate.ml index 8c96f26..1a960df 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -3,6 +3,7 @@ module Rite = Colitur_kernel.Rite module P = Colitur_kernel.Precedence module Layer = Colitur_kernel.Layer module Overlay = Colitur_kernel.Overlay +module Citation = Colitur_kernel.Citation module V = Rite_ef.Vocab_ef module T = Rite_ef.Temporal_ef @@ -299,12 +300,26 @@ module Synthetic = struct defaults against the default empty [layer], since nothing ever contests the temporal office there) so the resolution fixtures further down can override them without duplicating every other field. *) - (* No fixture here exercises citations -- readings is a harmless constant - [], the same role the other placeholder defaults above play. *) + (* Most fixtures here exercise no citations -- [readings] is a harmless + constant [], the same role the other placeholder defaults above play, + and {!Validate}'s own citation checks are gated on a rite producing SOME + citation somewhere, so a constant [] leaves them entirely dormant. Task + 10 makes it overridable ([?readings] below) so the citation fixtures at + the end of this file can drive those checks directly, exactly as every + other check here is driven -- rather than leaving two kernel checks with + no committed proof that they can fire at all. *) let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = [] + (* The shape {!Validate} accepts: exactly one First and one Gospel. The + references are deliberately nonsense -- these fixtures assert SHAPE, + never content. *) + let well_formed_citations = + [ { Citation.part = Citation.First; reference = "Synth 1:1" }; + { Citation.part = Citation.Gospel; reference = "Synth 2:2" } ] + let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) ?(rules = rules) - ?(transfer_target = fun _ origin _ -> origin) temporal : (season, rank) Rite.t = + ?(transfer_target = fun _ origin _ -> origin) ?(readings = readings) temporal : + (season, rank) Rite.t = { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs; transfer_target; readings } @@ -315,8 +330,11 @@ module Synthetic = struct unchallenged). Task 12's own resolution fixtures pass their own. *) let empty_layer = Layer.empty ~id:"synthetic-empty" ~name:"empty" - let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?(layer = empty_layer) temporal = - Val.run (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target temporal) layer ~year:2026 + let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?readings ?(layer = empty_layer) + temporal = + Val.run + (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target ?readings temporal) + layer ~year:2026 let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs @@ -708,6 +726,76 @@ let test_resolution_checks_clean_on_a_well_behaved_layer () = Alcotest.(check (list string)) "none of the five checks fire" [] (fired_task12_checks (run ~layer:clean_sanctoral_layer ~rules:clean_sanctoral_rules good)) +(* ---- Task 10: the citation invariants ---- + + Two new kernel checks, and on real EF data NEITHER can fire: every day of + every liturgical year 1583-9999 resolves exactly one Epistle and one + Gospel (measured, not assumed -- the exhaustive sweep is clean, and the + check was mutation-proved live rather than merely silent). That is the + good outcome and precisely why these fixtures are needed: a check with no + live witness and no negative-path test is indistinguishable from a check + that does nothing, which is the trap this whole section of the file exists + to avoid. + + All four drive the checks through [?readings], the same way every fixture + above drives its own check through [?vocab]/[temporal]/[?rules]. *) + +(* The gate itself, and the most load-bearing of the four: a rite that + computes no readings AT ALL (the default constant [], every other fixture + in this file, and any rite whose lectionary is simply not built yet) must + report neither check -- not "usually", not "on this year". Without this, + the natural implementation ("a day with no citations is a failure") would + turn every unrelated fixture here red and, worse, would make [Validate] + demand a lectionary of any rite that has none. *) +let test_citations_silent_without_a_lectionary () = + let fs = run good in + Alcotest.(check bool) "no citation check fires for a rite with no readings at all" false + (has_check "citations" fs || has_check "citations-unresolved" fs) + +(* The positive: well-formed citations on every day report nothing. *) +let test_citations_clean_when_well_formed () = + let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = well_formed_citations in + let fs = run ~readings good in + Alcotest.(check bool) "neither citation check fires when every day carries First + Gospel" false + (has_check "citations" fs || has_check "citations-unresolved" fs) + +(* Zero or two, never one: a lone Epistle is a malformed Mass. This is the + invariant the plan names first, and the one a bootstrap bug would most + plausibly produce -- half a lookup succeeding. *) +let test_citations_fires_on_a_lone_epistle () = + let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = + [ { Citation.part = Citation.First; reference = "Synth 1:1" } ] + in + Alcotest.(check bool) "citations check fires when a day carries an Epistle but no Gospel" true + (has_check "citations" (run ~readings good)) + +(* A part outside this plan's scope. The chants (Psalm/Second/Tract/Alleluia/ + Sequence) are deliberately unbuilt -- no source, no oracle -- so one + appearing is a defect, not a feature arriving early, and must be caught + even though the day is otherwise a well-formed pair. *) +let test_citations_fires_on_an_out_of_scope_part () = + let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = + { Citation.part = Citation.Tract; reference = "Synth 3:3" } :: well_formed_citations + in + Alcotest.(check bool) "citations check fires when a part outside First/Gospel appears" true + (has_check "citations" (run ~readings good)) + +(* The coverage half, kept a SEPARATE check name from the three above: a rite + that resolves readings on most days but falls through on one. On real EF + data this has no witness at all, so this fixture is the only thing that + holds it honest. [target] is the same mid-run day every other fixture in + this file singles out. *) +let test_citations_unresolved_fires_on_a_gap () = + let readings ~observed:_ ~temporal:_ ~date ~temporal_at:_ = + if D.compare date target = 0 then [] else well_formed_citations + in + Alcotest.(check bool) "citations-unresolved fires when one day of the year resolves nothing" true + (has_check "citations-unresolved" (run ~readings good)); + (* ...and the well-formedness check must stay silent on that same run: the + two are different faults and must not be reported as one. *) + Alcotest.(check bool) "the well-formedness check stays silent on a pure coverage gap" false + (has_check "citations" (run ~readings good)) + let suite = ( "Validate", [ Alcotest.test_case "landmark years" `Quick test_landmark_years; @@ -727,6 +815,16 @@ let suite = Alcotest.test_case "vocab rank injectivity fires" `Quick test_vocab_rank_injectivity_fires; Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires; Alcotest.test_case "slugs fires" `Quick test_slugs_fires; + Alcotest.test_case "citations silent without a lectionary" `Quick + test_citations_silent_without_a_lectionary; + Alcotest.test_case "citations clean when well formed" `Quick + test_citations_clean_when_well_formed; + Alcotest.test_case "citations fires on a lone epistle" `Quick + test_citations_fires_on_a_lone_epistle; + Alcotest.test_case "citations fires on an out-of-scope part" `Quick + test_citations_fires_on_an_out_of_scope_part; + Alcotest.test_case "citations-unresolved fires on a gap" `Quick + test_citations_unresolved_fires_on_a_gap; Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception; Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires; Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires; -- cgit v1.3