bitcoin.rs

#![allow(warnings)]
use vest_lib::combinators::mapped::spec::*;
use vest_lib::combinators::recursive::*;
use vest_lib::combinators::*;
use vest_lib::core::exec::bytes_eq;
use vest_lib::core::exec::input::{InputBuf, InputSlice};
use vest_lib::core::exec::output::OutputBuf;
use vest_lib::core::exec::parser::*;
use vest_lib::core::exec::serializer::*;
use vest_lib::core::exec::ParseError;
use vest_lib::core::{proof::*, spec::*};
use vest_lib::primitives::btcvarint::VarInt;
use vest_lib::primitives::leb128::ULeb128;
use vest_lib::Never;
use vstd::prelude::*;
use Sum::Inl as L;
use Sum::Inr as R;
verus! {

// ============================================================
// Data Types
// ============================================================
# [doc = "data type for `block`."]
# [derive (Debug, PartialEq, Eq, Clone)]
pub struct Block<'i> {
    pub version: u32,
    pub prev_block: &'i [u8],
    pub merkle_root: &'i [u8],
    pub timestamp: u32,
    pub bits: u32,
    pub nonce: u32,
    pub tx_count: u64,
    pub txs: Vec<Tx<'i>>,
}

# [verifier::ext_equal]
pub struct BlockSpec<
    T0 = u32,
    T1 = Seq<u8>,
    T2 = Seq<u8>,
    T3 = u32,
    T4 = u32,
    T5 = u32,
    T6 = u64,
    T7 = Seq<TxSpec>,
> {
    pub version: T0,
    pub prev_block: T1,
    pub merkle_root: T2,
    pub timestamp: T3,
    pub bits: T4,
    pub nonce: T5,
    pub tx_count: T6,
    pub txs: T7,
}

pub type BlockInner = (u32, (Seq<u8>, (Seq<u8>, (u32, (u32, (u32, (u64, Seq<TxSpec>)))))));

impl<'i> DeepView for Block<'i> {
    type V = BlockSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        BlockSpec {
            version: self.version.deep_view(),
            prev_block: self.prev_block.deep_view(),
            merkle_root: self.merkle_root.deep_view(),
            timestamp: self.timestamp.deep_view(),
            bits: self.bits.deep_view(),
            nonce: self.nonce.deep_view(),
            tx_count: self.tx_count.deep_view(),
            txs: self.txs.deep_view(),
        }
    }
}

impl<'i> Block<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().version == self.version.deep_view(),
            self.deep_view().prev_block == self.prev_block.deep_view(),
            self.deep_view().merkle_root == self.merkle_root.deep_view(),
            self.deep_view().timestamp == self.timestamp.deep_view(),
            self.deep_view().bits == self.bits.deep_view(),
            self.deep_view().nonce == self.nonce.deep_view(),
            self.deep_view().tx_count == self.tx_count.deep_view(),
            self.deep_view().txs == self.txs.deep_view(),
    {
        reveal(<Block as DeepView>::deep_view);
    }
}

impl<T0, T1, T2, T3, T4, T5, T6, T7> BlockSpec<T0, T1, T2, T3, T4, T5, T6, T7> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, (T1, (T2, (T3, (T4, (T5, (T6, T7)))))))) -> Self {
        let (version, (prev_block, (merkle_root, (timestamp, (bits, (nonce, (tx_count, txs))))))) =
            input;
        Self { version, prev_block, merkle_root, timestamp, bits, nonce, tx_count, txs }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, (T1, (T2, (T3, (T4, (T5, (T6, T7))))))) {
        let Self { version, prev_block, merkle_root, timestamp, bits, nonce, tx_count, txs } = self;
        (version, (prev_block, (merkle_root, (timestamp, (bits, (nonce, (tx_count, txs)))))))
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(BlockSpec::from_structural);
        reveal(BlockSpec::into_structural);
    }

    pub broadcast proof fn lemma_into_from(input: (T0, (T1, (T2, (T3, (T4, (T5, (T6, T7))))))))
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(BlockSpec::from_structural);
        reveal(BlockSpec::into_structural);
    }

    pub proof fn lemma_into_structural_fields(self)
        ensures
            Self::into_structural(self) == match self {
                Self {
                    version,
                    prev_block,
                    merkle_root,
                    timestamp,
                    bits,
                    nonce,
                    tx_count,
                    txs,
                } => (
                    version,
                    (prev_block, (merkle_root, (timestamp, (bits, (nonce, (tx_count, txs)))))),
                ),
            },
    {
        reveal(BlockSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct BlockForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct BlockReverse;

impl SpecMap for BlockForward {
    type Input = BlockInner;

    type Output = BlockSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        BlockSpec::from_structural(input)
    }
}

impl SpecMap for BlockReverse {
    type Input = BlockSpec;

    type Output = BlockInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `tx`."]
# [derive (Debug, PartialEq, Eq, Clone)]
pub struct Tx<'i> {
    pub version: u32,
    pub txin_count: u64,
    pub rem: TxRem<'i>,
}

# [verifier::ext_equal]
pub struct TxSpec<T0 = u32, T1 = u64, T2 = TxRemSpec> {
    pub version: T0,
    pub txin_count: T1,
    pub rem: T2,
}

pub type TxInner = (u32, (u64, TxRemSpec));

impl<'i> DeepView for Tx<'i> {
    type V = TxSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        TxSpec {
            version: self.version.deep_view(),
            txin_count: self.txin_count.deep_view(),
            rem: self.rem.deep_view(),
        }
    }
}

impl<'i> Tx<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().version == self.version.deep_view(),
            self.deep_view().txin_count == self.txin_count.deep_view(),
            self.deep_view().rem == self.rem.deep_view(),
    {
        reveal(<Tx as DeepView>::deep_view);
    }
}

impl<T0, T1, T2> TxSpec<T0, T1, T2> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, (T1, T2))) -> Self {
        let (version, (txin_count, rem)) = input;
        Self { version, txin_count, rem }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, (T1, T2)) {
        let Self { version, txin_count, rem } = self;
        (version, (txin_count, rem))
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(TxSpec::from_structural);
        reveal(TxSpec::into_structural);
    }

    pub broadcast proof fn lemma_into_from(input: (T0, (T1, T2)))
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(TxSpec::from_structural);
        reveal(TxSpec::into_structural);
    }

    pub proof fn lemma_into_structural_fields(self)
        ensures
            Self::into_structural(self) == match self {
                Self { version, txin_count, rem } => (version, (txin_count, rem)),
            },
    {
        reveal(TxSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxReverse;

impl SpecMap for TxForward {
    type Input = TxInner;

    type Output = TxSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        TxSpec::from_structural(input)
    }
}

impl SpecMap for TxReverse {
    type Input = TxSpec;

    type Output = TxInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `tx_segwit`."]
# [derive (Debug, PartialEq, Eq, Clone)]
pub struct TxSegwit<'i> {
    pub flag: u8,
    pub txin_count: u64,
    pub txins: Vec<Txin<'i>>,
    pub txout_count: u64,
    pub txouts: Vec<Txout<'i>>,
    pub witness: Vec<Witness<'i>>,
    pub lock_time: LockTime,
}

# [verifier::ext_equal]
pub struct TxSegwitSpec<
    T0 = u8,
    T1 = u64,
    T2 = Seq<TxinSpec>,
    T3 = u64,
    T4 = Seq<TxoutSpec>,
    T5 = Seq<WitnessSpec>,
    T6 = LockTimeSpec,
> {
    pub flag: T0,
    pub txin_count: T1,
    pub txins: T2,
    pub txout_count: T3,
    pub txouts: T4,
    pub witness: T5,
    pub lock_time: T6,
}

pub type TxSegwitInner = (
    u8,
    (u64, (Seq<TxinSpec>, (u64, (Seq<TxoutSpec>, (Seq<WitnessSpec>, LockTimeSpec))))),
);

impl<'i> DeepView for TxSegwit<'i> {
    type V = TxSegwitSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        TxSegwitSpec {
            flag: self.flag.deep_view(),
            txin_count: self.txin_count.deep_view(),
            txins: self.txins.deep_view(),
            txout_count: self.txout_count.deep_view(),
            txouts: self.txouts.deep_view(),
            witness: self.witness.deep_view(),
            lock_time: self.lock_time.deep_view(),
        }
    }
}

impl<'i> TxSegwit<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().flag == self.flag.deep_view(),
            self.deep_view().txin_count == self.txin_count.deep_view(),
            self.deep_view().txins == self.txins.deep_view(),
            self.deep_view().txout_count == self.txout_count.deep_view(),
            self.deep_view().txouts == self.txouts.deep_view(),
            self.deep_view().witness == self.witness.deep_view(),
            self.deep_view().lock_time == self.lock_time.deep_view(),
    {
        reveal(<TxSegwit as DeepView>::deep_view);
    }
}

impl<T0, T1, T2, T3, T4, T5, T6> TxSegwitSpec<T0, T1, T2, T3, T4, T5, T6> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, (T1, (T2, (T3, (T4, (T5, T6))))))) -> Self {
        let (flag, (txin_count, (txins, (txout_count, (txouts, (witness, lock_time)))))) = input;
        Self { flag, txin_count, txins, txout_count, txouts, witness, lock_time }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, (T1, (T2, (T3, (T4, (T5, T6)))))) {
        let Self { flag, txin_count, txins, txout_count, txouts, witness, lock_time } = self;
        (flag, (txin_count, (txins, (txout_count, (txouts, (witness, lock_time))))))
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(TxSegwitSpec::from_structural);
        reveal(TxSegwitSpec::into_structural);
    }

    pub broadcast proof fn lemma_into_from(input: (T0, (T1, (T2, (T3, (T4, (T5, T6)))))))
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(TxSegwitSpec::from_structural);
        reveal(TxSegwitSpec::into_structural);
    }

    pub proof fn lemma_into_structural_fields(self)
        ensures
            Self::into_structural(self) == match self {
                Self { flag, txin_count, txins, txout_count, txouts, witness, lock_time } => (
                    flag,
                    (txin_count, (txins, (txout_count, (txouts, (witness, lock_time))))),
                ),
            },
    {
        reveal(TxSegwitSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxSegwitForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxSegwitReverse;

impl SpecMap for TxSegwitForward {
    type Input = TxSegwitInner;

    type Output = TxSegwitSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        TxSegwitSpec::from_structural(input)
    }
}

impl SpecMap for TxSegwitReverse {
    type Input = TxSegwitSpec;

    type Output = TxSegwitInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `witness`."]
# [derive (Debug, PartialEq, Eq, Clone)]
pub struct Witness<'i> {
    pub count: u64,
    pub data: Vec<WitnessComponent<'i>>,
}

# [verifier::ext_equal]
pub struct WitnessSpec<T0 = u64, T1 = Seq<WitnessComponentSpec>> {
    pub count: T0,
    pub data: T1,
}

pub type WitnessInner = (u64, Seq<WitnessComponentSpec>);

impl<'i> DeepView for Witness<'i> {
    type V = WitnessSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        WitnessSpec { count: self.count.deep_view(), data: self.data.deep_view() }
    }
}

impl<'i> Witness<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().count == self.count.deep_view(),
            self.deep_view().data == self.data.deep_view(),
    {
        reveal(<Witness as DeepView>::deep_view);
    }
}

impl<T0, T1> WitnessSpec<T0, T1> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, T1)) -> Self {
        let (count, data) = input;
        Self { count, data }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, T1) {
        let Self { count, data } = self;
        (count, data)
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(WitnessSpec::from_structural);
        reveal(WitnessSpec::into_structural);
    }

    pub broadcast proof fn lemma_into_from(input: (T0, T1))
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(WitnessSpec::from_structural);
        reveal(WitnessSpec::into_structural);
    }

    pub proof fn lemma_into_structural_fields(self)
        ensures
            Self::into_structural(self) == match self {
                Self { count, data } => (count, data),
            },
    {
        reveal(WitnessSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct WitnessForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct WitnessReverse;

impl SpecMap for WitnessForward {
    type Input = WitnessInner;

    type Output = WitnessSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        WitnessSpec::from_structural(input)
    }
}

impl SpecMap for WitnessReverse {
    type Input = WitnessSpec;

    type Output = WitnessInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `witness_component`."]
# [derive (Debug, PartialEq, Eq, Clone, Copy)]
pub struct WitnessComponent<'i> {
    pub l: u64,
    pub data: &'i [u8],
}

# [verifier::ext_equal]
pub struct WitnessComponentSpec<T0 = u64, T1 = Seq<u8>> {
    pub l: T0,
    pub data: T1,
}

pub type WitnessComponentInner = (u64, Seq<u8>);

impl<'i> DeepView for WitnessComponent<'i> {
    type V = WitnessComponentSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        WitnessComponentSpec { l: self.l.deep_view(), data: self.data.deep_view() }
    }
}

impl<'i> WitnessComponent<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().l == self.l.deep_view(),
            self.deep_view().data == self.data.deep_view(),
    {
        reveal(<WitnessComponent as DeepView>::deep_view);
    }
}

impl<T0, T1> WitnessComponentSpec<T0, T1> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, T1)) -> Self {
        let (l, data) = input;
        Self { l, data }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, T1) {
        let Self { l, data } = self;
        (l, data)
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(WitnessComponentSpec::from_structural);
        reveal(WitnessComponentSpec::into_structural);
    }

    pub broadcast proof fn lemma_into_from(input: (T0, T1))
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(WitnessComponentSpec::from_structural);
        reveal(WitnessComponentSpec::into_structural);
    }

    pub proof fn lemma_into_structural_fields(self)
        ensures
            Self::into_structural(self) == match self {
                Self { l, data } => (l, data),
            },
    {
        reveal(WitnessComponentSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct WitnessComponentForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct WitnessComponentReverse;

impl SpecMap for WitnessComponentForward {
    type Input = WitnessComponentInner;

    type Output = WitnessComponentSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        WitnessComponentSpec::from_structural(input)
    }
}

impl SpecMap for WitnessComponentReverse {
    type Input = WitnessComponentSpec;

    type Output = WitnessComponentInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `tx_nonsegwit`."]
# [derive (Debug, PartialEq, Eq, Clone)]
pub struct TxNonsegwit<'i> {
    pub txins: Vec<Txin<'i>>,
    pub txout_count: u64,
    pub txouts: Vec<Txout<'i>>,
    pub lock_time: LockTime,
}

# [verifier::ext_equal]
pub struct TxNonsegwitSpec<T0 = Seq<TxinSpec>, T1 = u64, T2 = Seq<TxoutSpec>, T3 = LockTimeSpec> {
    pub txins: T0,
    pub txout_count: T1,
    pub txouts: T2,
    pub lock_time: T3,
}

pub type TxNonsegwitInner = (Seq<TxinSpec>, (u64, (Seq<TxoutSpec>, LockTimeSpec)));

impl<'i> DeepView for TxNonsegwit<'i> {
    type V = TxNonsegwitSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        TxNonsegwitSpec {
            txins: self.txins.deep_view(),
            txout_count: self.txout_count.deep_view(),
            txouts: self.txouts.deep_view(),
            lock_time: self.lock_time.deep_view(),
        }
    }
}

impl<'i> TxNonsegwit<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().txins == self.txins.deep_view(),
            self.deep_view().txout_count == self.txout_count.deep_view(),
            self.deep_view().txouts == self.txouts.deep_view(),
            self.deep_view().lock_time == self.lock_time.deep_view(),
    {
        reveal(<TxNonsegwit as DeepView>::deep_view);
    }
}

impl<T0, T1, T2, T3> TxNonsegwitSpec<T0, T1, T2, T3> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, (T1, (T2, T3)))) -> Self {
        let (txins, (txout_count, (txouts, lock_time))) = input;
        Self { txins, txout_count, txouts, lock_time }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, (T1, (T2, T3))) {
        let Self { txins, txout_count, txouts, lock_time } = self;
        (txins, (txout_count, (txouts, lock_time)))
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(TxNonsegwitSpec::from_structural);
        reveal(TxNonsegwitSpec::into_structural);
    }

    pub broadcast proof fn lemma_into_from(input: (T0, (T1, (T2, T3))))
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(TxNonsegwitSpec::from_structural);
        reveal(TxNonsegwitSpec::into_structural);
    }

    pub proof fn lemma_into_structural_fields(self)
        ensures
            Self::into_structural(self) == match self {
                Self { txins, txout_count, txouts, lock_time } => (
                    txins,
                    (txout_count, (txouts, lock_time)),
                ),
            },
    {
        reveal(TxNonsegwitSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxNonsegwitForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxNonsegwitReverse;

impl SpecMap for TxNonsegwitForward {
    type Input = TxNonsegwitInner;

    type Output = TxNonsegwitSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        TxNonsegwitSpec::from_structural(input)
    }
}

impl SpecMap for TxNonsegwitReverse {
    type Input = TxNonsegwitSpec;

    type Output = TxNonsegwitInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `lock_time`."]
# [derive (Debug, PartialEq, Eq, Clone, Copy)]
pub enum LockTime {
    BlockNo(u32),
    Timestamp(u32),
}

# [verifier::ext_equal]
pub enum LockTimeSpec<T0 = u32, T1 = u32> {
    BlockNo(T0),
    Timestamp(T1),
}

pub type LockTimeInner = Sum<u32, u32>;

impl DeepView for LockTime {
    type V = LockTimeSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        match self {
            LockTime::BlockNo(v) => LockTimeSpec::BlockNo(v.deep_view()),
            LockTime::Timestamp(v) => LockTimeSpec::Timestamp(v.deep_view()),
        }
    }
}

impl LockTime {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view() == match self {
                LockTime::BlockNo(v) => LockTimeSpec::BlockNo(v.deep_view()),
                LockTime::Timestamp(v) => LockTimeSpec::Timestamp(v.deep_view()),
            },
    {
        reveal(<LockTime as DeepView>::deep_view);
    }
}

impl<T0, T1> LockTimeSpec<T0, T1> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: Sum<T0, T1>) -> Self {
        match input {
            L(value) => Self::BlockNo(value),
            R(value) => Self::Timestamp(value),
        }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> Sum<T0, T1> {
        match self {
            Self::BlockNo(value) => L(value),
            Self::Timestamp(value) => R(value),
        }
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(LockTimeSpec::from_structural);
        reveal(LockTimeSpec::into_structural);
        match self {
            Self::BlockNo(_) => {},
            Self::Timestamp(_) => {},
        }
    }

