1use std::{collections::BTreeSet, marker::PhantomData};
11
12use omena_abstract_value::{AbstractPropertyValueV0, CascadeValueFamilyV0};
13use omena_cascade::{
14 CascadeDeclaration, CascadeRefinementContextV0,
15 refine_declaration_in_context as refine_cascade_declaration_in_context,
16};
17use omena_refinement_trait::{
18 PropertyIndexV0, REFINEMENT_FEATURE_GATE_V0, REFINEMENT_LAYER_MARKER_V0,
19 REFINEMENT_SCHEMA_VERSION_V0, RefinementPredicateV0, RefinementVerdictV0, RefinementWitnessV0,
20 refinement_provenance_v0, refinement_witness_v0,
21};
22use omena_syntax::ident::{AuthoredPropertyTextV0, PropertyNameV0};
23use serde::Serialize;
24
25pub const REFINEMENT_BRIDGE_CLAIM_LEVEL_V0: &str = "m6DimensionalRefinementBridgeSubstrate";
26
27fn authored_property_same(left: &AuthoredPropertyTextV0, right: &AuthoredPropertyTextV0) -> bool {
28 left.to_property_name().same_as(&right.to_property_name())
29}
30
31fn property_names_same(left: &AuthoredPropertyTextV0, right: &AuthoredPropertyTextV0) -> bool {
32 authored_property_same(left, right)
33}
34
35#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
36#[serde(rename_all = "camelCase")]
37pub enum AbstractValueShapeV0 {
38 Bottom,
39 Exact,
40 FiniteSet,
41 CustomPropertyReference,
42 Top,
43}
44
45#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
46#[serde(rename_all = "camelCase")]
47pub struct TopPredicateV0 {
48 pub schema_version: &'static str,
49 pub product: &'static str,
50 pub layer_marker: &'static str,
51 pub feature_gate: &'static str,
52}
53
54impl Default for TopPredicateV0 {
55 fn default() -> Self {
56 Self {
57 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
58 product: "omena-refinement.top-predicate",
59 layer_marker: REFINEMENT_LAYER_MARKER_V0,
60 feature_gate: REFINEMENT_FEATURE_GATE_V0,
61 }
62 }
63}
64
65impl RefinementPredicateV0 for TopPredicateV0 {
66 const PREDICATE_ID: &'static str = "top";
67}
68
69#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
70#[serde(rename_all = "camelCase")]
71pub struct AnyPropertyIndexV0 {
72 pub schema_version: &'static str,
73 pub product: &'static str,
74 pub layer_marker: &'static str,
75 pub feature_gate: &'static str,
76}
77
78impl Default for AnyPropertyIndexV0 {
79 fn default() -> Self {
80 Self {
81 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
82 product: "omena-refinement.any-property-index",
83 layer_marker: REFINEMENT_LAYER_MARKER_V0,
84 feature_gate: REFINEMENT_FEATURE_GATE_V0,
85 }
86 }
87}
88
89impl PropertyIndexV0 for AnyPropertyIndexV0 {
90 const PROPERTY_NAME: &'static str = "*";
91}
92
93#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
94#[serde(rename_all = "camelCase", bound = "")]
95pub struct RefinedAbstractPropertyValueV0<P: PropertyIndexV0, R: RefinementPredicateV0> {
96 pub schema_version: &'static str,
97 pub product: &'static str,
98 pub layer_marker: &'static str,
99 pub feature_gate: &'static str,
100 pub property_name: &'static str,
101 pub predicate_id: &'static str,
102 pub value_shape: AbstractValueShapeV0,
103 pub legacy_value: AbstractPropertyValueV0,
104 pub strict_superset_of_legacy_v0: bool,
105 #[serde(skip)]
106 marker: PhantomData<(P, R)>,
107}
108
109#[derive(Debug, Clone, Serialize)]
110#[serde(rename_all = "camelCase")]
111pub enum RefinementPropertyPredicateV0 {
112 Any,
113 ExactValue {
114 property_name: AuthoredPropertyTextV0,
115 value: String,
116 },
117 OneOfValues {
118 property_name: AuthoredPropertyTextV0,
119 values: Vec<String>,
120 },
121 CustomPropertyReference {
122 property_name: AuthoredPropertyTextV0,
123 custom_property_name: AuthoredPropertyTextV0,
124 },
125 NumericRange {
126 property_name: AuthoredPropertyTextV0,
127 min_inclusive: Option<i64>,
128 max_inclusive: Option<i64>,
129 unit: Option<String>,
130 },
131 HasPseudoState {
132 property_name: AuthoredPropertyTextV0,
133 pseudo_state: String,
134 },
135 And {
136 predicates: Vec<RefinementPropertyPredicateV0>,
137 },
138 Or {
139 predicates: Vec<RefinementPropertyPredicateV0>,
140 },
141 Not {
142 predicate: Box<RefinementPropertyPredicateV0>,
143 },
144}
145
146impl PartialEq for RefinementPropertyPredicateV0 {
147 fn eq(&self, other: &Self) -> bool {
148 match (self, other) {
149 (Self::Any, Self::Any) => true,
150 (
151 Self::ExactValue {
152 property_name: left_property,
153 value: left_value,
154 },
155 Self::ExactValue {
156 property_name: right_property,
157 value: right_value,
158 },
159 ) => authored_property_same(left_property, right_property) && left_value == right_value,
160 (
161 Self::OneOfValues {
162 property_name: left_property,
163 values: left_values,
164 },
165 Self::OneOfValues {
166 property_name: right_property,
167 values: right_values,
168 },
169 ) => {
170 authored_property_same(left_property, right_property) && left_values == right_values
171 }
172 (
173 Self::CustomPropertyReference {
174 property_name: left_property,
175 custom_property_name: left_custom_property,
176 },
177 Self::CustomPropertyReference {
178 property_name: right_property,
179 custom_property_name: right_custom_property,
180 },
181 ) => {
182 authored_property_same(left_property, right_property)
183 && left_custom_property.to_custom_key() == right_custom_property.to_custom_key()
184 }
185 (
186 Self::NumericRange {
187 property_name: left_property,
188 min_inclusive: left_min,
189 max_inclusive: left_max,
190 unit: left_unit,
191 },
192 Self::NumericRange {
193 property_name: right_property,
194 min_inclusive: right_min,
195 max_inclusive: right_max,
196 unit: right_unit,
197 },
198 ) => {
199 authored_property_same(left_property, right_property)
200 && left_min == right_min
201 && left_max == right_max
202 && left_unit == right_unit
203 }
204 (
205 Self::HasPseudoState {
206 property_name: left_property,
207 pseudo_state: left_pseudo_state,
208 },
209 Self::HasPseudoState {
210 property_name: right_property,
211 pseudo_state: right_pseudo_state,
212 },
213 ) => {
214 authored_property_same(left_property, right_property)
215 && left_pseudo_state == right_pseudo_state
216 }
217 (Self::And { predicates: left }, Self::And { predicates: right })
218 | (Self::Or { predicates: left }, Self::Or { predicates: right }) => left == right,
219 (Self::Not { predicate: left }, Self::Not { predicate: right }) => left == right,
220 _ => false,
221 }
222 }
223}
224
225impl Eq for RefinementPropertyPredicateV0 {}
226
227#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
228#[serde(rename_all = "camelCase")]
229pub struct RefinementPredicateEvaluationV0 {
230 pub schema_version: &'static str,
231 pub product: &'static str,
232 pub layer_marker: &'static str,
233 pub feature_gate: &'static str,
234 pub predicate_expression_id: String,
235 pub value_shape: AbstractValueShapeV0,
236 pub verdict: RefinementVerdictV0,
237 pub matched_clause_count: usize,
238 pub witness: RefinementWitnessV0,
239}
240
241#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
242#[serde(rename_all = "camelCase")]
243pub struct RefinementContextSummaryV0 {
244 pub schema_version: &'static str,
245 pub product: &'static str,
246 pub layer_marker: &'static str,
247 pub feature_gate: &'static str,
248 pub predicate_count: usize,
249 pub context_digest: u64,
250 pub witness_provenance_count: usize,
251 pub downstream_invalidation_required: bool,
252}
253
254#[derive(Debug, Clone, Serialize)]
260#[serde(rename_all = "camelCase")]
261pub struct CascadeDimensionalRefinementBridgeV0 {
262 pub schema_version: &'static str,
263 pub product: &'static str,
264 pub layer_marker: &'static str,
265 pub feature_gate: &'static str,
266 pub claim_level: &'static str,
267 pub property_name: AuthoredPropertyTextV0,
268 pub cascade_family_product: &'static str,
269 pub predicate_count: usize,
270 pub context_value_count: usize,
271 pub restriction_map_count: usize,
272 pub context_evaluation_count: usize,
273 pub satisfied_all_context_count: usize,
274 pub satisfied_some_context_count: usize,
275 pub unknown_context_count: usize,
276 pub unsatisfiable_context_count: usize,
277 pub witness_provenance_count: usize,
278 pub property_consistent: bool,
279 pub uses_existing_abstract_property_value_substrate: bool,
280 pub uses_existing_cascade_family_substrate: bool,
281 pub uses_existing_refinement_predicate_substrate: bool,
282 pub forks_unit_system: bool,
283 pub liquid_haskell_complete: bool,
284 pub smt_backend_available: bool,
285 pub smt_complete: bool,
286 pub theorem_claimed: bool,
287 pub product_path_evidence_ready: bool,
288 pub stronger_type_safety_claim_ready: bool,
289 pub dimension_vector_domain_ready: bool,
290 pub calc_dimension_diagnostics_ready: bool,
291 pub dimension_vector_domain: DimensionVectorDomainSummaryV0,
292 pub calc_dimension_diagnostics: CalcDimensionDiagnosticSummaryV0,
293 pub evaluations: Vec<CascadeDimensionalRefinementContextEvaluationV0>,
294}
295
296impl PartialEq for CascadeDimensionalRefinementBridgeV0 {
297 fn eq(&self, other: &Self) -> bool {
298 self.schema_version == other.schema_version
299 && self.product == other.product
300 && self.layer_marker == other.layer_marker
301 && self.feature_gate == other.feature_gate
302 && self.claim_level == other.claim_level
303 && authored_property_same(&self.property_name, &other.property_name)
304 && self.cascade_family_product == other.cascade_family_product
305 && self.predicate_count == other.predicate_count
306 && self.context_value_count == other.context_value_count
307 && self.restriction_map_count == other.restriction_map_count
308 && self.context_evaluation_count == other.context_evaluation_count
309 && self.satisfied_all_context_count == other.satisfied_all_context_count
310 && self.satisfied_some_context_count == other.satisfied_some_context_count
311 && self.unknown_context_count == other.unknown_context_count
312 && self.unsatisfiable_context_count == other.unsatisfiable_context_count
313 && self.witness_provenance_count == other.witness_provenance_count
314 && self.property_consistent == other.property_consistent
315 && self.uses_existing_abstract_property_value_substrate
316 == other.uses_existing_abstract_property_value_substrate
317 && self.uses_existing_cascade_family_substrate
318 == other.uses_existing_cascade_family_substrate
319 && self.uses_existing_refinement_predicate_substrate
320 == other.uses_existing_refinement_predicate_substrate
321 && self.forks_unit_system == other.forks_unit_system
322 && self.liquid_haskell_complete == other.liquid_haskell_complete
323 && self.smt_backend_available == other.smt_backend_available
324 && self.smt_complete == other.smt_complete
325 && self.theorem_claimed == other.theorem_claimed
326 && self.product_path_evidence_ready == other.product_path_evidence_ready
327 && self.stronger_type_safety_claim_ready == other.stronger_type_safety_claim_ready
328 && self.dimension_vector_domain_ready == other.dimension_vector_domain_ready
329 && self.calc_dimension_diagnostics_ready == other.calc_dimension_diagnostics_ready
330 && self.dimension_vector_domain == other.dimension_vector_domain
331 && self.calc_dimension_diagnostics == other.calc_dimension_diagnostics
332 && self.evaluations == other.evaluations
333 }
334}
335
336impl Eq for CascadeDimensionalRefinementBridgeV0 {}
337
338#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Serialize)]
339#[serde(rename_all = "camelCase")]
340pub struct DimensionVectorV0 {
341 pub length: i8,
342 pub angle: i8,
343 pub time: i8,
344 pub percentage: i8,
345 pub number: i8,
346}
347
348#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
349#[serde(rename_all = "camelCase")]
350pub struct DimensionVectorValueV0 {
351 pub source_value: String,
352 pub unit: String,
353 pub unit_family: &'static str,
354 pub vector: DimensionVectorV0,
355}
356
357#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
358#[serde(rename_all = "camelCase")]
359pub struct DimensionVectorDomainSummaryV0 {
360 pub schema_version: &'static str,
361 pub product: &'static str,
362 pub feature_gate: &'static str,
363 pub claim_level: &'static str,
364 pub theorem_claimed: bool,
365 pub forks_unit_system: bool,
366 pub value_count: usize,
367 pub vector_count: usize,
368 pub values: Vec<DimensionVectorValueV0>,
369}
370
371#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize)]
372#[serde(rename_all = "camelCase")]
373pub enum CalcDimensionDiagnosticKindV0 {
374 DimensionalMismatch,
375 MixedDimension,
376 ContextDependentDimension,
377}
378
379#[derive(Debug, Clone, Serialize)]
380#[serde(rename_all = "camelCase")]
381pub struct CalcDimensionDiagnosticV0 {
382 pub schema_version: &'static str,
383 pub product: &'static str,
384 pub feature_gate: &'static str,
385 pub claim_level: &'static str,
386 pub theorem_claimed: bool,
387 pub public_safety_claim_ready: bool,
388 pub kind: CalcDimensionDiagnosticKindV0,
389 pub property_name: AuthoredPropertyTextV0,
390 pub expression: String,
391 pub observed_units: Vec<String>,
392 pub observed_vectors: Vec<DimensionVectorV0>,
393}
394
395impl PartialEq for CalcDimensionDiagnosticV0 {
396 fn eq(&self, other: &Self) -> bool {
397 self.schema_version == other.schema_version
398 && self.product == other.product
399 && self.feature_gate == other.feature_gate
400 && self.claim_level == other.claim_level
401 && self.theorem_claimed == other.theorem_claimed
402 && self.public_safety_claim_ready == other.public_safety_claim_ready
403 && self.kind == other.kind
404 && authored_property_same(&self.property_name, &other.property_name)
405 && self.expression == other.expression
406 && self.observed_units == other.observed_units
407 && self.observed_vectors == other.observed_vectors
408 }
409}
410
411impl Eq for CalcDimensionDiagnosticV0 {}
412
413#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
414#[serde(rename_all = "camelCase")]
415pub struct CalcDimensionDiagnosticSummaryV0 {
416 pub schema_version: &'static str,
417 pub product: &'static str,
418 pub feature_gate: &'static str,
419 pub claim_level: &'static str,
420 pub theorem_claimed: bool,
421 pub forks_unit_system: bool,
422 pub smt_complete: bool,
423 pub liquid_haskell_complete: bool,
424 pub stronger_type_safety_claim_ready: bool,
425 pub diagnostic_count: usize,
426 pub diagnostics: Vec<CalcDimensionDiagnosticV0>,
427}
428
429#[derive(Debug, Clone, PartialEq, Eq, Serialize)]
430#[serde(rename_all = "camelCase")]
431pub struct CascadeDimensionalRefinementContextEvaluationV0 {
432 pub schema_version: &'static str,
433 pub product: &'static str,
434 pub layer_marker: &'static str,
435 pub feature_gate: &'static str,
436 pub context_id: String,
437 pub selector_count: usize,
438 pub condition_count: usize,
439 pub layer_count: usize,
440 pub value_shape: AbstractValueShapeV0,
441 pub combined_verdict: RefinementVerdictV0,
442 pub predicate_evaluation_count: usize,
443 pub matched_clause_count: usize,
444 pub witness_provenance_count: usize,
445 pub predicate_expression_ids: Vec<String>,
446}
447
448pub fn project_legacy_to_refined_v0<P, R>(
449 legacy_value: AbstractPropertyValueV0,
450) -> RefinedAbstractPropertyValueV0<P, R>
451where
452 P: PropertyIndexV0,
453 R: RefinementPredicateV0,
454{
455 let mut refined = RefinedAbstractPropertyValueV0 {
456 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
457 product: "omena-refinement.refined-abstract-property-value",
458 layer_marker: REFINEMENT_LAYER_MARKER_V0,
459 feature_gate: REFINEMENT_FEATURE_GATE_V0,
460 property_name: P::PROPERTY_NAME,
461 predicate_id: R::PREDICATE_ID,
462 value_shape: abstract_property_value_shape_v0(&legacy_value),
463 legacy_value,
464 strict_superset_of_legacy_v0: false,
465 marker: PhantomData,
466 };
467 refined.strict_superset_of_legacy_v0 =
468 refined_projection_preserves_legacy_value_v0::<P, R>(&refined);
469 refined
470}
471
472pub fn project_refined_to_legacy_v0<P, R>(
473 refined: &RefinedAbstractPropertyValueV0<P, R>,
474) -> AbstractPropertyValueV0
475where
476 P: PropertyIndexV0,
477 R: RefinementPredicateV0,
478{
479 refined.legacy_value.clone()
480}
481
482pub fn refined_projection_preserves_legacy_value_v0<P, R>(
483 refined: &RefinedAbstractPropertyValueV0<P, R>,
484) -> bool
485where
486 P: PropertyIndexV0,
487 R: RefinementPredicateV0,
488{
489 refined.schema_version == REFINEMENT_SCHEMA_VERSION_V0
490 && refined.layer_marker == REFINEMENT_LAYER_MARKER_V0
491 && refined.feature_gate == REFINEMENT_FEATURE_GATE_V0
492 && PropertyNameV0::canonical_standard_key(refined.property_name)
493 == PropertyNameV0::canonical_standard_key(P::PROPERTY_NAME)
494 && refined.predicate_id == R::PREDICATE_ID
495 && abstract_property_value_shape_v0(&project_refined_to_legacy_v0(refined))
496 == refined.value_shape
497}
498
499pub fn evaluate_refinement_property_predicate_v0(
500 predicate: &RefinementPropertyPredicateV0,
501 value: &AbstractPropertyValueV0,
502) -> RefinementPredicateEvaluationV0 {
503 let verdict = evaluate_refinement_predicate_verdict_v0(predicate, value);
504 let matched_clause_count = count_satisfied_refinement_clauses_v0(predicate, value);
505 let predicate_expression_id = refinement_predicate_expression_id_v0(predicate);
506 let witness = refinement_witness_v0(
507 "property-grammar",
508 verdict,
509 refinement_predicate_provenance_v0(predicate),
510 );
511
512 RefinementPredicateEvaluationV0 {
513 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
514 product: "omena-refinement.property-predicate-evaluation",
515 layer_marker: REFINEMENT_LAYER_MARKER_V0,
516 feature_gate: REFINEMENT_FEATURE_GATE_V0,
517 predicate_expression_id,
518 value_shape: abstract_property_value_shape_v0(value),
519 verdict,
520 matched_clause_count,
521 witness,
522 }
523}
524
525pub fn refine_declaration_in_context(
526 declaration: &CascadeDeclaration,
527 context: &CascadeRefinementContextV0,
528) -> RefinementWitnessV0 {
529 refine_cascade_declaration_in_context(declaration, context)
530}
531
532pub fn summarize_refinement_context_v0(
533 predicates: &[RefinementPropertyPredicateV0],
534) -> RefinementContextSummaryV0 {
535 let mut expression_ids = predicates
536 .iter()
537 .map(refinement_predicate_expression_id_v0)
538 .collect::<Vec<_>>();
539 expression_ids.sort();
540
541 let witness_provenance_count = predicates
542 .iter()
543 .flat_map(refinement_predicate_provenance_v0)
544 .map(|provenance| provenance.source)
545 .collect::<std::collections::BTreeSet<_>>()
546 .len();
547 let context_digest = deterministic_refinement_digest_v0(expression_ids.join("\n").as_bytes());
548
549 RefinementContextSummaryV0 {
550 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
551 product: "omena-refinement.context-summary",
552 layer_marker: REFINEMENT_LAYER_MARKER_V0,
553 feature_gate: REFINEMENT_FEATURE_GATE_V0,
554 predicate_count: predicates.len(),
555 context_digest,
556 witness_provenance_count,
557 downstream_invalidation_required: !predicates.is_empty(),
558 }
559}
560
561pub fn summarize_dimension_vector_domain_v0(values: &[String]) -> DimensionVectorDomainSummaryV0 {
562 let mut entries = values
563 .iter()
564 .flat_map(|value| {
565 extract_calc_expression_v0(value)
566 .map(parse_dimension_vector_values_from_expression_v0)
567 .unwrap_or_else(|| parse_dimension_vector_value_v0(value).into_iter().collect())
568 })
569 .collect::<Vec<_>>();
570 entries.sort_by(|left, right| {
571 left.source_value
572 .cmp(&right.source_value)
573 .then_with(|| left.unit.cmp(&right.unit))
574 });
575 entries.dedup_by(|left, right| {
576 left.source_value == right.source_value
577 && left.unit == right.unit
578 && left.unit_family == right.unit_family
579 && left.vector == right.vector
580 });
581 let vector_count = entries
582 .iter()
583 .map(|entry| entry.vector)
584 .collect::<BTreeSet<_>>()
585 .len();
586
587 DimensionVectorDomainSummaryV0 {
588 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
589 product: "omena-refinement.dimension-vector-domain",
590 feature_gate: "dimension-vector-domain-v0",
591 claim_level: "fixtureWitnessDimensionVectorDomain",
592 theorem_claimed: false,
593 forks_unit_system: false,
594 value_count: entries.len(),
595 vector_count,
596 values: entries,
597 }
598}
599
600pub fn summarize_calc_dimension_diagnostics_v0(
601 property_name: &AuthoredPropertyTextV0,
602 values: &[String],
603) -> CalcDimensionDiagnosticSummaryV0 {
604 let mut diagnostics = values
605 .iter()
606 .filter_map(|value| calc_dimension_diagnostic_for_value_v0(property_name, value))
607 .collect::<Vec<_>>();
608 diagnostics.sort_by(|left, right| {
609 left.property_name
610 .to_property_name()
611 .canonical_key()
612 .cmp(&right.property_name.to_property_name().canonical_key())
613 .then_with(|| left.expression.cmp(&right.expression))
614 });
615
616 CalcDimensionDiagnosticSummaryV0 {
617 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
618 product: "omena-refinement.calc-dimension-diagnostics",
619 feature_gate: "calc-dimension-diagnostics-v0",
620 claim_level: "researchGradeHint",
621 theorem_claimed: false,
622 forks_unit_system: false,
623 smt_complete: false,
624 liquid_haskell_complete: false,
625 stronger_type_safety_claim_ready: false,
626 diagnostic_count: diagnostics.len(),
627 diagnostics,
628 }
629}
630
631pub fn summarize_cascade_dimensional_refinement_bridge_v0(
632 family: &CascadeValueFamilyV0,
633 predicates: &[RefinementPropertyPredicateV0],
634) -> CascadeDimensionalRefinementBridgeV0 {
635 let exact_values = family
636 .members
637 .iter()
638 .filter_map(|member| match &member.value {
639 AbstractPropertyValueV0::Exact { value, .. } => Some(value.clone()),
640 _ => None,
641 })
642 .collect::<Vec<_>>();
643 let dimension_vector_domain = summarize_dimension_vector_domain_v0(&exact_values);
644 let calc_dimension_diagnostics =
645 summarize_calc_dimension_diagnostics_v0(&family.property_name, &exact_values);
646 let mut global_provenance_sources = BTreeSet::new();
647 let mut evaluations = family
648 .members
649 .iter()
650 .map(|member| {
651 let predicate_evaluations = predicates
652 .iter()
653 .map(|predicate| {
654 evaluate_refinement_property_predicate_v0(predicate, &member.value)
655 })
656 .collect::<Vec<_>>();
657 let verdicts = predicate_evaluations
658 .iter()
659 .map(|evaluation| evaluation.verdict)
660 .collect::<Vec<_>>();
661 let combined_verdict = combine_and_refinement_verdicts_v0(&verdicts);
662 let mut context_provenance_sources = BTreeSet::new();
663 for evaluation in &predicate_evaluations {
664 for provenance in &evaluation.witness.provenance {
665 context_provenance_sources.insert(provenance.source);
666 global_provenance_sources.insert(provenance.source);
667 }
668 }
669
670 CascadeDimensionalRefinementContextEvaluationV0 {
671 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
672 product: "omena-refinement.cascade-dimensional-refinement-context-evaluation",
673 layer_marker: REFINEMENT_LAYER_MARKER_V0,
674 feature_gate: REFINEMENT_FEATURE_GATE_V0,
675 context_id: member.context.id.clone(),
676 selector_count: member.context.selectors.len(),
677 condition_count: member.context.conditions.len(),
678 layer_count: member.context.layers.len(),
679 value_shape: abstract_property_value_shape_v0(&member.value),
680 combined_verdict,
681 predicate_evaluation_count: predicate_evaluations.len(),
682 matched_clause_count: predicate_evaluations
683 .iter()
684 .map(|evaluation| evaluation.matched_clause_count)
685 .sum(),
686 witness_provenance_count: context_provenance_sources.len(),
687 predicate_expression_ids: predicate_evaluations
688 .into_iter()
689 .map(|evaluation| evaluation.predicate_expression_id)
690 .collect(),
691 }
692 })
693 .collect::<Vec<_>>();
694 evaluations.sort_by(|left, right| left.context_id.cmp(&right.context_id));
695
696 CascadeDimensionalRefinementBridgeV0 {
697 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
698 product: "omena-refinement.cascade-dimensional-refinement-bridge",
699 layer_marker: REFINEMENT_LAYER_MARKER_V0,
700 feature_gate: REFINEMENT_FEATURE_GATE_V0,
701 claim_level: REFINEMENT_BRIDGE_CLAIM_LEVEL_V0,
702 property_name: family.property_name.clone(),
703 cascade_family_product: family.product,
704 predicate_count: predicates.len(),
705 context_value_count: family.context_value_count,
706 restriction_map_count: family.restriction_map_count,
707 context_evaluation_count: evaluations.len(),
708 satisfied_all_context_count: count_context_verdicts_v0(
709 &evaluations,
710 RefinementVerdictV0::SatisfiedAll,
711 ),
712 satisfied_some_context_count: count_context_verdicts_v0(
713 &evaluations,
714 RefinementVerdictV0::SatisfiedSome,
715 ),
716 unknown_context_count: count_context_verdicts_v0(
717 &evaluations,
718 RefinementVerdictV0::Unknown,
719 ),
720 unsatisfiable_context_count: count_context_verdicts_v0(
721 &evaluations,
722 RefinementVerdictV0::Unsatisfiable,
723 ),
724 witness_provenance_count: global_provenance_sources.len(),
725 property_consistent: family.property_consistent,
726 uses_existing_abstract_property_value_substrate: true,
727 uses_existing_cascade_family_substrate: true,
728 uses_existing_refinement_predicate_substrate: true,
729 forks_unit_system: false,
730 liquid_haskell_complete: false,
731 smt_backend_available: refinement_smt_backend_available_v0(),
732 smt_complete: false,
733 theorem_claimed: false,
734 product_path_evidence_ready: true,
735 stronger_type_safety_claim_ready: false,
736 dimension_vector_domain_ready: dimension_vector_domain.value_count > 0
737 && !dimension_vector_domain.forks_unit_system
738 && !dimension_vector_domain.theorem_claimed,
739 calc_dimension_diagnostics_ready: !calc_dimension_diagnostics.forks_unit_system
740 && !calc_dimension_diagnostics.smt_complete
741 && !calc_dimension_diagnostics.liquid_haskell_complete
742 && !calc_dimension_diagnostics.stronger_type_safety_claim_ready
743 && !calc_dimension_diagnostics.theorem_claimed,
744 dimension_vector_domain,
745 calc_dimension_diagnostics,
746 evaluations,
747 }
748}
749
750pub fn abstract_property_value_shape_v0(value: &AbstractPropertyValueV0) -> AbstractValueShapeV0 {
751 match value {
752 AbstractPropertyValueV0::Bottom { .. } => AbstractValueShapeV0::Bottom,
753 AbstractPropertyValueV0::Exact { .. } => AbstractValueShapeV0::Exact,
754 AbstractPropertyValueV0::FiniteSet { .. } => AbstractValueShapeV0::FiniteSet,
755 AbstractPropertyValueV0::CustomPropertyReference { .. } => {
756 AbstractValueShapeV0::CustomPropertyReference
757 }
758 AbstractPropertyValueV0::Top { .. } => AbstractValueShapeV0::Top,
759 }
760}
761
762fn count_context_verdicts_v0(
763 evaluations: &[CascadeDimensionalRefinementContextEvaluationV0],
764 verdict: RefinementVerdictV0,
765) -> usize {
766 evaluations
767 .iter()
768 .filter(|evaluation| evaluation.combined_verdict == verdict)
769 .count()
770}
771
772fn evaluate_refinement_predicate_verdict_v0(
773 predicate: &RefinementPropertyPredicateV0,
774 value: &AbstractPropertyValueV0,
775) -> RefinementVerdictV0 {
776 match predicate {
777 RefinementPropertyPredicateV0::Any => RefinementVerdictV0::SatisfiedAll,
778 RefinementPropertyPredicateV0::ExactValue {
779 property_name,
780 value: expected,
781 } => evaluate_exact_value_predicate_v0(property_name, expected, value),
782 RefinementPropertyPredicateV0::OneOfValues {
783 property_name,
784 values,
785 } => evaluate_one_of_values_predicate_v0(property_name, values, value),
786 RefinementPropertyPredicateV0::CustomPropertyReference {
787 property_name,
788 custom_property_name,
789 } => evaluate_custom_property_reference_predicate_v0(
790 property_name,
791 custom_property_name,
792 value,
793 ),
794 RefinementPropertyPredicateV0::NumericRange {
795 property_name,
796 min_inclusive,
797 max_inclusive,
798 unit,
799 } => evaluate_numeric_range_predicate_v0(
800 property_name,
801 *min_inclusive,
802 *max_inclusive,
803 unit.as_deref(),
804 value,
805 ),
806 RefinementPropertyPredicateV0::HasPseudoState {
807 property_name,
808 pseudo_state,
809 } => evaluate_pseudo_state_predicate_v0(property_name, pseudo_state, value),
810 RefinementPropertyPredicateV0::And { predicates } => combine_and_refinement_verdicts_v0(
811 &predicates
812 .iter()
813 .map(|predicate| evaluate_refinement_predicate_verdict_v0(predicate, value))
814 .collect::<Vec<_>>(),
815 ),
816 RefinementPropertyPredicateV0::Or { predicates } => combine_or_refinement_verdicts_v0(
817 &predicates
818 .iter()
819 .map(|predicate| evaluate_refinement_predicate_verdict_v0(predicate, value))
820 .collect::<Vec<_>>(),
821 ),
822 RefinementPropertyPredicateV0::Not { predicate } => {
823 match evaluate_refinement_predicate_verdict_v0(predicate, value) {
824 RefinementVerdictV0::SatisfiedAll => RefinementVerdictV0::Unsatisfiable,
825 RefinementVerdictV0::Unsatisfiable => RefinementVerdictV0::SatisfiedAll,
826 RefinementVerdictV0::SatisfiedSome | RefinementVerdictV0::Unknown => {
827 RefinementVerdictV0::Unknown
828 }
829 }
830 }
831 }
832}
833
834fn evaluate_numeric_range_predicate_v0(
835 property_name: &AuthoredPropertyTextV0,
836 min_inclusive: Option<i64>,
837 max_inclusive: Option<i64>,
838 unit: Option<&str>,
839 value: &AbstractPropertyValueV0,
840) -> RefinementVerdictV0 {
841 match value {
842 AbstractPropertyValueV0::Exact {
843 property_name: actual_property,
844 value: actual_value,
845 ..
846 } if property_names_same(actual_property, property_name) => {
847 if numeric_range_contains_value_v0(actual_value, min_inclusive, max_inclusive, unit) {
848 RefinementVerdictV0::SatisfiedAll
849 } else {
850 RefinementVerdictV0::Unsatisfiable
851 }
852 }
853 AbstractPropertyValueV0::FiniteSet {
854 property_name: actual_property,
855 values,
856 ..
857 } if property_names_same(actual_property, property_name) => {
858 let matched = values
859 .iter()
860 .filter(|candidate| {
861 numeric_range_contains_value_v0(candidate, min_inclusive, max_inclusive, unit)
862 })
863 .count();
864 if matched == values.len() {
865 RefinementVerdictV0::SatisfiedAll
866 } else if matched > 0 {
867 RefinementVerdictV0::SatisfiedSome
868 } else {
869 RefinementVerdictV0::Unsatisfiable
870 }
871 }
872 AbstractPropertyValueV0::Top {
873 property_name: actual_property,
874 }
875 | AbstractPropertyValueV0::CustomPropertyReference {
876 property_name: actual_property,
877 ..
878 } if property_names_same(actual_property, property_name) => RefinementVerdictV0::Unknown,
879 _ => RefinementVerdictV0::Unsatisfiable,
880 }
881}
882
883fn evaluate_pseudo_state_predicate_v0(
884 property_name: &AuthoredPropertyTextV0,
885 expected_pseudo_state: &str,
886 value: &AbstractPropertyValueV0,
887) -> RefinementVerdictV0 {
888 match value {
889 AbstractPropertyValueV0::Exact {
890 property_name: actual_property,
891 pseudo_state,
892 ..
893 }
894 | AbstractPropertyValueV0::CustomPropertyReference {
895 property_name: actual_property,
896 pseudo_state,
897 ..
898 } if property_names_same(actual_property, property_name) => {
899 if pseudo_state.as_deref() == Some(expected_pseudo_state) {
900 RefinementVerdictV0::SatisfiedAll
901 } else {
902 RefinementVerdictV0::Unsatisfiable
903 }
904 }
905 AbstractPropertyValueV0::FiniteSet {
906 property_name: actual_property,
907 pseudo_states,
908 ..
909 } if property_names_same(actual_property, property_name) => {
910 if pseudo_states.len() == 1
911 && pseudo_states
912 .iter()
913 .any(|pseudo_state| pseudo_state == expected_pseudo_state)
914 {
915 RefinementVerdictV0::SatisfiedAll
916 } else if pseudo_states
917 .iter()
918 .any(|pseudo_state| pseudo_state == expected_pseudo_state)
919 {
920 RefinementVerdictV0::SatisfiedSome
921 } else {
922 RefinementVerdictV0::Unsatisfiable
923 }
924 }
925 AbstractPropertyValueV0::Top {
926 property_name: actual_property,
927 } if property_names_same(actual_property, property_name) => RefinementVerdictV0::Unknown,
928 _ => RefinementVerdictV0::Unsatisfiable,
929 }
930}
931
932fn evaluate_exact_value_predicate_v0(
933 property_name: &AuthoredPropertyTextV0,
934 expected: &str,
935 value: &AbstractPropertyValueV0,
936) -> RefinementVerdictV0 {
937 match value {
938 AbstractPropertyValueV0::Exact {
939 property_name: actual_property,
940 value: actual_value,
941 ..
942 } if property_names_same(actual_property, property_name) && actual_value == expected => {
943 RefinementVerdictV0::SatisfiedAll
944 }
945 AbstractPropertyValueV0::FiniteSet {
946 property_name: actual_property,
947 values,
948 ..
949 } if property_names_same(actual_property, property_name)
950 && values.iter().any(|value| value == expected) =>
951 {
952 if values.len() == 1 {
953 RefinementVerdictV0::SatisfiedAll
954 } else {
955 RefinementVerdictV0::SatisfiedSome
956 }
957 }
958 AbstractPropertyValueV0::Top {
959 property_name: actual_property,
960 }
961 | AbstractPropertyValueV0::CustomPropertyReference {
962 property_name: actual_property,
963 ..
964 } if property_names_same(actual_property, property_name) => RefinementVerdictV0::Unknown,
965 _ => RefinementVerdictV0::Unsatisfiable,
966 }
967}
968
969fn evaluate_one_of_values_predicate_v0(
970 property_name: &AuthoredPropertyTextV0,
971 expected_values: &[String],
972 value: &AbstractPropertyValueV0,
973) -> RefinementVerdictV0 {
974 match value {
975 AbstractPropertyValueV0::Exact {
976 property_name: actual_property,
977 value: actual_value,
978 ..
979 } if property_names_same(actual_property, property_name) => {
980 if expected_values.contains(actual_value) {
981 RefinementVerdictV0::SatisfiedAll
982 } else {
983 RefinementVerdictV0::Unsatisfiable
984 }
985 }
986 AbstractPropertyValueV0::FiniteSet {
987 property_name: actual_property,
988 values,
989 ..
990 } if property_names_same(actual_property, property_name) => {
991 let matched = values
992 .iter()
993 .filter(|value| expected_values.contains(*value))
994 .count();
995 if matched == values.len() {
996 RefinementVerdictV0::SatisfiedAll
997 } else if matched > 0 {
998 RefinementVerdictV0::SatisfiedSome
999 } else {
1000 RefinementVerdictV0::Unsatisfiable
1001 }
1002 }
1003 AbstractPropertyValueV0::Top {
1004 property_name: actual_property,
1005 }
1006 | AbstractPropertyValueV0::CustomPropertyReference {
1007 property_name: actual_property,
1008 ..
1009 } if property_names_same(actual_property, property_name) => RefinementVerdictV0::Unknown,
1010 _ => RefinementVerdictV0::Unsatisfiable,
1011 }
1012}
1013
1014fn evaluate_custom_property_reference_predicate_v0(
1015 property_name: &AuthoredPropertyTextV0,
1016 expected_custom_property: &AuthoredPropertyTextV0,
1017 value: &AbstractPropertyValueV0,
1018) -> RefinementVerdictV0 {
1019 match value {
1020 AbstractPropertyValueV0::CustomPropertyReference {
1021 property_name: actual_property,
1022 custom_property_name,
1023 ..
1024 } if property_names_same(actual_property, property_name)
1025 && property_names_same(custom_property_name, expected_custom_property) =>
1026 {
1027 RefinementVerdictV0::SatisfiedAll
1028 }
1029 AbstractPropertyValueV0::Top {
1030 property_name: actual_property,
1031 } if property_names_same(actual_property, property_name) => RefinementVerdictV0::Unknown,
1032 _ => RefinementVerdictV0::Unsatisfiable,
1033 }
1034}
1035
1036fn combine_and_refinement_verdicts_v0(verdicts: &[RefinementVerdictV0]) -> RefinementVerdictV0 {
1037 if verdicts.is_empty()
1038 || verdicts
1039 .iter()
1040 .all(|verdict| *verdict == RefinementVerdictV0::SatisfiedAll)
1041 {
1042 RefinementVerdictV0::SatisfiedAll
1043 } else if verdicts.contains(&RefinementVerdictV0::Unsatisfiable) {
1044 RefinementVerdictV0::Unsatisfiable
1045 } else if verdicts.contains(&RefinementVerdictV0::SatisfiedAll)
1046 || verdicts.contains(&RefinementVerdictV0::SatisfiedSome)
1047 {
1048 RefinementVerdictV0::SatisfiedSome
1049 } else {
1050 RefinementVerdictV0::Unknown
1051 }
1052}
1053
1054fn combine_or_refinement_verdicts_v0(verdicts: &[RefinementVerdictV0]) -> RefinementVerdictV0 {
1055 if verdicts.is_empty() || verdicts.contains(&RefinementVerdictV0::SatisfiedAll) {
1056 RefinementVerdictV0::SatisfiedAll
1057 } else if verdicts.contains(&RefinementVerdictV0::SatisfiedSome) {
1058 RefinementVerdictV0::SatisfiedSome
1059 } else if verdicts
1060 .iter()
1061 .all(|verdict| *verdict == RefinementVerdictV0::Unsatisfiable)
1062 {
1063 RefinementVerdictV0::Unsatisfiable
1064 } else {
1065 RefinementVerdictV0::Unknown
1066 }
1067}
1068
1069fn count_satisfied_refinement_clauses_v0(
1070 predicate: &RefinementPropertyPredicateV0,
1071 value: &AbstractPropertyValueV0,
1072) -> usize {
1073 match predicate {
1074 RefinementPropertyPredicateV0::And { predicates }
1075 | RefinementPropertyPredicateV0::Or { predicates } => predicates
1076 .iter()
1077 .map(|predicate| count_satisfied_refinement_clauses_v0(predicate, value))
1078 .sum(),
1079 RefinementPropertyPredicateV0::Not { predicate } => usize::from(matches!(
1080 evaluate_refinement_predicate_verdict_v0(predicate, value),
1081 RefinementVerdictV0::Unsatisfiable
1082 )),
1083 _ => usize::from(matches!(
1084 evaluate_refinement_predicate_verdict_v0(predicate, value),
1085 RefinementVerdictV0::SatisfiedAll | RefinementVerdictV0::SatisfiedSome
1086 )),
1087 }
1088}
1089
1090fn refinement_predicate_expression_id_v0(predicate: &RefinementPropertyPredicateV0) -> String {
1091 match predicate {
1092 RefinementPropertyPredicateV0::Any => "any".to_string(),
1093 RefinementPropertyPredicateV0::ExactValue {
1094 property_name,
1095 value,
1096 } => {
1097 let mut expression = String::from("exact:");
1098 if property_name.write_into(&mut expression).is_err() {
1099 return expression;
1100 }
1101 expression.push(':');
1102 expression.push_str(value);
1103 expression
1104 }
1105 RefinementPropertyPredicateV0::OneOfValues {
1106 property_name,
1107 values,
1108 } => {
1109 let mut expression = String::from("one-of:");
1110 if property_name.write_into(&mut expression).is_err() {
1111 return expression;
1112 }
1113 expression.push(':');
1114 expression.push_str(&values.join("|"));
1115 expression
1116 }
1117 RefinementPropertyPredicateV0::CustomPropertyReference {
1118 property_name,
1119 custom_property_name,
1120 } => {
1121 let mut expression = String::from("custom-ref:");
1122 if property_name.write_into(&mut expression).is_err() {
1123 return expression;
1124 }
1125 expression.push(':');
1126 if custom_property_name.write_into(&mut expression).is_err() {
1127 return expression;
1128 }
1129 expression
1130 }
1131 RefinementPropertyPredicateV0::NumericRange {
1132 property_name,
1133 min_inclusive,
1134 max_inclusive,
1135 unit,
1136 } => {
1137 let mut expression = String::from("numeric-range:");
1138 if property_name.write_into(&mut expression).is_err() {
1139 return expression;
1140 }
1141 expression.push(':');
1142 expression.push_str(
1143 &min_inclusive
1144 .map(|value| value.to_string())
1145 .unwrap_or_else(|| "-inf".to_string()),
1146 );
1147 expression.push_str("..");
1148 expression.push_str(
1149 &max_inclusive
1150 .map(|value| value.to_string())
1151 .unwrap_or_else(|| "inf".to_string()),
1152 );
1153 expression.push(':');
1154 expression.push_str(unit.as_deref().unwrap_or("*"));
1155 expression
1156 }
1157 RefinementPropertyPredicateV0::HasPseudoState {
1158 property_name,
1159 pseudo_state,
1160 } => {
1161 let mut expression = String::from("pseudo-state:");
1162 if property_name.write_into(&mut expression).is_err() {
1163 return expression;
1164 }
1165 expression.push(':');
1166 expression.push_str(pseudo_state);
1167 expression
1168 }
1169 RefinementPropertyPredicateV0::And { predicates } => format!(
1170 "and({})",
1171 predicates
1172 .iter()
1173 .map(refinement_predicate_expression_id_v0)
1174 .collect::<Vec<_>>()
1175 .join(",")
1176 ),
1177 RefinementPropertyPredicateV0::Or { predicates } => format!(
1178 "or({})",
1179 predicates
1180 .iter()
1181 .map(refinement_predicate_expression_id_v0)
1182 .collect::<Vec<_>>()
1183 .join(",")
1184 ),
1185 RefinementPropertyPredicateV0::Not { predicate } => {
1186 format!("not({})", refinement_predicate_expression_id_v0(predicate))
1187 }
1188 }
1189}
1190
1191fn refinement_predicate_provenance_v0(
1192 predicate: &RefinementPropertyPredicateV0,
1193) -> Vec<omena_refinement_trait::RefinementProvenanceV0> {
1194 let mut provenance = Vec::new();
1195 collect_refinement_predicate_provenance_v0(predicate, &mut provenance);
1196 provenance
1197}
1198
1199fn collect_refinement_predicate_provenance_v0(
1200 predicate: &RefinementPropertyPredicateV0,
1201 provenance: &mut Vec<omena_refinement_trait::RefinementProvenanceV0>,
1202) {
1203 push_refinement_provenance_v0(provenance, "property-grammar", None);
1204 match predicate {
1205 RefinementPropertyPredicateV0::Any => {}
1206 RefinementPropertyPredicateV0::ExactValue { .. }
1207 | RefinementPropertyPredicateV0::OneOfValues { .. } => {
1208 push_refinement_provenance_v0(provenance, "finite-property-domain", None);
1209 }
1210 RefinementPropertyPredicateV0::CustomPropertyReference { .. } => {
1211 push_refinement_provenance_v0(provenance, "custom-property-reference", None);
1212 }
1213 RefinementPropertyPredicateV0::NumericRange { .. } => {
1214 push_refinement_provenance_v0(provenance, "numeric-range-interval", None);
1215 }
1216 RefinementPropertyPredicateV0::HasPseudoState { .. } => {
1217 push_refinement_provenance_v0(provenance, "pseudo-state-refinement", None);
1218 }
1219 RefinementPropertyPredicateV0::And { predicates }
1220 | RefinementPropertyPredicateV0::Or { predicates } => {
1221 push_refinement_provenance_v0(provenance, "predicate-composition", None);
1222 for predicate in predicates {
1223 collect_refinement_predicate_provenance_v0(predicate, provenance);
1224 }
1225 }
1226 RefinementPropertyPredicateV0::Not { predicate } => {
1227 push_refinement_provenance_v0(provenance, "predicate-composition", None);
1228 collect_refinement_predicate_provenance_v0(predicate, provenance);
1229 }
1230 }
1231}
1232
1233fn push_refinement_provenance_v0(
1234 provenance: &mut Vec<omena_refinement_trait::RefinementProvenanceV0>,
1235 source: &'static str,
1236 legacy_proof_primitive: Option<&'static str>,
1237) {
1238 if provenance.iter().any(|entry| {
1239 entry.source == source && entry.legacy_proof_primitive == legacy_proof_primitive
1240 }) {
1241 return;
1242 }
1243 provenance.push(refinement_provenance_v0(source, legacy_proof_primitive));
1244}
1245
1246fn numeric_range_contains_value_v0(
1247 value: &str,
1248 min_inclusive: Option<i64>,
1249 max_inclusive: Option<i64>,
1250 expected_unit: Option<&str>,
1251) -> bool {
1252 let Some((magnitude, unit)) = parse_css_integer_with_unit_v0(value) else {
1253 return false;
1254 };
1255 if let Some(expected_unit) = expected_unit
1256 && unit != expected_unit
1257 {
1258 return false;
1259 }
1260 if let Some(min_inclusive) = min_inclusive
1261 && magnitude < min_inclusive
1262 {
1263 return false;
1264 }
1265 if let Some(max_inclusive) = max_inclusive
1266 && magnitude > max_inclusive
1267 {
1268 return false;
1269 }
1270 true
1271}
1272
1273fn parse_css_integer_with_unit_v0(value: &str) -> Option<(i64, &str)> {
1274 let trimmed = value.trim();
1275 let mut end = 0;
1276 for (index, ch) in trimmed.char_indices() {
1277 if ch.is_ascii_digit() || (index == 0 && (ch == '-' || ch == '+')) {
1278 end = index + ch.len_utf8();
1279 } else {
1280 break;
1281 }
1282 }
1283 if end == 0 || trimmed[..end].ends_with(['-', '+']) {
1284 return None;
1285 }
1286 let magnitude = trimmed[..end].parse::<i64>().ok()?;
1287 Some((magnitude, trimmed[end..].trim()))
1288}
1289
1290fn calc_dimension_diagnostic_for_value_v0(
1291 property_name: &AuthoredPropertyTextV0,
1292 value: &str,
1293) -> Option<CalcDimensionDiagnosticV0> {
1294 let expression = extract_calc_expression_v0(value)?;
1295 let dimension_values = parse_dimension_vector_values_from_expression_v0(expression);
1296 let non_number_values = dimension_values
1297 .iter()
1298 .filter(|entry| entry.vector != dimension_vector_number_v0())
1299 .collect::<Vec<_>>();
1300 if non_number_values.len() < 2 {
1301 return None;
1302 }
1303
1304 let observed_units = non_number_values
1305 .iter()
1306 .map(|entry| entry.unit.clone())
1307 .collect::<BTreeSet<_>>()
1308 .into_iter()
1309 .collect::<Vec<_>>();
1310 let observed_vectors = non_number_values
1311 .iter()
1312 .map(|entry| entry.vector)
1313 .collect::<BTreeSet<_>>()
1314 .into_iter()
1315 .collect::<Vec<_>>();
1316 let unit_families = non_number_values
1317 .iter()
1318 .map(|entry| entry.unit_family)
1319 .collect::<BTreeSet<_>>();
1320 let has_percentage = non_number_values
1321 .iter()
1322 .any(|entry| entry.vector.percentage != 0);
1323 let has_non_percentage = non_number_values
1324 .iter()
1325 .any(|entry| entry.vector.percentage == 0);
1326 let kind = if has_percentage && has_non_percentage {
1327 CalcDimensionDiagnosticKindV0::ContextDependentDimension
1328 } else if observed_vectors.len() > 1 {
1329 CalcDimensionDiagnosticKindV0::DimensionalMismatch
1330 } else if unit_families.len() > 1 {
1331 CalcDimensionDiagnosticKindV0::MixedDimension
1332 } else {
1333 return None;
1334 };
1335
1336 Some(CalcDimensionDiagnosticV0 {
1337 schema_version: REFINEMENT_SCHEMA_VERSION_V0,
1338 product: "omena-refinement.calc-dimension-diagnostic",
1339 feature_gate: "calc-dimension-diagnostics-v0",
1340 claim_level: "researchGradeHint",
1341 theorem_claimed: false,
1342 public_safety_claim_ready: false,
1343 kind,
1344 property_name: property_name.clone(),
1345 expression: expression.to_string(),
1346 observed_units,
1347 observed_vectors,
1348 })
1349}
1350
1351fn parse_dimension_vector_values_from_expression_v0(
1352 expression: &str,
1353) -> Vec<DimensionVectorValueV0> {
1354 expression
1355 .split(|ch: char| {
1356 ch.is_ascii_whitespace() || matches!(ch, '+' | '-' | '*' | '/' | '(' | ')' | ',')
1357 })
1358 .filter_map(parse_dimension_vector_value_v0)
1359 .collect()
1360}
1361
1362fn parse_dimension_vector_value_v0(value: &str) -> Option<DimensionVectorValueV0> {
1363 let trimmed = value.trim();
1364 if trimmed.is_empty() {
1365 return None;
1366 }
1367 let (unit_start, _) = trimmed
1368 .char_indices()
1369 .find(|(index, ch)| {
1370 *index > 0 && !(ch.is_ascii_digit() || *ch == '.' || *ch == '_' || *ch == '-')
1371 })
1372 .unwrap_or((trimmed.len(), '\0'));
1373 if unit_start == 0 {
1374 return None;
1375 }
1376 let number = trimmed[..unit_start].replace('_', "");
1377 if number.parse::<f64>().is_err() {
1378 return None;
1379 }
1380 let unit = trimmed[unit_start..].trim().to_ascii_lowercase();
1381 let (unit_family, vector) = dimension_vector_for_unit_v0(&unit)?;
1382
1383 Some(DimensionVectorValueV0 {
1384 source_value: trimmed.to_string(),
1385 unit,
1386 unit_family,
1387 vector,
1388 })
1389}
1390
1391fn extract_calc_expression_v0(value: &str) -> Option<&str> {
1392 let start = value.find("calc(")? + "calc(".len();
1393 let rest = &value[start..];
1394 let end = rest.rfind(')')?;
1395 Some(rest[..end].trim())
1396}
1397
1398fn dimension_vector_for_unit_v0(unit: &str) -> Option<(&'static str, DimensionVectorV0)> {
1399 let vector = match unit {
1400 "" => ("number", dimension_vector_number_v0()),
1401 "%" => (
1402 "percentage",
1403 DimensionVectorV0 {
1404 length: 0,
1405 angle: 0,
1406 time: 0,
1407 percentage: 1,
1408 number: 0,
1409 },
1410 ),
1411 "px" | "cm" | "mm" | "q" | "in" | "pt" | "pc" => {
1412 ("absoluteLength", dimension_vector_length_v0())
1413 }
1414 "em" | "rem" | "ex" | "ch" | "ic" | "lh" | "rlh" => {
1415 ("fontRelativeLength", dimension_vector_length_v0())
1416 }
1417 "vw" | "vh" | "vi" | "vb" | "vmin" | "vmax" | "svw" | "svh" | "lvw" | "lvh" | "dvw"
1418 | "dvh" => ("viewportLength", dimension_vector_length_v0()),
1419 "deg" | "grad" | "rad" | "turn" => (
1420 "angle",
1421 DimensionVectorV0 {
1422 length: 0,
1423 angle: 1,
1424 time: 0,
1425 percentage: 0,
1426 number: 0,
1427 },
1428 ),
1429 "s" | "ms" => (
1430 "time",
1431 DimensionVectorV0 {
1432 length: 0,
1433 angle: 0,
1434 time: 1,
1435 percentage: 0,
1436 number: 0,
1437 },
1438 ),
1439 _ => return None,
1440 };
1441 Some(vector)
1442}
1443
1444fn dimension_vector_length_v0() -> DimensionVectorV0 {
1445 DimensionVectorV0 {
1446 length: 1,
1447 angle: 0,
1448 time: 0,
1449 percentage: 0,
1450 number: 0,
1451 }
1452}
1453
1454fn dimension_vector_number_v0() -> DimensionVectorV0 {
1455 DimensionVectorV0 {
1456 length: 0,
1457 angle: 0,
1458 time: 0,
1459 percentage: 0,
1460 number: 1,
1461 }
1462}
1463
1464fn deterministic_refinement_digest_v0(bytes: &[u8]) -> u64 {
1465 bytes.iter().fold(0xcbf29ce484222325, |hash, byte| {
1466 (hash ^ u64::from(*byte)).wrapping_mul(0x100000001b3)
1467 })
1468}
1469
1470#[cfg(feature = "refinement-smt")]
1471pub fn refinement_smt_backend_available_v0() -> bool {
1472 let _ = omena_smt::cascade_theory_signature_v0();
1473 true
1474}
1475
1476#[cfg(not(feature = "refinement-smt"))]
1477pub fn refinement_smt_backend_available_v0() -> bool {
1478 false
1479}
1480
1481#[cfg(test)]
1482mod tests {
1483 use super::*;
1484 use omena_abstract_value::{
1485 CascadeContextV0, CascadeValueFamilyMemberV0,
1486 derive_context_indexed_cascade_restriction_maps_v0,
1487 summarize_context_indexed_cascade_value_family_v0,
1488 };
1489
1490 fn authored_property(value: &str) -> AuthoredPropertyTextV0 {
1491 AuthoredPropertyTextV0::new(value)
1492 }
1493
1494 #[test]
1495 fn refined_value_round_trips_to_legacy_without_mutating_v0() {
1496 let top = TopPredicateV0::default();
1497 let any = AnyPropertyIndexV0::default();
1498 assert_eq!(top.schema_version, "0");
1499 assert_eq!(any.layer_marker, "refinement-cascade");
1500
1501 let legacy = AbstractPropertyValueV0::Top {
1502 property_name: authored_property("color"),
1503 };
1504 let refined =
1505 project_legacy_to_refined_v0::<AnyPropertyIndexV0, TopPredicateV0>(legacy.clone());
1506 assert_eq!(refined.schema_version, "0");
1507 assert_eq!(refined.layer_marker, "refinement-cascade");
1508 assert!(refined.strict_superset_of_legacy_v0);
1509 assert!(refined_projection_preserves_legacy_value_v0::<
1510 AnyPropertyIndexV0,
1511 TopPredicateV0,
1512 >(&refined));
1513 assert_eq!(project_refined_to_legacy_v0(&refined), legacy);
1514 }
1515
1516 #[test]
1517 fn refinement_property_grammar_evaluates_exact_and_one_of_values() {
1518 let exact = AbstractPropertyValueV0::Exact {
1519 property_name: authored_property("display"),
1520 value: "grid".to_string(),
1521 pseudo_state: None,
1522 };
1523 let predicate = RefinementPropertyPredicateV0::OneOfValues {
1524 property_name: authored_property("display"),
1525 values: vec!["grid".to_string(), "flex".to_string()],
1526 };
1527 let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &exact);
1528
1529 assert_eq!(evaluation.schema_version, "0");
1530 assert_eq!(
1531 evaluation.product,
1532 "omena-refinement.property-predicate-evaluation"
1533 );
1534 assert_eq!(evaluation.value_shape, AbstractValueShapeV0::Exact);
1535 assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedAll);
1536 assert_eq!(evaluation.matched_clause_count, 1);
1537 assert_eq!(evaluation.witness.predicate_id, "property-grammar");
1538 assert!(evaluation.witness.legacy_proofs_byte_untouched);
1539 }
1540
1541 #[test]
1542 fn refinement_property_predicate_identity_uses_sealed_keys() {
1543 let standard = |property: &str| RefinementPropertyPredicateV0::ExactValue {
1544 property_name: authored_property(property),
1545 value: "grid".to_string(),
1546 };
1547 let custom = |property: &str| RefinementPropertyPredicateV0::CustomPropertyReference {
1548 property_name: authored_property("color"),
1549 custom_property_name: authored_property(property),
1550 };
1551
1552 assert_eq!(standard(r"D\49 SPLAY"), standard("display"));
1553 assert_eq!(custom(r"--f\6f o"), custom("--foo"));
1554 assert_ne!(custom("--foo"), custom("--FOO"));
1555 }
1556
1557 #[test]
1558 fn refinement_predicate_composition_tracks_partial_and_negative_witnesses() {
1559 let finite = AbstractPropertyValueV0::FiniteSet {
1560 property_name: authored_property("color"),
1561 values: vec!["red".to_string(), "blue".to_string()],
1562 pseudo_states: Vec::new(),
1563 };
1564 let predicate = RefinementPropertyPredicateV0::And {
1565 predicates: vec![
1566 RefinementPropertyPredicateV0::OneOfValues {
1567 property_name: authored_property("color"),
1568 values: vec!["red".to_string()],
1569 },
1570 RefinementPropertyPredicateV0::Not {
1571 predicate: Box::new(RefinementPropertyPredicateV0::ExactValue {
1572 property_name: authored_property("color"),
1573 value: "green".to_string(),
1574 }),
1575 },
1576 ],
1577 };
1578 let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &finite);
1579
1580 assert_eq!(evaluation.value_shape, AbstractValueShapeV0::FiniteSet);
1581 assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedSome);
1582 assert_eq!(evaluation.matched_clause_count, 2);
1583 assert_eq!(
1584 evaluation.predicate_expression_id,
1585 "and(one-of:color:red,not(exact:color:green))"
1586 );
1587 assert_eq!(evaluation.witness.provenance[0].source, "property-grammar");
1588 }
1589
1590 #[test]
1591 fn refinement_custom_property_reference_predicate_is_not_wrapper_only() {
1592 let reference = AbstractPropertyValueV0::CustomPropertyReference {
1593 property_name: authored_property("color"),
1594 custom_property_name: authored_property("--brand"),
1595 pseudo_state: None,
1596 };
1597 let predicate = RefinementPropertyPredicateV0::CustomPropertyReference {
1598 property_name: authored_property("color"),
1599 custom_property_name: authored_property("--brand"),
1600 };
1601 let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &reference);
1602
1603 assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedAll);
1604 assert_eq!(
1605 evaluation.predicate_expression_id,
1606 "custom-ref:color:--brand"
1607 );
1608 }
1609
1610 #[test]
1611 fn refinement_numeric_range_and_pseudo_state_predicates_are_evaluated() {
1612 let finite = AbstractPropertyValueV0::FiniteSet {
1613 property_name: authored_property("opacity"),
1614 values: vec!["0".to_string(), "50%".to_string(), "100%".to_string()],
1615 pseudo_states: vec![":hover".to_string(), ":focus".to_string()],
1616 };
1617 let predicate = RefinementPropertyPredicateV0::And {
1618 predicates: vec![
1619 RefinementPropertyPredicateV0::NumericRange {
1620 property_name: authored_property("opacity"),
1621 min_inclusive: Some(0),
1622 max_inclusive: Some(100),
1623 unit: Some("%".to_string()),
1624 },
1625 RefinementPropertyPredicateV0::HasPseudoState {
1626 property_name: authored_property("opacity"),
1627 pseudo_state: ":hover".to_string(),
1628 },
1629 ],
1630 };
1631 let evaluation = evaluate_refinement_property_predicate_v0(&predicate, &finite);
1632
1633 assert_eq!(evaluation.value_shape, AbstractValueShapeV0::FiniteSet);
1634 assert_eq!(evaluation.verdict, RefinementVerdictV0::SatisfiedSome);
1635 assert_eq!(
1636 evaluation.predicate_expression_id,
1637 "and(numeric-range:opacity:0..100:%,pseudo-state:opacity::hover)"
1638 );
1639 assert!(
1640 evaluation
1641 .witness
1642 .provenance
1643 .iter()
1644 .any(|entry| entry.source == "numeric-range-interval")
1645 );
1646 assert!(
1647 evaluation
1648 .witness
1649 .provenance
1650 .iter()
1651 .any(|entry| entry.source == "pseudo-state-refinement")
1652 );
1653 assert!(
1654 evaluation
1655 .witness
1656 .provenance
1657 .iter()
1658 .any(|entry| entry.source == "predicate-composition")
1659 );
1660 }
1661
1662 #[test]
1663 fn refinement_context_digest_is_order_stable_and_invalidation_sensitive() {
1664 let range = RefinementPropertyPredicateV0::NumericRange {
1665 property_name: authored_property("z-index"),
1666 min_inclusive: Some(0),
1667 max_inclusive: Some(10),
1668 unit: None,
1669 };
1670 let exact = RefinementPropertyPredicateV0::ExactValue {
1671 property_name: authored_property("display"),
1672 value: "grid".to_string(),
1673 };
1674 let first = summarize_refinement_context_v0(&[range.clone(), exact.clone()]);
1675 let reordered = summarize_refinement_context_v0(&[exact.clone(), range.clone()]);
1676 let changed = summarize_refinement_context_v0(&[
1677 exact,
1678 RefinementPropertyPredicateV0::NumericRange {
1679 property_name: authored_property("z-index"),
1680 min_inclusive: Some(0),
1681 max_inclusive: Some(11),
1682 unit: None,
1683 },
1684 ]);
1685
1686 assert_eq!(first.schema_version, "0");
1687 assert_eq!(first.product, "omena-refinement.context-summary");
1688 assert_eq!(first.predicate_count, 2);
1689 assert!(first.downstream_invalidation_required);
1690 assert_eq!(first.context_digest, reordered.context_digest);
1691 assert_ne!(first.context_digest, changed.context_digest);
1692 assert!(first.witness_provenance_count >= 3);
1693 }
1694
1695 #[test]
1696 fn cascade_dimensional_refinement_bridge_reuses_existing_substrates() {
1697 let members = vec![
1698 CascadeValueFamilyMemberV0 {
1699 context: CascadeContextV0 {
1700 id: "base".to_string(),
1701 parent_id: None,
1702 selectors: vec![":root".to_string()],
1703 conditions: Vec::new(),
1704 layers: vec!["tokens".to_string()],
1705 },
1706 value: AbstractPropertyValueV0::Exact {
1707 property_name: authored_property("width"),
1708 value: "12px".to_string(),
1709 pseudo_state: None,
1710 },
1711 },
1712 CascadeValueFamilyMemberV0 {
1713 context: CascadeContextV0 {
1714 id: "fluid".to_string(),
1715 parent_id: Some("base".to_string()),
1716 selectors: vec![":root".to_string()],
1717 conditions: vec!["@media (orientation: portrait)".to_string()],
1718 layers: vec!["tokens".to_string()],
1719 },
1720 value: AbstractPropertyValueV0::Exact {
1721 property_name: authored_property("width"),
1722 value: "50%".to_string(),
1723 pseudo_state: None,
1724 },
1725 },
1726 CascadeValueFamilyMemberV0 {
1727 context: CascadeContextV0 {
1728 id: "unknown".to_string(),
1729 parent_id: Some("base".to_string()),
1730 selectors: vec![":root".to_string()],
1731 conditions: vec!["@container card".to_string()],
1732 layers: vec!["tokens".to_string()],
1733 },
1734 value: AbstractPropertyValueV0::Top {
1735 property_name: authored_property("width"),
1736 },
1737 },
1738 ];
1739 let restrictions = derive_context_indexed_cascade_restriction_maps_v0(&members);
1740 let family = summarize_context_indexed_cascade_value_family_v0(
1741 authored_property("width"),
1742 members,
1743 restrictions,
1744 );
1745 let predicate = RefinementPropertyPredicateV0::NumericRange {
1746 property_name: authored_property("width"),
1747 min_inclusive: Some(0),
1748 max_inclusive: Some(100),
1749 unit: Some("px".to_string()),
1750 };
1751
1752 let bridge = summarize_cascade_dimensional_refinement_bridge_v0(&family, &[predicate]);
1753
1754 assert_eq!(
1755 bridge.product,
1756 "omena-refinement.cascade-dimensional-refinement-bridge"
1757 );
1758 assert_eq!(bridge.claim_level, REFINEMENT_BRIDGE_CLAIM_LEVEL_V0);
1759 assert_eq!(bridge.cascade_family_product, family.product);
1760 assert_eq!(bridge.context_evaluation_count, 3);
1761 assert_eq!(bridge.restriction_map_count, 2);
1762 assert_eq!(bridge.satisfied_all_context_count, 1);
1763 assert_eq!(bridge.unsatisfiable_context_count, 1);
1764 assert_eq!(bridge.unknown_context_count, 1);
1765 assert_eq!(bridge.witness_provenance_count, 2);
1766 assert!(bridge.uses_existing_abstract_property_value_substrate);
1767 assert!(bridge.uses_existing_cascade_family_substrate);
1768 assert!(bridge.uses_existing_refinement_predicate_substrate);
1769 assert!(!bridge.forks_unit_system);
1770 assert!(!bridge.liquid_haskell_complete);
1771 assert!(!bridge.smt_complete);
1772 assert!(!bridge.theorem_claimed);
1773 assert!(bridge.product_path_evidence_ready);
1774 assert!(!bridge.stronger_type_safety_claim_ready);
1775 assert!(bridge.dimension_vector_domain_ready);
1776 assert!(bridge.calc_dimension_diagnostics_ready);
1777 assert!(!bridge.dimension_vector_domain.forks_unit_system);
1778 assert!(!bridge.dimension_vector_domain.theorem_claimed);
1779 assert_eq!(bridge.dimension_vector_domain.value_count, 2);
1780 assert_eq!(bridge.calc_dimension_diagnostics.diagnostic_count, 0);
1781 assert!(!bridge.calc_dimension_diagnostics.smt_complete);
1782 assert!(!bridge.calc_dimension_diagnostics.liquid_haskell_complete);
1783 assert!(
1784 !bridge
1785 .calc_dimension_diagnostics
1786 .stronger_type_safety_claim_ready
1787 );
1788 assert_eq!(bridge.evaluations[0].context_id, "base");
1789 assert_eq!(
1790 bridge.evaluations[0].combined_verdict,
1791 RefinementVerdictV0::SatisfiedAll
1792 );
1793 assert_eq!(
1794 bridge.evaluations[0].predicate_expression_ids,
1795 vec!["numeric-range:width:0..100:px".to_string()]
1796 );
1797 }
1798
1799 #[test]
1800 fn dimensional_refinement_bridge_identity_uses_standard_property_keys() {
1801 let members = vec![CascadeValueFamilyMemberV0 {
1802 context: CascadeContextV0 {
1803 id: "base".to_string(),
1804 parent_id: None,
1805 selectors: vec![":root".to_string()],
1806 conditions: Vec::new(),
1807 layers: Vec::new(),
1808 },
1809 value: AbstractPropertyValueV0::Exact {
1810 property_name: authored_property("width"),
1811 value: "12px".to_string(),
1812 pseudo_state: None,
1813 },
1814 }];
1815 let family = summarize_context_indexed_cascade_value_family_v0(
1816 authored_property("width"),
1817 members,
1818 Vec::new(),
1819 );
1820 let bridge = summarize_cascade_dimensional_refinement_bridge_v0(&family, &[]);
1821 let mut equivalent = bridge.clone();
1822 equivalent.property_name = authored_property(r"W\49 DTH");
1823
1824 assert_eq!(bridge, equivalent);
1825 }
1826
1827 #[test]
1828 fn calc_dimension_diagnostics_classify_fixture_mismatches_without_unit_fork() {
1829 let values = vec![
1830 "calc(1px + 2s)".to_string(),
1831 "calc(1px + 2rem)".to_string(),
1832 "calc(100% - 1rem)".to_string(),
1833 "calc(1px + 2px)".to_string(),
1834 ];
1835 let domain = summarize_dimension_vector_domain_v0(&values);
1836 let diagnostics =
1837 summarize_calc_dimension_diagnostics_v0(&authored_property("width"), &values);
1838
1839 assert_eq!(domain.product, "omena-refinement.dimension-vector-domain");
1840 assert_eq!(domain.feature_gate, "dimension-vector-domain-v0");
1841 assert_eq!(domain.claim_level, "fixtureWitnessDimensionVectorDomain");
1842 assert!(!domain.forks_unit_system);
1843 assert!(!domain.theorem_claimed);
1844 assert!(domain.vector_count >= 3);
1845
1846 assert_eq!(
1847 diagnostics.product,
1848 "omena-refinement.calc-dimension-diagnostics"
1849 );
1850 assert_eq!(diagnostics.feature_gate, "calc-dimension-diagnostics-v0");
1851 assert_eq!(diagnostics.claim_level, "researchGradeHint");
1852 assert!(!diagnostics.forks_unit_system);
1853 assert!(!diagnostics.smt_complete);
1854 assert!(!diagnostics.liquid_haskell_complete);
1855 assert!(!diagnostics.stronger_type_safety_claim_ready);
1856 assert!(!diagnostics.theorem_claimed);
1857 assert_eq!(diagnostics.diagnostic_count, 3);
1858 assert!(diagnostics.diagnostics.iter().any(|diagnostic| {
1859 diagnostic.kind == CalcDimensionDiagnosticKindV0::DimensionalMismatch
1860 && diagnostic.expression == "1px + 2s"
1861 }));
1862 assert!(diagnostics.diagnostics.iter().any(|diagnostic| {
1863 diagnostic.kind == CalcDimensionDiagnosticKindV0::MixedDimension
1864 && diagnostic.expression == "1px + 2rem"
1865 }));
1866 assert!(diagnostics.diagnostics.iter().any(|diagnostic| {
1867 diagnostic.kind == CalcDimensionDiagnosticKindV0::ContextDependentDimension
1868 && diagnostic.expression == "100% - 1rem"
1869 }));
1870 }
1871
1872 #[test]
1873 fn calc_dimension_diagnostic_identity_uses_standard_property_keys() {
1874 let values = vec!["calc(1px + 2s)".to_string()];
1875 let escaped =
1876 summarize_calc_dimension_diagnostics_v0(&authored_property(r"W\49 DTH"), &values);
1877 let decoded = summarize_calc_dimension_diagnostics_v0(&authored_property("width"), &values);
1878
1879 assert_eq!(escaped.diagnostics, decoded.diagnostics);
1880 }
1881}