bits.rs

//! Handwritten reference implementations for prospective Vest DSL bit-packed formats.
//!
//! The corresponding DSL shapes are roughly:
//!
//! ```vest
//! !BIG_ENDIAN
//!
//! version_ihl = bits {
//!     version: u4,
//!     ihl: u4,
//! }
//!
//! cross_byte_span = bits {
//!     prefix: u3,
//!     span: u10,
//!     suffix: u3,
//! }
//!
//! payload_kind = enum {
//!     Raw         = 0u3,
//!     Words       = 1u3,
//!     Tiny        = 2u3,
//!     ...
//! }
//!
//! packet_header = bits {
//!     @kind: payload_kind,
//!     @count: u5 | { 1..31 },
//!     @len: u8,
//! }
//!
//! choice_packet = {
//!     @hdr: packet_header,
//!     payload: choose(@hdr.kind) {
//!         Raw        => [u8; @hdr.len],
//!         Words      => [u16; @hdr.count],
//!         Tiny       => u8,
//!         _          => [u8; @hdr.len],
//!     },
//! }
//!
//! closed_payload_kind = enum {
//!     Raw         = 0u3,
//!     Words       = 1u3,
//!     Tiny        = 2u3,
//! }
//!
//! closed_packet_header = bits {
//!     @kind: closed_payload_kind,
//!     @count: u5 | { 1..31 },
//!     @len: u8,
//! }
//!
//! closed_choice_packet = {
//!     @hdr: closed_packet_header,
//!     payload: choose(@hdr.kind) {
//!         Raw        => [u8; @hdr.len],
//!         Words      => [u16; @hdr.count],
//!         Tiny       => u8,
//!     },
//! }
//! ```
//!
use crate::combinators::bits::Bits;
use crate::combinators::mapped::spec::*;
use crate::combinators::*;
use crate::core::exec::input::{InputBuf, InputSlice};
use crate::core::exec::output::OutputBuf;
use crate::core::exec::parser::*;
use crate::core::exec::serializer::*;
use crate::core::exec::ParseError;
use crate::core::spec::*;
use crate::core::{proof::*, spec};
use vstd::prelude::*;
verus! {

// ============================================================
// Data Types
// ============================================================
#[derive(Debug, PartialEq, Eq, Clone, Copy)]
#[verifier::ext_equal]
pub struct VersionIhl {
    pub version: u8,
    pub ihl: u8,
}

pub type VersionIhlSpec = VersionIhl;

pub type VersionIhlInner = u8;

impl DeepView for VersionIhl {
    type V = Self;

    open spec fn deep_view(&self) -> Self::V {
        *self
    }
}

#[derive(Debug, PartialEq, Eq, Clone, Copy)]
#[verifier::ext_equal]
pub struct CrossByteSpan {
    pub prefix: u8,
    pub span: u16,
    pub suffix: u8,
}

pub type CrossByteSpanSpec = CrossByteSpan;

pub type CrossByteSpanInner = u16;

impl DeepView for CrossByteSpan {
    type V = Self;

    open spec fn deep_view(&self) -> Self::V {
        *self
    }
}

#[repr(u8)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Structural)]
pub enum PayloadKind {
    Raw = 0,
    Words = 1,
    Tiny = 2,
    Unknown(u8),
}

pub type PayloadKindSpec = PayloadKind;

impl DeepView for PayloadKind {
    type V = Self;

    open spec fn deep_view(&self) -> Self::V {
        *self
    }
}



#[derive(Debug, PartialEq, Eq, Clone, Copy)]
#[verifier::ext_equal]
pub struct PacketHeader {
    pub kind: PayloadKind,
    pub count: u8,
    pub len: u8,
}

pub type PacketHeaderSpec = PacketHeader;

pub type PacketHeaderInner = u16;

impl DeepView for PacketHeader {
    type V = Self;

    open spec fn deep_view(&self) -> Self::V {
        *self
    }
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub enum ChoicePayload<'i> {
    Raw(&'i [u8]),
    Words(Vec<u16>),
    Tiny(u8),
    Default(&'i [u8]),
}

#[verifier::ext_equal]
pub enum ChoicePayloadSpec {
    Raw(Seq<u8>),
    Words(Seq<u16>),
    Tiny(u8),
    Default(Seq<u8>),
}

pub type ChoicePayloadInner = Sum<Seq<u8>, Sum<Seq<u16>, Sum<u8, Seq<u8>>>>;

impl<'i> DeepView for ChoicePayload<'i> {
    type V = ChoicePayloadSpec;

    open spec fn deep_view(&self) -> Self::V {
        match self {
            ChoicePayload::Raw(bytes) => ChoicePayloadSpec::Raw(bytes.deep_view()),
            ChoicePayload::Words(words) => ChoicePayloadSpec::Words(words.deep_view()),
            ChoicePayload::Tiny(x) => ChoicePayloadSpec::Tiny(x.deep_view()),
            ChoicePayload::Default(bytes) => ChoicePayloadSpec::Default(bytes.deep_view()),
        }
    }
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct ChoicePacket<'i> {
    pub hdr: PacketHeader,
    pub payload: ChoicePayload<'i>,
}

#[verifier::ext_equal]
pub struct ChoicePacketSpec {
    pub hdr: PacketHeaderSpec,
    pub payload: ChoicePayloadSpec,
}

pub type ChoicePacketInner = (PacketHeaderSpec, ChoicePayloadSpec);

impl<'i> DeepView for ChoicePacket<'i> {
    type V = ChoicePacketSpec;

    open spec fn deep_view(&self) -> Self::V {
        ChoicePacketSpec { hdr: self.hdr.deep_view(), payload: self.payload.deep_view() }
    }
}

#[repr(u8)]
#[derive(Debug, PartialEq, Eq, Clone, Copy, Structural)]
pub enum ClosedPayloadKind {
    Raw = 0,
    Words = 1,
    Tiny = 2,
}

pub type ClosedPayloadKindSpec = ClosedPayloadKind;

impl DeepView for ClosedPayloadKind {
    type V = Self;

    open spec fn deep_view(&self) -> Self::V {
        *self
    }
}



#[derive(Debug, PartialEq, Eq, Clone, Copy)]
#[verifier::ext_equal]
pub struct ClosedPacketHeader {
    pub kind: ClosedPayloadKind,
    pub count: u8,
    pub len: u8,
}

pub type ClosedPacketHeaderSpec = ClosedPacketHeader;

pub type ClosedPacketHeaderInner = u16;

impl DeepView for ClosedPacketHeader {
    type V = Self;

    open spec fn deep_view(&self) -> Self::V {
        *self
    }
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub enum ClosedChoicePayload<'i> {
    Raw(&'i [u8]),
    Words(Vec<u16>),
    Tiny(u8),
}

#[verifier::ext_equal]
pub enum ClosedChoicePayloadSpec {
    Raw(Seq<u8>),
    Words(Seq<u16>),
    Tiny(u8),
}

pub type ClosedChoicePayloadInner = Sum<Seq<u8>, Sum<Seq<u16>, u8>>;

impl<'i> DeepView for ClosedChoicePayload<'i> {
    type V = ClosedChoicePayloadSpec;

    open spec fn deep_view(&self) -> Self::V {
        match self {
            ClosedChoicePayload::Raw(bytes) => ClosedChoicePayloadSpec::Raw(bytes.deep_view()),
            ClosedChoicePayload::Words(words) => ClosedChoicePayloadSpec::Words(words.deep_view()),
            ClosedChoicePayload::Tiny(x) => ClosedChoicePayloadSpec::Tiny(x.deep_view()),
        }
    }
}

#[derive(Debug, PartialEq, Eq, Clone)]
pub struct ClosedChoicePacket<'i> {
    pub hdr: ClosedPacketHeader,
    pub payload: ClosedChoicePayload<'i>,
}

#[verifier::ext_equal]
pub struct ClosedChoicePacketSpec {
    pub hdr: ClosedPacketHeaderSpec,
    pub payload: ClosedChoicePayloadSpec,
}

pub type ClosedChoicePacketInner = (ClosedPacketHeaderSpec, ClosedChoicePayloadSpec);

impl<'i> DeepView for ClosedChoicePacket<'i> {
    type V = ClosedChoicePacketSpec;

    open spec fn deep_view(&self) -> Self::V {
        ClosedChoicePacketSpec { hdr: self.hdr.deep_view(), payload: self.payload.deep_view() }
    }
}

// ============================================================
// Bit helpers
// ============================================================
// Version/IHL field (version: u4, ihl: u4)
pub const VERSION_MASK: u8 = 0b00001111u8;

pub const IHL_MASK: u8 = 0b00001111u8;

pub const VERSION_SHIFT: u8 = 4u8;

pub const PREFIX_MASK_U16: u16 = 0b0000000000000111u16;

pub const SPAN_MASK: u16 = 0b0000001111111111u16;

pub const SUFFIX_MASK: u16 = 0b0000000000000111u16;

pub const PREFIX_SHIFT: u16 = 13u16;

pub const SPAN_SHIFT: u16 = 3u16;

pub const KIND_MASK: u16 = 0b0000000000000111u16;

pub const COUNT_MASK: u16 = 0b0000000000011111u16;

pub const LEN_MASK: u16 = 0b0000000011111111u16;

pub const KIND_SHIFT: u16 = 13u16;

pub const COUNT_SHIFT: u16 = 8u16;

pub const VERSION_MAX: u8 = 0b00010000u8;

pub const IHL_MAX: u8 = 0b00010000u8;

pub const PREFIX_MAX: u8 = 0b00001000u8;

pub const SPAN_MAX: u16 = 0b10000000000u16;

pub const SUFFIX_MAX: u8 = 0b00001000u8;

pub const KIND_MAX: u8 = 0b00001000u8;

pub const COUNT_MAX: u8 = 0b00100000u8;

#[verifier::allow_in_spec]
pub fn unpack_version_ihl(raw: u8) -> (u8, u8)
    returns
        (((raw >> VERSION_SHIFT) & VERSION_MASK), (raw & IHL_MASK)),
{
    (((raw >> VERSION_SHIFT) & VERSION_MASK), (raw & IHL_MASK))
}

#[verifier::allow_in_spec]
pub fn pack_version_ihl(version: u8, ihl: u8) -> u8
    returns
        ((version & VERSION_MASK) << VERSION_SHIFT) | (ihl & IHL_MASK),
{
    ((version & VERSION_MASK) << VERSION_SHIFT) | (ihl & IHL_MASK)
}

#[verifier::allow_in_spec]
pub fn version_ihl_bounds(version: u8, ihl: u8) -> bool
    returns
        version < VERSION_MAX && ihl < IHL_MAX,
{
    version < VERSION_MAX && ihl < IHL_MAX
}

pub broadcast proof fn lemma_version_ihl_unpack_pack(raw: u8)
    by (bit_vector)
    ensures
        #[trigger] pack_version_ihl(unpack_version_ihl(raw).0, unpack_version_ihl(raw).1) == raw,
{
}

pub broadcast proof fn lemma_version_ihl_pack_unpack(version: u8, ihl: u8)
    by (bit_vector)
    requires
        #[trigger] version_ihl_bounds(version, ihl),
    ensures
        unpack_version_ihl(pack_version_ihl(version, ihl)).0 == version,
        unpack_version_ihl(pack_version_ihl(version, ihl)).1 == ihl,
{
}

pub broadcast proof fn lemma_version_ihl_mapper_wf_in_out(i: u8)
    by (bit_vector)
    ensures
        #[trigger] version_ihl_bounds(unpack_version_ihl(i).0, unpack_version_ihl(i).1),
{
}

#[verifier::allow_in_spec]
pub fn unpack_cross_byte_span(raw: u16) -> (u8, u16, u8)
    returns
        (
            (((raw >> PREFIX_SHIFT) & PREFIX_MASK_U16) as u8),
            (((raw >> SPAN_SHIFT) & SPAN_MASK) as u16),
            ((raw & SUFFIX_MASK) as u8),
        ),
{
    (
        (((raw >> PREFIX_SHIFT) & PREFIX_MASK_U16) as u8),
        (((raw >> SPAN_SHIFT) & SPAN_MASK) as u16),
        ((raw & SUFFIX_MASK) as u8),
    )
}

#[verifier::allow_in_spec]
pub fn pack_cross_byte_span(prefix: u8, span: u16, suffix: u8) -> u16
    returns
        ((((prefix as u16) & PREFIX_MASK_U16) << PREFIX_SHIFT) | (((span as u16) & SPAN_MASK)
            << SPAN_SHIFT) | ((suffix as u16) & SUFFIX_MASK)),
{
    (((prefix as u16) & PREFIX_MASK_U16) << PREFIX_SHIFT) | (((span as u16) & SPAN_MASK)
        << SPAN_SHIFT) | ((suffix as u16) & SUFFIX_MASK)
}

#[verifier::allow_in_spec]
pub fn cross_byte_span_bounds(prefix: u8, span: u16, suffix: u8) -> bool
    returns
        prefix < PREFIX_MAX && span < SPAN_MAX && suffix < SUFFIX_MAX,
{
    prefix < PREFIX_MAX && span < SPAN_MAX && suffix < SUFFIX_MAX
}

pub broadcast proof fn lemma_cross_byte_span_unpack_pack(raw: u16)
    by (bit_vector)
    ensures
        #[trigger] pack_cross_byte_span(
            unpack_cross_byte_span(raw).0,
            unpack_cross_byte_span(raw).1,
            unpack_cross_byte_span(raw).2,
        ) == raw,
{
}

pub broadcast proof fn lemma_cross_byte_span_pack_unpack(prefix: u8, span: u16, suffix: u8)
    by (bit_vector)
    requires
        #[trigger] cross_byte_span_bounds(prefix, span, suffix),
    ensures
        unpack_cross_byte_span(pack_cross_byte_span(prefix, span, suffix)).0 == prefix,
        unpack_cross_byte_span(pack_cross_byte_span(prefix, span, suffix)).1 == span,
        unpack_cross_byte_span(pack_cross_byte_span(prefix, span, suffix)).2 == suffix,
{
}

pub broadcast proof fn lemma_cross_byte_span_mapper_wf_in_out(i: u16)
    by (bit_vector)
    ensures
        #[trigger] cross_byte_span_bounds(
            unpack_cross_byte_span(i).0,
            unpack_cross_byte_span(i).1,
            unpack_cross_byte_span(i).2,
        ),
{
}

#[verifier::allow_in_spec]
pub fn unpack_packet_header(raw: u16) -> (u8, u8, u8)
    returns
        (
            (((raw >> KIND_SHIFT) & KIND_MASK) as u8),
            (((raw >> COUNT_SHIFT) & COUNT_MASK) as u8),
            ((raw & LEN_MASK) as u8),
        ),
{
    (
        ((raw >> KIND_SHIFT) & KIND_MASK) as u8,
        ((raw >> COUNT_SHIFT) & COUNT_MASK) as u8,
        (raw & LEN_MASK) as u8,
    )
}

#[verifier::allow_in_spec]
pub fn pack_packet_header(kind_bits: u8, count: u8, len: u8) -> u16
    returns
        ((((kind_bits as u16) & KIND_MASK) << KIND_SHIFT) | (((count as u16) & COUNT_MASK)
            << COUNT_SHIFT) | ((len as u16) & LEN_MASK)),
{
    (((kind_bits as u16) & KIND_MASK) << KIND_SHIFT) | (((count as u16) & COUNT_MASK)
        << COUNT_SHIFT) | ((len as u16) & LEN_MASK)
}

#[verifier::allow_in_spec]
pub fn packet_header_bounds(kind_bits: u8, count: u8, _len: u8) -> bool
    returns
        kind_bits < KIND_MAX && count < COUNT_MAX,
{
    kind_bits < KIND_MAX && count < COUNT_MAX
}

pub broadcast proof fn lemma_packet_header_unpack_pack(raw: u16)
    by (bit_vector)
    ensures
        #[trigger] pack_packet_header(
            unpack_packet_header(raw).0,
            unpack_packet_header(raw).1,
            unpack_packet_header(raw).2,
        ) == raw,
{
}

