js_randomness_predictor/
safari_predictor.rs1use crate::{Predictor, errors::InitError};
2use std::error::Error;
3use z3::{self, Config, Context, SatResult, Solver, ast::*};
4
5pub struct SafariPredictor {
6 sequence: Vec<f64>,
7 is_solved: bool,
8 conc_state_0: u64,
9 conc_state_1: u64,
10}
11
12impl Predictor for SafariPredictor {
13 fn predict_next(&mut self) -> Result<f64, Box<dyn Error>> {
14 self.solve_symbolic_state()?; let v = self.xor_shift_128_plus_concrete();
16 return Ok(self.to_double(v));
17 }
18}
19
20impl SafariPredictor {
21 const SS_0_STR: &str = "sym_state_0";
22 const SS_1_STR: &str = "sym_state_1";
23
24 pub fn new(seq: Vec<f64>) -> Self {
25 return SafariPredictor {
26 sequence: seq,
27 is_solved: false,
28 conc_state_0: 0,
29 conc_state_1: 0,
30 };
31 }
32
33 #[allow(dead_code)]
34 pub fn sequence(&self) -> &[f64] {
35 return &self.sequence;
36 }
37
38 pub fn predict_next(&mut self) -> Result<f64, Box<dyn Error>> {
40 return <Self as Predictor>::predict_next(self);
41 }
42
43 fn xor_shift_128_plus_concrete(&mut self) -> u64 {
44 let mut s1 = self.conc_state_0;
45 let s0 = self.conc_state_1;
46 self.conc_state_0 = s0;
47 s1 = s1 ^ s1 << 23;
48 self.conc_state_1 = s1 ^ s0 ^ (s1 >> 17) ^ (s0 >> 26);
49 return self.conc_state_1.wrapping_add(s0);
50 }
51
52 fn to_double(&self, value: u64) -> f64 {
53 return ((value & 0x1FFFFFFFFFFFFF) as f64) / ((1u64 << 53) as f64);
54 }
55
56 fn solve_symbolic_state(&mut self) -> Result<(), InitError> {
57 if self.is_solved {
58 return Ok(());
59 }
60
61 let config = Config::new();
62 let context = Context::new(&config);
63 let solver = Solver::new(&context);
64
65 let mut sym_state_0 = BV::new_const(&context, Self::SS_0_STR, 64);
66 let mut sym_state_1 = BV::new_const(&context, Self::SS_1_STR, 64);
67
68 for &observed in &self.sequence {
69 Self::xor_shift_128_plus_symbolic(&context, &mut sym_state_0, &mut sym_state_1);
70 Self::constrain_mantissa(observed, &context, &solver, &sym_state_0, &sym_state_1);
71 }
72
73 if solver.check() != SatResult::Sat {
74 return Err(InitError::Unsat);
75 }
76
77 let model = solver.get_model().ok_or(InitError::MissingModel)?;
78
79 self.conc_state_0 = model
80 .eval(&sym_state_0, true)
81 .ok_or(InitError::EvalFailed(Self::SS_0_STR))?
82 .as_u64()
83 .ok_or(InitError::ConvertFailed(Self::SS_0_STR))?;
84
85 self.conc_state_1 = model
86 .eval(&sym_state_1, true)
87 .ok_or(InitError::EvalFailed(Self::SS_1_STR))?
88 .as_u64()
89 .ok_or(InitError::ConvertFailed(Self::SS_1_STR))?;
90
91 self.is_solved = true;
92 return Ok(());
93 }
94
95 fn xor_shift_128_plus_symbolic<'a>(
97 context: &'a Context,
98 state_0: &mut BV<'a>,
99 state_1: &mut BV<'a>,
100 ) {
101 let state_0_shifted_left = state_0.bvshl(&BV::from_u64(context, 23, 64));
102 let mut s1 = &*state_0 ^ state_0_shifted_left;
103 let s1_shifted_right = s1.bvlshr(&BV::from_u64(context, 17, 64));
104
105 s1 ^= s1_shifted_right;
106 s1 ^= state_1.clone();
107 s1 ^= state_1.bvlshr(&BV::from_u64(context, 26, 64));
108 std::mem::swap(state_0, state_1);
109 *state_1 = s1;
110 }
111
112 fn constrain_mantissa(
114 value: f64,
115 context: &Context,
116 solver: &Solver,
117 state_0: &BV,
118 state_1: &BV,
119 ) {
120 let mantissa = (value * (1u64 << 53) as f64) as u64;
121 let symbolic_mask = &BV::from_u64(context, 0x1FFFFFFFFFFFFF, 64);
122 solver.assert(
123 &BV::from_u64(context, mantissa, 64)._eq(&state_0.bvadd(state_1).bvand(symbolic_mask)),
124 );
125 }
126}
127
128#[cfg(test)]
129mod tests {
130 use std::error::Error;
131
132 #[test]
133 fn correctly_predicts_sequence() -> Result<(), Box<dyn Error>> {
134 let sequence = vec![
135 0.8651485656540925,
136 0.11315724215685208,
137 0.3153950773233716,
138 0.45825597860463274,
139 ];
140 let expected = vec![
141 0.31143815234233363,
142 0.6973996606199063,
143 0.2146174701215342,
144 0.098415677735185,
145 0.6908723218385805,
146 0.43568239375320583,
147 0.5537079837658566,
148 0.9190574467880481,
149 0.14789834036423333,
150 0.8477134504145751,
151 0.8636173753361875,
152 0.921914547452633,
153 0.4377690900199249,
154 0.759557924932666,
155 0.5003933241991145,
156 0.0589099881389864,
157 ];
158
159 let mut ffp = crate::SafariPredictor::new(sequence);
160 let mut predictions = vec![];
161
162 for _ in 0..expected.len() {
163 let prediction = ffp.predict_next()?;
164 predictions.push(prediction);
165 }
166
167 assert_eq!(predictions, expected);
168 return Ok(());
169 }
170}