OneBit.v

From RecordUpdate Require Import RecordUpdate.
From stdpp Require Import gmap.

From TLA Require Import logic.

Module OneBit.

  Inductive pc := ncs | wait | w2 | w3 | w4 | cs | exit.
  Inductive threads := t0 | t1.

  Local Open Scope positive.
  Instance threads_eqdecision : EqDecision threads.
  Proof.
    solve_decision.
  Defined.
  Program Instance threads_countable : Countable threads := {|
      encode t := match t with t0 => 1 | t1 => 2 end;
      decode t := Some match t return threads with 1 => t0 | _ => t1 end
  |}.
  Next Obligation. by intros []. Qed.

  Record state := mkState
    {
       thpc : gmap threads pc;
       thflag : gmap threads bool;
    }.
  Instance _eta : Settable _ := settable! mkState <thpc; thflag>.

  Definition init (s: state) :=
      (forall  t : threads, s.(thpc) !! t = Some ncs)
   /\ (forall  t : threads, s.(thflag) !! t = Some false).

  Definition pc_ncs (t: threads) : action state :=
     fun s s' => s.(thpc) !! t = Some ncs /\
                 s' = s <| thpc ::= <[ t := wait ]> |>.

  Definition pc_wait (t: threads) : action state :=
      fun s s' => s.(thpc) !! t = Some wait /\
                  s' = s <| thpc ::= <[ t := w2 ]> |>
                         <| thflag ::= <[ t := true ]> |>.

  Definition pc_w2 (t: threads) : action state :=
     fun s s' => (
                   t = t0 /\
                   s.(thpc) !! t = Some w2 /\
                   s.(thflag) !! t1 = Some false /\
                   s' = s <| thpc ::= <[ t := cs ]> |>
                 )
                 \/
                 (
                   t = t1 /\
                   s.(thpc) !! t = Some w2 /\
                   s.(thflag) !! t0 = Some true /\
                   s' = s <| thpc ::= <[ t1 := w3 ]> |>
                 )
                 \/
                 (
                   t = t1 /\
                   s.(thpc) !! t = Some w2 /\
                   s.(thflag) !! t0 = Some false /\
                   s' = s <| thpc ::= <[ t1 := cs ]> |>
                 ).

   Definition pc_w3 (th: threads) : action state :=
     fun s s' => s.(thpc) !! th = Some w3 /\
                 s' = s <| thflag ::= <[ t1 := false]> |>
                        <| thpc ::= <[ th := w4 ]> |>.

   Definition pc_w4 (th: threads) : action state :=
     fun s s' => s.(thpc) !! th = Some w4 /\
                 s.(thflag) !! t0 = Some false /\
                 s' = s <| thpc ::= <[ th := wait ]> |>.

   Definition pc_cs (th: threads) : action state :=
     fun s s' => s.(thpc) !! th = Some cs /\
                 s' = s <| thpc ::= <[ th := exit ]> |>.

   Definition pc_exit (th: threads) : action state :=
     fun s s' => s.(thpc) !! th = Some exit /\
                 s' = s <| thflag ::= <[ th := false]> |>
                        <| thpc ::= <[ th := ncs ]> |>.

   Definition pnext : action state :=
     fun s s' => (
                   exists th, pc_wait th s s' \/
                              pc_w2 th s s' \/
                              pc_w3 th s s' \/
                              pc_w4 th s s' \/
                              pc_cs th s s' \/
                              pc_exit th s s'
                 ).

   Definition next : action state :=
     fun s s' => (exists th, pc_ncs th s s') \/ pnext s s' \/ s = s'.

   Definition OBFair := weak_fairness pnext.

   Definition spec : predicate state :=
     ⌜init⌝ ∧ □⟨next⟩ ∧ OBFair.

   #[global]
   Hint Unfold init next pc_ncs pc_wait
               pc_w2 pc_w3 pc_w4 pc_cs pc_exit pnext: stm.

   Ltac lookup_simp :=
     subst;
     repeat
       match goal with
       | H: _ |- _ => rewrite lookup_insert in H
       | H: _ |- _ => rewrite -> lookup_insert_ne in H by congruence
       | _ => rewrite lookup_insert
       | _ => rewrite -> lookup_insert_ne by congruence
       end;
     try congruence.

   Ltac threads_simp :=
      subst;
      match goal with
        | th: threads |- _ => destruct th
      end;
      try congruence.

   Ltac stm_simp :=
     autounfold with stm in *;
     intros; (intuition (repeat deex; subst; trivial));
     repeat deex;
     repeat (match goal with
        | s: state |- _ => (destruct s; cbn in * )
        | H: ?x = ?x |- _ => clear H
        | H: @eq state (mkState _ _) (mkState _ _) |- _ =>
            invc H; cbn in *
        | H: context[@set state _ _ _ _ _] |- _ =>
            progress (unfold set in H; simpl in H)
        | H: @eq bool _ _ |- _ => solve [ inversion H ]
        | _ => progress (unfold set; simpl)
        | _ => progress lookup_simp
        | _ => progress threads_simp
        | _ => progress cbn in *
        end).

   Ltac stm :=
     stm_simp;
     try solve [ intuition (repeat deex; eauto) ];
     try congruence.

   Definition ind_invariant : state -> Prop :=
     fun s => (forall th, s.(thpc) !! th = Some w2
                       \/ s.(thpc) !! th = Some cs
                          -> s.(thflag) !! th = Some true)
           /\ (forall th, s.(thpc) !! th = Some cs ->
                          (forall th2, th2 <> th
                                       -> s.(thpc) !! th2 <> Some cs))
           /\ (forall th, s.(thpc) !! th = Some w3
                       \/ s.(thpc) !! th = Some w4 -> th <> t0).

   Lemma ind_invariant_lemma :
     spec ⊢ □⌜ind_invariant⌝.
   Proof.
     rewrite /spec. tla_clear OBFair.
     apply init_invariant.
     + stm.
       unfold ind_invariant.
       split.
       - stm.
       - stm.
     + intros s s' H1 H2.
       unfold next in H2.
       destruct H2 as [H2 | H3].
       - destruct H2 as [th H2]; stm; unfold ind_invariant in *; stm.
       - destruct H3 as [H3 | H4].
           { stm; unfold ind_invariant in *; repeat split; stm.
             + pose proof (H4 t0 (or_introl H0)).
               pose proof (H3 eq_refl). contradiction.
             + pose proof (H4 t0 (or_introl H0)).
               pose proof (H3 eq_refl). contradiction.
             + pose proof (H4 t1 (or_intror H0)).
               rewrite -> H7 in H. inversion H.
             + pose proof (H4 t1 (or_intror H3)).
               rewrite -> H7 in H. inversion H.
             + pose proof (H4 t0 (or_intror H3)).
               rewrite -> H0 in H7. inversion H7.
             + pose proof (H4 t0 (or_intror H0)).
               rewrite -> H3 in H7. inversion H7.
           }
           -- rewrite -> H4 in H1. exact H1.
   Qed.

   Definition safety : state -> Prop :=
     fun s => (forall th, s.(thpc) !! th = Some cs ->
                          (forall th2, th2 <> th
                                       -> s.(thpc) !! th2 <> Some cs)).

   Theorem safety_theorem :
     spec ⊢ □⌜safety⌝.
   Proof.
     rewrite ind_invariant_lemma.
     apply always_impl_proper.
     unseal. intros H.
     unfold ind_invariant in H.
     unfold safety.
     apply H.
   Qed.

End OneBit.