more latex

tesi/conv.py

@@ -3,8 +3,8 @@ import re
 from sys import argv
 
 allsymbols = json.load(open('./unicode-latex.json'))
-mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃' ]
-extrasymbols = {'〚': '\llbracket', '〛': '\rrbracket'}
+mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀',  'ε', '₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π', 'α', 'β', '∞', 'σ', '≤', '⊈', '∧', '∨', '∃', '⇒', '∩', '∉', '⋃', 'ᵏ', 'ₗ', 'ˡ', 'ₒ', 'ᵣ', 'ᴵ', '≈' ]
+extrasymbols = {'〚': '\llbracket', '〛': r'\rrbracket', '̸': '\neg', '¬̸': '\neg', '∈': '\in ', 'ₛ': '_S', 'ₜ': '_T'}
 
 symbols = {s: allsymbols[s] for s in mysymbols}
 symbols.update(extrasymbols)
@@ -13,8 +13,8 @@ mathsymbols = {s: '$'+v+'$' for s, v in symbols.items()}
 def read_by_char(fname):
     # Yield character and True/False if inside mathmode block
     mathmode = False
-    mathmode_begin = set(['\\begin{equation*}', '\\begin{equation}'])
-    mathmode_end = set(['\\end{equation*}', '\\end{equation}'])
+    mathmode_begin = set(['\\begin{equation*}', '\\begin{equation}', '\[', '\\begin{mathpar}'])
+    mathmode_end = set(['\\end{equation*}', '\\end{equation}', '\]', '\\end{mathpar}'])
     cnt = 0
     with open(fname, 'r') as fp:
         for line in fp.readlines():
@@ -50,11 +50,26 @@ def latex_errors_replacements(charlist):
             yield from word
         yield ' '
 
+def ll_rr_bracket(charlist):
+    llrr_mode = False
+
+    for i, ch in enumerate(charlist):
+        if ch == '\\':
+            if charlist[i:i+10] == '\llbracket':
+                assert llrr_mode is False ; llrr_mode = True
+            elif charlist[i:i+10] == '\rrbracket':
+                assert llrr_mode is True ; llrr_mode = False
+
+        if not (llrr_mode and ch == '$'):
+            yield ch
+
+
 # convert symbols except the one requiring math mode modifiers
 firstpass = [convert(*c) for c in read_by_char(argv[1])]
 # remove a latex error
 secondpass = latex_errors_replacements(firstpass)
+thirdpass = ll_rr_bracket(list(secondpass))
 
-newfile = ''.join(secondpass)
+newfile = ''.join(thirdpass)
 with open(argv[2], 'w') as f:
     f.write(newfile)

tesi/files/symb_exec

