diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-13 21:19:12 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-13 21:19:12 +0200 |
| commit | 2af482c7293d821f10c3bbc96b7913d658c5839c (patch) | |
| tree | 608eaf6bcc46d9dbda0a6dd3a830a5967b201bfa /lib/kernel | |
| parent | a3afb19dc6390c9e33ed5fa0ecbd6e5895e60e8d (diff) | |
| parent | 72b19098905cd609d87783f6e68311de4f1b61a0 (diff) | |
| download | colitur-2af482c7293d821f10c3bbc96b7913d658c5839c.tar.gz colitur-2af482c7293d821f10c3bbc96b7913d658c5839c.zip | |
Merge branch 'ef-major-litanies': the Major Litanies, and a kernel bug
Builds the Major Litanies (RG 80, 81, 109(f)) -- an item deferred three
times, each time on a reason that did not survive contact. Two recorded
blockers were false (a kernel signature said to be missing already
carried what was needed; Easter Monday, said to be unmarkable, occurs
exactly 8417 times in 8417 years) and a displacement estimate of ~97.7%
of years measured at 4 years in 46.
8611 days change in four shapes, zero unclassified: the commemoration
appearing on ordinary 25 Aprils, displacing St Mark's own on the four
II-class Sundays RG 111(b) governs, and relocating to the following
Tuesday in the 194 years RG 80's transfer clause fires. No day outside
25/26/27 April differs at all, and observed, rank, colour, season, week
and transferred_in are byte-identical across all 3074246 days.
The entity is a Commemoration_only sanctoral entry, which honours RG 81
structurally rather than by special case: Precedence.resolve partitions
such candidates out of the band contest, so 'nihil fit in Officio' holds
by construction, and being sanctoral-origin it can never claim RG 113's
de-Tempore first place.
And it surfaced a latent kernel bug. Calendar.build_day decided whether
a transferred candidate had settled by testing only whether it became
that day's observed celebration -- correct for every prior use, a losing
feast that wins its unblocked target, and wrong for a Commemoration_only
candidate, which can never be observed by the same status that lets it
transfer. The first fix accepted two settlement channels and the review
found a third: a candidate capped out by admit at its target. That third
case was already visible inside the task's own mutation proof, as an
undiagnosed ninth failure it had set aside.
The fix is a provable no-op in isolation: a3afb19 plus the new
calendar.ml alone, swept over every day of the domain, is byte-identical
to base.
Diffstat (limited to 'lib/kernel')
| -rw-r--r-- | lib/kernel/calendar.ml | 112 |
1 files changed, 107 insertions, 5 deletions
diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index 5d3572c..cffdf69 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -304,14 +304,116 @@ 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 under any of THREE conditions, not two + (fix round 1, ef-major-litanies task -- the first version of this + function, and this comment, claimed two, missing exactly the same + shape one channel further out than the bug it had just fixed; see + below for how that was found). + + (1) 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 used to answer this, and + still would). + + (2) 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). The FIRST version of this function + stopped here, at (1) and (2) -- {!Liturgical_day.t}'s own doc comment + promises [observed] and [commemorations] are never silently lost, and + this read as "the same two channels", which is where the "two, not + three" miscount came from: that promise is about {!Liturgical_day.t}'s + OWN five fields, not an exhaustive account of every way + {!Precedence.resolve} can dispose of a candidate at one date. + + (3) It reaches the target and is disposed there as [Omit] by + {!Precedence.rules.disposition} itself (RG 33's vigil omission, RG + 16(a)'s Sunday suppression, RG 26's IV-class-feria omission, the + Lord-vs-Lord exclusion, ...) OR is offered to + {!Precedence.rules.admit} there but capped out by an admission-count + limit RG 111 itself imposes (e.g. a Class1 day admits only ONE + privileged commemoration; a second one due the same day, or the SAME + Litanies candidate no longer privileged, loses that slot) -- both + land in the target's own [omitted], with their own accurate, + already-diagnostic reason ("omitted: yielded to a higher day" / + "omitted: admission limit reached"), and both are just as genuinely + "delivered and considered" as (1)/(2), not stuck anywhere. Missing + this third channel reproduces the EXACT ORIGINAL BUG this function was + written to fix, one level further out: a candidate settled (via (3)) + at its target was still reported [unresolved] at its ORIGIN, under + the same wrong, hardcoded [unconverged_reason] label, and + double-counted by {!Validate}'s own "duplicated" check the same way. + + Found, not merely reasoned to: fix round 1's review reproduced it two + ways. Constructively, a second privileged [Commemoration_only] entry + placed on the Litanies' own transfer target (Easter+2) that sorts + ahead of it forces the Litanies to lose {!Precedence.rules.admit}'s + own Class1 "one privileged commemoration only" cap there. And, + already present in this branch's own mutation-testing record without + being run to ground at the time: mutation 3 (this task's own report, + `privilege_of`'s RG 109(f) branch forced to [Ordinary]) makes the + transferred Litanies itself lose that SAME Class1 cap at its OWN + target -- no second candidate needed, since an [Ordinary] commemoration + has no standing at all against a [Class1] day's privileged-only + admission rule ({!Precedence_ef.admit}'s own Class1 case). That + mutation's 9th failure, the exhaustive `Validate` property sweep on a + random year, was this bug; the report noted the failure and declined + to diagnose it before reverting the mutation, which is precisely how + it survived one fix round. + + Unreachable on shipped EF data today (every `Commemoration_only` + candidate this rite's own real data carries is at most [Class3] + except the Litanies themselves, and no second privileged + commemoration can ever fall on Easter+2 -- {!Precedence_ef + .privilege_of}'s own (a)-(e) categories are all Sunday/Ember/Advent- + Lent-Passiontide/Nativity-octave shaped, none of which Easter+2 is or + can be), which is exactly why it survived this far: nothing in the + shipped calendar has ever exercised it. Fails LOUDLY (a wrong, + misleading label) rather than silently, and is fixed here rather than + left as a documented residual, since the fix is a one-line + generalisation of the same check, not new machinery. Kept + rite-agnostic: nothing here reads anything EF-specific, only + {!Precedence.resolution}'s own [observed]/[commemorations]/[omitted] + fields -- THREE of {!Precedence.resolution}'s four fields (the fourth, + [deferred], denotes a candidate that has NOT yet settled at this date, + by definition, so it is correctly never consulted here). + A SIGNAL TRADED AWAY, named because it is real (fix-round re-review): + channel (3) accepts both shapes of [omitted] -- the admission cap, and + a rite whose own [disposition] omits the candidate AT the target its + own [transfer_target] named. For the cap this is unambiguously + "settled". For the second it is a judgement: before this change that + shape produced a loud, if mislabelled, [Validate] "unconverged" + failure; now it is silent at the origin and honestly reported at the + target. The kernel cannot tell "the rite deliberately omitted it + there" from "the rite chose a bad target" without rite knowledge it + must not have, so accepting it is the right call -- but the diagnostic + it used to give up is gone. Unreachable in [Rite_ef] today: only the + Major Litanies transfer as [Commemoration_only], and RG 96's search + guarantees a transferred FEAST an unblocked target. *) + 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 + || List.exists (fun (c, _) -> matches c) target_resolution.Precedence.omitted + 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 |
