path: root/test/test_validate.ml

module Val = Colitur_kernel.Validate
module Rite = Colitur_kernel.Rite
module P = Colitur_kernel.Precedence
module Layer = Colitur_kernel.Layer
module Overlay = Colitur_kernel.Overlay
module Citation = Colitur_kernel.Citation
module V = Rite_ef.Vocab_ef
module T = Rite_ef.Temporal_ef

(* Task 12 widens Validate.run to take a resolved layer -- Precedence_ef and
   Calendar (Tasks 5-11) now exist, so the REAL EF rite (Rite_ef.context) and
   its REAL bootstrapped data replace the earlier placeholder rules/layer-less
   Rite.t this module used before Plan 3's resolution engine was built.
   Relative to this test's own build directory (_build/default/test/), same
   convention test_rite_ef.ml already uses -- test/dune declares both as deps
   of the (test ...) stanza. *)
let sanctoral_path = "../data/ef/sanctoral.sexp"
let adjustments_path = "../data/ef/adjustments.sexp"
let lectionary_path = "../data/ef/lectionary.sexp"
let commons_path = "../data/ef/commons.sexp"

(* Loaded once at module init, not per call: [run] below is called by every
   test and by the 200-sample property, and Calendar.year's own resolution
   cost already dominates -- there is no reason to also re-parse a 322-entry
   sexp file on every one of those calls. *)
let real_ef_layer =
  match Layer.load V.rank_of_sexp sanctoral_path with
  | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" sanctoral_path e)
  | Ok layer -> (
      match Overlay.load V.rank_of_sexp adjustments_path with
      | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" adjustments_path e)
      | Ok overlay ->
          let layer, diagnostics = Overlay.apply layer overlay in
          if diagnostics <> [] then
            failwith
              (Printf.sprintf "unexpected overlay diagnostics: %s"
                 (String.concat "; " (List.map Overlay.diagnostic_to_string diagnostics)));
          layer)

(* [Rite_ef.context] takes [~lectionary] (fix round 1, coordinator review) --
   caller-supplied, same as [real_ef_layer] above. *)
let real_ef_lectionary =
  match Colitur_kernel.Lectionary.load lectionary_path with
  | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" lectionary_path e)
  | Ok l -> l

(* The Commons (data/ef/commons.sexp) travel the same caller-supplied seam
   as the lectionary above, and [~commons] is required rather than defaulted
   so that no caller can silently run with none -- nothing in layers 3-5
   compares reading citations, so a rite quietly missing its Commons would
   be invisible. Loaded here even where this file asserts nothing about
   readings, so that the rite under test is the same one bin/main.ml
   assembles. *)
let real_ef_commons =
  match Rite_ef.Lectionary_ef.Commons.load commons_path with
  | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" commons_path e)
  | Ok c -> c

let real_ef_rite = Rite_ef.context ~lectionary:real_ef_lectionary ~commons:real_ef_commons

let run year = Val.run real_ef_rite real_ef_layer ~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 ]

