section \<open>A Compiler for the Register Machine from Hell\<close>

text \<open>
\<^emph>\<open>Processors from Hell\<close> has released its next-generation RISC processor RMfH.
It features an infinite bank of registers \<open>R\<^sub>0\<close>, \<open>R\<^sub>1\<close>, \<dots> holding unbounded
integers. Register \<open>R\<^sub>0\<close> plays the role of the accumulator and is the
implicit source or destination register of all instructions. Any other
register involved in an instruction must be distinct from \<open>R\<^sub>0\<close>, which is
enforced by implicitly incrementing its index.

There are four instructions

  \<^descr> \<open>LDI i\<close> has the effect \<open>R\<^sub>0 := i\<close>
  \<^descr> \<open>LD n\<close> has the effect \<open>R\<^sub>0 := R\<^sub>n\<^sub>+\<^sub>1\<close>
  \<^descr> \<open>ST n\<close> has the effect \<open>R\<^sub>n\<^sub>+\<^sub>1 := R\<^sub>0\<close>
  \<^descr> \<open>ADD n\<close> has the effect \<open>R\<^sub>0 := R\<^sub>0 + R\<^sub>n\<^sub>+\<^sub>1\<close>

were \<open>i\<close> is an integer and \<open>n\<close> a natural number.

In this project you will implement and verify a compiler for the
Register Machine from Hell (RMfH).

(Adapted from \<^url>\<open>https://isabelle.in.tum.de/exercises/advanced/regmachine/ex.pdf\<close>)
\<close>

theory Project_Register_Machine_from_Hell
  imports Main
begin

text \<open>
Define a data type of instructions and an execution function \<open>exec\<close> that takes
an instruction and a state and returns the new state.
\<close>
type_synonym state = "nat \<Rightarrow> int"
datatype instr = Undefined

fun exec :: "instr \<Rightarrow> state \<Rightarrow> state"
  where
    "exec i s = undefined"

text \<open>
Extend @{const exec} to lists of instructions:
\<close>
fun execute :: "instr list \<Rightarrow> state \<Rightarrow> state"
  where
    "execute is s = undefined"

text \<open>
The engineers of \<^emph>\<open>PfH\<close> soon got tired of writing assembly language code
and designed their own high-level programming language of arithmetic
expressions. An expression can be

  \<^item> an integer constant,
  \<^item> one of the variables \<open>v\<^sub>0\<close>, \<open>v\<^sub>1\<close>, \<dots>, or
  \<^item> the sum of two expressions

Define a data type of expressions and an evaluation function that takes
an expression and a state and returns the resulting value. Because this
is a clean language, there is no implicit increment going on:
the value of \<open>v\<^sub>n\<close> in state \<open>s\<close> is simply \<open>s n\<close>.
\<close>
datatype expr = Undefined

fun "value" :: "expr \<Rightarrow> state \<Rightarrow> int"
  where
    "value e s = undefined"


subsection \<open>A Compiler\<close>

text \<open>
You have been recruited to write a compiler from @{typ expr} to @{typ "instr list"}.
You remember your compiler course and decide to emulate a stack machine using free
registers, that is, registers not used by the expression you are compiling.

Implement a compiler \<open>compile :: expr \<Rightarrow> nat \<Rightarrow> instr list\<close> where the second argument
is the index of the first free register that can be used to store intermediate results.
The result of an expression should be returned in \<open>R\<^sub>0\<close>.

Because \<open>R\<^sub>0\<close> is the accumulator, you decide on the following compilation scheme:
\<open>v\<^sub>i\<close> will be held in \<open>R\<^sub>i\<^sub>+\<^sub>1\<close>.
\<close>
fun compile :: "expr \<Rightarrow> nat \<Rightarrow> instr list"
  where
    "compile e k = undefined"


subsection \<open>Compiler Verification\<close>

text \<open>
Having earned a PhD in theoretical computer science you want to impress your
boss and colleagues at \<^emph>\<open>PfH\<close> by verifying your compiler. Unfortunately, your
colleagues could not care less, and your boss explicitly forbids you to pursue
this ill-guided project during working hours. As a result you decide to take
a week's holiday in the Austrian Alps to work hard on your proof. On the train
you have already sketched the correctness statement below.

However, there is definitely a precondition missing because \<open>k\<close> should be
large enough not to interfere with any of the variables in \<open>e\<close>. Moreover,
you have some lingering doubts about having the same \<open>s\<close> on both sides
despite the index shift between variables and registers. But because all
your definitions are executable, you hope that Isabelle will spot any
incorrect propositions before you even start its proofs. What worries you most
is the number of auxiliary lemmas it may take to prove your proposition.
\<close>
lemma
  "execute (compile e k) s 0 = value e s"
  sorry

end