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 {
73        self.to_usize().cmp(&other.to_usize())
74    }
75}
76
77impl PartialOrd for PushDataLenLen {
78    #[cfg_attr(creusot, ensures(result == (*self).deep_model().partial_cmp_log((*other).deep_model())))]
79    fn partial_cmp(&self, other: &Self) -> Option<core::cmp::Ordering> {
80        Some(self.cmp(other))
81    }
82}
83
84#[cfg(creusot)]
85impl View for PushDataLenLen {
86    type ViewTy = Int;
87
88    #[logic(open, inline)]
89    fn view(self) -> Self::ViewTy {
90        match self {
91            Self::One => 1,
92            Self::Two => 2,
93            Self::Four => 4,
94        }
95    }
96}
97
98#[cfg(creusot)]
99impl DeepModel for PushDataLenLen {
100    type DeepModelTy = Int;
101
102    #[logic(open, inline)]
103    fn deep_model(self) -> Self::DeepModelTy {
104        self.view()
105    }
106}
107
108/// Indicates that we tried to read more bytes from the script than available.
109#[derive(Debug)]
110pub struct EarlyEndOfScriptError;
111
112#[cfg(test)]
113mod tests {
114    use super::*;
115
116    #[test]
117    fn reads_4_bytes() {
118        let bytes = [0x01, 0x23, 0x45, 0x67];
119        let want = u32::from_le_bytes([0x01, 0x23, 0x45, 0x67]);
120        let got = read_push_data_len(&mut bytes.iter(), PushDataLenLen::Four).unwrap();
121        assert_eq!(got, want);
122    }
123
124    #[test]
125    fn reads_2_bytes() {
126        let bytes = [0x01, 0x23];
127        let want = u16::from_le_bytes([0x01, 0x23]);
128        let got = read_push_data_len(&mut bytes.iter(), PushDataLenLen::Two).unwrap();
129        assert_eq!(got, u32::from(want));
130    }
131
132    #[test]
133    fn reads_1_byte() {
134        let bytes = [0x01];
135        let want = 0x01u32;
136        let got = read_push_data_len(&mut bytes.iter(), PushDataLenLen::One).unwrap();
137        assert_eq!(got, want);
138    }
139}
bitcoin_internals/script.rs

bitcoin_internals/
script.rs
