Previous Next Contents

Chapter 7:   Example: a simple parity checker

This chapter consists of a worked example: the specification and verification of a simple sequential parity checker. The intention is to accomplish two things:

  1. To present a complete piece of work with HOL.
  2. To give a flavour of what it is like to use the HOL system for a tricky proof.
Concerning (ii), note that although the theorems proved are, in fact, rather simple, the way they are proved illustrates the kind of intricate `proof engineering' that is typical. The proofs could be done more elegantly, but presenting them that way would defeat the purpose of illustrating various features of HOL. It is hoped that the small example here will give the reader a feel for what it is like to do a big one.

Readers who are not interested in hardware verification should be able to learn something about the HOL system even if they do not wish to penetrate the details of the parity-checking example used here. The specification and verification of a slightly more complex parity checker is set as an exercise (a solution is provided).

7.1   Introduction

This case study is supported by three files in the HOL distribution directory. These files are:

   examples/parity/PARITY.sml
   examples/parity/RESET_REG.sml
   examples/parity/RESET_PARITY.sml

The file PARITY.sml contains the HOL sessions in this chapter; the files RESET_REG.sml and RESET_PARITY.sml contain the solutions to the exercises described in Section 7.5.

The goal of the case study is to illustrate detailed `proof hacking' on a small and fairly simple example.

The sessions of this example comprise the specification and verification of a device that computes the parity of a sequence of bits. More specifically, a detailed verification is given of a device with an input in, an output out and the specification that the nth output on out is T if and only if there have been an even number of T's input on in. A theory named PARITY is constructed; this contains the specification and verification of the device. All the ML input in the boxes below can be found in the file parity/PARITY.sml. It is suggested that the reader interactively input this to get a `hands on' feel for the example.

7.2   Specification

The first step is to start up the HOL system. We will again use hol.unquote and start by loading and opening bossLib. The ML prompt is -, so lines beginning with - are typed by the user and other lines are the system's response.




1 
% hol.unquote
Moscow ML version 1.44 (August 1999)
  ...
[closing file "/local/scratch/mn200/Work/hol98/tools/unquote-init.sml"]
- load "bossLib";
> val it = () : unit
- open bossLib;



To specify the device, a primitive recursive function PARITY is defined so that for n>0, PARITY n f is true if the number of T's in the sequence f(1), ... , f(n) is even.




2 
- val PARITY_def = Define`
    (PARITY 0 f = T) /\
    (PARITY(SUC n)f = if f(SUC n) then ~(PARITY n f) else PARITY n f)`;
Definition stored under "PARITY_def".
> val PARITY_DEF =
    |- (!f. PARITY 0 f = T) /\
       !n f. PARITY (SUC n) f =
             (if f (SUC n) then ~PARITY n f else PARITY n f)
    : thm



The effect of our call to Define is to store the definition of PARITY on the current theory with name PARITY_def and to bind the defining theorem to the ML variable with the same name. Notice that there are two name spaces being written into: the names of constants in theories and the names of variables in ML. The user is generally free to manage these names however he or she wishes (subject to the various lexical requirements), but a common convention is (as here) to give the definition of a constant CON the name CON_DEF in the theory and also in ML. Another commonly-used convention is to use just CON for the theory and ML name of the definition of a constant CON. Unfortunately, the HOL system does not use a uniform convention, but users are recommended to adopt one. In this case Define has made one of the choices for us, but there are other scenarios where have to choose the name used in the theory file.

The specification of the parity checking device can now be given as:

   !t. out t = PARITY t inp
It is intuitively clear that this specification will be satisfied if the signal1 functions inp and out satisfy2:

   out(0) = T
and

   !t. out(t+1)  =  (if inp(t+1) then ~(out t) else out t)
This can be verified formally in HOL by proving the following lemma:

   !in out.
    (out 0 = T) /\ (!t. out(SUC t) = (if inp(SUC t) then ~(out t) else out t))
    ==>
    (!t. out t = PARITY t inp)
The proof of this is done by Mathematical Induction and, although trivial, is a good illustration of how such proofs are done. The lemma is proved interactively using HOL's subgoal package. The proof is started by putting the goal to be proved on a goal stack using the function g which takes a goal as argument.




