\documentclass{beamer}
\usetheme[style=plain]{uu}

%% unicode support, for text and code :)
\usepackage[utf8x]{inputenc}
\usepackage{ucs}
\usepackage{autofe}

\usepackage{mathtools}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{color}


%% Haskell syntax highlighting and code font
\usepackage{minted}
\usepackage{fancyvrb}
\usemintedstyle{default}
\newminted{coq}{gobble=8,xleftmargin=20pt,mathescape,fontfamily=tt,fontsize=\footnotesize}



%% Metainformation
%% PDF stuff
\usepackage{datetime}
\usepackage{ifpdf}
\ifpdf
\pdfinfo{
    /Author (J.P.PizaniFlor)
    /Title (Coquet: A Coq library for verifying hardware)
    /Keywords (Hardware verification, Dependently-typed programming, Coq, Proof assistant)
    /CreationDate (D:\pdfdate)
}
\fi

\title[Coquet]{Coquet: A Coq library for verifying hardware}

\date{June 13th, 2013}

\author[Pizani Flor]
{
    João Paulo Pizani Flor
}

\institute[Utrecht University]
{
    Department of Information and Computing Sciences,
    Utrecht University
}

\subject{Dependently-typed programming, Hardware verification}




\begin{document}

%% Code excerpts
\defverbatim[colored]\coqSampleInterface{
    \begin{coqcode}
        example : Circuit n m
    \end{coqcode}
}

\defverbatim[colored]\coqNBitAdder{
    \begin{coqcode}
        nBitAdd : Circuit (U :+: sumn U n :+: sumn U n)
                          (sumn U n :+: U)
    \end{coqcode}
}

\defverbatim[colored]\coqPlugDuplicateType{
    \begin{coqcode}
        dup : Circuit U (U :+: U)
    \end{coqcode}
}

\defverbatim[colored]\coqTaggedUnits{
    \begin{coqcode}
        Inductive tag (t : string) : Type := _tag : tag t
    \end{coqcode}
}

\defverbatim[colored]\coqTaggedAdder{
    \begin{coqcode}
        halfAdder : Circuit (_tag "in1" :+: _tag "in2")
                            (_tag "sum" :+: _tag "cout")
    \end{coqcode}
}

\defverbatim[colored]\coqFinTypeclass{
    \begin{coqcode}
        Class Fin A := {
            eq_fin : eqT A;
            enum   : list A;
            axiom  : forall (x : A), count (equal x) enum = 1 
        }.
    \end{coqcode}
}

\defverbatim[colored]\coqCircuit{
    \begin{coqcode}
        Context {tech : Techno}
        Inductive Circuit : Type -> Type -> Type :=
        | Atom : forall {n m : Type} {Fn : Fin n} {Fm : Fin m},
            techno n m -> Circuit n m
        | Plug : forall {n m : Type} {Fn : Fin n} {Fm : Fin m},
            (f : m -> n) -> Circuit n m
        | Ser : forall {n m p : Type},
            Circuit n m -> Circuit m p -> Circuit n p
        | Par : forall {n m p q : Type},
            Circuit n p -> Circuit m q -> Circuit (n :+: m) (p :+: q)
        | Loop : forall {n m p : Type},
            Circuit (n :+: p) (m :+: p) -> Circuit n m
    \end{coqcode}
}

\defverbatim[colored]\coqTechno{
    \begin{coqcode}
        Class Techno := techno : Type -> Type -> Type.
    \end{coqcode}
}

\defverbatim[colored]\coqPlugConstructor{
    \begin{coqcode}
        Inductive Circuit : Type -> Type -> Type :=
        | Plug : forall {n m : Type} {Fn : Fin n} {Fm : Fin m},
            (f : m -> n) -> Circuit n m
    \end{coqcode}
}

\defverbatim[colored]\coqPlugDuplicate{
    \begin{coqcode}
        Plug (fun x => match x with
                       | inl e => e
                       | inr e => e
                       end).
    \end{coqcode}
}

