aboutsummaryrefslogtreecommitdiff
path: root/lib/kernel/validate.mli
diff options
context:
space:
mode:
authorLukasz Kasprzak <lukas@labunix.xyz>2026-08-11 14:56:09 +0200
committerLukasz Kasprzak <lukas@labunix.xyz>2026-08-11 15:09:53 +0200
commite15fe4952a569f08900f9d602f7bc98afd298542 (patch)
tree48aaec659196a00aaaea47ee3cffc57ea5291b15 /lib/kernel/validate.mli
parent849ca6e118f765597e8d74272e1432a6391853c1 (diff)
downloadcolitur-e15fe4952a569f08900f9d602f7bc98afd298542.tar.gz
colitur-e15fe4952a569f08900f9d602f7bc98afd298542.zip
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.
Diffstat (limited to 'lib/kernel/validate.mli')
-rw-r--r--lib/kernel/validate.mli16
1 files changed, 16 insertions, 0 deletions
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