3 
- g `!inp out.
        (out 0 = T) /\
        (!t. out(SUC t) = (if inp(SUC t) then ~(out t) else out t)) ==>
        (!t. out t = PARITY t inp)`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         !inp out.
           (out 0 = T) /\
           (!t. out (SUC t) = (if inp (SUC t) then ~out t else out t)) ==>
           !t. out t = PARITY t inp



The subgoal package prints out the goal on the top of the goal stack. The top goal is expanded by stripping off the universal quantifier (with GEN_TAC) and then making the two conjuncts of the antecedent of the implication into assumptions of the goal (with STRIP_TAC). The ML function expand takes a tactic and applies it to the top goal; the resulting subgoals are pushed on to the goal stack. The message `OK..' is printed out just before the tactic is applied. The resulting subgoal is then printed.




4 
- expand(REPEAT GEN_TAC THEN STRIP_TAC);
OK..
1 subgoal:
> val it =
    !t. out t = PARITY t inp
    ------------------------------------
      0.  out 0 = T
      1.  !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)



Next induction on t is done using Induct, which does induction on the outermost universally quantified variable.




5 
- expand Induct;
OK..
2 subgoals:
> val it =
    out (SUC t) = PARITY (SUC t) inp
    ------------------------------------
      0.  out 0 = T
      1.  !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)
      2.  out t = PARITY t inp

    out 0 = PARITY 0 inp
    ------------------------------------
      0.  out 0 = T
      1.  !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)



The assumptions of the two subgoals are shown in numbered underneath the horizontal lines of hyphens. The last goal printed is the one on the top of the stack, which is the basis case. This is solved by rewriting with its assumptions and the definition of PARITY.




6 
- expand(ASM_REWRITE_TAC[PARITY_def]);
OK..

Goal proved.
 [.] |- out 0 = PARITY 0 inp

Remaining subgoals:
> val it =
    out (SUC t) = PARITY (SUC t) inp
    ------------------------------------
      0.  out 0 = T
      1.  !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)
      2.  out t = PARITY t inp



The top goal is proved, so the system pops it from the goal stack (and puts the proved theorem on a stack of theorems). The new top goal is the step case of the induction. This goal is also solved by rewriting.




7 
- expand(ASM_REWRITE_TAC[PARITY_DEF]);
OK..

Goal proved.
 [..] |- out (SUC t) = PARITY (SUC t) inp

Goal proved.
 [..] |- !t. out t = PARITY t inp
> val it =
    Initial goal proved.
    |- !inp out.
         (out 0 = T) /\
         (!t. out (SUC t) = (if inp (SUC t) then ~out t else out t)) ==>
         !t. out t = PARITY t inp



The goal is proved, i.e. the empty list of subgoals is produced. The system now applies the justification functions produced by the tactics to the lists of theorems achieving the subgoals (starting with the empty list). These theorems are printed out in the order in which they are generated (note that assumptions of theorems are printed as dots).

The ML function

   top_thm : unit -> thm
returns the theorem just proved (i.e. on the top of the theorem stack) in the current theory, and we bind this to the ML name UNIQUENESS_LEMMA.




8 
- val UNIQUENESS_LEMMA = top_thm();
> val UNIQUENESS_LEMMA =
    |- !inp out.
         (out 0 = T) /\
         (!t. out (SUC t) = (if inp (SUC t) then ~out t else out t)) ==>
         !t. out t = PARITY t inp
    : thm



7.3   Implementation

The lemma just proved suggests that the parity checker can be implemented by holding the parity value in a register and then complementing the contents of the register whenever T is input. To make the implementation more interesting, it will be assumed that registers `power up' storing F. Thus the output at time 0 cannot be taken directly from a register, because the output of the parity checker at time 0 is specified to be T. Another tricky thing to notice is that if t>0, then the output of the parity checker at time t is a function of the input at time t. Thus there must be a combinational path from the input to the output.

