Skip to content

Instantly share code, notes, and snippets.

@rkern

rkern/Z3PRNG.ipynb

Created October 23, 2021 18:07
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save rkern/4712fdca09c36f84dccd21662fd0afc3 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save rkern/4712fdca09c36f84dccd21662fd0afc3 to your computer and use it in GitHub Desktop.
Download ZIP
Notebook demonstrating the use of Z3 to try to solve for the state of PCG PRNGs
Display the source blob
Display the rendered blob
Raw
Z3PRNG.ipynb
{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Cracking PCG with Z3\n",
"\n",
"Currently, 32-bit states seem to be in reach, but 64-bit states seem to be out of reach in a reasonable amount of time (overnight)."
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"import abc\n",
"from itertools import islice\n",
"\n",
"from tqdm.auto import tqdm\n",
"import z3"
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {},
"outputs": [],
"source": [
"MASK8 = (1<<8) - 1\n",
"MASK16 = (1<<16) - 1\n",
"MASK32 = (1<<32) - 1\n",
"MASK64 = (1<<64) - 1\n",
"MASK128 = (1<<128) - 1"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": [
"class OverconstrainedError(Exception):\n",
" \"\"\" The SMT problem is overconstrained, and there is no possible solution.\n",
" \"\"\"\n",
" \n",
" \n",
"class UnsolvedError(Exception):\n",
" \"\"\" The SMT problem's satisfiability is unknown for the given reason.\n",
" \"\"\"\n",
"\n",
" \n",
"def check_solution(solver, verbose=True):\n",
" if verbose:\n",
" print('Assertions:')\n",
" for assertion in solver.assertions():\n",
" print(assertion.sexpr())\n",
" print()\n",
" return solver.check()\n",
"\n",
"\n",
"class SimPRNG(abc.ABC):\n",
" \"\"\" Encapsulate the concrete implementation of a PRNG and its Z3 symbolic \"simulation\".\n",
" \n",
" Attributes\n",
" ----------\n",
" variables : list of (Z3 symbol, int) pairs\n",
" These are the free variables to solve for and their corresponding concrete values.\n",
" For now, the symbols are almost certain to be named `BitVec` instances of some bit size\n",
" and the concrete values will be integers that can be cast to the corresponding `BitVecSort`.\n",
" \"\"\"\n",
" \n",
" @abc.abstractmethod\n",
" def prng(self):\n",
" \"\"\" Generator that yields sample output from the real PRNG.\n",
" \"\"\"\n",
" raise NotImplementedError\n",
" \n",
" @abc.abstractmethod\n",
" def simulation(self):\n",
" \"\"\" Generator that yields the successive symbolic Z3 expressions for each output of the PRNG.\n",
" \"\"\"\n",
" raise NotImplementedError\n",
" \n",
" @property\n",
" def gold_values(self):\n",
" \"\"\" The known input values, organized as a dict mapping the name to the value.\n",
" \"\"\"\n",
" values = {var.decl().name(): value\n",
" for var, value in self.variables}\n",
" return values\n",
" \n",
" def confirm_simulation(self, n_samples):\n",
" \"\"\" Generate pairs of output values from the concrete PRNG and the output expression from the\n",
" simulation to confirm that they implement the same algorithm.\n",
" \"\"\"\n",
" prng = self.prng()\n",
" sim = self.simulation()\n",
" variables = [(var, var.sort().cast(value)) for var, value in self.variables]\n",
" for i, (sample, expr) in enumerate(islice(zip(prng, sim), 0, n_samples)):\n",
" sim_sample = z3.simplify(z3.substitute(expr, variables)).as_long()\n",
" if sim_sample != sample:\n",
" raise AssertionError(f\"Mismatch at i={i}:\\n\"\n",
" f\" sample = {sample}\\n\"\n",
" f\" sim_sample = {sim_sample}\")\n",
" return True\n",
" \n",
" def solve(self, start_sample=0, max_samples=100, solver=None, verbose=True, simplify=True):\n",
" \"\"\" Solve for the initial state of the PRNG with the minimum number of sample outputs.\n",
" \"\"\"\n",
" prng = self.prng()\n",
" sim = self.simulation()\n",
"\n",
" if solver is None:\n",
" solver = z3.Solver()\n",
" for i in tqdm(range(1, max_samples + 1), disable=not verbose):\n",
" sample = next(prng)\n",
" expression = next(sim)\n",
" constraint = sample == expression\n",
" if simplify:\n",
" constraint = z3.simplify(constraint)\n",
" solver.assert_exprs(constraint)\n",
" if i > start_sample:\n",
" check_result = check_solution(solver, verbose=verbose)\n",
" if verbose:\n",
" print('Statistics:')\n",
" print(solver.statistics())\n",
" print()\n",
" if check_result == z3.unknown:\n",
" reason = solver.reason_unknown()\n",
" raise UnsolvedError(f\"Unsolved at {i} samples: {reason}\")\n",
" elif check_result == z3.sat:\n",
" model = solver.model()\n",
" # Check for uniqueness.\n",
" unique_constraint = z3.Not(z3.And(*[var == model[var]\n",
" for var, _ in self.variables]))\n",
" solver.push()\n",
" solver.assert_exprs(unique_constraint)\n",
" if verbose:\n",
" print('Checking solution for uniqueness:')\n",
" check_result = check_solution(solver, verbose=verbose)\n",
" if check_result == z3.unknown:\n",
" reason = solver.reason_unknown()\n",
" raise UnsolvedError(f\"Unsolved at {i} samples: {reason}\")\n",
" elif check_result == z3.unsat:\n",
" # A unique result. The PRNG has been solved.\n",
" # Gather up all of the model values into a dict.\n",
" values = {var.decl().name(): model[var].as_long()\n",
" for var, _ in self.variables}\n",
" return i, values\n",
" else:\n",
" # A non-unique result.\n",
" # Restore the solver state to before the unique_constraint.\n",
" solver.pop()\n",
" continue\n",
" else:\n",
" raise OverconstrainedError(f\"PRNG is overconstrained at {i} samples\")\n",
" # We reached the maximum number of samples without finding a solution or infeasibility.\n",
" return i, None"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## MSVC2013 PRNG\n",
"\n",
"This has a 32-bit state (with a 31-bit seed) and a 15-bit output. This is easily solved by Z3 with 3-4 samples."
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {},
"outputs": [],
"source": [
"class SimMSVC2013(SimPRNG):\n",
" def __init__(self, seed_value):\n",
" self.seed_value = seed_value\n",
" \n",
" # This PRNG only accepts 31-bit seeds.\n",
" self.seed_var = z3.BitVec('seed', 31)\n",
" self.variables = [(self.seed_var, self.seed_value)]\n",
" \n",
" def prng(self):\n",
" state = self.seed_value\n",
" while True:\n",
" state = (state * 214013 + 2531011) & MASK32\n",
" output = (state // 65536) % 32768\n",
" yield output\n",
"\n",
" def simulation(self):\n",
" # Extend the 31-bit seed value to the full 32-bit state size.\n",
" state = z3.ZeroExt(1, self.seed_var)\n",
" while True:\n",
" state = state * 214013 + 2531011\n",
" output = z3.URem(z3.UDiv(state, 65536), 32768)\n",
" yield output"
]
},
{
"cell_type": "code",
"execution_count": 5,
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "898d2037f92b4ebb8c7cf04e2f382227",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"HBox(children=(FloatProgress(value=0.0), HTML(value='')))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Assertions:\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x00269ec3 (bvmul #x000343fd (concat #b0 seed))))))\n",
" (= a!1 #b000111111100100))\n",
"\n",
"Statistics:\n",
"(:max-memory 27.98\n",
" :memory 19.23\n",
" :num-allocs 11094910\n",
" :rlimit-count 88258\n",
" :sat-backjumps 104\n",
" :sat-conflicts 104\n",
" :sat-decisions 201\n",
" :sat-del-clause 4401\n",
" :sat-elim-bool-vars-res 823\n",
" :sat-elim-clauses 29\n",
" :sat-elim-literals 25\n",
" :sat-minimized-lits 776\n",
" :sat-mk-clause-2ary 1965\n",
" :sat-mk-clause-3ary 4137\n",
" :sat-mk-clause-nary 3254\n",
" :sat-mk-var 1324\n",
" :sat-probing-assigned 7\n",
" :sat-propagations-2ary 13195\n",
" :sat-propagations-3ary 17772\n",
" :sat-propagations-nary 2426\n",
" :sat-scc-elim-vars 16\n",
" :sat-subs-resolution-dyn 18\n",
" :sat-subsumed 1288\n",
" :sat-units 7\n",
" :time 0.02)\n",
"\n",
"Assertions:\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x00269ec3 (bvmul #x000343fd (concat #b0 seed))))))\n",
" (= a!1 #b000111111100100))\n",
"(not (and (= #b0001101101101011000000011100001 seed)))\n",
"\n",
"Assertions:\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x00269ec3 (bvmul #x000343fd (concat #b0 seed))))))\n",
" (= a!1 #b000111111100100))\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x1e278e7a (bvmul #xa9fc6809 (concat #b0 seed))))))\n",
" (= a!1 #b000000011010101))\n",
"\n",
"Statistics:\n",
"(:added-eqs 15\n",
" :arith-make-feasible 3\n",
" :arith-max-columns 4\n",
" :binary-propagations 2235749\n",
" :bv-bit2core 30\n",
" :bv-diseqs 7\n",
" :bv-dynamic-diseqs 1\n",
" :conflicts 10041\n",
" :decisions 12300\n",
" :del-clause 4152\n",
" :final-checks 2\n",
" :max-memory 27.98\n",
" :memory 21.29\n",
" :minimized-lits 221693\n",
" :mk-bool-var 2235\n",
" :mk-clause 14628\n",
" :num-allocs 15678432\n",
" :num-checks 2\n",
" :propagations 5982596\n",
" :restarts 71\n",
" :rlimit-count 5918831\n",
" :time 0.51)\n",
"\n",
"Assertions:\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x00269ec3 (bvmul #x000343fd (concat #b0 seed))))))\n",
" (= a!1 #b000111111100100))\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x1e278e7a (bvmul #xa9fc6809 (concat #b0 seed))))))\n",
" (= a!1 #b000000011010101))\n",
"(not (and (= #b0000000000000000000010011010010 seed)))\n",
"\n",
"Assertions:\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x00269ec3 (bvmul #x000343fd (concat #b0 seed))))))\n",
" (= a!1 #b000111111100100))\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x1e278e7a (bvmul #xa9fc6809 (concat #b0 seed))))))\n",
" (= a!1 #b000000011010101))\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #xd2f65b55 (bvmul #x45c82be5 (concat #b0 seed))))))\n",
" (= a!1 #b011000111011001))\n",
"\n",
"Statistics:\n",
"(:added-eqs 26\n",
" :arith-make-feasible 5\n",
" :arith-max-columns 4\n",
" :binary-propagations 16408772\n",
" :bv-bit2core 45\n",
" :bv-diseqs 14\n",
" :bv-dynamic-diseqs 2\n",
" :conflicts 54990\n",
" :decisions 61527\n",
" :del-clause 48927\n",
" :final-checks 4\n",
" :max-memory 27.98\n",
" :memory 25.44\n",
" :minimized-lits 1618774\n",
" :mk-bool-var 3475\n",
" :mk-clause 62120\n",
" :num-allocs 25650588\n",
" :num-checks 4\n",
" :propagations 44052891\n",
" :restarts 294\n",
" :rlimit-count 43116968\n",
" :time 0.02)\n",
"\n",
"Assertions:\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x00269ec3 (bvmul #x000343fd (concat #b0 seed))))))\n",
" (= a!1 #b000111111100100))\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #x1e278e7a (bvmul #xa9fc6809 (concat #b0 seed))))))\n",
" (= a!1 #b000000011010101))\n",
"(let ((a!1 ((_ extract 30 16)\n",
" (bvadd #xd2f65b55 (bvmul #x45c82be5 (concat #b0 seed))))))\n",
" (= a!1 #b011000111011001))\n",
"(not (and (= #b0000000000000000000010011010010 seed)))\n",
"\n"
]
},
{
"data": {
"text/plain": [
"((3, {'seed': 1234}), {'seed': 1234})"
]
},
"execution_count": 5,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sim_msvc = SimMSVC2013(1234)\n",
"assert sim_msvc.confirm_simulation(100)\n",
"print(f'Expected values: {sim_msvc.gold_values}')\n",
"sim_msvc.solve()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Truncated LCG\n",
"\n",
"The next step up to the PCG family is a truncated LCG where we iterate the `N`-bit state and return the upper `N//2` bits as the output, but otherwise no massaging of the output. We can choose state sizes from `{8, 16, 32, 64, 128}`. The 32-bit state (16-bit output) is also easily solved. The 64-bit state (32-bit output) does not get solved in a reasonable amount of time (overnight) at checking just 2 samples.\n",
"\n",
"We use the multiplier and increment constants from the PCG implementations."
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [],
"source": [
"PCG_STATE_ONESEQ_8_INITIALIZER = 0xd7\n",
"PCG_STATE_ONESEQ_16_INITIALIZER = 0x20df\n",
"PCG_STATE_ONESEQ_32_INITIALIZER = 0x46b56677\n",
"PCG_STATE_ONESEQ_64_INITIALIZER = 0x4d595df4d0f33173\n",
"PCG_STATE_ONESEQ_128_INITIALIZER = (0xb8dc10e158a92392 << 64) + 0x98046df007ec0a53\n",
"\n",
"PCG_DEFAULT_MULTIPLIER_8 = 141\n",
"PCG_DEFAULT_MULTIPLIER_16 = 12829\n",
"PCG_DEFAULT_MULTIPLIER_32 = 747796405\n",
"PCG_DEFAULT_MULTIPLIER_64 = 6364136223846793005\n",
"PCG_DEFAULT_MULTIPLIER_128 = (2549297995355413924 << 64) + 4865540595714422341\n",
"\n",
"PCG_DEFAULT_INCREMENT_8 = 77\n",
"PCG_DEFAULT_INCREMENT_16 = 47989\n",
"PCG_DEFAULT_INCREMENT_32 = 2891336453\n",
"PCG_DEFAULT_INCREMENT_64 = 1442695040888963407\n",
"PCG_DEFAULT_INCREMENT_128 = (6364136223846793005 << 64) + 1442695040888963407\n",
"\n",
"PCG_SETTINGS = {\n",
" 8: (PCG_DEFAULT_MULTIPLIER_8, PCG_DEFAULT_INCREMENT_8, PCG_STATE_ONESEQ_8_INITIALIZER),\n",
" 16: (PCG_DEFAULT_MULTIPLIER_16, PCG_DEFAULT_INCREMENT_16, PCG_STATE_ONESEQ_16_INITIALIZER),\n",
" 32: (PCG_DEFAULT_MULTIPLIER_32, PCG_DEFAULT_INCREMENT_32, PCG_STATE_ONESEQ_32_INITIALIZER),\n",
" 64: (PCG_DEFAULT_MULTIPLIER_64, PCG_DEFAULT_INCREMENT_64, PCG_STATE_ONESEQ_64_INITIALIZER),\n",
" 128: (PCG_DEFAULT_MULTIPLIER_128, PCG_DEFAULT_INCREMENT_128, PCG_STATE_ONESEQ_128_INITIALIZER),\n",
"}"
]
},
{
"cell_type": "code",
"execution_count": 7,
"metadata": {},
"outputs": [],
"source": [
"class SimTruncLCG(SimPRNG):\n",
" def __init__(self, state_bits=64, seed_value=None):\n",
" self.state_bits = state_bits\n",
" self.mult, self.inc, default_seed = PCG_SETTINGS[self.state_bits]\n",
" if seed_value is None:\n",
" seed_value = default_seed\n",
" self.seed_value = seed_value\n",
" \n",
" self.output_bits = state_bits // 2\n",
" self.seed_var = z3.BitVec('seed', self.state_bits)\n",
" self.variables = [(self.seed_var, self.seed_value)]\n",
" self.state_den = (1 << self.state_bits)\n",
" self.output_den = (1 << self.output_bits)\n",
" self.state_mask = (1 << self.state_bits) - 1\n",
" self.output_mask = (1 << self.output_bits) - 1\n",
" \n",
" def prng(self):\n",
" state = self.seed_value\n",
" while True:\n",
" state = ((state * self.mult) + self.inc) & self.state_mask\n",
" output = state >> self.output_bits\n",
" yield output\n",
" \n",
" def simulation(self):\n",
" state = self.seed_var\n",
" constraint = z3.BoolVal(True)\n",
" while True:\n",
" state = state * self.mult + self.inc\n",
" output = z3.Extract(self.state_bits - 1, self.output_bits, state)\n",
" yield output"
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "af276eb8776f4a8bbbbf278e5a5770ec",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"HBox(children=(FloatProgress(value=0.0), HTML(value='')))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Assertions:\n",
"(= ((_ extract 31 16) (bvadd #xac564b05 (bvmul #x2c9277b5 seed))) #xe117)\n",
"\n",
"Statistics:\n",
"(:eliminated-applications 4\n",
" :final-checks 2\n",
" :max-memory 129.83\n",
" :memory 40.24\n",
" :mk-bool-var 2\n",
" :num-allocs 39138368879.00\n",
" :num-checks 2\n",
" :rlimit-count 203913832\n",
" :time 0.00)\n",
"\n",
"Assertions:\n",
"(= ((_ extract 31 16) (bvadd #xac564b05 (bvmul #x2c9277b5 seed))) #xe117)\n",
"(not (and (= #xf7e907ef seed)))\n",
"\n",
"Assertions:\n",
"(= ((_ extract 31 16) (bvadd #xac564b05 (bvmul #x2c9277b5 seed))) #xe117)\n",
"(= ((_ extract 31 16) (bvadd #x4712a88e (bvmul #xfa6dc5f9 seed))) #x7c07)\n",
"\n",
"Statistics:\n",
"(:added-eqs 15\n",
" :arith-make-feasible 3\n",
" :arith-max-columns 4\n",
" :binary-propagations 21580007\n",
" :bv-bit2core 32\n",
" :bv-diseqs 7\n",
" :bv-dynamic-diseqs 1\n",
" :conflicts 68976\n",
" :decisions 80246\n",
" :del-clause 25614\n",
" :final-checks 2\n",
" :max-memory 129.83\n",
" :memory 48.20\n",
" :minimized-lits 2142322\n",
" :mk-bool-var 2973\n",
" :mk-clause 75120\n",
" :num-allocs 40918985068.00\n",
" :num-checks 2\n",
" :propagations 59910554\n",
" :restarts 295\n",
" :rlimit-count 261582607\n",
" :time 5.94)\n",
"\n",
"Assertions:\n",
"(= ((_ extract 31 16) (bvadd #xac564b05 (bvmul #x2c9277b5 seed))) #xe117)\n",
"(= ((_ extract 31 16) (bvadd #x4712a88e (bvmul #xfa6dc5f9 seed))) #x7c07)\n",
"(not (and (= #x46b56677 seed)))\n",
"\n"
]
},
{
"data": {
"text/plain": [
"((2, {'seed': 1186293367}), {'seed': 1186293367})"
]
},
"execution_count": 9,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sim_lcg32 = SimTruncLCG(32)\n",
"assert sim_lcg32.confirm_simulation(1000)\n",
"print(f'Expected values: {sim_lcg32.gold_values}')\n",
"sim_lcg32.solve()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The following takes too long to compute, so it is commented out, but the output of a cancelled run is included."
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "d19e4695fbb24ca1ae4a7c8d18910071",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"HBox(children=(FloatProgress(value=0.0), HTML(value='')))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Assertions:\n",
"(= ((_ extract 63 32)\n",
" (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed)))\n",
" #x132190a1)\n",
"\n",
"Statistics:\n",
"(:eliminated-applications 4\n",
" :final-checks 2\n",
" :max-memory 129.83\n",
" :memory 41.71\n",
" :mk-bool-var 2\n",
" :num-allocs 44219919456.00\n",
" :num-checks 2\n",
" :rlimit-count 281405951\n",
" :time 0.00)\n",
"\n",
"Assertions:\n",
"(= ((_ extract 63 32)\n",
" (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed)))\n",
" #x132190a1)\n",
"(not (and (= #xe22f157b21535015 seed)))\n",
"\n",
"Assertions:\n",
"(= ((_ extract 63 32)\n",
" (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed)))\n",
" #x132190a1)\n",
"(= ((_ extract 63 32)\n",
" (bvadd #x1a08ee1184ba6d32 (bvmul #x685f98a2018fade9 seed)))\n",
" #x065e20e8)\n",
"\n",
"Statistics:\n",
"(:added-eqs 14\n",
" :arith-make-feasible 2\n",
" :arith-max-columns 4\n",
" :binary-propagations 434852113\n",
" :bv-bit2core 64\n",
" :bv-diseqs 7\n",
" :bv-dynamic-diseqs 2\n",
" :conflicts 801743\n",
" :decisions 922000\n",
" :del-clause 766282\n",
" :final-checks 1\n",
" :max-memory 129.83\n",
" :memory 58.75\n",
" :minimized-lits 34313790\n",
" :mk-bool-var 11348\n",
" :mk-clause 824799\n",
" :num-allocs 71453847536.00\n",
" :num-checks 2\n",
" :propagations 1248152696\n",
" :restarts 792\n",
" :rlimit-count 1472432635\n",
" :time 123.74)\n",
"\n"
]
},
{
"ename": "UnsolvedError",
"evalue": "Unsolved at 2 samples: canceled",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mUnsolvedError\u001b[0m Traceback (most recent call last)",
"\u001b[0;32m<ipython-input-10-c479fca2787d>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[1;32m 1\u001b[0m \u001b[0msim_lcg64\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0mSimTruncLCG\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;36m64\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 2\u001b[0m \u001b[0;32massert\u001b[0m \u001b[0msim_lcg64\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mconfirm_simulation\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;36m1000\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 3\u001b[0;31m \u001b[0msim_lcg64\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0msolve\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0msim_lcg64\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mgold_values\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;32m<ipython-input-3-3d9cb9169d3e>\u001b[0m in \u001b[0;36msolve\u001b[0;34m(self, start_sample, max_samples, solver, verbose, simplify)\u001b[0m\n\u001b[1;32m 87\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mcheck_result\u001b[0m \u001b[0;34m==\u001b[0m \u001b[0mz3\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0munknown\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 88\u001b[0m \u001b[0mreason\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0msolver\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mreason_unknown\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 89\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mUnsolvedError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34mf\"Unsolved at {i} samples: {reason}\"\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 90\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0mcheck_result\u001b[0m \u001b[0;34m==\u001b[0m \u001b[0mz3\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0msat\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 91\u001b[0m \u001b[0mmodel\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0msolver\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmodel\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;31mUnsolvedError\u001b[0m: Unsolved at 2 samples: canceled"
]
}
],
"source": [
"sim_lcg64 = SimTruncLCG(64)\n",
"assert sim_lcg64.confirm_simulation(1000)\n",
"print(f'Expected values: {sim_lcg64.gold_values}')\n",
"#sim_lcg64.solve()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## PCG\n",
"\n",
"Now we can implement members of the PCG family. The goal is to implement the PCG64 (128-bit state, 64-bit output) variants in `numpy`: one with the once-standard XSL-RR output function and then the newer, stronger DXSM output function. The standard implementations for the smaller PCG state sizes use stronger output functions, but I am interested in the reduced-size versions only insofar as they provide a warm-up exercise and apples-to-apples comparisons with the standard PCG64 implementations, so I have implemented XSL-RR for them. DXSM will not be easy to apply to the smaller sizes, so I will only implement it for the 128-bit state size, and then only when PCG32 (64-bit state, 32-bit output) is solvable.\n",
"\n",
"The current implementations use the fixed recommended increments and only solve for the state variable. Eventually, we will work up to solving for both the state and the increment as both are seedable in the `numpy` implementation.\n",
"\n",
"Like the 64-bit state LCG, PCG32 is fails to solve in a reasonable amount of time when checking merely 2 samples."
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {},
"outputs": [],
"source": [
"def rotr8(value, rot):\n",
" return ((value >> rot) | (value << (8 - rot))) & MASK8\n",
" \n",
"def rotr16(value, rot):\n",
" return ((value >> rot) | (value << (16 - rot))) & MASK16\n",
"\n",
"def rotr32(value, rot):\n",
" return ((value >> rot) | (value << (32 - rot))) & MASK32\n",
"\n",
"\n",
"class SimPCG16OneSeq(SimPRNG):\n",
" def __init__(self, seed_value=PCG_STATE_ONESEQ_32_INITIALIZER):\n",
" self.seed_value = seed_value\n",
" \n",
" self.seed_var = z3.BitVec('seed', 32)\n",
" self.variables = [(self.seed_var, self.seed_value)]\n",
" \n",
" def prng(self):\n",
" state = self.seed_value\n",
" while True:\n",
" state = (state * PCG_DEFAULT_MULTIPLIER_32 + PCG_DEFAULT_INCREMENT_32) & MASK32\n",
" output = rotr16((state >> 16) ^ (state & MASK16), state >> 28)\n",
" yield output\n",
" \n",
" def simulation(self):\n",
" state = self.seed_var\n",
" while True:\n",
" state = state * PCG_DEFAULT_MULTIPLIER_32 + PCG_DEFAULT_INCREMENT_32\n",
" xsl = z3.Extract(31, 16, state) ^ z3.Extract(15, 0, state)\n",
" rot = z3.Extract(15, 0, state >> 28)\n",
" output = z3.RotateRight(xsl, rot)\n",
" yield output\n",
"\n",
" \n",
"class SimPCG32OneSeq(SimPRNG):\n",
" def __init__(self, seed_value=PCG_STATE_ONESEQ_64_INITIALIZER):\n",
" self.seed_value = seed_value\n",
" \n",
" self.seed_var = z3.BitVec('seed', 64)\n",
" self.variables = [(self.seed_var, self.seed_value)]\n",
" \n",
" def prng(self):\n",
" state = self.seed_value\n",
" while True:\n",
" state = (state * PCG_DEFAULT_MULTIPLIER_64 + PCG_DEFAULT_INCREMENT_64) & MASK64\n",
" output = rotr32((state >> 32) ^ (state & MASK32), state >> 59)\n",
" yield output\n",
" \n",
" def simulation(self):\n",
" state = self.seed_var\n",
" while True:\n",
" state = state * PCG_DEFAULT_MULTIPLIER_64 + PCG_DEFAULT_INCREMENT_64\n",
" xsl = z3.Extract(63, 32, state) ^ z3.Extract(31, 0, state)\n",
" rot = z3.Extract(31, 0, state >> 59)\n",
" output = z3.RotateRight(xsl, rot)\n",
" yield output"
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Expected values: {'seed': 5573589319906701683}\n"
]
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "08b1c2a009074901a0dbbb262bca93aa",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"HBox(children=(FloatProgress(value=0.0), HTML(value='')))"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Assertions:\n",
"(let ((a!1 (bvxor ((_ extract 63 32)\n",
" (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed)))\n",
" (bvadd #xf767814f (bvmul #x4c957f2d ((_ extract 31 0) seed)))))\n",
" (a!2 ((_ extract 31 0)\n",
" (bvashr (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed))\n",
" #x000000000000003b))))\n",
" (= (ext_rotate_right a!1 a!2) #xd42febc9))\n",
"\n",
"Statistics:\n",
"(:max-memory 129.83\n",
" :memory 27.74\n",
" :num-allocs 128009861869.00\n",
" :rlimit-count 1513636068\n",
" :sat-backjumps 65006\n",
" :sat-conflicts 65006\n",
" :sat-decisions 78632\n",
" :sat-del-clause 75647\n",
" :sat-elim-bool-vars-res 4870\n",
" :sat-elim-clauses 3250\n",
" :sat-elim-literals 5113\n",
" :sat-gc-clause 43203\n",
" :sat-minimized-lits 752846\n",
" :sat-mk-clause-2ary 13595\n",
" :sat-mk-clause-3ary 35132\n",
" :sat-mk-clause-nary 82529\n",
" :sat-mk-var 9303\n",
" :sat-probing-assigned 708\n",
" :sat-propagations-2ary 5513169\n",
" :sat-propagations-3ary 20808670\n",
" :sat-propagations-nary 14942501\n",
" :sat-restarts 6257\n",
" :sat-scc-elim-binary 168\n",
" :sat-subs-resolution 165\n",
" :sat-subs-resolution-dyn 37683\n",
" :sat-subsumed 7700\n",
" :sat-units 708\n",
" :time 5.96)\n",
"\n",
"Assertions:\n",
"(let ((a!1 (bvxor ((_ extract 63 32)\n",
" (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed)))\n",
" (bvadd #xf767814f (bvmul #x4c957f2d ((_ extract 31 0) seed)))))\n",
" (a!2 ((_ extract 31 0)\n",
" (bvashr (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed))\n",
" #x000000000000003b))))\n",
" (= (ext_rotate_right a!1 a!2) #xd42febc9))\n",
"(not (and (= #x5bc79915e375dbda seed)))\n",
"\n",
"Assertions:\n",
"(let ((a!1 (bvxor ((_ extract 63 32)\n",
" (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed)))\n",
" (bvadd #xf767814f (bvmul #x4c957f2d ((_ extract 31 0) seed)))))\n",
" (a!2 ((_ extract 31 0)\n",
" (bvashr (bvadd #x14057b7ef767814f (bvmul #x5851f42d4c957f2d seed))\n",
" #x000000000000003b))))\n",
" (= (ext_rotate_right a!1 a!2) #xd42febc9))\n",
"(let ((a!1 (bvxor ((_ extract 63 32)\n",
" (bvadd #x1a08ee1184ba6d32 (bvmul #x685f98a2018fade9 seed)))\n",
" (bvadd #x84ba6d32 (bvmul #x018fade9 ((_ extract 31 0) seed)))))\n",
" (a!2 ((_ extract 31 0)\n",
" (bvashr (bvadd #x1a08ee1184ba6d32 (bvmul #x685f98a2018fade9 seed))\n",
" #x000000000000003b))))\n",
" (= (ext_rotate_right a!1 a!2) #x1ae40535))\n",
"\n",
"Statistics:\n",
"(:added-eqs 3026\n",
" :arith-make-feasible 2\n",
" :arith-max-columns 4\n",
" :binary-propagations 160738587\n",
" :bv-bit2core 64\n",
" :bv-diseqs 14\n",
" :bv-dynamic-diseqs 2\n",
" :bv-dynamic-eqs 10\n",
" :bv->core-eq 3007\n",
" :conflicts 217339\n",
" :decisions 319815\n",
" :del-clause 194146\n",
" :final-checks 1\n",
" :max-memory 129.83\n",
" :memory 51.65\n",
" :minimized-lits 5472974\n",
" :mk-bool-var 19843\n",
" :mk-clause 262192\n",
" :num-allocs 161363282669.00\n",
" :num-checks 2\n",
" :propagations 456792511\n",
" :restarts 406\n",
" :rlimit-count 1951070608\n",
" :time 38.47)\n",
"\n"
]
},
{
"ename": "UnsolvedError",
"evalue": "Unsolved at 2 samples: canceled",
"output_type": "error",
"traceback": [
"\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
"\u001b[0;31mUnsolvedError\u001b[0m Traceback (most recent call last)",
"\u001b[0;32m<ipython-input-13-5a50857d8300>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[1;32m 2\u001b[0m \u001b[0;32massert\u001b[0m \u001b[0msim_pcg32\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mconfirm_simulation\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;36m1000\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 3\u001b[0m \u001b[0mprint\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34mf'Expected values: {sim_pcg32.gold_values}'\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m----> 4\u001b[0;31m \u001b[0msim_pcg32\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0msolve\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
"\u001b[0;32m<ipython-input-3-3d9cb9169d3e>\u001b[0m in \u001b[0;36msolve\u001b[0;34m(self, start_sample, max_samples, solver, verbose, simplify)\u001b[0m\n\u001b[1;32m 87\u001b[0m \u001b[0;32mif\u001b[0m \u001b[0mcheck_result\u001b[0m \u001b[0;34m==\u001b[0m \u001b[0mz3\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0munknown\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 88\u001b[0m \u001b[0mreason\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0msolver\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mreason_unknown\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m---> 89\u001b[0;31m \u001b[0;32mraise\u001b[0m \u001b[0mUnsolvedError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34mf\"Unsolved at {i} samples: {reason}\"\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m 90\u001b[0m \u001b[0;32melif\u001b[0m \u001b[0mcheck_result\u001b[0m \u001b[0;34m==\u001b[0m \u001b[0mz3\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0msat\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m 91\u001b[0m \u001b[0mmodel\u001b[0m \u001b[0;34m=\u001b[0m \u001b[0msolver\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mmodel\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
"\u001b[0;31mUnsolvedError\u001b[0m: Unsolved at 2 samples: canceled"
]
}
],
"source": [
"sim_pcg32 = SimPCG32OneSeq()\n",
"assert sim_pcg32.confirm_simulation(1000)\n",
"print(f'Expected values: {sim_pcg32.gold_values}')\n",
"#sim_pcg32.solve()"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {},
"outputs": [],
"source": []
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.6.13"
}
},
"nbformat": 4,
"nbformat_minor": 4
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment