Re: [isabelle] I need a fixed mutable array



On 14-06-18 19:43, Gerwin Klein wrote:
A formalisation of (very) basic machine language is explained in Section 8.1 of Concrete Semantics:
http://www21.in.tum.de/~nipkow/Concrete-Semantics/

Gerwin,

Thanks again. That's short, but very useful. I kind of knew that my instruction set is one, big datatype, but it hadn't yet entered my mind what my execution function was going to be for the datatype, so seeing "iexec" is helpful.

Also, I'll be looking at the info about the program counter again, and other tips there.

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”

I've looked at that briefly now, and I start at section 3.1, where they're starting with num0 and num1. It would take me a lot of work to work through the details, and I'm assuming, it's safe to assume, it's not what I need, where my assumption is based on my work with Num.num, which I really like.

For what I'm trying to do, everything is about trying to precisely model the specific registers of a particular CPU. With a CPU, the register set and size of registers is fixed, and there's nothing that complex about them, though how they're used may be complex. For 64-bit registers, you usually only have 8-bit, 16-bit, 32-bit, and 64-bit words. Also, my choice of bool for the bits is based on the fact that True and False are fundamental to HOL, which might become very useful to me.

Arbitrary will be important, if I can get to it, but arbitrary has to be implemented as it's implemented by the good math libraries, and the precise way that they use fixed sized registers. For arbitrary, the first place I'll look to see how arithmetic is done will the GnuMP library. I'll be asking, "What's special about the way they deal with registers, and assembly language instructions?"

There's another issue here. For pattern matching with "fun", it's important that a datatype use only 0-ary type constructors, like True and False. My awareness of this is a result of having been working with Num.num. What I've done is use Num.num as a template, and I've implement the functionality of Num.num as a "bool list". For example, "[]" is 1, and [True,True] is 7. That allows me to pattern match in ways I otherwise couldn't pattern match.

Having spent a lot of time learning how Num.num works, I'm not very motivated to do it all again with Word, and I assume that doing things more straightforward will help me in some ways.

There always more. I'm talking prematurely, but suppose I need a sign bit for signed integers. I could do something like this for a 16-bit signed integer:

datatype d7T = d7C bool bool bool bool bool bool bool
datatype d8uT = d8uC bool bool bool bool bool bool bool bool
datatype d16sT = d16C bool d7T d8uT

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.

In times like these, a person like me would actually like to understand a phrase like "basic functions are as mutable as records", but I don't worry about understanding everything.

I'm actually liking what I stumbled onto, which is to generate a list of the CPU register and memory state for each instruction. That would get me a debugger by default. Compiled languages are bigger hassle to use, and with assembly language, it becomes more important to use GNU gdb, or some other IDE.

If I could get a state machine thing accurately modeling assembly language, then I could run it with a combination of Isabelle/HOL and ML, in Isabelle/jEdit. That would be nice.

Well, this is all premature.

Regards,
GB





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