Enum CheckResult 

pub(crate) enum CheckResult {
    ProvedByRule,
    ProvedBySmt,
    Failed,
    Unknown(UnknownReason),
}

Verification status for one required property on one path.

Variants

ProvedByRule

Proved by a sound structural rule (a fast-path that needs no solver query): ZST guards, zero-element access, tracked invariants/flags, type-level transparency, provenance-origin classification. These are the rules that must be audited for soundness.

ProvedBySmt

Proved by an SMT query: the solver showed the negation is unsatisfiable (numeric bounds, byte-range coverage, alignment modulo/linear checks).

Failed

The verifier found a possible violation for this path.

Unknown(UnknownReason)

The verifier has not implemented or completed the proof for this path; the reason is carried in the payload.

Implementations

impl CheckResult

pub(crate) fn is_proved(&self) -> bool

Whether this result counts as “proved” (by rule or by SMT).

pub(crate) fn label(&self) -> &'static str

The user-facing label for this result. ProvedByRule and ProvedBySmt both report as "Proved" — the rule/SMT distinction is an internal audit signal, not part of the report. An Unknown result is suffixed with its reason when it is not the generic unimplemented case.

pub(crate) fn and(self, other: CheckResult) -> CheckResult

AND-combine two results: any Failed → Failed; any Unknown → Unknown; only all-proved → proved (Rule when every conjunct was a rule, otherwise Smt).

pub(crate) fn or(self, other: CheckResult) -> CheckResult

OR-combine two results: any proved → proved (a Rule proof dominates); all Failed → Failed; otherwise Unknown.

Trait Implementations

impl Clone for CheckResult

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CheckResult

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

Formats the value using the given formatter.

impl PartialEq for CheckResult

fn eq(&self, other: &Self) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for CheckResult