pub struct CascadeDimensionalRefinementBridgeV0 {Show 28 fields
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 evaluations: Vec<CascadeDimensionalRefinementContextEvaluationV0>,
}Expand description
M6 #69 bridge between context-indexed property values and refinement facts.
This is a research-staged substrate: it evaluates the existing cascade family through the existing refinement predicate evaluator. It does not claim Liquid-Haskell-style inference, SMT completeness, or a theorem.
Fields§
§schema_version: &'static str§product: &'static str§layer_marker: &'static str§feature_gate: &'static str§claim_level: &'static str§property_name: String§cascade_family_product: &'static str§predicate_count: usize§context_value_count: usize§restriction_map_count: usize§context_evaluation_count: usize§satisfied_all_context_count: usize§satisfied_some_context_count: usize§unknown_context_count: usize§unsatisfiable_context_count: usize§witness_provenance_count: usize§property_consistent: bool§uses_existing_abstract_property_value_substrate: bool§uses_existing_cascade_family_substrate: bool§uses_existing_refinement_predicate_substrate: bool§forks_unit_system: bool§liquid_haskell_complete: bool§smt_backend_available: bool§smt_complete: bool§theorem_claimed: bool§product_path_evidence_ready: bool§stronger_type_safety_claim_ready: bool§evaluations: Vec<CascadeDimensionalRefinementContextEvaluationV0>Trait Implementations§
Source§impl Clone for CascadeDimensionalRefinementBridgeV0
impl Clone for CascadeDimensionalRefinementBridgeV0
Source§fn clone(&self) -> CascadeDimensionalRefinementBridgeV0
fn clone(&self) -> CascadeDimensionalRefinementBridgeV0
Returns a duplicate of the value. Read more
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source. Read moreimpl Eq for CascadeDimensionalRefinementBridgeV0
Source§impl PartialEq for CascadeDimensionalRefinementBridgeV0
impl PartialEq for CascadeDimensionalRefinementBridgeV0
Source§fn eq(&self, other: &CascadeDimensionalRefinementBridgeV0) -> bool
fn eq(&self, other: &CascadeDimensionalRefinementBridgeV0) -> bool
Tests for
self and other values to be equal, and is used by ==.impl StructuralPartialEq for CascadeDimensionalRefinementBridgeV0
Auto Trait Implementations§
impl Freeze for CascadeDimensionalRefinementBridgeV0
impl RefUnwindSafe for CascadeDimensionalRefinementBridgeV0
impl Send for CascadeDimensionalRefinementBridgeV0
impl Sync for CascadeDimensionalRefinementBridgeV0
impl Unpin for CascadeDimensionalRefinementBridgeV0
impl UnsafeUnpin for CascadeDimensionalRefinementBridgeV0
impl UnwindSafe for CascadeDimensionalRefinementBridgeV0
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> CloneToUninit for Twhere
T: Clone,
impl<T> CloneToUninit for Twhere
T: Clone,
Source§impl<Q, K> Equivalent<K> for Q
impl<Q, K> Equivalent<K> for Q
Source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key and return true if they are equal.