pub broadcast proof fn lemma_packet_header_pack_unpack(kind_bits: u8, count: u8, len: u8)
    by (bit_vector)
    requires
        #[trigger] packet_header_bounds(kind_bits, count, len),
    ensures
        unpack_packet_header(pack_packet_header(kind_bits, count, len)).0 == kind_bits,
        unpack_packet_header(pack_packet_header(kind_bits, count, len)).1 == count,
        unpack_packet_header(pack_packet_header(kind_bits, count, len)).2 == len,
{
}

pub broadcast proof fn lemma_packet_header_mapper_wf_in_out(i: u16)
    by (bit_vector)
    ensures
        #[trigger] packet_header_bounds(
            unpack_packet_header(i).0,
            unpack_packet_header(i).1,
            unpack_packet_header(i).2,
        ),
{
}

#[verifier::allow_in_spec]
pub fn payload_kind_wf(kind: PayloadKind) -> bool
    returns
        kind matches PayloadKind::Unknown(x) ==> x != 0 && x != 1 && x != 2,
{
    matches!(kind, PayloadKind::Raw | PayloadKind::Words | PayloadKind::Tiny)
        || matches!(kind, PayloadKind::Unknown(x) if x != 0 && x != 1 && x != 2)
}

#[verifier::allow_in_spec]
pub fn payload_kind_from_bits(bits: u8) -> PayloadKind
    returns
        match bits {
            0 => PayloadKind::Raw,
            1 => PayloadKind::Words,
            2 => PayloadKind::Tiny,
            _ => PayloadKind::Unknown(bits),
        },
{
    match bits {
        0 => PayloadKind::Raw,
        1 => PayloadKind::Words,
        2 => PayloadKind::Tiny,
        _ => PayloadKind::Unknown(bits),
    }
}

