vest_lib 0.2.2

//! Executable implementations for end-of-input and remaining-input formats.
use crate::combinators::{Eof, Opt, Optional, Pair, Repeat, Star};
use crate::core::exec::output::*;
use crate::core::exec::{
    input::InputBuf,
    parser::{PResult, Parser},
    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
    ParseError,
};
use crate::core::proof::Productive;
use crate::core::spec::SafeParser;
use crate::core::spec::{Consistency, SpecByteLen};
#[cfg(feature = "alloc")]
use alloc::vec::Vec;
use vstd::prelude::*;
use OutputBuf;

verus! {

impl<I: InputBuf> Parser<I> for super::Tail {
    type PT = I;

    fn min_byte_len(&self) -> usize {
        // The remaining input may be empty.
        0
    }

    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
        let len = ibuf.len();
        let tail = ibuf.take(len);
        proof {
            assert(tail.deep_view() == ibuf@);
        }
        Ok((len, tail))
    }
}

impl<Output: OutputBuf> Serializer<Output, [u8]> for super::Tail {
    fn serialize_into(&self, v: &[u8], obuf: &mut Output) {
        obuf.write_bytes(v);
    }
}

impl<'i, Output: OutputBuf> Serializer<Output, &'i [u8]> for super::Tail {
    fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output) {
        obuf.write_bytes(*v);
    }
}

impl ByteLen<[u8]> for super::Tail {
    open spec fn exec_inv(&self) -> bool {
        true
    }

    fn length(&self, v: &[u8]) -> (len: usize) {
        v.len()
    }
}

impl<'i> ByteLen<&'i [u8]> for super::Tail {
    open spec fn exec_inv(&self) -> bool {
        true
    }

    fn length(&self, v: &&'i [u8]) -> (len: usize) {
        v.len()
    }
}

impl Prepare<[u8]> for super::Tail {
    fn prepare(&self, v: &[u8]) -> (checked: Result<usize, PreSerializeError>) {
        Ok(v.len())
    }
}

impl<'i> Prepare<&'i [u8]> for super::Tail {
    fn prepare(&self, v: &&'i [u8]) -> (checked: Result<usize, PreSerializeError>) {
        Ok(v.len())
    }
}

impl<I: InputBuf> Parser<I> for super::Eof {
    type PT = ();

    fn min_byte_len(&self) -> usize {
        0
    }

    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
        let len = ibuf.len();
        if len == 0 {
            Ok((0, ()))
        } else {
            Err(ParseError::expecting_eof())
        }
    }
}

impl<Output: OutputBuf> Serializer<Output, ()> for super::Eof {
    fn serialize_into(&self, _v: &(), _obuf: &mut Output) {
        broadcast use crate::core::exec::output::outbuf_lemmas;

    }
}

impl ByteLen<()> for super::Eof {
    fn length(&self, _v: &()) -> (len: usize) {
        0
    }
}

impl Prepare<()> for super::Eof {
    fn prepare(&self, _v: &()) -> (checked: Result<usize, PreSerializeError>) {
        Ok(0)
    }
}

impl<A, B, AVal, BVal> ByteLen<(AVal, BVal)> for super::PairRev<A, B> where
    AVal: DeepView,
    BVal: DeepView,
    A: ByteLen<AVal>,
    B: ByteLen<BVal>,
 {
    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& self.1.exec_inv()
    }

    fn length(&self, v: &(AVal, BVal)) -> (len: usize) {
        let la = self.1.length(&v.0);
        let lb = self.0.length(&v.1);
        proof {
            assert((la + lb) as nat == la as nat + lb as nat);
        }
        la + lb
    }
}

impl<A, B, AVal, BVal> Prepare<(AVal, BVal)> for super::PairRev<A, B> where
    AVal: DeepView,
    BVal: DeepView,
    A: Prepare<AVal>,
    B: Prepare<BVal>,
 {
    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& self.1.exec_inv()
    }

    fn prepare(&self, v: &(AVal, BVal)) -> Result<usize, PreSerializeError> {
        let la = self.1.prepare(&v.0)?;
        let lb = self.0.prepare(&v.1)?;
        if let Some(total) = la.checked_add(lb) {
            Ok(total)
        } else {
            Err(PreSerializeError::length_too_large())
        }
    }
}

