Struct EnvironmentCertificate 

pub struct EnvironmentCertificate {
    pub schema: String,
    pub prelude_version: String,
    pub base: EnvironmentBase,
    pub conversion: ConversionDiscipline,
    pub nodes: Vec<TermNode>,
    pub entries: Vec<EnvironmentEntry>,
    pub target: String,
    pub binder_kinds: BTreeMap<String, Vec<BinderKind>>,
}

A proof together with the complete environment it needs, rebuilt and re-checked from nothing but the declared base.

Fields

schema: String

ENVIRONMENT_SCHEMA for original entry kinds, or OPAQUE_ENVIRONMENT_SCHEMA with opaque declarations.

prelude_version: String

The prelude/kernel version this certificate was minted against.

base: EnvironmentBase

conversion: ConversionDiscipline

nodes: Vec<TermNode>

The term table, children before parents.

entries: Vec<EnvironmentEntry>

The declarations, in dependency order: every name an entry cites is the base’s or an earlier entry’s.

target: String

The name of the definition or theorem this certificate proves.

binder_kinds: BTreeMap<String, Vec<BinderKind>>

Source binder annotations of declarations’ leading telescopes, by name. Presentation metadata: it changes no judgement, and a reader of the LOGOS document is told which annotations the fully explicit kernel terms do not write.

Implementations

impl EnvironmentCertificate

pub fn admitted_depth( &self, limits: &EnvironmentLimits, ) -> Result<usize, EnvironmentError>

The deepest term in the certificate, after admission. A caller sizes the stack of the thread that runs EnvironmentCertificate::rebuild from it.

pub fn rebuild( &self, limits: &EnvironmentLimits, ) -> Result<RebuiltEnvironment, EnvironmentError>

Rebuild the environment from the declared base, kernel-checking every entry, and return the checked context with the target’s statement and proof.

Runs on the caller’s thread; a caller holding a deep certificate sizes that thread’s stack with EnvironmentCertificate::admitted_depth and crate::term_store::stack_bytes_for_depth first.

impl EnvironmentCertificate

pub fn capture( request: &CaptureRequest<'_>, ) -> Result<EnvironmentCertificate, EnvironmentError>

Capture the target’s complete dependency closure from a checked context, in dependency order. Every captured declaration is exactly what the context checked; capture decides nothing, and EnvironmentCertificate::rebuild re-decides everything.

Trait Implementations

impl Clone for EnvironmentCertificate

fn clone(&self) -> EnvironmentCertificate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for EnvironmentCertificate

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for EnvironmentCertificate

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for EnvironmentCertificate

fn eq(&self, other: &EnvironmentCertificate) -> 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 Serialize for EnvironmentCertificate

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 EnvironmentCertificate