kernel(validate): resolution invariants

Widen Validate.run to take the rite's sanctoral layer alongside the rite
itself (Calendar.year needs both), and add five checks over the fully
resolved liturgical year, on top of the existing temporal-only pass:

- observed: a day's observed celebration never also appears among that
  same day's own commemorations/omissions.
- lost: no sanctoral entry is silently dropped. Per slug, the number of
  times it is actually sighted (observed + commemorations + omitted,
  summed over the year) must never fall below the number of times its
  own Date_spec resolves within the year's span -- also fires if
  resolving the year raises at all, the most total form of loss.
- duplicated: the same per-slug count must never exceed the number of
  Date_spec resolutions either. Deliberately NOT "no slug appears
  twice": a fixed date can legitimately resolve twice in the ~20% of
  liturgical years whose 371-day span reaches it on both ends (30
  November/St Andrew is the worked example in validate.mli).
- unconverged: no day's omitted reason indicates Calendar's placement
  pass hit its round guard before reaching a fixed point.
- admission: the rite's own rules.admit is a fixed point on what it
  already admitted -- the rite-agnostic form of "the admission limit
  was not exceeded" available without embedding a rite's own numeric
  caps (RG 111's, for EF) into kernel code.

Each check has a dedicated negative fixture in the synthetic rite
(test_validate.ml), hand-traced against Calendar's actual resolution
mechanics before writing the assertion, and verified to fail for the
right reason against the code before this change. One pair
(unconverged/duplicated) is not fully independent: hitting the round
guard genuinely also trips duplicated, a real consequence of Calendar's
own accounting once a candidate is simultaneously sighted at its
permanent natural date and wherever the last placement round left it --
documented in guard_rules's own comment, not papered over.

test_validate.ml's ef_rite/run now use the real Rite_ef.context and the
real bootstrapped data/ef layer (Precedence_ef and the sanctoral
bootstrap did not exist when this scaffolding was first written) rather
than the earlier placeholder rules. Validate is clean across the whole
1583..9999 domain against real EF data except the one already-documented
year-9999 truncation case (test_year_9999_does_not_raise).

1 files changed, 131 insertions, 1 deletions

diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml
index c6501a9..d8de31b 100644
--- a/lib/kernel/validate.ml
+++ b/lib/kernel/validate.ml
@@ -20,7 +20,20 @@ let has_duplicate strings =
   let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in
   go sorted
 
-let run (rite : ('s, 'r) Rite.t) ~year =
+(* Task 12's "unconverged" check has no structural signal to key off --
+   Calendar's placement pass records its round-guard reason as a plain
+   string in [Liturgical_day.omitted] (calendar.ml's own [unconverged_reason],
+   not exposed as a public constant), and [Liturgical_day.omitted]'s own doc
+   comment says exactly this check is meant to read it. A short, distinctive
+   substring rather than the full literal keeps the coupling to calendar.ml's
+   exact wording as loose as it can be while still being unambiguous: nothing
+   else this kernel emits into [omitted] talks about "converging". *)
+let contains_substring s ~needle =
+  let ls = String.length s and ln = String.length needle in
+  let rec at i = i + ln <= ls && (String.sub s i ln = needle || at (i + 1)) in
+  ln = 0 || at 0
+
+let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year =
   let vocab = rite.Rite.vocab in
   let year_start = rite.Rite.year_start in
   let temporal = rite.Rite.temporal in
@@ -164,4 +177,121 @@ let run (rite : ('s, 'r) Rite.t) ~year =
           if actual <> expected_slug then
             fail date "anchor" (Printf.sprintf "expected slug %S, got %S" expected_slug actual))
     anchor_pairs;
