Skip to content

Certificate-check the 52 by(bit_vector) ASIL-D obligations with ordeal (drop unchecked Z3 for the BV fragment) #173

Description

@avrabe

gale's 39 Verus modules ("805 properties verified by Z3") include 52 by(bit_vector) obligations (src/fault_decode.rs, src/mpu.rs, src/cpu_mask.rs, work.rs, userspace.rs, event.rs, atomic.rs) that are pure QF_BV — u8/u32/u64, only bitwise/shift/sub/compare — discharged today by unchecked Z3 inside a safety case (artifacts/safety_case.yaml) that names "Verus SMT/Z3" as the evidence.

Proposal: re-discharge those leaf obligations through ordeal (pure-Rust, certificate-checked QF_BV; ordeal = "0.9") and bind the portable cert.recheck()-able LRAT certificate as ASIL-D evidence — the CompCert-style "the solver is untrusted, the checker is Lean-proven" argument. Highest-value sites: mpu.rs/cpu_mask.rs (memory-isolation validity) and fault_decode.rs (mask disjointness/exhaustiveness).

Enabler: an SMT-LIB2 QF_BV front-end so ordeal ingests the VC Verus already emits to Z3 — ordeal roadmap pulseengine/ordeal#65 (v0.11.0). Boundary: only the leaf by(bit_vector) lemmas are QF_BV; the 805 top-level forall/exists properties need quantifiers and stay on Verus/Rocq/Lean.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions