From c99c5ba5f9ef8af5b102d7ca85d65170215d7846 Mon Sep 17 00:00:00 2001
From: Irene Yoon <euisuny@cis.upenn.edu>
Date: Sun, 10 Dec 2023 18:49:35 -0500
Subject: [PATCH] Existence proofs
---
theories/vir/contextual_laws.v | 30 ++-
theories/vir/examples/examples.v | 250 +++++++++++++++++--
theories/vir/instr_laws.v | 396 ++++++++++++++++++++++++++++++-
theories/vir/logical_relations.v | 1 +
theories/vir/spec.v | 27 ++-
5 files changed, 665 insertions(+), 39 deletions(-)
diff --git a/theories/vir/contextual_laws.v b/theories/vir/contextual_laws.v
index 55ff9de2..f5dfd3cc 100644
--- a/theories/vir/contextual_laws.v
+++ b/theories/vir/contextual_laws.v
@@ -204,17 +204,28 @@ Section contextual_properties.
Definition new_frame args := {| alloca_dom := ∅; local_dom := (list_to_set args) |}.
- Theorem code_to_fn_contextual_args name args c_t c_s i_t i_s C args_t args_s:
+ Definition local_args_own_target args_name args_val i :=
+ ([∗ list] '(l, v) ∈ combine args_name args_val, [ l := v ]t i)%I.
+
+ Definition local_args_own_source args_name args_val i :=
+ ([∗ list] '(l, v) ∈ combine args_name args_val, [ l := v ]s i)%I.
+
+ Theorem code_to_fn_contextual_args
+ name args c_t c_s i_t i_s C args_t args_s:
NoDup args ->
length args = length args_t ->
length args = length args_s ->
initial_frame_res [i_t] [i_s] C -∗
- □ (∀ j_t j_s, frame_WF j_t j_s ∗
- frame_resources_own j_t j_s (new_frame args) (new_frame args) C -∗
+ □ (∀ j_t j_s, (frame_WF j_t j_s ∗
+ frame_resources_own j_t j_s (new_frame args) (new_frame args) C ∗
+ local_args_own_target args args_t j_t ∗
+ local_args_own_source args args_s j_s) -∗
instr_conv (denote_code c_t) ⪯
instr_conv (denote_code c_s)
[{ (x, y), frame_WF j_t j_s ∗
- frame_resources_own_exist j_t j_s C }]) -∗
+ frame_resources_own_exist j_t j_s C ∗
+ local_args_own_target args args_t j_t ∗
+ local_args_own_source args args_s j_s }]) -∗
(<{{ (make_fn name c_t args) (args_t) }}> ) ⪯
(<{{ (make_fn name c_s args) (args_s) }}> )
[{ fun x y => initial_frame_res [i_t] [i_s] C }].
@@ -223,7 +234,7 @@ Section contextual_properties.
cbn -[instr_conv denote_code].
rewrite Hlen_t in Hlen_s.
- rewrite Hlen_t Hlen_s Nat.eqb_refl; cbn.
+ rewrite Hlen_t Hlen_s Nat.eqb_refl.
rewrite !bind_ret_l.
Opaque denote_code.
@@ -257,13 +268,15 @@ Section contextual_properties.
(@Monad.ret (itree L0) (@Monad_itree L0) T)) ?x)
with (instr_conv x).
iAssert (frame_resources_own
- [j_t; i_t] [j_s; i_s] (new_frame args) (new_frame args)
- C)
+ [j_t; i_t] [j_s; i_s] (new_frame args) (new_frame args) C ∗
+ local_args_own_target args args_t [j_t; i_t] ∗
+ local_args_own_source args args_s [j_s; i_s])%I
with "[H HC]" as "Hi".
{ rewrite /frame_resources_exist; iFrame.
iDestruct "H" as "(?&?&?&?&?&?&?&?)"; cbn; iFrame.
cbn. rewrite !combine_fst; eauto.
2 : by rewrite Hlen_t Hlen_s. iFrame.
+
iExists nil, nil; cbn; repeat iSplitL; try done;
iPureIntro; constructor. }
@@ -301,7 +314,8 @@ Section contextual_properties.
setoid_rewrite interp_ret.
iApply sim_expr_Φ_Proper; last first.
{ iApply (sim_expr_bupd_mono with "[HC Halloc Hdom]"); cycle 1.
- { iDestruct "Hbij" as (??) "Hbij".
+ { iDestruct "Hbij" as "(Hbij & Hlv_t & Hlv_s)".
+ iDestruct "Hbij" as (??) "Hbij".
iDestruct "Hbij" as
"(((Ha_t&Ha_s)&((Hl_t&Hl_s)&(Hs_t&Hs_s)))
& (HC&H))".
diff --git a/theories/vir/examples/examples.v b/theories/vir/examples/examples.v
index 9da81bec..5bd4d6f7 100644
--- a/theories/vir/examples/examples.v
+++ b/theories/vir/examples/examples.v
@@ -507,27 +507,243 @@ Section examples.
End examples.
+(* Existence proofs for function specifications *)
+Section attr_fns.
-(** *Exmaple external functions *)
+ Context {Σ : gFunctors} `{!sheapGS Σ, !checkedoutGS Σ, !heapbijGS Σ}.
-(* A function that reads from its single argument *)
-Definition reads_only : fn_name := "reads_only".
+ Definition nil_fn_ex_name : fn_name := "nil_fn_ex".
-Definition reads_only_args arg : code dtyp :=
- ((IId (Raw 0), INSTR_Load true (DTYPE_I 32)
- (DTYPE_I 32, EXP_Ident (ID_Local arg)) None) :: nil).
+ Definition nil_fn_ex : code dtyp := nil.
-Definition reads_only_args_fn arg : definition dtyp (cfg dtyp) :=
- make_fn reads_only (reads_only_args arg) [arg].
+ Definition nil_fn_ex_fn :=
+ make_fn nil_fn_ex_name nil_fn_ex nil.
-(* A function that stores to its single argument *)
-Definition argmems_only : fn_name := "argmems_only".
+ (* The empty function satisfies all attributes *)
+ Lemma nil_fn_ex_sat dv C i_t i_s attr:
+ attribute_interp
+ (ExternalCall DTYPE_Void dv nil attr)
+ (ExternalCall DTYPE_Void dv nil attr) C ->
+ initial_frame_res [i_t] [i_s] C -∗
+ (<{{ (make_fn nil_fn_ex_name nil_fn_ex nil) (nil) }}> ) ⪯
+ (<{{ (make_fn nil_fn_ex_name nil_fn_ex nil) (nil) }}> )
+ [{ fun x y =>
+ initial_frame_res [i_t] [i_s] C }].
+ Proof with clean.
+ iIntros (?); simp attribute_interp in H.
+ destruct H as (?&?).
+ destruct x eqn: Hx;
+ iIntros "Hi"; clear H;
+ iApply (code_to_fn_contextual with "Hi");
+ iModIntro; iIntros (??) "(#HWF & Hbij)";
+ cbn; rewrite bind_ret_l;
+ rewrite instr_conv_ret;
+ iApply sim_expr_base;
+ iExists _, _; do 2 (iSplitL ""; first done); iFrame "HWF";
+ iDestruct "Hbij" as "(Hbij & HC)";
+ iExists empty_frame, empty_frame; iFrame.
+ Qed.
-Definition argmems_only_args arg : code dtyp :=
- ((IVoid 2, INSTR_Store true
- (DTYPE_I 32, EXP_Integer 2)
- (DTYPE_Pointer, EXP_Ident (ID_Local arg))
- None) :: nil).
+ (* Readonly *)
+ Definition readonly_ex_name : fn_name := "readonly_ex".
+
+ Definition readonly_ex : code dtyp :=
+ (IId (Raw 1), INSTR_Alloca (DTYPE_I 32) None None) ::
+ (IId (Raw 3), INSTR_Load true (DTYPE_I 32)
+ (DTYPE_I 32, EXP_Ident (ID_Local (Raw 1))) None) :: nil.
+
+ Definition readonly_ex_fn :=
+ make_fn readonly_ex_name readonly_ex nil.
+
+ Lemma readonly_ex_sat dv C i_t i_s:
+ attribute_interp
+ (ExternalCall DTYPE_Void dv nil [FNATTR_Readonly])
+ (ExternalCall DTYPE_Void dv nil [FNATTR_Readonly]) C ->
+ initial_frame_res [i_t] [i_s] C -∗
+ (<{{ (make_fn readonly_ex_name readonly_ex nil) (nil) }}> ) ⪯
+ (<{{ (make_fn readonly_ex_name readonly_ex nil) (nil) }}> )
+ [{ fun x y =>
+ initial_frame_res [i_t] [i_s] C }].
+ Proof with clean.
+ iIntros (?); simp attribute_interp in H.
+ destruct H as (?&?).
+ destruct x eqn: Hx; cycle 4; destruct H as (?&?);
+ compute in H; try done; cycle 1.
+ { destruct H0 as (?&?&?); by compute in H0. }
+
+ destruct H0.
+ iIntros "Hi"; iApply (code_to_fn_contextual with "Hi").
+ iModIntro; iIntros (??) "(#HWF & Hbij)".
+
+ rewrite /frame_resources_own -frame_resources_eq.
+ iDestruct "Hbij" as "(Hbij & HC)".
+ rewrite /load_readonly_source_code /load_readonly_target_code.
+ to_instr.
+ iDestruct "HC" as "(HC & HA)".
+ iDestruct "Hbij" as "((Hs_t & Ha_t & Hd_t)&(Hs_s & Ha_s & Hd_s))"...
+
+ iApply sim_expr_bind; iApply (sim_expr_bupd_mono with "[HA]");
+ [ | iApply (sim_instr_alloca_checkout with
+ "Ha_t Ha_s Hd_t Hd_s Hs_t Hs_s HC")];
+ [ | by intro | ..]...
+
+ iDestruct "H" as (????)
+ "(Hl_t & Hl_s & Ha_t & Ha_s & Hd_t & Hd_s &
+ H1_t & H1_s & Hs_t & Hs_s & Hb_t & Hb_s & HC & %Hcn)"...
+
+ target:
+ iApply (target_instr_load1 with "Hl_t H1_t Hd_t Hs_t");
+ [ constructor | cbn; set_solver | ].
+ iModIntro. iIntros "H1 H3 Hl_t Hd_t Hs_t"; target_base.
+
+ source:
+ iApply (source_instr_load1 with "Hl_s H1_s Hd_s Hs_s");
+ [ constructor | cbn; set_solver | ].
+ iIntros "H1_s H3_s Hl_s Hd_s Hs_s"; source_base.
+
+ iApply (sim_insert_loc_bij with "Hl_t Hl_s Hb_t Hb_s").
+ { iApply lb_rel_empty_blocks. }
+ iIntros "#Hbij".
+
+ iApply sim_expr_base; frame_res_exists...
+ iDestruct "HA" as (??????) "HA". iFrame.
+ iExists [l_t0], [l_s0].
+ repeat (iSplitL ""; try eauto using NoDup_singleton); cbn; eauto;
+ try (iPureIntro; set_solver).
+ Qed.
+
+ (* Argmemonly, readonly *)
+ Definition argmemonly_readonly_ex_name : fn_name := "argmemonly_readonly_ex".
+
+ Definition argmemonly_readonly_ex : code dtyp :=
+ (IId (Raw 3), INSTR_Load true (DTYPE_I 32)
+ (DTYPE_I 32, EXP_Ident (ID_Local (Raw 1))) None) :: nil.
+
+ Definition argmemonly_readonly_ex_fn :=
+ make_fn argmemonly_readonly_ex_name argmemonly_readonly_ex nil.
+
+ Lemma argmemonly_readonly_ex_sat dv C i_t i_s l_t l_s:
+ attribute_interp
+ (ExternalCall DTYPE_Void dv [UVALUE_Addr l_t] [FNATTR_Argmemonly; FNATTR_Readonly])
+ (ExternalCall DTYPE_Void dv [UVALUE_Addr l_s] [FNATTR_Argmemonly; FNATTR_Readonly]) C ->
+ l_t ↔h l_s -∗
+ initial_frame_res [i_t] [i_s] C -∗
+ (<{{ (make_fn argmemonly_readonly_ex_name argmemonly_readonly_ex [Raw 1])
+ ([UVALUE_Addr l_t]) }}> ) ⪯
+ (<{{ (make_fn argmemonly_readonly_ex_name argmemonly_readonly_ex [Raw 1])
+ ([UVALUE_Addr l_s]) }}> )
+ [{ fun x y =>
+ initial_frame_res [i_t] [i_s] C }].
+ Proof with clean.
+ iIntros (?); simp attribute_interp in H.
+ destruct H as (?&?).
+ destruct x eqn: Hx; cycle 4; destruct H as (?&?);
+ compute in H; try done;
+ try (destruct H0 as (?&?); by compute in H0).
+ clear H.
+
+ iIntros "#Hl Hi".
+ iApply (code_to_fn_contextual_args with "Hi"); try done.
+ { apply NoDup_singleton. }
+
+ iModIntro; iIntros (??) "(#HWF & Hbij)".
+
+ rewrite /frame_resources_own -frame_resources_eq.
+ rewrite /local_args_own_target /local_args_own_source.
+ iDestruct "Hbij" as "((Hbij & HC) & Hlv_t & Hlv_s)".
+ to_instr.
+ iDestruct "HC" as "(HC & HA)".
+ iDestruct "Hbij" as "((Hs_t & Ha_t & Hd_t)&(Hs_s & Ha_s & Hd_s))"...
+ iDestruct "Hlv_t" as "(Hlv_t & _)"; iDestruct "Hlv_s" as "(Hlv_s & _)".
+
+ specialize (H0 l_t l_s 0%nat eq_refl).
+ destruct H0 as (?&?&?).
+ iApply sim_expr_bind.
+ iApply (sim_expr_bupd_mono with "[Ha_t Ha_s HA]");
+ last (iApply (sim_instr_load_bij_Some with
+ "Hl HC Hd_t Hd_s Hs_t Hs_s Hlv_t Hlv_s");
+ first eauto; try set_solver).
+ 2: try done. 2: try constructor.
+
+ cont.
+ iDestruct "H" as "(HC & Hd_t & Hd_s & Hs_t & Hs_s& H1_t & H1_s & H)".
+
+ iApply sim_expr_base; iFrame.
+ iExists tt, tt; do 2 (iSplitL ""; first done).
+ iFrame "HWF".
+ iExists (instr_laws.Frame ∅ {[Raw 3; Raw 1]}),
+ (instr_laws.Frame ∅ {[Raw 3; Raw 1]}); by iFrame.
+ Qed.
+
+ (* Argmemonly *)
+ Definition argmemonly_ex_name : fn_name := "argmemonly_ex".
+
+ Definition argmemonly_ex : code dtyp :=
+ (IVoid 2, INSTR_Store true
+ (DTYPE_I 32, EXP_Integer 2)
+ (DTYPE_Pointer, EXP_Ident (ID_Local (Raw 1)))
+ None) :: nil.
+
+ Definition argmemonly_ex_fn :=
+ make_fn argmemonly_ex_name argmemonly_ex nil.
+
+ Lemma argmemonly_ex_sat dv C i_t i_s l_t l_s:
+ attribute_interp
+ (ExternalCall DTYPE_Void dv [UVALUE_Addr l_t] [FNATTR_Argmemonly])
+ (ExternalCall DTYPE_Void dv [UVALUE_Addr l_s] [FNATTR_Argmemonly]) C ->
+ l_t ↔h l_s -∗
+ initial_frame_res [i_t] [i_s] C -∗
+ (<{{ (make_fn argmemonly_ex_name argmemonly_ex [Raw 1])
+ ([UVALUE_Addr l_t]) }}> ) ⪯
+ (<{{ (make_fn argmemonly_ex_name argmemonly_ex [Raw 1])
+ ([UVALUE_Addr l_s]) }}> )
+ [{ fun x y =>
+ initial_frame_res [i_t] [i_s] C }].
+ Proof with clean.
+ iIntros (?); simp attribute_interp in H.
+ destruct H as (?&?).
+ destruct x eqn: Hx; cycle 4; destruct H as (?&?);
+ compute in H; try done;
+ try (destruct H0 as (?&?); by compute in H0).
+ clear H.
+
+ iIntros "#Hl Hi".
+ iApply (code_to_fn_contextual_args with "Hi"); try done.
+ { apply NoDup_singleton. }
+
+ iModIntro; iIntros (??) "(#HWF & Hbij)".
+
+ rewrite /frame_resources_own -frame_resources_eq.
+ rewrite /local_args_own_target /local_args_own_source.
+ iDestruct "Hbij" as "((Hbij & HC) & Hlv_t & Hlv_s)".
+ to_instr.
+ iDestruct "HC" as "(HC & HA)".
+ iDestruct "Hbij" as "((Hs_t & Ha_t & Hd_t)&(Hs_s & Ha_s & Hd_s))"...
+ iDestruct "Hlv_t" as "(Hlv_t & _)"; iDestruct "Hlv_s" as "(Hlv_s & _)".
+ destruct H0 as (?&?).
+
+ specialize (H0 l_t l_s 0%nat eq_refl).
+ iApply sim_expr_bind.
+ iAssert (dval_rel
+ (DVALUE_I32 (DynamicValues.Int32.repr 2))
+ (DVALUE_I32 (DynamicValues.Int32.repr 2)))%I as "Hdv".
+ { iApply dval_rel_I32. }
+ iApply (sim_expr_bupd_mono with "[Ha_t Ha_s HA]");
+ last (iApply (sim_instr_store_bij1 with
+ "Hl HC Hd_t Hd_s Hs_t Hs_s Hdv Hlv_t Hlv_s");
+ first eauto; try set_solver).
+ 2: try done. 2: try constructor.
+ 2: iApply target_red_denote_exp_i32.
+ 2: iApply source_red_denote_exp_i32.
+
+ cont.
+ iDestruct "H" as "(HC & Hd_t & Hd_s & Hs_t & Hs_s& H1_t & H1_s)".
+
+ iApply sim_expr_base; iFrame.
+ iExists tt, tt; do 2 (iSplitL ""; first done).
+ iFrame "HWF".
+ iExists (instr_laws.Frame ∅ {[Raw 1]}),
+ (instr_laws.Frame ∅ {[Raw 1]}); by iFrame.
+ Qed.
-Definition argmems_only_args_fn arg : definition dtyp (cfg dtyp) :=
- make_fn argmems_only (argmems_only_args arg) [arg].
+End attr_fns.
diff --git a/theories/vir/instr_laws.v b/theories/vir/instr_laws.v
index 2a42f0c9..bcddbeb9 100644
--- a/theories/vir/instr_laws.v
+++ b/theories/vir/instr_laws.v
@@ -610,6 +610,105 @@ Section instruction_laws.
iApply target_red_tau. by destruct v0.
Qed.
+ Lemma source_instr_load1 l dt du b o L i pid id q Ψ size bytes cid:
+ is_supported dt ->
+ pid ∉ L ->
+ ⊢ l ↦{q}s [ LBlock size bytes cid ] -∗
+ [ id := UVALUE_Addr (l, 0%Z) ]s i -∗
+ ldomain_src i L -∗
+ stack_src i -∗
+ ([ id := UVALUE_Addr (l, 0%Z) ]s i -∗
+ [ pid := (read_in_mem_block bytes 0%Z dt)]s i -∗
+ l ↦{q}s [ LBlock size bytes cid ] -∗
+ ldomain_src i ({[ pid ]} ∪ L) -∗
+ stack_src i -∗
+ source_red (η := vir_handler) (Ret ()) Ψ) -∗
+ source_red (η := vir_handler)
+ (<{ %(IId pid) = (INSTR_Load b dt (du, EXP_Ident (ID_Local id)) o) }>)
+ Ψ.
+ Proof.
+ iIntros (WF Ht) "Hp Hl Hd Hf H".
+
+ cbn. rewrite /instr_conv.
+ iApply source_red_eq_itree.
+ { rewrite interp_bind interp_translate; cbn.
+ rewrite translate_vis interp_vis bind_bind.
+ setoid_rewrite translate_ret.
+ setoid_rewrite interp_ret.
+ setoid_rewrite bind_tau.
+ setoid_rewrite bind_ret_l.
+ rewrite /LU_to_exp; cbn; rewrite /exp_to_instr.
+ simp instrE_conv. reflexivity. }
+
+ iApply source_red_bind.
+ iApply (source_red_mono with "[Hp Hd H] [Hf Hl]");
+ [ | iApply (source_local_read with "Hl Hf"); auto]; cycle 1.
+ { iIntros "Hl Hf".
+ iApply source_red_base.
+ Unshelve.
+ 2 : exact (lift_unary_post (fun x => ⌜x = UVALUE_Addr (l, 0%Z)⌝
+ ∗ stack_src i ∗ [id := UVALUE_Addr (l, 0%Z)]s i)%I).
+ iExists _. do 2 (iSplitL ""; [ done | ]). iFrame. }
+
+ iIntros (?) "HP".
+ iDestruct "HP" as (???) "(Hf & Hl)".
+ iApply source_red_eq_itree.
+ { by rewrite H bind_ret_l. }
+
+ iApply source_red_tau.
+
+ rewrite H0; cbn.
+
+ iApply source_red_eq_itree.
+ { setoid_rewrite interp_bind.
+ setoid_rewrite interp_ret.
+ rewrite bind_ret_l. reflexivity. }
+
+ destruct (dvalue_eq_dec (d1:=DVALUE_Addr (l, 0%Z)) (d2:=DVALUE_Poison)) eqn: Heq ; [ done | ].
+ iApply source_red_eq_itree.
+ { rewrite interp_bind.
+
+ cbn.
+ setoid_rewrite interp_vis.
+ setoid_rewrite interp_ret.
+ Unshelve.
+ 2 : exact (x <- trigger (Load dt (DVALUE_Addr (l, 0%Z))) ;;
+ x <- Tau (trigger (LocalWrite pid x)) ;; Tau (Ret x)).
+ rewrite bind_bind.
+ setoid_rewrite bind_tau.
+ setoid_rewrite bind_ret_l.
+ repeat setoid_rewrite bind_vis.
+ repeat setoid_rewrite bind_ret_l.
+ eapply eqit_Vis; intros.
+ apply eqit_Tau.
+ eapply eqit_Vis; intros. reflexivity. }
+
+ iApply source_red_bind.
+
+ change l with ((l, 0%Z).1) at 1.
+ iApply (source_red_load1 with "Hp").
+
+ iIntros "H'".
+ iApply source_red_base.
+
+ iApply source_red_eq_itree.
+ { by rewrite bind_ret_l !bind_tau. }
+
+ iApply source_red_tau; iApply source_red_bind.
+
+ iApply (source_local_write_alloc _ _ _ _ _ Ht with "Hd Hf").
+ iIntros "Hi H_t H_s".
+
+ iApply source_red_base.
+
+ iApply source_red_eq_itree.
+ { by rewrite bind_ret_l. }
+
+ iApply source_red_tau.
+
+ by iSpecialize ("H" with "Hl Hi H' H_t H_s").
+ Qed.
+
Lemma source_instr_load l dt du b o L i pid v id q Ψ:
is_supported dt ->
dvalue_has_dtyp v dt ->
@@ -1672,6 +1771,122 @@ Section exp_laws.
Unshelve. all : eauto.
Qed.
+ Lemma sim_instr_alloca_checkout
+ l_t l_s dt t o i_t S_t i_s S_s `{non_void dt} L_t L_s C:
+ l_t ∉ L_t ->
+ l_s ∉ L_s ->
+ ⊢ alloca_tgt i_t S_t -∗
+ alloca_src i_s S_s -∗
+ ldomain_tgt i_t L_t -∗
+ ldomain_src i_s L_s -∗
+ stack_tgt i_t -∗
+ stack_src i_s -∗
+ checkout C -∗
+ <{ %(IId l_t) = (INSTR_Alloca dt t o) }> ⪯
+ <{ %(IId l_s) = (INSTR_Alloca dt t o) }>
+ [{ (v_t, v_s), ∃ l_t0 l_s0,
+ ⌜l_t0 ∉ S_t⌝ ∗
+ ⌜l_s0 ∉ S_s⌝ ∗
+ l_t0 ↦t [make_empty_logical_block dt] ∗
+ l_s0 ↦s [make_empty_logical_block dt] ∗
+ alloca_tgt i_t ({[l_t0]} ∪ S_t) ∗
+ alloca_src i_s ({[l_s0]} ∪ S_s) ∗
+ ldomain_tgt i_t ({[ l_t ]} ∪ L_t) ∗
+ ldomain_src i_s ({[ l_s ]} ∪ L_s) ∗
+ [ l_t := UVALUE_Addr (l_t0, 0%Z) ]t i_t ∗
+ [ l_s := UVALUE_Addr (l_s0, 0%Z) ]s i_s ∗
+ stack_tgt i_t ∗
+ stack_src i_s ∗
+ target_block_size l_t0 (Some (N.to_nat (sizeof_dtyp dt))) ∗
+ source_block_size l_s0 (Some (N.to_nat (sizeof_dtyp dt))) ∗
+ checkout C ∗
+ ⌜C !! (l_t0, l_s0) = None⌝
+ }].
+ Proof.
+ iIntros (Hnt Hns) "Ha_t Ha_s Hd_t Hd_s Hf_t Hf_s HC".
+ setoid_rewrite interp_bind.
+ iApply sim_expr_bind.
+
+ assert (Heq : forall dt,
+ instr_conv (trigger (Alloca dt)) ≅
+ x <- trigger (Alloca dt) ;; Tau (Ret x)).
+ { intros. rewrite /instr_conv.
+ rewrite interp_vis. setoid_rewrite interp_ret.
+
+ rewrite /subevent /resum /ReSum_inr /cat /Cat_IFun /inr_ /Inr_sum1.
+ simp instrE_conv. rewrite bind_trigger.
+ reflexivity. }
+ setoid_rewrite Heq.
+
+ iApply sim_expr_bind.
+
+ iApply (sim_expr_bupd_mono with
+ "[HC Hd_t Hd_s] [Hf_t Hf_s Ha_t Ha_s]");
+ [ | iApply (sim_alloca with "Ha_t Ha_s Hf_t Hf_s") ; eauto ].
+ cbn. iIntros (??) "H".
+ iDestruct "H" as (??????????)
+ "(Ht & Hs & Ha_t & Ha_s & Hf_t & Hf_s & Hb_t & Hb_s)"; subst.
+
+ rewrite H H0 !bind_ret_l; subst.
+ iApply sim_expr_tau.
+ iApply sim_expr_base.
+ rewrite !bind_ret_l.
+
+ iApply sim_update_si.
+ iModIntro; iIntros (??) "SI".
+ iDestruct "SI" as (???) "(Hh_s & Hh_t & H_c & Hbij & %WF_SI & SI)".
+
+ iAssert ((¬ ⌜set_Exists (λ '(b_t', b_s'), l_t0 = b_t') S⌝)%I) as "%Hext_t".
+ { iIntros (([b_t' b_s'] & Hin & <-)).
+ iDestruct "Hbij" as "(Hbij & Hheap)".
+ iPoseProof (big_sepS_elem_of with "Hheap") as "Hr"; first by apply Hin.
+ iDestruct "Hr" as (? v_t' v_s') "(Hr_t & Ha_t' & Ha_s')".
+ by iApply (heap_block_size_excl with "Hb_t Ha_t'"). }
+
+ iPoseProof (lb_rel_empty_blocks dt) as "Hrel".
+
+ destruct_HC "Hh_s".
+ iDestruct (ghost_var_agree with "Hf_s HCF") as %Hd_s; subst.
+ iDestruct (ghost_var_agree with "HC H_c") as %Hc_s; subst.
+ rewrite allocaS_eq.
+ iDestruct (ghost_var_agree with "Ha_s HA") as %Hd_s; subst.
+
+ iDestruct "Hh_t" as (cft hFt)
+ "(Hσ_t&HB_t&HCF_t&HA_t&HL_t&HD_t&HSA_t&HG_t&%Hdup_t&%Hbs_t&%Hwf_t)".
+ iDestruct (ghost_var_agree with "Hf_t HCF_t") as %Hd_t; subst.
+ iDestruct (ghost_var_agree with "Ha_t HA_t") as %Hd_t; subst.
+ iFrame.
+
+ iSplitR "Hd_t Hd_s HC Ha_t Ha_s Ht Hs Hb_t Hb_s Hf_t Hf_s".
+ { iExists _, S, G; iFrame.
+ iSplitR "HB_t HCF_t HA_t HL_t HD_t HSA_t".
+ { iModIntro; iExists _, _; iFrame. done. }
+ iSplitR "".
+ { iModIntro; iExists _, _; iFrame. done. }
+ iModIntro. iPureIntro. set_solver. }
+
+ setoid_rewrite instr_conv_localwrite. cbn.
+
+ iApply sim_expr_vis.
+
+ iApply (sim_expr_bupd_mono with
+ "[HC Ht Hs Ha_t Ha_s Hb_t Hb_s] [Hf_t Hf_s Hd_t Hd_s]");
+ [ | iApply (sim_local_write_alloc with "Hd_t Hd_s Hf_t Hf_s") ; eauto ].
+ cbn.
+ iIntros (??) "H".
+ iDestruct "H" as (????) "(Hp_t & Hp_s & Hf_t & Hf_s)".
+ rewrite H1 H2 !bind_ret_l.
+
+ iApply sim_expr_tau; iApply sim_expr_base.
+ iExists tt, tt; destruct v1, v2.
+ do 2 (iSplitL ""; [ done |]).
+ iExists l_t0, l_s0. base. iFrame.
+ iDestruct "Hf_s" as "(?&?&?)"; iFrame.
+ iPureIntro. clear -WF_SI Hext_t.
+ apply not_elem_of_dom_1.
+ set_solver.
+ Qed.
+
Lemma source_instr_bij_load {R} l dt b du o L i pid id Ψ l_t C (e_t : _ R) (k : _ R):
pid ∉ L ->
⊢ l_t ↔h l -∗
@@ -1917,9 +2132,9 @@ Section more_properties.
(λ '(t, op), translate exp_to_instr (denote_exp (Some t) op)) p_s)
[{ (args_t, args_s),
([∗ list] x;y ∈ args_t; args_s, uval_rel x y) ∗
- ⌜∀ (l_t0 l_s0 : loc) (n : nat),
+ ⌜∀ l_t0 l_s0 (n : nat),
nth_error (zip args_t args_s) n =
- Some (# l_t0 ̂, # l_s0 ̂) → C !! (l_t0, l_s0) = None⌝
+ Some (UVALUE_Addr l_t0, UVALUE_Addr l_s0 ) → C !! (l_t0.1, l_s0.1) = None⌝
∗ Q ∗
ldomain_tgt i_t L_t ∗ ldomain_src i_s L_s ∗
stack_tgt i_t ∗ stack_src i_s }]) -∗
@@ -2031,9 +2246,10 @@ Section more_properties.
(λ '(t, op), translate exp_to_instr (denote_exp (Some t) op)) p_s)
[{ (args_t, args_s),
([∗ list] x;y ∈ args_t; args_s, uval_rel x y) ∗
- ⌜∀ (l_t0 l_s0 : loc) (n : nat),
+ ⌜∀ l_t0 l_s0 (n : nat),
nth_error (zip args_t args_s) n =
- Some (# l_t0 ̂, # l_s0 ̂) → C !! (l_t0, l_s0) = None⌝
+ Some (UVALUE_Addr l_t0, UVALUE_Addr l_s0) →
+ C !! (l_t0.1, l_s0.1) = None⌝
∗ Q ∗
ldomain_tgt i_t L_t ∗ ldomain_src i_s L_s ∗
stack_tgt i_t ∗ stack_src i_s }]) -∗
@@ -2320,4 +2536,176 @@ Section more_properties.
by iSpecialize ("H" with "Hl Hi H' H_t H_s").
Qed.
+ Lemma sim_instr_load_bij_Some
+ l_t l_s dt o i_t i_s `{non_void dt} L_t L_s C id_t id_s b du l_t0 l_s0 q:
+ l_t0 ∉ L_t ->
+ l_s0 ∉ L_s ->
+ dtyp_WF dt ->
+ (q < 1)%Qp ->
+ C !! (l_t.1, l_s.1) = Some q ->
+ ⊢ l_t ↔h l_s -∗
+ checkout C -∗
+ ldomain_tgt i_t L_t -∗
+ ldomain_src i_s L_s -∗
+ stack_tgt i_t -∗
+ stack_src i_s -∗
+ [ id_t := UVALUE_Addr l_t ]t i_t -∗
+ [ id_s := UVALUE_Addr l_s ]s i_s -∗
+ <{ %(IId l_t0) =
+ (INSTR_Load b dt (du, EXP_Ident (ID_Local id_t)) o) }> ⪯
+ <{ %(IId l_s0) =
+ (INSTR_Load b dt (du, EXP_Ident (ID_Local id_s)) o)}>
+ [{ (v_t, v_s),
+ checkout C ∗
+ ldomain_tgt i_t ({[ l_t0 ]} ∪ L_t) ∗
+ ldomain_src i_s ({[ l_s0 ]} ∪ L_s) ∗
+ stack_tgt i_t ∗
+ stack_src i_s ∗
+ [ id_t := UVALUE_Addr l_t ]t i_t ∗
+ [ id_s := UVALUE_Addr l_s ]s i_s ∗
+ ∃ v_t v_s,
+ [ l_t0 := v_t ]t i_t ∗ [ l_s0 := v_s ]s i_s ∗
+ uval_rel v_t v_s
+ }].
+ Proof.
+ iIntros (Ht Hs WF Hq Hc) "#Hl HC Hd_t Hd_s Hf_t Hf_s Hid_t Hid_s".
+ setoid_rewrite interp_bind.
+ iApply sim_expr_bind; iApply exp_conv_to_instr.
+
+ iApply (sim_expr_bupd_mono with "[HC Hd_t Hd_s]");
+ [ | iApply (sim_local_read_exp_conv with "Hf_t Hf_s Hid_t Hid_s")].
+
+ cont.
+ iDestruct "H" as (??) "(Hf_t & Hf_s & Hid_t & Hid_s)"; subst.
+ cbn. rewrite !bind_ret_l.
+ destruct (dvalue_eq_dec
+ (d1:=DVALUE_Addr l_t)
+ (d2:=DVALUE_Poison)) eqn: Heq ; [ done | ]; clear Heq.
+ destruct (dvalue_eq_dec
+ (d1:=DVALUE_Addr l_s)
+ (d2:=DVALUE_Poison)) eqn: Heq ; [ done | ]; clear Heq.
+ rewrite !interp_bind !interp_vis !bind_bind; iApply sim_expr_bind.
+
+ iApply (sim_expr_bupd_mono with "[Hd_t Hd_s Hf_t Hf_s Hid_t Hid_s]");
+ last iApply (bij_laws.sim_bij_load_Some with "Hl HC"); eauto.
+
+ cont.
+
+ rewrite !bind_tau !interp_ret !bind_ret_l.
+ iApply sim_expr_tau.
+ setoid_rewrite instr_conv_localwrite.
+
+ iApply sim_expr_vis.
+
+ iApply (sim_expr_bupd_mono with "[Hid_t Hid_s H]"); last
+ iApply (sim_local_write_alloc _ _ _ _ _ _ _ _ Ht Hs with
+ "Hd_t Hd_s Hf_t Hf_s").
+ iDestruct "H" as "(#Hv & HC)".
+
+ cont.
+ iApply sim_expr_tau; iApply sim_expr_base; iFrame.
+ iDestruct "H" as "(Hid_t & Hid_s & Hd_t & Hd_s & Hs_t & Hs_s)".
+ iExists _, _; iFrame; try done.
+ do 2 (iSplitL ""; [ done | ]). iExists _, _; by iFrame.
+ Qed.
+
+ Lemma sim_instr_store_bij1 vt vs
+ l_t l_s dt o i_t i_s `{non_void dt} L_t L_s C id_t id_s
+ b v_t v_s val_t val_s:
+ dtyp_WF dt ->
+ dvalue_has_dtyp_fun v_t dt ->
+ dvalue_has_dtyp_fun v_s dt ->
+ C !! (l_t.1, l_s.1) = None ->
+ ⊢ l_t ↔h l_s -∗
+ checkout C -∗
+ ldomain_tgt i_t L_t -∗
+ ldomain_src i_s L_s -∗
+ stack_tgt i_t -∗
+ stack_src i_s -∗
+ dval_rel v_t v_s -∗
+ [ id_t := UVALUE_Addr l_t ]t i_t -∗
+ [ id_s := UVALUE_Addr l_s ]s i_s -∗
+ target_red (η := vir_handler)
+ (exp_conv (denote_exp (Some dt) val_t))
+ (lift_unary_post
+ (fun x =>
+ ⌜is_concrete x⌝ ∗ ⌜dvalue_to_uvalue v_t = x⌝ ∗
+ ⌜dvalue_has_dtyp_fun v_t dt⌝)) -∗
+ source_red (η := vir_handler)
+ (exp_conv (denote_exp (Some dt) val_s))
+ (lift_unary_post
+ (fun x =>
+ ⌜is_concrete x⌝ ∗ ⌜dvalue_to_uvalue v_s = x⌝ ∗
+ ⌜dvalue_has_dtyp_fun v_s dt⌝)) -∗
+ <{ %(IVoid vt) =
+ (INSTR_Store b (dt, val_t)
+ (DTYPE_Pointer, EXP_Ident (ID_Local id_t)) o) }> ⪯
+ <{ %(IVoid vs) =
+ (INSTR_Store b (dt, val_s)
+ (DTYPE_Pointer, EXP_Ident (ID_Local id_s)) o) }>
+ [{ (x_t, x_s),
+ checkout C ∗
+ ldomain_tgt i_t L_t ∗
+ ldomain_src i_s L_s ∗
+ stack_tgt i_t ∗
+ stack_src i_s ∗
+ [ id_t := UVALUE_Addr l_t ]t i_t ∗
+ [ id_s := UVALUE_Addr l_s ]s i_s }].
+ Proof.
+ iIntros (WF Htyp_t Htyp_s H)
+ "#Hl HC Hd_t Hd_s Hf_t Hf_s #Hdv Hid_t Hid_s Hdt Hds".
+
+ setoid_rewrite interp_bind.
+ iApply sim_expr_bind; iApply exp_conv_to_instr.
+ iApply source_red_sim_expr.
+ iApply (source_red_mono with "[HC Hd_t Hd_s Hf_t Hf_s Hid_t Hid_s Hdt]");
+ last iApply "Hds".
+ iIntros (?) "H".
+ iDestruct "H" as (????) "%Hv"; subst.
+ rewrite H0; clear H0.
+
+ iApply target_red_sim_expr.
+ iApply (target_red_mono with "[HC Hd_t Hd_s Hf_t Hf_s Hid_t Hid_s]");
+ last iApply "Hdt".
+ iIntros (?) "H".
+ iDestruct "H" as (????) "%Hv'"; subst.
+ rewrite H0; clear H0.
+ iApply sim_expr_base.
+ rewrite !bind_ret_l. cbn.
+ rewrite /concretize_or_pick !is_concrete_dvalue_to_uvalue.
+ rewrite !uvalue_to_dvalue_of_dvalue_to_uvalue !interp_bind.
+ rewrite /lift_err !interp_ret !bind_ret_l.
+ destruct (dvalue_has_dtyp_fun v_t dt) eqn: Hv_t; try inversion Hv'.
+ destruct (dvalue_has_dtyp_fun v_s dt) eqn: Hv_s; try inversion Hv.
+ rewrite !interp_bind.
+
+ iApply sim_expr_bind; iApply exp_conv_to_instr.
+
+ iApply (sim_expr_bupd_mono with "[HC Hd_t Hd_s]");
+ [ | iApply (sim_local_read_exp_conv with "Hf_t Hf_s Hid_t Hid_s")].
+
+ cont.
+ iDestruct "H" as (??) "(Hf_t & Hf_s & Hid_t & Hid_s)"; subst.
+ cbn. rewrite !bind_ret_l.
+ destruct (dvalue_eq_dec
+ (d1:=DVALUE_Addr l_t)
+ (d2:=DVALUE_Poison)) eqn: Heq ; [ done | ]; clear Heq.
+ destruct (dvalue_eq_dec
+ (d1:=DVALUE_Addr l_s)
+ (d2:=DVALUE_Poison)) eqn: Heq ; [ done | ]; clear Heq.
+ rewrite !interp_vis; iApply sim_expr_bind.
+
+ iApply (sim_expr_bupd_mono with "[Hd_t Hd_s Hf_t Hf_s Hid_t Hid_s]");
+ last iApply (bij_laws.sim_bij_store1 with "Hdv Hl HC");
+ eauto.
+ 2,3 : by eapply dvalue_has_dtyp_fun_sound.
+
+ cont.
+
+ rewrite !interp_ret; iApply sim_expr_tau.
+ iApply sim_expr_base; iFrame.
+
+ iExists _, _; iFrame; try done.
+ Qed.
+
End more_properties.
diff --git a/theories/vir/logical_relations.v b/theories/vir/logical_relations.v
index 6741e666..96c4277d 100644
--- a/theories/vir/logical_relations.v
+++ b/theories/vir/logical_relations.v
@@ -1107,4 +1107,5 @@ Section logical_relations_properties.
Unshelve. all : set_solver.
Qed.
+
End logical_relations_properties.
diff --git a/theories/vir/spec.v b/theories/vir/spec.v
index eca19d65..7fa5eb64 100644
--- a/theories/vir/spec.v
+++ b/theories/vir/spec.v
@@ -34,7 +34,7 @@ Definition HasAttr : fn_attr -> list fn_attr -> bool :=
| nil => false
| l =>
foldl (fun p b =>
- p && (Coqlib.proj_sumbool (decide (b = attr)))) true l
+ p || (Coqlib.proj_sumbool (decide (b = attr)))) false l
end.
Definition HaveAttr : fn_attr -> list fn_attr -> list fn_attr -> bool :=
@@ -79,21 +79,28 @@ Section spec.
∃ (c : attr_case),
match c with
| ARG_READ => have FNATTR_Argmemonly && have FNATTR_Readonly /\
- (∀ (l_t l_s : Z) n,
- nth_error (zip args_t args_s) n = Some (# l_t̂, # l_ŝ) ->
- ∃ q, C !! (l_t, l_s) = Some q ∧ Qp.lt q 1)
+ (∀ l_t l_s n,
+ nth_error (zip args_t args_s) n =
+ Some (UVALUE_Addr l_t, UVALUE_Addr l_s) ->
+ ∃ q, C !! (l_t.1, l_s.1) = Some q ∧ Qp.lt q 1)
| WRITEONLY => have FNATTR_Writeonly /\ C = ∅
| NOFREE => have FNATTR_Nofree /\ C = ∅
| ARGMONLY => have FNATTR_Argmemonly /\ not (have FNATTR_Readonly) /\
- (∀ (l_t l_s : loc) n,
- nth_error (zip args_t args_s) n = Some (#l_t̂, #l_ŝ) ->
- C !! (l_t, l_s) = None)
+ (∀ l_t l_s n,
+ nth_error (zip args_t args_s) n =
+ Some (UVALUE_Addr l_t, UVALUE_Addr l_s) ->
+ C !! (l_t.1, l_s.1) = None)
| READONLY => have FNATTR_Readonly /\ not (have FNATTR_Argmemonly) /\
(∀ (l_t l_s : loc) q, C !! (l_t, l_s) = Some q -> Qp.lt q 1)
| INACC_OR_ARGMONLY => have FNATTR_Inaccessiblemem_or_argmemonly /\
- (∀ (l_t l_s : loc) n,
- nth_error (zip args_t args_s) n = Some (#l_t̂, # l_ŝ) ->
- C !! (l_t, l_s) = None)
+ (∀ l_t l_s n,
+ nth_error (zip args_t args_s) n =
+ Some (UVALUE_Addr l_t, UVALUE_Addr l_s) ->
+ C !! (l_t.1, l_s.1) = None) /\
+ (∀ (l_t l_s : Z * Z),
+ (l_t.1, l_s.1) ∈ dom C ->
+ (UVALUE_Addr l_t, UVALUE_Addr l_s) ∉ (zip args_t args_s) ->
+ C !! (l_t.1, l_s.1) = Some 1%Qp)
| OTHER =>
not (have FNATTR_Argmemonly) /\
not (have FNATTR_Readonly) /\
--
GitLab