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