Type Alias CustomPropertyBoundedFixedPointComputationWitnessV0 

pub type CustomPropertyBoundedFixedPointComputationWitnessV0 = CustomPropertyLeastFixedPointProofV0;

Preferred machine-readable name for the bounded custom-property computation witness.

Aliased Type

pub struct CustomPropertyBoundedFixedPointComputationWitnessV0 {
    pub finite_domain: &'static str,
    pub transfer_function: &'static str,
    pub bounded_fixed_point_computation_witness: &'static str,
    pub monotone_witness: &'static str,
    pub monotonic_progress_witness: &'static str,
    pub iteration_bound_formula: &'static str,
    pub cycle_policy: &'static str,
    pub proof_obligations: Vec<&'static str>,
}

Fields

finite_domain: &'static str

transfer_function: &'static str

bounded_fixed_point_computation_witness: &'static str

monotone_witness: &'static str

Compatibility wording; prefer Self::monotonic_progress_witness.

monotonic_progress_witness: &'static str

iteration_bound_formula: &'static str

cycle_policy: &'static str

proof_obligations: Vec<&'static str>

Compatibility wording retained alongside the computation-witness fields.