1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
|
(* RG 475-476, the Creed -- see lib/rites/rite_ef/rubrics_ef.ml for the
rubric quoted in full and every branch's own citation.
One end-to-end test per clause of 475, plus a 476 negative, resolved
against REAL calendar dates through the shipped sanctoral data (the same
pipeline `colitur day`/`colitur rubrics` use) -- every expected value
below was derived from the rubric's own text and checked against
`colitur day <year>`'s real output (slug/rank/subject/weekday) BEFORE
this module existed, never read off [Rubrics_ef.creed]'s own answer.
Two synthetic unit tests isolate Trap One (RG 475(a) reads [temporal],
never [observed]) directly, without depending on finding a real-calendar
coincidence.
One further test (celebrant-rubrics-phase1 review, finding 1) is
different in kind from the rest: not an end-to-end [creed] check
against a single real date, but a direct sweep of {!Rite_ef.Temporal_ef}
output across a century, asserting the unstated invariant [creed]'s own
RG 24/25 ferial branches rely on rather than leaving it asserted only
in prose -- see its own header comment for the full account. *)
module Cal = Colitur_kernel.Calendar
module LD = Colitur_kernel.Liturgical_day
module Date = Colitur_kernel.Date
module Cel = Colitur_kernel.Celebration
module Colour = Colitur_kernel.Colour
module Subject = Colitur_kernel.Subject
module Slug = Colitur_kernel.Slug
module Temporal = Colitur_kernel.Temporal
module V = Rite_ef.Vocab_ef
module RE = Rite_ef.Rubrics_ef
module TE = Rite_ef.Temporal_ef
let mk y m d = match Date.make ~year:y ~month:m ~day:d with Ok t -> t | Error e -> failwith e
(* Loaded once, module-level: every test below is a lookup against the same
shipped calendar, and {!Cal.day} recomputes its whole liturgical year on
every call (calendar.mli's own documented cost), so at minimum the layer
itself should not be reloaded and re-merged per test case. *)
let layer =
match Test_support.load_ef_layer () with Ok l -> l | Error e -> Alcotest.failf "%s" e
let ctx = Test_support.ef_context ()
let creed_on y m d = (Cal.day ctx layer (mk y m d)).LD.creed
let check name y m d expected = Alcotest.(check bool) name expected (creed_on y m d)
(* ---- RG 475(a): "in qualibet dominica, etsi eius Officium alicui festo
locum cedat" ---- *)
let test_475a_ordinary_sunday () =
(* 2026-01-25: an ordinary Time-after-Epiphany Sunday, Class2, green,
"Dominica III post Epiphaniam" -- confirmed via `colitur day 2026`,
no other clause of 475 could apply (Class2, subject Temporal, no
octave, no apostle/vigil slug), so [true] here can only come from
475(a) itself. *)
check "475(a): an ordinary Sunday" 2026 1 25 true
(* Trap One, isolated directly: RG 475(a)'s own "ETSI EIUS OFFICIUM ALICUI
FESTO LOCUM CEDAT" -- even when a feast has displaced the Sunday's own
office, the Creed is still said. [observed] below is deliberately shaped
so that NONE of 475(b)/(c)/(e) can produce [true] on their own (Class3,
subject Saint, a slug on no list this module knows); the only way
[creed] can return [true] is by reading [temporal]'s own [weekday],
never [observed]. The synthetic [date] (an ordinary July day, itself a
Wednesday in 2026) is chosen so nothing about the DATE itself suggests
a Sunday either -- proving the function reads [temporal.weekday], not
[Date.weekday date]. *)
let impeded_observed =
Cel.make ~slug:(Slug.of_string_exn "some-impeding-feast-of-the-lord") ~rank:V.Class3
~status:Cel.Feast ~colour:Colour.Red ~subject:Subject.Saint ~layer:"synthetic" ()
let synthetic_temporal ~weekday : (V.season, V.rank) Temporal.t =
{ Temporal.season = V.Time_after_pentecost; week = Some 1; weekday; office = impeded_observed }
let test_475a_reads_temporal_not_observed () =
Alcotest.(check bool) "Sunday-shaped [temporal] overrides a non-Sunday-shaped [observed]" true
(RE.creed ~temporal:(synthetic_temporal ~weekday:Date.Sun) ~observed:impeded_observed
~date:(mk 2026 7 1));
Alcotest.(check bool) "same [observed], non-Sunday [temporal]: false" false
(RE.creed ~temporal:(synthetic_temporal ~weekday:Date.Wed) ~observed:impeded_observed
~date:(mk 2026 7 1))
(* ---- RG 475(b): "in festis I classis" ---- *)
let test_475b_class1_feast () =
(* 2026-08-15: the Assumption, Class1. *)
check "475(b): a I-class feast" 2026 8 15 true
(* ---- RG 475(c): "in festis II classis Domini et B. Mariae Virg." ---- *)
let test_475c_lord () =
(* 2026-09-14: Exaltation of the Holy Cross, Class2, subject Lord. *)
check "475(c): a II-class feast of the Lord" 2026 9 14 true
let test_475c_bvm_via_marian_slugs () =
(* 2026-08-22: Immaculate Heart of Mary, Class2 -- ships [subject =
Saint] in data/ef/sanctoral.sexp (confirmed by grep), so this can only
come out [true] via {!Rite_ef.Precedence_ef.marian_slugs}, not via
[subject = Bvm]. Also carries a real commemoration
(+sts-timothy-hippolytus-and-symphorianus-martyrs), a live instance of
476(e): the commemoration plays no part in this answer. *)
check "475(c): a II-class BVM feast (via marian_slugs, subject=Saint in the data)" 2026 8 22 true
(* ---- RG 475(d): "per octavas Nativitatis Domini, Paschatis et
Pentecostes, etiam in festis occurrentibus et in Missis votivis" ---- *)
let test_475d_octave_even_occurring_feast () =
(* 2026-12-26: St Stephen, Class2, "S. Stephani Protomartyris" -- a real
saint's feast OCCURRING within the Octave of the Nativity (RG 67's own
"Com. octavae Nativitatis", carried as +ef-nativity-octave-day-2 in
colitur's own commemoration). RG 475(d)'s own "etiam in festis
occurrentibus" is written for exactly this shape: the Creed is said
regardless. (This is the one place this suite deliberately diverges
from the task brief's own worked example, which expected [false] here
-- the brief mis-cited 26 December as 476(b)'s "plain II-class feast"
case, missing that RG 475(d) explicitly overrides 476(b) inside the
Nativity octave; see the task report.) *)
check "475(d): a saint's feast occurring within the Nativity octave" 2026 12 26 true
let test_475d_octave_day_boundary () =
(* 2026-01-01: the Octave Day of the Nativity itself (Circumcision),
Class1 -- also [true] via 475(b) alone, kept as a boundary check that
1 January is correctly included in the 8-day window. *)
check "475(d): 1 January, the Octave Day of the Nativity" 2026 1 1 true
(* ---- RG 475(e): "in festis nataliciis Apostolorum et Evangelistarum,
necnon in festis Cathedrae S. Petri et S. Barnabae Ap." ---- *)
let test_475e_apostle_natalicium () =
(* 2026-11-30: St Andrew, Class2, subject Saint -- not covered by 475(c)
(not Domini/BVM), so [true] here can only come from 475(e)'s own
natalicia list. Also carries a real commemoration
(+ef-advent-1-monday), another live 476(e) instance. *)
check "475(e): an Apostle's own natalicium (Andrew)" 2026 11 30 true
let test_475e_barnabas_named_explicitly () =
(* 2026-06-11: St Barnabas, Class3 -- named explicitly by the clause
("S. Barnabae Ap."); at Class3 it could not reach [true] via 475(b) or
(c) regardless. *)
check "475(e): St Barnabas, named explicitly" 2026 6 11 true
let test_475e_chair_of_peter_named_explicitly () =
(* 2027-02-22 (NOT 2026: Feb 22 2026 is impeded by Lent I Sunday, so the
Chair is not observed that year -- checked via `colitur day 2026`
before picking 2027 instead): the Chair of St Peter, Class2, subject
Saint -- NOT a natalicium (Peter's own is 29 June, shared with Paul),
so [true] here can only come from the clause's own explicit "Cathedrae
S. Petri" naming, not from the natalicium reading in general. *)
check "475(e): the Chair of St Peter, named explicitly (not a natalicium)" 2027 2 22 true
let test_475e_excludes_conversion_of_paul () =
(* Trap Two, directly: 2027-01-25, the Conversion of St Paul, Class3 --
names an Apostle but is NOT his natalicium (his own is 29 June, with
Peter); Class3 rules out 475(b)/(c), and this slug is deliberately
absent from [creed_apostle_slugs]. Picked 2027 for the same impeded-
Sunday reason as the Chair of Peter above (25 January 2026 is itself a
Sunday). *)
check "475(e) does NOT cover the Conversion of St Paul (not a natalicium)" 2027 1 25 false
(* ---- RG 23 (feriae) / RG 476(a): Ash Wednesday, Holy Week's own feriae,
the Chrism/Lord's Supper Mass, the Easter Vigil Mass ---- *)
let test_ash_wednesday_no_creed () =
check "RG 23(a)/476: Ash Wednesday, a I-class FERIA, not a festum" 2026 2 18 false
let test_holy_thursday_no_creed () =
(* 2026-04-02: "Feria V in Cena Domini" -- RG 23(b)'s own "omnes feriae
Hebdomadae sanctae"; also explicitly named by 476(a) ("sive... in
Cena Domini"). *)
check "RG 23(b)/476(a): Holy Thursday (Mass of the Lord's Supper)" 2026 4 2 false
let test_holy_saturday_easter_vigil_no_creed () =
(* 2026-04-04: "Sabbato sanctum" -- RG 23(b) again; also explicitly named
by 476(a) ("in Missa Vigiliae paschalis"). *)
check "RG 23(b)/476(a): Holy Saturday (the Easter Vigil Mass)" 2026 4 4 false
(* ---- RG 476(b) negative: a plain II-class saint, not Domini/BVM, not an
Apostle/Evangelist ---- *)
let test_476b_plain_class2_saint () =
(* 2026-08-10: St Lawrence, Class2, subject Saint -- a deacon and martyr,
no Apostle/Evangelist connection, not on any list this module reads. *)
check "476(b): a plain II-class saint (Lawrence) does not say the Creed" 2026 8 10 false
(* ---- RG 28-34 (vigils): checked ahead of 475(c) so a Class2 vigil that
is ALSO on marian_slugs is still excluded ---- *)
let test_vigil_excluded_even_when_class2_and_marian () =
(* 2026-08-14: Vigil of the Assumption, Class2 -- IS on
{!Rite_ef.Precedence_ef.marian_slugs} (a real Marian entry), so without
the vigil check ahead of 475(c) this would wrongly come out [true].
Also carries a real commemoration (+eusebius-confessor), a second live
476(e) instance. *)
check "vigils are excluded even when Class2 and Marian (Vigil of the Assumption)" 2026 8 14 false
(* ---- RG 476(d): a IV-class office (also exercises RG 78/309(a)'s votive
Office of the BVM on Saturday, itself IV class) ---- *)
let test_476d_bvm_saturday_office () =
(* 2026-07-11: the unoccupied Saturday's Office of Our Lady, Class4 --
already a pinned example in test/cli.t (Task 4). *)
check "476(d): the BVM Saturday Office, IV class" 2026 7 11 false
(* One full civil year, walked day by day: RG 475(a)'s own invariant, "every
Sunday says the Creed, no exceptions" -- the same sanity check the task
asks for at the domain-measurement step, pinned here as a real assertion
rather than left to a one-off shell scan. *)
let test_every_sunday_in_2026_says_the_creed () =
let days = Cal.year ctx layer 2026 in
Array.iter
(fun (d : (V.season, V.rank) LD.t) ->
if d.LD.temporal.Temporal.weekday = Date.Sun then
Alcotest.(check bool)
(Printf.sprintf "%s is a Sunday: creed must be true" (Date.to_iso8601 d.LD.date))
true d.LD.creed)
days
(* ---- Review finding 1 (celebrant-rubrics-phase1 fix task): RG 24/25's
feriae II and III classis (the Advent ferias 17-23 December, the
Advent/Lent/September Ember sets, and the numbered Lenten/Passiontide
ferias) are excluded from the Creed by NO check in rubrics_ef.ml -- see
that file's own RG 23 comment (the [n = -46 ...] branch) for the full
account. [creed]'s correct [false] answer for them rests entirely on an
unstated property of {!Rite_ef.Temporal_ef}: no ferial-origin office it
ever builds carries [subject = Lord] or [subject = Bvm] at [Class2]
(RG 475(c)'s own rank guard), and none carries a slug on
[RE.creed_apostle_slugs] (RG 475(e), which has no rank guard at all).
This test asserts that property directly against real Temporal_ef
output, rather than leaving it asserted only in prose, so a future
Temporal_ef change that breaks it fails HERE loudly instead of silently
changing the Creed.
Two real, harmless, already-documented exceptions are excluded from the
[subject] checks rather than papered over: the Sacred Triduum
([subject = Lord], [Class1] -- verified in temporal_ef.ml's own
[triduum_names] branch) and the votive Office of the BVM on Saturday,
RG 91 entry 27 ([subject = Bvm], [Class4] -- {!TE}'s own [is_bvm_saturday]
citation). Neither can ever reach [creed]'s 475(c) branch: the Triduum
is caught earlier by the explicit feria-I-classis check (its own
[Class1] is not [Class2]), and the BVM Saturday Office is [Class4], not
[Class2], so 475(c)'s own rank guard excludes it regardless of subject.
Excluding them here is not a loophole in the test -- it is the precise
boundary of what RG 475(c) actually reads, confirmed rather than
assumed by restricting the [Lord]/[Bvm] checks to exactly [Class2] (RG
24's own II-class population) and [Class3] (RG 25's III-class
population), the two ranks a real feria can carry that are NOT already
handled by an explicit branch or a rank mismatch. The apostle-slug
check has no such carve-out: it is asserted for every ferial-origin day
of every rank, matching 475(e)'s own unguarded text.
A THIRD exception -- not anticipated when this test was first written,
found by actually running it, not by inspection -- had to be excluded
from the POPULATION itself, not from the subject checks: RG 17(a)'s own
"secus die 2 ianuarii" fallback (2 January, only in a civil year with
no 2-5 January Sunday) is a genuine FEAST, [subject = Lord], [Class2],
sitting outside {!TE.named}'s table for a purely architectural reason
(temporal_ef.ml's own citation: that table's shape cannot express a
fallback conditional on a per-year fact) and not always a Sunday
either, so neither of [is_ferial_origin]'s two filters caught it on the
first run -- it failed on 1584-01-02 before {!is_holy_name_fallback}
below was added. Left in as evidence the sweep has real teeth rather
than trimmed from the span: excluding a genuine mistaken positive by
name, once found, is the correct fix; narrowing the span to dodge it
would not have been.
A day is "ferial-origin" here iff {!TE.named} returns [None] for it
(nothing in the fixed/movable table of named feasts, vigils and octave
days claims it), it is not a Sunday (RG 21's own definition: "Nomine
feriae intelleguntur singuli dies hebdomadae, praeter dominicam" --
every day of the week EXCEPT Sunday), and it is not the RG 17(a)
fallback date just above. *)
let contains_substring ~needle haystack =
let nl = String.length needle and hl = String.length haystack in
let rec loop i = (i + nl <= hl) && (String.sub haystack i nl = needle || loop (i + 1)) in
nl = 0 || loop 0
(* RG 17(a)'s own "secus die 2 ianuarii" fallback (temporal_ef.ml's own
citation on [holy_name_fallback_date]): a genuine FEAST, [subject =
Lord], [Class2] -- legitimately outside {!TE.named}'s table only for an
architectural reason (that table's bare [Date.t -> ... option] shape
cannot express a fallback conditional on a per-year fact,
[holy_name_sunday y = None]), never a ferial one, and it is not always
a Sunday, so the weekday filter below does not catch it either. Found
by running this test before this exclusion existed: it failed on
1584-01-02, a real year with no 2-5 January Sunday. *)
let is_holy_name_fallback (d : Date.t) =
let y = Date.year d in
Date.compare d (TE.holy_name_fallback_date y) = 0 && TE.holy_name_sunday y = None
let is_ferial_origin (d : Date.t) =
TE.named d = None && Date.weekday d <> Date.Sun && not (is_holy_name_fallback d)
(* Span: civil years 1583-1682, the domain's own opening century -- every
RG 24/25 population recurs every civil year (Advent 17-23, all three
non-Whitsun Ember sets, and Lenten/Passiontide ferias are none of them
rare or conditional), so one year already gives full COVERAGE; a
century instead of one is for confidence the invariant is not an
accident of a single Easter date, at a cost (day-by-day calls to the
pure {!TE.temporal}, no Calendar/Precedence resolution) cheap enough to
stay in the default, unsampled suite. 1583 is also the domain's own
lower bound, and this span contains 1598, the earliest possible Easter
(22 March) in [1583, 2500] per {!test_easter_extremes} above -- a real,
not merely nominal, edge case. Coverage is VERIFIED below via counters,
not assumed: a test that never actually walks an Ember day would prove
nothing about Ember days. *)
let test_ferial_origin_never_carries_lord_bvm_or_apostle_slug () =
let total = ref 0
and advent_ember = ref 0
and lent_ember = ref 0
and september_ember = ref 0
and advent_17_23 = ref 0
and lenten_passiontide_class3 = ref 0 in
for y = 1583 to 1682 do
let dec31 = mk y 12 31 in
let d = ref (mk y 1 1) in
while Date.compare !d dec31 <= 0 do
(if is_ferial_origin !d then begin
let t = TE.temporal !d in
incr total;
let office = t.Temporal.office in
let slug = Slug.to_string office.Cel.slug in
let label = Printf.sprintf "%s (%s, rank=%s)" (Date.to_iso8601 !d) slug
(match office.Cel.rank with
| V.Class1 -> "1"
| V.Class2 -> "2"
| V.Class3 -> "3"
| V.Class4 -> "4")
in
(* Coverage tallies -- checked against zero below. *)
if contains_substring ~needle:"advent-ember" slug then incr advent_ember;
if contains_substring ~needle:"lent-ember" slug then incr lent_ember;
if contains_substring ~needle:"september-ember" slug then incr september_ember;
if Date.month !d = 12 && Date.day !d >= 17 && Date.day !d <= 23 then incr advent_17_23;
if
office.Cel.rank = V.Class3
&& (t.Temporal.season = V.Lent || t.Temporal.season = V.Passiontide)
then incr lenten_passiontide_class3;
(* The invariant itself. Apostle slugs: every rank, no carve-out. *)
Alcotest.(check bool) (label ^ ": not on the apostle-natalicium slug list") false
(List.mem slug RE.creed_apostle_slugs);
(* Lord/Bvm subject: only at the two ranks a real RG 24/25 feria
can carry -- see this test's own header for why Class1
(Triduum) and Class4 (BVM Saturday) are deliberately excluded. *)
if office.Cel.rank = V.Class2 || office.Cel.rank = V.Class3 then begin
Alcotest.(check bool) (label ^ ": not subject Lord") false (office.Cel.subject = Subject.Lord);
Alcotest.(check bool) (label ^ ": not subject Bvm") false (office.Cel.subject = Subject.Bvm)
end
end);
d := Date.add_days !d 1
done
done;
Alcotest.(check bool) "span examined a real number of ferial-origin days" true (!total > 10_000);
Alcotest.(check bool) "span reached Advent Ember days" true (!advent_ember > 0);
Alcotest.(check bool) "span reached Lent Ember days" true (!lent_ember > 0);
Alcotest.(check bool) "span reached September Ember days" true (!september_ember > 0);
Alcotest.(check bool) "span reached Advent 17-23 ferias" true (!advent_17_23 > 0);
Alcotest.(check bool) "span reached Lenten/Passiontide III-class ferias" true
(!lenten_passiontide_class3 > 0)
let suite =
( "Rubrics_ef",
[ Alcotest.test_case "475(a): ordinary Sunday" `Quick test_475a_ordinary_sunday;
Alcotest.test_case "475(a): reads [temporal], not [observed] (Trap One)" `Quick
test_475a_reads_temporal_not_observed;
Alcotest.test_case "475(b): I-class feast" `Quick test_475b_class1_feast;
Alcotest.test_case "475(c): II-class feast of the Lord" `Quick test_475c_lord;
Alcotest.test_case "475(c): II-class BVM feast via marian_slugs" `Quick
test_475c_bvm_via_marian_slugs;
Alcotest.test_case "475(d): octave overrides an occurring feast" `Quick
test_475d_octave_even_occurring_feast;
Alcotest.test_case "475(d): 1 January octave-day boundary" `Quick test_475d_octave_day_boundary;
Alcotest.test_case "475(e): an Apostle's own natalicium" `Quick test_475e_apostle_natalicium;
Alcotest.test_case "475(e): Barnabas, named explicitly" `Quick
test_475e_barnabas_named_explicitly;
Alcotest.test_case "475(e): Chair of Peter, named explicitly" `Quick
test_475e_chair_of_peter_named_explicitly;
Alcotest.test_case "475(e) excludes the Conversion of St Paul (Trap Two)" `Quick
test_475e_excludes_conversion_of_paul;
Alcotest.test_case "RG 23/476: Ash Wednesday" `Quick test_ash_wednesday_no_creed;
Alcotest.test_case "RG 23/476(a): Holy Thursday" `Quick test_holy_thursday_no_creed;
Alcotest.test_case "RG 23/476(a): Holy Saturday / Easter Vigil" `Quick
test_holy_saturday_easter_vigil_no_creed;
Alcotest.test_case "476(b): plain II-class saint (negative)" `Quick
test_476b_plain_class2_saint;
Alcotest.test_case "vigils excluded even when Class2 and Marian" `Quick
test_vigil_excluded_even_when_class2_and_marian;
Alcotest.test_case "476(d): BVM Saturday Office, IV class" `Quick test_476d_bvm_saturday_office;
Alcotest.test_case "every Sunday in 2026 says the Creed" `Quick
test_every_sunday_in_2026_says_the_creed;
Alcotest.test_case "RG 24/25: no ferial-origin office carries Lord/Bvm or an apostle slug" `Quick
test_ferial_origin_never_carries_lord_bvm_or_apostle_slug ] )
|