\defverbatim[colored]\coqTechnologySpec{
    \begin{coqcode}
        Class Technology_spec (tech : Techno) T :=
            spec : forall {a b : Type},
            tech a b -> (a -> T) -> (b -> T) -> Prop
    \end{coqcode}
}

\defverbatim[colored]\coqRealiseImplement{
    \begin{coqcode}
        Context {n m N M : Type}
                (Rn : Iso (n -> T) N) (Rm : Iso (m -> T) M)
        Class Realise (c : Circuit n m) (R : N -> M -> Prop) :=
            realise : forall ins outs,
                Meaning c ins outs -> R (iso ins) (iso outs)
        Class Implement (c : Circuit n m) (f : N -> M) :=
            implement : forall ins outs,
                Meaning c ins outs -> iso outs = f (iso ins)
    \end{coqcode}
}

\defverbatim[colored]\coqHalfAdderDef{
    \begin{coqcode}
        Context a b s c : string (* section variables *)

        Definition HADD :
            Circuit (_tag a :+: _tag b) (_tag s :+: _tag c) :=
            Fork2 (_tag a :+: _tag b) |> (XOR a b s & AND a b c).
    \end{coqcode}
}

\defverbatim[colored]\coqhadd{
    \begin{coqcode}
        Definition hadd : (bool, bool) -> (bool, bool) := fun x =>
            match x with
            | (a, b) => (a xor b, a /\ b)
            end.
    \end{coqcode}
}

\defverbatim[colored]\coqHADDhaddInstance{
    \begin{coqcode}
        Instance HADD_Spec : Implement
            (* iso on inputs *)
            (* iso on outputs *)
            HADD hadd.
        Proof.
            ...
    \end{coqcode}
}


