aboutsummaryrefslogtreecommitdiff
path: root/lib/kernel/validate.ml
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-11 16:23:27 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-11 16:23:27 +0200
commit23892f0a5933851e90fb8b6aef5c3b6f7e24bc1b (patch)
treed1c0cc11678bc43ad3fee19273334e3f32adb72f /lib/kernel/validate.ml
parent68cff511cd79ca5450c4f21dffba1b1e4ac93389 (diff)
downloadcolitur-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.ml')
-rw-r--r--lib/kernel/validate.ml70
1 files changed, 67 insertions, 3 deletions
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml
index b11c05c..7be3425 100644
--- a/lib/kernel/validate.ml
+++ b/lib/kernel/validate.ml
@@ -7,13 +7,46 @@ type failure = { year : int; date : string; check : string; detail : string }
let failure_to_string f =
Printf.sprintf "%d %s [%s] %s" f.year f.date f.check f.detail
-let run vocab ~year_start ~temporal ~year =
+(* The kernel's domain ends at year 9999 (Date.make's documented 1583..9999
+ bound). 31 December 9999 is always constructible: it is in-range by
+ definition, so this cannot itself raise. *)
+let domain_max_date =
+ match Date.make ~year:9999 ~month:12 ~day:31 with
+ | Ok d -> d
+ | Error e -> failwith e
+
+let has_duplicate strings =
+ let sorted = List.sort String.compare strings in
+ let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in
+ go sorted
+
+let run vocab ~year_start ~temporal ~anchors ~year =
let start = year_start year in
- let stop = Date.add_days (year_start (year + 1)) (-1) in
+ let stop =
+ (* [year_start (year + 1)] needs a date in civil year (year+1); at
+ [year] = 9999, the domain maximum, that lands out of range and would
+ raise. Clamp to 31 Dec 9999 instead of raising: kernel computation
+ must never raise on in-range input, and 9999 is in range. This
+ validates a truncated final liturgical year (through New Year's Eve
+ 9999 only) rather than not being able to run the year at all --
+ see test_validate.ml's [test_year_9999_does_not_raise]. *)
+ if year >= 9999 then domain_max_date
+ else Date.add_days (year_start (year + 1)) (-1)
+ in
let failures = ref [] in
let fail date check detail =
failures := { year; date = Date.to_iso8601 date; check; detail } :: !failures
in
+ (* Vocabulary injectivity: the closure checks below compare ranks and
+ seasons via their _to_string images ([List.mem] has no equality on
+ function-carrying types), which is only sound if those images are
+ distinct per value. A rite whose rank_to_string collapses two ranks to
+ the same string would pass every rank both ranks share -- flag that
+ directly instead of relying on it silently by construction. *)
+ if has_duplicate (List.map vocab.Vocab.rank_to_string vocab.Vocab.ranks) then
+ fail start "vocab" "rank_to_string is not injective over vocab.ranks";
+ if has_duplicate (List.map vocab.Vocab.season_to_string vocab.Vocab.seasons) then
+ fail start "vocab" "season_to_string is not injective over vocab.seasons";
(* Walk the liturgical year once, collecting what the checks need. *)
let days = ref [] in
let d = ref start in
@@ -53,7 +86,15 @@ let run vocab ~year_start ~temporal ~year =
vocab.Vocab.ranks)
then fail date "rank" "rank not in the rite vocabulary";
if not (List.mem cel.Celebration.colour Colour.all) then
- fail date "colour" "colour not among the six")
+ fail date "colour" "colour not among the six";
+ (* Determinism: a second, independent call for the same date must
+ structurally agree with the first. temporal takes no wall-clock,
+ randomness or environment input, so any difference here is a
+ purity bug in the rite's own code, not a property of the date. *)
+ (match (try Some (temporal date) with _ -> None) with
+ | Some t2 when t2 = t -> ()
+ | Some _ -> fail date "determinism" "a second call to temporal returned a different result"
+ | None -> fail date "determinism" "a second call to temporal raised where the first succeeded"))
days;
let observed = List.rev !observed in
(* Season contiguity and completeness: the run-length-compressed sequence must
@@ -93,4 +134,27 @@ let run vocab ~year_start ~temporal ~year =
check_weeks (Some s) carry rest
in
check_weeks None None observed;
+ (* Anchor agreement: dates the rite itself flags as fixed/Easter-derived
+ anchors (register/spec §5.7) must land where the rite's own independent
+ restatement of them says. [anchors] takes a civil year and returns dates
+ within it; a liturgical year straddles two civil years (most of Advent's
+ year plus most of the following civil year), so both are consulted and
+ the result filtered to the dates actually walked above. Guarded with a
+ safe wrapper: at [year] = 9999, [anchors (year + 1)] asks for civil year
+ 10000, out of the kernel's domain, and must not propagate a raise here
+ any more than [year_start] may above. *)
+ let safe_anchors y = try anchors y with _ -> [] in
+ let anchor_pairs =
+ safe_anchors year @ safe_anchors (year + 1)
+ |> List.filter (fun (_, date) -> Date.compare date start >= 0 && Date.compare date stop <= 0)
+ in
+ List.iter
+ (fun (expected_slug, date) ->
+ match temporal date with
+ | exception exn -> fail date "anchor" (Printexc.to_string exn)
+ | t ->
+ let actual = Slug.to_string t.Temporal.office.Celebration.slug in
+ if actual <> expected_slug then
+ fail date "anchor" (Printf.sprintf "expected slug %S, got %S" expected_slug actual))
+ anchor_pairs;
List.rev !failures