Library OracleLanguages.Imp.Oracles.ValueChange

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

Module Make
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT).

  Definition _genv := list varid.

  Inductive _state : Type :=
  | State : state → state → _state.

  Definition _step (_ : _genv) (S : _state) : option _state :=
    match S with
    | State S₁ S₂ ⇒
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      Some (State S₁' S₂')
    end.

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

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

  Inductive same_control_cmd (modified_vars : list varid) : cmd → cmd → Prop :=
  | same_skip :
      same_control_cmd modified_vars Skip Skip
  | same_seq : ∀ c₁₁ c₂₁ c₁₂ c₂₂,
      same_control_cmd modified_vars c₁₁ c₂₁ →
      same_control_cmd modified_vars c₁₂ c₂₂ →
      same_control_cmd modified_vars (Seq c₁₁ c₁₂) (Seq c₂₁ c₂₂)
  | same_ITE : ∀ b c₁₁ c₂₁ c₁₂ c₂₂,
      same_control_cmd modified_vars c₁₁ c₂₁ →
      same_control_cmd modified_vars c₁₂ c₂₂ →
      (∀ x, In_bexp_var x b → ¬ In x modified_vars) →
      same_control_cmd modified_vars (ITE b c₁₁ c₁₂) (ITE b c₂₁ c₂₂)
  | same_While : ∀ b c₁ c₂,
      same_control_cmd modified_vars c₁ c₂ →
      (∀ x, In_bexp_var x b → ¬ In x modified_vars) →
      same_control_cmd modified_vars (While b c₁) (While b c₂)
  | same_assign : ∀ x e,
      (∀ x, In_exp_var x e → ¬ In x modified_vars) →
      same_control_cmd modified_vars (Assign x e) (Assign x e)
  | close_assign : ∀ x e₁ e₂,
      
      (∀ x, In_exp_var x e₁ ↔ In_exp_var x e₂) →
      (∀ d, In_exp_div d e₁ ↔ In_exp_div d e₂) →
      
      (∀ d, In_exp_div d e₁ → ∀ x, In_exp_var x d → ¬ In x modified_vars) →
      (∀ d, In_exp_div d e₂ → ∀ x, In_exp_var x d → ¬ In x modified_vars) →
      In x modified_vars →
      same_control_cmd modified_vars (Assign x e₁) (Assign x e₂)
  | same_assert : ∀ b,
      (∀ x, In_bexp_var x b → ¬ In x modified_vars) →
      same_control_cmd modified_vars (Assert b) (Assert b).

  Definition same_control_cont (modified_vars : list varid) (k₁ k₂ : cont) :=
    Forall2 (same_control_cmd modified_vars) k₁ k₂.

  Definition same_control_store (modified_vars : list varid) (s₁ s₂ : store) : Prop :=
    (∀ x, M.In x s₁ ↔ M.In x s₂)
    ∧ ∀ x, (¬ In x modified_vars) → M.find x s₁ = M.find x s₂.

  Lemma same_control_store_eval_exp:
    ∀ m s₁ s₂ e,
      same_control_store m s₁ s₂ →
      (∀ x, In_exp_var x e → ¬ In x m) →
      eval_exp s₁ e = eval_exp s₂ e.

  Lemma same_control_store_eval_bexp:
    ∀ m s₁ s₂ b,
      same_control_store m s₁ s₂ →
      (∀ x, In_bexp_var x b → ¬ In x m) →
      eval_bexp s₁ b = eval_bexp s₂ b.

  Definition _invariant (m : _genv) (S : _state) : Prop :=
    match S with
    | State (k₁, s₁) (k₂, s₂) ⇒
      same_control_cont m k₁ k₂
      ∧ same_control_store m s₁ s₂
    end.

  Lemma same_control_exp_crash:
    ∀ m s₁ s₂ e e',
    same_control_store m s₁ s₂ →
    (∀ x, In_exp_var x e ↔ In_exp_var x e') →
    (∀ d, In_exp_div d e ↔ In_exp_div d e') →
    (∀ d, In_exp_div d e → ∀ x, In_exp_var x d → ¬ In x m) →
    (∀ d, In_exp_div d e' → ∀ x, In_exp_var x d → ¬ In x m) →
    eval_exp s₁ e = None ↔ eval_exp s₂ e' = None.
  Lemma same_control_store_add_stable:
    ∀ m s₁ s₂, same_control_store m s₁ s₂ →
    ∀ x v, same_control_store m (M.add x v s₁) (M.add x v s₂).

  Lemma same_control_store_add_stable':
    ∀ m s₁ s₂, same_control_store m s₁ s₂ →
    ∀ x v v',
    In x m →
    same_control_store m (M.add x v s₁) (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 valuechange_oracle : oracle_language imp_language imp_language :=
    {|
      oracle_state := _state;
      oracle_genv := _genv;
      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.