diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/kernel/validate.ml | 70 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 20 |
2 files changed, 84 insertions, 6 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 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 |