diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-11 16:23:27 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-11 16:23:27 +0200 |
| commit | 23892f0a5933851e90fb8b6aef5c3b6f7e24bc1b (patch) | |
| tree | d1c0cc11678bc43ad3fee19273334e3f32adb72f /lib/kernel/validate.mli | |
| parent | 68cff511cd79ca5450c4f21dffba1b1e4ac93389 (diff) | |
| download | colitur-23892f0a5933851e90fb8b6aef5c3b6f7e24bc1b.tar.gz colitur-23892f0a5933851e90fb8b6aef5c3b6f7e24bc1b.zip | |
kernel(validate): never raise at 9999; add anchor, determinism, vocab checks
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).
Diffstat (limited to 'lib/kernel/validate.mli')
| -rw-r--r-- | lib/kernel/validate.mli | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index b557731..709a711 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,12 +5,26 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run vocab ~year_start ~temporal ~year] returns every invariant violation in - the liturgical year opening in civil year [year]. An empty list means the - year is clean. *) +(** [run vocab ~year_start ~temporal ~anchors ~year] returns every invariant + violation in the liturgical year opening in civil year [year]. An empty + list means the year is clean. + + [anchors y] is the rite's own independent restatement of its fixed and + Easter-derived named days for civil year [y], as (expected slug, date) + pairs -- not derived from [temporal] itself, so a drift between the two + is caught rather than invisible. [run] consults both [anchors year] and + [anchors (year + 1)], since a liturgical year straddles two civil years, + and checks only the pairs whose date actually falls within the year + walked. + + Total over the whole 1583..9999 domain, including [year] = 9999: the + liturgical year opening there continues into out-of-domain civil year + 10000, so the walk is clamped to 31 December 9999 and the checks run + against that truncated final year rather than raising. *) val run : ('s, 'r) Vocab.t -> year_start:(int -> Date.t) -> temporal:(Date.t -> ('s, 'r) Temporal.t) -> + anchors:(int -> (string * Date.t) list) -> year:int -> failure list |
