Sun Mar 14 13:53:49 CET 2010

Dirty machine language

It is about proving an embedding of 2 semantics.

Let's start with an example.  I want to prove this rule correct:

 (([qw a ] [qw b] -)             ([qw (tv: a b -)]))
 (([addlw a] [qw b] -)           ([addlw (tv: a b -)]))
 (([qw a] -)                     ([addlw (tv: a -1 *)]))

This relates machine language elements (qw, addlw)  source language
elements (-) and meta language elements (-).

A thorn in my side has always been the presence of real machine
instructions.  What you want is something like this:

 (([qw a ]    [qw b] -)           ([qw (tv: a b -)]))
 (([iw (a +)] [qw b] -)           ([iw ((tv: a b -) +)]))
 (([qw a] -)                      ([iw ((tv: a -1 *) +]))

I.e. where the addlw machine instruction is represented by a piece of
source language code: map its semantics into the language that's being
compiled.  The problem is that the machine code is really messy, and
more specific and stateful than the language to compile.  I.e. flags
are affected, which do not show up in the source language, so it might
not be embedded directly.

The problem needs to be solved in reverse: give a correct semantics to
the machine language, and see if there is an embedding of the source
language that preserves the original semantics constrained by extra

I.e. the main problem is that the machine language isn't clean.
Otherwise mapping would be really trivial.  Representing this
dirtyness to verify that original semantics is preserved by adding
extra constraints, like which registers are clobbered, is the real

What would help is to try to express this in Haskell, so at least some
form of structure can fall out of the description when everything is
made explicit.