use std::{collections::BTreeSet, marker::PhantomData};
use omena_abstract_value::{AbstractPropertyValueV0, CascadeValueFamilyV0};
use omena_cascade::{
CascadeDeclaration, CascadeRefinementContextV0,
refine_declaration_in_context as refine_cascade_declaration_in_context,
};
use omena_refinement_trait::{
PropertyIndexV0, REFINEMENT_FEATURE_GATE_V0, REFINEMENT_LAYER_MARKER_V0,
REFINEMENT_SCHEMA_VERSION_V0, RefinementPredicateV0, RefinementVerdictV0, RefinementWitnessV0,
refinement_provenance_v0, refinement_witness_v0,
};
use serde::Serialize;
pub const REFINEMENT_BRIDGE_CLAIM_LEVEL_V0: &str = "m6DimensionalRefinementBridgeSubstrate";
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub enum AbstractValueShapeV0 {
Bottom,
Exact,
FiniteSet,
CustomPropertyReference,
Top,
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct TopPredicateV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
}
impl Default for TopPredicateV0 {
fn default() -> Self {
Self {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.top-predicate",
layer_marker: REFINEMENT_LAYER_MARKER_V0,
feature_gate: REFINEMENT_FEATURE_GATE_V0,
}
}
}
impl RefinementPredicateV0 for TopPredicateV0 {
const PREDICATE_ID: &'static str = "top";
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct AnyPropertyIndexV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
}
impl Default for AnyPropertyIndexV0 {
fn default() -> Self {
Self {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.any-property-index",
layer_marker: REFINEMENT_LAYER_MARKER_V0,
feature_gate: REFINEMENT_FEATURE_GATE_V0,
}
}
}
impl PropertyIndexV0 for AnyPropertyIndexV0 {
const PROPERTY_NAME: &'static str = "*";
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase", bound = "")]
pub struct RefinedAbstractPropertyValueV0<P: PropertyIndexV0, R: RefinementPredicateV0> {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
pub property_name: &'static str,
pub predicate_id: &'static str,
pub value_shape: AbstractValueShapeV0,
pub legacy_value: AbstractPropertyValueV0,
pub strict_superset_of_legacy_v0: bool,
#[serde(skip)]
marker: PhantomData<(P, R)>,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub enum RefinementPropertyPredicateV0 {
Any,
ExactValue {
property_name: String,
value: String,
},
OneOfValues {
property_name: String,
values: Vec<String>,
},
CustomPropertyReference {
property_name: String,
custom_property_name: String,
},
NumericRange {
property_name: String,
min_inclusive: Option<i64>,
max_inclusive: Option<i64>,
unit: Option<String>,
},
HasPseudoState {
property_name: String,
pseudo_state: String,
},
And {
predicates: Vec<RefinementPropertyPredicateV0>,
},
Or {
predicates: Vec<RefinementPropertyPredicateV0>,
},
Not {
predicate: Box<RefinementPropertyPredicateV0>,
},
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct RefinementPredicateEvaluationV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
pub predicate_expression_id: String,
pub value_shape: AbstractValueShapeV0,
pub verdict: RefinementVerdictV0,
pub matched_clause_count: usize,
pub witness: RefinementWitnessV0,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct RefinementContextSummaryV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
pub predicate_count: usize,
pub context_digest: u64,
pub witness_provenance_count: usize,
pub downstream_invalidation_required: bool,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct CascadeDimensionalRefinementBridgeV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
pub claim_level: &'static str,
pub property_name: String,
pub cascade_family_product: &'static str,
pub predicate_count: usize,
pub context_value_count: usize,
pub restriction_map_count: usize,
pub context_evaluation_count: usize,
pub satisfied_all_context_count: usize,
pub satisfied_some_context_count: usize,
pub unknown_context_count: usize,
pub unsatisfiable_context_count: usize,
pub witness_provenance_count: usize,
pub property_consistent: bool,
pub uses_existing_abstract_property_value_substrate: bool,
pub uses_existing_cascade_family_substrate: bool,
pub uses_existing_refinement_predicate_substrate: bool,
pub forks_unit_system: bool,
pub liquid_haskell_complete: bool,
pub smt_backend_available: bool,
pub smt_complete: bool,
pub theorem_claimed: bool,
pub product_path_evidence_ready: bool,
pub stronger_type_safety_claim_ready: bool,
pub dimension_vector_domain_ready: bool,
pub calc_dimension_diagnostics_ready: bool,
pub dimension_vector_domain: DimensionVectorDomainSummaryV0,
pub calc_dimension_diagnostics: CalcDimensionDiagnosticSummaryV0,
pub evaluations: Vec<CascadeDimensionalRefinementContextEvaluationV0>,
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct DimensionVectorV0 {
pub length: i8,
pub angle: i8,
pub time: i8,
pub percentage: i8,
pub number: i8,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct DimensionVectorValueV0 {
pub source_value: String,
pub unit: String,
pub unit_family: &'static str,
pub vector: DimensionVectorV0,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct DimensionVectorDomainSummaryV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub feature_gate: &'static str,
pub claim_level: &'static str,
pub theorem_claimed: bool,
pub forks_unit_system: bool,
pub value_count: usize,
pub vector_count: usize,
pub values: Vec<DimensionVectorValueV0>,
}
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub enum CalcDimensionDiagnosticKindV0 {
DimensionalMismatch,
MixedDimension,
ContextDependentDimension,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct CalcDimensionDiagnosticV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub feature_gate: &'static str,
pub claim_level: &'static str,
pub theorem_claimed: bool,
pub public_safety_claim_ready: bool,
pub kind: CalcDimensionDiagnosticKindV0,
pub property_name: String,
pub expression: String,
pub observed_units: Vec<String>,
pub observed_vectors: Vec<DimensionVectorV0>,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct CalcDimensionDiagnosticSummaryV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub feature_gate: &'static str,
pub claim_level: &'static str,
pub theorem_claimed: bool,
pub forks_unit_system: bool,
pub smt_complete: bool,
pub liquid_haskell_complete: bool,
pub stronger_type_safety_claim_ready: bool,
pub diagnostic_count: usize,
pub diagnostics: Vec<CalcDimensionDiagnosticV0>,
}
#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
#[serde(rename_all = "camelCase")]
pub struct CascadeDimensionalRefinementContextEvaluationV0 {
pub schema_version: &'static str,
pub product: &'static str,
pub layer_marker: &'static str,
pub feature_gate: &'static str,
pub context_id: String,
pub selector_count: usize,
pub condition_count: usize,
pub layer_count: usize,
pub value_shape: AbstractValueShapeV0,
pub combined_verdict: RefinementVerdictV0,
pub predicate_evaluation_count: usize,
pub matched_clause_count: usize,
pub witness_provenance_count: usize,
pub predicate_expression_ids: Vec<String>,
}
pub fn project_legacy_to_refined_v0<P, R>(
legacy_value: AbstractPropertyValueV0,
) -> RefinedAbstractPropertyValueV0<P, R>
where
P: PropertyIndexV0,
R: RefinementPredicateV0,
{
let mut refined = RefinedAbstractPropertyValueV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.refined-abstract-property-value",
layer_marker: REFINEMENT_LAYER_MARKER_V0,
feature_gate: REFINEMENT_FEATURE_GATE_V0,
property_name: P::PROPERTY_NAME,
predicate_id: R::PREDICATE_ID,
value_shape: abstract_property_value_shape_v0(&legacy_value),
legacy_value,
strict_superset_of_legacy_v0: false,
marker: PhantomData,
};
refined.strict_superset_of_legacy_v0 =
refined_projection_preserves_legacy_value_v0::<P, R>(&refined);
refined
}
pub fn project_refined_to_legacy_v0<P, R>(
refined: &RefinedAbstractPropertyValueV0<P, R>,
) -> AbstractPropertyValueV0
where
P: PropertyIndexV0,
R: RefinementPredicateV0,
{
refined.legacy_value.clone()
}
pub fn refined_projection_preserves_legacy_value_v0<P, R>(
refined: &RefinedAbstractPropertyValueV0<P, R>,
) -> bool
where
P: PropertyIndexV0,
R: RefinementPredicateV0,
{
refined.schema_version == REFINEMENT_SCHEMA_VERSION_V0
&& refined.layer_marker == REFINEMENT_LAYER_MARKER_V0
&& refined.feature_gate == REFINEMENT_FEATURE_GATE_V0
&& refined.property_name == P::PROPERTY_NAME
&& refined.predicate_id == R::PREDICATE_ID
&& abstract_property_value_shape_v0(&project_refined_to_legacy_v0(refined))
== refined.value_shape
}
pub fn evaluate_refinement_property_predicate_v0(
predicate: &RefinementPropertyPredicateV0,
value: &AbstractPropertyValueV0,
) -> RefinementPredicateEvaluationV0 {
let verdict = evaluate_refinement_predicate_verdict_v0(predicate, value);
let matched_clause_count = count_satisfied_refinement_clauses_v0(predicate, value);
let predicate_expression_id = refinement_predicate_expression_id_v0(predicate);
let witness = refinement_witness_v0(
"property-grammar",
verdict,
refinement_predicate_provenance_v0(predicate),
);
RefinementPredicateEvaluationV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.property-predicate-evaluation",
layer_marker: REFINEMENT_LAYER_MARKER_V0,
feature_gate: REFINEMENT_FEATURE_GATE_V0,
predicate_expression_id,
value_shape: abstract_property_value_shape_v0(value),
verdict,
matched_clause_count,
witness,
}
}
pub fn refine_declaration_in_context(
declaration: &CascadeDeclaration,
context: &CascadeRefinementContextV0,
) -> RefinementWitnessV0 {
refine_cascade_declaration_in_context(declaration, context)
}
pub fn summarize_refinement_context_v0(
predicates: &[RefinementPropertyPredicateV0],
) -> RefinementContextSummaryV0 {
let mut expression_ids = predicates
.iter()
.map(refinement_predicate_expression_id_v0)
.collect::<Vec<_>>();
expression_ids.sort();
let witness_provenance_count = predicates
.iter()
.flat_map(refinement_predicate_provenance_v0)
.map(|provenance| provenance.source)
.collect::<std::collections::BTreeSet<_>>()
.len();
let context_digest = deterministic_refinement_digest_v0(expression_ids.join("\n").as_bytes());
RefinementContextSummaryV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.context-summary",
layer_marker: REFINEMENT_LAYER_MARKER_V0,
feature_gate: REFINEMENT_FEATURE_GATE_V0,
predicate_count: predicates.len(),
context_digest,
witness_provenance_count,
downstream_invalidation_required: !predicates.is_empty(),
}
}
pub fn summarize_dimension_vector_domain_v0(values: &[String]) -> DimensionVectorDomainSummaryV0 {
let mut entries = values
.iter()
.flat_map(|value| {
extract_calc_expression_v0(value)
.map(parse_dimension_vector_values_from_expression_v0)
.unwrap_or_else(|| parse_dimension_vector_value_v0(value).into_iter().collect())
})
.collect::<Vec<_>>();
entries.sort_by(|left, right| {
left.source_value
.cmp(&right.source_value)
.then_with(|| left.unit.cmp(&right.unit))
});
entries.dedup_by(|left, right| {
left.source_value == right.source_value
&& left.unit == right.unit
&& left.unit_family == right.unit_family
&& left.vector == right.vector
});
let vector_count = entries
.iter()
.map(|entry| entry.vector)
.collect::<BTreeSet<_>>()
.len();
DimensionVectorDomainSummaryV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.dimension-vector-domain",
feature_gate: "dimension-vector-domain-v0",
claim_level: "fixtureWitnessDimensionVectorDomain",
theorem_claimed: false,
forks_unit_system: false,
value_count: entries.len(),
vector_count,
values: entries,
}
}
pub fn summarize_calc_dimension_diagnostics_v0(
property_name: &str,
values: &[String],
) -> CalcDimensionDiagnosticSummaryV0 {
let mut diagnostics = values
.iter()
.filter_map(|value| calc_dimension_diagnostic_for_value_v0(property_name, value))
.collect::<Vec<_>>();
diagnostics.sort_by(|left, right| {
left.property_name
.cmp(&right.property_name)
.then_with(|| left.expression.cmp(&right.expression))
});
CalcDimensionDiagnosticSummaryV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.calc-dimension-diagnostics",
feature_gate: "calc-dimension-diagnostics-v0",
claim_level: "researchGradeHint",
theorem_claimed: false,
forks_unit_system: false,
smt_complete: false,
liquid_haskell_complete: false,
stronger_type_safety_claim_ready: false,
diagnostic_count: diagnostics.len(),
diagnostics,
}
}
pub fn summarize_cascade_dimensional_refinement_bridge_v0(
family: &CascadeValueFamilyV0,
predicates: &[RefinementPropertyPredicateV0],
) -> CascadeDimensionalRefinementBridgeV0 {
let exact_values = family
.members
.iter()
.filter_map(|member| match &member.value {
AbstractPropertyValueV0::Exact { value, .. } => Some(value.clone()),
_ => None,
})
.collect::<Vec<_>>();
let dimension_vector_domain = summarize_dimension_vector_domain_v0(&exact_values);
let calc_dimension_diagnostics =
summarize_calc_dimension_diagnostics_v0(&family.property_name, &exact_values);
let mut global_provenance_sources = BTreeSet::new();
let mut evaluations = family
.members
.iter()
.map(|member| {
let predicate_evaluations = predicates
.iter()
.map(|predicate| {
evaluate_refinement_property_predicate_v0(predicate, &member.value)
})
.collect::<Vec<_>>();
let verdicts = predicate_evaluations
.iter()
.map(|evaluation| evaluation.verdict)
.collect::<Vec<_>>();
let combined_verdict = combine_and_refinement_verdicts_v0(&verdicts);
let mut context_provenance_sources = BTreeSet::new();
for evaluation in &predicate_evaluations {
for provenance in &evaluation.witness.provenance {
context_provenance_sources.insert(provenance.source);
global_provenance_sources.insert(provenance.source);
}
}
CascadeDimensionalRefinementContextEvaluationV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.cascade-dimensional-refinement-context-evaluation",
layer_marker: REFINEMENT_LAYER_MARKER_V0,
feature_gate: REFINEMENT_FEATURE_GATE_V0,
context_id: member.context.id.clone(),
selector_count: member.context.selectors.len(),
condition_count: member.context.conditions.len(),
layer_count: member.context.layers.len(),
value_shape: abstract_property_value_shape_v0(&member.value),
combined_verdict,
predicate_evaluation_count: predicate_evaluations.len(),
matched_clause_count: predicate_evaluations
.iter()
.map(|evaluation| evaluation.matched_clause_count)
.sum(),
witness_provenance_count: context_provenance_sources.len(),
predicate_expression_ids: predicate_evaluations
.into_iter()
.map(|evaluation| evaluation.predicate_expression_id)
.collect(),
}
})
.collect::<Vec<_>>();
evaluations.sort_by(|left, right| left.context_id.cmp(&right.context_id));
CascadeDimensionalRefinementBridgeV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.cascade-dimensional-refinement-bridge",
layer_marker: REFINEMENT_LAYER_MARKER_V0,
feature_gate: REFINEMENT_FEATURE_GATE_V0,
claim_level: REFINEMENT_BRIDGE_CLAIM_LEVEL_V0,
property_name: family.property_name.clone(),
cascade_family_product: family.product,
predicate_count: predicates.len(),
context_value_count: family.context_value_count,
restriction_map_count: family.restriction_map_count,
context_evaluation_count: evaluations.len(),
satisfied_all_context_count: count_context_verdicts_v0(
&evaluations,
RefinementVerdictV0::SatisfiedAll,
),
satisfied_some_context_count: count_context_verdicts_v0(
&evaluations,
RefinementVerdictV0::SatisfiedSome,
),
unknown_context_count: count_context_verdicts_v0(
&evaluations,
RefinementVerdictV0::Unknown,
),
unsatisfiable_context_count: count_context_verdicts_v0(
&evaluations,
RefinementVerdictV0::Unsatisfiable,
),
witness_provenance_count: global_provenance_sources.len(),
property_consistent: family.property_consistent,
uses_existing_abstract_property_value_substrate: true,
uses_existing_cascade_family_substrate: true,
uses_existing_refinement_predicate_substrate: true,
forks_unit_system: false,
liquid_haskell_complete: false,
smt_backend_available: refinement_smt_backend_available_v0(),
smt_complete: false,
theorem_claimed: false,
product_path_evidence_ready: true,
stronger_type_safety_claim_ready: false,
dimension_vector_domain_ready: dimension_vector_domain.value_count > 0
&& !dimension_vector_domain.forks_unit_system
&& !dimension_vector_domain.theorem_claimed,
calc_dimension_diagnostics_ready: !calc_dimension_diagnostics.forks_unit_system
&& !calc_dimension_diagnostics.smt_complete
&& !calc_dimension_diagnostics.liquid_haskell_complete
&& !calc_dimension_diagnostics.stronger_type_safety_claim_ready
&& !calc_dimension_diagnostics.theorem_claimed,
dimension_vector_domain,
calc_dimension_diagnostics,
evaluations,
}
}
pub fn abstract_property_value_shape_v0(value: &AbstractPropertyValueV0) -> AbstractValueShapeV0 {
match value {
AbstractPropertyValueV0::Bottom { .. } => AbstractValueShapeV0::Bottom,
AbstractPropertyValueV0::Exact { .. } => AbstractValueShapeV0::Exact,
AbstractPropertyValueV0::FiniteSet { .. } => AbstractValueShapeV0::FiniteSet,
AbstractPropertyValueV0::CustomPropertyReference { .. } => {
AbstractValueShapeV0::CustomPropertyReference
}
AbstractPropertyValueV0::Top { .. } => AbstractValueShapeV0::Top,
}
}
fn count_context_verdicts_v0(
evaluations: &[CascadeDimensionalRefinementContextEvaluationV0],
verdict: RefinementVerdictV0,
) -> usize {
evaluations
.iter()
.filter(|evaluation| evaluation.combined_verdict == verdict)
.count()
}
fn evaluate_refinement_predicate_verdict_v0(
predicate: &RefinementPropertyPredicateV0,
value: &AbstractPropertyValueV0,
) -> RefinementVerdictV0 {
match predicate {
RefinementPropertyPredicateV0::Any => RefinementVerdictV0::SatisfiedAll,
RefinementPropertyPredicateV0::ExactValue {
property_name,
value: expected,
} => evaluate_exact_value_predicate_v0(property_name, expected, value),
RefinementPropertyPredicateV0::OneOfValues {
property_name,
values,
} => evaluate_one_of_values_predicate_v0(property_name, values, value),
RefinementPropertyPredicateV0::CustomPropertyReference {
property_name,
custom_property_name,
} => evaluate_custom_property_reference_predicate_v0(
property_name,
custom_property_name,
value,
),
RefinementPropertyPredicateV0::NumericRange {
property_name,
min_inclusive,
max_inclusive,
unit,
} => evaluate_numeric_range_predicate_v0(
property_name,
*min_inclusive,
*max_inclusive,
unit.as_deref(),
value,
),
RefinementPropertyPredicateV0::HasPseudoState {
property_name,
pseudo_state,
} => evaluate_pseudo_state_predicate_v0(property_name, pseudo_state, value),
RefinementPropertyPredicateV0::And { predicates } => combine_and_refinement_verdicts_v0(
&predicates
.iter()
.map(|predicate| evaluate_refinement_predicate_verdict_v0(predicate, value))
.collect::<Vec<_>>(),
),
RefinementPropertyPredicateV0::Or { predicates } => combine_or_refinement_verdicts_v0(
&predicates
.iter()
.map(|predicate| evaluate_refinement_predicate_verdict_v0(predicate, value))
.collect::<Vec<_>>(),
),
RefinementPropertyPredicateV0::Not { predicate } => {
match evaluate_refinement_predicate_verdict_v0(predicate, value) {
RefinementVerdictV0::SatisfiedAll => RefinementVerdictV0::Unsatisfiable,
RefinementVerdictV0::Unsatisfiable => RefinementVerdictV0::SatisfiedAll,
RefinementVerdictV0::SatisfiedSome | RefinementVerdictV0::Unknown => {
RefinementVerdictV0::Unknown
}
}
}
}
}
fn evaluate_numeric_range_predicate_v0(
property_name: &str,
min_inclusive: Option<i64>,
max_inclusive: Option<i64>,
unit: Option<&str>,
value: &AbstractPropertyValueV0,
) -> RefinementVerdictV0 {
match value {
AbstractPropertyValueV0::Exact {
property_name: actual_property,
value: actual_value,
..
} if actual_property == property_name => {
if numeric_range_contains_value_v0(actual_value, min_inclusive, max_inclusive, unit) {
RefinementVerdictV0::SatisfiedAll
} else {
RefinementVerdictV0::Unsatisfiable
}
}
AbstractPropertyValueV0::FiniteSet {
property_name: actual_property,
values,
..
} if actual_property == property_name => {
let matched = values
.iter()
.filter(|candidate| {
numeric_range_contains_value_v0(candidate, min_inclusive, max_inclusive, unit)
})
.count();
if matched == values.len() {
RefinementVerdictV0::SatisfiedAll
} else if matched > 0 {
RefinementVerdictV0::SatisfiedSome
} else {
RefinementVerdictV0::Unsatisfiable
}
}
AbstractPropertyValueV0::Top {
property_name: actual_property,
}
| AbstractPropertyValueV0::CustomPropertyReference {
property_name: actual_property,
..
} if actual_property == property_name => RefinementVerdictV0::Unknown,
_ => RefinementVerdictV0::Unsatisfiable,
}
}
fn evaluate_pseudo_state_predicate_v0(
property_name: &str,
expected_pseudo_state: &str,
value: &AbstractPropertyValueV0,
) -> RefinementVerdictV0 {
match value {
AbstractPropertyValueV0::Exact {
property_name: actual_property,
pseudo_state,
..
}
| AbstractPropertyValueV0::CustomPropertyReference {
property_name: actual_property,
pseudo_state,
..
} if actual_property == property_name => {
if pseudo_state.as_deref() == Some(expected_pseudo_state) {
RefinementVerdictV0::SatisfiedAll
} else {
RefinementVerdictV0::Unsatisfiable
}
}
AbstractPropertyValueV0::FiniteSet {
property_name: actual_property,
pseudo_states,
..
} if actual_property == property_name => {
if pseudo_states.len() == 1
&& pseudo_states
.iter()
.any(|pseudo_state| pseudo_state == expected_pseudo_state)
{
RefinementVerdictV0::SatisfiedAll
} else if pseudo_states
.iter()
.any(|pseudo_state| pseudo_state == expected_pseudo_state)
{
RefinementVerdictV0::SatisfiedSome
} else {
RefinementVerdictV0::Unsatisfiable
}
}
AbstractPropertyValueV0::Top {
property_name: actual_property,
} if actual_property == property_name => RefinementVerdictV0::Unknown,
_ => RefinementVerdictV0::Unsatisfiable,
}
}
fn evaluate_exact_value_predicate_v0(
property_name: &str,
expected: &str,
value: &AbstractPropertyValueV0,
) -> RefinementVerdictV0 {
match value {
AbstractPropertyValueV0::Exact {
property_name: actual_property,
value: actual_value,
..
} if actual_property == property_name && actual_value == expected => {
RefinementVerdictV0::SatisfiedAll
}
AbstractPropertyValueV0::FiniteSet {
property_name: actual_property,
values,
..
} if actual_property == property_name && values.iter().any(|value| value == expected) => {
if values.len() == 1 {
RefinementVerdictV0::SatisfiedAll
} else {
RefinementVerdictV0::SatisfiedSome
}
}
AbstractPropertyValueV0::Top {
property_name: actual_property,
}
| AbstractPropertyValueV0::CustomPropertyReference {
property_name: actual_property,
..
} if actual_property == property_name => RefinementVerdictV0::Unknown,
_ => RefinementVerdictV0::Unsatisfiable,
}
}
fn evaluate_one_of_values_predicate_v0(
property_name: &str,
expected_values: &[String],
value: &AbstractPropertyValueV0,
) -> RefinementVerdictV0 {
match value {
AbstractPropertyValueV0::Exact {
property_name: actual_property,
value: actual_value,
..
} if actual_property == property_name => {
if expected_values.contains(actual_value) {
RefinementVerdictV0::SatisfiedAll
} else {
RefinementVerdictV0::Unsatisfiable
}
}
AbstractPropertyValueV0::FiniteSet {
property_name: actual_property,
values,
..
} if actual_property == property_name => {
let matched = values
.iter()
.filter(|value| expected_values.contains(*value))
.count();
if matched == values.len() {
RefinementVerdictV0::SatisfiedAll
} else if matched > 0 {
RefinementVerdictV0::SatisfiedSome
} else {
RefinementVerdictV0::Unsatisfiable
}
}
AbstractPropertyValueV0::Top {
property_name: actual_property,
}
| AbstractPropertyValueV0::CustomPropertyReference {
property_name: actual_property,
..
} if actual_property == property_name => RefinementVerdictV0::Unknown,
_ => RefinementVerdictV0::Unsatisfiable,
}
}
fn evaluate_custom_property_reference_predicate_v0(
property_name: &str,
expected_custom_property: &str,
value: &AbstractPropertyValueV0,
) -> RefinementVerdictV0 {
match value {
AbstractPropertyValueV0::CustomPropertyReference {
property_name: actual_property,
custom_property_name,
..
} if actual_property == property_name
&& custom_property_name == expected_custom_property =>
{
RefinementVerdictV0::SatisfiedAll
}
AbstractPropertyValueV0::Top {
property_name: actual_property,
} if actual_property == property_name => RefinementVerdictV0::Unknown,
_ => RefinementVerdictV0::Unsatisfiable,
}
}
fn combine_and_refinement_verdicts_v0(verdicts: &[RefinementVerdictV0]) -> RefinementVerdictV0 {
if verdicts.is_empty()
|| verdicts
.iter()
.all(|verdict| *verdict == RefinementVerdictV0::SatisfiedAll)
{
RefinementVerdictV0::SatisfiedAll
} else if verdicts.contains(&RefinementVerdictV0::Unsatisfiable) {
RefinementVerdictV0::Unsatisfiable
} else if verdicts.contains(&RefinementVerdictV0::SatisfiedAll)
|| verdicts.contains(&RefinementVerdictV0::SatisfiedSome)
{
RefinementVerdictV0::SatisfiedSome
} else {
RefinementVerdictV0::Unknown
}
}
fn combine_or_refinement_verdicts_v0(verdicts: &[RefinementVerdictV0]) -> RefinementVerdictV0 {
if verdicts.is_empty() || verdicts.contains(&RefinementVerdictV0::SatisfiedAll) {
RefinementVerdictV0::SatisfiedAll
} else if verdicts.contains(&RefinementVerdictV0::SatisfiedSome) {
RefinementVerdictV0::SatisfiedSome
} else if verdicts
.iter()
.all(|verdict| *verdict == RefinementVerdictV0::Unsatisfiable)
{
RefinementVerdictV0::Unsatisfiable
} else {
RefinementVerdictV0::Unknown
}
}
fn count_satisfied_refinement_clauses_v0(
predicate: &RefinementPropertyPredicateV0,
value: &AbstractPropertyValueV0,
) -> usize {
match predicate {
RefinementPropertyPredicateV0::And { predicates }
| RefinementPropertyPredicateV0::Or { predicates } => predicates
.iter()
.map(|predicate| count_satisfied_refinement_clauses_v0(predicate, value))
.sum(),
RefinementPropertyPredicateV0::Not { predicate } => usize::from(matches!(
evaluate_refinement_predicate_verdict_v0(predicate, value),
RefinementVerdictV0::Unsatisfiable
)),
_ => usize::from(matches!(
evaluate_refinement_predicate_verdict_v0(predicate, value),
RefinementVerdictV0::SatisfiedAll | RefinementVerdictV0::SatisfiedSome
)),
}
}
fn refinement_predicate_expression_id_v0(predicate: &RefinementPropertyPredicateV0) -> String {
match predicate {
RefinementPropertyPredicateV0::Any => "any".to_string(),
RefinementPropertyPredicateV0::ExactValue {
property_name,
value,
} => format!("exact:{property_name}:{value}"),
RefinementPropertyPredicateV0::OneOfValues {
property_name,
values,
} => format!("one-of:{property_name}:{}", values.join("|")),
RefinementPropertyPredicateV0::CustomPropertyReference {
property_name,
custom_property_name,
} => format!("custom-ref:{property_name}:{custom_property_name}"),
RefinementPropertyPredicateV0::NumericRange {
property_name,
min_inclusive,
max_inclusive,
unit,
} => format!(
"numeric-range:{property_name}:{}..{}:{}",
min_inclusive
.map(|value| value.to_string())
.unwrap_or_else(|| "-inf".to_string()),
max_inclusive
.map(|value| value.to_string())
.unwrap_or_else(|| "inf".to_string()),
unit.as_deref().unwrap_or("*")
),
RefinementPropertyPredicateV0::HasPseudoState {
property_name,
pseudo_state,
} => format!("pseudo-state:{property_name}:{pseudo_state}"),
RefinementPropertyPredicateV0::And { predicates } => format!(
"and({})",
predicates
.iter()
.map(refinement_predicate_expression_id_v0)
.collect::<Vec<_>>()
.join(",")
),
RefinementPropertyPredicateV0::Or { predicates } => format!(
"or({})",
predicates
.iter()
.map(refinement_predicate_expression_id_v0)
.collect::<Vec<_>>()
.join(",")
),
RefinementPropertyPredicateV0::Not { predicate } => {
format!("not({})", refinement_predicate_expression_id_v0(predicate))
}
}
}
fn refinement_predicate_provenance_v0(
predicate: &RefinementPropertyPredicateV0,
) -> Vec<omena_refinement_trait::RefinementProvenanceV0> {
let mut provenance = Vec::new();
collect_refinement_predicate_provenance_v0(predicate, &mut provenance);
provenance
}
fn collect_refinement_predicate_provenance_v0(
predicate: &RefinementPropertyPredicateV0,
provenance: &mut Vec<omena_refinement_trait::RefinementProvenanceV0>,
) {
push_refinement_provenance_v0(provenance, "property-grammar", None);
match predicate {
RefinementPropertyPredicateV0::Any => {}
RefinementPropertyPredicateV0::ExactValue { .. }
| RefinementPropertyPredicateV0::OneOfValues { .. } => {
push_refinement_provenance_v0(provenance, "finite-property-domain", None);
}
RefinementPropertyPredicateV0::CustomPropertyReference { .. } => {
push_refinement_provenance_v0(provenance, "custom-property-reference", None);
}
RefinementPropertyPredicateV0::NumericRange { .. } => {
push_refinement_provenance_v0(provenance, "numeric-range-interval", None);
}
RefinementPropertyPredicateV0::HasPseudoState { .. } => {
push_refinement_provenance_v0(provenance, "pseudo-state-refinement", None);
}
RefinementPropertyPredicateV0::And { predicates }
| RefinementPropertyPredicateV0::Or { predicates } => {
push_refinement_provenance_v0(provenance, "predicate-composition", None);
for predicate in predicates {
collect_refinement_predicate_provenance_v0(predicate, provenance);
}
}
RefinementPropertyPredicateV0::Not { predicate } => {
push_refinement_provenance_v0(provenance, "predicate-composition", None);
collect_refinement_predicate_provenance_v0(predicate, provenance);
}
}
}
fn push_refinement_provenance_v0(
provenance: &mut Vec<omena_refinement_trait::RefinementProvenanceV0>,
source: &'static str,
legacy_proof_primitive: Option<&'static str>,
) {
if provenance.iter().any(|entry| {
entry.source == source && entry.legacy_proof_primitive == legacy_proof_primitive
}) {
return;
}
provenance.push(refinement_provenance_v0(source, legacy_proof_primitive));
}
fn numeric_range_contains_value_v0(
value: &str,
min_inclusive: Option<i64>,
max_inclusive: Option<i64>,
expected_unit: Option<&str>,
) -> bool {
let Some((magnitude, unit)) = parse_css_integer_with_unit_v0(value) else {
return false;
};
if let Some(expected_unit) = expected_unit
&& unit != expected_unit
{
return false;
}
if let Some(min_inclusive) = min_inclusive
&& magnitude < min_inclusive
{
return false;
}
if let Some(max_inclusive) = max_inclusive
&& magnitude > max_inclusive
{
return false;
}
true
}
fn parse_css_integer_with_unit_v0(value: &str) -> Option<(i64, &str)> {
let trimmed = value.trim();
let mut end = 0;
for (index, ch) in trimmed.char_indices() {
if ch.is_ascii_digit() || (index == 0 && (ch == '-' || ch == '+')) {
end = index + ch.len_utf8();
} else {
break;
}
}
if end == 0 || trimmed[..end].ends_with(['-', '+']) {
return None;
}
let magnitude = trimmed[..end].parse::<i64>().ok()?;
Some((magnitude, trimmed[end..].trim()))
}
fn calc_dimension_diagnostic_for_value_v0(
property_name: &str,
value: &str,
) -> Option<CalcDimensionDiagnosticV0> {
let expression = extract_calc_expression_v0(value)?;
let dimension_values = parse_dimension_vector_values_from_expression_v0(expression);
let non_number_values = dimension_values
.iter()
.filter(|entry| entry.vector != dimension_vector_number_v0())
.collect::<Vec<_>>();
if non_number_values.len() < 2 {
return None;
}
let observed_units = non_number_values
.iter()
.map(|entry| entry.unit.clone())
.collect::<BTreeSet<_>>()
.into_iter()
.collect::<Vec<_>>();
let observed_vectors = non_number_values
.iter()
.map(|entry| entry.vector)
.collect::<BTreeSet<_>>()
.into_iter()
.collect::<Vec<_>>();
let unit_families = non_number_values
.iter()
.map(|entry| entry.unit_family)
.collect::<BTreeSet<_>>();
let has_percentage = non_number_values
.iter()
.any(|entry| entry.vector.percentage != 0);
let has_non_percentage = non_number_values
.iter()
.any(|entry| entry.vector.percentage == 0);
let kind = if has_percentage && has_non_percentage {
CalcDimensionDiagnosticKindV0::ContextDependentDimension
} else if observed_vectors.len() > 1 {
CalcDimensionDiagnosticKindV0::DimensionalMismatch
} else if unit_families.len() > 1 {
CalcDimensionDiagnosticKindV0::MixedDimension
} else {
return None;
};
Some(CalcDimensionDiagnosticV0 {
schema_version: REFINEMENT_SCHEMA_VERSION_V0,
product: "omena-refinement.calc-dimension-diagnostic",
feature_gate: "calc-dimension-diagnostics-v0",
claim_level: "researchGradeHint",
theorem_claimed: false,
public_safety_claim_ready: false,
kind,
property_name: property_name.to_string(),
expression: expression.to_string(),
observed_units,
observed_vectors,
})
}
fn parse_dimension_vector_values_from_expression_v0(
expression: &str,
) -> Vec<DimensionVectorValueV0> {
expression
.split(|ch: char| {
ch.is_ascii_whitespace() || matches!(ch, '+' | '-' | '*' | '/' | '(' | ')' | ',')
})
.filter_map(parse_dimension_vector_value_v0)
.collect()
}
fn parse_dimension_vector_value_v0(value: &str) -> Option<DimensionVectorValueV0> {
let trimmed = value.trim();
if trimmed.is_empty() {
return None;
}
let (unit_start, _) = trimmed
.char_indices()
.find(|(index, ch)| {
*index > 0 && !(ch.is_ascii_digit() || *ch == '.' || *ch == '_' || *ch == '-')
})
.unwrap_or((trimmed.len(), '\0'));
if unit_start == 0 {
return None;
}
let number = trimmed[..unit_start].replace('_', "");
if number.parse::<f64>().is_err() {
return None;
}
let unit = trimmed[unit_start..].trim().to_ascii_lowercase();
let (unit_family, vector) = dimension_vector_for_unit_v0(&unit)?;
Some(DimensionVectorValueV0 {
source_value: trimmed.to_string(),
unit,
unit_family,
vector,
})
}
fn extract_calc_expression_v0(value: &str) -> Option<&str> {
let start = value.find("calc(")? + "calc(".len();
let rest = &value[start..];
let end = rest.rfind(')')?;
Some(rest[..end].trim())
}
fn dimension_vector_for_unit_v0(unit: &str) -> Option<(&'static str, DimensionVectorV0)> {
let vector = match unit {
"" => ("number", dimension_vector_number_v0()),
"%" => (
"percentage",
DimensionVectorV0 {
length: 0,
angle: 0,
time: 0,
percentage: 1,
number: 0,
},
),
"px" | "cm" | "mm" | "q" | "in" | "pt" | "pc" => {
("absoluteLength", dimension_vector_length_v0())
}
"em" | "rem" | "ex" | "ch" | "ic" | "lh" | "rlh" => {
("fontRelativeLength", dimension_vector_length_v0())
}
"vw" | "vh" | "vi" | "vb" | "vmin" | "vmax" | "svw" | "svh" | "lvw" | "lvh" | "dvw"
| "dvh" => ("viewportLength", dimension_vector_length_v0()),
"deg" | "grad" | "rad" | "turn" => (
"angle",
DimensionVectorV0 {
length: 0,
angle: 1,
time: 0,
percentage: 0,
number: 0,
},
),
"s" | "ms" => (
"time",
DimensionVectorV0 {
length: 0,
angle: 0,
time: 1,
percentage: 0,
number: 0,
},
),
_ => return None,
};
Some(vector)
}
fn dimension_vector_length_v0() -> DimensionVectorV0 {
DimensionVectorV0 {
length: 1,
angle: 0,
time: 0,
percentage: 0,
number: 0,
}
}
fn dimension_vector_number_v0() -> DimensionVectorV0 {
DimensionVectorV0 {
length: 0,
angle: 0,
time: 0,
percentage: 0,
number: 1,
}
}
fn deterministic_refinement_digest_v0(bytes: &[u8]) -> u64 {
bytes.iter().fold(0xcbf29ce484222325, |hash, byte| {
(hash ^ u64::from(*byte)).wrapping_mul(0x100000001b3)
})
}
#[cfg(feature = "refinement-smt")]
pub fn refinement_smt_backend_available_v0() -> bool {
let _ = omena_smt::cascade_theory_signature_v0();
true
}
#[cfg(not(feature = "refinement-smt"))]
pub fn refinement_smt_backend_available_v0() -> bool {
false
}
#[cfg(test)]
mod tests {
use super::*;
use omena_abstract_value::{
CascadeContextV0, CascadeValueFamilyMemberV0, derive_cascade_restriction_maps_v0,
summarize_cascade_value_family_v0,
};
#[test]
fn refined_value_round_trips_to_legacy_without_mutating_v0() {
let top = TopPredicateV0::default();
let any = AnyPropertyIndexV0::default();
assert_eq!(top.schema_version, "0");
assert_eq!(any.layer_marker, "refinement-cascade");
let legacy = AbstractPropertyValueV0::Top {
property_name: "color".to_string(),
};
let refined =
project_legacy_to_refined_v0::<AnyPropertyIndexV0, TopPredicateV0>(legacy.clone());
assert_eq!(refined.schema_version, "0");
assert_eq!(refined.layer_marker, "refinement-cascade");
assert!(refined.strict_superset_of_legacy_v0);
assert!(refined_projection_preserves_legacy_value_v0::<
AnyPropertyIndexV0,
TopPredicateV0,
>(&refined));
assert_eq!(project_refined_to_legacy_v0(&refined), legacy);
}
#[test]
fn refinement_property_grammar_evaluates_exact_and_one_of_values() {
let exact = AbstractPropertyValueV0::Exact {
property_name: "display".to_string(),
value: "grid".to_string(),
pseudo_state: None,
};
let predicate = RefinementPropertyPredicateV0::OneOfValues {
property_name: "display".to_string(),
values: vec!["grid".to_string(), "flex".to_string()],
};
let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &exact);
assert_eq!(evaluation.schema_version, "0");
assert_eq!(
evaluation.product,
"omena-refinement.property-predicate-evaluation"
);
assert_eq!(evaluation.value_shape, AbstractValueShapeV0::Exact);
assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedAll);
assert_eq!(evaluation.matched_clause_count, 1);
assert_eq!(evaluation.witness.predicate_id, "property-grammar");
assert!(evaluation.witness.legacy_proofs_byte_untouched);
}
#[test]
fn refinement_predicate_composition_tracks_partial_and_negative_witnesses() {
let finite = AbstractPropertyValueV0::FiniteSet {
property_name: "color".to_string(),
values: vec!["red".to_string(), "blue".to_string()],
pseudo_states: Vec::new(),
};
let predicate = RefinementPropertyPredicateV0::And {
predicates: vec![
RefinementPropertyPredicateV0::OneOfValues {
property_name: "color".to_string(),
values: vec!["red".to_string()],
},
RefinementPropertyPredicateV0::Not {
predicate: Box::new(RefinementPropertyPredicateV0::ExactValue {
property_name: "color".to_string(),
value: "green".to_string(),
}),
},
],
};
let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &finite);
assert_eq!(evaluation.value_shape, AbstractValueShapeV0::FiniteSet);
assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedSome);
assert_eq!(evaluation.matched_clause_count, 2);
assert_eq!(
evaluation.predicate_expression_id,
"and(one-of:color:red,not(exact:color:green))"
);
assert_eq!(evaluation.witness.provenance[0].source, "property-grammar");
}
#[test]
fn refinement_custom_property_reference_predicate_is_not_wrapper_only() {
let reference = AbstractPropertyValueV0::CustomPropertyReference {
property_name: "color".to_string(),
custom_property_name: "--brand".to_string(),
pseudo_state: None,
};
let predicate = RefinementPropertyPredicateV0::CustomPropertyReference {
property_name: "color".to_string(),
custom_property_name: "--brand".to_string(),
};
let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &reference);
assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedAll);
assert_eq!(
evaluation.predicate_expression_id,
"custom-ref:color:--brand"
);
}
#[test]
fn refinement_numeric_range_and_pseudo_state_predicates_are_evaluated() {
let finite = AbstractPropertyValueV0::FiniteSet {
property_name: "opacity".to_string(),
values: vec!["0".to_string(), "50%".to_string(), "100%".to_string()],
pseudo_states: vec![":hover".to_string(), ":focus".to_string()],
};
let predicate = RefinementPropertyPredicateV0::And {
predicates: vec![
RefinementPropertyPredicateV0::NumericRange {
property_name: "opacity".to_string(),
min_inclusive: Some(0),
max_inclusive: Some(100),
unit: Some("%".to_string()),
},
RefinementPropertyPredicateV0::HasPseudoState {
property_name: "opacity".to_string(),
pseudo_state: ":hover".to_string(),
},
],
};
let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &finite);
assert_eq!(evaluation.value_shape, AbstractValueShapeV0::FiniteSet);
assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedSome);
assert_eq!(
evaluation.predicate_expression_id,
"and(numeric-range:opacity:0..100:%,pseudo-state:opacity::hover)"
);
assert!(
evaluation
.witness
.provenance
.iter()
.any(|entry| entry.source == "numeric-range-interval")
);
assert!(
evaluation
.witness
.provenance
.iter()
.any(|entry| entry.source == "pseudo-state-refinement")
);
assert!(
evaluation
.witness
.provenance
.iter()
.any(|entry| entry.source == "predicate-composition")
);
}
#[test]
fn refinement_context_digest_is_order_stable_and_invalidation_sensitive() {
let range = RefinementPropertyPredicateV0::NumericRange {
property_name: "z-index".to_string(),
min_inclusive: Some(0),
max_inclusive: Some(10),
unit: None,
};
let exact = RefinementPropertyPredicateV0::ExactValue {
property_name: "display".to_string(),
value: "grid".to_string(),
};
let first = summarize_refinement_context_v0(&[range.clone(), exact.clone()]);
let reordered = summarize_refinement_context_v0(&[exact.clone(), range.clone()]);
let changed = summarize_refinement_context_v0(&[
exact,
RefinementPropertyPredicateV0::NumericRange {
property_name: "z-index".to_string(),
min_inclusive: Some(0),
max_inclusive: Some(11),
unit: None,
},
]);
assert_eq!(first.schema_version, "0");
assert_eq!(first.product, "omena-refinement.context-summary");
assert_eq!(first.predicate_count, 2);
assert!(first.downstream_invalidation_required);
assert_eq!(first.context_digest, reordered.context_digest);
assert_ne!(first.context_digest, changed.context_digest);
assert!(first.witness_provenance_count >= 3);
}
#[test]
fn cascade_dimensional_refinement_bridge_reuses_existing_substrates() {
let members = vec![
CascadeValueFamilyMemberV0 {
context: CascadeContextV0 {
id: "base".to_string(),
parent_id: None,
selectors: vec![":root".to_string()],
conditions: Vec::new(),
layers: vec!["tokens".to_string()],
},
value: AbstractPropertyValueV0::Exact {
property_name: "width".to_string(),
value: "12px".to_string(),
pseudo_state: None,
},
},
CascadeValueFamilyMemberV0 {
context: CascadeContextV0 {
id: "fluid".to_string(),
parent_id: Some("base".to_string()),
selectors: vec![":root".to_string()],
conditions: vec!["@media (orientation: portrait)".to_string()],
layers: vec!["tokens".to_string()],
},
value: AbstractPropertyValueV0::Exact {
property_name: "width".to_string(),
value: "50%".to_string(),
pseudo_state: None,
},
},
CascadeValueFamilyMemberV0 {
context: CascadeContextV0 {
id: "unknown".to_string(),
parent_id: Some("base".to_string()),
selectors: vec![":root".to_string()],
conditions: vec!["@container card".to_string()],
layers: vec!["tokens".to_string()],
},
value: AbstractPropertyValueV0::Top {
property_name: "width".to_string(),
},
},
];
let restrictions = derive_cascade_restriction_maps_v0(&members);
let family = summarize_cascade_value_family_v0("width", members, restrictions);
let predicate = RefinementPropertyPredicateV0::NumericRange {
property_name: "width".to_string(),
min_inclusive: Some(0),
max_inclusive: Some(100),
unit: Some("px".to_string()),
};
let bridge = summarize_cascade_dimensional_refinement_bridge_v0(&family, &[predicate]);
assert_eq!(
bridge.product,
"omena-refinement.cascade-dimensional-refinement-bridge"
);
assert_eq!(bridge.claim_level, REFINEMENT_BRIDGE_CLAIM_LEVEL_V0);
assert_eq!(bridge.cascade_family_product, family.product);
assert_eq!(bridge.context_evaluation_count, 3);
assert_eq!(bridge.restriction_map_count, 2);
assert_eq!(bridge.satisfied_all_context_count, 1);
assert_eq!(bridge.unsatisfiable_context_count, 1);
assert_eq!(bridge.unknown_context_count, 1);
assert_eq!(bridge.witness_provenance_count, 2);
assert!(bridge.uses_existing_abstract_property_value_substrate);
assert!(bridge.uses_existing_cascade_family_substrate);
assert!(bridge.uses_existing_refinement_predicate_substrate);
assert!(!bridge.forks_unit_system);
assert!(!bridge.liquid_haskell_complete);
assert!(!bridge.smt_complete);
assert!(!bridge.theorem_claimed);
assert!(bridge.product_path_evidence_ready);
assert!(!bridge.stronger_type_safety_claim_ready);
assert!(bridge.dimension_vector_domain_ready);
assert!(bridge.calc_dimension_diagnostics_ready);
assert!(!bridge.dimension_vector_domain.forks_unit_system);
assert!(!bridge.dimension_vector_domain.theorem_claimed);
assert_eq!(bridge.dimension_vector_domain.value_count, 2);
assert_eq!(bridge.calc_dimension_diagnostics.diagnostic_count, 0);
assert!(!bridge.calc_dimension_diagnostics.smt_complete);
assert!(!bridge.calc_dimension_diagnostics.liquid_haskell_complete);
assert!(
!bridge
.calc_dimension_diagnostics
.stronger_type_safety_claim_ready
);
assert_eq!(bridge.evaluations[0].context_id, "base");
assert_eq!(
bridge.evaluations[0].combined_verdict,
RefinementVerdictV0::SatisfiedAll
);
assert_eq!(
bridge.evaluations[0].predicate_expression_ids,
vec!["numeric-range:width:0..100:px".to_string()]
);
}
#[test]
fn calc_dimension_diagnostics_classify_fixture_mismatches_without_unit_fork() {
let values = vec![
"calc(1px + 2s)".to_string(),
"calc(1px + 2rem)".to_string(),
"calc(100% - 1rem)".to_string(),
"calc(1px + 2px)".to_string(),
];
let domain = summarize_dimension_vector_domain_v0(&values);
let diagnostics = summarize_calc_dimension_diagnostics_v0("width", &values);
assert_eq!(domain.product, "omena-refinement.dimension-vector-domain");
assert_eq!(domain.feature_gate, "dimension-vector-domain-v0");
assert_eq!(domain.claim_level, "fixtureWitnessDimensionVectorDomain");
assert!(!domain.forks_unit_system);
assert!(!domain.theorem_claimed);
assert!(domain.vector_count >= 3);
assert_eq!(
diagnostics.product,
"omena-refinement.calc-dimension-diagnostics"
);
assert_eq!(diagnostics.feature_gate, "calc-dimension-diagnostics-v0");
assert_eq!(diagnostics.claim_level, "researchGradeHint");
assert!(!diagnostics.forks_unit_system);
assert!(!diagnostics.smt_complete);
assert!(!diagnostics.liquid_haskell_complete);
assert!(!diagnostics.stronger_type_safety_claim_ready);
assert!(!diagnostics.theorem_claimed);
assert_eq!(diagnostics.diagnostic_count, 3);
assert!(diagnostics.diagnostics.iter().any(|diagnostic| {
diagnostic.kind == CalcDimensionDiagnosticKindV0::DimensionalMismatch
&& diagnostic.expression == "1px + 2s"
}));
assert!(diagnostics.diagnostics.iter().any(|diagnostic| {
diagnostic.kind == CalcDimensionDiagnosticKindV0::MixedDimension
&& diagnostic.expression == "1px + 2rem"
}));
assert!(diagnostics.diagnostics.iter().any(|diagnostic| {
diagnostic.kind == CalcDimensionDiagnosticKindV0::ContextDependentDimension
&& diagnostic.expression == "100% - 1rem"
}));
}
}