js_randomness_predictor/
safari_predictor.rs

1use 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()?; // if solving fails, error is returned early
15    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  // So consumers don't have to import the Predictor trait as well as the struct.
39  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  // Static 'helper' method
96  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  // Static 'helper' method
113  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}