From 4235a6aa18b815c5457a7eb97fd97eb4919dfd4b Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 02:37:03 +0200 Subject: kernel(validate): fold in Plan 2's carried guards Three carried items from Plan 2's parked rulings, closed: 1. Slug uniqueness moves from a 200-sample QCheck property scoped to one rite (test_temporal_ef.ml) into Validate's own "slugs" check, so every consumer gets it. The resumed-Sunday exemption that property carried is dropped, not weakened elsewhere: Plan 2 verified zero duplicate slugs domain-wide (all 8 416 years), and by construction a resumed Sunday only ever backfills a week number Septuagesima cut short that same liturgical year, so it can never repeat a number that year's own January Sundays already used. The now-redundant property and its is_resumable_sunday_slug helper are removed from test_temporal_ef.ml; test_validate.ml's own domain-wide property covers the same ground for every consumer. 2. The anchors-erosion guard (Plan 2: deleting entries from a rite's anchors list left the whole suite green) is implemented, but not in Validate. Which of a rite's named days are Easter-derived is knowledge only the rite's own `named` function has; Rite.t deliberately exposes only `temporal` and `anchors`, never `named`, so a rite-agnostic Validate has no ground truth to check anchors' completeness against. Hardcoding an Easter offset, or even Easter itself, would smuggle Western/Gregorian-specific knowledge into code meant to also serve a future Julian-reckoning rite; rediscovering "named-ness" structurally from `temporal` alone is unsound for EF, since most ordinary Sunday/feria slugs from Septuagesima onward are also constant-offset-from-Easter by construction. The guard is therefore EF-specific and lives in test_temporal_ef.ml, discovering the Easter-derived slug set mechanically (scanning a window around Easter and keeping whatever `named` answers Some for) rather than hand-copying either named's or anchors' own offset list, then asserting completeness against the real anchors for the domain's Easter extremes (1598, 1666) plus an ordinary year. A negative fixture proves the guard has teeth, matching Plan 2's exact regression (anchors missing "ef-ascension" reports it, and only it, as missing). 3. test_validate.ml's extreme_years comment claimed 1818/2038; verified against Computus.gregorian_easter directly, the domain's actual Easter extremes (1583..2500) are 1598/1666. Corrected. Verification: the full 1583..9999 domain sweep (233 tests via dune test's 200-sample default, plus a manual full sweep) reports exactly one failure -- the known, already-pinned year-9999 season-truncation case -- and zero occurrences of the new "slugs" check anywhere in the domain. Deleting "ef-ascension" from the real anchors list (reproducing Plan 2's regression directly) is caught immediately by the new EF test and, confirmed empirically, invisible to Validate's own full property sweep -- direct evidence for why item 2 cannot live in Validate. --- test/test_temporal_ef.ml | 140 ++++++++++++++++++++++++++++++++++++----------- 1 file changed, 109 insertions(+), 31 deletions(-) (limited to 'test/test_temporal_ef.ml') diff --git a/test/test_temporal_ef.ml b/test/test_temporal_ef.ml index 2ad93e8..477651c 100644 --- a/test/test_temporal_ef.ml +++ b/test/test_temporal_ef.ml @@ -306,36 +306,112 @@ let test_christmastide_feria_slugs () = Alcotest.(check string) "13 Jan (Tue, on/after the origin)" "ef-time-after-epiphany-1-tuesday" (slug_of (d 2026 1 13)) -(* The general property behind the fix above: no two dates in one liturgical - year may share a slug, except the deliberate resumed-Sunday reuse (see - test_resumed_sundays). Random years across the whole domain, not just - 2026 -- the original bug (controller finding A) was found by grepping one - year's CLI output for duplicates, and other years could hide others. *) -let is_resumable_sunday_slug s = - let prefix = "ef-time-after-epiphany-sunday-" in - String.length s > String.length prefix && String.sub s 0 (String.length prefix) = prefix - -let prop_slugs_unique_within_liturgical_year = - QCheck.Test.make ~count:200 - ~name:"no two dates in one liturgical year share a slug, apart from the resumed-Sunday reuse" - (QCheck.int_range 1583 9998) +(* The general property behind the fix above -- no two dates in one + liturgical year may share a slug -- moved to + [Colitur_kernel.Validate]'s own ["slugs"] check (Plan 2 carried item 4), + asserted outright with no resumed-Sunday exemption: Plan 2 verified zero + duplicate slugs domain-wide, so the exemption this property used to carry + protected nothing real. [Validate]'s own 200-sample property + (test_validate.ml's [prop_invariants]) now covers every consumer, + including this rite, over the same 1583..9998 domain this property used + to sweep alone. *) + +(* ---- Plan 2 carried item 5: the anchors list has no guard against its own + erosion ---- + + [Colitur_kernel.Validate] cannot own this completeness check: which of + [named]'s entries are Easter-derived is knowledge only [named] itself + has. [Rite.t] deliberately exposes just [temporal] (the merged result) + and [anchors] (the independent restatement), never [named] -- so a + rite-agnostic [Validate] has no ground truth to compare [anchors] + against, short of inventing one. Two ways of inventing one were + considered and rejected: + + - Hardcoding a specific Easter offset (Ash Wednesday = Easter-46, say) + inside [Validate] would smuggle Western/Gregorian-Paschal-cycle + knowledge into code the design intends to also serve a future + Julian-reckoning rite (Byzantine, named explicitly as a future module + in this project's own architecture note) -- for which neither that + offset, nor even Gregorian Easter itself as the reference point + ([Computus.gregorian_easter], not [julian_easter]), is the right one. + Even [Computus]'s own [ash_wednesday]/[palm_sunday]/[ascension]/ + [pentecost] helpers are documented "(OF + EF)" -- i.e. already scoped + to the two WESTERN forms, not to "any rite" the way [Validate] must + stay. + - Rediscovering "Easter-derived" structurally from [temporal] alone (scan + near Easter, keep whatever recurs at the same offset across years with + different Easters) is unsound for EF specifically: [Time_after_epiphany] + onward, week numbering itself is computed from Easter-relative origins + ([week_origin]), so almost every ORDINARY Sunday/feria slug in + Septuagesima/Lent/Passiontide/Paschaltide/Time_after_pentecost is ALSO + constant-offset-from-Easter across years -- structurally + indistinguishable from a genuinely named day by that test alone. Rank + does not separate them either: RG 91 entry 10 makes the privileged + Easter/Pentecost octave FERIAS class 1 too, same as many named days. + + This guard is therefore entirely EF-specific and lives here, against + [T.named] and [T.anchors] directly -- both accessible in this file, not + through the [Rite.t] boundary. *) + +(* "Easter-derived" is discovered mechanically from [named] itself, not + hand-copied from either [named]'s or [anchors]'s own source: scan a + window of dates around a year's Easter and keep whatever [named] answers + [Some] for. [named] returns [Some] only for its ~20 genuinely proper/named + days -- ordinary Sundays and ferias are produced by other functions + entirely, in [temporal]'s [None] branch -- so this cannot pick up an + ordinary week's slug by accident regardless of window width. [-60, +75] + safely isolates the Easter-relative half of [named] from its + fixed-calendar half: exhaustively checked over 1583..2500, the nearest + fixed named date to Easter (6 January, Epiphany) is never less than 75 + days before the EARLIEST possible Easter (22 March), so a 60-day backward + reach cannot cross into it even in the closest year, while the window + still comfortably covers [named]'s actual Easter-relative range (Ash + Wednesday at Easter-46 the earliest, Sacred Heart at Easter+68 the + latest). *) +let easter_relative_named_slugs y = + let easter = Colitur_kernel.Computus.gregorian_easter y in + List.filter_map + (fun n -> match T.named (D.add_days easter n) with Some (_, slug, _, _) -> Some slug | None -> None) + (List.init 136 (fun i -> i - 60)) + |> List.sort_uniq compare + +let anchor_slugs y = List.map fst (T.anchors y) |> List.sort_uniq compare + +(* The mechanism both tests below share: which of [named]'s Easter-derived + slugs [anchors] fails to restate. [] means complete. *) +let missing_from_anchors ~named_easter_slugs ~anchors = + List.filter (fun slug -> not (List.mem slug anchors)) named_easter_slugs + +(* The real guard: for the domain's own Easter extremes (1598 earliest, 1666 + latest -- see test_validate.ml's own [extreme_years], corrected by this + same task) plus an ordinary year, nothing [named] produces at an + Easter-relative offset is missing from [anchors]. *) +let test_anchors_cover_easter_derived_named_days () = + List.iter (fun y -> - let start = T.year_start y in - let stop = D.add_days (T.year_start (y + 1)) (-1) in - let n = D.to_rata stop - D.to_rata start + 1 in - let seen = Hashtbl.create 512 in - let rec check i = - i >= n - || - let s = slug_of (D.add_days start i) in - (is_resumable_sunday_slug s - || (not (Hashtbl.mem seen s)) - && ( - Hashtbl.replace seen s (); - true)) - && check (i + 1) + let missing = + missing_from_anchors ~named_easter_slugs:(easter_relative_named_slugs y) ~anchors:(anchor_slugs y) in - check 0) + Alcotest.(check (list string)) + (Printf.sprintf "%d: every Easter-derived named slug is restated in anchors" y) + [] missing) + [ 1598; 1666; 2026 ] + +(* Proves the guard above actually has teeth, per this task's negative-fixture + requirement: [T.anchors]'s real slug set with one genuinely Easter-derived + entry ("ef-ascension") struck out must fail [missing_from_anchors] the same + way the real list passes it -- reproducing, in miniature, exactly what + "deleting four entries leaves the whole suite green" (Plan 2, carried item + 5) looked like before this test existed. *) +let test_anchors_erosion_is_caught () = + let y = 2026 in + let named_easter_slugs = easter_relative_named_slugs y in + Alcotest.(check bool) "sanity: ef-ascension is genuinely in the Easter-derived set" true + (List.mem "ef-ascension" named_easter_slugs); + let eroded_anchors = List.filter (fun s -> s <> "ef-ascension") (anchor_slugs y) in + Alcotest.(check (list string)) "the erosion is caught: the missing entry is reported, and only it" + [ "ef-ascension" ] + (missing_from_anchors ~named_easter_slugs ~anchors:eroded_anchors) let test_totality () = (* Every day of 2026 yields an office without raising. Not a slug @@ -367,12 +443,14 @@ let suite_extra = Alcotest.test_case "colours" `Quick test_colours; Alcotest.test_case "christmastide feria slugs" `Quick test_christmastide_feria_slugs; Alcotest.test_case "named days carry their week" `Quick test_named_days_carry_their_week; - Alcotest.test_case "totality" `Quick test_totality ] + Alcotest.test_case "totality" `Quick test_totality; + Alcotest.test_case "anchors cover easter-derived named days" `Quick + test_anchors_cover_easter_derived_named_days; + Alcotest.test_case "anchors erosion is caught" `Quick test_anchors_erosion_is_caught ] let suite = ( "Rite_ef", [ Alcotest.test_case "vocab roundtrips" `Quick test_vocab_roundtrips; Alcotest.test_case "slug words" `Quick test_slug_words ] @ suite_extra - @ List.map QCheck_alcotest.to_alcotest - [ prop_temporal_week_matches_week; prop_slugs_unique_within_liturgical_year ] ) + @ List.map QCheck_alcotest.to_alcotest [ prop_temporal_week_matches_week ] ) -- cgit v1.3 From b12043525ea674148c0c297b8a1792299c2f6956 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 10:20:05 +0200 Subject: test(temporal-ef): extend the anchors-erosion guard to fixed-date anchors The guard added under Plan 2's carried item 5 only scanned a +/-window of dates around Easter, so it caught erosion of an Easter-relative anchor but missed a fixed-date one entirely: deleting ("ef-nativity", ...), ("ef-epiphany", ...) or ("ef-christ-the-king", ...) from temporal_ef.ml's anchors list left the whole suite green. Item 5 -- the item this guard exists to satisfy -- was therefore only half-closed while being reported as closed, and the least-covered anchor was exactly the one with the weakest citation (Christ the King's last-Sunday-of-October placement, oracle-backed but not yet primary-verified as of this commit). Widened the scan from an Easter-centred window to the whole civil year: named only ever answers Some for its ~20 genuinely proper/named days, so scanning every day of the year is no more likely to pick up an ordinary week's slug by accident than the narrower window was -- it is simply no longer selective about which KIND of named day it notices. Renamed easter_relative_named_slugs to named_slugs_for_year and the covering test to test_anchors_cover_all_named_days accordingly; broadened the negative fixture (test_anchors_erosion_is_caught) to strike an Easter-relative and a fixed-date anchor together. Verified by deleting each of the three previously-unguarded anchors in turn (locally, reverted after each), rebuilding and re-running the suite: delete ef-nativity: Received: `["ef-nativity"]' delete ef-epiphany: Received: `["ef-epiphany"]' delete ef-christ-the-king: Received: `["ef-christ-the-king"]' each against the same assertion: ASSERT 1598: every named slug is restated in anchors FAIL 1598: every named slug is restated in anchors Expected: `[]' All three reversions applied only to temporal_ef.ml (not committed); the tree is unchanged there. Test count unchanged (259); no behaviour change. --- test/test_temporal_ef.ml | 107 ++++++++++++++++++++++++++++------------------- 1 file changed, 63 insertions(+), 44 deletions(-) (limited to 'test/test_temporal_ef.ml') diff --git a/test/test_temporal_ef.ml b/test/test_temporal_ef.ml index 477651c..751abd2 100644 --- a/test/test_temporal_ef.ml +++ b/test/test_temporal_ef.ml @@ -351,67 +351,86 @@ let test_christmastide_feria_slugs () = This guard is therefore entirely EF-specific and lives here, against [T.named] and [T.anchors] directly -- both accessible in this file, not - through the [Rite.t] boundary. *) - -(* "Easter-derived" is discovered mechanically from [named] itself, not - hand-copied from either [named]'s or [anchors]'s own source: scan a - window of dates around a year's Easter and keep whatever [named] answers - [Some] for. [named] returns [Some] only for its ~20 genuinely proper/named - days -- ordinary Sundays and ferias are produced by other functions - entirely, in [temporal]'s [None] branch -- so this cannot pick up an - ordinary week's slug by accident regardless of window width. [-60, +75] - safely isolates the Easter-relative half of [named] from its - fixed-calendar half: exhaustively checked over 1583..2500, the nearest - fixed named date to Easter (6 January, Epiphany) is never less than 75 - days before the EARLIEST possible Easter (22 March), so a 60-day backward - reach cannot cross into it even in the closest year, while the window - still comfortably covers [named]'s actual Easter-relative range (Ash - Wednesday at Easter-46 the earliest, Sacred Heart at Easter+68 the - latest). *) -let easter_relative_named_slugs y = - let easter = Colitur_kernel.Computus.gregorian_easter y in + through the [Rite.t] boundary. + + EXTENDED (final fix wave, item 3): the guard originally scanned only a + 60/+75-day window around Easter, so it caught erosion of an + Easter-relative anchor (Ascension, say) but not of a FIXED-date one -- + Nativity, the Nativity vigil, the three Nativity octave days, the + Circumcision, Epiphany -- nor of [christ_the_king], which is neither + fixed nor Easter-relative (the last Sunday of October). Deleting any of + those from [T.anchors] left the whole suite green: Plan 2's carried item + 5 was therefore only half-closed while being reported as closed, and the + worst-covered anchor was exactly the one with the weakest citation + (Christ the King -- oracle-backed, not yet primary-verified when this + note was written; see docs/research/rules-register.md §4/§6, since + primary-verified at RG 17(d) by this same fix wave). Fixed by widening + the scan from an Easter-centred window to the WHOLE civil year: [named] + only ever answers [Some] for its ~20 genuinely proper/named days + (ordinary Sundays and ferias are produced entirely by [temporal]'s own + [None] branch, never by [named]), so scanning every day of the year + cannot pick up an ordinary week's slug by accident any more than the + narrower window could -- it is simply no longer selective about WHICH + kind of named day it is willing to notice. *) + +(* Every slug [named] can produce for civil year [y] -- fixed-date AND + Easter-relative alike -- discovered mechanically by asking [named] itself + about every day of the year (366 days from 1 January, safely covering a + leap year plus one day of spillover into the next, which duplicates + rather than misleads: every slug [named] returns is a year-invariant + string), not hand-copied from either [named]'s or [anchors]'s own + source. *) +let named_slugs_for_year y = + let jan1 = d y 1 1 in List.filter_map - (fun n -> match T.named (D.add_days easter n) with Some (_, slug, _, _) -> Some slug | None -> None) - (List.init 136 (fun i -> i - 60)) + (fun i -> match T.named (D.add_days jan1 i) with Some (_, slug, _, _) -> Some slug | None -> None) + (List.init 366 (fun i -> i)) |> List.sort_uniq compare let anchor_slugs y = List.map fst (T.anchors y) |> List.sort_uniq compare -(* The mechanism both tests below share: which of [named]'s Easter-derived - slugs [anchors] fails to restate. [] means complete. *) -let missing_from_anchors ~named_easter_slugs ~anchors = - List.filter (fun slug -> not (List.mem slug anchors)) named_easter_slugs +(* The mechanism both tests below share: which of [named]'s slugs [anchors] + fails to restate. [] means complete. *) +let missing_from_anchors ~named_slugs ~anchors = + List.filter (fun slug -> not (List.mem slug anchors)) named_slugs (* The real guard: for the domain's own Easter extremes (1598 earliest, 1666 latest -- see test_validate.ml's own [extreme_years], corrected by this - same task) plus an ordinary year, nothing [named] produces at an - Easter-relative offset is missing from [anchors]. *) -let test_anchors_cover_easter_derived_named_days () = + same task) plus an ordinary year, nothing [named] produces -- fixed-date + or Easter-relative -- is missing from [anchors]. *) +let test_anchors_cover_all_named_days () = List.iter (fun y -> let missing = - missing_from_anchors ~named_easter_slugs:(easter_relative_named_slugs y) ~anchors:(anchor_slugs y) + missing_from_anchors ~named_slugs:(named_slugs_for_year y) ~anchors:(anchor_slugs y) in Alcotest.(check (list string)) - (Printf.sprintf "%d: every Easter-derived named slug is restated in anchors" y) + (Printf.sprintf "%d: every named slug is restated in anchors" y) [] missing) [ 1598; 1666; 2026 ] (* Proves the guard above actually has teeth, per this task's negative-fixture - requirement: [T.anchors]'s real slug set with one genuinely Easter-derived - entry ("ef-ascension") struck out must fail [missing_from_anchors] the same - way the real list passes it -- reproducing, in miniature, exactly what - "deleting four entries leaves the whole suite green" (Plan 2, carried item - 5) looked like before this test existed. *) + requirement, now over BOTH shapes of anchor: [T.anchors]'s real slug set + with one Easter-relative entry ("ef-ascension") AND one fixed-date entry + ("ef-nativity") struck out together must fail [missing_from_anchors] the + same way the real list passes it -- reproducing, in miniature, exactly + what "deleting ef-nativity, ef-epiphany and ef-christ-the-king leaves the + whole suite green" (final fix wave, item 3) looked like before this test + existed. *) let test_anchors_erosion_is_caught () = let y = 2026 in - let named_easter_slugs = easter_relative_named_slugs y in - Alcotest.(check bool) "sanity: ef-ascension is genuinely in the Easter-derived set" true - (List.mem "ef-ascension" named_easter_slugs); - let eroded_anchors = List.filter (fun s -> s <> "ef-ascension") (anchor_slugs y) in - Alcotest.(check (list string)) "the erosion is caught: the missing entry is reported, and only it" - [ "ef-ascension" ] - (missing_from_anchors ~named_easter_slugs ~anchors:eroded_anchors) + let named_slugs = named_slugs_for_year y in + Alcotest.(check bool) "sanity: ef-ascension is genuinely a named slug" true + (List.mem "ef-ascension" named_slugs); + Alcotest.(check bool) "sanity: ef-nativity is genuinely a named slug" true + (List.mem "ef-nativity" named_slugs); + let eroded_anchors = + List.filter (fun s -> s <> "ef-ascension" && s <> "ef-nativity") (anchor_slugs y) + in + Alcotest.(check (list string)) + "the erosion is caught: both missing entries are reported, and only them" + [ "ef-ascension"; "ef-nativity" ] + (missing_from_anchors ~named_slugs ~anchors:eroded_anchors) let test_totality () = (* Every day of 2026 yields an office without raising. Not a slug @@ -444,8 +463,8 @@ let suite_extra = Alcotest.test_case "christmastide feria slugs" `Quick test_christmastide_feria_slugs; Alcotest.test_case "named days carry their week" `Quick test_named_days_carry_their_week; Alcotest.test_case "totality" `Quick test_totality; - Alcotest.test_case "anchors cover easter-derived named days" `Quick - test_anchors_cover_easter_derived_named_days; + Alcotest.test_case "anchors cover all named days" `Quick + test_anchors_cover_all_named_days; Alcotest.test_case "anchors erosion is caught" `Quick test_anchors_erosion_is_caught ] let suite = -- cgit v1.3