Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <29139.9303101113@frogland.inmos.co.uk>
Subject: Re: Constructive logic, Nuprl and Hardware Verification
To: windley@edu.uidaho.cs.panther (Phil Windley)
Date: Wed, 10 Mar 1993 11:13:22 +0000 (GMT)
Cc: info-hol@edu.uidaho.cs.ted (info-hol mailing list)
In-Reply-To: <199303091609.AA04493@panther.cs.uidaho.edu> from "Phil Windley" at Mar 9, 93 08:09:32 am
Content-Type: text
Content-Length: 3746

Phil Windley has said:
> On Fri, 05 Mar 93 20:56:50 EST, mel@ultrastar.EE.CORNELL.EDU wrote:
> +------------
> | In the HOL workshop last September, Mark Aagaard and I had a paper
> | discussing how to exploit Nuprl's type theory to support multiple
> | hardware implementations of the same specification.  This work could
> | be done in HOL.  We believe that this would essentially require
> | duplicating the support of dependent types in HOL.  
> 
> Indeed has been.  I came home from the HOL workshop and used my abstract
> theory package (ATP) to implement the functions that Mark talked about.
> You don't really need dependent type to duplicate what Mark and Miriam did,
> but you do need subtypes (Miriam concurs here).  The ATP does subtypes, but
> not dependent types.
> 
> The place that I wish most for dependent types is in formulating vectors,
> particularly vectors of bits.  From what Mark and Miriam tell me, they have
> found NUPRL's dependent type mechanism helpful in describing vectors.  I
> remember a very nice talk by Keith Hanna at the second HOL workshop on
> VERITAS and how he formulated n-bit words.  Does anyone have a copy of his
> slides by any chance?

Sounds similar to what I am currently doing. I'll have to look into the
paper in HOL92 to see if it helps.

A couple of years ago I did a set of vector/array theories (based on
list which turned out to be a bit of a mistake I think). I had one
central theory which contained a bunch of theorems about operations
on list and then an ML file which was parameterized by a variable
to generate a theory of n-bit vectors for a given n.

Now, under the version of your abstract theory package that I have 
translated into HOL90 I am doing this again, except this time using
abstract theories. As the underlying representation I am using
functions from :num to :'a (for arrays) and :bool for the bit vector
subtype. What I am doing is having the abstract entity contain some
type which is an abstraction of a function whose value is set to a
constant arbitrary value for all arguments over a given number (the
wordlength). In addition there are abstraction and representation
functions between this functional representation and the type in the
abstract entity which satisfy all the properties of a defined type.
Using this I am now proving all the theorems I require in the abstract
theory. To get a concrete n-bit vector theory now all that is required
is to create a (sub-)type of functions from :num to :'a satisfying the
restriction, extract the properties of the defined type and insantiate
in all the abstarct theories.

As I have been doing this I have realised, as you report, that you
can take this one stage further. I have been developing proofs 
of hardware around a "correctness condition" which is a theorem
of the form

! SMod_0 ... SMod_n. (SMod_0 IMPLEMENTS SSpec_0) /\
                      ...
                     (SMod_n IMPLEMENTS SSpec_n)
                     ==> Mod(SMod_0, ..., SMod_n)
                         IMPLEMENTS Spec

I.e. given any sumbmodules that satisfy a set of sub-specifications
then a given combination of these defined by Mod satisfies the
specification Spec. This can all be taken up to the abstract theory
level. Here each specification becomes an abstract entity which
contains the specification as obligations. Not entirely sure how this
all works out in practice or whether it actually gains anything.

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		Life doesn't imitate art, it imitates bad television
						      - Husbands and Wives