mirror of
https://github.com/block/buzz.git
synced 2026-10-28 04:51:40 +00:00
b0aafc41e7
The equivalence catch-all sent every unclassified field to identity-class byte-equality, but the provenance class named only snapshot version and verification-key identity. The remaining revalidation_dependencies members -- binding, lifecycle, local-policy, and resource versions; status source and version; proof and replay witnesses; the confidential JWS handle -- defaulted to byte-equality, making "changed dependencies require current revalidation to an equivalent result" unsatisfiable on any version bump and the concurrent-enrollment recompute never equivalent. Both readings failed closed; this was an availability and interoperability defect. The repair classifies every revalidation_dependencies member: bounds-class if it is a deadline, provenance-class otherwise, with the identity-class catch-all narrowed to assertion-content fields. Provenance-class ignoring is conditional on successful current revalidation, so it is safe only for members final admission actually rereads -- and the reread list at final admission named status nowhere, while the per-use check already checks status versions. Under the guards as literally written, demoting status to provenance-class would have let final admission admit with upstream status inactive: the one dependency the residual-revocation bound exists to close. Status joins the final-admission reread list. Verified by a bounded model of the composed system in two encodings (strict = inferred guards, literal = written guards only), 8748 reachable states per arm: baseline classification reads 0 authority extensions / 127 unsatisfiable in both encodings; the reclassification without the status reread reads 64 extensions under the literal encoding, all rooted in status_active=False; with the status reread, 0 extensions and 0 unsatisfiable in both encodings. Controls: a deadline demoted to provenance-class is detected (128 states, still detected against the fixed reread set), and a per-member sweep is structurally blind to the status defect -- only promoting a predicate's whole detector group exposes it. Delegated leases carry their own dependency list in NIP-FI-DELEG and were not remodelled; this classification governs the direct-path equivalence rule it amends. Co-authored-by: Eva <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz> Signed-off-by: Eva <011987e296fd5006292d2f930b574be47c7801048d1983c46c425d3c95f0cffd@buzz.block.builderlab.xyz>