Library OracleLanguages.Imp.Oracles.CrashFixWhile

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

Module Make
       (Var_as_DT : UsualDecidableTypeOrig)
       (Import Lang : ImpProgrammingLanguage Var_as_DT)
       (Import OracleHelpers : ImpOracleHelpers Var_as_DT Lang).
  Record modif := {
    expression :
    bound :
    body :
      store nat;
       s, eval_exp s expression = Some bound
        nsteps υ (crash_bound s) (body::k', s) = None;

  Inductive _cont_mod : Type := .

  Definition _genv := unit.

  Inductive _state : Type :=
  | StuckLeft : state state _state
  | State : state state list (cont_mod modif _cont_mod) _state.

  Definition _step (_ : _genv) (S : _state) : option _state :=
    match S with
    | StuckLeft S₁ S₂
      step υ S₂ >>= λ S₂',
      Some (StuckLeft S₁ S₂')
    | State S₁ S₂ km
      match step_helper S₁ S₂ km with
      | None
      | Some StuckStep
      | Some (GenericStep S₁' S₂' km') ⇒
        Some (State S₁' S₂' km')
      | Some (SpecialCmdStep m km') ⇒
        eval_exp (snd S₂) (expression m) >>= λ val,
        if Z.eqb val (bound m) then
          step υ S₂ >>= λ S₂',
          let b := crash_bound m (snd S₁) in
          Some (StuckLeft (fst (nsteps' υ (Datatypes.S b) S₁)) S₂')
          step υ S₁ >>= λ S₁',
          step υ S₂ >>= λ S₂',
          match fst S₂ with | While b _ :: _Some b | _None end >>= λ b,
          eval_bexp (snd S₂) b >>= λ v,
          Some (State S₁' S₂'
                      (if v then
                         CmdMod Id :: CmdMod (LeafMod m) :: km'
      | Some (SpecialContStep _ km') ⇒

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

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

  Inductive mod_invariant : cmd_mod modif cmd cmd Prop :=
  | mod_id :
        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 :
        mod_invariant (LeafMod m)
                      (While (LE (expression m) (Int (bound m))) (body m))
                      (While (LT (expression m) (Int (bound m))) (body m))
  | mod_special' :
        mod_invariant (LeafMod m)
                      (While (LE (Int (bound m)) (expression m)) (body m))
                      (While (LT (Int (bound m)) (expression m)) (body m)).

  Inductive km_invariant : list (cont_mod modif _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
    | StuckLeft S₁ _step υ S₁ = None
    | State (k₁, s₁) (k₂, s₂) km
      km_invariant km k₁ k₂ M.Equal s₁ 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 crashfixwhile_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.