*To*: Gottfried Barrow <igbi at gmx.com>*Subject*: Re: [isabelle] I need a fixed mutable array*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Wed, 18 Jun 2014 20:26:48 +0100*Cc*: Anthony Fox <acjf3 at cam.ac.uk>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <53A0C73F.7080407@gmx.com>*References*: <53A0652B.7000509@gmx.com> <42AC1402-3D1F-48C6-98F0-47D3176D34D9@nicta.com.au> <53A0C73F.7080407@gmx.com>*Sender*: ramana.kumar at gmail.com

On Tue, Jun 17, 2014 at 11:54 PM, Gottfried Barrow <igbi at gmx.com> wrote: > On 14-06-17 16:58, Gerwin Klein wrote: > >> most assembly formalisation don’t represent memory as an array, but as a >> function from address to value (usually byte or word). With that, read is >> just function application, store is function update. These are easier to >> reason about than arrays. >> > Gerwin, > > I do actually have a set of word datatypes in mind. At the moment, this is > what I'm thinking: > > type_synonym b8T = "bool * bool * bool * bool * bool * bool * bool * > bool" > type_synonym b16T = "b8T * b8T" > type_synonym b32T = "b16T * b16T" > type_synonym b64T = "b32T * b32T" > type_synonym b128T = "b64T * b64T" > type_synonym b256T = "b128T * b128T" > > If someone showed me specifically the memory representation you're talking > about, along with some supplementary documentation and explanations, I > could probably figure out in about 15 minutes to an hour whether trying to > go that route would be within my ability. > > There are existing large formalisations of x86 out there that you might >> want to look at. E.g. the Cambridge model in HOL4, which is close to what >> you’d do in Isabelle... >> > > Initially, I did have the idea to try and model things at the bit and > opcode level, but I decided that's not doable. Lifetimes have an upper > limit, and it's hard to produce something as it is. > > I've started to compartmentalize more between programming and proving. I > don't have to do proofs for all the functions, datatypes, and lines of > logic I define in Isabelle/HOL, though proofs are desirable. Isabelle is > useful just as a way to work with functions and datatypes at a higher > level, to experiment with ideas. > > My idea now is to take a very minimal model of an Intel cpu and implement > pseudo-assembly language around that model, for the smallest number of > instructions possible. > > It seems it should be very simple. I move data in and out of registers, > back and forth to memory, doing bit operations and arithmetic, and look at > flags to make decisions. As far as proving, that wouldn't be simple at all. > > I have to go with what I know, and I always learn something in the process > anyway. The only mutable datatype I know about in Isabelle/HOL is a record, > so it seems a mutable array would have to be something like I defined. > > I did a few searches on the HOL4 model you mentioned, but my motivation is > low to pursue that. It's got to be very complex and huge. > I recommend looking at the other (non-x86) processor models in HOL4 too. Not all are complex and huge (though I guess that depends on your perspective). > > Thanks, > GB > > > >

**Follow-Ups**:**Re: [isabelle] I need a fixed mutable array***From:*Gottfried Barrow

**References**:**[isabelle] I need a fixed mutable array***From:*Gottfried Barrow

**Re: [isabelle] I need a fixed mutable array***From:*Gerwin Klein

**Re: [isabelle] I need a fixed mutable array***From:*Gottfried Barrow

- Previous by Date: Re: [isabelle] I need a fixed mutable array
- Next by Date: Re: [isabelle] Bound variables in Code_Evaluation.term
- Previous by Thread: Re: [isabelle] I need a fixed mutable array
- Next by Thread: Re: [isabelle] I need a fixed mutable array
- Cl-isabelle-users June 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list