#[verifier::allow_in_spec]
pub fn payload_kind_to_bits(kind: PayloadKind) -> u8
    returns
        match kind {
            PayloadKind::Raw => 0,
            PayloadKind::Words => 1,
            PayloadKind::Tiny => 2,
            PayloadKind::Unknown(x) => x,
        },
{
    match kind {
        PayloadKind::Raw => 0,
        PayloadKind::Words => 1,
        PayloadKind::Tiny => 2,
        PayloadKind::Unknown(x) => x,
    }
}

#[verifier::allow_in_spec]
pub fn closed_payload_kind_from_bits(bits: u8) -> ClosedPayloadKind
    returns
        match bits {
            0 => ClosedPayloadKind::Raw,
            1 => ClosedPayloadKind::Words,
            _ => ClosedPayloadKind::Tiny,
        },
{
    match bits {
        0 => ClosedPayloadKind::Raw,
        1 => ClosedPayloadKind::Words,
        _ => ClosedPayloadKind::Tiny,
    }
}

#[verifier::allow_in_spec]
pub fn closed_payload_kind_to_bits(kind: ClosedPayloadKind) -> u8
    returns
        match kind {
            ClosedPayloadKind::Raw => 0u8,
            ClosedPayloadKind::Words => 1u8,
            ClosedPayloadKind::Tiny => 2u8,
        },
{
    match kind {
        ClosedPayloadKind::Raw => 0,
        ClosedPayloadKind::Words => 1,
        ClosedPayloadKind::Tiny => 2,
    }
}

