vest_lib 0.2.2

//! Specifications for fixed- and variable-length bytes.
use crate::combinators::length::AsLen;
use crate::core::{proof::*, spec::*};
use vstd::prelude::*;

use super::Varied;
use crate::combinators::Tail;

verus! {

pub uninterp spec fn array_from_seq<const N: usize, T>(s: Seq<T>) -> [T; N]
    recommends
        s.len() == N,
;

pub broadcast axiom fn axiom_array_from_seq<const N: usize, T>(s: Seq<T>)
    requires
        s.len() == N,
    ensures
        (#[trigger] array_from_seq::<N, T>(s))@ == s,
;

pub broadcast proof fn lemma_array_from_seq_roundtrip<const N: usize, T>(a: [T; N])
    ensures
        #[trigger] array_from_seq::<N, T>(a@) == a,
{
    broadcast use axiom_array_from_seq;

}

impl<const N: usize> SpecParser for super::Fixed<N> {
    type PVal = Seq<u8>;

    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
        if ibuf.len() < N as int {
            None
        } else {
            Some((N as int, ibuf[0..N]))
        }
    }
}

impl<const N: usize> Consistency for super::Fixed<N> {
    type Val = Seq<u8>;

    open spec fn consistent(&self, v: Self::Val) -> bool {
        v.len() == N
    }
}

impl<const N: usize> SafeParser for super::Fixed<N> {
    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
    }
}

impl<const N: usize> SoundParser for super::Fixed<N> {
    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
    }

    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
    }
}

impl<const N: usize> SpecSerializerDps for super::Fixed<N> {
    type SValue = Seq<u8>;

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

impl<const N: usize> SpecSerializer for super::Fixed<N> {
    type SVal = Seq<u8>;

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

impl<const N: usize> NonTailFmt for super::Fixed<N> {
    proof fn lemma_serialize_dps_prepend(&self, v: Seq<u8>, obuf: Seq<u8>) {
        assert(self.spec_serialize_dps(v, obuf) == v + obuf);
    }

    proof fn lemma_serialize_dps_len(&self, v: Seq<u8>, obuf: Seq<u8>) {
        assert(self.spec_serialize_dps(v, obuf).len() - obuf.len() == v.len());
    }
}

impl<const N: usize> GoodSerializer for super::Fixed<N> {
    proof fn lemma_serialize_len(&self, v: Self::SVal) {
        assert(self.spec_serialize(v).len() == v.len());
    }
}

impl<const N: usize> SpecByteLen for super::Fixed<N> {
    type T = Seq<u8>;

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

impl<const N: usize> MinMaxByteLen for super::Fixed<N> {
    open spec fn min(&self) -> nat {
        N as nat
    }

    open spec fn max(&self) -> nat {
        N as nat
    }

    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
    }
}

impl<const N: usize> StaticByteLen for super::Fixed<N> {
    open spec fn static_byte_len() -> nat {
        N as nat
    }

    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
    }
}

impl<const N: usize> ValueByteLen for super::Fixed<N> {
    open spec fn value_byte_len(_v: Self::T) -> nat {
        N as nat
    }

    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
    }
}

impl<const N: usize> BytesCombinator for super::Fixed<N> {
    proof fn lemma_byte_len_is_buf_len(&self, buf: Seq<u8>) {
    }
}

impl<Len: AsLen> SpecParser for super::Varied<Len> {
    type PVal = Seq<u8>;

    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
        if ibuf.len() < self.0.as_nat() {
            None
        } else {
            Some((self.0.as_nat() as int, ibuf[0..self.0.as_nat()]))
        }
    }
}

impl<Len: AsLen> Consistency for super::Varied<Len> {
    type Val = Seq<u8>;

    open spec fn consistent(&self, v: Self::Val) -> bool {
        v.len() == self.0.as_nat()
    }
}

impl<Len: AsLen> SafeParser for super::Varied<Len> {
    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
    }
}

impl<Len: AsLen> SoundParser for super::Varied<Len> {
    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
    }

    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
    }
}

impl<Len: AsLen> SpecSerializerDps for super::Varied<Len> {
    type SValue = Seq<u8>;

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

impl<Len: AsLen> SpecSerializer for super::Varied<Len> {
    type SVal = Seq<u8>;

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

impl<Len: AsLen> NonTailFmt for super::Varied<Len> {
    proof fn lemma_serialize_dps_prepend(&self, v: Seq<u8>, obuf: Seq<u8>) {
        assert(self.spec_serialize_dps(v, obuf) == v + obuf);
    }

