vest_lib 0.2.2

//! ASN.1 ANY / open-type values.
//!
//! An ANY value is one complete, self-delimiting TLV. The semantic representation
//! retains the decoded tag and opaque contents bytes.
use crate::combinators::{
    bytes::ExactLen, mapped::spec::FnSpecMapper, Bind, Mapped, Pair, Refined, Tail,
};
use crate::core::exec::input::InputBuf;
use crate::core::exec::output::OutputBuf;
use crate::core::exec::{
    parser::{PResult, Parser},
    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
    ParseError,
};
use crate::core::{proof::*, spec::*};
#[cfg(feature = "alloc")]
use alloc::vec::Vec;
use vstd::prelude::*;

use super::{AnyFmt, LengthFmt, Tag, TagFmt};

verus! {

pub type AnyWireFmt<const DER: bool> = Pair<
    TagFmt,
    Bind<LengthFmt<DER>, spec_fn(usize) -> ExactLen<Tail, usize>>,
>;

pub type AnyInnerFmt<const DER: bool> = Refined<
    Mapped<AnyWireFmt<DER>, FnSpecMapper<(Tag, (usize, Seq<u8>)), AnySpec>>,
    PredFnSpec<AnySpec>,
>;

/// Semantic representation of an open type.
#[verifier::ext_equal]
pub struct AnySpec {
    pub tag: Tag,
    pub content: Seq<u8>,
}

pub open spec fn any_fmt<const DER: bool>() -> AnyInnerFmt<DER> {
    Refined(
        Mapped {
            inner: Pair(TagFmt, Bind(LengthFmt::<DER>, |len: usize| ExactLen(len, Tail))),
            mapper: (
                |(tag, (_, content)): (Tag, (usize, Seq<u8>))| AnySpec { tag, content },
                |v: AnySpec| (v.tag, (v.content.len() as usize, v.content)),
            ),
        },
        |v: AnySpec| v.tag != TagFmt::EOC,
    )
}

proof fn lemma_any_mapped_sound_nonmal_inv()
    ensures
        any_fmt::<true>().0.sound_inv(),
        any_fmt::<true>().0.nonmal_inv(),
{
    let mapped = any_fmt::<true>().0;
    assert forall|v: (Tag, (usize, Seq<u8>))| #[trigger] mapped.inner.consistent(v) implies (
    mapped.mapper.1)((mapped.mapper.0)(v)) == v by {
        let (_tag, (len, content)) = v;
        assert(len as nat == content.len());
        assert(content.len() <= usize::MAX);
    }
}

proof fn lemma_any_mapped_unambiguous<const DER: bool>()
    ensures
        any_fmt::<DER>().0.unambiguous(),
{
    let mapped = any_fmt::<DER>().0;
    assert forall|v: AnySpec| #[trigger] mapped.consistent(v) implies (mapped.mapper.0)(
        (mapped.mapper.1)(v),
    ) == v by {}
}

mod derived_specs {
    use super::*;

    impl<const DER: bool> SpecParser for AnyFmt<DER> {
        type PVal = AnySpec;

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

    impl<const DER: bool> Consistency for AnyFmt<DER> {
        type Val = AnySpec;

        open spec fn consistent(&self, v: Self::Val) -> bool {
            any_fmt::<DER>().consistent(v)
        }
    }

    impl<const DER: bool> SpecSerializerDps for AnyFmt<DER> {
        type SValue = AnySpec;

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

    impl<const DER: bool> SpecSerializer for AnyFmt<DER> {
        type SVal = AnySpec;

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

    impl<const DER: bool> SpecByteLen for AnyFmt<DER> {
        type T = AnySpec;

        open spec fn byte_len(&self, v: Self::T) -> nat {
            any_fmt::<DER>().byte_len(v)
        }
    }

}

mod derived_proofs {
    use super::*;

    impl<const DER: bool> SafeParser for AnyFmt<DER> {
        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
            any_fmt::<DER>().lemma_parse_safe(ibuf);
        }
    }

    impl<const DER: bool> Productive for AnyFmt<DER> {
        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
            any_fmt::<DER>().lemma_productive(ibuf);
        }
    }

