Skip to content

Commit e3c6394

Browse files
committed
feat(i128): Add lt for i128
Also adds variant `I128` to `DataType`.
1 parent bb67184 commit e3c6394

File tree

6 files changed

+348
-0
lines changed

6 files changed

+348
-0
lines changed
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
[
2+
{
3+
"name": "tasmlib_arithmetic_i128_lt",
4+
"benchmark_result": {
5+
"clock_cycle_count": 55,
6+
"hash_table_height": 48,
7+
"u32_table_height": 198,
8+
"op_stack_table_height": 27,
9+
"ram_table_height": 0
10+
},
11+
"case": "CommonCase"
12+
},
13+
{
14+
"name": "tasmlib_arithmetic_i128_lt",
15+
"benchmark_result": {
16+
"clock_cycle_count": 55,
17+
"hash_table_height": 48,
18+
"u32_table_height": 198,
19+
"op_stack_table_height": 27,
20+
"ram_table_height": 0
21+
},
22+
"case": "WorstCase"
23+
}
24+
]

tasm-lib/src/arithmetic.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
pub mod bfe;
2+
pub mod i128;
23
pub mod u128;
34
pub mod u32;
45
pub mod u64;

tasm-lib/src/arithmetic/i128.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
pub mod lt;

tasm-lib/src/arithmetic/i128/lt.rs

