Crate omena_cascade_proof 

Product-owned cascade proof contracts.

The default solver-free proof path is part of the shipped product surface: product diagnostics and transform safety checks rely on it even when no external solver is enabled. Solver-backed experiments live outside this crate.

Re-exports

pub use discharge_ledger::DISCHARGE_LEDGER_PRODUCT_V1;

pub use discharge_ledger::DISCHARGE_LEDGER_SCHEMA_VERSION_V1;

pub use discharge_ledger::DischargeLedgerLookupStatusV0;

pub use discharge_ledger::DischargeLedgerLookupV0;

pub use discharge_ledger::DischargeLedgerVerdictV0;

pub use discharge_ledger::discharge_ledger_cell_key_v0;

pub use discharge_ledger::lookup_discharge_ledger_entry_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 proof_kernel::*;

Modules

discharge_ledger

fuzz

proof_kernel

Small, solver-free rewrite certificate checker.

Structs

CanonicalSmtInputV0

CascadeSMTProofV0

LayerFlattenInversionVerdictV0

LayerInversionDeclarationV0

SmtBackendCheckV0

StubSmtBackendV0

TransformRewriteProofInputV0

Enums

SmtBackendKindV0

SmtBackendSatResultV0

SmtVerdictV0

Constants

SMT_FEATURE_GATE_V0

SMT_LAYER_MARKER_V0

SMT_SCHEMA_VERSION_V0

TRANSFORM_REWRITE_PROOF_INPUT_OBLIGATION_FAMILY_V0

Traits

SmtBackendV0

Functions

canonical_input_has_unknown_v0

canonical_layer_flatten_inversion_input_v0

canonical_requirement_value_v0

canonical_smt_input_v0

canonical_smt_input_with_script_v0

canonical_smtlib2_script_v0

canonicalize_layer_inversion_declarations_v0

cascade_spec_digest_v0

layer_inversion_declaration_v0

smt_check_layer_flatten_inversion_v0

smt_evaluate_static_supports_condition_v0

smt_prove_box_shorthand_combination_v0

smt_prove_layer_flatten_candidate_v0

smt_prove_longhand_merge_v0

smt_prove_scope_flatten_candidate_v0

smt_verify_transform_rewrite_candidate_v0