Module proof_cert 

Proof Certificate System — compact, verifiable records of kernel-checked proofs. Proof Certificate System for OxiLean Kernel.

A proof certificate is a compact, checkable record that a term has been verified by the kernel. Certificates enable exporting and importing proofs without re-checking from scratch: the consumer verifies structural hashes and, optionally, replays reduction steps.

Overview

1. Create — call create_certificate immediately after the kernel accepts a declaration to produce a ProofCertificate.
2. Store — add certificates to a CertificateStore for persistence.
3. Verify — call verify_certificate (or CertificateStore::verify_all) to check that stored hashes still match the live environment.
4. Serialize / deserialize — use serialize_cert / deserialize_cert to persist certificates as text (e.g. in .oxicert files).

Re-exports

pub use functions::create_certificate;

pub use functions::deserialize_cert;

pub use functions::hash_declaration;

pub use functions::hash_expr;

pub use functions::serialize_cert;

pub use functions::verify_certificate;

pub use types::CertCheckResult;

pub use types::CertificateStore;

pub use types::ProofCertId;

pub use types::ProofCertificate;

pub use types::ProofStep;

Modules

functions

Functions for the Proof Certificate System.

types

Types for the Proof Certificate System.