\documentclass[11pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amsfonts,amssymb,amsthm}
\usepackage{geometry}
\usepackage{booktabs}
\usepackage{xcolor}
\usepackage{titlesec}
\usepackage{microtype}
\usepackage{graphicx}

% Page geometry
\geometry{margin=1in}

% Color definitions
\definecolor{primary}{RGB}{31, 78, 121}
\definecolor{secondary}{RGB}{90, 107, 124}
\definecolor{lightbg}{RGB}{245, 247, 250}

% Section styling
\titleformat{\section}{\color{primary}\large\bfseries}{\thesection}{1em}{}[{\titlerule[0.5pt]}]
\titleformat{\subsection}{\color{secondary}\normalsize\bfseries}{\thesubsection}{1em}{}

\newtheorem{theorem}{Theorem}


\title{\textbf{\color{primary}Termination of the Engel4 Program}}
\author{\textbf{Program Verification \& Analysis}}
\date{\today}

\begin{document}

\maketitle

\begin{abstract}
\noindent \em This file provides some additional information about the termination proof of the Engel4 program
\end{abstract}

% ------------------------------------------------------------------------------
\section{The Engel4 Program}
% ------------------------------------------------------------------------------
\noindent The Engel4 program shown below is based on problem 4 in \cite[pp. 9]{Enge91}. Since the program listed in \cite[pp. 9]{Enge91} terminates only if the sum of the variables \texttt{a} and \texttt{b} is a power of 2, the program below computes for a given number \texttt{a} the least power of two greater than \texttt{a} such that \texttt{b} can be determined accordingly:

 
\begin{center}\footnotesize
\begin{minipage}{0.8\textwidth}
\begin{verbatim}
    module Engel4(nat ?aIn, event !rdy) {
        nat a,b,lg1,lg2,pow2;
        a = aIn;
        // ---------------------------------------------------------------------
        // determine the least power of 2 greater than a and its logarithm
        // ---------------------------------------------------------------------
        lg1 = 0;
        pow2 = 1;
        while(a>=pow2) {
            next(lg1) = lg1+1;
            next(pow2) = pow2+pow2;
            p1:pause;
        }
        b = pow2-a;
        lg2 = 0;
        // ---------------------------------------------------------------------
        // the following is the core of the program which only terminates
        // if a+b is a power of 2, and a,b>0 holds as ensured by the loop above.
        // We have next(a) == (2*a<pow2 ? 2*a : 2*a-pow2) during the loop.
        // ---------------------------------------------------------------------
        while(a>0) {
            if(a<b) {
                next(a) = a+a;
                next(b) = b-a;
            } else {
                next(a) = a-b;
                next(b) = b+b;
            }
            next(lg2) = lg2 + 1;
            p2:pause;
        }
        emit(rdy);
    }
\end{verbatim}
\end{minipage}
\end{center}


\noindent Hence, the above program consists of two parts: The first part stores the given input \texttt{aIn} in the local variable \texttt{a} and computes then \texttt{pow2} as the least power of two which is greater than \texttt{a}. In each iteration of the second loop, there are two possible computation paths, and both maintain the invariant \texttt{(a+b) == pow2} until termination of the program. To determine a ranking function, we add further variable \texttt{lg2} to count the number of iterations of the second loop.

Since SMT solvers such as Z3 cannot deal with nonlinear functions, we assume the following axioms about the exponential function:

\begin{verbatim}
    (A1) G(exp(2,0)==1)
    (A2a) G(exp(2,lg2+1)==2*exp(2,lg2))
    (A2b) G(exp(2,lg1+1)==2*exp(2,lg1))
    (A3) G(lg1<lg2 -> exp(2,lg1)<exp(2,lg2))
    (A4) G(lg2<lg1 -> ((2*a) % exp(2,lg1)) % exp(2,lg2+1) == (2*a) % exp(2,lg2+1))
\end{verbatim}

\noindent Axiom \texttt{A4} is thereby a key property which could be reduced further since \texttt{lg2<lg1} implies that \texttt{exp(2,lg2+1) * exp(2,lg1-(lg2-1)) == exp(2,lg1)} holds. Since in general \texttt{(a\%(b*c))\%c == a\%c} holds, this implies axiom \texttt{A4}. However, it was not possible to prove this using Z3, so that axiom \texttt{A4} is stated in the above form. Using these axioms, we can prove the following invariants in the given order:
\begin{verbatim}
    (I1) G(1<=pow2)
    (I2) G(p1 -> a>0)
    (I3) G(pow2 == exp(2,lg1))
    (I4) G(start & a==0 -> b==1 & pow2==1 & (a+b) == pow2 & rdy)
    (I5) G(p1 & a<pow2 
            -> 0<b & b<pow2 & 
               0<a & a<pow2 &
               pow2==a+b &
               lg2==0 & 0<lg1)
    (I6) G(p2 -> 0<b & b<=pow2 & a<pow2 & (a+b) == pow2 & (a+b) == pow2)
    (I7) G(p1 & 0<a & a<pow2 | p2 & 0<a -> next(a) == (2*a) % pow2)
    (I8) G(0<a & a<pow2 & (a % exp(2,lg2)) == 0 -> lg2<lg1)
    (I9) G(p1 & 0<a & a<pow2 -> (a % exp(2,lg2)) == 0)
    (I10) G(p2 & 0<a -> (a % exp(2,lg2)) == 0)