// ============================================================
// Format Specifications
// ============================================================
#[derive(Clone, Copy)]
pub struct VersionIhlFmt;

pub type VersionIhlFmtSpec = Named<Bits<U8, (u8, u8), VersionIhlSpec>>;

impl VersionIhlFmt {
    pub open spec fn spec_inner() -> VersionIhlFmtSpec {
        Named(
            "version_ihl",
            Bits {
                repr: U8,
                unpack: |packed: u8| unpack_version_ihl(packed),
                pack: |unpacked: (u8, u8)|
                    {
                        let (version, ihl) = unpacked;
                        pack_version_ihl(version, ihl)
                    },
                refinement: |unpacked: (u8, u8)| true,
                ctor: |parsed: (u8, u8)|
                    {
                        let (version, ihl) = parsed;
                        VersionIhl { version, ihl }
                    },
                dtor: |value: VersionIhlSpec|
                    {
                        let VersionIhl { version, ihl } = value;
                        (version, ihl)
                    },
                consistent: |value: VersionIhlSpec|
                    {
                        let VersionIhl { version, ihl } = value;
                        version_ihl_bounds(version, ihl)
                    },
            },
        )
    }
}

#[derive(Clone, Copy)]
pub struct CrossByteSpanFmt;

pub type CrossByteSpanFmtSpec = Named<Bits<U16Be, (u8, u16, u8), CrossByteSpanSpec>>;