Lines changed: 251 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,251 @@
1+
use triton_vm::isa::triton_asm;
2+
use triton_vm::prelude::LabelledInstruction;
3+
4+
use crate::arithmetic;
5+
use crate::data_type::DataType;
6+
use crate::library::Library;
7+
use crate::prelude::BasicSnippet;
8+
9+
/// Less-than operator for `i128`
10+
///
11+
/// # Behavior
12+
///
13+
/// BEFORE: `_ [rhs: i128] [lhs: i128]`
14+
///
15+
/// AFTER: `_ (lhs < rhs)`
16+
///
17+
/// # Preconditions
18+
///
19+
/// - `rhs` and `lhs` consists of 4 `u32`s.
20+
///
21+
/// # Postconditions
22+
///
23+
/// - `result = lhs < rhs` is `true` or `false`.
24+
///
25+
/// # Panics
26+
///
27+
/// - If preconditions are not met.
28+
pub struct Lt;
29+
30+
impl BasicSnippet for Lt {
31+
fn inputs(&self) -> Vec<(DataType, String)> {
32+
["rhs", "lhs"]
33+
.map(|s| (DataType::I128, s.to_string()))
34+
.to_vec()
35+
}
36+
37+
fn outputs(&self) -> Vec<(DataType, String)> {
38+
vec![(DataType::Bool, "result".to_string())]
39+
}
40+
41+
fn entrypoint(&self) -> String {
42+
"tasmlib_arithmetic_i128_lt".to_owned()
43+
}
44+
45+
fn code(&self, library: &mut Library) -> Vec<LabelledInstruction> {
46+
let entrypoint = self.entrypoint();
47+
let u128_lt = library.import(Box::new(arithmetic::u128::lt_u128::LtU128));
48+
49+
const TWO_POW_31: u32 = 1 << 31;
50+
let flip_msbs = triton_asm!(
51+
// _ [rhs: i128] [lhs: i128]
52+
swap 3
53+
push {TWO_POW_31}
54+
xor
55+
swap 3
56+
57+
swap 7
58+
push {TWO_POW_31}
59+
xor
60+
swap 7
61+
// _ [rhs+(1<<127): u128] [rhs+(1<<127): u128]
62+
);
63+
64+
triton_asm!(
65+
{entrypoint}:
66+
// _ [rhs] [lhs]
67+
68+
/* Flip most-significant bit, then do u128-lt. */
69+
70+
{&flip_msbs}
71+
// _ [rhs'] [lhs']
72+
73+
call {u128_lt}
74+
// _ (rhs > lhs)
75+
76+
return
77+
)
78+
}
79+
}
80+
81+
#[cfg(test)]
82+
mod tests {
83+
use itertools::Itertools;
84+
use proptest_arbitrary_interop::arb;
85+
use rand::random;
86+
use rand::rngs::StdRng;
87+
use rand::Rng;
88+
use rand::SeedableRng;
89+
use test_strategy::proptest;
90+
use triton_vm::error::InstructionError;
91+
use triton_vm::error::OpStackError;
92+
use triton_vm::prelude::bfe;
93+
use triton_vm::prelude::BFieldElement;
94+
use triton_vm::vm::NonDeterminism;
95+
96+
use super::*;
97+
use crate::push_encodable;
98+
use crate::snippet_bencher::BenchmarkCase;
99+
use crate::test_helpers::negative_test;
100+
use crate::test_helpers::test_rust_equivalence_given_complete_state;
101+
use crate::traits::closure::Closure;
102+
use crate::traits::closure::ShadowedClosure;
103+
use crate::traits::rust_shadow::RustShadow;
104+
use crate::InitVmState;
105+
106+
#[test]
107+
fn i128_lt_proptest() {
108+
ShadowedClosure::new(Lt).test();
109+
}
110+
111+
#[proptest]
112+
fn input_not_u32_words_negative_test(
113+
#[strategy(0usize..8)] stack_index_bad_word: usize,
114+
#[strategy(arb())]
115+
#[filter(#bad_word.value() > u32::MAX as u64)]
116+
bad_word: BFieldElement,
117+
) {
118+
fn init_state_not_u32_words(
119+
stack_index_bad_word: usize,
120+
bad_word: BFieldElement,
121+
) -> InitVmState {
122+
let mut stack = Lt.init_state(random(), random());
123+
let last_elem_index = stack.len() - 1;
124+
stack[last_elem_index - stack_index_bad_word] = bad_word;
125+
126+
InitVmState::with_stack(stack)
127+
}
128+
129+
negative_test(
130+
&ShadowedClosure::new(Lt),
131+
init_state_not_u32_words(stack_index_bad_word, bad_word),
132+
&[InstructionError::OpStackError(
133+
OpStackError::FailedU32Conversion(bad_word),
134+
)],
135+
);
136+
}
137+
138+
#[test]
139+
fn i128_lt_unit_test_min_max() {
140+
let init_stack = Lt.init_state(i128::MIN, i128::MAX);
141+
let mut expected_end_stack = Lt.init_stack_for_isolated_run();
142+
expected_end_stack.push(bfe!(true as u64));
143+
144+
let stdin = &[];
145+
test_rust_equivalence_given_complete_state(
146+
&ShadowedClosure::new(Lt),
147+
&init_stack,
148+
stdin,
149+
&NonDeterminism::default(),
150+
&None,
151+
Some(&expected_end_stack),
152+
);
153+
}
154+
155+
#[test]
156+
fn i128_lt_unit_test_zero_zero() {
157+
let init_stack = Lt.init_state(0, 0);
158+
let mut expected_end_stack = Lt.init_stack_for_isolated_run();
159+
expected_end_stack.push(bfe!(false as u64));
160+
161+
let stdin = &[];
162+
test_rust_equivalence_given_complete_state(
163+
&ShadowedClosure::new(Lt),
164+
&init_stack,
165+
stdin,
166+
&NonDeterminism::default(),
167+
&None,
168+
Some(&expected_end_stack),
169+
);
170+
}
171+
172+
impl Lt {
173+
fn init_state(&self, lhs: i128, rhs: i128) -> Vec<BFieldElement> {
174+
let mut stack = self.init_stack_for_isolated_run();
175+
push_encodable(&mut stack, &(rhs as u128));
176+
push_encodable(&mut stack, &(lhs as u128));
177+
178+
stack
179+
}
180+
}
181+
182+
impl Closure for Lt {
183+
fn rust_shadow(&self, stack: &mut Vec<BFieldElement>) {
184+
fn pop_i128(stack: &mut Vec<BFieldElement>) -> i128 {
185+
let num_limbs = 4;
186+
let limbs: Vec<u32> = (0..num_limbs)
187+
.map(|_| stack.pop().unwrap().try_into().unwrap())
188+
.collect_vec();
189+
190+
let mut acc = ((limbs[3] as i32) as i128) << 96;
191+
for (i, limb) in limbs[0..3].iter().enumerate() {
192+
acc += (*limb as i128) << (i * 32);
193+
}
194+
195+
acc
196+
}
197+
let lhs = pop_i128(stack);
198+
let rhs = pop_i128(stack);
199+
200+
stack.push(bfe!((lhs < rhs) as u64));
201+
}
202+
203+
fn pseudorandom_initial_state(
204+
&self,
205+
seed: [u8; 32],
206+
_bench_case: Option<BenchmarkCase>,
207+
) -> Vec<BFieldElement> {
208+
let mut rng = StdRng::from_seed(seed);
209+
self.init_state(rng.gen(), rng.gen())
210+
}
211+
212+
fn corner_case_initial_states(&self) -> Vec<Vec<BFieldElement>> {
213+
let points_with_plus_minus_one = [
214+
i128::MIN,
215+
-(1 << 96),
216+
-(1 << 64),
217+
-(1 << 32),
218+
-1,
219+
0,
220+
1,
221+
1 << 32,
222+
1 << 64,
223+
1 << 96,
224+
1 << 126,
225+
i128::MAX,
226+
]
227+
.into_iter()
228+
.flat_map(|p| [p.checked_sub(1), Some(p), p.checked_add(1)])
229+
.flatten()
230+
.collect_vec();
231+
232+
points_with_plus_minus_one
233+
.iter()
234+
.cartesian_product(&points_with_plus_minus_one)
235+
.map(|(&l, &r)| self.init_state(l, r))
236+
.collect()
237+
}
238+
}
239+
}
240+
241+
#[cfg(test)]
242+
mod benches {
243+
use super::*;
244+
use crate::traits::closure::ShadowedClosure;
245+
use crate::traits::rust_shadow::RustShadow;
246+
247+
#[test]
248+
fn lt_i128_benchmark() {
249+
ShadowedClosure::new(Lt).bench();
250+
}
251+
}

0 commit comments

Comments
 (0)