Add/generate Isabelle lemmas about the monad lifting

Architecture-specific lemmas about concrete registers and types are generated
and written to a file <prefix>_lemmas.thy, generic lemmas are in the
theories *_extras.thy in lib/isabelle.  In particular, State_extras contains
simplification lemmas about the lifting from prompt to state monad.

1 files changed, 88 insertions, 86 deletions

diff --git a/src/gen_lib/state_monad.lem b/src/gen_lib/state_monad.lem
index f324a9f4..8ff39d62 100644
--- a/src/gen_lib/state_monad.lem
+++ b/src/gen_lib/state_monad.lem
@@ -24,7 +24,6 @@ let init_state regs =
      last_exclusive_operation_was_load = false |>
 
 type ex 'e =
-  | Exit
   | Failure of string
   | Throw of 'e
 
@@ -49,12 +48,24 @@ let bindS m f (s : sequential_state 'regs) =
 val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e
 let seqS m n = bindS m (fun (_ : unit) -> n)
 
-val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
-let exitS () s = [(Ex Exit, s)]
+let inline (>>$=) = bindS
+let inline (>>$) = seqS
+
+val chooseS : forall 'regs 'a 'e. list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = List.map (fun x -> (Value x, s)) xs
+
+val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
+let readS f = (fun s -> returnS (f s) s)
+
+val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e
+let updateS f = (fun s -> returnS () (f s))
 
 val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
 let failS msg s = [(Ex (Failure msg), s)]
 
+val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
+let exitS () = failS "exit"
+
 val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e
 let throwS e s = [(Ex (Throw e), s)]
 
@@ -63,7 +74,6 @@ let try_catchS m h s =
   List.concatMap (function
                   | (Value a, s') -> returnS a s'
                   | (Ex (Throw e), s') -> h e s'
-                  | (Ex Exit, s') -> [(Ex Exit, s')]
                   | (Ex (Failure msg), s') -> [(Ex (Failure msg), s')]
                   end) (m s)
 
@@ -99,85 +109,77 @@ let try_catchSR m h =
       | Right e -> h e
      end)
 
-val range : integer -> integer -> list integer
-let rec range i j =
-  if j < i then []
-  else if i = j then [i]
-  else i :: range (i+1) j
-
-val get_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a
-let get_regS state reg = reg.read_from state.regstate
-
-val set_regS : forall 'regs 'rv 'a. sequential_state 'regs -> register_ref 'regs 'rv 'a -> 'a -> sequential_state 'regs
-let set_regS state reg v =
-  <| state with regstate = reg.write_to state.regstate v |>
-
-
-val read_memS : forall 'regs 'e. read_kind -> integer -> integer -> monadS 'regs (list memory_byte) 'e
-let read_memS read_kind addr sz s =
-  (*let addr = unsigned (bitv_of_address_lifted addr) in
-  let sz = integerFromNat sz in*)
-  let addrs = range addr (addr+sz-1) in
-  match just_list (List.map (fun addr -> Map.lookup addr s.memstate) addrs) with
+val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
+let read_tagS addr =
+  readS (fun s -> fromMaybe B0 (Map.lookup (unsigned addr) s.tagstate))
+
+(* Read bytes from memory and return in little endian order *)
+val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
+let read_mem_bytesS read_kind addr sz =
+  let addr = unsigned addr in
+  let sz = integerFromNat sz in
+  let addrs = index_list addr (addr+sz-1) 1 in
+  let read_byte s addr = Map.lookup addr s.memstate in
+  readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
     | Just mem_val ->
