From 7fd646af75e377f53e084a4dd98e454f5b80dc2e Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Thu, 14 Nov 2024 23:18:32 +0100
Subject: [PATCH] add insert read example
---
_CoqProject | 1 +
.../examples/protected/shared_insert_read.v | 174 ++++++++++++++++++
2 files changed, 175 insertions(+)
create mode 100644 theories/tree_borrows/examples/protected/shared_insert_read.v
diff --git a/_CoqProject b/_CoqProject
index 431e6908..89aa4ad8 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -195,6 +195,7 @@ theories/tree_borrows/examples/protected/mutable_reorder_read_down.v
theories/tree_borrows/examples/protected/mutable_reorder_read_up.v
theories/tree_borrows/examples/protected/shared_reorder_read_down_escaped.v
theories/tree_borrows/examples/protected/shared_reorder_read_up_escaped.v
+theories/tree_borrows/examples/protected/shared_insert_read.v
theories/tree_borrows/examples/protected/mutable_reorder_write_down_activated.v
theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated.v
theories/tree_borrows/examples/protected/mutable_reorder_write_up_activated_paper.v
diff --git a/theories/tree_borrows/examples/protected/shared_insert_read.v b/theories/tree_borrows/examples/protected/shared_insert_read.v
new file mode 100644
index 00000000..80ecf513
--- /dev/null
+++ b/theories/tree_borrows/examples/protected/shared_insert_read.v
@@ -0,0 +1,174 @@
+(** This file has been adapted from the Stacked Borrows development, available at
+ https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
+From simuliris.simulation Require Import lifting.
+From simuliris.tree_borrows Require Import proofmode lang adequacy examples.lib.
+From iris.prelude Require Import options.
+
+
+
+(** Moving read of shared ref up across code that *may* use that ref. *)
+
+(** This is a variant using protectors.
+ See delete_read_pubic_escaped_unprotected.v for the original optimization without protectors and with deferred UB.
+ *)
+
+(* Assuming x : & i32 *)
+
+Definition prot_shared_insert_read_unopt : expr :=
+ let: "c" := InitCall in
+
+ (* "x" is the local variable that stores the pointer value "i" *)
+ let: "x" := new_place sizeof_scalar "i" in
+
+ (* retag_place reborrows the pointer value stored in "x" (which is "i"),
+ then updates "x" with the new pointer value.
+ Using a protector here.
+ *)
+ retag_place "x" ShrRef TyFrz sizeof_scalar FnEntry "c";;
+
+ (* The unknown code is represented by a call to an unknown function "f" *)
+ let: "tst" := Call #[ScFnPtr "f"] (#[]) in
+ (* if tst is negative, if so read from x, otherwise return tst *)
+ let: "result" := if: "tst" ≤ (#[0])%V
+ then Copy *{sizeof_scalar} "x"
+ else "tst" in
+
+ (* Free the local variable *)
+ Free "x" ;;
+
+ (* Finally, return the read value *)
+ EndCall "c";;
+ "result"
+ .
+
+Definition prot_shared_insert_read_opt : expr :=
+ let: "c" := InitCall in
+ let: "x" := new_place sizeof_scalar "i" in
+ retag_place "x" ShrRef TyFrz sizeof_scalar FnEntry "c";;
+ let: "tst" := Call #[ScFnPtr "f"] (#[]) in
+ let: "v" := Copy *{sizeof_scalar} "x" in
+ let: "result" := if: "tst" ≤ (#[0])%V then "v" else "tst" in
+ Free "x" ;;
+ EndCall "c";;
+ "result"
+ .
+
+Lemma prot_shared_insert_read `{sborGS Σ} :
+ ⊢ log_rel prot_shared_insert_read_opt prot_shared_insert_read_unopt.
+Proof.
+ log_rel.
+ iIntros "%r_t %r_s #Hrel !# %Ï€ _".
+ sim_pures.
+ sim_apply InitCall InitCall sim_init_call "". iIntros (c) "Hcall". iApply sim_expr_base. sim_pures.
+
+ (* new place *)
+ simpl. source_bind (new_place _ _).
+ iApply source_red_safe_reach.
+ { intros. rewrite subst_result. eapply new_place_safe_reach. }
+ simpl. iIntros "(%v_s & -> & %Hsize)". destruct v_s as [|v_s [|?]]; try done.
+ iPoseProof (rrel_value_source with "Hrel") as (v_t) "(-> & #Hv)".
+ iPoseProof (value_rel_length with "Hv") as "%Hlen". destruct v_t as [|v_t [|?]]; try done.
+ iApply source_red_base. iModIntro. to_sim.
+ sim_apply (new_place _ _) (new_place _ _) sim_new_place_local "%t %l % % Htag Ht Hs"; first done.
+ sim_pures.
+
+ target_apply (Copy _) (target_copy_local with "Htag Ht") "Ht Htag". 2: done. 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+ source_apply (Copy _) (source_copy_local with "Htag Hs") "Hs Htag". 2: done. 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+
+ (* do the retag *)
+ sim_bind (Retag _ _ _ _ _ _) (Retag _ _ _ _ _ _).
+ iApply sim_safe_implies.
+ iIntros ((_ & ot & i & [= ->] & _)).
+ iPoseProof (value_rel_singleton_source with "Hv") as (sc_t [= ->]) "Hscrel".
+ iPoseProof (sc_rel_ptr_source with "Hscrel") as ([= ->]) "Htagged".
+ iApply (sim_retag_fnentry with "Hscrel Hcall"). 1: by cbv.
+ iIntros (t_i v_t v_s _ Hlen_t Hlen_s) "Hcall #Hvrel #Htag_i Hi_t Hi_s".
+ destruct v_t as [|v_t []]; try done.
+ destruct v_s as [|v_s []]; try done. iSimpl in "Hcall".
+ iApply sim_expr_base.
+ target_apply (Write _ _) (target_write_local with "Htag Ht") "Ht Htag".
+ 2-3: done. 1: rewrite /write_range bool_decide_true. 2: simpl; lia. 1: rewrite Z.sub_diag /= //.
+ source_apply (Write _ _) (source_write_local with "Htag Hs") "Hs Htag".
+ 2: done. 1: rewrite /write_range bool_decide_true. 2: simpl; lia. 1: rewrite Z.sub_diag /= //.
+ sim_pures.
+
+ (* do the call *)
+ sim_pures.
+ sim_apply (Call _ _) (Call _ _) (sim_call _ (ValR []) (ValR [])) "".
+ { iApply big_sepL2_nil. done. }
+ iIntros (r_t r_s) "#Hfres". sim_pures.
+
+ (* do the target load *)
+ target_apply (Copy (Place _ _ _)) (target_copy_local with "Htag Ht") "Ht Htag". 2: done.
+ 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+ target_pures. target_bind (Copy _).
+ iApply (target_copy_protected with "Hcall Htag_i Hi_t"). 1: done.
+ 2: simpl; lia. 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+ 2: by rewrite lookup_insert.
+ { intros off Hoff. simpl in *. rewrite /range'_contains /sizeof_scalar /= in Hoff. assert (off = i.2)%nat as -> by lia. rewrite /shift_loc /= Z.add_0_r /call_set_in lookup_insert /=. by eexists. }
+ iIntros "Hi_t _ Hcall". target_finish.
+ sim_pures. simpl. rewrite !subst_result.
+
+ source_bind (BinOp _ _ _).
+ Search BinOp.
+ iApply source_red_safe_implies. 1: eapply (safe_implies_le r_s (ValR [ScInt 0]%V)%V).
+ iIntros ((zres_s & z2 & -> & [= <-])).
+ destruct r_t as [[|zres_t []]|]; simpl; try done.
+ 2: { iExFalso. iPoseProof (big_sepL2_length with "Hfres") as "%HH". done. }
+ iEval (rewrite /value_rel /= /sc_rel) in "Hfres". iDestruct "Hfres" as "[Hfres _]".
+ destruct zres_t; try done. iPure "Hfres" as ->.
+ sim_pures. target_pures. sim_pures.
+ destruct (bool_decide (zres_s ≤ 0%nat)%Z).
+ - simpl. target_case; first done. source_case; first done. sim_pures.
+ (* do the source load *)
+ source_apply (Copy (Place _ _ _)) (source_copy_local with "Htag Hs") "Hs Htag". 2: done.
+ 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+ source_pures. source_bind (Copy _).
+ iApply (source_copy_protected with "Hcall Htag_i Hi_s"). 1: done.
+ 2: simpl; lia. 1: rewrite read_range_heaplet_to_list // Z.sub_diag /= //.
+ 2: by rewrite lookup_insert.
+ { intros off Hoff. simpl in *. rewrite /range'_contains /sizeof_scalar /= in Hoff. assert (off = i.2)%nat as -> by lia. rewrite /shift_loc /= Z.add_0_r /call_set_in lookup_insert /=. by eexists. }
+ iIntros "Hi_s _ Hcall". source_finish.
+ sim_pures.
+
+ (* cleanup: remove the protector ghost state, make the external locations public, free the local locations*)
+ sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
+ iApply (sim_protected_unprotect_public with "Hcall Htag_i"). 1: by rewrite lookup_insert.
+ iIntros "Hc". iEval (rewrite delete_insert) in "Hc".
+ sim_apply (EndCall _) (EndCall _) (sim_endcall_own with "Hc") "".
+ sim_pures.
+ sim_val. iModIntro. iSplit; first done. done.
+ - simpl. target_case; first done. source_case; first done. sim_pures.
+
+ (* cleanup: remove the protector ghost state, make the external locations public, free the local locations*)
+ sim_apply (Free _) (Free _) (sim_free_local with "Htag Ht Hs") "Htag"; [done..|]. sim_pures.
+ iApply (sim_protected_unprotect_public with "Hcall Htag_i"). 1: by rewrite lookup_insert.
+ iIntros "Hc". iEval (rewrite delete_insert) in "Hc".
+ sim_apply (EndCall _) (EndCall _) (sim_endcall_own with "Hc") "".
+ sim_pures.
+ sim_val. iModIntro. iSplit; first done.
+Qed.
+
+
+Section closed.
+ (** Obtain a closed proof of [ctx_ref]. *)
+ Lemma prot_shared_insert_read_ctx : ctx_ref prot_shared_insert_read_opt prot_shared_insert_read_unopt.
+ Proof.
+ set Σ := #[sborΣ].
+ apply (log_rel_adequacy Σ)=>?.
+ apply prot_shared_insert_read.
+ Qed.
+End closed.
+
+Check prot_shared_insert_read_ctx.
+Print Assumptions prot_shared_insert_read_ctx.
+(*
+prot_shared_insert_read_ctx
+ : ctx_ref prot_shared_insert_read_opt prot_shared_insert_read_unopt
+Axioms:
+IndefiniteDescription.constructive_indefinite_description : ∀ (A : Type) (P : A → Prop), (∃ x : A, P x) → {x : A | P x}
+Classical_Prop.classic : ∀ P : Prop, P ∨ ¬ P
+*)
+
--
GitLab