From 2f6d25aff88b4c76c61e36889f1c017b3cc8faee Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 26 Aug 2026 23:40:17 +0200 Subject: fix(of): anticipate St Joseph onto 18 March per Normae n. 56(f) W1: when 19 March (St Joseph) falls on Palm Sunday, colitur sent him forward to Easter+9 instead of anticipating the solemnity backward to 18 March, the one rule in the whole Normae transfer machinery that names an earlier date. Live in 16 of 1583-2100 (1595, 1606, 1617, 1690, 1758, 1769, 1780, 1815, 1826, 1837, 1967, 1978, 1989, 2062, 2073, 2084). Blocked on a kernel contract: Rite.t.transfer_target required its result be strictly later than the impeded date, an obligation argued purely from the EF's RG 96. Traced against Calendar's actual placement pass rather than assumed unsafe: the round loop re-resolves the whole year fresh every round, and its two safety nets (~start/~stop; the round-count guard) both test the target's own value with no comparison against origin, so a bounded backward jump converges the same way a bounded forward one does. The one requirement that stays load-bearing is target <> origin: Precedence.resolve never deduplicates by slug, so a candidate returning its own argument unchanged would collide with itself in the same round's contest. Relaxed the obligation accordingly (rite.mli) and added the fourth transfer_target branch in Precedence_of, ahead of the existing three (Precedence_of.transfer_target, Rule 0). calendar.ml needed no logic change, only two comments that asserted "every genuine transfer moves forward" as a blanket fact. Unpinned the two tests that asserted the old wrong (forward) behaviour and replaced them with assertions of the correct one, plus a new direct unit test of the backward branch across two independent years. EF output is untouched: data/ef/ and lib/rites/rite_ef/ carry no diff, and colitur day/readings for 2026, 1583 and 9999 are byte-identical against a build of the prior commit. OF's own 2005-2050 window carries none of the 16 affected years and shows zero unexpected diffs; the full 1583-9999 domain still reaches a fixed point under the exhaustive sweep. --- lib/kernel/rite.mli | 82 +++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 64 insertions(+), 18 deletions(-) (limited to 'lib/kernel/rite.mli') diff --git a/lib/kernel/rite.mli b/lib/kernel/rite.mli index ec850f8..b0ba7ac 100644 --- a/lib/kernel/rite.mli +++ b/lib/kernel/rite.mli @@ -75,24 +75,70 @@ type ('s, 'r) t = { just to answer "what sits here". OBLIGATIONS (not enforced by the type, and {!Calendar}'s own - termination argument depends on both): the result must be - {b strictly later} than the [Date.t] argument (the date the - candidate was impeded on) -- {!Calendar}'s placement pass treats - [target = origin] or [target < origin] as a legitimate placement, - not an error, so a rite whose search can stand still or go - backward would silently loop candidates in place or resurrect an - already-superseded occupant rather than failing loudly. The call - must also {b terminate} on its own: {!Calendar}'s round guard - (calendar.ml's [max_transfer_rounds]) bounds how many ROUNDS the - whole-year placement pass takes, which is a distinct, outer thing - from whatever internal search a single call to this function runs - -- an implementation that walks forward day by day looking for an - admissible date, without its own bound, can hang the caller - outright on a rite/data shape it does not handle, never reaching - the round guard at all. See rite_ef/precedence_ef.ml's - [transfer_target] for a concrete termination argument (a - structural step bound, not an appeal to the real calendar's own - structure). *) + termination argument depends on both): the result must {b differ + from} the [Date.t] argument (the date the candidate was impeded + on) -- {!Calendar}'s placement pass treats [target = origin] as a + legitimate placement, not an error, and {!Precedence.resolve} + itself never deduplicates by slug, so a rite that can stand still + would hand it the SAME candidate twice at the SAME date in the + SAME contest (once via {!Layer.on_date}'s permanent natural + entry, once via the injection this module's placement pass adds) + -- a genuine self-collision (the candidate disposed of as both + [winner] and [loser] against itself), not merely a docstring + worry: reachable the moment any rite returns its argument + unchanged. The call must also {b terminate} on its own: + {!Calendar}'s round guard (calendar.ml's [max_transfer_rounds]) + bounds how many ROUNDS the whole-year placement pass takes, which + is a distinct, outer thing from whatever internal search a single + call to this function runs -- an implementation that walks day by + day (in EITHER direction) looking for an admissible date, without + its own bound, can hang the caller outright on a rite/data shape + it does not handle, never reaching the round guard at all. See + rite_ef/precedence_ef.ml's [transfer_target] for a concrete + termination argument (a structural step bound, not an appeal to + the real calendar's own structure). + + {b EARLIER targets are permitted} (CORRECTED, + [of-normae-56f]/W1, 2026-08-26: this obligation previously read + "strictly later", full stop, and warned that an earlier target + "would silently loop candidates in place or resurrect an + already-superseded occupant rather than failing loudly" -- traced + against the placement pass actually implemented, not merely + against this comment's own prior claim, and found to overstate + the risk). {!Calendar}'s round loop re-resolves the {b entire} + year fresh from the currently-settled [assignment] every round + (never patched incrementally), and its two safety nets -- + [~start]/[~stop] catching a target outside the liturgical year, + and [max_transfer_rounds] catching non-convergence -- both test + the target's value directly ([target < start || target > stop]; + round count) with no comparison against [origin] anywhere, so + neither depends on which side of [origin] the target falls. + "Resurrecting a superseded occupant" cannot occur either: a day's + occupant is decided fresh each round by the same RG 91/Tabula + contest every other day is, so a backward-placed candidate either + wins that contest or is itself deferred and re-targeted like any + other loser -- there is no stale state to resurrect FROM. A + candidate's own permanent loss at its structural origin is + rediscovered every round regardless of target direction and is + filtered as stale under the identical rule either way (actionable + only if never yet assigned, or if the sighting is at the + candidate's OWN current target -- calendar.ml's [place_transfers], + the [deferred] filter's own comment). + + This is a general property of the mechanism, not a special case + carved out for one rite: it holds for ANY single call that + returns a date [<> origin] and terminates on its own, per the two + obligations above. What it does {b not} license is assuming an + UNBOUNDED backward search is safe merely because a bounded one is + -- the termination obligation still falls entirely on the rite, + exactly as it always did for a forward search. The safest shape, + and the only one exercised so far, is a CONSTANT one-shot + displacement for a specifically-named collision (no internal + search at all, hence trivially terminating) -- see + rite_of/precedence_of.ml's [transfer_target] (Normae n. 56(f), St + Joseph anticipated backward onto Palm Sunday) for the concrete + worked example, the same role rite_ef/precedence_ef.ml's own + [transfer_target] plays for a bounded FORWARD search above. *) readings : observed:'r Celebration.t -> temporal:('s, 'r) Temporal.t -> -- cgit v1.3