From 94fc488cc9c6b4a050d90c4250f6e166b40088e7 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 01:16:22 +0200 Subject: 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. --- lib/rites/rite_ef/precedence_ef.mli | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'lib/rites/rite_ef/precedence_ef.mli') 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) -- -- cgit v1.3