open Statement 

(*Mapping:
  load -> FNO
  store -> STA
  op -> RMW(op)*)

type instruction
type action

val stwcx_of : instruction -> instruction
val ssc : action -> action*action

(* ----- We define/reuse the list of writes that have reached their coherence
point, which we call rcp (Reaches Coherence Point) ------ *)

val rcp : (action*action) set

(*note: place holder, should be instantiated by the list iws that is made a set in MachineDefStorageSubsystem.lem:
writes_past_coherence_point = if m.coherence_points then Set`from_list iws else
{};*)
let rcp = { }

(* ----- We need a lemma which says that rcp is acyclic; this comes from
the fact that the list is augmented by the machine, in a linear way. ----- *)

let acyclic_rcp_lemma =
  is_acyclic (tc rcp)

(*Proof:

Suppose not. Then there is a cycle in the list of storage subsystem
transitions.*)

(* ----- Now we want to show that our mapping enforces SC executions ----- *)

val po : (action*action) set
val rf : (action*action) set
val fr : (action*action) set
val co : (action*action) set
let mapping_forces_sc_lemma = 
  is_acyclic (tc (fr union rf union po union co))

(*Proof:

Suppose not. Then there is a cycle in tc (fr union rf union po union co). We
show that this induces a cycle in rcp. Thus we contradict the acyclicity of
rcp.

QED with key lemma below*)

(* ----- We show that for all path ia1,ia2 in tc (fr U rf U po U co), there is a path wc1,wc2 in rcp ----- *) 

let sc_path_implies_rcp_path_lemma =
  forall ia1 ia2.
    (ia1,ia2) IN tc (fr union rf union po union co) -->
      (snd(ssc ia1), snd(ssc ia2)) IN tc rcp

(* Proof:

By induction on the length of the chain (ia1,ia2).

Suppose the base case proved (see below), and assume given a chain (ia1,ian),
such that (ia2,ian) verifies (snd(ssc ia2), snd(ssc ian)) IN tc rcp. Then by
applying the base case to (ia1,ia2) we have (snd(ssc ia1), snd(ssc ia2)) IN
rcp, hence the result by transitivity.

. Base case:

  . Suppose ia1 --po--> ia2.

(*
Our mapping imposes that for any action ia, there are a lwarx and a stwcx. such
that lwarx -dd-> ia -dd-> stwcx. (e.g. ia is an add) or ia = lwarx or ia =
stwcx.

Thus, in any of these cases, the write-conditional request (wp1,wc1) from the
stwcx. associated with ia1, is sent before the write-conditional requestion
(wp2,wc2) from the stwcx. associated with a2 (Pre condition 2 of Commit in the
first case, Pre condition 11 of Commit in the others).
*)

let wc_request_between_commits_lemma =
  forall ia1 ia2 t.
    (ia1,ia2) IN (trace_to_po t) -->
    ((commit_transition_of t ia1, commit_transition_of t (stwcx_of ia1)) IN rc (trace_to_order t) &&
      ((commit_transition_of t (stwcx_of ia1), commit_transition_of t ia2) IN rc (trace_to_order t)) &&
      ((commit_transition_of t ia2, commit_transition_of t (stwcx_of ia2)) IN rc (trace_to_order t)) 
    )

(*
Now, for all pair of stwcx. committed in program order, since the writes of
thei successful write-conditional request reach coherence points exactly when
they are committed, they are in this order in rcp.  *)

let in_po_reach_cp_in_order_lemma =
  forall ia1 ia2.
    (commit_transition_of t (stwcx_of ia1), commit_transition of t (stwcx_of ia2)) IN tc (trace_to_order t) -->
    (snd(ssc ia1), snd(ssc ia2)) IN tc rcp

(* Suppose ia1 --rf--> ia2.

Our mapping imposes ia1 = stwcx. and ia2 = lwarx, thus ia2 reads from the
stwcx. of ia1, i.e. there is a write wc2 from the stwcx. of ia2 s.t. ssc ia2 =
(snd(ssc ia1), wc2). By Accept a successful write-conditional request Pre
condition 2, we know that snd(ssc ia1) has reached CP. By Action 3, we know
that wc2 has reached CP. By Action 4b, we know that (snd(ssc ia1), wc2) in tc
rcp.

*)

let in_rf_reach_cp_in_order_lemma =
  forall ia1 ia2.
    fst (ssc ia2) = snd (ssc ia1) -->
    (snd (ssc ia1), snd (ssc ia2)) IN tc rcp
      

(* Suppose ia1 --co--> ia2.

Our mapping imposes ia1 and ia2 = stwcx., thus we directly have the result.

*)

(* Suppose ia1 --fr--> ia2.

Our mapping imposes ia1 = lwarx and ia2 = stwcx. 

By definition of fr, we have ia3 = stwcx. s.t. ia3 --rf--> ia1 and ia3 --co-->
ia2. From the case rf above, we have a write wc1 s.t. ssc ia1 = (snd (ssc
ia3), wc1).  

Now, by Accept a successful write-conditional request Pre condition 2 applied to ia1, we know that snd(ssc ia3) has reached CP, and that no coherence-successor of snd(ssc ia3) has reached CP, in particular not snd(ssc ia2).

By Action 3, we know that snd(ssc ia1) has reached CP, hence the result.
QED Base case *)