From 11b8ffd8b6e7b138fe8502e0fc65dfae8ef6cd23 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Fri, 9 Mar 2018 21:39:58 0500
Subject: [PATCH] books/bookvol13 add chapter Here is the Problem
Goal: Proving Axiom Correct

books/bookvol13.pamphlet  421 ++++++++++++++++++++++++++++++++++++++++
changelog  2 +
patch  91 +
src/axiomwebsite/patches.html  2 +
4 files changed, 424 insertions(+), 92 deletions()
diff git a/books/bookvol13.pamphlet b/books/bookvol13.pamphlet
index 5736bc2..6ad3f57 100644
 a/books/bookvol13.pamphlet
+++ b/books/bookvol13.pamphlet
@@ 431,6 +431,29 @@ proofs which were checked algorithmically.
\chapter{Here is a problem}
+Axiom has a domainspecific language for mathematical computation
+called Spad. This is implemented in Common Lisp. Our version of
+Common Lisp compiles to C. The C code is then compiled to machine
+code. The machine code is executed by a physical machine.
+
+There are various attacks on each of these areas. We will be
+addressing them all at some point, from the mathematical specification,
+through the Spad code all the way down to the hardware timing signals.
+
+One useful technique to exploit is mentioned by Myreen, Slind, and
+Gordon \cite{Myre09a}. They 'forward compile' the code to $f$, collect
+the result as $f^\prime$, and then prove the $f=f^\prime$. This proof
+is sufficient to show that the compile step is correct.
+
+\section{Proving the Algebra}
+\subsection{Defining the Spad syntax}
+\subsection{Defining the Spad semantics}
+
+Floyd \cite{Floy67}, Back \cite{Back81}, Caldwell \cite{Cald97},
+Filliatre \cite{Fill03}, Filliatre and Paskevich \cite{Fill13}
+
+\section{Proving the Logic}
+
Proving programs correct involves working with a second programming
language, the proof language, that is wellfounded on some theory.
Proofs (programs), can be reduced (compiled) in this new language
@@ 442,6 +465,53 @@ the proof language. Unfortunately that is not (yet?) the case with Spad.
The COQ system language, Gallina, is the closest match to Spad.
+
+Davis \cite{Davi09},
+Myreen and Davis \cite{Myre11}, Myreen and Davis \cite{Myre14},
+Davis and Myreen \cite{Davi15}
+
+\subsection{Defining the Algebra specifications}
+
+Talpin and Jouvelot \cite{Talp92}
+
+\section{Proving the Lisp}
+
+Myreen \cite{Myre12}
+
+\section{Proving the Compiler}
+
+Myreen \cite{Myre10}
+
+\section{Proving to the metal}
+
+Myreen and Gordon \cite{Myre09}, Myreen, Slind, and Gordon \cite{Myre09a}
+
+
+Domipheus \cite{Domi18} provides a VHDL (hardware description language)
+CPU which provides the actual electrical timing of signals all the way
+up to a machine language which consists of
+
+\begin{tabular}{ll}
+\hline
+OPERATION & FUNCTION\\
+\hline
+Add & D = A + B\\
+Substrct & D = A  B\\
+Bitwise Or & D = A or B\\
+Bitwise Xor & D = A xor B\\
+Bitwise And & D = A and B\\
+Bitwise Not & B = not A\\
+Read & D = Memory[A]\\
+Write & Memory[A] = B\\
+Load & D = 8bit immediate value\\
+Compare & D = cmp(A,B)\\
+Shift Left & D = A $<<$ B\\
+Shift Right & D = A $>>$ B\\
+Jump/Branch & PC = A Register or Immediate Value\\
+Jump/Brance conditionally & PC = Register if (condition) else nop\\
+\hline
+\end{tabular}
+
\section{Setting up the problem}
The GCD function will be our first example of a proof.
@@ 3446,8 +3516,6 @@ $\bot \rightarrow \exists k A(k)$ of exfalsoquodlibet.
In our case, when the existential quantifier is of type nat
one might as well pick the constant 0 (as we did in the text).


