Commit 3aa99b84 by Allan Blanchard

### [wp/doc] Reorganizes tactics documentation

parent a0ed60b5
 ... @@ -256,6 +256,8 @@ This mode replays the automated proofs and the interactive ones, re-running Alt- ... @@ -256,6 +256,8 @@ This mode replays the automated proofs and the interactive ones, re-running Alt- \newcommand{\TACTIC}[2]{#1\quad\quad\triangleright\quad\quad#2} \newcommand{\TACTIC}[2]{#1\quad\quad\triangleright\quad\quad#2} \subsubsection{General} \paragraph{Absurd} Contradict a Hypothesis\\ \paragraph{Absurd} Contradict a Hypothesis\\ The user can select a hypothesis $H$, and change the goal to $\neg H$: The user can select a hypothesis $H$, and change the goal to $\neg H$: ... @@ -303,6 +305,9 @@ $$\TACTIC{\Delta\models\,G}{% ... @@ -303,6 +305,9 @@$$\TACTIC{\Delta\models\,G}{% \Delta,\neg C \models G \Delta,\neg C \models G \end{array}} $$\end{array}}$$ \paragraph{Definition} Unfold predicate and logic function definition\\ The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available. \paragraph{Filter} Erase Hypotheses \\ \paragraph{Filter} Erase Hypotheses \\ The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed. The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed. ... @@ -323,22 +328,11 @@ $$\TACTIC{\Delta,\,\forall x\, P(x)\models G}{\Delta,P(n)\ldots P(m)\models G}$$ ... @@ -323,22 +328,11 @@ $$\TACTIC{\Delta,\,\forall x\, P(x)\models G}{\Delta,P(n)\ldots P(m)\models G}$$ When instantiating a goal with an expression $e$: When instantiating a goal with an expression $e$: $$\TACTIC{\Delta\models \exists x\,G(x)}{\Delta\models G(e)}$$ $$\TACTIC{\Delta\models \exists x\,G(x)}{\Delta\models G(e)}$$ \paragraph{Lemma} Search \& Instantiate Lemma\\ The user start by selecting a term in the goal. Then, the search button in the tactic panel will display a list of lemma related to the term. Then, he can instantiate the parameters of the lemma, like with the Instance tactic. \paragraph{Intuition} Decompose with Conjunctive/Disjunctive Normal Form\\ \paragraph{Intuition} Decompose with Conjunctive/Disjunctive Normal Form\\ The user can select a hypothesis or a goal with nested conjunctions and disjunctions. The tactics then computes the conjunctive or disjunctive normal form of the selection and split the goal accordingly. The user can select a hypothesis or a goal with nested conjunctions and disjunctions. The tactics then computes the conjunctive or disjunctive normal form of the selection and split the goal accordingly. \paragraph{Range} Enumerate a range of values for an integer term\\ \paragraph{Lemma} Search \& Instantiate Lemma\\ The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $eb$: The user start by selecting a term in the goal. Then, the search button in the tactic panel will display a list of lemma related to the term. Then, he can instantiate the parameters of the lemma, like with the Instance tactic. $$\TACTIC{\Delta\models\,G}{% \begin{array}[t]{ll} \Delta,eb &\models G \end{array}}$$ \paragraph{Rewrite} Replace Terms\\ \paragraph{Rewrite} Replace Terms\\ This tactic uses an equality in a hypothesis to replace each occurrence of term by another one. This tactic uses an equality in a hypothesis to replace each occurrence of term by another one. ... @@ -384,49 +378,7 @@ Finally, when the user select a arithmetic comparison over $a$ and $b$, the tact ... @@ -384,49 +378,7 @@ Finally, when the user select a arithmetic comparison over $a$ and $b$, the tact \Delta,a>b&\models G \Delta,a>b&\models G \end{array}} \] \end{array}} \] \paragraph{Definition} Unfold predicate and logic function definition\\ \subsubsection{Over integers} The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available. \paragraph{Bitwise} Decompose equalities over $N$-bits\\ The use selects an integer equality and a number of bits. Providing the two members of the equality are in range $0..2^N-1$, the equality is decomposed into $N$ bit-tests equalities: $\TACTIC{\Delta\models G}{% \begin{array}[t]{rcl} \Delta\phantom{)} &\models & 0 \leq a,b < 2^N \\ \sigma(\Delta) & \models & \sigma(G) \end{array} }$ where $\sigma$ is the following subsitution: $\sigma \equiv \left[ a=b \quad \leftarrow \bigwedge_{k\in 0..N-1} \mathtt{bit\_test}(a,k) = \mathtt{bit\_test}(b,k) \right]$ The \lstinline{bit_test(a,b)} function is predefined in \textsf{WP} and is equivalent to the \textsf{ACSL} expression \lstinline{(a & (1 << k)) != 0}. The \textsf{Qed} engine has many simplification rules that applies to such patterns, and the a tactic is good way to reason over bits. \paragraph{Shift} Transform logical shifts into arithmetics\\ For positive integers, logical shifts such as \lstinline{a << k} and \lstinline{a >> k} where \lstinline$k$ is a constant can be interpreted into a multiplication or a division by $2^k$. When selecting a logical-shift, the tactic performs: $\TACTIC{\Delta\models G}{% \begin{array}[t]{rcl} \Delta\phantom{)} &\models& 0 \leq a \\ \sigma(\Delta) &\models& \sigma(G) \end{array} }$ where: \begin{tabular}[t]{ll} $\sigma = [ \mathtt{lsl}(a,k) \leftarrow a * 2^k ]$ & for left-shift, \\ $\sigma = [ \mathtt{lsr}(a,k) \leftarrow a / 2^k ]$ & for right-shifts. \end{tabular} \paragraph{BitRange} Range of logical bitwise operators \\ \paragraph{BitRange} Range of logical bitwise operators \\ This tactical applies the two following lemmas to the current goal. This tactical applies the two following lemmas to the current goal. ... @@ -453,6 +405,28 @@ to apply the theorems. Such a strategy is \emph{not} complete in general. ... @@ -453,6 +405,28 @@ to apply the theorems. Such a strategy is \emph{not} complete in general. Typically, $\mathtt{land}(x,y) < 38$ is true whenever both $x$ and $y$ are in range $0\ldots 31$, but this is also true Typically, $\mathtt{land}(x,y) < 38$ is true whenever both $x$ and $y$ are in range $0\ldots 31$, but this is also true in other cases. in other cases. \paragraph{Bitwise} Decompose equalities over $N$-bits\\ The use selects an integer equality and a number of bits. Providing the two members of the equality are in range $0..2^N-1$, the equality is decomposed into $N$ bit-tests equalities: $\TACTIC{\Delta\models G}{% \begin{array}[t]{rcl} \Delta\phantom{)} &\models & 0 \leq a,b < 2^N \\ \sigma(\Delta) & \models & \sigma(G) \end{array} }$ where $\sigma$ is the following subsitution: $\sigma \equiv \left[ a=b \quad \leftarrow \bigwedge_{k\in 0..N-1} \mathtt{bit\_test}(a,k) = \mathtt{bit\_test}(b,k) \right]$ The \lstinline{bit_test(a,b)} function is predefined in \textsf{WP} and is equivalent to the \textsf{ACSL} expression \lstinline{(a & (1 << k)) != 0}. The \textsf{Qed} engine has many simplification rules that applies to such patterns, and the a tactic is good way to reason over bits. \paragraph{Congruence} Simplify Divisions and Products \\ \paragraph{Congruence} Simplify Divisions and Products \\ This tactic rewrites integer comparisons involving products and divisions. This tactic rewrites integer comparisons involving products and divisions. The tactic applies one of the following theorems to the current goal. The tactic applies one of the following theorems to the current goal. ... @@ -471,7 +445,7 @@ n|k, n|k', & (k/n).a = (k'/n).b &\Longleftrightarrow& k.a = k'.b ... @@ -471,7 +445,7 @@ n|k, n|k', & (k/n).a = (k'/n).b &\Longleftrightarrow& k.a = k'.b \] \] \paragraph{Overflow} Integer Conversions \\ \paragraph{Overflow} Integer Conversions \\ This tactic rewrites machine integer conversions by identify, This tactic rewrites machine integer conversions by identity, providing the converted value is in available range. The tactic applies on expression providing the converted value is in available range. The tactic applies on expression with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer name, with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer name, \emph{eg.} \texttt{to\_uint32}. \emph{eg.} \texttt{to\_uint32}. ... @@ -485,6 +459,36 @@ with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer n ... @@ -485,6 +459,36 @@ with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a a machine-integer n where $\sigma = [ \mathtt{to\_iota}(e) \mapsto e ]$ and $[a..b]$ is the range where $\sigma = [ \mathtt{to\_iota}(e) \mapsto e ]$ and $[a..b]$ is the range of the \texttt{iota} integer domain. of the \texttt{iota} integer domain. \paragraph{Range} Enumerate a range of values for an integer term\\ The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $eb$: $$\TACTIC{\Delta\models\,G}{% \begin{array}[t]{ll} \Delta,eb &\models G \end{array}}$$ \paragraph{Shift} Transform logical shifts into arithmetics\\ For positive integers, logical shifts such as \lstinline{a << k} and \lstinline{a >> k} where \lstinline$k$ is a constant can be interpreted into a multiplication or a division by $2^k$. When selecting a logical-shift, the tactic performs: $\TACTIC{\Delta\models G}{% \begin{array}[t]{rcl} \Delta\phantom{)} &\models& 0 \leq a \\ \sigma(\Delta) &\models& \sigma(G) \end{array} }$ where: \begin{tabular}[t]{ll} $\sigma = [ \mathtt{lsl}(a,k) \leftarrow a * 2^k ]$ & for left-shift, \\ $\sigma = [ \mathtt{lsr}(a,k) \leftarrow a / 2^k ]$ & for right-shifts. \end{tabular} \subsection{Strategies} \subsection{Strategies} Strategies are heuristics that generate a prioritized bunch of tactics to be tried on the current goal. Strategies are heuristics that generate a prioritized bunch of tactics to be tried on the current goal. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!