Skip to content

Commit 4c7a81b

Browse files
pgiarrusso-slpgiarrusso-sl
committed
step 1
1 parent 41f0dd6 commit 4c7a81b

2 files changed

Lines changed: 109 additions & 58 deletions

File tree

‎rocq-brick-libstdcpp/proof/mutex/demo_cpp_proof.v‎

Lines changed: 107 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ Definition CR
3939
structR "C" q **
4040
_field "C::mut" |-> recursive_mutex.R γ.(recursive_mutex.lock_gname) q **
4141
as_Rep (fun this : ptr =>
42-
recursive_mutex.inv_rmutex γ (∃ a b, this |-> CR' a b)).
42+
recursive_mutex.inv_rmutex γ (∃ a_b : tele_arg _, tele_app (P this) a_b)).
4343

4444
#[only(cfractional,ascfractional,type_ptr)] derive CR.
4545
#[only(lazy_unfold)] derive CR.
@@ -75,83 +75,142 @@ Section with_cpp.
7575
\arg{x} "x" (Vint x)
7676
\prepost{γ q} this |-> CR γ q
7777
\prepost{q'} recursive_mutex.token γ.(recursive_mutex.lock_gname) q'
78-
\pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (fun a b => this |-> CR' a b)
79-
\post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) b) args) (fun a b => this |-> CR' a b)).
78+
\pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (P this)
79+
\post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) b) args) (P this)).
8080

8181
cpp.spec "C::update_b(long)" as C_update_b from demo_cpp.source with
8282
(\this this
8383
\arg{x} "x" (Vint x)
8484
\prepost{γ q} this |-> CR γ q
8585
\prepost{q'} recursive_mutex.token γ.(recursive_mutex.lock_gname) q'
86-
\pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (fun a b => this |-> CR' a b)
87-
\post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk a (trim 64 (b + x))) args) (fun a b => this |-> CR' a b)).
86+
\pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (P this)
87+
\post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk a (trim 64 (b + x))) args) (P this)).
8888

8989
#[global] Instance CR_learn : Cbn (Learn (learn_eq ==> any ==> learn_hints.fin) CR).
9090
Proof. solve_learnable. Qed.
9191

92-
Lemma tele_app_mk_beta (P : Z -> Z -> mpred) (x y : Z) :
93-
tele_app (TT := TT) (λ a b : Z, P a b) (mk x y) = P x y.
94-
Proof. reflexivity. Qed.
92+
Import recursive_mutex.
9593

96-
(** "Eta-expand" [∃ xy : TT, ... tele_app P xy ... ] to [∃ (x y : Z), ... tele_app P (mk x y) ...].
97-
This is useful because [tele_app (λ a b : Z, Q a b) (mk x y)] simplifies to [Q x y] ([tele_app_mk_beta]). *)
98-
#[program] Definition learn_args_C (P : TT -t> mpred) :=
99-
\cancelx
100-
\bound_existential args
101-
\proving tele_app P args
102-
\exist a b
103-
\instantiate args := mk a b
104-
\through tele_app P (mk a b)
105-
\end.
106-
Next Obligation. work. Qed.
107-
#[local] Hint Resolve learn_args_C : br_hints.
94+
#[global] Instance: `{Proper (equiv ==> equiv) (inv_rmutex γ)}.
95+
Proof. rewrite inv_rmutex.unlock. solve_proper. Qed.
10896