#[cfg(feature = "alloc")]
impl<I, A> Parser<I> for super::RepeatTillEnd<A> where
    I: InputBuf,
    A: Parser<I> + SafeParser + Productive + Copy,
 {
    type PT = Vec<A::PT>;

    fn min_byte_len(&self) -> usize {
        // A repetition may be empty.
        0
    }

    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& self.0.safe_inv()
        &&& self.0.productive_inv()
    }

    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
        let (n, (r, _)) = Repeat(self.0, super::Eof).parse(ibuf)?;
        Ok((n, r))
    }
}

impl<I, A> Parser<I> for super::OptionalEnd<A> where I: InputBuf, A: Parser<I> + SafeParser {
    type PT = Option<A::PT>;

    fn min_byte_len(&self) -> usize {
        // The inner format may be absent.
        0
    }

    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& self.0.safe_inv()
    }

    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
        let (n, (r, _)) = Optional(&self.0, super::Eof).parse(ibuf)?;
        Ok((n, r))
    }
}

impl<Output: OutputBuf, A, T> Serializer<Output, &[T]> for super::RepeatTillEnd<A> where
    A: Serializer<Output, T> + Copy,
    T: DeepView,
 {
    #[verifier::prophetic]
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn serialize_into(&self, v: &&[T], obuf: &mut Output) {
        Star(self.0).serialize_into(v, obuf);
    }
}

impl<A, T> ByteLen<&[T]> for super::RepeatTillEnd<A> where A: ByteLen<T> + Copy, T: DeepView {
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn length(&self, v: &&[T]) -> (len: usize) {
        Star(self.0).length(v)
    }
}

impl<A, T> Prepare<&[T]> for super::RepeatTillEnd<A> where A: Prepare<T> + Copy, T: DeepView {
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn prepare(&self, v: &&[T]) -> Result<usize, PreSerializeError> {
        Star(self.0).prepare(v)
    }
}

#[cfg(feature = "alloc")]
impl<Output: OutputBuf, A, T> Serializer<Output, Vec<T>> for super::RepeatTillEnd<A> where
    A: Serializer<Output, T> + Copy,
    T: DeepView,
 {
    #[verifier::prophetic]
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn serialize_into(&self, v: &Vec<T>, obuf: &mut Output) {
        let values = v.as_slice();
        proof {
            assert(values.deep_view() == v.deep_view());
        }
        Star(self.0).serialize_into(&values, obuf);
    }
}

#[cfg(feature = "alloc")]
impl<A, T> ByteLen<Vec<T>> for super::RepeatTillEnd<A> where A: ByteLen<T> + Copy, T: DeepView {
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn length(&self, v: &Vec<T>) -> (len: usize) {
        let values = v.as_slice();
        proof {
            assert(values.deep_view() == v.deep_view());
        }
        Star(self.0).length(&values)
    }
}

#[cfg(feature = "alloc")]
impl<A, T> Prepare<Vec<T>> for super::RepeatTillEnd<A> where A: Prepare<T> + Copy, T: DeepView {
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn prepare(&self, v: &Vec<T>) -> Result<usize, PreSerializeError> {
        let values = v.as_slice();
        proof {
            assert(values.deep_view() == v.deep_view());
        }
        Star(self.0).prepare(&values)
    }
}

impl<Output: OutputBuf, A, T> Serializer<Output, Option<T>> for super::OptionalEnd<A> where
    A: Serializer<Output, T>,
    T: DeepView,
 {
    #[verifier::prophetic]
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn serialize_into(&self, v: &Option<T>, obuf: &mut Output) {
        Opt(&self.0).serialize_into(v, obuf);
    }
}

impl<A, AST> ByteLen<Option<AST>> for super::OptionalEnd<A> where A: ByteLen<AST>, AST: DeepView {
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn length(&self, v: &Option<AST>) -> (len: usize) {
        Opt(&self.0).length(v)
    }
}

impl<A, AST> Prepare<Option<AST>> for super::OptionalEnd<A> where A: Prepare<AST>, AST: DeepView {
    open spec fn exec_inv(&self) -> bool {
        self.0.exec_inv()
    }

    fn prepare(&self, v: &Option<AST>) -> Result<usize, PreSerializeError> {
        Opt(&self.0).prepare(v)
    }
}

} // verus!