Crate omena_smt 

SMT-encoded cascade verification contracts.

The crate keeps the M4-gamma three-layer split explicit: L1 cascade proof primitives remain in omena-cascade, L2 refinement delegates live beside the cascade crate, and this crate owns L3 encoding, proof contracts, backend selection, and unsat-core audit metadata.

Most obligations are propositional (require:name=bool) conjunctions the Rust code already decided; the layer_inversion obligation is the exception, emitting a QF_LIA cascade-ordering search the opt-in smt-z3 backend genuinely solves and the propositional stub cannot.

claim_level: default stub plus opt-in solver-backed checking, where the opt-in z3 backend genuinely solves one non-trivial QF_LIA cascade-ordering obligation the stub cannot, while the remaining obligations stay propositional and not default build SMT completeness.

Re-exports

pub use backend::SmtBackendCheckV0;

pub use backend::SmtBackendKindV0;

pub use backend::SmtBackendSatResultV0;

pub use backend::SmtBackendV0;

pub use backend::StubSmtBackendV0;

pub use encoder::CanonicalSmtInputV0;

pub use encoder::canonical_smt_input_v0;

pub use encoder::canonical_smt_input_with_script_v0;

pub use encoder::canonical_smtlib2_script_v0;

pub use fuzz::SmtBisimulationFuzzCaseV0;

pub use fuzz::SmtBisimulationFuzzReportV0;

pub use fuzz::run_smt_bisimulation_fuzz_case_v0;

pub use fuzz::run_smt_bisimulation_fuzz_seed_corpus_v0;

pub use fuzz::smt_bisimulation_fuzz_case_v0;

pub use layer_inversion::LayerFlattenInversionVerdictV0;

pub use layer_inversion::LayerInversionDeclarationV0;

pub use layer_inversion::canonical_layer_flatten_inversion_input_v0;

pub use layer_inversion::layer_inversion_declaration_v0;

pub use layer_inversion::smt_check_layer_flatten_inversion_v0;

pub use obligations::smt_evaluate_static_supports_condition_v0;

pub use obligations::smt_prove_box_shorthand_combination_v0;

pub use obligations::smt_prove_layer_flatten_candidate_v0;

pub use obligations::smt_prove_scope_flatten_candidate_v0;

pub use proof::CascadeSMTProofAuditLogV0;

pub use proof::CascadeSMTProofV0;

pub use proof::SmtVerdictV0;

pub use proof::cascade_spec_digest_v0;

pub use theory::CascadeTheorySignatureV0;

pub use theory::cascade_theory_signature_v0;

pub use unsat_core::CascadeUnsatCoreLabelV0;

pub use unsat_core::cascade_unsat_core_label_v0;

Modules

backend

encoder

fuzz

layer_inversion

Non-trivial cascade-ordering obligation for @layer flattening.

obligations

proof

theory

unsat_core

Constants

SMT_FEATURE_GATE_V0

SMT_LAYER_MARKER_V0

SMT_SCHEMA_VERSION_V0