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

open HolDoc;
val _ = new_theory "common_types";


(* ************* Types **************** *)

(* type of address values and of values stored in registers *)
val _ = type_abbrev("Ximm", ``: word32``);

(* here we use a single value type, embedding the types of values in
normal registers, flags, and memory locations *)

val _ = type_abbrev  ("address", ``:Ximm``);
val _ = type_abbrev  ("value", ``:Ximm``); 
val _ = type_abbrev  ("eiid", ``:num``);
val _ = type_abbrev  ("reln", ``:'a # 'a -> bool``);
val _ = Hol_datatype `dirn = R | W`;
val _ = Hol_datatype `location = Location_reg of proc => 'reg 
             | Location_mem of address
             | Location_res of proc 
             | Location_res_addr of proc 
`;
(* *** Barriers are synchronization instructions (DMB in ARM, sync in PPC, both written as Sync here) *)
val _ = Hol_datatype `synchronization = Sync`; 

val _ = Hol_datatype `action = Access of dirn => 'reg location => value 
                             | Barrier of synchronization`;
val _ = Hol_datatype `event = <| eiid : eiid ; 
                                 iiid : iiid ; 
                                 action : 'reg action |> `;
val _ = Hol_datatype `architecture = Power205 | ARMv7  `;

val _ = Hol_datatype `event_structure = <| events : ('reg event) set ; 
                                             intra_causality_data : ('reg event) reln;
                                             intra_causality_control : ('reg event) reln;
                                             atomicity : ('reg event) set set;
                                             arch : architecture ;
                                             granule_size_exponent : num |> `;

(* Intra-causality is split into two relations. The idea is that flag
   --> PC iico in branches is recorded in intra_dependency_control,
   while reg32 --> non-PC-reg iico in arith instructions is recorded
   in intra_dependency_data.  Which relation is used for
   flag --> reg32 (eg in ADC) or reg32 --> PC (eg in shifts that
   target the PC directly) is unclear from the vendor docs.  *)

val _ = type_abbrev ("state_constraint", ``: ('reg location) -> value option``);

val _ = type_abbrev ("view_orders", ``:proc -> ('reg event) reln``);

val _ = Hol_datatype `
  execution_witness = 
    <| initial_state : ('reg state_constraint);
       vo : ('reg view_orders);
       write_serialization : ('reg event reln)     |> `;



(* we abstract out the eiid gensym, to make it nondeterministic here, for simple proofs, but deterministic in future code-extracted versions *)
val _ = type_abbrev("eiid_state", ``: eiid set ``);
val _ = Define `(next_eiid : eiid_state -> (eiid # eiid_state) set) eiids = { (eiid,eiids UNION {eiid}) | eiid | ~(eiid IN eiids)}`;
val _ = Define `(initial_eiid_state : eiid_state) = {} `;


val _ = type_abbrev("program_word8",  ``: (address -> word8 option) ``);
 
val _ = type_abbrev("run_skeleton", ``: (proc -> (program_order_index -> address option)) ``);

(* a run skeleton is well-formed if it is down-closed at each
processor and only mentions addresses in addrs*)

val _ = Define `(run_skeleton_wf:address set -> run_skeleton->bool) addrs rs = 
  (!p i i'.  ((~((rs p i') = NONE)) /\ (i<i')) ==>  (~((rs p i) = NONE))) /\
  (!p i a. (rs p i = SOME a) ==> a IN addrs) /\
  FINITE {p | ?i a. rs p i = SOME a}` ;




val _ = export_theory ();