Struct WcetRecursionCert 

pub struct WcetRecursionCert {
    pub self_label: String,
    pub max_depth: u64,
    pub hint: u64,
}

(#778 phase 4 / #49) A proven SELF-recursion certificate: the function is a single-self-call chain whose controlling value is entry-independently bounded (a masked-slot counter decreasing by a const step toward a base guard on the SAME masked quantity), so its maximum recursion DEPTH is DERIVED (not hint-supplied) as an entry-independent ceiling. The composer folds the self-edge as frame_count × frame_cost (frame_count = max_depth + 1, counting the base frame) instead of declining Recursion.

A certificate is attached ONLY after the depth was cross-checked against a --wcet-hints recursion_depth entry (the untrusted oracle asserts intent; synth’s derived ceiling is what is emitted). Without a hint the recursion still declines (a bound this consequential is opt-in, mirroring the equality-exit loop-hint gate). self_label is the function’s own func_<idx> self-call label so the composer can identify and special-case exactly that edge.

Fields

self_label: String

The self-call BL label (func_<idx>) this certificate authorizes.

max_depth: u64

The DERIVED maximum recursion depth (entry-independent ceiling). The base frame is NOT included here — the composer uses max_depth + 1 frames.

hint: u64

The hint value that gated this certificate (recorded for the sidecar; the emitted depth is always the derived max_depth, never the raw hint).

Trait Implementations

impl Clone for WcetRecursionCert

fn clone(&self) -> WcetRecursionCert

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for WcetRecursionCert

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

Formats the value using the given formatter.

impl Eq for WcetRecursionCert

impl PartialEq for WcetRecursionCert

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for WcetRecursionCert