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.

4 files changed, 154 insertions, 1 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
diff --git a/test/test_colitur.ml b/test/test_colitur.ml
index 293e439..ae58607 100644
--- a/test/test_colitur.ml
+++ b/test/test_colitur.ml
@@ -2,4 +2,4 @@
 let () =
   Alcotest.run "colitur"
     [ Test_date.suite; Test_computus.suite; Test_colour.suite; Test_slug.suite; Test_names.suite;
-      Test_overlay.suite; Test_temporal_ef.suite ]
+      Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite ]
diff --git a/test/test_validate.ml b/test/test_validate.ml
new file mode 100644
index 0000000..e293dfd
--- /dev/null
+++ b/test/test_validate.ml
@@ -0,0 +1,45 @@
+module Val = Colitur_kernel.Validate
+module V = Rite_ef.Vocab_ef
+module T = Rite_ef.Temporal_ef
+
+let run year =
+  Val.run V.vocab ~year_start:T.year_start ~temporal:T.temporal ~year
+
+let check_year year =
+  match run year with
+  | [] -> ()
+  | fs ->
+      Alcotest.failf "%d: %s" year
+        (String.concat "; " (List.map Val.failure_to_string (List.filteri (fun i _ -> i < 5) fs)))
+
+let test_landmark_years () = List.iter check_year [ 1583; 2026; 2035; 9998 ]
+
+(* Easter extremes: the earliest possible date is 22 March and the latest is
+   25 April. Find one of each inside the domain and validate those years. *)
+let extreme_years () =
+  let module C = Colitur_kernel.Computus in
+  let module D = Colitur_kernel.Date in
+  let earliest = ref None and latest = ref None in
+  for y = 1583 to 2500 do
+    let e = C.gregorian_easter y in
+    if D.month e = 3 && D.day e = 22 && !earliest = None then earliest := Some y;
+    if D.month e = 4 && D.day e = 25 && !latest = None then latest := Some y
+  done;
+  List.filter_map Fun.id [ !earliest; !latest ]
+
+let test_easter_extremes () =
+  let ys = extreme_years () in
+  Alcotest.(check bool) "found at least one extreme year" true (ys <> []);
+  List.iter check_year ys
+
+(* The confidence-to-9999 core: random years across the whole domain. *)
+let prop_invariants =
+  QCheck.Test.make ~count:200 ~name:"EF temporal invariants hold across 1583..9998"
+    (QCheck.int_range 1583 9998)
+    (fun y -> run y = [])
+
+let suite =
+  ( "Validate",
+    [ Alcotest.test_case "landmark years" `Quick test_landmark_years;
+      Alcotest.test_case "easter extremes" `Quick test_easter_extremes ]
+    @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] )