From 89b6cfbc8c2a9f5921c19543f893decc2497ef69 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Sat, 22 Aug 2026 12:29:06 +0200 Subject: fix(ef): check RG 24/25's ferial invariant instead of asserting it rubrics_ef.ml's Creed check excluded feriae from 475(b)/(c)/(e) via an explicit test for feria I classis (Ash Wednesday, Holy Week) and vigils only. RG 24/25's feriae II and III classis (Advent 17-23 December, the Advent/Lent/September Ember sets, the numbered Lenten/Passiontide ferias) were excluded by no check at all, correct today only because of an unstated Temporal_ef property (no ferial-origin office it builds carries subject Lord/Bvm or an apostle-list slug). A comment read as if this were established "by construction of the two exclusions immediately above", which overclaimed: those two exclusions cover feria I classis only. Corrected the comments to name RG 24/25 explicitly, state what is and is not checked, and cite where the real guarantee comes from. Added a test that sweeps Temporal_ef.temporal across a century (1583-1682), asserting the invariant directly against every ferial-origin day found, with its own coverage counters confirming the span actually reaches Advent 17-23, all three non-Whitsun Ember sets, and Lenten/Passiontide ferias. The first run of the test found a real gap in its own population filter (RG 17(a)'s 2 January Holy Name fallback, a genuine feast sitting outside Temporal_ef.named for an architectural reason), fixed by naming that date explicitly rather than narrowing the span. Proved the test has teeth by mutation: forcing the ferial builder's default subject to Lord reddened it (and 24 other tests, expected collateral from an intentionally broad mutation) before being reverted. No production logic changed -- only comments in rubrics_ef.ml. day, readings and rubrics output confirmed byte-identical against the pre-fix binary for four spot years across the domain. Also corrects a stale test-case count in a prior task report (18 in the array, not the 19 recorded there); the array now genuinely holds 19. --- test/test_rubrics_ef.ml | 156 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 154 insertions(+), 2 deletions(-) (limited to 'test/test_rubrics_ef.ml') diff --git a/test/test_rubrics_ef.ml b/test/test_rubrics_ef.ml index 2000d61..5109c69 100644 --- a/test/test_rubrics_ef.ml +++ b/test/test_rubrics_ef.ml @@ -9,7 +9,14 @@ this module existed, never read off [Rubrics_ef.creed]'s own answer. Two synthetic unit tests isolate Trap One (RG 475(a) reads [temporal], never [observed]) directly, without depending on finding a real-calendar - coincidence. *) + coincidence. + + One further test (celebrant-rubrics-phase1 review, finding 1) is + different in kind from the rest: not an end-to-end [creed] check + against a single real date, but a direct sweep of {!Rite_ef.Temporal_ef} + output across a century, asserting the unstated invariant [creed]'s own + RG 24/25 ferial branches rely on rather than leaving it asserted only + in prose -- see its own header comment for the full account. *) module Cal = Colitur_kernel.Calendar module LD = Colitur_kernel.Liturgical_day @@ -21,6 +28,7 @@ module Slug = Colitur_kernel.Slug module Temporal = Colitur_kernel.Temporal module V = Rite_ef.Vocab_ef module RE = Rite_ef.Rubrics_ef +module TE = Rite_ef.Temporal_ef let mk y m d = match Date.make ~year:y ~month:m ~day:d with Ok t -> t | Error e -> failwith e @@ -208,6 +216,148 @@ let test_every_sunday_in_2026_says_the_creed () = true d.LD.creed) days +(* ---- Review finding 1 (celebrant-rubrics-phase1 fix task): RG 24/25's + feriae II and III classis (the Advent ferias 17-23 December, the + Advent/Lent/September Ember sets, and the numbered Lenten/Passiontide + ferias) are excluded from the Creed by NO check in rubrics_ef.ml -- see + that file's own RG 23 comment (the [n = -46 ...] branch) for the full + account. [creed]'s correct [false] answer for them rests entirely on an + unstated property of {!Rite_ef.Temporal_ef}: no ferial-origin office it + ever builds carries [subject = Lord] or [subject = Bvm] at [Class2] + (RG 475(c)'s own rank guard), and none carries a slug on + [RE.creed_apostle_slugs] (RG 475(e), which has no rank guard at all). + This test asserts that property directly against real Temporal_ef + output, rather than leaving it asserted only in prose, so a future + Temporal_ef change that breaks it fails HERE loudly instead of silently + changing the Creed. + + Two real, harmless, already-documented exceptions are excluded from the + [subject] checks rather than papered over: the Sacred Triduum + ([subject = Lord], [Class1] -- verified in temporal_ef.ml's own + [triduum_names] branch) and the votive Office of the BVM on Saturday, + RG 91 entry 27 ([subject = Bvm], [Class4] -- {!TE}'s own [is_bvm_saturday] + citation). Neither can ever reach [creed]'s 475(c) branch: the Triduum + is caught earlier by the explicit feria-I-classis check (its own + [Class1] is not [Class2]), and the BVM Saturday Office is [Class4], not + [Class2], so 475(c)'s own rank guard excludes it regardless of subject. + Excluding them here is not a loophole in the test -- it is the precise + boundary of what RG 475(c) actually reads, confirmed rather than + assumed by restricting the [Lord]/[Bvm] checks to exactly [Class2] (RG + 24's own II-class population) and [Class3] (RG 25's III-class + population), the two ranks a real feria can carry that are NOT already + handled by an explicit branch or a rank mismatch. The apostle-slug + check has no such carve-out: it is asserted for every ferial-origin day + of every rank, matching 475(e)'s own unguarded text. + + A THIRD exception -- not anticipated when this test was first written, + found by actually running it, not by inspection -- had to be excluded + from the POPULATION itself, not from the subject checks: RG 17(a)'s own + "secus die 2 ianuarii" fallback (2 January, only in a civil year with + no 2-5 January Sunday) is a genuine FEAST, [subject = Lord], [Class2], + sitting outside {!TE.named}'s table for a purely architectural reason + (temporal_ef.ml's own citation: that table's shape cannot express a + fallback conditional on a per-year fact) and not always a Sunday + either, so neither of [is_ferial_origin]'s two filters caught it on the + first run -- it failed on 1584-01-02 before {!is_holy_name_fallback} + below was added. Left in as evidence the sweep has real teeth rather + than trimmed from the span: excluding a genuine mistaken positive by + name, once found, is the correct fix; narrowing the span to dodge it + would not have been. + + A day is "ferial-origin" here iff {!TE.named} returns [None] for it + (nothing in the fixed/movable table of named feasts, vigils and octave + days claims it), it is not a Sunday (RG 21's own definition: "Nomine + feriae intelleguntur singuli dies hebdomadae, praeter dominicam" -- + every day of the week EXCEPT Sunday), and it is not the RG 17(a) + fallback date just above. *) +let contains_substring ~needle haystack = + let nl = String.length needle and hl = String.length haystack in + let rec loop i = (i + nl <= hl) && (String.sub haystack i nl = needle || loop (i + 1)) in + nl = 0 || loop 0 + +(* RG 17(a)'s own "secus die 2 ianuarii" fallback (temporal_ef.ml's own + citation on [holy_name_fallback_date]): a genuine FEAST, [subject = + Lord], [Class2] -- legitimately outside {!TE.named}'s table only for an + architectural reason (that table's bare [Date.t -> ... option] shape + cannot express a fallback conditional on a per-year fact, + [holy_name_sunday y = None]), never a ferial one, and it is not always + a Sunday, so the weekday filter below does not catch it either. Found + by running this test before this exclusion existed: it failed on + 1584-01-02, a real year with no 2-5 January Sunday. *) +let is_holy_name_fallback (d : Date.t) = + let y = Date.year d in + Date.compare d (TE.holy_name_fallback_date y) = 0 && TE.holy_name_sunday y = None + +let is_ferial_origin (d : Date.t) = + TE.named d = None && Date.weekday d <> Date.Sun && not (is_holy_name_fallback d) + +(* Span: civil years 1583-1682, the domain's own opening century -- every + RG 24/25 population recurs every civil year (Advent 17-23, all three + non-Whitsun Ember sets, and Lenten/Passiontide ferias are none of them + rare or conditional), so one year already gives full COVERAGE; a + century instead of one is for confidence the invariant is not an + accident of a single Easter date, at a cost (day-by-day calls to the + pure {!TE.temporal}, no Calendar/Precedence resolution) cheap enough to + stay in the default, unsampled suite. 1583 is also the domain's own + lower bound, and this span contains 1598, the earliest possible Easter + (22 March) in [1583, 2500] per {!test_easter_extremes} above -- a real, + not merely nominal, edge case. Coverage is VERIFIED below via counters, + not assumed: a test that never actually walks an Ember day would prove + nothing about Ember days. *) +let test_ferial_origin_never_carries_lord_bvm_or_apostle_slug () = + let total = ref 0 + and advent_ember = ref 0 + and lent_ember = ref 0 + and september_ember = ref 0 + and advent_17_23 = ref 0 + and lenten_passiontide_class3 = ref 0 in + for y = 1583 to 1682 do + let dec31 = mk y 12 31 in + let d = ref (mk y 1 1) in + while Date.compare !d dec31 <= 0 do + (if is_ferial_origin !d then begin + let t = TE.temporal !d in + incr total; + let office = t.Temporal.office in + let slug = Slug.to_string office.Cel.slug in + let label = Printf.sprintf "%s (%s, rank=%s)" (Date.to_iso8601 !d) slug + (match office.Cel.rank with + | V.Class1 -> "1" + | V.Class2 -> "2" + | V.Class3 -> "3" + | V.Class4 -> "4") + in + (* Coverage tallies -- checked against zero below. *) + if contains_substring ~needle:"advent-ember" slug then incr advent_ember; + if contains_substring ~needle:"lent-ember" slug then incr lent_ember; + if contains_substring ~needle:"september-ember" slug then incr september_ember; + if Date.month !d = 12 && Date.day !d >= 17 && Date.day !d <= 23 then incr advent_17_23; + if + office.Cel.rank = V.Class3 + && (t.Temporal.season = V.Lent || t.Temporal.season = V.Passiontide) + then incr lenten_passiontide_class3; + (* The invariant itself. Apostle slugs: every rank, no carve-out. *) + Alcotest.(check bool) (label ^ ": not on the apostle-natalicium slug list") false + (List.mem slug RE.creed_apostle_slugs); + (* Lord/Bvm subject: only at the two ranks a real RG 24/25 feria + can carry -- see this test's own header for why Class1 + (Triduum) and Class4 (BVM Saturday) are deliberately excluded. *) + if office.Cel.rank = V.Class2 || office.Cel.rank = V.Class3 then begin + Alcotest.(check bool) (label ^ ": not subject Lord") false (office.Cel.subject = Subject.Lord); + Alcotest.(check bool) (label ^ ": not subject Bvm") false (office.Cel.subject = Subject.Bvm) + end + end); + d := Date.add_days !d 1 + done + done; + Alcotest.(check bool) "span examined a real number of ferial-origin days" true (!total > 10_000); + Alcotest.(check bool) "span reached Advent Ember days" true (!advent_ember > 0); + Alcotest.(check bool) "span reached Lent Ember days" true (!lent_ember > 0); + Alcotest.(check bool) "span reached September Ember days" true (!september_ember > 0); + Alcotest.(check bool) "span reached Advent 17-23 ferias" true (!advent_17_23 > 0); + Alcotest.(check bool) "span reached Lenten/Passiontide III-class ferias" true + (!lenten_passiontide_class3 > 0) + let suite = ( "Rubrics_ef", [ Alcotest.test_case "475(a): ordinary Sunday" `Quick test_475a_ordinary_sunday; @@ -237,4 +387,6 @@ let suite = test_vigil_excluded_even_when_class2_and_marian; Alcotest.test_case "476(d): BVM Saturday Office, IV class" `Quick test_476d_bvm_saturday_office; Alcotest.test_case "every Sunday in 2026 says the Creed" `Quick - test_every_sunday_in_2026_says_the_creed ] ) + test_every_sunday_in_2026_says_the_creed; + Alcotest.test_case "RG 24/25: no ferial-origin office carries Lord/Bvm or an apostle slug" `Quick + test_ferial_origin_never_carries_lord_bvm_or_apostle_slug ] ) -- cgit v1.3