Skip to main content

Crate omena_refinement

Crate omena_refinement 

Source
Expand description

Refinement type system contracts for cascade analysis.

The crate keeps legacy abstract property values wire-compatible by adding a strict-superset wrapper and delegating cascade checks to the byte-stable omena-cascade proof primitives.

claim_level: cascade refinement bridge substrate, not Liquid-Haskell inference or SMT completeness.

Structs§

AnyPropertyIndexV0
CascadeDimensionalRefinementBridgeV0
M6 #69 bridge between context-indexed property values and refinement facts.
CascadeDimensionalRefinementContextEvaluationV0
RefinedAbstractPropertyValueV0
RefinementContextSummaryV0
RefinementPredicateEvaluationV0
TopPredicateV0

Enums§

AbstractValueShapeV0
RefinementPropertyPredicateV0

Functions§

abstract_property_value_shape_v0
evaluate_refinement_property_predicate_v0
project_legacy_to_refined_v0
project_refined_to_legacy_v0
refine_declaration_in_context
refined_projection_preserves_legacy_value_v0
refinement_smt_backend_available_v0
summarize_cascade_dimensional_refinement_bridge_v0
summarize_refinement_context_v0