(* 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 KNOWN, PINNED-NOT-FIXED GAPS (Task 5's own report; do not relitigate here, only avoid papering over them). Originally three; now ONE -- items 1 and 2 are both CLOSED (see each one's own CLOSED note): 1. CLOSED, W2 fix (CLAUDE.md, temporal_of.ml). Used to read: "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." {!Rite_of.Temporal_of.temporal} now consults {!Rite_of.Temporal_of.holy_family} directly, independent of weekday, so this fires on ZERO years now, verified across the whole domain by [test_exhaustive_domain_sweep]'s own [holy_family_gap_years] counter below -- not merely assumed from the fix. [is_known_holy_family_ fallback_gap] itself is kept, as a dedicated "this must never recur" check, not deleted -- the same discipline item 2 already established. 2. CLOSED, fix wave I8 (final-review.md, 2026-08-25-colitur-of-phases- 3-5). Used to read: "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". tools/bootstrap_lectionary_of.ml's own [hand_authored] table now injects the Christmas Day Mass directly (Isa 52:7-10/John 1:1-18, OLM 1981's own "16 Ad Missam in die"), so this fires on ZERO years now, verified across the whole domain by [test_exhaustive_domain_sweep]'s own [nativity_gap_years] counter below -- not merely assumed from the fix. [is_known_nativity_gap] itself is kept, as a dedicated "this must never recur" check, not deleted. 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 (* CLOSED, fix wave I8 (final-review.md, 2026-08-25-colitur-of-phases-3-5): see test_rite_of.ml's own [is_known_nativity_gap] header for the citation and the full argument (this predicate is duplicated from that file, this file's own header already states why -- not shared through a .mli). Kept as an explicit "this must never fire again" check, no longer part of [is_known_gap]'s own filter below. *) 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 (* CLOSED, W2 fix (CLAUDE.md, temporal_of.ml): see this file's own header, item 1. Kept as an explicit "this must never fire again" check, no longer part of [is_known_gap]'s own filter below -- the same discipline [is_known_nativity_gap] just above already established. *) let is_known_holy_family_fallback_gap (f : Val.failure) = f.Val.check = "anchor" && contains ~substring:"of-holy-family" f.Val.detail (* Fix wave I8 + W2: both [is_known_nativity_gap] and [is_known_holy_family_fallback_gap] are deliberately excluded now -- see each one's own header just above. A recurrence of either now surfaces as an ordinary unexpected failure everywhere this predicate is used to filter. Kept as a named hook (not inlined to [false] at each call site) so a future gap has an obvious place to land. *) let is_known_gap (_ : Val.failure) = false 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 () = (* [is_known_gap] now filters nothing (both gaps CLOSED) -- kept in the pipeline anyway so a future gap has the same obvious place to land, but [fs] here is really just [run 9999] unfiltered. *) 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 fired (both known \ gaps are CLOSED)" [ "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). Both known gaps are now CLOSED *) (* (this file's own header), so [is_known_gap] filters nothing any more -- *) (* [unexplained_failures y = []] below is really [run y = []] UNFILTERED, *) (* a strictly stronger assertion than this property used to make while *) (* either gap was still open. [is_known_gap] is kept in the pipeline (not *) (* inlined away) so a future gap has the same obvious, narrow, field- *) (* checked place to land that the two closed ones already used. *) let prop_invariants = QCheck.Test.make ~count:200 ~name:"OF temporal invariants hold across 1583..9998 (no known gaps remain)" (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 (* Fix wave I8 + W2: expected to be [false] every single year now for BOTH counters -- kept as a live measurement, not deleted, so a regression anywhere in the domain increments the relevant counter AND (via [is_known_gap] no longer absorbing either shape) fails the loop below immediately, on the first year it recurs, rather than only being caught by the summary assertion after the full sweep completes. *) 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 fired (both \ known gaps are CLOSED)" [ "seasons" ] (List.sort_uniq compare (List.map (fun f -> f.Val.check) (List.filter (fun f -> not (is_known_gap f)) fs_9999))); (* CLOSED, W2 fix: the Holy Family gap used to fire on roughly one year in seven (whenever 25 December is a Sunday) -- real and not vacuous across the FULL domain, not merely the handful of years the sampled property happens to draw. {!Rite_of.Temporal_of.temporal} now consults {!Rite_of.Temporal_of.holy_family} directly, independent of weekday, so this now fires on ZERO years -- across the WHOLE domain, not merely the 4 landmark years test_rite_of.ml's own [test_landmark_years] already checks, which is the entire reason this dedicated exhaustive counter is kept rather than deleted alongside the rest of the old gap-tracking, mirroring the Nativity counter's own already-established pattern just below. *) Alcotest.(check int) "the Holy Family fallback gap fires on NONE of the 8 416 swept years (W2 fix -- was \ roughly one in seven, ~1200)" 0 !holy_family_gap_years; (* CLOSED, fix wave I8: the Nativity gap used to fire on literally every one of the 8 416 swept years (25 December always exists). Now exactly zero -- across the WHOLE domain, not merely the 4 landmark years test_rite_of.ml's own [test_landmark_years] already checks, which is the entire reason this dedicated exhaustive counter is kept rather than deleted alongside the rest of the old gap-tracking. *) Alcotest.(check int) "the Nativity citation/formulary gap fires on NONE of the 8 416 swept years (fix \ wave I8 -- was 8 416)" 0 !nativity_gap_years end let suite = ( "Validate (OF, real data: Rite_of.context)", [ Alcotest.test_case "landmark years validate cleanly (both known gaps are CLOSED)" `Quick test_landmark_years; Alcotest.test_case "year 9999 does not raise; seasons flags the clamp, nothing else 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 ] )