-       let s' =
+       updateS (fun s ->
          if read_is_exclusive read_kind
          then <| s with last_exclusive_operation_was_load = true |>
-         else s
-       in
-       returnS (List.reverse mem_val) s'
-    | Nothing -> failS "read_memS" s
-  end
-
-(* caps are aligned at 32 bytes *)
-let cap_alignment = (32 : integer)
-
-val read_tagS : forall 'regs 'a 'e. Bitvector 'a => read_kind -> 'a -> monadS 'regs bitU 'e
-let read_tagS read_kind addr state =
-  let addr = (unsigned addr) / cap_alignment in
-  let tag = match (Map.lookup addr state.tagstate) with
-    | Just t -> t
-    | Nothing -> B0
-  end in
-  if read_is_exclusive read_kind
-  then [(Value tag, <| state with last_exclusive_operation_was_load = true |>)]
-  else [(Value tag, state)]
+         else s) >>$
+       returnS mem_val
+    | Nothing -> failS "read_memS"
+  end)
+
+val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
+let read_memS rk a sz =
+  read_mem_bytesS rk a (natFromInteger sz) >>$= (fun bytes ->
+  returnS (bits_of_mem_bytes bytes))
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS () state =
-  let success =
-    (Value true,  <| state with last_exclusive_operation_was_load = false |>) in
-  (Value false, state) :: if state.last_exclusive_operation_was_load then [success] else []
-
-val write_mem_eaS : forall 'regs 'e. write_kind -> integer -> integer -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz state =
-  (*let addr = unsigned (bitv_of_address_lifted addr) in
-  let sz = integerFromNat sz in*)
-  [(Value (), <| state with write_ea = Just (write_kind, addr, sz) |>)]
-
-val write_mem_valS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_valS v state =
-  let (_,addr,sz) = match state.write_ea with
-    | Nothing -> failwith "write ea has not been announced yet"
-    | Just write_ea -> write_ea end in
-  let addrs = range addr (addr+sz-1) in
-  (*let v = external_mem_value (bits_of v) in*)
-  let addresses_with_value = List.zip addrs (List.reverse v) in
-  let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
-                            state.memstate addresses_with_value in
-  [(Value true,  <| state with memstate = memstate |>)]
+let excl_resultS () =
+  readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
+  updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
+  chooseS (if excl_load then [false; true] else [false]))
+
+val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
+let write_mem_eaS write_kind addr sz =
+  let addr = unsigned addr in
+  let sz = integerFromNat sz in
+  updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>)
+
+(* Write little-endian list of bytes to previously announced address *)
+val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
+let write_mem_bytesS v =
+  readS (fun s -> s.write_ea) >>$= (function
+      | Nothing -> failS "write ea has not been announced yet"
+      | Just (_, addr, sz) ->
+         let addrs = index_list addr (addr+sz-1) 1 in
+         (*let v = external_mem_value (bits_of v) in*)
+         let a_v = List.zip addrs v in
+         let write_byte mem (addr, v) = Map.insert addr v mem in
+         updateS (fun s ->
+           <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
+         returnS true
+    end)
+
+val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
+let write_mem_valS v = match mem_bytes_of_bits v with
+  | Just v -> write_mem_bytesS v
+  | Nothing -> failS "write_mem_val"
+end
 
 val write_tagS : forall 'regs 'e. bitU -> monadS 'regs bool 'e
-let write_tagS t state =
-  let (_,addr,_) = match state.write_ea with
-    | Nothing -> failwith "write ea has not been announced yet"
-    | Just write_ea -> write_ea end in
-  let taddr = addr / cap_alignment in
-  let tagstate = Map.insert taddr t state.tagstate in
-  [(Value true,  <| state with tagstate = tagstate |>)]
+let write_tagS t =
+  readS (fun s -> s.write_ea) >>$= (function
+      | Nothing -> failS "write ea has not been announced yet"
+      | Just (_, addr, _) ->
+         (*let taddr = addr / cap_alignment in*)
+         updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
+         returnS true
+    end)
 
 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
-let read_regS reg s = [(Value (reg.read_from s.regstate), s)]
+let read_regS reg = readS (fun s -> reg.read_from s.regstate)
 
 (* TODO
 let read_reg_range reg i j state =
@@ -195,23 +197,23 @@ let read_reg_bitfield reg regfield =
 
 val read_regvalS : forall 'regs 'rv 'e.
   register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e
-let read_regvalS (read, _) reg s =
-  match read reg s.regstate with
-    | Just v ->  returnS v s
-    | Nothing -> failS ("read_regvalS " ^ reg) s
-  end
+let read_regvalS (read, _) reg =
+  readS (fun s -> read reg s.regstate) >>$= (function
+      | Just v ->  returnS v
+      | Nothing -> failS ("read_regvalS " ^ reg)
+    end)
 
 val write_regvalS : forall 'regs 'rv 'e.
   register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e
-let write_regvalS (_, write) reg v s =
-  match write reg v s.regstate with
-    | Just rs' -> returnS () (<| s with regstate = rs' |>)
-    | Nothing ->  failS ("write_regvalS " ^ reg) s
-  end
+let write_regvalS (_, write) reg v =
+  readS (fun s -> write reg v s.regstate) >>$= (function
+      | Just rs' -> updateS (fun s -> <| s with regstate = rs' |>)
+      | Nothing ->  failS ("write_regvalS " ^ reg)
+    end)
 
 val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e
-let write_regS reg v state =
-  [(Value (), <| state with regstate = reg.write_to state.regstate v |>)]
+let write_regS reg v =
+  updateS (fun s -> <| s with regstate = reg.write_to v s.regstate |>)
 
 (* TODO
 val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e