(** Instantiation of the intransitive interference with an "array machine" *)
Require Import NI.Rushby.
From stdpp Require Import list relations gmap sets fin_sets.

Module ArrayMachine.

Definition state := nat -> nat.
Inductive command :=
  | Write : nat -> nat -> command
  | Read : nat -> command
.
Definition action := command.
Definition out := nat.

Definition extendS (s : state) (n : nat) (m : nat) : state :=
  fun x => if beq_nat x n then m else s x.

Definition preform (s : state) (a : action) : state * out :=
  match a with
    | Write i j => (extendS s i j, 0)
    | Read i => (s, s i)
  end.

Definition step s a := fst (preform s a).
Definition output s a := snd (preform s a).
Definition initial (x : nat) := 0.

End ArrayMachine.
Import ArrayMachine.
Instance ArrayMealyMachine : Mealy state action out :=
  { initial := initial;
    step := step;
    output := output }.

Eval compute in (do_actions [Write 1 1] 2).
(** ===> 0 *)

Definition domain := action.
Definition nameA := nat.
Definition valA := nat.
Definition observeA (u : domain) : gset nameA :=
  match u with
    | Read i => {[ i ]}
    | Write _ _ => ∅
  end.
Definition alterA (u : domain) : gset valA :=
  match u with
    | Read _ => ∅
    | Write i _ => {[ i ]}
  end.


Instance domain_dec : EqDecision domain.
Proof. intros u v.
unfold Decision.
repeat (decide equality).
Defined.

Instance domain_countable : Countable domain.
 refine (inj_countable' (λ x, match x with
  | Write i1 i2 => (inl (i1, i2))
  | Read i => (inr i)
  end) (λ x, match x with
  | inl (i1, i2) => Write i1 i2
  | inr i => Read i
  end) _); by intros [].
Defined.

Instance arraymachine_ss : StructuredState domain :=
  { name := nameA; value := valA; contents s n := s n
  ; observe := observeA; alter := alterA }.

Definition interference (u v : domain) :=
  (exists (n : nameA), n ∈ alterA u ∧ n ∈ observeA v).

Inductive interferenceR : relation domain :=
  | interference_refl : forall (u : domain), interferenceR u u
  | interference_step : forall (u v: domain), interference u v -> interferenceR u v.

Instance: Set_ nameA (gset nameA).
apply _.
Qed.

Instance policy_ss : Policy domain :=
  { policy := interferenceR
  ; dom := fun (a : action) => (a : domain) }.
Proof.
- intros v w.
  destruct v as [i j | i]; destruct w as [m n | m].
  + destruct (decide (i = m)). destruct (decide (j = n)); subst; auto.
    left. constructor.
    right. intro I. inversion I; subst. apply n0. auto.
    inversion H. unfold observeA in *. destruct H0 as [HH HHH].
    apply (not_elem_of_empty x HHH).
    right. intro. inversion H; subst. apply n0. auto.
    inversion H0. unfold alterA, observeA in *. destruct H1 as [HH HHH].
    apply (not_elem_of_empty x HHH).
  + destruct (decide (i = m)); subst. left. right. unfold interference.
    simpl. exists m. split; apply elem_of_singleton; auto.
    right. intro. inversion H; subst. inversion H0. simpl in H1.
    destruct H1. apply elem_of_singleton in H1; apply elem_of_singleton in H2. subst. apply n;auto.
  + right. intro. inversion H;subst. inversion H0; subst.
  simpl in H1; inversion H1. eapply (not_elem_of_empty x); eassumption.
  + destruct (decide (i = m)); subst.
    left. constructor.
    right. intro. inversion H; subst. auto.
    inversion H0; subst. simpl in H1; inversion H1.
    eapply (not_elem_of_empty x); eassumption.
- intro u. constructor.
Defined.

Instance rma_yay :  RefMonAssumptions.
Proof.
  split; simpl; unfold RMA_partition.
  - intros a s t Hst;
      unfold contents in *; simpl in *.
    unfold output.
    unfold preform. destruct a as [i j | i]; simpl in *. reflexivity.
    apply Hst. eapply elem_of_singleton. reflexivity.
  - intros a s t n Hst Hn.
    unfold step, preform. destruct a as [i j | i]. simpl in *.
    destruct (decide (i = n)); subst; unfold extendS; simpl.
    replace (beq_nat n n) with true; auto. apply beq_nat_refl.
    destruct Hn as [Hn|Hn].
    unfold step in Hn; simpl in Hn. unfold extendS in Hn; simpl in Hn.
    replace (beq_nat n i) with false in *; auto.
    congruence. symmetry. apply beq_nat_false_iff. omega.
    unfold step in Hn; simpl in Hn. unfold extendS in Hn; simpl in Hn.
    replace (beq_nat n i) with false in *; auto.
    congruence. symmetry. apply beq_nat_false_iff. omega.

    simpl. destruct Hn as [Hn|Hn]; unfold step, preform in Hn; simpl in Hn;
       congruence.
  - intros a s n Hst.
    unfold step, preform in Hst; simpl in Hst. destruct a; simpl in *.
    unfold extendS in Hst. destruct (decide (n = n0)); subst.
    apply elem_of_singleton; auto. replace (beq_nat n n0) with false in *; try (congruence). symmetry. apply beq_nat_false_iff. assumption.
congruence.
Defined.

Theorem yay : isecurity.
Proof.
  apply rma_secure_intransitive.
  intros u v n A1 A2. simpl.  right. firstorder.
Qed.