aboutsummaryrefslogtreecommitdiff
path: root/lib/kernel/validate.mli
Commit message (Collapse)AuthorAgeFilesLines
* kernel(validate): never raise at 9999; add anchor, determinism, vocab checksLukasz Kasprzak2026-08-111-3/+17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* kernel(validate): invariant harness over liturgical yearsLukasz Kasprzak2026-08-111-0/+16
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.