Skip to main content

omena_transform_egg/
lib.rs

1//! Optional e-graph rewrite boundary for Omena CSS transforms.
2//!
3//! Selector, shorthand, and computed-value rewrites are the current e-graph candidates.
4//! This crate keeps their proof requirements explicit without forcing an
5//! e-graph dependency into the core transform path.
6
7use std::fmt::Write as _;
8
9use egg::{
10    Analysis, Applier, EGraph, Extractor, Id, Pattern, PatternAst, RecExpr, Rewrite, Runner, Subst,
11    Symbol, Var, define_language, rewrite as egg_rewrite,
12};
13use omena_cascade_proof::{
14    REWRITE_CERTIFICATE_SCHEMA_VERSION_V0, RewriteCertificateEnvelopeV0, RewriteCertificateV0,
15    RewriteIssuanceTokenV0, RewriteSubstitutionEntryV0, RewriteTermV0, SideConditionCertV0,
16    check_rewrite_certificate_v0, selector_rewrite_rule_catalog_v0,
17};
18use omena_evidence_graph::ObligationFamilyIdV0;
19use omena_parser::StyleDialect;
20use omena_transform_cst::TransformPassKind;
21use omena_transform_passes::{
22    TransformPassPlanV0, collect_stale_vendor_prefix_removal_proof_candidates_from_source,
23    plan_transform_passes,
24};
25use serde::Serialize;
26
27mod mdl_cost;
28pub use mdl_cost::*;
29#[cfg(feature = "transform-catalog-saturation")]
30mod transform_catalog_analysis;
31#[cfg(feature = "transform-catalog-saturation")]
32pub use transform_catalog_analysis::*;
33
34define_language! {
35    enum CssRewriteLanguage {
36        Num(i64),
37        Symbol(Symbol),
38        "+" = Add([Id; 2]),
39        "-" = Sub([Id; 2]),
40        "*" = Mul([Id; 2]),
41        "/" = Div([Id; 2]),
42        "calc" = Calc(Id),
43        "unit" = Unit([Id; 2]),
44        "is" = Is(Id),
45        "where" = Where(Id),
46        "list" = List([Id; 2]),
47        "decl" = Declaration([Id; 3]),
48        "stale-prefix-decl" = StalePrefixDeclaration([Id; 4]),
49        "box1" = Box1(Id),
50        "box2" = Box2([Id; 2]),
51        "box3" = Box3([Id; 3]),
52        "box4" = Box4([Id; 4]),
53    }
54}
55
56#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
57#[serde(rename_all = "camelCase")]
58pub struct EggRewriteProofV0 {
59    pub specificity_preserved: bool,
60    #[serde(skip_serializing)]
61    obligation_family: ObligationFamilyIdV0,
62    pub computed_value_preserved: bool,
63    pub provenance_preserved: bool,
64    pub cascade_safe_witness: String,
65}
66
67impl EggRewriteProofV0 {
68    pub fn new(
69        specificity_preserved: bool,
70        obligation_family: ObligationFamilyIdV0,
71        provenance_preserved: bool,
72        cascade_safe_witness: impl Into<String>,
73    ) -> Self {
74        Self {
75            specificity_preserved,
76            obligation_family,
77            computed_value_preserved: obligation_family.preserves_computed_value(),
78            provenance_preserved,
79            cascade_safe_witness: cascade_safe_witness.into(),
80        }
81    }
82
83    pub const fn obligation_family(&self) -> ObligationFamilyIdV0 {
84        self.obligation_family
85    }
86}
87
88/// Evidence disposition for one caller-owned e-graph admission claim.
89///
90/// An issued token is bound to exact rewrite endpoints. A gap remains legal
91/// only as an explicit owner/re-entry declaration; it is never represented by
92/// a favourable Boolean.
93#[derive(Debug, Clone, PartialEq, Eq)]
94#[non_exhaustive]
95pub enum EggRewriteClaimEvidenceV0 {
96    IndependentlyChecked {
97        token: RewriteIssuanceTokenV0,
98    },
99    /// The checker derived the rewrite endpoints from a trusted catalog, but
100    /// the catalog rule carried no side-condition certificate for this claim.
101    DerivabilityOnly {
102        token: RewriteIssuanceTokenV0,
103    },
104    NotIndependentlyChecked {
105        owner: String,
106        reentry_condition: String,
107    },
108}
109
110impl EggRewriteClaimEvidenceV0 {
111    pub fn independently_checked(token: RewriteIssuanceTokenV0) -> Self {
112        Self::IndependentlyChecked { token }
113    }
114
115    pub fn derivability_only(token: RewriteIssuanceTokenV0) -> Self {
116        Self::DerivabilityOnly { token }
117    }
118
119    pub fn not_independently_checked(
120        owner: impl Into<String>,
121        reentry_condition: impl Into<String>,
122    ) -> Self {
123        Self::NotIndependentlyChecked {
124            owner: owner.into(),
125            reentry_condition: reentry_condition.into(),
126        }
127    }
128
129    fn issued_token(&self) -> Option<&RewriteIssuanceTokenV0> {
130        match self {
131            Self::IndependentlyChecked { token } | Self::DerivabilityOnly { token } => Some(token),
132            Self::NotIndependentlyChecked { .. } => None,
133        }
134    }
135
136    fn is_well_formed(&self) -> bool {
137        match self {
138            Self::IndependentlyChecked { .. } | Self::DerivabilityOnly { .. } => true,
139            Self::NotIndependentlyChecked {
140                owner,
141                reentry_condition,
142            } => !owner.trim().is_empty() && !reentry_condition.trim().is_empty(),
143        }
144    }
145}
146
147/// Additive typed replacement for the legacy Boolean proof carrier.
148///
149/// Computed-value preservation remains the existing obligation-family lookup;
150/// it is intentionally not represented as a fourth evidence claim.
151#[derive(Debug, Clone, PartialEq, Eq)]
152#[non_exhaustive]
153pub struct CheckedEggRewriteProofV0 {
154    pub specificity: EggRewriteClaimEvidenceV0,
155    obligation_family: ObligationFamilyIdV0,
156    pub provenance: EggRewriteClaimEvidenceV0,
157    pub cascade_safety: EggRewriteClaimEvidenceV0,
158}
159
160impl CheckedEggRewriteProofV0 {
161    pub fn new(
162        specificity: EggRewriteClaimEvidenceV0,
163        obligation_family: ObligationFamilyIdV0,
164        provenance: EggRewriteClaimEvidenceV0,
165        cascade_safety: EggRewriteClaimEvidenceV0,
166    ) -> Self {
167        Self {
168            specificity,
169            obligation_family,
170            provenance,
171            cascade_safety,
172        }
173    }
174
175    pub const fn obligation_family(&self) -> ObligationFamilyIdV0 {
176        self.obligation_family
177    }
178
179    pub const fn computed_value_preserved(&self) -> bool {
180        self.obligation_family.preserves_computed_value()
181    }
182}
183
184#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
185#[serde(rename_all = "camelCase")]
186pub struct EggRewriteCandidateV0 {
187    pub pass_id: &'static str,
188    pub before: String,
189    pub after: String,
190    pub proof: EggRewriteProofV0,
191}
192
193#[derive(Debug, Clone, PartialEq, Eq)]
194#[non_exhaustive]
195pub struct CheckedEggRewriteCandidateV0 {
196    pub pass_id: &'static str,
197    pub before: String,
198    pub after: String,
199    pub proof: CheckedEggRewriteProofV0,
200}
201
202impl CheckedEggRewriteCandidateV0 {
203    pub fn new(
204        pass_id: &'static str,
205        before: impl Into<String>,
206        after: impl Into<String>,
207        proof: CheckedEggRewriteProofV0,
208    ) -> Self {
209        Self {
210            pass_id,
211            before: before.into(),
212            after: after.into(),
213            proof,
214        }
215    }
216}
217
218#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
219#[serde(rename_all = "camelCase")]
220pub struct EggRewriteDecisionV0 {
221    pub schema_version: &'static str,
222    pub product: &'static str,
223    pub pass_id: &'static str,
224    pub accepted: bool,
225    pub blocked_reason: Option<&'static str>,
226}
227
228#[derive(Debug, Clone, PartialEq, Serialize)]
229#[serde(rename_all = "camelCase")]
230pub struct EggRewriteExecutionV0 {
231    pub schema_version: &'static str,
232    pub product: &'static str,
233    pub pass_id: &'static str,
234    pub accepted: bool,
235    pub blocked_reason: Option<&'static str>,
236    pub before: String,
237    pub after: String,
238    pub expected_after: String,
239    pub after_matches_candidate: bool,
240    pub engine: &'static str,
241    pub iteration_limit: usize,
242    pub iteration_count: usize,
243    pub eclass_count: usize,
244    pub enode_count: usize,
245    #[serde(skip_serializing_if = "Option::is_none")]
246    pub mdl_bits: Option<f64>,
247    #[serde(skip_serializing_if = "Option::is_none")]
248    pub mdl_residual_bits: Option<f64>,
249    #[serde(skip_serializing_if = "Option::is_none")]
250    pub mdl_unit: Option<&'static str>,
251}
252
253#[derive(Debug, Clone, PartialEq, Serialize)]
254#[serde(rename_all = "camelCase")]
255pub struct EggRewriteSourceWitnessV0 {
256    pub pass_id: &'static str,
257    pub source_kind: &'static str,
258    pub byte_offset: usize,
259    pub css_before: String,
260    pub css_after: String,
261    pub execution: EggRewriteExecutionV0,
262}
263
264#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
265#[serde(rename_all = "camelCase")]
266pub struct TransformEggBoundarySummaryV0 {
267    pub schema_version: &'static str,
268    pub product: &'static str,
269    pub managed_pass_ids: Vec<&'static str>,
270    pub optional_engine: &'static str,
271    pub proof_obligations: Vec<&'static str>,
272    pub planner_surface: &'static str,
273}
274
275#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
276#[serde(rename_all = "camelCase")]
277pub struct TransformEggPlanV0 {
278    pub schema_version: &'static str,
279    pub product: &'static str,
280    pub requested_pass_ids: Vec<&'static str>,
281    pub planned_pass_ids: Vec<&'static str>,
282    pub pass_plan: TransformPassPlanV0,
283}
284
285#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
286#[serde(rename_all = "camelCase")]
287pub struct ContextualEqSatScaffoldV0 {
288    pub schema_version: &'static str,
289    pub product: &'static str,
290    pub claim_level: &'static str,
291    pub scaffold_kind: &'static str,
292    pub execution_view: &'static str,
293    pub current_engine: &'static str,
294    pub egg_engine_ready: bool,
295    pub egglog_binding_ready: bool,
296    pub external_datalog_host_ready: bool,
297    pub three_view_fusion_ready: bool,
298    pub theorem_claimed: bool,
299    pub public_safety_claim_ready: bool,
300    pub modal_witness_product: &'static str,
301    pub modal_bridge_claim_level: &'static str,
302    pub paper_substrate_claim_level: &'static str,
303    pub managed_pass_ids: Vec<&'static str>,
304    pub substrate_products: Vec<&'static str>,
305    pub supported_claims: Vec<&'static str>,
306    pub deferred_claims: Vec<&'static str>,
307}
308
309#[derive(Debug, Clone, Copy)]
310enum CalcFoldOperator {
311    Add,
312    Sub,
313}
314
315#[derive(Debug, Clone)]
316struct ConstFoldSameUnitApplier {
317    left_var: Var,
318    right_var: Var,
319    unit_var: Option<Var>,
320    operator: CalcFoldOperator,
321}
322
323impl ConstFoldSameUnitApplier {
324    fn new(operator: CalcFoldOperator, unit_var: Option<Var>) -> Option<Self> {
325        Some(Self {
326            left_var: "?a".parse().ok()?,
327            right_var: "?b".parse().ok()?,
328            unit_var,
329            operator,
330        })
331    }
332}
333
334impl<N> Applier<CssRewriteLanguage, N> for ConstFoldSameUnitApplier
335where
336    N: Analysis<CssRewriteLanguage>,
337{
338    fn apply_one(
339        &self,
340        egraph: &mut EGraph<CssRewriteLanguage, N>,
341        eclass: Id,
342        subst: &Subst,
343        _searcher_ast: Option<&PatternAst<CssRewriteLanguage>>,
344        _rule_name: Symbol,
345    ) -> Vec<Id> {
346        let Some(left) = numeric_value_from_eclass(egraph, subst[self.left_var]) else {
347            return Vec::new();
348        };
349        let Some(right) = numeric_value_from_eclass(egraph, subst[self.right_var]) else {
350            return Vec::new();
351        };
352        let value = match self.operator {
353            CalcFoldOperator::Add => left + right,
354            CalcFoldOperator::Sub => left - right,
355        };
356        let value_id = egraph.add(CssRewriteLanguage::Num(value));
357        let result_id = if let Some(unit_var) = self.unit_var {
358            egraph.add(CssRewriteLanguage::Unit([value_id, subst[unit_var]]))
359        } else {
360            value_id
361        };
362        egraph.union(eclass, result_id);
363        vec![eclass]
364    }
365
366    fn vars(&self) -> Vec<Var> {
367        let mut vars = vec![self.left_var, self.right_var];
368        if let Some(unit_var) = self.unit_var {
369            vars.push(unit_var);
370        }
371        vars
372    }
373}
374
375pub fn summarize_omena_transform_egg_boundary() -> TransformEggBoundarySummaryV0 {
376    TransformEggBoundarySummaryV0 {
377        schema_version: "0",
378        product: "omena-transform-egg.boundary",
379        managed_pass_ids: managed_egg_passes().iter().map(|pass| pass.id()).collect(),
380        optional_engine: "egg-compatible equality saturation engine",
381        proof_obligations: vec![
382            "selector rewrites preserve specificity",
383            "calc rewrites preserve computed value",
384            "shorthand rewrites preserve computed value",
385            "stale-prefix removals preserve an exact unprefixed declaration peer",
386            "all rewrites preserve provenance",
387            "all accepted rewrites carry a cascade-safe witness",
388        ],
389        planner_surface: "omena-transform-passes.plan",
390    }
391}
392
393pub fn plan_egg_rewrite_passes(include_selector: bool, include_calc: bool) -> TransformEggPlanV0 {
394    let mut requested_passes = Vec::new();
395    if include_selector {
396        requested_passes.push(TransformPassKind::SelectorIsWhereCompression);
397    }
398    if include_calc {
399        requested_passes.push(TransformPassKind::CalcReduction);
400    }
401    let pass_plan = plan_transform_passes(&requested_passes);
402
403    TransformEggPlanV0 {
404        schema_version: "0",
405        product: "omena-transform-egg.plan",
406        requested_pass_ids: requested_passes.iter().map(|pass| pass.id()).collect(),
407        planned_pass_ids: pass_plan.ordered_pass_ids.clone(),
408        pass_plan,
409    }
410}
411
412pub fn plan_egg_rewrite_passes_for_source(source: &str) -> TransformEggPlanV0 {
413    plan_egg_rewrite_passes(
414        source.contains(":is(") || source.contains(":where("),
415        source.contains("calc("),
416    )
417}
418
419pub fn summarize_contextual_eqsat_scaffold_v0() -> ContextualEqSatScaffoldV0 {
420    let boundary = summarize_omena_transform_egg_boundary();
421
422    ContextualEqSatScaffoldV0 {
423        schema_version: "0",
424        product: "omena-transform-egg.contextual-eqsat-scaffold",
425        claim_level: "m6ScaffoldOnlyNoEgglogBinding",
426        scaffold_kind: "contextualEqualitySaturationExecutionView",
427        execution_view: "m6BridgeNodeExecutionView",
428        current_engine: "egg",
429        egg_engine_ready: true,
430        egglog_binding_ready: false,
431        external_datalog_host_ready: false,
432        three_view_fusion_ready: false,
433        theorem_claimed: false,
434        public_safety_claim_ready: false,
435        modal_witness_product: "omena-cascade.modal-check-witness",
436        modal_bridge_claim_level: "dependencyDeclaredOnly",
437        paper_substrate_claim_level: "draftScaffoldOnly",
438        managed_pass_ids: boundary.managed_pass_ids,
439        substrate_products: vec![
440            "omena-transform-egg.boundary",
441            "omena-transform-egg.plan",
442            "omena-transform-egg.execution",
443            "omena-cascade.modal-check-witness",
444        ],
445        supported_claims: vec![
446            "optional egg equality-saturation rewrite boundary",
447            "selector, calc, and shorthand rewrite proof obligations",
448            "contextual equality-saturation scaffold for M6 positioning",
449            "modal witness dependency declaration for #66/#73 paper substrate",
450        ],
451        deferred_claims: vec![
452            "egglog Rust binding",
453            "external Datalog host execution",
454            "full three-view fusion",
455            "Contextual EqSat theorem",
456            "production research-tier execution view",
457        ],
458    }
459}
460
461pub fn decide_egg_rewrite(candidate: EggRewriteCandidateV0) -> EggRewriteDecisionV0 {
462    // E7 measured every one of these seven blocking predicates constant-true
463    // on production witness paths. They remain here as the legacy contract and
464    // as a record of what callers claimed. Production selector safety actually
465    // comes from `selector_witness_candidate`'s syntax filter; the checked path
466    // below additionally requires an endpoint-bound kernel token.
467    let blocked_reason = if !is_managed_egg_pass_id(candidate.pass_id) {
468        Some("pass is not managed by omena-transform-egg")
469    } else if candidate.proof.cascade_safe_witness.is_empty() {
470        Some("missing cascade-safe witness")
471    } else if !candidate.proof.provenance_preserved {
472        Some("rewrite does not preserve provenance")
473    } else if candidate.pass_id == TransformPassKind::SelectorIsWhereCompression.id()
474        && !candidate.proof.specificity_preserved
475    {
476        Some("selector rewrite does not preserve specificity")
477    } else if candidate.pass_id == TransformPassKind::CalcReduction.id()
478        && !candidate.proof.computed_value_preserved
479    {
480        Some("calc rewrite does not preserve computed value")
481    } else if candidate.pass_id == TransformPassKind::ShorthandCombining.id()
482        && !candidate.proof.computed_value_preserved
483    {
484        Some("shorthand rewrite does not preserve computed value")
485    } else if candidate.pass_id == TransformPassKind::StalePrefixRemoval.id()
486        && !candidate.proof.computed_value_preserved
487    {
488        Some("stale-prefix removal does not preserve computed value")
489    } else {
490        None
491    };
492
493    EggRewriteDecisionV0 {
494        schema_version: "0",
495        product: "omena-transform-egg.decision",
496        pass_id: candidate.pass_id,
497        accepted: blocked_reason.is_none(),
498        blocked_reason,
499    }
500}
501
502pub fn decide_checked_egg_rewrite(
503    candidate: &CheckedEggRewriteCandidateV0,
504) -> EggRewriteDecisionV0 {
505    let endpoint_terms = selector_kernel_terms_v0(&candidate.before, &candidate.after);
506    let trusted_selector_catalog = selector_rewrite_rule_catalog_v0();
507    let evidence = [
508        &candidate.proof.specificity,
509        &candidate.proof.provenance,
510        &candidate.proof.cascade_safety,
511    ];
512    let blocked_reason = if !is_managed_egg_pass_id(candidate.pass_id) {
513        Some("pass is not managed by omena-transform-egg")
514    } else if evidence.iter().any(|claim| !claim.is_well_formed()) {
515        Some("independent-check gap is missing an owner or re-entry condition")
516    } else if candidate.pass_id == TransformPassKind::SelectorIsWhereCompression.id()
517        && candidate.proof.specificity.issued_token().is_none()
518    {
519        Some("selector rewrite requires a checker-issued derivability token for specificity")
520    } else if candidate.pass_id == TransformPassKind::SelectorIsWhereCompression.id()
521        && candidate.proof.cascade_safety.issued_token().is_none()
522    {
523        Some("selector rewrite requires a checker-issued derivability token for cascade safety")
524    } else if candidate.pass_id == TransformPassKind::SelectorIsWhereCompression.id()
525        && evidence
526            .iter()
527            .filter_map(|claim| claim.issued_token())
528            .any(|token| !token.matches_catalog_v0(&trusted_selector_catalog))
529    {
530        Some("rewrite certificate token does not match the trusted rule catalog")
531    } else if evidence
532        .iter()
533        .filter_map(|claim| claim.issued_token())
534        .any(|token| {
535            endpoint_terms
536                .as_ref()
537                .is_none_or(|(before, after)| !token.matches_endpoints_v0(before, after))
538        })
539    {
540        Some("rewrite certificate token does not match candidate endpoints")
541    } else if candidate.pass_id == TransformPassKind::CalcReduction.id()
542        && !candidate.proof.computed_value_preserved()
543    {
544        Some("calc rewrite does not preserve computed value")
545    } else if candidate.pass_id == TransformPassKind::ShorthandCombining.id()
546        && !candidate.proof.computed_value_preserved()
547    {
548        Some("shorthand rewrite does not preserve computed value")
549    } else if candidate.pass_id == TransformPassKind::StalePrefixRemoval.id()
550        && !candidate.proof.computed_value_preserved()
551    {
552        Some("stale-prefix removal does not preserve computed value")
553    } else {
554        None
555    };
556
557    EggRewriteDecisionV0 {
558        schema_version: "0",
559        product: "omena-transform-egg.decision",
560        pass_id: candidate.pass_id,
561        accepted: blocked_reason.is_none(),
562        blocked_reason,
563    }
564}
565
566pub fn execute_egg_rewrite(candidate: EggRewriteCandidateV0) -> EggRewriteExecutionV0 {
567    let decision = decide_egg_rewrite(candidate.clone());
568    execute_egg_rewrite_after_decision(
569        candidate.pass_id,
570        candidate.before,
571        candidate.after,
572        decision,
573    )
574}
575
576pub fn execute_checked_egg_rewrite(
577    candidate: CheckedEggRewriteCandidateV0,
578) -> EggRewriteExecutionV0 {
579    let decision = decide_checked_egg_rewrite(&candidate);
580    execute_egg_rewrite_after_decision(
581        candidate.pass_id,
582        candidate.before,
583        candidate.after,
584        decision,
585    )
586}
587
588fn execute_egg_rewrite_after_decision(
589    pass_id: &'static str,
590    before: String,
591    expected_after: String,
592    decision: EggRewriteDecisionV0,
593) -> EggRewriteExecutionV0 {
594    if !decision.accepted {
595        return blocked_execution_parts(pass_id, before, expected_after, decision.blocked_reason);
596    }
597
598    let expression = match before.parse::<RecExpr<CssRewriteLanguage>>() {
599        Ok(expression) => expression,
600        Err(_) => {
601            return blocked_execution_parts(
602                pass_id,
603                before,
604                expected_after,
605                Some("rewrite expression could not parse"),
606            );
607        }
608    };
609    let Some(rules) = rewrite_rules_for_pass::<()>(pass_id) else {
610        return blocked_execution_parts(
611            pass_id,
612            before,
613            expected_after,
614            Some("pass is not managed by omena-transform-egg"),
615        );
616    };
617
618    let iteration_limit = 8;
619    let runner = Runner::default()
620        .with_expr(&expression)
621        .with_iter_limit(iteration_limit)
622        .run(rules.as_slice());
623    let root = runner.roots[0];
624    let extractor = Extractor::new(&runner.egraph, MdlExtractionCostV0::default_ast_size());
625    let (_, extracted) = extractor.find_best(root);
626    let after = extracted.to_string();
627    let after_matches_candidate = after == expected_after;
628
629    EggRewriteExecutionV0 {
630        schema_version: "0",
631        product: "omena-transform-egg.execution",
632        pass_id,
633        accepted: after_matches_candidate,
634        blocked_reason: (!after_matches_candidate)
635            .then_some("egg extraction did not match candidate output"),
636        before,
637        after,
638        expected_after,
639        after_matches_candidate,
640        engine: "egg",
641        iteration_limit,
642        iteration_count: runner.iterations.len(),
643        eclass_count: runner.egraph.number_of_classes(),
644        enode_count: runner.egraph.total_size(),
645        mdl_bits: None,
646        mdl_residual_bits: None,
647        mdl_unit: None,
648    }
649}
650
651pub fn execute_egg_rewrite_witnesses_for_css_source(
652    source: &str,
653    dialect: StyleDialect,
654    transformed_source: &str,
655    planned_pass_ids: &[&'static str],
656) -> Vec<EggRewriteSourceWitnessV0> {
657    let mut witnesses = Vec::new();
658    if planned_pass_ids.contains(&TransformPassKind::SelectorIsWhereCompression.id()) {
659        witnesses.extend(selector_rewrite_witnesses(source, transformed_source));
660    }
661    if planned_pass_ids.contains(&TransformPassKind::CalcReduction.id()) {
662        witnesses.extend(calc_rewrite_witnesses(source, transformed_source));
663    }
664    if planned_pass_ids.contains(&TransformPassKind::StalePrefixRemoval.id()) {
665        witnesses.extend(stale_prefix_removal_witnesses(
666            source,
667            dialect,
668            transformed_source,
669        ));
670    }
671    witnesses
672}
673
674fn managed_egg_passes() -> [TransformPassKind; 4] {
675    [
676        TransformPassKind::SelectorIsWhereCompression,
677        TransformPassKind::CalcReduction,
678        TransformPassKind::ShorthandCombining,
679        TransformPassKind::StalePrefixRemoval,
680    ]
681}
682
683fn is_managed_egg_pass_id(pass_id: &str) -> bool {
684    managed_egg_passes().iter().any(|pass| pass.id() == pass_id)
685}
686
687fn numeric_value_from_eclass<N>(egraph: &EGraph<CssRewriteLanguage, N>, id: Id) -> Option<i64>
688where
689    N: Analysis<CssRewriteLanguage>,
690{
691    egraph[id].nodes.iter().find_map(|node| match node {
692        CssRewriteLanguage::Num(value) => Some(*value),
693        _ => None,
694    })
695}
696
697fn selector_rewrite_witnesses(
698    source: &str,
699    transformed_source: &str,
700) -> Vec<EggRewriteSourceWitnessV0> {
701    let mut witnesses = Vec::new();
702    for (prefix, source_kind) in [(":is(", "selectorIs"), (":where(", "selectorWhere")] {
703        let mut cursor = 0usize;
704        while let Some(relative_start) = source[cursor..].find(prefix) {
705            let start = cursor + relative_start;
706            let inner_start = start + prefix.len();
707            let Some(relative_end) = source[inner_start..].find(')') else {
708                break;
709            };
710            let end = inner_start + relative_end;
711            let inner = source[inner_start..end].trim();
712            let css_before = source[start..=end].to_string();
713            let pseudo_name = prefix.trim_start_matches(':').trim_end_matches('(');
714            if let Some((source_kind, css_after, before, after, _legacy_witness)) =
715                selector_witness_candidate(pseudo_name, source_kind, inner)
716                && transformed_source.contains(&css_after)
717                && !transformed_source.contains(&css_before)
718                && let Some(token) = selector_rewrite_issuance_token_v0(&before, &after)
719            {
720                let execution = execute_checked_egg_rewrite(CheckedEggRewriteCandidateV0 {
721                    pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
722                    before,
723                    after,
724                    proof: CheckedEggRewriteProofV0::new(
725                        EggRewriteClaimEvidenceV0::derivability_only(token.clone()),
726                        ObligationFamilyIdV0::CascadeSafetyFloor,
727                        declared_provenance_gap_v0(),
728                        EggRewriteClaimEvidenceV0::derivability_only(token),
729                    ),
730                });
731                witnesses.push(EggRewriteSourceWitnessV0 {
732                    pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
733                    source_kind,
734                    byte_offset: start,
735                    css_before,
736                    css_after,
737                    execution,
738                });
739            }
740            cursor = end + 1;
741        }
742    }
743    witnesses
744}
745
746fn calc_rewrite_witnesses(
747    source: &str,
748    transformed_source: &str,
749) -> Vec<EggRewriteSourceWitnessV0> {
750    let mut witnesses = Vec::new();
751    let mut cursor = 0usize;
752    while let Some(relative_start) = source[cursor..].find("calc(") {
753        let start = cursor + relative_start;
754        let inner_start = start + "calc(".len();
755        let Some(relative_end) = source[inner_start..].find(')') else {
756            break;
757        };
758        let end = inner_start + relative_end;
759        let inner = source[inner_start..end].trim();
760        let css_before = source[start..=end].to_string();
761        if let Some(candidate) = calc_rewrite_candidate(inner)
762            && transformed_source.contains(candidate.css_after.as_str())
763            && !transformed_source.contains(&css_before)
764        {
765            let execution = execute_checked_egg_rewrite(CheckedEggRewriteCandidateV0 {
766                pass_id: TransformPassKind::CalcReduction.id(),
767                before: format!("(calc {})", candidate.before),
768                after: candidate.after,
769                proof: CheckedEggRewriteProofV0::new(
770                    declared_specificity_gap_v0(),
771                    ObligationFamilyIdV0::ComputedValuePreservation,
772                    declared_provenance_gap_v0(),
773                    declared_cascade_safety_gap_v0(candidate.witness),
774                ),
775            });
776            witnesses.push(EggRewriteSourceWitnessV0 {
777                pass_id: TransformPassKind::CalcReduction.id(),
778                source_kind: candidate.source_kind,
779                byte_offset: start,
780                css_before,
781                css_after: candidate.css_after,
782                execution,
783            });
784        }
785        cursor = end + 1;
786    }
787    witnesses
788}
789
790fn stale_prefix_removal_witnesses(
791    source: &str,
792    dialect: StyleDialect,
793    transformed_source: &str,
794) -> Vec<EggRewriteSourceWitnessV0> {
795    collect_stale_vendor_prefix_removal_proof_candidates_from_source(source, dialect)
796        .into_iter()
797        .filter_map(|candidate| {
798            let css_before =
799                source[candidate.source_span_start..candidate.source_span_end].to_string();
800            if transformed_source.contains(&css_before) {
801                return None;
802            }
803            let css_after = source
804                [candidate.unprefixed_peer_span_start..candidate.unprefixed_peer_span_end]
805                .to_string();
806            if !transformed_source.contains(&css_after) {
807                return None;
808            }
809
810            let prefixed_property =
811                egg_safe_symbol(candidate.prefixed_property.to_standard_key().as_str());
812            let unprefixed_property = egg_safe_symbol(candidate.unprefixed_property);
813            let value = egg_safe_symbol(candidate.value.as_str());
814            let importance = if candidate.important {
815                "important"
816            } else {
817                "normal"
818            };
819            let mut cascade_safety_gap = String::new();
820            let _ = candidate
821                .prefixed_property
822                .write_into(&mut cascade_safety_gap);
823            let _ = write!(
824                &mut cascade_safety_gap,
825                " has exact unprefixed declaration peer {} with the same value and importance",
826                candidate.unprefixed_property
827            );
828            let execution = execute_checked_egg_rewrite(CheckedEggRewriteCandidateV0 {
829                pass_id: TransformPassKind::StalePrefixRemoval.id(),
830                before: format!(
831                    "(stale-prefix-decl {prefixed_property} {unprefixed_property} {value} {importance})"
832                ),
833                after: format!("(decl {unprefixed_property} {value} {importance})"),
834                proof: CheckedEggRewriteProofV0::new(
835                    declared_specificity_gap_v0(),
836                    ObligationFamilyIdV0::ComputedValuePreservation,
837                    declared_provenance_gap_v0(),
838                    declared_cascade_safety_gap_v0(cascade_safety_gap),
839                ),
840            });
841            Some(EggRewriteSourceWitnessV0 {
842                pass_id: TransformPassKind::StalePrefixRemoval.id(),
843                source_kind: "stalePrefixExactPeer",
844                byte_offset: candidate.source_span_start,
845                css_before,
846                css_after,
847                execution,
848            })
849        })
850        .collect()
851}
852
853fn declared_specificity_gap_v0() -> EggRewriteClaimEvidenceV0 {
854    EggRewriteClaimEvidenceV0::not_independently_checked(
855        "omena-transform-egg maintainers",
856        "supply an endpoint-bound specificity certificate before requiring this claim for non-selector rewrites",
857    )
858}
859
860fn declared_provenance_gap_v0() -> EggRewriteClaimEvidenceV0 {
861    EggRewriteClaimEvidenceV0::not_independently_checked(
862        "omena-transform-egg maintainers",
863        "supply SourceMapTraceCertV0 from emitted segments before treating provenance as independently checked",
864    )
865}
866
867fn declared_cascade_safety_gap_v0(producer_claim: impl Into<String>) -> EggRewriteClaimEvidenceV0 {
868    EggRewriteClaimEvidenceV0::not_independently_checked(
869        "omena-transform-egg maintainers",
870        format!(
871            "replace producer claim {:?} with a matching S1 certificate before tightening cascade-safety admission",
872            producer_claim.into()
873        ),
874    )
875}
876
877fn selector_rewrite_issuance_token_v0(before: &str, after: &str) -> Option<RewriteIssuanceTokenV0> {
878    let (before_term, after_term) = selector_kernel_terms_v0(before, after)?;
879    let certificate = selector_rewrite_certificate_v0(&before_term, &after_term)?;
880    check_rewrite_certificate_v0(
881        &before_term,
882        &after_term,
883        &selector_rewrite_rule_catalog_v0(),
884        &certificate,
885    )
886    .ok()
887}
888
889fn selector_rewrite_certificate_v0(
890    before: &RewriteTermV0,
891    after: &RewriteTermV0,
892) -> Option<RewriteCertificateEnvelopeV0> {
893    let rewrite = match (before, after) {
894        (RewriteTermV0::Apply { operator, operands }, after)
895            if operator == "selectorIs" && operands.as_slice() == [after.clone()] =>
896        {
897            selector_rule_application_v0("selector-is-single-v0", after)
898        }
899        (RewriteTermV0::Apply { operator, operands }, after) if operator == "selectorIs" => {
900            let [
901                RewriteTermV0::Apply {
902                    operator: list_operator,
903                    operands: list_operands,
904                },
905            ] = operands.as_slice()
906            else {
907                return None;
908            };
909            let [left, right] = list_operands.as_slice() else {
910                return None;
911            };
912            if list_operator != "selectorList2" || left != right || left != after {
913                return None;
914            }
915            RewriteCertificateV0::Trans {
916                left: Box::new(RewriteCertificateV0::Cong {
917                    operator: "selectorIs".to_owned(),
918                    certificates: vec![selector_rule_application_v0(
919                        "selector-list-deduplicate-v0",
920                        left,
921                    )],
922                }),
923                right: Box::new(selector_rule_application_v0("selector-is-single-v0", left)),
924            }
925        }
926        (
927            RewriteTermV0::Apply {
928                operator: before_operator,
929                operands: before_operands,
930            },
931            RewriteTermV0::Apply {
932                operator: after_operator,
933                operands: after_operands,
934            },
935        ) if before_operator == "selectorWhere" && after_operator == "selectorWhere" => {
936            let [
937                RewriteTermV0::Apply {
938                    operator: list_operator,
939                    operands: list_operands,
940                },
941            ] = before_operands.as_slice()
942            else {
943                return None;
944            };
945            let [left, right] = list_operands.as_slice() else {
946                return None;
947            };
948            let [after_operand] = after_operands.as_slice() else {
949                return None;
950            };
951            if list_operator != "selectorList2" || left != right || left != after_operand {
952                return None;
953            }
954            RewriteCertificateV0::Cong {
955                operator: "selectorWhere".to_owned(),
956                certificates: vec![selector_rule_application_v0(
957                    "selector-list-deduplicate-v0",
958                    left,
959                )],
960            }
961        }
962        _ => return None,
963    };
964    Some(RewriteCertificateEnvelopeV0 {
965        schema_version: REWRITE_CERTIFICATE_SCHEMA_VERSION_V0.to_owned(),
966        max_depth: 8,
967        max_nodes: 16,
968        certificate: rewrite,
969    })
970}
971
972fn selector_rule_application_v0(rule_id: &str, term: &RewriteTermV0) -> RewriteCertificateV0 {
973    RewriteCertificateV0::Rewrite {
974        rule_id: rule_id.to_owned(),
975        substitution: vec![RewriteSubstitutionEntryV0 {
976            variable: "x".to_owned(),
977            term: term.clone(),
978        }],
979        side_condition: SideConditionCertV0::NoSideCondition,
980    }
981}
982
983fn selector_kernel_terms_v0(before: &str, after: &str) -> Option<(RewriteTermV0, RewriteTermV0)> {
984    Some((
985        selector_kernel_term_v0(before)?,
986        selector_kernel_term_v0(after)?,
987    ))
988}
989
990fn selector_kernel_term_v0(source: &str) -> Option<RewriteTermV0> {
991    let expression = source.parse::<RecExpr<CssRewriteLanguage>>().ok()?;
992    let root = Id::from(expression.as_ref().len().checked_sub(1)?);
993    selector_kernel_term_at_v0(&expression, root)
994}
995
996fn selector_kernel_term_at_v0(
997    expression: &RecExpr<CssRewriteLanguage>,
998    id: Id,
999) -> Option<RewriteTermV0> {
1000    match &expression[id] {
1001        CssRewriteLanguage::Symbol(symbol) => Some(RewriteTermV0::atom(symbol.to_string())),
1002        CssRewriteLanguage::Is(child) => Some(RewriteTermV0::apply(
1003            "selectorIs",
1004            vec![selector_kernel_term_at_v0(expression, *child)?],
1005        )),
1006        CssRewriteLanguage::Where(child) => Some(RewriteTermV0::apply(
1007            "selectorWhere",
1008            vec![selector_kernel_term_at_v0(expression, *child)?],
1009        )),
1010        CssRewriteLanguage::List(children) => Some(RewriteTermV0::apply(
1011            "selectorList2",
1012            vec![
1013                selector_kernel_term_at_v0(expression, children[0])?,
1014                selector_kernel_term_at_v0(expression, children[1])?,
1015            ],
1016        )),
1017        _ => None,
1018    }
1019}
1020
1021fn selector_witness_candidate(
1022    pseudo_name: &str,
1023    source_kind: &'static str,
1024    inner: &str,
1025) -> Option<(&'static str, String, String, String, String)> {
1026    if pseudo_name == "is"
1027        && let Some((symbol, css_ident)) = selector_single_argument_parts(inner)
1028    {
1029        return Some((
1030            source_kind,
1031            format!(".{css_ident}"),
1032            format!("(is {symbol})"),
1033            symbol,
1034            "actual CSS selectorIs single-argument rewrite".to_string(),
1035        ));
1036    }
1037
1038    let args = split_simple_selector_arguments(inner)?;
1039    let [left, right] = args.as_slice() else {
1040        return None;
1041    };
1042    if left != right {
1043        return None;
1044    }
1045    let (symbol, css_ident) = selector_single_argument_parts(left)?;
1046    match pseudo_name {
1047        "is" => Some((
1048            "selectorIsDedup",
1049            format!(".{css_ident}"),
1050            format!("(is (list {symbol} {symbol}))"),
1051            symbol,
1052            "actual CSS selectorIs duplicate-argument rewrite".to_string(),
1053        )),
1054        "where" => Some((
1055            "selectorWhereDedup",
1056            format!(":where(.{css_ident})"),
1057            format!("(where (list {symbol} {symbol}))"),
1058            format!("(where {symbol})"),
1059            "actual CSS selectorWhere duplicate-argument rewrite".to_string(),
1060        )),
1061        _ => None,
1062    }
1063}
1064
1065fn egg_safe_symbol(value: &str) -> String {
1066    let mut symbol = String::with_capacity(value.len().max(1));
1067    for byte in value.bytes() {
1068        let character = byte as char;
1069        if character.is_ascii_alphanumeric() {
1070            symbol.push(character.to_ascii_lowercase());
1071        } else {
1072            let _ = write!(&mut symbol, "_{byte:02x}");
1073        }
1074    }
1075    if symbol.is_empty() {
1076        "empty".to_string()
1077    } else if symbol
1078        .as_bytes()
1079        .first()
1080        .is_some_and(|byte| byte.is_ascii_digit())
1081    {
1082        format!("v_{symbol}")
1083    } else {
1084        symbol
1085    }
1086}
1087
1088fn split_simple_selector_arguments(inner: &str) -> Option<Vec<String>> {
1089    let args = inner
1090        .split(',')
1091        .map(str::trim)
1092        .map(str::to_string)
1093        .collect::<Vec<_>>();
1094    (!args.is_empty() && args.iter().all(|arg| !arg.is_empty())).then_some(args)
1095}
1096
1097fn selector_single_argument_parts(inner: &str) -> Option<(String, String)> {
1098    let class_name = inner.trim().strip_prefix('.')?;
1099    if class_name.is_empty()
1100        || !class_name
1101            .chars()
1102            .all(|ch| ch.is_ascii_alphanumeric() || matches!(ch, '_' | '-'))
1103    {
1104        return None;
1105    }
1106    Some((symbol_for_css_ident(class_name), class_name.to_string()))
1107}
1108
1109fn symbol_for_css_ident(value: &str) -> String {
1110    value.replace('-', "_")
1111}
1112
1113#[derive(Debug, Clone, PartialEq, Eq)]
1114struct CalcRewriteCandidate {
1115    before: String,
1116    after: String,
1117    css_after: String,
1118    source_kind: &'static str,
1119    witness: String,
1120}
1121
1122#[derive(Debug, Clone, PartialEq, Eq)]
1123struct CalcNumericValue {
1124    value: i64,
1125    unit: String,
1126}
1127
1128fn calc_rewrite_candidate(inner: &str) -> Option<CalcRewriteCandidate> {
1129    let parts = inner.split_whitespace().collect::<Vec<_>>();
1130    let [left, operator, right] = parts.as_slice() else {
1131        return None;
1132    };
1133    let left_value = parse_calc_numeric_value(left)?;
1134    let right_value = parse_calc_numeric_value(right)?;
1135    if left_value.unit != right_value.unit {
1136        return None;
1137    }
1138    let term_left = calc_numeric_term(&left_value);
1139    let term_right = calc_numeric_term(&right_value);
1140    match *operator {
1141        "+" => Some(calc_fold_candidate(
1142            format!("(+ {term_left} {term_right})"),
1143            left_value.value + right_value.value,
1144            &left_value.unit,
1145            "calcSameUnitAdd",
1146            "actual CSS calc same-unit addition rewrite",
1147        )),
1148        "-" => Some(calc_fold_candidate(
1149            format!("(- {term_left} {term_right})"),
1150            left_value.value - right_value.value,
1151            &left_value.unit,
1152            "calcSameUnitSub",
1153            "actual CSS calc same-unit subtraction rewrite",
1154        )),
1155        "*" if right_value.value == 1 && right_value.unit.is_empty() => {
1156            Some(calc_passthrough_candidate(
1157                format!("(* {term_left} 1)"),
1158                &left_value,
1159                "calcIdentity",
1160                "actual CSS calc multiplicative identity rewrite",
1161            ))
1162        }
1163        "*" if left_value.value == 1 && left_value.unit.is_empty() => {
1164            Some(calc_passthrough_candidate(
1165                format!("(* 1 {term_right})"),
1166                &right_value,
1167                "calcIdentity",
1168                "actual CSS calc multiplicative identity rewrite",
1169            ))
1170        }
1171        "*" if right_value.value == 0 && right_value.unit.is_empty() => Some(calc_fold_candidate(
1172            format!("(* {term_left} 0)"),
1173            0,
1174            "",
1175            "calcZero",
1176            "actual CSS calc safe zero multiplication rewrite",
1177        )),
1178        "*" if left_value.value == 0 && left_value.unit.is_empty() => Some(calc_fold_candidate(
1179            format!("(* 0 {term_right})"),
1180            0,
1181            "",
1182            "calcZero",
1183            "actual CSS calc safe zero multiplication rewrite",
1184        )),
1185        "/" if right_value.value == 1 && right_value.unit.is_empty() => {
1186            Some(calc_passthrough_candidate(
1187                format!("(/ {term_left} 1)"),
1188                &left_value,
1189                "calcIdentity",
1190                "actual CSS calc division identity rewrite",
1191            ))
1192        }
1193        _ => None,
1194    }
1195}
1196
1197fn parse_calc_numeric_value(text: &str) -> Option<CalcNumericValue> {
1198    let split = text
1199        .char_indices()
1200        .find_map(|(index, ch)| (!matches!(ch, '-' | '+') && !ch.is_ascii_digit()).then_some(index))
1201        .unwrap_or(text.len());
1202    let (value, unit) = text.split_at(split);
1203    let value = value.parse::<i64>().ok()?;
1204    unit.chars()
1205        .all(|ch| ch.is_ascii_alphabetic() || ch == '%')
1206        .then_some(CalcNumericValue {
1207            value,
1208            unit: unit.to_string(),
1209        })
1210}
1211
1212fn calc_numeric_term(value: &CalcNumericValue) -> String {
1213    if value.unit.is_empty() {
1214        value.value.to_string()
1215    } else {
1216        format!("(unit {} {})", value.value, value.unit)
1217    }
1218}
1219
1220fn calc_fold_candidate(
1221    before: String,
1222    value: i64,
1223    unit: &str,
1224    source_kind: &'static str,
1225    witness: &'static str,
1226) -> CalcRewriteCandidate {
1227    let result = CalcNumericValue {
1228        value,
1229        unit: unit.to_string(),
1230    };
1231    CalcRewriteCandidate {
1232        before,
1233        after: calc_numeric_term(&result),
1234        css_after: format!("{}{}", result.value, result.unit),
1235        source_kind,
1236        witness: witness.to_string(),
1237    }
1238}
1239
1240fn calc_passthrough_candidate(
1241    before: String,
1242    value: &CalcNumericValue,
1243    source_kind: &'static str,
1244    witness: &'static str,
1245) -> CalcRewriteCandidate {
1246    CalcRewriteCandidate {
1247        before,
1248        after: calc_numeric_term(value),
1249        css_after: format!("{}{}", value.value, value.unit),
1250        source_kind,
1251        witness: witness.to_string(),
1252    }
1253}
1254
1255fn rewrite_pattern(text: &str) -> Option<Pattern<CssRewriteLanguage>> {
1256    text.parse().ok()
1257}
1258
1259pub(crate) fn calc_const_fold_rule<N>(
1260    name: &'static str,
1261    search: &'static str,
1262    operator: CalcFoldOperator,
1263    unit_var: Option<Var>,
1264) -> Option<Rewrite<CssRewriteLanguage, N>>
1265where
1266    N: Analysis<CssRewriteLanguage>,
1267{
1268    Rewrite::new(
1269        name,
1270        rewrite_pattern(search)?,
1271        ConstFoldSameUnitApplier::new(operator, unit_var)?,
1272    )
1273    .ok()
1274}
1275
1276fn egg_var(name: &str) -> Option<Var> {
1277    name.parse().ok()
1278}
1279
1280pub(crate) fn rewrite_rules_for_pass<N>(
1281    pass_id: &'static str,
1282) -> Option<Vec<Rewrite<CssRewriteLanguage, N>>>
1283where
1284    N: Analysis<CssRewriteLanguage>,
1285{
1286    if pass_id == TransformPassKind::SelectorIsWhereCompression.id() {
1287        return Some(vec![
1288            egg_rewrite!("single-is-selector"; "(is ?a)" => "?a"),
1289            egg_rewrite!("nested-is-selector"; "(is (is ?a))" => "?a"),
1290            egg_rewrite!("duplicate-is-selector"; "(is (list ?a ?a))" => "?a"),
1291            egg_rewrite!("duplicate-where-selector"; "(where (list ?a ?a))" => "(where ?a)"),
1292        ]);
1293    }
1294    if pass_id == TransformPassKind::CalcReduction.id() {
1295        let mut rules = vec![
1296            egg_rewrite!("unwrap-calc"; "(calc ?a)" => "?a"),
1297            egg_rewrite!("add-zero-right"; "(+ ?a 0)" => "?a"),
1298            egg_rewrite!("add-zero-left"; "(+ 0 ?a)" => "?a"),
1299            egg_rewrite!("sub-zero-right"; "(- ?a 0)" => "?a"),
1300            egg_rewrite!("self-sub"; "(- ?a ?a)" => "0"),
1301            egg_rewrite!("mul-one-right"; "(* ?a 1)" => "?a"),
1302            egg_rewrite!("mul-one-left"; "(* 1 ?a)" => "?a"),
1303            egg_rewrite!("mul-zero-right"; "(* ?a 0)" => "0"),
1304            egg_rewrite!("mul-zero-left"; "(* 0 ?a)" => "0"),
1305            egg_rewrite!("div-one-right"; "(/ ?a 1)" => "?a"),
1306        ];
1307        if let Some(rule) = calc_const_fold_rule(
1308            "constfold-add-number",
1309            "(+ ?a ?b)",
1310            CalcFoldOperator::Add,
1311            None,
1312        ) {
1313            rules.push(rule);
1314        }
1315        if let Some(unit_var) = egg_var("?u")
1316            && let Some(rule) = calc_const_fold_rule(
1317                "constfold-add-same-unit",
1318                "(+ (unit ?a ?u) (unit ?b ?u))",
1319                CalcFoldOperator::Add,
1320                Some(unit_var),
1321            )
1322        {
1323            rules.push(rule);
1324        }
1325        if let Some(rule) = calc_const_fold_rule(
1326            "constfold-sub-number",
1327            "(- ?a ?b)",
1328            CalcFoldOperator::Sub,
1329            None,
1330        ) {
1331            rules.push(rule);
1332        }
1333        if let Some(unit_var) = egg_var("?u")
1334            && let Some(rule) = calc_const_fold_rule(
1335                "constfold-sub-same-unit",
1336                "(- (unit ?a ?u) (unit ?b ?u))",
1337                CalcFoldOperator::Sub,
1338                Some(unit_var),
1339            )
1340        {
1341            rules.push(rule);
1342        }
1343        return Some(rules);
1344    }
1345    if pass_id == TransformPassKind::ShorthandCombining.id() {
1346        return Some(vec![
1347            egg_rewrite!("box4-all-equal"; "(box4 ?a ?a ?a ?a)" => "(box1 ?a)"),
1348            egg_rewrite!("box4-vertical-horizontal"; "(box4 ?a ?b ?a ?b)" => "(box2 ?a ?b)"),
1349            egg_rewrite!("box4-horizontal-pair"; "(box4 ?a ?b ?c ?b)" => "(box3 ?a ?b ?c)"),
1350        ]);
1351    }
1352    if pass_id == TransformPassKind::StalePrefixRemoval.id() {
1353        return Some(vec![
1354            egg_rewrite!("stale-prefix-exact-peer"; "(stale-prefix-decl ?p ?u ?v ?i)" => "(decl ?u ?v ?i)"),
1355        ]);
1356    }
1357    None
1358}
1359
1360#[cfg(feature = "transform-catalog-saturation")]
1361fn blocked_execution(
1362    candidate: EggRewriteCandidateV0,
1363    blocked_reason: Option<&'static str>,
1364) -> EggRewriteExecutionV0 {
1365    blocked_execution_parts(
1366        candidate.pass_id,
1367        candidate.before,
1368        candidate.after,
1369        blocked_reason,
1370    )
1371}
1372
1373fn blocked_execution_parts(
1374    pass_id: &'static str,
1375    before: String,
1376    expected_after: String,
1377    blocked_reason: Option<&'static str>,
1378) -> EggRewriteExecutionV0 {
1379    EggRewriteExecutionV0 {
1380        schema_version: "0",
1381        product: "omena-transform-egg.execution",
1382        pass_id,
1383        accepted: false,
1384        blocked_reason,
1385        before: before.clone(),
1386        after: before,
1387        expected_after,
1388        after_matches_candidate: false,
1389        engine: "egg",
1390        iteration_limit: 0,
1391        iteration_count: 0,
1392        eclass_count: 0,
1393        enode_count: 0,
1394        mdl_bits: None,
1395        mdl_residual_bits: None,
1396        mdl_unit: None,
1397    }
1398}
1399
1400#[cfg(test)]
1401mod tests {
1402    use super::*;
1403    use omena_evidence_graph::ObligationFamilyIdV0;
1404    use omena_parser::StyleDialect;
1405    use omena_transform_cst::TransformPassKind;
1406
1407    #[test]
1408    fn exposes_selector_calc_and_shorthand_optional_egg_boundary() {
1409        let boundary = summarize_omena_transform_egg_boundary();
1410
1411        assert_eq!(boundary.product, "omena-transform-egg.boundary");
1412        assert_eq!(
1413            boundary.managed_pass_ids,
1414            vec![
1415                "selector-is-where-compression",
1416                "calc-reduction",
1417                "shorthand-combining",
1418                "stale-prefix-removal"
1419            ]
1420        );
1421        assert_eq!(boundary.proof_obligations.len(), 6);
1422    }
1423
1424    #[test]
1425    fn mdl_extraction_default_preserves_ast_size() {
1426        let summary = summarize_mdl_extraction_mode();
1427
1428        assert_eq!(summary.schema_version, "0");
1429        assert_eq!(summary.product, "omena-transform-egg.mdl-extraction");
1430        assert!(summary.default_preserves_ast_size);
1431        assert_eq!(summary.layer_marker, "mdl-bits");
1432        assert_eq!(summary.unit, "bit");
1433        assert_eq!(summary.feature_gate, "mdl");
1434    }
1435
1436    #[test]
1437    fn plans_requested_egg_passes_through_transform_pass_planner() {
1438        let plan = plan_egg_rewrite_passes(true, true);
1439
1440        assert_eq!(
1441            plan.planned_pass_ids,
1442            vec!["selector-is-where-compression", "calc-reduction"]
1443        );
1444        assert_eq!(plan.pass_plan.violated_dag_edge_count, 0);
1445    }
1446
1447    #[test]
1448    fn plans_egg_passes_from_css_source() {
1449        let plan = plan_egg_rewrite_passes_for_source(".a:is(.ready) { width: calc(7 + 0); }");
1450
1451        assert_eq!(
1452            plan.planned_pass_ids,
1453            vec!["selector-is-where-compression", "calc-reduction"]
1454        );
1455        assert_eq!(plan.pass_plan.violated_dag_edge_count, 0);
1456    }
1457
1458    #[test]
1459    fn contextual_eqsat_scaffold_stays_no_egglog_binding() {
1460        let scaffold = summarize_contextual_eqsat_scaffold_v0();
1461
1462        assert_eq!(scaffold.schema_version, "0");
1463        assert_eq!(
1464            scaffold.product,
1465            "omena-transform-egg.contextual-eqsat-scaffold"
1466        );
1467        assert_eq!(scaffold.claim_level, "m6ScaffoldOnlyNoEgglogBinding");
1468        assert_eq!(scaffold.current_engine, "egg");
1469        assert!(scaffold.egg_engine_ready);
1470        assert!(!scaffold.egglog_binding_ready);
1471        assert!(!scaffold.external_datalog_host_ready);
1472        assert!(!scaffold.three_view_fusion_ready);
1473        assert!(!scaffold.theorem_claimed);
1474        assert!(!scaffold.public_safety_claim_ready);
1475        assert_eq!(
1476            scaffold.modal_witness_product,
1477            "omena-cascade.modal-check-witness"
1478        );
1479        assert_eq!(scaffold.modal_bridge_claim_level, "dependencyDeclaredOnly");
1480        assert_eq!(scaffold.paper_substrate_claim_level, "draftScaffoldOnly");
1481        assert_eq!(
1482            scaffold.managed_pass_ids,
1483            vec![
1484                "selector-is-where-compression",
1485                "calc-reduction",
1486                "shorthand-combining",
1487                "stale-prefix-removal"
1488            ]
1489        );
1490        assert!(
1491            scaffold
1492                .supported_claims
1493                .contains(&"contextual equality-saturation scaffold for M6 positioning")
1494        );
1495        assert!(scaffold.deferred_claims.contains(&"egglog Rust binding"));
1496        assert!(scaffold.deferred_claims.contains(&"full three-view fusion"));
1497    }
1498
1499    #[test]
1500    fn accepts_selector_rewrite_only_with_specificity_and_provenance_witnesses() {
1501        let decision = decide_egg_rewrite(EggRewriteCandidateV0 {
1502            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1503            before: ":is(.a, .b)".to_string(),
1504            after: ".a,.b".to_string(),
1505            proof: EggRewriteProofV0::new(
1506                true,
1507                ObligationFamilyIdV0::CascadeSafetyFloor,
1508                true,
1509                "specificity tuple preserved",
1510            ),
1511        });
1512
1513        assert!(decision.accepted);
1514        assert_eq!(decision.blocked_reason, None);
1515    }
1516
1517    #[test]
1518    fn rejects_calc_rewrite_without_computed_value_witness() {
1519        let decision = decide_egg_rewrite(EggRewriteCandidateV0 {
1520            pass_id: TransformPassKind::CalcReduction.id(),
1521            before: "calc(1rem + 2px)".to_string(),
1522            after: "1rem".to_string(),
1523            proof: EggRewriteProofV0::new(
1524                false,
1525                ObligationFamilyIdV0::CascadeSafetyFloor,
1526                true,
1527                "candidate generated",
1528            ),
1529        });
1530
1531        assert!(!decision.accepted);
1532        assert_eq!(
1533            decision.blocked_reason,
1534            Some("calc rewrite does not preserve computed value")
1535        );
1536    }
1537
1538    #[test]
1539    fn rejects_shorthand_rewrite_without_computed_value_witness() {
1540        let decision = decide_egg_rewrite(EggRewriteCandidateV0 {
1541            pass_id: TransformPassKind::ShorthandCombining.id(),
1542            before: "(box4 0 0 0 0)".to_string(),
1543            after: "(box1 0)".to_string(),
1544            proof: EggRewriteProofV0::new(
1545                false,
1546                ObligationFamilyIdV0::CascadeSafetyFloor,
1547                true,
1548                "candidate generated",
1549            ),
1550        });
1551
1552        assert!(!decision.accepted);
1553        assert_eq!(
1554            decision.blocked_reason,
1555            Some("shorthand rewrite does not preserve computed value")
1556        );
1557    }
1558
1559    #[test]
1560    fn egg_rewrite_family_derivation_preserves_legacy_json_contract()
1561    -> Result<(), serde_json::Error> {
1562        for (family, expected_preserved, witness) in [
1563            (
1564                ObligationFamilyIdV0::CascadeSafetyFloor,
1565                false,
1566                "candidate generated",
1567            ),
1568            (
1569                ObligationFamilyIdV0::ComputedValuePreservation,
1570                true,
1571                "computed value preserved",
1572            ),
1573        ] {
1574            let proof = EggRewriteProofV0::new(true, family, false, witness);
1575            let json = serde_json::to_value(&proof)?;
1576
1577            assert_eq!(
1578                json,
1579                serde_json::json!({
1580                    "specificityPreserved": true,
1581                    "computedValuePreserved": expected_preserved,
1582                    "provenancePreserved": false,
1583                    "cascadeSafeWitness": witness,
1584                })
1585            );
1586            assert!(json.get("obligationFamily").is_none());
1587            assert_eq!(proof.obligation_family(), family);
1588        }
1589
1590        Ok(())
1591    }
1592
1593    #[test]
1594    fn checked_selector_certificate_preserves_execution_bytes() -> Result<(), serde_json::Error> {
1595        let before = "(is (list ready ready))";
1596        let after = "ready";
1597        let token = selector_rewrite_issuance_token_v0(before, after);
1598        assert!(token.is_some(), "fixture certificate must issue a token");
1599        let Some(token) = token else {
1600            return Ok(());
1601        };
1602        let checked = execute_checked_egg_rewrite(CheckedEggRewriteCandidateV0 {
1603            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1604            before: before.to_owned(),
1605            after: after.to_owned(),
1606            proof: CheckedEggRewriteProofV0::new(
1607                EggRewriteClaimEvidenceV0::derivability_only(token.clone()),
1608                ObligationFamilyIdV0::CascadeSafetyFloor,
1609                declared_provenance_gap_v0(),
1610                EggRewriteClaimEvidenceV0::derivability_only(token),
1611            ),
1612        });
1613        let legacy = execute_egg_rewrite(EggRewriteCandidateV0 {
1614            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1615            before: before.to_owned(),
1616            after: after.to_owned(),
1617            proof: EggRewriteProofV0::new(
1618                true,
1619                ObligationFamilyIdV0::CascadeSafetyFloor,
1620                true,
1621                "duplicate :is() argument keeps specificity",
1622            ),
1623        });
1624
1625        assert!(checked.accepted);
1626        assert_eq!(serde_json::to_vec(&checked)?, serde_json::to_vec(&legacy)?);
1627        Ok(())
1628    }
1629
1630    #[test]
1631    fn checked_selector_rejects_token_for_different_endpoints() {
1632        let token = selector_rewrite_issuance_token_v0("(is ready)", "ready");
1633        assert!(token.is_some(), "fixture certificate must issue a token");
1634        let Some(token) = token else {
1635            return;
1636        };
1637        let decision = decide_checked_egg_rewrite(&CheckedEggRewriteCandidateV0 {
1638            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1639            before: "(is other)".to_owned(),
1640            after: "other".to_owned(),
1641            proof: CheckedEggRewriteProofV0::new(
1642                EggRewriteClaimEvidenceV0::derivability_only(token.clone()),
1643                ObligationFamilyIdV0::CascadeSafetyFloor,
1644                declared_provenance_gap_v0(),
1645                EggRewriteClaimEvidenceV0::derivability_only(token),
1646            ),
1647        });
1648
1649        assert!(!decision.accepted);
1650        assert_eq!(
1651            decision.blocked_reason,
1652            Some("rewrite certificate token does not match candidate endpoints")
1653        );
1654    }
1655
1656    #[test]
1657    fn checked_selector_rejects_token_issued_by_spoofed_catalog() {
1658        let before = RewriteTermV0::apply("selectorIs", vec![RewriteTermV0::atom("ready")]);
1659        let after = RewriteTermV0::atom("ready");
1660        let spoofed_catalog = omena_cascade_proof::RewriteRuleCatalogV0 {
1661            schema_version: omena_cascade_proof::REWRITE_RULE_CATALOG_SCHEMA_VERSION_V0.to_owned(),
1662            operators: vec![omena_cascade_proof::RewriteOperatorV0 {
1663                operator: "selectorIs".to_owned(),
1664                arity: 1,
1665            }],
1666            rules: vec![omena_cascade_proof::RewriteRuleV0 {
1667                rule_id: "selector-is-single-v0".to_owned(),
1668                before_pattern: omena_cascade_proof::RewritePatternV0::variable("anything"),
1669                after_pattern: omena_cascade_proof::RewritePatternV0::variable("whatever"),
1670                side_condition_kind:
1671                    omena_cascade_proof::RewriteSideConditionKindV0::NoSideCondition,
1672            }],
1673        };
1674        let certificate = RewriteCertificateEnvelopeV0 {
1675            schema_version: REWRITE_CERTIFICATE_SCHEMA_VERSION_V0.to_owned(),
1676            max_depth: 1,
1677            max_nodes: 1,
1678            certificate: RewriteCertificateV0::Rewrite {
1679                rule_id: "selector-is-single-v0".to_owned(),
1680                substitution: vec![
1681                    RewriteSubstitutionEntryV0 {
1682                        variable: "anything".to_owned(),
1683                        term: before,
1684                    },
1685                    RewriteSubstitutionEntryV0 {
1686                        variable: "whatever".to_owned(),
1687                        term: after,
1688                    },
1689                ],
1690                side_condition: SideConditionCertV0::NoSideCondition,
1691            },
1692        };
1693        let token = check_rewrite_certificate_v0(
1694            &RewriteTermV0::apply("selectorIs", vec![RewriteTermV0::atom("ready")]),
1695            &RewriteTermV0::atom("ready"),
1696            &spoofed_catalog,
1697            &certificate,
1698        );
1699        assert!(
1700            token.is_ok(),
1701            "spoof fixture must reach the consumer: {token:?}"
1702        );
1703        let Ok(token) = token else {
1704            return;
1705        };
1706
1707        let decision = decide_checked_egg_rewrite(&CheckedEggRewriteCandidateV0 {
1708            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1709            before: "(is ready)".to_owned(),
1710            after: "ready".to_owned(),
1711            proof: CheckedEggRewriteProofV0::new(
1712                EggRewriteClaimEvidenceV0::independently_checked(token.clone()),
1713                ObligationFamilyIdV0::CascadeSafetyFloor,
1714                declared_provenance_gap_v0(),
1715                EggRewriteClaimEvidenceV0::independently_checked(token),
1716            ),
1717        });
1718
1719        assert!(
1720            !decision.accepted,
1721            "spoofed catalog token reached admission"
1722        );
1723        assert_eq!(
1724            decision.blocked_reason,
1725            Some("rewrite certificate token does not match the trusted rule catalog")
1726        );
1727    }
1728
1729    #[test]
1730    fn favourable_legacy_booleans_cannot_replace_checked_selector_token() {
1731        let decision = decide_checked_egg_rewrite(&CheckedEggRewriteCandidateV0 {
1732            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1733            before: "(is ready)".to_owned(),
1734            after: "ready".to_owned(),
1735            proof: CheckedEggRewriteProofV0::new(
1736                declared_specificity_gap_v0(),
1737                ObligationFamilyIdV0::CascadeSafetyFloor,
1738                declared_provenance_gap_v0(),
1739                declared_cascade_safety_gap_v0(
1740                    "legacy caller would have supplied true/true/non-empty",
1741                ),
1742            ),
1743        });
1744
1745        assert!(!decision.accepted);
1746        assert_eq!(
1747            decision.blocked_reason,
1748            Some("selector rewrite requires a checker-issued derivability token for specificity")
1749        );
1750    }
1751
1752    #[test]
1753    fn executes_selector_rewrite_through_egg_engine() {
1754        let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1755            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1756            before: "(is buttonPrimary)".to_string(),
1757            after: "buttonPrimary".to_string(),
1758            proof: EggRewriteProofV0::new(
1759                true,
1760                ObligationFamilyIdV0::CascadeSafetyFloor,
1761                true,
1762                "single :is() argument keeps specificity",
1763            ),
1764        });
1765
1766        assert!(execution.accepted);
1767        assert_eq!(execution.product, "omena-transform-egg.execution");
1768        assert_eq!(execution.engine, "egg");
1769        assert_eq!(execution.after, "buttonPrimary");
1770        assert_eq!(execution.iteration_limit, 8);
1771        assert!(execution.iteration_count > 0);
1772        assert!(execution.eclass_count > 0);
1773        assert!(execution.enode_count > 0);
1774    }
1775
1776    #[test]
1777    fn executes_selector_dedup_rewrites_through_egg_engine() {
1778        let is_execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1779            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1780            before: "(is (list ready ready))".to_string(),
1781            after: "ready".to_string(),
1782            proof: EggRewriteProofV0::new(
1783                true,
1784                ObligationFamilyIdV0::CascadeSafetyFloor,
1785                true,
1786                "duplicate :is() argument keeps specificity",
1787            ),
1788        });
1789        let where_execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1790            pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1791            before: "(where (list ready ready))".to_string(),
1792            after: "(where ready)".to_string(),
1793            proof: EggRewriteProofV0::new(
1794                true,
1795                ObligationFamilyIdV0::CascadeSafetyFloor,
1796                true,
1797                "duplicate :where() argument keeps zero specificity",
1798            ),
1799        });
1800
1801        assert!(is_execution.accepted);
1802        assert_eq!(is_execution.after, "ready");
1803        assert!(where_execution.accepted);
1804        assert_eq!(where_execution.after, "(where ready)");
1805    }
1806
1807    #[test]
1808    fn executes_calc_rewrite_through_egg_engine() {
1809        let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1810            pass_id: TransformPassKind::CalcReduction.id(),
1811            before: "(calc (+ width 0))".to_string(),
1812            after: "width".to_string(),
1813            proof: EggRewriteProofV0::new(
1814                false,
1815                ObligationFamilyIdV0::ComputedValuePreservation,
1816                true,
1817                "additive identity preserves computed value",
1818            ),
1819        });
1820
1821        assert!(execution.accepted);
1822        assert_eq!(execution.after, "width");
1823        assert!(execution.after_matches_candidate);
1824    }
1825
1826    #[test]
1827    fn executes_extended_calc_identity_rewrites_through_egg_engine() {
1828        for (before, after) in [
1829            ("(calc (- width 0))", "width"),
1830            ("(calc (/ width 1))", "width"),
1831            ("(calc (* width 0))", "0"),
1832            ("(calc (- width width))", "0"),
1833        ] {
1834            let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1835                pass_id: TransformPassKind::CalcReduction.id(),
1836                before: before.to_string(),
1837                after: after.to_string(),
1838                proof: EggRewriteProofV0::new(
1839                    false,
1840                    ObligationFamilyIdV0::ComputedValuePreservation,
1841                    true,
1842                    "calc algebra identity preserves computed value",
1843                ),
1844            });
1845
1846            assert!(execution.accepted, "{before} -> {after}");
1847            assert_eq!(execution.after, after);
1848        }
1849    }
1850
1851    #[test]
1852    fn executes_same_unit_calc_const_folding_through_egg_engine() {
1853        for (before, after) in [
1854            ("(calc (+ (unit 1 px) (unit 2 px)))", "(unit 3 px)"),
1855            ("(calc (- (unit 10 rem) (unit 2 rem)))", "(unit 8 rem)"),
1856            ("(calc (+ 1 2))", "3"),
1857        ] {
1858            let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1859                pass_id: TransformPassKind::CalcReduction.id(),
1860                before: before.to_string(),
1861                after: after.to_string(),
1862                proof: EggRewriteProofV0::new(
1863                    false,
1864                    ObligationFamilyIdV0::ComputedValuePreservation,
1865                    true,
1866                    "same-unit calc arithmetic preserves computed value",
1867                ),
1868            });
1869
1870            assert!(execution.accepted, "{before} -> {after}");
1871            assert_eq!(execution.after, after);
1872        }
1873    }
1874
1875    #[test]
1876    fn executes_box_shorthand_rewrites_through_egg_engine() {
1877        for (before, after) in [
1878            ("(box4 0 0 0 0)", "(box1 0)"),
1879            ("(box4 1 2 1 2)", "(box2 1 2)"),
1880            ("(box4 1 2 3 2)", "(box3 1 2 3)"),
1881        ] {
1882            let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1883                pass_id: TransformPassKind::ShorthandCombining.id(),
1884                before: before.to_string(),
1885                after: after.to_string(),
1886                proof: EggRewriteProofV0::new(
1887                    false,
1888                    ObligationFamilyIdV0::ComputedValuePreservation,
1889                    true,
1890                    "box shorthand expansion preserves computed value",
1891                ),
1892            });
1893
1894            assert!(execution.accepted, "{before} -> {after}");
1895            assert_eq!(execution.after, after);
1896        }
1897    }
1898
1899    #[test]
1900    fn exposes_shorthand_rewrite_rules_for_managed_pass() {
1901        let rules = rewrite_rules_for_pass::<()>(TransformPassKind::ShorthandCombining.id());
1902
1903        assert!(rules.is_some_and(|rules| rules.len() == 3));
1904    }
1905
1906    #[test]
1907    fn executes_css_source_witnesses_through_egg_engine() {
1908        let source = ".a:is(.ready) { width: calc(1px + 2px); } .b:is(.x, .x) { color: red; } .c:where(.y, .y) { color: blue; }";
1909        let transformed =
1910            ".a.ready { width: 3px; } .b.x { color: red; } .c:where(.y) { color: blue; }";
1911        let plan = plan_egg_rewrite_passes_for_source(source);
1912        let witnesses = execute_egg_rewrite_witnesses_for_css_source(
1913            source,
1914            StyleDialect::Css,
1915            transformed,
1916            &plan.planned_pass_ids,
1917        );
1918
1919        assert_eq!(witnesses.len(), 4);
1920        assert!(witnesses.iter().all(|witness| witness.execution.accepted));
1921        assert!(
1922            witnesses
1923                .iter()
1924                .any(|witness| witness.pass_id == "selector-is-where-compression")
1925        );
1926        assert!(
1927            witnesses
1928                .iter()
1929                .any(|witness| witness.pass_id == "calc-reduction")
1930        );
1931        assert!(witnesses.iter().any(|witness| {
1932            witness.source_kind == "selectorIsDedup" && witness.css_after == ".x"
1933        }));
1934        assert!(witnesses.iter().any(|witness| {
1935            witness.source_kind == "selectorWhereDedup" && witness.css_after == ":where(.y)"
1936        }));
1937        assert!(witnesses.iter().any(|witness| {
1938            witness.source_kind == "calcSameUnitAdd"
1939                && witness.css_after == "3px"
1940                && witness.execution.after == "(unit 3 px)"
1941        }));
1942    }
1943
1944    #[test]
1945    fn executes_stale_prefix_removal_source_witness_through_egg_engine() {
1946        let source = ".a { -webkit-user-select: none; user-select: none; }";
1947        let transformed = ".a {  user-select: none; }";
1948        let witnesses = execute_egg_rewrite_witnesses_for_css_source(
1949            source,
1950            StyleDialect::Css,
1951            transformed,
1952            &[TransformPassKind::StalePrefixRemoval.id()],
1953        );
1954
1955        assert_eq!(witnesses.len(), 1);
1956        let witness = &witnesses[0];
1957        assert_eq!(witness.pass_id, "stale-prefix-removal");
1958        assert_eq!(witness.source_kind, "stalePrefixExactPeer");
1959        assert_eq!(witness.css_before, "-webkit-user-select: none;");
1960        assert_eq!(witness.css_after, "user-select: none;");
1961        assert!(witness.execution.accepted);
1962        assert_eq!(witness.execution.engine, "egg");
1963        assert_eq!(witness.execution.after, witness.execution.expected_after);
1964    }
1965
1966    #[test]
1967    fn mdl_default_ast_size_matches_100_fixture_differential_corpus() {
1968        let selector_cases = (0..50).map(|index| {
1969            (
1970                TransformPassKind::SelectorIsWhereCompression.id(),
1971                format!("(is token{index})"),
1972                format!("token{index}"),
1973                true,
1974                false,
1975                "single :is() argument keeps specificity",
1976            )
1977        });
1978        let calc_cases = (0..50).map(|index| {
1979            let left = index + 1;
1980            let right = 50 - index;
1981            (
1982                TransformPassKind::CalcReduction.id(),
1983                format!("(calc (+ (unit {left} px) (unit {right} px)))"),
1984                format!("(unit {} px)", left + right),
1985                false,
1986                true,
1987                "same-unit calc arithmetic preserves computed value",
1988            )
1989        });
1990        let cases = selector_cases.chain(calc_cases).collect::<Vec<_>>();
1991
1992        assert_eq!(cases.len(), 100);
1993        for (
1994            pass_id,
1995            before,
1996            expected_after,
1997            specificity_preserved,
1998            computed_value_preserved,
1999            witness,
2000        ) in cases
2001        {
2002            let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
2003                pass_id,
2004                before: before.clone(),
2005                after: expected_after.clone(),
2006                proof: EggRewriteProofV0::new(
2007                    specificity_preserved,
2008                    ObligationFamilyIdV0::from_computed_value_preservation(
2009                        computed_value_preserved,
2010                    ),
2011                    true,
2012                    witness,
2013                ),
2014            });
2015
2016            assert!(execution.accepted, "{before} -> {expected_after}");
2017            assert_eq!(execution.after, expected_after);
2018            assert!(execution.after_matches_candidate);
2019            assert_eq!(execution.mdl_bits, None);
2020            assert_eq!(execution.mdl_unit, None);
2021        }
2022    }
2023}