Struct IrSourced 

pub struct IrSourced;

Proposition: The VerifiedTree passed to a renderer was produced by a canonical model’s to_verified_tree() call, not constructed ad-hoc or bypassed.

Any frontend renderer that requires this proof can only be invoked after to_verified_tree() has been called, giving all frontends contractually enforced equivalency at the type level.

Trait Implementations

impl Prop for IrSourced

fn kani_proof() -> TokenStream

Generate a Kani proof harness for this proposition.

fn verus_proof() -> TokenStream

Generate a Verus proof for this proposition.

fn creusot_proof() -> TokenStream

Generate a Creusot contract proof for this proposition.

fn creusot_invariant_fn_name() -> &'static str

The name of the Creusot pearlite #[logic] function that expresses this proposition as a predicate over the machine state.

fn kani_invariant_fn_name() -> &'static str

The name of a #[cfg(kani)] boolean predicate function that expresses this proposition as a Kani-evaluable invariant check.

fn verus_invariant_fn_name() -> &'static str

The name of a Verus pub open spec fn that expresses this proposition as a Verus-verifiable predicate over the machine state.