VFS.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# Verificação Formal de um Programa\n",
    "\n",
    "\n",
    "**Grupo 7:**\n",
    "\n",
    "- Luís Almeida A84180\n",
    "- João Pedro Antunes A86813 "
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    " Considere o seguinte programa, em Python anotado, para multiplicação de dois inteiros de precisão limitada a 16 bits.  Assume-se que os inteiros são representáveis na teoria `BitVecSort(16)` do Z3.\n",
    "\n",
    "```python\n",
    "           assume m >= 0 and n >= 0 and r == 0 and x == m and y == n \n",
    "        0: while y > 0:\n",
    "        1:    if y & 1 == 1: \n",
    "                    y , r  = y-1 , r+x\n",
    "        2:    x , y = x<<1  ,  y>>1\n",
    "        3: assert r == m * n ```\n",
    "\n",
    "   1. Usando  indução verifique a terminação deste programa.\n",
    "   2. Pretende-se verificar a correção parcial deste  programa usando duas formas alternativas para lidar com programas iterativos: havoc e  unfold.\n",
    "        1. Usando o comando havoc e a metodologia WPC  (weakest pre-condition) gere a condição de verificação que garanta a correção parcial.\n",
    "        2. Usando a metodologia SPC (strongest pos-condition), para um parâmetro inteiro $N$,  gere o fluxo que resulta do unfold do ciclo $N$  vezes e construa a respetiva condição de verificação. \n",
    "   3. Codifique, em SMT’s  e em ambos os casos, a verificação da correcção parcial."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Construção do FOTS que modela o programa"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Para usarmos indução e provarmos que o programa apresentado termina vamos começar por construir um FOTS que o modela. Temos então as variáveis $x,y,r,m,n$ que irão fazer parte do FOTS. Podemos ainda considerar uma variável $pc$ que nos indicará em que instrução nos encontramos. Define-se então a função que declara as variáveis do FOTS:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "from z3 import *\n",
    "\n",
    "\n",
    "def declare(i):\n",
    "    state = {}\n",
    "    \n",
    "    state['x'] = BitVec('x'+str(i),16)\n",
    "    state['y'] = BitVec('y'+str(i),16)\n",
    "    state['r'] = BitVec('r'+str(i),16)\n",
    "    state['m'] = BitVec('m'+str(i),16)\n",
    "    state['n'] = BitVec('n'+str(i),16)\n",
    "    state['pc'] = Int('pc'+str(i))\n",
    "    \n",
    "    return state"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Para definirmos o predicado *init* que determina o estado inicial do FOTS basta olharmos para a pré-condição do programa. Assim, o predicado *init* será:\n",
    "\n",
    "$$\n",
    " pc == 0 \\wedge m \\ge 0 \\wedge n \\ge 0 \\wedge r == 0 \\wedge x == m \\wedge y == n \n",
    "$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "def init(state):\n",
    "    l = []\n",
    "    \n",
    "    l.append(state['m'] >= 0)\n",
    "    l.append(state['n'] >= 0)\n",
    "    l.append(state['r'] == 0)\n",
    "    l.append(state['x'] == state['m'])\n",
    "    l.append(state['y'] == state['n'])\n",
    "    l.append(state['pc'] == 0)\n",
    "    \n",
    "    return And(l)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Defina-se agora a função de transição. Sabemos que, quando a variável $pc$ tiver o valor $0$, estamos na condição do ciclo, portanto $2$ situações podem ocorrer: transitar para dentro do ciclo caso a condição seja verdadeira ou transitar para o fim do programa caso a condição seja falsa. Estas situações correspondem aos predicados:\n",
    "\n",
    "$$\n",
    "pc == 0 \\wedge y \\gt 0 \\wedge y' == y \\wedge m' == m \\wedge r' == r \\wedge x' == x \\wedge n' == n \\wedge pc' == 1\n",
    "$$\n",
    "\n",
    "$$\n",
    "pc == 0 \\wedge y \\le 0 \\wedge y' == y \\wedge m' == m \\wedge r' == r \\wedge x' == x \\wedge n' == n \\wedge pc' == 3\n",
    "$$\n",
    "\n",
    "Ora, quando o valor de $pc$ for $1$, sabemos que entramos dentro do ciclo. A próxima instrução volta a ser uma condição e portanto, temos novamente duas situações: a condição é verdadeira e as variáveis $y$ e $r$ são alteradas ou então a condição é falsa e as variáveis $y$ e $r$ não são alteradas. Assim, temos os seguintes predicados:\n",
    "\n",
    "$$\n",
    "pc == 1 \\wedge \\quad y \\& 1 == 1 \\quad \\wedge \\quad y' == y - 1 \\quad \\wedge \\quad m' == m \\quad \\wedge \\quad r' == r + x \\quad \\wedge \n",
    "$$\n",
    "$$\n",
    "\\quad x' == x \\quad \\wedge \\quad n' == n \\quad \\wedge \\quad pc' == 2\n",
    "$$\n",
    "\n",
    "$$\n",
    "pc == 1 \\quad \\wedge \\quad \\neg(y \\& 1 == 1) \\quad \\wedge \\quad y' == y \\quad \\wedge \\quad m' == m \\quad \\wedge \\quad r' == r \\quad \\wedge \n",
    "$$\n",
    "$$ \n",
    "\\quad x' == x \\quad \\wedge \\quad n' == n \\quad \\wedge \\quad pc' == 2\n",
    "$$\n",
    "\n",
    "Quando o valor de $pc$ é $2$, temos apenas de executar as últimas instruções do ciclo e voltar a colocar o valor de $pc$ a $0$, para a condição de ciclo ser testada novamente.\n",
    "\n",
    "$$\n",
    "pc == 2 \\wedge y' == y >> 1 \\wedge m' == m \\wedge r' == r \\wedge x' == x << 1 \\wedge n' == n \\wedge pc' == 0\n",
    "$$\n",
    "\n",
    "Falta apenas adicionar o lacete final, em que o estado final transita para ele próprio:\n",
    "\n",
    "$$\n",
    "pc == 3 \\wedge y' == y \\wedge m' == m \\wedge r' == r \\wedge x' == x \\wedge n' == n \\wedge pc' == 3\n",
    "$$"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [],
   "source": [
    "def trans(curr,prox):\n",
    "    l = []\n",
    "    \n",
    "    l.append(And(curr['pc'] == 0, curr['y'] > 0, prox['y'] == curr['y'], prox['m'] == curr['m'],\n",
    "                 prox['r'] == curr['r'], prox['x'] == curr['x'], prox['n'] == curr['n'], prox['pc'] == 1))\n",
    "    \n",
    "    l.append(And(curr['pc'] == 0, curr['y'] <= 0, prox['y'] == curr['y'], prox['m'] == curr['m'],\n",
    "                 prox['r'] == curr['r'], prox['x'] == curr['x'], prox['n'] == curr['n'], prox['pc'] == 3))\n",
    "    \n",
    "    l.append(And(curr['pc'] == 1, curr['y'] & 1 == 1, prox['y'] == curr['y'] - 1,\n",
    "                 prox['r'] == curr['r'] + curr['x'], prox['x'] == curr['x'], prox['m'] == curr['m'],\n",
    "                prox['n'] == curr['n'], prox['pc'] == 2))\n",
    "    \n",
    "    l.append(And(curr['pc'] == 1, Not(curr['y'] & 1 == 1), prox['y'] == curr['y'],\n",
    "                 prox['r'] == curr['r'], prox['x'] == curr['x'], prox['m'] == curr['m'],\n",
    "                prox['n'] == curr['n'], prox['pc'] == 2))\n",
    "    \n",
    "    l.append(And(curr['pc'] == 2, prox['x'] == curr['x'] << 1, prox['y'] == curr['y'] >> 1,\n",
    "                prox['m'] == curr['m'], prox['n'] == curr['n'], prox['r'] == curr['r'], prox['pc'] == 0))\n",
    "    \n",
    "    l.append(And(curr['pc'] == 3, prox['y'] == curr['y'], prox['m'] == curr['m'],\n",
    "                 prox['r'] == curr['r'], prox['x'] == curr['x'], prox['n'] == curr['n'], prox['pc'] == 3))\n",
    "    \n",
    "    return Or(l)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "De seguida apresenta-se uma função que gera um traço de execução do FOTS construído"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0\n",
      "x = 512\n",
      "y = 39\n",
      "r = 0\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 0\n",
      "1\n",
      "x = 512\n",
      "y = 39\n",
      "r = 0\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 1\n",
      "2\n",
      "x = 512\n",
      "y = 38\n",
      "r = 512\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 2\n",
      "3\n",
      "x = 1024\n",
      "y = 19\n",
      "r = 512\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 0\n",
      "4\n",
      "x = 1024\n",
      "y = 19\n",
      "r = 512\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 1\n",
      "5\n",
      "x = 1024\n",
      "y = 18\n",
      "r = 1536\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 2\n",
      "6\n",
      "x = 2048\n",
      "y = 9\n",
      "r = 1536\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 0\n",
      "7\n",
      "x = 2048\n",
      "y = 9\n",
      "r = 1536\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 1\n",
      "8\n",
      "x = 2048\n",
      "y = 8\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 2\n",
      "9\n",
      "x = 4096\n",
      "y = 4\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 0\n",
      "10\n",
      "x = 4096\n",
      "y = 4\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 1\n",
      "11\n",
      "x = 4096\n",
      "y = 4\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 2\n",
      "12\n",
      "x = 8192\n",
      "y = 2\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 0\n",
      "13\n",
      "x = 8192\n",
      "y = 2\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 1\n",
      "14\n",
      "x = 8192\n",
      "y = 2\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 2\n",
      "15\n",
      "x = 16384\n",
      "y = 1\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 0\n",
      "16\n",
      "x = 16384\n",
      "y = 1\n",
      "r = 3584\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 1\n",
      "17\n",
      "x = 16384\n",
      "y = 0\n",
      "r = 19968\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 2\n",
      "18\n",
      "x = 32768\n",
      "y = 0\n",
      "r = 19968\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 0\n",
      "19\n",
      "x = 32768\n",
      "y = 0\n",
      "r = 19968\n",
      "m = 512\n",
      "n = 39\n",
      "pc = 3\n"
     ]
    }
   ],
   "source": [
    "def gera_traco(declare,init,trans,k):\n",
    "    trace = [declare(i) for i in range(k)]\n",
    "    s = Solver()\n",
    "    \n",
    "    s.add(init(trace[0]))\n",
    "    \n",
    "    for i in range(k-1):\n",
    "        s.add(trans(trace[i],trace[i+1]))\n",
    "    \n",
    "    r = s.check()\n",
    "    if r == sat:\n",
    "        m = s.model()\n",
    "        for i in range(k):\n",
    "            print(i)\n",
    "            for v in trace[i]:\n",
    "                print(v, '=', m[trace[i][v]])\n",
    "        return\n",
    "    \n",
    "    print('UNSAT')\n",
    "    return \n",
    "\n",
    "gera_traco(declare,init,trans,20)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Prova da terminação do programa\n",
    "\n",
    "Vamos então utilizar indução para demonstrar que o programa termina. Como queremos provar uma propriedade de *liveness*, podemos utilizar *k-lookahead* para fazer esta demonstração. Ora, temos portanto de encontrar um variante $V$ que satisfaça as seguintes condições:\n",
    "\n",
    "- O variante é sempre positivo, ou seja, $G\\ (V(s) \\ge 0)$\n",
    "- O variante descresce sempre (estritamente) ou atinge o valor 0, ou seja, $G\\ (\\forall s' . \\mathit{trans}(s,s') \\rightarrow (V(s') < V(s) \\vee V(s') = 0))$\n",
    "- Quando o variante é 0 verifica-se necessariamente $\\phi$, ou seja, $G\\ (V(s)=0 \\rightarrow \\phi(s))$\n",
    "\n",
    "No entanto, como vamos utilizar *k-lookahead*, acabamos por relaxar a $2º$ condição e permitir que o variante decresça apenas de $3$ em $3$ transições. Considera-se um lookahead de $3$ pois é o valor que nos permite \"saltar\" o corpo do ciclo na última iteração. Sendo assim, podemos utilizar o variante:\n",
    "\n",
    "$$\n",
    "V(s) \\equiv \\quad y_{s} - pc_{s} + 3\n",
    "$$\n",
    "\n",
    "Comecemos por provar que $V$ é sempre positivo:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Verifica-se\n"
     ]
    }
   ],
   "source": [
    "def variante(state):\n",
    "    return BV2Int(state['y']) - state['pc'] + 3\n",
    "\n",
    "def kinduction_always(declare,init,trans,inv,k):\n",
    "    trace = [declare(i) for i in range(k+1)]\n",
    "    s = Solver()\n",
    "    s.add(init(trace[0]))  \n",
    "    for i in range(k-1):                     \n",
    "        s.add(trans(trace[i],trace[i+1]))\n",
    "    \n",
    "    l = [Not(inv(trace[i])) for i in range(k)]\n",
    "    \n",
    "    s.add(Or(l))\n",
    "    \n",
    "    r = s.check()\n",
    "    \n",
    "    if r == sat:\n",
    "        print('Falhou no caso base')\n",
    "        m = s.model()\n",
    "        for i in range(k):\n",
    "            print(i)\n",
    "            for v in trace[i]:\n",
    "                print(v,m[trace[i][v]])\n",
    "        return\n",
    "    \n",
    "    s = Solver()\n",
    "    for i in range(k):\n",
    "        s.add(trans(trace[i],trace[i+1]))\n",
    "        s.add(inv(trace[i]))\n",
    "    s.add(Not(inv(trace[k])))\n",
    "    \n",
    "    r = s.check()\n",
    "    \n",
    "    if r == sat:\n",
    "        print('Falhou no passo de k-indução')\n",
    "        return\n",
    "    \n",
    "    if r == unsat:\n",
    "        print('Verifica-se')\n",
    "        return\n",
    "    return\n",
    "\n",
    "def positivo(state):\n",
    "    return variante(state) >= 0\n",
    "\n",
    "kinduction_always(declare,init,trans,positivo,3)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "De seguida, temos de provar a $2º$ condição, ou seja, $V$ decresce de $3$ em $3$ transições:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Verifica-se\n"
     ]
    }
   ],
   "source": [
    "def decresce(state):\n",
    "    state1 = declare(-1)\n",
    "    state2 = declare(-2)\n",
    "    state3 = declare(-3)\n",
    "    \n",
    "    return ForAll(list(state1.values()) + list(state2.values()) + list(state3.values()),\n",
    "                  Implies(And(trans(state,state1),trans(state1,state2),trans(state2,state3))\n",
    "                                                ,Or(variante(state3) < variante(state), variante(state3) == 0)))\n",
    "\n",
    "kinduction_always(declare,init,trans,decresce,3)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Finalmente, prova-se que quando $V$ tem o valor $0$, o programa termina:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Verifica-se\n"
     ]
    }
   ],
   "source": [
    "def term(state):\n",
    "    return Implies(variante(state) == 0, state['pc'] == 3)\n",
    "\n",
    "kinduction_always(declare,init,trans,term,4)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## Verificação da Correção Parcial do programa"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Comecemos por provar a correção parcial do programa utilizando o comando *havoc* e a metodologia *WPC*.\n",
    "Na metodologia *havoc*, o ciclo (${\\sf while} \\; b \\;{\\sf do }\\{\\theta\\} \\;C$), com um invariante $\\theta$ é transformado num fluxo não iterativo da seguinte forma: \n",
    "\n",
    "$$\n",
    "{{\\sf assert}\\; \\theta\\; ; \\sf havoc }\\;\\vec{x} \\; ; (\\,({\\sf assume }\\; b \\wedge \\theta \\; ; \\; C \\; ; {\\sf assert}\\;\\theta \\; ; {\\sf assume}\\; \\mathit{False}) \\: || \\:\n",
    "{\\sf assume}\\; \\neg b \\wedge \\theta \\,)\n",
    "$$\n",
    "\n",
    "Assim, temos agora de definir um invariante $\\theta$. Seja $\\theta \\equiv m * n == x * y + r \\wedge y \\ge 0$. Desta forma podemos traduzir o programa na seguinte linguagem de fluxos:\n",
    "\n",
    "```python\n",
    "assume m >= 0 and n >= 0 and r == 0 and x == m and y == n;\n",
    "assert m * n == x * y + r and y >= 0;\n",
    "havoc x; havoc y;\n",
    "\n",
    "(assume y > 0 and m * n == x * y + r and y >= 0; \n",
    "(assume y & 1 == 1; y,r = y -1, r + x; \n",
    "|| assume not(y & 1 == 1); skip;); x, y = x << 1, y >> 1;\n",
    "assert m * n == x * y + r and y >= 0; assume False;\n",
    "||\n",
    "assume not(y > 0) and m * n == x * y + r and y >= 0;\n",
    ")\n",
    "assert r == m * n;\n",
    "```\n",
    "Ora, vamos agora utilizar as regras da metodologia *WPC* para gerar a condição de verificação:\n",
    "\n",
    "$$\n",
    "[{\\sf skip}] = True\n",
    "$$\n",
    "$$\n",
    "[{\\sf assume}\\:\\phi] = True\n",
    "$$\n",
    "$$\n",
    "[{\\sf assert}\\:\\phi] = \\phi\n",
    "$$\n",
    "$$\n",
    "[ x = e ] = True\n",
    "$$\n",
    "$$\n",
    "[(C_1 || C_2)] = [C_1] \\wedge [C_2]\n",
    "$$\n",
    "$$\n",
    "[{\\sf skip}\\, ; C] = [C]\n",
    "$$\n",
    "$$\n",
    "[{\\sf assume}\\:\\phi\\, ; C] = \\phi \\to [C]\n",
    "$$\n",
    "$$\n",
    "[{\\sf assert}\\:\\phi\\, ; C] = \\phi \\wedge [C]\n",
    "$$\n",
    "$$\n",
    "[ x = e \\, ; C] = [C][e/x]\n",
    "$$\n",
    "$$\n",
    "[(C_1 || C_2)\\, ; C] = [(C_1 ; C) || (C_2 ; C)]\n",
    "$$\n",
    "\n",
    "```python\n",
    "m >= 0 and n >= 0 and r == 0 and x == m and y == n ->\n",
    "m * n == x * y + r and\n",
    "forall x forall y\n",
    "\n",
    "(y > 0 and m * n == x * y + r ->  \n",
    "(y & 1 == 1 -> m * n == x * y + r and False -> r == m * n)[y-1/y][r+x/r][x<<1/x][y>>1/y] and \n",
    "not(y & 1 == 1) -> (m * n == x * y + r and False -> r == m * n)[x<<1/x][y>>1/y]\n",
    "and\n",
    "not(y > 0) and m * n == x * y + r -> r == m * n)\n",
    "```\n",
    "\n",
    "De seguida implementamos esta fórmula no *z3* e tentamos provar a sua veracidade:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "'Valid'"
      ]
     },
     "execution_count": 15,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "def prove(f):\n",
    "    s = Solver()\n",
    "    s.add(Not(f))\n",
    "    if s.check() == unsat:\n",
    "        return \"Valid\"\n",
    "    \n",
    "    if s.check() == sat:\n",
    "        mod = s.model()\n",
    "        \n",
    "        print('x = ' + str(mod[x].as_long()))\n",
    "        print('y = ' + str(mod[y].as_long()))\n",
    "        print('m = ' + str(mod[m].as_long()))\n",
    "        print('n = ' + str(mod[n].as_long()))\n",
    "        print('r = ' + str(mod[r].as_long()))\n",
    "        \n",
    "        return \"False\"\n",
    "    \n",
    "    return \"Unknown\"\n",
    "\n",
    "x,y,m,n,r = BitVecs(\"x y m n r\",8)\n",
    "\n",
    "pre = And(m >= 0, n >= 0, r == 0, x == m, y == n)\n",
    "\n",
    "pos = (r == m * n)\n",
    "\n",
    "inv = And(m * n == x * y + r, y>=0)\n",
    "\n",
    "f4 = Implies(y & 1 == 1,substitute(substitute(substitute(substitute(inv,(y,y>>1)),(x,x<<1)),(r,r+x)),(y,y-1)))\n",
    "\n",
    "f5 = Implies(Not(y & 1 == 1),substitute(substitute(inv,(y,y>>1)),(x,x<<1)))\n",
    "\n",
    "f2 = Implies(And(y > 0, inv),And(f4,f5))\n",
    "\n",
    "f3 = Implies(And(Not(y > 0), inv), pos)\n",
    "\n",
    "resto = ForAll([x,y],f2)\n",
    "\n",
    "F = Implies(pre,And(inv,resto,f3))\n",
    "\n",
    "\n",
    "prove(F)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Vamos agora utilizar a metodologia *SPC* e a técnica de *unfold*. Esta técnica consiste em desenrolar o ciclo $k$-vezes, adicionando uma *unwinding assertion* para verificar que não existem execuções que exigem mais do que $k$-iterações ou uma *unwinding assumption* para excluir as execuções que exigem mais do que $k$-iterações para serem verificadas.\n",
    "$$\n",
    "\\begin{array}{ll|ll}\n",
    "{\\sf if} \\; b \\;{\\sf then } \\;C; & \\quad & \\quad & {\\sf if} \\; b \\;{\\sf then } \\;C; \\\\\n",
    "\\quad {\\sf if} \\; b \\;{\\sf then } \\;C; &\\quad & \\quad & \\quad {\\sf if} \\; b \\;{\\sf then } \\;C; \\\\\n",
    "\\qquad \\ldots &\\quad & \\quad & \\qquad \\ldots \\\\\n",
    "\\quad \\qquad {\\sf if} \\; b \\;{\\sf then } \\;\\{C\\;; {\\sf assert}\\; \\neg b \\} &\\quad & \\quad & \\quad \\qquad {\\sf if} \\; b \\;{\\sf then } \\;\\{C\\;; {\\sf assume}\\; \\neg b \\}\n",
    "\\end{array}\n",
    "$$\n",
    "\n",
    "Como sabemos que no fim de cada iteração do ciclo é feito um *shift-right* do BitVec $y$ e que este tem no máximo $16 bits$, então o ciclo irá ter no máximo $16$ iterações. Sendo assim, apresenta-se um exemplo de um *unfold* do ciclo de $16$ convertido para SA:\n",
    "\n",
    "``` python\n",
    "    assume m0 >= 0 and n0 >= 0 and r0 == 0 and x0 == m0 and y0 == n0;\n",
    "    \n",
    "    if(y0 > 0):                      #1\n",
    "       if y0 & 1 == 1: \n",
    "             y1 , r1  = y0-1 , r0+x0;\n",
    "       else:\n",
    "           y1 = y0;\n",
    "           r1 = r0;\n",
    "        \n",
    "       x1 , y2 = x0<<1  ,  y1>>1;\n",
    "       \n",
    "        if(y2 > 0):                   #2\n",
    "           if y1 & 1 == 1: \n",
    "                 y3 , r2  = y2-1 , r1+x1;\n",
    "           else:\n",
    "            y3 = y2;\n",
    "            r2 = r1;\n",
    "            \n",
    "           x2 , y4 = x1<<1  ,  y3>>1;\n",
    "            \n",
    "            if(y4 > 0):                   #3\n",
    "               if y4 & 1 == 1: \n",
    "                    y5 , r3  = y4-1 , r2+x2;\n",
    "               \n",
    "               else:\n",
    "                y5 = y4;\n",
    "                r3 = r2;\n",
    "                \n",
    "               x3 , y6 = x2<<1  ,  y5>>1;\n",
    "                \n",
    "                if(y6 > 0):                   #4\n",
    "                   if y6 & 1 == 1: \n",
    "                     y7 , r4  = y6-1 , r3+x3;\n",
    "                   \n",
    "                   else:\n",
    "                    y7 = y6;\n",
    "                    r4 = r3;\n",
    "                    \n",
    "                   x4 , y8 = x3<<1  ,  y7>>1;\n",
    "                \n",
    "                    if(y8 > 0):                   #5\n",
    "                       if y8 & 1 == 1: \n",
    "                         y9 , r5  = y8-1 , r4+x4;\n",
    "                    \n",
    "                       else:\n",
    "                        y9 = y8;\n",
    "                        r5 = r4;\n",
    "                        \n",
    "                       x5 , y10 = x4<<1  ,  y9>>1;\n",
    "                    \n",
    "                        if(y10 > 0):                   #6\n",
    "                           if y10 & 1 == 1: \n",
    "                             y11 , r6  = y10-1 , r5+x5;\n",
    "                           \n",
    "                           else:\n",
    "                            y11 = y10;\n",
    "                            r6 = r5;\n",
    "                            \n",
    "                           x6 , y12 = x5<<1  ,  y11>>1;\n",
    "                        \n",
    "                            if(y12 > 0):                   #7\n",
    "                               if y12 & 1 == 1: \n",
    "                                 y13 , r7  = y12-1 , r6+x6;\n",
    "                                \n",
    "                               else:\n",
    "                                y13 = y12;\n",
    "                                r7 = r6;\n",
    "                                \n",
    "                               x7 , y14 = x6<<1  ,  y13>>1;\n",
    "                            \n",
    "                                if(y14 > 0):                   #8\n",
    "                                   if y14 & 1 == 1: \n",
    "                                     y15 , r8  = y14-1 , r7+x7;\n",
    "                                   \n",
    "                                   else:\n",
    "                                    y15 = y14;\n",
    "                                    r8 = r7;\n",
    "                                    \n",
    "                                   x8 , y16 = x7<<1  ,  y15>>1;\n",
    "                                \n",
    "                                    if(y16 > 0):                   #9\n",
    "                                       if y16 & 1 == 1: \n",
    "                                         y17 , r9  = y16-1 , r8+x8;\n",
    "                                            \n",
    "                                       else:\n",
    "                                        y17 = y16;\n",
    "                                        r9 = r8;\n",
    "                                        \n",
    "                                       x9 , y18 = x8<<1  ,  y17>>1;\n",
    "                                    \n",
    "                                        if(y18 > 0):                   #10\n",
    "                                           if y18 & 1 == 1: \n",
    "                                             y19 , r10  = y18-1 , r9+x9;\n",
    "                                           \n",
    "                                           else:\n",
    "                                            y19 = y18;\n",
    "                                            r10 = r9;\n",
    "                                            \n",
    "                                           x10 , y20 = x9<<1  ,  y19>>1;\n",
    "                                        \n",
    "                                            if(y20 > 0):                   #11\n",
    "                                               if y20 & 1 == 1: \n",
    "                                                 y21 , r11  = y20-1 , r10+x10;\n",
    "                                               \n",
    "                                               else:\n",
    "                                                y21 = y20;\n",
    "                                                r11 = r10;\n",
    "                                                \n",
    "                                               x11 , y22 = x10<<1  ,  y21>>1;\n",
    "                                            \n",
    "                                                if(y22 > 0):                   #12\n",
    "                                                   if y22 & 1 == 1: \n",
    "                                                     y23 , r12  = y22-1 , r11+x11;\n",
    "                                                        \n",
    "                                                   else:\n",
    "                                                    y23 = y22;\n",
    "                                                    r12 = r11;\n",
    "                                                    \n",
    "                                                   x12 , y24 = x12<<1  ,  y23>>1;\n",
    "                                                \n",
    "                                                    if(y24 > 0):                   #13\n",
    "                                                       if y24 & 1 == 1: \n",
    "                                                         y25 , r13  = y24-1 , r12+x12;\n",
    "                                                       \n",
    "                                                       else:\n",
    "                                                        y25 = y24;\n",
    "                                                        r13 = r12;\n",
    "                                                        \n",
    "                                                       x13 , y26 = x12<<1  ,  y25>>1;\n",
    "                                                    \n",
    "                                                        if(y26 > 0):                   #14\n",
    "                                                           if y26 & 1 == 1: \n",
    "                                                             y27 , r14  = y26-1 , r13+x13;\n",
    "                                                                \n",
    "                                                           else:\n",
    "                                                            y27 = y26;\n",
    "                                                            r14 = r13;\n",
    "                                                            \n",
    "                                                           x14 , y28 = x13<<1  ,  y27>>1;\n",
    "                                                        \n",
    "                                                            if(y28 > 0):                   #15\n",
    "                                                               if y28 & 1 == 1: \n",
    "                                                                 y29 , r15  = y28-1 , r14+x14;\n",
    "                                                               \n",
    "                                                               else:\n",
    "                                                                y29 = y28;\n",
    "                                                                r15 = r14;\n",
    "                                                                \n",
    "                                                               x15 , y30 = x14<<1  ,  y29>>1;\n",
    "                                                            \n",
    "                                                                if(y30 > 0):                   #16\n",
    "                                                                   if y30 & 1 == 1: \n",
    "                                                                     y31 , r16  = y30-1 , r15+x15;\n",
    "                                                                    \n",
    "                                                                   else:\n",
    "                                                                    y31 = y30;\n",
    "                                                                    r16 = r15;\n",
    "                                                                    \n",
    "                                                                   x16 , y32 = x15<<1  ,  y31>>1;\n",
    "                                                                   assert not(y32>0);\n",
    "                                                                \n",
    "                                                                else:\n",
    "                                                                    r16 = r15;\n",
    "        \n",
    "                                                            else:\n",
    "                                                                r16 = r14;\n",
    "            \n",
    "                                                        else:\n",
    "                                                            r16 = r13;\n",
    "                \n",
    "                                                    else:\n",
    "                                                        r16 = r12;\n",
    "                \n",
    "                                                else:\n",
    "                                                    r16 = r11;\n",
    "                        \n",
    "                                            else:\n",
    "                                                r16 = r10;\n",
    "                            \n",
    "                                        else:\n",
    "                                            r16 = r9;\n",
    "                                \n",
    "                                    else:\n",
    "                                        r16 = r8;\n",
    "                                    \n",
    "                                else:\n",
    "                                    r16 = r7;\n",
    "                                        \n",
    "                            else:\n",
    "                                r16 = r6;\n",
    "                                            \n",
    "                        else:\n",
    "                            r16 = r5;\n",
    "                                                \n",
    "                    else:\n",
    "                        r16 = r4;\n",
    "                                                    \n",
    "                else:\n",
    "                    r16 = r3;\n",
    "                                                        \n",
    "            else:\n",
    "                r16 = r2;\n",
    "                                                            \n",
    "        else:\n",
    "            r16 = r1;\n",
    "                                                                \n",
    "    else:\n",
    "        r16 = r0;\n",
    "                                                                    \n",
    "        \n",
    "    assert r16 == m0 * n0;\n",
    "```\n",
    "\n",
    "No entanto, a anotação gerada acima engloba os casos em que o ciclo não é executado $16$ vezes, pelo que não irá representar a anotação em linguagem de fluxos que modela a execução do ciclo $16$ vezes. Neste caso específico não existirão alternativas aos \"*if*\" que testam a continuidade do ciclo, ou seja, força-se que o ciclo corra $16$ vezes. Temos então a seguinte anotação em linguagem de fluxos:\n",
    "\n",
    "``` python\n",
    "assume m0 >= 0 and n0 >= 0 and r0 == 0 and x0 == m0 and y0 == n0;\n",
    "assume y0 > 0;\n",
    "(  assume y0 & 1 == 1;\n",
    "  y1 = y0 - 1;\n",
    "  r1 = r0 + x0;\n",
    " \n",
    "||\n",
    "  assume not(y0 & 1 == 1);\n",
    "  y1 = y0;\n",
    "  r1 = r0;\n",
    ");\n",
    "y2 = y1 >> 1;\n",
    "x1 = x0 << 1;\n",
    "assume y2 > 0;\n",
    "(  assume y2 & 1 == 1;\n",
    "  y3 = y2 - 1;\n",
    "  r2 = r1 + x1;\n",
    " \n",
    "||\n",
    "  assume not(y2 & 1 == 1);\n",
    "  y3 = y2;\n",
    "  r2 = r1;\n",
    ");\n",
    "y4 = y3 >> 1;\n",
    "x2 = x1 << 1;\n",
    "assume y4 > 0;\n",
    "(  assume y4 & 1 == 1;\n",
    "  y5 = y4 - 1;\n",
    "  r3 = r2 + x2;\n",
    " \n",
    "||\n",
    "  assume not(y4 & 1 == 1);\n",
    "  y5 = y4;\n",
    "  r3 = r2;\n",
    ");\n",
    "y6 = y5 >> 1;\n",
    "x3 = x2 << 1;\n",
    "assume y6 > 0;\n",
    "(  assume y6 & 1 == 1;\n",
    "  y7 = y6 - 1;\n",
    "  r4 = r3 + x3;\n",
    " \n",
    "||\n",
    "  assume not(y6 & 1 == 1);\n",
    "  y7 = y6;\n",
    "  r4 = r3;\n",
    ");\n",
    "y8 = y7 >> 1;\n",
    "x4 = x3 << 1;\n",
    "assume y8 > 0;\n",
    "(  assume y8 & 1 == 1;\n",
    "  y9 = y8 - 1;\n",
    "  r5 = r4 + x4;\n",
    " \n",
    "||\n",
    "  assume not(y8 & 1 == 1);\n",
    "  y9 = y8;\n",
    "  r5 = r4;\n",
    ");\n",
    "y10 = y9 >> 1;\n",
    "x5 = x4 << 1;\n",
    "assume y10 > 0;\n",
    "(  assume y10 & 1 == 1;\n",
    "  y11 = y10 - 1;\n",
    "  r6 = r5 + x5;\n",
    " \n",
    "||\n",
    "  assume not(y10 & 1 == 1);\n",
    "  y11 = y10;\n",
    "  r6 = r5;\n",
    ");\n",
    "y12 = y11 >> 1;\n",
    "x6 = x5 << 1;\n",
    "assume y12 > 0;\n",
    "(  assume y12 & 1 == 1;\n",
    "  y13 = y12 - 1;\n",
    "  r7 = r6 + x6;\n",
    " \n",
    "||\n",
    "  assume not(y12 & 1 == 1);\n",
    "  y13 = y12;\n",
    "  r7 = r6;\n",
    ");\n",
    "y14 = y13 >> 1;\n",
    "x7 = x6 << 1;\n",
    "assume y14 > 0;\n",
    "(  assume y14 & 1 == 1;\n",
    "  y15 = y14 - 1;\n",
    "  r8 = r7 + x7;\n",
    " \n",
    "||\n",
    "  assume not(y14 & 1 == 1);\n",
    "  y15 = y14;\n",
    "  r8 = r7;\n",
    ");\n",
    "y16 = y15 >> 1;\n",
    "x8 = x7 << 1;\n",
    "assume y16 > 0;\n",
    "(  assume y16 & 1 == 1;\n",
    "  y17 = y16 - 1;\n",
    "  r9 = r8 + x8;\n",
    " \n",
    "||\n",
    "  assume not(y16 & 1 == 1);\n",
    "  y17 = y16;\n",
    "  r9 = r8;\n",
    ");\n",
    "y18 = y17 >> 1;\n",
    "x9 = x8 << 1;\n",
    "assume y18 > 0;\n",
    "(  assume y18 & 1 == 1;\n",
    "  y19 = y18 - 1;\n",
    "  r10 = r9 + x9;\n",
    " \n",
    "||\n",
    "  assume not(y18 & 1 == 1);\n",
    "  y19 = y18;\n",
    "  r10 = r9;\n",
    ");\n",
    "y20 = y19 >> 1;\n",
    "x10 = x9 << 1;\n",
    "assume y20 > 0;\n",
    "(  assume y20 & 1 == 1;\n",
    "  y21 = y20 - 1;\n",
    "  r11 = r10 + x10;\n",
    " \n",
    "||\n",
    "  assume not(y20 & 1 == 1);\n",
    "  y21 = y20;\n",
    "  r11 = r10;\n",
    ");\n",
    "y22 = y21 >> 1;\n",
    "x11 = x10 << 1;\n",
    "assume y22 > 0;\n",
    "(  assume y22 & 1 == 1;\n",
    "  y23 = y22 - 1;\n",
    "  r12 = r11 + x11;\n",
    " \n",
    "||\n",
    "  assume not(y22 & 1 == 1);\n",
    "  y23 = y22;\n",
    "  r12 = r11;\n",
    ");\n",
    "y24 = y23 >> 1;\n",
    "x12 = x11 << 1;\n",
    "assume y24 > 0;\n",
    "(  assume y24 & 1 == 1;\n",
    "  y25 = y24 - 1;\n",
    "  r13 = r12 + x12;\n",
    " \n",
    "||\n",
    "  assume not(y24 & 1 == 1);\n",
    "  y25 = y24;\n",
    "  r13 = r12;\n",
    ");\n",
    "y26 = y25 >> 1;\n",
    "x13 = x12 << 1;\n",
    "assume y26 > 0;\n",
    "(  assume y26 & 1 == 1;\n",
    "  y27 = y26 - 1;\n",
    "  r14 = r13 + x13;\n",
    " \n",
    "||\n",
    "  assume not(y26 & 1 == 1);\n",
    "  y27 = y26;\n",
    "  r14 = r13;\n",
    ");\n",
    "y28 = y27 >> 1;\n",
    "x14 = x13 << 1;\n",
    "assume y28 > 0;\n",
    "(  assume y28 & 1 == 1;\n",
    "  y29 = y28 - 1;\n",
    "  r15 = r14 + x14;\n",
    " \n",
    "||\n",
    "  assume not(y28 & 1 == 1);\n",
    "  y29 = y28;\n",
    "  r15 = r14;\n",
    ");\n",
    "y30 = y29 >> 1;\n",
    "x15 = x14 << 1;\n",
    "assume y30 > 0;\n",
    "(  assume y30 & 1 == 1;\n",
    "  y31 = y30 - 1;\n",
    "  r16 = r15 + x15;\n",
    " \n",
    "||\n",
    "  assume not(y30 & 1 == 1);\n",
    "  y31 = y30;\n",
    "  r16 = r15;\n",
    ");\n",
    "y32 = y31 >> 1;\n",
    "x16 = x15 << 1;\n",
    "assert r16 == m0 * n0 and not(y32 > 0);\n",
    "```\n",
    "\n",
    "Ora, resta-nos agora utilizar a metodologia *SPC* para gerar a condição de verificação do programa. Temos:\n",
    "\n",
    "$$\n",
    "[{\\sf skip}] = True\n",
    "$$\n",
    "$$\n",
    "[{\\sf assume}\\:\\phi] = \\phi\n",
    "$$\n",
    "$$\n",
    "[{\\sf assert}\\:\\phi] = \\phi\n",
    "$$\n",
    "$$\n",
    "[x = e ] = (x = e)\n",
    "$$\n",
    "$$\n",
    "[(C_1 || C_2)] = [C_1] \\vee [C_2]\n",
    "$$\n",
    "$$\n",
    "[C \\, ; {\\sf skip}\\;] = [C]\n",
    "$$\n",
    "$$\n",
    "[C \\, ;{\\sf assume}\\:\\phi] = [C] \\wedge \\phi\n",
    "$$\n",
    "$$\n",
    "[C \\, ;{\\sf assert}\\:\\phi] = [C] \\to \\phi\n",
    "$$\n",
    "$$\n",
    "[ C \\, ; x = e ] = [C] \\wedge (x = e)\n",
    "$$\n",
    "$$\n",
    "[C\\,; (C_1 || C_2)] = [(C ; C_1) || (C; C_2)]\n",
    "$$\n",
    "\n",
    "\n",
    "No entanto, devido à dimensão da fórmula lógica a ser gerada, resolvemos automatizar este processo com algumas funções:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [],
   "source": [
    "def SPC(inst):\n",
    "\treturn SPCaux(inst)[0]\n",
    "\n",
    "\n",
    "def SPCaux(inst):\n",
    "\tif not inst:\n",
    "\t\treturn False,False\n",
    "\n",
    "\th = inst[-1]\n",
    "\ttyp,pars = h \n",
    "\t\n",
    "\tif typ == \"alternative\":\n",
    "\t\tlef = SPCaux(inst[:-1] + pars[0])\n",
    "\t\trig = SPCaux(inst[:-1] + pars[1])\n",
    "\t\trzt = Or(lef[0],rig[0])\n",
    "\n",
    "\t\treturn rzt,True\n",
    "\n",
    "\n",
    "\t\n",
    "\tzt,h = SPCaux(inst[:-1])\n",
    "\tif h:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trzt = And(zt,pars[0])\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trzt = Implies(zt,pars[0])\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trzt = zt\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trzt = And(zt,pars[0] == pars[2])\n",
    "\n",
    "\telse:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trzt = pars[0]\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trzt = pars[0]\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trzt = True\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trzt = pars[0] == pars[2]\n",
    "\n",
    "\treturn rzt,True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Podemos olhar para o programa como uma lista de comandos à qual temos de aplicar certas regras. Então podemos iterar esta lista seguindo as regras da *SPC* para gerar a fórmula em *z3* que modela a condição de verificação. É apenas este procedimento que a função SPC() implementa. Acabamos por fazer o mesmo para a metodologia *WPC*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "def WPC(inst):\n",
    "\treturn WPCaux(inst)[0]\n",
    "\n",
    "\n",
    "def WPCaux(inst):\n",
    "\tif not inst:\n",
    "\t\treturn False,False\n",
    "\n",
    "\ttyp,pars = inst[0]\n",
    "\t\n",
    "\tif typ == \"alternative\":\n",
    "\t\te = pars[0].copy()\n",
    "\t\td = pars[1].copy()\n",
    "\t\te.extend(inst[1:])\n",
    "\t\td.extend(inst[1:])\n",
    "\t\tlef = WPCaux(e)\n",
    "\t\trig = WPCaux(d)\n",
    "\n",
    "\t\trzt = And(lef[0],rig[0])\n",
    "\t\treturn rzt,True\n",
    "\n",
    "\n",
    "\tzt,h = WPCaux(inst[1:])\n",
    "\tif h:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trzt = Implies(pars[0],zt)\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trzt = And(pars[0],zt)\n",
    "\n",
    "\t\telif typ == \"havoc\":\n",
    "\t\t\trzt = ForAll(pars[0],zt)\n",
    "\n",
    "\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trzt = zt\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trzt = substitute(zt,(pars[0],pars[2]))\n",
    "\n",
    "\telse:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trzt = BoolVal(True)\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trzt = pars[0]\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trzt = BoolVal(True)\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trzt = BoolVal(True)\n",
    "\n",
    "\treturn rzt,True\n"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Podemos também escrever uma função que gere a tradução em linguagem de fluxos do nosso programa:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [],
   "source": [
    "def FLOW(inst):\n",
    "\treturn FLOWaux(inst,0)\n",
    "\n",
    "\n",
    "\n",
    "def FLOWaux(inst,ident):\n",
    "\tif not inst:\n",
    "\t\treturn \"\"\n",
    "\n",
    "\th = inst[0]\n",
    "\ttyp,pars = h \n",
    "\t\n",
    "\tif typ == \"alternative\":\n",
    "\t\tlef = FLOWaux(pars[0].copy(), ident+1)\n",
    "\t\trig = FLOWaux(pars[1].copy(), ident+1)\n",
    "\n",
    "\t\trst = (\"  \" * ident) + f\"({lef} \\n{'  ' * ident}||\\n{rig}{'  ' * ident});\\n{FLOWaux(inst[1:],ident)}\"\n",
    "\n",
    "\t\treturn rst\n",
    "\n",
    "\ta = FLOWaux(inst[1:],ident)\n",
    "\n",
    "\tif typ == \"assume\":\n",
    "\t\trst =  \"  \" * ident + f\"assume {pars[1]};\\n{a}\"\n",
    "\n",
    "\telif typ == \"assert\":\n",
    "\t\trst = \"  \" * ident + f\"assert {pars[1]};\\n{a}\"\n",
    "\n",
    "\telif typ == \"skip\":\n",
    "\t\trst = \"  \" * ident + f\"skip;\\n{a}\"\n",
    "\n",
    "\telif typ == \"atrib\":\n",
    "\t\trst = \"  \" * ident + f\"{pars[1]} = {pars[3]};\\n{a}\"\n",
    "\n",
    "\telif typ == \"havoc\":\n",
    "\t\trst = \"  \" * ident + f\"havoc {pars[1]};\\n{a}\"\n",
    "\t\n",
    "\treturn rst"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "De seguida apresentam-se duas funções que geram a condição de verificação (em *string*) de uma anotação em linguagem de fluxos segundo a metodologia *SPC* e *WPC*, respetivamente:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [],
   "source": [
    "def SPCstr(inst):\n",
    "\treturn SPCstraux(inst)[0]\n",
    "\n",
    "def SPCstraux(inst):\n",
    "\tif not inst:\n",
    "\t\treturn \"\",False\n",
    "\n",
    "\th = inst[-1]\n",
    "\ttyp,pars = h \n",
    "\t\n",
    "\tif typ == \"alternative\":\n",
    "\t\tlef = SPCstraux(inst[:-1] + pars[0])\n",
    "\t\trig = SPCstraux(inst[:-1] + pars[1])\n",
    "\n",
    "\t\trst = f\"({lef[0]}) V ({rig[0]})\\n\"\n",
    "\n",
    "\t\treturn rst,True\n",
    "\n",
    "\n",
    "\t\n",
    "\tst,h = SPCstraux(inst[:-1])\n",
    "\tif h:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trst = f\" ({st}) ∧ ({pars[1]})\"\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trst = f\"({st}) → ({pars[1]})\"\n",
    "\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trst = st\n",
    "\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trst = f\"({pars[1]} == {pars[3]}) ∧ ({st})\"\n",
    "\n",
    "\telse:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trst = pars[1]\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trst = pars[1]\n",
    "\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trst = \"True\"\n",
    "\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trst = f\"({pars[1]} == {pars[3]})\"\n",
    "\n",
    "\n",
    "\treturn rst,True\n",
    "\n",
    "def WPCstr(inst):\n",
    "\treturn WPCstraux(inst)[0]\n",
    "\n",
    "\n",
    "def WPCstraux(inst):\n",
    "\tif not inst:\n",
    "\t\treturn False,\"\"\n",
    "\n",
    "\ttyp,pars = inst[0]\n",
    "\t\n",
    "\tif typ == \"alternative\":\n",
    "\t\te = pars[0].copy()\n",
    "\t\td = pars[1].copy()\n",
    "\t\te.extend(inst[1:])\n",
    "\t\td.extend(inst[1:])\n",
    "\t\tlef = WPCstraux(e)\n",
    "\t\trig = WPCstraux(d)\n",
    "\n",
    "\t\trst = f\"({lef[0]}) ∧ ({rig[0]})\"\n",
    "\t\treturn rst,True\n",
    "\n",
    "\n",
    "\tst,h = WPCstraux(inst[1:])\n",
    "\tif h:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trst = f\"({pars[1]}) → ({st})\"\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trst = f\"({pars[1]}) ∧ ({st})\"\n",
    "\n",
    "\t\telif typ == \"havoc\":\n",
    "\t\t\trst = f\"∀{pars[1]} ({st})\"\n",
    "\n",
    "\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trst = st\n",
    "\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trst = f\"({st}) [{pars[3]}/{pars[1]}]\"\n",
    "\n",
    "\telse:\n",
    "\t\tif typ == \"assume\":\n",
    "\t\t\trst = \"True\"\n",
    "\n",
    "\n",
    "\t\telif typ == \"assert\":\n",
    "\t\t\trst = pars[1]\n",
    "\n",
    "\t\telif typ == \"skip\":\n",
    "\t\t\trst = \"True\"\n",
    "\n",
    "\n",
    "\t\telif typ == \"atrib\":\n",
    "\t\t\trst = \"True\"\n",
    "\n",
    "\treturn rst,True"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Para podermos parametrizar o *unfold* e gerarmos todas as condições de verificação respetivas a cada *unfold* de $0$ a $16$ para assim garantirmos a correção parcial do programa, criamos a função unfold(N) que recebe um número $N$ e cria a lista de instruções do programa para um *unfold* de $N$-vezes. Assim, para verificarmos a correção parcial do programa simplesmente executamos a função unfold() com todos os números de $0$ a $16$, aplicamos a função SPC() ao seu resultado, que irá gerar a condição de verificação em *z3* e tentamos prova-la."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "Unfolding 0...\n",
      "Solving for unfold 0...\n",
      "Proved for unfold 0!\n",
      "Unfolding 1...\n",
      "Solving for unfold 1...\n",
      "Proved for unfold 1!\n",
      "Unfolding 2...\n",
      "Solving for unfold 2...\n",
      "Proved for unfold 2!\n",
      "Unfolding 3...\n",
      "Solving for unfold 3...\n",
      "Proved for unfold 3!\n",
      "Unfolding 4...\n",
      "Solving for unfold 4...\n",
      "Proved for unfold 4!\n",
      "Unfolding 5...\n",
      "Solving for unfold 5...\n",
      "Proved for unfold 5!\n",
      "Unfolding 6...\n",
      "Solving for unfold 6...\n",
      "Proved for unfold 6!\n",
      "Unfolding 7...\n",
      "Solving for unfold 7...\n",
      "Proved for unfold 7!\n",
      "Unfolding 8...\n",
      "Solving for unfold 8...\n",
      "Proved for unfold 8!\n"
     ]
    }
   ],
   "source": [
    "import gc\n",
    "\n",
    "maxFold = 8\n",
    "bits = 8\n",
    "varbs = {\n",
    "         \"y\":[BitVec(f\"y{i}\",bits) for i in range((maxFold+1)*2)], \n",
    "         \"x\":[BitVec(f\"x{i}\",bits) for i in range(maxFold+1)],\n",
    "         \"r\":[BitVec(f\"r{i}\",bits) for i in range(maxFold+1)],\n",
    "         \"m\":[BitVec(f\"m0\",bits)],\n",
    "         \"n\":[BitVec(f\"n0\",bits)]\n",
    "        }\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "def internPattern(varbs,i):\n",
    "    internThen = [\n",
    "                    (\"assume\",[varbs[\"y\"][(2*i)] & 1 == 1, f\"y{(2*i)} & 1 == 1\"]),\n",
    "                    (\"atrib\",[varbs[\"y\"][(2*i)+1], f\"y{(2*i)+1}\",varbs[\"y\"][(2*i)] - 1,f\"y{(2*i)} - 1\"]),\n",
    "                    (\"atrib\",[varbs[\"r\"][i+1], f\"r{i+1}\",varbs[\"r\"][i] + varbs[\"x\"][i],f\"r{i} + x{i}\"])\n",
    "                ]\n",
    "    \n",
    "    internElse = [\n",
    "                    (\"assume\",[Not(varbs[\"y\"][(2*i)] & 1 == 1), f\"not(y{(2*i)} & 1 == 1)\"]),\n",
    "                    (\"atrib\",[varbs[\"y\"][(2*i)+1], f\"y{(2*i)+1}\", varbs[\"y\"][(2*i)],  f\"y{(2*i)}\"]),\n",
    "                    (\"atrib\",[varbs[\"r\"][i+1], f\"r{i+1}\", varbs[\"r\"][i],  f\"r{i}\"])\n",
    "                ]\n",
    "    \n",
    "\n",
    "    res = [\n",
    "            (\"alternative\",[internThen,internElse]),\n",
    "            (\"atrib\",[varbs[\"y\"][(2*i)+2],f\"y{(2*i)+2}\",varbs[\"y\"][(2*i)+1] >> 1, f\"y{(2*i)+1} >> 1\"]),\n",
    "            (\"atrib\",[varbs[\"x\"][i+1],f\"x{i+1}\",varbs[\"x\"][i] << 1, f\"x{i} << 1\"])\n",
    "        ]\n",
    "\n",
    "    return res\n",
    "\n",
    "\n",
    "\n",
    "\n",
    "def unfold(N):\n",
    "    \n",
    "    pre = And(varbs[\"m\"][0]>= 0, varbs[\"n\"][0]>= 0, varbs[\"r\"][0] == 0, varbs[\"x\"][0] == varbs[\"m\"][0], varbs[\"y\"][0] == varbs[\"n\"][0])\n",
    "    prestr = \"m0 >= 0 and n0 >= 0 and r0 == 0 and x0 == m0 and y0 == n0\"\n",
    "    pos = And(varbs[\"r\"][maxFold] == varbs[\"m\"][0] * varbs[\"n\"][0])\n",
    "    postr = f\"r{maxFold} == m0 * n0\"\n",
    "    acc = [(\"assume\", [pre, prestr])]\n",
    "    \n",
    "\n",
    "\n",
    "    for i in range(N):\n",
    "        body = internPattern(varbs,i)\n",
    "\n",
    "        acc += [\n",
    "                (\"assume\",[varbs[\"y\"][(2*i)] > 0, f\"y{(2*i)} > 0\"]),\n",
    "                *body\n",
    "                ]\n",
    "\n",
    "    if N != maxFold:\n",
    "        acc += [\n",
    "                (\"assume\", [Not(varbs[\"y\"][(2*N)] > 0), f\"not(y{(2*N)} > 0)\"]),\n",
    "                (\"atrib\", [varbs[\"y\"][2*maxFold], f\"y{maxFold}\", varbs[\"y\"][2*N],  f\"y{N}\"]),\n",
    "                (\"atrib\", [varbs[\"x\"][maxFold], f\"x{maxFold}\", varbs[\"x\"][N],  f\"x{N}\"]),\n",
    "                (\"atrib\", [varbs[\"r\"][maxFold], f\"r{maxFold}\", varbs[\"r\"][N],  f\"r{N}\"]),\n",
    "                (\"assert\", [pos, postr])\n",
    "               ]\n",
    "\n",
    "    else:\n",
    "        acc += [\n",
    "        (\"assert\",[And(pos,Not(varbs[\"y\"][2*maxFold] > 0)), postr + f\" and not(y{2*maxFold} > 0)\"])\n",
    "        ]\n",
    "\n",
    "\n",
    "\n",
    "    return acc\n",
    "\n",
    "\n",
    "\n",
    "def proveUnfold():\n",
    "\n",
    "    for i in range(maxFold+1):\n",
    "        gc.collect()\n",
    "        print(f\"Unfolding {i}...\")\n",
    "        res = unfold(i)\n",
    "        zExp = SPC(res)\n",
    "\n",
    "        print(f\"Solving for unfold {i}...\")\n",
    "        \n",
    "        s = Solver()\n",
    "        s.add(Not(zExp))\n",
    "        res = s.check()\n",
    "        \n",
    "        if res == unsat:\n",
    "            print(f\"Proved for unfold {i}!\")\n",
    "        \n",
    "        elif res == sat:\n",
    "            m = s.model()\n",
    "            for i in m:\n",
    "                print(f\"{i} = {m[i]}\")\n",
    "            print(f\"Could not Prove for unfold {i}\")\n",
    "        \n",
    "        else:\n",
    "            print(f\"Unknown result for unfold {i}\")\n",
    "\n",
    "    return\n",
    "\n",
    "#unfold8 = unfold(16)\n",
    "\n",
    "#print(FLOW(unfold5))\n",
    "#print(SPCstr(unfold5))\n",
    "\n",
    "\n",
    "#z3_form = SPC(unfold8)\n",
    "#prove(z3_form)\n",
    "proveUnfold()"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "Podemos adotar o mesmo procedimento para o comando *havoc* e utilizar a metodologia *WPC*:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": [
    "bits = 16\n",
    "x,y,m,n,r = BitVecs(\"x y m n r\",bits)\n",
    "\n",
    "inv = And(m*n == x*y + r,y >= 0)\n",
    "invStr = \"m * n == x * y + r and y >= 0\"\n",
    "\n",
    "pre = And( m>=0, n>=0, r == 0, x == m, y == n)\n",
    "preStr = \"m >= 0 and n >= 0 and r == 0 and x == m and y == n\"\n",
    "\n",
    "pos = r == m*n\n",
    "posStr = \"r == m*n\"\n",
    "\n",
    "\n",
    "\n",
    "havocInternIF = [\n",
    "\t\t\t\t\t(\"assume\", [y&1 == 1, \"y & 1 == 1\"]),\n",
    "\t\t\t\t\t(\"atrib\", [y, \"y\", y-1, \"y-1\"]),\n",
    "\t\t\t\t\t(\"atrib\", [r, \"r\", r+x, \"r+x\"])\n",
    "\t\t\t\t]\n",
    "\n",
    "havocInternElse = [\n",
    "\t\t\t\t\t(\"assume\", [Not(y&1 == 1), \"not(y & 1 == 1)\"]),\n",
    "\t\t\t\t\t(\"skip\",[])\n",
    "\t\t\t\t  ]\n",
    "\n",
    "\n",
    "havocThen = [\n",
    "\t\t\t\t(\"assume\", [And(y > 0, inv) , f\"y > 0 and {invStr}\"]),\n",
    "\t\t\t\t(\"alternative\", [havocInternIF, havocInternElse]),\n",
    "\t\t\t\t(\"atrib\", [x, \"x\", x<<1, \"x<<1\"]),\n",
    "\t\t\t\t(\"atrib\", [y, \"y\", y>>1, \"y>>1\"]),\n",
    "\t\t\t\t(\"assert\", [inv,invStr]),\n",
    "\t\t\t\t(\"assume\",[False,\"False\"])\n",
    "\t\t\t]\n",
    "\n",
    "\n",
    "\n",
    "havocElse = [\n",
    "\t\t\t\t(\"assume\", [And(Not(y>0),inv), f\"not(y > 0) and {invStr}\"])\n",
    "\t\t\t]\n",
    "\n",
    "\n",
    "havoc  = [\n",
    "\t\t\t(\"assume\", [pre,preStr]),\n",
    "\t\t \t(\"assert\", [inv,invStr]),\n",
    "\t\t \t(\"havoc\", [x,\"x\"]),\n",
    "\t\t \t(\"havoc\", [y,\"y\"]),\n",
    "\t\t \t(\"alternative\", [havocThen,havocElse]),\n",
    "\t\t \t(\"assert\", [pos,posStr])\n",
    "\t\t ]\n",
    "\n",
    "def prove(f):\n",
    "    s = Solver()\n",
    "    s.add(Not(f))\n",
    "    r = s.check()\n",
    "    if r == unsat:\n",
    "        print(\"Proved\")\n",
    "    elif r == sat:\n",
    "        print(\"Failed to prove\")\n",
    "        m = s.model()\n",
    "        for v in m:\n",
    "            print(v,'=', m[v])\n",
    "    elif r == unknown:\n",
    "        print(\"unknown\")\n",
    "\n",
    "# tudo com 16 bits \n",
    "#print(FLOW(havoc))\n",
    "#print(WPCstr(havoc))\n",
    "\n",
    "#logic = WPC(havoc)\n",
    "\n",
    "#prove(logic)"
   ]
  },
  {
   "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.8.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}