diff options
| -rw-r--r-- | lib/kernel/validate.ml | 132 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 46 | ||||
| -rw-r--r-- | test/test_validate.ml | 307 |
3 files changed, 458 insertions, 27 deletions
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:_ _ -> []) } +(* 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" -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) } +(* 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 ef_rite ~year +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 ] ) |