    proof fn lemma_serialize_dps_len(&self, v: Seq<u8>, obuf: Seq<u8>) {
        assert(self.spec_serialize_dps(v, obuf).len() - obuf.len() == v.len());
    }
}

impl<Len: AsLen> GoodSerializer for super::Varied<Len> {
    proof fn lemma_serialize_len(&self, v: Self::SVal) {
        assert(self.spec_serialize(v).len() == v.len());
    }
}

impl<Len: AsLen> SpecByteLen for super::Varied<Len> {
    type T = Seq<u8>;

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

impl<Len: AsLen> MinMaxByteLen for super::Varied<Len> {
    open spec fn min(&self) -> nat {
        self.0.as_nat()
    }

    open spec fn max(&self) -> nat {
        self.0.as_nat()
    }

    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
    }
}

impl<Len: AsLen> super::Varied<Len> {
    pub open spec fn byte_len(v: <Self as SpecByteLen>::T) -> nat {
        v.len()
    }
}

impl<Len: AsLen> BytesCombinator for super::Varied<Len> {
    proof fn lemma_byte_len_is_buf_len(&self, s: Seq<u8>) {
    }
}

impl<Len: AsLen> ValueByteLen for super::Varied<Len> {
    open spec fn value_byte_len(v: Self::T) -> nat {
        v.len()
    }

    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
    }
}

impl<Inner: SpecParser, Len: AsLen> SpecParser for super::ExactLen<Inner, Len> {
    type PVal = Inner::PVal;

    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
        super::AndThen(super::Varied(self.0), self.1).spec_parse(ibuf)
    }
}

impl<Inner: Consistency + SpecByteLen<T = Inner::Val>, Len: AsLen> Consistency for super::ExactLen<
    Inner,
    Len,
> {
    type Val = Inner::Val;

    open spec fn consistent(&self, v: Self::Val) -> bool {
        &&& self.1.consistent(v)
        &&& self.0.as_nat() == self.1.byte_len(v)
    }
}

impl<Inner: SafeParser, Len: AsLen> SafeParser for super::ExactLen<Inner, Len> {
    open spec fn safe_inv(&self) -> bool {
        super::AndThen(super::Varied(self.0), self.1).safe_inv()
    }

    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
        super::AndThen(super::Varied(self.0), self.1).lemma_parse_safe(ibuf);
    }
}

impl<Inner: SoundParser, Len: AsLen> SoundParser for super::ExactLen<Inner, Len> {
    open spec fn sound_inv(&self) -> bool {
        super::AndThen(super::Varied(self.0), self.1).sound_inv()
    }

    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
        super::AndThen(super::Varied(self.0), self.1).lemma_parse_sound_consumption(ibuf);
    }

    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
        super::AndThen(super::Varied(self.0), self.1).lemma_parse_sound_value(ibuf);
    }
}

impl<Inner: SpecSerializerDps, Len: AsLen> SpecSerializerDps for super::ExactLen<Inner, Len> {
    type SValue = Inner::SValue;

    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
        super::AndThen(super::Varied(self.0), self.1).spec_serialize_dps(v, obuf)
    }
}

impl<Inner: SpecSerializer, Len: AsLen> SpecSerializer for super::ExactLen<Inner, Len> {
    type SVal = Inner::SVal;

    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
        super::AndThen(super::Varied(self.0), self.1).spec_serialize(v)
    }
}

impl<Inner, Len> NonTailFmt for super::ExactLen<Inner, Len> where
    Inner: GoodSerializer + EquivSerializers,
    Len: AsLen,
 {
    open spec fn serialize_dps_inv(&self) -> bool {
        super::AndThen(super::Varied(self.0), self.1).serialize_dps_inv()
    }

    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_dps_prepend(v, obuf);
    }

    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_dps_len(v, obuf);
    }
}

impl<Inner: GoodSerializer, Len: AsLen> GoodSerializer for super::ExactLen<Inner, Len> {
    open spec fn serialize_inv(&self) -> bool {
        super::AndThen(super::Varied(self.0), self.1).serialize_inv()
    }

    proof fn lemma_serialize_len(&self, v: Self::SVal) {
        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_len(v);
    }
}

impl<Inner: SpecByteLen, Len: AsLen> SpecByteLen for super::ExactLen<Inner, Len> {
    type T = Inner::T;

    open spec fn byte_len(&self, v: Self::T) -> nat {
        super::AndThen(super::Varied(self.0), self.1).byte_len(v)
    }
}

impl<Inner, Len> MinMaxByteLen for super::ExactLen<Inner, Len> where
    Inner: SpecByteLen + Consistency<Val = Inner::T>,
    Len: AsLen,
 {
    open spec fn min(&self) -> nat {
        self.0.as_nat()
    }

    open spec fn max(&self) -> nat {
        self.0.as_nat()
    }

    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
        assert(self.0.as_nat() == self.1.byte_len(v));
    }
}

impl<Inner: SpecByteLen, Len: AsLen> super::ExactLen<Inner, Len> {
    pub open spec fn byte_len(inner: Inner, v: <Self as SpecByteLen>::T) -> nat {
        inner.byte_len(v)
    }
}

