Commit 5242d5ce authored by Léon Gondelman's avatar Léon Gondelman
Browse files

work in progress. take off.

parent 87adc879
From iris.heap_lang Require Export proofmode notation.
From iris.bi Require Import big_op.
From iris_c.c_translation Require Import monad translation proofmode.
Definition known_locs := list loc.
Inductive dloc :=
| dLoc : nat dloc
| dLocUnknown : loc dloc.
Global Instance dloc_decision : EqDecision dloc.
Proof. solve_decision. Defined.
Inductive dbase_lit : Type :=
| dLitInt : Z dbase_lit
| dLitBool : bool dbase_lit
| dLitUnit : dbase_lit
| dLitLoc : dloc dbase_lit
| dLitUnknown : base_lit dbase_lit.
Global Instance dlit_decision : EqDecision dbase_lit.
Proof. solve_decision. Defined.
Inductive dval : Type :=
| dLitV : dbase_lit dval
| dPairV : dval dval dval
| dValUnknown : val dval.
Global Instance dval_EqDecision : EqDecision dval.
Proof. solve_decision. Defined.
Inductive doption (A : Type) : Type :=
| dNone : doption A
| dSome : A doption A
| dUnknown : option A doption A.
Arguments dNone {_}.
Arguments dSome {_} _.
Arguments dUnknown {_} _.
Global Instance doption_fmap : FMap doption := λ A B f m,
match m with
| dNone => dNone
| dSome x => dSome (f x)
| dUnknown o => dUnknown (f <$> o)
end.
Definition dloc_interp (E : known_locs) (dl : dloc) : loc :=
match dl with
| dLoc i => from_option id inhabitant (E !! i)
| dLocUnknown l => l
end.
Definition dbase_lit_interp (E : known_locs) (l : dbase_lit) : base_lit :=
match l with
| dLitInt x => LitInt x
| dLitBool b => LitBool b
| dLitUnit => LitUnit
| dLitLoc dl => LitLoc (dloc_interp E dl)
| dLitUnknown l => l
end.
Fixpoint dval_interp (E : known_locs) (v : dval) : val :=
match v with
| dLitV l => LitV (dbase_lit_interp E l)
| dPairV dv1 dv2 => PairV (dval_interp E dv1) (dval_interp E dv2)
| dValUnknown v => v
end.
Fixpoint doption_interp {A} (mx : doption A) : option A :=
match mx with
| dNone => None
| dSome x => Some x
| dUnknown mx => mx
end.
Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
match op with
| PlusOp => dLitInt (n1 + n2)
| MinusOp => dLitInt (n1 - n2)
| MultOp => dLitInt (n1 * n2)
| QuotOp => dLitInt (n1 `quot` n2)
| RemOp => dLitInt (n1 `rem` n2)
| AndOp => dLitInt (Z.land n1 n2)
| OrOp => dLitInt (Z.lor n1 n2)
| XorOp => dLitInt (Z.lxor n1 n2)
| ShiftLOp => dLitInt (n1 n2)
| ShiftROp => dLitInt (n1 n2)
| LeOp => dLitBool (bool_decide (n1 n2))
| LtOp => dLitBool (bool_decide (n1 < n2))
| EqOp => dLitBool (bool_decide (n1 = n2))
end.
Lemma dbin_op_eval_int_correct E op n1 n2 :
bin_op_eval_int op n1 n2 = dbase_lit_interp E (dbin_op_eval_int op n1 n2).
Proof. by destruct op. Qed.
Definition dbin_op_eval_bool
(op : bin_op) (b1 b2 : bool) : doption dbase_lit :=
match op with
| PlusOp | MinusOp | MultOp | QuotOp | RemOp => dNone (* Arithmetic *)
| AndOp => dSome (dLitBool (b1 && b2))
| OrOp => dSome (dLitBool (b1 || b2))
| XorOp => dSome (dLitBool (xorb b1 b2))
| ShiftLOp | ShiftROp => dNone (* Shifts *)
| LeOp | LtOp => dNone (* InEquality *)
| EqOp => dSome (dLitBool (bool_decide (b1 = b2)))
end.
Lemma dbin_op_eval_bool_correct E op b1 b2 w :
dbin_op_eval_bool op b1 b2 = dSome w
bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp E w).
Proof. destruct op; simpl; try by inversion 1. Qed.
Definition dbin_op_eval
(E : known_locs) (op : bin_op) (dv1 dv2 : dval) : doption dval :=
match dv1,dv2 with
| dPairV _ _, _ | _, dPairV _ _ => dNone
| dValUnknown _, _ | _,dValUnknown _ =>
dUnknown
(dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
| dLitV l1, dLitV l2 =>
if decide (op = EqOp)
then dSome $ dLitV $ dLitBool
$ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
else match l1, l2 with
| (dLitInt n1), (dLitInt n2) =>
dSome $ dLitV $ dbin_op_eval_int op n1 n2
| (dLitBool b1), (dLitBool b2) =>
dLitV <$> dbin_op_eval_bool op b1 b2
| dLitUnknown _, _ | _, dLitUnknown _ =>
dUnknown (dValUnknown <$>
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
| _, _ => dNone
end
end.
Lemma dbin_op_eval_correct E op dv1 dv2 w :
doption_interp (dbin_op_eval E op dv1 dv2) = Some w
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
Some (dval_interp E w).
Proof.
destruct dv1 as [dl1 | | v1 ]; try done.
- destruct dv2 as [dl2 | | v2 ]; try done.
+ unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
{ inversion 1. rewrite /bin_op_eval /=. f_equal. simplify_eq /=.
do 2 case_bool_decide; simplify_eq /=; eauto. destruct H0. done. }
{ rewrite /bin_op_eval; intros; destruct dl1, dl2;
rewrite /bin_op_eval_int /bin_op_eval_bool; simplify_eq /=; f_equal;
try (destruct op; done); simpl.
- rewrite /bin_op_eval in H0; case_decide; first done.
destruct b; simplify_eq /=; f_equal.
- destruct op; simplify_eq /=; try done.
- case_decide; first done. destruct b0; simplify_eq /=; f_equal.
destruct op; simplify_eq /=; try done.
- case_decide; first done. destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b; simplify_eq /=; f_equal;
destruct op; simplify_eq /=; try done.
- case_decide; first done; destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b; simplify_eq /=; f_equal.
- case_decide; first done; destruct b,b0; simplify_eq /=; f_equal.
destruct op; simplify_eq /=; try done. }
+ simpl; by destruct (bin_op_eval op #(dbase_lit_interp E dl1) v2);
inversion 1.
- destruct dv2 as [dl2 | | v2 ]; try done.
+ simpl; by destruct (bin_op_eval op v1 #(dbase_lit_interp E dl2));
inversion 1.
+ simpl; intros. by destruct (bin_op_eval op v1 v2); simplify_eq /=.
Qed.
Definition dun_op_eval
(E : known_locs) (op : un_op) (dv : dval) : doption dval :=
match dv with
| dPairV _ _ => dNone
| dValUnknown _ => dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
| dLitV dl =>
match op, dl with
| NegOp, dLitBool b => dSome $ dLitV $ dLitBool (negb b)
| NegOp, dLitInt n => dSome $ dLitV $ dLitInt (Z.lnot n)
| MinusUnOp, dLitInt n => dSome $ dLitV $ dLitInt (- n)
| _, dLitUnknown l =>
dUnknown (dValUnknown <$> un_op_eval op (dval_interp E dv))
| _,_ => dNone
end
end.
Lemma dun_op_eval_correct E op dv w :
doption_interp (dun_op_eval E op dv) = Some w
un_op_eval op (dval_interp E dv) = Some (dval_interp E w).
Proof.
destruct dv as [dl | | v]; simpl; try done; last first.
- destruct (un_op_eval op v); simpl; by inversion 1.
- destruct op.
+ destruct dl; simpl; try by inversion 1.
destruct b; by inversion 1.
+ destruct dl; simpl; try by inversion 1.
destruct b; by inversion 1.
Qed.
(** DCexpr *)
Inductive dcexpr : Type :=
| dCRet : dval dcexpr
| dCAlloc : dcexpr dcexpr
| dCLoad : dcexpr dcexpr
| dCStore : dcexpr dcexpr dcexpr
| dCBinOp : bin_op dcexpr dcexpr dcexpr
| dCUnOp : un_op dcexpr dcexpr
| dCSeq : dcexpr dcexpr dcexpr
| dCPar : dcexpr dcexpr dcexpr
| dCUnknown (e : expr) `{!Closed [] e}.
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
match de with
| dCRet dv => a_ret (dval_interp E dv)
| dCAlloc de1 => a_alloc (dcexpr_interp E de1)
| dCLoad de1 => a_load (dcexpr_interp E de1)
| dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
| dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
| dCUnOp op de => a_un_op op (dcexpr_interp E de)
| dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2
| dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
| dCUnknown e1 => e1
end.
(** Well-foundness of dcexpr w.r.t. known_locs *)
Fixpoint dval_wf (E: known_locs) (dv : dval) : bool :=
match dv with
| dLitV (dLitLoc (dLoc i)) => bool_decide (is_Some (E!!i))
| dPairV dv1 dv2 => dval_wf E dv1 && dval_wf E dv2
| _ => true
end.
Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
match de with
| dCRet dv => dval_wf E dv
| dCAlloc de1 | dCLoad de1 | dCUnOp _ de1 => dcexpr_wf E de1
| dCStore de1 de2 | dCBinOp _ de1 de2 | dCSeq de1 de2 | dCPar de1 de2 =>
dcexpr_wf E de1 && dcexpr_wf E de2
| dCUnknown _ => true
end.
(*TODO: Fuse wf_mono and interp_mono into one lemma for dval and dcexpr *)
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
dval_wf E dv E `prefix_of` E' dval_wf E' dv.
Proof.
induction dv as [d| | dv1 dv2 ]; try naive_solver.
destruct d; eauto.
destruct d as [i|]; last done; simplify_eq /=.
intros Hb Hpre. case_bool_decide; last done.
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.
destruct E'. by apply prefix_nil_not in Hpre. naive_solver.
+ 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 is_Some_None in H.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
Qed.
Lemma dcexpr_wf_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_wf E' de.
Proof.
induction de; simplify_eq /=; try eauto; [ apply dval_wf_mono | | | |];
naive_solver.
Qed.
Lemma dun_op_eval_dSome_wf E dv u dw:
dval_wf E dv dun_op_eval E u dv = dSome dw dval_wf E dw.
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
Lemma dun_op_eval_dUnknown_wf E dv u w:
dval_wf E dv dun_op_eval E u dv = dUnknown (Some w) dval_wf E w.
Proof. destruct u, dv; simpl; repeat case_match; naive_solver. Qed.
Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2
dbin_op_eval E op dv1 dv2 = dSome dw dval_wf E dw.
Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed.
(** / Well-foundness of dcexpr w.r.t. known_locs *)
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.
Proof.
induction dv as [d| | dv1 dv2 ]; try naive_solver.
destruct d; eauto.
destruct d as [i|]; last done; simplify_eq /=.
intros Hb Hpre. case_bool_decide; last done.
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.
destruct E'. by apply prefix_nil_not in Hpre.
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.
* by apply prefix_nil_not in Hpre.
* by apply is_Some_None in H.
* specialize (prefix_cons_inv_2 _ _ _ _ Hpre). naive_solver.
+ intros; simpl; f_equal; naive_solver.
Qed.
Lemma dcexpr_interp_mono (E E': known_locs) (de: dcexpr) :
dcexpr_wf E de E `prefix_of` E' dcexpr_interp E de = dcexpr_interp E' de.
Proof.
induction de; simplify_eq /=; intros H Hpre;
try (by rewrite IHde ) ||
(apply andb_prop_elim in H as [H1 H2];
rewrite IHde2; [rewrite IHde1; done | done | done ];
by rewrite (IHde1 H1 Hpre (dcexpr_interp E de1))) || eauto.
do 2 f_equal. by apply dval_interp_mono.
Qed.
Global Instance dcexpr_closed E de : Closed [] (dcexpr_interp E de).
Proof. induction de; simpl; solve_closed. Qed.
(** * Reification of C syntax *)
(** ** LocLookup *)
Class LocLookup (E : known_locs) (l : loc) (i : nat) :=
loc_lookup : E !! i = Some l.
Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
Proof. done. Qed.
Global Instance loc_lookup_there l l' E i :
LocLookup E l i LocLookup (l' :: E) l (S i).
Proof. done. Qed.
(** ** BaseLitQuote *)
Class BaseLitQuote (E : known_locs) (l : base_lit) (dl : dbase_lit) :=
{ base_lit_quote : l = dbase_lit_interp E dl;
base_lit_quote_wf : dval_wf E (dLitV dl) }.
(** BaseLitQuote for locs *)
Global Instance base_lit_quote_loc E l i :
LocLookup E l i BaseLitQuote E (LitLoc l) (dLitLoc (dLoc i)) | 1.
Proof.
rewrite /LocLookup=>Hi.
split; rewrite /= ?Hi //.
Qed.
Global Instance base_lit_quote_loc_unknown E l :
BaseLitQuote E (LitLoc l) (dLitLoc (dLocUnknown l)) | 10.
Proof. done. Qed.
(** BaseLitQuote for constants *)
Global Instance base_lit_quote_int E i :
BaseLitQuote E (LitInt i) (dLitInt i).
Proof. split; eauto. Qed.
Global Instance base_lit_quote_default E l :
BaseLitQuote E l (dLitUnknown l) | 1000.
Proof. split; eauto. Qed.
(** ** ExprIntoDVal *)
Class ExprIntoDVal (E : known_locs) (e : expr) (dv : dval) :=
{ expr_into_dval : e = of_val (dval_interp E dv);
expr_into_dval_wf : dval_wf E dv }.
Global Instance expr_into_dval_loc E l dl :
BaseLitQuote E l dl ExprIntoDVal E (Lit l) (dLitV dl).
Proof.
intros ?; split; simpl; eauto using base_lit_quote_wf.
rewrite -base_lit_quote //.
Qed.
Global Instance expr_into_dval_default E e v :
IntoVal e v ExprIntoDVal E e (dValUnknown v) | 1000.
Proof. done. Qed.
(** ** IntoDVal *)
Class IntoDVal (E : known_locs) (v : val) (dv : dval) :=
{ into_dval : v = dval_interp E dv;
into_dval_wf : dval_wf E dv }.
Global Instance into_dval_loc E l dl :
BaseLitQuote E l dl IntoDVal E (LitV l) (dLitV dl).
Proof.
intros ?; split; simpl; eauto using base_lit_quote_wf.
rewrite -base_lit_quote //.
Qed.
Global Instance into_dval_default E v : IntoDVal E v (dValUnknown v) | 1000.
Proof. done. Qed.
(** ** IntoDCexpr *)
Class IntoDCexpr (E: known_locs) (e: expr) (de: dcexpr) :=
{ into_dcexpr : e = dcexpr_interp E de;
into_dcexpr_wf : dcexpr_wf E de }.
Global Instance into_dcexpr_ret E v dv:
ExprIntoDVal E v dv
IntoDCexpr E (a_ret v) (dCRet dv).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dcexpr_alloc E e de:
IntoDCexpr E e de
IntoDCexpr E (a_alloc e) (dCAlloc de).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dcexpr_load E e de:
IntoDCexpr E e de
IntoDCexpr E (a_load e) (dCLoad de).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dcexpr_store E e1 e2 de1 de2:
IntoDCexpr E e1 de1
IntoDCexpr E e2 de2
IntoDCexpr E (a_store e1 e2) (dCStore de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_binop E e1 e2 op de1 de2:
IntoDCexpr E e1 de1
IntoDCexpr E e2 de2
IntoDCexpr E (a_bin_op op e1 e2) (dCBinOp op de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_unop E e op de:
IntoDCexpr E e de
IntoDCexpr E (a_un_op op e) (dCUnOp op de).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dcexpr_sequence E e1 e2 de1 de2:
IntoDCexpr E e1 de1
IntoDCexpr E e2 de2
IntoDCexpr E (e1 ; e2) (dCSeq de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_par E e1 e2 de1 de2:
IntoDCexpr E e1 de1
IntoDCexpr E e2 de2
IntoDCexpr E (e1 ||| e2) (dCPar de1 de2).
Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_unknown E e `{Closed [] e}:
IntoDCexpr E e (dCUnknown e) | 100.
Proof. done. Qed.
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