Skip to main content

core::proof — Proof infrastructure

Runtime support for @verify(certified) and proof-carrying bytecode. Two public files; one legacy.

FileWhat's in it
pcc.vrGoalHash, ProofCertificate, ProofBundle, BundleMetadata, BundleCert, bundle ops
reflection.vrReflectedFunction, ReflectabilityVerdict, reflection SMT-LIB rendering
contracts_old.vrlegacy contract machinery (internal; replaced by Hoare logic in verum_verification)

Proof-Carrying Code — pcc.vr​

The Necula-style proof bundle: a VBC module can carry certificates for the SMT goals its compilation discharged, so downstream consumers can re-verify the proofs without invoking the whole compiler.

GoalHash​

type GoalHash is { digest: Text };         // SHA-256 of the SMT-LIB goal

fn goal_hash(digest: Text) -> GoalHash

ProofCertificate​

type ProofCertificate is {
    goal_text: Text,                     // rendered SMT-LIB goal
    solver: Text,                        // "z3" | "cvc5" | "portfolio" | "manual"
    proof_object: Text,                  // solver-native proof term (base64)
    duration_ms: Int { >= 0 },
    timestamp: Text,                     // ISO-8601
};

fn proof_certificate(
    goal_text: Text,
    solver: Text,
    proof_object: Text,
    duration_ms: Int { >= 0 },
    timestamp: Text,
) -> ProofCertificate

BundleMetadata​

type BundleMetadata is {
    compiler_version: Text,
    source_path: Text,
    certificate_count: Int { >= 0 },
    total_duration_ms: Int { >= 0 },
};

ProofBundle​

type BundleCert is { hash: GoalHash, cert: ProofCertificate };

type ProofBundle is {
    certificates: List<BundleCert>,
    metadata: BundleMetadata,
};

fn empty_bundle(compiler_version: Text, source_path: Text) -> ProofBundle
fn bundle_add(b: ProofBundle, h: GoalHash, c: ProofCertificate) -> ProofBundle
fn bundle_lookup(b: &ProofBundle, digest: Text) -> Maybe<&ProofCertificate>
fn bundle_size(b: &ProofBundle) -> Int
fn bundle_total_duration_ms(b: &ProofBundle) -> Int
fn bundle_merge(a: ProofBundle, b: ProofBundle) -> ProofBundle

Example​

let mut bundle = empty_bundle("verum-0.32", "src/main.vr");

let cert = proof_certificate(
    "(assert (not (forall ((x Int)) (=> (> x 0) (> (+ x 1) 0)))))",
    "z3",
    BASE64_PROOF_BLOB,
    duration_ms = 3,
    timestamp = "2026-04-15T20:30:00Z",
);
bundle = bundle_add(bundle, goal_hash("g/binary_search/postcond#1"), cert);

if let Maybe.Some(c) = bundle_lookup(&bundle, "g/binary_search/postcond#1") {
    print(f"verified by {c.solver} in {c.duration_ms} ms");
}

Embedding into VBC​

verum_vbc serialises a ProofBundle into the VBC archive's proof_certificates section when @verify(certified) is in effect. A consumer can:

  • trust the certificate and skip verification;
  • re-verify offline by feeding cert.goal_text + cert.proof_object back into the named solver;
  • reject if the bundle is missing or invalid.

Refinement reflection — reflection.vr​

Lets user-defined @logic functions appear as axioms in the SMT solver. The soundness gate enforces that only pure + total + closed functions are reflectable — the rest are rejected by the compiler.

ReflectedFunction​

type ReflectedFunction is {
    name: Text,
    parameters: List<Text>,
    body_smtlib: Text,
    return_sort: Text,
    parameter_sorts: List<Text>,
};

fn reflected_fn(
    name: Text,
    parameters: List<Text>,
    body_smtlib: Text,
    return_sort: Text,
    parameter_sorts: List<Text>,
) -> ReflectedFunction

ReflectabilityVerdict​

type ReflectabilityVerdict is
    | Reflectable
    | NotReflectable { reason: Text };

fn is_reflectable(
    name: Text,
    is_pure: Bool,
    is_total: Bool,
    is_closed: Bool,
) -> ReflectabilityVerdict

A function is reflectable iff all three conditions hold. Typical failure reasons: calls to IO, non-structural recursion without a decreases measure, free variables captured from environment.

SMT-LIB rendering​

fn to_smtlib_decl(f: &ReflectedFunction) -> Text
fn to_smtlib_axiom(f: &ReflectedFunction) -> Text
  • to_smtlib_decl emits a declare-fun for uninterpreted use.
  • to_smtlib_axiom emits a define-fun-rec with the function's body.

Example​

@logic
fn is_sorted(xs: &List<Int>) -> Bool {
    forall i in 0..xs.len() - 1. xs[i] <= xs[i + 1]
}

// Compiler generates equivalent ReflectedFunction:
let r = reflected_fn(
    "is_sorted",
    list!["xs"],
    "(forall ((i Int)) (=> (and (>= i 0) (< i (- (List.len xs) 1))) (<= (List.get xs i) (List.get xs (+ i 1)))))",
    "Bool",
    list!["(List Int)"],
);

// The axiom form is what the solver sees:
let ax = to_smtlib_axiom(&r);

Now Sorted<Int> is List<Int> { is_sorted(self) } is a usable refinement, with is_sorted as a named predicate the SMT solver can unfold on demand.

Cross-references​