aboutsummaryrefslogtreecommitdiff
path: root/test/test_rite_ef.ml
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-13 21:19:12 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-13 21:19:12 +0200
commit2af482c7293d821f10c3bbc96b7913d658c5839c (patch)
tree608eaf6bcc46d9dbda0a6dd3a830a5967b201bfa /test/test_rite_ef.ml
parenta3afb19dc6390c9e33ed5fa0ecbd6e5895e60e8d (diff)
parent72b19098905cd609d87783f6e68311de4f1b61a0 (diff)
downloadcolitur-2af482c7293d821f10c3bbc96b7913d658c5839c.tar.gz
colitur-2af482c7293d821f10c3bbc96b7913d658c5839c.zip
Merge branch 'ef-major-litanies': the Major Litanies, and a kernel bug
Builds the Major Litanies (RG 80, 81, 109(f)) -- an item deferred three times, each time on a reason that did not survive contact. Two recorded blockers were false (a kernel signature said to be missing already carried what was needed; Easter Monday, said to be unmarkable, occurs exactly 8417 times in 8417 years) and a displacement estimate of ~97.7% of years measured at 4 years in 46. 8611 days change in four shapes, zero unclassified: the commemoration appearing on ordinary 25 Aprils, displacing St Mark's own on the four II-class Sundays RG 111(b) governs, and relocating to the following Tuesday in the 194 years RG 80's transfer clause fires. No day outside 25/26/27 April differs at all, and observed, rank, colour, season, week and transferred_in are byte-identical across all 3074246 days. The entity is a Commemoration_only sanctoral entry, which honours RG 81 structurally rather than by special case: Precedence.resolve partitions such candidates out of the band contest, so 'nihil fit in Officio' holds by construction, and being sanctoral-origin it can never claim RG 113's de-Tempore first place. And it surfaced a latent kernel bug. Calendar.build_day decided whether a transferred candidate had settled by testing only whether it became that day's observed celebration -- correct for every prior use, a losing feast that wins its unblocked target, and wrong for a Commemoration_only candidate, which can never be observed by the same status that lets it transfer. The first fix accepted two settlement channels and the review found a third: a candidate capped out by admit at its target. That third case was already visible inside the task's own mutation proof, as an undiagnosed ninth failure it had set aside. The fix is a provable no-op in isolation: a3afb19 plus the new calendar.ml alone, swept over every day of the domain, is byte-identical to base.
Diffstat (limited to 'test/test_rite_ef.ml')
-rw-r--r--test/test_rite_ef.ml53
1 files changed, 50 insertions, 3 deletions
diff --git a/test/test_rite_ef.ml b/test/test_rite_ef.ml
index 9a1e6d5..6cd8709 100644
--- a/test/test_rite_ef.ml
+++ b/test/test_rite_ef.ml
@@ -233,6 +233,21 @@ let sample_years =
let rec range a b = if a > b then [] else a :: range (a + 1) b in
range 2005 2050
+(* ef-major-litanies task: [major-litanies] (RG 80, Precedence_ef's own
+ [major_litanies_slug]) is a DELIBERATE, cited exception to this
+ property, not a bug to catch -- RG 80's own text sends the Major
+ Litanies to "the following Tuesday" unconditionally in a transfer year,
+ which is always Easter+2, squarely inside [Easter, Easter+7]
+ (precedence_ef.ml's own [transfer_target] Litanies branch has the full
+ citation and the "why not the general RG96 search" argument). Every
+ OTHER slug this rite ever transfers is still held to the original
+ property below: RG 96's general walk (and its own named Annunciation
+ exception) is what this property actually protects, and neither of
+ those two mechanisms is exempted here -- only this one rite-cited,
+ hand-verified exception, matched by NAME so a future regression in some
+ OTHER slug cannot silently hide behind this exemption. *)
+let is_major_litanies_slug slug = String.equal slug PE.major_litanies_slug
+
(* Property 1: no day in the resolved output, across the whole sample, is
EVER a transfer's landing point inside [Easter, Easter+7] -- checked two
ways. [transferred_out]'s own recorded target is what [transfer_target]
@@ -248,7 +263,7 @@ let test_no_transfer_lands_in_easter_octave () =
Array.iter
(fun (d : (V.season, V.rank) LD.t) ->
(match d.LD.transferred_in with
- | Some c when in_easter_octave d.LD.date ->
+ | Some c when in_easter_octave d.LD.date && not (is_major_litanies_slug (slug_of c)) ->
violations :=
(Printf.sprintf "%s transferred_in on %s (Easter+%d)" (slug_of c)
(Date.to_iso8601 d.LD.date) (easter_offset d.LD.date))
@@ -256,7 +271,7 @@ let test_no_transfer_lands_in_easter_octave () =
| _ -> ());
List.iter
(fun (c, target) ->
- if in_easter_octave target then
+ if in_easter_octave target && not (is_major_litanies_slug (slug_of c)) then
violations :=
Printf.sprintf "%s transferred_out from %s to %s (Easter+%d)" (slug_of c)
(Date.to_iso8601 d.LD.date) (Date.to_iso8601 target) (easter_offset target)
@@ -265,7 +280,37 @@ let test_no_transfer_lands_in_easter_octave () =
days)
sample_years;
Alcotest.(check (list string))
- "no day in [Easter, Easter+7] is ever a transfer's target, 2005-2050" [] (List.rev !violations)
+ "no day (other than the RG80-cited Major Litanies exception) in [Easter, Easter+7] is ever a transfer's \
+ target, 2005-2050" []
+ (List.rev !violations)
+
+(* The positive contrast to the property above: RG 80's own exception DOES
+ fire, exactly twice in the 2005-2050 sample (register: 194/8417 domain-
+ wide trigger years; this task's own report has the full count), both
+ landing on Easter+2 as RG 80's text requires -- proving the exemption
+ above is not merely masking an absent case. 2011 (Easter Monday = 25
+ April, Easter = 24 April) and 2038 (Easter Sunday = 25 April) are this
+ file's own worked examples (precedence_ef.ml's [major_litanies_slug]
+ citation). *)
+let test_major_litanies_transfers_inside_easter_octave_exactly_when_rg80_requires () =
+ let layer = real_layer () in
+ let landings = ref [] in
+ List.iter
+ (fun y ->
+ let days = Cal.year Rite_ef.context layer y in
+ Array.iter
+ (fun (d : (V.season, V.rank) LD.t) ->
+ List.iter
+ (fun (c, target) ->
+ if is_major_litanies_slug (slug_of c) then
+ landings := (Date.to_iso8601 d.LD.date, Date.to_iso8601 target) :: !landings)
+ d.LD.transferred_out)
+ days)
+ sample_years;
+ Alcotest.(check (list (pair string string)))
+ "RG80 fires exactly twice in 2005-2050, both landing on Easter+2"
+ [ ("2011-04-25", "2011-04-26"); ("2038-04-25", "2038-04-27") ]
+ (List.rev !landings)
(* Property 2, and the LIVE case: [PE.transfer_target] called directly, with
an origin that genuinely starts the search INSIDE Holy Week -- Holy
@@ -381,6 +426,8 @@ let suite =
test_transfer_search_does_not_raise_at_domain_ceiling;
Alcotest.test_case "no transfer ever lands inside [Easter, Easter+7], 2005-2050" `Quick
test_no_transfer_lands_in_easter_octave;
+ Alcotest.test_case "RG80: the Major Litanies DO transfer inside the octave, exactly twice in 2005-2050"
+ `Quick test_major_litanies_transfers_inside_easter_octave_exactly_when_rg80_requires;
Alcotest.test_case "transfer_target skips the whole Easter octave from inside Holy Week" `Quick
test_transfer_target_skips_the_whole_easter_octave;
Alcotest.test_case "the search genuinely enters the window (not vacuous)" `Quick