diff options
| -rw-r--r-- | lib/kernel/validate.ml | 49 | ||||
| -rw-r--r-- | lib/kernel/validate.mli | 7 | ||||
| -rw-r--r-- | test/test_temporal_ef.ml | 138 | ||||
| -rw-r--r-- | test/test_validate.ml | 24 |
4 files changed, 173 insertions, 45 deletions
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 +(* 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. *) -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) +(* ---- 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; |