A HOL Semantics for a Subset of ELLA

Richard J. Boulton

University of Cambridge Computer Laboratory New Museums Site, Pembroke Street Cambridge CB2 3QG, ENGLAND

April 1992

Abstract

Formal verification is an important tool in the design of computer systems, especially when the systems are safety or security critical. However, the formal techniques currently available are not well integrated into the set of tools more traditionally used by designers. This work is aimed at improving the integration by providing a formal semantics for a subset of the hardware description language ELLA^{1}, and by supporting this semantics in the HOL theorem proving system, which has been used extensively for hardware verification.

A semantics for a subset of ELLA is described, and an outline of a proof of the equivalence of parallel and recursive implementations of an n-bit adder is given as an illustration of the semantics. The proof has been performed in an extension of the HOL system. Some proof tools written to support the verification are also described.

1ELLA is a registered trademark of the Secretary of State for Defence, UK.

1 Introduction

Formal verification is an important tool in the design of computer systems, especially when the systems are safety or security critical. However, the formal techniques currently available are not well integrated into the set of tools more traditionally used by designers. This work is aimed at improving the integration by providing a formal semantics for a subset of the hardware description language ELLA, and by supporting this semantics in the HOL theorem proving system [Gor87], which has been used extensively for hardware verification. ELLA was developed at the Royal Signals and Radar Establishment (RSRE) [MPT86] and is currently marketed by Computer General Electronic Design [Com89a]. The semantics of the ELLA subset is given in the higher-order classical logic supported by the HOL system.

The emphasis of the work has been on supporting a subset of ELLA large enough for real industrial designs and integrating this with the methodologies normally used for hardware verification in the HOL system. The work described here is only the first step towards this aim, but the aim itself has influenced many of the design decisions. In particular, the formality of the semantics has to a limited extent been sacrificed in order to cover a substantial subset of the language in a mechanisable way, and to fit in with the methodology of the HOL system. In effect ELLA is being used as a macro language for describing designs in the HOL system. However, care has been taken to accurately reflect the behaviour of the commercially available ELLA simulator and compiler.

The layout of this paper is as follows: Section 2 describes the semantics for the ELLA subset. As an illustration, Section 3 outlines a proof of the equivalence of parallel and recursive implementations of an n-bit adder. The proof has been performed in an extension of the HOL system. The ELLA definitions of the two adder implementations are automatically translated by the system, and the resulting logical terms are shown to be equivalent under certain justified assumptions. Section 4 describes some proof tools written to support the verification of designs described in ELLA and translated into logical terms by the system. Section 5 discusses related work, and in Section 6, significant issues are discussed and conclusions are drawn.

The reader is assumed to have a reasonable familiarity with both ELLA and HOL. The paper describing the project in which this work was done [BGHT90] gives a brief description of both ELLA and the HOL system. Consultation of that earlier paper is recommended before proceeding to read this paper. Some of the material in it is reproduced here so that this paper forms a self-contained and detailed description of the semantics for the ELLA subset.

2 HOL Semantics for a Subset of ELLA

The ELLA language is mostly functional in style and takes a fairly high-level view of hardware, though designs can be described at a variety of levels of abstraction. There are some imperative features to the language. However, imperative features require some notion of state within the semantics, whereas for a purely functional subset it is possible to give a semantics in terms of types and functions within higher order logic. The language is strongly typed and features the ability to declare new datatypes.

ELLA designs are built up from components which are declared as functions or macros (essentially parameterised functions). These can be implicitly connected together by function application. Constructs are also present which allow the designer to make connections between components explicitly.

This section describes a HOL semantics for a subset of ELLA (see Appendix A for the syntax of the subset, and compare it with the syntax for full ELLA given in the reference manual [Com89a]). For each ELLA construct in the subset, the corresponding logical term is given. The notation [[…]] is used to denote the meaning (or translation) of an ELLA text, where the ‘…’ represents the ELLA text in question. The meaning is a higher order logic term. HOL terms are enclosed in double quotation marks. A few of the subsections in this description are marked as ‘tentative semantics’. The semantics given to the constructs in these subsections has not been tested and is thought to be unsatisfactory, particularly with respect to undefinedness, which is described shortly.

The semantics is in a denotational style using HOL functions. The aim has been to produce a context-independent translation from ELLA text to HOL terms. This has the advantage that no global state is required in the system to support the translation. If it was necessary to retain information about ELLA identifiers (functions, types, constants, etc.) that is not captured in the HOL terms, the HOL system would need to be extended, either by an extension to the theory files or with support for auxiliary files to store the additional information. Retaining a contextindependent translation has imposed restrictions on the form of the semantics, but the benefits appear to outweigh the costs.

Various environments (associating the names of variables and constants to type information and the like) are used during the translation process, but none of this information has to be retained once the HOL definition corresponding to the ELLA declaration has been made. Following the definition, all necessary information is captured within the HOL theory file, without requiring modifications to the theory mechanism.

The static semantics^{2} of the ELLA subset has not been formalised in the logic. However, the translation procedure (written in ML [GMM^{+}78]) enforces restrictions on the form of the ELLA texts either directly or by making use of the built-in typechecking when HOL terms are constructed. This type-checker is part of the basic HOL system.

2Not all syntactically correct language texts are well-formed. For example, in a strongly-typed language, a text may violate type constraints. Type and other compile-time restrictions are referred to as the static semantics of the language.

The dynamic semantics^{3} is formalised within the logic. For most of the ELLA constructs in the subset the behaviour is captured by semantic constants. These correspond approximately to the non-terminals in the syntax of ELLA, so the translation process is straightforward. The ELLA texts are not transformed into simpler or alternative forms by the translator. Any such transformations are done by symbolic manipulation within the logic. This makes the transformations secure. A further advantage of the semantic constants is that they allow a HOL term representing an ELLA text to be printed as that ELLA text. This provides an added degree of assurance that the translation process is correct.

Most of the dynamic properties of the ELLA subset are captured within the definitions of the semantic constants. However, it has not been possible within the other constraints (such as having no extra-logical information) to capture all the meaning in a general way within the definitions. The remaining meaning is captured by less general logical expressions generated by the translator. For example, the translator may construct different terms according to the types involved. Structured types modelled by HOL tuples are a common source of this feature. It is difficult to define semantic constants that work for all types and capture all the meaning when the types may involve tuples. This is due to the nature of the type system of the higher order logic supported by the HOL system. The disadvantage of having the translator generating different expressions (terms) for different types is that it is doing more work. The code becomes more complex which increases the possibility of an error in the code. It is particularly important to avoid such errors when a system may be used for formal verification of safety or security-critical systems.

2.1 The Subset

The subset of ELLA considered is restricted to the declarative features of the language. In particular the imperative constructs called sequences are not included. ELLA characters, strings, function types^{4} and function-sets are not included in the subset. The form of DELAYs is restricted. Only pure unit delay is allowed. Attribute hooks and diagnostic statements are omitted since they have no useful semantics in the chosen framework. However, the translation program does not give an error when it encounters these constructs. Instead, it issues a warning and proceeds with the translation ignoring the constructs.

In addition to the omissions described above, there are many smaller restrictions imposed by the subset.

3The dynamic semantics of a programming language specifies the behaviour of language constructs at run-time. For a hardware description language it specifies the behaviour of the system described by a language text, which should also be the behaviour exhibited by the simulator for the language.

4ELLA function types have little in common with the function types of higher order logic.

2.2 The ELLA Unspecified Value

ELLA features an unspecified value denoted by ?. This value may be generated by arithmetic operations producing a result out of range, by CASE statements with choosers (selectors) which are not exhaustive, or it may even be generated explicitly in the ELLA text (source code). In each case ? represents one of the values of the appropriate type, but it is not known which.

An unknown value of some type can readily be represented in higher order logic either as a partial specification, or by use of Hilbert’s ε-operator. However, there is one place in the semantics of ELLA where ? behaves not as an unknown value of the type, but as an additional value of the type. Use of partial specification or Hilbert’s ε-operator cannot represent such an additional value. There was, therefore, a choice between making a small modification to the semantics of ELLA or adding an extra value to every HOL type used to represent an ELLA type. The latter was chosen, partly to find out whether the extra complexity introduced would inhibit the verification process. However, as discussed shortly, there are pragmatic difficulties to overcome if the semantics does not accurately represent the behaviour of the ELLA compiler.

An example of the feature of ELLA which considers ? to be an additional value is as follows. Suppose an ELLA type bit has been defined:

  TYPE bit = NEW (hi | lo).

This specifies bit to be an enumerated type with two elements, hi and lo. According to the reference manual [Com89a] the ELLA constant:

                                  hi | lo

should match hi or lo, but not the unspecified value. However, the constant:

                                    bit

should match any value of type bit, i.e., hi or lo or the unspecified value. Unless an extra element is added to the representation of the type bit, these two constants cannot be distinguished in the HOL semantics, when clearly they have different interpretations as far as the ELLA compiler/simulator is concerned.

Rather than adding an extra element to every HOL type representing an ELLA type, the more uniform approach of lifting has been taken. A value of type bit in ELLA is represented by a value of type (bit)lifted in HOL. A value of type (bit)lifted is either an application of the type constructor LIFT to some value of HOL type bit, or it is the value UU, representing the unspecified value of ELLA type bit. Only one constant is used to represent the unspecified value for all types, and lifting can be made use of for ordinary HOL types as well as for the HOL types being used to represent ELLA types. In particular, lifted Booleans are required for the semantics of the ELLA CASE statement.

In addition to LIFT and UU, the theory of lifting has other constants. The two most important of these are UNLIFT and LIFT_apply1. UNLIFT converts a value of type (*)lifted (where * can be any type) to a value of type *, but only if its argument is of the form LIFT(x) for some term x. The term UNLIFT(UU) cannot be simplified. This can be seen from the definition of UNLIFT below, in which the result of applying UNLIFT is only specified when the argument is of the form LIFT(x).

  ⊢ ∀(x:*). UNLIFT (LIFT x) = x

UNLIFT is a partially-specified total function. It has a result for all possible argument values, but when the argument is UU nothing can be proved about the value of the result, i.e., the result is some value of the appropriate type but there is no way of knowing which value.

Note that in higher order logic a function application such as LIFT(x) is often written as (LIFTx). The turnstile ‘⊢’ denotes the fact that the equation is a theorem (in this case a constant definition).

The HOL constant LIFT_apply1 is used to ‘lift’ a function. Its type is given by:

  LIFT_apply1 : (*→**) → ((*)lifted → (**)lifted)

where * and ** are type variables, and the definition of LIFT_apply1 is:

  ⊢ ∀(f:*→**) xl.
     LIFT_apply1 f xl = ((xl = UU) ⇒ UU | (LIFT (f (UNLIFT xl))))

It can be seen that the first argument, f, is a function not involving lifted values. Applying LIFT_apply1 to such an argument yields a new function which returns UU when given UU as argument, or else it applies f ‘under’ the lifting.

The corresponding function for binary operations has type:

  LIFT_apply2 : (*→**→***) → (*)lifted → (**)lifted → (***)lifted

and is defined by:

  ⊢ ∀(f:*→**→***) xl yl.
     LIFT_apply2 f xl yl =
        (((xl = UU) ∨ (yl = UU)) ⇒ UU | (LIFT (f (UNLIFT xl) (UNLIFT yl))))

UNLIFT_LIFT_apply1 is a slight variation of LIFT_apply1 which allows the function being lifted to itself return a lifted value:

  ⊢ ∀(f:*→(**)lifted) xl.
     UNLIFT_LIFT_apply1 f xl = ((xl = UU) ⇒ UU | (f (UNLIFT xl)))

The alternative of having a semantics that does not conform to the behaviour of the ELLA compiler is now discussed. The circumstances in which there is a discrepancy in behaviour are likely to be rare. The discrepancy will only manifest itself if a constant is used that enumerates all the possible values that can be taken on by the type. To the ELLA compiler, such a constant does not match the unspecified value, but in a formal semantics without lifting (or an equivalent), the constant would match the unspecified value. Such a difference could affect the validity of a formal verification. It is conceivable that under a semantics without lifting, the device could be shown to meet its specification, while the actual hardware produced from the ELLA text did not. Such a possibility cannot be ignored, for to do so would undermine the original motivation for performing a formal verification.

So, the user must at least be warned that a construct has been used for which the semantics of the ELLA compiler may differ from the one used by the verification system. It is not sensible to warn the user about every constant, for then any significant warning would be drowned in a mass of unnecessary warnings. So the more specific cases that can cause the problem must be detected. At first sight this may seem to be a relatively straightforward requirement. In the example above it is only necessary to check for a constant that enumerates both hi and lo. However, when the constants concerned are of structured types, or the elements of the type are constructed from values of other types, the situation is not so simple.

Testing for coverage of all possible values may be possible but it would in general appear to be a computationally intensive task. In practice though, the program would only be looking for evidence that the constant is not an exhaustive enumeration. The question remains as to whether every constant in the text can be checked in a reasonable amount of time. Until this question is answered, or an alternative approach is found, the use of a semantics without lifting will in certain respects be unsatisfactory.

2.3 Declarations

For each ELLA declaration a corresponding HOL definition is produced. In the case of type declarations, a new HOL type is defined, together with appropriate constants. The other kinds of declaration only introduce new HOL constants. This is illustrated in the following sections.

The ELLA language allows declarations to be made locally, for example within series. Local constant and type declarations are not possible in HOL, so taking the approach of translating an ELLA declaration to a HOL definition, local declarations have to be prohibited. An alternative approach would be to model local constant declarations in ELLA by local variable declarations in HOL, but there is no analogous way of having local type declarations. Another alternative would be to have global declarations in HOL for local ELLA declarations. By choosing appropriate identifier names, it might be possible to provide a satisfactory model. However, such a system was considered to be too untidy and prone to inconsistencies.

2.4 Types

ELLA allows new types to be defined for signal values. In fact the basic language has no predefined types as such. Integers, characters and character strings are present but cannot be used directly as signal values. There are however some language features that behave a lot like type constructs. For example, ELLA structures and rows can be modelled with HOL tuples and lists respectively.

The use of lists to represent ELLA rows is somewhat unsatisfactory since lists of different lengths can be of the same type in HOL, but in ELLA, rows have a specific length. An alternative is to model rows using HOL tuples. This would correctly represent the fixed-length property of rows, but the logical constants for the ELLA constructs cannot be defined generically; tuples of different sizes cannot be represented by the simple polymorphism of HOL. Dependent types are really required to represent ELLA rows. The type needs to be parameterised by an integer specifying its length. Unfortunately the logic of the HOL system does not feature dependent types, though the possibility of simulating them is currently under investigation.

Functions could also be used instead of lists to represent rows. The functions would be mappings from a component position (a number) to the value of that component of the row. This still does not capture the fixed-size property of ELLA rows. Lists were chosen because they are suggested by the syntax of the ELLA row constructs. Currently, no checks are made on the sizes of ELLA rows during the translation and very few restrictions are imposed by the semantic functions on the lengths of the corresponding lists.

A new ELLA type can be either an enumerated type or an abbreviation for an existing type. Enumerated types are formed by explicit enumeration of the elements, by defining integer ranges, or by defining character ranges. Henceforth only the first form will be referred to as ‘an enumerated type’. The second form will be called ‘integer sub-range types’ and the last form is not included in the subset.

2.4.1 Simple Enumerated Types

New enumerated types are dealt with using the HOL type definition package [Mel89]. This produces a new HOL type corresponding to the ELLA type. The theorem produced by the type package justifies the existence of the new type. Additional theorems are also produced which express useful properties of the type. For example, the ELLA type declaration:

  TYPE bit = NEW (hi | lo).

is passed to the HOL system’s type definition package. The result is the introduction of a new HOL type bit and a theorem which characterises the new type. In the example above, the theorem is:

  ⊢ ∀e0 e1. ∃! fn. (fn hi = e0) ∧ (fn lo = e1)

(The notation ‘∃!fn.’ means ‘there exists a unique function fn such that …’). The system then proves four useful properties of the new type: a structural induction property, injectivity of the constructors (i.e., they are one-to-one), distinctness of the elements (constructors), and a case-analysis property. For the above type these are respectively:

  ⊢ ∀P. P hi ∧ P lo ⟹ (∀b. P b)
  ⊢ T
  ⊢ ¬(hi = lo)
  ⊢ ∀b. (b = hi) ∨ (b = lo)

In this example the second theorem just states that true (T) is true. None of the constructors are functions, so there is nothing that can be said about the injectivity of them. For more complex types the corresponding theorem is not vacuous. If there is only one constructor in the new type, the theorem stating that the constructors (elements) are distinct is also vacuous.

The system also generates a theorem for each constructor. Each of these theorems defines an abbreviation for the lift of the constructor. In the case when the constructor is just an element (as for all the constructors in the example) the definition is trivial:

  ⊢ LIFT_hi = LIFT hi
  ⊢ LIFT_lo = LIFT lo

An ELLA type name is represented by a HOL type (name)lifted. The typeoperator lifted yields a type with one more element than the type it takes as argument. The extra element is used to represent the ELLA unspecified value. In the example above, a value of type (bit)lifted is either an application of the function LIFT to some value of type bit (i.e., either hi or lo), or it is the value UU. UU represents the unspecified value.

2.4.2 Structured Enumerated Types

As an example of how type constructors that take arguments are translated, consider the declaration:

  TYPE tests = NEW (notest | test & ([8](bit,bit),[8](bit,bit,bit))).

where bit is a previously defined type. notest does not take an argument but test does. The definition of LIFT_test below uses functions for pulling LIFT through tuples and lists. This is required because structured units are represented by structures of lifted basic values rather than as lifted structures. The definition of LIFT_test is:

  ⊢ ∀x. LIFT_test x =
         LIFT_apply1 test
          (LIFT_thru_pair_after
            (LIFT_thru_list_after (LIFT_thru_pair_after (I,I)),
             LIFT_thru_list_after
              (LIFT_thru_pair_after (I,LIFT_thru_pair_after (I,I)))) x)

The identity function, I, is used to eliminate the need to deal with special cases in the translator.

If the CASE statement is to work, tuples must be tuples of lifted values, not lifted tuples. For consistency and to retain as much information as possible, the same applies to lists. In fact, only values of user-defined (primitive) types are lifted; compound types are represented as structures of lifted primitive types.

2.4.3 Integer Sub-range Types

A type defined as an integer sub-range is represented by a new HOL type whose elements are in one-to-one correspondence with the specified subset of the integers. A function for mapping integers to the new type is also defined. For example, consider the following ELLA type declaration:

  TYPE octal = NEW oct/(0..7).