impl CrossByteSpanFmt {
    pub open spec fn spec_inner() -> CrossByteSpanFmtSpec {
        Named(
            "cross_byte_span",
            Bits {
                repr: U16Be,
                unpack: |packed: u16| unpack_cross_byte_span(packed),
                pack: |unpacked: (u8, u16, u8)|
                    {
                        let (prefix, span, suffix) = unpacked;
                        pack_cross_byte_span(prefix, span, suffix)
                    },
                refinement: |unpacked: (u8, u16, u8)| true,
                ctor: |parsed: (u8, u16, u8)| -> CrossByteSpanSpec
                    {
                        let (prefix, span, suffix) = parsed;
                        CrossByteSpan { prefix, span, suffix }
                    },
                dtor: |value: CrossByteSpanSpec|
                    {
                        let CrossByteSpan { prefix, span, suffix } = value;
                        (prefix, span, suffix)
                    },
                consistent: |value: CrossByteSpanSpec|
                    {
                        let CrossByteSpan { prefix, span, suffix } = value;
                        cross_byte_span_bounds(prefix, span, suffix)
                    },
            },
        )
    }
}

#[derive(Clone, Copy)]
pub struct PacketHeaderFmt;

pub type PacketHeaderFmtSpec = Named<Bits<U16Be, (u8, u8, u8), PacketHeaderSpec>>;

