From 7c3964be29a8902ec6fa3965a67586483313dc4e Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Thu, 13 Aug 2026 20:15:14 +0200 Subject: fix(kernel): a transferred candidate can settle as a commemoration, not only as observed Calendar.build_day's `unresolved` check decided whether a Transfer-disposed candidate had genuinely settled at its target by checking only whether it became that day's own `observed` celebration. That was correct for every prior use of Precedence.Transfer: a losing FEAST, which RG-96-style rules guarantee an unblocked target to win outright once it arrives. It is not correct in general. A rite's rules are free to dispose a Celebration.status = Commemoration_only candidate as Transfer too (the EF Major Litanies, RG 80, do exactly this) -- and such a candidate can never become `observed` anywhere, by the same status that makes it eligible to transfer in the first place. The old check mislabelled a cleanly-settled transfer of that shape as "did not converge" (a hardcoded string, not a real read of the placement pass's own convergence) and double-counted it in Validate's own duplicated-sighting check. Replaced with `settled_at`, which re-resolves the target date and accepts either `observed` or membership in that day's own admitted commemorations. A strict superset of the old check -- every existing use (a transferred feast winning its target) is unaffected -- and stays rite-agnostic: it reads only Precedence.resolution's existing fields, no EF-specific knowledge added to the kernel. Found by the exhaustive property sweep (COLITUR_EXHAUSTIVE_SWEEP=1) the moment a rite first produced this shape, not anticipated in advance. --- lib/kernel/calendar.ml | 45 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 40 insertions(+), 5 deletions(-) (limited to 'lib/kernel/calendar.ml') diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index 5d3572c..27e564f 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -304,14 +304,49 @@ let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.by_date) day it landed and [transferred_out] here, not via [omitted] too -- double-booking it in both would fail Task 12's "appears exactly once" reading of this day alone. *) + (* Whether a transferred/injected candidate is genuinely accounted for at + its assigned target -- true if it won the day outright there (every + [Transfer]-disposed candidate this kernel produced before a rite could + transfer a [Celebration.status = Commemoration_only] one: a losing + FEAST, which RG 96's own "next day not I or II class" guarantees an + unblocked day to win once it arrives -- [occupant_of] alone answered + this), OR if it survives at the target as one of the day's own admitted + COMMEMORATIONS instead (a shape [place_transfers] itself never used to + produce, because nothing before could dispose a [Commemoration_only] + candidate as [Transfer] -- {!Precedence.resolve} holds such a candidate + out of the band contest entirely, so it can never win a day outright, + only ever be commemorated on one; a rite is nonetheless free to + [Transfer] one to a named date, e.g. RG 80's Major Litanies, RG 81's + own "nihil fit in Officio" making [observed] structurally impossible + for it anywhere). [occupant_of] alone under-reports this second shape + as unsettled, which previously had no live witness to catch it: a + transferred candidate that only ever becomes a commemoration, never the + day's own office, was mislabelled here with [unconverged_reason] (a + hardcoded string, not a true read of the placement pass's own + convergence -- {!place_transfers} itself had already reached a fixed + point) and double-counted by {!Validate}'s own "duplicated" check + (sighted once in [omitted] here under that wrong label, and correctly + again in [commemorations] at its target) -- found by this kernel's own + exhaustive property sweep once a rite (Rite_ef, RG 80) first produced + this shape, not guessed at in advance. Kept rite-agnostic: nothing here + reads anything EF-specific, only {!Precedence.resolution}'s own + [observed]/[commemorations] fields, the same two channels + {!Liturgical_day.t} already promises never to lose. *) + let settled_at target slug = + let _, _, target_resolution = resolve_with_injected rite idx injected target in + let matches (c : 'r Precedence.candidate) = + Slug.equal c.Precedence.cel.Celebration.slug slug + in + matches target_resolution.Precedence.observed + || List.exists (fun (c, _) -> matches c) target_resolution.Precedence.commemorations + in let unresolved c = - let slug = Slug.to_string c.Precedence.cel.Celebration.slug in - if Hashtbl.mem out_of_range slug then true + let slug = c.Precedence.cel.Celebration.slug in + if Hashtbl.mem out_of_range (Slug.to_string slug) then true else - match Hashtbl.find_opt assignment slug with + match Hashtbl.find_opt assignment (Slug.to_string slug) with | None -> true - | Some (_, target) -> - not (Slug.equal (occupant_of rite idx injected target).Celebration.slug c.Precedence.cel.Celebration.slug) + | Some (_, target) -> not (settled_at target slug) in let reason_for c = if Hashtbl.mem out_of_range (Slug.to_string c.Precedence.cel.Celebration.slug) then -- cgit v1.3