tasm_lib/arithmetic/u64/
lt_preserve_args.rs

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

tasm_lib/arithmetic/u64/
lt_preserve_args.rs
