Crate guarded_continuation_checker

Expand description

Stable client APIs for GCC predicate and named event-contract workflows.

The verifier implementation remains in the separately versioned executable. This library invokes it directly without a shell and validates its advertised versioned CLI contract before exposing typed certificate operations.

Modules§

aiger_obligation: Exact, resource-bounded AIGER transition evaluation and CNF obligations.
btor2: Strict, resource-bounded BTOR2 bit-vector semantic core.
btor2_bitblast: Proof-carrying bounded bit-blasting for the strict BTOR2 semantic core.
btor2_bounded: Static exact portfolio for bounded BTOR2 reachability.
btor2_braking: Exact compressed SAFE certificates for a resettable braking controller.
btor2_component: Exact source-separated controller and plant verification certificates.
btor2_family: Canonical structural composition for repeated BTOR2 component families.
btor2_family_orbit: Representative proof reuse for structurally identical BTOR2 channel orbits.
btor2_family_proof: Exact both-answer evidence over source-bound BTOR2 channel families.
btor2_invariant_chain: Exact invariant-chained recurrence analysis for bounded BTOR2 property sets.
btor2_motion: Exact compressed SAFE certificates for a coupled velocity-position recurrence.
btor2_phase: Source-bound closed-form certificates for a strict BTOR2 counter subset.
btor2_predicate_set: Proof-carrying batches of bounded BTOR2 predicates over one recurrence.
btor2_region: Exact compressed SAFE certificates for recognised one-word BTOR2 recurrences.
btor2_region_equivalence: Exact structural equivalence for extracted repeated BTOR2 channel regions.
btor2_region_extract: Static repeated-state region extraction for source-attested Yosys BTOR2.
btor2_region_property: Exact channel-local property models over source-bound repeated BTOR2 regions.
btor2_search: Exact bounded reachability certificates for the strict BTOR2 semantic core.
compiled_mmio_branching_dag: Exact finite-domain control-flow DAG for compiled-MMIO execution.
compiled_mmio_certificate: Canonical certificate binding a bounded compiled-MMIO extraction to its complete source, toolchain, image and symbol inputs.
compiled_mmio_decode_graph: Source-bound multi-successor decode graph for compiled-MMIO execution.
compiled_mmio_explicit_transcript: Canonical explicit execution transcripts for the compiled-MMIO closest system baseline.
compiled_mmio_file: Strict file boundary for compiled-MMIO certificates.
compiled_mmio_predicate_certificate: Canonical bounded evidence for an exact finite-domain compiled-MMIO predicate workflow.
compiled_mmio_predicate_portfolio: Static routing between finite-domain predicate evidence and the complete exact compiled-MMIO reference.
compiled_mmio_quotient: Exact all-input reference for guarded compiled-MMIO continuation research.
compiled_mmio_rtl_certificate: Canonical proof-carrying evidence for the retained compiled-firmware to OpenTitan PWM RTL composition.
compiled_mmio_rtl_mapping: Exact translation from the retained OpenTitan PWM MMIO schedule to the source-attested per-channel RTL input boundary.
composed_witness: Deterministic safety-witness composition for the FM 2026 baseline.
controller_mtbdd: Source-bound exact controller functions represented as reduced MTBDDs.
controller_mtbdd_proof: Proof-carrying equivalence between an AIGER controller and an exact MTBDD.
controller_plant: Exact sampled-control composition of a verified controller transducer and plant.
controller_plant_aiger: Bounded-equivalent AIGER export for sampled controller and plant composition.
controller_plant_artifact: Canonical, source-bound artifacts for proof-carrying controller/plant batches.
controller_transducer: Source-bound, proof-carrying symbolic controller transducers.
dense_relation: Resource-bounded finite relations for proof-carrying interface composition.
firmware_transaction_contract: Proof-carrying composition of one fixed firmware transaction contract with an exact two-component RTL revision-impact bundle.
revision_batch: Canonical content-addressed batches for revision-local certificates.
revision_impact: Canonical bounded certificates for revision-impact counterfactuals.
revision_local: Canonical envelope primitives for revision-local component evidence.
riscv32imc: Bounded RV32IMC execution for source-bound firmware contract extraction.
riscv32imc_predicate: Exact finite-domain RV32IMC execution for one canonical input predicate.
riscv32imc_predicate_checker: Independent scalar checker for finite-domain predicate transducer evidence.
source_model_attestation: Canonical source-to-model attestation verification.
unsat_proof: Resource-bounded generation and independent checking of Varisat UNSAT proofs.