Library OracleLanguages.Imp.Oracles.SwapAssign

Require Import Common.
Require Import Imp.Lang.
Require Import ProgrammingLanguage.
Require Import OracleLanguage.
Require Import OracleHelpers.

Module Make
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT)
       (Import OracleHelpers : ImpOracleHelpers Var_as_DT Lang).
  Inductive mod :=
  | Swap.

  Inductive _cont_mod :=
  | SwapCont.

  Definition _genv := unit.

  Inductive _state : Type :=
  | Stuck : state → state → _state
  | State : state → state → list (cont_mod mod _cont_mod) → _state.

  Definition perform_n_steps
             (n : nat) (S₁ S₂ : state)
             (km' : list (cont_mod mod _cont_mod)) : option _state :=
    
    match step υ S₁, step υ S₂ with
    | None, None ⇒
      None
    | _, _ ⇒
      match nsteps' υ n S₁, nsteps' υ n S₂ with
      | (S₁', 0), (S₂', 0) ⇒
        
        Some (State S₁' S₂' km')
      | (S₁', S _), (S₂', S _) ⇒
        
        Some (Stuck S₁' S₂')
      | _, _ ⇒
        
        None
      end
    end.

  Definition _step (_ : _genv) (S : _state) : option _state :=
    match S with
    | Stuck S₁ S₂ ⇒
      None
    | State S₁ S₂ km ⇒
      match step_helper S₁ S₂ km with
      | None ⇒
        None
      | Some StuckStep ⇒
        None
      | Some (GenericStep S₁' S₂' km') ⇒
        Some (State S₁' S₂' km')
      | Some (SpecialCmdStep _ km') ⇒
        perform_n_steps 1 S₁ S₂ ((ContMod SwapCont)::km')
      | Some (SpecialContStep _ km') ⇒
        perform_n_steps 2 S₁ S₂ km'
      end
    end.

  Definition _left_state (S : _state) : ProgrammingLanguage.state imp_language :=
    match S with
    | Stuck S₁ _ | State S₁ _ _ ⇒
      S₁
    end.

  Definition _right_state (S : _state) : ProgrammingLanguage.state imp_language :=
    match S with
    | Stuck _ S₂ | State _ S₂ _ ⇒
      S₂
    end.

  Definition swap_assignments c :=
    match c with
    | Seq (Assign x e) (Assign y e') ⇒
      ret (Seq (Assign y e') (Assign x e))
    | _ ⇒ None
    end.

  Fixpoint apply_cmd_mod c m :=
    match m with
    | Id ⇒ Some c
    | RecMod m₁ m₂ ⇒
      match c with
      | Seq c₁ c₂ ⇒
        apply_cmd_mod c₁ m₁ >>= λ c₁',
        apply_cmd_mod c₂ m₂ >>= λ c₂',
        Some (Seq c₁' c₂')
      | ITE b c₁ c₂ ⇒
        apply_cmd_mod c₁ m₁ >>= λ c₁',
        apply_cmd_mod c₂ m₂ >>= λ c₂',
        Some (ITE b c₁' c₂')
      | While b c ⇒
        apply_cmd_mod c m₁ >>= λ c',
        Some (While b c')
      | Skip | Assign _ _ | Assert _ ⇒
        None
      end
    | LeafMod Swap ⇒ swap_assignments c
    end.

  Lemma apply_cmd_mod_id:
    ∀ c, apply_cmd_mod c Id = Some c.

  Definition assign_indep' c :=
    match c with
    | Seq (Assign x e) (Assign y e') ⇒
      if In_exp_var_dec x e' then
        false
      else
        if In_exp_var_dec y e then
          false
        else
          negb (MFacts.eqb x y)
    | _ ⇒ false
    end.

  Fixpoint assign_indep m c :=
    match m with
    | Id ⇒ true
    | LeafMod Swap ⇒
      assign_indep' c
    | RecMod m₁ m₂ ⇒
      match c with
      | Seq c₁ c₂ | ITE _ c₁ c₂ ⇒ assign_indep m₁ c₁ && assign_indep m₂ c₂
      | While _ c₁ ⇒ assign_indep m₁ c₁
      | Skip | Assign _ _ | Assert _ ⇒ false
      end
    end.

  Inductive km_invariant : list (cont_mod mod _cont_mod) → cont → cont → Prop :=
  | empty_cont_mod : km_invariant [] [] []
  | cont_mod_inv :
      ∀ x₁ e₁ x₂ e₂ km k₁ k₂,
        x₁ ≠ x₂ →
        (¬ In_exp_var x₁ e₂) →
        (¬ In_exp_var x₂ e₁) →
        km_invariant km k₁ k₂ →
        km_invariant (ContMod SwapCont::km)
                     (Assign x₁ e₁::Assign x₂ e₂::k₁)
                     (Assign x₂ e₂::Assign x₁ e₁::k₂)
  | cmd_cont : ∀ c c' m km k₁ k₂,
      assign_indep m c = true →
      apply_cmd_mod c m = Some c' →
      km_invariant km k₁ k₂ →
      km_invariant (CmdMod m::km) (c::k₁) (c'::k₂).

  Definition _invariant (_ : _genv) (S : _state) : Prop :=
    match S with
    | Stuck S₁ S₂ ⇒ step υ S₁ = None ∧ step υ S₂ = None
    | State (k₁, s₁) (k₂, s₂) km ⇒
      km_invariant km k₁ k₂ ∧ M.Equal s₁ s₂
    end.

  Lemma eval_exp_add_neq:
    ∀ s x v e,
      (¬ In_exp_var x e) →
      eval_exp s e = eval_exp (M.add x v s) e.

  Lemma eval_exp_add_neq':
    ∀ s₁ s₂ x v e,
      M.Equal s₁ s₂ →
      (¬ In_exp_var x e) →
      eval_exp s₁ e = eval_exp (M.add x v s₂) e.

  Lemma map_swap_add_neq:
    ∀ {X : Type} s₁ s₂ x y (v₁ v₂ : X),
      M.Equal s₁ s₂ →
      x ≠ y →
      M.Equal (M.add x v₁ (M.add y v₂ s₁)) (M.add y v₂ (M.add x v₁ s₂)).

  Lemma _invariant_1:
    ∀ genv os os',
      _invariant genv os →
      _step genv os = Some os' →
      _invariant genv os'.
  Lemma _prediction_soundness :
    ∀ genv os os',
      _invariant genv os →
      _step genv os = Some os' →
      ∃ n₁ n₂,
        opt_state_eq (nsteps υ n₁ (_left_state os))
                       (Some (_left_state os'))
        ∧ opt_state_eq (nsteps υ n₂ (_right_state os))
                       (Some (_right_state os'))
        ∧ n₁ + n₂ > 0.

  Lemma _prediction_completeness :
    ∀ genv os,
      _invariant genv os →
      _step genv os = None →
      step υ (_left_state os) = None
      ∧ step υ (_right_state os) = None.
  Definition swapassign_oracle : oracle_language imp_language imp_language :=
    {|
      oracle_state := _state;
      oracle_genv := unit;
      oracle_step := _step;
      left_state := _left_state;
      right_state := _right_state;
      left_genv := λ _, υ;
      right_genv := λ _, υ;
      invariant := _invariant;
      invariant_1 := _invariant_1;
      prediction_soundness := _prediction_soundness;
      prediction_completeness := _prediction_completeness
    |}.
End Make.