Commit 2fbd018d authored by Michael Sammler's avatar Michael Sammler
Browse files

Remove Movable typeclass

parent 762260eb
Pipeline #58399 passed with stage
in 20 minutes and 41 seconds
......@@ -14,13 +14,13 @@ Section type.
Proof.
iIntros (? ?) "Hl". iApply ty_share => //.
unshelve iApply (@ty_ref with "[] Hl").
{ apply _. }
{ apply: (UntypedOp struct_latch). }
{ apply: MCNone. }
{ solve_goal. }
{ done. }
rewrite /ty_own_val/=. repeat iSplit => //.
rewrite /ty_own_val /= /ty_own_val /=. iSplit => //.
iExists false. iSplit; last done. by iExists _.
unfold atomic_bool; simpl_type. iExists false.
unfold boolean; simpl_type. iSplit => //.
by iExists _.
Qed.
End type.
......@@ -8,8 +8,6 @@ Section type.
Definition spinlock (γ : lock_id) : type :=
struct struct_spinlock [atomic_bool u8 True (lock_token γ [])].
Global Program Instance movable_spinlock γ : Movable (spinlock γ) := ltac:(apply: movable_struct).
Global Instance alloc_alive_spinlock γ β : AllocAlive (spinlock γ) β True.
Proof. apply: _. Qed.
......
......@@ -10,13 +10,14 @@ Section type.
n1 n2, subsume (v1 ◁ᵥ ty1) (v1 ◁ᵥ n1 @ int it1) (
subsume (v2 ◁ᵥ ty2) (v2 ◁ᵥ n2 @ int it2) (
(n1 it1 - n2 it2 - it1 = it2 it_signed it1 = false (
v, T v (t2mt (((n1 + n2) `mod` int_modulus it1) @ int it1)))))))) -
v, T v (((n1 + n2) `mod` int_modulus it1) @ int it1))))))) -
typed_macro_expr (WrappingAdd it1 it2) [e1 ; e2] T.
Proof.
iIntros "HT". rewrite /typed_macro_expr/WrappingAdd. iApply type_bin_op.
iIntros (Φ) "HΦ". iApply "HT". iIntros (v1 ty1) "Hty1 HT". iApply ("HΦ" with "Hty1"). clear.
iIntros (Φ) "HΦ". iApply "HT". iIntros (v2 ty2) "Hty2 HT". iApply ("HΦ" with "Hty2"). clear.
iIntros "Hty1 Hty2". iDestruct "HT" as (n1 n2) "HT".
unfold int; simpl_type.
iDestruct ("HT" with "Hty1") as (Hv1) "HT".
iDestruct ("HT" with "Hty2") as (Hv2) "HT".
iIntros (Φ) "HΦ".
......@@ -31,7 +32,7 @@ Section type.
+ move => ->. apply: ArithOpII => //.
by destruct it1 as [? []]; simplify_eq/=.
}
iIntros "!>". iApply "HΦ"; last done. iPureIntro.
iIntros "!>". iApply "HΦ"; last done. simpl_type. iPureIntro.
by eapply val_to_of_Z.
Qed.
......
......@@ -148,3 +148,17 @@ typedef void (*test_fn)(void);
test_fn test_fn_params(test_fn f) {
return f;
}
struct [[rc::parameters("z: Z", "n : Z")]] [[rc::refined_by("x: unit")]] test2 {
[[rc::field("z @ int<i32>")]]
int a;
[[rc::field("&own<test2<n, z>>")]]
struct test2 * next;
};
[[rc::parameters("z : Z", "n : Z")]]
[[rc::args("test2<z, n>")]]
[[rc::returns("z @ int<i32>")]]
int test_struct2(struct test2 s) {
return s.a;
}
......@@ -888,11 +888,13 @@ let pp_spec : Coq_path.t -> import list -> inlined_code ->
opaque := !opaque @ [id ^ "_rec"];
pp "@;Global Instance %s_rec_ne : Contractive %s_rec." id id;
pp "@;Proof. solve_type_proper. Qed.\n@;";
pp "@;Proof. solve_type_proper. Qed.";
pp "@;Global Instance %s_rec_proper : Proper ((≡) ==> (≡)) %s_rec." id id;
pp "@;Proof. apply contractive_proper, _. Qed.\n@;";
pp "@[<v 2>Definition %s %a: rtype := {|@;" id pp_params params;
pp "rty_type := %a;@;" pp_prod ref_types;
pp "rty r__ := fixp %s %a@]@;|}.\n" (id ^ "_rec")
pp "rty r__ := %s_rec (fixp %s) %a@]@;|}.\n" id (id ^ "_rec")
(pp_as_tuple pp_str) ("r__" :: par_names);
(* Generation of the unfolding lemma. *)
......@@ -906,35 +908,24 @@ let pp_spec : Coq_path.t -> import list -> inlined_code ->
let guard = Guard_in_lem(id) in
pp_struct_def_np ast.structs guard annot fields ff struct_id;
pp "@]@;)%%I.@]@;";
pp "Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.\n";
(* Movable instance. *)
let pp_movable_instance () =
pp "\n@;Global Program Instance %s_rmovable %a: RMovable %a :=@;"
id pp_params params (pp_id_args true id) par_names;
pp " {| rmovable patt__ := movable_eq _ _ (%s_unfold" id;
List.iter (fun n -> pp " %s" n) par_names;
pp " patt__) |}.\n";
in
if not annot.st_immovable then pp_movable_instance ();
pp "Proof. apply: (fixp_unfold' %s_rec). Qed.\n" id;
(* Generation of the global instances. *)
let pp_instance_place inst_name type_name =
pp "@;Global Instance %s_%s_inst_generated l_ β_ %apatt__:@;"
id inst_name pp_params params;
pp " %s l_ β_ (patt__ @@ %a)%%I (Some 100%%N) :=@;"
type_name (pp_id_args false id) par_names;
pp " %s l_ β_ (patt__ @@ %a)%%I (Some %i%%N) :=@;"
type_name (pp_id_args false id) par_names annot.st_unfold_prio;
pp " λ T, i2p (%s_eq l_ β_ _ _ T (%s_unfold" inst_name id;
List.iter (fun _ -> pp " _") par_names; pp " _))."
in
let pp_instance_val inst_name type_name =
pp "@;Global Program Instance %s_%s_inst_generated v_ %apatt__:@;"
pp "@;Global Instance %s_%s_inst_generated v_ %apatt__:@;"
id inst_name pp_params params;
pp " %s v_ (patt__ @@ %a)%%I (Some 100%%N) :=@;"
type_name (pp_id_args false id) par_names;
pp " λ T, i2p (%s_eq v_ _ _ (%s_unfold" inst_name id;
List.iter (fun _ -> pp " _") par_names; pp " _) T _).";
pp "@;Next Obligation. done. Qed."
pp " %s v_ (patt__ @@ %a)%%I (Some %i%%N) :=@;"
type_name (pp_id_args false id) par_names annot.st_unfold_prio;
pp " λ T, i2p (%s_eq v_ _ _ T (%s_unfold" inst_name id;
List.iter (fun _ -> pp " _") par_names; pp " _)).";
in
pp_instance_place "simplify_hyp_place" "SimplifyHypPlace";
pp_instance_place "simplify_goal_place" "SimplifyGoalPlace";
......
......@@ -252,6 +252,9 @@ let parser annot_constr : constr Earley.grammar =
let parser annot_let : (ident * coq_expr option * coq_expr) Earley.grammar =
| id:ident ty:{":" coq_expr}? "=" def:coq_expr
let parser annot_unfold_prio : int Earley.grammar =
| i:integer
(** {4 Annotations on tagged unions} *)
type tag_spec = string * (string * coq_expr) list
......@@ -347,6 +350,7 @@ type annot =
| Annot_block
| Annot_full_block
| Annot_inlined
| Annot_unfold_prio of int
let annot_lemmas : string list -> string list =
List.map (Printf.sprintf "all: try by apply: %s; solve_goal.")
......@@ -460,6 +464,7 @@ let parse_attr : rc_attr -> annot = fun attr ->
| "block" -> no_args Annot_block
| "full_block" -> no_args Annot_full_block
| "inlined" -> no_args Annot_inlined
| "unfold_prio" -> single_arg annot_unfold_prio (fun i -> Annot_unfold_prio(i))
| _ -> error "undefined"
(** {3 High level parsing of attributes} *)
......@@ -590,24 +595,26 @@ let expr_annot : rc_attr list -> expr_annot = fun attrs ->
| _ -> error "is invalid (wrong kind)"
type basic_struct_annot =
{ st_parameters : (ident * coq_expr) list
; st_refined_by : (ident * coq_expr) list
; st_exists : (ident * coq_expr) list
; st_lets : (ident * coq_expr option * coq_expr) list
; st_constrs : constr list
; st_size : coq_expr option
; st_ptr_type : (ident * type_expr) option
; st_immovable : bool }
{ st_parameters : (ident * coq_expr) list
; st_refined_by : (ident * coq_expr) list
; st_exists : (ident * coq_expr) list
; st_lets : (ident * coq_expr option * coq_expr) list
; st_constrs : constr list
; st_size : coq_expr option
; st_ptr_type : (ident * type_expr) option
; st_immovable : bool
; st_unfold_prio : int }
let default_basic_struct_annot : basic_struct_annot =
{ st_parameters = []
; st_refined_by = []
; st_exists = []
; st_lets = []
; st_constrs = []
; st_size = None
; st_ptr_type = None
; st_immovable = false }
{ st_parameters = []
; st_refined_by = []
; st_exists = []
; st_lets = []
; st_constrs = []
; st_size = None
; st_ptr_type = None
; st_immovable = false
; st_unfold_prio = 100 }
type struct_annot =
| SA_union
......@@ -624,6 +631,7 @@ let struct_annot : rc_attr list -> struct_annot = fun attrs ->
let ptr = ref None in
let immovable = ref false in
let tagged_union = ref None in
let unfold_prio = ref None in
let handle_attr ({rc_attr_id = id; _} as attr) =
let error msg =
......@@ -648,6 +656,12 @@ let struct_annot : rc_attr list -> struct_annot = fun attrs ->
| (Annot_immovable , None ) ->
if !immovable then error "already specified";
immovable := true
| (Annot_unfold_prio(i) , None ) ->
begin
match !unfold_prio with
| Some _ -> error "already specified"
| None -> unfold_prio := Some(i)
end
| (Annot_parameters(_) , _ )
| (Annot_refined_by(_) , _ )
| (Annot_exist(_) , _ )
......@@ -665,14 +679,15 @@ let struct_annot : rc_attr list -> struct_annot = fun attrs ->
| Some(e) -> SA_tagged_u(e)
| None ->
let basic_annot =
{ st_parameters = !parameters
; st_refined_by = !refined_by
; st_exists = !exists
; st_lets = !lets
; st_constrs = !constrs
; st_size = !size
; st_ptr_type = !ptr
; st_immovable = !immovable }
{ st_parameters = !parameters
; st_refined_by = !refined_by
; st_exists = !exists
; st_lets = !lets
; st_constrs = !constrs
; st_size = !size
; st_ptr_type = !ptr
; st_immovable = !immovable
; st_unfold_prio = Option.get 100 !unfold_prio }
in
SA_basic(basic_annot)
......
......@@ -8,6 +8,7 @@ Section proofs.
Context `{!typeG Σ} `{!globalG Σ} `{!lockG Σ} `{!spinlockG Σ}.
Typeclasses Transparent hyp_spinlock_t spinlock_token.
Typeclasses Transparent frac_ptr_type.
(* Typing proof for [hyp_spin_lock_init]. *)
Lemma type_hyp_spin_lock_init :
......@@ -75,7 +76,7 @@ Section proofs.
iExists _, _, True%I. iFrame. iSplit; [done|].
unshelve iApply type_read_copy. { apply _. } simpl.
iSplit; [done|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v) "_ Hl Hv !>".
iExists tytrue, (t2mt (next @ int u16)). iSplit; [done|]. iSplit; [done|]. iModIntro.
iExists tytrue, (next @ int u16)%I. iSplit; [done|]. iSplit; [done|]. iModIntro.
iSplitL "Howner Hrest Hl Hv". {
iNext. rewrite /hyp_spinlock_t_invariant. iExists owner, next.
iFrame "Hrest". iSplit; first done. iFrame.
......@@ -102,7 +103,7 @@ Section proofs.
iExists _, _, True%I. iFrame.
unshelve iApply type_read_copy. { apply _. } simpl.
iSplit; [done|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v') "_ Hl Hv !>".
iExists tytrue, (t2mt (next @ int u16)). iSplit; [done|]. iSplit; [done|]. iModIntro.
iExists tytrue, (next @ int u16)%I. iSplit; [done|]. iSplit; [done|]. iModIntro.
iSplitL "Howner Hrest Hl Hv". {
iNext. rewrite /hyp_spinlock_t_invariant. iExists owner, next.
iFrame "Hrest". iSplit; first done. iFrame.
......@@ -128,7 +129,7 @@ Section proofs.
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_suc_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (true @ builtin_boolean))%I) => //.
iNext. iIntros "??". iApply ("HΦ" $! _ (true @ builtin_boolean)%I) => //.
{ iExists _. done. }
repeat liRStep; liShow.
rewrite /hyp_spinlock_t_invariant.
......@@ -151,7 +152,7 @@ Section proofs.
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_fail_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (false @ builtin_boolean))%I) => //.
iNext. iIntros "??". iApply ("HΦ" $! _ (false @ builtin_boolean)%I) => //.
{ by iExists _. }
repeat liRStep; liShow.
rewrite /hyp_spinlock_t_invariant.
......@@ -171,7 +172,7 @@ Section proofs.
iExists _, _, True%I. iFrame. iSplit; [done|].
unshelve iApply type_read_copy. { apply _. } simpl.
iSplit; [done|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v') "_ Hl Hv !>".
iExists tytrue, (t2mt (next @ int u16)). iSplit; [done|]. iSplit; [done|]. iModIntro.
iExists tytrue, (next @ int u16)%I. iSplit; [done|]. iSplit; [done|]. iModIntro.
iSplitL "Howner Hrest Hl Hv". {
iNext. rewrite /hyp_spinlock_t_invariant. iExists owner, next.
iFrame "Hrest". iSplit; first done. iFrame.
......@@ -189,7 +190,7 @@ Section proofs.
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_suc_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (true @ builtin_boolean))%I) => //.
iNext. iIntros "??". iApply ("HΦ" $! _ (true @ builtin_boolean)%I) => //.
{ by iExists _. }
iRename select (p at{struct_hyp_spinlock} "next" ◁ₗ _)%I into "Hnext".
iDestruct "Hrest" as "(Hfrag&Hr1&Hr2&Hcases)".
......@@ -208,7 +209,7 @@ Section proofs.
iDestruct select (local_ticket ◁ᵥ _)%I as "[_ Hticket]".
iDestruct select (p at{_} _ ◁ᵥ _)%I as "[_ ->]".
iApply (wp_cas_fail_int with "Hnext Hticket [$]"). { cbv. lia. } done.
iNext. iIntros "??". iApply ("HΦ" $! _ (t2mt (false @ builtin_boolean))%I) => //.
iNext. iIntros "??". iApply ("HΦ" $! _ (false @ builtin_boolean)%I) => //.
{ by iExists _. }
iRename select (p at{struct_hyp_spinlock} _ ◁ₗ _)%I into "Hnext".
iMod ("Hclose_inv" with "[Howner Hnext Hrest]") as "_".
......@@ -246,7 +247,7 @@ Section proofs.
iExists _, _, True%I. iFrame. iSplit; [done|].
unshelve iApply type_read_copy. { apply _. } simpl.
iSplit; [done|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v') "_ Hl Hv !>".
iExists tytrue, (t2mt (owner @ int u16)). iSplit; [done|]. iSplit; [done|]. iModIntro.
iExists tytrue, (owner @ int u16)%I. iSplit; [done|]. iSplit; [done|]. iModIntro.
destruct (decide (i owner)).
* iSplitL "Hnext Hrest Hl Hv". {
iNext. rewrite /hyp_spinlock_t_invariant. iExists owner, next.
......@@ -262,7 +263,7 @@ Section proofs.
{ rewrite /ty_own_val /=. by iDestruct "Hv" as %Hv%val_to_Z_in_range. }
iAssert (owner < next)%I as %?.
{ destruct (decide (owner < next)); first done. iExFalso.
iDestruct (ty_size_eq (IntOp _) MCNone with "Hv") as %?; [done|].
iDestruct (ty_size_eq _ (IntOp _) MCNone with "Hv") as %?; [done|].
iDestruct (ticket_not_NO_TICKET with "Hticket") as %Howner.
iApply (ticket_already_in_range with "[] Hr2 Hticket").
iPureIntro. clear Q. apply elem_of_seqZ. lia. }
......@@ -328,7 +329,7 @@ Section proofs.
iExists _, _, True%I. iFrame. iSplit; [done|].
unshelve iApply type_read_copy. { apply _. } simpl.
iSplit; [done|]. iSplit; [iPureIntro; solve_ndisj|]. iIntros (v') "_ Hl Hv !>".
iExists tytrue, (t2mt (owner @ int u16)). iSplit; [done|]. iSplit; [done|]. iModIntro.
iExists tytrue, (owner @ int u16)%I. iSplit; [done|]. iSplit; [done|]. iModIntro.
iSplitL "Hnext Hrest Hl Hv H◯". {
iNext. rewrite /hyp_spinlock_t_invariant. iExists owner, next.
iFrame "Hrest". iSplit; first done. iFrame.
......@@ -350,12 +351,13 @@ Section proofs.
iMod (owner_auth_update _ _ _ _ 0%nat with "H● H◯") as "[H● H◯]".
(* Learn that [next'] actually is [max_int u16]. *)
iAssert next' = max_int u16%I as %->.
{ iDestruct (ty_deref (IntOp _) MCNone with "Hnext") as (w) "[_ H]"; [done|]. iDestruct "H" as %Hnext.
{ iDestruct (ty_deref _ (IntOp _) MCNone with "Hnext") as (w) "[_ H]"; [done|].
unfold int; simpl_type. iDestruct "H" as %Hnext.
iPureIntro. apply val_to_Z_in_range in Hnext as [??]. lia. }
(* We perform the write and close the invariant. *)
iApply typed_write_end_mono_strong; [done|].
iIntros "Hv2 _ !>". iExists (t2mt _), _, _, True%I. iFrame. iSplit; [done|].
unshelve iApply type_write_own_copy. { apply _. } iSplit; [done|]. iSplit; [done|].
iIntros "Hv2 _ !>". iExists _, _, _, True%I. iFrame. iSplit; [done|].
iApply type_write_own_copy. iSplit; [done|].
iIntros "Hv _ Hl !>". iExists tytrue. iSplit; [done|]. iModIntro.
iSplitL "Htok H● H◯ Hnext Hl Hv". {
iNext. iExists 0, (LAST_TICKET + 1). iFrame.
......@@ -375,7 +377,8 @@ Section proofs.
(* We can get [owner' = 0] since we have all the tickets. *)
iAssert owner' = 0%I as %->.
{ destruct (decide (owner' = 0)) => //. iExFalso.
iDestruct (ty_deref (IntOp _) MCNone with "Howner") as (?) "[? Hv]"; [done|].
iDestruct (ty_deref _ (IntOp _) MCNone with "Howner") as (?) "[? Hv]"; [done|].
unfold int; simpl_type.
iDestruct "Hv" as %Howner%val_to_Z_in_range.
destruct Howner as [Howner ?].
iDestruct (overlaping_ticket_ranges with "[] Htk Htr1") as "$".
......@@ -394,8 +397,8 @@ Section proofs.
iExists next''. iPureIntro. split; apply elem_of_seqZ; lia. }
(* We perform the write and close the invariant. *)
iApply typed_write_end_mono_strong; [done|].
iIntros "Hv2 _ !>". iExists (t2mt _), _, _, True%I. iFrame. iSplit; [done|].
unshelve iApply type_write_own_copy. { apply _. } iSplit; [done|]. iSplit; [done|].
iIntros "Hv2 _ !>". iExists _, _, _, True%I. iFrame. iSplit; [done|].
iApply type_write_own_copy. iSplit; [done|].
iIntros "Hv _ Hl !>". iExists tytrue. iSplit; [done|]. iModIntro.
iRename select (ticket ◁ₗ _)%I into "Hticket_var".
iSplitR "Hticket_var". { iNext. iExists 0, 0. by iFrame. }
......@@ -415,8 +418,8 @@ Section proofs.
(* The owner will be [owner + 1], update the witness. *)
iMod (owner_auth_update _ _ _ _ (owner + 1) with "H● H◯") as "[H● H◯]".
iApply typed_write_end_mono_strong; [done|].
iIntros "Hv2 _ !>". iExists (t2mt _), _, _, True%I. iFrame. iSplit; [done|].
unshelve iApply type_write_own_copy. { apply _. } iSplit; [done|]. iSplit; [done|].
iIntros "Hv2 _ !>". iExists _, _, _, True%I. iFrame. iSplit; [done|].
iApply type_write_own_copy. iSplit; [done|].
iIntros "Hv _ Hl !>". iExists tytrue. iSplit; [done|]. iModIntro.
iSplitL "Htok H● H◯ Hticket Hnext Hl Htk1 Htk2". {
iNext. iExists (owner + 1), next'. iFrame.
......
......@@ -79,7 +79,7 @@ Proof.
iIntros "!#" (? main ?); iDestruct 1 as (P) "[Hmain HP]".
iApply (type_call with "[-]"). 2: { by iIntros (??) "??". }
iApply type_val. iApply type_val_context.
iExists (t2mt (main @ function_ptr (main_type P))) => /=. iFrame => /=.
iExists (main @ function_ptr (main_type P))%I => /=. iFrame => /=.
iApply type_call_fnptr. iIntros "_". iExists () => /=. iFrame. by iIntros (v []) "Hv" => /=.
- iFrame. iIntros (?? _ _ ?) "_ _ _". iApply fupd_mask_intro_discard => //. iPureIntro. by eauto.
- by iFrame.
......@@ -111,7 +111,6 @@ Ltac adequacy_intro_parameter :=
Ltac adequacy_unfold_equiv :=
lazymatch goal with
| |- Build_mtype _ _ _ _ Build_mtype _ _ _ _ => constructor => /=; [|move => ??|move => ?]
| |- fixp _ _ fixp _ _ => apply: fixp_proper; [|move => ??]
| |- ty_own_val _ _ ty_own_val _ _ => unfold ty_own_val => /=
| |- _ =@{struct_layout} _ => apply: struct_layout_eq
......
......@@ -7,42 +7,25 @@ Section array.
Context `{typeG Σ}.
(*** arrays *)
Program Definition array (ly : layout) (tys : list type) : type := {|
ty_has_op_type ot mt := ot = UntypedOp (mk_array_layout ly (length tys)) mt = MCNone layout_wf ly Forall (λ ty, ty.(ty_has_op_type) (UntypedOp ly) MCNone) tys;
ty_own β l := (
l `has_layout_loc` ly
loc_in_bounds l (ly_size ly * length tys)%nat
[ list] i ty tys, (l offset{ly} i) ◁ₗ{β} ty
)%I
)%I;
ty_own_val v :=
(v `has_layout_val` (mk_array_layout ly (length tys))
[ list] v';tyreshape (replicate (length tys) (ly_size ly)) v;tys, (v' ◁ᵥ ty))%I;
|}.
Next Obligation.
iIntros (ly tys l E He) "($&$&Ha)". iApply big_sepL_fupd. iApply (big_sepL_impl with "Ha").
iIntros "!#" (???). by iApply ty_share.
Qed.
Global Instance array_ne n : Proper ((=) ==> (dist n) ==> (dist n)) array.
Proof.
move => ? sl -> tys1 tys2 Htys. constructor => β l; rewrite/ty_own/=.
f_equiv. f_equiv; first by rewrite ->Htys.
elim: Htys l => // ???????? /=. f_equiv. solve_proper.
by setoid_rewrite offset_loc_S.
Qed.
Global Instance array_proper : Proper ((=) ==> () ==> ()) array.
Proof. move => ??->. apply ne_proper, _. Qed.
Global Program Instance movable_array ly tys `{!MovableLst tys} : Movable (array ly tys) := {|
ty_has_op_type ot mt := ot = UntypedOp (mk_array_layout ly (length tys)) mt = MCNone layout_wf ly Forall (λ ty, (ty : mtype).(ty_has_op_type) (UntypedOp ly) MCNone) (movablelst_to_list tys);
ty_own_val v :=
(v `has_layout_val` (mk_array_layout ly (length tys))
[ list] v';tyreshape (replicate (length tys) (ly_size ly)) v;(movablelst_to_list tys), (v' ◁ᵥ (ty : mtype)))%I;
|}.
Next Obligation. by iIntros (ly tys ? ot mt l [-> ?]) "[% _]". Qed.
Next Obligation. by iIntros (ly tys ? ot mt v [-> ?]) "(?&_)". Qed.
Next Obligation. by iIntros (ly tys ot mt l [-> ?]) "[% _]". Qed.
Next Obligation. by iIntros (ly tys ot mt v [-> ?]) "(?&_)". Qed.
Next Obligation.
move => ly tys ? ot mt l [? [? [? ]]]. rewrite {2}(to_movablelst tys).
move Heq: (movablelst_to_list tys) => tys'.
have ->: (length tys = length tys') by rewrite -Heq movablelst_to_list_length.
clear dependent tys. rewrite /ty_own/=. iIntros (Hlys) "(_&#Hb&Htys)".
iInduction (tys') as [|ty tys] "IH" forall (l); csimpl.
move => ly tys ot mt l [? [? [? ]]]. iIntros (Hlys) "(_&#Hb&Htys)". subst.
iInduction (tys) as [|ty tys] "IH" forall (l Hlys); csimpl.
{ iExists []. iSplitR => //.
- iApply heap_mapsto_nil; first by iApply (loc_in_bounds_shorten with "Hb"); lia.
- iSplit => //. iPureIntro. rewrite /has_layout_val/ly_size/=. lia. }
......@@ -52,20 +35,16 @@ Section array.
iDestruct (ty_deref with "Hty") as (v') "[Hl Hty]"; [done|].
iDestruct (ty_size_eq with "Hty") as %Hszv; [done|].
setoid_rewrite offset_loc_S.
iDestruct ("IH" $! _ (l offset{ly} 1) with "[Hb2] Htys") as (vs') "(Hl' & Hsz & Htys)".
iDestruct ("IH" $! (l offset{ly} 1) with "[//] [Hb2] Htys") as (vs') "(Hl' & Hsz & Htys)".
{ by rewrite /offset_loc Z.mul_1_r. }
iDestruct "Hsz" as %Hsz. iExists (v' ++ vs').
rewrite /has_layout_val heap_mapsto_app Hszv offset_loc_1 take_app_alt // drop_app_alt // app_length Hszv Hsz.
iFrame. iPureIntro. rewrite /ly_size/= -/(ly_size _). lia.
Unshelve. done.
Qed.
Next Obligation.
move => ly tys ? ot mt l v [-> [? [? ]]]. rewrite {6}(to_movablelst tys).
move Heq: (movablelst_to_list tys) => tys'.
have ->: (length tys = length tys') by rewrite -Heq movablelst_to_list_length.
clear dependent tys. iIntros (Hlys Hl) "Hl". rewrite /ty_own/=.
move => ly tys ot mt l v [-> [? [? ]]]. iIntros (Hlys Hl) "Hl".
iDestruct 1 as (Hv) "Htys". iSplit => //.
iInduction (tys') as [|ty tys] "IH" forall (l v Hv Hl); csimpl in *.
iInduction (tys) as [|ty tys] "IH" forall (l v Hlys Hv Hl); csimpl in *.
{ rewrite mult_0_r right_id. by iApply heap_mapsto_loc_in_bounds_0. }
move: Hlys. intros [? ?]%Forall_cons. iDestruct "Htys" as "[Hty Htys]".
rewrite -{1}(take_drop (ly_size ly) v).
......@@ -80,7 +59,24 @@ Section array.
iApply loc_in_bounds_split_mul_S. rewrite take_length min_l; first by eauto.
rewrite Hv. repeat unfold ly_size => /=; lia.
Qed.
Next Obligation. iIntros (???????[?[-> ?]]) "?". done. Qed.
Next Obligation. iIntros (??????[?[-> ?]]) "?". done. Qed.
Global Instance array_ne n : Proper ((=) ==> (dist n) ==> (dist n)) array.
Proof.
move => ? sl -> tys1 tys2 Htys. constructor.
- move => /= ??. erewrite Forall2_length; [|done]. do 3 f_equiv => //.
elim: Htys => //???? Hty ? IH. rewrite !Forall_cons IH. f_equiv. apply Hty.
- move => β l; rewrite/ty_own/=.
f_equiv. f_equiv; first by rewrite ->Htys.
elim: Htys l => // ???????? /=. f_equiv. solve_proper.
by setoid_rewrite offset_loc_S.
- move => v; rewrite/ty_own_val/=.
f_equiv. f_equiv; first by rewrite ->Htys.
elim: Htys v => // ???? Hty Htys IH v /=. f_equiv. { solve_proper. }
apply: IH.
Qed.
Global Instance array_proper : Proper ((=) ==> () ==> ()) array.
Proof. move => ??->. apply ne_proper, _. Qed.
Global Instance array_loc_in_bounds ly β tys : LocInBounds (array ly tys) β (ly_size ly * length tys).
Proof. constructor. iIntros (?) "(?&$&?)". Qed.
......@@ -146,8 +142,11 @@ Section array.
l `has_layout_loc` ly
0 idx len
loc_in_bounds base (ly_size (mk_array_layout ly len))
)%I
)%I;
ty_has_op_type _ _ := False%type;
ty_own_val _ := True%I;
|}.
Solve Obligations with try done.
Next Obligation. iIntros (ly base idx len l E ?) "(%&%&$)". done. Qed.
Global Instance array_ptr_loc_in_bounds ly base idx β len : LocInBounds (array_ptr ly base idx len) β ((len - Z.to_nat idx) * ly_size ly).
......@@ -240,13 +239,14 @@ Section array.
SubsumePlace l β (array ly1 tys1) (array ly2 tys2) | 100 :=
λ T, i2p (subsume_array ly1 ly2 tys1 tys2 l β T).
Lemma type_place_array l β T ly1 it v (tyv : mtype) tys ly2 K:
Lemma type_place_array l β T ly1 it v tyv tys ly2 K:
( i, ly1 = ly2 subsume (v ◁ᵥ tyv) (v ◁ᵥ i @ int it) (0 i i < length tys
ty, tys !! Z.to_nat i = Some ty -
typed_place K (l offset{ly2} i) β ty (λ l2 β2 ty2 typ, T l2 β2 ty2 (λ t, array ly2 (<[Z.to_nat i := typ t]>tys))))) -
typed_place (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array ly2 tys) T.
Proof.
iDestruct 1 as (i ->) "HP". iIntros (Φ) "(%&#Hb&Hl) HΦ" => /=. iIntros "Hv".
unfold int; simpl_type.
iDestruct ("HP" with "Hv") as (Hv) "HP".
iDestruct "HP" as (? Hlen) "HP".
have [|ty ?]:= lookup_lt_is_Some_2 tys (Z.to_nat i). lia.
......@@ -259,21 +259,21 @@ Section array.
iMod ("Htyp" with "Hl'") as "[? $]".
iSplitR => //. iSplitR; first by rewrite insert_length. by iApply "Hc".
Qed.
Global Instance type_place_array_inst l β ly1 it v (tyv : mtype) tys ly2 K:
Global Instance type_place_array_inst l β ly1 it v tyv tys ly2 K:
TypedPlace (BinOpPCtx (PtrOffsetOp ly1) (IntOp it) v tyv :: K) l β (array ly2 tys):=