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