diff options
| -rw-r--r-- | lib/kernel/validate.ml | 70 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 20 | ||||
| -rw-r--r-- | test/test_validate.ml | 101 |
3 files changed, 177 insertions, 14 deletions
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index b11c05c..7be3425 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -7,13 +7,46 @@ 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 -let run vocab ~year_start ~temporal ~year = +(* 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 + +let run vocab ~year_start ~temporal ~anchors ~year = let start = year_start year in - let stop = Date.add_days (year_start (year + 1)) (-1) 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 @@ -53,7 +86,15 @@ let run vocab ~year_start ~temporal ~year = 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") + 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 (* Season contiguity and completeness: the run-length-compressed sequence must @@ -93,4 +134,27 @@ let run vocab ~year_start ~temporal ~year = 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; List.rev !failures diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index b557731..709a711 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,12 +5,26 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run vocab ~year_start ~temporal ~year] returns every invariant violation in - the liturgical year opening in civil year [year]. An empty list means the - year is clean. *) +(** [run vocab ~year_start ~temporal ~anchors ~year] returns every invariant + violation in the liturgical year opening in civil year [year]. An empty + list means the year is clean. + + [anchors y] is the rite's own independent restatement of its fixed and + Easter-derived named days for civil year [y], as (expected slug, date) + pairs -- not derived from [temporal] itself, so a drift between the two + is caught rather than invisible. [run] consults both [anchors year] and + [anchors (year + 1)], since a liturgical year straddles two civil years, + and checks only the pairs whose date actually falls within the year + walked. + + Total over the whole 1583..9999 domain, including [year] = 9999: the + liturgical year opening there continues into out-of-domain civil year + 10000, so the walk is clamped to 31 December 9999 and the checks run + against that truncated final year rather than raising. *) val run : ('s, 'r) Vocab.t -> year_start:(int -> Date.t) -> temporal:(Date.t -> ('s, 'r) Temporal.t) -> + anchors:(int -> (string * Date.t) list) -> year:int -> failure list diff --git a/test/test_validate.ml b/test/test_validate.ml index a2478f7..c19957d 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -3,7 +3,7 @@ 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 ~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 @@ -14,6 +14,23 @@ let check_year year = 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 () = @@ -29,7 +46,10 @@ let extreme_years () = let test_easter_extremes () = let ys = extreme_years () in - Alcotest.(check bool) "found at least one extreme year" true (ys <> []); + (* 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. *) @@ -77,6 +97,14 @@ module Synthetic = struct 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 = @@ -108,12 +136,22 @@ module Synthetic = struct { 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. 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:15 with Ok d -> d | Error e -> failwith e + (* 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 run ?(vocab = vocab) temporal = Val.run vocab ~year_start ~temporal ~year:2026 let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs end @@ -184,9 +222,51 @@ let test_colour_fires () = 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; @@ -194,5 +274,10 @@ let suite = 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 "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 ] ) |