Re: [isabelle] I need a fixed mutable array



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






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