(**************************************************************************)
(*     ARM/Power Multiprocessor Machine Code Semantics: HOL sources       *)
(*                                                                        *)
(*                                                                        *)
(*  Jade Alglave (2), Anthony Fox (1), Samin Isthiaq (3),                 *)
(*  Magnus Myreen (1), Susmit Sarkar (1), Peter Sewell (1),               *)
(*  Francesco Zappa Nardelli (2)                                          *)
(*                                                                        *)
(*   (1) Computer Laboratory, University of Cambridge                     *)
(*   (2) Moscova project, INRIA Paris-Rocquencourt                        *)
(*   (3) Microsoft Research Cambridge                                     *)
(*                                                                        *)
(*     Copyright 2007-2008                                                *)
(*                                                                        *)
(*  Redistribution and use in source and binary forms, with or without    *)
(*  modification, are permitted provided that the following conditions    *)
(*  are met:                                                              *)
(*                                                                        *)
(*  1. Redistributions of source code must retain the above copyright     *)
(*     notice, this list of conditions and the following disclaimer.      *)
(*  2. Redistributions in binary form must reproduce the above copyright  *)
(*     notice, this list of conditions and the following disclaimer in    *)
(*     the documentation and/or other materials provided with the         *)
(*     distribution.                                                      *)
(*  3. The names of the authors may not be used to endorse or promote     *)
(*     products derived from this software without specific prior         *)
(*     written permission.                                                *)
(*                                                                        *)
(*  THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS    *)
(*  OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED     *)
(*  WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE    *)
(*  ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY       *)
(*  DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL    *)
(*  DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE     *)
(*  GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS         *)
(*  INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,          *)
(*  WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING             *)
(*  NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS    *)
(*  SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.          *)
(*                                                                        *)
(**************************************************************************)

open HolKernel boolLib bossLib Parse;
open wordsTheory bit_listTheory listTheory;

open ppc_coretypesTheory;

open HolDoc;
val _ = new_theory "ppc_seq_monad";


(* state *)

