diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-13 20:15:42 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-13 20:15:42 +0200 |
| commit | 84333a8c74ddb3988ad88398632ca5e1c7788e56 (patch) | |
| tree | 08b998e72818752dad163343c98f70a78243e33e /test/test_precedence_ef.ml | |
| parent | 3364e23fc49dc5b49576a97315326de030376e31 (diff) | |
| download | colitur-84333a8c74ddb3988ad88398632ca5e1c7788e56.tar.gz colitur-84333a8c74ddb3988ad88398632ca5e1c7788e56.zip | |
test(ef): commemoration, transfer, and privilege coverage for the Major Litanies
test_precedence_ef.ml: a privilege_cases row for RG109(f), deliberately
rank Class4 so it cannot pass via the pre-existing "of a I-class day"
branch by accident. Three disposition_cases rows: the two RG80 trigger
shapes (Transfer, not Commemorate) and a synthetic third row proving the
winner-slug guard is specific to the two named trigger days, not "any
I-class winner". Two transfer_target unit tests, both using a pathological
always-blocking occupant to prove no RG96 search runs at all for this
candidate -- a much stronger witness than a cooperative occupant, which
could pass by accident.
test_golden.ml: three new pinned tests through the real data pipeline --
the ordinary case (2026-04-25, matches the oracle's own M5 date), the four
Sunday-displacement years in 2005-2050 (2010, 2021, 2027, 2032, RG111(b)),
and the Easter-Monday transfer shape (2011, complementing the
Easter-Sunday shape already pinned by the existing 1666/2038 Easter-extreme
tests, now widened to include the transfer and its target).
test_rite_ef.ml: the existing "no transfer lands inside the Easter octave"
property gets a named, cited exemption for the Major Litanies (RG80's own
deliberate exception), plus a positive companion test asserting the
exemption is not vacuous (exactly two landings in 2005-2050, both
Easter+2). That companion test was written but never registered in its
own suite list -- caught while mutation-testing the transfer (a mutation
that should have failed it passed silently); fixed by registering it.
Mutation-tested, each of the three parts separately (recorded in the
task's own report): moving the data entity off 25 April fails 7 tests
(golden + oracle only -- zero unit tests, since they build synthetic
candidates); corrupting the transfer's winner-slug guard fails 6 (the two
disposition_cases rows, 3 golden pins, and the newly-registered
transfer-count test); flipping the privilege to Ordinary fails 9
(privilege_cases, the disposition SYNTHETIC row, the oracle's count pin,
5 golden pins, and the exhaustive Validate property sweep).
Diffstat (limited to 'test/test_precedence_ef.ml')
| -rw-r--r-- | test/test_precedence_ef.ml | 124 |
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 ] ) |