The theorem characterising the new type is:

  ⊢ ∃rep.
     TYPE_DEFINITION
     (NEW_INT_TYPE
      #00000000000000000000000000000000
      #00000000000000000000000000000111)
     rep

where NEW_INT_TYPE is a constant defined as follows:

  ⊢ ∀low high.
     NEW_INT_TYPE low high =
     (λi. (Int_of_word32 low) Leq (Int_of_word32 i) ∧
          (Int_of_word32 i) Leq (Int_of_word32 high))

NEW_INT_TYPE converts its arguments from 32-bit words to integers and returns a predicate that tests the argument i to see if it is in the range specified by low and high (Leq is the less-than-or-equal-to relation). NEW_INT_TYPE is used to characterise the subset of 32-bit words to be used for the new type.

There are several other theorems generated, the most interesting of which is the definition of a function oct for mapping integers to lifted values of the new type. This function corresponds to the entity of the same name given in the ELLA type declaration.

  ⊢ ∀i'. oct i' = LIFT(ABS_octal i')

ABS_octal is a constant defined by one of the other theorems. The name i' is used for the variable rather than i to ensure that it doesn’t clash with any identifier in the ELLA text. ELLA names cannot contain single quotation marks.

The integer expressions used to define a new integer sub-range type must (in the subset) be numeric constants (i.e., not expressions). Not even −1 can be used since this is considered to be an application of the minus operator. However −1 can be used as a value by writing it as 2r1...1 (twos complement binary). The restrictions are necessary to allow an existence theorem to be proved for the type. They are more severe than really necessary, for simplicity.

2.4.4 Type Abbreviations

It has not been practical to allow the type abbreviation form of ELLA type declarations. HOL has a type abbreviation facility, but lifting prevents it from being used. To define a new type bitpair:

  TYPE bitpair = (bit,bit).

the HOL type abbreviation:

  bitpair = bit # bit

could be used, but when the type bitpair is actually used in an ELLA text, the equivalent HOL type is (bitpair)lifted. HOL expands this to:

                            (bit # bit) lifted

Recall that due to other restrictions in the semantics, types are lifted at the lowest level of a structured type, so the following type is expected:

                         (bit)lifted # (bit)lifted

It is possible to get around this problem by expanding the abbreviation prior to lifting (to a large extent this happens automatically), but there would still be a problem in that the size of row types is not captured in the corresponding HOL lists used by the semantics, and so the abbreviation does not possess this information either. For most purposes this does not matter, but when generating undefined values of row types, the size is required. A satisfactory solution to this problem has not been found, and so type abbreviations have been omitted from the subset. This is not a great loss since it does not reduce the expressive power of the language; it merely reduces the legibility of the ELLA text.

2.5 Integers

ELLA integers are 32-bit twos-complement numbers. They are represented in HOL by (lifted) 32-bit words. The arithmetic operators are modelled by converting the word to an integer (in the mathematical sense), applying an appropriate integer operator, then converting back to a word. If the integer result is out of the word range, the result is undefined (UU). Other operators are modelled by bitwise operations on the 32-bit words.

2.5.1 Integer and Boolean Operators

HOL constants have been defined for the ELLA integer and Boolean operators. To avoid naming conflicts with built-in HOL constants, the ELLA name is translated using Table 1. Observe that if the ELLA name is alphanumeric it is simply prefixed with the letter ‘E’.

ELLA operator HOL operator
+ (unary)  EPOS
- (unary)  ENEG

INOT          EINOT
ABS           EABS
SQRT          ESQRT
NOT           ENOT

+ (binary)  EPLUS
- (binary)  EMINUS

*             EMULT
% or IDIV      EIDIV
MOD           EMOD
SL            ESL
SR            ESR
IAND          EIAND
IOR           EIOR
=             EEQ
/=            ENEQ
>             EGT
<             ELT
>=            EGE
<=            ELE
AND           EAND
OR            EOR

Table 1: Translation of operator names

At the time of writing the operators ESQRT and EIDIV have not been defined since the square-root operation and integer division are not present in the general theory of integers used to support the ELLA semantics.

Here, as an example, is the definition of one of the integer operators:

  ⊢ ∀il1 il2.
     EPLUS il1 il2 =
     UNLIFT_LIFT_apply2
     (λi1 i2. LIFT_word32_of_int ((Int_of_word32 i1) plus (Int_of_word32 i2)))
     il1
     il2

LIFT_word32_of_int checks that the result of the integer operation is within the range of ELLA integers. If it is, the value is made into an ELLA integer and lifted. If not, the result is undefined, as it is also if either of the arguments is undefined. This is achieved by UNLIFT_LIFT_apply2 (see page 6 for descriptions of similar constants).

2.5.2 Integer-Valued Conditionals

The ELLA conditional construct for integers is translated as follows:

[[IF boolean THEN int_{1} ELSE int_{2} FI]] = "IF [[boolean]] [[int_{1}]] [[int_{2}]]"

where [[boolean]], [[int_{1}]] and [[int_{2}]] are the translations of boolean, int_{1} and int_{2} respectively. The constant defined here is polymorphic, but the only place it can be used in the subset is for integers:

  ⊢ (∀b (x:(*)lifted) y. IF (LIFT b) x y = (b ⇒ x | y)) ∧
    (∀(x:(*)lifted) y. IF UU x y = UU)

(b ⇒ x | y) evaluates to the value of x if b is true, or to y if b is false.

2.6 Constants

ELLA constants need not simply be individual constants. They can also be a set of constants. Their use in the CASE statement suggests that they are intended to behave more like patterns. A suitable representation for an ELLA constant in HOL is therefore a new HOL constant that is a predicate. The predicate is true for any constant in the set, and for no other. It is also possible to have an ELLA constant which matches any object of a type. This can be represented by a predicate which always returns true.

Constants have two functions in ELLA. They are primarily used as choosers in the CASE statement. In this capacity, they behave as patterns. For example, the constant:

                                  hi | lo

matches a value if it is either hi or lo. The other use for constants is as initial values for devices which have state. In this capacity, ELLA constants are constants in the conventional sense.

The syntax of ELLA has a single syntactic category for constants, but only certain parts of it make sense as choosers. An overlapping, but different subset of the syntax of constants makes sense as initial values. Since constants can be bound to an identifier by a constant declaration, and the identifier used elsewhere in the ELLA text, it is not possible to determine at translation time whether the constant will be used as a chooser or as an initial value. So, constants are translated in the same way wherever they appear. They are modelled as predicates. This fits in with their use as choosers. For use as initial values, Hilbert’s ε-operator [Gor87] is applied to the predicate. This returns a value satisfying the predicate, so when the predicate specifies a unique value (as is required for initial values), the application returns that unique value. In any other case, it is not possible to eliminate the ε-operator to yield a specific value, and so proofs depending on the identity of the constant will be inhibited.

2.6.1 Chooser Values

Chooser values in ELLA CASE statements yield either match (represented by LIFT T), nomatch (represented by LIFT F) or ? (UU). These values have to be combined to obtain results for compound choosers. For tuples (e.g., (hi,lo)), the basic chooser values are combined using an AND operation. For ‘sets’ of choosers (e.g., (hi | lo)) an OR operation is used. The following two functions implement the ‘truth’ tables in the ELLA Language Reference Manual [Com89a]. The ‘truth’ tables are given in Table 2 and Table 3.

  ⊢ ∀b1 b2.
     Chooser_AND b1 b2 =
     (((b1 = LIFT F) ∨ (b2 = LIFT F)) ⇒
      LIFT F |
      LIFT_apply2 $∧ b1 b2)

  ⊢ ∀b1 b2.
     Chooser_OR b1 b2 =
     (((b1 = LIFT T) ∨ (b2 = LIFT T)) ⇒
      LIFT T |
      LIFT_apply2 $∨ b1 b2)

where the dollar sign ($) enables an infix operator to be used as an argument to another function.

The two lemmas below confirm the logical nature of the operations when both chooser values are fully determined. Observe that here lifting is being used on Boolean values of higher order logic to express the semantics of matching in choosers. The values are not representing an ELLA type, but are internal to the semantics.

x  y  x AND y
match  match  match
match  nomatch nomatch
match  ?         ?
nomatch match  nomatch
nomatch nomatch nomatch
nomatch ?  nomatch
? match ?
?  nomatch nomatch

?         ?         ?

Table 2: AND operation on chooser values

x  y  x OR y
match  match  match
match  nomatch match
match ? match
nomatch match  match
nomatch nomatch nomatch
nomatch ?         ?
? match match
?  nomatch ?

?         ?         ?

Table 3: OR operation on chooser values

  ⊢ ∀x y. Chooser_AND (LIFT x) (LIFT y) = LIFT (x ∧ y)

  ⊢ ∀x y. Chooser_OR (LIFT x) (LIFT y) = LIFT (x ∨ y)

2.6.2 Simple Constants

The simplest form of ELLA constant is a single constant of some defined type. This is represented by a predicate which is true if and only if its argument is the constant value in question. For example, the representation of the ELLA constant hi in higher order logic is given by:

  [[hi]] = "CONST hi"

So, the translation for an ELLA constant consisting of the name of a fixed value of an enumerated type is in general:

[[name]] = "CONST name"

The HOL constant CONST (a semantic constant) is defined by:

  ⊢ ∀(c:*). CONST c = LIFT_apply1 (λx. x = c)

The notation (c:*) labels the argument of the function CONST as c and specifies its type to be * (a polymorphic type). The result of applying CONST is a lifted predicate. Lifting is explained and justified in Section 2.2.

2.6.3 Sets of Constants

The translation of a set of constants is given by:

[[const1_{1} | ... | const1_{n}]] = "CONST_SET [[[const1_{1}]]; ... ;[[const1_{n}]]]"

where CONST_SET is defined by:

  ⊢ (∀(x:*). CONST_SET [] x = LIFT F) ∧
    (∀f l x. CONST_SET (CONS f l) x = (f x) Chooser_OR (CONST_SET l x))

This HOL constant recursively applies the chooser ‘OR’ operation (used here as an infix operator) between elements of the set of ELLA constants. [] denotes an empty HOL list. CONS is the list constructor function. The result of applying CONST_SET to a list of constants is a predicate that is ‘true’ if the argument x matches any of the constants in the list.

2.6.4 Replicated Constants (tentative semantics)

A ‘row’ consisting of a constant replicated int times is translated by:

[[[int]const1]] = "CONST_ROW [[int]] [[const1]]"

  ⊢ ∀int (const:*→(bool)lifted).
     CONST_ROW int const =
     (λrow.
       (LENGTH row = UNLIFT (LIFT_num_of_word32 (UNLIFT int))) ⇒
       (ITLIST $Chooser_AND (MAP const row) (LIFT T)) |
       (εx. T))

Since rows in ELLA (which are of fixed length) are represented by lists in HOL (which are of variable length), part of the ELLA type-constraint has to be made explicitly in HOL. In most parts of the semantics, checks are not made explicitly that rows are of the correct length. The test will be made implicitly when two rows are equated. However, here there is no such equation.

If the integer expression int is undefined or not a natural number the evaluation of the application of CONST_ROW cannot proceed. This is achieved by the applications of UNLIFT. If int is a known natural number but not equal to the size of row, the conditional expression evaluates to the irreducible term (εx. T). In this way all proofs will be blocked unless the length of row can be shown to be equal to int.

Provided row is of the correct size, the representation yields true if const is true of every element of row. Chooser_AND is used to combine the results rather than logical AND. (MAP const row) produces a list of the results of applying const to each element of the row. ITLIST then combines the results to give a lifted Boolean value. ITLIST is used to avoid making an ad hoc auxiliary recursive definition. Its definition is:

  ⊢ (∀f x. ITLIST f [] x = x) ∧
    (∀f h t x. ITLIST f (CONS h t) x = f h (ITLIST f t x))

2.6.5 Type Names as Constants

An ELLA constant consisting of a type name matches any value of the type including the undefined value:

  [[type name]] = "MATCH_ALL : (type name)lifted → (bool)lifted"

Such a constant is modelled by a predicate that always returns true:

  ⊢ ∀(xl:(*)lifted). MATCH_ALL xl = LIFT T

2.6.6 Constants of an Integer Sub-Range Type (tentative semantics)

[[name/formula2]] = "CONST_INT name [[formula2]]"

  ⊢ ∀(constr:word32→(*)lifted) int.
     CONST_INT constr int =
     LIFT_apply2 $= (UNLIFT_LIFT_apply1 constr int)

If int is undefined, or application of constr yields an undefined value, then the result of applying the constant will be undefined. This will also be the case if the value being tested against the constant is undefined. Ignoring undefinedness, an informal specification of the behaviour is:

  CONST_INT constr int = (λx. x = constr int)

2.6.7 Associated Values (tentative semantics)

[[name & const2]] = "CONST_ASSOC_VAL LIFT_name [[const2]]"

const2 is an ELLA constant and is therefore modelled by a predicate. The HOL term "CONST_ASSOC_VAL LIFT_name [[const2]]" is also a predicate. It yields true of a value x if there is a value y such that x = name & y and for which [[const2]] yields true. The type of y is not (*)lifted because lifting may not be at the top level of the type it is instantiated to.

  ⊢ ∀(constr:*→(**)lifted) arg.
     CONST_ASSOC_VAL constr arg =
     LIFT_apply1 (λx. ∃y. (LIFT x = constr y) ∧ UNLIFT (arg y))

UNLIFT is used here because the body of the existential quantification must be Boolean-valued. The use of UNLIFT is unsatisfactory.

2.6.8 Tuples of Constants

[[(const_{1}, ... ,const_{n})]] =

  "λ(x1', ... ,xn'). CONST_MULTIPLE [([[const_{1}]] x1'); ... ;([[const_{n}]] xn')]"

  ⊢ (CONST_MULTIPLE [] = LIFT T) ∧
    (∀x l. CONST_MULTIPLE (CONS x l) = x Chooser_AND (CONST_MULTIPLE l))

The infix Chooser_AND combines the results of matching the separate components of the tuple.

2.6.9 Undefined Values as Constants (tentative semantics)

Undefined constants cannot be used as choosers. They are used as initial values for devices with state. They are represented by a predicate which yields ‘true’ if and only if its argument is the unspecified value. By applying Hilbert’s epsilon operator to such a predicate, the unspecified value itself is obtained.

For generating undefined values for a basic type, the following translation is used:

  [[? type]] = "UNDEFINED_CONST : (type)lifted → (bool)lifted"

  ⊢ ∀(xl:(*)lifted). UNDEFINED_CONST xl = LIFT (xl = UU)

If the type is structured (i.e., it contains tuples) or has rows (lists), the representation is a recursive construction using CONST_MULTIPLE and CONST_ROW. For example, the ELLA constant:

  ? ([3]bit,bit)

where bit is a basic type, is represented by:

  λ(x1',x2').
   CONST_MULTIPLE
   [CONST_ROW [[3]] UNDEFINED_CONST x1';UNDEFINED_CONST x2']

2.6.10 Sets of Integers (tentative semantics)

The semantics of an ELLA constant specifying a set of integers is given by:

[[name/(int_{1}..int_{2})]] = "CONST_INT_SET name [[int_{1}]] [[int_{2}]]"

  ⊢ ∀(constr:word32→(*)lifted) int1 int2.
     CONST_INT_SET constr int1 int2 =
     (λxl. LIFT (∃y. (xl = constr y) ∧
                     UNLIFT (int1 ELE (LIFT y)) ∧
                     UNLIFT ((LIFT y) ELE int2)))

The representation is a predicate which yields true of an argument xl if there is some integer y in the range int_{1} … int_{2} such that xl = name(y). The integer operator ELE is exploited in the definition of CONST_INT_SET. The treatment of the unspecified value is not satisfactory.

2.7 Functions

Each ELLA function declaration becomes a definition in the HOL system. Ideally the definitions would be of the form:

  FUN(u_{1},. . .,u_{n}) = . . .

where each u_{i} is a unit, and units are functions from time to some type. This is a problem when the function is applied because it is expecting a tuple of signals as its argument, but the unit it is applied to will be a tuple-valued signal, i.e., a function from time to some tuple type.

There are a number of possible solutions:

1. Represent units by tuples of signals,

2. Make FUN take a tuple-valued signal as its argument,

3. Push the time down through the tuple before applying FUN.

It is not possible to solve the problem by making the inputs to FUN time-independent because that would prohibit functions involving some notion of state. See the following section for an example of such a function. Solution (1) gives rise to a semantics for units that is too complicated. Solution (2) merges the inputs into one so that they can no longer be accessed directly within the body of the function, but access to them as separate inputs is required, so they would have to be regenerated within the body of the function. This is basically the same as option (3).

So approach (3) has been used. Specifically, a type-casting function is applied prior to the application of a function to a unit. The type-casting function has the following form:

  λx'. ε(f1',...,fn'). ∀t'. ((f1' t'),...,(fn' t')) = (x' t')

Informally, its behaviour is to take a tuple-valued signal x' and return the tuple of signals (f1',...,fn') such that for all times t' the tuple composed of the values of these signals at t' is equal to the value of the tuple-valued signal at t'.

There are no checks during translation to make sure that the name of an input does not appear more than once in the type declaration part of a function or macro declaration. Such repetition could allow an input to be given more than one type. This could result in a HOL definition for an invalid ELLA declaration. The repeated name could be interpreted by HOL as two separate identifiers (since the types are distinct).

2.7.1 Delays

There are four kinds of delay in ELLA (see the reference manual [Com89a]):

• Pure delay: DELAY (x,1)

• Almost pure delay: DELAY (x,n)

• Ambiguity delay: DELAY (z,n,x,m)

• Inertial delay: IDELAY (x,n)

Only pure delay is included in the subset. The subset requires that the integer argument for the length of the delay be 1, so this argument is redundant. It has been left in the syntax so that a helpful error message can be given instead of a parsing error.

The ELLA delay primitive is represented by a function DELAY1 which maps a signal to a delayed signal. The definition below models pure unit transport delay. If delays of more than one unit of time were allowed this would need to be redefined since the actual delay primitive of ELLA maps changes shorter than the delay period to a given ‘undefined’ value. However, for unit delays this notion is equivalent to pure transport delay. The initial value is assumed to be a predicate, true only for the value required. The select operator (Hilbert’s epsilon operator, ε) is used to obtain the value from the predicate.

The semantics of the ELLA DELAY construct is given by:

  [[DELAY(const, 1)]] = "DELAY1 [[const]]"

where DELAY1 is defined by:

  ⊢ ∀(c:*→(bool)lifted) in (t:time)
     DELAY1 c in t = ((t=0) ⇒ (εv. (c v) = (LIFT T)) | in(t-1))

The initial value const is an ELLA constant, i.e., a lifted predicate (see Section 2.6). Provided the predicate is true for exactly one value, the use of Hilbert’s ε-operator yields that value. This value is used as the output of the delay at time 0. For all later times, the output is the input at the previous time. Time is represented by natural numbers.

The following lemmas are generally more useful than the definition of DELAY1:

  ⊢ ∀c. DELAY1 (CONST c) = (λin t. ((t = 0) ⇒ LIFT c | in(t - 1)))

  ⊢ DELAY1 UNDEFINED_CONST = (λin t. ((t = 0) ⇒ UU | in(t - 1)))

2.7.2 Arithmetic Operations

The ARITH statement is used to perform arithmetic on units. The syntax of ELLA includes integer expressions. However, integer operations cannot be used directly on units, even when they are of an integer or enumerated type. The ARITH statement is provided to allow the integer operations to be applied to units. The ARITH statement must form the entire body of the function declaration, where the units given as arguments are signals. These signals have a value for every time step. At each time the ARITH statement takes the values of the function’s arguments and casts them into integers (provided they are of an appropriate type for doing this). It then evaluates the integer expression and casts the result into the output type.

For integer sub-range types the interpretation of the units as integers is obvious. For enumerated types the ordering of the elements in the type definition is used. The latter case is not included in the subset.

As an example, the function declaration:

  FN MATHS = (numtype1: i, numtype2: j) -> numtype3: ARITH int.

causes the following theorem to be generated:

  ⊢ ∀(i:time→(numtype1)lifted) (j:time→(numtype2)lifted).
     MATHS (i,j) =
     ARITH
     (REP_numtype3,ABS_numtype3)
     (λt'. let i = LIFT_apply1 REP_numtype1 (i t')
           and j = LIFT_apply1 REP_numtype2 (j t')

in [[int]])

The let construct is used to cast the function’s arguments (units) into ELLA integers. In the example, the same variable names are used for both the units and the integers so that the names don’t have to be changed in [[int]]. In practice, restrictions in the definitional mechanism of the HOL system cause the variables for the integers to have to be renamed. Any occurrences of i and j within [[int]] are bound by the let construct, so they do not directly correspond to the arguments of the function.

ARITH is defined by:

  ⊢ ∀(repf:*→word32) absf rsig (t:time).
     ARITH (repf,absf) rsig t =
     UNLIFT_LIFT_apply1
     (λr. (repf (absf r) = r) ⇒ LIFT (absf r) | UU)
     (rsig t)

where repf and absf are functions for converting between the type of the unit and ELLA integers, and between ELLA integers and the type of the unit.

The requirement that (repf (absf r) = r) in the definition of ARITH ensures that the result of the arithmetic evaluation (rsig t) is within the range of the output type. Note also that if the result of the evaluation is undefined, the result of the entire ARITH statement will be undefined. The use of LIFT_apply1 in the translation also propagates undefined values.

2.8 Units

ELLA units are represented in HOL by signal-valued expressions. A signal is a function from time to some value. Times are represented as natural numbers. A HOL type abbreviation is used:

  new_type_abbrev (`time`,":num");;

2.8.1 Time-Independent Units

The syntax of ELLA allows a fixed value to be used instead of a signal in certain places. Such occurrences are represented by an application of the HOL semantic constant SIGNAL to the fixed value. SIGNAL is defined by:

  ⊢ ∀(v:*) (t:time). SIGNAL v t = v

For a constant value of some enumerated type the translation is:

  [[name]] = "SIGNAL LIFT_name"

See Section 2.4 for a description of LIFT_name.

2.8.2 Infix Function Applications

Infix applications of ELLA functions (or macros):

[[unit fnname unit1]] = "[[fnname]] ([[unit]],[[unit1]])"

2.8.3 Prefix Function Applications

Prefix applications of ELLA functions (or macros):

[[fnname unit1]] =

  "INVOKE (λx'. ε(f1',...,fn'). ∀t'. ((f1' t'),...,(fn' t')) = (x' t'))

[[fnname]] [[unit1]]"

  ⊢ ∀(g:(time→*)→**) (f:**→time→***) x t. INVOKE g f x t = f (g x) t

INVOKE is simply used to apply a type-casting function to the unit so that it matches up with the type of the function (see Section 2.7).

2.8.4 Concatenating Rows

Row concatenation (if unit and unit1 are both rows):

[[unit CONC unit1]] = "[[unit]] CONC [[unit1]]"

⊢ ∀(l1:time→(*)list) l2 t. CONC l1 l2 t = APPEND (l1 t) (l2 t)

Row concatenation (if only unit1 is a row):

[[unit CONC unit1]] = "(λt'. [[[unit]] t']) CONC [[unit1]]"

Row concatenation (if only unit is a row):

[[unit CONC unit1]] = "[[unit]] CONC (λt'. [[[unit1]] t'])"

ELLA does not allow CONC to be used on two units neither of which are rows. Also, the types must be consistent. In the semantics, the type system of HOL enforces this.

2.8.5 Simple Replication

[[[int]unit1]] = "SIMP_REP [[int]] [[unit1]]"

⊢ ∀int (unit:time→*) t.
SIMP_REP int unit t =
REPLICATE (UNLIFT (LIFT_num_of_word32 (UNLIFT int))) (unit t)

SIMP_REP uses the function REPLICATE to make a list (representing an ELLA row) consisting of int copies of unit. The ELLA integer int has to be converted to a natural number before it can be used as an argument to REPLICATE.

2.8.6 Variable Replication

[[[INT name = int_{1}..int_{2}]unit1]] = "VAR_REP [[int_{1}]] [[int_{2}]] (λname. [[unit1]])"

⊢ ∀int1 int2 (f:(word32)lifted→(time→*)) t.
VAR_REP int1 int2 f t =
MAP
(λn. f (LIFT_word32_of_num n) t)
((UNLIFT (LIFT_num_of_word32 (UNLIFT int1))) UPTO
 (UNLIFT (LIFT_num_of_word32 (UNLIFT int2))))

VAR_REP uses UPTO to construct a list of natural numbers ranging from int1 to int2. The function (λname. [[unit1]]) is then applied to each number in the list to give a list of units (an ELLA row). Note that if the integer range involves negative integers the logical term produced will be irreducible. The function UPTO is defined such that (m UPTO n) evaluates to the list:

[m;m + 1;…;n − 1;n]

If n is less than m the result is an empty list. The alternative is to have an undefined result in this case, but that would not provide the behaviour required for the ELLA semantics.

2.8.7 Associated Values

Generating associated values:

[[name & unit1]] = "ASSOC_VAL LIFT_name [[unit1]]"

LIFT_name must have been defined by an ELLA type declaration (see Section 2.4.2). ASSOC_VAL is defined by:

  ⊢ ∀(constr:*→(**)lifted) arg (t:time).
     ASSOC_VAL constr arg t = constr (arg t)

Recovering associated values:

  [[unit2 // name]] = "RECOVER_ASSOC_VAL [[unit2]] LIFT_name"

  ⊢ ∀arg (constr:*→(**)lifted) (t:time).
     RECOVER_ASSOC_VAL arg constr t = (εx. constr x = arg t)

The right-hand side of the defining equation for RECOVER_ASSOC_VAL means “an x such that application of the constructor to x yields the value of the unit arg at the current time”. arg is instantiated to the denotation of unit2. If this is of the correct form for a value to be recovered from it using name (the constructor), then the x will be unique, because constructors are one-to-one. However, if the wrong constructor name is being used to extract the associated value, there will be no x satisfying:

                             constr x = arg t

Hence, the epsilon term in the definition of RECOVER_ASSOC_VAL will denote an arbitrary value of the appropriate type, i.e., the result of the extraction will be unspecified in HOL.

The representations given here for associated values have not yet been used in a significant example. The following property should hold under the semantics, but as yet this has not been verified:

[[(name & unit1) // name]] = [[unit1]]

For structured types the proof of this property is likely to be non-trivial. It would be useful to have an automatic tool that could prove the property for any type. The use of lifting might prevent the property from holding unless values are restricted to those that are defined.

2.8.8 Undefined Values

For generating undefined values for a basic type, the following translation is used:

  [[? type]] = "UNDEFINED : time → (type)lifted"

  ⊢ ∀(t:time). UNDEFINED t = (UU:(*)lifted)

If the type is structured (i.e., it contains tuples) or has rows (lists), the representation is a recursive construction using MULTIPLE (defined in Section 2.8.12) and SIMP_REP. For example, the ELLA unit:

  ? ([3]bit,bit)

where bit is a basic type, is represented by:

  "MULTIPLE(λt'. (SIMP_REP [[3]] UNDEFINED t',UNDEFINED t'))"

2.8.9 Integer-Valued Units

[[name/formula2]] = "INT name [[formula2]]"

  ⊢ (∀(constr:word32→(*)lifted) (t:time). INT constr UU t = UU) ∧
    (∀constr int t. INT constr (LIFT int) t = constr int)

The value of this unit does not change with time, hence t does not appear on the right-hand sides of the equations defining INT. The definition could have been given

using UNLIFT_LIFT_apply1.

2.8.10 Accessing Components of Structures

The subset imposes restrictions on the indexing of ELLA units, which has the syntax:

unit2[int]

If the unit2 is a tuple, then the int used to index it must be a numeric constant and must have a value in the appropriate range, e.g., for a triple the index must be 1, 2 or 3. Similar restrictions apply to subsetting:

unit2[int..int]

Dynamic indexing of tuples is not permitted. That is the syntax

unit2[[unit]]

is not permitted if the unit2 is a tuple.

The semantics of indexing when unit2 is a row:

[[unit2[int]]] = "INDEX [[unit2]] [[int]]"

  ⊢ ∀(unit:time→(*)list) int t.
     INDEX unit int t =
     EL' (UNLIFT (LIFT_num_of_word32 (UNLIFT int))) (unit t)

For the term representing the semantics to be reducible, [[int]] must have a value in the range 1 … m where m is the size of the row. The HOL constant EL' takes a natural number, n, and a list as arguments. The result is the n^{th} element of the list. The built-in HOL constant EL was not used because it is defined so that (EL 0) rather than (EL 1) is the head (first element) of the list. This was considered to be confusing in the context of the ELLA semantics.

Indexing when unit2 is a tuple:

  [[unit2[int]]] = "INDEX_MULT [[unit2]] (λ(x1',...,xn'). xi')"

where n is the ‘size’ of the tuple and i is the value of int. This must be a numeric constant and in the range 1 … n for the translation to succeed.

  ⊢ ∀(unit:time→*) (f:*→**) t. INDEX_MULT unit f t = f (unit t)

Dynamic indexing:

[[unit2[[unit]]]] = "DYNAMIC_INDEX [[unit2]] REP_type name [[unit]]"

where type name is the (integer) type of unit. The construct is not in the subset when unit2 is a tuple.

⊢ ∀(unit:time→(*)list) (rep_fn:**→word32) int t.
DYNAMIC_INDEX unit rep_fn int t =
EL' (UNLIFT (LIFT_num_of_word32 (rep_fn (UNLIFT (int t))))) (unit t)

Subsetting when unit2 is a row:

[[unit2[int_{1}..int_{2}]]] = "SUBSET [[unit2]] [[int_{1}]] [[int_{2}]]"

⊢ ∀(unit:time→(*)list) int1 int2 t.
SUBSET unit int1 int2 t =
MAP
(λn. EL' n (unit t))
((UNLIFT (LIFT_num_of_word32 (UNLIFT int1))) UPTO
 (UNLIFT (LIFT_num_of_word32 (UNLIFT int2))))

For the term representing the semantics to be reducible, int_{1} and int_{2} must satisfy:

1 ≤ int_{1} ≤ int_{2} ≤ m

where m is the size of the row.

Subsetting when unit2 is a tuple:

[[unit2[int_{1}..int_{2}]]] = "SUBSET_MULT [[unit2]] (λ(x1',...,xn'). (xi',...,xj'))"

where n is the ‘size’ of the tuple, i is the value of int_{1}, and j is the value of int_{2}. i and j must both be numeric constants and i … j must be a sub-range of 1 … n for the translation to succeed. The definition of SUBSET_MULT is:

⊢ ∀(unit:time→*) (f:*→**) t. SUBSET_MULT unit f t = f (unit t)

2.8.11 Conditionals

[[IF boolean THEN unit_{1} ELSE unit_{2} FI]] = "IF_UNIT [[boolean]] [[unit_{1}]] [[unit_{2}]]"

⊢ ∀b (x:time→*) y t. IF_UNIT b x y t = (UNLIFT b ⇒ x t | y t)

2.8.12 Tuples of Units

  [[(unit_{1}, ... ,unit_{n})]] = "MULTIPLE (λt'. ([[unit_{1}]] t', ... ,[[unit_{n}]] t'))"

  ⊢ ∀(f:time→*) t. MULTIPLE f t = f t

Each unit_{i} is a signal, a function from time to some type ty_{i}. The tuple is to be represented by a function from time to the type (ty_{1} × … × ty_{n}). In order to do this time must be moved up through the tuple of signals. In the HOL type system this cannot be done in a generic way, that is to say, for general n it cannot be captured within the definition of MULTIPLE.

The constant MULTIPLE is redundant, but is included in the translation since it indicates to the system’s tools that the construct was generated by translation of a tuple of units. A family of constants could be defined, one for each possible size of tuple, but this would not be generic because in principle there are infinitely many constants in the family, and they could not all be defined within the system. However, such constants could capture the type-casting within their definitions.

2.9 The ELLA CASE Statement

The ELLA CASE statement behaves as a generalised multiplexer. An input (a unit) is compared with ELLA constants. If one of the constants matches the input, an ELLA expression corresponding to the constant is used as the result of the CASE statement. The statement may have an optional ‘default’ result. If none of the constants match the input, this default is used. If no default is present, the result of the CASE statement is undefined. The construct has the following semantics:

[[CASE unit_{1}

OF choices_{1} ELSEOF choices_{2} ... ELSEOF choices_{n} ELSE unit_{2}

   ESAC]] =

"CASE [[unit_{1}]] [[[choices_{1}]]; ... ;[[choices_{n}]]] [[unit_{2}]]"

where the HOL constant CASE is defined by:

  ⊢ (∀(unit:time→*) (else:time→**) t. CASE unit [] else t = else t) ∧
    (∀unit f l else t.
      CASE unit (CONS f l) else t = f unit (CASE unit l else t) t)

The first argument to CASE is an ELLA unit. It is the input to the CASE statement. The second argument is a list. There is one element in this list for each OF or ELSEOF in the ELLA text. The third argument is the default output unit. The HOL constant CASE is defined recursively on the second argument. Note that the input and output to the CASE statement are signals, i.e., functions of time.

The semantics of the CASE statement requires choices_{1} to be tested first for a match with the input, and only if there is no match should the other choices be considered. If no choices provide a match, the ELSE clause is used as the output. The definition of CASE expresses this semantics by making the tail of the list of choices a default to be used if the head does not provide a match, or in the case of the list being empty, the ELSE clause is immediately used as the default. Here is a simple example:

  CASE in OF lo: hi, hi: lo ESAC.

The HOL representation for this ELLA text is:

  CASE
  in
  [OF[CONST lo,SIGNAL LIFT_hi;CONST hi,SIGNAL LIFT_lo]]
  (εx'. T)

Here, the second argument to CASE is a list of one element. The value of that element and the value of the third argument are explained shortly. Applying the HOL term above to a variable t representing a time, and expanding once with the definition of CASE yields:

  OF
  [CONST lo,SIGNAL LIFT_hi;CONST hi,SIGNAL LIFT_lo]
  in
  (CASE in [] (εx'. T) t)
  t

Expanding once more gives:

  OF
  [CONST lo,SIGNAL LIFT_hi;CONST hi,SIGNAL LIFT_lo]
  in
  ((εx'. T) t)
  t

For the first expansion, the second clause of the definition of CASE was used. For the second expansion the list argument was empty, so the first clause of the definition was used. It can now be seen that the value of the HOL term depends on the definition of the semantic constant OF.

If no ELSE clause is present, as in the example above, the translation is given by:

[[CASE unit

OF choices_{1} ELSEOF choices_{2} ... ELSEOF choices_{n}

   ESAC]] =

"CASE [[unit]] [[[choices_{1}]]; ... ;[[choices_{n}]]] ((εx'. T):time→type)"

where type is the result type of the CASE statement. (εx'. T) is a value which cannot be simplified and so it behaves as an unspecified value. If the choosers are sensible, this term will be discarded. Only if none of the choosers match will it become the result of the CASE statement. In this case a value for the CASE statement will be unobtainable because (εx'. T) is irreducible. This corresponds to the statement being undefined in practice because none of the choosers match and there is no default option (ELSE clause).

It would have been preferable to have used UU to represent the undefinedness, but the result type could be structured, so it would have been necessary to build a term of the appropriate structure with UUs as its basic elements. This is undesirable because it is not a generic approach.

Each OF and ELSEOF clause of a CASE statement consists of a set of choices:

{[[choosers_{1}: unit_{1}, ... ,choosers_{n}: unit_{n}]] = \atop "OF [[[choosers_{1}]],[[unit_{1}]]; ... ;[[choosers_{n}]],[[unit_{n}]]]"}

where each chooser is used as a pattern, and each unit as an output value. This has already been illustrated by the example. The HOL constant OF is defined by:

  ⊢ (∀(in:time→*) (else:**) t. OF [] in else t = else) ∧
    (∀pair rest in else t.
      OF (CONS pair rest) in else t =
      (UNLIFT ((FST pair) (in t)) ⇒ (SND pair) t | OF rest in else t))

OF is defined recursively in a similar way to CASE. If all the choosers have been tried without success, the default is used. The default is the remainder of the CASE statement (see above). Otherwise the list of chooser/unit pairs is not exhausted, so the first pair is tested. The chooser (represented by a predicate) is applied to the input value. If the result is not defined, then the CASE statement is not defined. If the result is true, the corresponding unit becomes the result of the statement, otherwise the next chooser is tested by a recursive call. So, continuing the example given earlier by expanding with the definition of OF, the following term is obtained:

  (UNLIFT ((FST (CONST lo,SIGNAL LIFT_hi)) (in t))) ⇒
  ((SND (CONST lo,SIGNAL LIFT_hi)) t) |
  (OF [CONST hi,SIGNAL LIFT_lo] in ((εx'. T) t) t)

Using the definitions of FST and SND this simplifies to:

  (UNLIFT (CONST lo (in t))) ⇒
  (SIGNAL LIFT_hi t) |
  (OF [CONST hi,SIGNAL LIFT_lo] in ((εx'. T) t) t)

The ELLA system requires that the choosers of each OF are distinct. The HOL semantics assumes that this is the case though the translator does not currently check this. It does not however seem an unreasonable assumption, since any ELLA design to be verified could have previously been passed through the compiler of the ELLA system. In the event that the choosers are not distinct, the HOL semantics uses the unit associated with the first chooser (in textual order) to match.

2.10 Series

ELLA series can be used to describe hardware structurally. The MAKE statement allows instances of ELLA functions (representing components) to be created and named. These can then be connected together using the JOIN statement. The LET statement allows expressions (ELLA units) to be given an abbreviation (a local identifier is declared).

ELLA series are translated as follows:

  [[BEGIN step_{1}. ... step_{n}. OUTPUT unit END]] =

"εOUTPUT. ∃local variables. SERIES [[[step_{1}]]; ... ;[[step_{n}]]] OUTPUT [[unit]]"

[[( step_{1}. ... step_{n}. OUTPUT unit )]] =

"εOUTPUT. ∃local variables. SERIES [[[step_{1}]]; ... ;[[step_{n}]]] OUTPUT [[unit]]"

A series is represented by considering each step to be a Boolean-valued expression. A variable called OUTPUT is introduced which is equated with the value of the output unit. This equation and the representation of the steps are conjoined to yield a Boolean value. Having existentially quantified over the variables local to the steps, a value of OUTPUT that makes the expression true is selected. This is done using Hilbert’s ε-operator. Provided the series is well-formed, the value selected is unique.

The HOL constant SERIES is defined recursively by:

  ⊢ (∀result (unit:*). SERIES [] result unit = (result = unit)) ∧
    (∀x l result unit.
      SERIES (CONS x l) result unit = x ∧ SERIES l result unit)

For each internal ‘line’ of the series, there are two local variables. One represents the value on the line (and has the same name as the line). The other is used as a link between MAKE and JOIN statements (see below) and has the name of the line appended with ‘_fn’. For example, the series:

  BEGIN
     MAKE INV: out.
     JOIN in -> out.
  OUTPUT out
  END

is translated to:

  εOUTPUT.
   ∃out out_fn.
    SERIES
    [MAKE[[MAKEITEM INV out_fn]];
     JOIN[JOINITEM in out out_fn(λx'. εf1'. ∀t'. f1' t' = x' t')]]
    OUTPUT
    out

where out_fn makes a connection between the MAKE and JOIN parts of the translation.

For typing reasons, it is not possible to use the value on the line (out) as a link. The idea of using the additional linking variable is due to Mike Gordon. Note that in the HOL translation SERIES is a constant, whereas OUTPUT is a variable of the same type as [[unit]].

2.10.1 MAKE statements

A MAKE statement creates and names instances of functions. The semantics of MAKE is given by:

[[MAKE makeitem_{1}, ... ,makeitem_{n}]] = "MAKE [[[makeitem_{1}]]; ... ;[[makeitem_{n}]]]"

  ⊢ ∀l. MAKE l = ITLIST $∧ (MAP (λx. ITLIST $∧ x T) l) T

MAKE forms a conjunction of equations. The equations are present in the makeitems, which have the following semantics:

[[fnname: name_{1} ... name_{n}]] =

  "[MAKEITEM fnname name_{1}_fn; ... ;MAKEITEM fnname name_{n}_fn]"

where for each i, name_{i}_fn is a variable of the same type as fnname.

Each application of MAKEITEM yields a Boolean value, and MAKE simply conjoins these together. The definition of MAKEITEM is an equation between the two arguments:

  ⊢ ∀(dev:*) fun. MAKEITEM dev fun = (fun = dev)

The argument of MAKE is a list of lists. This allows for the abbreviations possible in ELLA. For example,

  MAKE INV: l1,
       MUX: l3 out,
       REG: l2 l4.

is represented by:

  MAKE [[MAKEITEM INV l1_fn];
        [MAKEITEM MUX l3_fn;MAKEITEM MUX out_fn];
        [MAKEITEM REG l2_fn;MAKEITEM REG l4_fn]]

Multiple instances of functions can be created using MAKE. The constants MAKE_REP and MAKEITEM_REP are used to represent this:

[[[int] fnname: name_{1} ... name_{n}]] =

  "[MAKEITEM_REP (MAKE_REP [[int]] fnname) name_{1} name_{1}_fn; ... ;
    MAKEITEM_REP (MAKE_REP [[int]] fnname) name_{n} name_{n}_fn]"

MAKE_REP makes a list of copies of fnname. Having a list of functions as the type for name_{i}_fn only works because ELLA insists that each individual component be ‘connected’ separately. See the discussion of JOIN for more details.

  ⊢ ∀int (dev:*).
     MAKE_REP int dev =
     REPLICATE (UNLIFT (LIFT_num_of_word32 (UNLIFT int))) dev

MAKEITEM_REP is similar to MAKEITEM but has an additional constraint:

  ⊢ ∀(dev:(*)list) (line:time→(**)list) fun.
     MAKEITEM_REP dev line fun =
     (fun = dev) ∧ (∀t. LENGTH (line t) = LENGTH dev)

The constraint on the length of the row called line is required because of the inadequacy of representing ELLA rows with HOL lists. Without the restriction it is possible to do much of what one would expect. However, if the row appears existentially quantified in the term being dealt with then it may be underspecified, preventing required properties from being proved. In particular, equality between rows may be expressed by equalities between corresponding elements. This is only adequate if the rows are known to be of the same length and an equation is given for each element up to that length.

2.10.2 JOIN statements

The JOIN statement ‘connects’ an input unit to a function. It is represented in a similar way to MAKE; it conjoins the elements of the list it takes as an argument:

[[JOIN joinitem_{1}, ... ,joinitem_{n}]] = "JOIN [[[joinitem_{1}]]; ... ;[[joinitem_{n}]]]"

  ⊢ ∀l. JOIN l = ITLIST $∧ l T

Connecting a row to an output (name) declared by a MAKE of the form:

  MAKE [int]fnname: name

is not allowed in ELLA, i.e., the following cannot be used:

  JOIN row -> name

Instead each element of the row has to be connected explicitly:

  FOR INT i = 1..int JOIN row[i] -> name[i]

The FOR statement (multiplier) has the following semantics:

[[FOR INT name_{1} = int_{11}..int_{12} ... INT name_{m} = int_{m1}..int_{m2}

JOIN joinitem_{1}, ... ,joinitem_{n}]] = "JOIN (FOR [[int_{11}]] [[int_{12}]] (λname_{1}. FOR [[int_{21}]] [[int_{22}]]

   (λname_{2}. FOR ...

⋮      ⋮

(λname_{m}. [[[joinitem_{1}]]; ... ;[[joinitem_{n}]]]))...))"

The behaviour of the ELLA compiler suggests that the last INT variable should be nested most deeply. Consider the following ELLA text:

  TYPE bit = NEW (hi | lo).
  FN COMP = (bit) -> bit: DELAY(lo, 1).
  FN TEST = ([8]bit: in) -> [8]bit:
   BEGIN
      MAKE [8]COMP: comps.
      FOR INT i = 1..4 INT i = 5..8 JOIN in[i] -> comps[i].
   OUTPUT comps
   END.

This fails to compile. The error messages say that the input of comps[5] has already been joined. The same is stated about comps[6], comps[7] and comps[8]. Each message appears three times. This indicates that the i in the body of the FOR statement is bound by the most deeply nested of the INT variables. However, there is a confusing feature: all three error messages for comps[5] appear before the error messages for comps[6], and so on. This suggests that each value of the outer INT is being explored for the first value of the inner INT (namely 5) before the second value of the inner INT is considered. Error messages also appear stating that the inputs

of comps[1], comps[2], comps[3] and comps[4] have not been supplied.

The HOL constant FOR instantiates the body of the FOR construct it represents with each integer in the range int_{1} … int_{2}. Each instantiation produces a list of Boolean values. From each list a conjunction is formed, so the result of the entire application of FOR is a new list of Booleans to be further conjoined by another FOR or by JOIN:

  ⊢ ∀int1 int2 f.
     FOR int1 int2 f =
     MAP
     (λn. ITLIST $∧ (f (LIFT_word32_of_num n)) T)
     ((UNLIFT (LIFT_num_of_word32 (UNLIFT int1))) UPTO
      (UNLIFT (LIFT_num_of_word32 (UNLIFT int2))))

If the range of a FOR construct is empty (the second integer is less than the first), the HOL infix function UPTO in the definition of FOR evaluates to an empty list. This will result in the JOIN statement being denoted by T (true) in the logic. Such a denotation asserts nothing about the lines involved in the JOIN statement. The intuitive meaning of this is that no lines are connected.

Joinitems have the following semantics:

[[unit -> name]] = "JOINITEM [[unit]] name name_fn ty cast"

where name_fn is a variable of function type, the function being from an entity with the type of [[unit]] to an entity with the type of name. ty cast is a type casting function which converts a tuple-valued signal into a tuple of signals. This has to be applied to [[unit]] for types to match. Type casting in the opposite direction is required in other parts of the semantics for ELLA.

JOINITEM is defined by:

  ⊢ ∀in (out:***) fun (g:*→**). JOINITEM in out fun g = (fun (g in) = out)

Joining to individual components of a ‘row’ of components is translated as follows:

[[unit -> name [int]]] =

"JOINITEM [[unit]] (INDEX name [[int]]) (JOIN_INDEX name_fn [[int]]) ty cast"

INDEX is defined on page 27. JOIN_INDEX is defined by:

  ⊢ ∀(devs:(*)list) int.
     JOIN_INDEX devs int =
     EL' (UNLIFT (LIFT_num_of_word32 (UNLIFT int))) devs

The HOL variable corresponding to name must be of type time→(*)list so that it can be used as part of the input to a JOIN or as the OUTPUT. In other words it must conform to the structure of units.

The ‘outputs’ of a JOIN statement may also be used as inputs. In particular, the output of one joinitem may be used as an input to an earlier joinitem. This means that the translator has to make all the outputs available in the environment when processing the joinitems. However, two passes are not required because the outputs of the joinitems must have already been declared in preceding makeitems.

2.10.3 LET statements

The semantics of the LET statement is given by:

[[LET letitem_{1}, ... ,letitem_{n}]] = "LET' [[[letitem_{1}]]; ... ;[[letitem_{n}]]]"

The name LET' has to be used for the HOL constant because LET is already a defined constant in the HOL system.

  ⊢ ∀l. LET' l = ITLIST $∧ l T

Letitems simply form an equation between a local identifier and a unit:

[[name = unit]] = "LETITEM name [[unit]]"

  ⊢ ∀(name:*) unit. LETITEM name unit = (name = unit)

2.11 Macros

ELLA macros are in essence parameterised functions. The parameterisation can be for size (e.g., for an n-bit adder the macro would be parameterised by n) or datatype. Macros provide the means for making recursive definitions. The translation of macros into the HOL system is not as straightforward as for most of the constructs in the subset. In this respect the semantics given to macros here is not entirely formal. This was considered to be a reasonable compromise because the inclusion of macros significantly increases the expressive power of the ELLA subset.

Recursive macro declarations are supported provided they are primitive recursive. However, there can be only one recursive macro parameter and it must be the only explicit parameter.

Macro parameters can be integers or types. The HOL representations involve an additional variable for the integer parameters, and polymorphic types for the type parameters. An ELLA type parameter called name becomes a HOL polymorphic type *name. By including a dummy argument of a polymorphic type for each type parameter, it is possible to match the actual parameters used in an invocation of a macro to the parameters specified in the macro declaration. The parameterised types in the macro declaration become instantiated in the invocation of the macro via the dummy arguments.

2.11.1 Implicit and Explicit Macro Parameters

Implicit macro parameters allow variable numbers of inputs (actually a variablesized ELLA row). By modelling the inputs as a HOL list, it is possible to deal with implicit macro parameters. The variable length of the HOL list models the variable number of inputs to the ELLA macro. Checking that the number of inputs (size of list) is correct when a macro is instantiated is a type-checking task in the ELLA system. In the HOL representation, part of the job is left as a proof obligation.

The explicit parameters of a macro are translated to a tuple. The implicit parameters are also modelled as a tuple, but a lifted one. This allows UU to be used to represent the implicit parameters when they are not given explicitly (HOL functions cannot have optional arguments). The body of the HOL function representing the macro is defined so that if its implicit-parameters argument is UU it infers the values of the implicit parameters from the other parameters.

Here is an example:

  MAC TEST {INT x} = ([INT n]TYPE t: in1 in2, [INT m]bit: in3) -> t: in1 [n].

The translation into HOL is given below. However, the body of the declaration has been displayed as ELLA text rather then the HOL term representing it. This is appropriate because the translation of the body is straightforward; it is only the parameters that are translated in an ad hoc manner. The naming of the parameters is explained in Section 2.11.2.

  TEST x_mac implicit' (in1,in2,in3) =
     let n_mac = (implicit' = UU) ⇒
                 (εx'. (∀t'. x' = LENGTH (in1 t'))) |
                 (λ(x1',x2',x3'). x1') (UNLIFT implicit')
     and m_mac = (implicit' = UU) ⇒
                 (εx'. (∀t'. x' = LENGTH (in3 t'))) |
                 (λ(x1',x2',x3'). x3') (UNLIFT implicit')
     in (let x = LIFT_word32_of_num x_mac
         and n = LIFT_word32_of_num n_mac
         and m = LIFT_word32_of_num m_mac
         in in1[n])

In a MAKE statement the implicit parameters have to be given explicitly because they cannot be inferred:

  FN TEST1 = ([8]bit: in) -> bit:
   BEGIN
      MAKE TEST {5} {8,bit,8}: test.
      JOIN (in,in,in) -> test.
   OUTPUT test
   END.

With special pretty-printing for HOL terms representing ELLA text, the result of the translation is:

  TEST1 in = BEGIN
                MAKE TEST 5 (LIFT (8,(εx'. T),8)): test.
                JOIN (in, in, in) -> test.
             OUTPUT test
             END

Observe that the implicit parameters are given explicitly as a lifted tuple. The second implicit parameter is a type. In the HOL representation the type is instantiated by supplying an arbitrary term (εx'. T) of the appropriate type. The type is not shown in the term above.

An example of a macro with an explicit type parameter is:

  MAC LAST {TYPE tp} = ([INT n]tp: in) -> tp: in [n].

This translates to:

  LAST TYPE1 implicit' in =
     let n_mac = (implicit' = UU) ⇒
                 (εx'. (∀t'. x' = LENGTH (in t'))) |
                 (λx1'. x1') (UNLIFT implicit')
     in (let n = LIFT_word32_of_num n_mac in INDEX in n)

where TYPE1 is a dummy variable, used only so that the type parameter can be instantiated later. The instantiation is illustrated by:

  FN EIGHTH = ([8]bit: in) -> bit: LAST {bit} in.

which translates to:

  EIGHTH in = INVOKE (λx'. (εf1'. (∀t'. f1' t' = x' t'))) (LAST (εx'. T) UU) in

Note that UU is used in the translation when the implicit parameters are not given. INVOKE is described on page 23.

The polymorphic types used to represent type macro parameters have to be general. They cannot be restricted to lifted types as one might expect because the lifting in types may not be at the top level. For a structured type, the lifting occurs at the level of the basic types, e.g.:

                         (bit)lifted # (bit)lifted

So, if the type (*)lifted were used to represent the macro parameter, it would not be instantiatable to the above type. The polymorphic types used to represent type parameters have to be made available to the routine that translates the body of the macro declaration since the type parameters may be used within the body.

2.11.2 Representation of Integer Macro Parameters

Integers used as macro parameters are not translated in the usual way to a 32-bit word. Instead they are translated to natural numbers. Restrictions are placed on the form of the expressions used to instantiate macro parameters. For example, negative constants are not permitted.

For recursive macros, the recursive macro parameter (suppose it is called n) is translated to the HOL term (SUC n_mac). (SUC n_mac) is also used at the recursive call. In all other places in the body of the macro, occurrences of n are translated to the HOL variable n which is defined to be the 32-bit-word equivalent of (SUC n_mac). This enforces a restriction on the range of the number anywhere it is used in the body other than in macro calls. If the number is out of the 32-bit range, then n is undefined. To illustrate this, here is a rather contrived example:

  MAC FIRST {INT n} = ([8]bit: in) -> bit:
   IF n = 1 THEN in[n] ELSE FIRST {n - 1} in FI.

  FIRST(SUC n_mac)in =
  (let n = LIFT_word32_of_num(SUC n_mac)
   in
    IF_UNIT
    (n EEQ (LIFT #00000000000000000000000000000001))
    (INDEX in n)
    (INVOKE(λx'. εf1'. ∀t'. f1' t' = x' t')(FIRST n_mac)in))

Before attempting to make a primitive recursive definition in HOL, terms of the form (SUC n_mac)-1 are simplified to n_mac. If this were not done the definition would fail. The primitive recursive definition mechanism in the HOL system allows the case for zero to be omitted. This is very useful since there is no need to find the base case in the ELLA declaration. To do so would require analysis of the declaration and it would also be necessary to construct a simplified version of the body of the declaration to be used as the zero case for the HOL definition.

The lack of a definition of the behaviour of the macro when the recursive parameter is zero is consistent with the behaviour of the ELLA compiler/simulator. An instantiation with zero should be undefined because it corresponds to a null circuit. The ELLA system appears to expect the base case of a recursive macro to be at least 1. There is no clear meaning for instances of a macro parameter with values less than the base-case value. Tests indicate that the ELLA compiler accepts such instances of macros but there is a failure at either the assembly or simulation stage.

Due to restrictions imposed by the recursive definition facility of the HOL system, a recursive macro parameter must be the only explicit parameter. This is because the explicit parameters are translated to a tuple, and the HOL recursive definition system does not currently allow a recursive argument to appear in a tuple. The HOL definition mechanism could in principle be extended to allow other parameters, but such work was beyond the scope of the project to support ELLA in HOL.

3 An Example with Parameterised Adders

Confirmation of the correctness of the HOL semantics for the ELLA subset is difficult, if not impossible, to achieve formally. ELLA is a real rather than a toy hardware description language, and its semantics is given only by the behaviour of the standard compiler and simulator for the language. As a means of obtaining confirmation of its correctness, the HOL semantics has been exercised by attempting proofs involving as much as possible of the ELLA subset. The first proof performed in the combined HOL-ELLA system was a proof of correctness of a parity checker [BGHT90], but this exercised only a small part of the supported ELLA subset.

For a more thorough test of the semantics, a proof of the equivalence of the HOL representations of two ELLA descriptions of n-bit adders was chosen. The descriptions are given in the ELLA documentation [Com89b], so in some sense can be considered to be real examples. They also have the advantage that they make use of a significant proportion of the subset of ELLA supported in the HOL-ELLA system. However, to date not all of the subset has been tested.

In addition to confirming that the semantics is indeed an accurate representation of the behaviour of ELLA descriptions, the example was worthwhile because it provided information concerning the difficulty of proofs about terms that have been generated by machine rather than thought up by a person. There are a number of features of the semantics in HOL that tend to make proofs from ELLA text more difficult than conventional verification proofs in HOL. The proof described below brought to light several inadequacies in the original semantics. These inadequacies were rectified before proceeding with the example and the changes are present in the semantics described in Section 2.

The two descriptions of n-bit adders to be proved equivalent are both examples of ELLA macros. One is a parallel implementation of an n-bit adder. The other is a recursive implementation. Both make use of a subcomponent called FULL_ADDER which behaves as a one-bit full adder. The only fact about FULL_ADDER required for the equivalence proof is that when its inputs are defined, so are its outputs. The particular lemma used takes a more specific form than this, but the preceding statement captures the thrust of the lemma.

The ELLA descriptions of the adder implementations are given below:

  MAC N_BIT_ADDER = ([INT n]tri: i j, tri: carryin) -> ([n]tri, tri):
   BEGIN
      MAKE [n]FULL_ADDER: fulladd.
      LET carry = carryin CONC ([INT k=1..n-1]fulladd[k][2]).
      FOR INT k=1..n JOIN (i[k], j[k], carry[k]) -> fulladd[k].
   OUTPUT ([INT k=1..n]fulladd[k][1], fulladd[n][2])
   END.

MAC REC_ADDER {INT n} = ([n]tri: i j, tri: carryin) -> ([n]tri, tri):
(LET oneadd = FULL_ADDER(i[1], j[1], carryin).
OUTPUT IF n=1
       THEN ([1]oneadd[1], oneadd[2])
       ELSE (LET recadder =
              REC_ADDER{n-1}(i[2..n], j[2..n], oneadd[2]).
             OUTPUT (oneadd[1] CONC recadder[1], recadder[2]))
       FI).

The two adder implementations are described in the ELLA tutorial [Com89b]. Circuit diagrams are given in Figure 1 of this paper. N_BIT_ADDER is a parallel adder. REC_ADDER is specified recursively.

An outline of the main steps of the equivalence proof is as follows:

• Elimination of semantic constants.

• Introduction of assumptions.

• Manual simplification of the definitions.

• Use of induction on the size of the adders, and proof of the base case.

• Enriching of the assumptions.

• Use of the induction hypothesis. This stage requires the lemma mentioned above about the definedness of FULL_ADDER.

• Splitting of the internal bus of signals appearing in the left-hand side of the equation so that the two sides of the equation can be shown to be the same.

• Unwinding of internal signals by substitution using their equations followed by quantifier elimination. A lemma asserting the existence of a unique solution to the recursive equation for the internal bus is required at this stage.

Before this proof of equivalence is discussed in detail, the definitions of the lowerlevel components are given, all of which are automatically translated into HOL.

3.1 A One-Bit Full Adder

The adders described in this section operate over a three-valued logic. The ELLA type is defined below. The declaration gives rise to a new HOL type tri as described in Section 2.4.

TYPE tri = NEW (hi | lo | xx).

The one-bit full adder is described using an ELLA series. It has three inputs, two outputs, and uses two half adders and an OR gate as sub-components:

[figure: FULL_ADDER; FULL_ADDER; FULL_ADDER; FULL_ADDER; j[n]; i[n]; j[3]; i[3]; j[2]; i[2]; j[1]; i[1]; fulladd[n][1]; fulladd[3][1]; fulladd[2][1]; fulladd[1][1]; carry[n]; carry[3]; carry[2]; carry[1]; carryin; fulladd[n][2]]

            REC_ADDER{n-1}

              FULL_ADDER
j[n]

i[n]

j[3]

i[3]

j[2]

i[2]

j[1]

i[1]
                                   recadder[1][n-1]

                                   recadder[1][2]

                                   recadder[1][1]

                                   oneadd[1]
                    oneadd[2]

                carryin
              recadder[2]

.

.

. .

.

.

Figure 1: N_BIT_ADDER (at top) and REC_ADDER{n}

FN FULL_ADDER = (tri: a b carryin) -> (tri, tri):
BEGIN
   LET first  = HALF_ADDER(b, carryin),
       second = HALF_ADDER(a,first[2]),
       carry  = TRI_OR(first[1], second[1]),
       sum    = second[2].
OUTPUT (carry, sum)
END.

The half adder is also described using an ELLA series:

FN HALF_ADDER = (tri: inp1 inp2) -> (tri, tri):
BEGIN
   MAKE TRI_NOT: n1 n2,
        TRI_AND: a1 a2 a3,
        TRI_OR:  o1.
   JOIN (inp1, inp2) -> a1,
        inp1         -> n1,
        inp2         -> n2,
        (inp1, n2)   -> a3,
        (inp2, n1)   -> a2,
        (a2, a3)     -> o1.
OUTPUT (a1, o1)
END.

The basic logic gates are described using simple CASE statements:

FN TRI_OR = (tri: input1 input2) -> tri:
CASE (input1, input2)
OF (lo, lo): lo,
   (hi, tri) | (tri, hi): hi
ELSE xx
ESAC.

FN TRI_AND = (tri: input1 input2) -> tri:
CASE (input1, input2)
OF (hi, hi): hi,
   (lo, tri) | (tri, lo): lo
ELSE xx
ESAC.

FN TRI_NOT = (tri: input) -> tri:
CASE input
OF lo: hi,
   hi: lo
ELSE xx
ESAC.

3.1.1 Translation to HOL

As examples of the translation process, the HOL theorems (definitions) corresponding to the ELLA declarations of TRI_OR and HALF_ADDER are given below. The logical terms may appear at first glance to be quite different from the original ELLA text, but closer inspection should reveal a close correspondence between the logical term and the abstract-syntax tree of the ELLA text.

1

  ⊢ ∀input1 input2.
     TRI_OR(input1,input2) =
     CASE
     (MULTIPLE(λt'. (input1 t',input2 t')))
     [OF
      [(λ(x1',x2'). CONST_MULTIPLE[CONST lo x1';CONST lo x2']),
       SIGNAL LIFT_lo;
       CONST_SET
       [λ(x1',x2'). CONST_MULTIPLE[CONST hi x1';MATCH_ALL x2'];
        λ(x1',x2'). CONST_MULTIPLE[MATCH_ALL x1';CONST hi x2']],
       SIGNAL LIFT_hi]]
     (SIGNAL LIFT_xx)

The number in the small box in the top right corner of the box above labels the definition so that it can be referred to later. Lemmas and assumptions are also labelled in this way.

2 ⊢ ∀inp1 inp2.

HALF_ADDER(inp1,inp2) =
(εOUTPUT.
∃n1 n2 a1 a2 a3 o1 n1_fn n2_fn a1_fn a2_fn a3_fn o1_fn.
SERIES
[MAKE
[[MAKEITEM TRI_NOT n1_fn;MAKEITEM TRI_NOT n2_fn];
[MAKEITEM TRI_AND a1_fn;MAKEITEM TRI_AND a2_fn;
 MAKEITEM TRI_AND a3_fn];[MAKEITEM TRI_OR o1_fn]];
JOIN
[JOINITEM
(MULTIPLE(λt'. (inp1 t',inp2 t')))
a1
a1_fn
(λx'. ε(f1',f2'). ∀t'. f1' t',f2' t' = x' t');
JOINITEM inp1 n1 n1_fn(λx'. εf1'. ∀t'. f1' t' = x' t');
JOINITEM inp2 n2 n2_fn(λx'. εf1'. ∀t'. f1' t' = x' t');
JOINITEM
(MULTIPLE(λt'. (inp1 t',n2 t')))
a3
a3_fn
(λx'. ε(f1',f2'). ∀t'. f1' t',f2' t' = x' t');
JOINITEM
(MULTIPLE(λt'. (inp2 t',n1 t')))
a2
a2_fn
(λx'. ε(f1',f2'). ∀t'. f1' t',f2' t' = x' t');
JOINITEM
(MULTIPLE(λt'. (a2 t',a3 t')))
o1
o1_fn
(λx'. ε(f1',f2'). ∀t'. f1' t',f2' t' = x' t')]]
OUTPUT
(MULTIPLE(λt'. (a1 t',o1 t'))))

3.1.2 Verification of One-Bit Adder

The half adder and full adder have been proved correct with respect to behavioural specifications. The proofs of correctness are straightforward though the use of lifting in the semantics causes complications. These have largely been overcome by the use of automatic tools. As an illustration of how lifting can be dealt with in a uniform way, here is a lemma about TRI_OR used in the correctness proofs:

3 ⊢ ∀x y.

TRI_OR(LIFT o x,LIFT o y) =
LIFT o (λt. (((x t = lo) ∧ (y t = lo)) ⇒ lo |
       (((x t = hi) ∨ (y t = hi)) ⇒ hi | xx)))

This lemma has been proved using the automatic simplification tools in the HOL-ELLA system together with a small number of simple logical steps. The simplification tools expand using the definitions of the semantic constants (the logical functions that capture the abstract syntax and the semantics of ELLA constructs) and simplify the resulting terms as far as possible. The lemma above states that if the values on the inputs of TRI_OR are defined for all times then the output will be defined for all times and at time t the value is given by:

  (((x t = lo) ∧ (y t = lo)) ⇒ lo |
  (((x t = hi) ∨ (y t = hi)) ⇒ hi | xx)))

This consists of two nested conditional statements. They test the inputs at the given time and if both are lo return lo. If either input is hi, then hi is returned. Otherwise xx is returned. As can be seen, the variables x and y range freely over all functions of type time→tri. Precomposing them with LIFT converts them to functions of type time→(tri)lifted, but these functions (e.g., (LIFT o x)) do not range freely over the type, but are restricted to functions which are defined for all times.

3.1.3 Automatic Simplification

The theorem defining HALF_ADDER can be simplified in a single step using the automatic tools:

4 ⊢ ∀inp1 inp2.

     HALF_ADDER(inp1,inp2) =
     (εOUTPUT.
       ∃n1 n2 a1 a2 a3 o1.
        (TRI_AND(inp1,inp2) = a1) ∧
        (TRI_NOT inp1 = n1) ∧
        (TRI_NOT inp2 = n2) ∧
        (TRI_AND(inp1,n2) = a3) ∧
        (TRI_AND(inp2,n1) = a2) ∧
        (TRI_OR(a2,a3) = o1) ∧
        (OUTPUT = (λt. (a1 t,o1 t))))

Another tool further simplifies this theorem by unwinding the equations:

5 ⊢ ∀inp1 inp2.

     HALF_ADDER(inp1,inp2) =
     (λt.
       (TRI_AND(inp1,inp2)t,
        TRI_OR(TRI_AND(inp2,TRI_NOT inp1),TRI_AND(inp1,TRI_NOT inp2))t))

Unwinding is the process of making substitutions for existentially quantified variables using equations featuring the variables. In the example above, the second equation (which has n1 as its right-hand side) is used to replace the occurrence of n1 in the left-hand side of the fifth equation with the term (TRI_NOT inp1). When sufficient unwinding has been done for a variable to appear only in its ‘defining’ equation, the equation and the existential quantification for the variable can be eliminated. This is only possible if the equation is not recursive.

3.1.4 Definedness Lemma for the One-Bit Adder

Before the proof of equivalence of the n-bit adders is described, a lemma required for the proof is considered. The lemma concerns the second component of the pair of signals forming the output of FULL_ADDER. The second component is in fact the sum, the first component being the carry. The lemma says that if the inputs are always defined then the sum will be too, and hence unlifting the sum and then lifting it again results in the same value as the sum (see Section 2.2 for details on UNLIFT and

LIFT).

6 ⊢ ∀a b c t.

LIFT (UNLIFT (SND (FULL_ADDER (LIFT o a,LIFT o b,LIFT o c) t))) =
SND (FULL_ADDER (LIFT o a,LIFT o b,LIFT o c) t)

3.2 Translation and Simplification of the n-bit Adders

The ELLA declarations of the n-bit adder implementations give rise to the following HOL definitions:

⊢ ∀implicit' i j carryin.
N_BIT_ADDER implicit' (i,j,carryin) =
let n_mac = (implicit' = UU) ⇒
      (εx'. (∀t'. x' = LENGTH (i t'))) |
      (λx1'. x1') (UNLIFT implicit')
in (let n = LIFT_word32_of_num n_mac
in BEGIN
    MAKE [n]FULL_ADDER: fulladd.
    LET carry = carryin CONC
                   [INT k = 1..(n - 1)]fulladd[k][2].
    FOR INT k = 1..n
       JOIN (i[k], j[k], carry[k]) -> fulladd[k].
 OUTPUT ([INT k = 1..n]fulladd[k][1], fulladd[n][2])
 END)

⊢ ∀n_mac i j carryin.
REC_ADDER (SUC n_mac) (i,j,carryin) =
let n = LIFT_word32_of_num (SUC n_mac)
in BEGIN
LET oneadd = FULL_ADDER (i[1], j[1], carryin).
OUTPUT
IF (n = 1)
THEN ([1]oneadd[1], oneadd[2])
ELSE BEGIN
        LET recadder = REC_ADDER n_mac
                       (i[2..n], j[2..n], oneadd[2]).
     OUTPUT (oneadd[1] CONC recadder[1], recadder[2])
     END
FI
END

The definitions above were displayed using a pretty-printer extended to support ELLA syntax. The theorems are given below in their raw form:

7

⊢ ∀implicit' i j carryin.
N_BIT_ADDER implicit'(i,j,carryin) =
(let n_mac =
((implicit' = UU) ⇒
(εx'. ∀t'. x' = LENGTH(i t')) |
(λx1'. x1')(UNLIFT implicit'))
in
let n = LIFT_word32_of_num n_mac
in
(εOUTPUT.
∃fulladd carry fulladd_fn.
SERIES
[MAKE
[[MAKEITEM_REP(MAKE_REP n FULL_ADDER)fulladd fulladd_fn]];
LET'
[LETITEM
carry
((λt'. [carryin t']) CONC
(VAR_REP
(LIFT #00000000000000000000000000000001)
(n EMINUS (LIFT #00000000000000000000000000000001))
(λk. INDEX_MULT(INDEX fulladd k)(λ(x1',x2'). x2'))))];
JOIN
(FOR
(LIFT #00000000000000000000000000000001)
n
(λk.
[JOINITEM
 (MULTIPLE
  (λt'. (INDEX i k t',INDEX j k t',INDEX carry k t')))
 (INDEX fulladd k)
 (JOIN_INDEX fulladd_fn k)
 (λx'. ε(f1',f2',f3'). ∀t'. f1' t',f2' t',f3' t' = x' t')]))]
OUTPUT
(MULTIPLE
(λt'.
(VAR_REP
(LIFT #00000000000000000000000000000001)
n
(λk. INDEX_MULT(INDEX fulladd k)(λ(x1',x2'). x1'))
t',INDEX_MULT(INDEX fulladd n)(λ(x1',x2'). x2')t')))))

8

⊢ ∀n_mac i j carryin.
REC_ADDER(SUC n_mac)(i,j,carryin) =
(let n = LIFT_word32_of_num(SUC n_mac)
in
(εOUTPUT.
∃oneadd.
SERIES
[LET'
[LETITEM
oneadd
(INVOKE
(λx'. ε(f1',f2',f3'). ∀t'. f1' t',f2' t',f3' t' = x' t')
FULL_ADDER
(MULTIPLE
(λt'.
  (INDEX i(LIFT #00000000000000000000000000000001)t',
   INDEX j(LIFT #00000000000000000000000000000001)t',
   carryin t'))))]]
OUTPUT
(IF_UNIT
(n EEQ (LIFT #00000000000000000000000000000001))
(MULTIPLE
(λt'.
(SIMP_REP
 (LIFT #00000000000000000000000000000001)
 (INDEX_MULT oneadd(λ(x1',x2'). x1'))
 t',INDEX_MULT oneadd(λ(x1',x2'). x2')t')))
(εOUTPUT'.
∃recadder.
SERIES
[LET'
 [LETITEM
  recadder
  (INVOKE
   (λx'. ε(f1',f2',f3'). ∀t'. f1' t',f2' t',f3' t' = x' t')
   (REC_ADDER n_mac)
   (MULTIPLE
    (λt'.
      (SUBSET i (LIFT #00000000000000000000000000000010) n t',
       SUBSET j (LIFT #00000000000000000000000000000010) n t',
       INDEX_MULT oneadd(λ(x1',x2'). x2')t'))))]]
OUTPUT'
(MULTIPLE
 (λt'.
   (((λt''. [INDEX_MULT oneadd(λ(x1',x2'). x1')t'']) CONC
     (INDEX_MULT recadder(λ(x1',x2'). x1')))
    t',INDEX_MULT recadder(λ(x1',x2'). x2')t')))))))

Note that the size argument (SUC n_mac) to REC_ADDER has to be greater than zero. This is a manifestation of the translation process but also makes sense physically because with zero as the argument the expression would represent a null circuit.

3.2.1 Elimination of Semantic Constants

The first step of the proof is to eliminate as much of the surface syntax in the definitions as possible. Much of this can be done automatically by system proof tools. The result of automatic simplification of N_BIT_ADDER is:

9

⊢ ∀implicit' i j carryin.
N_BIT_ADDER implicit'(i,j,carryin) =
(let n_mac =
((implicit' = UU) ⇒
(εx'. ∀t'. x' = LENGTH(i t')) |
(λx1'. x1')(UNLIFT implicit'))
in
let n = LIFT_word32_of_num n_mac
in
(εOUTPUT.
∃fulladd carry.
(∀t. LENGTH(fulladd t) = UNLIFT(LIFT_num_of_word32(UNLIFT n))) ∧
(carry =
(λt.
APPEND
[carryin t]
(MAP
 (λn'. (λt. (λ(x1',x2'). x2') (EL'(...n'...)(fulladd t))) t)
 (1 UPTO
  (UNLIFT
   (LIFT_num_of_word32
    (UNLIFT
     (n EMINUS (LIFT #00000000000000000000000000000001))))))))) ∧
ITLIST
$∧
(MAP
(λn'.
EL'
(...n'...)
(REPLICATE(UNLIFT(LIFT_num_of_word32(UNLIFT n)))FULL_ADDER)
((λt'. EL'(...n'...)(i t')),
 (λt'. EL'(...n'...)(j t')),
 (λt'. EL'(...n'...)(carry t'))) =
(λt. EL'(...n'...)(fulladd t)))
(1 UPTO (UNLIFT(LIFT_num_of_word32(UNLIFT n)))))
T ∧
(OUTPUT =
(λt.
(MAP
 (λn'. (λt'. (λ(x1',x2'). x1') (EL'(...n'...)(fulladd t'))) t)
 (1 UPTO (UNLIFT(LIFT_num_of_word32(UNLIFT n)))),
 (λt'.
   (λ(x1',x2'). x2')
   (EL'(UNLIFT(LIFT_num_of_word32(UNLIFT n)))(fulladd t')))
 t)))))

Several subterms have been elided to (...n'...) in the above term. In each case the elided subterm is:

  UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num n')))

3.2.2 Introduction of Assumptions

Further simplification is not practical unless some assumptions are made: The inputs are assumed to be defined for all times and the size of the adder is assumed to be given explicitly and to be a natural number greater than zero. In accordance with this, the input signals are specialised to:

                  (LIFT o carryin) : time → (tri)lifted
               ((MAP LIFT) o i) : time → ((tri)lifted)list
               ((MAP LIFT) o j) : time → ((tri)lifted)list

and the implicit macro parameter is set to the explicit value:

                               LIFT (SUC n)

where n is a variable which ranges freely over the natural numbers. SUC is the successor function on natural numbers. It adds 1 to its argument.

3.2.3 Elimination of let Statements

The body of the simplified theorem for N_BIT_ADDER has the form:

  let n_mac =
     ((implicit' = UU) ⇒
      (εx'. ∀t'. x' = LENGTH(i t')) |
      (λx1'. x1')(UNLIFT implicit'))
  in  let n = LIFT_word32_of_num n_mac
      in  ...

Now that implicit' has been instantiated to LIFT(SUC n) these let expressions can be eliminated. LIFT(SUC n) is not equal to UU by the definition of the lifting type^{5}. So, the second branch of the conditional statement is taken:

  let n_mac = (λx1'. x1')(UNLIFT (LIFT (SUC n)))
  in  let n' = LIFT_word32_of_num n_mac
      in  ...

5LIFT and UU are both constructors of the type. The results of applying two distinct constructors of a type are by definition unequal. UU is a constructor that takes no arguments.

Notice that the local n has had to be renamed n'. The subterm (λx1'. x1') is the identity function and UNLIFT of LIFT is also the identity function. Hence the term can be simplified to:

  let n_mac = SUC n
  in  let n' = LIFT_word32_of_num n_mac
      in  ...

which further simplifies to:

  let n' = LIFT_word32_of_num (SUC n)
  in  ...

Substituting for n' in the body gives rise to the following theorem:

10

⊢ N_BIT_ADDER
(LIFT(SUC n))
((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
(εOUTPUT.
∃fulladd carry.
(∀t.
LENGTH(fulladd t) =
UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num(SUC n))))) ∧
(carry =
(λt.
APPEND
[(LIFT o carryin)t]
(MAP
(λn''. (λt'. (λ(x1',x2'). x2') (EL'(...n''...)(fulladd t'))) t)
(1 UPTO
 (UNLIFT
  (LIFT_num_of_word32
   (UNLIFT
    ((LIFT_word32_of_num(SUC n)) EMINUS
     (LIFT #00000000000000000000000000000001))))))))) ∧
ITLIST
$∧
(MAP
(λn''.
EL'
(...n''...)
(REPLICATE
(UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num(SUC n)))))
FULL_ADDER)
((λt'. EL'(...n''...)(((MAP LIFT) o i)t')),
(λt'. EL'(...n''...)(((MAP LIFT) o j)t')),
(λt'. EL'(...n''...)(carry t'))) =
(λt. EL'(...n''...)(fulladd t)))
(1 UPTO
(UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num(SUC n)))))))
T ∧
(OUTPUT =
(λt.
(MAP
(λn''. (λt'. (λ(x1',x2'). x1') (EL'(...n''...)(fulladd t'))) t)
(1 UPTO
 (UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num(SUC n)))))),
(λt'.
  (λ(x1',x2'). x2')
  (EL'
   (UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num(SUC n)))))
   (fulladd t')))
t))))

Again, some subterms have been elided. Subterms appearing as (...n''...) are abbreviations for the term:

UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num n'')))

3.2.4 Valid ELLA Integers

Much of the remaining simplification relies on an assumption about the size of the parameterised device. The number of bits in the adder is assumed to be a valid ELLA integer. ELLA integers are 32-bit two’s complement numbers, so this is not an unreasonable assumption. An adder for 2^{31}-bit numbers would be a very large device! So the assumption added for the next stage of the simplification is:

11

  VALID_ELLA_INTEGER(Int_of_num(SUC n))

where Int_of_num converts a natural number to an integer.

The first simplification eliminates function composition using the theorem:

12

  ⊢ ∀f g. (f o g) = (λx. f (g x))

followed, where possible, by beta-reduction.

Now consider the following subterm which appears near the beginning of the

theorem for N_BIT_ADDER:
  ∀t.
   LENGTH(fulladd t) =
   UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num(SUC n))))

The right-hand side of this equation takes the natural number (SUC n) and converts it to a lifted 32-bit word (an ELLA integer). The lifting allows the result to be undefined if the natural number is too big to be an ELLA integer. The result is then unlifted and converted back to a (lifted) natural number. This time the lifting allows the result to be undefined if the ELLA integer being converted is negative. Finally, the lifted natural number is unlifted. Unlifting cannot take place if the value is undefined.

This process may seem ludicrous, but it is a consequence of the automatic translation of ELLA to HOL. The conversion from natural numbers to ELLA integers came from a different part of the original ELLA declaration to the conversion from ELLA integers to natural numbers. The translator did not know that they would eventually come together in this way. In principle a translator could be written that would be able to determine this, but it would have to have a very global view. More importantly, having the translator perform an optimisation would leave open the possibility of an error in the translator giving an invalid semantics. This is particularly likely in the example where it is crucial that the lifting and unlifting is done to check the value ranges.

Observe that the two-step type conversion is not the identity function for all possible values of n, but only those for which (SUC n) is a valid ELLA integer. However, in order to simplify it must be the identity function, hence the need for assumption (11).

Using the lemma:

13 ⊢ ∀n.

VALID_ELLA_INTEGER(Int_of_num n) ⟹
(UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num n))) = n)

the subterm can be transformed to:

∀t. LENGTH(fulladd t) = SUC n

When the lemma is used as a rewrite rule, the instantiated hypothesis is:

VALID_ELLA_INTEGER(Int_of_num(SUC n))

This has to be satisfied. The subgoal package of the HOL system can easily be persuaded to set this up as a new subgoal to be proved. However, in this case the hypothesis is already one of the assumptions (11), so no further proof is required.

The following subterm appears in another part of the theorem for N_BIT_ADDER:

MAP
(λn''.
(λt'.
 (λ(x1',x2'). x2')
 (EL'
  (UNLIFT
   (LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num n''))))
  (fulladd t')))
t)
(1 UPTO
(UNLIFT
(LIFT_num_of_word32
(UNLIFT
 ((LIFT_word32_of_num(SUC n)) EMINUS
  (LIFT #00000000000000000000000000000001))))))

This can be simplified in a similar manner to that just described using the lemma:

14 ⊢ ∀n.

VALID_ELLA_INTEGER(Int_of_num(SUC n)) ⟹
(UNLIFT
 (LIFT_num_of_word32
  (UNLIFT
   ((LIFT_word32_of_num(SUC n)) EMINUS
    (LIFT #00000000000000000000000000000001)))) =
 n)

to give the term:

  MAP
  (λn''.
    (λt'.
      (λ(x1',x2'). x2')
      (EL'
       (UNLIFT
        (LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num n''))))
       (fulladd t')))
    t)
  (1 UPTO n)

Unfortunately, further simplification of this term is not nearly so straightforward. The problem is that the n'' which undergoes the type transformations is local to the subterm above. The necessary assumption to simplify this term is not available. Application of lemma (13) does not succeed because the antecedent of this lemma becomes instantiated to:

  VALID_ELLA_INTEGER(Int_of_num n'')

This term cannot be passed out of the scope of n'' and so cannot be set up as a subgoal. This is because the rule:

\frac{Γ ⊢ t[x] = t′[x]}{Γ ⊢ λx. t[x] = t′[x]}

is only valid if x does not appear free in the assumptions Γ.

However, the subterm in question can be simplified using the following lemma:

15 ⊢ ∀f n.

     VALID_ELLA_INTEGER(Int_of_num n) ⟹
     (MAP
      (λm. f(UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num m)))))
      (1 UPTO n) =
      MAP(λm. f m)(1 UPTO n))

To use this lemma the following assumption has to be justified:

  VALID_ELLA_INTEGER(Int_of_num n)

but here the variable n is the global n and so the assumption can be set up as a subgoal to be proved. The proof is simple, since (SUC n) is known to be a valid ELLA integer. The required fact that n is a valid ELLA integer follows from this.

Unfortunately the above lemma does not match the part of the subterm it is to be applied to. That is to say, the rewriting tools of the HOL system will not apply the lemma because they only implement first-order matching, whereas here higherorder matching is required. This is because the variable f in the lemma represents a ‘skeleton’: the application of f to an argument is intended to be a pattern for any term containing the argument as a subterm^{6}. To support the proof, rewriting tools that perform a restricted form of higher-order matching have been implemented. They are discussed in Section 4.3. The lemma could be instantiated by hand and the result used by substitution. However, in practice this is very awkward and time-consuming. The tools were almost essential since the higher-order matching requirement arises many times during the equivalence proof.

The remaining occurrences of:

  UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num(SUC n))))

and:

  UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num n'')))

can be reduced in a similar way, so that the body of (10) becomes:

  εOUTPUT.
   ∃fulladd carry.
    (∀t. LENGTH(fulladd t) = SUC n) ∧
    (carry =
     (λt.
       APPEND
       [LIFT(carryin t)]
       (MAP(λm. (λ(x1',x2'). x2')(EL' m(fulladd t)))(1 UPTO n)))) ∧
    ITLIST
    $∧
    (MAP
     (λm.
       EL'
       m
       (REPLICATE(SUC n)FULL_ADDER)
       ((λt'. EL' m(MAP LIFT(i t'))),(λt'. EL' m(MAP LIFT(j t'))),
        (λt'. EL' m(carry t'))) =
       (λt. EL' m(fulladd t)))
     (1 UPTO (SUC n)))
    T ∧
    (OUTPUT =
     (λt.
       (MAP(λm. (λ(x1',x2'). x1')(EL' m(fulladd t)))(1 UPTO (SUC n)),
        (λ(x1',x2'). x2')(EL'(SUC n)(fulladd t)))))

3.2.5 Obtaining an Equation for the Outputs of the Adder

The aim now is to obtain an equation for the outputs of the adder. The variable fulladd represents the output signals, together with some internal signals. However, before proceeding further the following lemmas are used to tidy up the term:

6Or more generally any term that contains a subterm to which the argument matches. In the example, first-order matching is sufficient for the inner match, but in general higher-order matching might be required!

16 ⊢ (λ(x,y). x) = FST

  ⊢ (λ(x,y). y) = SND

The higher-order rewriting tools are then used to simplify with the following lemma:

17 ⊢ ∀f x n.

     MAP(λm. f m(EL' m(REPLICATE n x)))(1 UPTO n) =
     MAP(λm. f m x)(1 UPTO n)

(REPLICATE n x) is a list of n copies of x. (1 UPTO n) is the list [1;2;...;n]. (EL' m)

extracts element m of a list. The ‘skeleton’ f has to take m as an argument as well as the term to be reduced in order to ‘mop up’ extra occurrences of the bound variable. This is discussed in detail in Section 4.3.

The simplification yields the following subterm:

  ITLIST
  $∧
  (MAP
   (λm.
     FULL_ADDER
     ((λt'. EL' m(MAP LIFT(i t'))),(λt'. EL' m(MAP LIFT(j t'))),
      (λt'. EL' m(carry t'))) =
     (λt. EL' m(fulladd t)))
   (1 UPTO (SUC n)))
  T

which can be simplified further (again using higher-order rewriting) with the lemma:

18

  ⊢ ∀f g l. ITLIST $∧(MAP(λx. f x = g x)l)T = (MAP f l = MAP g l)

The result is:

  MAP
  (λm.
    FULL_ADDER
    ((λt'. EL' m(MAP LIFT(i t'))),(λt'. EL' m(MAP LIFT(j t'))),
     (λt'. EL' m(carry t'))))
  (1 UPTO (SUC n)) =
  MAP(λm t. EL' m(fulladd t))(1 UPTO (SUC n))

The next goal is to isolate fulladd on the left-hand side of an equation, but before this can be done the time t must be brought to the outside of the subterm using the following lemma:

19

  ⊢ ∀fl1 fl2. (fl1 = fl2) = (∀t. MAP(λf. f t)fl1 = MAP(λf. f t)fl2)

This lemma is quite tricky to prove. The following induction scheme was used to prove it:

20

⊢ ∀(P:(*)list→(**)list→bool).
  P[][] ∧
  (∀t1 t2. P t1 t2 ⟹ (∀h1 h2. P(CONS h1 t1)(CONS h2 t2))) ⟹
  (∀l1 l2. (LENGTH l1 = LENGTH l2) ⟹ P l1 l2)

This scheme does induction simultaneously over two lists of equal length. The result of applying the lemma is:

∀t.
MAP
(λf. f t)
(MAP
 (λm.
   FULL_ADDER
   ((λt'. EL' m(MAP LIFT(i t'))),(λt'. EL' m(MAP LIFT(j t'))),
    (λt'. EL' m(carry t'))))
 (1 UPTO (SUC n))) =
MAP(λf. f t)(MAP(λm t. EL' m(fulladd t))(1 UPTO (SUC n)))

Applying the lemma:

21

⊢ ∀f g l. MAP f(MAP g l) = MAP(f o g)l

to both sides of this equation, followed by elimination of the function composition symbols introduced by the lemma yields the subterm:

∀t.
MAP
(λx.
  FULL_ADDER
  ((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
   (λt'. EL' x(carry t')))
  t)
(1 UPTO (SUC n)) =
MAP(λx. EL' x(fulladd t))(1 UPTO (SUC n))

Having reversed this equation so that fulladd appears on the left and having opened up the APPEND in another part of the theorem, the following term for the body is obtained:

εOUTPUT.
∃fulladd carry.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(carry =
(λt.
 CONS(LIFT(carryin t))(MAP(λm. SND(EL' m(fulladd t)))(1 UPTO n)))) ∧
(∀t.
MAP(λx. EL' x(fulladd t))(1 UPTO (SUC n)) =
MAP
(λx.
  FULL_ADDER
  ((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
   (λt'. EL' x(carry t')))
  t)
(1 UPTO (SUC n))) ∧
(OUTPUT =
(λt.
 (MAP(λm. FST(EL' m(fulladd t)))(1 UPTO (SUC n)),
  SND(EL'(SUC n)(fulladd t)))))

The equation for carry can be used as a substitution in the remainder of the term and then discarded:

εOUTPUT.
∃fulladd.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(∀t.
MAP(λx. EL' x(fulladd t))(1 UPTO (SUC n)) =
MAP
(λx.
  FULL_ADDER
  ((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
   (λt'.
     EL'
     x
     (CONS
      (LIFT(carryin t'))
      (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO n)))))
  t)
(1 UPTO (SUC n))) ∧
(OUTPUT =
(λt.
 (MAP(λm. FST(EL' m(fulladd t)))(1 UPTO (SUC n)),
  SND(EL'(SUC n)(fulladd t)))))

The conjunct:

∀t. LENGTH(fulladd t) = SUC n

together with the lemma:

22 ⊢ ∀f n.

     (∀t. LENGTH(f t) = n) ⟹ (∀t. MAP(λm. EL' m(f t))(1 UPTO n) = f t)

allows:

  MAP(λx. EL' x(fulladd t))(1 UPTO (SUC n))

to be simplified to:

  fulladd t

In a similar way the lemma:

23 ⊢ ∀f g n.

     (∀t. LENGTH(g t) = n) ⟹
     (∀t. MAP(λm. f(EL' m(g t)))(1 UPTO n) = MAP f(g t))

can be used to simplify:

  MAP(λm. FST(EL' m(fulladd t)))(1 UPTO (SUC n))

to:

  MAP FST(fulladd t)

Without the conjunct that specifies the size of fulladd these manipulations would not be possible, for there would be no information about ‘elements’ n + 2, n + 3, etc., of fulladd.

This gives the final simplified theorem for N_BIT_ADDER:

24

⊢ ∀n i j carryin.
VALID_ELLA_INTEGER(Int_of_num(SUC n)) ⟹
(N_BIT_ADDER
(LIFT(SUC n))
((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
(εOUTPUT.
∃fulladd.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(∀t.
fulladd t =
MAP
(λx.
  FULL_ADDER
  ((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
   (λt'.
     EL'
     x
     (CONS
      (LIFT(carryin t'))
      (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO n)))))
  t)
(1 UPTO (SUC n))) ∧
(OUTPUT = (λt. (MAP FST(fulladd t),SND(EL'(SUC n)(fulladd t)))))))

There are further manipulations that could be performed on this theorem, but at this point it was felt that the theorem had been simplified sufficiently to embark on the equivalence proof. The equation for fulladd is recursive, so there is little to be gained from using it as a substitution in the equation for OUTPUT.

3.2.6 Simplification of the Recursive Adder

Now attention is turned to REC_ADDER. Automatic simplification followed by specialisation of the inputs and elimination of the let statement yield the theorem:

25

⊢ REC_ADDER(SUC n)((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
(εOUTPUT.
∃oneadd.
(oneadd =
FULL_ADDER
((λt'. EL' 1(((MAP LIFT) o i)t')),
(λt'. EL' 1(((MAP LIFT) o j)t')),LIFT o carryin)) ∧
(OUTPUT =
(λt.
(UNLIFT
((LIFT_word32_of_num(SUC n)) EEQ
(LIFT #00000000000000000000000000000001)) ⇒
(REPLICATE 1((λt'. (λ(x1',x2'). x1')(oneadd t'))t),
(λt'. (λ(x1',x2'). x2')(oneadd t'))t) |
(εOUTPUT'.
∃recadder.
(recadder =
REC_ADDER
n
((λt'.
MAP
(λn''. EL' n''(((MAP LIFT) o i)t'))
(2 UPTO
 (UNLIFT
  (LIFT_num_of_word32
   (UNLIFT(LIFT_word32_of_num(SUC n))))))),
(λt'.
MAP
(λn''. EL' n''(((MAP LIFT) o j)t'))
(2 UPTO
 (UNLIFT
  (LIFT_num_of_word32
   (UNLIFT(LIFT_word32_of_num(SUC n))))))),
(λt''. (λ(x1',x2'). x2')(oneadd t'')))) ∧
(OUTPUT' =
(λt''.
(APPEND
[(λt'. (λ(x1',x2'). x1')(oneadd t'))t'']
((λt'. (λ(x1',x2'). x1')(recadder t'))t''),
(λt'. (λ(x1',x2'). x2')(recadder t'))t''))))
t))))

Expanding out occurrences of the function composition symbol, and simplifying using lemmas (13), (16) and:

26 ⊢ ∀n.

VALID_ELLA_INTEGER(Int_of_num n) ⟹
(UNLIFT
 ((LIFT_word32_of_num n) EEQ
  (LIFT #00000000000000000000000000000001)) =
 (n = 1))

yields the following term for the right-hand side:

εOUTPUT.
∃oneadd.
(oneadd =
FULL_ADDER
((λt'. EL' 1(MAP LIFT(i t'))),(λt'. EL' 1(MAP LIFT(j t'))),
 (λx. LIFT(carryin x)))) ∧
(OUTPUT =
(λt.
  ((SUC n = 1) ⇒
   (REPLICATE 1(FST(oneadd t)),SND(oneadd t)) |
   (εOUTPUT'.
     ∃recadder.
      (recadder =
       REC_ADDER
       n
       ((λt'. MAP(λn''. EL' n''(MAP LIFT(i t')))(2 UPTO (SUC n))),
        (λt'. MAP(λn''. EL' n''(MAP LIFT(j t')))(2 UPTO (SUC n))),
        (λt''. SND(oneadd t'')))) ∧
      (OUTPUT' =
       (λt''.
         (APPEND[FST(oneadd t'')](FST(recadder t'')),
          SND(recadder t'')))))
   t)))

The next step is to simplify:

EL' 1(MAP LIFT(i t'))

to:

HD(MAP LIFT(i t'))

and:

MAP(λn''. EL' n''(MAP LIFT(i t')))(2 UPTO (SUC n))

to:

  TL(MAP LIFT(i t'))

and similarly for j. To do this the following lemmas are required:

27

  ⊢ ∀l. ¬NULL l ⟹ (EL' 1 l = HD l)

28

  ⊢ ∀l. ¬NULL l ⟹ (MAP(λn. EL' n l)(2 UPTO (LENGTH l)) = TL l)

To apply these lemmas some more assumptions have to be made about the input values. The input buses are assumed to be the correct width for the adder. This assumption is necessary because of the somewhat unsatisfactory use of HOL lists to represent ELLA fixed-size buses (rows). The assumption is satisfied implicitly when ELLA descriptions are used to generate real hardware. The assumptions take the form:

29

  ∀(t:time). LENGTH (i t) = SUC n

30

  ∀(t:time). LENGTH (j t) = SUC n

From these assumptions the following statements can be derived:

  ∀(t:time). LENGTH(MAP LIFT(i t)) = SUC n
  ∀(t:time). ¬NULL(MAP LIFT(i t))

These are sufficient to allow lemmas (27) and (28) to be applied.

Simplification of (SUC n = 1) to (n = 0), expansion of APPEND and use of the lemma:

31

  ⊢ ∀x. REPLICATE 1 x = [x]

gives the following theorem for REC_ADDER from which to do the equivalence proof:

32

⊢ ∀n i j carryin.
VALID_ELLA_INTEGER(Int_of_num(SUC n)) ∧
(∀t. LENGTH(i t) = SUC n) ∧
(∀t. LENGTH(j t) = SUC n) ⟹
(REC_ADDER(SUC n)((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
 (εOUTPUT.
   ∃oneadd.
    (oneadd =
     FULL_ADDER
     ((λt'. HD(MAP LIFT(i t'))),(λt'. HD(MAP LIFT(j t'))),
      (λx. LIFT(carryin x)))) ∧
    (OUTPUT =
     (λt.
       ((n = 0) ⇒
        ([FST(oneadd t)],SND(oneadd t)) |
        (εOUTPUT'.
          ∃recadder.
           (recadder =
            REC_ADDER
            n
            ((λt'. TL(MAP LIFT(i t'))),(λt'. TL(MAP LIFT(j t'))),
             (λt''. SND(oneadd t'')))) ∧
           (OUTPUT' =
            (λt''.
              (CONS(FST(oneadd t''))(FST(recadder t'')),
               SND(recadder t'')))))
        t)))))

3.3 The Main Theorem

The main conjecture is:

∀n i j carryin.
VALID_ELLA_INTEGER(Int_of_num(SUC n)) ∧
(∀t. LENGTH(i t) = SUC n) ∧
(∀t. LENGTH(j t) = SUC n) ⟹
(N_BIT_ADDER
(LIFT(SUC n))
((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
REC_ADDER(SUC n)((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin))

The proof is by induction on n.

3.3.1 Base Case of Induction

To prove the base case, the simplified theorems for N_BIT_ADDER (24) and REC_ADDER (32) are used. These theorems are applicable because of the assumptions in the conjecture above. Simplification leaves the following goal:

(εOUTPUT.
  ∃fulladd.
   (∀t. LENGTH(fulladd t) = SUC 0) ∧
   (∀t.
     fulladd t =
     [FULL_ADDER
      ((λt'. HD(MAP LIFT(i t'))),(λt'. HD(MAP LIFT(j t'))),
       (λt'. LIFT(carryin t')))
      t]) ∧
   (OUTPUT = (λt. (MAP FST(fulladd t),SND(HD(fulladd t)))))) =
(εOUTPUT.
  ∃oneadd.
   (oneadd =
    FULL_ADDER
    ((λt'. HD(MAP LIFT(i t'))),(λt'. HD(MAP LIFT(j t'))),
     (λx. LIFT(carryin x)))) ∧
   (OUTPUT = (λt. ([FST(oneadd t)],SND(oneadd t)))))

Unwinding and elimination of the existentially quantifed variables fulladd and oneadd followed by a small amount of simplification is sufficient to prove this goal and hence the base case of the induction.

3.3.2 Enriching the Assumptions

Before the step case can be proved the assumptions need to be enriched. To begin with there is the induction hypothesis:

33

∀i j carryin.
 VALID_ELLA_INTEGER(Int_of_num(SUC n)) ∧
 (∀t. LENGTH(i t) = SUC n) ∧
 (∀t. LENGTH(j t) = SUC n) ⟹
 (N_BIT_ADDER
  (LIFT(SUC n))
  ((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
  REC_ADDER(SUC n)((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin))

and the following assumptions:

34

VALID_ELLA_INTEGER(Int_of_num(SUC(SUC n)))

35

∀t. LENGTH(i t) = SUC(SUC n)

36

∀t. LENGTH(j t) = SUC(SUC n)

Assumption (34) gives rise to:

37

  VALID_ELLA_INTEGER(Int_of_num(SUC n))

Assumptions (35) and (36) imply the following statements:

38

  ∀t. LENGTH((TL o i)t) = SUC n

39

  ∀t. LENGTH((TL o j)t) = SUC n

Formulae (33), (37), (38) and (39) can be used to derive:

40 ∀carryin.

   REC_ADDER
   (SUC n)
   ((λx. MAP LIFT(TL(i x))),(λx. MAP LIFT(TL(j x))),(λx. LIFT(carryin x))) =
   N_BIT_ADDER
   (LIFT(SUC n))
   ((MAP LIFT) o (TL o i),(MAP LIFT) o (TL o j),LIFT o carryin)

The exact form of this statement is the most appropriate for use later in the mechanical proof, but it could just as easily have been expressed with all function composition symbols eliminated, or none eliminated. The statement is the induction hypothesis required later.

The following consequences of the assumptions are also useful:

41

  ∀t. LENGTH(MAP LIFT(i t)) = SUC(SUC n)
  ∀t. LENGTH(MAP LIFT(j t)) = SUC(SUC n)
  ∀t. LENGTH(MAP LIFT((TL o i)t)) = SUC n
  ∀t. LENGTH(MAP LIFT((TL o j)t)) = SUC n
  ∀t. ¬NULL(i t)
  ∀t. ¬NULL(j t)
  ∀t. ¬NULL(TL(i t))
  ∀t. ¬NULL(TL(j t))
  ∀t. ¬NULL(MAP LIFT(i t))
  ∀t. ¬NULL(MAP LIFT(j t))
  ∀t. ¬NULL(MAP LIFT(TL(i t)))
  ∀t. ¬NULL(MAP LIFT(TL(j t)))

Finally, the following theorem, which is not a consequence of the assumptions is used several times to justify manipulations in the main part of the proof:

42

  ⊢ ∀m. EVERY(λn. 0 < n)(1 UPTO m)

This says that every element of the list [1;2;...;m] is greater than zero.

3.3.3 Using the Induction Hypothesis

The consequent of the step case is now manipulated so that the induction hypothesis can be used. First the application of REC_ADDER is opened up using (32). After some simplification the result is:

N_BIT_ADDER
(LIFT(SUC(SUC n)))
((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
(εOUTPUT.
  ∃oneadd.
   (oneadd =
    FULL_ADDER
    ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),(λx. LIFT(carryin x)))) ∧
   (OUTPUT =
    (λt.
      (εOUTPUT'.
        ∃recadder.
         (recadder =
          REC_ADDER
          (SUC n)
          ((λt'. MAP LIFT(TL(i t'))),(λt'. MAP LIFT(TL(j t'))),
           (λt''. SND(oneadd t'')))) ∧
         (OUTPUT' =
          (λt''.
            (CONS(FST(oneadd t''))(FST(recadder t'')),SND(recadder t'')))))
      t)))

Unwinding oneadd produces a right-hand side of the form:

εOUTPUT. OUTPUT = ...

which can be simplified using the lemma:

43 ⊢ ∀y. (εx. x = y) = y

The right-hand side now contains a recursive call of REC_ADDER of the form:

REC_ADDER
(SUC n)
((λt'. MAP LIFT(TL(i t'))),(λt'. MAP LIFT(TL(j t'))),
 (λt''.
   SND
   (FULL_ADDER
    ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
     (λx. LIFT(carryin x)))
    t'')))

The next step is to use the induction hypothesis (40), but it does not quite match the term above. The third component of the triple that forms the second argument to REC_ADDER needs to be of the form:

  λx. LIFT(carryin x)

but in fact it is:

  λt''.
    SND
    (FULL_ADDER
    ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
     (λx. LIFT(carryin x)))
    t'')

This is where lemma (6) about the definedness of FULL_ADDER is used. The term is transformed to:

  λt''.
   LIFT
   (UNLIFT
    (SND
     (FULL_ADDER
      ((λx. LIFT(HD(i x))),(λx. LIFT(HD(j x))),
       (λx. LIFT(carryin x)))
      t'')))

Since carryin is universally quantified in the induction hypothesis (40), this hypothesis can now be used. The application of it is a little delicate because it still doesn’t quite match the term, but the manipulations required are simple. The result is a recursive statement for N_BIT_ADDER:

  N_BIT_ADDER
  (LIFT(SUC(SUC n)))
  ((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
  (εOUTPUT'.
    ∃recadder.
     (recadder = N_BIT_ADDER (LIFT(SUC n)) (...)) ∧
     (OUTPUT' = ...))

It is not wise to unwind recadder at this point because it occurs twice in the righthand side of the equation for OUTPUT'. Instead the proof proceeds by opening up both occurrences of N_BIT_ADDER using (24). Note that N_BIT_ADDER does not have a recursive definition, so the induction hypothesis has been used to eliminate the recursive references. The definedness lemma (6) can now be used in reverse to simplify the term. However, in the mechanical proof this step is delayed until after the opening-up of N_BIT_ADDER because it simplifies the proof. After doing these things, the conjecture left to prove is:

(εOUTPUT.
∃fulladd.
(∀t. LENGTH(fulladd t) = SUC(SUC n)) ∧
(∀t.
fulladd t =
MAP
(λx.
FULL_ADDER
((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
 (λt'.
   EL'
   x
   (CONS
    (LIFT(carryin t'))
    (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO (SUC n))))))
t)
(1 UPTO (SUC(SUC n)))) ∧
(OUTPUT =
(λt. (MAP FST(fulladd t),SND(EL'(SUC(SUC n))(fulladd t)))))) =
(εOUTPUT'.
∃recadder.
(recadder =
(εOUTPUT.
∃fulladd.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(∀t.
  fulladd t =
  MAP
  (λx.
    FULL_ADDER
    ((λt'. EL' x(MAP LIFT(TL(i t')))),
     (λt'. EL' x(MAP LIFT(TL(j t')))),
     (λt'.
       EL'
       x
       (CONS
        (SND
         (FULL_ADDER
          ((λx. LIFT(HD(i x))),(λx. LIFT(HD(j x))),
           (λx. LIFT(carryin x)))
          t'))
        (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO n)))))
    t)
  (1 UPTO (SUC n))) ∧
(OUTPUT = (λt. (MAP FST(fulladd t),SND(EL'(SUC n)(fulladd t))))))) ∧
(OUTPUT' =
(λt''.
(CONS
(FST
 (FULL_ADDER
  ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
   (λx. LIFT(carryin x)))
  t''))
(FST(recadder t'')),SND(recadder t'')))))

3.3.4 Splitting the Internal Bus

Both sides of the equation involve an internal variable called fulladd. These represent the outputs from the adders. However, the one on the left-hand side is one element wider than the one on the right. So, to prove the equivalence it is necessary to split the (n + 2)-element fulladd appearing in the left-hand side into a singleelement output and an (n+1)-element output. This is achieved by first splitting the (1 UPTO (SUC(SUC n))) that appears in the left-hand side. The following lemma is used:

44

  ⊢ ∀m n. m ≤ n ⟹ (m UPTO n = CONS m((SUC m) UPTO n))

It is applicable because of the theorem:

  45 ⊢ 1 ≤ (SUC(SUC n))

The following subterm is obtained within the left-hand side:

  MAP
  (λx.
    FULL_ADDER
    ((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
     (λt'.
       EL'
       x
       (CONS
        (LIFT(carryin t'))
        (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO (SUC n))))))
    t)
  (CONS 1((SUC 1) UPTO (SUC(SUC n))))

Using the lemmas:

46

  ∀f h t. MAP f(CONS h t) = CONS(f h)(MAP f t)

47

  ⊢ ∀m n. (SUC m) UPTO (SUC n) = MAP SUC(m UPTO n)

the term becomes:

CONS
(FULL_ADDER
 ((λt'. EL' 1(MAP LIFT(i t'))),(λt'. EL' 1(MAP LIFT(j t'))),
  (λt'.
    EL'
    1
    (CONS
     (LIFT(carryin t'))
     (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO (SUC n))))))
 t)
(MAP
 (λx.
   FULL_ADDER
   ((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
    (λt'.
      EL'
      x
      (CONS
       (LIFT(carryin t'))
       (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO (SUC n))))))
   t)
 (MAP SUC(1 UPTO (SUC n))))

This term represents a list. The head of the list can be simplified to:

FULL_ADDER
((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
 (λt'. LIFT(carryin t')))
t

using the fact that (El' 1) applied to a list is the first element of the list, i.e., its head, and the following lemma:

48

⊢ ∀f l. ¬NULL l ⟹ (HD(MAP f l) = f(HD l))

which is applicable because of assumptions (41) generated earlier.

The rest of the list can be simplified by moving the first SUC occurring in:

MAP SUC(1 UPTO (SUC n))

into the function that is being mapped over this list. This can be done using lemma (21):

⊢ ∀f g l. MAP f(MAP g l) = MAP(f o g)l

where g becomes instantiated to the SUC that is to be moved inside the function. So, (f o g) is:

(λx.
FULL_ADDER
((λt'. EL' x(MAP LIFT(i t'))),(λt'. EL' x(MAP LIFT(j t'))),
(λt'.
  EL'
  x
  (CONS
   (LIFT(carryin t'))
   (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO (SUC n))))))
t) o
SUC

By the definition of function composition the list becomes:

MAP
(λx.
FULL_ADDER
((λt'. EL'(SUC x)(MAP LIFT(i t'))),
(λt'. EL'(SUC x)(MAP LIFT(j t'))),
(λt'.
  EL'
  (SUC x)
  (CONS
   (LIFT(carryin t'))
   (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO (SUC n))))))
t)
(1 UPTO (SUC n))

which can be simplified further using the lemmas:

49 ⊢ ∀l f g.

EVERY(λn. 0 < n)l ∧ (∀t. ¬NULL(g t)) ⟹
(MAP(λn. f n(λt. EL'(SUC n)(g t)))l =
 MAP(λn. f n(λt. EL' n(TL(g t))))l)

50 ⊢ ∀l l' h' f.

EVERY(λn. 0 < n)l ⟹
(MAP(λn. f n(λt. EL'(SUC n)(CONS(h' t)(l' t))))l =
 MAP(λn. f n(λt. EL' n(l' t)))l)

The assumptions (41) and (42) generated earlier and the higher-order rewriting facility described in Section 4.3 are required in order to apply these lemmas. The lemma:

51

⊢ ∀f l. ¬NULL l ⟹ (TL(MAP f l) = MAP f(TL l))

can then be used to give the following term:

MAP
(λx.
FULL_ADDER
((λt'. EL' x(MAP LIFT(TL(i t')))),
 (λt'. EL' x(MAP LIFT(TL(j t')))),
 (λt'. EL' x(MAP(λm. SND(EL' m(fulladd t')))(1 UPTO (SUC n)))))
t)
(1 UPTO (SUC n))

The inner (1 UPTO (SUC n)) can now be split in a similar way to the above to give the following term:

MAP
(λx.
FULL_ADDER
((λt'. EL' x(MAP LIFT(TL(i t')))),
 (λt'. EL' x(MAP LIFT(TL(j t')))),
 (λt'.
   EL'
   x
   (CONS
    (SND(EL' 1(fulladd t')))
    (MAP(λx. SND(EL'(SUC x)(fulladd t')))(1 UPTO n)))))
t)
(1 UPTO (SUC n))

It is now possible to split fulladd. The left-hand side of the formula to be proved looks like this:

εOUTPUT.
∃fulladd.
(∀t. LENGTH(fulladd t) = SUC(SUC n)) ∧
(∀t. fulladd t = CONS (...) (...)) ∧
(OUTPUT = (λt. (MAP FST(fulladd t),SND(EL'(SUC(SUC n))(fulladd t)))))

fulladd is split using the following lemma:

52 ⊢ ∀n P.

 (∃f. (∀t. LENGTH(f t) = SUC n) ∧ P f) =
 (∃g h. (∀t. LENGTH(g t) = n) ∧ P(λt. CONS(h t)(g t)))

The higher-order rewriting tools (Section 4.3) have to be used to apply this lemma to the term above. The result after beta-reduction is:

εOUTPUT.
∃fulladd h.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(∀t.
  CONS(h t)(fulladd t) =
  CONS
  (FULL_ADDER
   ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
    (λt'. LIFT(carryin t')))
   t)
  (MAP
   (λx.
     FULL_ADDER
     ((λt'. EL' x(MAP LIFT(TL(i t')))),
      (λt'. EL' x(MAP LIFT(TL(j t')))),
      (λt'.
        EL'
        x
        (CONS
         (SND(EL' 1(CONS(h t')(fulladd t'))))
         (MAP
          (λx'. SND(EL'(SUC x')(CONS(h t')(fulladd t'))))
          (1 UPTO n)))))
     t)
   (1 UPTO (SUC n)))) ∧
(OUTPUT =
 (λt.
   (MAP FST(CONS(h t)(fulladd t)),
    SND(EL'(SUC(SUC n))(CONS(h t)(fulladd t))))))

fulladd is now one element narrower than it used to be, and h represents the element that has been broken off. The lemma:

53

⊢ ∀h f h' f'. (CONS h f = CONS h' f') = (h = h') ∧ (f = f')

can now be used to obtain separate equations for h and fulladd:

εOUTPUT.
∃fulladd h.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(∀t. (h t = ...) ∧ (fulladd t = ...)) ∧
(OUTPUT = ...)

Rearrangement of the conjunction permits substitution for h in the other conjuncts. The result of doing this is:

εOUTPUT.
∃fulladd.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(∀t.
fulladd t =
MAP
(λx.
FULL_ADDER
((λt'. EL' x(MAP LIFT(TL(i t')))),(λt'. EL' x(MAP LIFT(TL(j t')))),
 (λt'.
   EL'
   x
   (CONS
    (SND
     (EL'
      1
      (CONS
       (FULL_ADDER
        ((λt''. LIFT(HD(i t''))),(λt''. LIFT(HD(j t''))),
         (λt''. LIFT(carryin t'')))
        t')
       (fulladd t'))))
    (MAP
     (λx'.
       SND
       (EL'
        (SUC x')
        (CONS
         (FULL_ADDER
          ((λt''. LIFT(HD(i t''))),(λt''. LIFT(HD(j t''))),
           (λt''. LIFT(carryin t'')))
          t')
         (fulladd t'))))
     (1 UPTO n)))))
t)
(1 UPTO (SUC n))) ∧
(OUTPUT =
(λt.
(MAP
FST
(CONS
 (FULL_ADDER
  ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),(λt'. LIFT(carryin t')))
  t)
 (fulladd t)),
SND
(EL'
 (SUC(SUC n))
 (CONS
  (FULL_ADDER
   ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),(λt'. LIFT(carryin t')))
   t)
  (fulladd t))))))

The term can be simplified using lemma (46) together with the following lemmas:

54

⊢ ∀h l. EL' 1(CONS h l) = h

55 ⊢ ∀l l' h' f.

EVERY(λn. 0 < n)l ⟹
(MAP(λn. f n(EL'(SUC n)(CONS h' l')))l = MAP(λn. f n(EL' n l'))l)

56

⊢ EL'(SUC(SUC n))(CONS h l) = EL'(SUC n)l

Lemma (55) is only applicable because of assumption (42), and if the higher-order rewriting tools are used.

3.3.5 Unwinding and Quantifier Elimination

Now that the left-hand side of the goal has been manipulated, the differences between it and the right-hand side are quite small. The entire goal (abbreviated) is:

(εOUTPUT.
∃fulladd.
(∀t. LENGTH(fulladd t) = SUC n) ∧
(...) ∧
(OUTPUT =
 (λt.
   (CONS
    (FST
     (FULL_ADDER
      ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
       (λt'. LIFT(carryin t')))
      t))
    (MAP FST(fulladd t)),SND(EL'(SUC n)(fulladd t)))))) =
(εOUTPUT'.
∃recadder.
(recadder =
 (εOUTPUT.
   ∃fulladd.
    (∀t. LENGTH(fulladd t) = SUC n) ∧
    (...) ∧
    (OUTPUT = (λt. (MAP FST(fulladd t),SND(EL'(SUC n)(fulladd t))))))) ∧
(OUTPUT' =
 (λt''.
   (CONS
    (FST
     (FULL_ADDER
      ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
       (λx. LIFT(carryin x)))
      t''))
    (FST(recadder t'')),SND(recadder t'')))))

where up to the renaming of bound variables, the two elided subterms are both:

∀t.
fulladd t =
MAP
(λx.
  FULL_ADDER
  ((λt'. EL' x(MAP LIFT(TL(i t')))),
   (λt'. EL' x(MAP LIFT(TL(j t')))),
   (λt'.
     EL'
     x
     (CONS
      (SND
       (FULL_ADDER
        ((λt''. LIFT(HD(i t''))),(λt''. LIFT(HD(j t''))),
         (λt''. LIFT(carryin t'')))
        t'))
      (MAP(λx'. SND(EL' x'(fulladd t')))(1 UPTO n)))))
  t)
(1 UPTO (SUC n))

The natural thing to do now is to unwind and eliminate the variable recadder that appears in the right-hand side of the equation. The right-hand side becomes:

εOUTPUT'.
OUTPUT' =
(λt''.
  (CONS
   (FST
    (FULL_ADDER
     ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),
      (λx. LIFT(carryin x)))
     t''))
   (FST
    ((εOUTPUT.
       ∃fulladd.
        (∀t. LENGTH(fulladd t) = SUC n) ∧
        (∀t. fulladd t = ...) ∧
        (OUTPUT = (λt. (MAP FST(fulladd t),SND(EL'(SUC n)(fulladd t))))))
     t'')),
   SND
   ((εOUTPUT.
      ∃fulladd.
       (∀t. LENGTH(fulladd t) = SUC n) ∧
       (∀t. fulladd t = ...) ∧
       (OUTPUT = (λt. (MAP FST(fulladd t),SND(EL'(SUC n)(fulladd t))))))
    t'')))

Lemma (43):

⊢ ∀y. (εx. x = y) = y

can now be used to eliminate OUTPUT'. It would be useful to eliminate OUTPUT from the left-hand side in a similar way, but unfortunately fulladd cannot be fully unwound because it is specified by a recursive equation. However, the following lemma:

57

⊢ ∀f g. (∃! x. f x) ⟹ ((∃x. f x ∧ (y = g x)) = (y = g(εx. f x)))

can be used to transform the left-hand side into:

εOUTPUT.
OUTPUT =
(λt.
(CONS
 (FST
  (FULL_ADDER
   ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),(λt'. LIFT(carryin t')))
   t))
 (MAP FST ((εx. (∀t'. LENGTH(x t') = SUC n) ∧ (∀t''. x t'' = ...)) t)),
 SND
 (EL'
  (SUC n)
  ((εx. (∀t'. LENGTH(x t') = SUC n) ∧ (∀t''. x t'' = ...)) t))))

In order to apply lemma (57) the following unique-existence property of fulladd has to be proved:

58

⊢ ∀n i j carryin.
VALID_ELLA_INTEGER(Int_of_num(SUC(SUC n))) ∧
(∀t. LENGTH(i t) = SUC(SUC n)) ∧
(∀t. LENGTH(j t) = SUC(SUC n)) ⟹
(∃! fulladd.
  (∀t. LENGTH(fulladd t) = SUC n) ∧
  (∀t.
    fulladd t =
    MAP
    (λx.
      FULL_ADDER
      ((λt'. EL' x(MAP LIFT(TL(i t')))),
       (λt'. EL' x(MAP LIFT(TL(j t')))),
       (λt'.
         EL'
         x
         (CONS
          (SND
           (FULL_ADDER
            ((λx'. LIFT(HD(i x'))),(λx'. LIFT(HD(j x'))),
             (λx'. LIFT(carryin x')))
            t'))
          (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO n)))))
      t)
    (1 UPTO (SUC n))))

The hypotheses of this lemma can be satisfied using assumptions (34), (35) and (36). The proof of lemma (58) is discussed in Section 3.4.

Having transformed the left-hand side, OUTPUT can be eliminated. The final step of the proof is to make use of lemma (57) again, this time in the right-hand side. The occurrences of the epsilon operator within the right-hand side need to be moved deeper into the terms so that the functions FST and SND can be applied to the pair:

  (MAP FST(fulladd t),SND(EL'(SUC n)(fulladd t)))

Lemmas (57) and (43) achieve this. After beta-reduction the new right-hand side is:

  λt''.
   (CONS
    (FST
     (FULL_ADDER
      ((λt'. LIFT(HD(i t'))),(λt'. LIFT(HD(j t'))),(λx. LIFT(carryin x)))
      t''))
    (FST
     (MAP FST ((εx. (∀t'. LENGTH(x t') = SUC n) ∧ (∀t'''. x t''' = ...)) t''),
      SND
      (EL'
       (SUC n)
       ((εx. (∀t'. LENGTH(x t') = SUC n) ∧ (∀t'''. x t''' = ...)) t'')))),
    SND
    (MAP FST ((εx. (∀t'. LENGTH(x t') = SUC n) ∧ (∀t'''. x t''' = ...)) t''),
     SND
     (EL'
      (SUC n)
      ((εx. (∀t'. LENGTH(x t') = SUC n) ∧ (∀t'''. x t''' = ...)) t''))))

Note that fulladd has been replaced by the epsilon term that satisfies its recursive specification. Application of the lemmas:

59

  ⊢ ∀x y. FST(x,y) = x

60

  ⊢ ∀x y. SND(x,y) = y

results in a term which, up to renaming of bound variables, is equivalent to the left-hand side of the conjecture. This completes the proof.

3.4 A Unique-Existence Lemma

The proof of equivalence of the n-bit adders relies on lemma (58). Roughly, this states that the values on the internal lines and outputs of the parallel adder are uniquely defined by the recursive specification, i.e., the recursive specification has a solution and the solution is unique. The proof of the lemma is by induction on the number of bits.

3.4.1 Base Case of Induction

The base case of the induction is:

∀i j carryin.
VALID_ELLA_INTEGER(Int_of_num(SUC(SUC 0))) ∧
(∀t. LENGTH(i t) = SUC(SUC 0)) ∧
(∀t. LENGTH(j t) = SUC(SUC 0)) ⟹
(∃! fulladd.
  (∀t. LENGTH(fulladd t) = SUC 0) ∧
  (∀t.
    fulladd t =
    MAP
    (λx.
      FULL_ADDER
      ((λt'. EL' x(MAP LIFT(TL(i t')))),
       (λt'. EL' x(MAP LIFT(TL(j t')))),
       (λt'.
         EL'
         x
         (CONS
          (SND
           (FULL_ADDER
            ((λx'. LIFT(HD(i x'))),(λx'. LIFT(HD(j x'))),
             (λx'. LIFT(carryin x')))
            t'))
          (MAP(λm. SND(EL' m(fulladd t')))(1 UPTO 0)))))
      t)
    (1 UPTO (SUC 0))))

After some straightforward simplifications, the conclusion of the base case becomes:

∃! fulladd.
(∀t. LENGTH(fulladd t) = SUC 0) ∧
(∀t.
  fulladd t =
  [FULL_ADDER
   ((λt'. HD(MAP LIFT(TL(i t')))),(λt'. HD(MAP LIFT(TL(j t')))),
    (λt'.
      SND
      (FULL_ADDER
       ((λx'. LIFT(HD(i x'))),(λx'. LIFT(HD(j x'))),
        (λx'. LIFT(carryin x')))
       t')))
   t])"

The existence of such a fulladd can be proved by exhibiting the following term as a witness:

λt. [FULL_ADDER
((λt'. HD(MAP LIFT(TL(i t')))),(λt'. HD(MAP LIFT(TL(j t')))),
(λt'.
SND
(FULL_ADDER
 ((λx'. LIFT(HD(i x'))),(λx'. LIFT(HD(j x'))),
  (λx'. LIFT(carryin x')))
 t')))
t]

This leaves the proof of uniqueness to be done:

∀fulladd fulladd'.
((∀t. LENGTH(fulladd t) = SUC 0) ∧
(∀t.
fulladd t =
[FULL_ADDER
((λt'. HD(MAP LIFT(TL(i t')))),(λt'. HD(MAP LIFT(TL(j t')))),
(λt'.
SND
(FULL_ADDER
 ((λx'. LIFT(HD(i x'))),(λx'. LIFT(HD(j x'))),
  (λx'. LIFT(carryin x')))
 t')))
t])) ∧
(∀t. LENGTH(fulladd' t) = SUC 0) ∧
(∀t.
fulladd' t =
[FULL_ADDER
((λt'. HD(MAP LIFT(TL(i t')))),(λt'. HD(MAP LIFT(TL(j t')))),
(λt'.
SND
(FULL_ADDER
((λx'. LIFT(HD(i x'))),(λx'. LIFT(HD(j x'))),
 (λx'. LIFT(carryin x')))
t')))
t]) ⟹
(fulladd = fulladd')

Since the equations for fulladd and fulladd' are not recursive and the right-hand sides are the same for both, it is easy to prove that (fulladd = fulladd'). This concludes the proof of the base case.

3.4.2 Step Case of Induction

The initial part of the proof of the step case follows closely parts of the proof of the main equivalence theorem as described in Section 3.3. First, useful assumptions are generated from the induction hypothesis and the other initial assumptions. The term is then prepared for a splitting of fulladd. The result of this process is:

  ∃! fulladd.
   (∀t. LENGTH(fulladd t) = SUC(SUC n)) ∧
   (∀t.
     fulladd t =
     CONS
     (FULL_ADDER
      ((λt'. LIFT(HD(TL(i t')))),(λt'. LIFT(HD(TL(j t')))),
       (λt'.
         SND
         (FULL_ADDER
          ((λx'. LIFT(HD(i x'))),(λx'. LIFT(HD(j x'))),
           (λx'. LIFT(carryin x')))
          t')))
      t)
     (MAP
      (λx.
        FULL_ADDER
        ((λt'. EL' x(MAP LIFT(TL(TL(i t'))))),
         (λt'. EL' x(MAP LIFT(TL(TL(j t'))))),
         (λt'.
           EL'
           x
           (CONS
            (SND(EL' 1(fulladd t')))
            (MAP(λx. SND(EL'(SUC x)(fulladd t')))(1 UPTO n)))))
        t)
      (1 UPTO (SUC n))))

Before the conjecture is separated into two cases, one for existence and one for uniqueness, some delicate manipulations are performed on it to make it easy for the induction hypothesis to be applied later. First, the definedness lemma (6) for FULL_ADDER is used. Then (TL(i t')) is converted into ((TL o i)t') and similarly for j. The i and j in the term to be proved are of size SUC(SUC(SUC n)). The i and j in the induction hypothesis are of size SUC(SUC n), but they are also universally quantified. Hence they can be instantiated to the (TL o i) and (TL o j) of the term to be proved. This works because these (TL o i) and (TL o j) are of size SUC(SUC n) as required by the induction hypothesis. So the term to be proved becomes:

∃! fulladd.
(∀t. LENGTH(fulladd t) = SUC(SUC n)) ∧
(∀t.
fulladd t =
CONS
(FULL_ADDER
 ((λt'. LIFT(HD((TL o i)t'))),(λt'. LIFT(HD((TL o j)t'))),
  (λt'.
    LIFT
    ((UNLIFT o
      (SND o
       (FULL_ADDER
        ((λx. LIFT(HD(i x))),(λx. LIFT(HD(j x))),
         (λx. LIFT(carryin x))))))
     t')))
 t)
(MAP
 (λx.
   FULL_ADDER
   ((λt'. EL' x(MAP LIFT(TL((TL o i)t')))),
    (λt'. EL' x(MAP LIFT(TL((TL o j)t')))),
    (λt'.
      EL'
      x
      (CONS
       (SND(EL' 1(fulladd t')))
       (MAP(λx. SND(EL'(SUC x)(fulladd t')))(1 UPTO n)))))
   t)
 (1 UPTO (SUC n))))

This is separated into the existence and uniqueness cases. The following lemmas are then used to split fulladd:

⊢ ∀n P.
(∃f. (∀t. LENGTH(f t) = SUC n) ∧ P f) =
(∃g h. (∀t. LENGTH(g t) = n) ∧ P(λt. CONS(h t)(g t)))

61 ⊢ ∀n P.

(∀f1 f2.
  ((∀t. LENGTH(f1 t) = SUC n) ∧ P f1) ∧
  ((∀t. LENGTH(f2 t) = SUC n) ∧ P f2) ⟹
  (f1 = f2)) =
(∀g1 h1 g2 h2.
  ((∀t. LENGTH(g1 t) = n) ∧ P(λt. CONS(h1 t)(g1 t))) ∧
  ((∀t. LENGTH(g2 t) = n) ∧ P(λt. CONS(h2 t)(g2 t))) ⟹
  (g1 = g2) ∧ (h1 = h2))

The first of these lemmas is also used in the proof of the main theorem. It is lemma (52). The proofs of lemmas (52) and (61) are not trivial. However, they will not be described here.

More manipulations similar to those used in the proof of the main equivalence theorem in Section 3.3, together with use of the induction hypothesis completes the proof of each of the two cases.

3.5 Summary of Proof

In the preceding sections a proof of equivalence of two n-bit adder implementations has been described. Both adders were specified in the ELLA language:

  MAC N_BIT_ADDER = ([INT n]tri: i j, tri: carryin) -> ([n]tri, tri):
   BEGIN
      MAKE [n]FULL_ADDER: fulladd.
      LET carry = carryin CONC ([INT k=1..n-1]fulladd[k][2]).
      FOR INT k=1..n JOIN (i[k], j[k], carry[k]) -> fulladd[k].
   OUTPUT ([INT k=1..n]fulladd[k][1], fulladd[n][2])
   END.

  MAC REC_ADDER {INT n} = ([n]tri: i j, tri: carryin) -> ([n]tri, tri):
   (LET oneadd = FULL_ADDER(i[1], j[1], carryin).
    OUTPUT IF n=1
           THEN ([1]oneadd[1], oneadd[2])
           ELSE (LET recadder =
                  REC_ADDER{n-1}(i[2..n], j[2..n], oneadd[2]).
                 OUTPUT (oneadd[1] CONC recadder[1], recadder[2]))
           FI).

These texts were automatically translated into HOL formulae which have a close correspondence with the abstract syntax trees for the texts. The formulae were then shown to be equivalent (under certain assumptions) using the HOL proof generating system:

  ⊢ ∀n i j carryin.
     VALID_ELLA_INTEGER(Int_of_num(SUC n)) ∧
     (∀t. LENGTH(i t) = SUC n) ∧
     (∀t. LENGTH(j t) = SUC n) ⟹
     (N_BIT_ADDER(LIFT(SUC n))((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin) =
      REC_ADDER(SUC n)((MAP LIFT) o i,(MAP LIFT) o j,LIFT o carryin))

This equivalence is relative to the semantics given to the subset of the ELLA language. The proof is of interest in two respects. First, it can be considered in some sense to be a proof of equivalence of the two original ELLA texts under the semantics. Since the adders were expected to be equivalent, the proof provides evidence that the semantics accurately captures the intended meaning of the ELLA constructs used. Second, the proof gives some indication of the difficulty of producing proofs for terms that have been automatically generated from hardware description language source code. It is not particularly difficult to outline the proof on paper, but due to the size and complexity of the terms, the soundness of a full hand-proof would have to be questioned. Mechanisation in a secure theorem prover solves this problem, but a great deal of work is required to do the proof in such a framework.

4 Proof Tools

The semantic embedding of the ELLA language within higher-order logic generated a need for proof tools that were not available in the basic HOL system. Some of these are specific to the ELLA language. Others are related to the use within the semantics of particular combinations of logical constructs not normally exploited in HOL. In this section the more significant of these tools are described.

4.1 Automatic Elimination of Semantic Constants

In order to prove that an ELLA description meets some formal specification written directly in higher-order logic, the term representing the description must be transformed into a form which can more easily be reasoned about. In particular, it is helpful to expand the logical constants used to capture the abstract syntax and the semantics of ELLA constructs. This can be done by rewriting with the definitions of these semantic constants.

The constants can be expanded by manual application of the definitions. However, this is tedious, and when definitions are recursive, can involve multiple applications of a definition. The process could be automated by repeatedly rewriting with all the definitions until no further changes take place. However, this is highly inefficient. Instead, the syntax of the language can be exploited to guide the application of the definitions. This is possible because the term representing the ELLA text is machine-generated. It therefore has a predictable form, and more significantly the form corresponds closely to the grammar of the ELLA language. Simplification procedures can be written which recurse in the same way as the productions of the grammar. This is much more efficient than using brute-force rewriting with all of the definitions.

An application of one of the semantic constants in the logic denotes the meaning of the ELLA construct to which the constant corresponds. The arguments of the application represent the sub-constructs. A simple example from the ELLA subset is the constant CONC which concatenates two time-varying ‘buses’. Here is its definition:

  ⊢ ∀l1 l2 t. (l1 CONC l2) t = APPEND (l1 t) (l2 t)

An example of the use of this construct appears in the definition of N_BIT_ADDER in Section 3:

  carryin CONC [INT k = 1..(n - 1)]fulladd[k][2]

For this ELLA text, the following HOL term is generated:

  (λt'. [carryin t']) CONC
  (VAR_REP
   (LIFT #00000000000000000000000000000001)
   (n EMINUS (LIFT #00000000000000000000000000000001))
   (λk. INDEX_MULT(INDEX fulladd k)(λ(x1',x2'). x2')))

The constant elimination procedure is built from procedures for each construct by first combining them into procedures for each syntactic category in the ELLA subset, and then combining those to make the main procedure. The procedure for an individual construct will apply the definition of the corresponding semantic constant. It may also do further simplification if this is possible.

In the example, CONC is in the syntactic category unit, so the elimination procedure will be in the sub-procedure for unit when it encounters the term above. The sub-procedure will examine the top-level function application to determine the name of the constant being applied. In this case, the constant is CONC. The sub-procedure for unit will then call the basic procedure for expanding CONC. The procedure for CONC applies the definition to give the term:

  λt. APPEND
      ((λt'. [carryin t']) t)
      (VAR_REP
       (LIFT #00000000000000000000000000000001)
       (n EMINUS (LIFT #00000000000000000000000000000001))
       (λk. INDEX_MULT(INDEX fulladd k)(λ(x1',x2'). x2'))
       t)

The procedure is also aware that some beta-reduction may be possible, as is the case for the first argument to APPEND in the example above. It will perform the beta-reduction and then make calls to other elimination procedures for the two subconstructs. The first of these is in syntactic category unit and the second is in the category unit1. The procedures for these categories will be called directly on the subterms. This avoids testing for semantic constants which couldn’t be the toplevel constant in the subterm because of syntactic restrictions. So, the elimination procedures know about the syntax of the language and exploit this to gain efficiency.

There is a potential problem with this approach. Suppose the syntax is mutually recursive as is the case for the ELLA subset. The following ‘loop’ occurs in the grammar:

unit → unit1 → unit2 → unit3 → unit

Now, if the procedure for one of these syntactic categories calls the procedure for the next category in the chain before considering a non-recursive case, the procedures may loop. This kind of looping can happen in the elimination procedures even when it cannot in the translator. This is because in the syntax there may be parentheses that have to be consumed before recursing, but in the logical term there may be nothing corresponding to the parentheses.

Looping can be prevented by passing a flag around the mutually recursive procedures. The flag is set to false on entering the procedures and at some point in the ‘loop’ the flag is tested. If it is true, the non-recursive possibilities are investigated. Otherwise the flag is set to true and recursion continues. If the execution reaches this point again, the flag will be true and so no further looping will occur. This prevents the procedures from going around the ‘loop’ two or more times on the same term.

4.2 Rewriting Using Theorems with Assumptions

Many of the simplifications used in Section 3.2 require the use of conditional rewrite rules. For example, some assume that a numeric variable is a valid ELLA integer:

  ⊢ ∀n.
     VALID_ELLA_INTEGER(Int_of_num n) ⟹
     (UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num n))) = n)

Such rules cannot normally be applied using the rewriting tactics of HOL because the assumptions have to be satisfied before the equation can be used. Resolution with the theorem above, followed by rewriting with the new assumptions so generated may work, but only if the hypotheses of this conditional rewrite rule can be satisfied directly by assumptions already present.

It can be very tedious to generate the assumptions required by performing forward proof starting from the existing assumptions. For this reason tactics and tacticals for HOL have been implemented that allow a theorem with assumptions to be used directly as a rewrite rule. The assumptions become instantiated when the equation is used, and are set up as new subgoals for the user to prove. They can then be proved by backward proof from the existing assumptions of the goal. This is usually a lot easier than trying to generate the required assumptions by forward proof.

Unfortunately it is not always valid to bring the instantiated hypotheses of the conditional rewrite rule to the top level as new subgoals. Consider the following goal:

  "MAP
   (λx'. UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num x'))))
   (1 UPTO x) =
   1 UPTO x"
      [ "VALID_ELLA_INTEGER(Int_of_num x)" ]

where the term in square brackets is an assumption and (1 UPTO x) denotes the list [1;2;...;x]. It can be deduced that all the elements in this list are valid ELLA integers because there is an assumption stating that x is a valid ELLA integer. It would be convenient to be able to use the conditional rewrite rule given above to rewrite the function:

  (λx'. UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num x'))))

to the identity function (λx'. x'). However the hypothesis of the conditional rewrite rule becomes instantiated to:

  VALID_ELLA_INTEGER(Int_of_num x')

Note that this term contains the variable x', so it cannot be set up as a new subgoal at top level because that would be taking x' out of its scope. The only solution is to prove and use a different rewrite rule, e.g.:

  ⊢ ∀n.
     VALID_ELLA_INTEGER(Int_of_num n) ⟹
     (MAP
      (λm. UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num m))))
      (1 UPTO n) =
      (1 UPTO n))

This rule is of course the theorem to be proved, so the proof will have to be more fundamental, but once this theorem has been proved ‘by hand’ it can be applied as a rewrite rule deep within another term.

The reason for the discussion concerning the problem of instantiated hypotheses being passed out of scope is that (as now explained) they cause the rewrite to fail on a larger subterm of the goal than is necessary. The failure occurs when the procedure tries to construct an equality between the original lambda-abstraction:

  (λx'. UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num x'))))

and the new abstraction:

  (λx'. x')

The theorem:

  VALID_ELLA_INTEGER (Int_of_num x') ⊢
     UNLIFT(LIFT_num_of_word32(UNLIFT(LIFT_word32_of_num x'))) = x'

has been generated successfully, but when the procedure attempts to apply the rule:

\frac{Γ ⊢ t[x] = t′[x]}{Γ ⊢ λx. t[x] = t′[x]}

failure occurs because this rule is only applicable if x does not appear free in Γ. In the example, the failure occurs immediately after the conditional rewrite rule is applied, but suppose that the lambda-abstraction contained another subterm not involving x' to which the rewrite rule was also applicable. This subterm could be successfully rewritten and the instantiated hypothesis taken to the top level, but because of the presence of the original subterm, the whole abstraction would be rejected.

The procedure needs to know that it should not try to apply the conditional rewrite to the subterm involving x' because x' is not free in the goal and the application will ultimately fail. By getting the procedure to ignore the bad subterm it can go on to successfully apply the rewrite rule to the other subterm. This is achieved by providing the procedure with extra information, namely a list of bound variables. Whenever the procedure goes inside a lambda-abstraction the bound variable is added to the list. When the procedure comes to apply a conditional rewrite rule it fails immediately if any of the bound variables in its list appear free in the instantiated hypotheses.

The situation described of having two subterms within an abstraction, one of which can be successfully rewritten by the conditional rewrite rule and one that cannot, may seem to be a bit unlikely in practice. In fact, an example of this occurs in the proof described in Section 3.

When the procedure is about to set up an instantiated hypothesis as a new subgoal, it first checks to see whether it can be immediately satisfied by existing assumptions. If it can, the procedure proves the instantiated hypothesis without presenting it to the user. In addition, when the hypothesis has to be given to the user to prove, it is added to the list of assumptions in the main subgoal so that if the same instantiated hypothesis is generated again later in the proof the user will not have to justify it all over again. Together these two properties make the system convenient to use. A further enhancement would be to process the instantiated hypothesis before setting it up as a new subgoal. It might, for example, be a conjunction of two existing assumptions, so by splitting the conjunction it could be satisfied immediately without having to give it to the user to prove.

4.3 Restricted Higher-Order Matching

The proof described in Section 3 involves some delicate manipulations and many of the simplifications used are highly context-dependent. In their most general form many of the simplification theorems cannot be applied by first-order rewriting; they require higher-order matching. The theorems can be instantiated by hand to make them applicable by simple first-order rewriting, but due to the complexity of the theorems and of the terms being simplified, it is very time-consuming to do this. So, to make the proof feasible a tool for instantiating the theorems automatically has been implemented. This performs a restricted form of higher-order matching.

Consider the following HOL term:

  MAP (λn. (EL ((n-1)+1) l) + 2) (1 UPTO ((LENGTH l) - 1))

where l is a list and EL is a function such that (EL 0 l) returns the head (first element) of l, (EL 1 l) returns the second element, and so on. UPTO is an infix function such that (UPTO m n) returns the list [m;m+1;...;n-1;n]. If n is less than m then (UPTO m n) returns an empty list.

The above term ‘evaluates’ to the tail of the list l with 2 added to every element. If l is an empty list, the result is an empty list. Now suppose the term is to be transformed to:

  MAP (λn. (EL n l) + 2) (1 UPTO ((LENGTH l) - 1))

For natural numbers it is not in general true that ((n − 1) + 1) is n, for if n is 0, then (n − 1) is 0, and so ((n − 1) + 1) is 1. So, for the transformation to be valid it must be possible to show that n cannot be zero. This is the case, because for the arguments in the example, the result of applying UPTO cannot yield a list containing zero as an element. However, the equation (n − 1) + 1 = n cannot be used for rewriting because it is not a theorem. The following can be proved:

  ⊢ MAP (λn. f ((n-1)+1)) (1 UPTO m) = MAP (λn. f n) (1 UPTO m)

It would suffice to prove the specific theorem required for the example, but a large number of similar theorems might have to be proved. It is better to have the general theorem above. However, the example cannot be rewritten with this theorem because f((n-1)+1) does not match (EL ((n-1)+1) l) + 2. The theorem can be specialised though. Instantiating f to (λx. (EL x l) + 2) and m to (LENGTH l) - 1, the following theorem is obtained:

  ⊢ MAP (λn. (λx. (EL x l) + 2) ((n-1)+1)) (1 UPTO ((LENGTH l) - 1)) =
    MAP (λn. (λx. (EL x l) + 2) n) (1 UPTO ((LENGTH l) - 1))

Beta-reduction yields a theorem for the required transformation:

  ⊢ MAP (λn. (EL ((n-1)+1) l) + 2) (1 UPTO ((LENGTH l) - 1)) =
    MAP (λn. (EL n l) + 2) (1 UPTO ((LENGTH l) - 1))

This is a fairly simple example. More generally, there may be more than one function variable being used as a higher-order pattern as f is above. Furthermore, the arguments to these function symbols may themselves contain applications of such function symbols. In fact, the nesting may be arbitrarily deep. Here is an example:

  ⊢ ∀l l' h' f g.
     EVERY (λn. 0 < n) l ⟹
     (MAP (λn. f (λt. g (EL' (SUC n) (CONS (h' t) (l' t))))) l =
      MAP (λn. f (λt. g (EL' n (l' t)))) l)

This theorem will match a term of the form:

  MAP
  (λn. ... (λt. ... (EL' (SUC n) (CONS (... t ...) (... t ...))) ...) ...)
  l

So all four of the variables f, g, h' and l' can act as higher-order patterns. The term above could not be matched with the theorem:

  ⊢ ∀l l' h' f.
     EVERY (λn. 0 < n) l ⟹
     (MAP (λn. f (EL' (SUC n) (CONS h' l'))) l = MAP (λn. f (EL' n l')) l)

because both h' and l' would become bound to terms containing the variable t. This would result in an attempt to pass t out of its scope. Hypothetically, the application of f would be matched to:

  (λx. ... (λt. ... x ...) ...) (EL' (SUC n) (CONS (... t ...) (... t ...)))

Observe that when this is beta-reduced, the occurrences of t in the argument are captured by the binding of t in the function. As a result, they have to be renamed leaving a term that is different from the one to be rewritten.

In addition to having multiple higher-order patterns, each function used in such a pattern may have more than one argument. This allows for multiple subterms that must be first-order matched. In particular, it is often necessary to have a bound variable appear as an extra argument to a function being used as a higher-order pattern. Extending the previous example in this way, the theorem becomes:

  ⊢ ∀l l' h' f g.
     EVERY (λn. 0 < n) l ⟹
     (MAP (λn. f n (λt. g (EL' (SUC n) (CONS (h' t) (l' t))))) l =
      MAP (λn. f n (λt. g (EL' n (l' t)))) l)

Note that f now has n (a bound variable) as an extra argument. This theorem can be used to match the term:

  MAP (λn. ... (λt. ... (EL' (SUC n) (CONS (h' t) (l' t))) ...) ... n ...) l

whereas the previous one couldn’t because the lone occurrence of n would get passed out of its scope. The extra argument to f effectively ‘mops up’ any occurrences of n which are not within a subterm matched by the other argument. Note that if the lone occurrence of n occurred inside the abstraction for t the function g would have to have the extra argument, rather than f.

5 Related Work

The work of Goossens [Goo91] is probably the most closely related to the work described in this paper. Goossens describes the embedding of a subset of ELLA in the Lambda proof system. The Lambda system supports a constructive higher order logic whereas the logic of the HOL system is classical. However, the biggest difference between Goossens work and the work described here is that the former is an operational semantics while the latter is denotational in style. In this respect the work of Goossens is closer to that of Van Tassel on embedding the hardware description language VHDL in the HOL system [Tas92]. Goossens has used his operational semantics to perform symbolic simulation of his ELLA subset. The work described here has been more oriented towards proving properties of ELLA texts.

Van Tassel’s work on VHDL is significantly different in many respects from the work described here. First, VHDL is very different from ELLA. Second, the thrust of Van Tassel’s work has been to formalise the VHDL simulation cycle. His semantics is operational, and the syntax of his VHDL subset is formalised within the logic, allowing general properties of the language to be proved.

Work on the semantics of ELLA has been taking place at Manchester and RSRE. The work at Manchester [BGL^{+}91] is for an abstraction of ELLA referred to as Boolean Kernel ELLA. A semantics for this language is given in terms of IO automata with automatic verification in mind. The work at RSRE is aimed at providing a formal semantics for the Core of ELLA, in the belief that the constructs of full ELLA can be transformed into constructs in the Core. The static semantics has already been formalised [MH91].

Other related work includes the embedding of a semantics for a subset of the synchronous hardware description language Silage in HOL [Gor], and the formal development of the language FUNNEL [SEA] which has much in common with ELLA. The semantics given to Silage is, like the semantics described here, denotational in style.

6 Conclusions

A proof of equivalence of two n-bit adder implementations under certain justified assumptions has been described. The proof is relative to a semantics for a subset of ELLA, and is by induction on n. In HOL the proof involves some very delicate manipulations and many of the simplifications are highly context-dependent. Due to the nature of these simplification theorems and the complexity of the terms being simplified, it is very time-consuming to instantiate the theorems by hand. So, to make the proof feasible a proof tool for instantiating the theorems automatically has been implemented.

The proof involved two months solid work for one person, but much of that time was spent proving lemmas and developing tools. A proof of similar complexity would, at a guess, take two or three weeks. To do the proof fully automatically the system would probably have to conjecture lemmas for higher-order rewriting. Perhaps the most difficult lemma to conjecture would be the unique-existence lemma. It is the presence of Hilbert’s epsilon operator in the semantics that produces this requirement for a unique-existence lemma. So the presence of the epsilon operator might make it reasonably clear to an automatic procedure that the lemma is required to complete the proof. Knowledge of appropriate lemmas about the epsilon operator might also help to make this apparent.

One thing to consider is whether the presence of lifting makes the need for unique-existence proofs more likely. The conclusion is that it does not, but lifting will make such proofs more difficult because proving a recursively specified function exists and is unique is more difficult when the definedness of one value depends on the definedness of the result of the recursive call.

Some questions that arise from the experience of doing the proof are:

• Would the adders be easier to specify in pure logic?

• Would the proof have been easier if ELLA rows had been modelled by functions rather than lists?

In answer to the first question: The logical representations of the implementations after translation from ELLA text are very complex. To write them by hand correctly would be very difficult. Descriptions written directly in logic would be much simpler, but probably no simpler than the ELLA texts.

The descriptions produced by the translator do not have the optimisations a person would make. This is not to say that optimisations could not be made, but it is part of the methodology not to do this. The translation should be as simple as possible because the translator is not verified. The aim is to have the optimisations performed by logical inference after translation. This means that the descriptions generated are more difficult to reason about than hand-written descriptions.

The second question is difficult to answer without actually trying both approaches. However, the operations on lists are largely analogous to the operations that would be performed if functions were used to represent ELLA rows. The big difference would probably be in the better support for functions present in the HOL system. Less work would have been required in building up infrastructure to support the proof. Now that much of that infrastructure has been developed there is not such a strong argument against the use of lists. Furthermore, lists probably seem more natural to most engineers and computer scientists. The syntax of ELLA is also very suggestive of lists so the hardware designer familiar with ELLA would probably find lists in the logic easier to deal with than functions representing rows.

Both lists and functions are inadequate representations for ELLA rows in that they do not capture the size of the row. To model ELLA rows well, dependent types are required. These allow the type for rows to be dependent on a term, in this case on the number representing the size of the row. HOL does not have dependent types, though they can to some extent be simulated in the logic. This could have been done, but it would have imposed extra burdens on the proof because part of the type constraint would appear as assertions about terms (specifically about the length of lists). The assertions would have to be justified by proof rather than automatic type checking, though it might be possible to automate these justifications. Work is ongoing to look for a more general method of representing dependent types in the higher order logic used by the HOL system.

The approach to the formal semantics has been determined by a mixture of constraints imposed by the informal semantics of ELLA, the limitations of the logic, and the practical considerations of automatic translation. The biggest problems have been the representation of ELLA rows (already discussed) and of the ELLA unspecified value. The difficulties are particularly acute when the two features interact under the constraints of the methodology for combining ELLA with the HOL system. An example of this is to be found in the semantics for conditional statements (IF and CASE).

The IF and CASE statements may produce the unspecified value. For the IF statement the cause can be the condition being undefined. For the CASE statement it is because none of the choosers match. In such cases it is very difficult to produce an undefined value of the right type because the lifting may not be at the top level of the type. The type may be structured with HOL tuples and lists. Since the lifting is done at the level of the basic types, constructing an undefined value of a structured type involves building up lists or tuples of UU (undefined) values. This is particularly difficult with lists because due to the inadequacy of using lists to represent ELLA rows together with the requirement that an extra-logical environment is not used (see the introduction to Section 2), the translator does not know how long to make the list.

The simplest solution to this problem is to make the result undefined without using lifting. A value (of the correct type) is returned about which nothing can be proved. This inhibits any proofs about the ELLA text when the inputs are such that the ELLA simulator would yield the unspecified value. However, this is less satisfactory than having explicit UU’s. In particular, it means that the representation of undefinedness in the semantics is not uniform. In some places it is represented by UU, and in others it is represented by irreducibility of the term. UU values are not always propagated, but instead are caught by UNLIFT. Such occurrences of (UNLIFT UU) are one example of undefinedness being represented by the irreducibility of a term.

One task for future work is to make the treatment of undefinedness as uniform as possible. This has already been done for the semantics of the arithmetical operators by ensuring that UU values are propagated as much as possible, and that the two arguments of binary operators are treated symmetrically with respect to undefinedness.

Another problem with undefinedness is that of strictness. Suppose it is necessary to have the lifting at the top level of a structured type. Then a term such as:

         (UU,LIFT x,UU) : (bit)lifted # (bit)lifted # (bit)lifted

would have to be transformed into:

                       UU : (bit # bit # bit)lifted

The second term is less defined than the first. One problem with this is that useful information is being lost. Even if only one component of the structure is initially undefined, after transformation the whole structure is undefined. If the structure is then indexed to obtain one of the components that originally had a defined value, the result is an undefined value, when it could have (if the transformation had not taken place) been defined.

However, having non-strict functions can cause problems. Undefined values can disappear from a proof about a circuit. This may hide a problem in a sub-component of the circuit because the undefinedness of the result of the sub-component is not propagated thanks to a non-strict function. On the other hand it may be the intention of the designer that under certain conditions the sub-component delivers an undefined value. A non-strict function can then be used to ignore the output of that circuit under those conditions, by multiplexing for example. It is well known that multiplexers (or conditional statements in a programming language) should be non-strict.

The strictness issue is less clear for something like a multiplication operation, in which it is reasonable to return zero as the result when one argument is zero and the other is undefined. At least it is reasonable when the arguments are being provided by pieces of hardware. In the context of a programming language that evaluates both the arguments before trying to evaluate the function, it would not be appropriate to have a non-strict semantics when one of the arguments is zero, for in this case undefinedness is a non-terminating computation. If the evaluation of one of the arguments fails to terminate then the evaluation of the product will also fail to terminate. So, there is a difference here between giving a semantics to a strict-evaluation programming language and giving a semantics to a hardware description language where the language texts represent hardware. It would appear that semantics for hardware description languages may have more in common with the semantics for lazy (non-strict) programming languages.

Acknowledgements

Thanks are due to members of the Hardware Verification Group in Cambridge who have been associated with the HOL-ELLA project during this work: Mike Gordon, John Harrison, John Herbert and John Van Tassel. Discussions with Kees Goossens of the University of Edinburgh and Andrew Gordon of Cambridge have also been helpful. Thanks too to Tom Melham for providing the theories of integers and n-bit words used in the semantics, and for help with using HOL.

This work has been supported by the Department of Trade and Industry and the Science and Engineering Research Council of Great Britain through the “HOL Verification of ELLA Designs” project, and more recently by a studentship from the SERC. ACM SIGDA generously provided funds for travel.

References

[BGHT90] R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel. The HOL verification of ELLA designs. Technical Report 199, University of Cambridge Computer Laboratory, August 1990. Revised version in Proceedings of the International Workshop on Formal Methods in VLSI Design, Miami, January 1991. To be published by Springer-Verlag.

[BGL^{+}91] H. Barringer, G. Gough, T. Longshaw, B. Monahan, M. Peim, and A. Williams. Semantics and verification for Boolean Kernel ELLA using IO automata. In Proceedings of the Advanced Research Workshop on Correct Hardware Design Methodologies (CHARME’91), Turin, Italy, June 1991.

[Com89a] Computer General Electronic Design, 5 Greenways Business Park, Bellinger Close, Chippenham, Wiltshire, SN15 1BN, United Kingdom. The ELLA Language Reference Manual, Issue 4.0, 1989.

[Com89b] Computer General Electronic Design, 5 Greenways Business Park, Bellinger Close, Chippenham, Wiltshire, SN15 1BN, United Kingdom. The ELLA Tutorial, Issue 4.0, 1989.

[GMM^{+}78] M. Gordon, R. Milner, L. Morris, M. Newey, and C. Wadsworth. A metalanguage for interactive proof in LCF. In Proceedings of the 5th ACM Conference on Principles of Programming Languages, Tucson, Arizona, January 1978. Also issued as Report CSR-16-77, Department of Computer Science, University of Edinburgh, 1977.

[Goo91] K. G. W. Goossens. Embedding a CHDDL in a proof system. In Proceedings of the Advanced Research Workshop on Correct Hardware Design Methodologies (CHARME’91), Turin, Italy, June 1991. Also available as University of Edinburgh LFCS, Technical Report ECS-LFCS-91-155, May 1991.

[Gor] A. D. Gordon. The formal definition of a synchronous hardwaredescription language in higher order logic. To appear in the International Conference on Computer Design, Cambridge, Mass., October 1992.

[Gor87] M. J. C. Gordon. HOL: A proof generating system for higher-order logic. Technical Report 103, University of Cambridge Computer Laboratory, 1987. Revised version in G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, Kluwer, 1987.

[Mel89] T. F. Melham. Automating recursive type definitions in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989. Also available as University of Cambridge Computer Laboratory Technical Report 146.

[MH91] J. D. Morison and M. G. Hill. A formal definition of the static semantics of ELLA’s core. Report No. 91024, Royal Signals and Radar Establishment, August 1991.

[MPT86] J. D. Morison, N. E. Peeling, and T. L. Thorp. The design rationale of ELLA, a hardware design and description language. In C. J. Koomen and T. Moto-oka, editors, Proceedings of the Seventh International Conference on Computer Hardware Description Languages and their Applications, Tokyo 1985, pages 303–320, Amsterdam, 1986. North-Holland.

[SEA] V. Stavridou, S. M. Eker, and S. Aloneftis. FUNNEL: A CHDL with formal semantics. Submitted for publication, 1991.

[Tas92] J. P. Van Tassel. A formalisation of the VHDL simulation cycle. Technical Report 249, University of Cambridge Computer Laboratory, March 1992.

A Syntax of the Subset

Notation:

Lower-case identifiers are syntax elements. Upper-case identifiers are keywords. The symbol :- means that the syntax element to its left expands to one of the entities on its right. Each alternative on the right begins on a new line. The symbols << and >> are used to bracket a piece of syntax. All the elements within these brackets are optional. The symbol * is used for repetition. A syntax element or a piece of bracketed syntax that is followed by a * can appear zero or more times. Any symbol other than the four just described is a special symbol of the language (like a keyword, but non-alphanumeric).

A.1 Declarations

text         :-  declaration. <<declaration.>>*
declaration  :-  TYPE typedec <<,typedec>>*
                 INT intdec <<,intdec>>*
                 CONST constdec <<,constdec>>*
                 FN fndec <<,fndec>>*
                 MAC macdec <<,macdec>>*

A.2 Types

typedec      :-  name = enumerated
enumerated   :-  NEW( name <<& type>> <<| name <<& type>> >>* )
                 NEW name/(int..int)
type         :-  type1
type1        :-  name
                 (type)
                 [int]type
                 ( type <<,type>>* )
                 type2
type2        :-  [INT name] type
                 TYPE name

A.3 Integers

intdec       :-  name = int
int          :-  formula
formula      :-  <<formula operator>> formula1

formula1     :-  operator* formula2
formula2     :-  name
integervalue
IF boolean THEN int ELSE int FI
(int)
boolean      :-  formula

A.4 Constants

constdec     :-  name = const
const        :-  const1 <<| const1 >>*
const1       :-  [int]const1
const2
const2       :-  name
name/formula2
name & const2
(const)
( const <<, const>>* )
? type
name/(int..int)

A.5 Functions

fndec        :-  fnname = input -> type : fnbody
input        :-  ( inputitem <<,inputitem>>* )
inputitem    :-  type << : name name* >>
fnbody       :-  unit
ARITH int
DELAY (const1,int)

A.6 Units

unit         :-  unit fnname unit1
unit macname <<{macparams}>> unit1
unit CONC unit1
unit1
macparams    :-  macparam <<, macparam>>*
macparam     :-  int
type

unit1        :-  unit2
fnname unit1
macname <<{macparams}>> unit1
[int]unit1
[INT name = int..int]unit1
name & unit1
unit2 // name
unit2        :-  ? type
name
name/formula2
unit2[int]
unit2[[unit]]
unit2[int..int]
IF boolean THEN unit ELSE unit FI
unit3
unit3        :-  ( unit )
( unit <<,unit>>* )
caseclause
series
caseclause   :-  CASE unit OF choices <<ELSEOF choices>>*
                        <<ELSE unit>> ESAC
choices      :-  choosers:unit <<,choosers:unit>>*
choosers     :-  const

A.7 Series

series       :-  BEGIN <<step.>>* OUTPUT unit END
( <<step.>>* OUTPUT unit )
step         :-  MAKE makeitem <<,makeitem>>*
LET letitem <<,letitem>>*
<<FOR multiplier>> JOIN joinitem <<,joinitem>>*
makeitem     :-  <<[int]>> fnname : name name*
<<[int]>> macname <<{macparams}>> <<{macparams}>>
                                       : name name*
letitem      :-  name = unit
joinitem     :-  unit -> name <<[int]>>
multiplier   :-  INT name = int..int <<INT name = int..int>>*

A.8 Macros

macdec       :-  macname <<{macspec}>> = input -> type : fnbody
macspec      :-  mactype name name* << , mactype name name* >>*
mactype      :-  INT
                 TYPE