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