Struct ProofCertificate 

pub struct ProofCertificate {
    pub id: ProofCertId,
    pub decl_name: String,
    pub type_hash: u64,
    pub proof_hash: u64,
    pub reduction_steps: Vec<ProofStep>,
    pub verified_at: u64,
}

A compact verification record for a single declaration.

Certificates record the structural hashes of the type and proof term, together with the sequence of reduction steps performed during kernel type-checking. They can be stored externally and replayed cheaply via hash verification.

Fields

id: ProofCertId

Unique certificate identifier (derived from content at creation time).

decl_name: String

Name of the declaration this certificate vouches for.

type_hash: u64

FNV-1a structural hash of the declaration’s type expression.

proof_hash: u64

FNV-1a structural hash of the proof term expression.

reduction_steps: Vec<ProofStep>

Ordered sequence of reduction steps taken during type-checking.

verified_at: u64

Unix timestamp (seconds) at which the certificate was created.

Implementations

impl ProofCertificate

pub fn step_count(&self) -> usize

Return the number of reduction steps recorded.

pub fn is_trivial(&self) -> bool

Return true if this certificate records no reduction steps.

Trait Implementations

impl Clone for ProofCertificate

fn clone(&self) -> ProofCertificate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofCertificate

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

Formats the value using the given formatter.

impl Display for ProofCertificate

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

Formats the value using the given formatter.

impl PartialEq for ProofCertificate

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for ProofCertificate

impl StructuralPartialEq for ProofCertificate