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.
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
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
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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and