1use crate::{Predictor, errors::InitError};
2use std::error::Error;
3use z3::{self, Config, Context, SatResult, Solver, ast::*};
4
5pub struct FirefoxPredictor {
6 sequence: Vec<f64>,
7 is_solved: bool,
8 conc_state_0: u64,
9 conc_state_1: u64,
10}
11
12impl Predictor for FirefoxPredictor {
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 FirefoxPredictor {
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 FirefoxPredictor {
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 sum = state_0.bvadd(state_1);
121 let symbolic_mask = BV::from_u64(context, 0x1FFFFFFFFFFFFF, 64);
122 let masked = sum.bvand(&symbolic_mask);
123 let mantissa = (value * (1u64 << 53) as f64) as u64;
124 let constraint = BV::from_u64(context, mantissa, 64)._eq(&masked).simplify();
125 solver.assert(&constraint);
126 }
127}
128
129#[cfg(test)]
130mod tests {
131 use std::error::Error;
132
133 #[test]
134 fn correctly_predicts_sequence() -> Result<(), Box<dyn Error>> {
135 let pool = vec![
136 0.5865531271930553,
137 0.5541046114391099,
138 0.21640895758393563,
139 0.7795614489825657,
140 0.45436917267245447,
141 0.23093540482617203,
142 0.38347603573221434,
143 0.5711709968714335,
144 0.30456387778967864,
145 0.8339269908305158,
146 0.452233580000003,
147 0.9901079314416401,
148 0.32987341924464075,
149 0.8988042405156045,
150 0.49552711891551626,
151 0.15029415930638967,
152 0.3937939136620475,
153 0.5314000592309004,
154 0.4137690151782778,
155 0.6762320890566726,
156 0.30490045333928995,
157 0.7093972241287271,
158 0.02546662110698006,
159 0.07499228034961558,
160 0.5360209481813598,
161 0.6698034264516716,
162 0.6193136766571286,
163 0.3303181016773604,
164 0.9518393946238296,
165 0.4487411266188046,
166 0.8007864085923057,
167 0.8146967187664399,
168 0.2901950937777532,
169 0.8953227326794915,
170 0.7361031066039209,
171 0.8987370273886456,
172 0.951031741251198,
173 0.4091339852815272,
174 0.9240165078425672,
175 0.8962808277375502,
176 0.11925094767049316,
177 0.6784859133555188,
178 0.07052010777228157,
179 0.7577282490015692,
180 0.22553130378286845,
181 0.2079625910699775,
182 0.2474793037417129,
183 0.8847355072588861,
184 0.009203220460777595,
185 0.7314825091606534,
186 0.9880363507547771,
187 0.2160974225822464,
188 0.6043743685351406,
189 0.9489747685109242,
190 0.5713408814075374,
191 0.9603730950150634,
192 0.5758706386904255,
193 0.07152684677986532,
194 0.5826674142710256,
195 0.20043688560962214,
196 0.09558968499870024,
197 0.25048591978527535,
198 0.7604745383338725,
199 0.8247513469575583,
200 0.6719489484014812,
201 0.6031207514397643,
202 0.2786151887322349,
203 0.11696233599010553,
204 0.9933163541971937,
205 0.6802048660091916,
206 0.164275982818593,
207 0.5098106908762376,
208 0.5251171753643626,
209 0.03511608122166543,
210 0.4080893060593229,
211 0.5753844387901543,
212 0.9437270993335143,
213 0.8712404063281237,
214 0.23884610934192596,
215 0.6287422235560856,
216 0.7682443480617352,
217 0.5557721036062607,
218 0.9685451347878308,
219 0.10263154582984746,
220 0.6000622095511561,
221 0.18652287567130887,
222 0.9290955404868614,
223 0.48073869875383335,
224 0.33628038907760527,
225 0.34021009749599807,
226 0.6478493707667935,
227 0.9834206056552957,
228 0.9954612050315345,
229 0.9613325220552444,
230 0.05334644695656576,
231 0.7839164925066305,
232 0.1723615567246204,
233 0.2546300256299039,
234 0.547551699464579,
235 0.7683498298049048,
236 0.6768919225469846,
237 0.5698840546440623,
238 0.8949865873521787,
239 0.2762337213638124,
240 0.2914971720512356,
241 0.667169971951049,
242 0.8788794238635516,
243 0.6056983582513188,
244 0.6978906292691608,
245 0.5084096818222084,
246 0.896188269616582,
247 0.8667876764604892,
248 0.19374598159155731,
249 0.4015724745166128,
250 0.31064329125730183,
251 0.9766275380602045,
252 0.8636977734026434,
253 0.4627411206679235,
254 0.561342325207,
255 0.22634904452671867,
256 0.37478402343588846,
257 0.7542758614904915,
258 0.6175364395459599,
259 0.3262852870701207,
260 0.8455197347573297,
261 0.9026190475484023,
262 0.6572894771664558,
263 0.6519086252140869,
264 0.30394338002136867,
265 0.7953303525841622,
266 0.6099029781271542,
267 0.26154318340801785,
268 0.6477675585737454,
269 0.6333782961115457,
270 0.1147088586664452,
271 0.21711127276046538,
272 0.26381584187088747,
273 0.7779240693517507,
274 0.3949347796416661,
275 0.557392304456174,
276 0.24353754703634467,
277 0.10435870903782773,
278 0.7774359221094169,
279 0.5011771001631059,
280 0.5359871744048943,
281 0.7543614234687356,
282 0.9018737462536165,
283 0.4256864139358444,
284 0.8459955606418031,
285 0.10187774474362776,
286 0.1322684500759459,
287 0.5683879339873796,
288 0.6418933999287194,
289 0.5180525345593695,
290 0.7398367852748235,
291 0.04506771148068134,
292 0.4040576526684111,
293 0.18468061507380096,
294 0.037779351685426454,
295 0.6347553707870932,
296 0.6792680290384384,
297 0.9731452716762597,
298 0.13864544178261173,
299 0.44213204597638234,
300 0.05975339784642919,
301 0.3380990206481682,
302 0.8687528558588666,
303 0.3741966792162065,
304 0.3597005796257373,
305 0.24972730955563194,
306 0.5396372344236281,
307 0.8003837342188123,
308 0.046792261641357746,
309 0.6948558885780519,
310 0.5815282975242501,
311 0.03158783480423033,
312 0.509867965086224,
313 0.5013656808194861,
314 0.5170834567632665,
315 0.8065444903386002,
316 0.7149598980173147,
317 0.34795569026047934,
318 0.33346333827030905,
319 0.8654948191105245,
320 0.24858241341438558,
321 0.12499803130944798,
322 0.210187765926808,
323 0.5617854328417712,
324 0.20412667813533958,
325 0.17872530426902922,
326 0.6554357665881997,
327 0.9724241011261335,
328 0.5423339454032328,
329 0.9079531006399448,
330 0.23952948581936262,
331 0.1875316127702139,
332 0.09697212594220317,
333 0.4708546636057608,
334 0.1524712450883936,
335 0.9070177617745666,
336 0.2557818955520905,
337 0.9166976165011695,
338 0.5944883555486884,
339 0.1587066693875202,
340 0.8541866326211491,
341 0.7245429295344993,
342 0.6886648121137378,
343 0.5929719106002956,
344 0.048398594104920645,
345 0.2877472889758885,
346 0.016429619433395493,
347 0.9482466638914043,
348 0.2966126049849438,
349 0.7428905512659318,
350 0.6273898872583024,
351 0.028099004230893065,
352 0.5774276166088086,
353 0.0800631334684968,
354 0.416018164166542,
355 0.08341006005719065,
356 0.43775565063572475,
357 0.5560849832857038,
358 0.6782857389644982,
359 0.06700454961827529,
360 0.22691174275649384,
361 0.8242450813155278,
362 0.29359123199020254,
363 0.997876090157192,
364 0.9493194126525922,
365 0.5900824457187492,
366 0.06298205353343977,
367 0.40358747854012833,
368 0.024146984264696858,
369 0.46015126057899836,
370 0.013991861862566513,
371 0.04704405615743401,
372 0.7851424860050942,
373 0.6651216343677179,
374 0.41931677510055043,
375 0.9146820338235684,
376 0.5869038070766122,
377 0.6340174106887423,
378 0.08400704658818536,
379 0.9864832639510085,
380 0.7151943759081495,
381 0.3853535252534469,
382 0.8696424871102053,
383 0.0673843955522534,
384 0.6239261009143927,
385 0.27365977073754477,
386 0.13211693865059848,
387 0.5688186108785191,
388 0.22940558182062598,
389 0.016169246164127404,
390 0.28470411575884724,
391 0.22720230375819672,
392 0.7225913099403145,
393 0.4259240909387264,
394 0.4461122206756156,
395 0.7474974204062478,
396 0.7659535586398175,
397 0.7168309872396994,
398 0.317293501331555,
399 0.81877150183118,
400 0.3120769303620744,
401 0.5804152015359736,
402 0.3040343619096133,
403 0.5816624465829855,
404 0.11994238443478811,
405 0.2815982796617005,
406 0.8234637990003068,
407 0.08392555545333702,
408 0.2614829907916557,
409 0.6437451060548047,
410 0.5629730762143647,
411 0.29931502438216795,
412 0.1595895651244934,
413 0.016918360912327124,
414 0.5798570627209118,
415 0.9758857221663496,
416 0.8750217802925053,
417 0.11110205308361909,
418 0.8104141136207583,
419 0.2723349439887208,
420 0.6461947788053617,
421 0.023351750222622036,
422 0.6972976116325138,
423 0.34423643145908955,
424 0.9368239911656492,
425 0.10815197944907251,
426 0.9589601798871525,
427 0.4143780833046157,
428 0.4650665362303995,
429 0.3657721527118005,
430 0.7841264681613905,
431 0.08672269562398693,
432 0.7355537227494491,
433 0.9272620235009659,
434 0.46902105162810703,
435 0.9204116180489463,
436 0.18522915389671835,
437 0.009607131558745818,
438 0.08405745608652804,
439 0.5284791325060331,
440 0.36757385936490594,
441 0.06898334407643647,
442 0.6909212815973119,
443 0.7679142424007818,
444 0.37610910303112965,
445 0.05208122260543557,
446 0.7800602608702812,
447 0.7592772264352324,
448 0.7328522162362429,
449 0.9917619102753855,
450 0.3145759590812792,
451 0.17520545738747595,
452 0.3279156985731282,
453 0.04472917454345138,
454 0.970756871443966,
455 0.4066193447288844,
456 0.2610986600840106,
457 0.15813875972457836,
458 0.20999876205937806,
459 0.10994646062452096,
460 0.6915366893751249,
461 0.8466796288317558,
462 0.4767129172207717,
463 0.12772079214030696,
464 0.3466170672147567,
465 0.42317599968776043,
466 0.1622062612512022,
467 0.2230515025459333,
468 0.8107333118415936,
469 0.2113749313486628,
470 0.5024954410639694,
471 0.8482093958964643,
472 0.5985244211727975,
473 0.86622696414705,
474 0.01281216961604914,
475 0.5751167715220191,
476 0.9444215182478257,
477 0.12791631407771153,
478 0.07110823492511875,
479 0.36665916967948997,
480 0.4357763962707135,
481 0.013768378613968846,
482 0.20290927574440676,
483 0.09791792152929635,
484 0.25668897581102323,
485 0.10415239170668067,
486 0.030148133859263293,
487 0.39916087076027995,
488 0.23937645138057062,
489 0.26541527828961586,
490 0.23775536399848263,
491 0.6981544757966329,
492 0.034474379818287826,
493 0.15702405712833167,
494 0.04933795426694132,
495 0.2640040834468361,
496 0.9051200924485773,
497 0.30460229768182623,
498 0.13874070233015756,
499 0.5357436895137105,
500 0.04145421794947868,
501 0.7106841141308103,
502 0.3680633229402389,
503 0.24190636573812052,
504 0.9463928684164328,
505 0.9057640453645545,
506 0.8623181861032716,
507 0.4550286789732636,
508 0.4400869943881256,
509 0.9065199975671652,
510 0.1261459343513971,
511 0.06488813423368744,
512 0.77791640033145,
513 0.5897900639443128,
514 0.05756822139642326,
515 0.9352171789216979,
516 0.12367414156389867,
517 0.13042016457468297,
518 0.3667417710228327,
519 0.8620384416057306,
520 0.5362882323005205,
521 0.1096425332111729,
522 0.3198259239548952,
523 0.9757891416632953,
524 0.34817402671960895,
525 0.9463540208396476,
526 0.15124375921444,
527 0.10364394924264919,
528 0.5560904235518845,
529 0.87522829578661,
530 0.7419379771918783,
531 0.7934003653423422,
532 0.8527438840879623,
533 0.7124943368375772,
534 0.5431301324998252,
535 0.07639180390334432,
536 0.37395145683192077,
537 0.14711038152957956,
538 0.8445936201403674,
539 0.49413406479527144,
540 0.8802394873974577,
541 0.42289700616045167,
542 0.6884929834272331,
543 0.042845740141808974,
544 0.6126934059809861,
545 0.6792533526966404,
546 0.855252611483559,
547 0.295896110978891,
548 0.4107892217148358,
549 0.5609864575170519,
550 0.9032304302157587,
551 0.8598123832943819,
552 0.8416952050262075,
553 0.9272969188006049,
554 0.9458019435477735,
555 0.620841557600415,
556 0.9127775366187049,
557 0.7368599610719945,
558 0.8747772265514103,
559 0.007965961452839454,
560 0.8700201951667574,
561 0.28313110107043704,
562 0.08815782041546838,
563 0.11300559412778066,
564 0.6514507772651915,
565 0.16830249695234734,
566 0.47723527853843595,
567 0.6867684699248284,
568 0.7914522117746634,
569 0.2803255455335468,
570 0.8155838418621151,
571 0.5589040133509352,
572 0.6309690118548176,
573 0.8883016292370474,
574 0.5270448338569975,
575 0.5425593816046722,
576 0.5274784343541568,
577 0.9545557277440215,
578 0.7318445922843663,
579 0.4685847261962366,
580 0.2783347870553693,
581 0.39825068467133595,
582 0.5538107976687636,
583 0.03293580343332114,
584 0.7932611630237487,
585 0.19179487220218683,
586 0.0790697008089577,
587 0.88403193841529,
588 0.03930432846700338,
589 0.731919319837637,
590 0.09682808939624576,
591 0.6158142000636625,
592 0.3925786713826186,
593 0.6351869378757524,
594 0.6992467596275356,
595 0.3419461195339333,
596 0.6211406096603801,
597 0.3261175948501531,
598 0.109151633747534,
599 0.19807230577737,
600 0.8499778579858915,
601 0.5698700287332708,
602 0.784468708086921,
603 0.3570880080965999,
604 0.11785052534144869,
605 0.18741539899992044,
606 0.8297695099948096,
607 0.0789934189863013,
608 0.5154449414971082,
609 0.5214753905634504,
610 0.5613884403604991,
611 0.41260606327600036,
612 0.5476649237174546,
613 0.662471909483809,
614 0.5049648804369952,
615 0.6826486330334145,
616 0.6160206170019211,
617 0.1545239206745902,
618 0.25191006782617,
619 0.5051235388041858,
620 0.4453697753074036,
621 0.5858660214491829,
622 0.5307136856458474,
623 0.8733801375466267,
624 0.26913035286487075,
625 0.25651252089632126,
626 0.45616771610445594,
627 0.19058888987038491,
628 0.8508685810625294,
629 0.2340826351126558,
630 0.4295582037776007,
631 0.6273731822388989,
632 ];
633
634 let mut ffp = crate::FirefoxPredictor::new(vec![
655 0.983788222968869,
656 0.6210323993153665,
657 0.37646090421893474,
658 0.13923801694587312,
659 ]);
660 let mut predictions = vec![];
661
662 for _ in 0..pool.len() {
663 let prediction = ffp.predict_next()?;
664 predictions.push(prediction);
665 }
666
667 assert_eq!(predictions, pool);
668 return Ok(());
669 }
670}