    impl SoundParser for AnyFmt<true> {
        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
            lemma_any_mapped_sound_nonmal_inv();
            any_fmt::<true>().lemma_parse_sound_consumption(ibuf);
        }

        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
            lemma_any_mapped_sound_nonmal_inv();
            any_fmt::<true>().lemma_parse_sound_value(ibuf);
        }
    }

    impl<const DER: bool> NonTailFmt for AnyFmt<DER> {
        proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
            any_fmt::<DER>().lemma_serialize_dps_prepend(v, obuf);
        }

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

    impl<const DER: bool> GoodSerializer for AnyFmt<DER> {
        proof fn lemma_serialize_len(&self, v: Self::SVal) {
            any_fmt::<DER>().lemma_serialize_len(v);
        }
    }

    impl<const DER: bool> SPRoundTripDps for AnyFmt<DER> {
        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
            lemma_any_mapped_unambiguous::<DER>();
            any_fmt::<DER>().theorem_serialize_dps_parse_roundtrip(v, obuf);
        }
    }

    impl NonMalleable for AnyFmt<true> {
        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
            lemma_any_mapped_sound_nonmal_inv();
            any_fmt::<true>().lemma_parse_non_malleable(buf1, buf2);
        }
    }

    impl<const DER: bool> EquivSerializersGeneral for AnyFmt<DER> {
        proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
            any_fmt::<DER>().lemma_serialize_equiv(v, obuf);
        }
    }

    impl<const DER: bool> EquivSerializers for AnyFmt<DER> {
        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
            any_fmt::<DER>().lemma_serialize_equiv_on_empty(v);
        }
    }

}

/// Borrowed executable open-type value.
pub struct Any<'a> {
    tag: Tag,
    content: &'a [u8],
}

impl<'a> DeepView for Any<'a> {
    type V = AnySpec;

    closed spec fn deep_view(&self) -> Self::V {
        AnySpec { tag: self.tag, content: self.content.deep_view() }
    }
}

