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. --- lib/kernel/validate.mli | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 lib/kernel/validate.mli (limited to 'lib/kernel/validate.mli') diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli new file mode 100644 index 0000000..b557731 --- /dev/null +++ b/lib/kernel/validate.mli @@ -0,0 +1,16 @@ +(** The invariant harness -- validation layer 2. Checks run over a *liturgical* + year, not a civil year: a season that straddles January would otherwise look + as though it recurs. *) +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. *) +val run : + ('s, 'r) Vocab.t -> + year_start:(int -> Date.t) -> + temporal:(Date.t -> ('s, 'r) Temporal.t) -> + year:int -> + failure list -- cgit v1.3