From e15fe4952a569f08900f9d602f7bc98afd298542 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 14:56:09 +0200 Subject: kernel(validate): invariant harness over liturgical years Coverage, season contiguity and completeness, Sunday-aligned week numbering, slug well-formedness, weekday agreement and vocabulary closure. Checks run over a liturgical year rather than a civil one, since Christmastide straddles January and would otherwise appear to recur. Run against EF temporal for landmark years, both Easter extremes, and 200 random years across 1583..9998 -- the property layer is how confidence reaches past the oracle horizon. --- test/test_colitur.ml | 2 +- test/test_validate.ml | 45 +++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 test/test_validate.ml (limited to 'test') diff --git a/test/test_colitur.ml b/test/test_colitur.ml index 293e439..ae58607 100644 --- a/test/test_colitur.ml +++ b/test/test_colitur.ml @@ -2,4 +2,4 @@ let () = Alcotest.run "colitur" [ Test_date.suite; Test_computus.suite; Test_colour.suite; Test_slug.suite; Test_names.suite; - Test_overlay.suite; Test_temporal_ef.suite ] + Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite ] diff --git a/test/test_validate.ml b/test/test_validate.ml new file mode 100644 index 0000000..e293dfd --- /dev/null +++ b/test/test_validate.ml @@ -0,0 +1,45 @@ +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 ~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 ] + +(* 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 + Alcotest.(check bool) "found at least one extreme year" true (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 = []) + +let suite = + ( "Validate", + [ Alcotest.test_case "landmark years" `Quick test_landmark_years; + Alcotest.test_case "easter extremes" `Quick test_easter_extremes ] + @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] ) -- cgit v1.3