diff options
| -rw-r--r-- | lib/rites/rite_ef/precedence_ef.ml | 35 | ||||
| -rw-r--r-- | lib/rites/rite_ef/precedence_ef.mli | 11 | ||||
| -rw-r--r-- | test/dune | 2 | ||||
| -rw-r--r-- | test/test_colitur.ml | 2 | ||||
| -rw-r--r-- | test/test_precedence_ef.ml | 32 | ||||
| -rw-r--r-- | test/test_rite_ef.ml | 81 |
6 files changed, 150 insertions, 13 deletions
diff --git a/lib/rites/rite_ef/precedence_ef.ml b/lib/rites/rite_ef/precedence_ef.ml index e1c13d1..b9b1731 100644 --- a/lib/rites/rite_ef/precedence_ef.ml +++ b/lib/rites/rite_ef/precedence_ef.ml @@ -573,6 +573,27 @@ let annunciation_slug = "annunciation-of-the-blessed-virgin-mary" than hanging the CLI. *) let max_search_days = 400 +(* The domain's own ceiling ({!Date.make}'s documented 1583..9999 bound, + also duplicated by calendar.ml's own [domain_max_date] for the same + reason: neither module exposes it to the other, and this is a three-line + constant, not worth a new signature just to share it). [search_from] + below must never call [occupant] on a date past this: [occupant] chains + through the rite's own [temporal] (calendar.ml's [resolve_with_injected]), + which for the real EF rite calls [Computus.gregorian_easter], which is + NOT total outside 1583..9999 -- it constructs a [Date.t] via [Date.make] + and [failwith]s on [Error]. [Date.add_days] itself has no such limit (it + is documented "unbounded total arithmetic"), so [search_from] CAN walk + [d] past 31 December 9999 without raising by itself -- the raise would + only happen on the NEXT [occupant d] call, which is exactly the bug this + guards against: an I-class feast impeded late enough in civil year 9999 + that every remaining day of the year is also I or II class (reachable + through the project's own overlay mechanism, confirmed by review: an + Add-ed I-class feast on 25 December leaves only Class2 Nativity-octave + days for the rest of 9999, so the unguarded walk reached 1 January 10000 + and crashed there). *) +let domain_max_date = + match Date.make ~year:9999 ~month:12 ~day:31 with Ok d -> d | Error e -> failwith e + (* Walks forward from [d], returning the first date [occupant] reports as NOT [is_blocking]. [steps] is a strictly increasing structural bound on the recursion, capped at [max_search_days]: the function decreases @@ -581,17 +602,19 @@ let max_search_days = 400 found), so THIS loop terminates by construction, regardless of what [occupant] reports -- it does not rely on the real EF calendar's own structure to guarantee termination the way the comment above explains - why the bound is never actually reached in practice. If the bound is - reached, the last date visited is returned WITHOUT probing [occupant] - again -- one more finite (not necessarily admissible) date, not a - further search -- because the val the caller ([transfer_target]) is - still owed is "a date", never an exception; {!Calendar}'s own + why the bound is never actually reached in practice. Also stops, without + calling [occupant] again, once [d] passes {!domain_max_date} -- see that + constant's own comment for why probing [occupant] beyond it can raise. + Either way the last date visited is returned WITHOUT a further + [occupant] probe -- one more finite (not necessarily admissible) date, + not a further search -- because the value the caller ([transfer_target]) + is still owed is "a date", never an exception; {!Calendar}'s own [~start ~stop] bound (calendar.ml's [place_transfers]) is what turns an implausible non-terminating real search into a recorded [omitted], not this function pretending to have found something admissible. *) let rec search_from (occupant : Date.t -> Vocab_ef.rank Celebration.t) (steps : int) (d : Date.t) : Date.t = - if steps >= max_search_days then d + if steps >= max_search_days || Date.compare d domain_max_date > 0 then d else if is_blocking (occupant d).Celebration.rank then search_from occupant (steps + 1) (Date.add_days d 1) else d diff --git a/lib/rites/rite_ef/precedence_ef.mli b/lib/rites/rite_ef/precedence_ef.mli index d06b058..7318ccd 100644 --- a/lib/rites/rite_ef/precedence_ef.mli +++ b/lib/rites/rite_ef/precedence_ef.mli @@ -199,10 +199,13 @@ val annunciation_slug : string round guard does not itself enforce (calendar.ml's [place_transfers] bounds ROUNDS across a whole year, not one call's internal walk). Terminating by a structural bound on the internal walk (max 400 days, - an engineering ceiling, not an RG citation -- see the .ml), not by an - argument about the real 1962 calendar's own structure, so a rite/data - shape this function has not anticipated fails FINITELY rather than - hanging the caller. Strictly later than [origin]: the ordinary search + an engineering ceiling, not an RG citation -- see the .ml) AND a guard + at {!Colitur_kernel.Date}'s own domain ceiling (31 December 9999, + beyond which probing [occupant] can itself raise -- see the .ml's + [domain_max_date]), not by an argument about the real 1962 calendar's + own structure, so a rite/data shape this function has not anticipated + fails FINITELY rather than hanging or crashing the caller. Strictly + later than [origin]: the ordinary search starts at [origin + 1] and only ever advances forward from there; the Annunciation's own starting point is provably later than 25 March for every representable year (Easter's documented range, register ยง0) -- @@ -1,7 +1,7 @@ (test (name test_colitur) (libraries colitur_kernel rite_ef alcotest qcheck qcheck-alcotest sexplib) - (deps ../data/ef/sanctoral.sexp) + (deps ../data/ef/sanctoral.sexp ../data/ef/adjustments.sexp) (preprocess (pps ppx_sexp_conv))) diff --git a/test/test_colitur.ml b/test/test_colitur.ml index ba82fcd..9f74e34 100644 --- a/test/test_colitur.ml +++ b/test/test_colitur.ml @@ -3,4 +3,4 @@ let () = Alcotest.run "colitur" [ Test_date.suite; Test_computus.suite; Test_colour.suite; Test_slug.suite; Test_names.suite; Test_overlay.suite; Test_temporal_ef.suite; Test_validate.suite; Test_precedence.suite; - Test_calendar.suite; Test_precedence_ef.suite; Test_sanctoral_ef.suite ] + Test_calendar.suite; Test_precedence_ef.suite; Test_sanctoral_ef.suite; Test_rite_ef.suite ] diff --git a/test/test_precedence_ef.ml b/test/test_precedence_ef.ml index 084d708..0973a93 100644 --- a/test/test_precedence_ef.ml +++ b/test/test_precedence_ef.ml @@ -897,6 +897,34 @@ let test_transfer_target_terminates_under_pathological_occupant () = true (D.compare target (D.add_days origin 1000) <= 0) +(* Coordinator review: [search_from] must not probe [occupant] past + {!Date}'s own domain ceiling (31 December 9999). A SYNTHETIC occupant + (like [occupant_always_blocking] above) can never actually discriminate + this: it never calls [Computus.gregorian_easter] itself, so it cannot + raise regardless of whether the domain guard exists -- a test built on + one would only prove [search_from]'s unrelated step bound, not this fix. + [occupant] here is instead the REAL [Temporal_ef.temporal] (no sanctoral + layer needed: 29-31 Dec are ALREADY II class via [named]'s own Nativity- + octave-day entries, so three real, unbroken blocking days already sit at + the very end of the domain) -- exactly the shape that raises without the + fix: 1 January of civil year 10000 is next, and [Computus.gregorian_easter + 10000] does [Date.make ~year:10000 ...] and [failwith]s (the .ml's own + [domain_max_date] comment; also how the reviewer reproduced the bug + through the project's own overlay mechanism -- see the task report for + that end-to-end reproduction). Mutation-verified: reverting the domain + guard makes this test error with exactly that uncaught [Failure], not + merely fail an assertion (see the task report). *) +let test_transfer_target_does_not_raise_at_domain_ceiling () = + let origin = mk 9999 12 28 in + let occupant d = (T.temporal d).Colitur_kernel.Temporal.office in + let c = cand ~origin:P.Sanctoral ~layer:PE.universal_layer "ef-domain-ceiling-case" in + let target = PE.transfer_target c origin occupant in + Alcotest.(check bool) "past 31 December 9999 (the guard engaged; nothing admissible remained \ + in-domain, so the search gave up at the ceiling rather than crashing)" + true + (D.compare target (mk 9999 12 31) > 0) + + let suite = ( "Precedence_ef", List.map @@ -947,4 +975,6 @@ let suite = "transfer_target: Annunciation exception searches onward if that Monday is blocked" `Quick test_transfer_target_annunciation_searches_onward_if_blocked; Alcotest.test_case "transfer_target: terminates and stays forward under a pathological occupant" - `Quick test_transfer_target_terminates_under_pathological_occupant ] ) + `Quick test_transfer_target_terminates_under_pathological_occupant; + Alcotest.test_case "transfer_target: does not raise probing past the domain ceiling" `Quick + test_transfer_target_does_not_raise_at_domain_ceiling ] ) diff --git a/test/test_rite_ef.ml b/test/test_rite_ef.ml new file mode 100644 index 0000000..7b60718 --- /dev/null +++ b/test/test_rite_ef.ml @@ -0,0 +1,81 @@ +(* Coordinator review (Task 11 fix round): integration tests wiring + [Rite_ef.context] together with the REAL data/ef/sanctoral.sexp + + data/ef/adjustments.sexp through [Colitur_kernel.Calendar] -- the same + pipeline `colitur day` uses, proven here at the OCaml level. *) + +module Cal = Colitur_kernel.Calendar +module Layer = Colitur_kernel.Layer +module Overlay = Colitur_kernel.Overlay +module LD = Colitur_kernel.Liturgical_day +module Slug = Colitur_kernel.Slug +module Date = Colitur_kernel.Date +module Date_spec = Colitur_kernel.Date_spec +module Cel = Colitur_kernel.Celebration +module Colour = Colitur_kernel.Colour +module V = Rite_ef.Vocab_ef + +(* Relative to this test's own build directory (_build/default/test/), same + convention test_sanctoral_ef.ml 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 real_layer () = + let layer = + match Layer.load V.rank_of_sexp sanctoral_path with + | Ok l -> l + | Error e -> Alcotest.failf "%s: failed to load: %s" sanctoral_path e + in + let overlay = + match Overlay.load V.rank_of_sexp adjustments_path with + | Ok o -> o + | Error e -> Alcotest.failf "%s: failed to load: %s" adjustments_path e + in + let layer, diagnostics = Overlay.apply layer overlay in + Alcotest.(check (list string)) "the committed overlay applies cleanly, no diagnostics" [] + (List.map Overlay.diagnostic_to_string diagnostics); + layer + +let slug_of (c : V.rank Cel.t) = Slug.to_string c.Cel.slug + +(* Coordinator review, finding 2, reproduced through the project's OWN + extension path (an overlay), the same way the reviewer found it: adding + an I-class feast on 25 December (competing against, and losing to, the + real Nativity) forces an RG 96 search starting 26 December -- which, with + the real sanctoral data (Stephen/John/the Innocents, all II class) plus + the temporal cycle's own Nativity-octave-day entries (29-31 Dec, also II + class), is blocking every single day through 31 December 9999. Before the + domain-ceiling fix this raised (Computus: year 10000 out of range); + confirmed by mutation-testing at the precedence_ef.ml unit level (see the + task report) -- this is the same defect reproduced end to end, through + Calendar, with real data, exactly as the review found it. *) +let test_transfer_search_does_not_raise_at_domain_ceiling () = + let layer = real_layer () in + let impeding_entry : V.rank Layer.entry = + { Layer.date = (match Date_spec.fixed ~month:12 ~day:25 with Ok d -> d | Error e -> failwith e); + cel = + Cel.make ~slug:(Slug.of_string_exn "test-domain-ceiling-impeder") ~rank:V.Class1 + ~colour:Colour.White ~layer:Rite_ef.Precedence_ef.universal_layer () } + in + let overlay : V.rank Overlay.t = + { Overlay.id = "test-domain-ceiling"; directives = [ Overlay.Add impeding_entry ] } + in + let layer, _diagnostics = Overlay.apply layer overlay in + (* Must not raise -- the whole point of the fix. *) + let days = Cal.year Rite_ef.context layer 9999 in + Alcotest.(check bool) "year 9999 resolves without raising, even with an impeded Christmas Day" + true (Array.length days > 0); + let impeder_placed_or_recorded = + Array.to_list days + |> List.exists (fun d -> + slug_of d.LD.observed = "test-domain-ceiling-impeder" + || List.exists (fun (c, _) -> slug_of c = "test-domain-ceiling-impeder") d.LD.omitted) + in + Alcotest.(check bool) "the impeding candidate is accounted for (observed somewhere, or omitted \ + with a recorded reason) -- never silently dropped" + true impeder_placed_or_recorded + +let suite = + ( "Rite_ef (real data: overlay-in-effect, domain-ceiling)", + [ Alcotest.test_case "RG96 search does not raise at the domain ceiling (real data)" `Quick + test_transfer_search_does_not_raise_at_domain_ceiling ] ) |