Commit b62c6ecc authored by Michael Sammler's avatar Michael Sammler
Browse files

autogenerate definition of latch

parent 35f1917d
Pipeline #42113 passed with stage
in 14 minutes and 37 seconds
......@@ -5,24 +5,22 @@
#include <stdbool.h>
#include <stdatomic.h>
//@rc::import latch_def from refinedc.examples.latch
//@rc::require refinedc.examples.latch
struct latch {
struct [[rc::refined_by("P : {iProp Σ}")]] latch {
[[rc::field("atomic_bool<bool_it, {(□ P)}, True>")]]
atomic_bool released;
};
#define LATCH_INIT ((struct latch){.released = false})
[[rc::parameters("p : loc", "beta : own_state", "P : {iProp Σ}")]]
[[rc::args("p @ &frac<beta, latch<P>>")]]
[[rc::ensures("frac beta p : latch<P>", "[P]")]]
[[rc::args("p @ &frac<beta, P @ latch>")]]
[[rc::ensures("frac beta p : P @ latch", "[P]")]]
void latch_wait(struct latch* latch);
[[rc::parameters("p : loc", "beta : own_state", "P : {iProp Σ}")]]
[[rc::args("p @ &frac<beta, latch<P>>")]]
[[rc::args("p @ &frac<beta, P @ latch>")]]
[[rc::requires("[□ P]")]]
[[rc::ensures("frac beta p : latch<P>")]]
[[rc::ensures("frac beta p : P @ latch")]]
void latch_release(struct latch* latch);
#endif
From refinedc.typing Require Import typing.
From refinedc.examples.latch Require Import generated_code.
From refinedc.examples.latch Require Import generated_spec.
From refinedc.examples.latch Require Import latch_def.
Set Default Proof Using "Type".
(* Generated from [examples/latch.c]. *)
......
From refinedc.typing Require Import typing.
From refinedc.examples.latch Require Import generated_code.
From refinedc.examples.latch Require Import generated_spec.
From refinedc.examples.latch Require Import latch_def.
Set Default Proof Using "Type".
(* Generated from [examples/latch.c]. *)
......@@ -16,7 +15,7 @@ Section proof_latch_wait.
start_function "latch_wait" ([[p beta] P]) => arg_latch.
split_blocks ((
<[ "#1" :=
arg_latch ◁ₗ (p @ (&frac{beta} (latch (P))))
arg_latch ◁ₗ (p @ (&frac{beta} (P @ (latch))))
]> $
)%I : gmap label (iProp Σ)) ((
......
From refinedc.typing Require Import typing.
From refinedc.examples.latch Require Import generated_code.
From refinedc.examples.latch Require Import latch_def.
Set Default Proof Using "Type".
(* Generated from [examples/latch.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Definition of type [latch]. *)
Definition latch_rec : ((iProp Σ) -d> typeO) ((iProp Σ) -d> typeO) := (λ self P,
struct struct_latch [@{type}
(atomic_bool (bool_it) (( P)) (True))
]
)%I.
Typeclasses Opaque latch_rec.
Global Instance latch_rec_ne : Contractive latch_rec.
Proof. solve_type_proper. Qed.
Definition latch : rtype := {|
rty_type := (iProp Σ);
rty r__ := fixp latch_rec r__
|}.
Lemma latch_unfold (P : (iProp Σ)):
(P @ latch)%I @{type} (
struct struct_latch [@{type}
(atomic_bool (bool_it) (( P)) (True))
]
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
Global Program Instance latch_rmovable : RMovable latch :=
{| rmovable patt__ := movable_eq _ _ (latch_unfold patt__) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance latch_simplify_hyp_place_inst l_ β_ patt__:
SimplifyHypPlace l_ β_ (patt__ @ latch)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (latch_unfold _)).
Global Instance latch_simplify_goal_place_inst l_ β_ patt__:
SimplifyGoalPlace l_ β_ (patt__ @ latch)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (latch_unfold _)).
Global Program Instance latch_simplify_hyp_val_inst v_ patt__:
SimplifyHypVal v_ (patt__ @ latch)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (latch_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance latch_simplify_goal_val_inst v_ patt__:
SimplifyGoalVal v_ (patt__ @ latch)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (latch_unfold _) T _).
Next Obligation. done. Qed.
(* Type definitions. *)
(* Function [atomic_thread_fence] has been skipped. *)
......@@ -15,11 +59,13 @@ Section spec.
(* Specifications for function [latch_wait]. *)
Definition type_of_latch_wait :=
fn( (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (latch (P)))); True)
() : (), (void); (p ◁ₗ{beta} (latch (P))) (P).
fn( (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (P @ (latch)))); True)
() : (), (void); (p ◁ₗ{beta} (P @ (latch))) (P).
(* Specifications for function [latch_release]. *)
Definition type_of_latch_release :=
fn( (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (latch (P)))); ( P))
() : (), (void); (p ◁ₗ{beta} (latch (P))).
fn( (p, beta, P) : loc * own_state * (iProp Σ); (p @ (&frac{beta} (P @ (latch)))); ( P))
() : (), (void); (p ◁ₗ{beta} (P @ (latch))).
End spec.
Typeclasses Opaque latch_rec.
From refinedc.typing Require Import typing.
From refinedc.examples.latch Require Import generated_code.
From refinedc.examples.latch Require Import generated_code generated_spec.
Set Default Proof Using "Type".
Definition latchN : namespace := nroot.@"lockN".
Section type.
Context `{!typeG Σ}.
Definition latch (P : iProp Σ) : type :=
struct struct_latch [atomic_bool bool_it ( P) True].
Global Program Instance movable_latch P : Movable (latch P) := ltac:(apply: movable_struct).
Lemma latch_simplify_hyp l β P T:
(l ◁ₗ{β} struct struct_latch [atomic_bool bool_it ( P) True] - T) -
simplify_hyp (l ◁ₗ{β} latch P) T.
Proof. done. Qed.
Global Instance latch_simplify_hyp_inst l β P:
SimplifyHypPlace l β (latch P) (Some 100%N) :=
λ T, i2p (latch_simplify_hyp l β P T).
Lemma latch_simplify_goal l β P T:
T (l ◁ₗ{β} struct struct_latch [atomic_bool bool_it ( P) True]) -
simplify_goal (l ◁ₗ{β} latch P) T.
Proof. iIntros "HT". iExists _. iFrame. iIntros "$". Qed.
Global Instance latch_simplify_goal_inst l β P:
SimplifyGoalPlace l β (latch P) (Some 100%N) :=
λ T, i2p (latch_simplify_goal l β P T).
Lemma latch_subsume P1 P2 l T β:
P1 = P2 T -
subsume (l ◁ₗ{β} latch P1) (l ◁ₗ{β} latch P2) T.
Proof. iIntros "[-> $] $". Qed.
Global Instance latch_subsume_inst P1 P2 l β:
Subsume (l ◁ₗ{β} latch P1) (l ◁ₗ{β} latch P2) :=
λ T, i2p (latch_subsume P1 P2 l T β).
Definition LATCH_INIT := val_of_bool false.
Lemma latch_init l E P:
shrN E
l `has_layout_loc` struct_latch
l LATCH_INIT ={E}= l ◁ₗ{Shr} latch P.
l LATCH_INIT ={E}= l ◁ₗ{Shr} P @ latch.
Proof.
iIntros (? ?) "Hl".
iApply ty_share => //. iApply (ty_ref with "[] Hl") => //.
rewrite /ty_own_val/=. repeat iSplit => //. rewrite /ty_own_val/=/ty_own_val/=. by iExists false.
iApply ty_share => //. unshelve iApply (@ty_ref with "[] Hl") => //. apply _. done.
rewrite /ty_own_val/=. repeat iSplit => //. rewrite /ty_own_val/=/ty_own_val/=. iSplit => //. by iExists false.
Qed.
End type.
Typeclasses Opaque latch.
......@@ -383,9 +383,51 @@ Proof.
- rewrite take_length in Hin. lia.
- rewrite drop_length in Hin. lia.
Qed.
Lemma big_sepL_impl' {B} Φ (Ψ : _ B _) (l1 : list A) (l2 : list B) :
length l1 = length l2
([ list] kx l1, Φ k x) -
( k x1 x2, l1 !! k = Some x1 - l2 !! k = Some x2 - Φ k x1 - Ψ k x2) -
[ list] kx l2, Ψ k x.
Proof.
iIntros (Hlen) "Hl #Himpl".
iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen); destruct l2 => //=; simpl in *.
iDestruct "Hl" as "[Hx1 Hl]". iSplitL "Hx1". by iApply "Himpl".
iApply ("IH" $! (Φ S) (Ψ S) l2 _ with "[] Hl").
iIntros "!>" (k y1 y2 ?) "Hl2 /= ?".
by iApply ("Himpl" with "[] [Hl2]").
Unshelve. lia.
Qed.
End sep_list.
Lemma big_sepL2_impl' {A B C D} (Φ : _ _ _ PROP) (Ψ : _ _ _ _) (l1 : list A) (l2 : list B) (l1' : list C) (l2' : list D) `{!BiAffine PROP} :
length l1 = length l1' length l2 = length l2'
([ list] kx;y l1; l2, Φ k x y) -
( k x1 x2 y1 y2, l1 !! k = Some x1 - l2 !! k = Some x2 - l1' !! k = Some y1 - l2' !! k = Some y2 - Φ k x1 x2 - Ψ k y1 y2) -
[ list] kx;y l1';l2', Ψ k x y.
Proof.
iIntros (Hlen1 Hlen2) "Hl #Himpl".
rewrite !big_sepL2_alt. iDestruct "Hl" as (Hl1) "Hl".
iSplit. { iPureIntro. congruence. }
iApply (big_sepL_impl' with "Hl"). { rewrite !zip_with_length. lia. }
iIntros "!>" (k [x1 x2] [y1 y2]).
rewrite !lookup_zip_with_Some.
iDestruct 1 as %(?&?&?&?).
iDestruct 1 as %(?&?&?&?). simplify_eq. destruct_and!.
by iApply "Himpl".
Qed.
End big_op.
Lemma vec_cast {A} n (v : vec A n) m:
n = m v' : vec A m, vec_to_list v = vec_to_list v'.
Proof.
elim: v m => [|??? IH] [|m']// ?.
- by eexists vnil.
- have [|??]:= IH m'. { lia. }
eexists (vcons _ _) => /=. by f_equal.
Qed.
Lemma filter_nil_inv {A} P `{! x, Decision (P x)} (l : list A):
filter P l = [] ( x : A, x l ¬ P x).
Proof.
......
From iris.program_logic Require Export adequacy weakestpre.
From iris.algebra Require Import csum excl auth cmra_big_op gmap.
From refinedc.typing Require Export type.
From refinedc.typing Require Import programs function uninit globals int.
From refinedc.typing Require Import programs function uninit globals int fixpoint.
From refinedc.lang Require Import heap.
From iris.program_logic Require Export language.
Set Default Proof Using "Type".
......@@ -96,3 +96,29 @@ Proof.
rewrite /fn_lists_to_fns /= big_sepM_insert //.
apply not_elem_of_list_to_map_1. rewrite fst_zip => //; lia.
Qed.
(** * Tactics for solving conditions in an adequacy proof *)
Ltac adequacy_intro_parameter :=
repeat lazymatch goal with
| |- _ : (), _ => case
| |- _ : (_ * _), _ => case
| |- _ : _, _ => move => ?
end.
Ltac adequacy_unfold_equiv :=
lazymatch goal with
| |- Build_mtype _ _ _ _ Build_mtype _ _ _ _ => constructor => /=; [| |move => ?]
| |- fixp _ _ fixp _ _ => apply: fixp_proper; [|move => ??]
| |- ty_own_val _ _ ty_own_val _ _ => unfold ty_own_val => /=
| |- _ =@{struct_layout} _ => apply: struct_layout_eq
end.
Ltac adequacy_solve_equiv unfold_tac :=
first [ eassumption | fast_reflexivity | unfold_type_equiv | adequacy_unfold_equiv | f_contractive | f_equiv' | reflexivity | progress unfold_tac ].
Ltac adequacy_solve_typed_function lemma unfold_tac :=
iApply typed_function_equiv; [
done |
| iApply lemma => //; iExists _; repeat iSplit => //];
adequacy_intro_parameter => /=; eexists eq_refl => /=; split_and!; [..|adequacy_intro_parameter => /=; split_and!]; repeat adequacy_solve_equiv unfold_tac.
......@@ -21,7 +21,20 @@ Section fixpoint.
Lemma fixp_unfold n:
fixp n T (λ n, fixp n) n.
Proof. rewrite /fixp. rewrite ->fixpoint_unfold. rewrite /apply_dfun{1}/type_fixpoint. f_equiv. Qed.
End fixpoint.
Section fixpoint.
Context `{!typeG Σ}.
Lemma fixp_proper {A} x1 x2 (T1 T2 : (A -d> typeO) (A -d> typeO)) `{!Contractive T1} `{!Contractive T2}:
x1 = x2 ( f x, T1 f x T2 f x)
fixp T1 x1 fixp T2 x2.
Proof.
move => ? HT. rewrite /fixp.
apply apply_dfun_proper => //.
apply fixpoint_proper => ?.
rewrite /type_fixpoint.
apply: HT.
Qed.
End fixpoint.
(*** Tests *)
......
......@@ -27,6 +27,47 @@ Section function.
Global Instance typed_function_persistent fn fp : Persistent (typed_function fn fp) := _.
Import EqNotations.
Lemma typed_function_equiv fn1 fn2 (fp1 fp2 : A _) :
fn1 = fn2
(* TODO: replace the following with an equivalenve relation for fn_params? *)
( x, Heq : (fp1 x).(fp_rtype) = (fp2 x).(fp_rtype),
(fp1 x).(fp_atys) (fp2 x).(fp_atys)
(fp1 x).(fp_Pa) (fp2 x).(fp_Pa)
( y, ((fp1 x).(fp_fr) y).(fr_rty) ((fp2 x).(fp_fr) (rew [λ x : Type, x] Heq in y)).(fr_rty)
((fp1 x).(fp_fr) y).(fr_R) ((fp2 x).(fp_fr) (rew [λ x : Type, x] Heq in y)).(fr_R)))
typed_function fn1 fp1 - typed_function fn2 fp2.
Proof.
iIntros (-> Hfn) "HT".
rewrite /typed_function.
iIntros (x). iDestruct ("HT" $! x) as ([Hlen Hall]%Forall2_same_length_lookup) "#HT".
have [Heq [Hatys [HPa Hret]]] := Hfn x.
iSplit. {
iPureIntro. apply: Forall2_same_length_lookup_2. { rewrite -Hlen. symmetry. by apply: length_proper. }
move => i ty [??] Haty Harg.
move: Hatys => /list_equiv_lookup Hatys.
have := Hatys i. rewrite Haty => /(equiv_Some_inv_r' _ _)[? [? [?->?]]].
by apply: (Hall _ _ (_, _)).
}
iIntros "!>" (lsa lsv) "[Hv Ha] %". rewrite -HPa.
have [|lsa' Hlsa]:= vec_cast _ lsa (length (fp_atys (fp1 x))). { by rewrite Hatys. }
iApply (wps_wand with "[Hv Ha]").
- iSpecialize ("HT" $! lsa' lsv with "[Hv Ha]"); rewrite Hlsa. {
iFrame. iApply (big_sepL2_impl' with "Hv") => //. by rewrite Hatys.
move: Hatys => /list_equiv_lookup Hatys.
iIntros "!>" (k ????? Haty2 ? Haty1) "?".
have := Hatys k. rewrite Haty1 Haty2=> /(equiv_Some_inv_r' _ _)[? [? [Heql ??]]].
rewrite Heql. by simplify_eq.
}
iApply "HT". by rewrite -Hlsa.
- rewrite /typed_stmt_post_cond. iIntros (v).
iDestruct 1 as (y) "[?[??]]".
have [[?? ->] ->]:= Hret y.
iExists (rew [λ x : Type, x] Heq in y).
rewrite Hlsa. iFrame.
Qed.
Program Definition function_ptr (fp : A fn_params) : rtype := {|
rty_type := loc;
rty f := {|
......
......@@ -357,12 +357,12 @@ Section proper.
T (l ◁ₗ{β} ty2) - simplify_goal (l◁ₗ{β} ty1) T.
Proof. iIntros (Heq) "HT". iExists _. iFrame. rewrite Heq. by iIntros "?". Qed.
Lemma simplify_hyp_val_eq v ty1 ty2 (Heq : ty1 ty2) {Hm: Movable ty1} `{!Movable ty2} T:
Lemma simplify_hyp_val_eq v ty1 ty2 (Heq : ty1 @{type} ty2) {Hm: Movable ty1} `{!Movable ty2} T:
Hm = movable_eq ty1 ty2 Heq
(v ◁ᵥ ty2 - T) - simplify_hyp (v ◁ᵥ ty1) T.
Proof. by move => ->. Qed.
Lemma simplify_goal_val_eq v ty1 ty2 (Heq : ty1 ty2) {Hm: Movable ty1} `{!Movable ty2} T:
Lemma simplify_goal_val_eq v ty1 ty2 (Heq : ty1 @{type} ty2) {Hm: Movable ty1} `{!Movable ty2} T:
Hm = movable_eq ty1 ty2 Heq
T (v ◁ᵥ ty2) - simplify_goal (v ◁ᵥ ty1) T.
Proof. iIntros (->) "HT". iExists _. iFrame. by iIntros "?". Qed.
......
......@@ -482,6 +482,10 @@ Section ofe.
Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
Global Instance ty_own_proper : Proper (() ==> eq ==> eq ==> ()) ty_own.
Proof. intros ?? EQ ??-> ??->. apply EQ. Qed.
Lemma ty_own_entails `{!typeG Σ} ty1 ty2 β l:
ty1 @{type} ty2
ty_own ty1 β l - ty_own ty2 β l.
Proof. by move => [->]. Qed.
Global Instance type_cofe : Cofe typeO.
Proof.
......@@ -543,6 +547,28 @@ Section ofe.
(* Proper (dist n ==> eq ==> dist n) with_refinement. *)
(* Proof. intros ?? EQ ??-> ??->. apply EQ. Qed. *)
Inductive mtype_equiv' (ty1 ty2 : mtype) : Prop :=
MType_equiv :
ty1.(mt_type) ty2.(mt_type)
ty1.(ty_layout) = ty2.(ty_layout)
( v, ty1.(ty_own_val) v ty2.(ty_own_val) v)
mtype_equiv' ty1 ty2.
Global Instance mtype_equiv : Equiv mtype := mtype_equiv'.
Global Instance type_equivalence : Equivalence (@{type}).
Proof.
constructor.
- done.
- move => ?? [Heq]. constructor => ??. by symmetry.
- move => ??? [Heq1] [Heq2]. constructor => ??. etrans; [apply: Heq1|]. done.
Qed.
Global Instance mtype_equivalence : Equivalence (@{mtype}).
Proof.
constructor => //.
- move => ?? [? ? ?]. by constructor; intros; symmetry.
- move => ??? [?? Hv1] [???]. by constructor; etrans; try eassumption; try apply: Hv1.
Qed.
Program Definition movable_eq ty1 ty2 `{!Movable ty2} (_ : ty1 @{type} ty2): Movable ty1 := {|
ty_layout := ty2.(ty_layout);
(* This must be tc_opaque, otherwise Coq likes to unfold ty1 to ty2 via unification. *)
......
......@@ -3,7 +3,7 @@ From refinedc.examples.spinlock Require Import
generated_code spinlock_def spinlock_proof
generated_proof_sl_lock generated_proof_sl_unlock.
From refinedc.examples.latch Require Import
generated_code latch_def generated_proof_latch_release
generated_code generated_spec latch_def generated_proof_latch_release
generated_proof_latch_wait.
From refinedc.tutorial.t03_list Require Import
generated_code generated_spec generated_proof_test generated_proof_reverse
......@@ -72,9 +72,14 @@ Section adequate.
Definition global_types `{!typeG Σ} `{!lockG Σ} : gmap string global_type :=
<["allocator_state" := GT unit (λ '(), t04_alloc.generated_spec.alloc_state)]> $
(* We need to use initialized_raw to avoid a cyclic definition of globalG *)
<["initialized" := GT unit (λ '(), latch (initialized_raw "allocator_state" () (Some loc_allocator_state) (Some (GT unit (λ '(), t04_alloc.generated_spec.alloc_state)))))]> $
<["initialized" := GT unit (λ '(), (initialized_raw "allocator_state" () (Some loc_allocator_state) (Some (GT unit (λ '(), t04_alloc.generated_spec.alloc_state)))) @ latch )%I]> $
.
Ltac unfold_defs :=
unfold latch.generated_spec.latch_rec, latch_rec.
Lemma tutorial_adequate n κs t2 σ2 σ:
loc_allocator_data `has_layout_loc` void_ptr
loc_allocator_state `has_layout_loc` struct_alloc_state
......@@ -122,33 +127,37 @@ Section adequate.
simpl.
iLöb as "IH". iDestruct "IH" as "(?&?&?&?&?&?&?&?&?&?&?&?&?&?&?&?&?)".
repeat iSplit.
- iApply type_main2 => //; iExists _; repeat iSplit => //.
- iApply type_main => //; iExists _; repeat iSplit => //.
- iApply type_init_alloc => //; iExists _; repeat iSplit => //.
- iApply type_free => //; iExists _; repeat iSplit => //.
- iApply type_alloc => //; iExists _; repeat iSplit => //.
- iApply type_test => //; iExists _; repeat iSplit => //.
- iApply type_reverse => //; iExists _; repeat iSplit => //.
- iApply type_member => //; iExists _; repeat iSplit => //.
- iApply type_pop => //; iExists _; repeat iSplit => //.
- iApply type_push => //; iExists _; repeat iSplit => //.
- iApply type_is_empty => //; iExists _; repeat iSplit => //.
- iApply type_init => //; iExists _; repeat iSplit => //.
- iApply type_latch_release => //; iExists _; repeat iSplit => //.
- iApply type_latch_wait => //; iExists _; repeat iSplit => //.
- iApply type_sl_unlock => //; iExists _; repeat iSplit => //.
- iApply type_sl_lock => //; iExists _; repeat iSplit => //.
- iApply type_sl_init => //; iExists _; repeat iSplit => //.
- adequacy_solve_typed_function type_main2 unfold_defs.
- adequacy_solve_typed_function type_main unfold_defs.
- adequacy_solve_typed_function type_init_alloc unfold_defs.
- adequacy_solve_typed_function type_free unfold_defs.
- adequacy_solve_typed_function type_alloc unfold_defs.
- adequacy_solve_typed_function type_test unfold_defs.
- adequacy_solve_typed_function type_reverse unfold_defs.
- adequacy_solve_typed_function type_member unfold_defs.
- adequacy_solve_typed_function type_pop unfold_defs.
- adequacy_solve_typed_function type_push unfold_defs.
- adequacy_solve_typed_function type_is_empty unfold_defs.
- adequacy_solve_typed_function type_init unfold_defs.
- adequacy_solve_typed_function type_latch_release unfold_defs.
- adequacy_solve_typed_function type_latch_wait unfold_defs.
- adequacy_solve_typed_function type_sl_unlock unfold_defs.
- adequacy_solve_typed_function type_sl_lock unfold_defs.
- adequacy_solve_typed_function type_sl_init unfold_defs.
}
iMod (latch_init with "Hinit") as "#Hinit" => //.
iModIntro. iSplitL => //. 2: iSplitL => //.
all: iExists _; iSplitR; [iExists _; repeat iSplit => // |].
- iSplitR. 2: iSplitL "Hstate".
+ iApply initialized_intro => //=. iExists eq_refl => /=. iApply "Hinit".
+ iApply initialized_intro => //=. iExists eq_refl => /=.
iApply (ty_own_entails with "Hinit").
repeat adequacy_solve_equiv unfold_defs.
+ iExists _; iSplit => //; iExists _; iEval (simpl).
iFrame "Hstate" => //.
+ iExists _; iSplit => //; iExists _; iEval (simpl). iFrame "Hdata" => //.
- iApply initialized_intro => //=. iExists eq_refl => /=. iApply "Hinit".
- iApply initialized_intro => //=. iExists eq_refl => /=.
iApply (ty_own_entails with "Hinit").
repeat adequacy_solve_equiv unfold_defs.
Qed.
End adequate.
......
......@@ -2,4 +2,4 @@
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.tutorial.t05_main)
(theories refinedc.examples.latch refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
(theories refinedc.examples.spinlock refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
From refinedc.typing Require Import typing.
From refinedc.tutorial.t05_main Require Import generated_code.
From refinedc.tutorial.t05_main Require Import generated_spec.
From refinedc.examples.latch Require Import latch_def.
From refinedc.examples.spinlock Require Import spinlock_def.
Set Default Proof Using "Type".
......@@ -14,7 +13,7 @@ Section proof_main.
Lemma type_main (global_allocator_data global_initialized global_free global_init_alloc global_latch_release global_test : loc) :
global_locs !! "allocator_data" = Some global_allocator_data
global_locs !! "initialized" = Some global_initialized
global_initialized_types !! "initialized" = Some (GT () (λ '(), (latch (alloc_initialized)) : type)%I)
global_initialized_types !! "initialized" = Some (GT () (λ '(), ((alloc_initialized) @ (latch)) : type)%I)
global_free ◁ᵥ global_free @ function_ptr type_of_free -
global_init_alloc ◁ᵥ global_init_alloc @ function_ptr type_of_init_alloc -
global_latch_release ◁ᵥ global_latch_release @ function_ptr type_of_latch_release -
......
From refinedc.typing Require Import typing.
From refinedc.tutorial.t05_main Require Import generated_code.
From refinedc.tutorial.t05_main Require Import generated_spec.
From refinedc.examples.latch Require Import latch_def.
From refinedc.examples.spinlock Require Import spinlock_def.