use omena_cascade::{
BoxLonghandInputV0, LayerFlattenInputV0, ScopeFlattenInputV0, StaticSupportsAssumptionV0,
StaticSupportsEvalVerdictV0, evaluate_static_supports_condition,
prove_box_shorthand_combination, prove_layer_flatten_candidate, prove_scope_flatten_candidate,
};
use serde::Serialize;
use crate::{
SMT_FEATURE_GATE_V0, SMT_LAYER_MARKER_V0, SMT_SCHEMA_VERSION_V0, SmtVerdictV0,
StubSmtBackendV0, smt_evaluate_static_supports_condition_v0,
smt_prove_box_shorthand_combination_v0, smt_prove_layer_flatten_candidate_v0,
smt_prove_scope_flatten_candidate_v0,
};
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct SmtBisimulationFuzzCaseV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
pub seed: u64,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct SmtBisimulationFuzzReportV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
pub fixture_suite: &'static str,
pub seed: u64,
pub checked_obligation_count: usize,
pub l1_l3_mismatch_count: usize,
pub passed: bool,
}
pub fn smt_bisimulation_fuzz_case_v0(seed: u64) -> SmtBisimulationFuzzCaseV0 {
SmtBisimulationFuzzCaseV0 {
schema_version: SMT_SCHEMA_VERSION_V0,
product: "omena-smt.bisimulation-fuzz-case",
layer_marker: SMT_LAYER_MARKER_V0,
feature_gate: SMT_FEATURE_GATE_V0,
seed,
}
}
pub fn run_smt_bisimulation_fuzz_case_v0(
case: SmtBisimulationFuzzCaseV0,
) -> SmtBisimulationFuzzReportV0 {
let backend = StubSmtBackendV0::default();
let mut checked_obligation_count = 0;
let mut l1_l3_mismatch_count = 0;
let longhands = generated_box_longhands(case.seed);
let shorthand_property = if case.seed.is_multiple_of(7) {
"unsupported"
} else if case.seed.is_multiple_of(3) {
"padding"
} else {
"margin"
};
let l1_box = prove_box_shorthand_combination(shorthand_property, &longhands);
let l3_box = smt_prove_box_shorthand_combination_v0(shorthand_property, &longhands, &backend);
checked_obligation_count += 1;
if l3_box.verdict != expected_verdict_from_l1_accepted(Some(l1_box.accepted)) {
l1_l3_mismatch_count += 1;
}
let supports_condition = generated_supports_condition(case.seed);
let l1_supports = evaluate_static_supports_condition(
supports_condition,
StaticSupportsAssumptionV0::ModernBrowser,
);
let l3_supports = smt_evaluate_static_supports_condition_v0(
supports_condition,
StaticSupportsAssumptionV0::ModernBrowser,
&backend,
);
checked_obligation_count += 1;
if l3_supports.verdict != expected_verdict_from_supports(l1_supports.verdict) {
l1_l3_mismatch_count += 1;
}
let scope_input = generated_scope_input(case.seed);
let l1_scope = prove_scope_flatten_candidate(scope_input.clone());
let l3_scope = smt_prove_scope_flatten_candidate_v0(scope_input, &backend);
checked_obligation_count += 1;
if l3_scope.verdict != expected_verdict_from_l1_accepted(Some(l1_scope.accepted)) {
l1_l3_mismatch_count += 1;
}
let layer_input = generated_layer_input(case.seed);
let l1_layer = prove_layer_flatten_candidate(layer_input.clone());
let l3_layer = smt_prove_layer_flatten_candidate_v0(layer_input, &backend);
checked_obligation_count += 1;
if l3_layer.verdict != expected_verdict_from_l1_accepted(Some(l1_layer.accepted)) {
l1_l3_mismatch_count += 1;
}
SmtBisimulationFuzzReportV0 {
schema_version: SMT_SCHEMA_VERSION_V0,
product: "omena-smt.bisimulation-fuzz-report",
layer_marker: SMT_LAYER_MARKER_V0,
feature_gate: SMT_FEATURE_GATE_V0,
fixture_suite: "m3-cascade-proof-fixtures",
seed: case.seed,
checked_obligation_count,
l1_l3_mismatch_count,
passed: l1_l3_mismatch_count == 0,
}
}
pub fn run_smt_bisimulation_fuzz_seed_corpus_v0(case_count: usize) -> SmtBisimulationFuzzReportV0 {
let mut checked_obligation_count = 0;
let mut l1_l3_mismatch_count = 0;
for index in 0..case_count {
let report = run_smt_bisimulation_fuzz_case_v0(smt_bisimulation_fuzz_case_v0(stable_seed(
index as u64,
)));
checked_obligation_count += report.checked_obligation_count;
l1_l3_mismatch_count += report.l1_l3_mismatch_count;
}
SmtBisimulationFuzzReportV0 {
schema_version: SMT_SCHEMA_VERSION_V0,
product: "omena-smt.bisimulation-fuzz-seed-corpus",
layer_marker: SMT_LAYER_MARKER_V0,
feature_gate: SMT_FEATURE_GATE_V0,
fixture_suite: "m3-cascade-proof-fixtures",
seed: 0,
checked_obligation_count,
l1_l3_mismatch_count,
passed: l1_l3_mismatch_count == 0,
}
}
fn expected_verdict_from_l1_accepted(accepted: Option<bool>) -> SmtVerdictV0 {
match accepted {
Some(true) => SmtVerdictV0::Accepted,
Some(false) => SmtVerdictV0::Rejected,
None => SmtVerdictV0::Unknown,
}
}
fn expected_verdict_from_supports(verdict: StaticSupportsEvalVerdictV0) -> SmtVerdictV0 {
match verdict {
StaticSupportsEvalVerdictV0::AlwaysTrue => SmtVerdictV0::Accepted,
StaticSupportsEvalVerdictV0::AlwaysFalse => SmtVerdictV0::Rejected,
StaticSupportsEvalVerdictV0::Unknown => SmtVerdictV0::Unknown,
}
}
fn generated_box_longhands(seed: u64) -> Vec<BoxLonghandInputV0> {
let shorthand = if seed.is_multiple_of(3) {
"padding"
} else {
"margin"
};
let properties = [
format!("{shorthand}-top"),
format!("{shorthand}-right"),
format!("{shorthand}-bottom"),
format!("{shorthand}-left"),
];
let maybe_permuted = if seed.is_multiple_of(5) {
vec![1, 0, 2, 3]
} else {
vec![0, 1, 2, 3]
};
maybe_permuted
.into_iter()
.enumerate()
.map(|(source_index, property_index)| BoxLonghandInputV0 {
property: properties[property_index].clone(),
value: if seed.is_multiple_of(11) {
String::new()
} else {
format!("{}px", (seed + source_index as u64) % 17)
},
important: seed.is_multiple_of(13),
source_order: if seed.is_multiple_of(17) {
(source_index as u32) * 2 + 1
} else {
source_index as u32 + 1
},
})
.collect()
}
fn generated_supports_condition(seed: u64) -> &'static str {
const CONDITIONS: &[&str] = &[
"(display: grid)",
"(display: unknown-omena)",
"selector(:has(*))",
"not (display: grid)",
"((display: grid) or (display: unknown-omena))",
"((display: grid) and selector(:has(*)))",
"font-tech(color-COLRv1)",
];
CONDITIONS[(seed as usize) % CONDITIONS.len()]
}
fn generated_scope_input(seed: u64) -> ScopeFlattenInputV0 {
ScopeFlattenInputV0 {
root_selector: if seed.is_multiple_of(2) {
":root".to_string()
} else {
".scope".to_string()
},
limit_selector: seed.is_multiple_of(3).then(|| ".limit".to_string()),
scoped_rule_count: (seed % 4) as usize,
peer_scope_count: (seed % 3) as usize,
competing_unscoped_rule_count: (seed % 2) as usize,
inside_layer: seed.is_multiple_of(5),
}
}
fn generated_layer_input(seed: u64) -> LayerFlattenInputV0 {
LayerFlattenInputV0 {
layer_name: seed.is_multiple_of(2).then(|| "components".to_string()),
layer_rule_count: (seed % 5) as usize,
peer_layer_count: (seed % 3) as usize,
unlayered_rule_count: (seed % 4) as usize,
important_declaration_count: (seed % 2) as usize,
closed_bundle: !seed.is_multiple_of(7),
}
}
fn stable_seed(index: u64) -> u64 {
index
.wrapping_mul(0x9e37_79b9_7f4a_7c15)
.wrapping_add(0xd1b5_4a32_d192_ed03)
}