1use egg::{
8 Analysis, Applier, EGraph, Extractor, Id, Pattern, PatternAst, RecExpr, Rewrite, Runner, Subst,
9 Symbol, Var, define_language, rewrite as egg_rewrite,
10};
11use omena_transform_cst::TransformPassKind;
12use omena_transform_passes::{TransformPassPlanV0, plan_transform_passes};
13use serde::Serialize;
14
15mod mdl_cost;
16pub use mdl_cost::*;
17#[cfg(feature = "lawvere-saturation")]
18mod lawvere_analysis;
19#[cfg(feature = "lawvere-saturation")]
20pub use lawvere_analysis::*;
21
22define_language! {
23 enum CssRewriteLanguage {
24 Num(i64),
25 Symbol(Symbol),
26 "+" = Add([Id; 2]),
27 "-" = Sub([Id; 2]),
28 "*" = Mul([Id; 2]),
29 "/" = Div([Id; 2]),
30 "calc" = Calc(Id),
31 "unit" = Unit([Id; 2]),
32 "is" = Is(Id),
33 "where" = Where(Id),
34 "list" = List([Id; 2]),
35 }
36}
37
38#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
39#[serde(rename_all = "camelCase")]
40pub struct EggRewriteProofV0 {
41 pub specificity_preserved: bool,
42 pub computed_value_preserved: bool,
43 pub provenance_preserved: bool,
44 pub cascade_safe_witness: String,
45}
46
47#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
48#[serde(rename_all = "camelCase")]
49pub struct EggRewriteCandidateV0 {
50 pub pass_id: &'static str,
51 pub before: String,
52 pub after: String,
53 pub proof: EggRewriteProofV0,
54}
55
56#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
57#[serde(rename_all = "camelCase")]
58pub struct EggRewriteDecisionV0 {
59 pub schema_version: &'static str,
60 pub product: &'static str,
61 pub pass_id: &'static str,
62 pub accepted: bool,
63 pub blocked_reason: Option<&'static str>,
64}
65
66#[derive(Debug, Clone, PartialEq, Serialize)]
67#[serde(rename_all = "camelCase")]
68pub struct EggRewriteExecutionV0 {
69 pub schema_version: &'static str,
70 pub product: &'static str,
71 pub pass_id: &'static str,
72 pub accepted: bool,
73 pub blocked_reason: Option<&'static str>,
74 pub before: String,
75 pub after: String,
76 pub expected_after: String,
77 pub after_matches_candidate: bool,
78 pub engine: &'static str,
79 pub iteration_limit: usize,
80 pub iteration_count: usize,
81 pub eclass_count: usize,
82 pub enode_count: usize,
83 #[serde(skip_serializing_if = "Option::is_none")]
84 pub mdl_bits: Option<f64>,
85 #[serde(skip_serializing_if = "Option::is_none")]
86 pub mdl_residual_bits: Option<f64>,
87 #[serde(skip_serializing_if = "Option::is_none")]
88 pub mdl_unit: Option<&'static str>,
89}
90
91#[derive(Debug, Clone, PartialEq, Serialize)]
92#[serde(rename_all = "camelCase")]
93pub struct EggRewriteSourceWitnessV0 {
94 pub pass_id: &'static str,
95 pub source_kind: &'static str,
96 pub byte_offset: usize,
97 pub css_before: String,
98 pub css_after: String,
99 pub execution: EggRewriteExecutionV0,
100}
101
102#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
103#[serde(rename_all = "camelCase")]
104pub struct TransformEggBoundarySummaryV0 {
105 pub schema_version: &'static str,
106 pub product: &'static str,
107 pub managed_pass_ids: Vec<&'static str>,
108 pub optional_engine: &'static str,
109 pub proof_obligations: Vec<&'static str>,
110 pub planner_surface: &'static str,
111}
112
113#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
114#[serde(rename_all = "camelCase")]
115pub struct TransformEggPlanV0 {
116 pub schema_version: &'static str,
117 pub product: &'static str,
118 pub requested_pass_ids: Vec<&'static str>,
119 pub planned_pass_ids: Vec<&'static str>,
120 pub pass_plan: TransformPassPlanV0,
121}
122
123#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
124#[serde(rename_all = "camelCase")]
125pub struct ContextualEqSatScaffoldV0 {
126 pub schema_version: &'static str,
127 pub product: &'static str,
128 pub claim_level: &'static str,
129 pub scaffold_kind: &'static str,
130 pub execution_view: &'static str,
131 pub current_engine: &'static str,
132 pub egg_engine_ready: bool,
133 pub egglog_binding_ready: bool,
134 pub external_datalog_host_ready: bool,
135 pub three_view_fusion_ready: bool,
136 pub theorem_claimed: bool,
137 pub public_safety_claim_ready: bool,
138 pub modal_witness_product: &'static str,
139 pub modal_bridge_claim_level: &'static str,
140 pub paper_substrate_claim_level: &'static str,
141 pub managed_pass_ids: Vec<&'static str>,
142 pub substrate_products: Vec<&'static str>,
143 pub supported_claims: Vec<&'static str>,
144 pub deferred_claims: Vec<&'static str>,
145}
146
147#[derive(Debug, Clone, Copy)]
148enum CalcFoldOperator {
149 Add,
150 Sub,
151}
152
153#[derive(Debug, Clone)]
154struct ConstFoldSameUnitApplier {
155 left_var: Var,
156 right_var: Var,
157 unit_var: Option<Var>,
158 operator: CalcFoldOperator,
159}
160
161impl ConstFoldSameUnitApplier {
162 fn new(operator: CalcFoldOperator, unit_var: Option<Var>) -> Option<Self> {
163 Some(Self {
164 left_var: "?a".parse().ok()?,
165 right_var: "?b".parse().ok()?,
166 unit_var,
167 operator,
168 })
169 }
170}
171
172impl<N> Applier<CssRewriteLanguage, N> for ConstFoldSameUnitApplier
173where
174 N: Analysis<CssRewriteLanguage>,
175{
176 fn apply_one(
177 &self,
178 egraph: &mut EGraph<CssRewriteLanguage, N>,
179 eclass: Id,
180 subst: &Subst,
181 _searcher_ast: Option<&PatternAst<CssRewriteLanguage>>,
182 _rule_name: Symbol,
183 ) -> Vec<Id> {
184 let Some(left) = numeric_value_from_eclass(egraph, subst[self.left_var]) else {
185 return Vec::new();
186 };
187 let Some(right) = numeric_value_from_eclass(egraph, subst[self.right_var]) else {
188 return Vec::new();
189 };
190 let value = match self.operator {
191 CalcFoldOperator::Add => left + right,
192 CalcFoldOperator::Sub => left - right,
193 };
194 let value_id = egraph.add(CssRewriteLanguage::Num(value));
195 let result_id = if let Some(unit_var) = self.unit_var {
196 egraph.add(CssRewriteLanguage::Unit([value_id, subst[unit_var]]))
197 } else {
198 value_id
199 };
200 egraph.union(eclass, result_id);
201 vec![eclass]
202 }
203
204 fn vars(&self) -> Vec<Var> {
205 let mut vars = vec![self.left_var, self.right_var];
206 if let Some(unit_var) = self.unit_var {
207 vars.push(unit_var);
208 }
209 vars
210 }
211}
212
213pub fn summarize_omena_transform_egg_boundary() -> TransformEggBoundarySummaryV0 {
214 TransformEggBoundarySummaryV0 {
215 schema_version: "0",
216 product: "omena-transform-egg.boundary",
217 managed_pass_ids: managed_egg_passes().iter().map(|pass| pass.id()).collect(),
218 optional_engine: "egg-compatible equality saturation engine",
219 proof_obligations: vec![
220 "selector rewrites preserve specificity",
221 "calc rewrites preserve computed value",
222 "all rewrites preserve provenance",
223 "all accepted rewrites carry a cascade-safe witness",
224 ],
225 planner_surface: "omena-transform-passes.plan",
226 }
227}
228
229pub fn plan_egg_rewrite_passes(include_selector: bool, include_calc: bool) -> TransformEggPlanV0 {
230 let mut requested_passes = Vec::new();
231 if include_selector {
232 requested_passes.push(TransformPassKind::SelectorIsWhereCompression);
233 }
234 if include_calc {
235 requested_passes.push(TransformPassKind::CalcReduction);
236 }
237 let pass_plan = plan_transform_passes(&requested_passes);
238
239 TransformEggPlanV0 {
240 schema_version: "0",
241 product: "omena-transform-egg.plan",
242 requested_pass_ids: requested_passes.iter().map(|pass| pass.id()).collect(),
243 planned_pass_ids: pass_plan.ordered_pass_ids.clone(),
244 pass_plan,
245 }
246}
247
248pub fn plan_egg_rewrite_passes_for_source(source: &str) -> TransformEggPlanV0 {
249 plan_egg_rewrite_passes(
250 source.contains(":is(") || source.contains(":where("),
251 source.contains("calc("),
252 )
253}
254
255pub fn summarize_contextual_eqsat_scaffold_v0() -> ContextualEqSatScaffoldV0 {
256 let boundary = summarize_omena_transform_egg_boundary();
257
258 ContextualEqSatScaffoldV0 {
259 schema_version: "0",
260 product: "omena-transform-egg.contextual-eqsat-scaffold",
261 claim_level: "m6ScaffoldOnlyNoEgglogBinding",
262 scaffold_kind: "contextualEqualitySaturationExecutionView",
263 execution_view: "m6BridgeNodeExecutionView",
264 current_engine: "egg",
265 egg_engine_ready: true,
266 egglog_binding_ready: false,
267 external_datalog_host_ready: false,
268 three_view_fusion_ready: false,
269 theorem_claimed: false,
270 public_safety_claim_ready: false,
271 modal_witness_product: "omena-cascade.modal-check-witness",
272 modal_bridge_claim_level: "dependencyDeclaredOnly",
273 paper_substrate_claim_level: "draftScaffoldOnly",
274 managed_pass_ids: boundary.managed_pass_ids,
275 substrate_products: vec![
276 "omena-transform-egg.boundary",
277 "omena-transform-egg.plan",
278 "omena-transform-egg.execution",
279 "omena-cascade.modal-check-witness",
280 ],
281 supported_claims: vec![
282 "optional egg equality-saturation rewrite boundary",
283 "selector and calc rewrite proof obligations",
284 "contextual equality-saturation scaffold for M6 positioning",
285 "modal witness dependency declaration for #66/#73 paper substrate",
286 ],
287 deferred_claims: vec![
288 "egglog Rust binding",
289 "external Datalog host execution",
290 "full three-view fusion",
291 "Contextual EqSat theorem",
292 "production research-tier execution view",
293 ],
294 }
295}
296
297pub fn decide_egg_rewrite(candidate: EggRewriteCandidateV0) -> EggRewriteDecisionV0 {
298 let blocked_reason = if !is_managed_egg_pass_id(candidate.pass_id) {
299 Some("pass is not managed by omena-transform-egg")
300 } else if candidate.proof.cascade_safe_witness.is_empty() {
301 Some("missing cascade-safe witness")
302 } else if !candidate.proof.provenance_preserved {
303 Some("rewrite does not preserve provenance")
304 } else if candidate.pass_id == TransformPassKind::SelectorIsWhereCompression.id()
305 && !candidate.proof.specificity_preserved
306 {
307 Some("selector rewrite does not preserve specificity")
308 } else if candidate.pass_id == TransformPassKind::CalcReduction.id()
309 && !candidate.proof.computed_value_preserved
310 {
311 Some("calc rewrite does not preserve computed value")
312 } else {
313 None
314 };
315
316 EggRewriteDecisionV0 {
317 schema_version: "0",
318 product: "omena-transform-egg.decision",
319 pass_id: candidate.pass_id,
320 accepted: blocked_reason.is_none(),
321 blocked_reason,
322 }
323}
324
325pub fn execute_egg_rewrite(candidate: EggRewriteCandidateV0) -> EggRewriteExecutionV0 {
326 let decision = decide_egg_rewrite(candidate.clone());
327 if !decision.accepted {
328 return blocked_execution(candidate, decision.blocked_reason);
329 }
330
331 let expression = match candidate.before.parse::<RecExpr<CssRewriteLanguage>>() {
332 Ok(expression) => expression,
333 Err(_) => return blocked_execution(candidate, Some("rewrite expression could not parse")),
334 };
335 let Some(rules) = rewrite_rules_for_pass::<()>(candidate.pass_id) else {
336 return blocked_execution(
337 candidate,
338 Some("pass is not managed by omena-transform-egg"),
339 );
340 };
341
342 let iteration_limit = 8;
343 let runner = Runner::default()
344 .with_expr(&expression)
345 .with_iter_limit(iteration_limit)
346 .run(rules.as_slice());
347 let root = runner.roots[0];
348 let extractor = Extractor::new(&runner.egraph, MdlExtractionCostV0::default_ast_size());
349 let (_, extracted) = extractor.find_best(root);
350 let after = extracted.to_string();
351 let after_matches_candidate = after == candidate.after;
352
353 EggRewriteExecutionV0 {
354 schema_version: "0",
355 product: "omena-transform-egg.execution",
356 pass_id: candidate.pass_id,
357 accepted: after_matches_candidate,
358 blocked_reason: (!after_matches_candidate)
359 .then_some("egg extraction did not match candidate output"),
360 before: candidate.before,
361 after,
362 expected_after: candidate.after,
363 after_matches_candidate,
364 engine: "egg",
365 iteration_limit,
366 iteration_count: runner.iterations.len(),
367 eclass_count: runner.egraph.number_of_classes(),
368 enode_count: runner.egraph.total_size(),
369 mdl_bits: None,
370 mdl_residual_bits: None,
371 mdl_unit: None,
372 }
373}
374
375pub fn execute_egg_rewrite_witnesses_for_css_source(
376 source: &str,
377 transformed_source: &str,
378 planned_pass_ids: &[&'static str],
379) -> Vec<EggRewriteSourceWitnessV0> {
380 let mut witnesses = Vec::new();
381 if planned_pass_ids.contains(&TransformPassKind::SelectorIsWhereCompression.id()) {
382 witnesses.extend(selector_rewrite_witnesses(source, transformed_source));
383 }
384 if planned_pass_ids.contains(&TransformPassKind::CalcReduction.id()) {
385 witnesses.extend(calc_rewrite_witnesses(source, transformed_source));
386 }
387 witnesses
388}
389
390fn managed_egg_passes() -> [TransformPassKind; 2] {
391 [
392 TransformPassKind::SelectorIsWhereCompression,
393 TransformPassKind::CalcReduction,
394 ]
395}
396
397fn is_managed_egg_pass_id(pass_id: &str) -> bool {
398 managed_egg_passes().iter().any(|pass| pass.id() == pass_id)
399}
400
401fn numeric_value_from_eclass<N>(egraph: &EGraph<CssRewriteLanguage, N>, id: Id) -> Option<i64>
402where
403 N: Analysis<CssRewriteLanguage>,
404{
405 egraph[id].nodes.iter().find_map(|node| match node {
406 CssRewriteLanguage::Num(value) => Some(*value),
407 _ => None,
408 })
409}
410
411fn selector_rewrite_witnesses(
412 source: &str,
413 transformed_source: &str,
414) -> Vec<EggRewriteSourceWitnessV0> {
415 let mut witnesses = Vec::new();
416 for (prefix, source_kind) in [(":is(", "selectorIs"), (":where(", "selectorWhere")] {
417 let mut cursor = 0usize;
418 while let Some(relative_start) = source[cursor..].find(prefix) {
419 let start = cursor + relative_start;
420 let inner_start = start + prefix.len();
421 let Some(relative_end) = source[inner_start..].find(')') else {
422 break;
423 };
424 let end = inner_start + relative_end;
425 let inner = source[inner_start..end].trim();
426 let css_before = source[start..=end].to_string();
427 let pseudo_name = prefix.trim_start_matches(':').trim_end_matches('(');
428 if let Some((source_kind, css_after, before, after, witness)) =
429 selector_witness_candidate(pseudo_name, source_kind, inner)
430 && transformed_source.contains(&css_after)
431 && !transformed_source.contains(&css_before)
432 {
433 let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
434 pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
435 before,
436 after,
437 proof: EggRewriteProofV0 {
438 specificity_preserved: true,
439 computed_value_preserved: false,
440 provenance_preserved: true,
441 cascade_safe_witness: witness,
442 },
443 });
444 witnesses.push(EggRewriteSourceWitnessV0 {
445 pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
446 source_kind,
447 byte_offset: start,
448 css_before,
449 css_after,
450 execution,
451 });
452 }
453 cursor = end + 1;
454 }
455 }
456 witnesses
457}
458
459fn calc_rewrite_witnesses(
460 source: &str,
461 transformed_source: &str,
462) -> Vec<EggRewriteSourceWitnessV0> {
463 let mut witnesses = Vec::new();
464 let mut cursor = 0usize;
465 while let Some(relative_start) = source[cursor..].find("calc(") {
466 let start = cursor + relative_start;
467 let inner_start = start + "calc(".len();
468 let Some(relative_end) = source[inner_start..].find(')') else {
469 break;
470 };
471 let end = inner_start + relative_end;
472 let inner = source[inner_start..end].trim();
473 let css_before = source[start..=end].to_string();
474 if let Some(candidate) = calc_rewrite_candidate(inner)
475 && transformed_source.contains(candidate.css_after.as_str())
476 && !transformed_source.contains(&css_before)
477 {
478 let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
479 pass_id: TransformPassKind::CalcReduction.id(),
480 before: format!("(calc {})", candidate.before),
481 after: candidate.after,
482 proof: EggRewriteProofV0 {
483 specificity_preserved: false,
484 computed_value_preserved: true,
485 provenance_preserved: true,
486 cascade_safe_witness: candidate.witness,
487 },
488 });
489 witnesses.push(EggRewriteSourceWitnessV0 {
490 pass_id: TransformPassKind::CalcReduction.id(),
491 source_kind: candidate.source_kind,
492 byte_offset: start,
493 css_before,
494 css_after: candidate.css_after,
495 execution,
496 });
497 }
498 cursor = end + 1;
499 }
500 witnesses
501}
502
503fn selector_witness_candidate(
504 pseudo_name: &str,
505 source_kind: &'static str,
506 inner: &str,
507) -> Option<(&'static str, String, String, String, String)> {
508 if pseudo_name == "is"
509 && let Some((symbol, css_ident)) = selector_single_argument_parts(inner)
510 {
511 return Some((
512 source_kind,
513 format!(".{css_ident}"),
514 format!("(is {symbol})"),
515 symbol,
516 "actual CSS selectorIs single-argument rewrite".to_string(),
517 ));
518 }
519
520 let args = split_simple_selector_arguments(inner)?;
521 let [left, right] = args.as_slice() else {
522 return None;
523 };
524 if left != right {
525 return None;
526 }
527 let (symbol, css_ident) = selector_single_argument_parts(left)?;
528 match pseudo_name {
529 "is" => Some((
530 "selectorIsDedup",
531 format!(".{css_ident}"),
532 format!("(is (list {symbol} {symbol}))"),
533 symbol,
534 "actual CSS selectorIs duplicate-argument rewrite".to_string(),
535 )),
536 "where" => Some((
537 "selectorWhereDedup",
538 format!(":where(.{css_ident})"),
539 format!("(where (list {symbol} {symbol}))"),
540 format!("(where {symbol})"),
541 "actual CSS selectorWhere duplicate-argument rewrite".to_string(),
542 )),
543 _ => None,
544 }
545}
546
547fn split_simple_selector_arguments(inner: &str) -> Option<Vec<String>> {
548 let args = inner
549 .split(',')
550 .map(str::trim)
551 .map(str::to_string)
552 .collect::<Vec<_>>();
553 (!args.is_empty() && args.iter().all(|arg| !arg.is_empty())).then_some(args)
554}
555
556fn selector_single_argument_parts(inner: &str) -> Option<(String, String)> {
557 let class_name = inner.trim().strip_prefix('.')?;
558 if class_name.is_empty()
559 || !class_name
560 .chars()
561 .all(|ch| ch.is_ascii_alphanumeric() || matches!(ch, '_' | '-'))
562 {
563 return None;
564 }
565 Some((symbol_for_css_ident(class_name), class_name.to_string()))
566}
567
568fn symbol_for_css_ident(value: &str) -> String {
569 value.replace('-', "_")
570}
571
572#[derive(Debug, Clone, PartialEq, Eq)]
573struct CalcRewriteCandidate {
574 before: String,
575 after: String,
576 css_after: String,
577 source_kind: &'static str,
578 witness: String,
579}
580
581#[derive(Debug, Clone, PartialEq, Eq)]
582struct CalcNumericValue {
583 value: i64,
584 unit: String,
585}
586
587fn calc_rewrite_candidate(inner: &str) -> Option<CalcRewriteCandidate> {
588 let parts = inner.split_whitespace().collect::<Vec<_>>();
589 let [left, operator, right] = parts.as_slice() else {
590 return None;
591 };
592 let left_value = parse_calc_numeric_value(left)?;
593 let right_value = parse_calc_numeric_value(right)?;
594 if left_value.unit != right_value.unit {
595 return None;
596 }
597 let term_left = calc_numeric_term(&left_value);
598 let term_right = calc_numeric_term(&right_value);
599 match *operator {
600 "+" => Some(calc_fold_candidate(
601 format!("(+ {term_left} {term_right})"),
602 left_value.value + right_value.value,
603 &left_value.unit,
604 "calcSameUnitAdd",
605 "actual CSS calc same-unit addition rewrite",
606 )),
607 "-" => Some(calc_fold_candidate(
608 format!("(- {term_left} {term_right})"),
609 left_value.value - right_value.value,
610 &left_value.unit,
611 "calcSameUnitSub",
612 "actual CSS calc same-unit subtraction rewrite",
613 )),
614 "*" if right_value.value == 1 && right_value.unit.is_empty() => {
615 Some(calc_passthrough_candidate(
616 format!("(* {term_left} 1)"),
617 &left_value,
618 "calcIdentity",
619 "actual CSS calc multiplicative identity rewrite",
620 ))
621 }
622 "*" if left_value.value == 1 && left_value.unit.is_empty() => {
623 Some(calc_passthrough_candidate(
624 format!("(* 1 {term_right})"),
625 &right_value,
626 "calcIdentity",
627 "actual CSS calc multiplicative identity rewrite",
628 ))
629 }
630 "*" if right_value.value == 0 && right_value.unit.is_empty() => Some(calc_fold_candidate(
631 format!("(* {term_left} 0)"),
632 0,
633 "",
634 "calcZero",
635 "actual CSS calc safe zero multiplication rewrite",
636 )),
637 "*" if left_value.value == 0 && left_value.unit.is_empty() => Some(calc_fold_candidate(
638 format!("(* 0 {term_right})"),
639 0,
640 "",
641 "calcZero",
642 "actual CSS calc safe zero multiplication rewrite",
643 )),
644 "/" if right_value.value == 1 && right_value.unit.is_empty() => {
645 Some(calc_passthrough_candidate(
646 format!("(/ {term_left} 1)"),
647 &left_value,
648 "calcIdentity",
649 "actual CSS calc division identity rewrite",
650 ))
651 }
652 _ => None,
653 }
654}
655
656fn parse_calc_numeric_value(text: &str) -> Option<CalcNumericValue> {
657 let split = text
658 .char_indices()
659 .find_map(|(index, ch)| (!matches!(ch, '-' | '+') && !ch.is_ascii_digit()).then_some(index))
660 .unwrap_or(text.len());
661 let (value, unit) = text.split_at(split);
662 let value = value.parse::<i64>().ok()?;
663 unit.chars()
664 .all(|ch| ch.is_ascii_alphabetic() || ch == '%')
665 .then_some(CalcNumericValue {
666 value,
667 unit: unit.to_string(),
668 })
669}
670
671fn calc_numeric_term(value: &CalcNumericValue) -> String {
672 if value.unit.is_empty() {
673 value.value.to_string()
674 } else {
675 format!("(unit {} {})", value.value, value.unit)
676 }
677}
678
679fn calc_fold_candidate(
680 before: String,
681 value: i64,
682 unit: &str,
683 source_kind: &'static str,
684 witness: &'static str,
685) -> CalcRewriteCandidate {
686 let result = CalcNumericValue {
687 value,
688 unit: unit.to_string(),
689 };
690 CalcRewriteCandidate {
691 before,
692 after: calc_numeric_term(&result),
693 css_after: format!("{}{}", result.value, result.unit),
694 source_kind,
695 witness: witness.to_string(),
696 }
697}
698
699fn calc_passthrough_candidate(
700 before: String,
701 value: &CalcNumericValue,
702 source_kind: &'static str,
703 witness: &'static str,
704) -> CalcRewriteCandidate {
705 CalcRewriteCandidate {
706 before,
707 after: calc_numeric_term(value),
708 css_after: format!("{}{}", value.value, value.unit),
709 source_kind,
710 witness: witness.to_string(),
711 }
712}
713
714fn rewrite_pattern(text: &str) -> Option<Pattern<CssRewriteLanguage>> {
715 text.parse().ok()
716}
717
718pub(crate) fn calc_const_fold_rule<N>(
719 name: &'static str,
720 search: &'static str,
721 operator: CalcFoldOperator,
722 unit_var: Option<Var>,
723) -> Option<Rewrite<CssRewriteLanguage, N>>
724where
725 N: Analysis<CssRewriteLanguage>,
726{
727 Rewrite::new(
728 name,
729 rewrite_pattern(search)?,
730 ConstFoldSameUnitApplier::new(operator, unit_var)?,
731 )
732 .ok()
733}
734
735fn egg_var(name: &str) -> Option<Var> {
736 name.parse().ok()
737}
738
739pub(crate) fn rewrite_rules_for_pass<N>(
740 pass_id: &'static str,
741) -> Option<Vec<Rewrite<CssRewriteLanguage, N>>>
742where
743 N: Analysis<CssRewriteLanguage>,
744{
745 if pass_id == TransformPassKind::SelectorIsWhereCompression.id() {
746 return Some(vec![
747 egg_rewrite!("single-is-selector"; "(is ?a)" => "?a"),
748 egg_rewrite!("nested-is-selector"; "(is (is ?a))" => "?a"),
749 egg_rewrite!("duplicate-is-selector"; "(is (list ?a ?a))" => "?a"),
750 egg_rewrite!("duplicate-where-selector"; "(where (list ?a ?a))" => "(where ?a)"),
751 ]);
752 }
753 if pass_id == TransformPassKind::CalcReduction.id() {
754 let mut rules = vec![
755 egg_rewrite!("unwrap-calc"; "(calc ?a)" => "?a"),
756 egg_rewrite!("add-zero-right"; "(+ ?a 0)" => "?a"),
757 egg_rewrite!("add-zero-left"; "(+ 0 ?a)" => "?a"),
758 egg_rewrite!("sub-zero-right"; "(- ?a 0)" => "?a"),
759 egg_rewrite!("self-sub"; "(- ?a ?a)" => "0"),
760 egg_rewrite!("mul-one-right"; "(* ?a 1)" => "?a"),
761 egg_rewrite!("mul-one-left"; "(* 1 ?a)" => "?a"),
762 egg_rewrite!("mul-zero-right"; "(* ?a 0)" => "0"),
763 egg_rewrite!("mul-zero-left"; "(* 0 ?a)" => "0"),
764 egg_rewrite!("div-one-right"; "(/ ?a 1)" => "?a"),
765 ];
766 if let Some(rule) = calc_const_fold_rule(
767 "constfold-add-number",
768 "(+ ?a ?b)",
769 CalcFoldOperator::Add,
770 None,
771 ) {
772 rules.push(rule);
773 }
774 if let Some(unit_var) = egg_var("?u")
775 && let Some(rule) = calc_const_fold_rule(
776 "constfold-add-same-unit",
777 "(+ (unit ?a ?u) (unit ?b ?u))",
778 CalcFoldOperator::Add,
779 Some(unit_var),
780 )
781 {
782 rules.push(rule);
783 }
784 if let Some(rule) = calc_const_fold_rule(
785 "constfold-sub-number",
786 "(- ?a ?b)",
787 CalcFoldOperator::Sub,
788 None,
789 ) {
790 rules.push(rule);
791 }
792 if let Some(unit_var) = egg_var("?u")
793 && let Some(rule) = calc_const_fold_rule(
794 "constfold-sub-same-unit",
795 "(- (unit ?a ?u) (unit ?b ?u))",
796 CalcFoldOperator::Sub,
797 Some(unit_var),
798 )
799 {
800 rules.push(rule);
801 }
802 return Some(rules);
803 }
804 None
805}
806
807fn blocked_execution(
808 candidate: EggRewriteCandidateV0,
809 blocked_reason: Option<&'static str>,
810) -> EggRewriteExecutionV0 {
811 EggRewriteExecutionV0 {
812 schema_version: "0",
813 product: "omena-transform-egg.execution",
814 pass_id: candidate.pass_id,
815 accepted: false,
816 blocked_reason,
817 before: candidate.before.clone(),
818 after: candidate.before,
819 expected_after: candidate.after,
820 after_matches_candidate: false,
821 engine: "egg",
822 iteration_limit: 0,
823 iteration_count: 0,
824 eclass_count: 0,
825 enode_count: 0,
826 mdl_bits: None,
827 mdl_residual_bits: None,
828 mdl_unit: None,
829 }
830}
831
832#[cfg(test)]
833mod tests {
834 use super::{
835 EggRewriteCandidateV0, EggRewriteProofV0, decide_egg_rewrite, execute_egg_rewrite,
836 execute_egg_rewrite_witnesses_for_css_source, plan_egg_rewrite_passes,
837 plan_egg_rewrite_passes_for_source, summarize_contextual_eqsat_scaffold_v0,
838 summarize_mdl_extraction_mode, summarize_omena_transform_egg_boundary,
839 };
840 use omena_transform_cst::TransformPassKind;
841
842 #[test]
843 fn exposes_selector_and_calc_optional_egg_boundary() {
844 let boundary = summarize_omena_transform_egg_boundary();
845
846 assert_eq!(boundary.product, "omena-transform-egg.boundary");
847 assert_eq!(
848 boundary.managed_pass_ids,
849 vec!["selector-is-where-compression", "calc-reduction"]
850 );
851 assert_eq!(boundary.proof_obligations.len(), 4);
852 }
853
854 #[test]
855 fn mdl_extraction_default_preserves_ast_size() {
856 let summary = summarize_mdl_extraction_mode();
857
858 assert_eq!(summary.schema_version, "0");
859 assert_eq!(summary.product, "omena-transform-egg.mdl-extraction");
860 assert!(summary.default_preserves_ast_size);
861 assert_eq!(summary.layer_marker, "mdl-bits");
862 assert_eq!(summary.unit, "bit");
863 assert_eq!(summary.feature_gate, "mdl");
864 }
865
866 #[test]
867 fn plans_requested_egg_passes_through_transform_pass_planner() {
868 let plan = plan_egg_rewrite_passes(true, true);
869
870 assert_eq!(
871 plan.planned_pass_ids,
872 vec!["selector-is-where-compression", "calc-reduction"]
873 );
874 assert_eq!(plan.pass_plan.violated_dag_edge_count, 0);
875 }
876
877 #[test]
878 fn plans_egg_passes_from_css_source() {
879 let plan = plan_egg_rewrite_passes_for_source(".a:is(.ready) { width: calc(7 + 0); }");
880
881 assert_eq!(
882 plan.planned_pass_ids,
883 vec!["selector-is-where-compression", "calc-reduction"]
884 );
885 assert_eq!(plan.pass_plan.violated_dag_edge_count, 0);
886 }
887
888 #[test]
889 fn contextual_eqsat_scaffold_stays_no_egglog_binding() {
890 let scaffold = summarize_contextual_eqsat_scaffold_v0();
891
892 assert_eq!(scaffold.schema_version, "0");
893 assert_eq!(
894 scaffold.product,
895 "omena-transform-egg.contextual-eqsat-scaffold"
896 );
897 assert_eq!(scaffold.claim_level, "m6ScaffoldOnlyNoEgglogBinding");
898 assert_eq!(scaffold.current_engine, "egg");
899 assert!(scaffold.egg_engine_ready);
900 assert!(!scaffold.egglog_binding_ready);
901 assert!(!scaffold.external_datalog_host_ready);
902 assert!(!scaffold.three_view_fusion_ready);
903 assert!(!scaffold.theorem_claimed);
904 assert!(!scaffold.public_safety_claim_ready);
905 assert_eq!(
906 scaffold.modal_witness_product,
907 "omena-cascade.modal-check-witness"
908 );
909 assert_eq!(scaffold.modal_bridge_claim_level, "dependencyDeclaredOnly");
910 assert_eq!(scaffold.paper_substrate_claim_level, "draftScaffoldOnly");
911 assert_eq!(
912 scaffold.managed_pass_ids,
913 vec!["selector-is-where-compression", "calc-reduction"]
914 );
915 assert!(
916 scaffold
917 .supported_claims
918 .contains(&"contextual equality-saturation scaffold for M6 positioning")
919 );
920 assert!(scaffold.deferred_claims.contains(&"egglog Rust binding"));
921 assert!(scaffold.deferred_claims.contains(&"full three-view fusion"));
922 }
923
924 #[test]
925 fn accepts_selector_rewrite_only_with_specificity_and_provenance_witnesses() {
926 let decision = decide_egg_rewrite(EggRewriteCandidateV0 {
927 pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
928 before: ":is(.a, .b)".to_string(),
929 after: ".a,.b".to_string(),
930 proof: EggRewriteProofV0 {
931 specificity_preserved: true,
932 computed_value_preserved: false,
933 provenance_preserved: true,
934 cascade_safe_witness: "specificity tuple preserved".to_string(),
935 },
936 });
937
938 assert!(decision.accepted);
939 assert_eq!(decision.blocked_reason, None);
940 }
941
942 #[test]
943 fn rejects_calc_rewrite_without_computed_value_witness() {
944 let decision = decide_egg_rewrite(EggRewriteCandidateV0 {
945 pass_id: TransformPassKind::CalcReduction.id(),
946 before: "calc(1rem + 2px)".to_string(),
947 after: "1rem".to_string(),
948 proof: EggRewriteProofV0 {
949 specificity_preserved: false,
950 computed_value_preserved: false,
951 provenance_preserved: true,
952 cascade_safe_witness: "candidate generated".to_string(),
953 },
954 });
955
956 assert!(!decision.accepted);
957 assert_eq!(
958 decision.blocked_reason,
959 Some("calc rewrite does not preserve computed value")
960 );
961 }
962
963 #[test]
964 fn executes_selector_rewrite_through_egg_engine() {
965 let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
966 pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
967 before: "(is buttonPrimary)".to_string(),
968 after: "buttonPrimary".to_string(),
969 proof: EggRewriteProofV0 {
970 specificity_preserved: true,
971 computed_value_preserved: false,
972 provenance_preserved: true,
973 cascade_safe_witness: "single :is() argument keeps specificity".to_string(),
974 },
975 });
976
977 assert!(execution.accepted);
978 assert_eq!(execution.product, "omena-transform-egg.execution");
979 assert_eq!(execution.engine, "egg");
980 assert_eq!(execution.after, "buttonPrimary");
981 assert_eq!(execution.iteration_limit, 8);
982 assert!(execution.iteration_count > 0);
983 assert!(execution.eclass_count > 0);
984 assert!(execution.enode_count > 0);
985 }
986
987 #[test]
988 fn executes_selector_dedup_rewrites_through_egg_engine() {
989 let is_execution = execute_egg_rewrite(EggRewriteCandidateV0 {
990 pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
991 before: "(is (list ready ready))".to_string(),
992 after: "ready".to_string(),
993 proof: EggRewriteProofV0 {
994 specificity_preserved: true,
995 computed_value_preserved: false,
996 provenance_preserved: true,
997 cascade_safe_witness: "duplicate :is() argument keeps specificity".to_string(),
998 },
999 });
1000 let where_execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1001 pass_id: TransformPassKind::SelectorIsWhereCompression.id(),
1002 before: "(where (list ready ready))".to_string(),
1003 after: "(where ready)".to_string(),
1004 proof: EggRewriteProofV0 {
1005 specificity_preserved: true,
1006 computed_value_preserved: false,
1007 provenance_preserved: true,
1008 cascade_safe_witness: "duplicate :where() argument keeps zero specificity"
1009 .to_string(),
1010 },
1011 });
1012
1013 assert!(is_execution.accepted);
1014 assert_eq!(is_execution.after, "ready");
1015 assert!(where_execution.accepted);
1016 assert_eq!(where_execution.after, "(where ready)");
1017 }
1018
1019 #[test]
1020 fn executes_calc_rewrite_through_egg_engine() {
1021 let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1022 pass_id: TransformPassKind::CalcReduction.id(),
1023 before: "(calc (+ width 0))".to_string(),
1024 after: "width".to_string(),
1025 proof: EggRewriteProofV0 {
1026 specificity_preserved: false,
1027 computed_value_preserved: true,
1028 provenance_preserved: true,
1029 cascade_safe_witness: "additive identity preserves computed value".to_string(),
1030 },
1031 });
1032
1033 assert!(execution.accepted);
1034 assert_eq!(execution.after, "width");
1035 assert!(execution.after_matches_candidate);
1036 }
1037
1038 #[test]
1039 fn executes_extended_calc_identity_rewrites_through_egg_engine() {
1040 for (before, after) in [
1041 ("(calc (- width 0))", "width"),
1042 ("(calc (/ width 1))", "width"),
1043 ("(calc (* width 0))", "0"),
1044 ("(calc (- width width))", "0"),
1045 ] {
1046 let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1047 pass_id: TransformPassKind::CalcReduction.id(),
1048 before: before.to_string(),
1049 after: after.to_string(),
1050 proof: EggRewriteProofV0 {
1051 specificity_preserved: false,
1052 computed_value_preserved: true,
1053 provenance_preserved: true,
1054 cascade_safe_witness: "calc algebra identity preserves computed value"
1055 .to_string(),
1056 },
1057 });
1058
1059 assert!(execution.accepted, "{before} -> {after}");
1060 assert_eq!(execution.after, after);
1061 }
1062 }
1063
1064 #[test]
1065 fn executes_same_unit_calc_const_folding_through_egg_engine() {
1066 for (before, after) in [
1067 ("(calc (+ (unit 1 px) (unit 2 px)))", "(unit 3 px)"),
1068 ("(calc (- (unit 10 rem) (unit 2 rem)))", "(unit 8 rem)"),
1069 ("(calc (+ 1 2))", "3"),
1070 ] {
1071 let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1072 pass_id: TransformPassKind::CalcReduction.id(),
1073 before: before.to_string(),
1074 after: after.to_string(),
1075 proof: EggRewriteProofV0 {
1076 specificity_preserved: false,
1077 computed_value_preserved: true,
1078 provenance_preserved: true,
1079 cascade_safe_witness: "same-unit calc arithmetic preserves computed value"
1080 .to_string(),
1081 },
1082 });
1083
1084 assert!(execution.accepted, "{before} -> {after}");
1085 assert_eq!(execution.after, after);
1086 }
1087 }
1088
1089 #[test]
1090 fn executes_css_source_witnesses_through_egg_engine() {
1091 let source = ".a:is(.ready) { width: calc(1px + 2px); } .b:is(.x, .x) { color: red; } .c:where(.y, .y) { color: blue; }";
1092 let transformed =
1093 ".a.ready { width: 3px; } .b.x { color: red; } .c:where(.y) { color: blue; }";
1094 let plan = plan_egg_rewrite_passes_for_source(source);
1095 let witnesses = execute_egg_rewrite_witnesses_for_css_source(
1096 source,
1097 transformed,
1098 &plan.planned_pass_ids,
1099 );
1100
1101 assert_eq!(witnesses.len(), 4);
1102 assert!(witnesses.iter().all(|witness| witness.execution.accepted));
1103 assert!(
1104 witnesses
1105 .iter()
1106 .any(|witness| witness.pass_id == "selector-is-where-compression")
1107 );
1108 assert!(
1109 witnesses
1110 .iter()
1111 .any(|witness| witness.pass_id == "calc-reduction")
1112 );
1113 assert!(witnesses.iter().any(|witness| {
1114 witness.source_kind == "selectorIsDedup" && witness.css_after == ".x"
1115 }));
1116 assert!(witnesses.iter().any(|witness| {
1117 witness.source_kind == "selectorWhereDedup" && witness.css_after == ":where(.y)"
1118 }));
1119 assert!(witnesses.iter().any(|witness| {
1120 witness.source_kind == "calcSameUnitAdd"
1121 && witness.css_after == "3px"
1122 && witness.execution.after == "(unit 3 px)"
1123 }));
1124 }
1125
1126 #[test]
1127 fn mdl_default_ast_size_matches_100_fixture_differential_corpus() {
1128 let selector_cases = (0..50).map(|index| {
1129 (
1130 TransformPassKind::SelectorIsWhereCompression.id(),
1131 format!("(is token{index})"),
1132 format!("token{index}"),
1133 true,
1134 false,
1135 "single :is() argument keeps specificity",
1136 )
1137 });
1138 let calc_cases = (0..50).map(|index| {
1139 let left = index + 1;
1140 let right = 50 - index;
1141 (
1142 TransformPassKind::CalcReduction.id(),
1143 format!("(calc (+ (unit {left} px) (unit {right} px)))"),
1144 format!("(unit {} px)", left + right),
1145 false,
1146 true,
1147 "same-unit calc arithmetic preserves computed value",
1148 )
1149 });
1150 let cases = selector_cases.chain(calc_cases).collect::<Vec<_>>();
1151
1152 assert_eq!(cases.len(), 100);
1153 for (
1154 pass_id,
1155 before,
1156 expected_after,
1157 specificity_preserved,
1158 computed_value_preserved,
1159 witness,
1160 ) in cases
1161 {
1162 let execution = execute_egg_rewrite(EggRewriteCandidateV0 {
1163 pass_id,
1164 before: before.clone(),
1165 after: expected_after.clone(),
1166 proof: EggRewriteProofV0 {
1167 specificity_preserved,
1168 computed_value_preserved,
1169 provenance_preserved: true,
1170 cascade_safe_witness: witness.to_string(),
1171 },
1172 });
1173
1174 assert!(execution.accepted, "{before} -> {expected_after}");
1175 assert_eq!(execution.after, expected_after);
1176 assert!(execution.after_matches_candidate);
1177 assert_eq!(execution.mdl_bits, None);
1178 assert_eq!(execution.mdl_unit, None);
1179 }
1180 }
1181}