impl<Inner: ValueByteLen, Len: AsLen> ValueByteLen for super::ExactLen<Inner, Len> {
    open spec fn value_byte_len(v: Self::T) -> nat {
        Inner::value_byte_len(v)
    }

    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
        self.1.lemma_value_len_matches_byte_len(v);
    }
}

impl<Inner: StaticByteLen, Len: AsLen> StaticByteLen for super::ExactLen<Inner, Len> {
    open spec fn static_byte_len() -> nat {
        Inner::static_byte_len()
    }

    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
        self.1.lemma_static_len_matches_byte_len(v);
    }
}

impl<A, Then> SpecParser for super::AndThen<A, Then> where
    A: SpecParser<PVal = Seq<u8>>,
    Then: SpecParser,
 {
    type PVal = Then::PVal;

    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
        match self.0.spec_parse(ibuf) {
            None => None,
            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
                Some((len_b, v)) if len_a == len_b => Some((len_a, v)),
                _ => None,
            },
        }
    }
}

impl<A, Then> Consistency for super::AndThen<A, Then> where
    A: BytesCombinator + Consistency<Val = Seq<u8>>,
    Then: Consistency + SpecByteLen<T = Then::Val>,
 {
    type Val = Then::Val;

    open spec fn consistent(&self, v: Self::Val) -> bool {
        &&& self.1.consistent(v)
        &&& exists|chunk: Seq<u8>|
            self.0.consistent(chunk) && self.0.byte_len(chunk) == self.1.byte_len(v)
    }
}

pub broadcast proof fn lemma_tail_and_then_consistent<Then>(then: Then, v: Then::Val) where
    Then: Consistency + SpecByteLen<T = Then::Val>,

    ensures
        #[trigger] super::AndThen(Tail, then).consistent(v) == then.consistent(v),
{
    if then.consistent(v) {
        let chunk = Seq::new(then.byte_len(v), |_i| 0u8);
        assert(Tail.consistent(chunk));
        assert(Tail.byte_len(chunk) == then.byte_len(v));
        assert(super::AndThen(Tail, then).0.consistent(chunk));
    } else {
    }
}

pub broadcast group tail_and_then_lemmas {
    lemma_tail_and_then_consistent,
}

impl<A, Then> SafeParser for super::AndThen<A, Then> where
    A: BytesCombinator + SafeParser<PVal = Seq<u8>>,
    Then: SafeParser,
 {
    open spec fn safe_inv(&self) -> bool {
        self.0.safe_inv()
    }

    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
        self.0.lemma_parse_safe(ibuf);
    }
}

impl<A, Then> SoundParser for super::AndThen<A, Then> where
    A: BytesCombinator + SoundParser,
    Then: SoundParser,
 {
    open spec fn sound_inv(&self) -> bool {
        self.0.sound_inv() && self.1.sound_inv()
    }

    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
        match self.0.spec_parse(ibuf) {
            None => {},
            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
                Some((len_b, v)) if len_a == len_b => {
                    self.1.lemma_parse_sound_consumption(chunk);
                    assert(self.byte_len(v) == self.1.byte_len(v));
                },
                _ => {},
            },
        }
    }

    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
        match self.0.spec_parse(ibuf) {
            None => {},
            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
                Some((len_b, v)) if len_a == len_b => {
                    self.0.lemma_parse_sound_value(ibuf);
                    self.0.lemma_parse_sound_consumption(ibuf);
                    self.1.lemma_parse_sound_consumption(chunk);
                    self.1.lemma_parse_sound_value(chunk);
                    assert(self.0.consistent(chunk));
                },
                _ => {},
            },
        }
    }
}

impl<A, Then> SpecSerializerDps for super::AndThen<A, Then> where
    A: SpecSerializerDps<SValue = Seq<u8>>,
    Then: SpecSerializerDps,
 {
    type SValue = Then::SValue;

    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
        self.0.spec_serialize_dps(self.1.spec_serialize_dps(v, seq![]), obuf)
    }
}

impl<A, Then> SpecSerializer for super::AndThen<A, Then> where
    A: SpecSerializer<SVal = Seq<u8>>,
    Then: SpecSerializer,
 {
    type SVal = Then::SVal;

    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
        let inner_bytes = self.1.spec_serialize(v);
        self.0.spec_serialize(inner_bytes)
    }
}