(* Register finding 2 / controller finding B: [Validate.run ~year:9999] used
   to raise ([year_start (year + 1)] asks for civil year 10000, out of the
   kernel's domain), even though 9999 is in range and kernel computation must
   never raise on in-range input. [run] now clamps its scan to 31 Dec 9999
   instead. Calling [run 9999] directly (no [try]) is itself part of the
   pin: if the clamp regressed, this call would raise and the test would
   error. The clamped scan only covers Advent and the start of Christmastide,
   so it is *expected* to report the season run as incomplete -- this pins
   that the incompleteness surfaces as an ordinary "seasons" failure, not an
   uncaught exception, and that nothing else broke in the process. *)
let test_year_9999_does_not_raise () =
  let fs = run 9999 in
  Alcotest.(check bool) "no coverage failures (temporal stayed total through the clamp)" true
    (not (List.exists (fun f -> f.Val.check = "coverage") fs));
  Alcotest.(check bool) "seasons check flags the truncated final year as incomplete" true
    (List.exists (fun f -> f.Val.check = "seasons") fs)

(* 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
  (* Both extremes genuinely occur in 1583..2500 (earliest 1598, latest
     1666 -- verified against Computus.gregorian_easter directly, not
     transcribed). CORRECTED (final fix wave, item 7): this used to assert
     only [List.length ys = 2], a cardinality check where an identity check
     was called for -- the comment already named 1598 and 1666, but nothing
     confirmed [ys] actually contained THOSE two years rather than some
     other pair the search happened to find first; a version of
     [extreme_years] that silently found the wrong two years but still
     found exactly two would have passed this unchanged. Asserting the
     identities directly is strictly stronger and costs nothing extra. *)
  Alcotest.(check (list int)) "found exactly 1598 (earliest 22 Mar) and 1666 (latest 25 Apr)"
    [ 1598; 1666 ] 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 = [])

(* ---- final fix wave, item 6: the exhaustive sweep, committed ----

   The property above samples 200 of 8 416 years (2.4% of the domain) on a
   RANDOM seed -- QCheck.Test.make with no ~seed argument draws a fresh one
   from the environment/OS entropy each run, and two consecutive runs of
   this suite were observed using different seeds (see the task report for
   the transcript). CLAUDE.md's standing claim that Validate is "clean
   across all 8 416 years -- exhaustive, not sampled" was true whenever it
   was last actually re-run in full, but no committed artifact pinned it,
   and a year-specific regression (one bad year among 8 416) would show up
   in this suite only intermittently -- roughly 200/8416 of the time per
   run, i.e. most runs would NOT catch it.

   This is that committed artifact: every year 1583..9999, not a sample.
   Tagged `Slow (matching this file's own naming for the check it performs
   -- see [suite] below), but Alcotest's speed-level filtering is deliberately
   NOT used to keep it out of the default `dune test`: that filtering (the
   `-q`/`--quick-tests` flag, or dune wiring the runtest action to pass it)
   is ALL-OR-NOTHING per speed level, and this codebase already tags SIX
   OTHER cases `Slow -- the two pre-existing exhaustive Computus checks
   (test_computus.ml, both genuinely fast, sub-second) AND, found while
   implementing this item, EVERY QCheck property in the whole suite
   (test_date.ml x3, test_overlay.ml, test_temporal_ef.ml, and
   [prop_invariants] immediately above, since QCheck_alcotest.to_alcotest
   defaults ~speed_level to `Slow when not given explicitly, which none of
   this codebase's call sites do). Wiring `-q` at the dune level was tried
   and reverted: it made the default `dune test` report 251 tests instead
   of (the then-current) 260, silently excluding [prop_invariants] itself
   -- the "confidence-to-9999" mechanism CLAUDE.md documents as this
   project's central property-testing story -- along with five other
   properties, none of which this task asked to remove from the fast path.
   That is a far bigger, unintended regression than the one line this item
   asks to add.

   Instead, this test gates its OWN expensive body on an environment
   variable, [COLITUR_EXHAUSTIVE_SWEEP], and calls {!Alcotest.skip} (marked
   SKIPPED, not silently passed, when unset) so `dune test`'s default run
   stays at its normal speed and reports the skip honestly rather than a
   vacuous green. To run the real sweep (~35-45s, see the report for the
   measured figure):

     COLITUR_EXHAUSTIVE_SWEEP=1 dune test --force

   or invoke the built executable directly with the same variable set. *)
let colitur_exhaustive_sweep_env = "COLITUR_EXHAUSTIVE_SWEEP"

(* 9999 is a documented, non-regression truncation, not a fresh finding:
   [test_year_9999_does_not_raise] above already pins that [run 9999]
   reports exactly a "seasons" failure (the domain's own ceiling truncates
   the scan mid-Christmastide) and nothing else -- reused here rather than
   calling [check_year] on 9999, which would fail this sweep on a shape
   that is not a regression. *)
let test_exhaustive_domain_sweep () =
  if Sys.getenv_opt colitur_exhaustive_sweep_env = None then Alcotest.skip ()
  else begin
    for y = 1583 to 9998 do
      check_year y
    done;
    let fs = run 9999 in
    Alcotest.(check bool) "9999: no coverage failures (temporal stayed total through the clamp)" true
      (not (List.exists (fun f -> f.Val.check = "coverage") fs));
    Alcotest.(check bool) "9999: seasons check flags the truncated final year as incomplete" true
      (List.exists (fun f -> f.Val.check = "seasons") fs);
    Alcotest.(check (list string)) "9999: nothing OTHER than the documented seasons truncation fired"
      [ "seasons" ]
      (List.sort_uniq compare (List.map (fun f -> f.Val.check) fs))
  end

(* ---- negative-path fixture (Task 14 review, finding 1) ----

   Everything above only exercises the CLEAN path against real EF data: an
   empty failure list. That leaves nothing committed proving each check can
   actually fire -- a future edit that quietly weakens a check would still
   leave this suite green, since a weaker check only makes more inputs pass.

   This is a small, synthetic two-season, two-rank rite -- not EF -- built so
   each mutation below can violate exactly one invariant directly, rather
   than corrupting real rite data. [Validate] is rite-agnostic by design;
   this is that design's second "rite", proving the abstraction and the
   checks both hold up away from EF specifically. *)
module Synthetic = struct
  module D = Colitur_kernel.Date
  module Vocab = Colitur_kernel.Vocab
  module Cel = Colitur_kernel.Celebration
  module Slug = Colitur_kernel.Slug
  module Colour = Colitur_kernel.Colour
  module Temporal = Colitur_kernel.Temporal
  module P = Colitur_kernel.Precedence
  module Rite = Colitur_kernel.Rite
  module Layer = Colitur_kernel.Layer
  module Date_spec = Colitur_kernel.Date_spec

  type season = A | B
  type rank = R1 | R2

  let season_to_string = function A -> "a" | B -> "b"
  let season_of_string = function "a" -> Some A | "b" -> Some B | _ -> None
  let rank_to_string = function R1 -> "r1" | R2 -> "r2"
  let rank_of_string = function "r1" -> Some R1 | "r2" -> Some R2 | _ -> None

  let vocab : (season, rank) Vocab.t =
    { Vocab.seasons = [ A; B ]; season_to_string; season_of_string;
      ranks = [ R1; R2 ]; rank_to_string; rank_of_string }

  (* A vocab whose declared rank list omits R2 -- a realistic
     documentation/data-drift scenario. (Fabricating an out-of-type rank
     instead would need [Obj.magic] on a two-constructor variant, which is
     undefined behaviour the moment anything pattern-matches it -- see the
     colour mutation below, where that risk is called out explicitly.) *)
  let vocab_missing_rank = { vocab with Vocab.ranks = [ R1 ] }

  (* Register finding 8: rank_to_string collapsing two distinct ranks to the
     same string, and season_to_string doing the same -- a realistic
     documentation/data-drift scenario distinct from [vocab_missing_rank]
     above (that one omits a rank entirely; these make two indistinguishable
     instead). *)
  let vocab_collapsed_ranks = { vocab with Vocab.rank_to_string = (fun _ -> "same") }
  let vocab_collapsed_seasons = { vocab with Vocab.season_to_string = (fun _ -> "same") }

  (* The placeholder ruleset every TEMPORAL-only fixture below still uses:
     paired with the default empty [layer] (see [rite] below), there is never
     a sanctoral candidate for these three functions to be called against, so
     what they return is moot for those tests -- only the Task 12 resolution
     fixtures further down override [rules] (and supply a non-empty
     [layer]), each with its own small, deliberately-shaped ruleset. *)
  let rules : (season, rank) P.rules =
    { P.vigil_feast = (fun _ -> None); band = (fun _ _ -> 0);
      disposition = (fun ~winner:_ ~loser:_ -> P.Omit);
      admit = (fun ~observed:_ ~temporal:_ _ -> []) }

  let year_start y = match D.make ~year:y ~month:1 ~day:1 with Ok d -> d | Error e -> failwith e

  let weekday_index d =
    match D.weekday d with
    | D.Sun -> 0 | D.Mon -> 1 | D.Tue -> 2 | D.Wed -> 3 | D.Thu -> 4 | D.Fri -> 5 | D.Sat -> 6

  let sunday_on_or_before d = D.add_days d (-(weekday_index d))

  (* The first Sunday on or after 1 July: where season B and its own week
     origin begin. *)
  let split_date y =
    let jul1 = match D.make ~year:y ~month:7 ~day:1 with Ok d -> d | Error e -> failwith e in
    D.add_days jul1 ((7 - weekday_index jul1) mod 7)

  let floor_div a b = if a >= 0 then a / b else ((a + 1) / b) - 1

  (* The clean baseline: season A from New Year's Day to the Saturday before
     [split_date], season B from [split_date] onward. Both season-run origins
     are Sundays, so weeks are Sunday-aligned and non-decreasing throughout --
     this is what a zero-failure [Validate.run] looks like for a rite that
     actually is clean. *)
  let good d =
    let y = D.year d in
    let s = if D.compare d (split_date y) < 0 then A else B in
    let origin = if s = A then sunday_on_or_before (year_start y) else split_date y in
    let n = floor_div (D.to_rata d - D.to_rata origin) 7 + 1 in
    let slug = Printf.sprintf "syn-%s-%d" (season_to_string s) (D.to_rata d) in
    let rank = if D.weekday d = D.Sun then R1 else R2 in
    { Temporal.season = s; week = Some n; weekday = D.weekday d;
      office = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.Green ~layer:"synthetic" () }

  (* The one day each mutation below corrupts. Genuinely mid-week (Tuesday,
     not the Sunday that "2026-03-15" actually is despite the comment this
     replaces having claimed otherwise -- register finding 12): not a
     Sunday, and not New Year's Day or the season split, so it sits safely
     mid-run for every check that cares about run position. *)
  let target = match D.make ~year:2026 ~month:3 ~day:17 with Ok d -> d | Error e -> failwith e

  (* Register finding 3: the rite's own independent restatement of one fixed
     anchor -- [target]'s date, paired with the slug [good] already gives it
     -- so the anchor-agreement check has something non-trivial to check in
     this synthetic rite too, not only in EF. *)
  let anchors _y = [ (Slug.to_string (good target).Temporal.office.Cel.slug, target) ]

  (* Task 12: [rite] now also takes [rules]/[transfer_target] (defaulting to
     the placeholder above and to "stand still", respectively -- harmless
     defaults against the default empty [layer], since nothing ever contests
     the temporal office there) so the resolution fixtures further down can
     override them without duplicating every other field. *)
  (* Most fixtures here exercise no citations and no formulary -- [readings]
     is a harmless constant [(None, [])], the same role the other
     placeholder defaults above play, and {!Validate}'s own citation and
     formulary checks are gated on a rite producing SOME citation/formulary
     somewhere, so a constant [(None, [])] leaves them entirely dormant. Task
     10 makes it overridable ([?readings] below) so the citation fixtures at
     the end of this file can drive those checks directly, exactly as every
     other check here is driven -- rather than leaving kernel checks with no
     committed proof that they can fire at all. *)
  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = (None, [])

  (* The shape {!Validate} accepts: exactly one First and one Gospel. The
     references are deliberately nonsense -- these fixtures assert SHAPE,
     never content. *)
  let well_formed_citations =
    [ { Citation.part = Citation.First; reference = "Synth 1:1" };
      { Citation.part = Citation.Gospel; reference = "Synth 2:2" } ]

  (* The formulary equivalent of [well_formed_citations] above -- shape only,
     never rubrically meaningful content. *)
  let well_formed_formulary =
    { Colitur_kernel.Mass_formulary.said = Some (Slug.of_string_exn "syn-formulary");
      via = Colitur_kernel.Mass_formulary.Own_slug }

  (* No fixture here exercises the Creed or Gloria rubrics -- a rite that
     has not implemented them returns [false] explicitly,
     {!Rite.t.creed}/{!Rite.t.gloria}'s own documented default. Made
     overridable ([?creed]/[?gloria] below) on the same footing as
     [?readings] just above, for Task 6's own fixtures. *)
  let creed ~temporal:_ ~observed:_ ~date:_ = false
  let gloria ~temporal:_ ~observed:_ ~date:_ = false

  let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) ?(rules = rules)
      ?(transfer_target = fun _ origin _ -> origin) ?(readings = readings) ?(creed = creed)
      ?(gloria = gloria) temporal : (season, rank) Rite.t =
    { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs;
      (* Not a Roman rite, but a Rite.t must supply SOME Easter now that
         movable Date_spec variants exist. The Gregorian one is as good as
         any for a fixture; nothing here is Easter-relative, so the value
         is never actually read. *)
      easter = Colitur_kernel.Computus.gregorian_easter;
      (* Not a Roman rite either, so no bissextile-doubling convention:
         identity, {!Rite.t.fixed_key}'s own documented default. *)
      fixed_key = (fun d -> Some (D.month d, D.day d));
      transfer_target; readings; creed; gloria }

  (* Empty by default: every check built before Task 12 exercises the
     TEMPORAL-only pass, where an empty layer is exactly the fixture that
     leaves it unable to affect anything ([Precedence.resolve] against no
     sanctoral candidates always just observes the temporal office
     unchallenged). Task 12's own resolution fixtures pass their own. *)
  let empty_layer = Layer.empty ~id:"synthetic-empty" ~name:"empty"

  let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?readings ?(layer = empty_layer)
      temporal =
    Val.run
      (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target ?readings temporal)
      layer ~year:2026

  let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs

  (* A rite whose season B legitimately appears in two separate runs: the
     civil year is split into calendar quarters, seasons alternating A B A B
     -- as the modern form's Ordinary Time does (January-Ash Wednesday, then
     Pentecost-Advent, with Lent/Easter and Advent/Christmas between). Each
     quarter gets its own Sunday-aligned week origin, exactly as [good] does
     for its own two runs, so every other invariant (weekday, week
     numbering, rank, colour, determinism) stays clean and only the season
     check is actually exercised. *)
  let quarter_start y i =
    match D.make ~year:y ~month:(1 + (i * 3)) ~day:1 with Ok d -> d | Error e -> failwith e

  let quarter_index d = (D.month d - 1) / 3

  let two_run_temporal d =
    let y = D.year d in
    let qi = quarter_index d in
    let s = if qi mod 2 = 0 then A else B in
    let origin = sunday_on_or_before (quarter_start y qi) in
    let n = floor_div (D.to_rata d - D.to_rata origin) 7 + 1 in
    let slug = Printf.sprintf "syn2-%s-%d" (season_to_string s) (D.to_rata d) in
    let rank = if D.weekday d = D.Sun then R1 else R2 in
    { Temporal.season = s; week = Some n; weekday = D.weekday d;
      office = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.Green ~layer:"synthetic" () }

  let rite_with_two_runs : (season, rank) Rite.t =
    rite ~season_runs:[ A; B; A; B ] two_run_temporal

  (* ---- Task 12: resolution-level fixtures ----

     Everything above only ever drives the TEMPORAL-only pass: [run]'s
     default [layer] is empty, so [Precedence.resolve] never has a sanctoral
     candidate to contest against the temporal office, and [rules]/
     [transfer_target] are never meaningfully exercised. These five fixtures
     instead give [Calendar.year] real work -- a non-empty [layer] plus a
     small, deliberately-shaped [rules] (and, for two of them,
     [transfer_target]) -- each built so its OWN check label fires. Four of
     the five fire in clean isolation (the other four Task 12 labels stay
     silent); the fifth (["unconverged"]) genuinely also fires
     ["duplicated"] alongside it, a real consequence of Calendar's own round-
     guard accounting, not a fixture design flaw -- see guard_rules's own
     comment. Every fixture's isolation (or lack of it) was verified by
     hand-tracing [Calendar]'s resolution mechanics BEFORE writing its
     assertion (see the task report), not inferred from what the assertion
     happens to require -- the tests below check that trace against the
     actual engine output, one fixture at a time. [good] is reused,
     unchanged, as every fixture's [temporal]: only [rules]/[layer]/
     [transfer_target] vary, so the temporal-only checks (already proven
     clean against [good] by [test_synthetic_baseline_is_clean]) cannot be
     what fires here. *)

  let mk_entry ~month ~day ~slug ~rank =
    { Layer.date = (match Date_spec.fixed ~month ~day with Ok d -> d | Error e -> failwith e);
      cel = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.White
              ~layer:"synthetic-sanctoral" () }

  let task12_checks = [ "observed"; "lost"; "duplicated"; "unconverged"; "admission" ]

  (* The Task-12-owned subset of a failure list's own check labels, as a
     sorted, de-duplicated set -- what each isolation assertion below
     compares against, so a fixture that (by mistake) also trips an
     unrelated Task-12 check shows up as a wrong set, not a silently-passing
     [has_check]. *)
  let fired_task12_checks (fs : Val.failure list) =
    List.filter_map (fun f -> if List.mem f.Val.check task12_checks then Some f.Val.check else None) fs
    |> List.sort_uniq compare

  (* "duplicated": a single ordinary sanctoral entry, always losing to the
     temporal office (band: Temporal 0 < Sanctoral 10, unconditionally) and
     always Commemorate-disposed. [admit]'s bug is exactly the shape
     precedence_ef.mli's own [admit] contract warns against ("a value taken
     unchanged from comms, never rebuilt"): it REBUILDS every admitted pair
     via a record update, allocating a fresh, structurally-identical-but-
     physically-distinct candidate. Precedence.resolve's own [dropped]
     computation tells an admitted candidate from a dropped one by PHYSICAL
     equality, so the rebuild defeats it -- the one candidate ends up counted
     as both admitted (in [commemorations]) and dropped (in [omitted],
     "admission limit reached"): two sightings for one Date_spec
     resolution. *)
  let dup_entry = mk_entry ~month:5 ~day:5 ~slug:"dup-target" ~rank:R2
  let dup_layer = Layer.of_entries ~id:"dup" ~name:"dup" [ dup_entry ]

  let dup_rules : (season, rank) P.rules =
    { P.vigil_feast = (fun _ -> None); band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10);
      disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary);
      admit =
        (fun ~observed:_ ~temporal:_ cs ->
          List.map (fun (c, p, (_ : int)) -> ({ c with P.origin = c.P.origin }, p)) cs) }

  (* "unconverged": two entries collide on one date (6 June), both beating
     the temporal office and tied with each other, so slug decides:
     "guard-aaa" wins the day outright every time, "guard-zzz" is always the
     loser there and always Transfer-disposed. Paired with a
     [transfer_target] that always answers with the impeded day itself --
     never strictly forward -- this is the exact non-terminating shape
     test_calendar.ml's own
     [test_transfer_guard_records_failure_instead_of_looping] proves hits
     Calendar's round guard: "guard-zzz", re-injected into 6 June every
     round, can never win it (it always loses the tie to the natural
     "guard-aaa" copy already sitting there), so [deferred] never empties.

     GENUINE FINDING (see the task report): this ALSO fires "duplicated", not
     "unconverged" alone. Once the guard is hit, [build_day]'s final resolve
     at 6 June sees "guard-zzz" TWICE -- once as the permanent natural entry
     (which never stops losing there) and once as whatever the last round's
     [injected] state still holds for it -- and [unresolved] is evaluated per
     CANDIDATE OBJECT, not per slug, so BOTH copies land in [omitted] with
     the unconverged reason. Nothing is lost (both copies carry a recorded
     reason), but the slug is sighted twice against one Date_spec resolution,
     which is exactly what "duplicated" is for. The same double-recording is
     latent in test_calendar.ml's own guard fixture too (day_winner/eclipsed
     at 20 Dec, structurally identical) -- untested there only because that
     test uses [List.exists], not a count. Calendar's round guard is
     documented as "nothing in the 1962 calendar is expected to trigger"
     (calendar.ml), so this is a latent accounting quirk in an unreachable
     path, not a live bug, and calendar.ml is out of this task's file list --
     reported, not fixed here. *)
  let guard_winner_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-aaa" ~rank:R1
  let guard_loser_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-zzz" ~rank:R1
  let guard_layer = Layer.of_entries ~id:"guard" ~name:"guard" [ guard_winner_entry; guard_loser_entry ]

  let guard_rules : (season, rank) P.rules =
    { P.vigil_feast = (fun _ -> None); band = (fun _ c -> match c.P.origin with P.Temporal -> 50 | P.Sanctoral -> 10);
      disposition =
        (fun ~winner:_ ~loser ->
          match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary);
      admit = (fun ~observed:_ ~temporal:_ cs -> List.map (fun (c, p, (_ : int)) -> (c, p)) cs) }

  let guard_transfer_target (_ : rank P.candidate) (origin : D.t) (_ : D.t -> rank Cel.t) = origin

  (* "admission": three entries collide on one date (9 September), all
     losing to the temporal office (band: Temporal 0 < Sanctoral 10) and all
     Commemorate-disposed -- a genuine 3-candidate offer to [admit]. The bug:
     cap 2 when the offer's length is ODD, cap 1 when EVEN -- a length-keyed
     rule with no liturgical meaning, chosen as the simplest function that is
     NOT idempotent on its own output (offer 3, admit 2; re-offer those same
     2, admit only 1) while staying idempotent -- and so invisible -- on
     every OTHER shape this suite exercises (never offered exactly 2 or 3
     candidates elsewhere), including its own clean 3-candidate day. *)
  let adm_a_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-a" ~rank:R2
  let adm_b_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-b" ~rank:R2
  let adm_c_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-c" ~rank:R2
  let adm_layer = Layer.of_entries ~id:"adm" ~name:"adm" [ adm_a_entry; adm_b_entry; adm_c_entry ]

  let adm_compare_slug (c1, _, _) (c2, _, _) = Slug.compare c1.P.cel.Cel.slug c2.P.cel.Cel.slug

  let rec adm_take n = function
    | [] -> []
    | x :: xs -> if n <= 0 then [] else x :: adm_take (n - 1) xs

  let adm_rules : (season, rank) P.rules =
    { P.vigil_feast = (fun _ -> None); band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10);
      disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary);
      admit =
        (fun ~observed:_ ~temporal:_ cs ->
          let sorted = List.stable_sort adm_compare_slug cs in
          let taken = if List.length sorted mod 2 = 1 then adm_take 2 sorted else adm_take 1 sorted in
          List.map (fun (c, p, (_ : int)) -> (c, p)) taken) }

  (* "observed": two DIFFERENT layer entries sharing one slug -- a realistic
     data mistake (a renamed or duplicated entry), not prevented by
     [Layer.t]'s own type. [collide_a] (1 Feb, rank R1) always loses on its
     OWN date: [band] makes the temporal office win there specifically (5,
     beating R1's 10) and lose everywhere else (50), so [collide_a] is always
     Transfer-disposed at 1 Feb. Its constant [transfer_target] sends it to
     10 Feb -- [collide_b]'s own home date -- where [collide_a]'s rank R1
     (band 10) now beats both the temporal office (50, since the date is no
     longer 1 Feb) and [collide_b]'s own rank R2 (band 90): the ARRIVING
     [collide_a] wins 10 Feb outright, and [collide_b] -- same slug as the
     new winner -- is Commemorate-disposed (R2) right alongside it. One day
     ends up reporting the same slug as both its observed celebration and one
     of its own commemorations. *)
  let collide_d1 = match D.make ~year:2026 ~month:2 ~day:1 with Ok d -> d | Error e -> failwith e
  let collide_a_entry = mk_entry ~month:2 ~day:1 ~slug:"collide-x" ~rank:R1
  let collide_b_entry = mk_entry ~month:2 ~day:10 ~slug:"collide-x" ~rank:R2
  let collide_layer = Layer.of_entries ~id:"collide" ~name:"collide" [ collide_a_entry; collide_b_entry ]

  let collide_rules : (season, rank) P.rules =
    { P.vigil_feast = (fun _ -> None); band =
        (fun ctx c ->
          match c.P.origin with
          | P.Temporal -> if D.compare ctx.P.date collide_d1 = 0 then 5 else 50
          | P.Sanctoral -> ( match c.P.cel.Cel.rank with R1 -> 10 | R2 -> 90));
      disposition =
        (fun ~winner:_ ~loser ->
          match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary);
      admit = (fun ~observed:_ ~temporal:_ cs -> List.map (fun (c, p, (_ : int)) -> (c, p)) cs) }

  let collide_d2 = match D.make ~year:2026 ~month:2 ~day:10 with Ok d -> d | Error e -> failwith e
  let collide_transfer_target (_ : rank P.candidate) (_ : D.t) (_ : D.t -> rank Cel.t) = collide_d2

  (* A genuinely resolved, well-behaved day (one ordinary sanctoral entry,
     cleanly losing and commemorated, nothing transferred) -- proving the
     five checks stay silent against REAL resolution machinery, not merely
     against the default empty [layer] every fixture above this section
     uses. Without this, "no check fires" would only ever have been shown
     for a layer with nothing in it. *)
  let clean_sanctoral_entry = mk_entry ~month:8 ~day:8 ~slug:"clean-saint" ~rank:R2
  let clean_sanctoral_layer = Layer.of_entries ~id:"clean" ~name:"clean" [ clean_sanctoral_entry ]

  let clean_sanctoral_rules : (season, rank) P.rules =
    { P.vigil_feast = (fun _ -> None); band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10);
      disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary);
      admit = (fun ~observed:_ ~temporal:_ cs -> List.map (fun (c, p, (_ : int)) -> (c, p)) cs) }
end

open Synthetic

let test_synthetic_baseline_is_clean () =
  Alcotest.(check bool) "clean synthetic fixture has no failures" true (run good = [])

(* The point of this task: a rite whose season B genuinely appears in two
   separate runs (quarters 0,1,2,3 give season sequence A B A B, not a single
   A-then-B pair) validates clean when [season_runs] says so. Before this
   task, [Validate]'s season check hardcoded "compressed = vocab.seasons"
   ([A; B]) with no way to say otherwise -- against that check this fixture's
   compressed sequence, [A; B; A; B], would never match and every year would
   report a spurious "seasons" failure. *)
let test_two_run_season_is_accepted () =
  let r = Synthetic.rite_with_two_runs in
  Alcotest.(check (list string)) "no failures" []
    (List.map Val.failure_to_string (Val.run r Synthetic.empty_layer ~year:2026))

let test_coverage_fires () =
  let temporal d = if D.compare d target = 0 then failwith "boom" else good d in
  Alcotest.(check bool) "coverage check fires when temporal raises" true
    (has_check "coverage" (run temporal))

let test_seasons_fires () =
  let temporal d =
    let t = good d in
    let y = D.year d in
    let flip_after = match D.make ~year:y ~month:9 ~day:1 with Ok d -> d | Error e -> failwith e in
    (* Season A reappears after B: breaks the expected [A; B] run sequence. *)
    if D.compare d flip_after >= 0 then { t with Temporal.season = A } else t
  in
  Alcotest.(check bool) "seasons check fires when a season recurs outside season_runs" true
    (has_check "seasons" (run temporal))

let test_week_fires () =
  let temporal d =
    let t = good d in
    (* A single mid-run day's week drops below the day before it. *)
    if D.compare d target = 0 then { t with Temporal.week = Some 1 } else t
  in
  Alcotest.(check bool) "week check fires when a week number decreases mid-run" true
    (has_check "week" (run temporal))

let test_weekday_fires () =
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then
      { t with Temporal.weekday = (if t.Temporal.weekday = D.Sun then D.Mon else D.Sun) }
    else t
  in
  Alcotest.(check bool) "weekday check fires when it disagrees with Date.weekday" true
    (has_check "weekday" (run temporal))

let test_rank_fires () =
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then { t with Temporal.office = { t.Temporal.office with Cel.rank = R2 } }
    else { t with Temporal.office = { t.Temporal.office with Cel.rank = R1 } }
  in
  Alcotest.(check bool) "rank check fires when a rank is absent from the declared vocab" true
    (has_check "rank" (run ~vocab:vocab_missing_rank temporal))

let test_colour_fires () =
  (* Unlike rank, colour isn't rite-parameterised -- [Colour.t] is closed over
     exactly six constructors, all listed in [Colour.all], so no rite's own
     data can ever name a seventh. There is no type-safe way to construct an
     invalid one, so this is the one mutation that reaches for [Obj.magic] --
     safely here, because the colour check compares by structural equality
     ([List.mem], no pattern match), unlike [rank_to_string], which would hit
     undefined behaviour on an out-of-range tag (why the rank mutation above
     goes through an incomplete vocab list instead of doing the same trick). *)
  let bogus_colour : Colour.t = Obj.magic 99 in
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then { t with Temporal.office = { t.Temporal.office with Cel.colour = bogus_colour } }
    else t
  in
  Alcotest.(check bool) "colour check fires when the colour is outside Colour.all" true
    (has_check "colour" (run temporal))

(* Register finding 3 (§5.8 determinism). [target] alternates what it
   returns across successive calls with the same date -- everything else is
   [good], genuinely pure -- so the first call (feeding the season/week/etc.
   checks) and [run]'s own repeated call (the determinism check itself) see
   different results for that one date. *)
let test_determinism_fires () =
  let calls = ref 0 in
  let temporal d =
    if D.compare d target = 0 then begin
      incr calls;
      let t = good d in
      if !calls mod 2 = 0 then { t with Temporal.week = Some 999 } else t
    end
    else good d
  in
  Alcotest.(check bool) "determinism check fires when a repeated call returns a different result" true
    (has_check "determinism" (run temporal))

(* Register finding 3 (§5.7 anchor agreement). *)
let test_anchor_clean () =
  Alcotest.(check bool) "the rite's own anchor list agrees with its own temporal, so no anchor failures"
    true (not (has_check "anchor" (run ~anchors good)))

let test_anchor_fires () =
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then
      { t with Temporal.office = { t.Temporal.office with Cel.slug = Slug.of_string_exn "syn-wrong-anchor" } }
    else t
  in
  Alcotest.(check bool) "anchor check fires when temporal disagrees with the rite's own anchor list" true
    (has_check "anchor" (run ~anchors temporal))

let test_vocab_rank_injectivity_fires () =
  Alcotest.(check bool) "vocab check fires when rank_to_string collapses two ranks to one string" true
    (has_check "vocab" (run ~vocab:vocab_collapsed_ranks good))

let test_vocab_season_injectivity_fires () =
  Alcotest.(check bool) "vocab check fires when season_to_string collapses two seasons to one string" true
    (has_check "vocab" (run ~vocab:vocab_collapsed_seasons good))

(* Plan 2 carried item 4: slug uniqueness moves into [Validate] itself, no
   exemption. [target] (17 March, mid-run) is given the NEXT day's real slug
   verbatim -- a genuine collision between two distinct dates in the same
   walked year, touching only the [slug] field so every other check (season,
   week, weekday, rank, colour, determinism, anchor) stays silent against it. *)
let test_slugs_fires () =
  let colliding_slug = (good (D.add_days target 1)).Temporal.office.Cel.slug in
  let temporal d =
    let t = good d in
    if D.compare d target = 0 then
      { t with Temporal.office = { t.Temporal.office with Cel.slug = colliding_slug } }
    else t
  in
  Alcotest.(check bool) "slugs check fires when two dates in the year share a slug" true
    (has_check "slugs" (run temporal))

(* ---- Task 12: resolution invariants ----

   Each test below asserts that exactly one of the five new check labels
   fires for its own dedicated fixture (Synthetic's own comments carry the
   hand-traced mechanics) -- not merely "at least this one", so a fixture
   that turns out to also trip an unrelated Task 12 check would fail loudly
   here rather than reading as accidental corroboration. *)

let test_lost_fires_on_resolution_exception () =
  (* Reuses [test_coverage_fires]'s own broken [temporal]: [Calendar.year]
     calls [rite.temporal] with no exception guard of its own (unlike the
     temporal-only pass above, which wraps every call), so the same raise
     that trips "coverage" also makes resolution itself raise -- the most
     total form of "silently lost" there is, per validate.mli. *)
  let temporal d = if D.compare d target = 0 then failwith "boom" else good d in
  Alcotest.(check (list string)) "only the lost check fires" [ "lost" ] (fired_task12_checks (run temporal))

let test_duplicated_fires () =
  Alcotest.(check (list string)) "only the duplicated check fires" [ "duplicated" ]
    (fired_task12_checks (run ~layer:dup_layer ~rules:dup_rules good))

let test_unconverged_fires () =
  (* Also asserts "duplicated" fires alongside it -- see guard_rules's own
     comment for why that is the genuine, hand-verified consequence of
     hitting the round guard here, not an isolation failure. *)
  Alcotest.(check (list string)) "unconverged fires, and duplicated alongside it"
    [ "duplicated"; "unconverged" ]
    (fired_task12_checks
       (run ~layer:guard_layer ~rules:guard_rules ~transfer_target:guard_transfer_target good))

let test_admission_fires () =
  Alcotest.(check (list string)) "only the admission check fires" [ "admission" ]
    (fired_task12_checks (run ~layer:adm_layer ~rules:adm_rules good))

let test_observed_fires () =
  Alcotest.(check (list string)) "only the observed check fires" [ "observed" ]
    (fired_task12_checks
       (run ~layer:collide_layer ~rules:collide_rules ~transfer_target:collide_transfer_target good))

(* The positive counterpart: a genuinely resolved, well-behaved day (real
   sanctoral entry, real contest, real commemoration) must report none of the
   five checks -- proven against actual resolution machinery, not only
   against every OTHER fixture's default empty layer. *)
let test_resolution_checks_clean_on_a_well_behaved_layer () =
  Alcotest.(check (list string)) "none of the five checks fire" []
    (fired_task12_checks (run ~layer:clean_sanctoral_layer ~rules:clean_sanctoral_rules good))

(* ---- Task 10: the citation invariants ----

   Two new kernel checks, and on real EF data NEITHER can fire: every day of
   every liturgical year 1583-9999 resolves exactly one Epistle and one
   Gospel (measured, not assumed -- the exhaustive sweep is clean, and the
   check was mutation-proved live rather than merely silent). That is the
   good outcome and precisely why these fixtures are needed: a check with no
   live witness and no negative-path test is indistinguishable from a check
   that does nothing, which is the trap this whole section of the file exists
   to avoid.

   All four drive the checks through [?readings], the same way every fixture
   above drives its own check through [?vocab]/[temporal]/[?rules]. *)

(* The gate itself, and the most load-bearing of the four: a rite that
   computes no readings AT ALL (the default constant [], every other fixture
   in this file, and any rite whose lectionary is simply not built yet) must
   report neither check -- not "usually", not "on this year". Without this,
   the natural implementation ("a day with no citations is a failure") would
   turn every unrelated fixture here red and, worse, would make [Validate]
   demand a lectionary of any rite that has none. *)
let test_citations_silent_without_a_lectionary () =
  let fs = run good in
  Alcotest.(check bool) "no citation check fires for a rite with no readings at all" false
    (has_check "citations" fs || has_check "citations-unresolved" fs)

(* The positive: well-formed citations on every day report nothing. *)
let test_citations_clean_when_well_formed () =
  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = (None, well_formed_citations) in
  let fs = run ~readings good in
  Alcotest.(check bool) "neither citation check fires when every day carries First + Gospel" false
    (has_check "citations" fs || has_check "citations-unresolved" fs)

(* Zero or two, never one: a lone Epistle is a malformed Mass. This is the
   invariant the plan names first, and the one a bootstrap bug would most
   plausibly produce -- half a lookup succeeding. *)
let test_citations_fires_on_a_lone_epistle () =
  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ =
    (None, [ { Citation.part = Citation.First; reference = "Synth 1:1" } ])
  in
  Alcotest.(check bool) "citations check fires when a day carries an Epistle but no Gospel" true
    (has_check "citations" (run ~readings good))

(* A part outside this plan's scope. The chants (Psalm/Second/Tract/Alleluia/
   Sequence) are deliberately unbuilt -- no source, no oracle -- so one
   appearing is a defect, not a feature arriving early, and must be caught
   even though the day is otherwise a well-formed pair. *)
let test_citations_fires_on_an_out_of_scope_part () =
  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ =
    (None, { Citation.part = Citation.Tract; reference = "Synth 3:3" } :: well_formed_citations)
  in
  Alcotest.(check bool) "citations check fires when a part outside First/Gospel appears" true
    (has_check "citations" (run ~readings good))

(* The coverage half, kept a SEPARATE check name from the three above: a rite
   that resolves readings on most days but falls through on one. On real EF
   data this has no witness at all, so this fixture is the only thing that
   holds it honest. [target] is the same mid-run day every other fixture in
   this file singles out. *)
let test_citations_unresolved_fires_on_a_gap () =
  let readings ~observed:_ ~temporal:_ ~date ~temporal_at:_ =
    if D.compare date target = 0 then (None, []) else (None, well_formed_citations)
  in
  Alcotest.(check bool) "citations-unresolved fires when one day of the year resolves nothing" true
    (has_check "citations-unresolved" (run ~readings good));
  (* ...and the well-formedness check must stay silent on that same run: the
     two are different faults and must not be reported as one. *)
  Alcotest.(check bool) "the well-formedness check stays silent on a pure coverage gap" false
    (has_check "citations" (run ~readings good))

(* ---------------------------------------------------------------------- *)
(* The formulary invariant (Task 3, celebrant-rubrics-phase1): the same    *)
(* negative-path discipline the citation checks above already hold        *)
(* themselves to, driven through the same synthetic fixture. Model on the  *)
(* citations trio above -- "same shape, its own name" is what {!Validate}  *)
(* itself now does, so the tests proving it can fire follow the same       *)
(* pattern. *)
(* ---------------------------------------------------------------------- *)

(* The gate: a rite that resolves no formulary at all (the default constant
   [(None, [])]) must report nothing -- not "usually", not "on this year". *)
let test_formulary_silent_without_a_lectionary () =
  let fs = run good in
  Alcotest.(check bool) "no formulary check fires for a rite with no readings at all" false
    (has_check "formulary" fs)

(* The positive: a formulary on every day reports nothing. *)
let test_formulary_clean_when_well_formed () =
  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ =
    (Some well_formed_formulary, well_formed_citations)
  in
  Alcotest.(check bool) "formulary check stays silent when every day resolves one" false
    (has_check "formulary" (run ~readings good))

(* The coverage gap: a rite that resolves a formulary on most days but falls
   through on one. On real EF data this has no witness at all (Task 3's own
   [test_every_day_has_a_formulary] below confirms it directly), so this
   fixture is the only thing that holds it honest. *)
let test_formulary_fires_on_a_gap () =
  let readings ~observed:_ ~temporal:_ ~date ~temporal_at:_ =
    if D.compare date target = 0 then (None, [])
    else (Some well_formed_formulary, well_formed_citations)
  in
  Alcotest.(check bool) "formulary check fires when one day of the year resolves none" true
    (has_check "formulary" (run ~readings good))

(* ---------------------------------------------------------------------- *)
(* Direct real-EF-data coverage (Task 3 brief): every day of every year in *)
(* the sample resolves a formulary, the same discipline the "citations"    *)
(* checks already hold EF to -- asserted directly against                  *)
(* [Liturgical_day.t] rather than through [Validate.run]'s failure list,   *)
(* so a bug in [Validate]'s own gating could not hide this gap. *)
(* ---------------------------------------------------------------------- *)

(* 2005-2050: the same 46-year sample test_rite_ef.ml's own [sample_years]
   uses, for the same reason -- non-trivial, deterministic, and already the
   project's differential-testing window (CLAUDE.md). Defined locally
   rather than shared: test executables in this project cross-reference
   only [.suite] values (test_colitur.ml), never each other's internal
   helpers. *)
let sample_years =
  let rec range a b = if a > b then [] else a :: range (a + 1) b in
  range 2005 2050

let year_of y = Colitur_kernel.Calendar.year real_ef_rite real_ef_layer y

(* Every day of every year resolves a formulary, for the same reason
   [Validate] already asserts exactly one First and one Gospel: a day that
   says no Mass at all is a defect, not a gap. Mirrors the "citations"
   check. *)
let test_every_day_has_a_formulary () =
  let missing = ref [] in
  List.iter
    (fun y ->
      Array.iter
        (fun (d : (_, _) Colitur_kernel.Liturgical_day.t) ->
          if d.Colitur_kernel.Liturgical_day.formulary = None then
            missing :=
              Colitur_kernel.Date.to_iso8601 d.Colitur_kernel.Liturgical_day.date :: !missing)
        (year_of y))
    sample_years;
  Alcotest.(check (list string)) "every day resolves a formulary" [] !missing

let suite =
  ( "Validate",
    [ Alcotest.test_case "landmark years" `Quick test_landmark_years;
      Alcotest.test_case "year 9999 does not raise" `Quick test_year_9999_does_not_raise;
      Alcotest.test_case "easter extremes" `Quick test_easter_extremes;
      Alcotest.test_case "synthetic baseline is clean" `Quick test_synthetic_baseline_is_clean;
      Alcotest.test_case "two-run season is accepted" `Quick test_two_run_season_is_accepted;
      Alcotest.test_case "coverage fires" `Quick test_coverage_fires;
      Alcotest.test_case "seasons fires" `Quick test_seasons_fires;
      Alcotest.test_case "week fires" `Quick test_week_fires;
      Alcotest.test_case "weekday fires" `Quick test_weekday_fires;
      Alcotest.test_case "rank fires" `Quick test_rank_fires;
      Alcotest.test_case "colour fires" `Quick test_colour_fires;
      Alcotest.test_case "determinism fires" `Quick test_determinism_fires;
      Alcotest.test_case "anchor clean" `Quick test_anchor_clean;
      Alcotest.test_case "anchor fires" `Quick test_anchor_fires;
      Alcotest.test_case "vocab rank injectivity fires" `Quick test_vocab_rank_injectivity_fires;
      Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires;
      Alcotest.test_case "slugs fires" `Quick test_slugs_fires;
      Alcotest.test_case "citations silent without a lectionary" `Quick
        test_citations_silent_without_a_lectionary;
      Alcotest.test_case "citations clean when well formed" `Quick
        test_citations_clean_when_well_formed;
      Alcotest.test_case "citations fires on a lone epistle" `Quick
        test_citations_fires_on_a_lone_epistle;
      Alcotest.test_case "citations fires on an out-of-scope part" `Quick
        test_citations_fires_on_an_out_of_scope_part;
      Alcotest.test_case "citations-unresolved fires on a gap" `Quick
        test_citations_unresolved_fires_on_a_gap;
      Alcotest.test_case "formulary silent without a lectionary" `Quick
        test_formulary_silent_without_a_lectionary;
      Alcotest.test_case "formulary clean when well formed" `Quick
        test_formulary_clean_when_well_formed;
      Alcotest.test_case "formulary fires on a gap" `Quick test_formulary_fires_on_a_gap;
      Alcotest.test_case "every day (2005-2050) resolves a formulary" `Quick
        test_every_day_has_a_formulary;
      Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception;
      Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires;
      Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires;
      Alcotest.test_case "admission fires" `Quick test_admission_fires;
      Alcotest.test_case "observed fires" `Quick test_observed_fires;
      Alcotest.test_case "resolution checks clean on a well-behaved layer" `Quick
        test_resolution_checks_clean_on_a_well_behaved_layer;
      Alcotest.test_case "exhaustive domain sweep (1583..9999), committed not sampled" `Slow
        test_exhaustive_domain_sweep ]
    @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] )