Serial solver using Z3.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Example"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Using the constraints and computations specified in the binary, we'll write a Z3 script to give us our good serial."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Imports\n",
    "\n",
    "import z3"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Initialisation"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "# Initialising required variables\n",
    "\n",
    "# Z3's solver engine\n",
    "s = z3.Solver()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "We have to create an array such that operations could be done on it for the first transformation loop."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'(bvadd x #x02)'"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Declare a bitvector variable \n",
    "x = z3.BitVec('x', 8)\n",
    "\n",
    "# 'sexpr' method shows the internal representation.\n",
    "(x + 2).sexpr()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Which translates to: bit vector addition of x with the integral value 2."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "[serial_0,\n",
       " serial_1,\n",
       " serial_2,\n",
       " serial_3,\n",
       " serial_4,\n",
       " serial_5,\n",
       " serial_6,\n",
       " serial_7,\n",
       " serial_8,\n",
       " serial_9,\n",
       " serial_10,\n",
       " serial_11,\n",
       " serial_12]"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Input serial array of length 13, since the serial length is 13.\n",
    "serial = []\n",
    "\n",
    "for i in range(13):\n",
    "    serial.append(z3.BitVec(\"serial_{}\".format(i), 32))\n",
    "\n",
    "serial"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "# v4 initialised with 3.\n",
    "running_sum = [3]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Constraints"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Implementing constraints for the value boundations on every character in the input."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "for digit in serial:\n",
    "    s.add(z3.And(digit>48, digit<=57))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Check value of running sum at every iteration."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "sum_11"
      ],
      "text/plain": [
       "sum_11"
      ]
     },
     "execution_count": 7,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Append sum to a running sums array, and add it as a constraint at every interation.\n",
    "for i in range((len(serial)-1)):\n",
    "    current_sum = z3.BitVec(\"sum_{}\".format(i), 32)\n",
    "    s.add(current_sum==running_sum[-1]+((2*running_sum[-1])^(serial[i]-48)))\n",
    "    running_sum.append(current_sum)\n",
    "    \n",
    "running_sum[-1]"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Constraint on the last digit of the serial."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [],
   "source": [
    "s.add(serial[-1]==(running_sum[-1]%10+48))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### Constraint Solving"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Check if the problem is satisfiable."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<b>sat</b>"
      ],
      "text/plain": [
       "sat"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "s.check()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "[sum_3 = 247,\n",
       " sum_0 = 10,\n",
       " sum_5 = 2215,\n",
       " sum_6 = 6646,\n",
       " sum_7 = 19940,\n",
       " sum_1 = 27,\n",
       " sum_8 = 59823,\n",
       " sum_2 = 82,\n",
       " sum_9 = 179465,\n",
       " sum_4 = 736,\n",
       " sum_10 = 538396,\n",
       " serial_0 = 49,\n",
       " serial_5 = 55,\n",
       " serial_4 = 55,\n",
       " serial_11 = 52,\n",
       " serial_9 = 52,\n",
       " serial_3 = 49,\n",
       " serial_12 = 50,\n",
       " serial_10 = 49,\n",
       " serial_8 = 51,\n",
       " serial_7 = 50,\n",
       " serial_1 = 53,\n",
       " serial_6 = 49,\n",
       " serial_2 = 49,\n",
       " sum_11 = 1615192]"
      ],
      "text/plain": [
       "[sum_3 = 247,\n",
       " sum_0 = 10,\n",
       " sum_5 = 2215,\n",
       " sum_6 = 6646,\n",
       " sum_7 = 19940,\n",
       " sum_1 = 27,\n",
       " sum_8 = 59823,\n",
       " sum_2 = 82,\n",
       " sum_9 = 179465,\n",
       " sum_4 = 736,\n",
       " sum_10 = 538396,\n",
       " serial_0 = 49,\n",
       " serial_5 = 55,\n",
       " serial_4 = 55,\n",
       " serial_11 = 52,\n",
       " serial_9 = 52,\n",
       " serial_3 = 49,\n",
       " serial_12 = 50,\n",
       " serial_10 = 49,\n",
       " serial_8 = 51,\n",
       " serial_7 = 50,\n",
       " serial_1 = 53,\n",
       " serial_6 = 49,\n",
       " serial_2 = 49,\n",
       " sum_11 = 1615192]"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "if s.check() == z3.sat:\n",
    "    m = s.model()\n",
    "m"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Cleaning up and representing the answer in a readable form:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Serial object: [serial_0, serial_1, serial_2, serial_3, serial_4, serial_5, serial_6, serial_7, serial_8, serial_9, serial_10, serial_11, serial_12]\n",
      "Value of serial_0 is: 49\n",
      "Value of serial_1 is: 53\n",
      "Value of serial_2 is: 49\n",
      "Value of serial_3 is: 49\n",
      "Value of serial_4 is: 55\n",
      "Value of serial_5 is: 55\n",
      "Value of serial_6 is: 49\n",
      "Value of serial_7 is: 50\n",
      "Value of serial_8 is: 51\n",
      "Value of serial_9 is: 52\n",
      "Value of serial_10 is: 49\n",
      "Value of serial_11 is: 52\n",
      "Value of serial_12 is: 50\n"
     ]
    },
    {
     "data": {
      "text/plain": [
       "[49, 53, 49, 49, 55, 55, 49, 50, 51, 52, 49, 52, 50]"
      ]
     },
     "execution_count": 11,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "# Now m is a map. We dereference the values of serial required from it.\n",
    "print(\"Serial object:\", serial)\n",
    "\n",
    "inp = []\n",
    "for digit in serial:\n",
    "    # 'as_long' method used to convert vector value to long type.\n",
    "    print(\"Value of\", digit, \"is:\", m[digit])\n",
    "    inp.append(m[digit].as_long())\n",
    "    \n",
    "inp"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "These bytes give you the value of the good serial. Convert the ordinal values to their ASCII equivalents."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'1511771234142'"
      ]
     },
     "execution_count": 12,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "solution = \"\".join([chr(x) for x in inp])\n",
    "solution"
   ]
  }
 ],
 "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.8.2"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}