module Val = Colitur_kernel.Validate module V = Rite_ef.Vocab_ef module T = Rite_ef.Temporal_ef let run year = Val.run V.vocab ~year_start:T.year_start ~temporal:T.temporal ~anchors:T.anchors ~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 1818, latest 2038); requiring just "non-empty" would have passed even if the search silently found only one of them (register finding 15). *) Alcotest.(check int) "found both extreme years (earliest 22 Mar and latest 25 Apr)" 2 (List.length 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 = []) (* ---- 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 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") } 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) ] let run ?(vocab = vocab) ?(anchors = fun _ -> []) temporal = Val.run vocab ~year_start ~temporal ~anchors ~year:2026 let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs end open Synthetic let test_synthetic_baseline_is_clean () = Alcotest.(check bool) "clean synthetic fixture has no failures" true (run good = []) 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 "each season, one unbroken run". *) 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" 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)) 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 "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 ] @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] )