Skip to content

Kani CI failing since adding range-check to CompactSize deserialization #5954

Description

@i-a-m-d

After #5697, which added a range-check to CompactSize deserialization, two Kani proofs now fail:

Manual Harness Summary:
Verification failed for - consensus::verification::check_compact_size_large_u64_roundtrip
Verification failed for - consensus::verification::check_compact_size_roundtrip
Complete - 5 successfully verified harnesses, 2 failures, 7 total.

Initially reported in #5883.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions