bitcoin_internals/
script.rs

1// SPDX-License-Identifier: CC0-1.0
2
3//! Internal script related helper functions and types.
4
5#[cfg(creusot)]
6use creusot_std::prelude::*;
7#[cfg(creusot)]
8use creusot_std::prelude::{Clone, PartialEq};
9
10/// Reads a `usize` from an iterator.
11///
12/// A script push data instruction includes the length of the data being pushed, this function reads
13/// that length from an iterator (encoded in either 1, 2, or 4 bytes).
14///
15/// # Errors
16///
17/// Returns an error if the iterator does not contain enough bytes to read the length.
18// We internally use implementation based on iterator so that it automatically advances as needed.
19pub fn read_push_data_len(
20    data: &mut core::slice::Iter<'_, u8>,
21    size: PushDataLenLen,
22) -> Result<u32, EarlyEndOfScriptError> {
23    // The `size` enum enforces that the maximum shift will be 32 and
24    // that we can only ever read up to 4 bytes.
25    let size = size.to_usize();
26
27    if data.len() < size {
28        return Err(EarlyEndOfScriptError);
29    }
30
31    let mut ret = 0;
32    let mut i = 0u32;
33    #[cfg_attr(creusot, invariant(i@ == produced.len()))]
34    #[cfg_attr(creusot, variant(size@ - produced.len()))]
35    // Creusot has trouble proving take().enumerate() is correct, looks like a bug there
36    #[allow(clippy::explicit_counter_loop)]
37    for item in data.take(size) {
38        ret |= u32::from(*item) << (i * 8);
39        i += 1;
40    }
41    Ok(ret)
42}
43
44/// The number of bytes used to encode an unsigned integer as the length of a push data instruction.
45///
46/// This makes it easier to prove correctness of `next_push_data_len` and `read_push_data_len`.
47#[derive(Debug, Clone, Copy, Eq, PartialEq)]
48#[cfg_attr(not(creusot), derive(Hash))]
49pub enum PushDataLenLen {
50    /// Unsigned integer comprising of a single byte.
51    One = 1,
52    /// Unsigned integer comprising of two bytes.
53    Two = 2,
54    /// Unsigned integer comprising of four bytes.
55    Four = 4,
56}
57
58impl PushDataLenLen {
59    #[cfg_attr(creusot, ensures(result@ == self@))]
60    fn to_usize(self) -> usize {
61        // It seems Creusot doesn't translate casts properly
62        match self {
63            Self::One => 1,
64            Self::Two => 2,
65            Self::Four => 4,
66        }
67    }
68}
69
70impl Ord for PushDataLenLen {
71    #[cfg_attr(creusot, ensures(result == (*self).deep_model().cmp_log((*other).deep_model())))]
72    fn cmp(&self, other: &Self) -> core::cmp::Ordering { self.to_usize().cmp(&other.to_usize()) }
73}
74
75impl PartialOrd for PushDataLenLen {
76    #[cfg_attr(creusot, ensures(result == (*self).deep_model().partial_cmp_log((*other).deep_model())))]
77    fn partial_cmp(&self, other: &Self) -> Option<core::cmp::Ordering> { Some(self.cmp(other)) }
78}
79
80#[cfg(creusot)]
81impl View for PushDataLenLen {
82    type ViewTy = Int;
83
84    #[logic(open, inline)]
85    fn view(self) -> Self::ViewTy {
86        match self {
87            Self::One => 1,
88            Self::Two => 2,
89            Self::Four => 4,
90        }
91    }
92}
93
94#[cfg(creusot)]
95impl DeepModel for PushDataLenLen {
96    type DeepModelTy = Int;
97
98    #[logic(open, inline)]
99    fn deep_model(self) -> Self::DeepModelTy { self.view() }
100}
101
102/// Indicates that we tried to read more bytes from the script than available.
103#[derive(Debug)]
104pub struct EarlyEndOfScriptError;
105
106#[cfg(test)]
107mod tests {
108    use super::*;
109
110    #[test]
111    fn reads_4_bytes() {
112        let bytes = [0x01, 0x23, 0x45, 0x67];
113        let want = u32::from_le_bytes([0x01, 0x23, 0x45, 0x67]);
114        let got = read_push_data_len(&mut bytes.iter(), PushDataLenLen::Four).unwrap();
115        assert_eq!(got, want);
116    }
117
118    #[test]
119    fn reads_2_bytes() {
120        let bytes = [0x01, 0x23];
121        let want = u16::from_le_bytes([0x01, 0x23]);
122        let got = read_push_data_len(&mut bytes.iter(), PushDataLenLen::Two).unwrap();
123        assert_eq!(got, u32::from(want));
124    }
125
126    #[test]
127    fn reads_1_byte() {
128        let bytes = [0x01];
129        let want = 0x01u32;
130        let got = read_push_data_len(&mut bytes.iter(), PushDataLenLen::One).unwrap();
131        assert_eq!(got, want);
132    }
133}
bitcoin_internals/script.rs

bitcoin_internals/
script.rs
