summaryrefslogtreecommitdiff
path: root/test/test_precedence_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_precedence_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_precedence_ef.ml')
-rw-r--r--test/test_precedence_ef.ml124
1 files changed, 117 insertions, 7 deletions
diff --git a/test/test_precedence_ef.ml b/test/test_precedence_ef.ml
index 6f8b5b5..790dab6 100644
--- a/test/test_precedence_ef.ml
+++ b/test/test_precedence_ef.ml
@@ -555,6 +555,45 @@ let disposition_cases =
cand ~origin:P.Sanctoral ~status:Cel.Commemoration_only ~layer:PE.universal_layer
"ef-suppressed-vigil",
"Commemorate(Privileged)" );
+ (* RG 80 (ef-major-litanies task, NEW) -- {!PE.major_litanies_slug}'s
+ own citation (precedence_ef.ml, above [privilege_of]) has the full
+ text. The row immediately above proves "Commemoration_only is
+ ALWAYS Commemorate" as a GENERAL rule; these three rows prove
+ [PE.major_litanies_slug] is the ONE deliberate, cited EXCEPTION to
+ it, and prove the exception is gated on the WINNER's own slug, not
+ merely on the loser being this particular Commemoration_only
+ candidate. *)
+ ( "RG80 first trigger: the Litanies lose to Easter Sunday itself -> \
+ Transfer, not Commemorate (25 April IS Easter Sunday this year)",
+ cand "ef-easter-sunday",
+ cand ~origin:P.Sanctoral ~status:Cel.Commemoration_only ~rank:V.Class4 ~layer:PE.universal_layer
+ PE.major_litanies_slug,
+ "Transfer" );
+ ( "RG80 second trigger: the Litanies lose to Easter Monday -> \
+ Transfer (25 April IS Easter Monday this year, i.e. Easter itself \
+ is 24 April)",
+ cand "ef-easter-1-monday",
+ cand ~origin:P.Sanctoral ~status:Cel.Commemoration_only ~rank:V.Class4 ~layer:PE.universal_layer
+ PE.major_litanies_slug,
+ "Transfer" );
+ (* MUTATION-PROOFING the WINNER-slug guard specifically (not merely
+ "the Litanies can transfer at all"): losing to a THIRD I-class
+ temporal winner that is neither of RG 80's two named trigger days
+ must NOT transfer -- RG 80's own condition is exactly "Easter
+ Sunday or Easter Monday", not "any I-class day", and 25 April can
+ structurally never actually coincide with, say, the Nativity in
+ real data (this row is a deliberately synthetic collision, the
+ same "proves the guard, not merely the absence of its own bug"
+ shape {!band}'s own Holy-Family-window row uses) -- if
+ {!PE.disposition}'s own winner-slug test were ever loosened to
+ "any Class1 winner", this row would wrongly turn [Transfer] too. *)
+ ( "SYNTHETIC: the Litanies losing to an UNRELATED I-class day (not \
+ Easter Sunday or Monday) is an ordinary Commemoration_only loser \
+ -- Commemorate(Privileged) via RG109(f), NOT Transfer",
+ cand "ef-nativity",
+ cand ~origin:P.Sanctoral ~status:Cel.Commemoration_only ~rank:V.Class4 ~layer:PE.universal_layer
+ PE.major_litanies_slug,
+ "Commemorate(Privileged)" );
(* Totality (SANCTORAL side): the lower ranks the RG 33/RG 95/Task-16
branches never touch still reach the RG 95 "commemorated or omitted"
branch's [Commemorate] side, not an unhandled/exceptional case -- RG
@@ -865,12 +904,13 @@ let disposition_cases =
a plain [Feast]-status [Class1] loser can never reach [Commemorate] at
all in this ruleset (RG 95 routes it to [Transfer] instead), so no
further row for (b) is added here -- see the task report. Category (f),
- "of the Major Rogations, in Mass", has no row at all: no candidate this
- codebase can currently construct represents one (see [privilege_of]'s own
- comment on (f)) -- the negative row below proves the one slug this engine
- DOES compute that could be mistaken for it (the Minor Rogations) is
- correctly NOT conflated with it, which is the strongest claim available
- without inventing an unfounded slug convention. *)
+ "of the Major Litanies, in Mass" -- NOW LIVE (ef-major-litanies task):
+ [PE.major_litanies_slug]'s own data/ef/adjustments.sexp entry is the
+ real candidate; the positive row below is added alongside the existing
+ negative one, which still proves the one slug this engine ALSO computes
+ that could be mistaken for it (the Minor Rogations, RG 87 -- a
+ different observance RG 109(f) does not name) is correctly NOT
+ conflated with it. *)
let privilege_cases =
[ (* (a) RG 109(a) (§4): "of a Sunday". [an_ordinary_sunday] is Class2,
not Class1, not within the Nativity octave, not an Ember day, not a
@@ -960,6 +1000,26 @@ let privilege_cases =
cand "ef-nativity",
of_temporal (off (-39)),
"Commemorate(Privileged)" );
+ (* (f) RG 109(f) (§4; Caput XVI "De Commemorationibus"): "de Litaniis
+ maioribus, in Missa" -- ef-major-litanies task, NEW. [rank] is
+ DELIBERATELY [Class4], not [cand]'s own [Class1] default: category
+ (b) above ("of a I-class day") fires on [rank = Class1] alone and
+ is checked BEFORE (f) in [privilege_of]'s own branch order, so a
+ [Class1] row here would reach [Privileged] via (b) regardless of
+ whether (f) itself is even wired -- proving nothing about (f)
+ specifically (the exact "test day that is both [X] and [Y] proves
+ nothing about either" hazard this table's own header warns about,
+ worked for the FIRST time on this axis rather than Sunday-vs-
+ I-class). [Class4] (data/ef/adjustments.sexp's own honestly-flagged
+ placeholder rank, chosen for exactly this reason) rules out (b),
+ and the slug is neither a Sunday, within the Nativity octave, an
+ Ember day, nor an Advent/Lent/Passiontide feria -- (f) is this
+ row's only route to [Privileged], the real proof. *)
+ ( "(f) the Major Litanies commemoration is privileged (RG109(f))",
+ cand "ef-nativity",
+ cand ~origin:P.Sanctoral ~status:Cel.Commemoration_only ~rank:V.Class4 ~layer:PE.universal_layer
+ PE.major_litanies_slug,
+ "Commemorate(Privileged)" );
(* Negative, RG 109(f)'s own boundary: the Minor Litanies/Rogations
(Monday/Tuesday before Ascension, RG 87 -- [Temporal_ef.temporal]
DOES compute these, unlike the Major Litanies RG 109(f) actually
@@ -2006,6 +2066,49 @@ let test_transfer_target_does_not_raise_at_domain_ceiling () =
true
(D.compare target (mk 9999 12 31) > 0)
+(* RG 80 (ef-major-litanies task, NEW) -- {!PE.major_litanies_slug}'s own
+ citation has the full text. [occupant_always_blocking] is deliberately
+ PATHOLOGICAL (every day reports I-class, forever) -- for every OTHER
+ candidate this would send [search_from] to its own 400-day structural
+ ceiling ({!test_transfer_target_terminates_under_pathological_occupant}
+ above proves exactly that shape). Using it here is the mutation proof
+ this branch's own comment promises ("running search_from here would be
+ ACTIVELY WRONG"): if the Litanies' own early-return branch were ever
+ deleted or bypassed, this test would immediately land somewhere near
+ [origin + 1000], not Easter+2, and fail loudly -- a MUCH stronger
+ witness than a cooperative occupant could give, which would pass either
+ way by accident (Easter+2 is itself never blocking under a realistic
+ occupant, so a real [Temporal_ef.temporal] could not distinguish "no
+ search happened" from "a search happened and immediately succeeded"). *)
+let test_transfer_target_major_litanies_easter_sunday_shape () =
+ let easter_2038 = Comp.gregorian_easter 2038 in
+ Alcotest.(check string) "2038: Easter Sunday IS 25 April (this file's own worked example)" "2038-04-25"
+ (D.to_iso8601 easter_2038);
+ let origin = easter_2038 in
+ let c =
+ cand ~origin:P.Sanctoral ~status:Cel.Commemoration_only ~rank:V.Class4 ~layer:PE.universal_layer
+ PE.major_litanies_slug
+ in
+ let target = PE.transfer_target c origin occupant_always_blocking in
+ Alcotest.(check string) "lands on Easter+2 regardless of the pathological occupant (no RG96 search at all)"
+ (D.to_iso8601 (D.add_days easter_2038 2)) (D.to_iso8601 target);
+ Alcotest.(check bool) "strictly after origin (rite.mli's own obligation)" true (D.compare target origin > 0)
+
+let test_transfer_target_major_litanies_easter_monday_shape () =
+ let easter_2011 = Comp.gregorian_easter 2011 in
+ Alcotest.(check string) "2011: Easter Sunday is 24 April, so 25 April is Easter Monday" "2011-04-24"
+ (D.to_iso8601 easter_2011);
+ let origin = D.add_days easter_2011 1 (* 25 April 2011, Easter Monday *) in
+ let c =
+ cand ~origin:P.Sanctoral ~status:Cel.Commemoration_only ~rank:V.Class4 ~layer:PE.universal_layer
+ PE.major_litanies_slug
+ in
+ let target = PE.transfer_target c origin occupant_always_blocking in
+ Alcotest.(check string) "ALSO lands on Easter+2 (not Easter+3 -- both RG80 trigger shapes converge on the \
+ SAME offset), regardless of the pathological occupant"
+ (D.to_iso8601 (D.add_days easter_2011 2)) (D.to_iso8601 target);
+ Alcotest.(check bool) "strictly after origin (rite.mli's own obligation)" true (D.compare target origin > 0)
+
let suite =
( "Precedence_ef",
@@ -2098,4 +2201,11 @@ let suite =
Alcotest.test_case "transfer_target: terminates and stays forward under a pathological occupant"
`Quick test_transfer_target_terminates_under_pathological_occupant;
Alcotest.test_case "transfer_target: does not raise probing past the domain ceiling" `Quick
- test_transfer_target_does_not_raise_at_domain_ceiling ] )
+ test_transfer_target_does_not_raise_at_domain_ceiling;
+ Alcotest.test_case
+ "transfer_target: RG80, Easter-Sunday shape -- lands on Easter+2 with NO search, even under a \
+ pathological occupant"
+ `Quick test_transfer_target_major_litanies_easter_sunday_shape;
+ Alcotest.test_case
+ "transfer_target: RG80, Easter-Monday shape -- ALSO lands on Easter+2, not Easter+3" `Quick
+ test_transfer_target_major_litanies_easter_monday_shape ] )