Library CoqDefs
Require Import Utf8.
Require Import ZArith.
Require Import List.
Import ListNotations.
Require Import Bool.
Require Import Equalities.
Require Import FMapWeakList.
Require Import FMapFacts.
Definition ret {A : Type} (x : A) := Some x.
Definition bind {A B : Type} (a : option A) (f : A → option B) :=
match a with
| None ⇒ None
| Some x ⇒ f x
end.
Notation "a >>= f" := (bind a f) (at level 40, left associativity).
Module Languages (Var_as_DT : UsualDecidableTypeOrig).
Module VarMap := FMapWeakList.Make(Var_as_DT).
Module VarMapFacts := FMapFacts.WFacts_fun Var_as_DT VarMap.
Module VarMapProps := FMapFacts.WProperties_fun Var_as_DT VarMap.
Definition var := Var_as_DT.t.
Require Import ZArith.
Require Import List.
Import ListNotations.
Require Import Bool.
Require Import Equalities.
Require Import FMapWeakList.
Require Import FMapFacts.
Definition ret {A : Type} (x : A) := Some x.
Definition bind {A B : Type} (a : option A) (f : A → option B) :=
match a with
| None ⇒ None
| Some x ⇒ f x
end.
Notation "a >>= f" := (bind a f) (at level 40, left associativity).
Module Languages (Var_as_DT : UsualDecidableTypeOrig).
Module VarMap := FMapWeakList.Make(Var_as_DT).
Module VarMapFacts := FMapFacts.WFacts_fun Var_as_DT VarMap.
Module VarMapProps := FMapFacts.WProperties_fun Var_as_DT VarMap.
Definition var := Var_as_DT.t.
Lvalues
Abstract syntax of expressions
with exp :=
| Lval : lvalue → exp
| Int : Z → exp
| Sum : exp → exp → exp
| Diff : exp → exp → exp
| Mult : exp → exp → exp
| Div : exp → exp → exp.
Scheme exp_mut := Induction for exp Sort Prop
with lvalue_mut := Induction for lvalue Sort Prop.
Fixpoint exp_beq (e e' : exp) : bool :=
match e, e' with
| Lval x, Lval y ⇒ if lvalue_beq x y then true else false
| Int n, Int n' ⇒ Zeq_bool n n'
| Sum e₁ e₂, Sum e₁' e₂' | Diff e₁ e₂, Diff e₁' e₂'
| Mult e₁ e₂, Mult e₁' e₂' ⇒ andb (exp_beq e₁ e₁') (exp_beq e₂ e₂')
| _, _ ⇒ false
end
with lvalue_beq (x y : lvalue) : bool :=
match x, y with
| Var x, Var y ⇒ if Var_as_DT.eq_dec x y then true else false
| ArrayAccess x n, ArrayAccess y n' ⇒ andb (lvalue_beq x y) (exp_beq n n')
| _, _ ⇒ false
end.
| Lval : lvalue → exp
| Int : Z → exp
| Sum : exp → exp → exp
| Diff : exp → exp → exp
| Mult : exp → exp → exp
| Div : exp → exp → exp.
Scheme exp_mut := Induction for exp Sort Prop
with lvalue_mut := Induction for lvalue Sort Prop.
Fixpoint exp_beq (e e' : exp) : bool :=
match e, e' with
| Lval x, Lval y ⇒ if lvalue_beq x y then true else false
| Int n, Int n' ⇒ Zeq_bool n n'
| Sum e₁ e₂, Sum e₁' e₂' | Diff e₁ e₂, Diff e₁' e₂'
| Mult e₁ e₂, Mult e₁' e₂' ⇒ andb (exp_beq e₁ e₁') (exp_beq e₂ e₂')
| _, _ ⇒ false
end
with lvalue_beq (x y : lvalue) : bool :=
match x, y with
| Var x, Var y ⇒ if Var_as_DT.eq_dec x y then true else false
| ArrayAccess x n, ArrayAccess y n' ⇒ andb (lvalue_beq x y) (exp_beq n n')
| _, _ ⇒ false
end.
Abstract syntax of boolean expressions
Inductive bexp :=
| BTrue : bexp
| BFalse : bexp
| BAnd : bexp → bexp → bexp
| BOr : bexp → bexp → bexp
| BNot : bexp → bexp
| BLE : exp → exp → bexp
| BGE : exp → exp → bexp
| BLT : exp → exp → bexp
| BGT : exp → exp → bexp
| BEQ : exp → exp → bexp
| BNEQ : exp → exp → bexp.
| BTrue : bexp
| BFalse : bexp
| BAnd : bexp → bexp → bexp
| BOr : bexp → bexp → bexp
| BNot : bexp → bexp
| BLE : exp → exp → bexp
| BGE : exp → exp → bexp
| BLT : exp → exp → bexp
| BGT : exp → exp → bexp
| BEQ : exp → exp → bexp
| BNEQ : exp → exp → bexp.
Abstract syntax of commands
Inductive cmd_a :=
| Skip | Break | Continue
| Assign : lvalue → exp → cmd_a.
Fixpoint cmda_beq (a a' : cmd_a) : bool :=
match a, a' with
| Skip, Skip | Continue, Continue | Break, Break ⇒ true
| Assign x e, Assign y e' ⇒ andb (lvalue_beq x y) (exp_beq e e')
| _, _ ⇒ false
end.
Inductive cmd :=
| Leaf : cmd_a → cmd
| Seq : cmd → cmd → cmd
| While : bexp → cmd → cmd
| IfThenElse : bexp → cmd → cmd → cmd.
Inductive value :=
| IntValue : Z → value
| ArrayValue : list value → value.
Definition store := VarMap.t value.
Definition z_to_nat (n : Z) : option nat :=
match n with
| Z0 ⇒ Some 0
| Zpos p ⇒ Some (Pos.to_nat p)
| _ ⇒ None
end.
Fixpoint my_nth {A : Type} (n : nat) (l : list A) : option A :=
match n, l with
| O, x::_ ⇒ Some x
| S n', _::l' ⇒ my_nth n' l'
| _, _ ⇒ None
end.
Property my_nth_implies_nth:
∀ {A} (l : list A) n (x : A), my_nth n l = Some x →
∀ y, nth n l y = x.
Proof.
intros A l n. revert l. induction n ; intro l.
× intros x H. simpl in H. destruct l.
+ discriminate H.
+ inversion_clear H. simpl. auto.
× intros x H. destruct l.
+ discriminate H.
+ apply IHn. simpl in H. auto.
Qed.
| Skip | Break | Continue
| Assign : lvalue → exp → cmd_a.
Fixpoint cmda_beq (a a' : cmd_a) : bool :=
match a, a' with
| Skip, Skip | Continue, Continue | Break, Break ⇒ true
| Assign x e, Assign y e' ⇒ andb (lvalue_beq x y) (exp_beq e e')
| _, _ ⇒ false
end.
Inductive cmd :=
| Leaf : cmd_a → cmd
| Seq : cmd → cmd → cmd
| While : bexp → cmd → cmd
| IfThenElse : bexp → cmd → cmd → cmd.
Inductive value :=
| IntValue : Z → value
| ArrayValue : list value → value.
Definition store := VarMap.t value.
Definition z_to_nat (n : Z) : option nat :=
match n with
| Z0 ⇒ Some 0
| Zpos p ⇒ Some (Pos.to_nat p)
| _ ⇒ None
end.
Fixpoint my_nth {A : Type} (n : nat) (l : list A) : option A :=
match n, l with
| O, x::_ ⇒ Some x
| S n', _::l' ⇒ my_nth n' l'
| _, _ ⇒ None
end.
Property my_nth_implies_nth:
∀ {A} (l : list A) n (x : A), my_nth n l = Some x →
∀ y, nth n l y = x.
Proof.
intros A l n. revert l. induction n ; intro l.
× intros x H. simpl in H. destruct l.
+ discriminate H.
+ inversion_clear H. simpl. auto.
× intros x H. destruct l.
+ discriminate H.
+ apply IHn. simpl in H. auto.
Qed.
Interpretation of an expression e in a store s.
Returns None if the expression could not be evaluated within this
store. Returns Some v with v the result of the evaluation of e
in s otherwise.
Fixpoint interp_exp (e : exp) (s : store) : option Z :=
match e with
| Int n ⇒ ret n
| Lval x ⇒ read_lval x s >>= λ x, match x with
| IntValue n ⇒ Some n
| _ ⇒ None
end
| Sum e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x + y)%Z
| Diff e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x - y)%Z
| Mult e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x × y)%Z
| Div e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x / y)%Z
end
with read_lval (x : lvalue) (s : store) : option value :=
match x with
| Var x ⇒ VarMap.find x s
| ArrayAccess x n ⇒
interp_exp n s >>= λ idx,
read_lval x s >>= λ value,
match value with
| ArrayValue l ⇒
z_to_nat idx >>= λ n,
my_nth n l
| _ ⇒ None
end
end.
Fixpoint set_lval (x : lvalue) (v : value) (s : store) : option store :=
match x with
| Var x ⇒ Some (VarMap.add x v s)
| ArrayAccess x n ⇒
interp_exp n s >>= λ idx,
read_lval x s >>= λ value,
match value with
| ArrayValue l ⇒
z_to_nat idx >>= λ n,
let v' := (firstn n l) ++ [v] ++ (skipn (S n) l) in
set_lval x (ArrayValue v') s
| _ ⇒ None
end
end.
match e with
| Int n ⇒ ret n
| Lval x ⇒ read_lval x s >>= λ x, match x with
| IntValue n ⇒ Some n
| _ ⇒ None
end
| Sum e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x + y)%Z
| Diff e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x - y)%Z
| Mult e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x × y)%Z
| Div e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (x / y)%Z
end
with read_lval (x : lvalue) (s : store) : option value :=
match x with
| Var x ⇒ VarMap.find x s
| ArrayAccess x n ⇒
interp_exp n s >>= λ idx,
read_lval x s >>= λ value,
match value with
| ArrayValue l ⇒
z_to_nat idx >>= λ n,
my_nth n l
| _ ⇒ None
end
end.
Fixpoint set_lval (x : lvalue) (v : value) (s : store) : option store :=
match x with
| Var x ⇒ Some (VarMap.add x v s)
| ArrayAccess x n ⇒
interp_exp n s >>= λ idx,
read_lval x s >>= λ value,
match value with
| ArrayValue l ⇒
z_to_nat idx >>= λ n,
let v' := (firstn n l) ++ [v] ++ (skipn (S n) l) in
set_lval x (ArrayValue v') s
| _ ⇒ None
end
end.
Interpretation of a boolean expression b in a store s.
Returns None if the expression could not be evaluated within this
store. Returns Some v with v the result of the evaluation of b
in s otherwise.
Fixpoint interp_bexp (b : bexp) (s : store) : option bool :=
match b with
| BTrue ⇒ ret true
| BFalse ⇒ ret false
| BAnd b₁ b₂ ⇒
interp_bexp b₁ s >>= λ x, interp_bexp b₂ s >>= λ y, ret (x && y)
| BOr b₁ b₂ ⇒
interp_bexp b₁ s >>= λ x, interp_bexp b₂ s >>= λ y, ret (x || y)
| BNot b ⇒
interp_bexp b s >>= λ x, ret (negb x)
| BLE e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.leb x y)
| BGE e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.geb x y)
| BLT e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.ltb x y)
| BGT e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.gtb x y)
| BEQ e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.eqb x y)
| BNEQ e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (negb (Z.eqb x y))
end.
match b with
| BTrue ⇒ ret true
| BFalse ⇒ ret false
| BAnd b₁ b₂ ⇒
interp_bexp b₁ s >>= λ x, interp_bexp b₂ s >>= λ y, ret (x && y)
| BOr b₁ b₂ ⇒
interp_bexp b₁ s >>= λ x, interp_bexp b₂ s >>= λ y, ret (x || y)
| BNot b ⇒
interp_bexp b s >>= λ x, ret (negb x)
| BLE e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.leb x y)
| BGE e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.geb x y)
| BLT e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.ltb x y)
| BGT e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.gtb x y)
| BEQ e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (Z.eqb x y)
| BNEQ e₁ e₂ ⇒
interp_exp e₁ s >>= λ x, interp_exp e₂ s >>= λ y, ret (negb (Z.eqb x y))
end.
Execution mode used in the big-step semantics of the input language to
denote the different TODO
Big-step semantics of the input language
Inductive big_step : store → cmd → mode → store → Prop :=
| j_assign : ∀ x e v s s',
interp_exp e s = Some v →
set_lval x (IntValue v) s = Some s' →
big_step s (Leaf (Assign x e)) MNormal s'
| j_skip : ∀ s,
big_step s (Leaf Skip) MNormal s
| j_seq_normal : ∀ s m c₁ s₁ c₂ s',
big_step s c₁ MNormal s₁ →
big_step s₁ c₂ m s' →
big_step s (Seq c₁ c₂) m s'
| j_if_then : ∀ s m s' b c₁ c₂,
interp_bexp b s = Some true →
big_step s c₁ m s' →
big_step s (IfThenElse b c₁ c₂) m s'
| j_if_else : ∀ s m s' b c₁ c₂,
interp_bexp b s = Some false →
big_step s c₂ m s' →
big_step s (IfThenElse b c₁ c₂) m s'
| j_while_false : ∀ s b c,
interp_bexp b s = Some false →
big_step s (While b c) MNormal s
| j_while_true : ∀ s m s₁ s' b c₁,
interp_bexp b s = Some true →
big_step s c₁ m s₁ →
m ≠ MBreak →
big_step s₁ (While (b) c₁) MNormal s' →
big_step s (While (b) c₁) MNormal s'
| j_seq_interrupt : ∀ s c₁ c₂ m s',
m ≠ MNormal →
big_step s c₁ m s' →
big_step s (Seq c₁ c₂) m s'
| j_while_break : ∀ s s₁ b c₁,
interp_bexp b s = Some true →
big_step s c₁ MBreak s₁ →
big_step s (While (b) c₁) MNormal s₁
| j_break : ∀ s, big_step s (Leaf Break) MBreak s
| j_continue : ∀ s, big_step s (Leaf Continue) MContinue s.
Hint Constructors big_step.
Inductive guard :=
| ε : guard
| S0 : guard → guard
| S1 : guard → guard.
Lemma eq_guard_dec:
∀ (x y : guard), { x = y } + {x ≠ y }.
Proof.
decide equality.
Defined.
Module guard_as_DT <: DecidableType.
Definition t := guard.
Definition eq := @eq guard.
Definition eq_refl := @eq_refl t.
Definition eq_sym := @eq_sym t.
Definition eq_trans := @eq_trans t.
Definition eq_dec := eq_guard_dec.
End guard_as_DT.
Module GuardMap := FMapWeakList.Make(guard_as_DT).
Module GuardMapFacts := FMapFacts.WFacts_fun guard_as_DT GuardMap.
Module GuardMapProps := FMapFacts.WProperties_fun guard_as_DT GuardMap.
Definition gstore := GuardMap.t bool.
Definition path := guard.
Inductive path_suffix : path → path → Prop :=
| suffix_eq : ∀ s, path_suffix s s
| suffix_S0 : ∀ p s, path_suffix p s → path_suffix (S0 p) s
| suffix_S1 : ∀ p s, path_suffix p s → path_suffix (S1 p) s.
Hint Constructors path_suffix.
Definition guard_conj := list (bool × guard).
Definition guard_disj := list guard_conj.
Inductive acmd_g :=
| GAAssign : lvalue → exp → acmd_g
| GAGAssign : guard → bexp → acmd_g.
Inductive cmd_g :=
| GSeq : cmd_g → cmd_g → cmd_g
| GSkip : cmd_g
| GWhile : guard_disj → cmd_g → cmd_g
| GAtomic : guard_conj → acmd_g → cmd_g
| GCPoint : cmd_g.
Notation "A ; B" := (Seq A B)
(at level 80, right associativity, format "A ; '//' B") : ast_scope.
Notation "A ; B" := (GSeq A B)
(at level 80, right associativity, format "A ; '//' B") : gast_scope.
Delimit Scope ast_scope with AST.
Delimit Scope gast_scope with GAST.
Fixpoint interp_guard_conj G gl :=
match gl with
| [] ⇒ Some true
| (b, π)::gl' ⇒ GuardMap.find π G >>= λ v,
if eqb v b then interp_guard_conj G gl' else Some false
end.
Definition guard_conj_evals_to G gl b :=
interp_guard_conj G gl = Some b.
Definition guard_disj_evals_to G cl b :=
match b with
| true ⇒ List.Exists (λ gl, guard_conj_evals_to G gl true) cl
| false ⇒ List.Forall (λ gl, guard_conj_evals_to G gl false) cl
end.
Inductive big_step_g : store → gstore → cmd_g → store → gstore → Prop :=
| j_gatomic_false : ∀ a s gs l,
guard_conj_evals_to gs l false →
big_step_g s gs (GAtomic l a) s gs
| j_gassign : ∀ x e v s s' gs l,
interp_exp e s = Some v →
set_lval x (IntValue v) s = Some s' →
guard_conj_evals_to gs l true →
big_step_g s gs (GAtomic l (GAAssign x e)) s' gs
| j_ggassign : ∀ g b v s gs l,
interp_bexp b s = Some v →
guard_conj_evals_to gs l true →
big_step_g s gs (GAtomic l (GAGAssign g b)) s (GuardMap.add g v gs)
| j_gskip : ∀ s gs,
big_step_g s gs GSkip s gs
| j_gseq : ∀ s gs c₁ s₁ gs₁ c₂ s' gs',
big_step_g s gs c₁ s₁ gs₁ →
big_step_g s₁ gs₁ c₂ s' gs' →
big_step_g s gs (GSeq c₁ c₂) s' gs'
| j_gwhile_false : ∀ s gs cl c,
guard_disj_evals_to gs cl false →
big_step_g s gs (GWhile cl c) s gs
| j_gwhile_true : ∀ s gs s₁ gs₁ s' gs' cl c₁,
guard_disj_evals_to gs cl true →
big_step_g s gs c₁ s₁ gs₁ →
big_step_g s₁ gs₁ (GWhile cl c₁) s' gs' →
big_step_g s gs (GWhile cl c₁) s' gs'
| j_gcpoint : ∀ s gs,
big_step_g s gs GCPoint s gs.
Inductive cmd_diff :=
| SeqDelL : cmd → cmd_diff → cmd_diff
| SeqDelR : cmd_diff → cmd → cmd_diff
| SeqInsL : cmd → cmd_diff → cmd_diff
| SeqInsR : cmd_diff → cmd → cmd_diff
| SeqMut : cmd_diff → cmd_diff → cmd_diff
| IfMut : bexp × bexp → cmd_diff → cmd_diff → cmd_diff
| WhileMut : bexp × bexp → cmd_diff → cmd_diff
| ITEAddIf : bexp → cmd → cmd_diff → cmd_diff
| ITEAddElse : bexp → cmd_diff → cmd → cmd_diff
| ITEDelIf : bexp → cmd → cmd_diff → cmd_diff
| ITEDelElse : bexp → cmd_diff → cmd → cmd_diff
| WhileAdd : bexp → cmd_diff → cmd_diff
| WhileDel : bexp → cmd_diff → cmd_diff
| LeafSubst : cmd_a → cmd_a → cmd_diff
| CPoint : cmd_diff → cmd_diff.
Fixpoint Π₀ (cd : cmd_diff) : cmd :=
match cd with
| SeqDelL c cd ⇒ (c ; (Π₀ cd))%AST
| SeqDelR cd c ⇒ ((Π₀ cd) ; c)%AST
| SeqInsL _ c ⇒ Π₀ c
| SeqInsR c _ ⇒ Π₀ c
| SeqMut c c' ⇒ ((Π₀ c) ; (Π₀ c'))%AST
| IfMut (b, _) c c' ⇒ IfThenElse b (Π₀ c) (Π₀ c')
| WhileMut (b, _) c ⇒ While b (Π₀ c)
| ITEAddIf _ _ c' ⇒ Π₀ c'
| ITEAddElse _ c _ ⇒ Π₀ c
| ITEDelIf b c c' ⇒ IfThenElse b c (Π₀ c')
| ITEDelElse b c c' ⇒ IfThenElse b (Π₀ c) c'
| WhileAdd b c ⇒ Π₀ c
| WhileDel b c ⇒ While b (Π₀ c)
| LeafSubst a _ ⇒ Leaf a
| CPoint cd ⇒ Π₀ cd
end.
Fixpoint Π₁ (cd : cmd_diff) : cmd :=
match cd with
| SeqDelL c cd ⇒ (Π₁ cd)
| SeqDelR cd c ⇒ (Π₁ cd)
| SeqInsL c cd ⇒ (c ; (Π₁ cd))%AST
| SeqInsR cd c' ⇒ ((Π₁ cd) ; c')%AST
| SeqMut c c' ⇒ ((Π₁ c) ; (Π₁ c'))%AST
| IfMut (_, b') c c' ⇒ IfThenElse b' (Π₁ c) (Π₁ c')
| WhileMut (_, b') c ⇒ While b' (Π₁ c)
| ITEAddIf b c c' ⇒ IfThenElse b c (Π₁ c')
| ITEAddElse b c c' ⇒ IfThenElse b (Π₁ c) c'
| ITEDelIf _ _ c' ⇒ Π₁ c'
| ITEDelElse _ c _ ⇒ Π₁ c
| WhileAdd b c ⇒ While b (Π₁ c)
| WhileDel b c ⇒ Π₁ c
| LeafSubst _ a ⇒ Leaf a
| CPoint cd ⇒ Π₁ cd
end.
Definition tag_store t (s : store) :=
VarMap.fold (λ k v acc, VarMap.add (t k) v acc) s (VarMap.empty _).
Definition store_included_tagged t (s s' : store) :=
∀ x v, VarMap.MapsTo x v s → VarMap.MapsTo (t x) v s'.
Definition join_stores t t' S₀ S₁ :=
VarMapProps.update (tag_store t S₀) (tag_store t' S₁).
Definition cp_algorithm_sound t t' correlating_program :=
∀ S₀ S₀' S₁ S₁' cd,
big_step S₀ (Π₀ cd) MNormal S₀' →
big_step S₁ (Π₁ cd) MNormal S₁' →
∀ G, ∃ S' G',
big_step_g (join_stores t t' S₀ S₁) G (correlating_program cd) S' G'
∧ store_included_tagged t S₀' S' ∧ store_included_tagged t' S₁' S'.
End Languages.
| j_assign : ∀ x e v s s',
interp_exp e s = Some v →
set_lval x (IntValue v) s = Some s' →
big_step s (Leaf (Assign x e)) MNormal s'
| j_skip : ∀ s,
big_step s (Leaf Skip) MNormal s
| j_seq_normal : ∀ s m c₁ s₁ c₂ s',
big_step s c₁ MNormal s₁ →
big_step s₁ c₂ m s' →
big_step s (Seq c₁ c₂) m s'
| j_if_then : ∀ s m s' b c₁ c₂,
interp_bexp b s = Some true →
big_step s c₁ m s' →
big_step s (IfThenElse b c₁ c₂) m s'
| j_if_else : ∀ s m s' b c₁ c₂,
interp_bexp b s = Some false →
big_step s c₂ m s' →
big_step s (IfThenElse b c₁ c₂) m s'
| j_while_false : ∀ s b c,
interp_bexp b s = Some false →
big_step s (While b c) MNormal s
| j_while_true : ∀ s m s₁ s' b c₁,
interp_bexp b s = Some true →
big_step s c₁ m s₁ →
m ≠ MBreak →
big_step s₁ (While (b) c₁) MNormal s' →
big_step s (While (b) c₁) MNormal s'
| j_seq_interrupt : ∀ s c₁ c₂ m s',
m ≠ MNormal →
big_step s c₁ m s' →
big_step s (Seq c₁ c₂) m s'
| j_while_break : ∀ s s₁ b c₁,
interp_bexp b s = Some true →
big_step s c₁ MBreak s₁ →
big_step s (While (b) c₁) MNormal s₁
| j_break : ∀ s, big_step s (Leaf Break) MBreak s
| j_continue : ∀ s, big_step s (Leaf Continue) MContinue s.
Hint Constructors big_step.
Inductive guard :=
| ε : guard
| S0 : guard → guard
| S1 : guard → guard.
Lemma eq_guard_dec:
∀ (x y : guard), { x = y } + {x ≠ y }.
Proof.
decide equality.
Defined.
Module guard_as_DT <: DecidableType.
Definition t := guard.
Definition eq := @eq guard.
Definition eq_refl := @eq_refl t.
Definition eq_sym := @eq_sym t.
Definition eq_trans := @eq_trans t.
Definition eq_dec := eq_guard_dec.
End guard_as_DT.
Module GuardMap := FMapWeakList.Make(guard_as_DT).
Module GuardMapFacts := FMapFacts.WFacts_fun guard_as_DT GuardMap.
Module GuardMapProps := FMapFacts.WProperties_fun guard_as_DT GuardMap.
Definition gstore := GuardMap.t bool.
Definition path := guard.
Inductive path_suffix : path → path → Prop :=
| suffix_eq : ∀ s, path_suffix s s
| suffix_S0 : ∀ p s, path_suffix p s → path_suffix (S0 p) s
| suffix_S1 : ∀ p s, path_suffix p s → path_suffix (S1 p) s.
Hint Constructors path_suffix.
Definition guard_conj := list (bool × guard).
Definition guard_disj := list guard_conj.
Inductive acmd_g :=
| GAAssign : lvalue → exp → acmd_g
| GAGAssign : guard → bexp → acmd_g.
Inductive cmd_g :=
| GSeq : cmd_g → cmd_g → cmd_g
| GSkip : cmd_g
| GWhile : guard_disj → cmd_g → cmd_g
| GAtomic : guard_conj → acmd_g → cmd_g
| GCPoint : cmd_g.
Notation "A ; B" := (Seq A B)
(at level 80, right associativity, format "A ; '//' B") : ast_scope.
Notation "A ; B" := (GSeq A B)
(at level 80, right associativity, format "A ; '//' B") : gast_scope.
Delimit Scope ast_scope with AST.
Delimit Scope gast_scope with GAST.
Fixpoint interp_guard_conj G gl :=
match gl with
| [] ⇒ Some true
| (b, π)::gl' ⇒ GuardMap.find π G >>= λ v,
if eqb v b then interp_guard_conj G gl' else Some false
end.
Definition guard_conj_evals_to G gl b :=
interp_guard_conj G gl = Some b.
Definition guard_disj_evals_to G cl b :=
match b with
| true ⇒ List.Exists (λ gl, guard_conj_evals_to G gl true) cl
| false ⇒ List.Forall (λ gl, guard_conj_evals_to G gl false) cl
end.
Inductive big_step_g : store → gstore → cmd_g → store → gstore → Prop :=
| j_gatomic_false : ∀ a s gs l,
guard_conj_evals_to gs l false →
big_step_g s gs (GAtomic l a) s gs
| j_gassign : ∀ x e v s s' gs l,
interp_exp e s = Some v →
set_lval x (IntValue v) s = Some s' →
guard_conj_evals_to gs l true →
big_step_g s gs (GAtomic l (GAAssign x e)) s' gs
| j_ggassign : ∀ g b v s gs l,
interp_bexp b s = Some v →
guard_conj_evals_to gs l true →
big_step_g s gs (GAtomic l (GAGAssign g b)) s (GuardMap.add g v gs)
| j_gskip : ∀ s gs,
big_step_g s gs GSkip s gs
| j_gseq : ∀ s gs c₁ s₁ gs₁ c₂ s' gs',
big_step_g s gs c₁ s₁ gs₁ →
big_step_g s₁ gs₁ c₂ s' gs' →
big_step_g s gs (GSeq c₁ c₂) s' gs'
| j_gwhile_false : ∀ s gs cl c,
guard_disj_evals_to gs cl false →
big_step_g s gs (GWhile cl c) s gs
| j_gwhile_true : ∀ s gs s₁ gs₁ s' gs' cl c₁,
guard_disj_evals_to gs cl true →
big_step_g s gs c₁ s₁ gs₁ →
big_step_g s₁ gs₁ (GWhile cl c₁) s' gs' →
big_step_g s gs (GWhile cl c₁) s' gs'
| j_gcpoint : ∀ s gs,
big_step_g s gs GCPoint s gs.
Inductive cmd_diff :=
| SeqDelL : cmd → cmd_diff → cmd_diff
| SeqDelR : cmd_diff → cmd → cmd_diff
| SeqInsL : cmd → cmd_diff → cmd_diff
| SeqInsR : cmd_diff → cmd → cmd_diff
| SeqMut : cmd_diff → cmd_diff → cmd_diff
| IfMut : bexp × bexp → cmd_diff → cmd_diff → cmd_diff
| WhileMut : bexp × bexp → cmd_diff → cmd_diff
| ITEAddIf : bexp → cmd → cmd_diff → cmd_diff
| ITEAddElse : bexp → cmd_diff → cmd → cmd_diff
| ITEDelIf : bexp → cmd → cmd_diff → cmd_diff
| ITEDelElse : bexp → cmd_diff → cmd → cmd_diff
| WhileAdd : bexp → cmd_diff → cmd_diff
| WhileDel : bexp → cmd_diff → cmd_diff
| LeafSubst : cmd_a → cmd_a → cmd_diff
| CPoint : cmd_diff → cmd_diff.
Fixpoint Π₀ (cd : cmd_diff) : cmd :=
match cd with
| SeqDelL c cd ⇒ (c ; (Π₀ cd))%AST
| SeqDelR cd c ⇒ ((Π₀ cd) ; c)%AST
| SeqInsL _ c ⇒ Π₀ c
| SeqInsR c _ ⇒ Π₀ c
| SeqMut c c' ⇒ ((Π₀ c) ; (Π₀ c'))%AST
| IfMut (b, _) c c' ⇒ IfThenElse b (Π₀ c) (Π₀ c')
| WhileMut (b, _) c ⇒ While b (Π₀ c)
| ITEAddIf _ _ c' ⇒ Π₀ c'
| ITEAddElse _ c _ ⇒ Π₀ c
| ITEDelIf b c c' ⇒ IfThenElse b c (Π₀ c')
| ITEDelElse b c c' ⇒ IfThenElse b (Π₀ c) c'
| WhileAdd b c ⇒ Π₀ c
| WhileDel b c ⇒ While b (Π₀ c)
| LeafSubst a _ ⇒ Leaf a
| CPoint cd ⇒ Π₀ cd
end.
Fixpoint Π₁ (cd : cmd_diff) : cmd :=
match cd with
| SeqDelL c cd ⇒ (Π₁ cd)
| SeqDelR cd c ⇒ (Π₁ cd)
| SeqInsL c cd ⇒ (c ; (Π₁ cd))%AST
| SeqInsR cd c' ⇒ ((Π₁ cd) ; c')%AST
| SeqMut c c' ⇒ ((Π₁ c) ; (Π₁ c'))%AST
| IfMut (_, b') c c' ⇒ IfThenElse b' (Π₁ c) (Π₁ c')
| WhileMut (_, b') c ⇒ While b' (Π₁ c)
| ITEAddIf b c c' ⇒ IfThenElse b c (Π₁ c')
| ITEAddElse b c c' ⇒ IfThenElse b (Π₁ c) c'
| ITEDelIf _ _ c' ⇒ Π₁ c'
| ITEDelElse _ c _ ⇒ Π₁ c
| WhileAdd b c ⇒ While b (Π₁ c)
| WhileDel b c ⇒ Π₁ c
| LeafSubst _ a ⇒ Leaf a
| CPoint cd ⇒ Π₁ cd
end.
Definition tag_store t (s : store) :=
VarMap.fold (λ k v acc, VarMap.add (t k) v acc) s (VarMap.empty _).
Definition store_included_tagged t (s s' : store) :=
∀ x v, VarMap.MapsTo x v s → VarMap.MapsTo (t x) v s'.
Definition join_stores t t' S₀ S₁ :=
VarMapProps.update (tag_store t S₀) (tag_store t' S₁).
Definition cp_algorithm_sound t t' correlating_program :=
∀ S₀ S₀' S₁ S₁' cd,
big_step S₀ (Π₀ cd) MNormal S₀' →
big_step S₁ (Π₁ cd) MNormal S₁' →
∀ G, ∃ S' G',
big_step_g (join_stores t t' S₀ S₁) G (correlating_program cd) S' G'
∧ store_included_tagged t S₀' S' ∧ store_included_tagged t' S₁' S'.
End Languages.