Skip to content

GitLab

Commit 934172b1 authored by Heiko Becker's avatar Heiko Becker
Browse files

Next draft of soundness theorem

parent 42885f73
Hide whitespace changes
Inline Side-by-side
Showing with 350 additions and 67 deletions
coq/Infra/ExpressionAbbrevs.v
View file @ 934172b1
......@@ -211,9 +211,9 @@ Qed.
Definition toRTMap (tMap:FloverMap.t mType) : expr R -> option mType :=
let elements := FloverMap.elements (elt:=mType) tMap in
fun (e:expr R) =>
olet p := find (fun p => match R_orderedExps.compare e (toRExp (fst p)) with
olet p := findA (fun p => match R_orderedExps.compare e (toRExp p) with
| Eq => true |_ => false end) elements in
Some (snd p).
Some p.
Definition updDefVars (e:expr R) (m:mType) Gamma :=
fun eNew =>
......@@ -248,32 +248,77 @@ Proof.
apply IHl; auto.
Qed.
Lemma toRTMap_some tMap e m:
Lemma findA_swap (A B:Type) (f1:A -> bool) f2 (l: list (A*B)) r:
(forall k, f1 k = f2 k) ->
findA f1 l = Some r ->
findA f2 l = Some r.
Proof.
induction l; intros f_eq find1; simpl in *; try congruence.
destruct a.
destruct (f1 a) eqn:?.
- rewrite <- f_eq; rewrite Heqb0; congruence.
- rewrite <- f_eq; rewrite Heqb0.
apply IHl; auto.
Qed.
Lemma findA_swap2 (A B:Type) (f1:A -> bool) f2 (l: list (A*B)):
(forall k, f1 k = f2 k) ->
findA f1 l = findA f2 l.
Proof.
induction l; intros f_eq; simpl in *; try congruence.
destruct a.
destruct (f1 a) eqn:?.
- rewrite <- f_eq; rewrite Heqb0; congruence.
- rewrite <- f_eq; rewrite Heqb0.
apply IHl; auto.
Qed.
Lemma toRTMap_some tMap e e2 m:
e2 = toRExp e ->
FloverMap.find e tMap = Some m ->
toRTMap tMap (toRExp e) = Some m.
toRTMap tMap e2 = Some m.
Proof.
intros find_Q.
intros ? find_Q; subst.
rewrite FloverMapFacts.P.F.elements_o in find_Q.
unfold toRTMap.
unfold optionBind.
apply findA_find in find_Q as [key [find_Q k_eq]].
unfold FloverMapFacts.P.F.eqb in k_eq.
cut (find
(fun p : expr Q * mType =>
match R_orderedExps.compare (toRExp e) (toRExp (fst p)) with
| Eq => true
| _ => false
end) (FloverMap.elements (elt:=mType) tMap) = Some (key, m)).
- intros find_R. rewrite find_R. auto.
- eapply find_swap with (f1 := fun p => match Q_orderedExps.exprCompare e (fst p) with
|Eq => true |_ => false end).
+ intros. rewrite <- QcompareExp_RcompareExp; auto.
+ eapply find_swap; eauto.
intros; simpl.
destruct (Q_orderedExps.exprCompare e (fst k)) eqn:q_comp.
all: unfold FloverMapFacts.P.F.eqb.
all: unfold FloverMapFacts.P.F.eq_dec.
all: rewrite q_comp; auto.
erewrite <- findA_swap2 with (f1 := FloverMapFacts.P.F.eqb e).
- rewrite find_Q; auto.
- unfold R_orderedExps.compare.
intros.
rewrite <- QcompareExp_RcompareExp.
unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
Qed.
Lemma toRTMap_find_map tMap e m:
toRTMap tMap (toRExp e) = Some m ->
FloverMap.find e tMap = Some m.
Proof.
intros RTMap_def.
unfold toRTMap, optionBind in *.
Flover_compute.
inversion RTMap_def; subst.
rewrite FloverMapFacts.P.F.elements_o.
erewrite <- findA_swap2 with
(f1 := fun p => match R_orderedExps.compare (toRExp e) (toRExp p) with
|Eq => true |_ => false end); try auto.
intros. unfold R_orderedExps.compare; rewrite <- QcompareExp_RcompareExp.
unfold FloverMapFacts.P.F.eqb, FloverMapFacts.P.F.eq_dec.
destruct (Q_orderedExps.exprCompare e k) eqn:q_comp; auto.
Qed.
Lemma toRTMap_some_cases tMap e1 e2 m1 m2:
toRTMap (FloverMap.add e1 m1 tMap) (toRExp e2) = Some m2 ->
(R_orderedExps.exprCompare (toRExp e1) (toRExp e2) = Eq /\ m1 = m2) \/ toRTMap tMap (toRExp e2) = Some m2.
Proof.
intros map_def.
apply toRTMap_find_map in map_def.
rewrite FloverMapFacts.P.F.add_o in map_def.
destruct (FloverMap.E.eq_dec e1 e2) eqn:?.
- left. inversion map_def; split; try auto.
rewrite <- QcompareExp_RcompareExp; auto.
- right. eauto using toRTMap_some.
Qed.
(**
......
coq/TypeValidator.v
View file @ 934172b1
......@@ -46,34 +46,68 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType) :Prop :=
exists m1,
(FloverMap.find e1 Gamma = Some m1 /\ isMorePrecise m1 mG = true)
end /\
forall E,
(forall x, NatSet.In x (usedVars e) ->
exists v, E x = Some v) ->
(forall e1 e2 v m, e = Binop Div e1 e2 ->
eval_expr E (toRTMap Gamma) (toRExp e2) v m -> v <> 0%R) ->
exists v,
eval_expr E (toRTMap Gamma) (toRExp e) v mG.
(forall E Gamma2 v m,
(forall e m, FloverMap.find e Gamma = Some m -> FloverMap.find e Gamma2 = Some m) ->
eval_expr E (toRTMap Gamma2) (toRExp e) v m ->
m = mG).
(*
(forall E v m,
eval_expr E (toRTMap Gamma) (toRExp e) v m ->
m = mG) /\
forall E,
(forall x, NatSet.In x (usedVars e) ->
exists v, E x = Some v) ->
(forall e1 e2 v m, e = Binop Div e1 e2 ->
eval_expr E (toRTMap Gamma) (toRExp e2) v m -> v <> 0%R) ->
exists v,
eval_expr E (toRTMap Gamma) (toRExp e) v mG. *)
Corollary validTypes_single e Gamma:
validTypes e Gamma ->
exists m, FloverMap.find e Gamma = Some m /\
forall E,
(forall x, NatSet.In x (usedVars e) ->
exists v, E x = Some v) ->
(forall e1 e2 v m, e = Binop Div e1 e2 ->
eval_expr E (toRTMap Gamma) (toRExp e2) v m -> v <> 0%R) ->
exists v,
eval_expr E (toRTMap Gamma) (toRExp e) v m.
exists mG,
FloverMap.find e Gamma = Some mG /\
forall E v m,
eval_expr E (toRTMap Gamma) (toRExp e) v m ->
m = mG.
Proof.
destruct e; intros [? [valid_e [_ valid_top]]]; simpl in *; eauto.
destruct e; intros * [? [defined_m [check_t valid_top]]]; simpl in *; eauto.
Qed.
Ltac validTypes_split :=
match goal with
| [ H: validTypes (Const ?m ?v) ?Gamma |- _] => idtac
| [ H: validTypes (Var ?x) ?Gamma |- _] => idtac
| [ H: validTypes (Unop ?u ?e) ?Gamma |- _] =>
assert (validTypes e Gamma) by (destruct H as [? [? [[? ?] ?]]]; eauto)
| [ H: validTypes (Binop ?b ?e1 ?e2) ?Gamma |- _] =>
assert (validTypes e1 Gamma)
by (destruct H as [? [? [[? [? ?]] ?]]]; auto);
assert (validTypes e2 Gamma)
by (destruct H as [? [? [[? [? ?]] ?]]]; auto)
| [ H: validTypes (Fma ?e1 ?e2 ?e3) ?Gamma |- _] =>
assert (validTypes e1 Gamma)
by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
assert (validTypes e2 Gamma)
by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto);
assert (validTypes e3 Gamma)
by (destruct H as [? [? [[? [? [? ?]]] ?]]]; auto)
| [ H: validTypes (Downcast ?m ?e) ?Gamma |- _] =>
assert (validTypes e ?Gamma) by (destruct H as [? [? [[? ?] ?]]]; eauto)
end.
Ltac validTypes_simp :=
match goal with
| [ H: validTypes ?e ?Gamma |- _ ] => validTypes_split; apply validTypes_single in H
| _ => fail "No typing assumption found"
end.
Open Scope string_scope.
Definition getTypeMap (T:Type) (r:result (FloverMap.t T)) :FloverMap.t T:=
Definition getTypeMap (r:result (FloverMap.t mType)) :FloverMap.t mType:=
match r with
|Succes m => m
| _ => FloverMap.empty T
| _ => FloverMap.empty mType
end.
Definition isMonotone mOldO mNew :=
......@@ -82,6 +116,16 @@ Definition isMonotone mOldO mNew :=
|Some mOld => mTypeEq mOld mNew
end.
Definition addMono e m map :=
match FloverMap.find e map with
|Some mOld =>
if (mTypeEq m mOld)
then Succes map
else Fail _ "Nonmonotonic map update"
| None =>
Succes (FloverMap.add e m map)
end.
Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
(akk:FloverMap.t mType)
: result (FloverMap.t mType) :=
......@@ -106,38 +150,46 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
if (isFixedPointB m_e1)
then
match mOldO with
|Some mFix => Succes (FloverMap.add e mFix akk_new)
|Some mFix => addMono e mFix akk_new
|None => Fail _ "Undefined fixed-point type"
end
else
if (isMonotone mOldO m_e1)
then Succes (FloverMap.add e m_e1 akk_new)
then addMono e m_e1 akk_new
else Fail _ "Wrong type annotation for unary constant"
| None => Fail _ "Cannot Typecheck unary operator"
end
| Binop b e1 e2 =>
let akk1 := getTypeMap (getValidMap Gamma e1 akk) in
let akk2 := getTypeMap (getValidMap Gamma e2 akk1) in
let m1 := FloverMap.find e1 akk2 in
let m2 := FloverMap.find e2 akk2 in
match m1, m2 with
|Some t1, Some t2 =>
if (isFixedPointB t1 && isFixedPointB t2)
then
match mOldO with
| None => Fail _ "Undefined fixed-point type"
| Some mj =>
Succes (FloverMap.add e mj akk2)
match getValidMap Gamma e1 akk with
| Fail _ _ => Fail _ "First arg"
| FailDet _ _ => Fail _ "First arg"
| Succes akk1_map =>
match getValidMap Gamma e2 akk1_map with
| Fail _ _ => Fail _ "Second arg"
| FailDet _ _ => Fail _ "Second arg"
| Succes akk2_map =>
let m1 := FloverMap.find e1 akk2_map in
let m2 := FloverMap.find e2 akk2_map in
match m1, m2 with
|Some t1, Some t2 =>
if (isFixedPointB t1 && isFixedPointB t2)
then
match mOldO with
| None => Fail _ "Undefined fixed-point type"
| Some mj =>
Succes (FloverMap.add e mj akk2_map)
end
else
match (join_fl t1 t2) with
| Some m =>
if (isMonotone mOldO m)
then Succes (FloverMap.add e m akk2)
else Fail _ "Wrong type annotation for binary operator"
| None => Fail _ "Could not compute join for arguments"
else
match (join_fl t1 t2) with
| Some m =>
if (isMonotone mOldO m)
then Succes (FloverMap.add e m akk2_map)
else Fail _ "Wrong type annotation for binary operator"
| None => Fail _ "Could not compute join for arguments"
end
| _, _ => Fail _ "Could not compute type for arguments"
end
end
| _, _ => Fail _ "Could not compute type for arguments"
end
| Fma e1 e2 e3 =>
let akk1 := getTypeMap (getValidMap Gamma e1 akk) in
......@@ -199,8 +251,91 @@ Lemma toRTMap_def:
toRTMap (FloverMap.add e m akk) e' = Some m.
Proof.
intros.
subst; apply toRTMap_some.
auto using tMap_def.
subst; eapply toRTMap_some;
eauto using tMap_def.
Qed.
Lemma no_cycle_unop e:
forall u,
~ (fun e1 e2 : expr Q_orderedExps.V => Q_orderedExps.exprCompare e1 e2 = Eq)
e (Unop u e).
induction e; intros *; cbn in *; try congruence.
destruct (unopEq u u0) eqn:?; try auto.
destruct (unopEq u Neg); congruence.
Qed.
(* Lemma eval_expr_drop_unop_gamma e: *)
(* forall E Gamma u m v mres, *)
(* eval_expr E (toRTMap (FloverMap.add (Unop u e) m Gamma)) (toRExp e) v mres -> *)
(* eval_expr E (toRTMap Gamma) (toRExp e) v mres. *)
(* Proof. *)
(* pose (eT := e). *)
(* induction e; intros * eval_e; inversion eval_e; subst; *)
(* [ eapply Var_load | eapply Const_dist' *)
(* | eapply Unop_neg' | eapply Unop_inv' *)
(* | eapply Binop_dist' | eapply Fma_dist' *)
(* | eapply Downcast_dist' ]; eauto; *)
(* match goal with *)
(* | [H : toRTMap (FloverMap.add ?e1 ?m1 ?Gamma) ?e2 = Some ?m2 |- _] => *)
(* let tmp := fresh "tmp" in *)
(* let tmp2 := fresh "tmp" in *)
(* assert (toRTMap (FloverMap.add e1 m1 Gamma) (toRExp eT) = Some m2) *)
(* as tmp *)
(* by (subst eT; simpl; auto); *)
(* pose proof (toRTMap_find_map _ _ tmp) as tmp2 ; *)
(* rewrite FloverMapFacts.P.F.add_o in tmp2; *)
(* try assert (Q_orderedExps.exprCompare (Unop u eT) eT <> Eq) by (auto using no_cycle_unop) *)
(* end. *)
(* - destruct (FloverMapFacts.P.F.eq_dec (Unop u (Var Q_orderedExps.V n)) eT) eqn:?; *)
(* subst eT; try congruence. *)
(* eapply toRTMap_some; try eauto. simpl; auto. *)
(* - destruct (FloverMapFacts.P.F.eq_dec (Unop u (Const mres v)) eT) eqn:?; *)
(* subst eT; try congruence. *)
(* eapply toRTMap_some; try eauto. simpl; auto. *)
(* - eapply IHe; eauto. *)
(* eauto using toRTMap_some. *)
(* . subst eT. *)
(* rewrite H in tmp0. *)
(* - apply toRTMap_find_map in H0. some_cases in H0. *)
(* end). *)
(* Lemma validTypes_unop_mono u e m t: *)
(* validTypes e t -> *)
(* validTypes e (FloverMap.add (Unop u e) m t). *)
(* Proof. *)
(* induction e; intros validT; simpl in *. *)
(* - destruct validT as [? [t_def [? ?]]]; eexists; split; try eauto. *)
(* + erewrite FloverMapFacts.P.F.add_neq_o; eauto using no_cycle_unop. *)
(* + split; try auto. *)
(* intros. *)
Lemma validTypes_mono e:
forall map1 map2,
(forall e m, FloverMap.find e map1 = Some m -> FloverMap.find e map2 = Some m) ->
validTypes e map1 ->
validTypes e map2.
Proof.
induction e; intros * maps_mono valid_m1; simpl in *;
destruct valid_m1 as [t_m1 [find_map1 [check_top valid_rec]]];
pose proof (maps_mono _ _ find_map1) as find_mono; eexists; split; try eauto.
- repeat split; try eauto.
destruct check_top as [valid_e1 check_top]; eapply IHe; eauto.
- destruct check_top as [valid_e1 [valid_e2 validJoin]];
repeat split; try eauto.
destruct validJoin as [m1 [m2 [find_m1 [find_m2 join_true]]]].
pose proof (maps_mono e1 m1 find_m1) as find_m1_map2;
pose proof (maps_mono e2 m2 find_m2) as find_m2_map2.
eauto.
- destruct check_top as [valid_e1 [valid_e2 [valid_e3 validJoin]]];
repeat split; try eauto.
destruct validJoin as [m1 [m2 [m3 [find_m1 [find_m2 [find_m3 join_true]]]]]].
pose proof (maps_mono e1 m1 find_m1) as find_m1_map2;
pose proof (maps_mono e2 m2 find_m2) as find_m2_map2;
pose proof (maps_mono e3 m3 find_m3) as find_m3_map2.
repeat eexists; eauto.
- destruct check_top as [valid_e1 [m_eq [m_e1 [find_e1 morePrecise_res]]]].
repeat split; try eauto.
Qed.
Theorem getValidMap_correct e:
......@@ -210,13 +345,116 @@ Theorem getValidMap_correct e:
getValidMap Gamma e akk = Succes res ->
validTypes e res.
Proof.
pose (eT := e).
induction e ; intros Gamma akk res akk_sound validMap_succ;
pose (eT := e);
induction e ; intros Gamma akk res akk_sound validMap_succ;
destruct (FloverMap.mem eT akk) eqn:Hmem; subst;
cbn in validMap_succ; subst eT;
rewrite Hmem in *;
try (inversion validMap_succ; subst; apply akk_sound; auto).
- Flover_compute; simpl.
inversion validMap_succ; subst.
eexists; split; [eauto using tMap_def | split; try auto].
intros * map_mono eval_var.
inversion eval_var; subst.
assert (FloverMap.find (Var Q n) (FloverMap.add (Var Q n) m akk) = Some m)
by (eauto using tMap_def).
pose proof (map_mono _ _ H) as find_Gamma2.
assert (toRTMap Gamma2 (Var R n) = Some m).
{ eapply toRTMap_some; eauto; simpl; auto. }
congruence.
- Flover_compute; simpl.
destruct (isMonotone (FloverMap.find (elt:=mType) (Const m v) Gamma) m) eqn:?;
[ | congruence].
inversion validMap_succ; subst.
eexists; split; [eauto using tMap_def | split; try auto].
intros * map_mono eval_const; inversion eval_const; subst; auto.
- destruct (FloverMap.find (elt:=mType) e (getTypeMap (getValidMap Gamma e akk))) eqn:?;
try congruence.
destruct (isFixedPointB m) eqn:?.
+ destruct (getValidMap Gamma e akk) eqn:?; cbn in *; try congruence.
assert (validTypes e t) as valid_rec by (eapply IHe; eauto).
unfold addMono in validMap_succ.
Flover_compute.
* destruct (mTypeEq m0 m1) eqn:?; type_conv; subst; try congruence.
inversion validMap_succ; subst.
exists m1; repeat split; try eauto.
apply validTypes_single in valid_rec.
intros * map_mono eval_u.
destruct valid_rec as [m_e [find_me eval_valid]].
rewrite find_me in Heqo. inversion Heqo; subst.
pose proof (map_mono (Unop u e) _ Heqo1) as find_Gamma2.
assert (toRTMap Gamma2 (toRExp (Unop u e)) = Some m1).
{ eapply toRTMap_some; eauto. }
inversion eval_u; subst; simpl in *; congruence.
* inversion validMap_succ; subst.
exists m0; repeat split; try eauto using tMap_def.
{ apply validTypes_mono with (map1:=t); try eauto.
intros * find_t.
rewrite FloverMapFacts.P.F.add_o.
unfold FloverMapFacts.P.F.eq_dec.
destruct (Q_orderedExps.exprCompare (Unop u e) e0) eqn:?; try auto.
rewrite FloverMapFacts.P.F.find_o with (y:= e0) in Heqo1; try auto.
congruence. }
{ intros * map_mono eval_unop.
assert (FloverMap.find (elt:=mType) (Unop u e) (FloverMap.add (Unop u e) m0 t) = Some m0)
as find_unop_t
by (eauto using tMap_def).
pose proof (map_mono _ _ find_unop_t).
assert (toRTMap Gamma2 (toRExp (Unop u e)) = Some m0)
by (eapply toRTMap_some; eauto).
inversion eval_unop; subst; simpl in *; congruence. }
+ destruct (isMonotone (FloverMap.find (elt:=mType) (Unop u e) Gamma) m) eqn:?;
try congruence.
destruct (getValidMap Gamma e akk) eqn:?; cbn in *; try congruence.
unfold addMono in *.
Flover_compute.
* destruct (mTypeEq m m0) eqn:?; try congruence; type_conv; subst.
inversion validMap_succ; subst.
exists m0; repeat split; try eauto using IHe.
intros * map_mono eval_unop.
pose proof (map_mono _ _ Heqo0).
assert (toRTMap Gamma2 (toRExp (Unop u e)) = Some m0)
by (eapply toRTMap_some; eauto).
inversion eval_unop; subst; simpl in *; congruence.
* inversion validMap_succ; subst.
exists m; repeat split; try eauto using tMap_def.
{ eapply (validTypes_mono _) with (map1:= t); eauto.
intros * find_t.
rewrite FloverMapFacts.P.F.add_o.
unfold FloverMapFacts.P.F.eq_dec.
destruct (Q_orderedExps.exprCompare (Unop u e) e0) eqn:?; try auto.
rewrite FloverMapFacts.P.F.find_o with (y:= e0) in Heqo0; try auto.
congruence. }
{ intros * map_mono eval_unop.
assert (FloverMap.find (elt:=mType) (Unop u e) (FloverMap.add (Unop u e) m t) = Some m)
by (eauto using tMap_def).
pose proof (map_mono _ _ H).
assert (toRTMap Gamma2 (toRExp (Unop u e)) = Some m)
by (eapply toRTMap_some; eauto).
inversion eval_unop; subst; simpl in *; congruence. }
- destruct (getValidMap Gamma e1 akk) eqn:?; cbn in *; try congruence.
destruct (getValidMap Gamma e2 t) eqn:?; cbn in *; try congruence.
destruct (FloverMap.find (elt:=mType) e1 t0) eqn:e1_find; try congruence.
destruct (FloverMap.find (elt:=mType) e2 t0) eqn:e2_find; try congruence.
destruct (isFixedPointB m && isFixedPointB m0) eqn:?.
+ destruct (FloverMap.find (elt:=mType) (Binop b e1 e2) Gamma) eqn:?;
try congruence.
inversion validMap_succ; subst.
exists m1; repeat split; try eauto using tMap_def.
* eapply validTypes_mono with (map1:=t0).
{ admit. }
{ eapply validTypes_mono with (map1 := t).
- admit.
- eapply IHe1; eauto. }
* eapply validTypes_mono with (map1 := t0).
{ admit. }
{ eapply IHe2 with (akk := t); eauto. admit. }
* admit.
*
Flover_compute; simpl.
inversion validMap_succ; subst.
exists m; repeat split; [eauto using tMap_def | ].
intros * env_def no_div_zero; simpl in *.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment