tasm_lib/arithmetic/u64/
lt.rs

1use std::collections::HashMap;
2
3use triton_vm::prelude::*;
4
5use crate::prelude::*;
6use crate::traits::basic_snippet::Reviewer;
7use crate::traits::basic_snippet::SignOffFingerprint;
8
9/// Perform the “[less than](u64::lt)” operation.
10///
11/// ### Behavior
12///
13/// ```text
14/// BEFORE: _ [rhs: u64] [lhs: u64]
15/// AFTER:  _ [lhs < rhs: bool]
16/// ```
17///
18/// ### Preconditions
19///
20/// - all input arguments are properly [`BFieldCodec`] encoded
21///
22/// ### Postconditions
23///
24/// - the output is `true` if and only if the input argument `lhs` is less than
25///   the input argument `rhs`
26/// - the output is properly [`BFieldCodec`] encoded
27#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
28pub struct Lt;
29
30impl BasicSnippet for Lt {
31    fn inputs(&self) -> Vec<(DataType, String)> {
32        ["rhs", "lhs"]
33            .map(|s| (DataType::U64, s.to_owned()))
34            .to_vec()
35    }
36
37    fn outputs(&self) -> Vec<(DataType, String)> {
38        vec![(DataType::Bool, "lhs < rhs".to_owned())]
39    }
40
41    fn entrypoint(&self) -> String {
42        "tasmlib_arithmetic_u64_lt".to_owned()
43    }
44
45    fn code(&self, _: &mut Library) -> Vec<LabelledInstruction> {
46        triton_asm!(
47            {self.entrypoint()}:
48                // _ rhs_hi rhs_lo lhs_hi lhs_lo
49
50                /* lhs < rhs if and only if
51                 * lhs_hi < rhs_hi or
52                 * lhs_hi == rhs_hi and lhs_lo < rhs_lo
53                 */
54
55                dup 3
56                dup 2
57                // _ rhs_hi rhs_lo lhs_hi lhs_lo rhs_hi lhs_hi
58
59                lt
60                // _ rhs_hi rhs_lo lhs_hi lhs_lo (lhs_hi < rhs_hi)
61
62                pick 4
63                pick 3
64                eq
65                // _ rhs_lo lhs_lo (lhs_hi < rhs_hi) (rhs_hi == lhs_hi)
66
67                pick 3
68                pick 3
69                // _ (lhs_hi < rhs_hi) (rhs_hi == lhs_hi) rhs_lo lhs_lo
70
71                lt
72                // _ (lhs_hi < rhs_hi) (rhs_hi == lhs_hi) (lhs_lo < rhs_lo)
73
74                mul
75                add
76                // _ (lhs < rhs)
77
78                return
79        )
80    }
81
82    fn sign_offs(&self) -> HashMap<Reviewer, SignOffFingerprint> {
83        let mut sign_offs = HashMap::new();
84        sign_offs.insert(Reviewer("ferdinand"), 0x1e4d56adb16e1520.into());
85        sign_offs
86    }
87}
88
89#[cfg(test)]
90pub(crate) mod tests {
91    use super::*;
92    use crate::test_prelude::*;
93
94    impl Lt {
95        pub fn assert_expected_lt_behavior(&self, lhs: u64, rhs: u64) {
96            let initial_stack = self.set_up_test_stack((lhs, rhs));
97
98            let mut expected_stack = initial_stack.clone();
99            self.rust_shadow(&mut expected_stack);
100
101            test_rust_equivalence_given_complete_state(
102                &ShadowedClosure::new(Self),
103                &initial_stack,
104                &[],
105                &NonDeterminism::default(),
106                &None,
107                Some(&expected_stack),
108            );
109        }
110    }
111
112    impl Closure for Lt {
113        type Args = (u64, u64);
114
115        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) {
116            let (right, left) = pop_encodable::<Self::Args>(stack);
117            push_encodable(stack, &(left < right));
118        }
119
120        fn pseudorandom_args(
121            &self,
122            seed: [u8; 32],
123            bench_case: Option<BenchmarkCase>,
124        ) -> Self::Args {
125            match bench_case {
126                Some(BenchmarkCase::CommonCase) => (0x100_ffff_ffff, 0x100_ffff_fffe),
127                Some(BenchmarkCase::WorstCase) => (u64::MAX - 1, u64::MAX),
128                None => StdRng::from_seed(seed).random(),
129            }
130        }
131
132        fn corner_case_args(&self) -> Vec<Self::Args> {
133            let edge_case_points = [0, 1 << 29, 1 << 31, 1 << 32, u64::MAX]
134                .into_iter()
135                .flat_map(|p| [p.checked_sub(1), Some(p), p.checked_add(1)])
136                .flatten()
137                .collect_vec();
138
139            edge_case_points
140                .iter()
141                .cartesian_product(&edge_case_points)
142                .map(|(&left, &right)| (left, right))
143                .collect()
144        }
145    }
146
147    #[test]
148    fn rust_shadow_test() {
149        ShadowedClosure::new(Lt).test()
150    }
151
152    #[test]
153    fn unit_test() {
154        Lt.assert_expected_lt_behavior(11 * (1 << 32), 15 * (1 << 32));
155    }
156
157    #[proptest]
158    fn property_test(left: u64, right: u64) {
159        Lt.assert_expected_lt_behavior(left, right);
160    }
161}
162
163#[cfg(test)]
164mod benches {
165    use super::*;
166    use crate::test_prelude::*;
167
168    #[test]
169    fn benchmark() {
170        ShadowedClosure::new(Lt).bench();
171    }
172}
tasm_lib/arithmetic/u64/lt.rs

tasm_lib/arithmetic/u64/
lt.rs
