List of all items

Structs

• CanonicalSmtInputV0
• CascadeSMTProofV0
• LayerFlattenInversionVerdictV0
• LayerInversionDeclarationV0
• SmtBackendCheckV0
• StubSmtBackendV0
• TransformRewriteProofInputV0
• discharge_ledger::DischargeLedgerLookupV0
• fuzz::SmtBisimulationFuzzCaseV0
• fuzz::SmtBisimulationFuzzReportV0
• proof_kernel::CanonicalRewriteAssumptionV0
• proof_kernel::CanonicalRewriteAssumptionsV0
• proof_kernel::CascadeWinnerEqualityCertV0
• proof_kernel::CascadeWinnerKeyCertV0
• proof_kernel::CertificateRejectionV0
• proof_kernel::ComputedValueEnvironmentEntryV0
• proof_kernel::ComputedValueEqualityCertV0
• proof_kernel::RewriteCertificateEnvelopeV0
• proof_kernel::RewriteFailureSiteV0
• proof_kernel::RewriteIssuanceTokenV0
• proof_kernel::RewriteOperatorV0
• proof_kernel::RewriteRuleCatalogV0
• proof_kernel::RewriteRuleV0
• proof_kernel::RewriteSubstitutionEntryV0
• proof_kernel::SourceMapTraceCertV0
• proof_kernel::SourceMapTraceSegmentV0
• proof_kernel::TokenOwnershipCertEntryV0
• proof_kernel::TokenOwnershipSeparabilityCertV0
• proof_kernel::TransformIndependenceCertV0
• proof_kernel::TransformIndependenceObservationCertRowV0

Enums

• SmtBackendKindV0
• SmtBackendSatResultV0
• SmtVerdictV0
• discharge_ledger::DischargeLedgerLookupStatusV0
• discharge_ledger::DischargeLedgerVerdictV0
• proof_kernel::CascadeLevelCertV0
• proof_kernel::CertificateRejectionKindV0
• proof_kernel::ComputedValueTermV0
• proof_kernel::RewriteCertificateV0
• proof_kernel::RewriteCheckInputV0
• proof_kernel::RewritePatternV0
• proof_kernel::RewriteSideConditionKindV0
• proof_kernel::RewriteTermV0
• proof_kernel::SideConditionCertV0

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
• discharge_ledger::discharge_ledger_cell_key_v0
• discharge_ledger::lookup_discharge_ledger_entry_v0
• fuzz::run_smt_bisimulation_fuzz_case_v0
• fuzz::run_smt_bisimulation_fuzz_seed_corpus_v0
• fuzz::smt_bisimulation_fuzz_case_v0
• layer_inversion_declaration_v0
• proof_kernel::check_optional_rewrite_certificate_v0
• proof_kernel::check_rewrite_certificate_v0
• proof_kernel::check_serialized_rewrite_certificate_v0
• proof_kernel::rewrite_rule_catalog_content_digest_hex_v0
• proof_kernel::selector_rewrite_rule_catalog_v0
• proof_kernel::selector_rewrite_rule_catalog_with_cascade_winner_equality_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

Constants

• SMT_FEATURE_GATE_V0
• SMT_LAYER_MARKER_V0
• SMT_SCHEMA_VERSION_V0
• TRANSFORM_REWRITE_PROOF_INPUT_OBLIGATION_FAMILY_V0
• discharge_ledger::DISCHARGE_LEDGER_PRODUCT_V1
• discharge_ledger::DISCHARGE_LEDGER_SCHEMA_VERSION_V1
• proof_kernel::CANONICAL_REWRITE_ASSUMPTIONS_SCHEMA_VERSION_V0
• proof_kernel::REWRITE_CERTIFICATE_MAX_DEPTH_V0
• proof_kernel::REWRITE_CERTIFICATE_MAX_NODES_V0
• proof_kernel::REWRITE_CERTIFICATE_SCHEMA_VERSION_V0
• proof_kernel::REWRITE_RULE_CATALOG_MAX_OPERATORS_V0
• proof_kernel::REWRITE_RULE_CATALOG_MAX_RULES_V0
• proof_kernel::REWRITE_RULE_CATALOG_SCHEMA_ID_V0
• proof_kernel::REWRITE_RULE_CATALOG_SCHEMA_VERSION_V0