Why PRNGs are not the same as CSPRNGs

solver.py

import z3


def sym_xoroshiro128plus(solver, sym_s0, sym_s1, mask, result):
	s0 = sym_s0
	s1 = sym_s1
	sym_r = (sym_s0 + sym_s1)
	
	condition = z3.Bool('c0x%0.16x' % result)
	solver.add(z3.Implies(condition, (sym_r & mask) == result & mask))
	
	s1 ^= s0
	sym_s0 = z3.RotateLeft(s0, 55) ^ s1 ^ (s1 << 14)
	sym_s1 = z3.RotateLeft(s1, 36)
	
	return sym_s0, sym_s1, condition


def find_seed(results_with_masks):
	start_s0, start_s1 = z3.BitVecs('start_s0 start_s1', 64)
	sym_s0 = start_s0
	sym_s1 = start_s1
	solver = z3.Solver()
	conditions = []
	
	for result, mask in results_with_masks:
		sym_s0, sym_s1, condition = sym_xoroshiro128plus(solver, sym_s0, sym_s1, mask, result)
		conditions.append(condition)
	
	if solver.check(conditions) == z3.sat:
		model = solver.model()
		
		return (model[start_s0].as_long(), model[start_s1].as_long())
	
	else:
		return None


find_seed([(0x0, 0x0), (0x206e6172614b2020, 0xffffffffffffffff), (0x2020736e6f794c, 0xffffffffffffff)])
# Output: (12030599390342465081, 17190518429081885642)

xoroshiro128.py

def bin2chr(data):
	result = ''
	
	while data:
		char = data & 0xff
		result += chr(char)
		data >>= 8
	
	return result


class Xoroshiro128Plus(object):
	def __init__(self, seed):
		self.seed = seed
	
	@staticmethod
	def rotl(x, k):
		return ((x << k) & 0xffffffffffffffff) | (x >> 64 - k)
	
	def next(self):
		s0 = self.seed[0]
		s1 = self.seed[1]
		result = (s0 + s1) & 0xffffffffffffffff
		
		s1 ^= s0
		self.seed[0] = self.rotl(s0, 55) ^ s1 ^ ((s1 << 14) & 0xffffffffffffffff)
		self.seed[1] = self.rotl(s1, 36)
		
		return result


generator = Xoroshiro128Plus([0xb4581c52b5a611f1, 0x849afd73bea7cce9])
print(repr(''.join(bin2chr(generator.next()) for i in range(4))))
# Output: 'ÚÞMtÆ\x19ó8  Karan Lyons  3A?â\x11)ÐÑ{'

👏🏻