Enum WcetFunction 

pub enum WcetFunction {
    Bounded {
        name: String,
        cycles: u64,
        instr_count: usize,
        loops: Vec<WcetLoopBound>,
        recursion: Option<WcetRecursionBound>,
        hint_rejections: Vec<WcetHintRejection>,
    },
    Declined {
        name: String,
        reason: WcetDecline,
        note: String,
        hint_rejections: Vec<WcetHintRejection>,
    },
}

The per-function result: either a sound cycle bound or a loud decline.

Variants

Bounded

A sound upper bound on this function’s execution in cycles.

Fields

name: String

Function name (WASM export or generated).

cycles: u64

The sound worst-case cycle bound. For a loop-free function this is the SUM of each instruction’s documented worst-case cycles (each executes at most once). For a function whose loops ALL have proven trip counts (#778 phase 2) each instruction’s cost is multiplied by its proven worst-case execution count. Always ≥ any real execution under the stated precondition.

instr_count: usize

Number of ARM instructions summed (diagnostic).

loops: Vec<WcetLoopBound>

Proven loops (empty for a loop-free function), ascending head offset.

recursion: Option<WcetRecursionBound>

(#778 phase 4 / #49) Present iff this bound was composed via a verified self-recursion certificate; states the derived depth + frame count.

hint_rejections: Vec<WcetHintRejection>

Hints that were rejected (the static proof stands independently).

Declined

No bound emitted — a loud decline with a machine-readable reason. A decline is emitted (rather than the function omitted) so the map is COMPLETE: a consumer sees every function is either bounded or explicitly unbounded, never silently missing.

Fields

name: String

Function name.

reason: WcetDecline

Machine-readable reason.

note: String

Human-readable note (reason.note()).

hint_rejections: Vec<WcetHintRejection>

Hints that were offered for this function and rejected.

Implementations

impl WcetFunction

pub fn declined(name: impl Into<String>, reason: WcetDecline) -> Self

Construct a decline, filling in the note from the reason.

pub fn declined_with_rejections( name: impl Into<String>, reason: WcetDecline, hint_rejections: Vec<WcetHintRejection>, ) -> Self

Construct a decline carrying rejected-hint records.

Trait Implementations

impl Clone for WcetFunction

fn clone(&self) -> WcetFunction

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for WcetFunction

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for WcetFunction

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for WcetFunction

impl PartialEq for WcetFunction

fn eq(&self, other: &WcetFunction) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl Serialize for WcetFunction

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for WcetFunction