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.