1use std::collections::BTreeMap;
11
12use omena_evidence_graph::ObligationFamilyIdV0;
13use omena_transform_cst::{
14 TRANSFORM_PASS_CATALOG_LEN, TransformDagEdgeV0, TransformPassKind, all_transform_pass_kinds,
15 cascade_safe_obligation, default_transform_dag_edges,
16};
17use serde::Serialize;
18
19pub const LAWVERE_THEORY_VERSION_V0: &str = "lawvere-css-transform-catalog-v0";
20pub const LAWVERE_MECHANISM_SCOPE_V0: &str = "featureGatedDifferentialWitnessSubstrate";
21pub const LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0: bool = false;
22pub const LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0: bool = false;
23
24#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)]
25#[serde(rename_all = "camelCase")]
26pub enum AbstractDomainTagV0 {
27 SyntaxTrivia,
28 TokenValue,
29 SelectorShape,
30 CascadeStructural,
31 SemanticGraph,
32 TerminalEmission,
33}
34
35#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)]
36#[serde(rename_all = "camelCase")]
37pub enum LawvereCatalogRoleV0 {
38 Generator,
39 TerminalForgetfulFunctor,
40}
41
42#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)]
43#[serde(rename_all = "camelCase")]
44pub enum SaturationBudgetTierV0 {
45 Full,
46 Half,
47 Minimal,
48}
49
50impl SaturationBudgetTierV0 {
51 pub const fn fixture_count(self) -> usize {
52 match self {
53 Self::Minimal => 10,
54 Self::Half => 50,
55 Self::Full => 200,
56 }
57 }
58
59 pub const fn label(self) -> &'static str {
60 match self {
61 Self::Minimal => "Dev",
62 Self::Half => "CI",
63 Self::Full => "Nightly",
64 }
65 }
66}
67
68#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
69#[serde(rename_all = "camelCase")]
70pub struct LawvereGeneratorMetadataV0 {
71 pub schema_version: &'static str,
72 pub product: &'static str,
73 pub layer_marker: &'static str,
74 pub feature_gate: &'static str,
75 pub theory_version: &'static str,
76 pub pass_id: &'static str,
77 pub ordinal: u8,
78 pub title: &'static str,
79 pub catalog_role: LawvereCatalogRoleV0,
80 pub abstract_domain_tag: AbstractDomainTagV0,
81 pub execution_rank_hint: u32,
82 pub terminal_forgetful_functor: bool,
83 pub reads_fixed_point: bool,
84}
85
86#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
87#[serde(rename_all = "camelCase")]
88pub struct LawvereEquationClusterV0 {
89 pub schema_version: &'static str,
90 pub product: &'static str,
91 pub layer_marker: &'static str,
92 pub feature_gate: &'static str,
93 pub execution_rank_hint: u32,
94 pub pass_ids: Vec<&'static str>,
95 pub generator_count: usize,
96 pub saturation_budget_tier: SaturationBudgetTierV0,
97 pub theory_version: &'static str,
98}
99
100#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
101#[serde(rename_all = "camelCase")]
102pub struct LawvereDifferentialCorpusTierV0 {
103 pub schema_version: &'static str,
104 pub product: &'static str,
105 pub layer_marker: &'static str,
106 pub feature_gate: &'static str,
107 pub theory_version: &'static str,
108 pub tier: SaturationBudgetTierV0,
109 pub tier_label: &'static str,
110 pub fixture_count: usize,
111 pub required_pass_rate_percent: u8,
112}
113
114#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
115#[serde(rename_all = "camelCase")]
116pub struct ReorderabilityCertificateV0 {
117 pub schema_version: &'static str,
118 pub product: &'static str,
119 pub layer_marker: &'static str,
120 pub feature_gate: &'static str,
121 pub mechanism_scope: &'static str,
122 pub product_path_evidence_ready: bool,
123 pub global_transform_theorem_claimed: bool,
124 pub left_pass_id: &'static str,
125 pub right_pass_id: &'static str,
126 pub theory_version: &'static str,
127 pub differential_tier: SaturationBudgetTierV0,
128 pub commute_witness: &'static str,
129 pub differential_fixture_count: usize,
130 pub differential_equal_fixture_count: usize,
131 pub differential_mismatch_count: usize,
132 pub specificity_preserved: bool,
133 #[serde(skip_serializing)]
134 obligation_family: ObligationFamilyIdV0,
135 pub computed_value_preserved: bool,
136 pub provenance_preserved: bool,
137 pub cascade_safe_witness: String,
138 pub accepted: bool,
139}
140
141#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
142#[serde(rename_all = "camelCase")]
143pub struct LawvereDifferentialCommutativityCaseV0 {
144 pub label: String,
145 pub input_css: String,
146 pub left_then_right_css: String,
147 pub right_then_left_css: String,
148 pub left_then_right_mutation_count: usize,
149 pub right_then_left_mutation_count: usize,
150 pub equal_output: bool,
151}
152
153#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
154#[serde(rename_all = "camelCase")]
155pub struct LawvereDifferentialCommutativityWitnessV0 {
156 pub schema_version: &'static str,
157 pub product: &'static str,
158 pub layer_marker: &'static str,
159 pub feature_gate: &'static str,
160 pub mechanism_scope: &'static str,
161 pub product_path_evidence_ready: bool,
162 pub global_transform_theorem_claimed: bool,
163 pub theory_version: &'static str,
164 pub left_pass_id: &'static str,
165 pub right_pass_id: &'static str,
166 pub fixture_count: usize,
167 pub equal_fixture_count: usize,
168 pub mismatch_count: usize,
169 pub cases: Vec<LawvereDifferentialCommutativityCaseV0>,
170 pub accepted: bool,
171}
172
173#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
174#[serde(rename_all = "camelCase")]
175pub struct TransformPassParallelPlanV0 {
176 pub schema_version: &'static str,
177 pub product: &'static str,
178 pub layer_marker: &'static str,
179 pub feature_gate: &'static str,
180 pub mechanism_scope: &'static str,
181 pub product_path_evidence_ready: bool,
182 pub global_transform_theorem_claimed: bool,
183 pub scheduler_status: &'static str,
184 pub requested_pass_ids: Vec<&'static str>,
185 pub terminal_pass_ids: Vec<&'static str>,
186 pub rank_clusters: Vec<LawvereEquationClusterV0>,
187 pub executor_consumes_plan: bool,
188}
189
190#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
191#[serde(rename_all = "camelCase")]
192pub struct LawvereModelTraceV0 {
193 pub schema_version: &'static str,
194 pub product: &'static str,
195 pub layer_marker: &'static str,
196 pub feature_gate: &'static str,
197 pub mechanism_scope: &'static str,
198 pub product_path_evidence_ready: bool,
199 pub global_transform_theorem_claimed: bool,
200 pub theory_version: &'static str,
201 pub input_pass_ids: Vec<&'static str>,
202 pub ordered_pass_ids: Vec<&'static str>,
203 pub terminal_pass_ids: Vec<&'static str>,
204 pub rank_clusters: Vec<LawvereEquationClusterV0>,
205 pub preserves_existing_executor_signature: bool,
206}
207
208#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
209#[serde(rename_all = "camelCase")]
210pub struct LawvereSaturationExecutionV0 {
211 pub schema_version: &'static str,
212 pub product: &'static str,
213 pub layer_marker: &'static str,
214 pub feature_gate: &'static str,
215 pub mechanism_scope: &'static str,
216 pub product_path_evidence_ready: bool,
217 pub global_transform_theorem_claimed: bool,
218 pub theory_version: &'static str,
219 pub pass_id: &'static str,
220 pub analysis_slot: &'static str,
221 pub original_unit_analysis_path_preserved: bool,
222 pub differential_tier: SaturationBudgetTierV0,
223 pub differential_fixture_count: usize,
224 pub iteration_limit: usize,
225 pub iteration_count: usize,
226 pub eclass_count: usize,
227 pub enode_count: usize,
228 pub accepted: bool,
229 pub extracted_matches_candidate: bool,
230}
231
232#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
233#[serde(rename_all = "camelCase")]
234pub struct LawvereTheorySummaryV0 {
235 pub schema_version: &'static str,
236 pub product: &'static str,
237 pub layer_marker: &'static str,
238 pub feature_gate: &'static str,
239 pub theory_version: &'static str,
240 pub catalog_pass_count: usize,
241 pub catalog_entry_count: usize,
242 pub lawvere_generator_count: usize,
243 pub terminal_forgetful_functor_count: usize,
244 pub execution_rank_cluster_count: usize,
245 pub equation_clusters: Vec<LawvereEquationClusterV0>,
246 pub generators: Vec<LawvereGeneratorMetadataV0>,
247 pub dag_edges: Vec<TransformDagEdgeV0>,
248 pub saturation_budget_tiers: Vec<SaturationBudgetTierV0>,
249 pub differential_corpus_tiers: Vec<LawvereDifferentialCorpusTierV0>,
250 pub lawvere_saturation_feature_enabled_by_default: bool,
251 pub product_path_evidence_ready: bool,
252 pub mechanism_scope: &'static str,
253 pub omena_categorical_dependency_forbidden: bool,
254}
255
256pub fn summarize_lawvere_theory_v0() -> LawvereTheorySummaryV0 {
257 let generators = lawvere_generator_metadata_catalog_v0();
258 let terminal_forgetful_functor_count = generators
259 .iter()
260 .filter(|generator| generator.terminal_forgetful_functor)
261 .count();
262 let equation_clusters = lawvere_equation_clusters_v0(
263 generators
264 .iter()
265 .map(|generator| generator.pass_id)
266 .collect::<Vec<_>>()
267 .as_slice(),
268 );
269
270 LawvereTheorySummaryV0 {
271 schema_version: "0",
272 product: "omena-lawvere.theory-summary",
273 layer_marker: "enriched-algebraic",
274 feature_gate: "lawvere-saturation",
275 theory_version: LAWVERE_THEORY_VERSION_V0,
276 catalog_pass_count: TRANSFORM_PASS_CATALOG_LEN,
277 catalog_entry_count: generators.len(),
278 lawvere_generator_count: lawvere_theory_generator_count_v0(&generators),
279 terminal_forgetful_functor_count,
280 execution_rank_cluster_count: equation_clusters.len(),
281 equation_clusters,
282 generators,
283 dag_edges: default_transform_dag_edges(),
284 saturation_budget_tiers: vec![
285 SaturationBudgetTierV0::Minimal,
286 SaturationBudgetTierV0::Half,
287 SaturationBudgetTierV0::Full,
288 ],
289 differential_corpus_tiers: lawvere_differential_corpus_tiers_v0(),
290 lawvere_saturation_feature_enabled_by_default: false,
291 product_path_evidence_ready: LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0,
292 mechanism_scope: LAWVERE_MECHANISM_SCOPE_V0,
293 omena_categorical_dependency_forbidden: true,
294 }
295}
296
297pub fn lawvere_generator_metadata_catalog_v0() -> Vec<LawvereGeneratorMetadataV0> {
298 all_transform_pass_kinds()
299 .into_iter()
300 .map(lawvere_generator_metadata_v0)
301 .collect()
302}
303
304pub fn lawvere_generator_metadata_v0(kind: TransformPassKind) -> LawvereGeneratorMetadataV0 {
305 let terminal_forgetful_functor = kind == TransformPassKind::PrintCss;
306 LawvereGeneratorMetadataV0 {
307 schema_version: "0",
308 product: "omena-lawvere.generator-metadata",
309 layer_marker: "enriched-algebraic",
310 feature_gate: "lawvere-saturation",
311 theory_version: LAWVERE_THEORY_VERSION_V0,
312 pass_id: kind.id(),
313 ordinal: kind.ordinal(),
314 title: kind.title(),
315 catalog_role: if terminal_forgetful_functor {
316 LawvereCatalogRoleV0::TerminalForgetfulFunctor
317 } else {
318 LawvereCatalogRoleV0::Generator
319 },
320 abstract_domain_tag: abstract_domain_tag_for_pass(kind),
321 execution_rank_hint: u32::from(lawvere_execution_rank_hint(kind)),
322 terminal_forgetful_functor,
323 reads_fixed_point: matches!(
324 kind,
325 TransformPassKind::StaticVarSubstitution
326 | TransformPassKind::TreeShakeCustomProperty
327 | TransformPassKind::DesignTokenRouting
328 ),
329 }
330}
331
332pub fn lawvere_equation_clusters_v0(pass_ids: &[&'static str]) -> Vec<LawvereEquationClusterV0> {
333 let mut clusters = BTreeMap::<u32, Vec<&'static str>>::new();
334 for kind in all_transform_pass_kinds() {
335 if pass_ids.contains(&kind.id())
336 && lawvere_catalog_role_v0(kind) == LawvereCatalogRoleV0::Generator
337 {
338 clusters
339 .entry(u32::from(lawvere_execution_rank_hint(kind)))
340 .or_default()
341 .push(kind.id());
342 }
343 }
344 clusters
345 .into_iter()
346 .map(|(execution_rank_hint, mut pass_ids)| {
347 pass_ids.sort();
348 let generator_count = pass_ids.len();
349 LawvereEquationClusterV0 {
350 schema_version: "0",
351 product: "omena-lawvere.equation-cluster",
352 layer_marker: "enriched-algebraic",
353 feature_gate: "lawvere-saturation",
354 execution_rank_hint,
355 pass_ids,
356 generator_count,
357 saturation_budget_tier: budget_tier_for_cluster_size(generator_count),
358 theory_version: LAWVERE_THEORY_VERSION_V0,
359 }
360 })
361 .collect()
362}
363
364pub fn plan_transform_pass_parallel_layers_v0(
365 requested: &[TransformPassKind],
366) -> TransformPassParallelPlanV0 {
367 let requested_pass_ids = requested.iter().map(|kind| kind.id()).collect::<Vec<_>>();
368 TransformPassParallelPlanV0 {
369 schema_version: "0",
370 product: "omena-lawvere.transform-pass-parallel-plan",
371 layer_marker: "enriched-algebraic",
372 feature_gate: "lawvere-saturation",
373 mechanism_scope: LAWVERE_MECHANISM_SCOPE_V0,
374 product_path_evidence_ready: LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0,
375 global_transform_theorem_claimed: LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0,
376 scheduler_status: "scaffoldOnly",
377 requested_pass_ids: requested_pass_ids.clone(),
378 terminal_pass_ids: terminal_pass_ids_from_pass_kinds(requested),
379 rank_clusters: lawvere_equation_clusters_v0(requested_pass_ids.as_slice()),
380 executor_consumes_plan: false,
381 }
382}
383
384pub fn trace_lawvere_model_v0(
385 requested: &[TransformPassKind],
386 ordered_pass_ids: Vec<&'static str>,
387) -> LawvereModelTraceV0 {
388 let input_pass_ids = requested.iter().map(|kind| kind.id()).collect::<Vec<_>>();
389 LawvereModelTraceV0 {
390 schema_version: "0",
391 product: "omena-lawvere.model-trace",
392 layer_marker: "enriched-algebraic",
393 feature_gate: "lawvere-saturation",
394 mechanism_scope: LAWVERE_MECHANISM_SCOPE_V0,
395 product_path_evidence_ready: LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0,
396 global_transform_theorem_claimed: LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0,
397 theory_version: LAWVERE_THEORY_VERSION_V0,
398 rank_clusters: lawvere_equation_clusters_v0(ordered_pass_ids.as_slice()),
399 input_pass_ids,
400 terminal_pass_ids: terminal_pass_ids_from_pass_ids(ordered_pass_ids.as_slice()),
401 ordered_pass_ids,
402 preserves_existing_executor_signature: true,
403 }
404}
405
406pub fn reorderability_certificate_v0(
407 left: TransformPassKind,
408 right: TransformPassKind,
409) -> ReorderabilityCertificateV0 {
410 ReorderabilityCertificateV0 {
411 schema_version: "0",
412 product: "omena-lawvere.reorderability-certificate",
413 layer_marker: "enriched-algebraic",
414 feature_gate: "lawvere-saturation",
415 mechanism_scope: LAWVERE_MECHANISM_SCOPE_V0,
416 product_path_evidence_ready: LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0,
417 global_transform_theorem_claimed: LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0,
418 left_pass_id: left.id(),
419 right_pass_id: right.id(),
420 theory_version: LAWVERE_THEORY_VERSION_V0,
421 differential_tier: budget_tier_for_cluster_size(2),
422 commute_witness: "requiresDifferentialCommutativityWitness",
423 differential_fixture_count: 0,
424 differential_equal_fixture_count: 0,
425 differential_mismatch_count: 0,
426 specificity_preserved: false,
427 obligation_family: ObligationFamilyIdV0::CascadeSafetyFloor,
428 computed_value_preserved: ObligationFamilyIdV0::CascadeSafetyFloor
429 .preserves_computed_value(),
430 provenance_preserved: false,
431 cascade_safe_witness: format!(
432 "{}:{}",
433 cascade_safe_obligation(left),
434 cascade_safe_obligation(right)
435 ),
436 accepted: false,
437 }
438}
439
440pub fn lawvere_differential_commutativity_witness_v0(
441 left: TransformPassKind,
442 right: TransformPassKind,
443 cases: Vec<LawvereDifferentialCommutativityCaseV0>,
444) -> LawvereDifferentialCommutativityWitnessV0 {
445 let fixture_count = cases.len();
446 let equal_fixture_count = cases.iter().filter(|case| case.equal_output).count();
447 let mismatch_count = fixture_count.saturating_sub(equal_fixture_count);
448
449 LawvereDifferentialCommutativityWitnessV0 {
450 schema_version: "0",
451 product: "omena-lawvere.differential-commutativity-witness",
452 layer_marker: "enriched-algebraic",
453 feature_gate: "lawvere-saturation",
454 mechanism_scope: LAWVERE_MECHANISM_SCOPE_V0,
455 product_path_evidence_ready: LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0,
456 global_transform_theorem_claimed: LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0,
457 theory_version: LAWVERE_THEORY_VERSION_V0,
458 left_pass_id: left.id(),
459 right_pass_id: right.id(),
460 fixture_count,
461 equal_fixture_count,
462 mismatch_count,
463 cases,
464 accepted: fixture_count > 0 && mismatch_count == 0,
465 }
466}
467
468pub fn reorderability_certificate_from_differential_v0(
469 left: TransformPassKind,
470 right: TransformPassKind,
471 witness: &LawvereDifferentialCommutativityWitnessV0,
472) -> ReorderabilityCertificateV0 {
473 let mut certificate = reorderability_certificate_v0(left, right);
474 certificate.commute_witness = "differentialCommutativityCorpus";
475 certificate.differential_fixture_count = witness.fixture_count;
476 certificate.differential_equal_fixture_count = witness.equal_fixture_count;
477 certificate.differential_mismatch_count = witness.mismatch_count;
478 certificate.specificity_preserved = witness.accepted;
479 certificate.obligation_family =
480 ObligationFamilyIdV0::from_computed_value_preservation(witness.accepted);
481 certificate.computed_value_preserved = certificate.obligation_family.preserves_computed_value();
482 certificate.provenance_preserved = witness.accepted;
483 certificate.accepted = witness.accepted;
484 certificate
485}
486
487pub fn lawvere_differential_corpus_tiers_v0() -> Vec<LawvereDifferentialCorpusTierV0> {
488 [
489 SaturationBudgetTierV0::Minimal,
490 SaturationBudgetTierV0::Half,
491 SaturationBudgetTierV0::Full,
492 ]
493 .into_iter()
494 .map(|tier| LawvereDifferentialCorpusTierV0 {
495 schema_version: "0",
496 product: "omena-lawvere.differential-corpus-tier",
497 layer_marker: "enriched-algebraic",
498 feature_gate: "lawvere-saturation",
499 theory_version: LAWVERE_THEORY_VERSION_V0,
500 tier,
501 tier_label: tier.label(),
502 fixture_count: tier.fixture_count(),
503 required_pass_rate_percent: 100,
504 })
505 .collect()
506}
507
508pub fn summarize_lawvere_saturation_execution_v0(
509 pass_id: &'static str,
510 iteration_limit: usize,
511 iteration_count: usize,
512 eclass_count: usize,
513 enode_count: usize,
514 extracted_matches_candidate: bool,
515) -> LawvereSaturationExecutionV0 {
516 LawvereSaturationExecutionV0 {
517 schema_version: "0",
518 product: "omena-lawvere.saturation-execution",
519 layer_marker: "enriched-algebraic",
520 feature_gate: "lawvere-saturation",
521 mechanism_scope: LAWVERE_MECHANISM_SCOPE_V0,
522 product_path_evidence_ready: LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0,
523 global_transform_theorem_claimed: LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0,
524 theory_version: LAWVERE_THEORY_VERSION_V0,
525 pass_id,
526 analysis_slot: "LawvereAnalysis",
527 original_unit_analysis_path_preserved: true,
528 differential_tier: SaturationBudgetTierV0::Minimal,
529 differential_fixture_count: SaturationBudgetTierV0::Minimal.fixture_count(),
530 iteration_limit,
531 iteration_count,
532 eclass_count,
533 enode_count,
534 accepted: extracted_matches_candidate,
535 extracted_matches_candidate,
536 }
537}
538
539pub const fn lawvere_execution_rank_hint(kind: TransformPassKind) -> u8 {
540 match kind.ordinal() {
545 27..=29 => 10,
546 30..=40 => 20,
547 14..=25 | 42 | 43 => 30,
548 8..=13 | 26 => 40,
549 1..=7 => 50,
550 41 => 60,
551 _ => 70,
552 }
553}
554
555pub const fn lawvere_catalog_role_v0(kind: TransformPassKind) -> LawvereCatalogRoleV0 {
556 match kind {
557 TransformPassKind::PrintCss => LawvereCatalogRoleV0::TerminalForgetfulFunctor,
558 _ => LawvereCatalogRoleV0::Generator,
559 }
560}
561
562fn lawvere_theory_generator_count_v0(generators: &[LawvereGeneratorMetadataV0]) -> usize {
563 generators
564 .iter()
565 .filter(|generator| generator.catalog_role == LawvereCatalogRoleV0::Generator)
566 .count()
567}
568
569fn terminal_pass_ids_from_pass_kinds(requested: &[TransformPassKind]) -> Vec<&'static str> {
570 requested
571 .iter()
572 .filter(|kind| {
573 lawvere_catalog_role_v0(**kind) == LawvereCatalogRoleV0::TerminalForgetfulFunctor
574 })
575 .map(|kind| kind.id())
576 .collect()
577}
578
579fn terminal_pass_ids_from_pass_ids(pass_ids: &[&'static str]) -> Vec<&'static str> {
580 all_transform_pass_kinds()
581 .into_iter()
582 .filter(|kind| {
583 lawvere_catalog_role_v0(*kind) == LawvereCatalogRoleV0::TerminalForgetfulFunctor
584 })
585 .map(|kind| kind.id())
586 .filter(|pass_id| pass_ids.contains(pass_id))
587 .collect()
588}
589
590const fn abstract_domain_tag_for_pass(kind: TransformPassKind) -> AbstractDomainTagV0 {
591 match kind.ordinal() {
592 1..=7 => AbstractDomainTagV0::TokenValue,
593 8..=13 | 25 => AbstractDomainTagV0::SelectorShape,
594 14..=24 => AbstractDomainTagV0::CascadeStructural,
595 26..=39 => AbstractDomainTagV0::SemanticGraph,
596 40 => AbstractDomainTagV0::TerminalEmission,
597 _ => AbstractDomainTagV0::SyntaxTrivia,
598 }
599}
600
601const fn budget_tier_for_cluster_size(size: usize) -> SaturationBudgetTierV0 {
602 if size >= 10 {
603 SaturationBudgetTierV0::Full
604 } else if size >= 4 {
605 SaturationBudgetTierV0::Half
606 } else {
607 SaturationBudgetTierV0::Minimal
608 }
609}
610
611#[cfg(test)]
612mod tests {
613 use super::*;
614
615 #[test]
616 fn summarizes_forty_pass_lawvere_catalog_with_schema_zero() {
617 let summary = summarize_lawvere_theory_v0();
618
619 assert_eq!(summary.schema_version, "0");
620 assert_eq!(summary.layer_marker, "enriched-algebraic");
621 assert_eq!(summary.feature_gate, "lawvere-saturation");
622 assert_eq!(summary.catalog_pass_count, TRANSFORM_PASS_CATALOG_LEN);
623 assert_eq!(summary.catalog_entry_count, TRANSFORM_PASS_CATALOG_LEN);
624 assert_eq!(
625 summary.lawvere_generator_count,
626 TRANSFORM_PASS_CATALOG_LEN - 1
627 );
628 assert_eq!(summary.terminal_forgetful_functor_count, 1);
629 assert_eq!(summary.differential_corpus_tiers.len(), 3);
630 assert!(summary.differential_corpus_tiers.iter().any(|tier| {
631 tier.tier == SaturationBudgetTierV0::Minimal && tier.fixture_count == 10
632 }));
633 assert!(
634 summary.differential_corpus_tiers.iter().any(|tier| {
635 tier.tier == SaturationBudgetTierV0::Half && tier.fixture_count == 50
636 })
637 );
638 assert!(summary.differential_corpus_tiers.iter().any(|tier| {
639 tier.tier == SaturationBudgetTierV0::Full && tier.fixture_count == 200
640 }));
641 assert!(!summary.lawvere_saturation_feature_enabled_by_default);
642 assert_eq!(
643 summary.product_path_evidence_ready,
644 LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0
645 );
646 assert_eq!(summary.mechanism_scope, LAWVERE_MECHANISM_SCOPE_V0);
647 assert!(summary.omena_categorical_dependency_forbidden);
648 }
649
650 #[test]
651 fn execution_rank_hint_clusters_match_planner_promote_pattern() {
652 let metadata = lawvere_generator_metadata_catalog_v0();
653
654 assert_eq!(metadata.len(), TRANSFORM_PASS_CATALOG_LEN);
655 assert!(metadata.iter().any(|generator| {
656 generator.pass_id == "css-modules-class-hashing" && generator.execution_rank_hint == 20
657 }));
658 assert!(metadata.iter().any(|generator| {
659 generator.pass_id == "print-css"
660 && generator.catalog_role == LawvereCatalogRoleV0::TerminalForgetfulFunctor
661 && generator.terminal_forgetful_functor
662 && generator.execution_rank_hint == 60
663 }));
664 }
665
666 #[test]
667 fn parallel_plan_is_scaffold_only_and_does_not_consume_executor() {
668 let plan = plan_transform_pass_parallel_layers_v0(&[
669 TransformPassKind::ColorCompression,
670 TransformPassKind::NumberCompression,
671 TransformPassKind::PrintCss,
672 ]);
673
674 assert_eq!(plan.schema_version, "0");
675 assert_eq!(plan.scheduler_status, "scaffoldOnly");
676 assert!(!plan.executor_consumes_plan);
677 assert_eq!(plan.mechanism_scope, LAWVERE_MECHANISM_SCOPE_V0);
678 assert_eq!(
679 plan.product_path_evidence_ready,
680 LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0
681 );
682 assert_eq!(
683 plan.global_transform_theorem_claimed,
684 LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0
685 );
686 assert_eq!(plan.terminal_pass_ids, vec!["print-css"]);
687 assert_eq!(plan.rank_clusters.len(), 1);
688 }
689
690 #[test]
691 fn saturation_execution_contract_records_lawvere_analysis_slot() {
692 let execution = summarize_lawvere_saturation_execution_v0(
693 TransformPassKind::CalcReduction.id(),
694 8,
695 2,
696 5,
697 9,
698 true,
699 );
700
701 assert_eq!(execution.schema_version, "0");
702 assert_eq!(execution.layer_marker, "enriched-algebraic");
703 assert_eq!(execution.feature_gate, "lawvere-saturation");
704 assert_eq!(execution.analysis_slot, "LawvereAnalysis");
705 assert_eq!(execution.differential_fixture_count, 10);
706 assert!(execution.original_unit_analysis_path_preserved);
707 assert_eq!(execution.mechanism_scope, LAWVERE_MECHANISM_SCOPE_V0);
708 assert_eq!(
709 execution.product_path_evidence_ready,
710 LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0
711 );
712 assert_eq!(
713 execution.global_transform_theorem_claimed,
714 LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0
715 );
716 assert!(execution.accepted);
717 }
718
719 #[test]
720 fn rank_only_reorderability_certificate_requires_differential_witness() {
721 let certificate = reorderability_certificate_v0(
722 TransformPassKind::CommentStrip,
723 TransformPassKind::WhitespaceStrip,
724 );
725
726 assert_eq!(
727 certificate.commute_witness,
728 "requiresDifferentialCommutativityWitness"
729 );
730 assert_eq!(certificate.mechanism_scope, LAWVERE_MECHANISM_SCOPE_V0);
731 assert_eq!(
732 certificate.product_path_evidence_ready,
733 LAWVERE_PRODUCT_PATH_EVIDENCE_READY_V0
734 );
735 assert_eq!(
736 certificate.global_transform_theorem_claimed,
737 LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0
738 );
739 assert_eq!(certificate.differential_fixture_count, 0);
740 assert!(!certificate.accepted);
741 }
742
743 #[test]
744 fn reorderability_certificate_family_derivation_preserves_legacy_json_contract()
745 -> Result<(), serde_json::Error> {
746 let rank_only = reorderability_certificate_v0(
747 TransformPassKind::CommentStrip,
748 TransformPassKind::WhitespaceStrip,
749 );
750 let rank_only_json = serde_json::to_value(&rank_only)?;
751 assert_eq!(rank_only_json["computedValuePreserved"], false);
752 assert!(rank_only_json.get("obligationFamily").is_none());
753
754 let witness = lawvere_differential_commutativity_witness_v0(
755 TransformPassKind::CommentStrip,
756 TransformPassKind::WhitespaceStrip,
757 vec![LawvereDifferentialCommutativityCaseV0 {
758 label: "comment-whitespace".to_string(),
759 input_css: ".a { color : red ; /* x */ }".to_string(),
760 left_then_right_css: ".a{color:red}".to_string(),
761 right_then_left_css: ".a{color:red}".to_string(),
762 left_then_right_mutation_count: 2,
763 right_then_left_mutation_count: 2,
764 equal_output: true,
765 }],
766 );
767 let accepted = reorderability_certificate_from_differential_v0(
768 TransformPassKind::CommentStrip,
769 TransformPassKind::WhitespaceStrip,
770 &witness,
771 );
772 let accepted_json = serde_json::to_value(&accepted)?;
773
774 assert_eq!(accepted_json["computedValuePreserved"], true);
775 assert!(accepted_json.get("obligationFamily").is_none());
776 assert_eq!(
777 accepted_json["commuteWitness"],
778 "differentialCommutativityCorpus"
779 );
780
781 Ok(())
782 }
783
784 #[test]
785 fn differential_reorderability_certificate_accepts_only_equal_output_corpus() {
786 let witness = lawvere_differential_commutativity_witness_v0(
787 TransformPassKind::CommentStrip,
788 TransformPassKind::WhitespaceStrip,
789 vec![LawvereDifferentialCommutativityCaseV0 {
790 label: "comment-whitespace".to_string(),
791 input_css: ".a { color : red ; /* x */ }".to_string(),
792 left_then_right_css: ".a{color:red}".to_string(),
793 right_then_left_css: ".a{color:red}".to_string(),
794 left_then_right_mutation_count: 2,
795 right_then_left_mutation_count: 2,
796 equal_output: true,
797 }],
798 );
799 let certificate = reorderability_certificate_from_differential_v0(
800 TransformPassKind::CommentStrip,
801 TransformPassKind::WhitespaceStrip,
802 &witness,
803 );
804
805 assert!(witness.accepted);
806 assert_eq!(
807 certificate.commute_witness,
808 "differentialCommutativityCorpus"
809 );
810 assert_eq!(witness.mechanism_scope, LAWVERE_MECHANISM_SCOPE_V0);
811 assert_eq!(certificate.mechanism_scope, LAWVERE_MECHANISM_SCOPE_V0);
812 assert_eq!(
813 witness.global_transform_theorem_claimed,
814 LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0
815 );
816 assert_eq!(
817 certificate.global_transform_theorem_claimed,
818 LAWVERE_GLOBAL_TRANSFORM_THEOREM_CLAIMED_V0
819 );
820 assert_eq!(certificate.differential_fixture_count, 1);
821 assert_eq!(certificate.differential_mismatch_count, 0);
822 assert!(certificate.accepted);
823 }
824}