TP_4.ipynb

{
  "nbformat": 4,
  "nbformat_minor": 0,
  "metadata": {
    "colab": {
      "provenance": []
    },
    "kernelspec": {
      "name": "python3",
      "display_name": "Python 3"
    },
    "language_info": {
      "name": "python"
    }
  },
  "cells": [
    {
      "cell_type": "markdown",
      "source": [
        "\n",
        "#**Trabalho Prático 4**\n",
        "##Bárbara  Faria (A85774) , Bruna Araújo (A84408) e Tiago Lima (A85126)\n",
        "> Todos os problemas deste trabalho devem ser resolvidos usando pySMT   e  SMT’s  que suportem BitVec"
      ],
      "metadata": {
        "id": "xeRri53L4Wy0"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "!pip install z3-solver\n",
        "\n",
        "from z3 import *\n",
        "\n",
        "def prove(f):\n",
        "    s = Solver()\n",
        "    s.add(Not(f))\n",
        "    if s.check() == sat:\n",
        "        print(\"A fórmula não é válida...\")\n",
        "    else:\n",
        "        print(\"A fórmula é válida!\")"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "nJ41GKaqxEYV",
        "outputId": "018c4665-8351-4601-aa58-c8041c1a0001"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "Requirement already satisfied: z3-solver in /usr/local/lib/python3.7/dist-packages (4.8.14.0)\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "#Enunciado\n",
        "\n",
        "Considere o seguinte programa, em Python anotado, para multiplicação de dois inteiros de precisão limitada a 16 bits.\n",
        "\n",
        "```python\n",
        "assume (m>=0 and n>=0 and r==0 and x==m and y==n)\n",
        "while y > 0:\n",
        "  if y&1==1: \n",
        "    y, r  = y-1, r+x\n",
        "  x, y = x<<1, y>>1\n",
        "assert (r==m*n)\n",
        "```"
      ],
      "metadata": {
        "id": "7G_mz23s8qxQ"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "#Exercícios"
      ],
      "metadata": {
        "id": "q0ifzyat9GRZ"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "**1.** Prove por indução a terminação deste programa"
      ],
      "metadata": {
        "id": "xd2ss3PB4o4S"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "**2.** Pretende-se verificar a correção total deste  programa usando a metodologia dos invariantes e a metodologia do “single assignment unfolding”. Para isso,\n",
        "\n",
        "**a.** Codifique usando a LPA (linguagem de programas anotadas) a forma recursiva deste programa. "
      ],
      "metadata": {
        "id": "PB6PRtt44qes"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "O programa pode ser escrito como um triplo de Hoare \n",
        "$\\{\\phi\\} {\\sf while} \\; b \\;{\\sf do } \\;C \\{\\psi\\}$, onde $\\phi$ é a pré-condição, $\\psi$ é a pós-condição e $b$ é a condição do ciclo.\n",
        "\n",
        "Uma vez que vamos verificar a correção do programa através da metodologia dos invariantes, basta garantir a validade dos seguintes triplos:\n",
        "\n",
        "$\\{\\phi\\}{\\sf skip}\\{\\theta\\}$, que corresponde à \"inicialização\";\n",
        "\n",
        "$\\{\\theta\\wedge b\\}C\\{\\theta\\}$, que corresponde à \"preservação\";\n",
        "\n",
        "$\\{\\theta\\wedge\\neg b\\}{\\sf skip}\\{\\psi\\}$, que corresponde à \"utilidade\", \n",
        "\n",
        "onde $\\theta$ é o invariante.\n",
        "\n",
        "Se forem válidos, então o triplo que está na conclusão é válido."
      ],
      "metadata": {
        "id": "Bn8Habnp6bTv"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "Inicialização:\n",
        "\n",
        "LPA:\n",
        "\n",
        "assume $\\phi$ ; skip ; assert $\\theta$\n",
        "\n",
        "VC:\n",
        "\n",
        "[assume $\\phi$ ; skip ; assert $\\theta$]\n",
        "\n",
        "= $\\phi$ $\\to$ [skip ; assert $\\theta$]\n",
        "\n",
        "= $\\phi$ $\\to$ [assert $\\theta$]\n",
        "\n",
        "= $\\phi$ $\\to$ $\\theta$"
      ],
      "metadata": {
        "id": "nGtazWa3-0Wo"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "Preservação:\n",
        "\n",
        "LPA:\n",
        "\n",
        "assume ($\\theta \\wedge b$) ; (assume (y&1==1) ; y=y-1 ; r=r+x || assume (y&1!=1)) ; x=x<<1 ; y=y>>1 ; assert $\\theta$\n",
        "\n",
        "VC:\n",
        "\n",
        "[assume ($\\theta \\wedge b$) ; (assume (y&1==1) ; y=y-1 ; r=r+x || assume (y&1!=1)) ; x=x<<1 ; y=y>>1 ; assert $\\theta$]\n",
        "\n",
        "= ($\\theta \\wedge b) \\to$ [(assume (y&1==1) ; y=y-1 ; r=r+x || assume (y&1!=1)) ; x=x<<1 ; y=y>>1 ; assert $\\theta$]\n",
        "\n",
        "= ($\\theta \\wedge b) \\to$ [(assume (y&1==1) ; y=y-1 ; r=r+x ; x=x<<1 ; y=y>>1 ; assert $\\theta$) || (assume (y&1!=1) ; x=x<<1 ; y=y>>1 ; assert $\\theta$)]\n",
        "\n",
        "= ($\\theta \\wedge b) \\to$ ([assume (y&1==1) ; y=y-1 ; r=r+x ; x=x<<1 ; y=y>>1 ; assert $\\theta$] $\\wedge$ [assume (y&1!=1) ; x=x<<1 ; y=y>>1 ; assert $\\theta$])\n",
        "\n",
        "= ($\\theta \\wedge b) \\to$ (((y&1==1) $\\to$ [y=y-1 ; r=r+x ; x=x<<1 ; y=y>>1 ; assert $\\theta$]) $\\wedge$ ((y&1!=1) $\\to$ [x=x<<1 ; y=y>>1 ; assert $\\theta$]))\n",
        "\n",
        "= ($\\theta \\wedge b) \\to$ (((y&1==1) $\\to \\theta$ [y/y>>1][x/x<<1][r/r+x][y/y-1]) $\\wedge$ ((y&1!=1) $\\to \\theta$ [y/y>>1] [x/x<<1]))"
      ],
      "metadata": {
        "id": "fuWNe5F_Aeu7"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "Utilidade:\n",
        "\n",
        "LPA:\n",
        "\n",
        "assume ($\\theta \\wedge \\neg b$) ; skip ; assert $\\psi$\n",
        "\n",
        "VC:\n",
        "\n",
        "[assume ($\\theta \\wedge \\neg b$) ; skip ; assert $\\psi$]\n",
        "\n",
        "= ($\\theta \\wedge \\neg b$) $\\to$ [skip ; assert $\\psi$]\n",
        "\n",
        "= ($\\theta \\wedge \\neg b$) $\\to$ [assert $\\psi$]\n",
        "\n",
        "= ($\\theta \\wedge \\neg b$) $\\to$ $\\psi$"
      ],
      "metadata": {
        "id": "OxJO6eOCDmXt"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "**b.** Proponha o invariante mais fraco que assegure a correção, codifique-o em SMT e prove a correção."
      ],
      "metadata": {
        "id": "TyLkYmut44Il"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "Vamos determinar um invariante;\n",
        "\n",
        "Seja m==7, n==9, r==0, x==m, y==n e i a iteração do ciclo:\n",
        "\n",
        "| i | m | n | r  | x   | y |\n",
        "|---|---|---|----|-----|---|\n",
        "| 0 | 7 | 9 | 0  | 7   | 9 |\n",
        "| 1 | 7 | 9 | 7  | 14  | 4 |\n",
        "| 2 | 7 | 9 | 7  | 28  | 2 |\n",
        "| 3 | 7 | 9 | 7  | 56  | 1 |\n",
        "| 4 | 7 | 9 | 63 | 112 | 0 |\n",
        "\n",
        "Observando a tabela, concluímos que em cada iteração r+x*y = m*n\n",
        "\n",
        "Adicionando a condição do ciclo, obtemos o nosso invariante (em SMT):\n",
        "\n",
        "$\\theta$ = And(y >= 0, r+x*y==m*n)"
      ],
      "metadata": {
        "id": "ct4m4RcwFpbi"
      }
    },
    {
      "cell_type": "code",
      "source": [
        "m, n, r, x, y = BitVecs('m n r x y', 16)\n",
        "\n",
        "phi = And(m>=0, n>=0, r==0, x==m, y==n)\n",
        "theta = And(y>=0, r+x*y==m*n)\n",
        "b = y>0\n",
        "psi = r==m*n\n",
        "\n",
        "sub1 = substitute(substitute(substitute(substitute(theta,(y,y>>1)),(x,x<<1)),(r,r+x)),(y,y-1))\n",
        "sub2 = substitute(substitute(theta,(y,y>>1)),(x,x<<1))\n",
        "\n",
        "inic = Implies(phi, theta)\n",
        "pres = Implies(And(theta, b), And(Implies(y&1==1, sub1), Implies(y&1!=1, sub2)))\n",
        "util = Implies(And(theta, Not(b)), psi)\n",
        "\n",
        "print(\"\\nInicialização:\")\n",
        "prove(inic)\n",
        "\n",
        "print(\"\\nPreservação:\")\n",
        "prove(pres)\n",
        "\n",
        "print(\"\\nUtilidade:\")\n",
        "prove(util)"
      ],
      "metadata": {
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "id": "onxiSgJLKCH_",
        "outputId": "e214755b-ce79-4b72-f5b5-d93858610abe"
      },
      "execution_count": null,
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "\n",
            "Inicialização:\n",
            "A fórmula é válida!\n",
            "\n",
            "Preservação:\n",
            "A fórmula é válida!\n",
            "\n",
            "Utilidade:\n",
            "A fórmula é válida!\n"
          ]
        }
      ]
    },
    {
      "cell_type": "markdown",
      "source": [
        "**c.** Construa a definição iterativa do “single assignment unfolding”  usando um parâmetro limite $\\,N\\,$ e aumentando a pré-condição com a condição $$(n < N)\\,\\land\\,(m<N)$$\n",
        "O número de iterações vai ser controlado por este parâmetro $\\,N\\,$"
      ],
      "metadata": {
        "id": "YArb28sl46iD"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "I. Vamos começar por desenrolar o ciclo duas vezes:\n",
        "\n",
        "```python\n",
        "assume (m>=0 and n>=0 and r==0 and x==m and y==n)\n",
        "if (y>0):\n",
        "  if (y&1==1): \n",
        "    y=y-1 ; r=r+x\n",
        "  x=x<<1 ; y=y>>1\n",
        "  if (y > 0):\n",
        "    if (y&1==1): \n",
        "      y=y-1 ; r=r+x\n",
        "    x=x<<1 ; y=y>>1\n",
        "    assume (y<=0)\n",
        "assert (r==m*n)\n",
        "```"
      ],
      "metadata": {
        "id": "TJxfnPdzSt7Y"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "II. Convertemos o programa ao formato \"single assignment\" (SA):\n",
        "\n",
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "if (y0>0):\n",
        "  if (y0&1==1): \n",
        "    y1=y0-1 ; r1=r0+x0\n",
        "  else:\n",
        "    x0=x0 ; y1=y0 ; r1=r0 ;\n",
        "  x1=x0<<1 ; y2=y1>>1\n",
        "  if (y2 > 0):\n",
        "    if (y2&1==1): \n",
        "      y3=y2-1 ; r2=r1+x1\n",
        "    else:\n",
        "      x1=x1 ; y3=y2 ; r2=r1 ;\n",
        "    x2=x1<<1 ; y4=y3>>1\n",
        "    assume (y4<=0)\n",
        "  else:\n",
        "    x2=x1 ; y4=y2 ; r2=r1 ;\n",
        "else:\n",
        "  x2=x0 ; y4=y0 ; r2=r0 ;\n",
        "assert (r2==m0*n0)\n",
        "```"
      ],
      "metadata": {
        "id": "0GDeElIvSzlI"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "III. Vamos agora traduzir o programa para 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 ; r1=r0+x0\n",
        "  || assume (y0&1!=1) ;\n",
        "    x0=x0 ; y1=y0 ; r1=r0) ;\n",
        "  x1=x0<<1 ; y2=y1>>1\n",
        "  (assume (y2>0) ;\n",
        "    (assume (y2&1==1) ;\n",
        "      y3=y2-1 ; r2=r1+x1\n",
        "    || assume (y2&1!=1) ;\n",
        "      x1=x1 ; y3=y2 ; r2=r1 ;\n",
        "    x2=x1<<1 ; y4=y3>>1\n",
        "    assume (y4<=0)\n",
        "  || assume (y2<=0)) ;\n",
        "    x2=x1 ; y4=y2 ; r2=r1)\n",
        "|| assume(y0<=0) ; \n",
        "  x2=x0 ; y4=y0 ; r2=r0) ;\n",
        "assert (r2==m0*n0)\n",
        "```"
      ],
      "metadata": {
        "id": "cjZ2V20HS653"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "IV. Vamos calcular o conjunto de fluxos sem escolha não-determinista:\n",
        "\n",
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1==1) ; y1=y0-1 ; r1=r0+x0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1==1) ; y3=y2-1 ; r2=r1+x1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1!=1) ; x0=x0 ; y1=y0 ; r1=r0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1==1) ; y3=y2-1 ; r2=r1+x1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1==1) ; y1=y0-1 ; r1=r0+x0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1!=1) ; x1=x1 ; y3=y2 ; r2=r1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1!=1) ; x0=x0 ; y1=y0 ; r1=r0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1!=1) ; x1=x1 ; y3=y2 ; r2=r1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1==1) ; y1=y0-1 ; r1=r0+x0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2<=0) ; x2=x1 ; y4=y2 ; r2=r1 ;\n",
        "assert (r2==m0*n0)\n",
        "\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1!=1) ; x0=x0 ; y1=y0 ; r1=r0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2<=0) ; x2=x1 ; y4=y2 ; r2=r1 ;\n",
        "assert (r2==m0*n0)\n",
        "\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0<=0) ; x2=x0 ; y4=y0 ; r2=r0 ;\n",
        "assert (r2==m0*n0)\n",
        "```"
      ],
      "metadata": {
        "id": "xTK7o2PrTOXa"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "V. Para cada um destes fluxos, vamos calcular a respectiva denotação lógica (VC):\n",
        "\n",
        "Variáveis:\n",
        "```python\n",
        "phi = m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0\n",
        "b1 = y0>0\n",
        "i1 = y0&1==1\n",
        "ci1 = y1==y0-1 and r1==r0+x0 and x1==x0<<1 and y2==y1>>1\n",
        "b2 = y2>0\n",
        "i2 = y2&1==1\n",
        "ci2 = y3==y2-1 and r2==r1+x1 and x2==x1<<1 and y4==y3>>1 and y4<=0\n",
        "psi = r1==m0*n0\n",
        "cni1 = x0==x0 and y1==y0 and r1==r0 and x1==x0<<1 and y2==y1>>1\n",
        "cni2 = x1==x1 and y3==y2 and r2==r1 and x2==x1<<1 and y4==y3>>1 and y4<=0\n",
        "cnb2 = x2==x1 and y4==y2 and r2==r1\n",
        "cnb1 = x2==x0 and y4==y0 and r1==r0\n",
        "```"
      ],
      "metadata": {
        "id": "V7_aqGTbTFlF"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1==1) ; y1=y0-1 ; r1=r0+x0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1==1) ; y3=y2-1 ; r2=r1+x1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "```\n",
        "\n",
        "($\\phi \\wedge$ b1 $\\wedge$ i1 $\\wedge$ ci1 $\\wedge$ b2 $\\wedge$ i2 $\\wedge$ ci2) $\\to \\psi$ "
      ],
      "metadata": {
        "id": "3FiZYYonrU9K"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1!=1) ; x0=x0 ; y1=y0 ; r1=r0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1==1) ; y3=y2-1 ; r2=r1+x1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "```\n",
        "\n",
        "($\\phi \\wedge$ b1 $\\wedge \\neg$ i1 $\\wedge$ cni1 $\\wedge$ b2 $\\wedge$ i2 $\\wedge$ ci2) $\\to \\psi$"
      ],
      "metadata": {
        "id": "feQ3LrNqrboi"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1==1) ; y1=y0-1 ; r1=r0+x0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1!=1) ; x1=x1 ; y3=y2 ; r2=r1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "```\n",
        "\n",
        "($\\phi \\wedge$ b1 $\\wedge$ i1 $\\wedge$ ci1 $\\wedge$ b2 $\\wedge \\neg$ i2 $\\wedge$ cni2) $\\to \\psi$"
      ],
      "metadata": {
        "id": "Qo7m02v30wHP"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1!=1) ; x0=x0 ; y1=y0 ; r1=r0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2>0) ; assume (y2&1!=1) ; x1=x1 ; y3=y2 ; r2=r1 ; x2=x1<<1 ; y4=y3>>1 ; assume (y4<=0)\n",
        "assert (r2==m0*n0)\n",
        "```\n",
        "\n",
        "($\\phi \\wedge$ b1 $\\wedge \\neg$ i1 $\\wedge$ cni1 $\\wedge$ b2 $\\wedge \\neg$ i2 $\\wedge$ cni2) $\\to \\psi$"
      ],
      "metadata": {
        "id": "7wUPJpwqCUsN"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1==1) ; y1=y0-1 ; r1=r0+x0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2<=0) ; x2=x1 ; y4=y2 ; r2=r1 ;\n",
        "assert (r2==m0*n0)\n",
        "```\n",
        "\n",
        "($\\phi \\wedge$ b1 $\\wedge$ i1 $\\wedge$ ci1 $\\wedge \\neg$ b2 $\\wedge$ cnb2) $\\to \\psi$"
      ],
      "metadata": {
        "id": "LqO6s6HCCtzG"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0>0) ; assume (y0&1!=1) ; x0=x0 ; y1=y0 ; r1=r0 ; x1=x0<<1 ; y2=y1>>1\n",
        "assume (y2<=0) ; x2=x1 ; y4=y2 ; r2=r1 ;\n",
        "assert (r2==m0*n0)\n",
        "```\n",
        "\n",
        "($\\phi \\wedge$ b1 $\\wedge \\neg$ i1 $\\wedge$ cni1 $\\wedge \\neg$ b2 $\\wedge$ cnb2) $\\to \\psi$"
      ],
      "metadata": {
        "id": "xDFzfb3M3svM"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "```python\n",
        "assume (m0>=0 and n0>=0 and r0==0 and x0==m0 and y0==n0)\n",
        "assume (y0<=0) ; x2=x0 ; y4=y0 ; r2=r0 ;\n",
        "assert (r2==m0*n0)\n",
        "```\n",
        "\n",
        "($\\phi \\wedge \\neg$ b1 $\\wedge$ cnb1) $\\to \\psi$"
      ],
      "metadata": {
        "id": "Tf2gkmPh36HP"
      }
    },
    {
      "cell_type": "markdown",
      "source": [
        "VI. Vamos provar as VCs que calculamos:"
      ],
      "metadata": {
        "id": "ug63ZWRl9kIf"
      }
    },
    {
      "cell_type": "code",
      "execution_count": null,
      "metadata": {
        "id": "NeCXlTJR4Oul",
        "colab": {
          "base_uri": "https://localhost:8080/"
        },
        "outputId": "af7c7e61-2929-4bae-9725-22f55eda4401"
      },
      "outputs": [
        {
          "output_type": "stream",
          "name": "stdout",
          "text": [
            "A fórmula não é válida...\n",
            "A fórmula não é válida...\n",
            "A fórmula é válida!\n",
            "A fórmula é válida!\n",
            "A fórmula é válida!\n",
            "A fórmula é válida!\n",
            "A fórmula é válida!\n"
          ]
        }
      ],
      "source": [
        "m0, n0, r0, r1, r2, x0, x1, x2, y0, y1, y2, y3, y4 = BitVecs('m0 n0 r0 r1 r2 x0 x1 x2 y0 y1 y2 y3 y4', 16)\n",
        "\n",
        "phi = And(m0>=0, n0>=0, r0==0, x0==m0, y0==n0)\n",
        "b1 = y0>0\n",
        "i1 = y0&1==1\n",
        "ci1 = And(y1==y0-1, r1==r0+x0, x1==x0<<1, y2==y1>>1)\n",
        "b2 = y2>0\n",
        "i2 = y2&1==1\n",
        "ci2 = And(y3==y2-1, r2==r1+x1, x2==x1<<1, y4==y3>>1, y4<=0)\n",
        "psi = r1==m0*n0\n",
        "cni1 = And(x0==x0, y1==y0, r1==r0, x1==x0<<1, y2==y1>>1)\n",
        "cni2 = And(x1==x1, y3==y2, r2==r1, x2==x1<<1, y4==y3>>1, y4<=0)\n",
        "cnb2 = And(x2==x1, y4==y2, r2==r1)\n",
        "cnb1 = And(x2==x0, y4==y0, r1==r0)\n",
        "\n",
        "f1 = Implies(And(phi,b1,i1,ci1,b2,i2,ci2),psi)\n",
        "\n",
        "f2 = Implies(And(phi,b1,Not(i1),cni1,b2,i2,ci2),psi)\n",
        "\n",
        "f3 = Implies(And(phi,b1,i1,ci1,b2,Not(i2),cni2),psi)\n",
        "\n",
        "f4 = Implies(And(phi,b1,Not(i1),cni1,b2,Not(i2),cni2),psi)\n",
        "\n",
        "f5 = Implies(And(phi,b1,i1,ci1,Not(b2),cnb2),psi)\n",
        "\n",
        "f6 = Implies(And(phi,b1,Not(i1),cni1,Not(b2),cnb2),psi)\n",
        "\n",
        "f7 =Implies(And(phi,Not(b1),cnb1),psi)\n",
        "\n",
        "prove(f1)\n",
        "prove(f2)\n",
        "prove(f3)\n",
        "prove(f4)\n",
        "prove(f5)\n",
        "prove(f6)\n",
        "prove(f7)"
      ]
    }
  ]
}