theory i140618a__mem_write_execute_state_list
imports Complex_Main "~~/src/HOL/Library/Code_Target_Nat"
begin

(*16-bit dataword and a little notation.*)

  type_synonym b8T  = "bool * bool * bool * bool * bool * bool * bool * bool"
  type_synonym b16T = "b8T * b8T"

  notation (input) 
    False ("0\<^sub>B")
  notation (input) 
    True ("1\<^sub>B")
  abbreviation hex00 :: b8T ("00\<cdot>") where 
    "hex00 == (0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B,0\<^sub>B)"
  abbreviation hex55 :: b8T ("55\<cdot>") where 
    "hex55 == (0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B)"
  abbreviation hexAA :: b8T ("AA\<cdot>") where 
    "hexAA == (1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B,1\<^sub>B,0\<^sub>B)"
  abbreviation hex16 :: "b8T => b8T => b16T" where 
    "hex16 b1 b0 == (b1, b0)"
    notation hex16 ("x\<bar>__" [1000, 1000] 1000)

(*Indexed, fixed size b16T list. The list idx won't always match the pair idx.*)

  type_synonym idxed_flist = "(nat * b16T) list * nat"

  primrec idx0s_app_flist :: "(nat * b16T) list \<Rightarrow> nat \<Rightarrow> (nat * b16T) list" where
    "idx0s_app_flist nlist 0       = nlist"
   |"idx0s_app_flist nlist (Suc n) = idx0s_app_flist ((n,x\<bar>00\<cdot>00\<cdot>) # nlist) n"

  definition create_idxed_flist :: "nat \<Rightarrow> idxed_flist" where
    "create_idxed_flist lsize = (idx0s_app_flist [] lsize, lsize)"

  value "create_idxed_flist 0x10"
  value "length (fst (create_idxed_flist 0x10)) = 0x10"

(*The write function.*)
  
  primrec write_idxed_flist :: "idxed_flist \<Rightarrow> nat \<Rightarrow> b16T \<Rightarrow> idxed_flist option" 
    where
    "write_idxed_flist (flist, lsize) idx data = ( 
       if (idx >= lsize \<or> length flist \<noteq> lsize) then None 
       else Some (flist[idx := (idx, data)], lsize)
    )"

(*Two sequential writes done manually.*)

  value "write_idxed_flist 
    (the(write_idxed_flist (create_idxed_flist 0x10) 5 x\<bar>55\<cdot>55\<cdot>))
    3 x\<bar>AA\<cdot>AA\<cdot>"

(*Automate execution of a list of writes, to generate a list of states.*)

  fun execute_list :: "(idxed_flist option) list \<Rightarrow> (nat * b16T) list 
        \<Rightarrow> (idxed_flist option) list" where
    "execute_list [] _ = []"
   |"execute_list state_list [] = state_list"
   |"execute_list [s] ((idx,data) # xs)
       = execute_list ((write_idxed_flist (the s) idx data) # [s]) xs"
   |"execute_list (s # ss) ((idx,data) # xs)  
       = execute_list ((write_idxed_flist (the s) idx data) # (s # ss)) xs"
   (*Adding the third condition sped up the termination proof a lot. It probably 
     needs more conditions to speed it up more.*)

(*Execute a list of three instructions. The states are shown last to first.*)

  abbreviation "three_write_list == 
    [(5, x\<bar>55\<cdot>55\<cdot>), (3, x\<bar>AA\<cdot>AA\<cdot>), (0x10, x\<bar>55\<cdot>55\<cdot>)]"

  value "execute_list [Some (create_idxed_flist 0xF)] three_write_list"

(*Prove something trivial. The value of proving this wasn't trivial. It showed
  me I needed the condition "length flist \<noteq> lsize" in my function above.*)

  lemma "idx < lsize \<and> length flist = lsize
    \<Longrightarrow> write_idxed_flist (flist, lsize) idx dw \<noteq> None"
  by(simp)

(******************************************************************************)
end