aboutsummaryrefslogtreecommitdiff
path: root/lib/rites/rite_ef
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 01:16:22 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-12 01:16:22 +0200
commit94fc488cc9c6b4a050d90c4250f6e166b40088e7 (patch)
tree18f68c393a704c225c0124f6c9a30bdd96e444ae /lib/rites/rite_ef
parent9725195fc4a1050ded151854f6653459dacc35b0 (diff)
downloadcolitur-94fc488cc9c6b4a050d90c4250f6e166b40088e7.tar.gz
colitur-94fc488cc9c6b4a050d90c4250f6e166b40088e7.zip
rite(ef): clamp the RG96 search at the domain ceiling
search_from could walk up to 400 days past origin before Calendar's own ~start ~stop clamp is ever consulted, and nothing stopped it probing occupant on a date past 31 December 9999 -- occupant chains through the real EF rite's temporal, which calls Computus.gregorian_easter, not total outside 1583..9999 (it Date.makes and failwiths on Error). Not reachable with the shipped sanctoral data alone, but reachable through the project's own primary extension path: an overlay adding an I-class feast on 25 December leaves nothing but Class2 Nativity-octave days for the rest of civil year 9999, so the unguarded search reached 1 January of year 10000 and crashed there with 'computus: year 10000 out of range 1583..9999'. 9999 is an in-range year and the kernel's contract is 'never raises on in-range input'. search_from now also stops, without probing occupant again, once it passes Date's own domain ceiling -- the same 'return a finite date, let Calendar's own out-of-range handling record it, never pretend to have found something admissible' contract the existing step-count guard already follows. Two new tests, both mutation-verified to actually reproduce the crash when the guard is removed (see the task report): a precedence_ef.ml unit test using the real Temporal_ef.temporal as occupant (a synthetic occupant can never discriminate this, since it never calls Computus itself), and a Calendar-level integration test reproducing the exact overlay-based scenario the review found.
Diffstat (limited to 'lib/rites/rite_ef')
-rw-r--r--lib/rites/rite_ef/precedence_ef.ml35
-rw-r--r--lib/rites/rite_ef/precedence_ef.mli11
2 files changed, 36 insertions, 10 deletions
diff --git a/lib/rites/rite_ef/precedence_ef.ml b/lib/rites/rite_ef/precedence_ef.ml
index e1c13d1..b9b1731 100644
--- a/lib/rites/rite_ef/precedence_ef.ml
+++ b/lib/rites/rite_ef/precedence_ef.ml
@@ -573,6 +573,27 @@ let annunciation_slug = "annunciation-of-the-blessed-virgin-mary"
than hanging the CLI. *)
let max_search_days = 400
+(* The domain's own ceiling ({!Date.make}'s documented 1583..9999 bound,
+ also duplicated by calendar.ml's own [domain_max_date] for the same
+ reason: neither module exposes it to the other, and this is a three-line
+ constant, not worth a new signature just to share it). [search_from]
+ below must never call [occupant] on a date past this: [occupant] chains
+ through the rite's own [temporal] (calendar.ml's [resolve_with_injected]),
+ which for the real EF rite calls [Computus.gregorian_easter], which is
+ NOT total outside 1583..9999 -- it constructs a [Date.t] via [Date.make]
+ and [failwith]s on [Error]. [Date.add_days] itself has no such limit (it
+ is documented "unbounded total arithmetic"), so [search_from] CAN walk
+ [d] past 31 December 9999 without raising by itself -- the raise would
+ only happen on the NEXT [occupant d] call, which is exactly the bug this
+ guards against: an I-class feast impeded late enough in civil year 9999
+ that every remaining day of the year is also I or II class (reachable
+ through the project's own overlay mechanism, confirmed by review: an
+ Add-ed I-class feast on 25 December leaves only Class2 Nativity-octave
+ days for the rest of 9999, so the unguarded walk reached 1 January 10000
+ and crashed there). *)
+let domain_max_date =
+ match Date.make ~year:9999 ~month:12 ~day:31 with Ok d -> d | Error e -> failwith e
+
(* Walks forward from [d], returning the first date [occupant] reports as
NOT [is_blocking]. [steps] is a strictly increasing structural bound on
the recursion, capped at [max_search_days]: the function decreases
@@ -581,17 +602,19 @@ let max_search_days = 400
found), so THIS loop terminates by construction, regardless of what
[occupant] reports -- it does not rely on the real EF calendar's own
structure to guarantee termination the way the comment above explains
- why the bound is never actually reached in practice. If the bound is
- reached, the last date visited is returned WITHOUT probing [occupant]
- again -- one more finite (not necessarily admissible) date, not a
- further search -- because the val the caller ([transfer_target]) is
- still owed is "a date", never an exception; {!Calendar}'s own
+ why the bound is never actually reached in practice. Also stops, without
+ calling [occupant] again, once [d] passes {!domain_max_date} -- see that
+ constant's own comment for why probing [occupant] beyond it can raise.
+ Either way the last date visited is returned WITHOUT a further
+ [occupant] probe -- one more finite (not necessarily admissible) date,
+ not a further search -- because the value the caller ([transfer_target])
+ is still owed is "a date", never an exception; {!Calendar}'s own
[~start ~stop] bound (calendar.ml's [place_transfers]) is what turns an
implausible non-terminating real search into a recorded [omitted], not
this function pretending to have found something admissible. *)
let rec search_from (occupant : Date.t -> Vocab_ef.rank Celebration.t) (steps : int) (d : Date.t) :
Date.t =
- if steps >= max_search_days then d
+ if steps >= max_search_days || Date.compare d domain_max_date > 0 then d
else if is_blocking (occupant d).Celebration.rank then search_from occupant (steps + 1) (Date.add_days d 1)
else d
diff --git a/lib/rites/rite_ef/precedence_ef.mli b/lib/rites/rite_ef/precedence_ef.mli
index d06b058..7318ccd 100644
--- a/lib/rites/rite_ef/precedence_ef.mli
+++ b/lib/rites/rite_ef/precedence_ef.mli
@@ -199,10 +199,13 @@ val annunciation_slug : string
round guard does not itself enforce (calendar.ml's [place_transfers]
bounds ROUNDS across a whole year, not one call's internal walk).
Terminating by a structural bound on the internal walk (max 400 days,
- an engineering ceiling, not an RG citation -- see the .ml), not by an
- argument about the real 1962 calendar's own structure, so a rite/data
- shape this function has not anticipated fails FINITELY rather than
- hanging the caller. Strictly later than [origin]: the ordinary search
+ an engineering ceiling, not an RG citation -- see the .ml) AND a guard
+ at {!Colitur_kernel.Date}'s own domain ceiling (31 December 9999,
+ beyond which probing [occupant] can itself raise -- see the .ml's
+ [domain_max_date]), not by an argument about the real 1962 calendar's
+ own structure, so a rite/data shape this function has not anticipated
+ fails FINITELY rather than hanging or crashing the caller. Strictly
+ later than [origin]: the ordinary search
starts at [origin + 1] and only ever advances forward from there; the
Annunciation's own starting point is provably later than 25 March for
every representable year (Easter's documented range, register ยง0) --