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()

s.add(state2 == state1*214013+2531011)
s.add(state3 == state2*214013+2531011)
s.add(state4 == state3*214013+2531011)
s.add(state5 == state4*214013+2531011)
s.add(state6 == state5*214013+2531011)
s.add(state7 == state6*214013+2531011)
s.add(state8 == state7*214013+2531011)
s.add(state9 == state8*214013+2531011)

s.add(URem((state2>>16)&0x7FFF,10)==0)
s.add(URem((state3>>16)&0x7FFF,10)==0)
s.add(URem((state4>>16)&0x7FFF,10)==0)
s.add(URem((state5>>16)&0x7FFF,10)==0)
s.add(URem((state6>>16)&0x7FFF,10)==0)
s.add(URem((state7>>16)&0x7FFF,10)==0)
s.add(URem((state8>>16)&0x7FFF,10)==0)
s.add(URem((state9>>16)&0x7FFF,10)==0)

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!

What about other modulos?

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()

s.add(state2 == state1*214013+2531011)
s.add(state3 == state2*214013+2531011)
s.add(state4 == state3*214013+2531011)
s.add(state5 == state4*214013+2531011)

s.add(URem((state2>>16)&0x7FFF,100)==0)
s.add(URem((state3>>16)&0x7FFF,100)==0)
s.add(URem((state4>>16)&0x7FFF,100)==0)
s.add(URem((state5>>16)&0x7FFF,100)==0)

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/dennis714/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()

s.add(state2 == state1*214013+2531011)
s.add(state3 == state2*214013+2531011)
s.add(state4 == state3*214013+2531011)

s.add(URem((state2>>16)&0x7FFF,1000)==0)
s.add(URem((state3>>16)&0x7FFF,1000)==0)
s.add(URem((state4>>16)&0x7FFF,1000)==0)

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()

s.add(state2 == state1*214013+2531011)
s.add(state3 == state2*214013+2531011)

s.add((state2>>16)&0x7FFF==0)
s.add((state3>>16)&0x7FFF==0)

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

s.add(state2 == state1*214013+2531011)
s.add(state3 == state2*214013+2531011)
s.add(state4 == state3*214013+2531011)
s.add(state5 == state4*214013+2531011)
s.add(state6 == state5*214013+2531011)
s.add(state7 == state6*214013+2531011)

c = BitVec('c', 32)

s.add(URem((state2>>16)&0x7FFF,10)==c)
s.add(URem((state3>>16)&0x7FFF,10)==c)
s.add(URem((state4>>16)&0x7FFF,10)==c)
s.add(URem((state5>>16)&0x7FFF,10)==c)
s.add(URem((state6>>16)&0x7FFF,10)==c)
s.add(URem((state7>>16)&0x7FFF,10)==c)

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:

The files: https://github.com/dennis714/yurichev.com/tree/master/blog/LCG_Z3.

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.

→ [back to the main page]