+  (* Resolution invariants (Task 12): everything above only ever asked
+     [rite.temporal] for a date's office in isolation. From here on the
+     LITURGICAL YEAR IS ACTUALLY RESOLVED against [layer] -- occurrence,
+     transfer placement, commemorations, the works (spec §2.4) -- and the
+     result checked for five further properties a temporal-only pass cannot
+     see at all. [days] (the walk built above) is reused rather than
+     recomputed: it names exactly the same [start, stop] span
+     {!Calendar.year} resolves for this [year]. *)
+  (match Calendar.year rite layer year with
+   | exception exn ->
+       (* The kernel contract forbids [run] itself from ever raising on
+          in-range input, and an exception escaping resolution is the most
+          total form of "silently lost" there is: nothing about this year's
+          sanctoral entries could be verified as accounted for at all. *)
+       fail start "lost"
+         (Printf.sprintf "resolving the year raised (%s); nothing could be verified as accounted for"
+            (Printexc.to_string exn))
+   | resolved ->
+       let idx = Layer.index_by_date layer in
+       let bump tbl slug = Hashtbl.replace tbl slug (1 + (try Hashtbl.find tbl slug with Not_found -> 0)) in
+       (* Expected: how many times each layer entry's own Date_spec resolves
+          within [start, stop]. Walking dates and querying [Layer.on_date]
+          (rather than resolving each entry's Date_spec against candidate
+          civil years directly) is what naturally counts a fixed late-
+          November date TWICE in the ~20% of liturgical years whose 371-day
+          span reaches it on both ends -- see validate.mli's own note on 30
+          November / St Andrew. *)
+       let expected : (string, int) Hashtbl.t = Hashtbl.create 64 in
+       List.iter
+         (fun date ->
+           Layer.on_date idx ~month:(Date.month date) ~day:(Date.day date)
+           |> List.iter (fun (e : 'r Layer.entry) ->
+                  bump expected (Slug.to_string e.Layer.cel.Celebration.slug)))
+         days;
+       (* Actual: how many times each slug is actually sighted across the
+          resolved year. Deliberately [observed] + [commemorations] +
+          [omitted] only, NOT [transferred_out]: a successfully transferred
+          celebration is already counted once, via [observed] (+
+          [transferred_in]) on the day it lands; also counting
+          [transferred_out] at the day it left would double-book every clean
+          transfer, which is exactly what this check exists to catch, not
+          cause. *)
+       let actual : (string, int) Hashtbl.t = Hashtbl.create 64 in
+       let bump_cel tbl (c : 'r Celebration.t) = bump tbl (Slug.to_string c.Celebration.slug) in
+       Array.iter
+         (fun (d : ('s, 'r) Liturgical_day.t) ->
+           bump_cel actual d.Liturgical_day.observed;
+           List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.commemorations;
+           List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.omitted)
+         resolved;
+       Hashtbl.fold (fun slug exp acc -> (slug, exp) :: acc) expected []
+       |> List.sort compare (* stable failure order: Hashtbl.iter's own order is hash-seed-dependent *)
+       |> List.iter (fun (slug, exp) ->
+              let act = try Hashtbl.find actual slug with Not_found -> 0 in
+              if act < exp then
+                fail start "lost"
+                  (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves %d"
+                     slug act exp)
+              else if act > exp then
+                fail start "duplicated"
+                  (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves only %d"
+                     slug act exp));
+       Array.iter
+         (fun (d : ('s, 'r) Liturgical_day.t) ->
+           let date = d.Liturgical_day.date in
+           let observed_slug = Slug.to_string d.Liturgical_day.observed.Celebration.slug in
+           let has_slug (c, _) = Slug.to_string c.Celebration.slug = observed_slug in
+           (* "observed": the day's own winner must not ALSO be listed as one
+              of its own losers -- see validate.mli's own note on why this is
+              reachable (two distinct layer entries sharing a slug, one
+              transferred onto the other's natural date, the transferred one
+              winning) despite {!Precedence.resolve}'s fold never letting the
+              SAME candidate value appear as both winner and loser. *)
+           if List.exists has_slug d.Liturgical_day.commemorations
+              || List.exists has_slug d.Liturgical_day.omitted
+           then
+             fail date "observed"
+               (Printf.sprintf
+                  "%s is this day's observed celebration and also appears among its own \
+                   commemorations/omissions"
+                  observed_slug);
+           (* "unconverged": see [contains_substring]'s own comment above. *)
+           if
+             List.exists
+               (fun (_, reason) -> contains_substring reason ~needle:"did not converge")
+               d.Liturgical_day.omitted
+           then
+             fail date "unconverged"
+               "transfer placement did not reach a fixed point within the round guard (RG 96-98)";
+           (* "admission": re-offer this day's own admitted commemorations
+              back to [rite.rules.admit] and require the exact same set back.
+              [origin] is reconstructed as [Sanctoral] uniformly:
+              {!Liturgical_day.t} does not retain a commemoration's original
+              origin, and the real EF [admit] (precedence_ef.ml) reads only
+              rank and slug from a candidate, never [origin], so this
+              reconstruction is exact for it; documented in validate.mli as
+              the one place a rite whose [admit] DOES consult [origin] could
+              see a false negative from this check. *)
+           let observed_candidate : 'r Precedence.candidate =
+             { Precedence.cel = d.Liturgical_day.observed; origin = Precedence.Sanctoral }
+           in
+           let as_candidates comms =
+             List.map (fun (c, p) -> ({ Precedence.cel = c; origin = Precedence.Sanctoral }, p)) comms
+           in
+           let offered = as_candidates d.Liturgical_day.commemorations in
+           let readmitted = rite.Rite.rules.Precedence.admit ~observed:observed_candidate offered in
+           let norm l =
+             List.map (fun (c, p) -> (Slug.to_string c.Precedence.cel.Celebration.slug, p)) l
+             |> List.sort compare
+           in
+           if norm readmitted <> norm offered then
+             fail date "admission"
+               (Printf.sprintf
+                  "admit is not a fixed point on this day's own commemorations: re-offering %d \
+                   admitted %d back"
+                  (List.length offered) (List.length readmitted)))
+         resolved);
   List.rev !failures