109-
#[program] Definition P_unfold_split_args_F this args :=
97+
#[program]
98+
Definition inv_rmutex_iff_C γ :=
11099
\cancelx
111-
\consuming tele_app (P this) args
112-
\intro a
113-
\intro b
114-
\deduce tele_app (TT := TT) (fun a b => this |-> CR' a b) (mk a b)
115-
\deduce [| args = mk a b |]
100+
\preserving{P1} inv_rmutex γ P1
101+
\proving{P2} inv_rmutex γ P2
102+
\through [| P1 ⊣⊢@{mpredI} P2 |]
116103
\end.
117-
Next Obligation. iIntros (this [a [b []]]) "/= ?". iExists a, b. rewrite P.unlock. work. Qed.
104+
Next Obligation. work. by setoid_subst. Qed.
105+
#[local] Hint Resolve inv_rmutex_iff_C : br_hints.
118106

119-
#[program] Definition P_unfold_B :=
107+
#[program]
108+
Definition inv_rmutex_wand_C γ :=
120109
\cancelx
121-
\bound this a b
122-
\proving P this a b
123-
\through this |-> CR' a b
110+
\preserving{P1} inv_rmutex γ P1
111+
\proving{P2} inv_rmutex γ P2
112+
\through □ (P1 ∗-∗ P2)
124113
\end.
125-
Next Obligation. rewrite P.unlock. work. Qed.
114+
Next Obligation.
115+
rewrite inv_rmutex.unlock.
116+
iIntros "%% A %P2 #[? ?]".
117+
iApply (inv_iff with "A").
118+
iIntros "!> !>"; iSplit; ework with br_erefl; case_match; work.
119+
Qed.
120+
(* #[local] Hint Resolve inv_rmutex_wand_C : br_hints. *)
121+
122+
Lemma CR'_tele_equiv (this : ptr) :
123+
(∃ a b : Z, this |-> CR' a b) ⊣⊢
124+
∃ xs : TT, tele_app (TT := TT) (λ a b : Z, this |-> CR' a b) xs.
125+
Proof.
126+
iSplit.
127+
{ iDestruct 1 as (a b) "?"; iExists (mk a b); work. }
128+
iDestruct 1 as ([a [b []]]) "?"; iExists a, b; work.
129+
Qed.
130+
#[local] Hint Resolve CR'_tele_equiv : br_hints.
126131

127-
Section unfold_P.
128-
#[local] Hint Resolve P_unfold_split_args_F : br_hints.
129-
#[local] Hint Resolve P_unfold_B : br_hints.
132+
Lemma CR'_self_eq (this : ptr) :
133+
(∃ a b : Z, this |-> CR' a b) ⊣⊢
134+
(∃ a b : Z, this |-> CR' a b).
135+
Proof. done. Qed.
136+
#[local] Hint Resolve CR'_self_eq : br_hints.
130137

131-
Lemma update_a_ok : verify[source] "C::update_a(long)".
132-
Proof.
133-
verify_spec; go.
134-
Qed.
138+
Lemma refl_equiv (P : mpred) : P ⊣⊢ P.
139+
Proof. done. Qed.
140+
#[local] Hint Resolve refl_equiv : br_hints.
135141

136-
Lemma update_b_ok : verify[source] "C::update_b(long)".
137-
Proof.
138-
verify_spec; go.
139-
Qed.
140-
End unfold_P.
142+
Lemma CR'_P_tele_equiv (this : ptr) :
143+
(∃ a_b : TT, tele_app (TT := TT) (λ a b, this |-> CR' a b) a_b) ⊣⊢
144+
(∃ a_b : TT, tele_app (P this) a_b).
145+
Proof. by rewrite P.unlock. Qed.
146+
#[local] Hint Resolve CR'_P_tele_equiv : br_hints.
147+
148+
Lemma update_a_ok : verify[source] "C::update_a(long)".
149+
Proof.
150+
verify_spec; go.
151+
iExists TT.
152+
go.
153+
rewrite P.unlock.
154+
destruct args as [a [b []]]; simpl; go.
155+
iExists TT, (P this), _, (mk (trim 64 (a + x)) b).
156+
go.
157+
rewrite P.unlock.
158+
go.
159+
rewrite P.unlock.
160+
go.
161+
all: fail.
162+
Fail Qed.
163+
Admitted.
164+
165+
Lemma update_b_ok : verify[source] "C::update_b(long)".
166+
Proof.
167+
verify_spec; go.
168+
iExists TT.
169+
go.
170+
171+
rewrite P.unlock.
172+
destruct args as [a [b []]]; simpl; go.
173+
iExists TT, _, _, (mk a (trim 64 (b + x))).
174+
go.
175+
rewrite P.unlock.
176+
go.
177+
rewrite P.unlock.
178+
go.
179+
all: fail.
180+
Fail Qed.
181+
Admitted.
141182

142183
cpp.spec "C::transfer(int)" as C_transfer_int from demo_cpp.source with
143184
(\this this
144185
\arg{x} "x" (Vint x)
145186
\prepost{γ q} this |-> CR γ q
146187
\prepost{q'} recursive_mutex.token γ.(recursive_mutex.lock_gname) q'
147-
\pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (P this)
148-
\post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) (trim 64 (b-x))) args) (P this)).
188+
\pre{args th} recursive_mutex.acquireable γ th args (TT:=TT) (fun a b => this |-> CR' a b)
189+
\post recursive_mutex.acquireable γ th (TT:=TT) (recursive_mutex.update (TT:=TT) (fun (a b : Z) => mk (trim 64 (a+x)) (trim 64 (b-x))) args) (fun a b => this |-> CR' a b)).
190+
191+
Lemma P_CR'_tele_equiv (this : ptr) :
192+
(∃ a_b : TT, tele_app (P this) a_b) ⊣⊢
193+
(∃ a_b : TT, tele_app (TT := TT) (λ a b, this |-> CR' a b) a_b).
194+
Proof. by rewrite P.unlock. Qed.
195+
#[local] Hint Resolve P_CR'_tele_equiv : br_hints.
149196

150197
Lemma transfer_ok : verify[source] "C::transfer(int)".
151198
Proof.
152199
verify_spec; go.
153-
destruct args as [a [b []]]; work.
154-
Qed.
200+
iExists TT.
201+
go.
202+
iExists (Held _ args).
203+
destruct args as [a [b []]]; simpl.
204+
go.
205+
rewrite P.unlock.
206+
go.
207+
rewrite P.unlock.
208+
go.
209+
iExists TT.
210+
go.
211+
all: fail.
212+
Fail Qed.
213+
Admitted.
155214

156215
Lemma partial_transfer_link :
157216
denoteModule source ∗

‎rocq-brick-libstdcpp/proof/mutex/spec.v‎

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -329,14 +329,12 @@ Section with_cpp.
329329
Next Obligation. rewrite acquireable.unlock; work. Qed.
330330

331331
#[program]
332-
Definition own_P_is_acquireable_C {TT} g n P :=
332+
Definition own_P_is_acquireable_C {TT} g n P args :=
333333
\cancelx
334334
\preserving{th} current_thread th
335335
\consuming own g.(level_gname) (◯E (S n, th))
336-
\bound n' args
337-
\proving acquireable (TT := TT) g th (Held n' args) P
338336
\through tele_app P args
339-
\through [| n' = n |]
337+
\proving acquireable (TT := TT) g th (Held n args) P
340338
\end.
341339
Next Obligation. rewrite acquireable.unlock; work. Qed.
342340

@@ -352,12 +350,6 @@ Section with_cpp.
352350
[γ2 = γ1] }.
353351
Proof. solve_learnable. Qed.
354352

355-
#[global] Instance learn_inv_rmutex_TT : `{Learnable
356-
(inv_rmutex γ (∃ xs : tele_arg TT1, tele_app P1 xs))
357-
(inv_rmutex γ (∃ xs : tele_arg TT2, tele_app P2 xs))
358-
[TT2 = TT1] }.
359-
Proof. solve_learnable. Qed.
360-
361353
#[global] Instance learn_inv_rmutex_P TT : `{Learnable
362354
(inv_rmutex γ1 (∃ xs : tele_arg TT, tele_app P1 xs))
363355
(inv_rmutex γ2 (∃ xs : tele_arg TT, tele_app P2 xs))

0 commit comments

Comments
 (0)