section \A Compiler for the Register Machine from Hell\ text \ \<^emph>\Processors from Hell\ has released its next-generation RISC processor RMfH. It features an infinite bank of registers \R\<^sub>0\, \R\<^sub>1\, \ holding unbounded integers. Register \R\<^sub>0\ 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 \R\<^sub>0\, which is enforced by implicitly incrementing its index. There are four instructions \<^descr> \LDI i\ has the effect \R\<^sub>0 := i\ \<^descr> \LD n\ has the effect \R\<^sub>0 := R\<^sub>n\<^sub>+\<^sub>1\ \<^descr> \ST n\ has the effect \R\<^sub>n\<^sub>+\<^sub>1 := R\<^sub>0\ \<^descr> \ADD n\ has the effect \R\<^sub>0 := R\<^sub>0 + R\<^sub>n\<^sub>+\<^sub>1\ were \i\ is an integer and \n\ a natural number. In this project you will implement and verify a compiler for the Register Machine from Hell (RMfH). (Adapted from \<^url>\https://isabelle.in.tum.de/exercises/advanced/regmachine/ex.pdf\) \ theory Project_Register_Machine_from_Hell imports Main begin text \ Define a data type of instructions and an execution function \exec\ that takes an instruction and a state and returns the new state. \ type_synonym state = "nat \ int" datatype instr = Undefined fun exec :: "instr \ state \ state" where "exec i s = undefined" text \ Extend @{const exec} to lists of instructions: \ fun execute :: "instr list \ state \ state" where "execute is s = undefined" text \ The engineers of \<^emph>\PfH\ 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 \v\<^sub>0\, \v\<^sub>1\, \, 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 \v\<^sub>n\ in state \s\ is simply \s n\. \ datatype expr = Undefined fun "value" :: "expr \ state \ int" where "value e s = undefined" subsection \A Compiler\ text \ 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 \compile :: expr \ nat \ instr list\ 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 \R\<^sub>0\. Because \R\<^sub>0\ is the accumulator, you decide on the following compilation scheme: \v\<^sub>i\ will be held in \R\<^sub>i\<^sub>+\<^sub>1\. \ fun compile :: "expr \ nat \ instr list" where "compile e k = undefined" subsection \Compiler Verification\ text \ Having earned a PhD in theoretical computer science you want to impress your boss and colleagues at \<^emph>\PfH\ 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 \k\ should be large enough not to interfere with any of the variables in \e\. Moreover, you have some lingering doubts about having the same \s\ 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. \ lemma "execute (compile e k) s 0 = value e s" sorry end