Enum Certificate 

pub enum Certificate {
    Ring {
        lhs: RingExpr,
        rhs: RingExpr,
    },
    BoolCases {
        vars: u8,
        lhs: BoolExpr,
        rhs: BoolExpr,
    },
    Bitvector {
        check: fn() -> Result<(), String>,
    },
    LogosProperty {
        program: &'static str,
        expected: &'static str,
    },
}

Variants

Ring

lhs = rhs as polynomials — kernel ring tactic.

Fields

lhs: RingExpr

rhs: RingExpr

BoolCases

lhs = rhs for all Bool valuations of vars variables — each side normalized by the kernel.

Fields

vars: u8

lhs: BoolExpr

rhs: BoolExpr

Bitvector

Wrapping-i64 identity checked exhaustively on the boundary grid by the named check function (upgraded to a Z3 proof in M15).

Fields

check: fn() -> Result<(), String>

LogosProperty

An executable LOGOS property program (D11b — the language is its own test substrate): the program generates a deterministic corpus, compares the rule’s two sides over it, and Shows its failure count. Certification = the tree-walker printing expected.

Fields

program: &'static str

expected: &'static str