diff options
| -rw-r--r-- | lib/kernel/validate.ml | 20 | ||||
| -rw-r--r-- | test/test_validate.ml | 155 |
2 files changed, 166 insertions, 9 deletions
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index 9be030a..b11c05c 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -35,14 +35,18 @@ let run vocab ~year_start ~temporal ~year = (* Weekday agreement. *) if t.Temporal.weekday <> Date.weekday date then fail date "weekday" "temporal weekday disagrees with Date.weekday"; - (* Slug well-formed. Uniqueness *per date* needs no check: [temporal] - returns exactly one office by construction, which is the type - system delivering the invariant. Uniqueness *across the year* is - deliberately NOT asserted -- a resumed Sunday reuses an earlier - Epiphany key on purpose, so the check would be false. *) - (match Slug.of_string (Slug.to_string cel.Celebration.slug) with - | Ok _ -> () - | Error e -> fail date "slug" e); + (* Slug: three properties, none checked here, all delivered + elsewhere. 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 deliberately NOT asserted -- a resumed Sunday + reuses an earlier Epiphany key on purpose, so the check would be + false. *) (* Vocabulary closure. *) if not (List.exists (fun r -> vocab.Vocab.rank_to_string r = vocab.Vocab.rank_to_string cel.Celebration.rank) diff --git a/test/test_validate.ml b/test/test_validate.ml index e293dfd..a2478f7 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -38,8 +38,161 @@ let prop_invariants = (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 ] } + + 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. 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 + + 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 + +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)) + let suite = ( "Validate", [ Alcotest.test_case "landmark years" `Quick test_landmark_years; - Alcotest.test_case "easter extremes" `Quick test_easter_extremes ] + 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 ] @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] ) |