oxilean_kernel/proof_cert/mod.rs
1//! Proof Certificate System for OxiLean Kernel.
2//!
3//! A proof certificate is a compact, checkable record that a term has been
4//! verified by the kernel. Certificates enable exporting and importing proofs
5//! without re-checking from scratch: the consumer verifies structural hashes
6//! and, optionally, replays reduction steps.
7//!
8//! # Overview
9//!
10//! 1. **Create** — call [`create_certificate`] immediately after the kernel
11//! accepts a declaration to produce a `ProofCertificate`.
12//! 2. **Store** — add certificates to a [`CertificateStore`] for persistence.
13//! 3. **Verify** — call [`verify_certificate`] (or [`CertificateStore::verify_all`])
14//! to check that stored hashes still match the live environment.
15//! 4. **Serialize / deserialize** — use [`serialize_cert`] / [`deserialize_cert`]
16//! to persist certificates as text (e.g. in `.oxicert` files).
17
18pub mod functions;
19pub mod types;
20
21pub use functions::{
22 create_certificate, deserialize_cert, hash_declaration, hash_expr, serialize_cert,
23 verify_certificate,
24};
25pub use types::{CertCheckResult, CertificateStore, ProofCertId, ProofCertificate, ProofStep};