Library OracleLanguages.Imp.Oracles.MinimalRHL

Require Import Common.
Require Import Imp.Lang.
Require Import Imp.BigStep.
Require Import Imp.RHL.
Require Import Imp.DisjointStates.
Require Import ProgrammingLanguage.
Require Import OracleLanguage.
Require Import OracleHelpers.

Require Import Omega.

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

  Module BigStep := Imp.BigStep.Make Var_as_DT Lang.
  Module RHL := Imp.RHL.Make Var_as_DT Lang BigStep.
  Import RHL.
  Import Hoare.
  Import DisjointStates.

  Definition _genv : Type := assertion.
  Inductive proof_term :=
  | HoareProof:
      ∀ {P Q c₁ c₂},
        minimal_rhl_proof P c₁ c₂ Q →
        proof_term.

  Inductive _state :=
  | State :
      state →
      state →
      store →
      assertion →
      list proof_term →
      _state.

  Fixpoint proof_terms_consistent (l : list proof_term) (P Q : assertion) : Prop :=
    match l with
    | [] ⇒ P ⇒ Q
    | (@HoareProof P' Q' _ _ _)::l' ⇒
      P ⇒ P' ∧ proof_terms_consistent l' Q' Q
    end.

  Property proof_terms_consistent_1:
    ∀ l P P' Q,
      P ⇒ P' →
      proof_terms_consistent l P' Q →
      proof_terms_consistent l P Q.

  Inductive proof_terms_match : cont → cont → list proof_term → Prop :=
  | proof_terms_match_nil :
      proof_terms_match nil nil nil
  | proof_terms_match_cons :
      ∀ c₁ k₁ c₂ k₂ l P Q proof,
        proof_terms_match k₁ k₂ l →
        proof_terms_match (c₁::k₁) (c₂::k₂) (@HoareProof P Q c₁ c₂ proof::l).

  Hint Constructors proof_terms_match.

  Definition _invariant (Q : _genv) (os : _state) :=
    match os with
    | State S₁ S₂ s P l ⇒
      P s
      ∧ store_is_union s (snd S₁) (snd S₂)
      ∧ disjoint_states S₁ S₂
      ∧ proof_terms_consistent l P Q
      ∧ proof_terms_match (fst S₁) (fst S₂) l
    end.

  Fixpoint _step_helper {P Q c₁ c₂}
           (s : store)
           (H : minimal_rhl_proof P c₁ c₂ Q) (l' : list proof_term)
    : option (store × assertion × list proof_term) :=
    match H with
    | MinimalSkip P ⇒
      Some (s, P, l')
    | MinimalAssign P x e₁ y e₂ ⇒
      eval_exp s e₂ >>= λ v₁,
      let s' := M.add y v₁ s in
      eval_exp s e₁ >>= λ v₂,
      Some (M.add x v₂ s', P, l')
    | MinimalAssert P b₁ b₂ Hb ⇒
      
      Some (s, P, l')
    | MinimalSeq P Q R c₁₁ c₂₁ c₁₂ c₂₂ H₁ H₂ ⇒
      Some (s, P, (HoareProof H₁)::(HoareProof H₂)::l')
    | MinimalITE P Q b₁ b₂ c₁₁ c₂₁ c₁₂ c₂₂ H₁ H₂ Hb _ ⇒
      eval_bexp s b₁ >>= λ v,
      if v then
        Some (s,
              (λ S, P S ∧ assertion_of_bexp b₁ S),
              (HoareProof H₁)::l')
      else
        Some (s,
              (λ S, P S ∧ assertion_of_bexp (NOT b₁) S),
              (HoareProof H₂)::l')
    | MinimalWhile P b₁ b₂ c₁ c₂ H Hb Hnc ⇒
      eval_bexp s b₁ >>= λ v,
      if v then
        Some (s,
              (λ S, P S ∧ assertion_of_bexp b₁ S),
              (HoareProof H)::(HoareProof (MinimalWhile P b₁ b₂ c₁ c₂ H Hb Hnc))::l')
      else
        Some (s,
              (λ S, P S ∧ assertion_of_bexp (NOT b₁) S),
              l')
    | MinimalSub P P' Q Q' c₁ c₂ H HP'P HQQ' ⇒
      _step_helper s H l'
    end.

  Definition _step (_ : _genv) (S : _state) : option _state :=
    match S with
    | State S₁ S₂ s P [] ⇒
      
      None
    | State S₁ S₂ s P (HoareProof H::l') ⇒
      
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      _step_helper s H l' >>= λ res,
      let '(s', P', l') := res in
      Some (State S₁' S₂' s' P' l')
    end.

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

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

  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 _invariant_1:
    ∀ genv os os',
      _invariant genv os →
      _step genv os = Some os' →
      _invariant genv os'.

  Lemma no_crash :
    ∀ genv S₁ S₂ s P₀ H₀ l,
      _invariant genv (State S₁ S₂ s P₀ (H₀::l)) →
      ∃ os', _step genv (State S₁ S₂ s P₀ (H₀::l)) = Some os'.

  Lemma _prediction_completeness :
    ∀ genv os,
      _invariant genv os →
      _step genv os = None →
      step υ (_left_state os) = None
      ∧ step υ (_right_state os) = None.

  Definition minimal_rhl_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
    |}.

  Import BigStep.

  Lemma state_final_nocrash:
    ∀ genv os,
      _invariant genv os →
      let S₁ := _left_state os in
      let S₂ := _right_state os in
      step υ S₁ = None →
      step υ S₂ = None →
      ∃ v₁ v₂, state_final S₁ = Some v₁ ∧ state_final S₂ = Some v₂.

  Lemma minimal_rhl_soundness:
    ∀ c₁ s₁ c₂ s₂,
    terminates υ ([c₁], s₁) →
    terminates υ ([c₂], s₂) →
    ∀ s (P Q : assertion),
    store_is_union s s₁ s₂ →
    disjoint_states ([c₁], s₁) ([c₂], s₂) →
    P s →
    minimal_rhl_proof P c₁ c₂ Q →
    ∃ s' s₁' s₂',
      s₁ ⊢ c₁ ⇓ s₁'
    ∧ s₂ ⊢ c₂ ⇓ s₂'
    ∧ store_is_union s' s₁' s₂' ∧ Q s'.
End Make.