Commit 6bafb34f authored by Dan Frumin's avatar Dan Frumin

Get rid of `cloc_{add,lt}_Z` operations

parent d2649221
......@@ -116,70 +116,17 @@ Inductive 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
cl cloc_of_val v1;
o offset_of_val v2;
Some (cloc_to_val (cloc_add cl o))
| 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
cl1 cloc_of_val v1;
cl2 cloc_of_val v2;
Some #(cloc_lt cl1 cl2)
end.
Definition a_ptr_add : val := λ: "x" "y",
......@@ -522,26 +469,20 @@ Section proofs.
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Φ".
simpl in hop.
destruct (cloc_of_val v1) as [cl|] eqn:Hcl; simplify_eq/=.
destruct (offset_of_val v2) as [o|] eqn:Ho; simplify_eq/=.
iExists cl,o. iFrame.
rewrite -(cloc_to_of_val v1 cl) // (offset_to_of_val v2 o) //.
- 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.
destruct (cloc_of_val v1) as [cl1|] eqn:Hcl1; simplify_eq/=.
destruct (cloc_of_val v2) as [cl2|] eqn:Hcl2; simplify_eq/=.
iExists cl1, cl2. iFrame.
rewrite -(cloc_to_of_val v1 cl1) // -(cloc_to_of_val v2 cl2) //.
Qed.
Lemma a_pre_bin_op_spec R Φ Ψ1 Ψ2 e1 e2 op :
......
......@@ -101,6 +101,11 @@ Section definitions.
| (LitV (LitLoc l), LitV (LitInt i))%V => guard (0 i)%Z; Some (l, Z.to_nat i)
| _ => None
end.
Definition offset_of_val (v: val) : option nat :=
match v with
| LitV (LitInt i) => guard (0 i)%Z; Some (Z.to_nat i)
| _ => None
end.
Definition full_locking_heap (σ : gmap cloc (lvl * val)) :=
( τ : gmap loc (list (lvl * val)),
......@@ -215,6 +220,14 @@ Section properties.
destruct cl; repeat (case_match || simplify_option_eq); auto.
by rewrite Z2Nat.inj_pos positive_nat_Z.
Qed.
Lemma offset_of_to_val (o : nat) : offset_of_val #o = Some o.
Proof. by rewrite /= option_guard_True ?Nat2Z.id; last lia. Qed.
Lemma offset_to_of_val v (o : nat) : offset_of_val v = Some o v = #o.
Proof.
rewrite /offset_of_val =>?.
repeat (case_match; simplify_option_eq); eauto.
rewrite Z2Nat.inj_pos positive_nat_Z //.
Qed.
Lemma to_locking_heap_insert σ cl lv v :
to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
......
......@@ -20,26 +20,8 @@ Section memcpy.
while (∗ᶜ(a_ret "p") <∗ᶜ (a_ret "pend"))
{ ((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.
destruct o1,o2; simpl; compute[cloc_lt]; simpl; repeat case_bool_decide; eauto; try naive_solver.
- exfalso. apply H2. rewrite !SuccNat2Pos.id_succ in H1. done.
- exfalso. apply H1. rewrite !SuccNat2Pos.id_succ in H1. done.
Qed.
Lemma cloc_add_Z_eq l1 (o1 o2 : nat) :
cloc_add_Z l1 o1 o2 = Some (cloc_add (l1,o1) o2).
Proof.
destruct o1,o2; simpl; compute[cloc_add]; simpl;
repeat case_bool_decide; rewrite ?SuccNat2Pos.id_succ; eauto.
by rewrite Nat.add_0_r.
Qed.
Lemma cloc_add_0 cl : cloc_add cl 0 = cl.
Proof. destruct cl; cbv[cloc_add]. simpl. by rewrite Nat.add_0_r. Qed.
(* END TODO *)
Lemma memcpy_body_spec (* (i: nat) *) (pp qq p q : cloc) (n : nat) (ls1 ls2 : list val) R :
length ls1 = n
......@@ -63,7 +45,8 @@ Section memcpy.
simplify_eq/=. rewrite Nat.add_0_r.
iApply a_while_spec'.
iNext. vcg_solver. iExists #false. iSplit.
{ iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl.
{ iPureIntro. case_option_guard; last omega; simpl.
do 3 f_equal. rewrite /cloc_lt.
rewrite bool_decide_true // bool_decide_false //. omega. }
rewrite Qp_half_half. iIntros "? ?".
vcg_continue. iIntros "Hpp Hqq". iRight. iSplit; first done.
......@@ -77,24 +60,26 @@ Section memcpy.
rewrite {1}/(cloc_add q). etaprod q.
iApply a_while_spec'.
iNext. vcg_solver. iExists #true. iSplit.
{ iPureIntro. rewrite cloc_lt_Z_eq /= /cloc_lt. do 3 f_equal. simpl.
rewrite !bool_decide_true; auto. omega. }
{ iPureIntro. repeat (case_option_guard; last omega; simpl).
repeat f_equal. rewrite /cloc_lt /=.
rewrite !bool_decide_true; auto. apply Z2Nat.inj_lt; eauto.
apply Nat2Z.inj_lt. omega. }
rewrite Qp_half_half. iIntros "? ? ? ?".
vcg_continue. iIntros "Hqq Hpp Hw Hy". iLeft; iSplit; first done.
(* DF: vcgen doesnt do anything here *)
(* TODO: DF: vcgen doesnt do anything here *)
(* vcg_solver. iIntros "Hy Hw Hpp". *)
iApply (a_store_spec _ _
(λ v, v = cloc_to_val p pp C[LLvl] cloc_to_val (cloc_add p 1))
(λ v, v = w q C w qq C[LLvl] cloc_to_val (cloc_add q 1)) with "[Hpp] [Hqq Hw]")%I.
+ vcg_solver. iExists (dValUnknown (cloc_to_val (cloc_add p 1))).
iSplit.
{ iPureIntro. replace 1%Z with (Z.of_nat 1%nat); last done.
rewrite cloc_add_Z_eq. simpl. done. }
{ iPureIntro. case_option_guard; last omega; simpl.
repeat f_equal. rewrite Nat2Z.id. by destruct p. }
iIntros "Hpp /=". vcg_continue. eauto.
+ vcg_solver. iExists (dValUnknown (cloc_to_val (cloc_add q 1))).
iSplit.
{ iPureIntro. replace 1%Z with (Z.of_nat 1%nat); last done.
rewrite cloc_add_Z_eq. simpl. done. }
{ iPureIntro. case_option_guard; last omega; simpl.
repeat f_equal. rewrite Nat2Z.id. by destruct q. }
iIntros "Hq Hpp /=". vcg_continue. eauto with iFrame.
+ iNext. iIntros (? ?) "[% Hpp] (% & Hw & Hqq)"; simplify_eq/=.
iExists p,y. iSplit; eauto. iFrame. iIntros "Hy".
......@@ -145,7 +130,8 @@ Section memcpy.
- by vcg_solver.
- iNext. iIntros (? ?) "[% Hpp] %". simplify_eq/=.
iExists (cloc_to_val (p.1,p.2+length ls1))%nat; repeat iSplit; eauto.
{ rewrite cloc_add_Z_eq. done. }
{ iPureIntro. repeat (case_option_guard; last omega). simpl.
repeat f_equal. rewrite !Nat2Z.id //. }
awp_let. iApply (memcpy_body_spec with "Hp Hq Hpp Hqq"); auto.
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