Library OracleLanguages.Imp.Oracles.AbstractEquiv

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 either (A B : Type) :=
  | Left : A → either A B
  | Right : B → either A B.

  Record mod := {
    c_left :
      cmd;
    c_right :
      cmd;
    left_fun :
      store → either store nat;
    right_fun :
      store → either store nat;
    left_equiv_right:
      ∀ s₁ s₂,
        M.Equal s₁ s₂ →
        (∃ b₁ b₂, left_fun s₁ = Right b₁ ∧ right_fun s₂ = Right b₂)
        ∨ (∃ s₁' s₂', left_fun s₁ = Left s₁' ∧ right_fun s₂ = Left s₂'
                      ∧ M.Equal s₁' s₂');
    left_fun_spec_1 :
      ∀ s s', left_fun s = Left s' →
              ∃ n, nsteps υ n ([c_left], s) = Some ([], s');
    left_fun_spec_2 :
      ∀ s n, left_fun s = Right n →
             ∀ k, nsteps υ n (c_left::k, s) = None;
    right_fun_spec_1 :
      ∀ s s', right_fun s = Left s' →
              ∃ n, nsteps υ n ([c_right], s) = Some ([], s');
    right_fun_spec_2 :
      ∀ s n, right_fun s = Right n →
             ∀ k, nsteps υ n (c_right::k, s) = None
  }.

  Inductive _cont_mod : Type := .

  Definition _genv := unit.

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

  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 m km') ⇒
        match left_fun m (snd S₁), right_fun m (snd S₂) with
        | Right b₁, Right b₂ ⇒
          let (S₁', n₁) := nsteps' υ b₁ S₁ in
          let (S₂', n₂) := nsteps' υ b₂ S₂ in
          match (b₁ - n₁), (b₂ - n₂) with
          | O, O ⇒
            None
          | _, _ ⇒
            Some (Stuck S₁' S₂')
          end
        | Left s₁', Left s₂' ⇒
          Some (State (tl (fst S₁), s₁') (tl (fst S₂), s₂') km')
        | _, _ ⇒
          None
        end
      | Some (SpecialContStep _ km') ⇒
        None
      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.

  Inductive mod_invariant : cmd_mod mod → cmd → cmd → Prop :=
  | mod_id :
      ∀ c,
        mod_invariant Id c c
  | mod_rec_seq :
      ∀ m₁ m₂ c₁₁ c₁₂ c₂₁ c₂₂,
        mod_invariant m₁ c₁₁ c₂₁ →
        mod_invariant m₂ c₁₂ c₂₂ →
        mod_invariant (RecMod m₁ m₂) (Seq c₁₁ c₁₂) (Seq c₂₁ c₂₂)
  | mod_rec_ite :
      ∀ b m₁ m₂ c₁₁ c₁₂ c₂₁ c₂₂,
        mod_invariant m₁ c₁₁ c₂₁ →
        mod_invariant m₂ c₁₂ c₂₂ →
        mod_invariant (RecMod m₁ m₂) (ITE b c₁₁ c₁₂) (ITE b c₂₁ c₂₂)
  | mod_rec_while :
      ∀ b m m' c₁ c₂,
        mod_invariant m c₁ c₂ →
        mod_invariant (RecMod m m') (While b c₁) (While b c₂)
  | mod_special :
      ∀ m,
        mod_invariant (LeafMod m) (c_left m) (c_right m).

  Inductive km_invariant : list (cont_mod mod _cont_mod) → cont → cont → Prop :=
  | empty_cont_mod : km_invariant [] [] []
  | cmd_cont : ∀ c c' m km k₁ k₂,
      mod_invariant m c 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 _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 abstract_equiv_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.