From 6436509d6b599b7d7c6467bd39c8090cb9634889 Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Tue, 11 Aug 2026 19:39:37 +0200 Subject: kernel(rite): bundle what a rite supplies; make season runs rite-supplied Validate took four loose arguments that had to come from the same rite with nothing enforcing it, and Calendar is about to add more. Bundling makes a mismatched assembly unrepresentable through the normal path. season_runs replaces the hardcoded assumption that every season occupies exactly one unbroken run. That holds for the 1962 rite but is false for the modern form's Ordinary Time, which is one season in two runs -- as written the check would have reported a false failure every year for the second rite. --- lib/kernel/validate.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'lib/kernel/validate.ml') diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index 7be3425..c6501a9 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,11 @@ let has_duplicate strings = 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 run (rite : ('s, 'r) Rite.t) ~year = + let vocab = rite.Rite.vocab in + let year_start = rite.Rite.year_start in + let temporal = rite.Rite.temporal in + let anchors = rite.Rite.anchors in let start = year_start year in let stop = (* [year_start (year + 1)] needs a date in civil year (year+1); at @@ -98,8 +102,11 @@ let run vocab ~year_start ~temporal ~anchors ~year = days; let observed = List.rev !observed in (* Season contiguity and completeness: the run-length-compressed sequence must - equal vocab.seasons exactly -- all seasons, each in one unbroken run, in - canonical order. No EF season can be empty in any year. *) + equal the rite's own [season_runs] exactly, in canonical order. This is + NOT necessarily [vocab.seasons] -- most rites have each season in one + unbroken run, but a rite may legitimately have one season appear in two + separate runs (the modern form's Ordinary Time does), so the expected + sequence is rite-supplied rather than derived from the vocabulary. *) let compressed = List.fold_left (fun acc (_, t) -> @@ -108,7 +115,7 @@ let run vocab ~year_start ~temporal ~anchors ~year = [] observed |> List.rev in - let expected = List.map vocab.Vocab.season_to_string vocab.Vocab.seasons in + let expected = List.map vocab.Vocab.season_to_string rite.Rite.season_runs in if compressed <> expected then fail start "seasons" (Printf.sprintf "season runs %s; expected %s" -- cgit v1.3 From 633306c8a5ac1854f30749f498498104ebc84edc Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 02:12:03 +0200 Subject: kernel(validate): resolution invariants Widen Validate.run to take the rite's sanctoral layer alongside the rite itself (Calendar.year needs both), and add five checks over the fully resolved liturgical year, on top of the existing temporal-only pass: - observed: a day's observed celebration never also appears among that same day's own commemorations/omissions. - lost: no sanctoral entry is silently dropped. Per slug, the number of times it is actually sighted (observed + commemorations + omitted, summed over the year) must never fall below the number of times its own Date_spec resolves within the year's span -- also fires if resolving the year raises at all, the most total form of loss. - duplicated: the same per-slug count must never exceed the number of Date_spec resolutions either. Deliberately NOT "no slug appears twice": a fixed date can legitimately resolve twice in the ~20% of liturgical years whose 371-day span reaches it on both ends (30 November/St Andrew is the worked example in validate.mli). - unconverged: no day's omitted reason indicates Calendar's placement pass hit its round guard before reaching a fixed point. - admission: the rite's own rules.admit is a fixed point on what it already admitted -- the rite-agnostic form of "the admission limit was not exceeded" available without embedding a rite's own numeric caps (RG 111's, for EF) into kernel code. Each check has a dedicated negative fixture in the synthetic rite (test_validate.ml), hand-traced against Calendar's actual resolution mechanics before writing the assertion, and verified to fail for the right reason against the code before this change. One pair (unconverged/duplicated) is not fully independent: hitting the round guard genuinely also trips duplicated, a real consequence of Calendar's own accounting once a candidate is simultaneously sighted at its permanent natural date and wherever the last placement round left it -- documented in guard_rules's own comment, not papered over. test_validate.ml's ef_rite/run now use the real Rite_ef.context and the real bootstrapped data/ef layer (Precedence_ef and the sanctoral bootstrap did not exist when this scaffolding was first written) rather than the earlier placeholder rules. Validate is clean across the whole 1583..9999 domain against real EF data except the one already-documented year-9999 truncation case (test_year_9999_does_not_raise). --- lib/kernel/validate.ml | 132 +++++++++++++++++++- lib/kernel/validate.mli | 46 ++++++- test/test_validate.ml | 311 ++++++++++++++++++++++++++++++++++++++++++++---- 3 files changed, 460 insertions(+), 29 deletions(-) (limited to 'lib/kernel/validate.ml') diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index c6501a9..d8de31b 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,7 +20,20 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted -let run (rite : ('s, 'r) Rite.t) ~year = +(* Task 12's "unconverged" check has no structural signal to key off -- + Calendar's placement pass records its round-guard reason as a plain + string in [Liturgical_day.omitted] (calendar.ml's own [unconverged_reason], + not exposed as a public constant), and [Liturgical_day.omitted]'s own doc + comment says exactly this check is meant to read it. A short, distinctive + substring rather than the full literal keeps the coupling to calendar.ml's + exact wording as loose as it can be while still being unambiguous: nothing + else this kernel emits into [omitted] talks about "converging". *) +let contains_substring s ~needle = + let ls = String.length s and ln = String.length needle in + let rec at i = i + ln <= ls && (String.sub s i ln = needle || at (i + 1)) in + ln = 0 || at 0 + +let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = let vocab = rite.Rite.vocab in let year_start = rite.Rite.year_start in let temporal = rite.Rite.temporal in @@ -164,4 +177,121 @@ let run (rite : ('s, 'r) Rite.t) ~year = if actual <> expected_slug then fail date "anchor" (Printf.sprintf "expected slug %S, got %S" expected_slug actual)) anchor_pairs; + (* Resolution invariants (Task 12): everything above only ever asked + [rite.temporal] for a date's office in isolation. From here on the + LITURGICAL YEAR IS ACTUALLY RESOLVED against [layer] -- occurrence, + transfer placement, commemorations, the works (spec §2.4) -- and the + result checked for five further properties a temporal-only pass cannot + see at all. [days] (the walk built above) is reused rather than + recomputed: it names exactly the same [start, stop] span + {!Calendar.year} resolves for this [year]. *) + (match Calendar.year rite layer year with + | exception exn -> + (* The kernel contract forbids [run] itself from ever raising on + in-range input, and an exception escaping resolution is the most + total form of "silently lost" there is: nothing about this year's + sanctoral entries could be verified as accounted for at all. *) + fail start "lost" + (Printf.sprintf "resolving the year raised (%s); nothing could be verified as accounted for" + (Printexc.to_string exn)) + | resolved -> + let idx = Layer.index_by_date layer in + let bump tbl slug = Hashtbl.replace tbl slug (1 + (try Hashtbl.find tbl slug with Not_found -> 0)) in + (* Expected: how many times each layer entry's own Date_spec resolves + within [start, stop]. Walking dates and querying [Layer.on_date] + (rather than resolving each entry's Date_spec against candidate + civil years directly) is what naturally counts a fixed late- + November date TWICE in the ~20% of liturgical years whose 371-day + span reaches it on both ends -- see validate.mli's own note on 30 + November / St Andrew. *) + let expected : (string, int) Hashtbl.t = Hashtbl.create 64 in + List.iter + (fun date -> + Layer.on_date idx ~month:(Date.month date) ~day:(Date.day date) + |> List.iter (fun (e : 'r Layer.entry) -> + bump expected (Slug.to_string e.Layer.cel.Celebration.slug))) + days; + (* Actual: how many times each slug is actually sighted across the + resolved year. Deliberately [observed] + [commemorations] + + [omitted] only, NOT [transferred_out]: a successfully transferred + celebration is already counted once, via [observed] (+ + [transferred_in]) on the day it lands; also counting + [transferred_out] at the day it left would double-book every clean + transfer, which is exactly what this check exists to catch, not + cause. *) + let actual : (string, int) Hashtbl.t = Hashtbl.create 64 in + let bump_cel tbl (c : 'r Celebration.t) = bump tbl (Slug.to_string c.Celebration.slug) in + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + bump_cel actual d.Liturgical_day.observed; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.commemorations; + List.iter (fun (c, _) -> bump_cel actual c) d.Liturgical_day.omitted) + resolved; + Hashtbl.fold (fun slug exp acc -> (slug, exp) :: acc) expected [] + |> List.sort compare (* stable failure order: Hashtbl.iter's own order is hash-seed-dependent *) + |> List.iter (fun (slug, exp) -> + let act = try Hashtbl.find actual slug with Not_found -> 0 in + if act < exp then + fail start "lost" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves %d" + slug act exp) + else if act > exp then + fail start "duplicated" + (Printf.sprintf "%s: sighted %d time(s) this year, but its own Date_spec resolves only %d" + slug act exp)); + Array.iter + (fun (d : ('s, 'r) Liturgical_day.t) -> + let date = d.Liturgical_day.date in + let observed_slug = Slug.to_string d.Liturgical_day.observed.Celebration.slug in + let has_slug (c, _) = Slug.to_string c.Celebration.slug = observed_slug in + (* "observed": the day's own winner must not ALSO be listed as one + of its own losers -- see validate.mli's own note on why this is + reachable (two distinct layer entries sharing a slug, one + transferred onto the other's natural date, the transferred one + winning) despite {!Precedence.resolve}'s fold never letting the + SAME candidate value appear as both winner and loser. *) + if List.exists has_slug d.Liturgical_day.commemorations + || List.exists has_slug d.Liturgical_day.omitted + then + fail date "observed" + (Printf.sprintf + "%s is this day's observed celebration and also appears among its own \ + commemorations/omissions" + observed_slug); + (* "unconverged": see [contains_substring]'s own comment above. *) + if + List.exists + (fun (_, reason) -> contains_substring reason ~needle:"did not converge") + d.Liturgical_day.omitted + then + fail date "unconverged" + "transfer placement did not reach a fixed point within the round guard (RG 96-98)"; + (* "admission": re-offer this day's own admitted commemorations + back to [rite.rules.admit] and require the exact same set back. + [origin] is reconstructed as [Sanctoral] uniformly: + {!Liturgical_day.t} does not retain a commemoration's original + origin, and the real EF [admit] (precedence_ef.ml) reads only + rank and slug from a candidate, never [origin], so this + reconstruction is exact for it; documented in validate.mli as + the one place a rite whose [admit] DOES consult [origin] could + see a false negative from this check. *) + let observed_candidate : 'r Precedence.candidate = + { Precedence.cel = d.Liturgical_day.observed; origin = Precedence.Sanctoral } + in + let as_candidates comms = + List.map (fun (c, p) -> ({ Precedence.cel = c; origin = Precedence.Sanctoral }, p)) comms + in + let offered = as_candidates d.Liturgical_day.commemorations in + let readmitted = rite.Rite.rules.Precedence.admit ~observed:observed_candidate offered in + let norm l = + List.map (fun (c, p) -> (Slug.to_string c.Precedence.cel.Celebration.slug, p)) l + |> List.sort compare + in + if norm readmitted <> norm offered then + fail date "admission" + (Printf.sprintf + "admit is not a fixed point on this day's own commemorations: re-offering %d \ + admitted %d back" + (List.length offered) (List.length readmitted))) + resolved); List.rev !failures diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index d281f9a..511c78f 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -5,8 +5,9 @@ type failure = { year : int; date : string; check : string; detail : string } val failure_to_string : failure -> string -(** [run rite ~year] returns every invariant violation in the liturgical year - opening in civil year [year]. An empty list means the year is clean. +(** [run rite layer ~year] returns every invariant violation in the + liturgical year opening in civil year [year]. An empty list means the + year is clean. [rite.Rite.anchors y] is the rite's own independent restatement of its fixed and Easter-derived named days for civil year [y], as (expected @@ -21,8 +22,47 @@ val failure_to_string : failure -> string have one season appear in two separate runs (the modern form's Ordinary Time does), so the two are not necessarily the same list. + [layer] is resolved against [rite] via {!Calendar.year} (spec §2.4's + occurrence/transfer/commemoration pass), and the resulting fully-resolved + liturgical year is checked for five further invariants a temporal-only + pass cannot see (Task 12), each its own ["check"] label: + - ["observed"]: a day's [observed] celebration is never ALSO listed among + that same day's [commemorations] or [omitted] -- a day reports one + winner, not a winner that also lost to itself. + - ["lost"]: no sanctoral entry is silently dropped. Per slug, the number + of times it is actually sighted ([observed] + [commemorations] + + [omitted], summed over the whole year -- NOT [transferred_out], which + would double-count a successfully placed transfer against its own + arrival) must never fall below the number of times its own + {!Date_spec} resolves within the year's span (an entry with two + occurrences, e.g. 30 November in the nine liturgical years where the + 371-day span reaches it twice, must be sighted twice, not once). Also + fires if resolving the year raises at all -- an escaping exception is + the most total form of silent loss, and the kernel contract forbids + [run] itself from propagating it. + - ["duplicated"]: the same per-slug count must never EXCEED the number of + {!Date_spec} resolutions either. Deliberately NOT "no slug appears + twice in the year" -- a fixed date can legitimately resolve twice, per + ["lost"] above -- it is "resolutions and sightings agree", the property + that actually distinguishes a transfer that moved from one that + duplicated. + - ["unconverged"]: no day's [omitted] carries the reason {!Calendar}'s + placement pass records when its round guard (calendar.ml's + [max_transfer_rounds]) is hit before every deferred candidate reaches a + fixed point. + - ["admission"]: the rite's own [rules.admit] is a fixed point on what it + already admitted -- re-offering a day's [commemorations] back to + [admit] (reconstructed with {!Precedence.Sanctoral} origin; the real EF + admit reads only rank and slug, never origin, so this reconstruction is + exact for it) must return exactly that same set. A cap-enforcing + selector that is not idempotent on its own output has, by definition, + admitted something its own rule would not admit if asked again -- the + rite-agnostic form of "the admission limit was not exceeded" available + without embedding a rite's specific numeric caps (RG 111's, for EF) + into kernel code. + 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) Rite.t -> year:int -> failure list +val run : ('s, 'r) Rite.t -> 'r Layer.t -> year:int -> failure list diff --git a/test/test_validate.ml b/test/test_validate.ml index df8c99c..b2d4f34 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -1,24 +1,40 @@ module Val = Colitur_kernel.Validate module Rite = Colitur_kernel.Rite module P = Colitur_kernel.Precedence +module Layer = Colitur_kernel.Layer +module Overlay = Colitur_kernel.Overlay module V = Rite_ef.Vocab_ef module T = Rite_ef.Temporal_ef -(* Plan 3's real EF precedence rules (Precedence_ef, Tasks 7-11) don't exist - yet -- Validate.run doesn't read [rules] or [transfer_target] at all - (nothing does before Task 5's Calendar and Task 6's placement pass), so a - placeholder is enough to assemble a well-typed Rite.t here. *) -let ef_rules : (V.season, V.rank) P.rules = - { P.band = (fun _ _ -> 0); - disposition = (fun ~winner:_ ~loser:_ -> P.Omit); - admit = (fun ~observed:_ _ -> []) } - -let ef_rite : (V.season, V.rank) Rite.t = - { Rite.id = T.id; vocab = V.vocab; year_start = T.year_start; temporal = T.temporal; - anchors = T.anchors; rules = ef_rules; season_runs = V.seasons; - transfer_target = (fun _ origin _ -> origin) } - -let run year = Val.run ef_rite ~year +(* Task 12 widens Validate.run to take a resolved layer -- Precedence_ef and + Calendar (Tasks 5-11) now exist, so the REAL EF rite (Rite_ef.context) and + its REAL bootstrapped data replace the earlier placeholder rules/layer-less + Rite.t this module used before Plan 3's resolution engine was built. + Relative to this test's own build directory (_build/default/test/), same + convention test_rite_ef.ml already uses -- test/dune declares both as deps + of the (test ...) stanza. *) +let sanctoral_path = "../data/ef/sanctoral.sexp" +let adjustments_path = "../data/ef/adjustments.sexp" + +(* Loaded once at module init, not per call: [run] below is called by every + test and by the 200-sample property, and Calendar.year's own resolution + cost already dominates -- there is no reason to also re-parse a 322-entry + sexp file on every one of those calls. *) +let real_ef_layer = + match Layer.load V.rank_of_sexp sanctoral_path with + | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" sanctoral_path e) + | Ok layer -> ( + match Overlay.load V.rank_of_sexp adjustments_path with + | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" adjustments_path e) + | Ok overlay -> + let layer, diagnostics = Overlay.apply layer overlay in + if diagnostics <> [] then + failwith + (Printf.sprintf "unexpected overlay diagnostics: %s" + (String.concat "; " (List.map Overlay.diagnostic_to_string diagnostics))); + layer) + +let run year = Val.run Rite_ef.context real_ef_layer ~year let check_year year = match run year with @@ -94,6 +110,8 @@ module Synthetic = struct module Temporal = Colitur_kernel.Temporal module P = Colitur_kernel.Precedence module Rite = Colitur_kernel.Rite + module Layer = Colitur_kernel.Layer + module Date_spec = Colitur_kernel.Date_spec type season = A | B type rank = R1 | R2 @@ -122,8 +140,12 @@ module Synthetic = struct let vocab_collapsed_ranks = { vocab with Vocab.rank_to_string = (fun _ -> "same") } let vocab_collapsed_seasons = { vocab with Vocab.season_to_string = (fun _ -> "same") } - (* Precedence_ef doesn't exist yet (Tasks 7-11); Validate.run never reads - [rules], so a placeholder is enough to assemble a well-typed Rite.t. *) + (* The placeholder ruleset every TEMPORAL-only fixture below still uses: + paired with the default empty [layer] (see [rite] below), there is never + a sanctoral candidate for these three functions to be called against, so + what they return is moot for those tests -- only the Task 12 resolution + fixtures further down override [rules] (and supply a non-empty + [layer]), each with its own small, deliberately-shaped ruleset. *) let rules : (season, rank) P.rules = { P.band = (fun _ _ -> 0); disposition = (fun ~winner:_ ~loser:_ -> P.Omit); @@ -173,14 +195,25 @@ module Synthetic = struct this synthetic rite too, not only in EF. *) let anchors _y = [ (Slug.to_string (good target).Temporal.office.Cel.slug, target) ] - let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) temporal - : (season, rank) Rite.t = + (* Task 12: [rite] now also takes [rules]/[transfer_target] (defaulting to + the placeholder above and to "stand still", respectively -- harmless + defaults against the default empty [layer], since nothing ever contests + the temporal office there) so the resolution fixtures further down can + override them without duplicating every other field. *) + let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) ?(rules = rules) + ?(transfer_target = fun _ origin _ -> origin) temporal : (season, rank) Rite.t = { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs; - (* Validate.run doesn't read this either (see [ef_rules] above). *) - transfer_target = (fun _ origin _ -> origin) } + transfer_target } - let run ?vocab ?anchors ?season_runs temporal = - Val.run (rite ?vocab ?anchors ?season_runs temporal) ~year:2026 + (* Empty by default: every check built before Task 12 exercises the + TEMPORAL-only pass, where an empty layer is exactly the fixture that + leaves it unable to affect anything ([Precedence.resolve] against no + sanctoral candidates always just observes the temporal office + unchallenged). Task 12's own resolution fixtures pass their own. *) + let empty_layer = Layer.empty ~id:"synthetic-empty" ~name:"empty" + + let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?(layer = empty_layer) temporal = + Val.run (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target temporal) layer ~year:2026 let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs @@ -210,6 +243,180 @@ module Synthetic = struct let rite_with_two_runs : (season, rank) Rite.t = rite ~season_runs:[ A; B; A; B ] two_run_temporal + + (* ---- Task 12: resolution-level fixtures ---- + + Everything above only ever drives the TEMPORAL-only pass: [run]'s + default [layer] is empty, so [Precedence.resolve] never has a sanctoral + candidate to contest against the temporal office, and [rules]/ + [transfer_target] are never meaningfully exercised. These five fixtures + instead give [Calendar.year] real work -- a non-empty [layer] plus a + small, deliberately-shaped [rules] (and, for two of them, + [transfer_target]) -- each built so its OWN check label fires. Four of + the five fire in clean isolation (the other four Task 12 labels stay + silent); the fifth (["unconverged"]) genuinely also fires + ["duplicated"] alongside it, a real consequence of Calendar's own round- + guard accounting, not a fixture design flaw -- see guard_rules's own + comment. Every fixture's isolation (or lack of it) was verified by + hand-tracing [Calendar]'s resolution mechanics BEFORE writing its + assertion (see the task report), not inferred from what the assertion + happens to require -- the tests below check that trace against the + actual engine output, one fixture at a time. [good] is reused, + unchanged, as every fixture's [temporal]: only [rules]/[layer]/ + [transfer_target] vary, so the temporal-only checks (already proven + clean against [good] by [test_synthetic_baseline_is_clean]) cannot be + what fires here. *) + + let mk_entry ~month ~day ~slug ~rank = + { Layer.date = (match Date_spec.fixed ~month ~day with Ok d -> d | Error e -> failwith e); + cel = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.White + ~layer:"synthetic-sanctoral" () } + + let task12_checks = [ "observed"; "lost"; "duplicated"; "unconverged"; "admission" ] + + (* The Task-12-owned subset of a failure list's own check labels, as a + sorted, de-duplicated set -- what each isolation assertion below + compares against, so a fixture that (by mistake) also trips an + unrelated Task-12 check shows up as a wrong set, not a silently-passing + [has_check]. *) + let fired_task12_checks (fs : Val.failure list) = + List.filter_map (fun f -> if List.mem f.Val.check task12_checks then Some f.Val.check else None) fs + |> List.sort_uniq compare + + (* "duplicated": a single ordinary sanctoral entry, always losing to the + temporal office (band: Temporal 0 < Sanctoral 10, unconditionally) and + always Commemorate-disposed. [admit]'s bug is exactly the shape + precedence_ef.mli's own [admit] contract warns against ("a value taken + unchanged from comms, never rebuilt"): it REBUILDS every admitted pair + via a record update, allocating a fresh, structurally-identical-but- + physically-distinct candidate. Precedence.resolve's own [dropped] + computation tells an admitted candidate from a dropped one by PHYSICAL + equality, so the rebuild defeats it -- the one candidate ends up counted + as both admitted (in [commemorations]) and dropped (in [omitted], + "admission limit reached"): two sightings for one Date_spec + resolution. *) + let dup_entry = mk_entry ~month:5 ~day:5 ~slug:"dup-target" ~rank:R2 + let dup_layer = Layer.of_entries ~id:"dup" ~name:"dup" [ dup_entry ] + + let dup_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10); + disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> List.map (fun (c, p) -> ({ c with P.origin = c.P.origin }, p)) cs) } + + (* "unconverged": two entries collide on one date (6 June), both beating + the temporal office and tied with each other, so slug decides: + "guard-aaa" wins the day outright every time, "guard-zzz" is always the + loser there and always Transfer-disposed. Paired with a + [transfer_target] that always answers with the impeded day itself -- + never strictly forward -- this is the exact non-terminating shape + test_calendar.ml's own + [test_transfer_guard_records_failure_instead_of_looping] proves hits + Calendar's round guard: "guard-zzz", re-injected into 6 June every + round, can never win it (it always loses the tie to the natural + "guard-aaa" copy already sitting there), so [deferred] never empties. + + GENUINE FINDING (see the task report): this ALSO fires "duplicated", not + "unconverged" alone. Once the guard is hit, [build_day]'s final resolve + at 6 June sees "guard-zzz" TWICE -- once as the permanent natural entry + (which never stops losing there) and once as whatever the last round's + [injected] state still holds for it -- and [unresolved] is evaluated per + CANDIDATE OBJECT, not per slug, so BOTH copies land in [omitted] with + the unconverged reason. Nothing is lost (both copies carry a recorded + reason), but the slug is sighted twice against one Date_spec resolution, + which is exactly what "duplicated" is for. The same double-recording is + latent in test_calendar.ml's own guard fixture too (day_winner/eclipsed + at 20 Dec, structurally identical) -- untested there only because that + test uses [List.exists], not a count. Calendar's round guard is + documented as "nothing in the 1962 calendar is expected to trigger" + (calendar.ml), so this is a latent accounting quirk in an unreachable + path, not a live bug, and calendar.ml is out of this task's file list -- + reported, not fixed here. *) + let guard_winner_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-aaa" ~rank:R1 + let guard_loser_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-zzz" ~rank:R1 + let guard_layer = Layer.of_entries ~id:"guard" ~name:"guard" [ guard_winner_entry; guard_loser_entry ] + + let guard_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 50 | P.Sanctoral -> 10); + disposition = + (fun ~winner:_ ~loser -> + match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> cs) } + + let guard_transfer_target (_ : rank P.candidate) (origin : D.t) (_ : D.t -> rank Cel.t) = origin + + (* "admission": three entries collide on one date (9 September), all + losing to the temporal office (band: Temporal 0 < Sanctoral 10) and all + Commemorate-disposed -- a genuine 3-candidate offer to [admit]. The bug: + cap 2 when the offer's length is ODD, cap 1 when EVEN -- a length-keyed + rule with no liturgical meaning, chosen as the simplest function that is + NOT idempotent on its own output (offer 3, admit 2; re-offer those same + 2, admit only 1) while staying idempotent -- and so invisible -- on + every OTHER shape this suite exercises (never offered exactly 2 or 3 + candidates elsewhere), including its own clean 3-candidate day. *) + let adm_a_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-a" ~rank:R2 + let adm_b_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-b" ~rank:R2 + let adm_c_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-c" ~rank:R2 + let adm_layer = Layer.of_entries ~id:"adm" ~name:"adm" [ adm_a_entry; adm_b_entry; adm_c_entry ] + + let adm_compare_slug (c1, _) (c2, _) = Slug.compare c1.P.cel.Cel.slug c2.P.cel.Cel.slug + + let rec adm_take n = function + | [] -> [] + | x :: xs -> if n <= 0 then [] else x :: adm_take (n - 1) xs + + let adm_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10); + disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary); + admit = + (fun ~observed:_ cs -> + let sorted = List.stable_sort adm_compare_slug cs in + if List.length sorted mod 2 = 1 then adm_take 2 sorted else adm_take 1 sorted) } + + (* "observed": two DIFFERENT layer entries sharing one slug -- a realistic + data mistake (a renamed or duplicated entry), not prevented by + [Layer.t]'s own type. [collide_a] (1 Feb, rank R1) always loses on its + OWN date: [band] makes the temporal office win there specifically (5, + beating R1's 10) and lose everywhere else (50), so [collide_a] is always + Transfer-disposed at 1 Feb. Its constant [transfer_target] sends it to + 10 Feb -- [collide_b]'s own home date -- where [collide_a]'s rank R1 + (band 10) now beats both the temporal office (50, since the date is no + longer 1 Feb) and [collide_b]'s own rank R2 (band 90): the ARRIVING + [collide_a] wins 10 Feb outright, and [collide_b] -- same slug as the + new winner -- is Commemorate-disposed (R2) right alongside it. One day + ends up reporting the same slug as both its observed celebration and one + of its own commemorations. *) + let collide_d1 = match D.make ~year:2026 ~month:2 ~day:1 with Ok d -> d | Error e -> failwith e + let collide_a_entry = mk_entry ~month:2 ~day:1 ~slug:"collide-x" ~rank:R1 + let collide_b_entry = mk_entry ~month:2 ~day:10 ~slug:"collide-x" ~rank:R2 + let collide_layer = Layer.of_entries ~id:"collide" ~name:"collide" [ collide_a_entry; collide_b_entry ] + + let collide_rules : (season, rank) P.rules = + { P.band = + (fun ctx c -> + match c.P.origin with + | P.Temporal -> if D.compare ctx.P.date collide_d1 = 0 then 5 else 50 + | P.Sanctoral -> ( match c.P.cel.Cel.rank with R1 -> 10 | R2 -> 90)); + disposition = + (fun ~winner:_ ~loser -> + match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> cs) } + + let collide_d2 = match D.make ~year:2026 ~month:2 ~day:10 with Ok d -> d | Error e -> failwith e + let collide_transfer_target (_ : rank P.candidate) (_ : D.t) (_ : D.t -> rank Cel.t) = collide_d2 + + (* A genuinely resolved, well-behaved day (one ordinary sanctoral entry, + cleanly losing and commemorated, nothing transferred) -- proving the + five checks stay silent against REAL resolution machinery, not merely + against the default empty [layer] every fixture above this section + uses. Without this, "no check fires" would only ever have been shown + for a layer with nothing in it. *) + let clean_sanctoral_entry = mk_entry ~month:8 ~day:8 ~slug:"clean-saint" ~rank:R2 + let clean_sanctoral_layer = Layer.of_entries ~id:"clean" ~name:"clean" [ clean_sanctoral_entry ] + + let clean_sanctoral_rules : (season, rank) P.rules = + { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10); + disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary); + admit = (fun ~observed:_ cs -> cs) } end open Synthetic @@ -227,7 +434,7 @@ let test_synthetic_baseline_is_clean () = let test_two_run_season_is_accepted () = let r = Synthetic.rite_with_two_runs in Alcotest.(check (list string)) "no failures" [] - (List.map Val.failure_to_string (Val.run r ~year:2026)) + (List.map Val.failure_to_string (Val.run r Synthetic.empty_layer ~year:2026)) let test_coverage_fires () = let temporal d = if D.compare d target = 0 then failwith "boom" else good d in @@ -332,6 +539,53 @@ 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)) +(* ---- Task 12: resolution invariants ---- + + Each test below asserts that exactly one of the five new check labels + fires for its own dedicated fixture (Synthetic's own comments carry the + hand-traced mechanics) -- not merely "at least this one", so a fixture + that turns out to also trip an unrelated Task 12 check would fail loudly + here rather than reading as accidental corroboration. *) + +let test_lost_fires_on_resolution_exception () = + (* Reuses [test_coverage_fires]'s own broken [temporal]: [Calendar.year] + calls [rite.temporal] with no exception guard of its own (unlike the + temporal-only pass above, which wraps every call), so the same raise + that trips "coverage" also makes resolution itself raise -- the most + total form of "silently lost" there is, per validate.mli. *) + let temporal d = if D.compare d target = 0 then failwith "boom" else good d in + Alcotest.(check (list string)) "only the lost check fires" [ "lost" ] (fired_task12_checks (run temporal)) + +let test_duplicated_fires () = + Alcotest.(check (list string)) "only the duplicated check fires" [ "duplicated" ] + (fired_task12_checks (run ~layer:dup_layer ~rules:dup_rules good)) + +let test_unconverged_fires () = + (* Also asserts "duplicated" fires alongside it -- see guard_rules's own + comment for why that is the genuine, hand-verified consequence of + hitting the round guard here, not an isolation failure. *) + Alcotest.(check (list string)) "unconverged fires, and duplicated alongside it" + [ "duplicated"; "unconverged" ] + (fired_task12_checks + (run ~layer:guard_layer ~rules:guard_rules ~transfer_target:guard_transfer_target good)) + +let test_admission_fires () = + Alcotest.(check (list string)) "only the admission check fires" [ "admission" ] + (fired_task12_checks (run ~layer:adm_layer ~rules:adm_rules good)) + +let test_observed_fires () = + Alcotest.(check (list string)) "only the observed check fires" [ "observed" ] + (fired_task12_checks + (run ~layer:collide_layer ~rules:collide_rules ~transfer_target:collide_transfer_target good)) + +(* The positive counterpart: a genuinely resolved, well-behaved day (real + sanctoral entry, real contest, real commemoration) must report none of the + five checks -- proven against actual resolution machinery, not only + against every OTHER fixture's default empty layer. *) +let test_resolution_checks_clean_on_a_well_behaved_layer () = + Alcotest.(check (list string)) "none of the five checks fire" [] + (fired_task12_checks (run ~layer:clean_sanctoral_layer ~rules:clean_sanctoral_rules good)) + let suite = ( "Validate", [ Alcotest.test_case "landmark years" `Quick test_landmark_years; @@ -349,5 +603,12 @@ let suite = 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 ] + Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires; + Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception; + Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires; + Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires; + Alcotest.test_case "admission fires" `Quick test_admission_fires; + Alcotest.test_case "observed fires" `Quick test_observed_fires; + Alcotest.test_case "resolution checks clean on a well-behaved layer" `Quick + test_resolution_checks_clean_on_a_well_behaved_layer ] @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] ) -- cgit v1.3 From 4235a6aa18b815c5457a7eb97fd97eb4919dfd4b Mon Sep 17 00:00:00 2001 From: Lukasz Kasprzak Date: Wed, 12 Aug 2026 02:37:03 +0200 Subject: kernel(validate): fold in Plan 2's carried guards Three carried items from Plan 2's parked rulings, closed: 1. Slug uniqueness moves from a 200-sample QCheck property scoped to one rite (test_temporal_ef.ml) into Validate's own "slugs" check, so every consumer gets it. The resumed-Sunday exemption that property carried is dropped, not weakened elsewhere: Plan 2 verified zero duplicate slugs domain-wide (all 8 416 years), and by construction a resumed Sunday only ever backfills a week number Septuagesima cut short that same liturgical year, so it can never repeat a number that year's own January Sundays already used. The now-redundant property and its is_resumable_sunday_slug helper are removed from test_temporal_ef.ml; test_validate.ml's own domain-wide property covers the same ground for every consumer. 2. The anchors-erosion guard (Plan 2: deleting entries from a rite's anchors list left the whole suite green) is implemented, but not in Validate. Which of a rite's named days are Easter-derived is knowledge only the rite's own `named` function has; Rite.t deliberately exposes only `temporal` and `anchors`, never `named`, so a rite-agnostic Validate has no ground truth to check anchors' completeness against. Hardcoding an Easter offset, or even Easter itself, would smuggle Western/Gregorian-specific knowledge into code meant to also serve a future Julian-reckoning rite; rediscovering "named-ness" structurally from `temporal` alone is unsound for EF, since most ordinary Sunday/feria slugs from Septuagesima onward are also constant-offset-from-Easter by construction. The guard is therefore EF-specific and lives in test_temporal_ef.ml, discovering the Easter-derived slug set mechanically (scanning a window around Easter and keeping whatever `named` answers Some for) rather than hand-copying either named's or anchors' own offset list, then asserting completeness against the real anchors for the domain's Easter extremes (1598, 1666) plus an ordinary year. A negative fixture proves the guard has teeth, matching Plan 2's exact regression (anchors missing "ef-ascension" reports it, and only it, as missing). 3. test_validate.ml's extreme_years comment claimed 1818/2038; verified against Computus.gregorian_easter directly, the domain's actual Easter extremes (1583..2500) are 1598/1666. Corrected. Verification: the full 1583..9999 domain sweep (233 tests via dune test's 200-sample default, plus a manual full sweep) reports exactly one failure -- the known, already-pinned year-9999 season-truncation case -- and zero occurrences of the new "slugs" check anywhere in the domain. Deleting "ef-ascension" from the real anchors list (reproducing Plan 2's regression directly) is caught immediately by the new EF test and, confirmed empirically, invisible to Validate's own full property sweep -- direct evidence for why item 2 cannot live in Validate. --- lib/kernel/validate.ml | 49 +++++++++++++---- lib/kernel/validate.mli | 7 +++ test/test_temporal_ef.ml | 140 ++++++++++++++++++++++++++++++++++++----------- test/test_validate.ml | 24 +++++++- 4 files changed, 174 insertions(+), 46 deletions(-) (limited to 'lib/kernel/validate.ml') diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml index d8de31b..cc8bdce 100644 --- a/lib/kernel/validate.ml +++ b/lib/kernel/validate.ml @@ -20,6 +20,17 @@ let has_duplicate strings = let rec go = function a :: (b :: _ as rest) -> a = b || go rest | _ -> false in go sorted +(* Like [has_duplicate], but names the offender(s) instead of only reporting + that one exists -- the ["slugs"] check below wants a useful failure + detail, not just a bool. *) +let duplicates strings = + let sorted = List.sort String.compare strings in + let rec go acc = function + | a :: (b :: _ as rest) -> go (if a = b then a :: acc else acc) rest + | _ -> acc + in + List.sort_uniq String.compare (go [] sorted) + (* Task 12's "unconverged" check has no structural signal to key off -- Calendar's placement pass records its round-guard reason as a plain string in [Liturgical_day.omitted] (calendar.ml's own [unconverged_reason], @@ -85,18 +96,16 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = (* Weekday agreement. *) if t.Temporal.weekday <> Date.weekday date then fail date "weekday" "temporal weekday disagrees with Date.weekday"; - (* 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. *) + (* Slug: three properties. 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 asserted, below, once the whole + walk is in hand -- see the ["slugs"] check after this loop. *) (* Vocabulary closure. *) if not (List.exists (fun r -> vocab.Vocab.rank_to_string r = vocab.Vocab.rank_to_string cel.Celebration.rank) @@ -114,6 +123,22 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year = | None -> fail date "determinism" "a second call to temporal raised where the first succeeded")) days; let observed = List.rev !observed in + (* Slug uniqueness across the year (Plan 2 carried item 4): moved into + [Validate] itself so every consumer gets it, not only a 200-sample + QCheck property scoped to one rite. Asserted OUTRIGHT, no exemption: + Plan 2 verified zero duplicate slugs domain-wide, across all 8 416 + years, for the EF rite's own resumed-Sunday mechanism -- the exemption + the test property used to carry protected nothing real, because a + resumed Sunday only ever backfills a week number Septuagesima cut short + that same liturgical year (so it was never actually used that year to + begin with), never repeats one the year's own January Sundays already + used. If a future rite genuinely needs an exemption, it can supply one + then -- not speculatively here. *) + (match duplicates (List.map (fun (_, t) -> Slug.to_string t.Temporal.office.Celebration.slug) observed) with + | [] -> () + | dups -> + fail start "slugs" + (Printf.sprintf "slug(s) sighted on more than one date this year: %s" (String.concat ", " dups))); (* Season contiguity and completeness: the run-length-compressed sequence must equal the rite's own [season_runs] exactly, in canonical order. This is NOT necessarily [vocab.seasons] -- most rites have each season in one diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli index 511c78f..5e55fc5 100644 --- a/lib/kernel/validate.mli +++ b/lib/kernel/validate.mli @@ -17,6 +17,13 @@ val failure_to_string : failure -> string straddles two civil years, and checks only the pairs whose date actually falls within the year walked. + ["slugs"]: no two dates within the walked liturgical year may carry the + same office slug (Plan 2 carried item 4). Asserted outright, with no + exemption for the resumed-Sunday reuse a slug's own name might suggest: + a resumed Sunday only ever backfills a week number Septuagesima cut + short that same year, so by construction it never repeats a number that + year's own January Sundays actually used. + The season check compares the run-length-compressed season sequence against [rite.Rite.season_runs], not [rite.Rite.vocab.seasons]: a rite may have one season appear in two separate runs (the modern form's Ordinary diff --git a/test/test_temporal_ef.ml b/test/test_temporal_ef.ml index 2ad93e8..477651c 100644 --- a/test/test_temporal_ef.ml +++ b/test/test_temporal_ef.ml @@ -306,36 +306,112 @@ let test_christmastide_feria_slugs () = Alcotest.(check string) "13 Jan (Tue, on/after the origin)" "ef-time-after-epiphany-1-tuesday" (slug_of (d 2026 1 13)) -(* The general property behind the fix above: no two dates in one liturgical - year may share a slug, except the deliberate resumed-Sunday reuse (see - test_resumed_sundays). Random years across the whole domain, not just - 2026 -- the original bug (controller finding A) was found by grepping one - year's CLI output for duplicates, and other years could hide others. *) -let is_resumable_sunday_slug s = - let prefix = "ef-time-after-epiphany-sunday-" in - String.length s > String.length prefix && String.sub s 0 (String.length prefix) = prefix - -let prop_slugs_unique_within_liturgical_year = - QCheck.Test.make ~count:200 - ~name:"no two dates in one liturgical year share a slug, apart from the resumed-Sunday reuse" - (QCheck.int_range 1583 9998) +(* The general property behind the fix above -- no two dates in one + liturgical year may share a slug -- moved to + [Colitur_kernel.Validate]'s own ["slugs"] check (Plan 2 carried item 4), + asserted outright with no resumed-Sunday exemption: Plan 2 verified zero + duplicate slugs domain-wide, so the exemption this property used to carry + protected nothing real. [Validate]'s own 200-sample property + (test_validate.ml's [prop_invariants]) now covers every consumer, + including this rite, over the same 1583..9998 domain this property used + to sweep alone. *) + +(* ---- Plan 2 carried item 5: the anchors list has no guard against its own + erosion ---- + + [Colitur_kernel.Validate] cannot own this completeness check: which of + [named]'s entries are Easter-derived is knowledge only [named] itself + has. [Rite.t] deliberately exposes just [temporal] (the merged result) + and [anchors] (the independent restatement), never [named] -- so a + rite-agnostic [Validate] has no ground truth to compare [anchors] + against, short of inventing one. Two ways of inventing one were + considered and rejected: + + - Hardcoding a specific Easter offset (Ash Wednesday = Easter-46, say) + inside [Validate] would smuggle Western/Gregorian-Paschal-cycle + knowledge into code the design intends to also serve a future + Julian-reckoning rite (Byzantine, named explicitly as a future module + in this project's own architecture note) -- for which neither that + offset, nor even Gregorian Easter itself as the reference point + ([Computus.gregorian_easter], not [julian_easter]), is the right one. + Even [Computus]'s own [ash_wednesday]/[palm_sunday]/[ascension]/ + [pentecost] helpers are documented "(OF + EF)" -- i.e. already scoped + to the two WESTERN forms, not to "any rite" the way [Validate] must + stay. + - Rediscovering "Easter-derived" structurally from [temporal] alone (scan + near Easter, keep whatever recurs at the same offset across years with + different Easters) is unsound for EF specifically: [Time_after_epiphany] + onward, week numbering itself is computed from Easter-relative origins + ([week_origin]), so almost every ORDINARY Sunday/feria slug in + Septuagesima/Lent/Passiontide/Paschaltide/Time_after_pentecost is ALSO + constant-offset-from-Easter across years -- structurally + indistinguishable from a genuinely named day by that test alone. Rank + does not separate them either: RG 91 entry 10 makes the privileged + Easter/Pentecost octave FERIAS class 1 too, same as many named days. + + This guard is therefore entirely EF-specific and lives here, against + [T.named] and [T.anchors] directly -- both accessible in this file, not + through the [Rite.t] boundary. *) + +(* "Easter-derived" is discovered mechanically from [named] itself, not + hand-copied from either [named]'s or [anchors]'s own source: scan a + window of dates around a year's Easter and keep whatever [named] answers + [Some] for. [named] returns [Some] only for its ~20 genuinely proper/named + days -- ordinary Sundays and ferias are produced by other functions + entirely, in [temporal]'s [None] branch -- so this cannot pick up an + ordinary week's slug by accident regardless of window width. [-60, +75] + safely isolates the Easter-relative half of [named] from its + fixed-calendar half: exhaustively checked over 1583..2500, the nearest + fixed named date to Easter (6 January, Epiphany) is never less than 75 + days before the EARLIEST possible Easter (22 March), so a 60-day backward + reach cannot cross into it even in the closest year, while the window + still comfortably covers [named]'s actual Easter-relative range (Ash + Wednesday at Easter-46 the earliest, Sacred Heart at Easter+68 the + latest). *) +let easter_relative_named_slugs y = + let easter = Colitur_kernel.Computus.gregorian_easter y in + List.filter_map + (fun n -> match T.named (D.add_days easter n) with Some (_, slug, _, _) -> Some slug | None -> None) + (List.init 136 (fun i -> i - 60)) + |> List.sort_uniq compare + +let anchor_slugs y = List.map fst (T.anchors y) |> List.sort_uniq compare + +(* The mechanism both tests below share: which of [named]'s Easter-derived + slugs [anchors] fails to restate. [] means complete. *) +let missing_from_anchors ~named_easter_slugs ~anchors = + List.filter (fun slug -> not (List.mem slug anchors)) named_easter_slugs + +(* The real guard: for the domain's own Easter extremes (1598 earliest, 1666 + latest -- see test_validate.ml's own [extreme_years], corrected by this + same task) plus an ordinary year, nothing [named] produces at an + Easter-relative offset is missing from [anchors]. *) +let test_anchors_cover_easter_derived_named_days () = + List.iter (fun y -> - let start = T.year_start y in - let stop = D.add_days (T.year_start (y + 1)) (-1) in - let n = D.to_rata stop - D.to_rata start + 1 in - let seen = Hashtbl.create 512 in - let rec check i = - i >= n - || - let s = slug_of (D.add_days start i) in - (is_resumable_sunday_slug s - || (not (Hashtbl.mem seen s)) - && ( - Hashtbl.replace seen s (); - true)) - && check (i + 1) + let missing = + missing_from_anchors ~named_easter_slugs:(easter_relative_named_slugs y) ~anchors:(anchor_slugs y) in - check 0) + Alcotest.(check (list string)) + (Printf.sprintf "%d: every Easter-derived named slug is restated in anchors" y) + [] missing) + [ 1598; 1666; 2026 ] + +(* Proves the guard above actually has teeth, per this task's negative-fixture + requirement: [T.anchors]'s real slug set with one genuinely Easter-derived + entry ("ef-ascension") struck out must fail [missing_from_anchors] the same + way the real list passes it -- reproducing, in miniature, exactly what + "deleting four entries leaves the whole suite green" (Plan 2, carried item + 5) looked like before this test existed. *) +let test_anchors_erosion_is_caught () = + let y = 2026 in + let named_easter_slugs = easter_relative_named_slugs y in + Alcotest.(check bool) "sanity: ef-ascension is genuinely in the Easter-derived set" true + (List.mem "ef-ascension" named_easter_slugs); + let eroded_anchors = List.filter (fun s -> s <> "ef-ascension") (anchor_slugs y) in + Alcotest.(check (list string)) "the erosion is caught: the missing entry is reported, and only it" + [ "ef-ascension" ] + (missing_from_anchors ~named_easter_slugs ~anchors:eroded_anchors) let test_totality () = (* Every day of 2026 yields an office without raising. Not a slug @@ -367,12 +443,14 @@ let suite_extra = Alcotest.test_case "colours" `Quick test_colours; Alcotest.test_case "christmastide feria slugs" `Quick test_christmastide_feria_slugs; Alcotest.test_case "named days carry their week" `Quick test_named_days_carry_their_week; - Alcotest.test_case "totality" `Quick test_totality ] + Alcotest.test_case "totality" `Quick test_totality; + Alcotest.test_case "anchors cover easter-derived named days" `Quick + test_anchors_cover_easter_derived_named_days; + Alcotest.test_case "anchors erosion is caught" `Quick test_anchors_erosion_is_caught ] let suite = ( "Rite_ef", [ Alcotest.test_case "vocab roundtrips" `Quick test_vocab_roundtrips; Alcotest.test_case "slug words" `Quick test_slug_words ] @ suite_extra - @ List.map QCheck_alcotest.to_alcotest - [ prop_temporal_week_matches_week; prop_slugs_unique_within_liturgical_year ] ) + @ List.map QCheck_alcotest.to_alcotest [ prop_temporal_week_matches_week ] ) diff --git a/test/test_validate.ml b/test/test_validate.ml index b2d4f34..4b9c3c0 100644 --- a/test/test_validate.ml +++ b/test/test_validate.ml @@ -77,9 +77,10 @@ let extreme_years () = let test_easter_extremes () = let ys = extreme_years () in - (* 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). *) + (* Both extremes genuinely occur in 1583..2500 (earliest 1598, latest + 1666 -- verified against Computus.gregorian_easter directly, not + transcribed); 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 @@ -539,6 +540,22 @@ 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)) +(* Plan 2 carried item 4: slug uniqueness moves into [Validate] itself, no + exemption. [target] (17 March, mid-run) is given the NEXT day's real slug + verbatim -- a genuine collision between two distinct dates in the same + walked year, touching only the [slug] field so every other check (season, + week, weekday, rank, colour, determinism, anchor) stays silent against it. *) +let test_slugs_fires () = + let colliding_slug = (good (D.add_days target 1)).Temporal.office.Cel.slug 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.slug = colliding_slug } } + else t + in + Alcotest.(check bool) "slugs check fires when two dates in the year share a slug" true + (has_check "slugs" (run temporal)) + (* ---- Task 12: resolution invariants ---- Each test below asserts that exactly one of the five new check labels @@ -604,6 +621,7 @@ let suite = 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; + Alcotest.test_case "slugs fires" `Quick test_slugs_fires; Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception; Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires; Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires; -- cgit v1.3