\end{verbatim}
The proofs can be simplified by first proving the following equations:
\begin{verbatim}
  G(
    (next(start) <-> false) & 
    (next(p1) <-> (start|p1)&pow2<=a ) & 
    (next(p2) <-> p1&0<a&a<pow2 | p2&0<a ) & 
    (next(a)  == (p1&0<a&a<pow2 | p2&0<a ? (a<b ? a+a : a-b) : a) ) &
    (next(a)  == (p1&0<a&a<pow2 | p2&0<a ? (2*a<pow2 ? 2*a : 2*a-pow2) : a) ) &
    (start&a==0|p1&0<a&a<pow2 -> b==pow2-a & lg2 == 0) & 
    (p1&0<a&a<pow2 | p2&0<a -> next(b)  == (a<b ? b-a : 2*b) & next(lg2)==lg2+1) &
    (next(pow2) == ((start|p1)&pow2<=a ? pow2+pow2 : pow2) ) &
    (next(lg1)  == ((start|p1)&pow2<=a ? lg1+1 : lg1) ) &
    (rdy <-> (start|p2)&a==0 )
   )
\end{verbatim}
Invariants \texttt{(I1-I7)} can be easily proved. Due to \texttt{(I6)}, the sum \texttt{(a+b) == pow2} remains invariant, so that variable \texttt{a} is doubled in each iteration modulo \texttt{pow2}. Hence, if we consider the binary representation of number \texttt{a}, then the bits are shifted to the left losing the bits with weight \texttt{pow2}. Due to \texttt{(I1)}, the second loop can therefore iterate at most \texttt{lg1} many times (if all bits of the binary representation of \texttt{a} would be 1).

Invariant \texttt{(I8)} is seen as follows: If \texttt{lg1<=lg2} would hold, then \texttt{exp(2,lg1) <= exp(2,lg2) == pow1}. Note that we may consider the cases \texttt{lg1>lg2} and \texttt{lg1==lg2} to prove this using axiom \texttt{A3}. Moreover, since \texttt{a<pow2} holds, it would follow \texttt{a \% exp(2,lg2) == a == 0} which contradicts the assumption \texttt{0<a}. 

Invariant \texttt{(I9)} is proved as follows: if \texttt{p1 \& 0<a \& a<pow2} holds, then we have \texttt{lg2==0}, so that by assumption \texttt{(A1)}, we have \texttt{exp(2,lg2)==1}, and therefore, we have \texttt{(a \% exp(2,lg2)) == (a \% 1) == 0}. 

Invariant \texttt{(I10)} is the main invariant and is harder to prove. We prove it by induction where the induction base is trivial, since \texttt{p2} is initially false. For the induction step, we have the following proof goal:
\begin{verbatim}
    0: next(p2) & 0<next(a),
    1: p2 & 0<a -> (a % exp(2,lg2)) == 0
    |-t (next(a) % exp(2,next(lg2))) == 0
\end{verbatim}
We now prove the a couple of lemmata which is easily done with the available invariants so that we obtain the following proof goal:
\begin{verbatim}
  0 : (2*a) % exp(2,lg2+1) == 0
  1 : (2*a) % (2*exp(2,lg2)) == 0
  2 : lg2<lg1
  3 : a<pow2
  4 : next(lg2) == lg2+1
  5 : next(a) == (2*a) % pow2
  6 : (a % exp(2,lg2)) == 0
  7 : p1 & 0<a & a<pow2 | p2 & 0<a
  8 : next(p2) & 0<next(a)
  9 : p2 & 0<a -> (a % exp(2,lg2)) == 0
  |-t (next(a) % exp(2,next(lg2))) == 0
\end{verbatim}
At this point, we use \texttt{MpTac (pp "((2*a) \% exp(2,lg1)) \% exp(2,(lg2+1)) == 0")} to reduce the conclusion essentially to axiom \texttt{A4}.

The overall termination of the program follows now by the proven invariants where we use \texttt{lg1-lg2} as ranking function for the second loop, and \texttt{2*a-pow2} as ranking function for the first loop.

\bibliographystyle{acm}
\begin{thebibliography}{1}
\bibitem{Enge91}
{\sc Engel, A.}
\newblock {\em Problem-Solving Strategies}.
\newblock Problem Books in Mathematics. Springer, 1991.
\end{thebibliography}

\end{document}