val _ = type_abbrev("ppc_state",
  ``:(ppc_reg32 -> word32) # (ppc_bit -> bool option) # (word32 -> word8 option) # bool # word32``);
  (* tuple consists of registers, status bits, byte-addressed memory, reverse bit and reserve address *)

(* functions for reading/writing state *)

val PREAD_R_def = Define `PREAD_R rd ((r,s,m,rb,ra):ppc_state) = r rd`;
val PREAD_S_def = Define `PREAD_S rd ((r,s,m,rb,ra):ppc_state) = s rd`;
val PREAD_M_def = Define `PREAD_M rd ((r,s,m,rb,ra):ppc_state) = m rd`;

val PWRITE_R_def = Define `PWRITE_R rd x (r,s,m,rb,ra) = ((rd =+ x) r,s,m,rb,ra):ppc_state`;
val PWRITE_S_def = Define `PWRITE_S rd x (r,s,m,rb,ra) = (r,(rd =+ x) s,m,rb,ra):ppc_state`;
val PWRITE_M_def = Define `PWRITE_M rd x (r,s,m,rb,ra) = (r,s,(rd =+ x) m,rb,ra):ppc_state`;

val PREAD_REVERSE_BIT_def = Define `PREAD_REVERSE_BIT ((r,s,m,rb,ra):ppc_state) = rb`;
val PREAD_RESERVE_ADDRESS_def = Define `PREAD_REVERSE_ADDRESS ((r,s,m,rb,ra):ppc_state) = ra`;

val PWRITE_REVERSE_BIT_def = Define `PWRITE_REVERSE_BIT x ((r,s,m,rb,ra):ppc_state) = ((r,s,m,x,ra):ppc_state)`;
val PWRITE_RESERVE_ADDRESS_def = Define `PWRITE_REVERSE_ADDRESS x ((r,s,m,rb,ra):ppc_state) = ((r,s,m,rb,x):ppc_state)`;


(* ---------------------------------------------------------------------------------- *>

  We define a state and monads for constructing a sequential version of the semantics.

<* ---------------------------------------------------------------------------------- *)

val _ = type_abbrev("M",``:ppc_state -> ('a # ppc_state) option``); 


(* sequential monads for an option state *)

val constT_seq_def = Define `
  (constT_seq: 'a -> 'a M) x = \y. SOME (x,y)`;

val addT_seq_def = Define `
  (addT_seq: 'a -> 'b M -> ('a # 'b) M) x s = 
    \y. case s y of NONE -> NONE || SOME (z,t) -> SOME ((x,z),t)`;

val lockT_seq_def = Define `
  (lockT_seq: 'a M -> 'a M) s = s`;

val syncT_seq_def = Define `
  (syncT_seq: iiid -> unit M) x = constT_seq ()`;

val failureT_seq_def = Define `
  (failureT_seq: 'a M) = \y. NONE`;

val seqT_seq_def = Define `
  (seqT_seq: 'a M -> ('a -> 'b M) -> 'b M) s f = 
    \y. case s y of NONE -> NONE || SOME (z,t) -> f z t`;

val parT_seq_def = Define `
  (parT_seq: 'a M -> 'b M -> ('a # 'b) M) s t = 
    \y. case s y of NONE -> NONE || SOME (a,z) -> 
        case t z of NONE -> NONE || SOME (b,x) -> SOME ((a,b),x)`;

val parT_unit_seq_def = Define `
  (parT_unit_seq: unit M -> unit M -> unit M) s t = 
    \y. case s y of NONE -> NONE || SOME (a,z) -> 
        case t z of NONE -> NONE || SOME (b,x) -> SOME ((),x)`;

(* register reads/writes always succeed. *)

val write_reg_seq_def = Define `(write_reg_seq ii r x):unit M = 
  \s. SOME ((),PWRITE_R r x s)`;

val read_reg_seq_def = Define `(read_reg_seq ii r):word32 M = 
  \s. SOME (PREAD_R r s,s)`;

(* eflags can always be written, but reading a NONE status bit causes a failure *)

val write_status_seq_def = Define `(write_status_seq ii f x):unit M = 
  (\s. SOME ((),PWRITE_S f x s))`;

val read_status_seq_def  = Define `(read_status_seq ii f):bool M = 
  (\s. case PREAD_S f s of NONE -> NONE || SOME b -> SOME (b,s))`;

(* memory writes are only allowed to modelled memory, i.e. locations containing SOME ... *)

val write_mem8_seq_def   = Define `(write_mem8_seq ii a x):unit M = 
  (\s. case PREAD_M a s of NONE -> NONE || SOME y -> SOME ((),PWRITE_M a (SOME x) s))`;

(* a memory read to an unmodelled memory location causes a failure *)

val read_mem8_seq_def  = Define `(read_mem8_seq ii a):word8 M = 
  (\s. case PREAD_M a s of NONE -> NONE || SOME x -> SOME (x,s))`;

(* reading and writing 32-bit entities *)

val read_mem32_seq_def = Define `(read_mem32_seq ii a):word32 M =
  seqT_seq (parT_seq (read_mem8_seq ii (a+0w)) (parT_seq (read_mem8_seq ii (a+1w)) 
           (parT_seq (read_mem8_seq ii (a+2w)) (read_mem8_seq ii (a+3w)))))
       (\(x0,x1,x2,x3). constT_seq (bytes2word [x0;x1;x2;x3]))`;

val write_mem32_seq_def = Define `(write_mem32_seq ii a w):unit M =
    (let bs = word2bytes 4 w in
       parT_unit_seq (write_mem8_seq ii (a+0w) (EL 0 bs)) (parT_unit_seq (write_mem8_seq ii (a+1w) (EL 1 bs)) 
      (parT_unit_seq (write_mem8_seq ii (a+2w) (EL 2 bs)) (write_mem8_seq ii (a+3w) (EL 3 bs)))))`;

(* register reads/writes reverse bit and reverse address *)

val write_reserve_bit_seq_def = Define `(write_reserve_bit_seq (ii:iiid) x):unit M = 
  \s. SOME ((),PWRITE_REVERSE_BIT x s)`;

val read_reserve_bit_seq_def = Define `(read_reserve_bit_seq (ii:iiid)):bool M = 
  \s. SOME (PREAD_REVERSE_BIT s,s)`;

(* register reads/writes reverse bit and reverse address *)

val write_reserve_address_seq_def = Define `(write_reserve_address_seq (ii:iiid) x):unit M = 
  \s. SOME ((),PWRITE_REVERSE_ADDRESS x s)`;

val read_reserve_address_seq_def = Define `(read_reserve_address_seq (ii:iiid)):word32 M = 
  \s. SOME (PREAD_REVERSE_ADDRESS s,s)`;


(* export *)

val _ = Define `(constT: 'a -> 'a M)                                     = constT_seq`;
val _ = Define `(addT: 'a -> 'b M -> ('a # 'b) M)                        = addT_seq`;
val _ = Define `(lockT: unit M -> unit M)                                = lockT_seq`;
val _ = Define `(syncT: iiid -> unit M)                                  = syncT_seq`;
val _ = Define `(failureT: unit M)                                       = failureT_seq`;
val _ = Define `(control_seqT: 'a M -> (('a -> 'b M) -> 'b M))           = seqT_seq`;
val _ = Define `(seqT: 'a M -> (('a -> 'b M) -> 'b M))                   = seqT_seq`;
val _ = Define `(parT: 'a M -> 'b M -> ('a # 'b) M)                      = parT_seq`;
val _ = Define `(parT_unit: unit M -> unit M -> unit M)                  = parT_unit_seq`;
val _ = Define `(write_reg: iiid -> ppc_reg32 -> word32 -> unit M)         = write_reg_seq`;
val _ = Define `(read_reg: iiid -> ppc_reg32 -> word32 M)                  = read_reg_seq`;
val _ = Define `(write_status: iiid -> ppc_bit -> bool option -> unit M) = write_status_seq`;
val _ = Define `(read_status: iiid -> ppc_bit -> bool M)                 = read_status_seq`;
val _ = Define `(write_mem8: iiid -> word32 -> word8 -> unit M)          = write_mem8_seq`;
val _ = Define `(read_mem8: iiid -> word32 -> word8 M)                   = read_mem8_seq`;
val _ = Define `(write_mem32: iiid -> word32 -> word32 -> unit M)        = write_mem32_seq`;
val _ = Define `(read_mem32: iiid -> word32 -> word32 M)                 = read_mem32_seq`;
val _ = Define `(write_reserve_bit: iiid -> bool -> unit M)              = write_reserve_bit_seq`;
val _ = Define `(read_reserve_bit: iiid -> bool M)                       = read_reserve_bit_seq`;
val _ = Define `(write_reserve_address: iiid -> word32 -> unit M)        = write_reserve_address_seq`;
val _ = Define `(read_reserve_address: iiid -> word32 M)                 = read_reserve_address_seq`;


(* some rewriter-friendly theorems *)

val option_apply_def = Define `
  option_apply x f = if x = NONE then NONE else f (THE x)`;

val option_apply_SOME = prove(
  ``!x f. option_apply (SOME x) f = f x``,SRW_TAC [] [option_apply_def]);

val mem_seq_lemma = prove(
  ``(read_mem8_seq ii a s = option_apply (PREAD_M a s) (\x. SOME (x,s))) /\ 
    (write_mem8_seq ii a y s = option_apply (PREAD_M a s) (\x. SOME ((),PWRITE_M a (SOME y) s)))``,
  SRW_TAC [] [option_apply_def,read_mem8_seq_def,write_mem8_seq_def] 
  THEN Cases_on `PREAD_M a s` THEN FULL_SIMP_TAC std_ss []);

val read_status_seq_lemma = prove(
  ``read_status_seq ii f s = option_apply (PREAD_S f s) (\x. SOME (x,s))``,
  SRW_TAC [] [option_apply_def,read_status_seq_def] 
  THEN Cases_on `PREAD_S f s` THEN FULL_SIMP_TAC std_ss []);
  
val parT_unit_seq_lemma = prove(
  ``(parT_unit_seq s t = \y. option_apply (s y) (\z.
                         option_apply (t (SND z)) (\x. SOME ((),SND x))))``,
  SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `s y`
  THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x`
  THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def]
  THEN FULL_SIMP_TAC std_ss [] THEN Cases_on `t r`
  THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def] THEN Cases_on `x`  
  THEN SRW_TAC [] [parT_unit_seq_def,FUN_EQ_THM,option_apply_def]); 

val monad_simp_lemma = prove(
  ``(constT_seq x = \y. SOME (x,y)) /\ (failureT_seq = \y. NONE) /\  (lockT_seq d = d) /\
    (addT_seq q s = \y. option_apply (s y) (\t. SOME ((q,FST t),SND t))) /\
    (seqT_seq s f = \y. option_apply (s y) (\t. f (FST t) (SND t))) /\
    (parT_seq s t = \y. option_apply (s y) (\z.
                    option_apply (t (SND z)) (\x. SOME ((FST z,FST x),SND x))))``,
  SRW_TAC [] [parT_seq_def,seqT_seq_def,failureT_seq_def,lockT_seq_def,
                   addT_seq_def,constT_seq_def,FUN_EQ_THM]
  THEN Cases_on `s y` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def]
  THEN Cases_on `x` THEN POP_ASSUM MP_TAC THEN SRW_TAC [] [option_apply_def]
  THEN Cases_on `t r` THEN SRW_TAC [] [option_apply_def] THEN FULL_SIMP_TAC std_ss []
  THEN Cases_on `x` THEN SRW_TAC [] [option_apply_def]);

val seq_monad_thm = save_thm("seq_monad_thm",let
  val xs = option_apply_SOME :: mem_seq_lemma :: read_status_seq_lemma :: 
           parT_unit_seq_lemma :: (CONJUNCTS monad_simp_lemma)
  in LIST_CONJ (map GEN_ALL xs) end);

val PREAD_CLAUSES = store_thm("PREAD_CLAUSES",
  ``!s. (PREAD_R r (PWRITE_M a x s) = PREAD_R r s) /\
        (PREAD_R r (PWRITE_S f b s) = PREAD_R r s) /\
        (PREAD_M a (PWRITE_R r w s) = PREAD_M a s) /\
        (PREAD_M a (PWRITE_S f b s) = PREAD_M a s) /\
        (PREAD_S f (PWRITE_R r w s) = PREAD_S f s) /\
        (PREAD_S f (PWRITE_M a x s) = PREAD_S f s) /\
        (PREAD_R r (PWRITE_R r2 w s) = if r = r2 then w else PREAD_R r s) /\
        (PREAD_M a (PWRITE_M a2 x s) = if a = a2 then x else PREAD_M a s) /\
        (PREAD_S f (PWRITE_S f2 b s) = if f = f2 then b else PREAD_S f s)``,
  Cases THEN Cases_on `r'` THEN Cases_on `r''` THEN Cases_on `r'`
  THEN SRW_TAC [] [PREAD_R_def,PREAD_M_def,PREAD_S_def, 
    PWRITE_M_def,PWRITE_R_def,PWRITE_S_def, combinTheory.APPLY_UPDATE_THM]);


val _ = export_theory ();