%% The document itself
    \begin{frame}
        \titlepage
    \end{frame}

    \begin{frame}
        \frametitle{Table of Contents}
        \tableofcontents
    \end{frame}


    \section{Intro}
    \label{sec:intro}
        \frame{\sectionpage}

        \subsection{What is it}
        \label{subsec:what}
            \begin{frame}
                \frametitle{What is Coquet}
                A Coq \emph{library} for hardware specification and verification.
                \pause

                \begin{description}
                    \item[Library] Datatypes, typeclasses, instances, combinators, proofs, etc.
                    \item[Deep-embedded] \emph{Circuit} datatype, structurally defined.
                    \item[Dependently-typed] The \emph{circuit} AST is fully-typed.
                    \item[Provably correct] Circuits can be proven to \emph{realize} a specification.
                \end{description}
            \end{frame}

        \subsection{Why is it useful}
        \label{subsec:why}
            \begin{frame}
                \frametitle{Why is Coquet useful}

                \begin{itemize}
                    \item Coq is more expressive than other theorem provers (HOL, ACL2, etc.).
                    \item Dependent types help catch common errors soon in the design process.
                    \item Deep-embedding brings interesting possibilities:
                    \begin{itemize}
                        \item Functions that transform circuits (can be proven correct).
                        \item Simulating \emph{and synthesizing} circuits (netlists).
                    \end{itemize}
                \end{itemize}
            \end{frame}


    \section{Technical overview}
    \label{sec:overview}
        \frame{\sectionpage}

        \begin{frame}
            \frametitle{Circuit interface}

            \begin{itemize}
                \item The \emph{interface} of a circuit is the set of its input and output ports.
                \item Modeled in Coquet as \emph{parameters} of the circuit datatype.
                    \coqSampleInterface

                \pause

                \item The parameters n and m can be of any \emph{finite} type 
                \begin{itemize}
                    \item More details on these finite types later\ldots
                    \item For example, disjoint sums of ``units'':
                        \coqNBitAdder
                \end{itemize}
            \end{itemize}
        \end{frame}

        \begin{frame}
            \frametitle{Defining circuits with combinators}
            Circuits are modeled \emph{hierarchically} with combinators, closely mimicking the
            ``pen-and-paper'' approach.

            \pause

            Circuits are built using:
            \begin{itemize}
                \item Any of a set of \emph{fundamental} components, user-defined.
                \item Serial composition.
                \item Parallel composition.
                \item Re-arranging and re-ordering of ports, done by \emph{plugs}.
                \item Loop combinator, to create feedback loops.
            \end{itemize}

            Again, more details soon\ldots
        \end{frame}

        \begin{frame}
            \frametitle{Re-arranging wires with plugs}
            As the combinators connect the circuits in a ``nameless'' fashion, we need
            rewiring circuits, called \emph{plugs}

            \begin{itemize}
                \item The type of a plug that duplicates its input COULD be:
                    \coqPlugDuplicateType
                \item To \emph{construct} a plug, we need a function mapping
                    \emph{outputs} to \emph{inputs}. More details later.
            \end{itemize}
        \end{frame}

        \begin{frame}
            \frametitle{Circuit semantics}
            Until now, we have only dealt with the \emph{syntax} (the structure) of circuits.

            \begin{itemize}
                \item The meaning or \emph{semantics} of a circuit (\texttt{x : C n m}) is
                    defined as a relation between its inputs and outputs, where:
                \begin{itemize}
                    \item \emph{inputs} is a function of type $(n \rightarrow \mathbb{T})$.
                    \item \emph{outputs} has type $(m \rightarrow \mathbb{T})$.
                    \item $\mathbb{T}$ is the type of what is carried in the wires.
                \end{itemize}

                \item The relation is defined \emph{inductively} on x, and denoted as follows:
                    $ x \vdash^{n}_{m} \text{ins} \bowtie \text{outs} $.
            \end{itemize}
        \end{frame}


    \section{Diving into Coquet}
    \label{sec:in-depth}
        \frame{\sectionpage}

        \subsection{Interfaces}
        \label{subsec:interfaces}
            \begin{frame}
                \frametitle{Tagged unit types}
                Remember that Coquet uses arbitrary \emph{finite} types for the inputs and outputs
                of a circuit.

                \begin{itemize}
                    \item One way to build a finite type is by summing some \emph{units}.
                    \item This is inconvenient and confusing at \emph{least}.
                    \begin{itemize}
                        \item To allow easily discernible input/outputs, Coquet uses \emph{tags}:
                            \coqTaggedUnits
                        \item For example: \coqTaggedAdder
                    \end{itemize}
                    \item Also, this is not the only way to have finite types\ldots
                \end{itemize}
            \end{frame}

            \begin{frame}
                \frametitle{The Finite typeclass}
                In general, any type with an instance for the \texttt{Fin} typeclass can be used
                as input or output in circuits.

                \begin{itemize}
                    \item A typeclass in Coq has approx. the same meaning as in Haskell.
                        \begin{itemize}
                            \item Predicate/relation over/among type(s).
                            \item Instances are named and passed.
                            \item May contain (of course) proofs of properties over types.
                        \end{itemize}

                    \item The \texttt{Fin} typeclass looks like this:
                        \coqFinTypeclass

                    \item Instances for unit, tagged unit, sum, etc.
                \end{itemize}
            \end{frame}

        \subsection{Circuit type}
        \label{subsec:circuit-type}
            \begin{frame}
                \frametitle{The Circuit datatype}

                \begin{itemize}
                    \item The (dependent) type of circuits looks like:
                        \coqCircuit

                    \item Parameterized by the type of fundamental gates:
                        \coqTechno
                \end{itemize}
            \end{frame}

            \begin{frame}
                \frametitle{Plugs, plugs, plugs\ldots}
                As seen, a Plug requires a function from \texttt{m} to \texttt{n}.
                \coqPlugConstructor

                \begin{itemize}
                    \item Let's examine again the circuit which duplicates its input:
                        \coqPlugDuplicate

                    \item In simple enough cases (like this one), proof-search suffices.
                \end{itemize}
            \end{frame}

        \subsection{Semantics}
        \label{subsec:semantics}
            \begin{frame}
                \frametitle{Meaning relation over circuits}
                As already said: The semantics of a circuit is given by a relation between its
                inputs and outputs, defined inductively.

                \begin{itemize}
                    \item The base case involves defining instances of the \texttt{Techno} class for
                        a given set of basic gates:
                        \coqTechnologySpec

                    \item The meaning relation is generated using this parameter and other rules
                        (one for each constructor of \texttt{Circuit}).
                \end{itemize}
            \end{frame}

            \begin{frame}
                \frametitle{Realizing a spec, implementing a function}

                \begin{itemize}
                    \item The meaning relation is not a specification for a circuit.
                        \begin{itemize}
                            \item It is a strict and detailed definition of behaviour.
                            \item \emph{Too} detailed, in fact\ldots
                        \end{itemize}
                    \item Coquet relies on 2 typeclasses to let the user \emph{specify} a circuit:
                        \coqRealiseImplement

                    \item Proving the spec is done by providing instances of these classes (proof
                        objects).
                \end{itemize}

            \end{frame}


    \section{Applied example}
    \label{sec:usage-example}
        \frame{\sectionpage}

        \begin{frame}
            \frametitle{Case studies defined in the paper}

            \begin{itemize}
                \item Half-adder
                \item Full 1-bit adder
                \item Ripple-carry n-bit adder
                \item Divide-and-conquer n-bit adder
                \item Sequential circuits (memory elements)
            \end{itemize}

            \vspace{1cm}

            Here we'll only take a peek at a half-adder\ldots
        \end{frame}

        \subsection{A half-adder}
        \label{subsec:half-adder}
            \begin{frame}
                \frametitle{Definition of a half-adder circuit}

                (Nice diagram on the whiteboard\ldots)

                \vspace{1cm}

                \coqHalfAdderDef
            \end{frame}

            \begin{frame}
                \frametitle{Proving a half-adder circuit}
                \begin{itemize}
                    \item We must prove that \texttt{HADD} implements the function:
                        \coqhadd

                    \item Our claim that \texttt{HADD} implements \texttt{hadd} is written as:
                        \coqHADDhaddInstance

                    \item Then we need to prove it (goal on whiteboard\ldots).
                \end{itemize}
            \end{frame}


    \section{Conclusions}
    \label{sec:conclusions}
        \frame{\sectionpage}

        \begin{frame}
            \frametitle{Comparison with related works}

            \begin{itemize}
                \item Circuits were already modeled in the HOL theorem prover, but using a shallow
                    embedding.
                \pause
                \item In Coq, also only a shallow embedding had already been attempted.
                \pause
                \item In Haskell, there was Lava, in which verification is reduced to finite-sized
                    instances of circuits.
                    \begin{itemize}
                        \item In contrast, in Coq we prove the correctness of parametric circuits,
                            for any size of inputs.
                    \end{itemize}
            \end{itemize}
        \end{frame}

        \begin{frame}
            \frametitle{Final words}

            \begin{itemize}
                \item ``Programming'' hardware in functional languages has lots of advantages, and
                    using dependently-typed languages has even more.
                \pause
                \item Proving the correctness of hardware is an awesome idea.
                    \begin{itemize}
                        \item Even better if you can synthesize it to an FPGA or even ASIC.
                    \end{itemize}
                \pause
                \item There is still some polishing to be done:
                    \begin{itemize}
                        \item Couldn't make the lib compile in Coq 8.4.
                        \item There seems to be a synthesis facility, but I'm not sure\ldots
                        \item Have a ``standard library'' of basic circuits.
                    \end{itemize}
            \end{itemize}
        \end{frame}

        \begin{frame}[plain]
            \begin{center}
                \Huge Questions?
            \end{center}
        \end{frame}

\end{document}