@@ -0,0 +1 @@
+<mxfile host="app.diagrams.net" modified="2020-04-07T18:00:18.130Z" agent="5.0 (X11)" etag="UqJT9eDZirhT4ZuYmnlI" version="12.9.9" type="device"><diagram id="vkyFxs9FE47iKiCmcqWQ" name="Page-1">7VpLk+I2EP41rpoccFnyA/sIDJsckspjDsnuJaWxBahiW0QWC+yvj2RLfsmzDCwBdoYqCqyvpZb0dUvqlrHcWbb7kaH16hea4NSCTrKz3EcLwjAIxLcE9hXgRVEFLBlJKgg0wBP5ghXoKHRDElx0KnJKU07WXTCmeY5j3sEQY3TbrbagabfXNVpiA3iKUWqif5KEr9S0fKfBf8JkudI9A0dJMqQrK6BYoYRuW5A7t9wZo5RXT9luhlPJnealavfhBWk9MIZz/poGPz99+n3y6dcYzpztl+c/wH7ERiOl5TNKN2rCMc3WiAvswbbtH9TQ+V7zwegmT7BUCSx3ul0Rjp/WKJbSrXAAga14liqxUo4Zx7sXRw1qLoQPYZphzvaiimrgavq0/6jitjFGTfmqZQhdDyn7L2vNDUXiQbF0BGPQYMzyp8DyHw2qxKR5l4+CM/oPntGUMoHkNBc1pwuSpj0IpWSZi2IsSMICn0oKiXDKiRJkJElkN4MGaEzknMcGMOzawDdt4A2YAP5fJnBNE4zFPEV3QSoZL9Yo75gi+HcjV9k0xQvxMxEy33Ns33PXO9lMkiR2lXUlGvuBDUPYEi1ozkdFuTXJCiC0QQjCfoUFyki6r6oUKC9GBWZk0XQunpbl7+yDFdZjFQRUw1VCBUuNUo/eD7USMKBPz3rzbECvIMJ37MgZDxIRQNtzjHm2iACnczC3yrl8jQMJm3MSaEWOgsu+RtYcWmFoRfPKDVAmF4Kq7+jeBiTtZuM3vIS94OASBuNLrmHPXMN98nGeTOQJLllMUVGQuGsKvCP8L0mR7avSx5bkcafYKwt7XcjF4FuNZPFjW9Y0K0v7jglwYgQLPQOICdANi/HhI5cjtsT8K/WCYYO2LOYPGExjDKeIk8/d4Q5ZUfXwGyXljqOPXa/rL7VzaBXVNFWrdtTRV9RzPND3qIoHQ1HpVPW0T/ezwPCzjMg98aHcht1yAxAfQdCs3CnaILy98Kem72rxz3go/oHvKv4B7pUDoPAMAVDg2KEDjwiAXn22HzGIUGzDbnizUdgL8ImR1hjYILh8pFXuaKdEWm89Br1Q9Dl00hjHzIHQ1L2nN9+Va91KeiMl8CQHus5mdWDf/f5PlBO9OJJePLychTWCzkrvzSr6JieGxzlxqdS27bedS/uHw8E67blIPBgZ8WCMCv6w+VskVfJwuc2rXOhcO5cB5vX3e7mFCF55CxHd0i1E/Vbo6FuIqLdkg8veQoDBtwbuu8qaa+NdK2sG53hvcE+b72nzPW0+S1bjWCrLjayJZ9WJ8j0bfmsec8+G79nwPRt+o2GeB/2DYV4dfl8mzvO/Pas7Y6Z13Qxq3AvCo1MzqL6i8MIZlPkiV686ohccw4UcMV3ILWGFpQF3ON5wQnNd95kNrFnSYLd2RRKai+lcVySi2Pz5sDJT8w9Od/4f</diagram></mxfile>

tesi/tesi_unicode.org

@@ -31,6 +31,7 @@ Magari prima pattern matching poi compilatore?
 
 #+LANGUAGE: en
 #+LaTeX_CLASS: article
+#+LaTeX_HEADER: \linespread{1.25}
 #+LaTeX_HEADER: \usepackage{algorithm} 
 #+LaTeX_HEADER: \usepackage{comment} 
 #+LaTeX_HEADER: \usepackage{algpseudocode} 
@@ -41,11 +42,11 @@ Magari prima pattern matching poi compilatore?
 #+LaTeX_HEADER: \usepackage{listings} 
 #+LaTeX_HEADER: \usepackage{color} 
 #+LaTeX_HEADER: \usepackage{stmaryrd}
-#+LaTeX_HEADER: \newcommand{\sem}[1]{{\llbracket{#1}\rrbracket}}
-#+LaTeX_HEADER: \newcommand{\Equiv}[3]{\mathsf{equiv}(#1, #2, #3)} % \equiv is already taken
-#+LaTeX_HEADER: \newcommand{\covers}[2]{#1 \mathrel{\mathsf{covers}} #2}
-#+LaTeX_HEADER: \newcommand{\Yes}{\mathsf{Yes}}
-#+LaTeX_HEADER: \newcommand{\No}[2]{\mathsf{No}(#1, #2)}
+#+LaTeX_HEADER: \newcommand{\semTEX}[1]{{\llbracket{#1}\rrbracket}}
+#+LaTeX_HEADER: \newcommand{\EquivTEX}[3]{\mathsf{equiv}(#1, #2, #3)} % \equiv is already taken
+#+LaTeX_HEADER: \newcommand{\coversTEX}[2]{#1 \mathrel{\mathsf{covers}} #2}
+#+LaTeX_HEADER: \newcommand{\YesTEX}{\mathsf{Yes}}
+#+LaTeX_HEADER: \newcommand{\NoTEX}[2]{\mathsf{No}(#1, #2)}
 #+LaTeX_HEADER: \usepackage{comment}
 #+LaTeX_HEADER: \usepackage{mathpartir}
 #+LaTeX_HEADER: \usepackage{stmaryrd} % llbracket, rrbracket