impl PacketHeaderFmt {
    pub open spec fn spec_inner() -> PacketHeaderFmtSpec {
        Named(
            "packet_header",
            Bits {
                repr: U16Be,
                unpack: |packed: u16| unpack_packet_header(packed),
                pack: |unpacked: (u8, u8, u8)|
                    {
                        let (kind_bits, count, len) = unpacked;
                        pack_packet_header(kind_bits, count, len)
                    },
                refinement: |unpacked: (u8, u8, u8)|
                    {
                        let (kind_bits, count, len) = unpacked;
                        count >= 1u8
                    },
                ctor: |unpacked: (u8, u8, u8)|
                    {
                        let (kind_bits, count, len) = unpacked;
                        let kind = payload_kind_from_bits(kind_bits);
                        PacketHeaderSpec { kind, count, len }
                    },
                dtor: |value: PacketHeaderSpec|
                    {
                        let PacketHeaderSpec { kind, count, len } = value;
                        let kind_bits = payload_kind_to_bits(kind);
                        (kind_bits, count, len)
                    },
                consistent: |value: PacketHeaderSpec|
                    {
                        let PacketHeaderSpec { kind, count, len } = value;
                        &&& payload_kind_wf(kind)
                        &&& packet_header_bounds(payload_kind_to_bits(kind), count, len)
                    },
            },
        )
    }
}

pub type ChoicePayloadFmt = Mapped<
    Sum<Varied<u8>, Sum<RepeatN<U16Be, u8>, Sum<U8, Varied<u8>>>>,
    FnSpecMapper<ChoicePayloadInner, ChoicePayloadSpec>,
>;

pub open spec fn choice_packet_body_fmt(hdr: PacketHeaderSpec) -> ChoicePayloadFmt {
    Mapped {
        inner: match hdr.kind {
            PayloadKind::Raw => Sum::Inl(Varied(hdr.len)),
            PayloadKind::Words => Sum::Inr(Sum::Inl(RepeatN(hdr.count, U16Be))),
            PayloadKind::Tiny => Sum::Inr(Sum::Inr(Sum::Inl(U8))),
            PayloadKind::Unknown(_) => Sum::Inr(Sum::Inr(Sum::Inr(Varied(hdr.len)))),
        },
        mapper: (
            |parsed: ChoicePayloadInner| -> ChoicePayloadSpec
                {
                    match parsed {
                        Sum::Inl(bytes) => ChoicePayloadSpec::Raw(bytes),
                        Sum::Inr(Sum::Inl(words)) => ChoicePayloadSpec::Words(words),
                        Sum::Inr(Sum::Inr(Sum::Inl(x))) => ChoicePayloadSpec::Tiny(x),
                        Sum::Inr(Sum::Inr(Sum::Inr(bytes))) => ChoicePayloadSpec::Default(bytes),
                    }
                },
            |value: ChoicePayloadSpec| -> ChoicePayloadInner
                {
                    match value {
                        ChoicePayloadSpec::Raw(bytes) => Sum::Inl(bytes),
                        ChoicePayloadSpec::Words(words) => Sum::Inr(Sum::Inl(words)),
                        ChoicePayloadSpec::Tiny(x) => Sum::Inr(Sum::Inr(Sum::Inl(x))),
                        ChoicePayloadSpec::Default(bytes) => Sum::Inr(Sum::Inr(Sum::Inr(bytes))),
                    }
                },
        ),
    }
}

