Re: [isabelle] I need a fixed mutable array



Hi Gottfried,

are you aware of the HOL/Word library? It gives you arbitrary fixed-size words. With that, memory would be something like

type_synonym mem = “64 word => 8 word”

If the purpose is to model and reason only, basic functions are as mutable as records. If you want to generate efficient code from it, then it might be better to go with implementations like Peter’s.

A formalisation of (very) basic machine language is explained in Section 8.1 of Concrete Semantics:
http://www21.in.tum.de/~nipkow/Concrete-Semantics/

Cheers,
Gerwin

On 18.06.2014, at 8:54 am, 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.
>
> Thanks,
> GB
>
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.