@@ -142,7 +143,6 @@ the case of a production compiler and to integrate with an existing code base. T
 black-box and proof only depends on our equivalence algorithm.
 
 \subsection{Our approach}
-%% replace common TODO
 Our algorithm translates both source and target programs into a common
 representation, decision trees. Decision trees where chosen because
 they model the space of possible values at a given branch of
@@ -227,12 +227,12 @@ matched by the source clauses.
 \texttt{Unreachable} is used when we statically know that no value
 can flow to that subtree.
 
-We write $\sem{t_S}_S$ for the decision tree of the source program
-$t_S$, computed by a matrix decomposition algorithm (each column
+We write 〚tₛ〛ₛ for the decision tree of the source program
+t_S, computed by a matrix decomposition algorithm (each column
 decomposition step gives a \texttt{Switch} node).
 It satisfies the following correctness statement:
 \[
-\forall t_S, \forall v_S, \quad t_S(v_S) = \sem{t_S}_S(v_S)
+\forall t_s, \forall v_s, \quad t_s(v_s) = \semTEX{t_s}_s(v_s)
 \]
 Running any source value $v_S$ against the source program gives the
 same result as running it against the decision tree.
@@ -250,10 +250,10 @@ nodes are never emitted.
 Guards result in branching. In comparison with the source decision
 trees, \texttt{Unreachable} nodes are never emitted.
 
-We write $\sem{t_T}_T$ for the decision tree of the target program
+We write $\semTEX{t_T}_T$ for the decision tree of the target program
 $t_T$, satisfying the following correctness statement:
 \[
-\forall t_T, \forall v_T, \quad t_T(v_T) = \sem{t_T}_T(v_T)
+\forall t_T, \forall v_T, \quad t_T(v_T) = \semTEX{t_T}_T(v_T)
 \]
 
 \subsection{Equivalence checking}
@@ -262,36 +262,36 @@ possible values \emph{S} and a pair of source and target decision trees and
 in case the two trees are not equivalent it returns a counter example.
 The algorithm respects the following correctness statement:
 \begin{comment}
-% TODO: we have to define what \covers mean for readers to understand the specifications
-% (or we use a simplifying lie by hiding \covers in the statements).
+% TODO: we have to define what \coversTEX mean for readers to understand the specifications
+% (or we use a simplifying lie by hiding \coversTEX in the statements).
 \end{comment}
 
 \begin{align*}
- \Equiv S {C_S} {C_T} = \Yes \;\land\; \covers {C_T} S
+ \EquivTEX S {C_S} {C_T} = \YesTEX \;\land\; \coversTEX {C_T} S
  & \implies
  \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T)
 \\
- \Equiv S {C_S} {C_T} = \No {v_S} {v_T} \;\land\; \covers {C_T} S
+ \EquivTEX S {C_S} {C_T} = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S
  & \implies
  v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T)
 \end{align*}
 
 The algorithm proceeds by case analysis. Inference rules are shown.
-If $S$ is empty the results is $\Yes$.
+If $S$ is empty the results is $\YesTEX$.
 \begin{mathpar}
   \infer{ }
-  {\Equivrel \emptyset {C_S} {C_T} G}
+  {\EquivTEX \emptyset {C_S} {C_T} G}
 \end{mathpar}
 
 If the two decision trees are both terminal nodes the algorithm checks
 for content equality.
 \begin{mathpar}
   \infer{ }
-  {\Equivrel S \Failure \Failure \emptyqueue}
+  {\EquivTEX S \Failure \Failure \emptyqueue}
 \\
   \infer
   {\trel {t_S} {t_T}}
