Module proof_kernel 

Small, solver-free rewrite certificate checker.

The checker derives both endpoints from a certificate and compares those derived terms with the supplied endpoints. It never calls a rewrite search, reads a transform proof object, or accepts a producer-owned boolean.

This kernel has deliberately narrow authority:

• it cannot establish that a rule catalog is sound;
• it cannot establish that an observer profile models browser behaviour;
• it cannot detect a defect shared with an external side-condition source;
• it cannot see a defect that moves both sides of a comparison identically;
• for genuinely IR-computed requirements, it can add disclosure without adding independent semantic strength.

Structs

CanonicalRewriteAssumptionV0

CanonicalRewriteAssumptionsV0

CascadeWinnerEqualityCertV0

CascadeWinnerKeyCertV0

CertificateRejectionV0

ComputedValueEnvironmentEntryV0

ComputedValueEqualityCertV0

RewriteCertificateEnvelopeV0

RewriteFailureSiteV0

RewriteIssuanceTokenV0

Token issued only after the checker derives and matches both endpoints.

RewriteOperatorV0

RewriteRuleCatalogV0

RewriteRuleV0

RewriteSubstitutionEntryV0

SourceMapTraceCertV0

SourceMapTraceSegmentV0

TokenOwnershipCertEntryV0

TokenOwnershipSeparabilityCertV0

TransformIndependenceCertV0

TransformIndependenceObservationCertRowV0

Enums

CascadeLevelCertV0

CertificateRejectionKindV0

ComputedValueTermV0

RewriteCertificateV0

RewriteCheckInputV0

RewritePatternV0

RewriteSideConditionKindV0

RewriteTermV0

SideConditionCertV0

Constants

CANONICAL_REWRITE_ASSUMPTIONS_SCHEMA_VERSION_V0

REWRITE_CERTIFICATE_MAX_DEPTH_V0

REWRITE_CERTIFICATE_MAX_NODES_V0

REWRITE_CERTIFICATE_SCHEMA_VERSION_V0

REWRITE_RULE_CATALOG_MAX_OPERATORS_V0

REWRITE_RULE_CATALOG_MAX_RULES_V0

REWRITE_RULE_CATALOG_SCHEMA_ID_V0

REWRITE_RULE_CATALOG_SCHEMA_VERSION_V0

Functions

check_optional_rewrite_certificate_v0

check_rewrite_certificate_v0

check_serialized_rewrite_certificate_v0

rewrite_rule_catalog_content_digest_hex_v0

Return the order-independent digest used to bind an issuance token to the exact catalog content checked by the kernel.

selector_rewrite_rule_catalog_v0

selector_rewrite_rule_catalog_with_cascade_winner_equality_v0