Library OracleLanguages.Imp.ImpDifferenceLanguage
A difference language for IMP.
Require Import DifferenceLanguage.
Require Import ReductionTrace.
Require Import ReductionTracesRelation.
Require Import Common.
Require Import Imp.Syntax.
Require Import Imp.Lang.
Require Import OracleLanguage.
Require Imp.Oracles.OracleHelpers.
Require Imp.Oracles.SwapAssign.
Require Imp.Oracles.SwapBranches.
Require Imp.Oracles.SeqAssoc.
Require Imp.Oracles.RefactorCommonBranchRemainder.
Require Imp.Oracles.Renaming.
Require Imp.Oracles.CrashFix.
Require Imp.Oracles.CrashFixWhile.
Require Imp.Oracles.ValueChange.
Require Imp.Oracles.CoreRHLSC.
Require Imp.Oracles.AbstractEquiv.
Module Make (Var_as_DT : UsualDecidableTypeOrig)
(Import Imp : ImpProgrammingLanguage Var_as_DT).
Definition imp := Imp.imp_language.
Import ProgrammingLanguage.
Import Imp.
Inductive imp_ctx :=
| CtxHole : imp_ctx
| CtxSeqL : imp_ctx → cmd → imp_ctx
| CtxSeqR : cmd → imp_ctx → imp_ctx
| CtxIfThen : bexp → imp_ctx → cmd → imp_ctx
| CtxIfElse : bexp → cmd → imp_ctx → imp_ctx
| CtxWhile : bexp → imp_ctx → imp_ctx.
Module OracleHelpers := Imp.Oracles.OracleHelpers.Make Var_as_DT Imp.
Import OracleHelpers.
Fixpoint cmd_mod_from_imp_ctx
(A : Type) (f : prog imp → prog imp → option A)
(P₁ P₂ : prog imp) (ctx : imp_ctx)
: option (cmd_mod A) :=
match ctx, P₁, P₂ with
| CtxHole, _, _ ⇒
f P₁ P₂ >>= λ m,
Some (LeafMod m)
| CtxSeqL ctx' c, Seq c₁₁ c₁₂, Seq c₂₁ c₂₂ ⇒
if beq_cmd c₁₂ c && beq_cmd c₂₂ c then
cmd_mod_from_imp_ctx A f c₁₁ c₂₁ ctx' >>= λ m',
Some (RecMod m' Id)
else
None
| CtxSeqR c ctx', Seq c₁₁ c₁₂, Seq c₂₁ c₂₂ ⇒
if beq_cmd c₁₁ c && beq_cmd c₂₁ c then
cmd_mod_from_imp_ctx A f c₁₂ c₂₂ ctx' >>= λ m',
Some (RecMod Id m')
else
None
| CtxIfThen b ctx' c, ITE b₁ c₁₁ c₁₂, ITE b₂ c₂₁ c₂₂ ⇒
if beq_bexp b₁ b && beq_bexp b₂ b && beq_cmd c₁₂ c && beq_cmd c₂₂ c then
cmd_mod_from_imp_ctx A f c₁₁ c₂₁ ctx' >>= λ m',
Some (RecMod m' Id)
else
None
| CtxIfElse b c ctx', ITE b₁ c₁₁ c₁₂, ITE b₂ c₂₁ c₂₂ ⇒
if beq_bexp b₁ b && beq_bexp b₂ b && beq_cmd c₁₁ c && beq_cmd c₂₁ c then
cmd_mod_from_imp_ctx A f c₁₂ c₂₂ ctx' >>= λ m',
Some (RecMod Id m')
else
None
| CtxWhile b ctx', While b₁ c₁, While b₂ c₂ ⇒
if beq_bexp b₁ b && beq_bexp b₂ b then
cmd_mod_from_imp_ctx A f c₁ c₂ ctx' >>= λ m',
Some (RecMod m' Id)
else
None
| _, _, _ ⇒
None
end.
Module AbstractEquiv := Imp.Oracles.AbstractEquiv.Make Var_as_DT Imp OracleHelpers.
Module SwapAssign := Imp.Oracles.SwapAssign.Make Var_as_DT Imp OracleHelpers.
Module SwapBranches := Imp.Oracles.SwapBranches.Make Var_as_DT Imp OracleHelpers.
Module SeqAssoc := Imp.Oracles.SeqAssoc.Make Var_as_DT Imp OracleHelpers.
Module RefactorCommonBranchRemainder :=
Imp.Oracles.RefactorCommonBranchRemainder.Make Var_as_DT Imp OracleHelpers.
Module CrashFix := Imp.Oracles.CrashFix.Make Var_as_DT Imp OracleHelpers.
Module CrashFixWhile :=
Imp.Oracles.CrashFixWhile.Make Var_as_DT Imp OracleHelpers.
Module Renaming := Imp.Oracles.Renaming.Make Var_as_DT Imp.
Module ValueChange := Imp.Oracles.ValueChange.Make Var_as_DT Imp.
Module CoreRHLSC := Imp.Oracles.CoreRHLSC.Make Var_as_DT Imp.
Import CoreRHLSC.RHL.
Inductive primitive_difference : Type :=
| SwapAssign : imp_ctx → primitive_difference
| SeqAssoc : imp_ctx → primitive_difference
| RefactorCommonBranchRemainder : imp_ctx → primitive_difference
| SwapBranches : imp_ctx → primitive_difference
| Renaming : Renaming.bijection varid varid → primitive_difference
| CrashFixWhile :
imp_ctx →
∀ (body : cmd) (e : exp) (bound : Z) (f : store → nat),
(∀ s, eval_exp s e = Some bound →
∀ k',
nsteps υ (f s) (body::k', s) = None) →
primitive_difference
| ValueChange : list varid → primitive_difference
| RHLProof : ∀ {P c₁ c₂ Q}, core_rhl_sc_proof P c₁ c₂ Q → primitive_difference
| Optimize : primitive_difference
| FixCrash : primitive_difference
| Refactor :
(configuration imp → configuration imp → Prop) →
primitive_difference.
Record oracle :=
{
OT: oracle_language imp imp;
genv: oracle_genv OT;
state: oracle_state OT
}.
Definition oracle_step (o : oracle) : option oracle :=
OracleLanguage.oracle_step (OT o) (genv o) (state o) >>= λ os',
Some {| OT := OT o; genv := genv o; state := os' |}.
Definition oracle_from_primitive_diff (p : primitive_difference) (P₁ P₂ : prog imp)
: option oracle :=
let '(genv₁, S₁) := initial_state imp P₁ in
let '(genv₂, S₂) := initial_state imp P₂ in
match p with
| SwapAssign ctx ⇒
cmd_mod_from_imp_ctx _ (λ _ _, Some SwapAssign.Swap) P₁ P₂ ctx >>= λ m,
let os := SwapAssign.State S₁ S₂ [CmdMod m] in
Some {| OT := SwapAssign.swapassign_oracle; genv := tt; state := os |}
| SeqAssoc ctx ⇒
let f := SeqAssoc.leaf_mod_of_cmds in
cmd_mod_from_imp_ctx _ f P₁ P₂ ctx >>= λ m,
let os := SeqAssoc.State S₁ S₂ [CmdMod m] in
Some {| OT := SeqAssoc.seqassoc_oracle; genv := tt; state := os |}
| SwapBranches ctx ⇒
let f := SwapBranches.leaf_mod_of_cmds in
cmd_mod_from_imp_ctx _ f P₁ P₂ ctx >>= λ m,
let os := SwapBranches.State S₁ S₂ [CmdMod m] in
Some {| OT := SwapBranches.swapbranches_oracle; genv := tt; state := os |}
| RefactorCommonBranchRemainder ctx ⇒
let f := λ (_ _ : prog imp), Some RefactorCommonBranchRemainder.Refactor in
cmd_mod_from_imp_ctx _ f P₁ P₂ ctx >>= λ m,
let os := RefactorCommonBranchRemainder.State S₁ S₂ [CmdMod m] in
Some {| OT := RefactorCommonBranchRemainder.refactor_common_branch_trailer_oracle;
genv := tt;
state := os |}
| ValueChange modified_vars ⇒
Some {| OT := ValueChange.valuechange_oracle;
genv := modified_vars;
state := ValueChange.State S₁ S₂ |}
| Renaming bij ⇒
Some {| OT := Renaming.renaming_oracle;
genv := bij;
state := Renaming.State S₁ S₂ |}
| CrashFixWhile ctx c e b f H ⇒
let m := {| CrashFixWhile.expression := e;
CrashFixWhile.bound := b;
CrashFixWhile.body := c;
CrashFixWhile.crash_bound := f;
CrashFixWhile.crash_avoided_1 := H |} in
let f := λ (_ _ : prog imp), Some m in
cmd_mod_from_imp_ctx _ f P₁ P₂ ctx >>= λ m,
let os := CrashFixWhile.State S₁ S₂ [CmdMod m] in
Some {| OT := CrashFixWhile.crashfixwhile_oracle;
genv := tt;
state := os |}
| @RHLProof P c₁ c₂ Q H ⇒
if beq_cmd P₁ c₁ && beq_cmd P₂ c₂ then
let os := CoreRHLSC.State S₁ S₂
(M.empty Z) P
[@CoreRHLSC.HoareProof P Q c₁ c₂ H] in
Some {| OT := CoreRHLSC.core_rhl_oracle;
genv := Q;
state := os |}
else
None
| _ ⇒
None
end.
Definition interpret_primitive_difference (p : primitive_difference)
: trace_relation imp imp :=
match p with
| SwapAssign _ | SeqAssoc _ | SwapBranches _ | RefactorCommonBranchRemainder _
| ValueChange _ | RHLProof _ | Renaming _
| CrashFixWhile _ _ _ _ _ _ ⇒
λ tr₁ tr₂,
∃ P₁ P₂ oracle,
oracle_from_primitive_diff p P₁ P₂ = Some oracle
∧ oracle_correlation_relation (OT oracle) (genv oracle) (state oracle) tr₁ tr₂
| Optimize ⇒
λ tr₁ tr₂, ∃ n₁ n₂,
trace' imp tr₁ ∧ trace' imp tr₂
∧ nsteps_converging_trace n₁ tr₁
∧ nsteps_converging_trace n₂ tr₂
∧ n₁ > n₂
| FixCrash ⇒
λ tr₁ tr₂, ∃ n₁,
trace' imp tr₁ ∧ trace' imp tr₂
∧ nsteps_crashing_trace n₁ tr₁
∧ ¬ (∃ n₂, nsteps_crashing_trace n₂ tr₂)
| Refactor γ ⇒
λ tr₁ tr₂,
(∀ x, γ x x) → (∀ x y, γ x y → γ y x) → (∀ x y z, γ x y → γ y z → γ x z) →
trace' imp tr₁ ∧ trace' imp tr₂
∧ gamma_correlated γ tr₁ tr₂
end.
Inductive t :=
| Compose : t → t → t
| Superpose : t → t → t
| Compare : primitive_difference → t.
Fixpoint interpret_difference (δ : t) : trace_relation imp imp :=
match δ with
| Compose δ₁ δ₂ ⇒
compose_trace_relations_externally _ _ _
(interpret_difference δ₁)
(interpret_difference δ₂)
| Superpose δ₁ δ₂ ⇒
λ tr₁ tr₂, interpret_difference δ₁ tr₁ tr₂ ∧ interpret_difference δ₂ tr₁ tr₂
| Compare δprim ⇒
interpret_primitive_difference δprim
end.
Definition imp_difference_language :=
{|
difference := t;
interpret := interpret_difference
|}.
End Make.