1use omena_cascade::{
2 BoxLonghandInputV0, LayerFlattenInputV0, ScopeFlattenInputV0, StaticSupportsAssumptionV0,
3 StaticSupportsEvalVerdictV0, evaluate_static_supports_condition,
4 prove_box_shorthand_combination, prove_layer_flatten_candidate, prove_scope_flatten_candidate,
5};
6use serde::Serialize;
7
8use crate::{
9 SMT_FEATURE_GATE_V0, SMT_LAYER_MARKER_V0, SMT_SCHEMA_VERSION_V0, SmtVerdictV0,
10 StubSmtBackendV0, smt_evaluate_static_supports_condition_v0,
11 smt_prove_box_shorthand_combination_v0, smt_prove_layer_flatten_candidate_v0,
12 smt_prove_scope_flatten_candidate_v0,
13};
14
15#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
16#[serde(rename_all = "camelCase")]
17pub struct SmtBisimulationFuzzCaseV0 {
18 pub schema_version: &'static str,
19 pub product: &'static str,
20 pub layer_marker: &'static str,
21 pub feature_gate: &'static str,
22 pub seed: u64,
23}
24
25#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
26#[serde(rename_all = "camelCase")]
27pub struct SmtBisimulationFuzzReportV0 {
28 pub schema_version: &'static str,
29 pub product: &'static str,
30 pub layer_marker: &'static str,
31 pub feature_gate: &'static str,
32 pub fixture_suite: &'static str,
33 pub seed: u64,
34 pub checked_obligation_count: usize,
35 pub l1_l3_mismatch_count: usize,
36 pub passed: bool,
37}
38
39pub fn smt_bisimulation_fuzz_case_v0(seed: u64) -> SmtBisimulationFuzzCaseV0 {
40 SmtBisimulationFuzzCaseV0 {
41 schema_version: SMT_SCHEMA_VERSION_V0,
42 product: "omena-smt.bisimulation-fuzz-case",
43 layer_marker: SMT_LAYER_MARKER_V0,
44 feature_gate: SMT_FEATURE_GATE_V0,
45 seed,
46 }
47}
48
49pub fn run_smt_bisimulation_fuzz_case_v0(
50 case: SmtBisimulationFuzzCaseV0,
51) -> SmtBisimulationFuzzReportV0 {
52 let backend = StubSmtBackendV0::default();
53 let mut checked_obligation_count = 0;
54 let mut l1_l3_mismatch_count = 0;
55
56 let longhands = generated_box_longhands(case.seed);
57 let shorthand_property = if case.seed.is_multiple_of(7) {
58 "unsupported"
59 } else if case.seed.is_multiple_of(3) {
60 "padding"
61 } else {
62 "margin"
63 };
64 let l1_box = prove_box_shorthand_combination(shorthand_property, &longhands);
65 let l3_box = smt_prove_box_shorthand_combination_v0(shorthand_property, &longhands, &backend);
66 checked_obligation_count += 1;
67 if l3_box.verdict != expected_verdict_from_l1_accepted(Some(l1_box.accepted)) {
68 l1_l3_mismatch_count += 1;
69 }
70
71 let supports_condition = generated_supports_condition(case.seed);
72 let l1_supports = evaluate_static_supports_condition(
73 supports_condition,
74 StaticSupportsAssumptionV0::ModernBrowser,
75 );
76 let l3_supports = smt_evaluate_static_supports_condition_v0(
77 supports_condition,
78 StaticSupportsAssumptionV0::ModernBrowser,
79 &backend,
80 );
81 checked_obligation_count += 1;
82 if l3_supports.verdict != expected_verdict_from_supports(l1_supports.verdict) {
83 l1_l3_mismatch_count += 1;
84 }
85
86 let scope_input = generated_scope_input(case.seed);
87 let l1_scope = prove_scope_flatten_candidate(scope_input.clone());
88 let l3_scope = smt_prove_scope_flatten_candidate_v0(scope_input, &backend);
89 checked_obligation_count += 1;
90 if l3_scope.verdict != expected_verdict_from_l1_accepted(Some(l1_scope.accepted)) {
91 l1_l3_mismatch_count += 1;
92 }
93
94 let layer_input = generated_layer_input(case.seed);
95 let l1_layer = prove_layer_flatten_candidate(layer_input.clone());
96 let l3_layer = smt_prove_layer_flatten_candidate_v0(layer_input, &backend);
97 checked_obligation_count += 1;
98 if l3_layer.verdict != expected_verdict_from_l1_accepted(Some(l1_layer.accepted)) {
99 l1_l3_mismatch_count += 1;
100 }
101
102 SmtBisimulationFuzzReportV0 {
103 schema_version: SMT_SCHEMA_VERSION_V0,
104 product: "omena-smt.bisimulation-fuzz-report",
105 layer_marker: SMT_LAYER_MARKER_V0,
106 feature_gate: SMT_FEATURE_GATE_V0,
107 fixture_suite: "m3-cascade-proof-fixtures",
108 seed: case.seed,
109 checked_obligation_count,
110 l1_l3_mismatch_count,
111 passed: l1_l3_mismatch_count == 0,
112 }
113}
114
115pub fn run_smt_bisimulation_fuzz_seed_corpus_v0(case_count: usize) -> SmtBisimulationFuzzReportV0 {
116 let mut checked_obligation_count = 0;
117 let mut l1_l3_mismatch_count = 0;
118
119 for index in 0..case_count {
120 let report = run_smt_bisimulation_fuzz_case_v0(smt_bisimulation_fuzz_case_v0(stable_seed(
121 index as u64,
122 )));
123 checked_obligation_count += report.checked_obligation_count;
124 l1_l3_mismatch_count += report.l1_l3_mismatch_count;
125 }
126
127 SmtBisimulationFuzzReportV0 {
128 schema_version: SMT_SCHEMA_VERSION_V0,
129 product: "omena-smt.bisimulation-fuzz-seed-corpus",
130 layer_marker: SMT_LAYER_MARKER_V0,
131 feature_gate: SMT_FEATURE_GATE_V0,
132 fixture_suite: "m3-cascade-proof-fixtures",
133 seed: 0,
134 checked_obligation_count,
135 l1_l3_mismatch_count,
136 passed: l1_l3_mismatch_count == 0,
137 }
138}
139
140fn expected_verdict_from_l1_accepted(accepted: Option<bool>) -> SmtVerdictV0 {
141 match accepted {
142 Some(true) => SmtVerdictV0::Accepted,
143 Some(false) => SmtVerdictV0::Rejected,
144 None => SmtVerdictV0::Unknown,
145 }
146}
147
148fn expected_verdict_from_supports(verdict: StaticSupportsEvalVerdictV0) -> SmtVerdictV0 {
149 match verdict {
150 StaticSupportsEvalVerdictV0::AlwaysTrue => SmtVerdictV0::Accepted,
151 StaticSupportsEvalVerdictV0::AlwaysFalse => SmtVerdictV0::Rejected,
152 StaticSupportsEvalVerdictV0::Unknown => SmtVerdictV0::Unknown,
153 }
154}
155
156fn generated_box_longhands(seed: u64) -> Vec<BoxLonghandInputV0> {
157 let shorthand = if seed.is_multiple_of(3) {
158 "padding"
159 } else {
160 "margin"
161 };
162 let properties = [
163 format!("{shorthand}-top"),
164 format!("{shorthand}-right"),
165 format!("{shorthand}-bottom"),
166 format!("{shorthand}-left"),
167 ];
168 let maybe_permuted = if seed.is_multiple_of(5) {
169 vec![1, 0, 2, 3]
170 } else {
171 vec![0, 1, 2, 3]
172 };
173
174 maybe_permuted
175 .into_iter()
176 .enumerate()
177 .map(|(source_index, property_index)| BoxLonghandInputV0 {
178 property: properties[property_index].clone(),
179 value: if seed.is_multiple_of(11) {
180 String::new()
181 } else {
182 format!("{}px", (seed + source_index as u64) % 17)
183 },
184 important: seed.is_multiple_of(13),
185 source_order: if seed.is_multiple_of(17) {
186 (source_index as u32) * 2 + 1
187 } else {
188 source_index as u32 + 1
189 },
190 })
191 .collect()
192}
193
194fn generated_supports_condition(seed: u64) -> &'static str {
195 const CONDITIONS: &[&str] = &[
196 "(display: grid)",
197 "(display: unknown-omena)",
198 "selector(:has(*))",
199 "not (display: grid)",
200 "((display: grid) or (display: unknown-omena))",
201 "((display: grid) and selector(:has(*)))",
202 "font-tech(color-COLRv1)",
203 ];
204 CONDITIONS[(seed as usize) % CONDITIONS.len()]
205}
206
207fn generated_scope_input(seed: u64) -> ScopeFlattenInputV0 {
208 ScopeFlattenInputV0 {
209 root_selector: if seed.is_multiple_of(2) {
210 ":root".to_string()
211 } else {
212 ".scope".to_string()
213 },
214 limit_selector: seed.is_multiple_of(3).then(|| ".limit".to_string()),
215 scoped_rule_count: (seed % 4) as usize,
216 peer_scope_count: (seed % 3) as usize,
217 competing_unscoped_rule_count: (seed % 2) as usize,
218 inside_layer: seed.is_multiple_of(5),
219 }
220}
221
222fn generated_layer_input(seed: u64) -> LayerFlattenInputV0 {
223 LayerFlattenInputV0 {
224 layer_name: seed.is_multiple_of(2).then(|| "components".to_string()),
225 layer_rule_count: (seed % 5) as usize,
226 peer_layer_count: (seed % 3) as usize,
227 unlayered_rule_count: (seed % 4) as usize,
228 important_declaration_count: (seed % 2) as usize,
229 closed_bundle: !seed.is_multiple_of(7),
230 }
231}
232
233fn stable_seed(index: u64) -> u64 {
234 index
235 .wrapping_mul(0x9e37_79b9_7f4a_7c15)
236 .wrapping_add(0xd1b5_4a32_d192_ed03)
237}