#[derive(Clone, Copy)]
pub struct ChoicePacketFmt;

pub type ChoicePacketFmtSpec = Named<
    Mapped<
        Bind<PacketHeaderFmt, spec_fn(PacketHeaderSpec) -> ChoicePayloadFmt>,
        FnSpecMapper<ChoicePacketInner, ChoicePacketSpec>,
    >,
>;

impl ChoicePacketFmt {
    pub open spec fn spec_inner() -> ChoicePacketFmtSpec {
        Named(
            "choice_packet",
            Mapped {
                inner: Bind(PacketHeaderFmt, |hdr: PacketHeaderSpec| choice_packet_body_fmt(hdr)),
                mapper: (
                    |parsed: ChoicePacketInner| -> ChoicePacketSpec
                        {
                            let (hdr, payload) = parsed;
                            ChoicePacketSpec { hdr, payload }
                        },
                    |value: ChoicePacketSpec| -> ChoicePacketInner
                        {
                            let ChoicePacketSpec { hdr, payload } = value;
                            (hdr, payload)
                        },
                ),
            },
        )
    }
}

#[derive(Clone, Copy)]
pub struct ClosedPacketHeaderFmt;

pub type ClosedPacketHeaderFmtSpec = Named<Bits<U16Be, (u8, u8, u8), ClosedPacketHeaderSpec>>;

impl ClosedPacketHeaderFmt {
    pub open spec fn spec_inner() -> ClosedPacketHeaderFmtSpec {
        Named(
            "closed_packet_header",
            Bits {
                repr: U16Be,
                unpack: |packed: u16| unpack_packet_header(packed),
                pack: |unpacked: (u8, u8, u8)|
                    {
                        let (kind_bits, count, len) = unpacked;
                        pack_packet_header(kind_bits, count, len)
                    },
                refinement: |unpacked: (u8, u8, u8)|
                    {
                        let (kind_bits, count, len) = unpacked;
                        &&& kind_bits < 3u8
                        &&& count >= 1u8
                    },
                ctor: |hdr: (u8, u8, u8)|
                    {
                        let (kind_bits, count, len) = hdr;
                        ClosedPacketHeaderSpec {
                            kind: closed_payload_kind_from_bits(kind_bits),
                            count,
                            len,
                        }
                    },
                dtor: |value: ClosedPacketHeaderSpec|
                    {
                        let ClosedPacketHeaderSpec { kind, count, len } = value;
                        (closed_payload_kind_to_bits(kind), count, len)
                    },
                consistent: |value: ClosedPacketHeaderSpec|
                    {
                        let ClosedPacketHeaderSpec { kind, count, len } = value;
                        packet_header_bounds(closed_payload_kind_to_bits(kind), count, len)
                    },
            },
        )
    }
}

pub type ClosedChoicePayloadFmt = Mapped<
    Sum<Varied<u8>, Sum<RepeatN<U16Be, u8>, U8>>,
    FnSpecMapper<ClosedChoicePayloadInner, ClosedChoicePayloadSpec>,
>;

pub open spec fn closed_choice_packet_body_fmt(
    hdr: ClosedPacketHeaderSpec,
) -> ClosedChoicePayloadFmt {
    Mapped {
        inner: match hdr.kind {
            ClosedPayloadKind::Raw => Sum::Inl(Varied(hdr.len)),
            ClosedPayloadKind::Words => Sum::Inr(Sum::Inl(RepeatN(hdr.count, U16Be))),
            ClosedPayloadKind::Tiny => Sum::Inr(Sum::Inr(U8)),
        },
        mapper: (
            |parsed: ClosedChoicePayloadInner| -> ClosedChoicePayloadSpec
                {
                    match parsed {
                        Sum::Inl(bytes) => ClosedChoicePayloadSpec::Raw(bytes),
                        Sum::Inr(Sum::Inl(words)) => ClosedChoicePayloadSpec::Words(words),
                        Sum::Inr(Sum::Inr(x)) => ClosedChoicePayloadSpec::Tiny(x),
                    }
                },
            |value: ClosedChoicePayloadSpec| -> ClosedChoicePayloadInner
                {
                    match value {
                        ClosedChoicePayloadSpec::Raw(bytes) => Sum::Inl(bytes),
                        ClosedChoicePayloadSpec::Words(words) => Sum::Inr(Sum::Inl(words)),
                        ClosedChoicePayloadSpec::Tiny(x) => Sum::Inr(Sum::Inr(x)),
                    }
                },
        ),
    }
}

