diff options
| -rw-r--r-- | CLAUDE.md | 76 | ||||
| -rw-r--r-- | lib/kernel/calendar.ml | 46 | ||||
| -rw-r--r-- | lib/kernel/rite.mli | 82 | ||||
| -rw-r--r-- | lib/rites/rite_of/precedence_of.ml | 84 | ||||
| -rw-r--r-- | lib/rites/rite_of/precedence_of.mli | 95 | ||||
| -rw-r--r-- | lib/rites/rite_of/rite_of.mli | 9 | ||||
| -rw-r--r-- | test/test_precedence_of.ml | 57 | ||||
| -rw-r--r-- | test/test_rite_of.ml | 110 |
8 files changed, 404 insertions, 155 deletions
@@ -881,6 +881,82 @@ original, distinct architectural reason. dedicated unit test alone. Full account: `.superpowers/sdd/2026-08-12-colitur-rg16a/bvm-saturday-report.md`. +10. **OF W1 — Normae n. 56(f), St Joseph anticipated onto Palm Sunday — + RESOLVED (`of-normae-56f`, 2026-08-26), and the kernel contract change + it forced.** `Rite.t.transfer_target`'s own obligation used to require + the result be **strictly later** than the impeded date, justified + purely from the EF's RG 96 (rite.mli's own comment cited it, "the same + class of item CLAUDE.md tracks under 'EF-shaped things still in + rite-agnostic kernel code'" — item 8 above). This is the FIFTH + EF-shaped kernel misfit found while building OF (after `Preface.t`, + `Mass_formulary.source`, `transfer_target`'s own strictly-later + contract, and `citation_shapes`) and the SECOND fixed rather than only + documented — `citation_shapes` was the first. + + **The rule that forced it**: *"Sollemnitas S. Ioseph, ubi est de + praecepto servanda, si cum Dominica in palmis de Passione Domini + occurrit, anticipatur sabbato praecedenti, die 18 martii"* — St Joseph + impeded by Palm Sunday is ANTICIPATED BACKWARD to the preceding + Saturday, the one clause in the whole Tabula/Normae transfer machinery + that names an earlier date, not a later one. Live in 16 of 1583–2100 + (1595, 1606, 1617, 1690, 1758, 1769, 1780, 1815, 1826, 1837, 1967, + 1978, 1989, 2062, 2073, 2084) — colitur previously sent Joseph forward + to Easter+9 instead (past the Annunciation's own Easter+8, since both + solemnities were impeded that year and collided on the same forward + target). + + **The alternative rejected**: leaving it documented-but-unimplemented + indefinitely, precedence_of.mli's own status quo before this task. No + rite-local workaround exists instead — `Calendar.place_transfers` is + the only channel that ever places a transferred candidate, so a rule + the kernel contract forbids from returning cannot be smuggled in + beside it. + + **What it actually costs**: traced against `Calendar`'s real placement + pass (calendar.ml's `place_transfers`/`year`), not assumed unsafe by + inheritance from the EF-only citation that wrote the original text. + The round loop re-resolves the WHOLE year fresh every round from the + currently-settled assignment, and its two safety nets — the + `~start`/`~stop` domain bound and `max_transfer_rounds`'s round-count + guard — both test the target's own value with no comparison against + `origin` anywhere, so a bounded backward jump converges exactly the + way a bounded forward one does, and "resurrecting a superseded + occupant" cannot occur (a day's occupant is decided fresh each round + by the same contest every other day is). The ONE requirement that + really is load-bearing: `target <> origin`, not merely `target > + origin` — `Precedence.resolve` never deduplicates by slug, so a + candidate returning its own argument unchanged would be handed to the + RG 91/Tabula contest twice in the same round, a genuine self-collision + (disposed of as both `winner` and `loser` against itself), not a + docstring worry. The relaxed obligation is `Rite.t.transfer_target`'s + new text (rite.mli); it does NOT license an unbounded backward + SEARCH as safe merely because a bounded one is proven so — the + termination obligation still falls entirely on the rite, exactly as it + always did for a forward search, and the only shape actually verified + is a CONSTANT one-shot displacement for a specifically-named collision + (`Precedence_of.transfer_target`'s own Rule 0, `Date.add_days origin + (-1)`, no internal search at all). `calendar.ml` itself needed NO + logic change — only two comments correcting a blanket "every genuine + transfer moves forward" claim that the trace showed no longer holds + literally. + + **Blast radius, measured**: EF untouched — `git diff --stat + v1.0.0..HEAD -- data/ef/` and `lib/rites/rite_ef/` both empty (the + field's TYPE is unchanged, only its doc comment; no new required + field), and `colitur day`/`colitur readings` for 2026, 1583 and 9999 + are byte-`cmp`-identical between this change and a `git worktree` + build of the commit immediately before it. OF's own 2005–2050 + differential-testing window (CLAUDE.md's own oracle range) carries + zero of the 16 affected years, and a full sweep of it shows zero + unexpected diffs either. Each affected year's own diff is exactly two + lines (18 March gains Joseph; whichever memorial or feria previously + occupied the old, wrong Easter+9 target resurfaces there instead) — + confirmed on 2062 by direct `cmp` against the pre-fix binary. The + whole domain's transfer placement still reaches a fixed point: + `Validate.run`'s "unconverged" check stayed clean across the full + 1583–9999 exhaustive sweep (`COLITUR_EXHAUSTIVE_SWEEP=1 dune test + --force`, part of `make check`). + ## How to work here - **Superpowers workflow**: `brainstorming` → `writing-plans` → `executing-plans` diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml index a1309f9..a8c4725 100644 --- a/lib/kernel/calendar.ml +++ b/lib/kernel/calendar.ml @@ -113,33 +113,43 @@ let occupant_of (rite : ('s, 'r) Rite.t) (idx : 'r Layer.index) let _, _, resolution = resolve_with_injected rite idx injected date in resolution.Precedence.observed.Precedence.cel -(* Hard guard on the placement fixed point (spec §2.4): every genuine +(* Hard guard on the placement fixed point (spec §2.4): almost every transfer moves a celebration strictly forward and the celebration set is finite, so the round below always empties [deferred] within a handful of rounds in practice (an RG 97-98 collision of N feasts on one date costs at most N-1 extra rounds -- each round resolves the winner of whatever pile-up - occurred and re-defers the rest, one fewer each time). 64 is not tuned to - that bound; it is a defensive ceiling nothing in the 1962 calendar comes - close to, so that a rite/data combination this module has not anticipated - fails as a recorded, inspectable [omitted] reason (below) instead of - hanging the CLI. *) + occurred and re-defers the rest, one fewer each time). CORRECTED + (Normae n. 56(f)/W1, 2026-08-26): "every" no longer holds literally -- a + rite MAY now return a target earlier than origin (rite.mli's own + obligation was relaxed from "strictly later" to "different"; see its + comment for the argument) -- but the bound this guard exists for does + not actually rest on direction: [~start]/[~stop] and this round count + both test the target's own value, never a comparison against [origin], + so a bounded backward jump converges the same way a bounded forward one + does. 64 is not tuned to that bound; it is a defensive ceiling nothing + in either shipped calendar comes close to, so that a rite/data + combination this module has not anticipated fails as a recorded, + inspectable [omitted] reason (below) instead of hanging the CLI. *) let max_transfer_rounds = 64 let unconverged_reason = "omitted: transfer placement did not converge within max_transfer_rounds (RG 96-98)" -(* A rite-supplied [transfer_target] is trusted to search strictly forward - (rite.mli), but nothing stops it naming a date past the end of the - liturgical year it was asked about -- e.g. an I-class feast impeded in - the last days before Advent I, whose first admissible day genuinely - falls in the following liturgical year's own territory (unproven to - occur in the real EF calendar, but not something this module can rule - out by construction). [place_transfers] never injects such a target: the - [dates] array is exactly what [year]/[build_day] walk to produce the - result, so a candidate placed outside it would be [observed]/ - [transferred_in] nowhere in the output at all -- gone, not merely - mis-filed, and silently so, contradicting [calendar.mli]'s "never - silently dropped". This reason makes that failure mode visible instead. *) +(* A rite-supplied [transfer_target] is trusted to return a date genuinely + different from its argument and to terminate on its own (rite.mli), but + nothing stops it naming a date past either end of the liturgical year it + was asked about -- e.g. an I-class feast impeded in the last days before + Advent I, whose first admissible day genuinely falls in the following + liturgical year's own territory (unproven to occur in the real EF + calendar, but not something this module can rule out by construction), + or (since Normae n. 56(f)/W1) a backward-anticipated feast impeded close + enough to the liturgical year's own opening that its target lands before + it. [place_transfers] never injects such a target: the [dates] array is + exactly what [year]/[build_day] walk to produce the result, so a + candidate placed outside it would be [observed]/[transferred_in] nowhere + in the output at all -- gone, not merely mis-filed, and silently so, + contradicting [calendar.mli]'s "never silently dropped". This reason + makes that failure mode visible instead. *) let out_of_range_reason = "omitted: transfer target falls outside the liturgical year (RG 96)" (* RG 33: "Vigilia II aut III classis penitus omittitur... vel si festum cui 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 -> diff --git a/lib/rites/rite_of/precedence_of.ml b/lib/rites/rite_of/precedence_of.ml index 0587f0a..5344374 100644 --- a/lib/rites/rite_of/precedence_of.ml +++ b/lib/rites/rite_of/precedence_of.ml @@ -300,9 +300,22 @@ let vigil_feast (_ : Vocab_of.rank Precedence.candidate) : Slug.t option = None let rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules = { band; disposition; admit; vigil_feast } -(* Normae n. 60 and Normae n. 5 together. THREE rules, in this priority order - -- n. 60's own text defers to n. 5 explicitly ("servatis iis quae n. 5 - statuuntur"), so the two are one rule set, not two competing ones. +(* Normae n. 56(f), n. 60 and n. 5 together. FOUR rules, in this priority + order -- n. 60's own text defers to n. 5 explicitly ("servatis iis quae + n. 5 statuuntur"), and n. 56(f) names the single collision it overrides + outright, so all three are one rule set, not three competing ones. + + 0. ST JOSEPH ON PALM SUNDAY (Normae n. 56(f)): "Sollemnitas S. Ioseph, + ubi est de praecepto servanda, si cum Dominica in palmis de Passione + Domini occurrit, anticipatur sabbato praecedenti, die 18 martii" -- + ANTICIPATED BACKWARD to the preceding Saturday, 18 March, the one + named exception to every other rule here searching or landing + forward. RESOLVED (of-normae-56f/W1, 2026-08-26; previously KNOWN + UNIMPLEMENTED -- see this value's own .mli for the full history, + including why it was blocked on a kernel contract change and what + that change cost). Checked first, ahead of rule 1, because it names + a more specific collision (one candidate, one date shape) than any + rule below. 1. THE ANNUNCIATION IN HOLY WEEK (Normae n. 60): "Sollemnitas vero Annuntiationis Domini, quotiescumque occurrit aliquo die Hebdomadae @@ -328,15 +341,19 @@ let rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules = whose occupant bands ABOVE 80 (entry 8 x 10). TERMINATION, which Rite.t.transfer_target requires the rite to guarantee: - the search is bounded at [max_search_days] steps AND at {!domain_max_date}, - and returns the last date visited -- never raises -- if either bound is - reached before a free day is found. That bound is STRUCTURAL -- it does - not appeal to the real calendar's own shape -- because Calendar's round - guard bounds ROUNDS, not the internal search of a single call, and an - unbounded walk would hang the caller outright before that guard was ever - consulted; the domain bound additionally prevents the walk from ever - calling [occupant] on a date {!Computus.gregorian_easter} cannot construct - (see {!domain_max_date}'s own comment). *) + rules 1-3's search is bounded at [max_search_days] steps AND at + {!domain_max_date}, and returns the last date visited -- never raises -- + if either bound is reached before a free day is found. That bound is + STRUCTURAL -- it does not appeal to the real calendar's own shape -- + because Calendar's round guard bounds ROUNDS, not the internal search of + a single call, and an unbounded walk would hang the caller outright + before that guard was ever consulted; the domain bound additionally + prevents the walk from ever calling [occupant] on a date + {!Computus.gregorian_easter} cannot construct (see {!domain_max_date}'s + own comment). Rule 0 needs no bound of its own: it runs no search at + all, computing [Date.add_days origin (-1)] directly, so it terminates + trivially -- the one shape {!Colitur_kernel.Rite.t.transfer_target}'s own + comment names as always safe regardless of direction. *) let max_search_days = 400 @@ -361,8 +378,26 @@ let max_search_days = 400 let domain_max_date = match Date.make ~year:9999 ~month:12 ~day:31 with Ok d -> d | Error e -> failwith e +(* NOTE, found while adding [st_joseph_slug] below, NOT fixed here -- + out of scope for the W1 task this touches: [annunciation_slug] does not + match the real shipped entry's own slug (data/of/calendar-2002.sexp has + "annunciation-of-the-lord", not "of-annunciation"), so Rule 1 below + never actually fires against real sanctoral data -- only against the + synthetic candidate test_precedence_of.ml's own [annunciation] builds + with the same placeholder slug. Whether this is output-visible on real + data was not established either way here; Rule 3's general forward + search is a plausible fallback that could reach the identical Easter+8 + target by coincidence in the one case tested + ([test_annunciation_in_easter_octave]'s own comment says as much for a + collision NOT in Holy Week), but that is not the same claim as "the two + rules always agree", and this was not checked for Holy Week itself. *) let annunciation_slug = "of-annunciation" +(* The real shipped slug (data/of/calendar-2002.sexp) -- St Joseph's own + Rule 0 below is matched against the actual sanctoral entry, not a + placeholder, precisely because the note above exists. *) +let st_joseph_slug = "joseph-husband-of-the-blessed-virgin-mary" + (* Tabula entries 1-8, scaled: a day is FREE to receive a transfer when its occupant bands strictly above entry 8. *) let entry_8_band = 80 @@ -373,9 +408,27 @@ let transfer_target (c : Vocab_of.rank Precedence.candidate) (origin : Date.t) let easter = Computus.gregorian_easter year in let offset d = Date.to_rata d - Date.to_rata easter in let is_holy_week d = offset d >= -7 && offset d <= -1 in - (* Rule 1. *) - if Slug.to_string c.cel.slug = annunciation_slug && is_holy_week origin then - Date.add_days easter 8 + let is_palm_sunday d = offset d = -7 in + (* Rule 0 (Normae n. 56(f)): "Sollemnitas S. Ioseph, ubi est de praecepto + servanda, si cum Dominica in palmis de Passione Domini occurrit, + anticipatur sabbato praecedenti, die 18 martii" -- St Joseph, impeded + by Palm Sunday, is ANTICIPATED BACKWARD to the preceding Saturday, not + carried forward like every other rule here. A fixed one-day + displacement, not a search: [origin] is Palm Sunday itself whenever + this fires (a Sunday, by construction), so "the preceding Saturday" + and "the day before [origin]" are the same date, and computing it this + way -- rather than via [offset]/[easter] -- makes that identity exact + rather than incidental. This is the rite.mli-documented EARLIER-target + shape (rite.mli's own [transfer_target] comment): a single named + collision, no internal search, hence trivially terminating on its own. + Checked ahead of Rules 1-3, most-specific first, the same order this + whole function already keeps. *) + if Slug.to_string c.cel.slug = st_joseph_slug && is_palm_sunday origin then + Date.add_days origin (-1) + else if + (* Rule 1. *) + Slug.to_string c.cel.slug = annunciation_slug && is_holy_week origin + then Date.add_days easter 8 else let season_of d = (Temporal_of.temporal d).Temporal.season in let privileged_sunday d = @@ -384,7 +437,6 @@ let transfer_target (c : Vocab_of.rank Precedence.candidate) (origin : Date.t) | Vocab_of.Advent | Vocab_of.Lent | Vocab_of.Easter -> true | Vocab_of.Christmas | Vocab_of.Ordinary_time -> false in - let is_palm_sunday d = offset d = -7 in let is_easter_sunday d = offset d = 0 in (* Rule 2. *) if diff --git a/lib/rites/rite_of/precedence_of.mli b/lib/rites/rite_of/precedence_of.mli index 4ef81a5..1b9457b 100644 --- a/lib/rites/rite_of/precedence_of.mli +++ b/lib/rites/rite_of/precedence_of.mli @@ -90,6 +90,9 @@ val rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules Normae n. 60 and Normae n. 5 together -- n. 60 defers to n. 5 explicitly ("servatis iis quae n. 5 statuuntur"), so they are one rule set: + - St Joseph, impeded by falling on Palm Sunday, is ANTICIPATED BACKWARD to + the preceding Saturday, 18 March (n. 56(f), a fixed one-day + displacement, checked first as the most specific collision); - the Annunciation falling anywhere in Holy Week goes to Easter + 8, the Monday after the Second Sunday of Easter (n. 60, a fixed destination); - any other solemnity falling on a Sunday of Advent, Lent or Easter goes to @@ -97,52 +100,62 @@ val rules : (Vocab_of.season, Vocab_of.rank) Precedence.rules which n. 5 excludes and which fall through to the general rule; - otherwise, the nearest later day free of Tabula entries 1-8 (n. 60). - KNOWN UNIMPLEMENTED FOURTH RULE, recorded rather than built (final review - Important #5, ledger ruling R9): Normae n. 56(f) -- - "Sollemnitas S. Ioseph, ubi est de praecepto servanda, si cum Dominica in - palmis de Passione Domini occurrit, anticipatur sabbato praecedenti, die - 18 martii" -- St Joseph, where his solemnity is of precept, falling on - Palm Sunday is ANTICIPATED (a BACKWARD transfer) to the preceding - Saturday, 18 March, not carried forward like every rule above. It is - conditional ("ubi est de praecepto servanda") and the following sentence - gives Episcopal Conferences discretion where it is not, so the universal - calendar legitimately not implementing it is defensible; not citing it at - all was not, hence this note. + FOURTH RULE RESOLVED ([of-normae-56f]/W1, 2026-08-26; previously KNOWN + UNIMPLEMENTED here, final review Important #5, ledger ruling R9). Normae + n. 56(f): "Sollemnitas S. Ioseph, ubi est de praecepto servanda, si cum + Dominica in palmis de Passione Domini occurrit, anticipatur sabbato + praecedenti, die 18 martii" -- St Joseph, where his solemnity is of + precept, falling on Palm Sunday is ANTICIPATED (a BACKWARD transfer) to + the preceding Saturday, 18 March, not carried forward like the other + three rules. It is conditional ("ubi est de praecepto servanda") and the + following sentence gives Episcopal Conferences discretion where it is + not; the universal calendar implements the unconditional reading (the + same discipline every other rule here already applies to a Normae + clause with a conference-discretion escape hatch). - CORRECTED: this note previously said "No sanctoral data exists yet - (Phase 3), so nothing is WRONG today" and located the trigger at - "25 March co-occurring with Palm Sunday". Both are now false and were - already wrong about the date: St Joseph is 19 March, not 25 March (25 - March is the Annunciation, a separate solemnity with its own Holy-Week - handling). Phase 3 shipped sanctoral data on this same branch - (data/of/calendar-2002.sexp), so the defect this note warns about is now - LIVE: 19 March coincides with Palm Sunday in 16 of the 1583-2100 years - (e.g. 2062), and St Joseph lands forward at Easter+9 via rule 3 instead - of anticipated backward to 18 March. Pinned, not silently wrong: see - test_rite_of.ml's [test_joseph_palm_sunday_2062_known_wrong_forward_transfer] - (2062, both grade and identity) and allow-list entries L8/L9 - (data/of/expected-divergences-litcal.sexp, 2035-03-17, a second, distinct - year witnessing the same limitation). + HISTORY (kept for the record; the defect is fixed, not merely + documented, as of this revision). 19 March coincides with Palm Sunday + in 16 of the 1583-2100 years (e.g. 2062), and before this fix St Joseph + landed forward at Easter+9 via rule 3 instead of anticipated backward + to 18 March -- pinned on that shape until this revision, in + test_rite_of.ml's own now-renamed/re-asserted test (previously + [test_joseph_palm_sunday_2062_known_wrong_forward_transfer]; see that + file for its corrected form) and allow-list entries L8/L9 + (data/of/expected-divergences-litcal.sexp) -- L8/L9 name a DIFFERENT + year, 2035-03-17, where St Joseph is impeded by Holy Monday rather than + coinciding with Palm Sunday itself, so n. 56(f)'s own trigger does not + apply there; that instance of the general rule's forward-only reach is + untouched by this fix and remains open on its own terms. - Implementing it would need either a kernel signature change (out of - scope for this rite module and forbidden by this fix wave) or a - deliberate violation of a documented obligation {!Colitur_kernel.Calendar} - depends on: n. 60's own text is "ad proximiorem diem transferatur" -- - the NEAREST day, not "proximiorem diem SEQUENTEM" (the nearest - FOLLOWING one) -- yet every branch above only ever searches or lands - forward. The strictly-LATER reading is not this rite's own choice; it is - imposed by {!Colitur_kernel.Rite.t.transfer_target}'s own contract - (rite.mli:77-84), which is justified there purely by the EF's RG 96. That - is EF-shaped vocabulary constraining rite-agnostic kernel code -- the same - class of item CLAUDE.md already tracks under "EF-shaped things still in - rite-agnostic kernel code" -- so a real fix has to start at the kernel - field, not in this module. + What unblocked it: {!Colitur_kernel.Rite.t.transfer_target}'s own + contract (rite.mli) used to require the result be STRICTLY LATER than + [origin] -- an obligation argued there purely from the EF's RG 96, i.e. + EF-shaped vocabulary constraining rite-agnostic kernel code, the same + class of item CLAUDE.md tracks under "EF-shaped things still in + rite-agnostic kernel code". Traced against {!Colitur_kernel.Calendar}'s + actual placement pass (calendar.ml's [place_transfers]/[year], not + against the obligation's own prior wording) rather than assumed unsafe: + the round loop re-resolves the whole year fresh every round with no + comparison against [origin] anywhere in its two safety nets ([~start]/ + [~stop]; the round-count guard), so a target earlier than [origin] is + handled identically to a later one. The kernel contract was relaxed + (rite.mli, [transfer_target]'s own comment carries the full argument) + from "strictly later" to "different from origin" -- the one requirement + the trace showed is still load-bearing (a same-day target would hand + {!Colitur_kernel.Precedence.resolve} the same candidate twice, which it + does not deduplicate). No change was needed in calendar.ml's actual + logic; two of its comments were corrected for accuracy (the round-guard + rationale and the out-of-range rationale both previously asserted + "every genuine transfer moves forward" as a blanket fact). Shaped to match {!Colitur_kernel.Rite.t.transfer_target} exactly so a later phase wires it with no adaptation, and honours both obligations that field - states: the result is strictly later than [origin], and the search carries - its own step bound rather than relying on {!Colitur_kernel.Calendar}'s - round guard, which bounds rounds rather than one call's internal search. + states: the result differs from [origin] (rule 0's own [Date.add_days + origin (-1)] trivially satisfies this, going backward rather than + forward), and the search carries its own step bound rather than relying + on {!Colitur_kernel.Calendar}'s round guard, which bounds rounds rather + than one call's internal search (rule 0 needs no bound at all -- it runs + no search, so it terminates trivially). Never raises. If no free day is found within 400 days, or the walk would otherwise have to probe past 31 December 9999 (past which diff --git a/lib/rites/rite_of/rite_of.mli b/lib/rites/rite_of/rite_of.mli index 8124467..e537cbd 100644 --- a/lib/rites/rite_of/rite_of.mli +++ b/lib/rites/rite_of/rite_of.mli @@ -34,10 +34,11 @@ module Lectionary_of = Lectionary_of Ordinary Time runs in two separate blocks over one liturgical year (Normae n. 43-44), so the expected run-length-compressed sequence names it twice. - - [transfer_target]: {!Precedence_of.transfer_target}, Normae n. 60/n. 5. - Known incomplete on one named date shape (Normae n. 56(f), St - Joseph's backward anticipation onto Palm Sunday) -- documented on that - value's own .mli, not repeated or silently worked around here. + - [transfer_target]: {!Precedence_of.transfer_target}, Normae n. 56(f)/ + n. 60/n. 5 (St Joseph's backward anticipation onto Palm Sunday, + resolved [of-normae-56f]/W1, 2026-08-26, together with the general + forward search) -- documented on that value's own .mli, not repeated + or silently worked around here. - [readings]: {!Lectionary_of.readings} partially applied to the caller's own [~lectionary] and {!Temporal_of.year_start} (the OF reading-cycle arithmetic's own Advent anchor) -- no [~commons] diff --git a/test/test_precedence_of.ml b/test/test_precedence_of.ml index e1af486..23c26c2 100644 --- a/test/test_precedence_of.ml +++ b/test/test_precedence_of.ml @@ -405,7 +405,13 @@ let test_annunciation_in_easter_octave () = let test_solemnity_on_a_lenten_sunday () = (* Normae n. 5: a solemnity occurring on a Sunday of Advent, Lent or Easter goes to the FOLLOWING MONDAY, not to a searched free day. 19 March 2028 - (St Joseph) is the Third Sunday of Lent. *) + (St Joseph) is the Third Sunday of Lent, not Palm Sunday -- Rule 0 + (n. 56(f)) does not fire here even with the REAL slug (see the test + right below this one for that), because its own guard is [is_palm_sunday + origin], not merely "this candidate is St Joseph". A synthetic slug is + used deliberately, to keep this test about rule 2's own generic + "solemnity on a privileged Sunday" behaviour, not about St Joseph + specifically. *) let joseph = mk ~slug:"of-joseph" ~rank:Vocab_of.Sollemnitas ~origin:Precedence.Sanctoral () in let target = @@ -413,10 +419,48 @@ let test_solemnity_on_a_lenten_sunday () = Alcotest.(check string) "St Joseph 2028 goes to the following Monday" "2028-03-20" (Date.to_iso8601 target) +(* Normae n. 56(f), Rule 0 -- the one EARLIER-target shape + {!Colitur_kernel.Rite.t.transfer_target}'s relaxed obligation now permits + (rite.mli's own comment carries the argument; W1, + [of-normae-56f], 2026-08-26). Unit-level counterpart to + test_rite_of.ml's own full-Calendar [test_joseph_palm_sunday_2062_ + anticipated_backward] -- this one calls [transfer_target] directly, the + same shape every other test in this file uses, and checks the REAL + shipped slug (unlike [test_solemnity_on_a_lenten_sunday] above, which + uses a placeholder deliberately). Two independent years, not one: 2062 + and 1978 both have Gregorian Easter = 26 March (Palm Sunday = 19 March), + confirmed directly rather than assumed. *) +let test_st_joseph_on_palm_sunday_anticipated_backward () = + let joseph = + mk ~slug:"joseph-husband-of-the-blessed-virgin-mary" ~rank:Vocab_of.Sollemnitas + ~origin:Precedence.Sanctoral () in + List.iter + (fun (palm_sunday, expected_target) -> + let origin = iso palm_sunday in + Alcotest.(check bool) + (Printf.sprintf "%s really is a Sunday (Easter = 26 March that year)" palm_sunday) + true (Date.weekday origin = Date.Sun); + let target = Rite_of.Precedence_of.transfer_target joseph origin occupant in + Alcotest.(check string) + (Printf.sprintf "St Joseph on Palm Sunday %s is anticipated BACKWARD to the preceding Saturday" + palm_sunday) + expected_target (Date.to_iso8601 target); + Alcotest.(check bool) (Printf.sprintf "%s -> earlier than origin, not later" palm_sunday) true + (Date.compare target origin < 0)) + [ ("2062-03-19", "2062-03-18"); ("1978-03-19", "1978-03-18") ] + let test_target_is_strictly_later () = - (* Rite.t.transfer_target's own stated obligation: Calendar treats - target <= origin as a legitimate placement, so a rule that can stand - still would loop candidates in place rather than fail loudly. *) + (* This is the Annunciation's OWN obligation (rules 1-3), not a claim + about {!Rite_of.Precedence_of.transfer_target} as a whole any more -- + {!Colitur_kernel.Rite.t.transfer_target}'s kernel-level obligation was + relaxed from "strictly later" to "different from origin" (W1, + [of-normae-56f], 2026-08-26; see rite.mli's own comment), precisely so + Rule 0 above could return an EARLIER target for St Joseph. The + Annunciation's own three rules are untouched by that relaxation -- + none of them was rewritten, and Calendar's placement pass still treats + [target = origin] as a legitimate (bad) placement for whichever + candidate returns it, so a rule that can stand still would still loop + in place rather than fail loudly. *) List.iter (fun s -> let d = iso s in @@ -496,7 +540,10 @@ let suite = test_annunciation_in_easter_octave; Alcotest.test_case "solemnity on a Lenten Sunday -> following Monday" `Quick test_solemnity_on_a_lenten_sunday; - Alcotest.test_case "transfer_target is always strictly later" `Quick + Alcotest.test_case + "Normae n.56(f), W1: St Joseph on Palm Sunday is anticipated backward to 18 March" `Quick + test_st_joseph_on_palm_sunday_anticipated_backward; + Alcotest.test_case "the Annunciation's own rules 1-3 are always strictly later" `Quick test_target_is_strictly_later; Alcotest.test_case "transfer_target lands free of Tabula entries 1-8" `Quick test_target_is_free_of_entries_1_to_8; diff --git a/test/test_rite_of.ml b/test/test_rite_of.ml index 5e369b8..a7d3237 100644 --- a/test/test_rite_of.ml +++ b/test/test_rite_of.ml @@ -242,39 +242,35 @@ let test_transfers_reach_a_fixed_point_2005_2050 () = let slug_of (c : V.rank Cel.t) = Slug.to_string c.Cel.slug -(* precedence_of.mli's own documented, KNOWN-UNIMPLEMENTED fourth - transfer_target rule (final review Important #5, ledger ruling R9): - Normae n. 56(f) -- St Joseph's solemnity, falling on Palm Sunday, is - ANTICIPATED BACKWARD to 18 March, not carried forward. colitur's - [transfer_target] has no backward-search branch (rite.mli's own - [transfer_target] contract requires the result be strictly LATER than - the origin -- an EF-shaped kernel obligation, per that value's own - citation), so it instead sends Joseph forward via the general rule 3, - the same target date the Annunciation would already be heading to that - same year (Easter + 8). +(* RESOLVED ([of-normae-56f]/W1, 2026-08-26; previously the + precedence_of.mli-documented KNOWN-UNIMPLEMENTED fourth transfer_target + rule, final review Important #5, ledger ruling R9). Normae n. 56(f) -- + St Joseph's solemnity, falling on Palm Sunday, is ANTICIPATED BACKWARD + to 18 March, not carried forward. {!Colitur_kernel.Rite.t.transfer_target}'s + own obligation was relaxed from "strictly later than origin" to + "different from origin" (rite.mli's own comment carries the argument, + traced against {!Colitur_kernel.Calendar}'s actual placement pass, not + merely assumed safe), and [Precedence_of.transfer_target] gained a + Rule 0 for exactly this collision -- see that value's own .ml/.mli for + the full citation. - This is NOT fixed by this task (explicitly out of scope, per the task - brief) -- pinned here, on a REAL affected year, so the current - (known-wrong) behaviour is asserted deliberately rather than passing - silently as if it were correct. All years with Gregorian Easter = 26 - March put Palm Sunday on 19 March, coinciding with Joseph; 2062 is the - nearest one after today (2026) still inside the differential-adjacent - range this project favours for worked examples. + Previously pinned here as KNOWN WRONG (colitur sent Joseph forward to + Easter+9 via the general rule 3 instead); now pinned as CORRECT. All + years with Gregorian Easter = 26 March put Palm Sunday on 19 March, + coinciding with Joseph; 2062 is the nearest one after today (2026) + still inside the differential-adjacent range this project favours for + worked examples. 2062 is a doubly-worked example, not chosen only for Joseph: that same year, 25 March (the Annunciation) falls on HOLY SATURDAY (Easter - 1), - so BOTH solemnities are impeded and BOTH nominally target Easter + 8 via - the general rule -- {!Colitur_kernel.Calendar}'s own placement pass - settles that collision by landing whichever it processes first (Joseph, - departing the earlier date, 19 March) on Easter + 8 and pushing the - other to the next admissible day; empirically, on shipped data, it is - JOSEPH who is pushed one day further still, to Easter + 9 -- read as - further confirmation this is genuinely rule 3's general forward search - (sensitive to whatever else is competing that year), not the fixed, - collision-proof Easter+8 destination rule 3's cousin (the Annunciation's - own Holy-Week branch) names outright -- not as a claim about exactly - which of the two wins the tie, which this test does not depend on. *) -let test_joseph_palm_sunday_2062_known_wrong_forward_transfer () = + so the Annunciation is ALSO impeded and targets Easter + 8 via the + general rule -- independently of Joseph now, since Rule 0 is a fixed + one-day displacement that never enters the general search or competes + with the Annunciation's own target at all (Joseph departs 19 March for + 18 March; the Annunciation departs 25 March for Easter+8 -- the two no + longer collide the way they did when both were pushed toward the same + forward date). *) +let test_joseph_palm_sunday_2062_anticipated_backward () = let easter_2062 = Computus.gregorian_easter 2062 in Alcotest.(check string) "2062 Easter is really 26 March (the Normae n.56(f) trigger)" "2062-03-26" (Date.to_iso8601 easter_2062); @@ -285,36 +281,44 @@ let test_joseph_palm_sunday_2062_known_wrong_forward_transfer () = Alcotest.(check string) "25 March 2062 is really Holy Saturday, coinciding with the Annunciation too" "2062-03-25" (Date.to_iso8601 holy_saturday); let days = Cal.year real_of_rite real_of_layer 2061 in - let joseph_day = - Array.to_list days |> List.find (fun d -> Date.compare d.LD.date palm_sunday = 0) - in + let day_of d = Array.to_list days |> List.find (fun day -> Date.compare day.LD.date d = 0) in + let joseph_day = day_of palm_sunday in Alcotest.(check string) "Palm Sunday itself is observed on 19 March (Joseph impeded, correctly)" "of-palm-sunday" (slug_of joseph_day.LD.observed); let joseph_slug = "joseph-husband-of-the-blessed-virgin-mary" in let departure = List.find_opt (fun (c, _) -> slug_of c = joseph_slug) joseph_day.LD.transferred_out in - match departure with + let eighteen_march = Date.add_days palm_sunday (-1) in + (match departure with | None -> Alcotest.fail "expected Joseph to be transferred_out from 19 March 2062 (impeded by Palm Sunday)" | Some (_, target) -> - (* Concrete, not merely qualitative: 2062-04-04 is the actual pinned - value on shipped data today (Easter + 9, one day past the - Annunciation's own Easter + 8 -- see this test's own header). A - future data or Calendar change that moves it is meant to be - caught here; the point being pinned is the SHAPE (forward, past - Easter, not 18 March), asserted again below in a form that does - not depend on the exact day. *) Alcotest.(check string) - "KNOWN WRONG (Normae n.56(f) unimplemented, precedence_of.mli): Joseph lands forward, past \ - Easter (currently Easter+9, one day beyond the Annunciation's own Easter+8), not the \ - rubrically-correct 18 March (backward)" - "2062-04-04" (Date.to_iso8601 target); - Alcotest.(check bool) "not 18 March -- confirming this really is the anticipation defect, not a \ - coincidence" false - (Date.compare target (Date.add_days palm_sunday (-1)) = 0); - Alcotest.(check bool) "and it lands on or after Easter itself (rule 3's forward search, not a \ - backward anticipation)" true - (Date.compare target easter_2062 >= 0) + "Normae n.56(f): Joseph is anticipated BACKWARD to 18 March 2062, not carried forward" + "2062-03-18" (Date.to_iso8601 target); + Alcotest.(check bool) "which really is the day before Palm Sunday" true + (Date.compare target eighteen_march = 0)); + let march18_day = day_of eighteen_march in + Alcotest.(check string) "and 18 March 2062 itself observes St Joseph (not Cyril of Jerusalem's \ + ad-libitum memorial, not the ordinary Lenten Saturday feria)" + joseph_slug (slug_of march18_day.LD.observed); + let joseph_arrived = + match march18_day.LD.transferred_in with + | Some c -> slug_of c = joseph_slug + | None -> false + in + Alcotest.(check bool) "and 18 March 2062 records the arrival (transferred_in), not a silent placement" + true joseph_arrived; + (* {!Colitur_kernel.Rite.t.transfer_target}'s own second obligation + (terminate) reduces, for this liturgical year, to the whole-year + placement pass reaching a fixed point at all -- {!Val.run}'s own + "unconverged" check is exactly {!Colitur_kernel.Calendar}'s round + guard surfaced as a named failure (calendar.ml's own + [unconverged_reason]). *) + let failures = run 2061 in + Alcotest.(check bool) "the whole 2061 liturgical year still reaches a fixed point (no unconverged \ + transfer placement anywhere in it)" false + (List.exists (fun f -> f.Val.check = "unconverged") failures) (* Second NEWLY-FOUND defect, pinned the same way (see [is_known_holy_family_fallback_gap]'s own citation just above for the @@ -402,9 +406,9 @@ let suite = Alcotest.test_case "2005-2050: transfers reach a fixed point, nothing lost or duplicated" `Slow test_transfers_reach_a_fixed_point_2005_2050; Alcotest.test_case - "KNOWN OPEN DEFECT pinned, not fixed: St Joseph on Palm Sunday 2062 transfers forward, not \ - backward per Normae n.56(f)" `Quick - test_joseph_palm_sunday_2062_known_wrong_forward_transfer; + "RESOLVED (W1): St Joseph on Palm Sunday 2062 is anticipated backward to 18 March per Normae \ + n.56(f), converges, and is recorded as an arrival" `Quick + test_joseph_palm_sunday_2062_anticipated_backward; Alcotest.test_case "NEWLY-FOUND DEFECT pinned, not fixed: Holy Family's Normae n.35(a) 30-December fallback is \ unreached when Christmas Day is a Sunday (1583)" `Quick |