Library OracleLanguages.Imp.Oracles.CoreRHL


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₂},
        core_rhl_proof P c₁ c₂ Q
        proof_term
  | HoareProofL:
       {P Q c₁},
        core_rhl_proof P c₁ Skip Q
        proof_term
  | HoareProofR:
       {P Q c₂},
        core_rhl_proof P Skip 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
    | (@HoareProofL P' Q' _ _)::l'
    | (@HoareProofR P' Q' _ _)::l'
    | (@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)
  | proof_terms_match_cons_l :
       c₁ k₁ k₂ l P Q proof,
        proof_terms_match k₁ k₂ l
        proof_terms_match (c₁::k₁) k₂ (@HoareProofL P Q c₁ proof::l)
  | proof_terms_match_cons_r :
       k₁ c₂ k₂ l P Q proof,
        proof_terms_match k₁ k₂ l
        proof_terms_match k₁ (c₂::k₂) (@HoareProofR P Q 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₁ S₂ : state)
           (s : store)
           (H : core_rhl_proof P c₁ c₂ Q) (l' : list proof_term)
    : option _state :=
    match H with
    | CoreSkip P
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      Some (State S₁' S₂' s P l')
    | CoreAssign P x e₁ y e₂
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      eval_exp s e₂ >>= λ v₁,
      let s' := M.add y v₁ s in
      eval_exp s e₁ >>= λ v₂,
      Some (State S₁' S₂' (M.add x v₂ s') P l')
    | CoreAssert P b₁ b₂ Hb
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      Some (State S₁' S₂' s P l')
    | CoreSeq P Q R c₁₁ c₂₁ c₁₂ c₂₂ H₁ H₂
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      Some (State S₁' S₂' s P ((HoareProof H₁)::(HoareProof H₂)::l'))
    | CoreITE P Q b₁ b₂ c₁₁ c₂₁ c₁₂ c₂₂ H₁ H₂ Hb _
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      eval_bexp s b₁ >>= λ v,
      if v then
        Some (State S₁' S₂' s
                    (λ S, P S assertion_of_bexp b₁ S)
                    ((HoareProof H₁)::l'))
      else
        Some (State S₁' S₂' s
                    (λ S, P S assertion_of_bexp (NOT b₁) S)
                    ((HoareProof H₂)::l'))
    | CoreWhile P b₁ b₂ c₁ c₂ H Hb Hnc
      step υ S₁ >>= λ S₁',
      step υ S₂ >>= λ S₂',
      eval_bexp s b₁ >>= λ v,
      if v then
        Some (State S₁' S₂' s
                    (λ S, P S assertion_of_bexp b₁ S)
                    ((HoareProof H)::(HoareProof (CoreWhile P b₁ b₂ c₁ c₂ H Hb Hnc))::l'))
      else
        Some (State S₁' S₂' s
                    (λ S, P S assertion_of_bexp (NOT b₁) S)
                    l')
    | CoreSub P P' Q Q' c₁ c₂ H HP'P HQQ'
      _step_helper S₁ S₂ s H l'
    
    | CoreAssignLeft P Q x e _ H'
      step υ S₁ >>= λ S₁',
      eval_exp s e >>= λ v,
      Some (State S₁' S₂ (M.add x v s) P (HoareProofR H' :: l'))
    | CoreAssignRight P _ x e _ H'
      step υ S₂ >>= λ S₂',
      eval_exp s e >>= λ v,
      Some (State S₁ S₂' (M.add x v s) P (HoareProofL H' :: l'))
    | CoreAssertLeft P _ b _ H' _
      step υ S₁ >>= λ S₁',
      Some (State S₁' S₂ s P (HoareProofR H' :: l'))
    | CoreAssertRight P _ b _ H' _
      step υ S₂ >>= λ S₂',
      Some (State S₁ S₂' s P (HoareProofL H' :: l'))
    | CoreSeqSkipLeft P _ _ _ _ _ H₁ H₂
      step υ S₁ >>= λ S₁',
      Some (State S₁' S₂ s P (HoareProofL H₁ :: HoareProof H₂ :: l'))
    | CoreSeqSkipRight P Q R _ _ _ H₁ H₂
      step υ S₂ >>= λ S₂',
      Some (State S₁ S₂' s P (HoareProofR H₁ :: HoareProof H₂ :: l'))
    | CoreITELeft P Q b _ _ _ H₁ H₂ _
      step υ S₁ >>= λ S₁',
      eval_bexp s b >>= λ v,
      if v then
        Some (State S₁' S₂ s
                    (λ S, P S assertion_of_bexp b S)
                    ((HoareProof H₁)::l'))
      else
        Some (State S₁' S₂ s
                    (λ S, P S assertion_of_bexp (NOT b) S)
                    ((HoareProof H₂)::l'))
    | CoreITERight P Q b _ _ _ H₁ H₂ _
      step υ S₂ >>= λ S₂',
      eval_bexp s b >>= λ v,
      if v then
        Some (State S₁ S₂' s
                    (λ S, P S assertion_of_bexp b S)
                    ((HoareProof H₁)::l'))
      else
        Some (State S₁ S₂' s
                    (λ S, P S assertion_of_bexp (NOT b) S)
                    ((HoareProof H₂)::l'))
    end.

  Fixpoint _step_helper_left {P Q c₁ c₂}
           (S₁ S₂ : state)
           (s : store)
           
           (H : core_rhl_proof P c₁ c₂ Q)
           (l' : list proof_term)
    : option _state :=
    match H with
    | CoreSkip P
      step υ S₁ >>= λ S₁',
      Some (State S₁' S₂ s P l')
    | CoreSub P P' Q Q' c₁ Skip H HP'P HQQ'
      _step_helper_left S₁ S₂ s H l'
    
    | CoreAssignLeft P Q x e Skip H'
      step υ S₁ >>= λ S₁',
      eval_exp s e >>= λ v,
      
      Some (State S₁' S₂ (M.add x v s) Q l')
    | CoreAssertLeft P Q b Skip H' _
      step υ S₁ >>= λ S₁',
      
      Some (State S₁' S₂ s Q l')
    | CoreSeqSkipLeft P _ _ _ _ Skip H₁ H₂
      step υ S₁ >>= λ S₁',
      Some (State S₁' S₂ s P (HoareProofL H₁ :: HoareProofL H₂ :: l'))
    | CoreITELeft P Q b _ _ Skip H₁ H₂ _
      step υ S₁ >>= λ S₁',
      eval_bexp s b >>= λ v,
      if v then
        Some (State S₁' S₂ s
                    (λ S, P S assertion_of_bexp b S)
                    ((HoareProofL H₁)::l'))
      else
        Some (State S₁' S₂ s
                    (λ S, P S assertion_of_bexp (NOT b) S)
                    ((HoareProofL H₂)::l'))
    | _
      None
    end.

  Fixpoint _step_helper_right {P Q c₁ c₂}
           (S₁ S₂ : state)
           (s : store)
           
           (H : core_rhl_proof P c₁ c₂ Q)
           (l' : list proof_term)
    : option _state :=
    match H with
    | CoreSkip P
      step υ S₂ >>= λ S₂',
      Some (State S₁ S₂' s P l')
    | CoreSub P P' Q Q' Skip c₂ H HP'P HQQ'
      _step_helper_right S₁ S₂ s H l'
    
    | CoreAssignRight P Q x e Skip H'
      step υ S₂ >>= λ S₂',
      eval_exp s e >>= λ v,
      
      Some (State S₁ S₂' (M.add x v s) Q l')
    | CoreAssertRight P Q b Skip H' _
      step υ S₂ >>= λ S₂',
      
      Some (State S₁ S₂' s Q l')
    | CoreSeqSkipRight P _ _ Skip _ _ H₁ H₂
      step υ S₂ >>= λ S₂',
      Some (State S₁ S₂' s P (HoareProofR H₁ :: HoareProofR H₂ :: l'))
    | CoreITERight P Q b _ _ Skip H₁ H₂ _
      step υ S₂ >>= λ S₂',
      eval_bexp s b >>= λ v,
      if v then
        Some (State S₁ S₂' s
                    (λ S, P S assertion_of_bexp b S)
                    ((HoareProofR H₁)::l'))
      else
        Some (State S₁ S₂' s
                    (λ S, P S assertion_of_bexp (NOT b) S)
                    ((HoareProofR H₂)::l'))
    | _
      None
    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_helper S₁ S₂ s H l'
    | State S₁ S₂ s P (HoareProofL H::l') ⇒
      _step_helper_left S₁ S₂ s H l'
    | State S₁ S₂ s P (HoareProofR H::l') ⇒
      _step_helper_right S₁ S₂ s H 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 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 close_skip_skip:
     P Q s (H : core_rhl_proof P Skip Skip Q),
      P s Q s.

  Lemma _invariant_1:
     genv os os',
      _invariant genv os
      _step genv os = Some os'
      _invariant genv os'.

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

  Definition core_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 core_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
    core_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.