\subsection{Cardelli \cite{Card85}}
Cardelli states that {\bf coercions} are a
@@ 3477,8 +3545,195 @@ See p516 for the Classification of Type Systems diagram.
Clarke shows several proofs
+\newpage
+\subsection{Crocker \cite{Croc14}}
+
+\begin{center}
+{\bf Primary specification constructs}
+\end{center}
+
+\begin{tabular}{ll}
+\hline
+{\bf pre}(expressionlist) & Declares preconditions\\
+\hline
+{\bf post}(expressionlist) & Declares postconditions\\
+\hline
+& Declares the value returned by a\\
+& function. Equivalent to {\bf post(result)} ==\\
+{\bf returns}(expression) & {\sl expression} except that recursion is\\
+& permitted in {\sl expression}\\
+\hline
+{\bf assert}(expressionlist) & Asserts conditions\\
+\hline
+& Used in class declarations to declare\\
+{\bf invariant}(expressionlist) & class invariants, and in {\bf typedef}\\
+& declarations to declare constraints\\
+\hline
+{\bf keep}(expressionlist) & Declares loop invariants\\
+\hline
+{\bf decrease}(expressionlist) & Declares loop variant or recursion\\
+& variant expressions\\
+\hline
+& Declares what nonlocal variables the\\
+& function modifies. If a function is\\
+{\bf writes}(lvalueexpressionlist)
+& declared without a writesclause, then\\
+& a default writesclause is constructed\\
+& based on the signature of the function\\
+\hline
+{\bf assumes}(expressionlist) & Declares predicates to be assumed\\
+& without proof\\
+\hline
+{\bf ghost}(expressionlist) & Declares ghost variables, functions\\
+& parameters, etc.\\
+\hline
+\end{tabular}
+
+\newpage
+\begin{center}
+{\bf Additional specification expressions}
+\end{center}
+
+\begin{tabular}{ll}
+\hline
+{\bf exists} {\sl identifier} {\bf in} & Existential quantification over the\\
+{\sl expression} : {\sl predicate}
+& elements of {\sl expression} which must be\\
+& an array or an abstract collection type\\
+\hline
+{\bf exists} {\sl type identifier} := & Existential quantification over all\\
+{\sl predicate} & values of type\\
+\hline
+{\bf forall} {\sl identifier} {\bf in} & Universal quantification over the\\
+{\sl expression} : {\sl predicate}
+& elements of {\sl expression}, which must be \\
+& an array or an abstract collection type\\
+\hline
+{\bf forall} {\sl type identifier} : & Universal quantification over all\\
+{\sl predicate} & values of type\\
+\hline
+& Applies the mapping function\\
+{\bf for} {\sl identifier} {\bf in} {\sl expression1}
+& {\sl expression2} to each element of\\
+{\bf yield} {\sl expression2}
+& collection {\sl expression1}, yielding a new\\
+& collection\\
+\hline
+{\bf those} {\sl identifer} {\bf in} & Selects those elements of collection\\
+{\sl expression1} : {\sl predicate}
+& {\sl expression1} for which {\sl predicate} is\\
+& true\\
+\hline
+{\bf that} {\sl identifier} {\bf in} & Selects the single element of the\\
+{\sl expression1} : {\sl predicate}
+& collection {\sl expression1} for which\\
+& {\sl predicate} is true\\
+\hline
+& Shorthand for {\bf exists} {\sl id} {\bf in} {\sl expression2}\\
+{\sl expression1} {\bf in} {\sl expression2}
+& : {\sl id} == {\sl expression1}, where {\sl id} is a new\\
+& identifier\\
+\hline
+& {\sl expression} must have union type, and\\
+& {\sl member} must be a member of that\\
+{\sl expression} {\bf holds} {\sl member}
+& type. Yields true if and only if the\\
+& value of {\sl expression} was defined by\\
+& assignment or initialization through\\
+& {\sl member}\\
+\hline
+& Yields true if and only if no two\\
+& objects in the expression list have\\
+{\bf disjoint}({\sl lvalueexpressionlist})
+& overlapping storage. Typically used\\
+& in preconditions to state that parameters\\
+& passed by pointer or reference refer to\\
+& distinct objects\\
+\hline
+& Leftfold {\sl operator} over collection\\
+{\sl operator} {\bf over} {\sl expression}
+& {\sl expression}. Used to express e.g.\\
+& summation of the elements of an array\\
+\hline
+& When used in a postcondition, this\\
+& referes to the value of {\sl expression} when\\
+& the function was entered. When used\\
+{\bf old}{\sl (expreesion)} & in a loop invariant, it refers to the\\
+& value of {\sl expression} just before the\\
+& first iteration of the loop.\\
+\hline
+\end{tabular}
+
\subsection{Davenport \cite{Dave02}}
+\subsection{Davis \cite{Davi09}}
+
+Davis creates a verified proof checker by creating a simple, obviously
+correct ``level 1'' checker based on a few rules. A ``level 2''
+checker is implemented and verified by level 1. This bootsrap process
+continues up to level 11 which has significant power. Every level 11
+proof can be reduced to a level 1 proof, giving a solid foundation.
+
+
+\subsection{Filliatre \cite{Fill03}}
+
+A formal method to establish software correctness can involve several
+steps. The first one is the {\sl specification}. A second one is a
+method to generate some {\sl proof obligations}. And a third one is a
+framework to {\sl establish their validity}.
+
+Type theory identifies types with propositions and terms with proofs,
+through the widely known CurryHoward isomorphism. There is no real
+difference between the usual firstorder objects of the mathematical
+discourse  such as naturals, sets, and so forth  and the proof
+objects. The natural 2 is a firstorder object of type {\tt nat}, and
+a proof that 2 is even is a firstorder object of type {\sl
+even}(2). One can define a function $f$ taking as arguments a natural
+$n$ and a proof that $n$ is even, and its type would be something like
+$\forall n:{\tt nat}.even(n)\rightarrow\tau$. Such a function
+represents a {\sl partial function} on naturals, where the proof of
+{\sl even(n)} may be seen as a {\sl precondition}. Similarly, one can
+define a function returning a proof term. For instance, the function
+$f$ could return a natural $p$ and a proof that $n=2\times
+p$. Finally, the type of $f$ will look like
+\[\forall n:{\tt nat}.even(n)\rightarrow\exists p:{\tt nat}.n=2\times p\]
+where the proof of $n=2\times p$ may be seen as a {\sl
+postcondition}. More generally, a type of the form
+\[forall x : nat. P(x)\rightarrow\exists y:nat.Q(x,y)\]
+is the type of a function with a precondition $P$ and a postcondition
+$Q$. Building a term of this type is exactly like building a function
+together with a proof of its correctness, and consequently type theory
+appears as naturally suited for the proof of purely functional
+programs.
+
+We propose an interpretation of the Hoare triple $\{P\}e\{Q\}$ as a
+proof of the above proposition and then define a systematic
+construction of this proof from a given annotated program, where the
+lacking proof terms are the socalled proof obligations.
+
+The Coq {\bf Correctness} tactic takes an annotated program as
+argument and generates a set of goals, which are logical propositions
+to be proved by the user. Given an annotated program $e$, the tactic
+{\bf Correctness} applies the following steps:
+\begin{enumerate}
+\item It determines the type of computation of $\kappa$ of $e$ by the
+typing algorithm
+\item proposition $\hat{\kappa}$ is computed and declared as a goal
+\item The partial proof term $\hat{e}$ is computed following
+Definition 8 and is given to the proof engine, using the {\tt Refine}
+tactic developed on purpose, and each hole in $\hat{e}$ leads to a
+subgoal
+\item Once the proofs are completed, the program is added to the
+environment and may be used in other programs
+\end{enumerate}
+
+Some features have been added to simplify the specification of
+programs  mainly, the possibility of inserting labels in the
+programs and referring in annotations to the value that a reference
+had at the program points corresponding to those labels. In
+particular, a loop invariant may mention the values of the references
+at some point before the loop using such a label.
+
\subsection{Frege \cite{Freg1891}}
Function and Concept seminal paper
@@ 3807,6 +4062,122 @@ of multivariate polynomials in SML \cite{Mein13}.
details the foundations for relational logic programming
with polymorphically ordersorted data types.
+\subsection{Strub, Pierre Yves}
+\begin{verbatim}
+Formal Proofs and Decision Procedures (Strub, Pierre Yves)
+htps://www.youtube.com/watch?v=YgOoDNIT8A8
+year = "2016"
+
+Prop is a type containing other types
+The inhabitants of Prop are proof types or propositions
+If A:Prop and B:Prop are proof types then A>B is a proof type (implication)
+A proof type is valid if there exists a program of that type
+(fun (x:A) => x) is a proof of (A > A)
+
+Elimination of the \forall connector
+ \forall x,P
+ 
+ P{x \mapsto t}
+ We want to express a proof of (\forall x,P) by a function taking a t
+ and returning a proof of P(t)
+ The result type depends on the input
+ Dependent typ: type that depends on a value
+
+Arithmetic (P. Cregut)
+Real Arithmetic (L Pottier)
+First Order Logic (P Corbineau)
+Polynomial Systems (B Barras, B Gregoire, A Mahboubi)
+External Oracles (N Ayache JC Filliatre)
+
+two terms are computationally equal are considered identical
+
+Fact fact1 A B C : (A > B > C) > (A > B) > A > C
+fact1 = fun (A B C : Type) (HABC : A > B > C) (HAB : A > B) (HA : A) =>
+HABC HA (HAB HA) : forall A B C : Type, (A > B > C) > (A > B) > A > C
+
+Fact fact2 A B C : (A > B > C) > (A > B) > A > C
+fact2 = fun (A B C : Type) (X : A > B > C) (X0 : A > B) (X1 : A) =>
+let X2 := X X1 in let X3 := X0 X1 in unkeyed (X2 X3)
+ : forall A B C : (A > B > C) > (A > B) > A > C
+
+Fact fact3 (m n:Z) : (1 + 2 * m <> 2 * n)%Z
+fact3  fun (m n : Z) (H : (1 + 2 * M)%Z = (2 * n)%Z) =>
+let H0 :=
+ fact_Zmult comm 2 m (fun x : Z => (1 + x +  (2 * n))%Z = 0%Z > False)
+ (fast_Zplus_comm 1 (m * 2)
+ (fun x : Z => (x +  (2 * n))%Z = 0%Z > False)
+ (fast _Zmult_comm 2 n (fun x :Z => (M * 2 + 1  x)%Z = 0%Z > False)
+ (fast_Zopp_mult disr r n 2
+ (fun x : Z => (m * 2 + 1 + x)%Z = 0%Z > False)
+ (fast_Zplus_comm (m * 2 + 1) (n * 2)
+ (fun x : Z => x = 0%Z > False)
+ (fun Omega0 : (n * 2 + (m * 2 + 1))%Z = 0%Z =>
+ let H0 := erefl Gt in
+ (let H1 := erefl Gt in
+ fun auxiliary_1 : (1 > 0)%Z =>
+ OMEGA4 1 2 (n * 1 + (m * 1 + 0)) auxiliary_1 H1
+ (fast_OMEGA11 n (1) (m * 1 + 0) 1 2
+ (eq^ 0%Z)
+ (fast_OMEGA11 m 1 0 1 2
+ (fun x : Z => (n * (1 * 2) + x)%Z = 0%Z)
+
+Fact fact4: 2 + 2 = 4
+fact4 =
+ eq_ind_r (eq^  4)
+ (eq_ind_r (fun _pattern_value : nat => _pattern_value_.+1 = 4)
+ (eq_ind_r (fun _pattern_value : nat => _pattern_value_.+2 = 4) (erefl 4) (addn0 2))
+ (addnS 2 0))
+ (addnS 2 1) : 2 + 2 = 4
+
+ \forall x,x+0 = x \forall x y, x+S(y)=S(x+y)
+
+2+2 = 4 is proved by
+
+  \forall x,x+S(y)=S(x+y)  \forall x,x+S(y)=S(x+y)
+  
+  2+2 = S(2+1)  S(2+1) = S(S(2+0))  \forall x,x+0 = x
+  
+  2+2 = S(2+0)  S(2+0) = 4
+ 
+  2+2 = 4
+
+Calculus of Construction (Coquand, Huet, 1985)
+ \beta convertibility
+Calculus of Inductive Construction (Coquand, Paulin, 1990)
+ \beta convertibility + recursors for inductive types
+Extensional Calculus of Construction (Oury 05)
+ \beta + convertible
+ "any terms which can be proven equal are convertible"
+ (BUT proof checking isn't decidable because convertibility is not decidable)
+Coq Modulo Theory (TCS'08, CSL'10, LICS'11) (Strub, Pierre Yves)
+ add decision procedure to conversion rule
+Calculus of Presburger Constructions
+ \beta conversions (function evaluation)
+ recursor for natural numbers (def. by induction of functions and types)
+ a decision procedure for Presburger arithmetic in its conversion
+ an extraction from the proof environment of arithmtic equations
+ whose proof checking is decidable
+
+ \Gamma  t:T \Gamma  T':s' T ~r T'
+ 
+ \Gamma  t:T'
+
+ where ~r will include
+ \betaconvertibility (function evaluation)
+ recursor for natural numbers (fixpoint+match evaluation)
+ validity entailment of the Presburger arithmetic
+ At least, the conversion must consider equal
+ any pair of Presburgerequal algebraic terms
+ Algebraic terms are all terms built from 0, S,+ and variables with the right arity
+ This solves our motivation examples
+ list n + m ~ list m + n
+ because n + m and m + n are algebraic and Pequal
+ BUT this does not define a sound logic
+
+
+
+\end{verbatim}
+
\subsection{Sutor \cite{Suto87}}
Type inference and coercion in Scratchpad II.
@@ 3831,6 +4202,52 @@ syntactic criteria generalizes primitive recursion and handles
most of the examples given by Walthar. We call the corresponding
class of acceptable defintions ``Walther recursive''.",
+\appendix
+
+\chapter{Untyped Lambda in Common Lisp}
+See Garret \cite{Garr14}
+
+This is a compiler for the untyped lambda calculus.
+\begin{chunk}{lambda}
+(defmacro ulambda (args body)
+ (if (and args (atom args)) (setf args (list args)))
+ (if (and (consp body) (consp (car body))) (push 'funcall body))
+ (if (null args)
+ body
+ `(lambda (&rest args1)
+ (let ((,(first args) (first args1)))
+ (declare (ignorable ,(first args)))
+ (flet ((,(first args) (&rest args2) (apply ,(first args) args2)))
+ (if (rest args1)
+ (apply (ulambda ,(rest args) ,body) (rest args1))
+ (ulambda ,(rest args) ,body)))))))
+
+\end{chunk}
+
+The factorial function.
+\begin{chunk}{factorial}
+(ulambda (n f)
+ (n (ulambda (c i)
+ (i (c (ulambda (f x)
+ (i f (f x))))))
+ (ulambda x f)
+ (ulambda x x)))
+
+\end{chunk}
+
+The factorial of 10. factorial of 3, add 4, compute factorial of that.
+\begin{chunk}(factorial10}
+(ulambda ()
+ ((ulambda (f s) (f (s (s (s (s (f (s (s (s (ulambda (f x) x)))))))))))
+ (ulambda (n f) (n (ulambda (c i) (i (c (ulambda (f x) (i f (f x))))))
+ (ulambda x f) (ulambda x x)))
+ (ulambda (n f x) ((n f) (f x)))
+ '1+ 0))
+
+\end{chunk}
+
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\cleardoublepage
\phantomsection
diff git a/changelog b/changelog
index 7baf53f..125427a 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,5 @@
+20180309 tpd src/axiomwebsite/patches.html 20180309.03.tpd.patch
+20180309 tpd books/bookvol13 add chapter Here is the Problem
20180309 tpd src/axiomwebsite/patches.html 20180309.02.tpd.patch
20180309 tpd books/bookvolbib add references
20180309 tpd src/axiomwebsite/patches.html 20180309.01.tpd.patch
diff git a/patch b/patch
index 780bf5f..5481c88 100644
 a/patch
+++ b/patch
@@ 1,93 +1,4 @@
books/bookvolbib add references
+books/bookvol13 add chapter Here is the Problem
Goal: Proving Axiom Correct
\index{Myreen, Magnus O.}
\begin{chunk}{axiom.bib}
@article{Myre10,
 author = "Myreen, Magnus O.",
 title = {{Verified JustInTime Compiler on x86}},
 journal = "ACM SIGLAN Notices  POPL'10",
 volume = "45",
 number = "1",
 year = "2010",
 pages = "107118",
 abstract =
 "This paper presents a method for creating formally correct justin
 time (JIT) compilers. The tractability of our approach is demonstrated
 through, what we believe is the first, verification of a JIT
 compiler with respect to a realistic semantics of selfmodifying x86
 machine code. Our semantics includes a model of the instruction
 cache. Two versions of the verified JIT compiler are presented: one
 generates all of the machine code at once, the other one is incremental
 i.e. produces code ondemand. All proofs have been performed
 inside the HOL4 theorem prover.",
 paper = "Myre10.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Myreen, Magnus O.}
\index{Gordon, Michael J.C.}
\begin{chunk}{axiom.bib}
@article{Myre09,
 author = "Myreen, Magnus O. and Gordon, Michael J.C.",
 title = {{Verified LISP Implementations on ARM, x86 and PowerPC}},
 journal = "LNCS",
 volume = "5674",
 pages = "359374",
 year = "2009",
 abstract =
 "This paper reports on a case study, which we believe is the
 first to produce a formally verified endtoend implementation of a func
 tional programming language running on commercial processors. Inter
 preters for the core of McCarthyâ€™s LISP 1.5 were implemented in ARM,
 x86 and PowerPC machine code, and proved to correctly parse, evaluate
 and print LISP sexpressions. The proof of evaluation required working
 on top of verified implementations of memory allocation and garbage
 collection. All proofs are mechanised in the HOL4 theorem prover.",
 paper = "Myre09.pdf",
 keywords = "printed"
}

\end{chunk}

\index{Myreen, Magnus O.}
\index{Slind, Konrad}
\index{Gordon, Michael J.C.}
\begin{chunk}{axiom.bib}
@article{Myre09a,
 author = "Myreen, Magnus O. and Slind, Konrad and Gordon, Michael J.C.",
 title = {{Extensible ProofProducing Compilation}},
 journal = "LNCS",
 volume = "5501",
 pages = "216",
 year = "2009",
 abstract =
 "This paper presents a compiler which produces machine code from
 functions defined in the logic of a theorem prover, and at the same
 time proves that the generated code executes the source functions.
 Unlike previously published work on proofproducing compilation from a
 theorem prover, our compiler provides broad support for userdefined
 extensions, targets multiple carefully modelled commercial machine
 lan guages, and does not require termination proofs for input
 functions. As a case study, the compiler is used to construct verified
 interpreters for a small LISPlike language. The compiler has been
 implemented in the HOL4 theorem prover.",
 paper = "Myre09a.pdf",
 keywords = "printed"
}

\end{chunk}

\begin{chunk}{axiom.bib}
@misc{Domi18,
 author = "Domipheus",
 title = {{Designing a CPU in VHDL}},
 link = "\url{http://labs.domipheus.com/blog/tpuseriesquicklinks}",
 year = "2018",
 abstract = "A VHDL CPU"
}

\end{chunk}
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 810c053..3f895eb 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5920,6 +5920,8 @@ proposal
books/bookvolbib add references
20180309.02.tpd.patch
books/bookvolbib add references
+20180309.03.tpd.patch
+books/bookvol13 add chapter Here is the Problem

1.9.1