## Can rand() generate 10 consecutive zeroes?

I've always been wondering, if it's possible or not. As of simplest linear congruential generator from MSVC's rand(), I could get a state at which rand() will output 8 zeroes modulo 10:

#!/usr/bin/python
from z3 import *

state1 = BitVec('state1', 32)
state2 = BitVec('state2', 32)
state3 = BitVec('state3', 32)
state4 = BitVec('state4', 32)
state5 = BitVec('state5', 32)
state6 = BitVec('state6', 32)
state7 = BitVec('state7', 32)
state8 = BitVec('state8', 32)
state9 = BitVec('state9', 32)

s = Solver()

print(s.check())
print(s.model())


sat
[state3 = 1181667981,
state4 = 342792988,
state5 = 4116856175,
state7 = 1741999969,
state8 = 3185636512,
state2 = 1478548498,
state6 = 4036911734,
state1 = 286227003,
state9 = 1700675811]


This is a case if, in some video game, you'll find a code:

for (int i=0; i<8; i++)
printf ("%d\n", rand() % 10);


... and at some point, this piece of code can generate 8 zeroes in row, if the state will be 286227003 (decimal).

Just checked this piece of code in MSVC 2015:
// MSVC 2015 x86

#include <stdio.h>

int main()
{
srand(286227003);

for (int i=0; i<8; i++)
printf ("%d\n", rand() % 10);
};


Yes, its output is 8 zeroes!

I can get 4 consecutive zeroes modulo 100:

#!/usr/bin/python
from z3 import *

state1 = BitVec('state1', 32)
state2 = BitVec('state2', 32)
state3 = BitVec('state3', 32)
state4 = BitVec('state4', 32)
state5 = BitVec('state5', 32)

s = Solver()

print(s.check())
print(s.model())


sat
[state3 = 635704497,
state4 = 1644979376,
state2 = 1055176198,
state1 = 3865742399,
state5 = 1389375667]


However, 4 consecutive zeroes modulo 100 is impossible (given these constants at least), this gives "unsat": https://github.com/DennisYurichev/yurichev.com/blob/master/blog/LCG_Z3/LCG100_v1.py.

... and 3 consecutive zeroes modulo 1000:

#!/usr/bin/python
from z3 import *

state1 = BitVec('state1', 32)
state2 = BitVec('state2', 32)
state3 = BitVec('state3', 32)
state4 = BitVec('state4', 32)

s = Solver()

print(s.check())
print(s.model())


sat
[state3 = 1179663182,
state2 = 720934183,
state1 = 4090229556,
state4 = 786474201]


What if we could use rand()'s output without division? Which is in 0..0x7fff range (i.e., 15 bits)? As it can be checked quickly, 2 zeroes at output is possible:

#!/usr/bin/python
from z3 import *

state1 = BitVec('state1', 32)
state2 = BitVec('state2', 32)
state3 = BitVec('state3', 32)

s = Solver()

print(s.check())
print(s.model())


sat
[state2 = 20057, state1 = 3385131726, state3 = 22456]


### UNIX time and srand(time(NULL))

Given the fact that it's highly popular to initialize LCG PRNG with UNIX time (i.e., srand(time(NULL))), you can probably calculate a moment in time so that LCG PRNG will be initialized as you want to.

For example, can we get a moment in time from now (5-Dec-2017) till 12-Dec-2017 (that is one week from now), when, if initialized by UNIX time, rand() will output as many similar numbers (modulo 10), as possible?

#!/usr/bin/python
from z3 import *

state1 = BitVec('state1', 32)
state2 = BitVec('state2', 32)
state3 = BitVec('state3', 32)
state4 = BitVec('state4', 32)
state5 = BitVec('state5', 32)
state6 = BitVec('state6', 32)
state7 = BitVec('state7', 32)

s = Solver()

s.add(state1>=1512499124) # Tue Dec  5 20:38:44 EET 2017
s.add(state1<=1513036800) # Tue Dec 12 02:00:00 EET 2017

c = BitVec('c', 32)

print(s.check())
print(s.model())


Yes:
sat
[state3 = 2234253076,
state4 = 497021319,
state5 = 4160988718,
c = 3,
state2 = 333151205,
state6 = 46785593,
state1 = 1512500810,
state7 = 1158878744]


If srand(time(NULL)) will be executed at Tue Dec 5 21:06:50 EET 2017 (this precise second, UNIX time=1512500810), a next 6 rand() %10 lines will output six numbers of 3 in a row. Don't know if it useful or not, but you've got the idea.

### etc:

See also: Text strings right in the middle of compressed data. Also, my SAT/SMT notes has another LCG-related example.

Further work: check glibc's rand(), Mersenne Twister, etc. Simple 32-bit LCG as described can be checked using simple brute-force, I think.