Struct RunFrozen 

pub struct RunFrozen {
    pub completion: String,
    pub evidence: Option<Vec<EvidenceCite>>,
    pub cause: Option<FreezeCause>,
}

run_frozen: how a run ended, and what it cites for having ended that way.

The three endings are spelled by Completion::name, which stays the authority for the words: this struct carries whichever word that method printed rather than an enum that would have to agree with it. A run that ended any other way cites nothing, and the key is absent rather than empty, exactly as the hand-written writer left it.

Fields

completion: String

evidence: Option<Vec<EvidenceCite>>

cause: Option<FreezeCause>

Why the line was written by something other than the run’s own driver (crates/kernel/spec/Event/Record.lean §8-82-2). Absent on every freeze a run wrote for itself, so those lines keep the bytes they always had.

Implementations

impl RunFrozen

pub fn of(completion: &Completion) -> RunFrozen

The one projection from a verdict to the line that records it.

Reading is deliberately not the inverse: a Completion::Done holds EventRefs, and minting those from a line would forge the evidence the type exists to guarantee.

pub fn lost() -> RunFrozen

The freeze of a run whose process died before it froze itself: the one place that says which ending such a run has.

cancelled, because the run stopped without finishing - done needs evidence the city recorded and it has none - and no ceiling cut it, which is what limit says. The cause tells it apart from a cancel somebody asked for (kernel D14).

Trait Implementations

impl Clone for RunFrozen

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RunFrozen

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for RunFrozen

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for RunFrozen

impl PartialEq for RunFrozen

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

Equality operator ==.

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

Inequality operator !=.

impl Serialize for RunFrozen

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 RunFrozen