diff options
| author | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-11 21:29:13 +0200 |
|---|---|---|
| committer | Lukasz Kasprzak <lukas@labunix.xyz> | 2026-08-11 21:29:13 +0200 |
| commit | 1d6be4ac281e62accfb905b137b3c6b494183ee4 (patch) | |
| tree | 20e34ee8773db4cbcb8f06a29835a087a5219b8a /test/test_calendar.ml | |
| parent | f15e44dd4c1b871c2daeb952b1c8c848274ea1f1 (diff) | |
| download | colitur-1d6be4ac281e62accfb905b137b3c6b494183ee4.tar.gz colitur-1d6be4ac281e62accfb905b137b3c6b494183ee4.zip | |
kernel(calendar): fix multi-departure loss, band-order gap, off-array targets
Four findings from Task 6 review, addressed on top of f15e44d.
1. transferred_out was a single Date.t option, so when RG 97-98 collides
three or more feasts on one date (more than one loser), only the last
one Hashtbl.iter happened to visit survived -- a genuinely lost move,
and which one survived depended on OCaml's hash seed
(OCAMLRUNPARAM=R), an environment read a kernel invariant forbids.
RG 97-98 says coinciding feasts transfer "in order" -- plural -- so
the type was wrong, not the fixture: transferred_out is now
(Celebration.t * Date.t) list. transferred_in stays a single option,
deliberately: a day receives at most one arrival (RG 96 sends each
departure to the next non-I/II-class day, and the first to arrive
occupies it). The per-day list is canonicalised (sorted by target
date, then slug) after accumulation, the same fix layer.ml already
applies to its own date-bucket index and for the same reason.
Verified clean across 15 runs under OCAMLRUNPARAM=R; disabling the
canonicalisation step showed the raw order genuinely flip between
seeds, confirming the fix is load-bearing.
2. Every deferred candidate in the fixture was the same rank, so
compare_deferred's band branch was unreachable and reversing it broke
nothing -- the RG 97-98 test was pinning slug order, not band order.
The fixture now has three ranks (Hi1 outranks Hi2, both transfer,
both outrank Lo), with slugs chosen so band order and slug order
disagree. Reversing the band comparison now fails the test on
"higher-band loser claims 2 Feb first", received the wrong slug
instead.
3. A transfer_target free to name any date could place a candidate
outside the liturgical year's own start/stop bounds: invisible to
year/build_day, so it would be observed nowhere and, since its
origin's re-resolution would report it as settled, omitted nowhere
either -- genuinely gone, contradicting calendar.mli's "never
silently dropped". place_transfers now checks the range on every
placement and routes an out-of-range one to a permanent-exclusion
table instead of assignment, with its own cited omitted reason.
4. Precedence.resolve folds Transfer and Repose into one deferred case,
and place_transfers routed all of it through transfer_target (RG
96's search), which is only correct for Transfer. Repose is RG
100-102's repositio, a distinct rubric this module does not
implement. Documented rather than split into a second mechanism:
nothing in the EF ruleset returns Repose (design spec section 1.3,
"declared, not exercised"), so the gap is latent, not a live bug.
Two new tests (origin records every departure; transfer target outside
year is recorded not lost); the RG 97-98 test's fixture and assertions
rewritten for finding 2.
Diffstat (limited to 'test/test_calendar.ml')
| -rw-r--r-- | test/test_calendar.ml | 207 |
1 files changed, 142 insertions, 65 deletions
diff --git a/test/test_calendar.ml b/test/test_calendar.ml index 70823a4..505994e 100644 --- a/test/test_calendar.ml +++ b/test/test_calendar.ml @@ -9,8 +9,16 @@ let mk y m d = match D.make ~year:y ~month:m ~day:d with Ok t -> t | Error e -> (* A synthetic rite -- not EF -- so Calendar's behaviour is proven against the abstraction, not against EF's own real (and much larger) data. Two - seasons, two ranks: enough to exercise the type parameters without - dragging in real liturgical logic Calendar itself does not compute. *) + seasons, three ranks: enough to exercise the type parameters without + dragging in real liturgical logic Calendar itself does not compute. + + Three ranks, not two: Task 6 review finding 2. With only one + Transfer-disposed rank, every deferred candidate ties on [band] and + [compare_deferred]'s [b1 <> b2] branch (the one RG 97-98 actually depends + on -- coinciding I-class feasts transfer in TABLE order, not slug order) + was unreachable; reversing it broke no test. [Hi1] outranks [Hi2], both + outrank [Lo], both are [Transfer]-disposed -- so two colliding + transferables can now differ by band, not only by slug. *) module Fixture = struct module Vocab = Colitur_kernel.Vocab module Colour = Colitur_kernel.Colour @@ -20,16 +28,16 @@ module Fixture = struct module Date_spec = Colitur_kernel.Date_spec type season = A | B - type rank = Hi | Lo + type rank = Hi1 | Hi2 | Lo let season_to_string = function A -> "a" | B -> "b" let season_of_string = function "a" -> Some A | "b" -> Some B | _ -> None - let rank_to_string = function Hi -> "hi" | Lo -> "lo" - let rank_of_string = function "hi" -> Some Hi | "lo" -> Some Lo | _ -> None + let rank_to_string = function Hi1 -> "hi1" | Hi2 -> "hi2" | Lo -> "lo" + let rank_of_string = function "hi1" -> Some Hi1 | "hi2" -> Some Hi2 | "lo" -> Some Lo | _ -> None let vocab : (season, rank) Vocab.t = { Vocab.seasons = [ A; B ]; season_to_string; season_of_string; - ranks = [ Hi; Lo ]; rank_to_string; rank_of_string } + ranks = [ Hi1; Hi2; Lo ]; rank_to_string; rank_of_string } let weekday_index d = match D.weekday d with @@ -59,14 +67,15 @@ module Fixture = struct let temporal date : (season, rank) Temporal.t = { Temporal.season = season date; week = None; weekday = D.weekday date; office = office date } - (* Band: Hi beats Lo; Temporal breaks a tie in its own favour -- the same - convention test_precedence.ml uses. *) + (* Band: Hi1 beats Hi2 beats Lo; Temporal breaks a tie against a Lo-rank + Sanctoral entry in its own favour -- the same convention + test_precedence.ml uses. *) let band (_ : season P.context) (c : rank P.candidate) = - (match c.P.cel.Cel.rank with Hi -> 10 | Lo -> 20) + (match c.P.cel.Cel.rank with Hi1 -> 5 | Hi2 -> 10 | Lo -> 20) - (match c.P.origin with P.Temporal -> 1 | P.Sanctoral -> 0) let disposition ~winner:_ ~(loser : rank P.candidate) = - match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi -> P.Transfer + match loser.P.cel.Cel.rank with Lo -> P.Commemorate P.Ordinary | Hi1 | Hi2 -> P.Transfer (* Admits at most one commemoration -- mirrors test_precedence.ml's own example and, unlike "admit everything", actually gives the accounting @@ -77,12 +86,12 @@ module Fixture = struct (* RG 96, generic form: search forward from the day after [origin] for the first day whose occupant is not "blocking" -- in this synthetic - vocabulary Hi stands in for I/II class, Lo for everything else (the same - convention [band] already uses). No Annunciation-style starting-point - override: that exception is EF-specific (RG 96) and belongs to the real - rite (Task 11, pinned by Task 17's golden years), not to this - abstraction-level fixture, which only has to prove Calendar's placement - mechanism, not EF's own rubrics. *) + vocabulary Hi1/Hi2 stand in for I/II class, Lo for everything else (the + same convention [band] already uses). No Annunciation-style + starting-point override: that exception is EF-specific (RG 96) and + belongs to the real rite (Task 11, pinned by Task 17's golden years), + not to this abstraction-level fixture, which only has to prove + Calendar's placement mechanism, not EF's own rubrics. *) let transfer_target (_ : rank P.candidate) (origin : D.t) (occupant : D.t -> rank Cel.t) : D.t = let rec search d = if (occupant d).Cel.rank = Lo then d else search (D.add_days d 1) in search (D.add_days origin 1) @@ -96,20 +105,20 @@ module Fixture = struct cel = Cel.make ~slug:(Sl.of_string_exn slug) ~rank ~colour:Colour.White ~layer:"synthetic-sanctoral" () } - let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi + let big_feast = entry ~month:12 ~day:8 ~slug:"big-feast" ~rank:Hi1 let commem_worthy = entry ~month:12 ~day:15 ~slug:"commem-worthy" ~rank:Lo (* 20 Dec: four sanctoral entries on one date, for the full-accounting test. - "day-winner" and "eclipsed" tie on band (both Hi, both Sanctoral); ties - break on slug, so "day-winner" wins and "eclipsed" -- a Hi-rank loser -- - is [Transfer]-disposed, landing in [deferred]. "loser-a" and "loser-b" - are both Lo, both [Commemorate]-disposed, but [admit] only keeps one: - the other lands in Precedence's own [omitted] ("admission limit - reached"), distinct from "eclipsed"'s deferred reason. Four candidates, - three different fates -- observed, one specific omission reason, two - more. *) - let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi - let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi + "day-winner" and "eclipsed" tie on band (both Hi1, both Sanctoral); + ties break on slug, so "day-winner" wins and "eclipsed" -- a Hi1-rank + loser -- is [Transfer]-disposed, landing in [deferred]. "loser-a" and + "loser-b" are both Lo, both [Commemorate]-disposed, but [admit] only + keeps one: the other lands in Precedence's own [omitted] ("admission + limit reached"), distinct from "eclipsed"'s deferred reason. Four + candidates, three different fates -- observed, one specific omission + reason, two more. *) + let day_winner = entry ~month:12 ~day:20 ~slug:"day-winner" ~rank:Hi1 + let eclipsed = entry ~month:12 ~day:20 ~slug:"eclipsed" ~rank:Hi1 let loser_a = entry ~month:12 ~day:20 ~slug:"loser-a" ~rank:Lo let loser_b = entry ~month:12 ~day:20 ~slug:"loser-b" ~rank:Lo @@ -118,33 +127,40 @@ module Fixture = struct [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b ] (* RG 96 (Task 6): "transferable" is impeded on 10 Jan by "blocker-a" (both - Hi; ties break on slug, "blocker-a" < "transferable", so "blocker-a" + Hi1; ties break on slug, "blocker-a" < "transferable", so "blocker-a" wins and "transferable" is the loser). 11 and 12 Jan are ALSO occupied - by their own uncontested Hi-rank entries, so the placement search must + by their own uncontested Hi1-rank entries, so the placement search must walk past more than one ineligible day, not just try origin+1 and stop. 13 Jan carries nothing, so the feria (Lo) is the first admissible day. *) - let blocker_a = entry ~month:1 ~day:10 ~slug:"blocker-a" ~rank:Hi - let transferable = entry ~month:1 ~day:10 ~slug:"transferable" ~rank:Hi - let blocker_b = entry ~month:1 ~day:11 ~slug:"blocker-b" ~rank:Hi - let blocker_c = entry ~month:1 ~day:12 ~slug:"blocker-c" ~rank:Hi + let blocker_a = entry ~month:1 ~day:10 ~slug:"blocker-a" ~rank:Hi1 + let transferable = entry ~month:1 ~day:10 ~slug:"transferable" ~rank:Hi1 + let blocker_b = entry ~month:1 ~day:11 ~slug:"blocker-b" ~rank:Hi1 + let blocker_c = entry ~month:1 ~day:12 ~slug:"blocker-c" ~rank:Hi1 - (* RG 97-98: three Hi-rank entries coincide on 1 Feb. Sorted by band then - slug (all three tie on band, since Fixture's [band] only reads rank): - "collision-winner" < "transfer-a" < "transfer-b". The winner keeps 1 - Feb; the other two -- both losers, both Hi, both [Transfer]-disposed -- - must transfer in that same order. 2 and 3 Feb carry nothing of their - own, so they are the two admissible days the pair must land on, - consecutively, in that order: "transfer-a" (the higher-precedence - loser) gets first claim on 2 Feb, pushing "transfer-b" to 3 Feb. *) - let collision_winner = entry ~month:2 ~day:1 ~slug:"collision-winner" ~rank:Hi - let transfer_a = entry ~month:2 ~day:1 ~slug:"transfer-a" ~rank:Hi - let transfer_b = entry ~month:2 ~day:1 ~slug:"transfer-b" ~rank:Hi + (* RG 97-98: three entries coincide on 1 Feb, spanning both Transfer- + disposed ranks so band order and slug order genuinely disagree (Task 6 + review finding 2). "collision-winner" and "transfer-hi1" both tie at + the BETTER band (Hi1, 5); "transfer-hi2" is at the WORSE band (Hi2, + 10). Within the Hi1 tie, slug decides: "collision-winner" < "transfer- + hi1", so "collision-winner" keeps 1 Feb. Of the two losers, + "transfer-hi1" (band 5) outranks "transfer-hi2" (band 10) -- by BAND, + not by slug: "transfer-b" (transfer-hi2's slug) sorts alphabetically + *before* "transfer-z" (transfer-hi1's slug). A sort that used slug + instead of band, or compared band backwards, would place "transfer-b" + on 2 Feb instead of "transfer-z" -- exactly the wrong-order failure + mode finding 2 flagged as unreachable in the old two-Hi-rank fixture. + 2 and 3 Feb carry nothing of their own, so they are the two admissible + days the pair must land on, consecutively, in band order: + "transfer-hi1" claims 2 Feb, pushing "transfer-hi2" to 3 Feb. *) + let collision_winner = entry ~month:2 ~day:1 ~slug:"collision-winner" ~rank:Hi1 + let transfer_hi1 = entry ~month:2 ~day:1 ~slug:"transfer-z" ~rank:Hi1 + let transfer_hi2 = entry ~month:2 ~day:1 ~slug:"transfer-b" ~rank:Hi2 let layer_with_collision = Layer.of_entries ~id:"synthetic-with-collision" ~name:"Synthetic sanctoral (with collisions)" [ big_feast; commem_worthy; day_winner; eclipsed; loser_a; loser_b; blocker_a; transferable; blocker_b; blocker_c; - collision_winner; transfer_a; transfer_b ] + collision_winner; transfer_hi1; transfer_hi2 ] let liturgical_year_of date = let cy = D.year date in @@ -231,7 +247,7 @@ let test_day_near_domain_floor_does_not_raise () = duplicated into two buckets and another dropped, which this project has shipped before (register finding). - "eclipsed" -- the Hi-rank loser on 20 Dec -- no longer sits in [omitted] + "eclipsed" -- the Hi1-rank loser on 20 Dec -- no longer sits in [omitted] here (that was Task 5's honest placeholder, before Task 6 existed to place it): RG 95 gives an I-class loser the right of translation, so it is genuinely gone from this day's own accounting, and its departure is @@ -265,14 +281,14 @@ let test_full_day_accounting () = not something new. What IS new here: this day positively records that a transfer happened, via a different field entirely. *) Alcotest.(check bool) "20 Dec records that something transferred out" true - (d.LD.transferred_out <> None) + (d.LD.transferred_out <> []) (* Task 6's placement pass (RG 96-98), properties 1 and 2: a transferred celebration appears exactly once in the whole year -- transfer moves, not duplicates -- and [transferred_in]/[transferred_out] are set on the two ends of the move and point at each other. "transferable" is impeded on 10 Jan by "blocker-a" (same band, tie-broken by slug), and 11-12 Jan are also - occupied by their own uncontested Hi entries, so this also proves the + occupied by their own uncontested Hi1 entries, so this also proves the search walks past more than one ineligible day rather than only trying origin+1. *) let test_transfer_moves_and_does_not_duplicate () = @@ -292,22 +308,31 @@ let test_transfer_moves_and_does_not_duplicate () = | Some c -> Sl.to_string c.Cel.slug | None -> "<none>"); (* Located by its own known origin date, not by "the first day with - transferred_out set" -- layer_with_collision has more than one day that - transfers something out (20 Dec's "eclipsed", 1 Feb's "transfer-b"), so - that would silently pick up whichever happens to sort first in the - array rather than proving THIS origin points at THIS landing. *) + transferred_out <> []" -- layer_with_collision has more than one day + that transfers something out (20 Dec's "eclipsed", 1 Feb's two losers), + so that would silently pick up whichever happens to sort first in the + array rather than proving THIS origin points at THIS landing. Its own + origin has exactly one departure -- unlike 1 Feb below -- so a single + pair pins it. *) let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2027 1 10) = 0) in - Alcotest.(check bool) "origin points at the landing date" true - (origin.LD.transferred_out = Some landed.LD.date) + Alcotest.(check int) "exactly one departure recorded at the origin" 1 + (List.length origin.LD.transferred_out); + let departed_cel, departed_to = List.hd origin.LD.transferred_out in + Alcotest.(check string) "the departed celebration is \"transferable\"" "transferable" + (Sl.to_string departed_cel.Cel.slug); + Alcotest.(check string) "it points at the landing date" (D.to_iso8601 landed.LD.date) + (D.to_iso8601 departed_to) -(* Property 3: RG 97-98's ordering. Two Hi-rank losers coincide on 1 Feb - (with "collision-winner" keeping the day); band ties, so slug order IS - band order here, same convention Precedence.compare_by uses for real RG - 91 entries that tie within one table slot. Checked by DATE, not by - "b landed one day after a" -- Task 5's review flagged exactly that - style of check as satisfiable by construction (an Array.init built from - add_days would pass it trivially); asserting the literal landing dates - independently is what actually exercises the placement order. *) +(* Property 3: RG 97-98's ordering, genuinely by band (Task 6 review finding + 2) -- see the [layer_with_collision] comment for how the fixture is built + so band order and slug order actively disagree here: "transfer-hi1" + (slug "transfer-z", band 5) must claim 2 Feb before "transfer-hi2" (slug + "transfer-b", band 10), even though "transfer-b" sorts alphabetically + first. Checked by DATE, not by "b landed one day after a" -- Task 5's + review flagged exactly that style of check as satisfiable by construction + (an Array.init built from add_days would pass it trivially); asserting + the literal landing dates independently is what actually exercises the + placement order. *) let test_two_colliding_transferables_land_in_band_order () = let days = C.year Fixture.rite Fixture.layer_with_collision 2026 in let observed_on date = @@ -317,18 +342,66 @@ let test_two_colliding_transferables_land_in_band_order () = in Alcotest.(check string) "collision-winner keeps 1 Feb" "collision-winner" (observed_on (mk 2027 2 1)); - Alcotest.(check string) "higher-precedence loser (transfer-a) claims 2 Feb first" "transfer-a" + Alcotest.(check string) "higher-band loser (transfer-z, Hi1) claims 2 Feb first" "transfer-z" (observed_on (mk 2027 2 2)); - Alcotest.(check string) "lower-precedence loser (transfer-b) is pushed to 3 Feb" "transfer-b" + Alcotest.(check string) "lower-band loser (transfer-b, Hi2) is pushed to 3 Feb" "transfer-b" (observed_on (mk 2027 2 3)); let count slug = Array.to_list days |> List.filter (fun d -> Sl.to_string d.LD.observed.Cel.slug = slug) |> List.length in - Alcotest.(check int) "transfer-a appears exactly once in the year" 1 (count "transfer-a"); + Alcotest.(check int) "transfer-z appears exactly once in the year" 1 (count "transfer-z"); Alcotest.(check int) "transfer-b appears exactly once in the year" 1 (count "transfer-b") +(* Task 6 review finding 1: RG 97-98 says coinciding I-class feasts transfer + "in order" -- plural -- so 1 Feb's origin must record BOTH departures + ("transfer-z" -> 2 Feb, "transfer-b" -> 3 Feb), not just one. The + original [Date.t option] could only ever hold one; with three entries + colliding on the same date it silently dropped whichever [Hashtbl.iter] + visited last, which depends on OCaml's hash seed (OCAMLRUNPARAM=R) -- an + environment read in a kernel whose invariants forbid one. Sorting both + sides before comparing makes this assertion itself independent of + [transferred_out]'s own (now canonicalised, but not part of the + contract) internal order. *) +let test_origin_records_every_departure () = + let days = C.year Fixture.rite Fixture.layer_with_collision 2026 in + let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2027 2 1) = 0) in + let departures = + origin.LD.transferred_out + |> List.map (fun (c, target) -> (Sl.to_string c.Cel.slug, D.to_iso8601 target)) + |> List.sort compare + in + Alcotest.(check (list (pair string string))) + "both losers' departures are recorded, order-independently" + (List.sort compare [ ("transfer-z", "2027-02-02"); ("transfer-b", "2027-02-03") ]) + departures + +(* Task 6 review finding 3: a rite whose [transfer_target] names a date + outside the liturgical year's own [start, stop] must not make the + candidate vanish. "eclipsed" is impeded on 20 Dec as usual, but this + rite's search jumps 5000 days forward -- far past [stop] -- instead of + walking to the next admissible day. It must never become [observed] + anywhere in the array (there is nowhere in the array for it to land), + and its origin must record the specific out-of-range reason, not the + generic non-convergence one (this placement decides on round 1; the + round guard is never even approached). *) +let test_transfer_target_outside_year_is_recorded_not_lost () = + let stray_rite = + { Fixture.rite with Rite.transfer_target = (fun _ origin _ -> D.add_days origin 5000) } + in + let days = C.year stray_rite Fixture.layer 2026 in + let observed_anywhere = + Array.to_list days |> List.exists (fun d -> Sl.to_string d.LD.observed.Cel.slug = "eclipsed") + in + Alcotest.(check bool) "never becomes observed anywhere in the year" false observed_anywhere; + let origin = Array.to_list days |> List.find (fun d -> D.compare d.LD.date (mk 2026 12 20) = 0) in + let reason_of slug = + origin.LD.omitted |> List.find (fun (c, _) -> Sl.to_string c.Cel.slug = slug) |> snd + in + Alcotest.(check string) "recorded with the out-of-range reason, not silently dropped" + "omitted: transfer target falls outside the liturgical year (RG 96)" (reason_of "eclipsed") + (* Termination is a correctness requirement (brief): a rite whose [transfer_target] always answers with the impeded day itself (never strictly forward, so the pass can never reach a fixed point) must not @@ -366,5 +439,9 @@ let suite = test_transfer_moves_and_does_not_duplicate; Alcotest.test_case "two colliding transferables land in band order" `Quick test_two_colliding_transferables_land_in_band_order; + Alcotest.test_case "origin records every departure" `Quick + test_origin_records_every_departure; + Alcotest.test_case "transfer target outside year is recorded not lost" `Quick + test_transfer_target_outside_year_is_recorded_not_lost; Alcotest.test_case "transfer guard records failure instead of looping" `Quick test_transfer_guard_records_failure_instead_of_looping ] ) |
