Commit 98432a2e authored by Dan Frumin's avatar Dan Frumin

Uniform treatment of ML binops and C-level pointer operations

parent 7455d45f
...@@ -58,7 +58,7 @@ Section derived. ...@@ -58,7 +58,7 @@ Section derived.
Lemma awp_bin_op_load_load op (l r : cloc) (v1 v2: val) R Φ : Lemma awp_bin_op_load_load op (l r : cloc) (v1 v2: val) R Φ :
l C v1 - r C v2 - l C v1 - r C v2 -
(l C v1 - r C v2 - w : val, bin_op_eval op v1 v2 = Some w Φ w) - (l C v1 - r C v2 - w : val, cbin_op_eval op v1 v2 = Some w Φ w) -
awp (a_bin_op op (a_load (a_ret (cloc_to_val l))) (a_load (a_ret (cloc_to_val r)))) R Φ. awp (a_bin_op op (a_load (a_ret (cloc_to_val l))) (a_load (a_ret (cloc_to_val r)))) R Φ.
Proof. Proof.
iIntros "Hl Hr HΦ". iIntros "Hl Hr HΦ".
...@@ -75,7 +75,7 @@ Section derived. ...@@ -75,7 +75,7 @@ Section derived.
l C v - l C v -
AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} - AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - v1 = cloc_to_val l ( v1 v2, Ψ1 v1 - Ψ2 v2 - v1 = cloc_to_val l
w, bin_op_eval op v v2 = Some w w, cbin_op_eval op v v2 = Some w
(l C[LLvl] w - Φ v)) - (l C[LLvl] w - Φ v)) -
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}. AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof. Proof.
......
...@@ -75,30 +75,6 @@ Definition a_un_op (op : un_op) : val := λ: "x", ...@@ -75,30 +75,6 @@ Definition a_un_op (op : un_op) : val := λ: "x",
"v" ←ᶜ "x" ;; "v" ←ᶜ "x" ;;
a_ret (UnOp op "v"). a_ret (UnOp op "v").
(*Definition a_pre_un_op (op : un_op) : val := λ: "x",
"l" ←ᶜ "x" ;;ᶜ
a_atomic (λ: <>, a_store (a_ret "l") (a_un_op op (∗ᶜ (a_ret "l")))).*)
Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
a_ret (BinOp op (Fst "vv") (Snd "vv")).
Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope.
Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.
Definition a_pre_bin_op (op : bin_op) : val := λ: "x" "y",
"lv" ←ᶜ ("x" ||| "y");;
a_atomic (λ: <>,
"ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;
a_ret (Fst "lv") = a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;
a_ret "ov").
Notation "e1 +=ᶜ e2" := (a_pre_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
(* M () *) (* M () *)
(* The eta expansion is used to turn it into a value *) (* The eta expansion is used to turn it into a value *)
Definition a_seq : val := λ: <>, Definition a_seq : val := λ: <>,
...@@ -135,6 +111,77 @@ Notation "'callᶜ' ( f , a )" := ...@@ -135,6 +111,77 @@ Notation "'callᶜ' ( f , a )" :=
(at level 100, a at level 200, (at level 100, a at level 200,
format "'callᶜ' ( f , a )") : expr_scope. format "'callᶜ' ( f , a )") : expr_scope.
Inductive cbin_op :=
| CBinOp : bin_op cbin_op
| PtrPlusOp : cbin_op
| PtrLtOp : cbin_op.
(* TODO: move to locking_heap.v ?*)
Definition cloc_add_Z (l : loc) (o : Z) (o' : Z) : option cloc :=
match o,o' with
| Z0,Z0 => Some (l, O)
| Z0,Zpos k => Some (l, Pos.to_nat k)
| Zpos k,Z0 => Some (l, Pos.to_nat k)
| Zpos k1,Zpos k2 => Some (l, Pos.to_nat k1 + Pos.to_nat k2)%nat
| _,_ => None
end.
Lemma cloc_add_Z_spec l o o' cl :
cloc_add_Z l o o' = Some cl
cl.1 = l n n', cl.2 = (n + n')%nat Z.of_nat n = o Z.of_nat n' = o'.
Proof.
destruct o as [|o|], o' as [|o'|]; intros; simplify_eq/=; (split; first done).
naive_solver.
- exists 0%nat, (Pos.to_nat o'). eauto using positive_nat_Z.
- exists (Pos.to_nat o),0%nat. eauto using positive_nat_Z.
- exists (Pos.to_nat o),(Pos.to_nat o'). eauto using Pos2Nat.inj_add, positive_nat_Z.
Qed.
Definition cloc_lt_Z (l1 : loc) (o1 : Z) (l2 : loc) (o2 : Z) : option bool :=
match o1,o2 with
| Z0,Z0 => Some false
| Z0,Zpos k => Some (bool_decide (l1 = l2))
| Zpos k,Z0 => Some false
| Zpos k1,Zpos k2 => Some (bool_decide (l1 = l2) && bool_decide (Pos.to_nat k1 < Pos.to_nat k2)%nat)
| _,_ => None
end.
Lemma cloc_lt_Z_spec l1 o1 l2 o2 b :
cloc_lt_Z l1 o1 l2 o2 = Some b
n1 n2, Z.of_nat n1 = o1 Z.of_nat n2 = o2 cloc_lt (l1,n1) (l2,n2) = b.
Proof.
rewrite /cloc_lt /=.
destruct o1 as [|o1|], o2 as [|o2|]; intros; simplify_eq/=.
- exists 0%nat,0%nat. repeat split; try done.
repeat case_bool_decide; try done. inversion H0.
- exists 0%nat, (Pos.to_nat o2).
repeat split; try done; first eauto using positive_nat_Z.
repeat case_bool_decide; try done. exfalso. eauto using Pos2Nat.is_pos.
- exists (Pos.to_nat o1),0%nat.
repeat split; try done; first eauto using positive_nat_Z.
repeat case_bool_decide; try done. exfalso. inversion H0.
- exists (Pos.to_nat o1),(Pos.to_nat o2).
repeat split; eauto using positive_nat_Z.
Qed.
Definition cbin_op_eval (op : cbin_op) (v1 v2 : val) : option val :=
match op with
| CBinOp op' => bin_op_eval op' v1 v2
| PtrPlusOp =>
match v1,v2 with
| (LitV (LitLoc pl),LitV (LitInt po))%V,LitV (LitInt z) =>
cloc_to_val <$> cloc_add_Z pl po z
| _, _ => None
end
| PtrLtOp =>
match v1,v2 with
| (LitV (LitLoc pl),LitV (LitInt po))%V,
(LitV (LitLoc ql),LitV (LitInt qo))%V =>
(LitV LitBool) <$> cloc_lt_Z pl po ql qo
| _, _ => None
end
end.
Definition a_ptr_add : val := λ: "x" "y", Definition a_ptr_add : val := λ: "x" "y",
"lo" ←ᶜ ("x" ||| "y");; "lo" ←ᶜ ("x" ||| "y");;
let: "o'" := Snd (Fst "lo") + Snd "lo" in let: "o'" := Snd (Fst "lo") + Snd "lo" in
...@@ -145,8 +192,37 @@ Definition a_ptr_lt : val := λ: "x" "y", ...@@ -145,8 +192,37 @@ Definition a_ptr_lt : val := λ: "x" "y",
let: "p" := Fst "pq" in let: "p" := Fst "pq" in
let: "q" := Snd "pq" in let: "q" := Snd "pq" in
if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #false. if: Fst "p" = Fst "q" then a_ret (Snd "p" < Snd "q") else a_ret #false.
Notation "e1 +∗ᶜ e2" := (a_ptr_add e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <∗ᶜ e2" := (a_ptr_lt e1%E e2%E) (at level 80) : expr_scope. Definition a_bin_op (op : cbin_op) : val :=
match op with
| CBinOp op' =>
λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
a_ret (BinOp op' (Fst "vv") (Snd "vv"))
| PtrPlusOp => a_ptr_add
| PtrLtOp => a_ptr_lt
end.
Notation "e1 +ᶜ e2" := (a_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 -ᶜ e2" := (a_bin_op (CBinOp MinusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 *ᶜ e2" := (a_bin_op (CBinOp MultOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ≤ᶜ e2" := (a_bin_op (CBinOp LeOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <ᶜ e2" := (a_bin_op (CBinOp LtOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 ==ᶜ e2" := (a_bin_op (CBinOp EqOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op (CBinOp EqOp) e1%E e2%E)) (at level 80): expr_scope.
Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.
Notation "e1 +∗ᶜ e2" := (a_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 <∗ᶜ e2" := (a_bin_op PtrLtOp e1%E e2%E) (at level 80) : expr_scope.
Definition a_pre_bin_op (op : cbin_op) : val := λ: "x" "y",
"lv" ←ᶜ ("x" ||| "y");;
a_atomic (λ: <>,
"ov" ←ᶜ ∗ᶜ (a_ret (Fst "lv"));;
a_ret (Fst "lv") = a_bin_op op (a_ret "ov") (a_ret (Snd "lv"));;
a_ret "ov").
Notation "e1 +=ᶜ e2" := (a_pre_bin_op (CBinOp PlusOp) e1%E e2%E) (at level 80) : expr_scope.
Notation "e1 +∗=ᶜ e2" := (a_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) : expr_scope.
Section proofs. Section proofs.
Context `{amonadG Σ}. Context `{amonadG Σ}.
...@@ -256,82 +332,6 @@ Section proofs. ...@@ -256,82 +332,6 @@ Section proofs.
iApply awp_ret. by wp_op. iApply awp_ret. by wp_op.
Qed. Qed.
(*
Lemma a_pre_un_op_spec R Φ e op :
AWP e @ R {{ vl, R -∗ ∃ l v w, l ↦C v ∗ ⌜vl = #l⌝
∗ ⌜un_op_eval op v = Some w⌝
∗ (l ↦C[LLvl] w -∗ R ∗ Φ w) }} -∗
AWP a_pre_un_op op e @ R {{ Φ }}.
Proof.
iIntros "He". rewrite /a_pre_un_op.
awp_apply (a_wp_awp with "He"); iIntros (?) "HΦ"; awp_lam.
iApply awp_bind. iApply (awp_wand with "HΦ").
iIntros (vl) "H". awp_lam.
iApply awp_atomic. iNext.
iIntros "R". iDestruct ("H" with "R") as (l v w) "(Hl & % & % & HΦ)".
simplify_eq/=.
iExists True%I. rewrite left_id. awp_lam.
iApply (a_store_spec _ _ (λ v', ⌜v' = #l⌝)%I
(λ v', ⌜v' = w⌝ ∗ l ↦C v)%I
with "[] [Hl] [-]").
- iApply awp_ret. by wp_value_head.
- iApply a_un_op_spec. iApply a_load_spec.
iApply awp_ret. wp_value_head.
iExists _,_; iFrame. iSplit; eauto.
- iNext. iIntros (? ? ->) "[% Hl]". simplify_eq/=.
iExists _,_; iFrame. iSplit; eauto.
iIntros "? _". by iApply "HΦ".
Qed.
*)
Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : bin_op) (e1 e2: expr) :
AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - w, bin_op_eval op v1 v2 = Some w Φ w) -
AWP a_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
iApply awp_bind.
iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
iSpecialize ("HΦ" with "HΨ1 HΨ2").
iDestruct "HΦ" as (w0) "[% H]". by wp_pure _.
Qed.
Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - R -
cl v w, v1 = cloc_to_val cl
cl C v
bin_op_eval op v v2 = Some w
(cl C[LLvl] w - R Φ v)) -
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iApply awp_atomic. iNext.
iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)".
simplify_eq/=. iExists True%I. rewrite left_id. awp_lam.
iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head.
iExists cl, v; iFrame. iSplit; first done.
iIntros "Hl". awp_let. iApply awp_bind.
iApply (a_store_spec _ _
(λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
- awp_proj. iApply awp_ret; by wp_value_head.
- iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
try (try awp_proj; iApply awp_ret; by wp_value_head).
iNext. iIntros (? ? -> ->). eauto.
- iNext. iIntros (? ? -> ->).
iExists _, _; iFrame. iSplit; first done.
iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
iIntros "_". by iApply "HΦ".
Qed.
Lemma a_seq_spec R Φ : Lemma a_seq_spec R Φ :
U (Φ #()) - U (Φ #()) -
AWP (a_seq #()) @ R {{ Φ }}. AWP (a_seq #()) @ R {{ Φ }}.
...@@ -497,13 +497,84 @@ Section proofs. ...@@ -497,13 +497,84 @@ Section proofs.
do 2 (awp_proj; awp_let). do 2 awp_proj. do 2 (awp_proj; awp_let). do 2 awp_proj.
unfold cloc_lt; simpl. case_bool_decide as Hp; awp_op. unfold cloc_lt; simpl. case_bool_decide as Hp; awp_op.
- destruct Hp as [-> ?%Nat2Z.inj_lt]. - destruct Hp as [-> ?%Nat2Z.inj_lt].
rewrite bool_decide_true //. awp_if. do 2 awp_proj. rewrite (bool_decide_true (LitV pl = LitV pl)) //. awp_if. do 2 awp_proj.
iApply awp_ret. wp_op. rewrite bool_decide_true //. iApply awp_ret. wp_op.
- apply not_and_l_alt in Hp as [?|[? ->]]. rewrite (bool_decide_iff (pi < qi)%nat (pi < qi)); eauto using Nat2Z.inj_lt.
+ rewrite bool_decide_false; last congruence. - rewrite bool_decide_false; last congruence.
awp_if. iApply awp_ret. by iApply wp_value. awp_if. iApply awp_ret. by iApply wp_value.
+ rewrite bool_decide_true //. awp_if. iApply awp_ret. do 2 wp_proj. Qed.
wp_op. by rewrite bool_decide_false; last lia.
Lemma a_bin_op_spec R Φ Ψ1 Ψ2 (op : cbin_op) (e1 e2: expr) :
AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - w, cbin_op_eval op v1 v2 = Some w Φ w) -
AWP a_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
destruct op as [op'| |].
- awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
iApply awp_bind.
iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
iNext. awp_lam. iApply awp_ret. do 2 wp_proj.
iSpecialize ("HΦ" with "HΨ1 HΨ2").
iDestruct "HΦ" as (w0) "[% H]". by wp_pure _.
- iApply (a_ptr_add_spec with "H2").
iApply (awp_wand with "H1").
iIntros (v1) "HΨ1". iNext.
iIntros (v2) "HΨ2". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ".
destruct v1 as [ | |v11 v12| |],v2 as [|vl| | |]; simplify_eq/=;
destruct v11 as [|[]| | |],v12 as [|[o| | |]| | |]; simplify_eq/=.
destruct vl as [o'| | |]; simplify_eq/=.
destruct (cloc_add_Z l o o') as [cl|] eqn:Hcl; simplify_eq/=.
apply cloc_add_Z_spec in Hcl.
destruct Hcl as [Hcl1 (n & n' & Hcl2 & Hn & Hn')]. simplify_eq/=.
iExists (cl.1,n), n'. repeat iSplit; eauto.
compute [cloc_add]. simpl. rewrite -Hcl2. iApply "HΦ".
- iApply (a_ptr_lt_spec with "H1").
iApply (awp_wand with "H2").
iIntros (v2) "HΨ2". iNext.
iIntros (v1) "HΨ1". iDestruct ("HΦ" with "HΨ1 HΨ2") as (w hop) "HΦ".
simpl in hop.
destruct v1 as [ | |v11 v12| |],v2 as [| |v21 v22 | |]; simplify_eq;
destruct v11 as [|[| | |l1]| | |],v12 as [|[o1| | |]| | |]; simplify_eq.
destruct v21 as [|[| | |l2]| | |],v22 as [|[o2| | |]| | |]; simplify_eq/=.
destruct (cloc_lt_Z l1 o1 l2 o2) as [b|] eqn:Hcl; simplify_eq/=.
apply cloc_lt_Z_spec in Hcl.
destruct Hcl as (n1 & n2 & Hn1 & Hn2 & Hlt). simplify_eq/=.
iExists (l1,n1),(l2,n2). eauto.
Qed.
Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
AWP e1 @ R {{ Ψ1 }} - AWP e2 @ R {{ Ψ2 }} -
( v1 v2, Ψ1 v1 - Ψ2 v2 - R -
cl v w, v1 = cloc_to_val cl
cl C v
cbin_op_eval op v v2 = Some w
(cl C[LLvl] w - R Φ v)) -
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iApply awp_atomic. iNext.
iIntros "R". iDestruct ("HΦ" with "Hv1 Hv2 R") as (cl v w ->) "(Hl & % & HΦ)".
simplify_eq/=. iExists True%I. rewrite left_id. awp_lam.
iApply awp_bind. awp_proj. iApply a_load_spec. iApply awp_ret. wp_value_head.
iExists cl, v; iFrame. iSplit; first done.
iIntros "Hl". awp_let. iApply awp_bind.
iApply (a_store_spec _ _
(λ v', v' = cloc_to_val cl)%I (λ v', v' = w)%I with "[] [] [-]").
- awp_proj. iApply awp_ret; by wp_value_head.
- iApply (a_bin_op_spec _ _ (λ v', v' = v)%I (λ v', v' = v2)%I);
try (try awp_proj; iApply awp_ret; by wp_value_head).
iNext. iIntros (? ? -> ->). eauto.
- iNext. iIntros (? ? -> ->).
iExists _, _; iFrame. iSplit; first done.
iIntros "?". awp_seq. iApply awp_ret; wp_value_head.
iIntros "_". by iApply "HΦ".
Qed. Qed.
Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} : Lemma a_while_inv_spec I R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
...@@ -528,4 +599,4 @@ End proofs. ...@@ -528,4 +599,4 @@ End proofs.
(* Make sure that we only use the provided rules and don't break the abstraction *) (* Make sure that we only use the provided rules and don't break the abstraction *)
Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke. Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret. Global Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret.
...@@ -92,7 +92,7 @@ Section definitions. ...@@ -92,7 +92,7 @@ Section definitions.
(** Pointer arithmetic *) (** Pointer arithmetic *)
Definition cloc_lt (p q : cloc) : bool := Definition cloc_lt (p q : cloc) : bool :=
bool_decide (p.1 = q.1 p.2 < q.2). bool_decide (p.1 = q.1) && bool_decide (p.2 < q.2)%nat.
Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i). Definition cloc_add (cl : cloc) (i : nat) : cloc := (cl.1, cl.2 + i).
Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2). Definition cloc_to_val (cl : cloc) : val := (#cl.1, #cl.2).
......
...@@ -138,6 +138,14 @@ Definition dbin_op_eval ...@@ -138,6 +138,14 @@ Definition dbin_op_eval
| _, _ => dNone | _, _ => dNone
end. end.
Definition dcbin_op_eval (E: known_locs) (op : cbin_op) (dv1 dv2 : dval) : doption dval :=
match op with
| CBinOp op' => dbin_op_eval E op' dv1 dv2
| PtrPlusOp | PtrLtOp =>
dUnknown (dValUnknown <$> cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
end.
Lemma dbin_op_eval_correct E op dv1 dv2 w : Lemma dbin_op_eval_correct E op dv1 dv2 w :
doption_interp (dbin_op_eval E op dv1 dv2) = Some w doption_interp (dbin_op_eval E op dv1 dv2) = Some w
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
...@@ -170,6 +178,17 @@ Proof. ...@@ -170,6 +178,17 @@ Proof.
try by inversion 1. try by inversion 1.
Qed. Qed.
Lemma dcbin_op_eval_correct E op dv1 dv2 w :
doption_interp (dcbin_op_eval E op dv1 dv2) = Some w
cbin_op_eval op (dval_interp E dv1) (dval_interp E dv2) =
Some (dval_interp E w).
Proof.
destruct op as [op'| |].
- apply dbin_op_eval_correct.
- cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrPlusOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver.
- cbn-[cbin_op_eval]. destruct (cbin_op_eval PtrLtOp (dval_interp E dv1) (dval_interp E dv2)); naive_solver.
Qed.
Definition dun_op_eval Definition dun_op_eval
(E : known_locs) (op : un_op) (dv : dval) : doption dval := (E : known_locs) (op : un_op) (dv : dval) : doption dval :=
match dv with match dv with
...@@ -206,8 +225,8 @@ Inductive dcexpr : Type := ...@@ -206,8 +225,8 @@ Inductive dcexpr : Type :=
| dCAlloc : dcexpr dcexpr | dCAlloc : dcexpr dcexpr
| dCLoad : dcexpr dcexpr | dCLoad : dcexpr dcexpr
| dCStore : dcexpr dcexpr dcexpr | dCStore : dcexpr dcexpr dcexpr
| dCBinOp : bin_op dcexpr dcexpr dcexpr | dCBinOp : cbin_op dcexpr dcexpr dcexpr
| dCPreBinOp : bin_op dcexpr dcexpr dcexpr | dCPreBinOp : cbin_op dcexpr dcexpr dcexpr
| dCUnOp : un_op dcexpr dcexpr | dCUnOp : un_op dcexpr dcexpr
| dCSeq : dcexpr dcexpr dcexpr | dCSeq : dcexpr dcexpr dcexpr
| dCPar : dcexpr dcexpr dcexpr | dCPar : dcexpr dcexpr dcexpr
...@@ -286,6 +305,11 @@ Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw: ...@@ -286,6 +305,11 @@ Lemma dbin_op_eval_dSome_wf E dv1 dv2 op dw:
dbin_op_eval E op dv1 dv2 = dSome dw dval_wf E dw. 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. Proof. destruct op, dv1,dv2; simpl; repeat case_match; naive_solver. Qed.
Lemma dcbin_op_eval_dSome_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2
dcbin_op_eval E op dv1 dv2 = dSome dw dval_wf E dw.
Proof. destruct op; first eauto using dbin_op_eval_dSome_wf; naive_solver. Qed.
(** / Well-foundness of dcexpr w.r.t. known_locs *) (** / Well-foundness of dcexpr w.r.t. known_locs *)
Lemma dval_interp_mono (E E': known_locs) (dv: dval) : Lemma dval_interp_mono (E E': known_locs) (dv: dval) :
......
...@@ -18,7 +18,16 @@ Section memcpy. ...@@ -18,7 +18,16 @@ Section memcpy.
let: "n" := Snd (Snd "arg") in let: "n" := Snd (Snd "arg") in
"pend" ←ᶜ ∗ᶜ(a_ret "p") +∗ᶜ (a_ret "n");; "pend" ←ᶜ ∗ᶜ(a_ret "p") +∗ᶜ (a_ret "n");;
while (∗ᶜ(a_ret "p") <∗ᶜ (a_ret "pend")) while (∗ᶜ(a_ret "p") <∗ᶜ (a_ret "pend"))
{ ((a_ret "p")+=ᶜ♯1) = ∗ᶜ((a_ret "q")+=ᶜ♯1) }. { ((a_ret "p")+=ᶜ♯1) = ∗ᶜ((a_ret "q")+=ᶜ♯1) }.
(* TODO: move somewhere *)
Lemma cloc_lt_Z_eq l1 (o1 : nat) l2 (o2 : nat) :
cloc_lt_Z l1 o1 l2 o2 = Some (cloc_lt (l1,o1) (l2,o2)).
Proof. Admitted.
Lemma cloc_add_Z_eq l1 (o1 o2 : nat) :
cloc_add_Z l1 o1 o2 = Some (cloc_add (l1,o1) o2).
Proof. Admitted.
Lemma memcpy_body_spec (i: nat) (pp p q : cloc) (n : nat) (ls1 ls2 : list val) R : Lemma memcpy_body_spec (i: nat) (pp p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n length ls1 = n
...@@ -28,28 +37,25 @@ Section memcpy. ...@@ -28,28 +37,25 @@ Section memcpy.
q C ls2 - q C ls2 -
pp C (#p.1, #(p.2+i)%nat) - pp C (#p.1, #(p.2+i)%nat) -
AWP while (∗ᶜ (a_ret (#pp.1, #pp.2)) <∗ᶜ a_ret (#p.1, #(p.2 + n)%nat)) AWP while (∗ᶜ (a_ret (#pp.1, #pp.2)) <∗ᶜ a_ret (#p.1, #(p.2 + n)%nat))
{ (a_ret (#pp.1, #pp.2) += 1) = ∗ᶜ (a_ret (#q.1, #q.2) += 1) } { (a_ret (#pp.1, #pp.2) += 1) = ∗ᶜ (a_ret (#q.1, #q.2) += 1) }
@ R {{ _, p C ls2 q C ls2 }}. @ R {{ _, p C ls2 q C ls2 }}.
Proof. Proof.
iIntros (? ?) "Htake Hp Hq Hpp". iIntros (? ?) "Htake Hp Hq Hpp".
iLöb as "IH" forall (i). iDestruct "Htake" as %Htake. iLöb as "IH" forall (i). iDestruct "Htake" as %Htake.
iApply a_while_spec'. iApply a_while_spec'.
iNext. iNext. vcg_solver. simpl.
iApply (a_ptr_lt_spec _ _ (λ v, v = (#p.1, #(p.2+i)%nat)%V pp C (#p.1, #(p.2+i)%nat))%I with "[Hpp]").
{ vcg_solver. eauto. }
vcg_solver. iNext. iIntros (?) "[% Hpp]"; simplify_eq/=.
iExists (p.1,p.2+i)%nat,(p.1,p.2+length ls1)%nat; repeat iSplit; eauto.
destruct (decide (i < length ls1)%nat). destruct (decide (i < length ls1)%nat).
- iLeft. iSplit. - iExists (dValUnknown #true). iSplit.
{ iPureIntro. compute[cloc_lt]. f_equal. simpl. { iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl.
rewrite bool_decide_true; auto. split; auto. omega. } rewrite !bool_decide_true; auto. omega. }
vcg_continue. iLeft; iSplit; first done.
(* vcg_solver DF: doesnt do anything *)
admit. admit.
- iRight. iSplit. - iExists (dValUnknown #false). iSplit.
{ iPureIntro. compute[cloc_lt]. f_equal. simpl. { iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl.
rewrite bool_decide_false; auto. intros [? ?]. omega. } rewrite bool_decide_true // bool_decide_false //. omega. }
iApply a_seq_spec. iModIntro. vcg_continue. iRight; iSplit; first done.
iApply a_seq_spec. iModIntro. simplify_eq/=.
assert (ls1 = ls2) as ->. assert (ls1 = ls2) as ->.
{ generalize dependent i. generalize dependent ls2. induction ls1; simpl; eauto.