(* 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 ] )