impl<A, Then> NonTailFmt for super::AndThen<A, Then> where
    A: BytesCombinator + NonTailFmt,
    Then: GoodSerializer + EquivSerializers,
 {
    open spec fn serialize_dps_inv(&self) -> bool {
        &&& self.0.serialize_dps_inv()
        &&& self.1.serialize_inv()
        &&& self.1.equiv_inv()
    }

    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
        self.0.lemma_serialize_dps_prepend(self.1.spec_serialize_dps(v, seq![]), obuf);
    }

    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
        self.1.lemma_serialize_equiv_on_empty(v);
        self.1.lemma_serialize_len(v);
        let inner_bytes = self.1.spec_serialize_dps(v, seq![]);
        self.0.lemma_serialize_dps_len(inner_bytes, obuf);
        self.0.lemma_byte_len_is_buf_len(inner_bytes);
    }
}

impl<A, Then> GoodSerializer for super::AndThen<A, Then> where
    A: BytesCombinator + GoodSerializer,
    Then: GoodSerializer,
 {
    open spec fn serialize_inv(&self) -> bool {
        &&& self.0.serialize_inv()
        &&& self.1.serialize_inv()
    }

    proof fn lemma_serialize_len(&self, v: Self::SVal) {
        let inner_bytes = self.1.spec_serialize(v);
        self.1.lemma_serialize_len(v);
        self.0.lemma_serialize_len(inner_bytes);
        self.0.lemma_byte_len_is_buf_len(inner_bytes);
    }
}

impl<A, Then: SpecByteLen> SpecByteLen for super::AndThen<A, Then> {
    type T = Then::T;

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

impl<A, Then> MinMaxByteLen for super::AndThen<A, Then> where
    A: BytesCombinator + Consistency<Val = Seq<u8>>,
    Then: MinMaxByteLen,
 {
    open spec fn min(&self) -> nat {
        self.1.min()
    }

    open spec fn max(&self) -> nat {
        self.1.max()
    }

    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
        self.1.lemma_min_max_byte_len(v);
    }
}

impl<A, Then> ValueByteLen for super::AndThen<A, Then> where
    A: BytesCombinator + Consistency<Val = Seq<u8>>,
    Then: ValueByteLen,
 {
    open spec fn value_byte_len(v: Self::T) -> nat {
        Then::value_byte_len(v)
    }

    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
        self.1.lemma_value_len_matches_byte_len(v);
    }
}

impl<A, Then> StaticByteLen for super::AndThen<A, Then> where
    A: BytesCombinator + StaticByteLen,
    Then: Consistency + SpecByteLen<T = Then::Val>,
 {
    open spec fn static_byte_len() -> nat {
        A::static_byte_len()
    }

    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
        let chunk = choose|chunk: Seq<u8>|
            self.0.consistent(chunk) && self.0.byte_len(chunk) == self.1.byte_len(v);
        self.0.lemma_static_len_matches_byte_len(chunk);
    }
}

// pub open spec fn fill_array_rec<const N: usize>(base: [u8; N], s: Seq<u8>, i: nat) -> [u8; N]
//     recommends
//         s.len() == N,
//         i <= N,
//     decreases i,
// {
//     if i == 0 {
//         base
//     } else {
//         let idx = (i - 1) as int;
//         // base[idx] = s[idx];
//         fill_array_rec(spec_array_update(base, idx, s[idx]), s, idx as nat)
//     }
// }
// pub open spec fn array_from_seq<const N: usize>(s: Seq<u8>) -> [u8; N]
//     recommends s.len() == N
// {
//     let base = vstd::array::spec_array_fill_for_copy_type::<u8, N>(0);
//     fill_array_rec(base, s, N as nat)
// }
// proof fn lemma_fill_array_rec<const N: usize>(base: [u8; N], s: Seq<u8>, i: nat)
//     requires
//         s.len() == N,
//         i <= N,
//     ensures
//         ({
//             let res = fill_array_rec(base, s, i);
//             forall|k: int| #![auto] 0 <= k < i ==> res[k] == s[k]
//         }),
//         ({
//             let res = fill_array_rec(base, s, i);
//             forall|k: int| #![auto] i <= k < N ==> res[k] == base[k]
//         }),
//     decreases i,
// {
//     if i == 0 {
//     } else {
//         let idx = (i - 1) as int;
//         let new_base = spec_array_update(base, idx, s[idx]);
//         lemma_fill_array_rec(new_base, s, idx as nat);
//         let res = fill_array_rec(base, s, i);
//         // Help Verus with array length
//         // assert(res.len() == N);
//         // assert(0 <= idx < N);
//         assert(res[idx] == new_base[idx]);
//         assert(new_base[idx] == s[idx]);
//         assert(res[idx] == s[idx]);
//     }
// }
// proof fn lemma_array_from_seq<const N: usize>(s: Seq<u8>)
//     requires s.len() == N,
//     ensures
//         array_from_seq::<N>(s)@ == s,
// {
//     let base = spec_array_fill_for_copy_type::<u8, N>(0);
//     lemma_fill_array_rec(base, s, N as nat);
//     assert(array_from_seq::<N>(s)@ =~= s);
// }
} // verus!