Re: [isabelle] I need a fixed mutable array



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
>
>
>
>



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