path: root/lib/kernel/validate.ml

(* 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

(* 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

(* Like [has_duplicate], but names the offender(s) instead of only reporting
   that one exists -- the ["slugs"] check below wants a useful failure
   detail, not just a bool. *)
let duplicates strings =
  let sorted = List.sort String.compare strings in
  let rec go acc = function
    | a :: (b :: _ as rest) -> go (if a = b then a :: acc else acc) rest
    | _ -> acc
  in
  List.sort_uniq String.compare (go [] sorted)

(* 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
  let anchors = rite.Rite.anchors in
  let start = year_start year 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
  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: three properties. Well-formedness needs no check: [Slug.t]
             is a private string validated on every construction path
             ([of_string], [of_string_exn], [t_of_sexp]), and [to_string] is
             the identity, so round-tripping an existing [Slug.t] can never
             fail -- a check here would be structurally incapable of firing,
             which is worse than no check, since it would look like coverage
             that isn't there. Uniqueness *per date* needs no check either:
             [temporal] returns exactly one office by construction.
             Uniqueness *across the year* IS asserted, below, once the whole
             walk is in hand -- see the ["slugs"] check after this loop. *)
          (* 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";
          (* 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
  (* Slug uniqueness across the year (Plan 2 carried item 4): moved into
     [Validate] itself so every consumer gets it, not only a 200-sample
     QCheck property scoped to one rite. Asserted OUTRIGHT, no exemption:
     Plan 2 verified zero duplicate slugs domain-wide, across all 8 416
     years, for the EF rite's own resumed-Sunday mechanism -- the exemption
     the test property used to carry protected nothing real, because a
     resumed Sunday only ever backfills a week number Septuagesima cut short
     that same liturgical year (so it was never actually used that year to
     begin with), never repeats one the year's own January Sundays already
     used. If a future rite genuinely needs an exemption, it can supply one
     then -- not speculatively here. *)
  (match duplicates (List.map (fun (_, t) -> Slug.to_string t.Temporal.office.Celebration.slug) observed) with
   | [] -> ()
   | dups ->
       fail start "slugs"
         (Printf.sprintf "slug(s) sighted on more than one date this year: %s" (String.concat ", " dups)));
  (* Season contiguity and completeness: the run-length-compressed sequence must
     equal the rite's own [season_runs] exactly, in canonical order. This is
     NOT necessarily [vocab.seasons] -- most rites have each season in one
     unbroken run, but a rite may legitimately have one season appear in two
     separate runs (the modern form's Ordinary Time does), so the expected
     sequence is rite-supplied rather than derived from the vocabulary. *)
  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 rite.Rite.season_runs 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;
  (* 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;
  (* 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 ->
       (* Same span reasoning as {!Calendar.year}: the liturgical year
          straddles civil [year] and [year + 1], so both are resolved for
          movable entries. *)
       (* A liturgical year straddles two civil years, so both are named.
     [Layer.index] filters them to the kernel domain, which is what keeps
     the edges (year = 1583 naming 1582, year = 9999 naming 10000) from
     calling the rite's [easter] out of range. *)
  let idx = Layer.index layer ~easter:rite.Rite.easter ~years:[ year - 1; year; year + 1 ] 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 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 RECOVERED, not fabricated -- see the fuller note
              below on [as_candidates]. It was formerly reconstructed as
              [Sanctoral] uniformly, justified by the claim that the real EF
              [admit] reads only rank and slug and never [origin]. That claim
              is now FALSE: since ea22ad2 the EF [admit] orders by [band]
              (RG 113), and [band] does read [origin] via [is_temporal], so a
              temporal-origin commemoration relabelled [Sanctoral] would be
              scored on the wrong table entry. The recovery below is exact,
              not a heuristic: [resolve] builds exactly one temporal
              candidate per day, so a slug match against the day's own
              temporal office identifies it unambiguously. *)
           let observed_candidate : 'r Precedence.candidate =
             { Precedence.cel = d.Liturgical_day.observed; origin = Precedence.Sanctoral }
           in
           (* [~temporal] (fix round 1, RG16(a) task): {!Precedence.rules.admit}
              now also takes the day's own temporal-cycle candidate, reused
              here from {!Liturgical_day.t}'s own embedded [Temporal.t] --
              the exact same value {!Calendar} passed to {!Precedence.resolve}
              in the first place, so re-offering is against the SAME inputs,
              not a reconstruction that could itself introduce a false
              negative. [origin] is [Precedence.Temporal], genuinely (this IS
              the temporal candidate, not a reconstructed sanctoral one). *)
           let temporal_candidate : 'r Precedence.candidate =
             { Precedence.cel = d.Liturgical_day.temporal.Temporal.office;
               origin = Precedence.Temporal }
           in
           (* [band]'s own [context] (RG 113, docs/research/rules-register.md
              §4 "Commemorations" -- {!Precedence.rules.admit}'s own new
              [int] parameter, added alongside RG 113's fix: [admit] now
              orders/selects by the rite's table-of-precedence value
              {!resolve} attaches to each candidate, not by [Vocab.rank]
              alone). Reconstructed from {!Liturgical_day.t}'s own embedded
              [Temporal.t], the same source [temporal_candidate] above
              already draws its [cel] from, so this is the exact [ctx]
              {!Calendar} passed to {!Precedence.resolve} for this date in
              the first place, not a re-derivation that could itself drift. *)
           let day_ctx : 's Precedence.context =
             { Precedence.date;
               season = d.Liturgical_day.temporal.Temporal.season;
               weekday = d.Liturgical_day.temporal.Temporal.weekday }
           in
           (* CORRECTED (Task B fix round 1, coordinator finding 5): [origin]
              used to be reconstructed as [Sanctoral] UNCONDITIONALLY, which
              was harmless while nothing here called [band] on the result
              (the comment this replaces was correct about [PE.admit] itself:
              it never reads [origin]) -- but this function ALSO now calls
              [rite.rules.Precedence.band day_ctx cand] on every one of these
              reconstructed candidates (the line just below), and [band] DOES
              read [origin] (its own [is_temporal] test) to choose between its
              temporal- and sanctoral-keyed branches. A genuinely
              TEMPORAL-origin commemoration (a privileged Advent/Lent/
              Passiontide feria, an Ember day, an impeded Sunday) mislabelled
              [Sanctoral] would score the WRONG band entry (e.g. a Lent feria
              scoring entry 23, "III-class feasts in particular calendars",
              instead of its real entry 22) -- inert today only because
              nothing currently asserts on the SCORE [band] returns here, only
              on whether re-offering [admit] the same values round-trips
              (which happens not to depend on getting [origin] right for any
              case this codebase's data reaches -- unverified in general).
              [Liturgical_day.t] itself still does not retain a
              commemoration's original origin, so it is recovered the only
              way available: a commemoration whose SLUG matches the day's own
              temporal office is temporal-origin; every other commemoration
              is sanctoral-origin. This is exact whenever slugs cannot
              collide across the two streams (Task 12's own "observed" check
              already assumes this for a different purpose), which is the
              same assumption the rest of this codebase already leans on. *)
           let temporal_office_slug = d.Liturgical_day.temporal.Temporal.office.Celebration.slug in
           let as_candidates comms =
             List.map
               (fun (c, p) ->
                 let origin =
                   if Slug.equal c.Celebration.slug temporal_office_slug then Precedence.Temporal
                   else Precedence.Sanctoral
                 in
                 let cand : 'r Precedence.candidate = { Precedence.cel = c; origin } in
                 (cand, p, rite.Rite.rules.Precedence.band day_ctx cand))
               comms
           in
           let offered = as_candidates d.Liturgical_day.commemorations in
           let readmitted =
             rite.Rite.rules.Precedence.admit ~observed:observed_candidate
               ~temporal:temporal_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
           let offered_pairs = List.map (fun (c, p, _) -> (c, p)) offered in
           if norm readmitted <> norm offered_pairs 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;
       (* ---- Citation invariants (the lectionary, Plan 4) ----

          RITE-AGNOSTIC BY CONSTRUCTION, and this gating is the whole reason
          these can live in the kernel beside the temporal checks rather than
          in EF's own tests: a rite whose lectionary is not built yet returns
          [] from {!Rite.readings} on every day, so [year_has_citations] is
          false and not one of these fires. A rite that computes readings AT
          ALL is held to all of them, on every day of its year. That is also
          why test_validate.ml's own synthetic rite ([readings] a constant
          [], "a harmless placeholder" in its own words) stays unaffected --
          checked, not assumed: its negative-path fixtures would otherwise
          fail on every day of the year rather than on the one invariant each
          is built to violate.

          The single [match] below expresses THREE invariants at once, which
          is why it is a match on the sorted part list rather than three
          separate tests:

            - zero or two, never one -- an Epistle without a Gospel, or the
              reverse, is a malformed Mass, not a partial one;
            - only [First] and [Gospel] ever appear -- the chants (Psalm,
              Second, Tract, Alleluia, Sequence) are deliberately unbuilt,
              with no source and no oracle, so a citation carrying one is a
              defect and not a feature arriving early;
            - no part appears twice -- two Epistles and no Gospel has length
              two and would slip past a bare cardinality test.

          [Citation.part]'s own constructor order puts [First] before
          [Gospel], so the sorted well-formed list is literally
          [[First; Gospel]] and nothing else. *)
       let year_has_citations =
         Array.exists
           (fun (d : ('s, 'r) Liturgical_day.t) -> d.Liturgical_day.citations <> [])
           resolved
       in
       if year_has_citations then
         Array.iter
           (fun (d : ('s, 'r) Liturgical_day.t) ->
             let date = d.Liturgical_day.date in
             let parts =
               List.map (fun (c : Citation.t) -> c.Citation.part) d.Liturgical_day.citations
             in
             match List.sort compare parts with
             | [ Citation.First; Citation.Gospel ] -> ()
             | [] ->
                 (* Separate check name from the malformed case below on
                    purpose: this is the lectionary chain falling through
                    every one of its steps and resolving nothing, a COVERAGE
                    gap, where the other is a WELL-FORMEDNESS one. They want
                    different fixes and should be countable apart. *)
                 fail date "citations-unresolved"
                   "no reading citations resolved for this day: the lectionary chain fell through \
                    every step"
             | sorted ->
                 fail date "citations"
                   (Printf.sprintf "expected exactly one First and one Gospel, got [%s]"
                      (String.concat "," (List.map Citation.part_to_string sorted))))
           resolved);
  List.rev !failures