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. --- test/test_validate.ml | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'test/test_validate.ml') 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