Commit 621e070f authored by Léon Gondelman 's avatar Léon Gondelman
Browse files

Start work on deep-embedding 'bind'.

Some lemmas and instances broke because of
  1. well-foundness of dexpr and dcexpr is parameterized by the set of variable names.
  2. the well-foundness of dloc takes now into account offsets
parent 0c261f6f
...@@ -179,15 +179,17 @@ Qed. ...@@ -179,15 +179,17 @@ Qed.
(** Dexpr *) (** Dexpr *)
Inductive dexpr : Type := Inductive dexpr : Type :=
| dEVal : dval dexpr | dEVal : dval dexpr
| dEPair : dexpr dexpr dexpr | dEVar : string dexpr
| dEFst : dexpr dexpr | dEPair : dexpr dexpr dexpr
| dESnd : dexpr dexpr | dEFst : dexpr dexpr
| dESnd : dexpr dexpr
| dEUnknown (e : expr) `{!Closed [] e} : dexpr. | dEUnknown (e : expr) `{!Closed [] e} : dexpr.
Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr := Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
match de with match de with
| dEVal dv => dval_interp E dv | dEVal dv => dval_interp E dv
| dEVar x => Var x
| dEPair de1 de2 => (dexpr_interp E de1, dexpr_interp E de2) | dEPair de1 de2 => (dexpr_interp E de1, dexpr_interp E de2)
| dEFst de => Fst (dexpr_interp E de) | dEFst de => Fst (dexpr_interp E de)
| dESnd de => Snd (dexpr_interp E de) | dESnd de => Snd (dexpr_interp E de)
...@@ -197,6 +199,7 @@ Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr := ...@@ -197,6 +199,7 @@ Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
(** DCexpr *) (** DCexpr *)
Inductive dcexpr : Type := Inductive dcexpr : Type :=
| dCRet : dexpr dcexpr | dCRet : dexpr dcexpr
| dCBind : string dcexpr dcexpr dcexpr
| dCAlloc : dcexpr dcexpr dcexpr | dCAlloc : dcexpr dcexpr dcexpr
| dCLoad : dcexpr dcexpr | dCLoad : dcexpr dcexpr
| dCStore : dcexpr dcexpr dcexpr | dCStore : dcexpr dcexpr dcexpr
...@@ -211,9 +214,10 @@ Inductive dcexpr : Type := ...@@ -211,9 +214,10 @@ Inductive dcexpr : Type :=
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr := Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
match de with match de with
| dCRet de => a_ret (dexpr_interp E de) | dCRet de => a_ret (dexpr_interp E de)
| dCAlloc de1 de2 => a_alloc (dcexpr_interp E de1) (dcexpr_interp E de2) | dCBind x de1 de2 => x ←ᶜ (dcexpr_interp E de1) ;; (dcexpr_interp E de2)
| dCLoad de1 => a_load (dcexpr_interp E de1) | dCAlloc de1 de2 => alloc (dcexpr_interp E de1, dcexpr_interp E de2)
| dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2) | dCLoad de => ∗ᶜ (dcexpr_interp E de)
| dCStore de1 de2 => (dcexpr_interp E de1) = (dcexpr_interp E de2)
| dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2) | dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
| dCPreBinOp op de1 de2 => | dCPreBinOp op de1 de2 =>
a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2) a_pre_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
...@@ -221,39 +225,81 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr := ...@@ -221,39 +225,81 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
| dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2 | dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2
| dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2 | dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
| dCInvoke fv de => call (fv, dcexpr_interp E de) | dCInvoke fv de => call (fv, dcexpr_interp E de)
| dCUnknown e1 => e1 | dCUnknown e => e
end. end.
(** Well-foundness of dcexpr w.r.t. known_locs *) (** Closedness predicates for deep embedding of monadic C *)
Fixpoint is_de_closed (X : list string) (de: dexpr): bool :=
match de with
| dEVal dv => true
| dEVar x => bool_decide (x X)
| dEFst de | dESnd de => is_de_closed X de
| dEPair de1 de2 => is_de_closed X de1 && is_de_closed X de2
| dEUnknown e => true
end.
Fixpoint is_dce_closed (X : list string) (de: dcexpr): bool :=
match de with
| dCRet de => bool_decide (is_de_closed X de)
| dCBind x de1 de2 => is_dce_closed (x :: X) de1 && is_dce_closed X de2
| dCLoad de | dCUnOp _ de | dCInvoke _ de => is_dce_closed X de
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
is_dce_closed X de1 && is_dce_closed X de2
| dCUnknown _ => true
end.
Class DExprClosed (X : list string) (e : dexpr) :=
de_closed : is_de_closed X e.
Instance de_closed_proof_irrel X e : ProofIrrel (DExprClosed X e).
Proof. rewrite /DExprClosed. apply _. Qed.
Instance DExprClosed_dec X e : Decision (DExprClosed X e).
Proof. rewrite /DExprClosed. apply _. Defined.
Class DCExprClosed (X : list string) (e : dcexpr) :=
dce_closed : is_dce_closed X e.
Instance dce_closed_proof_irrel X e : ProofIrrel (DCExprClosed X e).
Proof. rewrite /DCExprClosed. apply _. Qed.
Instance DCExprClosed_dec X e : Decision (DCExprClosed X e).
Proof. rewrite /DCExprClosed. apply _. Defined.
(** Well-foundness predicates for deep embedding of monadic C *)
Fixpoint dloc_wf (E: known_locs) (dl : dloc) : bool := Fixpoint dloc_wf (E: known_locs) (dl : dloc) : bool :=
match dl with match dl with
| dLoc i _ => bool_decide (is_Some (E !! i)) | dLoc i j =>
| _ => true match E !! i with
| Some cl => bool_decide (j <= cloc_offset cl)
| None => false
end
| _ => true
end. end.
Fixpoint dval_wf (E: known_locs) (dv : dval) : bool := Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
match dv with match dv with
| dPairV dv1 dv2 => dval_wf E dv1 && dval_wf E dv2 | dPairV dv1 dv2 => dval_wf E dv1 && dval_wf E dv2
| dLocV (dLoc i _) => bool_decide (is_Some (E !! i)) | dLocV dl => bool_decide (dloc_wf E dl)
| _ => true | _ => true
end. end.
Fixpoint dexpr_wf (E: known_locs) (de: dexpr) : bool := Fixpoint dexpr_wf (X: list string) (E: known_locs) (de: dexpr) : bool :=
match de with match de with
| dEVal dv => dval_wf E dv | dEVal dv => dval_wf E dv
| dEFst de | dESnd de => dexpr_wf E de | dEVar x => bool_decide (x X)
| dEPair de1 de2 => dexpr_wf E de1 && dexpr_wf E de2 | dEFst de | dESnd de => dexpr_wf X E de
| dEPair de1 de2 => dexpr_wf X E de1 && dexpr_wf X E de2
| dEUnknown _ => true | dEUnknown _ => true
end. end.
Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool := Fixpoint dcexpr_wf (X: list string) (E: known_locs) (de: dcexpr) : bool :=
match de with match de with
| dCRet de => dexpr_wf E de | dCRet de => dexpr_wf X E de
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf E de1 | dCBind x de1 de2 => dcexpr_wf (x :: X) E de1 && dcexpr_wf X E de2
| dCLoad de1 | dCUnOp _ de1 | dCInvoke _ de1 => dcexpr_wf X E de1
| dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2 | dCAlloc de1 de2 | dCStore de1 de2 | dCBinOp _ de1 de2
| dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 => | dCPreBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
dcexpr_wf E de1 && dcexpr_wf E de2 dcexpr_wf X E de1 && dcexpr_wf X E de2
| dCUnknown _ => true | dCUnknown _ => true
end. end.
...@@ -261,7 +307,8 @@ Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool := ...@@ -261,7 +307,8 @@ Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
Lemma dval_wf_mono (E E': known_locs) (dv: dval) : Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
dval_wf E dv E `prefix_of` E' dval_wf E' dv. dval_wf E dv E `prefix_of` E' dval_wf E' dv.
Proof. Proof.
induction dv as [d| | |]; try naive_solver. Admitted.
(* induction dv as [d| | |]; try naive_solver.
destruct d as [i|]; last done; simplify_eq /=. destruct d as [i|]; last done; simplify_eq /=.
intros Hb Hpre. case_bool_decide; last done. intros Hb Hpre. case_bool_decide; last done.
clear Hb. generalize dependent E. revert E'. induction i as [| i]. clear Hb. generalize dependent E. revert E'. induction i as [| i].
...@@ -271,15 +318,19 @@ Proof. ...@@ -271,15 +318,19 @@ Proof.
* by apply prefix_nil_not in Hpre. * by apply prefix_nil_not in Hpre.
* by apply is_Some_None in H. * by apply is_Some_None in H.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver. * specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed. Qed. *)
Lemma dexpr_wf_mono (E E': known_locs) (de: dexpr) : Lemma dexpr_wf_mono (X: list string) (E E': known_locs) (de: dexpr) :
dexpr_wf E de E `prefix_of` E' dexpr_wf E' de. dexpr_wf X E de E `prefix_of` E' dexpr_wf X E' de.
Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed. Proof. induction de; simplify_eq /=; [apply dval_wf_mono|..]; naive_solver. Qed.
Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) : Lemma dcexpr_wf_mono (X: list string) (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de. dcexpr_wf X E de E `prefix_of` E' dcexpr_wf X E' de.
Proof. induction de; simplify_eq /=; [apply dexpr_wf_mono|..]; naive_solver. Qed. Proof.
revert X.
induction de; intros X; simplify_eq /=; [try apply dexpr_wf_mono|..];
naive_solver.
Qed.
Lemma dun_op_eval_Some_wf E dv u dw: Lemma dun_op_eval_Some_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = Some dw dval_wf E dw. dval_wf E dv dun_op_eval E u dv = Some dw dval_wf E dw.
...@@ -295,8 +346,8 @@ Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw: ...@@ -295,8 +346,8 @@ Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw:
dcbin_op_eval E op dv1 dv2 = Some dw dval_wf E dw. dcbin_op_eval E op dv1 dv2 = Some dw dval_wf E dw.
Proof. Proof.
destruct op; first eauto using dbin_op_eval_Some_wf; try naive_solver. destruct op; first eauto using dbin_op_eval_Some_wf; try naive_solver.
simpl. unfold dptr_plus_eval. repeat case_match; naive_solver. simpl. unfold dptr_plus_eval. repeat case_match; try naive_solver.
Qed. Admitted.
(** / Well-foundness of dcexpr w.r.t. known_locs *) (** / Well-foundness of dcexpr w.r.t. known_locs *)
...@@ -322,22 +373,23 @@ Qed. ...@@ -322,22 +373,23 @@ Qed.
Lemma dval_interp_mono (E E': known_locs) (dv: dval) : Lemma dval_interp_mono (E E': known_locs) (dv: dval) :
dval_wf E dv E `prefix_of` E' dval_interp E dv = dval_interp E' dv. dval_wf E dv E `prefix_of` E' dval_interp E dv = dval_interp E' dv.
Proof. Proof.
induction dv as [d|?|?|?]=>//. (* induction dv as [d|?|?|?]=>//.
{ simpl. intros. f_equal; naive_solver. } { simpl. intros. f_equal; naive_solver. }
destruct d as [i|]; last done; simplify_eq /=. destruct d as [i|]; last done; simplify_eq /=.
intros Hb Hpre. case_bool_decide; last done. intros Hb Hpre. case_bool_decide; last done.
clear Hb. generalize dependent E. revert E'. induction i as [| i]. clear Hb. generalize dependent E. revert E'. induction i as [| i].
+ intros E' E Hpre H. destruct E; first by apply is_Some_None in H. + intros E' E Hpre H. destruct E. first by apply is_Some_None in H.
destruct E'. by apply prefix_nil_not in Hpre. destruct E'. by apply prefix_nil_not in Hpre.
by apply prefix_cons_inv_1 in Hpre; subst. by apply prefix_cons_inv_1 in Hpre; subst.
+ intros E' E Hpre H. destruct E', E; first by apply is_Some_None in H. + intros E' E Hpre H. destruct E', E; first by apply is_Some_None in H.
* by apply prefix_nil_not in Hpre. * by apply prefix_nil_not in Hpre.
* by apply is_Some_None in H. * by apply is_Some_None in H.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver. * specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver. *)
Qed. Admitted.
Lemma dexpr_interp_mono (E E': known_locs) (de: dexpr) : Lemma dexpr_interp_mono (X: list string) (E E': known_locs) (de: dexpr) :
dexpr_wf E de E `prefix_of` E' dexpr_interp E de = dexpr_interp E' de. dexpr_wf X E de E `prefix_of` E'
dexpr_interp E de = dexpr_interp E' de.
Proof. Proof.
induction de; simplify_eq /=; intros H Hpre; induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) || try (by rewrite IHde ) ||
...@@ -347,17 +399,24 @@ Proof. ...@@ -347,17 +399,24 @@ Proof.
by rewrite (dval_interp_mono E E'). by rewrite (dval_interp_mono E E').
Qed. Qed.
Lemma dcexpr_interp_mono (E E': known_locs) (de: dcexpr) : Lemma dcexpr_interp_mono (X: list string) (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de. dcexpr_wf X E de E `prefix_of` E'
dcexpr_interp E de = dcexpr_interp E' de.
Proof. Proof.
induction de; simplify_eq /=; intros H Hpre; Admitted.
(*
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) || try (by rewrite IHde ) ||
(apply andb_prop_elim in H as [H1 H2]; (apply andb_prop_elim in H as [H1 H2];
rewrite IHde2; [rewrite IHde1; done | done | done ]; rewrite IHde2; [rewrite IHde1; done | done | done ];
by rewrite (IHde1 H1 Hpre (dcexpr_interp E de1))) || eauto. by rewrite (IHde1 H1 Hpre (dcexpr_interp E de1))) || eauto.
by rewrite (dexpr_interp_mono E E'). by rewrite (dexpr_interp_mono X E E').
Qed. rewrite IHde1. rewrite IHde2; naive_solver. eauto. done. *)
(* LG: This becomes false when add support for bind *)
(*
Global Instance dexpr_closed E de : Closed [] (dexpr_interp E de). Global Instance dexpr_closed E de : Closed [] (dexpr_interp E de).
Proof. induction de; simpl; try solve_closed. Qed. Proof. induction de; simpl; try solve_closed. Qed.
...@@ -366,9 +425,12 @@ Proof. ...@@ -366,9 +425,12 @@ Proof.
induction de; simpl; try solve_closed. rewrite /Closed /=. induction de; simpl; try solve_closed. rewrite /Closed /=.
split_and. change (Closed [] a_ret). solve_closed. apply (dexpr_closed E d). split_and. change (Closed [] a_ret). solve_closed. apply (dexpr_closed E d).
Qed. Qed.
*)
(** * Reification of C syntax *) (** * Reification of C syntax *)
(** ** LocLookup *) (** ** LocLookup *)
(*LG: I think we need to change to adapt it to offset *)
Class LocLookup (E : known_locs) (l : cloc) (i : nat) := Class LocLookup (E : known_locs) (l : cloc) (i : nat) :=
loc_lookup : E !! i = Some l. loc_lookup : E !! i = Some l.
...@@ -411,14 +473,18 @@ Global Instance expr_into_dval_lit E l dl : ...@@ -411,14 +473,18 @@ Global Instance expr_into_dval_lit E l dl :
IntoDBaseLit E l dl ExprIntoDVal E (Lit l) (dLitV dl). IntoDBaseLit E l dl ExprIntoDVal E (Lit l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed. Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.
(*LG: TODO: fix this ! *)
Global Instance expr_into_dval_loc E l k i j : Global Instance expr_into_dval_loc E l k i j :
IntoCLocPlus l k j IntoCLocPlus l k j
LocLookup E k i ExprIntoDVal E (cloc_to_val l) (dLocV (dLoc i j)) | 1. LocLookup E k i
Proof. rewrite /IntoCLocPlus /LocLookup=> -> Hi. split; rewrite /= ?Hi //. Qed. ExprIntoDVal E (cloc_to_val l) (dLocV (dLoc i j)) | 1.
Proof. rewrite /IntoCLocPlus /LocLookup=> -> Hi. split; rewrite /= ?Hi //.
Admitted.
(*LG: TODO: fix this ! *)
Global Instance expr_into_dval_loc_unknown E l : Global Instance expr_into_dval_loc_unknown E l :
ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 100. ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 100.
Proof. done. Qed. Proof. (* done. Qed. *) Admitted.
Global Instance expr_into_dval_default E e v : Global Instance expr_into_dval_default E e v :
IntoVal e v ExprIntoDVal E e (dValUnknown v) | 1000. IntoVal e v ExprIntoDVal E e (dValUnknown v) | 1000.
...@@ -433,14 +499,17 @@ Global Instance into_dval_lit E l dl : ...@@ -433,14 +499,17 @@ Global Instance into_dval_lit E l dl :
IntoDBaseLit E l dl IntoDVal E (LitV l) (dLitV dl). IntoDBaseLit E l dl IntoDVal E (LitV l) (dLitV dl).
Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed. Proof. intros ?; split=> //=. rewrite -into_dbase_lit //. Qed.
(*LG: TODO: fix this ! *)
Global Instance into_dval_loc E l k i j : Global Instance into_dval_loc E l k i j :
IntoCLocPlus l k j IntoCLocPlus l k j
LocLookup E k i IntoDVal E (cloc_to_val l) (dLocV (dLoc i j)) | 1. LocLookup E k i IntoDVal E (cloc_to_val l) (dLocV (dLoc i j)) | 1.
Proof. rewrite /IntoCLocPlus /LocLookup=> -> Hi. split; rewrite /= ?Hi //. Qed. Proof. rewrite /IntoCLocPlus /LocLookup=> -> Hi. split; rewrite /= ?Hi //.
Admitted.
Global Instance into_dval_loc_unknown E l : Global Instance into_dval_loc_unknown E l :
ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10. ExprIntoDVal E (cloc_to_val l) (dLocV (dLocUnknown l)) | 10.
Proof. done. Qed. Proof. Admitted.
(* done. Qed. *)
Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000. Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
Proof. done. Qed. Proof. done. Qed.
...@@ -448,7 +517,7 @@ Proof. done. Qed. ...@@ -448,7 +517,7 @@ Proof. done. Qed.
(** ** IntoDExpr *) (** ** IntoDExpr *)
Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) := Class IntoDExpr (E: known_locs) (e: expr) (de: dexpr) :=
{ into_dexpr : e = dexpr_interp E de; { into_dexpr : e = dexpr_interp E de;
into_dexpr_wf : dexpr_wf E de }. into_dexpr_wf : dexpr_wf [] E de }.
Global Instance into_dexpr_val E e dv : Global Instance into_dexpr_val E e dv :
ExprIntoDVal E e dv ExprIntoDVal E e dv
...@@ -477,7 +546,7 @@ Proof. done. Qed. ...@@ -477,7 +546,7 @@ Proof. done. Qed.
(** ** IntoDCExpr *) (** ** IntoDCExpr *)
Class IntoDCExpr (E: known_locs) (e: expr) (de: dcexpr) := Class IntoDCExpr (E: known_locs) (e: expr) (de: dcexpr) :=
{ into_dcexpr : e = dcexpr_interp E de; { into_dcexpr : e = dcexpr_interp E de;
into_dcexpr_wf : dcexpr_wf E de }. into_dcexpr_wf : dcexpr_wf [] E de }.
Global Instance into_dcexpr_ret E e de: Global Instance into_dcexpr_ret E e de:
IntoDExpr E e de IntoDExpr E e de
......
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