tasm_lib/arithmetic/u64/
decr.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/// [Decrement][dec] the given argument by 1.
10///
11/// ### Behavior
12///
13/// ```text
14/// BEFORE: _ [arg: u64]
15/// AFTER:  _ [arg-1: u64]
16/// ```
17///
18/// ### Preconditions
19///
20/// - the input `arg` is greater than 0
21/// - the input `arg` is properly [`BFieldCodec`] encoded
22///
23/// ### Postconditions
24///
25/// - the output is properly [`BFieldCodec`] encoded
26///
27/// [dec]: num::Integer::dec
28#[derive(Debug, Clone, Copy, Eq, PartialEq, Hash)]
29pub struct Decr;
30
31impl Decr {
32    pub const OVERFLOW_ERROR_ID: i128 = 110;
33}
34
35impl BasicSnippet for Decr {
36    fn parameters(&self) -> Vec<(DataType, String)> {
37        vec![(DataType::U64, "arg".to_string())]
38    }
39
40    fn return_values(&self) -> Vec<(DataType, String)> {
41        vec![(DataType::U64, "(arg-1)".to_string())]
42    }
43
44    fn entrypoint(&self) -> String {
45        "tasmlib_arithmetic_u64_decr".to_string()
46    }
47
48    fn code(&self, _: &mut Library) -> Vec<LabelledInstruction> {
49        let entrypoint = self.entrypoint();
50        let propagate_carry = format!("{entrypoint}_propagate_carry");
51
52        triton_asm!(
53            {entrypoint}:
54                addi -1
55                // _ arg_hi (arg_lo - 1)
56
57                dup 0
58                push -1
59                eq
60                skiz
61                    call {propagate_carry}
62                return
63
64            // BEFORE: _ arg_hi -1
65            // AFTER:  _ (arg_hi - 1) u32::MAX
66            {propagate_carry}:
67                add
68                // _ (arg_hi - 1)
69
70                dup 0
71                push -1
72                eq
73                // _ (arg_hi - 1) (arg_hi - 1 == -1)
74                // _ (arg_hi - 1) (arg_hi == 0)
75
76                push 0
77                eq
78                // _ (arg_hi - 1) (arg_hi != 0)
79
80                assert error_id {Self::OVERFLOW_ERROR_ID}
81
82                push {u32::MAX}
83                return
84        )
85    }
86
87    fn sign_offs(&self) -> HashMap<Reviewer, SignOffFingerprint> {
88        let mut sign_offs = HashMap::new();
89        sign_offs.insert(Reviewer("ferdinand"), 0xc5b5d50e60281819.into());
90        sign_offs
91    }
92}
93
94#[cfg(test)]
95mod tests {
96    use super::*;
97    use crate::test_prelude::*;
98
99    impl Closure for Decr {
100        type Args = u64;
101
102        fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) -> Result<(), RustShadowError> {
103            let arg = pop_encodable::<Self::Args>(stack)?;
104            let decremented = arg
105                .checked_sub(1)
106                .ok_or(RustShadowError::ArithmeticOverflow)?;
107            push_encodable(stack, &decremented);
108            Ok(())
109        }
110
111        fn pseudorandom_args(
112            &self,
113            seed: [u8; 32],
114            bench_case: Option<BenchmarkCase>,
115        ) -> Self::Args {
116            match bench_case {
117                Some(BenchmarkCase::CommonCase) => 7,
118                Some(BenchmarkCase::WorstCase) => 1 << 35,
119                None => StdRng::from_seed(seed).random_range(1..=u64::MAX),
120            }
121        }
122    }
123
124    #[macro_rules_attr::apply(test)]
125    fn rust_shadow() {
126        ShadowedClosure::new(Decr).test();
127    }
128
129    #[macro_rules_attr::apply(test)]
130    fn negative_test() {
131        test_assertion_failure(
132            &ShadowedClosure::new(Decr),
133            InitVmState::with_stack(Decr.set_up_test_stack(0)),
134            &[Decr::OVERFLOW_ERROR_ID],
135        );
136    }
137}
138
139#[cfg(test)]
140mod benches {
141    use super::*;
142    use crate::test_prelude::*;
143
144    #[macro_rules_attr::apply(test)]
145    fn benchmark() {
146        ShadowedClosure::new(Decr).bench();
147    }
148}
tasm_lib/arithmetic/u64/decr.rs

tasm_lib/arithmetic/u64/
decr.rs
