-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathrefs_implicit.v
144 lines (139 loc) · 6.33 KB
/
refs_implicit.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
From iris.proofmode Require Import tactics.
From mwp.mwp_modalities Require Import mwp_step_fupd.
From mwp.mwp_modalities.ni_logrel Require Import mwp_left mwp_right ni_logrel_lemmas
mwp_logrel_fupd ni_logrel_fupd_lemmas.
From logrel_ifc.lambda_sec Require Export lattice fundamental_binary notation.
(* This is an implicit variation of [refs.v] where we leak (temporarily)
information through an implicit flow but fix it before returning. *)
Definition prog : expr:=
(if: !$1 = 42 then $0 <- 1 else $0 <- 0);; $0 <- 0.
Local Instance tpSecurityLatticeH : SecurityLattice tplabel := { ζ := L }.
Notation H := (LLabel H).
Notation L := (LLabel L).
Section related.
Context `{!secG Σ}.
Lemma prog_related :
[TRef (TNat @ L) @ L; TRef (TNat @ H) @ L] ⊨ prog ≤ₗ prog : TUnit @ L.
Proof.
iIntros (θ ρ vvs Hpers) "[#Hcoh Henv]".
iDestruct (interp_env_length with "Henv") as %H.
do 2 (destruct vvs; [done|]); clear H.
iDestruct (interp_env_cons with "Henv") as "[Hlow Henv']".
iDestruct (interp_env_cons with "Henv'") as "[Hhigh _]".
rewrite !interp_sec_def !bool_decide_eq_true_2 // !interp_ref_def.
iDestruct "Hlow" as ([l1 l2]) "[-> #Hlow] /=".
iDestruct "Hhigh" as ([h1 h2]) "[-> #Hhigh] /=".
rewrite /interp_expr /=.
iApply (mwp_left_strong_bind _ _ (fill [BinOpLCtx _ _; IfCtx _ _; SeqCtx _])
(fill [BinOpLCtx _ _; IfCtx _ _; SeqCtx _])); simpl.
iApply (mwp_double_atomic_lr _ _ StronglyAtomic).
iInv (nroot.@(h1,h2)) as "Hh" "Hclose !>".
iDestruct "Hh" as (v1 v2) "(>Hh1 & >Hh2 & #Hv) /=".
rewrite !loc_to_val.
iApply (@mwp_step_fupd_load _ secG_un_left); [done|].
iFrame. iIntros "!> Hh1".
iApply (@mwp_fupd_load _ secG_un_right); [done|].
iFrame. iIntros "Hh2 /=".
iMod ("Hclose" with "[-]") as "_".
{ iExists _,_. iFrame. iFrame "#". }
iModIntro.
iDestruct (secbin_subsumes_secun with "[$Hcoh $Hv]") as "[#Hv1 #Hv2] /=".
rewrite ![⌊ TNat @ _ ⌋ₛ _ _]interp_un_sec_def !interp_un_nat_def.
iDestruct "Hv1" as (n1) "->". iDestruct "Hv2" as (n2) "->".
iApply (mwp_left_strong_bind _ _ (fill [IfCtx _ _; SeqCtx _])
(fill [IfCtx _ _; SeqCtx _])); simpl.
rewrite !nat_to_val.
iApply mwp_left_pure_step; [done|].
iApply mwp_left_pure_step_index; [done|]. simpl.
iApply (mwp_value mwp_binary); umods.
iApply (mwp_value (mwpd_right SI_right)); umods.
do 2 iModIntro.
iApply ni_logrel_fupd_ni_logrel. iSplit.
{ iLeft. iIntros (σ) "Hσ".
iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
iModIntro. iPureIntro.
eapply (fill_reducible [SeqCtx _]).
apply head_prim_reducible.
case_bool_decide; eexists [],_,_,[]; by econstructor. }
iInv (nroot.@(l1,l2)) as "Hl" "HcloseI".
iDestruct "Hl" as (w1 w2) "(Hl1 & Hl2 & _) /=".
do 2 iModIntro.
iApply mwp_un_bi_fupd_lr.
iApply (mwp_fupd_bind _ (fill [SeqCtx _])).
case_bool_decide.
- (* left then branch *)
iApply mwp_fupd_pure_step; [done|].
rewrite !loc_to_val !nat_to_val.
iApply ((@mwp_fupd_store _ secG_un_left)); [done|].
iFrame. iIntros "Hl1".
iApply mwp_fupd_pure_step; [done|].
iApply ((@mwp_fupd_store _ secG_un_left)); [done|].
iFrame. iIntros "Hl1".
case_bool_decide.
+ (* right then branch *)
iApply (mwp_fupd_bind _ (fill [SeqCtx _])).
iApply (mwp_fupd_pure_step); [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iApply mwp_fupd_pure_step; [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iMod ("HcloseI" with "[-]") as "_".
{ iExists _,_. iModIntro. iFrame. unats.
rewrite [bool_decide (⌊ L ⌋ₗ ρ ⊑ ζ)]bool_decide_eq_true_2 //=; auto. }
iIntros "!> /=".
rewrite [⟦ () @ L ⟧ₛ _ _ _]interp_sec_def interp_unit_def
bool_decide_eq_true_2 //.
+ (* right else branch *)
iApply (mwp_fupd_bind _ (fill [SeqCtx _])).
iApply (mwp_fupd_pure_step); [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iApply mwp_fupd_pure_step; [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iMod ("HcloseI" with "[-]") as "_".
{ iExists _,_. iModIntro. iFrame. unats.
rewrite [bool_decide (⌊ L ⌋ₗ ρ ⊑ ζ)]bool_decide_eq_true_2 //=; auto. }
iIntros "!> /=".
rewrite [⟦ () @ L ⟧ₛ _ _ _]interp_sec_def interp_unit_def
bool_decide_eq_true_2 //.
- (* left else branch - identical to above *)
iApply mwp_fupd_pure_step; [done|].
rewrite !loc_to_val !nat_to_val.
iApply ((@mwp_fupd_store _ secG_un_left)); [done|].
iFrame. iIntros "Hl1".
iApply mwp_fupd_pure_step; [done|].
iApply ((@mwp_fupd_store _ secG_un_left)); [done|].
iFrame. iIntros "Hl1".
case_bool_decide.
+ (* right then branch *)
iApply (mwp_fupd_bind _ (fill [SeqCtx _])).
iApply (mwp_fupd_pure_step); [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iApply mwp_fupd_pure_step; [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iMod ("HcloseI" with "[-]") as "_".
{ iExists _,_. iModIntro. iFrame. unats.
rewrite [bool_decide (⌊ L ⌋ₗ ρ ⊑ ζ)]bool_decide_eq_true_2 //=; auto. }
iIntros "!> /=".
rewrite [⟦ () @ L ⟧ₛ _ _ _]interp_sec_def interp_unit_def
bool_decide_eq_true_2 //.
+ (* right else branch *)
iApply (mwp_fupd_bind _ (fill [SeqCtx _])).
iApply (mwp_fupd_pure_step); [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iApply mwp_fupd_pure_step; [done|].
iApply ((@mwp_fupd_store _ secG_un_right)); [done|].
iFrame. iIntros "Hl2".
iMod ("HcloseI" with "[-]") as "_".
{ iExists _,_. iModIntro. iFrame. unats.
rewrite [bool_decide (⌊ L ⌋ₗ ρ ⊑ ζ)]bool_decide_eq_true_2 //=; auto. }
iIntros "!> /=".
rewrite [⟦ () @ L ⟧ₛ _ _ _]interp_sec_def interp_unit_def
bool_decide_eq_true_2 //.
Qed.
End related.