Re: [isabelle] I need a fixed mutable array



On 14-06-17 17:54, Gottfried Barrow wrote:
My idea now is to take a very minimal model of an Intel cpu and implement pseudo-assembly language around that model, for the smallest number of instructions possible.

A little feedback can go a long way towards getting me to the next step.

This all falls under a more general question: "How do I execute a list of instructions in Isabelle/HOL, like in a normal programming language?"

Even further: "How do I use GOTO in a functional programming language?"

That led, with some past information, to this thought (possibly wrong):

1) There is nothing mutable in Isabelle/HOL. Records only have the appearance of mutability. Consequently, for my case, a record adds needless complexity.

So, no mutability can lead to good things.

I include some source and attach some source. The idea behind it is to have a cpu datatype that holds the register and memory state. I execute a list of instructions, and it produces a list of states, not that I know anything about state machines, only that Ramon Zuniga used to implement them in programmable logic. I wonder what that guy's up to these days.

I did a trivial proof, to make sure I had a token proof to show, but the value wasn't trivial. There was a simple condition I needed, and it hadn't occurred to me that I needed it. Another example that shows that proofs are a good thing.

With no mutability, based on the basic idea, it seems I should be able to prove some complex things about executing a list of instructions.

Regards,
GB

(*****************************************)
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
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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.