\newchapter{Further reading}

\renewcommand{\CURPATH}{reading}

\leveldown{}

\begin{itemize}
\item Julien Vanegue, Sean Heelan, Rolf Rolles -- SMT Solvers for Software Security
\footnote{\url{https://yurichev.com/mirrors/SMT/woot12.pdf}}

\item Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh -- Handbook of Satisfiability (2009). The second edition came out in 2021.

\item Rui Reis -- Practical Symbolic Execution and SATisfiability Module Theories (SMT) 101
\footnote{\url{http://deniable.org/reversing/symbolic-execution}}.

\item Daniel Kroening and Ofer Strichman -- Decision Procedures -- An Algorithmic Point of View
\footnote{\url{http://www.decision-procedures.org}}.

\end{itemize}

\input{\CURPATH/Z3}
\input{\CURPATH/SAT}
\input{\CURPATH/SMT}
\input{\CURPATH/etc}

\myheading{Henry Warren -- Hacker's Delight}

Some people say these branchless tricks and hacks were only relevant for old RISC CPUs, so you don't need to read it.
Nevertheless, these hacks and understanding them helps immensely to get into boolean algebra and all the mathematics.

Also, such hacks got their second life to be used in cryptography.
Many important primitives should be executed in constant time, to prevent side-channel attacks.

\begin{lstlisting}[style=customc,caption=A piece of code from OpenSSH 7.x]
/*
 * increment counter 'ctr',
 * the counter is of size 'len' bytes and stored in network-byte-order.
 * (LSB at ctr[len-1], MSB at ctr[0])
 */
static inline void
aesctr_inc(u8 *ctr, u32 len)
{
        ssize_t i;

#ifndef CONSTANT_TIME_INCREMENT
        for (i = len - 1; i >= 0; i--)
                if (++ctr[i])   /* continue on overflow */
                        return;
#else
        u8 x, add = 1;

        for (i = len - 1; i >= 0; i--) {
                ctr[i] += add;
                /* constant time for: x = ctr[i] ? 1 : 0 */
                x = ctr[i];
                x = (x | (x >> 4)) & 0xf;
                x = (x | (x >> 2)) & 0x3;
                x = (x | (x >> 1)) & 0x1;
                add *= (x^1);
        }
#endif
}
\end{lstlisting}

\levelup{}