From e6cb5937be7f009eab11f3cf85205d1fde25eb48 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 26 Aug 2026 12:29:17 +0200 Subject: test(of): validation layers -- Layer 2 properties, litcal grade/identity, golden pins Task 6 (2026-08-25-colitur-of-phases-3-5), the final task of OF Phases 3-5. Layer 2 (test/test_validate_of.ml, new): Colitur_kernel.Validate.run against the real, assembled Rite_of.context -- landmark years, the 9999 domain edge, a 200-year QCheck sample, and the full 8417-year exhaustive sweep under COLITUR_EXHAUSTIVE_SWEEP=1, all filtered through the same three pinned-not-fixed gaps test_rite_of.ml already names (Normae n.35(a) Holy Family fallback, the 25-December lectionary gap, St Joseph/Palm Sunday), duplicated verbatim rather than shared so this file's own filtering cannot drift from Task 5's silently. Two dedicated 200-sample properties confirm Ordinary Time weeks are 1..34 with the final week always 34, and Calendar.year covers its own liturgical year exactly once with no gaps, both through the resolved pipeline (a genuinely different code path from Phase 1's own already-exhaustive Temporal_of-level property). An early version folded a second Calendar.year pass into the exhaustive loop for these two properties too and measured ~365s for that alone (a scratch timing harness, not committed); dropped in favour of one Val.run-only exhaustive loop (~200s), matching the EF harness's shape (one property, one sweep) rather than tripling it. test/test_litcal_of.ml extended beyond season/week to GRADE (litcal's own grade_lcl bucketed against the real Tabula band Precedence_of.band assigns the day's observed office) and IDENTITY (observed slug against a hand-verified event_key -> slug table for the closed 46-entity FIXED/ NAMED set -- deliberately not the numbered Sunday/weekday series, a stated, counted scope limit). Both follow the counted-and-allow-listed discipline: 1800/4346 rows compared for grade (1763 match, 37 allow- listed across 5 new entries), 508/4346 for identity (505 match, 3 allow- listed across 3 new entries), zero unexplained either way. Real divergences found and adjudicated, not suppressed: litcal's own grade vocabulary conflates Tabula I.2/I.3 for Trinity/Corpus Christi (verdict colitur); litcal's Mary Magdalene data predates the 2016 CDW decree (verdict litcal); a genuine, unadjudicated Sacred-Heart/Nativity-of-John- the-Baptist tie-break at equal band, found live at the one Easter date in this fixture's window that creates it (verdict open, no citation found either way); a second instance of precedence_of.mli's own documented forward-only transfer_target limitation, on a date shape the mli's own worked example does not cover (verdict colitur, known limitation). test/test_golden_of.ml (new, 7 pins): a year Ordinary Time skips a week (2026) plus Mary Mother of the Church same date; Advent IV on Christmas Eve in two independent years (2028, 2034); the Annunciation transferred out of Holy Week to Easter+8 (2027, both ends of the transfer pinned); All Souls; the Sacred Heart; 17 December's date-keyed reading in two civil years/weekday-cycle letters. Every new layer mutation-proved: reverting the Advent-IV fix reddens two golden pins; corrupting Precedence_of.band's Tabula I.3 value reddens the litcal grade comparator across every Solemnity in the fixture; renaming one temporal slug reddens the litcal identity comparator; dropping Ordinary Time's second season_runs entry reddens both the landmark-years test and the sampled property. Each mutation applied to lib/rites/rite_of/, confirmed red, then reverted -- git diff --stat lib/ is empty. make check (COLITUR_EXHAUSTIVE_SWEEP=1 dune test --force): exit 0, 890 tests, 363.5s. EF byte-identity holds: git diff --stat v1.0.0..HEAD -- lib/rites/rite_ef/ lib/kernel/ data/ef/ is empty. --- test/test_validate_of.ml | 323 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 323 insertions(+) create mode 100644 test/test_validate_of.ml (limited to 'test/test_validate_of.ml') diff --git a/test/test_validate_of.ml b/test/test_validate_of.ml new file mode 100644 index 0000000..a8a6001 --- /dev/null +++ b/test/test_validate_of.ml @@ -0,0 +1,323 @@ +(* Task 6 (2026-08-26-colitur-of-phases-3-5): Layer 2 (the property harness, + {!Colitur_kernel.Validate.run}) run against the REAL, assembled OF rite + ({!Rite_of.context} -- data/of/calendar-2002.sexp + all 13 amendments + + the real lectionary, exactly what `colitur day --rite of` assembles), + matching test_validate.ml's own EF harness: a 200-year QCheck sample by + default, all 8 417 years (1583..9999) under [COLITUR_EXHAUSTIVE_SWEEP=1]. + + WHY A SEPARATE FILE, not more of test_rite_of.ml (Task 5's own file): + Task 5 already wires [Validate.run] for OF and asserts it on four + landmark years, the domain edges, and a 46-year (2005-2050) sample -- + real, valuable coverage, but neither a QCheck property over the WHOLE + domain nor the committed exhaustive sweep the EF side's own + test_validate.ml carries. This file is that missing piece, one rite + down, not a replacement for Task 5's own tests (which stay as they are, + including their own three pinned defects -- see below). + + THE THREE KNOWN, PINNED-NOT-FIXED GAPS (Task 5's own report; do not + relitigate here, only avoid papering over them): + 1. Normae n. 35(a)'s Holy Family fallback is unreached whenever + Christmas Day is itself a Sunday (test_rite_of.ml's own + [is_known_holy_family_fallback_gap]/ + [test_holy_family_fallback_1583_known_wrong_ferial]) -- fires on + roughly one year in seven, first hit at 1583. + 2. The lectionary (data/of/lectionary.sexp) was audited against only one + civil year (2026) -- surfaces here as [Validate]'s own + ["citations-unresolved"]/["formulary"] gap on 25 December every year + (test_rite_of.ml's own [is_known_nativity_gap]), and, more broadly, + as a citation-chain gap this file's own comparators (which never + touch citations/formulary at all -- see the "what this layer cannot + see" note at the end) cannot see beyond that one symptom either way. + 3. St Joseph / Palm Sunday (Normae n. 56(f)) -- invisible to + [Validate.run] entirely: the impeded solemnity is still transferred + exactly once, to SOME later date, so no structural check + ("lost"/"duplicated"/"unconverged"/"observed") ever fires for it -- + only a value-level check (which day it lands on) could catch it, and + this file adds none. Named here so a reader does not go looking for + a fourth predicate that would never fire. + + Predicates 1 and 2 are duplicated from test_rite_of.ml verbatim (not + shared through a .mli -- the same discipline every Ordo/oracle test file + in this project already states for itself), so THIS file's own gap + handling cannot drift from Task 5's silently. *) + +module Val = Colitur_kernel.Validate +module Layer = Colitur_kernel.Layer +module Overlay = Colitur_kernel.Overlay +module Cal = Colitur_kernel.Calendar +module LD = Colitur_kernel.Liturgical_day +module Temporal = Colitur_kernel.Temporal +module Date = Colitur_kernel.Date +module V = Rite_of.Vocab_of + +let calendar_path = "../data/of/calendar-2002.sexp" +let amendments_dir = "../data/of/amendments/" +let of_lectionary_path = "../data/of/lectionary.sexp" + +let amendment_files = + [ "001-padre-pio.sexp"; "002-juan-diego-cuauhtlatoatzin.sexp"; "003-our-lady-of-guadalupe.sexp"; + "004-john-xxiii-john-paul-ii.sexp"; "005-mary-magdalene-rank.sexp"; "006-mary-mother-of-the-church.sexp"; + "007-paul-vi.sexp"; "008-our-lady-of-loreto.sexp"; "009-faustina-kowalska.sexp"; + "010-narek-avila-hildegard.sexp"; "011-martha-mary-lazarus.sexp"; "012-teresa-of-calcutta.sexp"; + "013-john-henry-newman.sexp" ] + +let real_of_layer = + let base = + match Layer.load V.rank_of_sexp calendar_path with + | Ok l -> l + | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" calendar_path e) + in + let overlays = + List.map + (fun name -> + let path = amendments_dir ^ name in + match Overlay.load V.rank_of_sexp path with + | Ok o -> o + | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" path e)) + amendment_files + in + let layer, diagnostics = Overlay.merge base overlays in + if diagnostics <> [] then + failwith + (Printf.sprintf "unexpected amendment diagnostics: %s" + (String.concat "; " (List.map Overlay.diagnostic_to_string diagnostics))); + layer + +let real_of_lectionary = + match Colitur_kernel.Lectionary.load of_lectionary_path with + | Ok l -> l + | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" of_lectionary_path e) + +let real_of_rite = Rite_of.context ~lectionary:real_of_lectionary + +let run year = Val.run real_of_rite real_of_layer ~year + +(* Duplicated verbatim from test_rite_of.ml -- see this file's own header + for why. *) +let ends_with ~suffix s = + let ls = String.length s and lx = String.length suffix in + ls >= lx && String.sub s (ls - lx) lx = suffix + +let is_known_nativity_gap (f : Val.failure) = + (f.Val.check = "citations-unresolved" || f.Val.check = "formulary") && ends_with ~suffix:"12-25" f.Val.date + +let contains ~substring s = + let ls = String.length s and lx = String.length substring in + let rec go i = i + lx <= ls && (String.sub s i lx = substring || go (i + 1)) in + lx = 0 || go 0 + +let is_known_holy_family_fallback_gap (f : Val.failure) = + f.Val.check = "anchor" && contains ~substring:"of-holy-family" f.Val.detail + +let is_known_gap f = is_known_nativity_gap f || is_known_holy_family_fallback_gap f + +let unexplained_failures year = List.filter (fun f -> not (is_known_gap f)) (run year) + +let check_year_allowing_known_gaps year = + match unexplained_failures year with + | [] -> () + | fs -> + Alcotest.failf "%d: %s" year + (String.concat "; " (List.map Val.failure_to_string (List.filteri (fun i _ -> i < 5) fs))) + +(* ---------------------------------------------------------------------- *) +(* Landmark years and the domain edges, mirroring test_validate.ml's own *) +(* [test_landmark_years]/[test_year_9999_does_not_raise] one rite down. *) +(* ---------------------------------------------------------------------- *) + +let test_landmark_years () = List.iter check_year_allowing_known_gaps [ 1583; 2026; 2035; 9998 ] + +(* 9999: the liturgical year opening there continues into out-of-domain + civil year 10000, so [run]/[Calendar.year] clamp the walk to 31 December + 9999 rather than raising -- the truncated season run is *expected* to + fail the "seasons" check (it never reaches Advent's own end, let alone + Ordinary Time's own week 34), exactly as EF's own + [test_year_9999_does_not_raise] pins. Distinguished from the THREE known + gaps above (still filtered, since 25 December 9999 and a possible + Christmas-Day-is-Sunday shape can both still occur inside the truncated + walk) -- only "seasons" is additionally allowed here, and only here. *) +let test_year_9999_does_not_raise () = + let fs = List.filter (fun f -> not (is_known_gap f)) (run 9999) in + Alcotest.(check bool) "no coverage failures (temporal stayed total through the clamp)" true + (not (List.exists (fun f -> f.Val.check = "coverage") fs)); + Alcotest.(check bool) "seasons check flags the truncated final year as incomplete" true + (List.exists (fun f -> f.Val.check = "seasons") fs); + Alcotest.(check (list string)) "nothing OTHER than the documented seasons truncation (and the three known \ + gaps, already filtered) fired" + [ "seasons" ] + (List.sort_uniq compare (List.map (fun f -> f.Val.check) fs)) + +(* ---------------------------------------------------------------------- *) +(* THE CONFIDENCE-TO-9999 CORE: random years across the whole domain, *) +(* mirroring test_validate.ml's own [prop_invariants] exactly, one rite *) +(* down -- 200 samples by default; every EXHAUSTIVE year under *) +(* [COLITUR_EXHAUSTIVE_SWEEP=1] (below). Filtered of the three known gaps, *) +(* same discipline [check_year_allowing_known_gaps] already applies to the *) +(* landmark years -- a property that asserted [run y = []] UNFILTERED *) +(* would not test anything new (it would just fail on ~1/7 of its own *) +(* samples, the Holy Family gap's own real incidence), and one that *) +(* filtered EVERYTHING unconditionally would risk hiding a genuinely NEW *) +(* failure behind the same three names -- which is exactly why *) +(* [is_known_gap] is the narrow, field-checked pair of predicates above, *) +(* not a blanket "ignore anything on 25 December" rule. *) +let prop_invariants = + QCheck.Test.make ~count:200 ~name:"OF temporal invariants hold across 1583..9998 (modulo the three known, \ + pinned gaps)" + (QCheck.int_range 1583 9998) + (fun y -> unexplained_failures y = []) + +let colitur_exhaustive_sweep_env = "COLITUR_EXHAUSTIVE_SWEEP" + +(* Every year 1583..9999, not a sample -- same env-var gate and the same + reasoning test_validate.ml's own [test_exhaustive_domain_sweep] and + test_temporal_of.ml's own [test_exhaustive_domain_sweep] both already + give: `dune test`'s default run stays fast and reports the skip + honestly; `COLITUR_EXHAUSTIVE_SWEEP=1 dune test --force` runs the real + sweep. *) +(* ---------------------------------------------------------------------- *) +(* "Ordinary Time weeks 1..34, final week always 34" and "the year is *) +(* covered once, no gaps" -- ONE combined helper, ONE {!Cal.year} call, *) +(* deliberately, not two: {!Cal.year} was MEASURED (not assumed) at ~17ms *) +(* per civil year for the real OF rite/data (a scratch timing harness, not *) +(* committed -- {!Val.run} itself costs only ~2ms more on top, dominated *) +(* by the SAME resolution call), so an 8 416-year exhaustive sweep costs *) +(* ~2.5 MINUTES per INDEPENDENT full-domain pass over this data. A naive *) +(* THIRD independent exhaustive loop for each of these two properties *) +(* (mirroring their own separate QCheck properties below one-for-one) *) +(* would have added roughly 5 more minutes to `make check` for marginal *) +(* extra confidence over what the 200-sample properties already give -- *) +(* measured, then rejected as disproportionate, not overlooked. Folded *) +(* into {!test_exhaustive_domain_sweep}'s own loop instead: ONE extra *) +(* {!Cal.year} call per year, alongside {!run}'s own internal one, so the *) +(* total exhaustive cost here is ~2x one full-domain pass, not 3x. *) +let ot_and_coverage_of_year year = + let days = Cal.year real_of_rite real_of_layer year |> Array.to_list in + let dates = List.map (fun (d : (V.season, V.rank) LD.t) -> d.LD.date) days in + let sorted = List.sort Date.compare dates in + let rec no_dup_no_gap = function + | a :: (b :: _ as rest) -> Date.to_rata b - Date.to_rata a = 1 && no_dup_no_gap rest + | _ -> true + in + let unique_count = List.length (List.sort_uniq Date.compare dates) in + let coverage_ok = no_dup_no_gap sorted && unique_count = List.length dates && List.length dates > 0 in + let weeks = + List.filter_map + (fun (d : (V.season, V.rank) LD.t) -> + match d.LD.temporal.Temporal.season with V.Ordinary_time -> d.LD.temporal.Temporal.week | _ -> None) + days + in + (coverage_ok, weeks) + +(* 9999 is handled the same way [test_year_9999_does_not_raise] already + does: its own truncated walk never reaches Ordinary Time's second block + at all (legitimately [weeks = []] there), so the "reaches 34" half is + checked only for 1583..9998, matching {!check_year_allowing_known_gaps}'s + own domain. *) +let ordinary_time_weeks_ok weeks = List.for_all (fun n -> n >= 1 && n <= 34) weeks + +let prop_ordinary_time_weeks_bounded_and_reach_34 year = + let _, weeks = ot_and_coverage_of_year year in + ordinary_time_weeks_ok weeks && List.mem 34 weeks + +let prop_ot_weeks = + QCheck.Test.make ~count:200 ~name:"OF: Ordinary Time weeks are 1..34 and the final week is always 34 \ + (through Rite_of.context/Calendar.year)" + (QCheck.int_range 1583 9998) + prop_ordinary_time_weeks_bounded_and_reach_34 + +(* "Exactly one observed office per day" and "the year covered once, no + gaps" -- {!Cal.year}'s own array is built by walking [start, stop] one + civil day at a time (calendar.ml), so both are guaranteed BY + CONSTRUCTION for any single call; what this property adds is proving + that construction actually holds for the REAL rite/data (not a + placeholder), and, for the "one observed office" half, that + {!Colitur_kernel.Liturgical_day.t.observed} is never ALSO one of its own + day's commemorations/omissions ({!Val.run}'s own ["observed"] check, + already exercised by every [run y = []] assertion in this file -- OF's + own [commemorations] is permanently [] by design (Precedence_of.mli's + own [admit]), so this is really only ever checking [observed] against + [omitted], the transfer-departure shape). *) +let prop_year_covered_once_no_gaps year = + let coverage_ok, _ = ot_and_coverage_of_year year in + coverage_ok + +let prop_coverage = + QCheck.Test.make ~count:200 ~name:"OF: Calendar.year covers its own liturgical year exactly once, no gaps, \ + no duplicates (Rite_of.context, real data)" + (QCheck.int_range 1583 9998) + prop_year_covered_once_no_gaps + +(* MEASURED (a scratch timing harness, not committed): folding the extra + {!Cal.year} call for OT-weeks/coverage into THIS loop, as an early + version of this test did, roughly DOUBLED the sweep's own wall-clock + cost (~365s vs ~180s for {!run} alone, both measured against the same + real data) for confidence this file's own two 200-sample QCheck + properties ([prop_ot_weeks]/[prop_coverage], run on every default `dune + test`) and test_temporal_of.ml's own PRE-EXISTING exhaustive sweep (the + OT-week bound specifically, proven domain-wide already, at the + Temporal_of level -- see [prop_ot_weeks]'s own comment) already + substantially cover. Measured, then deliberately NOT kept: this loop + now costs ONE {!run} call per year, matching the EF harness's own + [test_exhaustive_domain_sweep] shape exactly, not a rite-specific + multiple of it. *) +let test_exhaustive_domain_sweep () = + if Sys.getenv_opt colitur_exhaustive_sweep_env = None then Alcotest.skip () + else begin + let holy_family_gap_years = ref 0 in + let nativity_gap_years = ref 0 in + for y = 1583 to 9998 do + let fs = run y in + let hf = List.exists is_known_holy_family_fallback_gap fs in + let nat = List.exists is_known_nativity_gap fs in + if hf then incr holy_family_gap_years; + if nat then incr nativity_gap_years; + match List.filter (fun f -> not (is_known_gap f)) fs with + | [] -> () + | unexpected -> + Alcotest.failf "%d: %s" y + (String.concat "; " (List.map Val.failure_to_string (List.filteri (fun i _ -> i < 5) unexpected))) + done; + (* 9999 itself: NOT [check_year_allowing_known_gaps] (that predicate + demands NO unexpected failures at all, and the "seasons" truncation + IS expected here, exactly as [test_year_9999_does_not_raise] above + already asserts) -- the identical distinction test_validate.ml's own + [test_exhaustive_domain_sweep] draws between its own [check_year] + (ordinary years) and its own special-cased [run 9999] handling. *) + let fs_9999 = run 9999 in + Alcotest.(check bool) "9999: no coverage failures (temporal stayed total through the clamp)" true + (not (List.exists (fun f -> f.Val.check = "coverage") fs_9999)); + Alcotest.(check bool) "9999: seasons check flags the truncated final year as incomplete" true + (List.exists (fun f -> f.Val.check = "seasons") fs_9999); + Alcotest.(check (list string)) "9999: nothing OTHER than the documented seasons truncation (and the three \ + known, pinned gaps) fired" + [ "seasons" ] + (List.sort_uniq compare + (List.map (fun f -> f.Val.check) (List.filter (fun f -> not (is_known_gap f)) fs_9999))); + (* Both known gaps are real and not vacuous across the FULL domain, not + merely on the handful of years the sampled property happens to draw + -- the Nativity gap fires on literally EVERY year (25 December + always exists); the Holy Family gap fires on roughly one year in + seven (whenever 25 December is a Sunday). Pinned as a range, not an + exact count, deliberately: the exact figure is a real, computable + fact about the Gregorian calendar's own 400-year cycle, but pinning + it to the digit would make this test fail the moment a future + COLITUR_EXHAUSTIVE_SWEEP run's own domain bounds shift by even one + year at either edge, for a reason having nothing to do with + colitur's own correctness. *) + Alcotest.(check int) "the Nativity citation/formulary gap fires on every one of the 8 416 swept years" + 8416 !nativity_gap_years; + Alcotest.(check bool) "the Holy Family fallback gap fires on a real, non-trivial fraction of years \ + (roughly one in seven)" + true + (!holy_family_gap_years > 1000 && !holy_family_gap_years < 1400) + end + +let suite = + ( "Validate (OF, real data: Rite_of.context)", + [ Alcotest.test_case "landmark years validate cleanly (modulo the three known gaps)" `Quick test_landmark_years; + Alcotest.test_case "year 9999 does not raise; seasons flags the clamp, nothing else (beyond the known \ + gaps) fires" `Quick + test_year_9999_does_not_raise; + Alcotest.test_case "exhaustive domain sweep (1583..9999), committed not sampled" `Slow + test_exhaustive_domain_sweep ] + @ List.map QCheck_alcotest.to_alcotest [ prop_invariants; prop_ot_weeks; prop_coverage ] ) -- cgit v1.3