deterministic OCaml engine to compute and validate liturgical calendars for multiple rites, template-driven output to year 9999 https://git.labunix.xyz/colitur.git/atom?h=v0.3.0 2026-08-17T12:56:46Z 2026-08-17T12:56:46Z Lukasz Kasprzak lukas@labunix.xyz 2026-08-17T12:56:46Z urn:sha1:947cadfab527829f8e42a896339a0fa6c2e81ad9 Layers 2 and 5 for the reading citations, which until now had coverage from layers 3 and 4 only -- both oracle-bounded, at 2050 and 2027. test_validate.ml said so in its own words ("No fixture here exercises citations") and test_golden.ml's describe pinned twelve fields, none of them a citation. 358 tests -> 369, and 370 under the sweep. Layer 2 as two Validate checks rather than standalone QCheck properties, so they ride the existing prop_invariants and the exhaustive sweep instead of duplicating that machinery. "citations" asserts a day's parts, sorted, are exactly [First; Gospel] -- one condition carrying three invariants: zero or two but never one, nothing outside First and Gospel since the chants are deliberately unbuilt, and no part twice, which a bare cardinality test would miss. "citations-unresolved" is the separate coverage half: the chain fell through every step. Both are gated on the rite producing some citation somewhere, so a rite whose lectionary is not built is held to neither and the synthetic fixtures stay unaffected. The result over the whole domain: every day of every liturgical year 1583-9999 resolves exactly one Epistle and one Gospel. Mutation-proved live rather than merely silent -- treating a well-formed pair as malformed reddens the suite with real days showing [first,gospel]. citations-unresolved has no live witness at all, which is why test_validate.ml gains five fixtures driving both checks through a new ?readings override, including the gate itself. Layer 5 as six pins, one per chain step, so a regression names the step that broke. Every literal was read out of the scans before being compared with colitur, per that file's standing rule; scan lines are in each pin's comment. Two of the six cover step 4, and the plan's own dates for steps 1 and 4 were wrong: 2030-01-13 is a temporal day (Holy Family on the generic Sunday slug) and would not have exercised step 1, while 2038-03-08 is John of God, who has a full proper Mass and never routes through a Common -- so he becomes the step-1 pin instead. A separate formatter rather than widening describe: widening would invalidate all thirty existing literals at once and the only practical way back would be pasting in whatever colitur printed, which is what the file's header forbids. Restoring them honestly means hand-verifying thirty more Masses against the scans, a task of its own. Stated rather than hidden, and defensible because layer 2 now checks the shape of every day in every year, which is the breadth that widening would have bought. Two pins earned their keep immediately. Lent I Monday failed on "Ezek" against colitur's "Ezech" -- notation only, and colitur matches the Missal's own abbreviation; layer 3 normalises this away and cannot see it. The displaced-Sunday feria pins M26 shape 2(b)'s known-wrong walkback deliberately, labelled as such so a future fix fails loudly, and established two things M26 had not recorded: both parts come from the displacing feast, not only the Gospel it cites, and the reference carries a stray trailing period inherited through the bootstrap. Blast radius: zero. The CLI never calls Validate, no data file changed, and 20 years spanning 1583-9998 produce 7301 byte-identical lines between the pre-change binary and HEAD. Step 4's blind spot is now measured rather than argued. Corrupting the Common of Non-Virgins I's Epistle leaves layer 3 (16801 days) and layer 4 (730 days) both green, reddening only one unit test and one new pin. Both step-4 pins matched the scans on the first attempt -- the first independent confirmation that route has ever had. It narrows the gap without closing it: two of five Common-routed saints are witnessed, isidore-of-seville is not, and gregory-the-great and patrick are unreachable in any year 2005-2050. Register: section 6.7 addendum. validate.mli documents both new labels; liturgical_day.mli's "always empty until Plan 4" was outlived by the lectionary and is corrected. 2026-08-12T14:45:58Z Lukasz Kasprzak lukas@labunix.xyz 2026-08-12T14:45:58Z urn:sha1:5d5454208464892e96310efd99ec9db09171f982 Fix round 1 on the commemoration-identity/tie-break work: the "genuine same-band tie" M17 adjudicated as open was not a tie at all. RG 91's table enumerates only "dies liturgici" (real feasts) -- entry 24's own text is "Festa III classis, in calendario Ecclesiae universae inscripta" -- so a Celebration.t.status = Commemoration_only candidate (a saint reduced to a bare commemoration) has no row in the table to begin with. Precedence_ef.band used to read rank alone, so it silently lent such a candidate the same table entry as a genuine Feast of its own rank; the calendarium's own 22 September row confirms the distinction in its own notation ("S. Thomae de Villanova ... III classis. / Commemoratio Ss. Mauritii et Soc. Mm." -- Thomas carries a class number, Maurice carries none). Fixed at the source, not by adding a status tier to compare_precedence: band now checks status first, ahead of every rank-keyed branch, and returns unclassified for any Commemoration_only candidate. M17 deleted (not re-adjudicated) -- 22 September now resolves identically on both sides, with no divergence left to name. Blast radius measured independently (a temporary git worktree at the pre-fix commit): 4451 days change across the whole 1583-9999 domain, exactly 4 verified shapes -- 3576 x maurice-and-companions-martyrs -> thomas-of-villanova and 282 x eleutherius -> philip-neri (admitted set changes), 502 x appollonia/cyril-of-alexandria and 91 x dorothy/titus (order only, independently confirmed against the calendarium's own listing convention). Zero days change who is observed. Further swept the whole domain for a genuine "two different candidates on the identical real table entry" residual -- the shape RG 113 truly gives no instruction for -- and found it empty: of 109201 same-rank ties domain-wide, 83950 now resolve by band alone and the remaining 25251 are exclusively two Commemoration_only candidates tied at unclassified, never two real feasts. The residual admit still breaks alphabetically is real, but narrower than previously documented. The "66 days" figure is reconciled, not merely disputed: 599 is the tie population, 65 (whole-comparator: 67) is the real admitted-set decision count within it (independently reproduced against the pre-Task-B binary), 149 is order-only. Every one of the 65 real decisions traces to the same Commemoration_only/Feast root cause as Maurice/Thomas. Also: validate.ml's admission fixed-point check recovers a commemoration's real origin (by matching its slug against the day's own temporal office) instead of reconstructing every candidate as Sanctoral, since band -- unlike EF's own admit -- does read origin; precedence_ef.ml/.mli's motivating example and blast-radius claims corrected to no longer rest on the fixed Maurice/Thomas case; test_identity_rank_corroboration's own population count corrected now that 22 September (and 21 other Feast-status matches) became reachable; its rank-agreement pin documents exactly what it does and does not prove. Register (§4, §6.1, §6 checklist) and CLAUDE.md corrected in place, including the RG 113 first-sentence gap this exercise surfaced but did not close, recorded as a new open item. 275 -> 276 tests (with the exhaustive sweep), all green. 2026-08-12T00:37:03Z Lukasz Kasprzak lukas@labunix.xyz 2026-08-12T00:37:03Z urn:sha1:4235a6aa18b815c5457a7eb97fd97eb4919dfd4b Three carried items from Plan 2's parked rulings, closed: 1. Slug uniqueness moves from a 200-sample QCheck property scoped to one rite (test_temporal_ef.ml) into Validate's own "slugs" check, so every consumer gets it. The resumed-Sunday exemption that property carried is dropped, not weakened elsewhere: Plan 2 verified zero duplicate slugs domain-wide (all 8 416 years), and by construction a resumed Sunday only ever backfills a week number Septuagesima cut short that same liturgical year, so it can never repeat a number that year's own January Sundays already used. The now-redundant property and its is_resumable_sunday_slug helper are removed from test_temporal_ef.ml; test_validate.ml's own domain-wide property covers the same ground for every consumer. 2. The anchors-erosion guard (Plan 2: deleting entries from a rite's anchors list left the whole suite green) is implemented, but not in Validate. Which of a rite's named days are Easter-derived is knowledge only the rite's own `named` function has; Rite.t deliberately exposes only `temporal` and `anchors`, never `named`, so a rite-agnostic Validate has no ground truth to check anchors' completeness against. Hardcoding an Easter offset, or even Easter itself, would smuggle Western/Gregorian-specific knowledge into code meant to also serve a future Julian-reckoning rite; rediscovering "named-ness" structurally from `temporal` alone is unsound for EF, since most ordinary Sunday/feria slugs from Septuagesima onward are also constant-offset-from-Easter by construction. The guard is therefore EF-specific and lives in test_temporal_ef.ml, discovering the Easter-derived slug set mechanically (scanning a window around Easter and keeping whatever `named` answers Some for) rather than hand-copying either named's or anchors' own offset list, then asserting completeness against the real anchors for the domain's Easter extremes (1598, 1666) plus an ordinary year. A negative fixture proves the guard has teeth, matching Plan 2's exact regression (anchors missing "ef-ascension" reports it, and only it, as missing). 3. test_validate.ml's extreme_years comment claimed 1818/2038; verified against Computus.gregorian_easter directly, the domain's actual Easter extremes (1583..2500) are 1598/1666. Corrected. Verification: the full 1583..9999 domain sweep (233 tests via dune test's 200-sample default, plus a manual full sweep) reports exactly one failure -- the known, already-pinned year-9999 season-truncation case -- and zero occurrences of the new "slugs" check anywhere in the domain. Deleting "ef-ascension" from the real anchors list (reproducing Plan 2's regression directly) is caught immediately by the new EF test and, confirmed empirically, invisible to Validate's own full property sweep -- direct evidence for why item 2 cannot live in Validate. 2026-08-12T00:12:03Z Lukasz Kasprzak lukas@labunix.xyz 2026-08-12T00:12:03Z urn:sha1:633306c8a5ac1854f30749f498498104ebc84edc Widen Validate.run to take the rite's sanctoral layer alongside the rite itself (Calendar.year needs both), and add five checks over the fully resolved liturgical year, on top of the existing temporal-only pass: - observed: a day's observed celebration never also appears among that same day's own commemorations/omissions. - lost: no sanctoral entry is silently dropped. Per slug, the number of times it is actually sighted (observed + commemorations + omitted, summed over the year) must never fall below the number of times its own Date_spec resolves within the year's span -- also fires if resolving the year raises at all, the most total form of loss. - duplicated: the same per-slug count must never exceed the number of Date_spec resolutions either. Deliberately NOT "no slug appears twice": a fixed date can legitimately resolve twice in the ~20% of liturgical years whose 371-day span reaches it on both ends (30 November/St Andrew is the worked example in validate.mli). - unconverged: no day's omitted reason indicates Calendar's placement pass hit its round guard before reaching a fixed point. - admission: the rite's own rules.admit is a fixed point on what it already admitted -- the rite-agnostic form of "the admission limit was not exceeded" available without embedding a rite's own numeric caps (RG 111's, for EF) into kernel code. Each check has a dedicated negative fixture in the synthetic rite (test_validate.ml), hand-traced against Calendar's actual resolution mechanics before writing the assertion, and verified to fail for the right reason against the code before this change. One pair (unconverged/duplicated) is not fully independent: hitting the round guard genuinely also trips duplicated, a real consequence of Calendar's own accounting once a candidate is simultaneously sighted at its permanent natural date and wherever the last placement round left it -- documented in guard_rules's own comment, not papered over. test_validate.ml's ef_rite/run now use the real Rite_ef.context and the real bootstrapped data/ef layer (Precedence_ef and the sanctoral bootstrap did not exist when this scaffolding was first written) rather than the earlier placeholder rules. Validate is clean across the whole 1583..9999 domain against real EF data except the one already-documented year-9999 truncation case (test_year_9999_does_not_raise). 2026-08-11T17:39:37Z Lukasz Kasprzak lukas@labunix.xyz 2026-08-11T17:39:37Z urn:sha1:6436509d6b599b7d7c6467bd39c8090cb9634889 Validate took four loose arguments that had to come from the same rite with nothing enforcing it, and Calendar is about to add more. Bundling makes a mismatched assembly unrepresentable through the normal path. season_runs replaces the hardcoded assumption that every season occupies exactly one unbroken run. That holds for the 1962 rite but is false for the modern form's Ordinary Time, which is one season in two runs -- as written the check would have reported a false failure every year for the second rite. 2026-08-11T14:23:27Z Lukasz Kasprzak lukas@labunix.xyz 2026-08-11T14:23:27Z urn:sha1:23892f0a5933851e90fb8b6aef5c3b6f7e24bc1b Validate.run ~year:9999 raised (year_start (year + 1) asked year_start for civil year 10000, out of the kernel's 1583..9999 domain), even though 9999 is itself in range and kernel computation must never raise on in-range input; ~year:9998 already returned zero failures. run now clamps its scan to 31 December 9999 instead of computing year_start (year + 1) when year is the domain maximum, and validates the resulting truncated final liturgical year rather than not being able to run it at all. The design spec's validation §5 lists eight checks; only five were implemented (coverage, seasons, weeks, weekday, closure). The two missing were a real gap, not just a documentation slip: - §5.7 anchor agreement. All of an EF year's Easter-derived and fixed named days were pinned only by point assertions for 2026. run now takes an ~anchors:(int -> (string * Date.t) list) parameter -- the rite's own independent restatement of those dates, paired with the slug each should carry, not derived from temporal itself -- and checks that temporal agrees on every one of them. Temporal_ef.anchors supplies EF's list. Kept rite-agnostic: the anchor list comes from the rite argument, not the kernel. - §5.8 determinism. run now calls temporal a second time for every date and checks the result is structurally equal to the first. Also, finding 8: the rank/season closure checks compare vocab entries via their _to_string images, which is only sound if those images are injective. run now checks List.map rank_to_string ranks and List.map season_to_string seasons for duplicates up front and reports a "vocab" failure if either collapses two distinct values to the same string, rather than relying on that injectivity unasserted. Test-quality fixes to the existing synthetic fixture, found while adding coverage for the above: the fixture's own comment claimed its mutation target (2026-03-15) was "not a Sunday" and "sits safely mid-run" -- it is a Sunday, which made the coverage/week mutations cascade further than documented even though the assertions still target specific check labels. Moved to a genuine mid-week day (2026-03-17) and the comment corrected. extreme_years's own test required only "found at least one" of the two Easter-extreme years; tightened to require both, since both genuinely exist in 1583..2500. Covering tests: test_year_9999_does_not_raise (would error under the old code; the fix is pinned by calling run 9999 directly with no try, plus asserting the truncated year is reported via an ordinary "seasons" failure, not silently or via coverage); anchor-clean and anchor-fires cases on the synthetic rite; a determinism-fires case using a target date whose temporal alternates what it returns across successive calls; two vocab-injectivity-fires cases (collapsed rank strings, collapsed season strings). 2026-08-11T13:09:53Z Lukasz Kasprzak lukas@labunix.xyz 2026-08-11T12:56:09Z urn:sha1:e15fe4952a569f08900f9d602f7bc98afd298542 Coverage, season contiguity and completeness, Sunday-aligned week numbering, slug well-formedness, weekday agreement and vocabulary closure. Checks run over a liturgical year rather than a civil one, since Christmastide straddles January and would otherwise appear to recur. Run against EF temporal for landmark years, both Easter extremes, and 200 random years across 1583..9998 -- the property layer is how confidence reaches past the oracle horizon.