libgdx_xs128/
lib.rs

1#![no_std]
2pub mod new_rng;
3pub mod old_rng;
4pub use old_rng as rng;
5
6#[derive(Debug)]
7pub enum SeedInitializer {
8    SeedPair(u64, u64),
9    Seed(u64),
10    Seed0(u64),
11    Seed1(u64),
12}
13
14impl From<i64> for SeedInitializer {
15    fn from(seed: i64) -> Self {
16        Self::Seed(seed as u64)
17    }
18}
19
20impl From<(u64, u64)> for SeedInitializer {
21    fn from((seed0, seed1): (u64, u64)) -> Self {
22        Self::SeedPair(seed0, seed1)
23    }
24}
25
26pub const MH3_FACTOR_1: u64 = 0xff51afd7ed558ccd;
27pub const MH3_FACTOR_2: u64 = 0xc4ceb9fe1a85ec53;
28
29pub const INV_MH3_FACTOR_1: u64 = 0x9cb4b2f8129337db;
30pub const INV_MH3_FACTOR_2: u64 = 0x4f74430c22a54005;
31
32pub trait RandomXS128: 
33    From<SeedInitializer>
34{
35    fn new(seed: u64) -> Self;
36    fn next_u64(&mut self) -> u64;
37    fn advance(&mut self, n: u32) {
38        (0..n).for_each(|_| { let _ = self.next_u64(); })
39    }
40
41    fn next_capped_u64(&mut self, modulus: u64) -> u64 {
42        loop {
43            let (residue, overflowed) = 
44                self.overflowing_next_capped_u64(modulus);
45            #[cfg(feature = "reroll")]
46            if overflowed {
47                continue;
48            }
49            return residue;
50        }
51    }
52
53    fn unchecked_next_capped_u64(&mut self, modulus: u64) -> u64 {
54        self.overflowing_next_capped_u64(modulus).0
55    }
56
57    fn overflowing_next_capped_u64(&mut self, modulus: u64) -> (u64, bool);
58}
59
60#[cfg(test)]
61mod unit_tests {
62    enum RngValue {
63        U64(u64),
64        CappedU64 { modulus: u64, residue: u64 },
65        Advance(u32),
66    }
67
68    struct RngValues {
69        seed: u64,
70        values: [Option<RngValue>; 16],
71    }
72
73    use crate::{new_rng, old_rng, RandomXS128};
74
75    const VALUE_LISTS: [RngValues; 7] = [
76        RngValues {
77            seed: 12345i64 as u64,
78            values: [ Some(RngValue::U64(1382432690769144372i64 as u64)), Some(RngValue::Advance(10)), Some(RngValue::CappedU64 { modulus: 134, residue: 83, }), Some(RngValue::U64(-5355119237153046436i64 as u64)), None, None, None, None, None, None, None, None, None, None, None, None, ],
79        },
80        RngValues {
81            seed: 42i64 as u64,
82            values: [ Some(RngValue::CappedU64 { modulus: 1, residue: 0, }), Some(RngValue::CappedU64 { modulus: 2, residue: 1, }), Some(RngValue::CappedU64 { modulus: 3, residue: 0, }), Some(RngValue::CappedU64 { modulus: 4, residue: 0, }), Some(RngValue::CappedU64 { modulus: 5, residue: 1, }), Some(RngValue::CappedU64 { modulus: 6, residue: 5, }), Some(RngValue::CappedU64 { modulus: 7, residue: 5, }), Some(RngValue::CappedU64 { modulus: 8, residue: 3, }), Some(RngValue::CappedU64 { modulus: 9, residue: 7, }), Some(RngValue::CappedU64 { modulus: 10, residue: 7, }), Some(RngValue::CappedU64 { modulus: 11, residue: 9, }), Some(RngValue::CappedU64 { modulus: 12, residue: 9, }), Some(RngValue::CappedU64 { modulus: 13, residue: 4, }), Some(RngValue::CappedU64 { modulus: 14, residue: 13, }), Some(RngValue::CappedU64 { modulus: 15, residue: 3, }), Some(RngValue::CappedU64 { modulus: 16, residue: 6, }), ],
83        },
84        RngValues {
85            seed: -10i64 as u64,
86            values: [ Some(RngValue::CappedU64 { modulus: 5, residue: 3, }), Some(RngValue::CappedU64 { modulus: 2, residue: 0, }), Some(RngValue::CappedU64 { modulus: 9, residue: 7, }), Some(RngValue::Advance(1)), Some(RngValue::U64(-1057127458437580682i64 as u64)), Some(RngValue::CappedU64 { modulus: 7, residue: 6, }), Some(RngValue::CappedU64 { modulus: 13, residue: 3, }), Some(RngValue::CappedU64 { modulus: 8, residue: 0, }), Some(RngValue::CappedU64 { modulus: 6, residue: 0, }), Some(RngValue::CappedU64 { modulus: 4, residue: 0, }), Some(RngValue::CappedU64 { modulus: 3, residue: 1, }), Some(RngValue::CappedU64 { modulus: 11, residue: 3, }), Some(RngValue::CappedU64 { modulus: 16, residue: 7, }), Some(RngValue::CappedU64 { modulus: 12, residue: 7, }), Some(RngValue::CappedU64 { modulus: 15, residue: 8, }), None, ],
87        },
88        RngValues {
89            seed: 1000i64 as u64,
90            values: [ Some(RngValue::Advance(2)), Some(RngValue::Advance(3)), Some(RngValue::Advance(4)), Some(RngValue::CappedU64 { modulus: 1, residue: 0, }), Some(RngValue::CappedU64 { modulus: 999, residue: 913, }), Some(RngValue::CappedU64 { modulus: 555, residue: 61, }), Some(RngValue::CappedU64 { modulus: 100, residue: 79, }), Some(RngValue::Advance(5)), Some(RngValue::CappedU64 { modulus: 777, residue: 616, }), Some(RngValue::Advance(6)), Some(RngValue::CappedU64 { modulus: 123, residue: 23, }), Some(RngValue::Advance(7)), Some(RngValue::CappedU64 { modulus: 9999, residue: 7303, }), Some(RngValue::CappedU64 { modulus: 888, residue: 133, }), Some(RngValue::CappedU64 { modulus: 444, residue: 167, }), None, ],
91        },
92        RngValues {
93            seed: 1234567890i64 as u64,
94            values: [ Some(RngValue::CappedU64 { modulus: 5, residue: 3, }), Some(RngValue::CappedU64 { modulus: 10, residue: 5, }), Some(RngValue::CappedU64 { modulus: 15, residue: 4, }), Some(RngValue::CappedU64 { modulus: 20, residue: 13, }), Some(RngValue::CappedU64 { modulus: 25, residue: 1, }), Some(RngValue::CappedU64 { modulus: 30, residue: 10, }), Some(RngValue::CappedU64 { modulus: 35, residue: 5, }), Some(RngValue::CappedU64 { modulus: 40, residue: 1, }), Some(RngValue::CappedU64 { modulus: 45, residue: 41, }), Some(RngValue::CappedU64 { modulus: 50, residue: 14, }), Some(RngValue::CappedU64 { modulus: 55, residue: 35, }), Some(RngValue::CappedU64 { modulus: 60, residue: 40, }), Some(RngValue::CappedU64 { modulus: 65, residue: 11, }), Some(RngValue::CappedU64 { modulus: 70, residue: 22, }), Some(RngValue::CappedU64 { modulus: 75, residue: 40, }), Some(RngValue::CappedU64 { modulus: 80, residue: 5, }), ],
95        },
96        RngValues {
97            seed: -9876543210i64 as u64,
98            values: [ Some(RngValue::Advance(3)), Some(RngValue::CappedU64 { modulus: 42, residue: 25, }), Some(RngValue::Advance(6)), Some(RngValue::Advance(9)), Some(RngValue::CappedU64 { modulus: 99999999999999, residue: 21627940712847, }), Some(RngValue::CappedU64 { modulus: 77777777777777, residue: 75498257424579, }), Some(RngValue::CappedU64 { modulus: 88888888888888, residue: 14384965901149, }), Some(RngValue::CappedU64 { modulus: 1234567890, residue: 975571841, }), Some(RngValue::Advance(5)), Some(RngValue::CappedU64 { modulus: 55555555555555, residue: 29505003891522, }), Some(RngValue::CappedU64 { modulus: 10000000000000, residue: 551591108261, }), Some(RngValue::CappedU64 { modulus: 123, residue: 15, }), Some(RngValue::Advance(4)), Some(RngValue::CappedU64 { modulus: 99999999999, residue: 52894208431, }), Some(RngValue::Advance(1)), None, ],
99        },
100        RngValues {
101            seed: 9223372036854775807i64 as u64,
102            values: [ Some(RngValue::CappedU64 { modulus: 100, residue: 58, }), Some(RngValue::CappedU64 { modulus: 200, residue: 87, }), Some(RngValue::CappedU64 { modulus: 300, residue: 297, }), Some(RngValue::CappedU64 { modulus: 400, residue: 281, }), Some(RngValue::CappedU64 { modulus: 500, residue: 321, }), Some(RngValue::CappedU64 { modulus: 600, residue: 304, }), Some(RngValue::CappedU64 { modulus: 700, residue: 649, }), Some(RngValue::CappedU64 { modulus: 800, residue: 574, }), Some(RngValue::CappedU64 { modulus: 900, residue: 775, }), Some(RngValue::CappedU64 { modulus: 1000, residue: 373, }), Some(RngValue::CappedU64 { modulus: 1100, residue: 465, }), Some(RngValue::CappedU64 { modulus: 1200, residue: 980, }), Some(RngValue::CappedU64 { modulus: 1300, residue: 234, }), Some(RngValue::CappedU64 { modulus: 1400, residue: 917, }), Some(RngValue::CappedU64 { modulus: 1500, residue: 1185, }), None, ],
103        },
104    ];
105
106    #[test]
107    fn old_rng_vs_java_rng() {
108        for RngValues { seed, values } in VALUE_LISTS {
109            let mut rng = old_rng::Random::new(seed);
110            for value in values {
111                match value {
112                    Some(RngValue::U64(n)) =>
113                        assert_eq!(rng.next_u64(), n),
114                    Some(RngValue::CappedU64 { modulus, residue }) =>
115                        assert_eq!(rng.next_capped_u64(modulus), residue),
116                    Some(RngValue::Advance(k)) =>
117                        rng.advance(k),
118                    None => {}
119                }
120            }
121        }
122    }
123
124    #[test]
125    fn new_rng_vs_java_rng() {
126        for RngValues { seed, values } in VALUE_LISTS {
127            let mut rng = new_rng::Random::new(seed);
128            for value in values {
129                match value {
130                    Some(RngValue::U64(n)) => {
131                        assert_eq!(rng.next_u64(), n)
132                    }
133                    Some(RngValue::CappedU64 { modulus, residue }) => {
134                        assert_eq!(rng.next_capped_u64(modulus), residue)
135                    }
136                    Some(RngValue::Advance(k)) => (0..k).for_each(|_| {
137                        let _ = rng.next_u64();
138                    }),
139                    None => {}
140                }
141            }
142        }
143    }
144}
145
146#[cfg(kani)]
147mod verification {
148    
149    use crate::old_rng::Random as OldRandom;
150    use crate::new_rng::Random as NewRandom;
151    use super::*;
152
153    #[kani::proof]
154    fn next_u64() {
155        let seed0 = kani::any();
156        let seed1 = kani::any();
157        let mut old_rng: OldRandom = (seed0, seed1).into();
158        let mut new_rng: NewRandom = (seed0, seed1).into();
159        
160        assert!(
161            old_rng.next_u64() ==
162            new_rng.next_u64()
163        );
164    }
165
166    #[kani::proof]
167    fn overflowing_next_capped_u64() {
168        let seed0 = kani::any();
169        let seed1 = kani::any();
170        let modulus: u64 = kani::any();
171
172
173        kani::assume(
174            modulus.is_power_of_two() ||
175            [3, 5, 6, 7].contains(&modulus)
176        );
177
178        let mut old_rng: OldRandom = (seed0, seed1).into();
179        let mut new_rng: NewRandom = (seed0, seed1).into();
180        
181        assert!(
182            old_rng.overflowing_next_capped_u64(modulus) ==
183            new_rng.overflowing_next_capped_u64(modulus)
184        );
185    }
186
187    #[kani::proof]
188    fn unchecked_next_capped_u64() {
189        let seed0 = kani::any();
190        let seed1 = kani::any();
191        let modulus: u64 = kani::any();
192
193
194        kani::assume(
195            modulus.is_power_of_two()
196            // || [3, 5, 6, 7].contains(&modulus)
197        );
198
199        let mut old_rng: OldRandom = (seed0, seed1).into();
200        let mut new_rng: NewRandom = (seed0, seed1).into();
201        
202        assert!(
203            old_rng.unchecked_next_capped_u64(modulus) ==
204            new_rng.unchecked_next_capped_u64(modulus)
205        );
206    }
207
208    #[kani::proof]
209    fn wrapping_xor_shr33() {
210        let seed0 = kani::any();
211        
212        let old_shr33: u64 = seed0 ^ seed0 >> 33;
213        let new_shr33: u64 = new_rng::Random
214            ::wrapping_xor_shr33(seed0);
215        assert!(
216            old_shr33 ==
217            new_shr33
218        );
219    }
220
221    const FACTORS: [u64; 4] = [
222        MH3_FACTOR_1,
223        MH3_FACTOR_2,
224        INV_MH3_FACTOR_1,
225        INV_MH3_FACTOR_2
226    ];
227    
228    const SHIFTS: [u32; 8] = [0, 8, 16, 24, 32, 40, 48, 56];
229    
230    fn wrapping_mul
231    <const FACTOR: u64, const SHIFT: u32>
232    (seed0: u64) {
233        let old_mul: u64 = seed0.wrapping_mul(FACTOR);
234        let new_mul: u64 = new_rng::Random
235            ::wrapping_const_mul::<FACTOR>(seed0);
236        assert!(
237            old_mul.wrapping_shr(SHIFT) as u8 ==
238            new_mul.wrapping_shr(SHIFT) as u8
239        );
240    }
241    
242    #[kani::proof]
243    fn wrapping_mul_0_0() {
244        let seed0 = kani::any();
245        wrapping_mul::<{FACTORS[0]}, {SHIFTS[0]}>(seed0);
246    }
247
248    #[kani::proof]
249    fn wrapping_mul_0_1() {
250        let seed0 = kani::any();
251        wrapping_mul::<{FACTORS[0]}, {SHIFTS[1]}>(seed0);
252    }
253
254    // #[kani::proof]
255    // fn wrapping_mul_0_2() {
256    //     let seed0 = kani::any();
257    //     wrapping_mul::<{FACTORS[0]}, {SHIFTS[2]}>(seed0);
258    // }
259
260    // #[kani::proof]
261    // fn wrapping_mul_0_3() {
262    //     let seed0 = kani::any();
263    //     wrapping_mul::<{FACTORS[0]}, {SHIFTS[3]}>(seed0);
264    // }
265}
libgdx_xs128/lib.rs

libgdx_xs128/
lib.rs