impl<'a> Any<'a> {
    pub fn new(tag: Tag, content: &'a [u8]) -> (value: Self)
        ensures
            value.deep_view() == (AnySpec { tag, content: content.deep_view() }),
    {
        Self { tag, content }
    }

    pub fn tag(&self) -> (tag: Tag)
        ensures
            tag == self.deep_view().tag,
    {
        self.tag
    }

    pub fn content(&self) -> (content: &'a [u8])
        ensures
            content.deep_view() == self.deep_view().content,
    {
        self.content
    }
}

/// Owned executable open-type value.
///
/// This is the representation used by the recursive BER ANY parser: an indefinite-length
/// constructed value has no single borrowed content slice once its terminating EOC is removed.
#[cfg(feature = "alloc")]
pub struct AnyOwned {
    tag: Tag,
    content: Vec<u8>,
}

#[cfg(feature = "alloc")]
impl DeepView for AnyOwned {
    type V = AnySpec;

    closed spec fn deep_view(&self) -> Self::V {
        AnySpec { tag: self.tag, content: self.content.deep_view() }
    }
}

#[cfg(feature = "alloc")]
impl AnyOwned {
    pub fn new(tag: Tag, content: Vec<u8>) -> (value: Self)
        ensures
            value.deep_view() == (AnySpec { tag, content: content.deep_view() }),
    {
        Self { tag, content }
    }

    pub fn tag(&self) -> (tag: Tag)
        ensures
            tag == self.deep_view().tag,
    {
        self.tag
    }

    pub fn content(&self) -> (content: &[u8])
        ensures
            content.deep_view() == self.deep_view().content,
    {
        self.content.as_slice()
    }

    pub fn into_content(self) -> (content: Vec<u8>)
        ensures
            content.deep_view() == self.deep_view().content,
    {
        self.content
    }
}

impl<'a, const DER: bool> Parser<&'a [u8]> for AnyFmt<DER> {
    type PT = Any<'a>;

    fn parse(&self, ibuf: &&'a [u8]) -> PResult<Self::PT> {
        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
        broadcast use crate::core::spec::SoundParser::lemma_parse_sound_value;

        let _ = ibuf.len();
        let (n1, tag) = TagFmt.parse(ibuf)?;
        if tag == TagFmt::EOC {
            return Err(ParseError::invalid_tag());
        }
        let rest = ibuf.skip(n1);
        let (n2, len) = LengthFmt::<DER>.parse(&rest)?;
        let rest = rest.skip(n2);
        let (n3, content) = ExactLen(len, Tail).parse(&rest)?;
        Ok((n1 + n2 + n3, Any { tag, content }))
    }
}

impl<'a, Output: OutputBuf, const DER: bool> Serializer<Output, Any<'a>> for AnyFmt<DER> {
    fn serialize_into(&self, v: &Any<'a>, obuf: &mut Output) {
        broadcast use crate::core::exec::output::outbuf_lemmas;

        let len = v.content.len();
        TagFmt.serialize_into(&v.tag, obuf);
        LengthFmt::<DER>.serialize_into(&len, obuf);
        Tail.serialize_into(&v.content, obuf);
    }
}

impl<'a, const DER: bool> Prepare<Any<'a>> for AnyFmt<DER> {
    fn prepare(&self, v: &Any<'a>) -> Result<usize, PreSerializeError> {
        if v.tag == TagFmt::EOC {
            return Err(PreSerializeError::custom("EOC is not an open-type value"));
        }
        let n1 = TagFmt.prepare(&v.tag)?;
        let content_len = Tail.prepare(&v.content)?;
        let n2 = LengthFmt::<DER>.prepare(&content_len)?;
        let header = n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())?;
        let total = header.checked_add(content_len).ok_or(PreSerializeError::length_too_large())?;
        Ok(total)
    }
}

impl<'a, const DER: bool> ByteLen<Any<'a>> for AnyFmt<DER> {
    fn length(&self, v: &Any<'a>) -> usize {
        let n1 = TagFmt.length(&v.tag);
        let content_len = Tail.length(&v.content);
        let n2 = LengthFmt::<DER>.length(&content_len);
        n1 + n2 + content_len
    }
}

#[cfg(feature = "alloc")]
impl<Output: OutputBuf, const DER: bool> Serializer<Output, AnyOwned> for AnyFmt<DER> {
    fn serialize_into(&self, v: &AnyOwned, obuf: &mut Output) {
        broadcast use crate::core::exec::output::outbuf_lemmas;

        let len = v.content.len();
        TagFmt.serialize_into(&v.tag, obuf);
        LengthFmt::<DER>.serialize_into(&len, obuf);
        Tail.serialize_into(v.content.as_slice(), obuf);
    }
}

#[cfg(feature = "alloc")]
impl<const DER: bool> Prepare<AnyOwned> for AnyFmt<DER> {
    fn prepare(&self, v: &AnyOwned) -> Result<usize, PreSerializeError> {
        if v.tag == TagFmt::EOC {
            return Err(PreSerializeError::custom("EOC is not an open-type value"));
        }
        let n1 = TagFmt.prepare(&v.tag)?;
        let content_len = Tail.prepare(v.content.as_slice())?;
        let n2 = LengthFmt::<DER>.prepare(&content_len)?;
        let header = n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())?;
        let total = header.checked_add(content_len).ok_or(PreSerializeError::length_too_large())?;
        Ok(total)
    }
}

#[cfg(feature = "alloc")]
impl<const DER: bool> ByteLen<AnyOwned> for AnyFmt<DER> {
    fn length(&self, v: &AnyOwned) -> usize {
        let n1 = TagFmt.length(&v.tag);
        let content_len = Tail.length(v.content.as_slice());
        let n2 = LengthFmt::<DER>.length(&content_len);
        n1 + n2 + content_len
    }
}

} // verus!
#[cfg(test)]
mod tests {
    use crate::asn1::TagFmt;
    use crate::core::exec::{Parser, Prepare, SerializerExt};

    #[test]
    fn any_roundtrips_one_complete_tlv() {
        let input = [0x30, 0x03, 0x02, 0x01, 0x05, 0xff];
        let (n, value) = super::super::der::ANY.parse(&&input[..]).unwrap();
        assert_eq!(n, 5);
        assert_eq!(value.tag(), TagFmt::SEQUENCE);
        assert_eq!(value.content(), &[0x02, 0x01, 0x05]);

        let mut output = vec![0; super::super::der::ANY.prepare(&value).unwrap()];
        super::super::der::ANY.serialize(&value, &mut output);
        assert_eq!(output, &input[..5]);
    }

    #[test]
    fn any_rejects_eoc_as_a_value() {
        assert!(super::super::der::ANY.parse(&&[0x00, 0x00][..]).is_err());
    }
}