-  {\Equivrel S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
+  {\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
 
 \end{mathpar}
 
@@ -305,10 +305,10 @@ hand side.
   \infer
   {C_S \in {\Leaf t, \Failure}
    \\
-   \forall i,\; \Equivrel {(S \land a \in D_i)} {C_S} {C_i} G
+   \forall i,\; \EquivTEX {(S \land a \in D_i)} {C_S} {C_i} G
    \\
-   \Equivrel {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
-  {\Equivrel S
+   \EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
+  {\EquivTEX S
     {C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G}
 \end{mathpar}
 
@@ -331,15 +331,15 @@ result in an empty intersection. If the accessors are different,
 \begin{mathpar}
   \infer
   {\forall i,\;
-    \Equivrel
+    \EquivTEX
       {(S \land a = K_i)}
       {C_i} {\trim {C_T} {a = K_i}} G
    \\
-   \Equivrel
+   \EquivTEX
      {(S \land a \notin \Fam i {K_i})}
      \Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G
   }
-  {\Equivrel S
+  {\EquivTEX S
     {\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G}
 \end{mathpar}
 
@@ -355,17 +355,17 @@ Termination of the algorithm is successful only when the guards queue
 is empty.
 \begin{mathpar}
   \infer
-  {\Equivrel S {C_0} {C_T} {G, (t_S = 0)}
+  {\EquivTEX S {C_0} {C_T} {G, (t_S = 0)}
    \\
-   \Equivrel S {C_1} {C_T} {G, (t_S = 1)}}
-  {\Equivrel S
+   \EquivTEX S {C_1} {C_T} {G, (t_S = 1)}}
+  {\EquivTEX S
     {\Guard {t_S} {C_0} {C_1}} {C_T} G}
 
   \infer
   {\trel {t_S} {t_T}
    \\
-   \Equivrel S {C_S} {C_b} G}
-  {\Equivrel S
+   \EquivTEX S {C_S} {C_b} G}
+  {\EquivTEX S
     {C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}}
 \end{mathpar}
 
@@ -714,8 +714,8 @@ bad:
 The tree of the execution when the function is evaluated considering
 /int len/ our symbolic variable α, sa->sa_len as symbolic variable β
 and π as the set of constraints on a symbolic variable:
-
-#+BEGIN_SRC
+[[./files/symb_exec.png]]
+\begin{comment}
 [1]              compat (...)        { π_{α}: -∞ < α < ∞ }
                    |
 [2]              min (σ₁, σ₂)        { π_{σ}: -∞ < (σ₁,σ₂) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...}
@@ -723,7 +723,7 @@ and π as the set of constraints on a symbolic variable:
 [3]             cast(u_int) (...)    { π_{σ}: 0 ≤ (σ) < ∞ ; π_{α}: -∞ < α < β ; π_{β}: ...}
                    |   
                   ... // rest of the execution
-#+END_SRC
+\end{comment}
 We can see that at step 3 the set of possible values of the scrutinee
 α is bigger than the set of possible values of the input σ to the
 /cast/ directive, that is: π_{α} ⊈ π_{σ}. For this reason the /cast/ may fail when α is /len/
@@ -731,9 +731,9 @@ negative number, outside the domain π_{σ}. In C this would trigger undefined b
 overflow) that made the exploitation possible.
 
 Every step of evaluation can be modelled as the following transition:
-#+BEGIN_SRC
+\[
 (π_{σ}, (πᵢ)ⁱ) → (π'_{σ}, (π'ᵢ)ⁱ)
-#+END_SRC
+\]
 if we express the π constraints as logical formulas we can model the
 execution of the program in terms of Hoare Logic.
 State of the computation is a Hoare triple {P}C{Q} where P and Q are
@@ -742,50 +742,47 @@ constitute the assertions of the program. C is the directive being
 executed.
 The language of the assertions P is:
 #+BEGIN_SRC
-P ::= true | false | a < b | P₁ ∧ P₂ | P₁ ∨ P₂ | ~P
+P ::= true | false | a < b | P_{1} \wedge P_{2} | P_{1} \lor P_{2} | \notP
 #+END_SRC
 where a and b are numbers.
 In the Hoare rules assertions could also take the form of
 #+BEGIN_SRC
-P ::= ∀i. P | ∃i. P | P₁ ⇒ P₂
+P ::= \forall i. P | \exists i. P | P_{1} \Rightarrow P_{2}
 #+END_SRC
 where i is a logical variable, but assertions of these kinds increases
 the complexity of the symbolic engine.
 Execution follows the rules of Hoare logic:
 - Empty statement :
-\begin{verbatim}
-————————————
-{P}/skip/{P}
-\end{verbatim}
+\begin{mathpar}
+\infer{ }
+{ \{P\} skip \{P\} }
+\end{mathpar}
 - Assignment statement : The truthness of P[a/x] is equivalent to the
   truth of {P} after the assignment.
-\begin{verbatim}
-————————————
-{P[a/x]}x:=a{P}
-\end{verbatim}
+\begin{mathpar}
+\infer{ }
+{ \{P[a/x]\}x:=a\{P\} }
+\end{mathpar}
 
 - Composition : c₁ and c₂ are directives that are executed in order;
-  {Q} is the /midcondition/.
-\begin{verbatim}
-{P}c₁{R}, {R}c₂{Q}
-——————————————————
-   {P}c₁;c₂{Q}
-\end{verbatim}
+  {Q} is called the /midcondition/.
+\begin{mathpar}
+\infer { \{P\}c_1\{R\}, \{R\}c_2\{Q\} }
+ {  \{P\}c₁;c₂\{Q\} }
+\end{mathpar}
 
 - Conditional : 
-\begin{verbatim}
- {P∧b}c₁{Q}, {P∧~b}c₂{Q}
-————————————————————————
-{P}if b then c₁ else c₂{Q}
-\end{verbatim}
+\begin{mathpar}
+\infer { \{P \wedge b \} c_1 \{Q\}, \{P\wedge\not b\}c_2\{Q\} }
+{ \{P\}if b then c_1 else c_2\{Q\} }
+\end{mathpar}
 
 - Loop : {P} is the loop invariant. After the loop is finished /P/
-  holds and ~b caused the loop to end.
-\begin{verbatim}
- {P∧b}c{P}
-————————————————————————
-{P}while b do c{P∧~b}
-\end{verbatim}
+  holds and ¬̸b caused the loop to end.
+\begin{mathpar}
+\infer { \{P \wedge b \}c\{P\} }
+{ \{P\} while b do c \{P \wedge \neg b\} }
+\end{mathpar}
 
 Even if the semantics of symbolic execution engines are well defined,
 the user may run into different complications when applying such
@@ -1176,22 +1173,24 @@ possible values \emph{S} and a pair of source and target decision trees and
 in case the two trees are not equivalent it returns a counter example.
 The algorithm respects the following correctness statement:
 
-% TODO: we have to define what \covers mean for readers to understand the specifications
-% (or we use a simplifying lie by hiding \covers in the statements).
+\begin{comment}
+TODO: we have to define what \coversTEX mean for readers to understand the specifications
+(or we use a simplifying lie by hiding \coversTEX in the statements).
+\end{comment}
 
 \begin{align*}
- \Equiv S {C_S} {C_T} \emptyqueue = \Yes \;\land\; \covers {C_T} S
+ \EquivTEX S {C_S} {C_T} \emptyqueue = \YesTEX \;\land\; \coversTEX {C_T} S
  & \implies
  \forall v_S \approx v_T \in S,\; C_S(v_S) = C_T(v_T)
 \\
- \Equiv S {C_S} {C_T} \emptyqueue = \No {v_S} {v_T} \;\land\; \covers {C_T} S
+ \EquivTEX S {C_S} {C_T} \emptyqueue = \NoTEX {v_S} {v_T} \;\land\; \coversTEX {C_T} S
  & \implies
  v_S \approx v_T \in S \;\land\; C_S(v_S) \neq C_T(v_T)
 \end{align*}
 
-Our equivalence-checking algorithm $\Equiv S {C_S} {C_T} G$ is
+Our equivalence-checking algorithm $\EquivTEX S {C_S} {C_T} G$ is
 a exactly decision procedure for the provability of the judgment
-$(\Equivrel S {C_S} {C_T} G)$, defined below.
+$(\EquivTEX  S {C_S} {C_T} G)$, defined below.
 \begin{mathpar}
   \begin{array}{l@{~}r@{~}l}
     & & \text{\emph{constraint trees}} \\
@@ -1214,26 +1213,26 @@ $(\Equivrel S {C_S} {C_T} G)$, defined below.
   \end{array}
   \\
   \infer{ }
-  {\Equivrel \emptyset {C_S} {C_T} G}
+  {\EquivTEX \emptyset {C_S} {C_T} G}
 
   \infer{ }
-  {\Equivrel S \Failure \Failure \emptyqueue}
+  {\EquivTEX S \Failure \Failure \emptyqueue}
 
   \infer
   {\trel {t_S} {t_T}}
-  {\Equivrel S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
+  {\EquivTEX S {\Leaf {t_S}} {\Leaf {t_T}} \emptyqueue}
 
   \infer
   {\forall i,\;
-    \Equivrel
+    \EquivTEX
       {(S \land a = K_i)}
       {C_i} {\trim {C_T} {a = K_i}} G
    \\
-   \Equivrel
+   \EquivTEX
      {(S \land a \notin \Fam i {K_i})}
      \Cfb {\trim {C_T} {a \notin \Fam i {K_i}}} G
   }
-  {\Equivrel S
+  {\EquivTEX S
     {\Switch a {\Fam i {K_i, C_i}} \Cfb} {C_T} G}
 
 \begin{comment}
@@ -1244,30 +1243,30 @@ $(\Equivrel S {C_S} {C_T} G)$, defined below.
   \infer
   {C_S \in {\Leaf t, \Failure}
    \\
-   \forall i,\; \Equivrel {(S \land a \in D_i)} {C_S} {C_i} G
+   \forall i,\; \EquivTEX  {(S \land a \in D_i)} {C_S} {C_i} G
    \\
-   \Equivrel {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
-  {\Equivrel S
+   \EquivTEX {(S \land a \notin \Fam i {D_i})} {C_S} \Cfb G}
+  {\EquivTEX S
     {C_S} {\Switch a {\Fam i {D_i} {C_i}} \Cfb} G}
 
   \infer
-  {\Equivrel S {C_0} {C_T} {G, (t_S = 0)}
+  {\EquivTEX S {C_0} {C_T} {G, (t_S = 0)}
    \\
-   \Equivrel S {C_1} {C_T} {G, (t_S = 1)}}
-  {\Equivrel S
+   \EquivTEX S {C_1} {C_T} {G, (t_S = 1)}}
+  {\EquivTEX S
     {\Guard {t_S} {C_0} {C_1}} {C_T} G}
 
   \infer
   {\trel {t_S} {t_T}
    \\
-   \Equivrel S {C_S} {C_b} G}
-  {\Equivrel S
+   \EquivTEX S {C_S} {C_b} G}
+  {\EquivTEX S
     {C_S} {\Guard {t_T} {C_0} {C_1}} {(t_S = b), G}}
 \end{mathpar}
 
 * Correctness of the algorithm
 Running a program tₛ or its translation 〚tₛ〛 against an input vₛ
-produces as a result a result /r/ in the following way:
+produces as a result /r/ in the following way:
 | ( 〚tₛ〛ₛ(vₛ) = Cₛ(vₛ) ) → r
 | tₛ(vₛ) → r
 Likewise
@@ -1342,6 +1341,7 @@ and an optional fallback.
 Failure is emitted only when the patterns don't cover the whole set of
 possible input values /S/. The fallback is not needed when the user
 doesn't use a wildcard pattern.
+%%% Give example of thing
 
 | Cₛ ::= Leaf bb | Node(a, (Kᵢ → Cᵢ)^{i∈S} , C?)
 | a ::= Here | n.a
@@ -1352,17 +1352,17 @@ Are K and Here clear here?
 \end{comment}
 
 We define the decomposition matrix /mₛ/ as
-| SMatrix mₛ := (aⱼ)^{j∈J}, ((pᵢⱼ)^{j∈J} → bbᵢ)^{i∈I}
+| SMatrix mₛ := (aⱼ)^{j∈J}, ((p_{ij})^{j∈J} → bbᵢ)^{i∈I}
 \begin{comment}
 Correggi prendendo in considerazione l'accessor
 \end{comment}
 
 We define the decision tree of source programs
-  [|tₛ|]
+〚tₛ〛
 in terms of the decision tree of pattern matrices
-  [|mₛ|]
+  〚mₛ〛
 by the following:
-  〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛 # i ∈ I
+  〚((pᵢ → bbᵢ)^{i∈I}〛 := 〚(Root), (pᵢ → bbᵢ)^{i∈I} 〛
 
 decision tree computed from pattern matrices respect the following invariant:
 | ∀v (vᵢ)^{i∈I} = v(aᵢ)^{i∈I} → 〚m〛(v) = m(vᵢ)^{i∈I} for m = ((aᵢ)^{i∈I}, (rᵢ)^{i∈I})
@@ -1385,10 +1385,95 @@ Base cases:
 2. [| (aⱼ)ʲ, ∅ |] := Failure 
 
 Regarding non base cases:
-We define
-| let Idx(k) = [0; arity(k)[
-| let First(∅) = ⊥
-| let First((aⱼ)ʲ) = a_{min(j)} ## where j ∈ J ≠ ∅
+Let's first define
+| let Idx(k) := [0; arity(k)[
+| let First(∅) := ⊥
+| let First((aⱼ)ʲ) := a_{min(j∈J≠∅)} 
+\[
+m := ((a_i)^i ((p_{ij})^i \to e_j)^{ij})
+\]
+\[
+ (k_k)^k := headconstructor(p_{i0})^i
+\]
+\begin{equation}
+\begin{align}
+ Groups(m) := ( k_k \to  ((a)_{0.l})^{l  \in  Idx(k_k)} +++ (a_i)^{i \in I\backslash \{0\} }), \\
+    ( if p_{0j} is k(q_l) then \\
+        (qₗ)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}}  \to e_j \\
+     if p_{0j} is \_ then \\
+        (\_)^{l \in Idx(k_k)} +++ (p_{ij})^{i \in I\backslash \{0\}}   \to e_j \\
+     else \bot  )^j ), \\
+  ((a_i)^{i \in I\backslash \{0\}}, ((p_{ij})^{i \in I\backslash \{0\}}  \to eⱼ if p_{0j} is \_ else \bot)^{j \in J}) 
+\end{align}
+\end{equation}
+
+Groups(m) is an auxiliary function that decomposes a matrix m into
+submatrices, according to the head constructor of their first pattern.
+Groups(m) returns one submatrix m_r for each head constructor k that
+occurs on the first row of m, plus one "wildcard submatrix" m_{wild}
+that matches on all values that do not start with one of those head
+constructors.
+
+Intuitively, m is equivalent to its decompositionin the following
+sense: if the first pattern of an input vector (v_i)^i starts with one
+of the head constructors k, then running (v_i)^i against m is the same
+as running it against the submatrix m_k; otherwise (its head
+constructor is none of the k) it is equivalent to running it against
+the wildcard submatrix.
+
+We formalize this intuition as follows:
+Lemma (Groups):
+Let \[m\] be a matrix with \[Groups(m) = (k_r \to m_r)^k, m_{wild}\].
+For any value vector \[(v_i)^l\] such that \[v_0 = k(v'_l)^l\] for some
+constructor k,
+we have:
+\[
+  if k = kₖ for some k then
+    m(vᵢ)ⁱ = mₖ((v'ₗ)ˡ +++ (vᵢ)^{i∈I\backslash \{0\}})
+  else
+    m(vᵢ)ⁱ = m_{wild}(vᵢ)^{i∈I\backslash \{0\}}
+\]
+
+*** Proof:
+Let \[m\] be a matrix with \[Group(m) = (k_r \to m_r)^k, m_{wild}\].
+Let \[(v_i)^i\] be an input matrix with \[v_0 = k(v'_l)^l\] for some k.
+We proceed by case analysis:
+- either k is one of the kₖ for some k
+- or k is none of the (kₖ)ᵏ
+
+Both m(vᵢ)ⁱ and mₖ(vₖ)ᵏ are defined as the first matching result of
+a family over each row rⱼ of a matrix 
+
+We know, from the definition of
+Groups(m), that mₖ is 
+\[
+    ((a){0.l})^{l∈Idx(kₖ)} +++ (aᵢ)^{i∈I\backslash \{0\}}),
+    (
+     if p_{0j} is k(qₗ) then
+        (qₗ)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}} → eⱼ 
+     if p_{0j} is _ then
+        (_)ˡ +++ (p_{ij})^{i∈I\backslash \{0\}}   → eⱼ 
+     else ⊥
+    )ʲ
+\]
+
+By definition, m(vᵢ)ⁱ is
+m(vᵢ)ⁱ = First(rⱼ(vᵢ)ⁱ)ʲ for m = ((aᵢ)ⁱ, (rⱼ)ʲ)
+(pᵢ)ⁱ (vᵢ)ⁱ  =  {
+    if p₀ = k(qₗ)ˡ, v₀ = k'(v'ₖ)ᵏ, k=Idx(k') and l=Idx(k)
+      if k ≠ k' then ⊥ 
+      if k = k' then ((qₗ)ˡ +++ (pᵢ)^{i∈I\backslash \{0\}}) ((v'ₖ)ᵏ +++ (vᵢ)^{i∈I\backslash \{0\}})
+    if p₀ = (q₁|q₂) then
+      First(  (q₁pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}}, (q₂pᵢ^{i∈I \backslash \{0\}}) vᵢ^{i∈I \backslash \{0\}}  )
+}
+
+For this reason, if we can prova that 
+| ∀j,  rⱼ(vᵢ)ⁱ = r'ⱼ((v'ₖ)ᵏ ++ (vᵢ)ⁱ)
+it follows that 
+| m(vᵢ)ⁱ = mₖ((v'ₖ)ᵏ ++ (vᵢ)ⁱ)
+from the above definition.
+
+We can also show that aᵢ = a){0.l}ˡ +++ a_{i∈I\backslash \{0\}} because v(a₀) = K(v(a){0.l})ˡ)
 
 
 
@@ -1426,7 +1511,10 @@ an accessor → π relation (In other words???)
                             
    Covering lemma:
          ∀a,π covers(Cₜ,S) => covers(C_{t/a→π}, (S∩a→π))
-             Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %% # TODO swap π and π' 
+             Uᵢπⁱ ≈ Uᵢπ'∩(a→π) ≈ (Uᵢπ')∩(a→π) %%
+\begin{comment}
+Should I swap π and π' 
+\end{comment}
 
 \subsubsection Proof of equivalence checking
 The equivalence checking algorithm takes as parameters an input space
@@ -1462,12 +1550,16 @@ TODO: explain:
 \end{comment}
 
 We proceed by case analysis:
-1. equiv(∅, Cₛ, Cₜ) := Yes
 \begin{comment}
-Devo spiegarlo?
+I start numbering from zero to leave the numbers as they were on the blackboard, were we skipped some things
+I think the unreachable case should go at the end.
 \end{comment}
-In the other subcases S is always non-empty.
 0. in case of unreachable: Cₛ(vₛ) = Absurd(Unreachable) ≠ Cₜ(vₜ) ∀vₛ,vₜ
+1. In the case of an empty input space
+| equiv(∅, Cₛ, Cₜ) := Yes
+and that is trivial to prove because there is no pair of values (vₛ, vₜ) that could be
+tested against the decision trees.
+In the other subcases S is always non-empty.
 2. equiv(S, Failure, Failure) := Yes
    the statement holds because of equality between Failure nodes in
    the case of every possible value /v/.
@@ -1491,7 +1583,7 @@ In the other subcases S is always non-empty.
    | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I
 4. equiv(S, Node(a, (kᵢ → Cₛᵢ)ⁱ, C_{sf}), Cₜ) := 
     let π' = ⋃π(kᵢ) ∀i in
-    Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++   equiv(S∩(a→π(kᵢ)), Cₛ, C_{/a¬̸π'}))
+    Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ +++   equiv(S∩(a→π(kᵢ)), Cₛ, C_{/a̸¬̸π'}))
     The statement  holds because:
     a. Forall(equiv( S∩(a→π(kᵢ)ⁱ), Cₛᵢ, C_{t/a→π(kᵢ)})ⁱ = Yes
        In the yes case let's reason by case analysis:
@@ -1503,9 +1595,10 @@ In the other subcases S is always non-empty.
             Putting all together:
             Cₛ(vₛ) = Cₛᵢ(vₛ) = C_{t/a→πᵢ}(vₜ) = Cₜ(vₜ)
             
-       ii. or k∉(kᵢ)ⁱ ???
+       ii. when k∉(kᵢ)ⁱ ???
 
     b. Forall(...) = No(vₛ, vₜ)
         for a minimum k, equiv(Sₖ, Cₛₖ, C_{t/a→πₖ} = No(vₛ, vₜ)
            then Cₛₖ(vₛ) ≠ C_{t/a→πₖ}(vₜ)  and C_{t/a→πₖ}(vₜ) = Cₜ(vt) 
-             => (Cₛₖ(vₛ) = Cₛ(vₛ)) ≠ Cₜ(vₜ) # Same for fallback?
+             => (Cₛₖ(vₛ) = Cₛ(vₛ)) ≠ Cₜ(vₜ)
+        # Same for fallback?