kernel(validate): invariant harness over liturgical years

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.

2 files changed, 108 insertions, 0 deletions

diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml
new file mode 100644
index 0000000..9be030a
--- /dev/null
+++ b/lib/kernel/validate.ml
@@ -0,0 +1,92 @@
+(* The invariant harness: validation layer 2 of the spec's five. Checks run over
+   a LITURGICAL year (year_start y .. year_start (y+1) - 1), not a civil year:
+   Christmastide straddles January, so over a civil year it would falsely appear
+   to recur and break the contiguity check. *)
+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 =
+  let start = year_start year in
+  let stop = 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
+  (* Walk the liturgical year once, collecting what the checks need. *)
+  let days = ref [] in
+  let d = ref start in
+  while Date.compare !d stop <= 0 do
+    days := !d :: !days;
+    d := Date.add_days !d 1
+  done;
+  let days = List.rev !days in
+  let observed = ref [] in
+  List.iter
+    (fun date ->
+      match temporal date with
+      | exception exn ->
+          (* Coverage: temporal must be total. *)
+          fail date "coverage" (Printexc.to_string exn)
+      | t ->
+          let cel = t.Temporal.office in
+          observed := (date, t) :: !observed;
+          (* Weekday agreement. *)
+          if t.Temporal.weekday <> Date.weekday date then
+            fail date "weekday" "temporal weekday disagrees with Date.weekday";
+          (* Slug well-formed. Uniqueness *per date* needs no check: [temporal]
+             returns exactly one office by construction, which is the type
+             system delivering the invariant. Uniqueness *across the year* is
+             deliberately NOT asserted -- a resumed Sunday reuses an earlier
+             Epiphany key on purpose, so the check would be false. *)
+          (match Slug.of_string (Slug.to_string cel.Celebration.slug) with
+           | Ok _ -> ()
+           | Error e -> fail date "slug" e);
+          (* Vocabulary closure. *)
+          if not (List.exists (fun r -> vocab.Vocab.rank_to_string r
+                                        = vocab.Vocab.rank_to_string cel.Celebration.rank)
+                    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")
+    days;
+  let observed = List.rev !observed in
+  (* Season contiguity and completeness: the run-length-compressed sequence must
+     equal vocab.seasons exactly -- all seasons, each in one unbroken run, in
+     canonical order. No EF season can be empty in any year. *)
+  let compressed =
+    List.fold_left
+      (fun acc (_, t) ->
+        let s = vocab.Vocab.season_to_string t.Temporal.season in
+        match acc with hd :: _ when hd = s -> acc | _ -> s :: acc)
+      [] observed
+    |> List.rev
+  in
+  let expected = List.map vocab.Vocab.season_to_string vocab.Vocab.seasons in
+  if compressed <> expected then
+    fail start "seasons"
+      (Printf.sprintf "season runs %s; expected %s"
+         (String.concat "," compressed) (String.concat "," expected));
+  (* Week numbering: non-decreasing within a season run, and constant across each
+     Sunday-to-Saturday span inside that run. Deliberately NOT "starts at 1":
+     the numbering origin is season-specific. *)
+  let rec check_weeks prev_season prev_week = function
+    | [] -> ()
+    | (date, t) :: rest ->
+        let s = vocab.Vocab.season_to_string t.Temporal.season in
+        let same_run = prev_season = Some s in
+        (match (t.Temporal.week, prev_week) with
+         | Some n, Some p when same_run && n < p ->
+             fail date "week" (Printf.sprintf "week %d follows %d in the same season run" n p)
+         | _ -> ());
+        (* Within a run, a non-Sunday must carry the same week as the day before. *)
+        (match (t.Temporal.week, prev_week) with
+         | Some n, Some p when same_run && Date.weekday date <> Date.Sun && n <> p ->
+             fail date "week" (Printf.sprintf "week changed to %d on a non-Sunday (was %d)" n p)
+         | _ -> ());
+        let carry = match t.Temporal.week with Some _ as w -> w | None -> if same_run then prev_week else None in
+        check_weeks (Some s) carry rest
+  in
+  check_weeks None None observed;
+  List.rev !failures
diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli
new file mode 100644
index 0000000..b557731
--- /dev/null
+++ b/lib/kernel/validate.mli
@@ -0,0 +1,16 @@
+(** The invariant harness -- validation layer 2. Checks run over a *liturgical*
+    year, not a civil year: a season that straddles January would otherwise look
+    as though it recurs. *)
+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. *)
+val run :
+  ('s, 'r) Vocab.t ->
+  year_start:(int -> Date.t) ->
+  temporal:(Date.t -> ('s, 'r) Temporal.t) ->
+  year:int ->
+  failure list