tasm_lib/arithmetic/u128/
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/// Less-Than for `U128`s.
10///
11/// ### Behavior
12///
13/// ```text
14/// BEFORE: _ [rhs; 4] [lhs; 4]
15/// AFTER:  _ (lhs < rhs)
16/// ```
17///
18/// ### Preconditions
19///
20/// - all input arguments are properly [`BFieldCodec`] encoded
21///
22/// ### Postconditions
23///
24/// - the output is properly [`BFieldCodec`] encoded
25#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)]
26pub struct Lt;
27
28impl BasicSnippet for Lt {
29    fn parameters(&self) -> Vec<(DataType, String)> {
30        ["rhs", "lhs"]
31            .map(|s| (DataType::U128, s.to_string()))
32            .to_vec()
33    }
34
35    fn return_values(&self) -> Vec<(DataType, String)> {
36        vec![(DataType::Bool, "cmp".to_string())]
37    }
38
39    fn entrypoint(&self) -> String {
40        "tasmlib_arithmetic_u128_lt".to_string()
41    }
42
43    fn code(&self, library: &mut Library) -> Vec<LabelledInstruction> {
44        let entrypoint = self.entrypoint();
45
46        let compare_u64 = DataType::U64.compare();
47        let lt_u64 = library.import(Box::new(crate::arithmetic::u64::lt::Lt));
48
49        triton_asm! {
50            // BEFORE: _ r3 r2 r1 r0 l3 l2 l1 l0
51            // AFTER: _ (l < r)
52            {entrypoint}:
53
54                pick 5 pick 5
55                pick 3 pick 3
56                // _ r3 r2 l3 l2 r1 r0 l1 l0
57
58                call {lt_u64}
59                // _ r3 r2 l3 l2 (l1 || l0  <  r1 || r0)
60
61                dup 4
62                dup 4
63                dup 4
64                dup 4
65                {&compare_u64}
66                // _ r3 r2 l3 l2 (l1 || l0  <  r1 || r0) (l3 || l2  ==  r3 || r2)
67
68                mul
69                // _ r3 r2 l3 l2 ((l1 || l0  <  r1 || r0) * (l3 || l2  ==  r3 || r2))
70
71                place 4
72                // _ ((l1 || l0  <  r1 || r0) * (l3 || l2  ==  r3 || r2)) r3 r2 l3 l2
73
74                call {lt_u64}
75                // _ ((l1 || l0  <  r1 || r0) * (l3 || l2  ==  r3 || r2)) (l3 || l2  <  r3 || r2)
76
77                add
78                // _ (l < r)
79                return
80        }
81    }
82
83    fn sign_offs(&self) -> HashMap<Reviewer, SignOffFingerprint> {
84        let mut sign_offs = HashMap::new();
85        sign_offs.insert(Reviewer("ferdinand"), 0xf6188121bd7f252b.into());
86        sign_offs
87    }
88}
89
90#[cfg(test)]
91mod tests {
92    use rand::rngs::StdRng;
93
94    use super::*;
95    use crate::test_helpers::test_rust_equivalence_given_execution_state;
96    use crate::test_prelude::*;
97
98    impl Closure for Lt {
99        type Args = (u128, u128);
100
101        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) -> Result<(), RustShadowError> {
102            let (right, left) = pop_encodable::<Self::Args>(stack)?;
103            push_encodable(stack, &(left < right));
104            Ok(())
105        }
106
107        fn pseudorandom_args(&self, seed: [u8; 32], _: Option<BenchmarkCase>) -> Self::Args {
108            StdRng::from_seed(seed).random()
109        }
110    }
111
112    #[macro_rules_attr::apply(test)]
113    fn lt_u128_standard_test() {
114        ShadowedClosure::new(Lt).test()
115    }
116
117    fn test_rust_tasm_equivalence(left: u128, right: u128) {
118        let initial_state = InitVmState::with_stack(Lt.set_up_test_stack((left, right)));
119        test_rust_equivalence_given_execution_state(&ShadowedClosure::new(Lt), initial_state);
120    }
121
122    #[macro_rules_attr::apply(test)]
123    fn lt_u128_unit_test() {
124        test_rust_tasm_equivalence(1 << 64, 1 << 32);
125        test_rust_tasm_equivalence(1 << 32, 1 << 64);
126    }
127
128    #[macro_rules_attr::apply(test)]
129    fn lt_u128_edge_cases_test() {
130        let boundary_points = [0, 1 << 32, 1 << 64, 1 << 96, u128::MAX]
131            .into_iter()
132            .flat_map(|p| [p.checked_sub(1), Some(p), p.checked_add(1)])
133            .flatten()
134            .collect_vec();
135
136        for (&left, &right) in boundary_points.iter().cartesian_product(&boundary_points) {
137            test_rust_tasm_equivalence(left, right);
138        }
139    }
140
141    #[macro_rules_attr::apply(proptest)]
142    fn lt_u128_randomized_test_identical_args(v: u128) {
143        test_rust_tasm_equivalence(v, v);
144    }
145
146    #[macro_rules_attr::apply(proptest)]
147    fn lt_u128_randomized_test_identical_top_limbs(left: u128, right: u128) {
148        test_rust_tasm_equivalence(left, replace_bottom_n_bits::<32>(left, right));
149        test_rust_tasm_equivalence(left, replace_bottom_n_bits::<64>(left, right));
150        test_rust_tasm_equivalence(left, replace_bottom_n_bits::<96>(left, right));
151    }
152
153    /// Modify the first argument by replacing its least-significant 0 <= `N` < 128
154    /// bits with those of the second argument.
155    const fn replace_bottom_n_bits<const N: u8>(left: u128, right: u128) -> u128 {
156        let bottom_bits_mask = (1 << N) - 1;
157
158        ((left >> N) << N) | (right & bottom_bits_mask)
159    }
160
161    #[macro_rules_attr::apply(test)]
162    fn bit_replacement_works_as_expected() {
163        const fn abcd0xf<const N: u8>() -> u128 {
164            replace_bottom_n_bits::<N>(0xaaaa_aaaa_bbbb_bbbb_cccc_cccc_dddd_dddd, u128::MAX)
165        }
166
167        assert_eq!(0xaaaa_aaaa_bbbb_bbbb_cccc_cccc_dddd_dddd, abcd0xf::<0>());
168        assert_eq!(0xaaaa_aaaa_bbbb_bbbb_cccc_cccc_ffff_ffff, abcd0xf::<32>());
169        assert_eq!(0xaaaa_aaaa_bbbb_bbbb_ffff_ffff_ffff_ffff, abcd0xf::<64>());
170        assert_eq!(0xaaaa_aaaa_ffff_ffff_ffff_ffff_ffff_ffff, abcd0xf::<96>());
171        assert_eq!(0xffff_ffff_ffff_ffff_ffff_ffff_ffff_ffff, abcd0xf::<127>());
172    }
173}
174
175#[cfg(test)]
176mod benches {
177    use super::*;
178    use crate::test_prelude::*;
179
180    #[macro_rules_attr::apply(test)]
181    fn benchmark() {
182        ShadowedClosure::new(Lt).bench()
183    }
184}
tasm_lib/arithmetic/u128/lt.rs

tasm_lib/arithmetic/u128/
lt.rs