#[derive(Clone, Copy)]
pub struct ClosedChoicePacketFmt;

pub type ClosedChoicePacketFmtSpec = Named<
    Mapped<
        Bind<ClosedPacketHeaderFmt, spec_fn(ClosedPacketHeaderSpec) -> ClosedChoicePayloadFmt>,
        FnSpecMapper<ClosedChoicePacketInner, ClosedChoicePacketSpec>,
    >,
>;

impl ClosedChoicePacketFmt {
    pub open spec fn spec_inner() -> ClosedChoicePacketFmtSpec {
        Named(
            "closed_choice_packet",
            Mapped {
                inner: Bind(
                    ClosedPacketHeaderFmt,
                    |hdr: ClosedPacketHeaderSpec| closed_choice_packet_body_fmt(hdr),
                ),
                mapper: (
                    |parsed: ClosedChoicePacketInner| -> ClosedChoicePacketSpec
                        {
                            let (hdr, payload) = parsed;
                            ClosedChoicePacketSpec { hdr, payload }
                        },
                    |value: ClosedChoicePacketSpec| -> ClosedChoicePacketInner
                        {
                            let ClosedChoicePacketSpec { hdr, payload } = value;
                            (hdr, payload)
                        },
                ),
            },
        )
    }
}

// ============================================================
// Derived Specs and Proofs
// ============================================================
mod derived_specs_proofs {
    use super::*;

    impl SpecParser for VersionIhlFmt {
        type PVal = VersionIhlSpec;

        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
            VersionIhlFmt::spec_inner().spec_parse(ibuf)
        }
    }

    impl Consistency for VersionIhlFmt {
        type Val = VersionIhlSpec;

        open spec fn consistent(&self, v: Self::Val) -> bool {
            VersionIhlFmt::spec_inner().consistent(v)
        }
    }

    impl SpecSerializerDps for VersionIhlFmt {
        type SValue = VersionIhlSpec;

        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
            VersionIhlFmt::spec_inner().spec_serialize_dps(v, obuf)
        }
    }

    impl SpecSerializer for VersionIhlFmt {
        type SVal = VersionIhlSpec;

        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
            VersionIhlFmt::spec_inner().spec_serialize(v)
        }
    }

    impl SpecByteLen for VersionIhlFmt {
        type T = VersionIhlSpec;

        open spec fn byte_len(&self, v: Self::T) -> nat {
            VersionIhlFmt::spec_inner().byte_len(v)
        }
    }

    impl SafeParser for VersionIhlFmt {
        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
            VersionIhlFmt::spec_inner().lemma_parse_safe(ibuf);
        }
    }

    impl SoundParser for VersionIhlFmt {
        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
            let fmt = VersionIhlFmt::spec_inner();
            broadcast use lemma_version_ihl_unpack_pack, lemma_version_ihl_mapper_wf_in_out;

            assert(fmt.1.sound_inv());
            VersionIhlFmt::spec_inner().lemma_parse_sound_consumption(ibuf);
        }

        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
            broadcast use lemma_version_ihl_unpack_pack, lemma_version_ihl_mapper_wf_in_out;

            VersionIhlFmt::spec_inner().lemma_parse_sound_value(ibuf);
        }
    }

    impl NonTailFmt for VersionIhlFmt {
        proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
            VersionIhlFmt::spec_inner().lemma_serialize_dps_prepend(v, obuf);
        }

        proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
            VersionIhlFmt::spec_inner().lemma_serialize_dps_len(v, obuf);
        }
    }

    impl GoodSerializer for VersionIhlFmt {
        proof fn lemma_serialize_len(&self, v: Self::SVal) {
            VersionIhlFmt::spec_inner().lemma_serialize_len(v);
        }
    }