    pub broadcast proof fn lemma_into_from(input: Sum<T0, T1>)
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(LockTimeSpec::from_structural);
        reveal(LockTimeSpec::into_structural);
        match input {
            L(_) => {},
            R(_) => {},
        }
    }

    pub proof fn lemma_into_structural_variant(self)
        ensures
            Self::into_structural(self) == match self {
                Self::BlockNo(value) => L(value),
                Self::Timestamp(value) => R(value),
            },
    {
        reveal(LockTimeSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct LockTimeForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct LockTimeReverse;

impl SpecMap for LockTimeForward {
    type Input = LockTimeInner;

    type Output = LockTimeSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        LockTimeSpec::from_structural(input)
    }
}

impl SpecMap for LockTimeReverse {
    type Input = LockTimeSpec;

    type Output = LockTimeInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `txout`."]
# [derive (Debug, PartialEq, Eq, Clone, Copy)]
pub struct Txout<'i> {
    pub value: u64,
    pub script_pubkey: Script<'i>,
}

# [verifier::ext_equal]
pub struct TxoutSpec<T0 = u64, T1 = ScriptSpec> {
    pub value: T0,
    pub script_pubkey: T1,
}

pub type TxoutInner = (u64, ScriptSpec);

impl<'i> DeepView for Txout<'i> {
    type V = TxoutSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        TxoutSpec { value: self.value.deep_view(), script_pubkey: self.script_pubkey.deep_view() }
    }
}

impl<'i> Txout<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().value == self.value.deep_view(),
            self.deep_view().script_pubkey == self.script_pubkey.deep_view(),
    {
        reveal(<Txout as DeepView>::deep_view);
    }
}

impl<T0, T1> TxoutSpec<T0, T1> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, T1)) -> Self {
        let (value, script_pubkey) = input;
        Self { value, script_pubkey }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, T1) {
        let Self { value, script_pubkey } = self;
        (value, script_pubkey)
    }

    pub broadcast proof fn lemma_from_into(self)
        ensures
            # [trigger] Self::from_structural(Self::into_structural(self)) == self,
    {
        reveal(TxoutSpec::from_structural);
        reveal(TxoutSpec::into_structural);
    }

    pub broadcast proof fn lemma_into_from(input: (T0, T1))
        ensures
            # [trigger] Self::into_structural(Self::from_structural(input)) == input,
    {
        reveal(TxoutSpec::from_structural);
        reveal(TxoutSpec::into_structural);
    }

    pub proof fn lemma_into_structural_fields(self)
        ensures
            Self::into_structural(self) == match self {
                Self { value, script_pubkey } => (value, script_pubkey),
            },
    {
        reveal(TxoutSpec::into_structural);
    }
}

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxoutForward;

# [derive (Clone, Copy)]
# [doc (hidden)]
pub struct TxoutReverse;

impl SpecMap for TxoutForward {
    type Input = TxoutInner;

    type Output = TxoutSpec;

    open spec fn spec_map(&self, input: Self::Input) -> Self::Output {
        TxoutSpec::from_structural(input)
    }
}

impl SpecMap for TxoutReverse {
    type Input = TxoutSpec;

    type Output = TxoutInner;

    open spec fn spec_map(&self, value: Self::Input) -> Self::Output {
        value.into_structural()
    }
}

# [doc = "data type for `script`."]
# [derive (Debug, PartialEq, Eq, Clone, Copy)]
pub struct Script<'i> {
    pub l: u64,
    pub data: &'i [u8],
}

# [verifier::ext_equal]
pub struct ScriptSpec<T0 = u64, T1 = Seq<u8>> {
    pub l: T0,
    pub data: T1,
}

pub type ScriptInner = (u64, Seq<u8>);

impl<'i> DeepView for Script<'i> {
    type V = ScriptSpec;

    # [verifier::opaque]
    open spec fn deep_view(&self) -> Self::V {
        ScriptSpec { l: self.l.deep_view(), data: self.data.deep_view() }
    }
}

impl<'i> Script<'i> {
    pub proof fn lemma_deep_view_fields(&self)
        ensures
            self.deep_view().l == self.l.deep_view(),
            self.deep_view().data == self.data.deep_view(),
    {
        reveal(<Script as DeepView>::deep_view);
    }
}

impl<T0, T1> ScriptSpec<T0, T1> {
    # [verifier::opaque]
    pub open spec fn from_structural(input: (T0, T1)) -> Self {
        let (l, data) = input;
        Self { l, data }
    }

    # [verifier::opaque]
    pub open spec fn into_structural(self) -> (T0, T1) {
        let Self { l, data } = self;
        (l, data)