tasm_lib/arithmetic/u160/
lt.rs

1use triton_vm::prelude::*;
2
3use crate::prelude::*;
4
5/// Less-Than for `U160`s.
6///
7/// ### Behavior
8///
9/// ```text
10/// BEFORE: _ [rhs; 5] [lhs; 5]
11/// AFTER:  _ (lhs < rhs)
12/// ```
13///
14/// ### Preconditions
15///
16/// - all input arguments are properly [`BFieldCodec`] encoded
17///
18/// ### Postconditions
19///
20/// - the output is properly [`BFieldCodec`] encoded
21#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
22pub struct Lt;
23
24impl BasicSnippet for Lt {
25    fn parameters(&self) -> Vec<(DataType, String)> {
26        ["rhs", "lhs"]
27            .map(|s| (DataType::U160, s.to_string()))
28            .to_vec()
29    }
30
31    fn return_values(&self) -> Vec<(DataType, String)> {
32        vec![(DataType::Bool, "cmp".to_string())]
33    }
34
35    fn entrypoint(&self) -> String {
36        "tasmlib_arithmetic_u160_lt".to_string()
37    }
38
39    fn code(&self, library: &mut Library) -> Vec<LabelledInstruction> {
40        let entrypoint = self.entrypoint();
41
42        let lt_u128 = library.import(Box::new(crate::arithmetic::u128::lt::Lt));
43
44        triton_asm! {
45            // BEFORE: _ r4 r3 r2 r1 r0 l4 l3 l2 l1 l0
46            // AFTER: _ (l < r)
47            {entrypoint}:
48
49                // l < r <=> l4 < r4 || l4 == r4 && l3 < r3 || l4 == r4 && l3 == r3 && l2 < r2
50                //        || l4 == r4 && l3 == r3 && l2 == r2 && l1 < r1
51                //        || l4 == r4 && l3 == r3 && l2 == r2 && l1 == r1 && l0 < r0
52
53                // Expressed as u128 inequality
54                // l4 < r4 || l4 == r4 && l_lo < r_lo
55
56                pick 4
57                place 8
58                // _ r4 l4 r3 r2 r1 r0 l3 l2 l1 l0
59
60                call {lt_u128}
61                // _ r4 l4 (r_lo > l_lo)
62
63                dup 2
64                dup 2
65                eq
66                // _ r4 l4 (r_lo > l_lo) (r4 == l4)
67
68                mul
69                // _ r4 l4 ((r_lo > l_lo) && (r4 == l4))
70
71                place 2
72                lt
73                add
74                // _ (((r_lo > l_lo) && (r4 == l4)) || (r4 > l4))
75                // _ l < r
76
77                return
78        }
79    }
80}
81
82#[cfg(test)]
83mod tests {
84    use num::BigUint;
85    use rand::rngs::StdRng;
86
87    use super::*;
88    use crate::arithmetic::u160::u128_to_u160;
89    use crate::test_helpers::test_rust_equivalence_given_execution_state;
90    use crate::test_prelude::*;
91
92    impl Closure for Lt {
93        type Args = ([u32; 5], [u32; 5]);
94
95        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) -> Result<(), RustShadowError> {
96            let left: [u32; 5] = pop_encodable(stack)?;
97            let left: BigUint = BigUint::new(left.to_vec());
98
99            let right: [u32; 5] = pop_encodable(stack)?;
100            let right: BigUint = BigUint::new(right.to_vec());
101            push_encodable(stack, &(left < right));
102            Ok(())
103        }
104
105        fn pseudorandom_args(&self, seed: [u8; 32], _: Option<BenchmarkCase>) -> Self::Args {
106            StdRng::from_seed(seed).random()
107        }
108    }
109
110    fn test_rust_tasm_equivalence(left: [u32; 5], right: [u32; 5]) {
111        let initial_state = InitVmState::with_stack(Lt.set_up_test_stack((left, right)));
112        test_rust_equivalence_given_execution_state(&ShadowedClosure::new(Lt), initial_state);
113    }
114
115    #[macro_rules_attr::apply(test)]
116    fn lt_u160_standard_test() {
117        ShadowedClosure::new(Lt).test()
118    }
119
120    #[macro_rules_attr::apply(test)]
121    fn lt_u160_edge_cases_test() {
122        let mut boundary_points = [0, 1 << 32, 1 << 64, 1 << 96, u128::MAX]
123            .into_iter()
124            .flat_map(|p| [p.checked_sub(1), Some(p), p.checked_add(1)])
125            .flatten()
126            .map(u128_to_u160)
127            .collect_vec();
128        boundary_points.extend([
129            [u32::MAX; 5],
130            [1; 5],
131            [0, 0, 0, 0, 1],
132            [0, 0, 0, 0, u32::MAX],
133            [0x72581af6, 0, 0, 0, 0x72581af6],
134            [0x72581af6, 0, 0, 0, 0x72581af5],
135            [0x72581af5, 0, 0, 0, 0x72581af6],
136            [0x72581af5, 0, 0, 0, 0x72581af5],
137        ]);
138
139        for (&left, &right) in boundary_points.iter().cartesian_product(&boundary_points) {
140            test_rust_tasm_equivalence(left, right);
141        }
142    }
143
144    #[macro_rules_attr::apply(proptest)]
145    fn lt_u160_randomized_test_identical_args(v: [u32; 5]) {
146        test_rust_tasm_equivalence(v, v);
147    }
148}
149
150#[cfg(test)]
151mod benches {
152    use super::*;
153    use crate::test_prelude::*;
154
155    #[macro_rules_attr::apply(test)]
156    fn benchmark() {
157        ShadowedClosure::new(Lt).bench()
158    }
159}
tasm_lib/arithmetic/u160/lt.rs

tasm_lib/arithmetic/u160/
lt.rs