The schematic diagram below shows the design of a device that is intended to implement this specification. (The leftmost input to MUX is the selector.) This works by storing the parity of the sequence input so far in the lower of the two registers. Each time T is input at in, this stored value is complemented. Registers are assumed to `power up' in a state in which they are storing F. The second register (connected to ONE) initially outputs F and then outputs T forever. Its role is just to ensure that the device works during the first cycle by connecting the output out to the device ONE via the lower multiplexer. For all subsequent cycles out is connected to l3 and so either carries the stored parity value (if the current input is F) or the complement of this value (if the current input is T).


The devices making up this schematic will be modelled with predicates [4]. For example, the predicate ONE is true of a signal out if for all times t the value of out is T.




9 
- val ONE_def = Define `ONE(out:num->bool) = !t. out t = T`;
Definition stored under "ONE_def".
> val ONE_def = |- !out. ONE out = !t. out t = T : thm



Note that, as discussed above, `ONE_def' is used both as an ML variable and as the name of the definition in the theory. Note also how `:num->bool' has been added to resolve type ambiguities; without this (or some other type information) the typechecker would not be able to infer that t is to have type num.

The binary predicate NOT is true of a pair of signals (inp,out) if the value of out is always the negation of the value of inp. Inverters are thus modelled as having no delay. This is appropriate for a register-transfer level model, but not at a lower level.




10 
- val NOT_def = Define`NOT(inp, out:num->bool) = !t. out t = ~(inp t)`;
Definition stored under "NOT_def".
> val NOT_def = |- !inp out. NOT (inp,out) = !t. out t = ~inp t : Thm.thm



The final combinational device needed is a multiplexer. This is a `hardware conditional'; the input sw selects which of the other two inputs are to be connected to the output out.




11 
- val MUX_def = Define`
    MUX(sw,in1,in2,out:num->bool) =
      !t. out t = if sw t then in1 t else in2 t`;
Definition stored under "MUX_def".
> val MUX_def =
    |- !sw in1 in2 out.
         MUX (sw,in1,in2,out) = !t. out t = (if sw t then in1 t else in2 t)
    : thm



The remaining devices in the schematic are registers. These are unit-delay elements; the values output at time t+1 are the values input at the preceding time t, except at time 0 when the register outputs F.3




12 
- val REG_def =
    Define `REG(inp,out:num->bool) =
              !t. out t = if (t=0) then F else inp(t-1)`;
Definition stored under "REG_def".
> val REG_def =
    |- !inp out. REG (inp,out) = !t. out t =
                 (if t = 0 then F else inp (t - 1))
    : thm



The schematic diagram above can be represented as a predicate by conjoining the relations holding between the various signals and then existentially quantifying the internal lines. This technique is explained elsewhere (e.g. see [3, 4]).




13 
- val PARITY_IMP_def = Define
   `PARITY_IMP(inp,out) =
      ?l1 l2 l3 l4 l5.
        NOT(l2,l1) /\ MUX(inp,l1,l2,l3) /\ REG(out,l2) /\
        ONE l4     /\ REG(l4,l5)        /\ MUX(l5,l3,l4,out)`;
Definition stored under "PARITY_IMP_def".
> val PARITY_IMP_def =
    |- !inp out.
         PARITY_IMP (inp,out) =
         ?l1 l2 l3 l4 l5.
           NOT (l2,l1) /\ MUX (inp,l1,l2,l3) /\ REG (out,l2) /\ ONE l4 /\
           REG (l4,l5) /\ MUX (l5,l3,l4,out)
    : thm



7.4   Verification

The following theorem will eventually be proved: 
   |- !inp out. PARITY_IMP(inp,out) ==> (!t. out t = PARITY t inp)
This states that if inp and out are related as in the schematic diagram (i.e. as in the definition of PARITY_IMP), then the pair of signals (inp,out) satisfies the specification.

First, the following lemma is proved; the correctness of the parity checker follows from this and UNIQUENESS_LEMMA by the transitivity of ==>.




14 
- g `!inp out.
        PARITY_IMP(inp,out) ==>
        (out 0 = T) /\
        !t. out(SUC t) = if inp(SUC t) then ~(out t) else out t`;
> val it =
    Proof manager status: 2 proofs.
    2. Completed: ...
    1. Incomplete:
         Initial goal:
         !inp out.
           PARITY_IMP (inp,out) ==>
           (out 0 = T) /\
           !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)



The first step in proving this goal is to rewrite with definitions followed by a decomposition of the resulting goal using STRIP_TAC. The rewriting tactic PURE_REWRITE_TAC is used; this does no built-in simplifications, only the ones explicitly given in the list of theorems supplied as an argument. One of the built-in simplifications used by REWRITE_TAC is |- (x = T) = x. PURE_REWRITE_TAC is used to prevent rewriting with this being done.


15 
- expand(PURE_REWRITE_TAC
           [PARITY_IMP_def, ONE_def, NOT_def, MUX_def, REG_def] THEN
         REPEAT STRIP_TAC);
OK..
2 subgoals:
> val it =
    out (SUC t) = (if inp (SUC t) then ~out t else out t)
    ------------------------------------
      0.  !t. l1 t = ~l2 t
      1.  !t. l3 t = (if inp t then l1 t else l2 t)
      2.  !t. l2 t = (if t = 0 then F else out (t - 1))
      3.  !t. l4 t = T
      4.  !t. l5 t = (if t = 0 then F else l4 (t - 1))
      5.  !t. out t = (if l5 t then l3 t else l4 t)

    out 0 = T
    ------------------------------------
      0.  !t. l1 t = ~l2 t
      1.  !t. l3 t = (if inp t then l1 t else l2 t)
      2.  !t. l2 t = (if t = 0 then F else out (t - 1))
      3.  !t. l4 t = T
      4.  !t. l5 t = (if t = 0 then F else l4 (t - 1))
      5.  !t. out t = (if l5 t then l3 t else l4 t)



The top goal is the one printed last; its conclusion is out 0 = T and its assumptions are equations relating the values on the lines in the circuit. The natural next step would be to expand the top goal by rewriting with the assumptions. However, if this were done the system would go into an infinite loop because the equations for out, l2 and l3 are mutually recursive. Instead we use the first-order reasoner PROVE_TAC to do the work:




16 
- expand(PROVE_TAC []);
OK..
Meson search level: .....

Goal proved.
 [......] |- out 0 = T

Remaining subgoals:
> val it =
    out (SUC t) = (if inp (SUC t) then ~out t else out t)
    ------------------------------------
      0.  !t. l1 t = ~l2 t
      1.  !t. l3 t = (if inp t then l1 t else l2 t)
      2.  !t. l2 t = (if t = 0 then F else out (t - 1))
      3.  !t. l4 t = T
      4.  !t. l5 t = (if t = 0 then F else l4 (t - 1))
      5.  !t. out t = (if l5 t then l3 t else l4 t)

The first of the two subgoals is proved. Inspecting the remaining goal it can be seen that it will be solved if its left hand side, out(SUC t), is expanded using the assumption:

   !t. out t = if l5 t then l3 t else l4 t
However, if this assumption is used for rewriting, then all the subterms of the form out t will also be expanded. To prevent this, we really want to rewrite with a formula that is specifically about out (SUC t). We want to somehow pull the assumption that we do have out of the list and rewrite with a specialised version of it. We can do just this using PAT_ASSUM. This tactic is of type term -> thm -> tactic. It selects an assumption that is of the form given by its term argument, and passes it to the second argument, a function which expects a theorem and returns a tactic. Here it is in action:




17 
- e (PAT_ASSUM ``!t. out t = X t``
       (fn th => REWRITE_TAC [SPEC ``SUC t`` th]))
<<HOL message: inventing new type variable names: 'a, 'b.>>
OK..
1 subgoal:
> val it =
    (if l5 (SUC t) then l3 (SUC t) else l4 (SUC t)) =
    (if inp (SUC t) then ~out t else out t)
    ------------------------------------
      0.  !t. l1 t = ~l2 t
      1.  !t. l3 t = (if inp t then l1 t else l2 t)
      2.  !t. l2 t = (if t = 0 then F else out (t - 1))
      3.  !t. l4 t = T
      4.  !t. l5 t = (if t = 0 then F else l4 (t - 1))

The pattern used here exploited something called higher order matching. The actual assumption that was taken off the assumption stack did not have a RHS that looked like the application of a function (X in the pattern) to the t parameter, but the RHS could nonetheless be seen as equal to the application of some function to the t parameter. In fact, the value that matched X was ``\x. if l5 x then l3 x else l4 x``.

Inspecting the goal above, it can be seen that the next step is to unwind the equations for the remaining lines of the circuit. We do this using the arith_ss simpset that comes with bossLib to help with the arithmetic embodied by the subtractions and SUC terms.




18 
- e (RW_TAC arith_ss []);
OK..

Goal proved.
 [.....]
|- (if l5 (SUC t) then l3 (SUC t) else l4 (SUC t)) =
   (if inp (SUC t) then ~out t else out t)

Goal proved.
 [......] |- out (SUC t) = (if inp (SUC t) then ~out t else out t)
> val it =
    Initial goal proved.
    |- !inp out.
         PARITY_IMP (inp,out) ==>
         (out 0 = T) /\
         !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)



The theorem just proved is named PARITY_LEMMA and saved in the current theory.




19 
- val PARITY_LEMMA = top_thm ();
> val PARITY_LEMMA =
    |- !inp out.
         PARITY_IMP (inp,out) ==>
         (out 0 = T) /\
         !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)



PARITY_LEMMA could have been proved in one step with a single compound tactic. Our initial goal can be expanded with a single tactic corresponding to the sequence of tactics that were used interactively:




20 
- restart()
> ...
- e (PURE_REWRITE_TAC [PARITY_IMP_def, ONE_def, NOT_def,
                       MUX_def, REG_def] THEN
     REPEAT STRIP_TAC THENL [
       PROVE_TAC [],
       PAT_ASSUM ``!t. out t = X t``
                 (fn th => REWRITE_TAC [SPEC ``SUC t`` th]) THEN
       RW_TAC arith_ss []
     ]);
<<HOL message: inventing new type variable names: 'a, 'b.>>
OK..
Meson search level: .....
> val it =
    Initial goal proved.
    |- !inp out.
         PARITY_IMP (inp,out) ==>
         (out 0 = T) /\
         !t. out (SUC t) = (if inp (SUC t) then ~out t else out t)



Armed with PARITY_LEMMA, the final theorem is easily proved. This will be done in one step using the ML function prove.




21 
- val PARITY_CORRECT = prove(
    ``!inp out. PARITY_IMP(inp,out) ==> (!t. out t = PARITY t inp)``,
    REPEAT STRIP_TAC THEN MATCH_MP_TAC UNIQUENESS_LEMMA THEN
    MATCH_MP_TAC PARITY_LEMMA THEN ASM_REWRITE_TAC []);
> val PARITY_CORRECT =
    |- !inp out. PARITY_IMP (inp,out) ==> !t. out t = PARITY t inp



This completes the proof of the parity checking device.

7.5   Exercises

Two exercises are given in this section: Exercise 1 is straightforward, but Exercise 2 is quite tricky and might take a beginner several days to solve. The solutions to these exercises should be in the files:

   hol/examples/parity/RESET_REG.sml
   hol/examples/parity/RESET_PARITY.sml

7.5.1   Exercise 1

Using only the devices ONE, NOT, MUX and REG defined in Section 7.3, design and verify a register RESET_REG with an input in, reset line reset, output out and behaviour specified as follows. This is formalized in HOL by the definition:

   RESET_REG(reset,inp,out) =
    (!t. reset t ==> (out t = T)) /\
    (!t. out(t+1) = ((reset t  \/ reset(t+1)) => T | inp t))
Note that this specification is only partial; it doesn't specify the output at time 0 in the case that there is no reset.

The solution to the exercise should be a definition of a predicate RESET_REG_IMP as an existential quantification of a conjunction of applications of ONE, NOT, MUX and REG to suitable line names,4 together with a proof of:

   RESET_REG_IMP(reset,inp,out) ==> RESET_REG(reset,inp,out)

7.5.2   Exercise 2

  1. Formally specify a resetable parity checker that has two boolean inputs reset and inp, and one boolean output out with the following behaviour:
    The value at out is T if and only if there have been an even number of Ts input at inp since the last time that T was input at reset.
  2. Design an implementation of this specification built using only the devices ONE, NOT, MUX and REG defined in Section 7.3.
  3. Verify the correctness of your implementation in HOL.
1
Signals are modelled as functions from numbers, representing times, to booleans.
2
We'd like to use in as one of our variable names, but this is a reserved word for let-expressions.
3
Time 0 represents when the device is switched on.
4
i.e. a definition of the same form as that of PARITY_IMP in section 7.3
Previous Next Contents