vest_lib 0.2.2

//! Executable sequential composition.
use crate::combinators::mapped::spec::SpecMap;
use crate::core::exec::fns::MapRef;
use crate::core::exec::output::*;
use crate::core::{
    exec::{
        input::InputBuf,
        parser::{PResult, Parser},
        serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
    },
    spec::{SafeParser, SpecByteLen, SpecParser, SpecSerializer},
};
use vstd::prelude::*;
use OutputBuf;

verus! {

impl<I, A, B> Parser<I> for super::Pair<A, B> where
    I: InputBuf,
    A: Parser<I> + SafeParser,
    B: Parser<I> + SafeParser,
 {
    type PT = (A::PT, B::PT);

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

    fn min_byte_len(&self) -> usize {
        // This is only a hint, so a saturating sum is fine.
        self.0.min_byte_len().saturating_add(self.1.min_byte_len())
    }

    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
        assert(self.exec_inv());
        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;

        let (na, va) = self.0.parse(ibuf)?;
        let rest = ibuf.skip(na);
        let (nb, vb) = self.1.parse(&rest)?;

        let _total_len = ibuf.len();
        proof {
            assert(na + nb <= _total_len);
        }
        let nab = na + nb;
        let pair = (va, vb);
        assert(self.spec_parse(ibuf@) == Some((nab as int, pair.deep_view())));
        Ok((nab, pair))
    }
}

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

    fn serialize_into(&self, v: &(TA, TB), obuf: &mut Output) {
        broadcast use crate::core::exec::output::outbuf_lemmas;

        self.0.serialize_into(&v.0, obuf);
        self.1.serialize_into(&v.1, obuf);
    }
}

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

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

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

    fn length(&self, v: &(TA, TB)) -> (len: usize) {
        let la = self.0.length(&v.0);
        let lb = self.1.length(&v.1);
        la + lb
    }
}

impl<I, A, B> Parser<I> for super::Bind<A, B> where
    I: InputBuf,
    A: Parser<I> + SafeParser,
    B::O: Parser<I> + SafeParser,
    B: MapRef<A::PT, Input = A::PVal>,
 {
    type PT = (A::PT, <B::O as Parser<I>>::PT);

    fn min_byte_len(&self) -> usize {
        // `B` is built from `A`'s value, so only `A` is known statically.
        self.0.min_byte_len()
    }

    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& self.0.safe_inv()
        &&& forall|pb: B::O| #[trigger] pb.exec_inv() && pb.safe_inv()
    }

    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;

        let (na, key) = self.0.parse(ibuf)?;
        let rest = ibuf.skip(na);
        let next = self.1.map(&key);
        assert(next.exec_inv() && next.safe_inv());
        let (nb, val) = next.parse(&rest)?;

        let _total_len = ibuf.len();
        proof {
            assert(na + nb <= _total_len);
        }
        let nab = na + nb;
        let pair = (key, val);
        Ok((nab, pair))
    }
}

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for super::Bind<A, B> where
    TA: DeepView,
    TB: DeepView,
    A: Serializer<Output, TA>,
    B::O: Serializer<Output, TB>,
    B: MapRef<TA, Input = TA::V>,
 {
    #[verifier::prophetic]
    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
    }

    fn serialize_into(&self, v: &(TA, TB), obuf: &mut Output) {
        broadcast use crate::core::exec::output::outbuf_lemmas;

        let next = self.1.map(&v.0);
        self.0.serialize_into(&v.0, obuf);
        next.serialize_into(&v.1, obuf);
    }
}

impl<A, B, STA, STB> ByteLen<(STA, STB)> for super::Bind<A, B> where
    STA: DeepView,
    STB: DeepView,
    A: ByteLen<STA>,
    B::O: ByteLen<STB>,
    B: MapRef<STA, Input = STA::V>,
 {
    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
    }

    fn length(&self, v: &(STA, STB)) -> (len: usize) {
        let next = self.1.map(&v.0);
        let la = self.0.length(&v.0);
        let lb = next.length(&v.1);
        la + lb
    }
}

impl<A, B, STA, STB> Prepare<(STA, STB)> for super::Bind<A, B> where
    STA: DeepView,
    STB: DeepView,
    A: Prepare<STA>,
    B::O: Prepare<STB>,
    B: MapRef<STA, Input = STA::V>,
 {
    open spec fn exec_inv(&self) -> bool {
        &&& self.0.exec_inv()
        &&& forall|pb: B::O| #[trigger] pb.exec_inv()
    }

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

} // verus!