Theory RegisterMachineSpecification

section ‹Register Machines›

subsection ‹Register Machine Specification›
theory RegisterMachineSpecification
  imports Main
begin

subsubsection ‹Basic Datatype Definitions›

text ‹The following specification of register machines is inspired by \<^cite>‹"mech_turing"› (see 
      \<^cite>‹"mech_turing_afp"› for the corresponding AFP article).›

(* Type synonyms for registers (= register indices) the "tape" (sim. to a
 * Turing machine) that contains a list of register values.
 *)
type_synonym register = nat
type_synonym tape = "register list"

(* The register machine understands "instructions" that operate on state(-id)s
 * and modify register(-id)s. The machine stops at the HALT instruction.
 *)
type_synonym state = nat
datatype instruction =
  isadd: Add (modifies : register) (goes_to : state) |
  issub: Sub (modifies : register) (goes_to : state) (goes_to_alt : state) |
  ishalt: Halt
where
  "modifies Halt = 0" |
  "goes_to_alt (Add _ next) = next"

(* A program, then, just becomes a list of these instructions *)
type_synonym program = "instruction list"

(* A configuration of the (runtime of) a machine encodes information about the
 * instruction and the state of the registers (i.e., the tape). We describe it
 * here as a tuple.
 *)
type_synonym configuration = "(state * tape)"

subsubsection ‹Essential Functions to operate the Register Machine›

(* Given a tape of register values and some instruction(s) the register
 * machine first reads the value of the register from the tape (by convention
 * assume that the value "read" by the HALT state is zero). The machine then,
 * fetches the next instruction from the program, and finally updates the
 * tape to reflect changes by the last instruction.
 *)

definition read :: "tape ⇒ program ⇒ state ⇒ nat"
  where "read t p s = t ! (modifies (p!s))"

definition fetch :: "state ⇒ program ⇒ nat ⇒ state" where
  "fetch s p v = (if issub (p!s) ∧ v = 0 then goes_to_alt (p!s)
                       else if ishalt (p!s) then s
                       else goes_to (p!s))"

definition update :: "tape ⇒ instruction ⇒ tape" where
  "update t i = (if ishalt i then t
                    else if isadd i then list_update t (modifies i) (t!(modifies i) + 1)
                    else list_update t (modifies i) (if t!(modifies i) = 0 then 0 else (t!(modifies i)) - 1) )"

definition step :: "configuration ⇒ program ⇒ configuration"
  where
    "(step ic p) = (let nexts = fetch (fst ic) p (read (snd ic) p (fst ic));
                        nextt = update (snd ic) (p!(fst ic))
                        in (nexts, nextt))"

fun steps :: "configuration ⇒ program ⇒ nat ⇒ configuration"
  where
    steps_zero: "(steps c p 0) = c"
  | steps_suc:  "(steps c p (Suc n)) = (step (steps c p n) p)"


subsubsection ‹Validity Checks and Assumptions›

(* check bound for each type of instruction *)
(* take a m representing the upper bound for state number *)
fun instruction_state_check :: "nat ⇒ instruction ⇒ bool"
  where isc_halt: "instruction_state_check _ Halt = True"
  |     isc_add: "instruction_state_check m (Add _ ns) = (ns < m)"
  |     isc_sub: "instruction_state_check m (Sub _ ns1 ns2) = ((ns1 < m) & (ns2 < m))"

fun instruction_register_check :: "nat ⇒ instruction ⇒ bool"
  where "instruction_register_check _ Halt = True"
  |     "instruction_register_check n (Add reg _) = (reg < n)"
  |     "instruction_register_check n (Sub reg _ _) = (reg < n)"

(* passes function via currying into list_all *)
fun program_state_check :: "program ⇒ bool"
  where "program_state_check p = list_all (instruction_state_check (length p)) p"

fun program_register_check :: "program ⇒ nat ⇒ bool"
  where "program_register_check p n = list_all (instruction_register_check n) p"

fun tape_check_initial :: "tape ⇒ nat ⇒ bool"
  where "tape_check_initial t a = (t ≠ [] ∧ t!0 = a ∧ (∀l>0. t ! l = 0))"

fun program_includes_halt :: "program ⇒ bool"
  where "program_includes_halt p = (length p > 1 ∧ ishalt (p ! (length p -1)) ∧ (∀k<length p-1. ¬ ishalt (p!k)))"

text ‹Is Valid and Terminates›

definition is_valid
  where "is_valid c p = (program_includes_halt p ∧ program_state_check p
                            ∧ (program_register_check p (length (snd c))))"

definition is_valid_initial
  where "is_valid_initial c p a = ((is_valid c p)
                                ∧ (tape_check_initial (snd c) a)
                                ∧ (fst c = 0))"

definition correct_halt
  where "correct_halt c p q = (ishalt (p ! (fst (steps c p q)))  ― ‹halting›
                            ∧ (∀l<(length (snd c)). snd (steps c p q) ! l = 0))"

definition terminates :: "configuration ⇒ program ⇒ nat ⇒ bool"
  where "terminates c p q = ((q>0)
                          ∧ (correct_halt c p q)
                          ∧ (∀x<q. ¬ ishalt (p ! (fst (steps c p x)))))"

definition initial_config :: "nat ⇒ nat ⇒ configuration" where
  "initial_config n a = (0, (a # replicate n 0))"

end