Commit 2b8c7d91 by Dan Frumin

### Finish a stupid/naive/straightforward proof of counter refinement

`The current prove does not reuse certain lemmas`
parent d1a2a63a
 ... ... @@ -18,10 +18,10 @@ Definition CG_counter_body : val := λ: "x" "l", Definition CG_counter : expr := Let "l" newlock ((λ: "x", CG_counter_body "x" "l") (Alloc (#n 0))). Definition FG_increment : val := λ: "v", rec: "inc" "x" := Definition FG_increment : val := λ: "v", rec: "inc" <> := Let "c" (!"v") (If (CAS "v" "c" (BinOp Add (#n 1) "c")) (Unit) ("inc" "x")). ("inc" #())). Definition FG_counter_body : val := λ: "x", (FG_increment "x", counter_read "x"). ... ... @@ -306,26 +306,26 @@ Section CG_Counter. Definition counterN : namespace := nroot .@ "counter". Lemma bin_log_related_arrow Γ f x (e e' : expr) τ τ' (Hclosed : Closed ∅ e ) (Hclosed' : Closed ∅ e') : Lemma bin_log_related_arrow Γ (f x f' x' : binder) (e e' : expr) (τ τ' : type) (Hclosed : Closed ∅ (rec: f x := e)%E ) (Hclosed' : Closed ∅ (rec: f' x' := e')%E) : □(∀ Δ vv, ⟦ τ ⟧ Δ vv -∗ ∅ ⊨ App (Rec f x e) (of_val (vv.1)) ≤log≤ App (Rec f x e') (of_val (vv.2)) : τ') -∗ Γ ⊨ (Rec f x e) ≤log≤ (Rec f x e') : TArrow τ τ'. ∅ ⊨ App (Rec f x e) (of_val (vv.1)) ≤log≤ App (Rec f' x' e') (of_val (vv.2)) : τ') -∗ Γ ⊨ (Rec f x e) ≤log≤ (Rec f' x' e') : TArrow τ τ'. Proof. iIntros "#H". iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". rewrite /env_subst !Closed_subst_p_id. iIntros (Δ vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj". cbn-[subst_p]. rewrite /env_subst !Closed_subst_p_id. iModIntro. iApply wp_value; auto. { simpl. by rewrite decide_left. } iExists (RecV f x e'). simpl. { simpl. erewrite decide_left. done. } iExists (RecV f' x' e'). simpl. iFrame "Hj". iAlways. iIntros (vv) "Hvv". iSpecialize ("H" \$! Δ vv with "Hvv"). iSpecialize ("H" \$! Δ with "* Hs []"). iSpecialize ("H" \$! Δ with "Hs []"). { iAlways. iApply interp_env_nil. } rewrite ?fmap_nil. rewrite ?empty_env_subst. rewrite /interp_expr /env_subst /= !Closed_subst_p_id. done. rewrite !fmap_empty /env_subst !subst_p_empty. done. Unshelve. all: rewrite /Closed /= in Hclosed Hclosed'; eauto. Qed. Definition counter_inv l cnt cnt' : iProp Σ := ... ... @@ -391,44 +391,33 @@ Section CG_Counter. iIntros "#Hinv". Transparent CG_locked_increment with_lock. Transparent FG_increment. unfold CG_locked_increment, with_lock. unfold CG_locked_increment. unlock. unfold FG_increment. unlock. iApply (bin_log_related_rec_l _ ⊤ []); auto. iNext. simpl. rel_bind_r (App _ (#cnt')%E). iApply (bin_log_related_rec_r _ _ ⊤ ); auto. simpl. rewrite !Closed_subst_id. iApply (bin_log_related_rec_r _ [] ⊤); auto. simpl. rel_bind_r (App _ (λ: "l", _))%E. iApply (bin_log_related_rec_r _ _ ⊤); eauto. iApply (bin_log_related_rec_r _ [] ⊤); auto. simpl. rewrite !Closed_subst_id. unfold with_lock. unlock. rel_bind_r (App _ (λ: "l", _))%E. iApply (bin_log_related_rec_r Γ); eauto. { simpl. by rewrite decide_left. } simpl. rewrite !Closed_subst_id. iApply (bin_log_related_rec_r _ [] ⊤); eauto. simpl. rewrite !Closed_subst_id. (* STOPPED HERE: need a different environment *) (* iApply (bin_log_related_arrow); auto. *) (* iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ. simpl. *) (* (* fold this stuff back *) *) (* change (Rec *) (* (App *) (* (Rec *) (* (App (Rec (App (Rec (Var 3)) (App release (Loc l)))) *) (* (App (CG_increment (Loc cnt')).[ren (+4)] (Var 3)))) *) (* (App acquire (Loc l)))) *) (* with (CG_locked_increment (Loc cnt') (Loc l)). *) (* change (Rec *) (* (App *) (* (Rec *) (* (If *) (* (CAS (Loc cnt) (Var 1) *) (* (BinOp Add (#n 1) (Var 1))) Unit *) (* (App (Var 2) (Var 3)))) (Load (Loc cnt)))) *) (* with (FG_increment (Loc cnt)). *) (* Opaque FG_increment. *) iApply bin_log_related_arrow. iAlways. iIntros (Δ [v v']) "[% %]"; simpl in *; subst. clear Δ. (* TODO: cannot use FG_increment_logatomic atm *) (* iApply (bin_log_FG_increment_logatomic (fun n => (l ↦ₛ (#♭v false)) ∗ cnt' ↦ₛ #nv n)%I _ _ _ [] cnt with "[Hinv]"). *) (* iAlways. *) (* iInv counterN as ">Hcnt" "Hcl". iModIntro. *) (* iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]". *) (* iExists n. iFrame. clear n. *) (* iSplit. *) (* iSplit. *) (* - iDestruct 1 as (n) "[Hcnt [Hl Hcnt']]". *) (* iMod ("Hcl" with "[-]"). *) (* { iNext. iExists _. iFrame. } *) ... ... @@ -441,8 +430,54 @@ Section CG_Counter. (* simpl. *) (* iApply bin_log_related_unit. *) (* Opaque CG_locked_increment with_lock. *) admit. Admitted. iApply (bin_log_related_rec_r _ []); eauto. simpl. rewrite !Closed_subst_id. iLöb as "IH". iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl. rel_bind_l (! #cnt)%E. iApply (bin_log_related_load_l). iInv counterN as ">Hcnt" "Hcl". iModIntro. iDestruct "Hcnt" as (n) "[Hl [Hcnt Hcnt']]". iExists (#nv n). iFrame. iIntros "Hcnt". iMod ("Hcl" with "[-]"); simpl. { iNext. iExists _. iFrame. } iApply (bin_log_related_rec_l _ _ []); eauto. iNext. simpl. rel_bind_l (BinOp Add _ _). iApply bin_log_related_binop_l. iNext. simpl. rel_bind_l (CAS _ _ _). iApply (bin_log_related_cas_l); eauto. iInv counterN as ">Hcnt" "Hcl". iModIntro. iDestruct "Hcnt" as (m) "[Hl [Hcnt Hcnt']]". iExists _; iFrame. destruct (decide (m = n)) as [|Hmn]; subst. - (* CASE [m = n], CAS successful *) iSplitR. iIntros "%". by exfalso. iIntros "% Hcnt". rel_bind_r (acquire #l). iApply (bin_log_related_acquire_r with "Hl"); simpl; eauto. solve_ndisj. iIntros "Hl". iApply (bin_log_related_rec_r _ []); simpl; eauto. solve_ndisj. rel_bind_r (App _ #())%E. iApply (bin_log_related_rec_r _ _); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id. rel_bind_r (CG_increment _ _). iApply (bin_log_related_CG_increment_r with "Hcnt'"). solve_ndisj. simpl. iIntros "Hcnt'". iApply (bin_log_related_rec_r _ []); simpl; eauto. solve_ndisj. rewrite !Closed_subst_id. rel_bind_r (release #l)%E. iApply (bin_log_related_release_r with "Hl"). solve_ndisj. iIntros "Hl". simpl. iMod ("Hcl" with "[-]"). { iNext. iExists _. by iFrame. } iApply (bin_log_related_if_true_l _ _ []). iNext. simpl. iApply (bin_log_related_rec_r _ []); simpl; eauto. iApply bin_log_related_unit. - (* CASE [m ≠ n], CAS fails *) iSplitL; last first. iIntros "%". exfalso. apply Hmn. by inversion H1. iIntros "% Hcnt". simpl. iMod ("Hcl" with "[-]"). { iNext. iExists _. by iFrame. } iApply (bin_log_related_if_false_l _ []). iNext. simpl. iApply "IH". Qed. Lemma FG_CG_counter_refinement : ∅ ⊨ FG_counter ≤log≤ CG_counter : TProd (TArrow TUnit TUnit) (TArrow TUnit TNat). ... ...
 ... ... @@ -113,6 +113,7 @@ Ltac of_expr e := | _ => match goal with | [H : Closed ∅ e |- _] => constr:(@ClosedExpr e H) | [H : Is_true (is_closed ∅ e) |- _] => constr:(@ClosedExpr e H) | [H : to_val e = Some ?ev |- _] => constr:(@ClosedExpr e (to_val_closed e ev H)) end ... ...
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