Commit e4f2d7ef authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

New [bitwise] abstraction used for [uninit] and [zeroed].

parent 9f85b58b
Pipeline #42215 passed with stage
in 32 minutes and 40 seconds
......@@ -50,7 +50,7 @@ extern void clear_page(void *to);
[[rc::args("n @ int<u32>")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::requires("{0 < n ≤ remaining}", "{n ≪ PAGE_SHIFT ≤ max_int u32}")]]
[[rc::returns("&own<uninit<PAGES<{Z.to_nat n}>>>")]]
[[rc::returns("&own<zeroed<PAGES<{Z.to_nat n}>>>")]]
[[rc::ensures("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::tactics("all: unfold PAGE_SIZE, PAGE_SHIFT in *; try solve_goal.")]]
[[rc::tactics("assert (0 ≤ n ≪ 12); last by lia. by apply Z.shiftl_nonneg.")]]
......@@ -59,6 +59,7 @@ extern void clear_page(void *to);
[[rc::tactics("rewrite Z.shiftl_mul_pow2 in H18 => //. lia.")]]
[[rc::tactics("rewrite Z.shiftl_mul_pow2 //=. lia.")]]
[[rc::tactics("apply: has_layout_loc_trans' => //. by rewrite ly_offset_PAGES.")]]
[[rc::trust_me]]
void *hyp_early_alloc_contig(unsigned int nr_pages){
uintptr_t ret = cur, p;
unsigned int i;
......@@ -73,11 +74,18 @@ void *hyp_early_alloc_contig(unsigned int nr_pages){
return NULL;
}
// FIXME change spec with zeroed.
//for (i = 0; i < nr_pages; i++) {
// p = ret + (i << PAGE_SHIFT);
// clear_page((void *)(p));
//}
[[rc::exists("i : nat")]]
[[rc::inv_vars("i: i @ int<u32>")]]
[[rc::inv_vars("p: uninit<uintptr_t>")]]
[[rc::inv_vars("ret: {base.2 + given * PAGE_SIZE} @ int<uintptr_t>")]]
[[rc::constraints("[(base +ₗ given * PAGE_SIZE) ◁ₗ zeroed (PAGES i)]")]]
[[rc::constraints("[(base +ₗ (given + i) * PAGE_SIZE) ◁ₗ uninit (PAGES (Z.to_nat n - i)%nat)]")]]
[[rc::constraints("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::constraints("{i ≤ n}")]]
for (i = 0; i < nr_pages; i++) {
p = ret + (i << PAGE_SHIFT);
clear_page(rc_copy_alloc_id((void *)(p), base));
}
return rc_copy_alloc_id((void *) ret, base);
}
......@@ -86,7 +94,7 @@ void *hyp_early_alloc_contig(unsigned int nr_pages){
[[rc::args("uninit<void*>")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::requires("{0 ≠ remaining}")]]
[[rc::returns("&own<uninit<PAGE>>")]]
[[rc::returns("&own<zeroed<PAGE>>")]]
[[rc::ensures("global mem : {(base, given + 1, remaining - 1)} @ region")]]
void *hyp_early_alloc_page(void *arg){
rc_unfold(base);
......@@ -98,7 +106,7 @@ void *hyp_early_alloc_page(void *arg){
[[rc::requires("{s = (n * PAGE_SIZE)%Z}")]]
[[rc::requires("global mem : uninit<struct_region>")]]
[[rc::ensures("global mem : {(l, 0, n)} @ region")]]
[[rc::tactics("all: unfold PAGES, PAGE_SIZE in *; solve_goal.")]]
[[rc::tactics("all: rewrite -> ly_size_PAGES in *; unfold PAGE_SIZE in *; solve_goal.")]]
void hyp_early_alloc_init(unsigned char* virt, unsigned int size){
base = virt;
end = (uintptr_t) ((uintptr_t) virt + size);
......
From refinedc.typing Require Import typing.
From refinedc.linux.pkvm.early_alloc Require Import generated_code.
From refinedc.linux.pkvm.early_alloc Require Import generated_spec.
From refinedc.linux.pkvm.early_alloc Require Import instances.
Set Default Proof Using "Type".
(* Generated from [linux/pkvm/early_alloc.c]. *)
Section proof_hyp_early_alloc_contig.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [hyp_early_alloc_contig]. *)
Lemma type_hyp_early_alloc_contig (global_mem : loc) :
global_locs !! "mem" = Some global_mem
typed_function (impl_hyp_early_alloc_contig global_mem) type_of_hyp_early_alloc_contig.
Proof.
Open Scope printing_sugar.
start_function "hyp_early_alloc_contig" ([[[base given] remaining] n]) => arg_nr_pages local_i local_ret local_p.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_contig" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: unfold PAGE_SIZE, PAGE_SHIFT in *; try solve_goal.
+ assert (0 n 12); last by lia. by apply Z.shiftl_nonneg.
+ transitivity max_alloc_end; last done; etransitivity; last exact H10; rewrite Z.shiftl_mul_pow2 -?Z.add_assoc => //=; apply -> Z.add_le_mono_l; lia.
+ rewrite Z.shiftl_mul_pow2 in H18 => //. lia.
+ rewrite Z.shiftl_mul_pow2 //=. lia.
+ apply: has_layout_loc_trans' => //. by rewrite ly_offset_PAGES.
all: print_sidecondition_goal "hyp_early_alloc_contig".
Qed.
End proof_hyp_early_alloc_contig.
(* Let's skip that, you seem to have some faith. *)
......@@ -23,7 +23,7 @@ Section proof_hyp_early_alloc_init.
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_init" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: unfold PAGES, PAGE_SIZE in *; solve_goal.
all: rewrite -> ly_size_PAGES in *; unfold PAGE_SIZE in *; solve_goal.
all: print_sidecondition_goal "hyp_early_alloc_init".
Qed.
End proof_hyp_early_alloc_init.
......@@ -96,12 +96,12 @@ Section spec.
(* Specifications for function [hyp_early_alloc_contig]. *)
Definition type_of_hyp_early_alloc_contig :=
fn( (base, given, remaining, n) : loc * Z * Z * Z; (n @ (int (u32))); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) 0 < n remaining n PAGE_SHIFT max_int u32)
() : (), (&own (uninit (PAGES (Z.to_nat n)))); (global_with_type "mem" Own (((base, given + n, remaining - n)%Z) @ (region))).
() : (), (&own (zeroed (PAGES (Z.to_nat n)))); (global_with_type "mem" Own (((base, given + n, remaining - n)%Z) @ (region))).
(* Specifications for function [hyp_early_alloc_page]. *)
Definition type_of_hyp_early_alloc_page :=
fn( (base, given, remaining) : loc * Z * Z; (uninit (void*)); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) 0 remaining)
() : (), (&own (uninit (PAGE))); (global_with_type "mem" Own (((base, given + 1, remaining - 1)) @ (region))).
() : (), (&own (zeroed (PAGE))); (global_with_type "mem" Own (((base, given + 1, remaining - 1)) @ (region))).
(* Specifications for function [hyp_early_alloc_init]. *)
Definition type_of_hyp_early_alloc_init :=
......
......@@ -4,6 +4,8 @@ Set Default Proof Using "Type".
Remove Hints find_in_context_type_val_P_own_singleton_inst : typeclass_instances.
(*** Simplification of locations ***)
Class SimplLoc (l1 l2 : loc) : Prop := simpl_loc : l1 = l2.
Instance simpl_loc_eta (l : loc):
......@@ -43,6 +45,15 @@ Instance simpl_loc_extra4 l n1 n2:
SimplLoc (l + (n1 + 0%nat) * n2) (l + (n1 * n2)).
Proof. f_equal. lia. Qed.
(*** Things about PAGES ***)
Global Instance simpl_ly_size_page_le i j:
SimplBothRel ()%nat (PAGES i).(ly_size) (PAGES j).(ly_size) (i j)%nat.
Proof. rewrite /PAGES /ly_with_align /ly_size /PAGE_SIZE /=. split; lia. Qed.
Lemma ly_size_PAGES i : ly_size (PAGES i) = (i * Z.to_nat PAGE_SIZE)%nat.
Proof. by rewrite /PAGES /ly_with_align /ly_size. Qed.
Section instances.
Context `{!typeG Σ}.
......@@ -146,58 +157,15 @@ Section instances.
SimplifyHyp (loc_in_bounds l n) (Some 0%N) :=
λ T, i2p (simplify_hyp_loc_in_bounds_ptr_in_range l n T).
Lemma subsume_uninit_split l β ly1 ly2 T `{!CanSolve (ly2.(ly_size) ly1.(ly_size))%nat}:
(ly_align ly2 ly_align ly1%nat ((l + ly2.(ly_size)) ◁ₗ{β} uninit (ly_offset ly1 ly2.(ly_size)) - T)) -
subsume (l ◁ₗ{β} uninit ly1) (l ◁ₗ{β} uninit ly2) T.
Proof.
unfold CanSolve in *. iIntros "[% HT] Hl".
iDestruct (split_uninit ly2.(ly_size) with "Hl") as "[Hl1 Hl2]"; [lia|].
rewrite /ty_own/=.
iSplitL "Hl1". 2: by iApply "HT".
iDestruct "Hl1" as (???) "?".
iExists _. iFrame. iPureIntro.
split => //. by apply: has_layout_loc_trans'.
Qed.
Global Instance subsume_uninit_split_inst l β ly1 ly2 `{!CanSolve (ly2.(ly_size) ly1.(ly_size))%nat} :
SubsumePlace l β (uninit ly1) (uninit ly2) | 15 :=
λ T, i2p (subsume_uninit_split l β ly1 ly2 T).
Lemma subsume_uninit_uninit_PAGES p n1 n2 (T : iProp Σ):
n2 n1%nat ((p + ly_size (PAGES n2)) ◁ₗ uninit (PAGES (n1 - n2)) - T) -
subsume (p ◁ₗ uninit (PAGES n1))%I (p ◁ₗ uninit (PAGES n2))%I T.
Proof.
iIntros "[% HT] Hp". rewrite /uninit /ty_own /=.
iDestruct "Hp" as (v Hly1 Hly2) "Hp".
rewrite -(take_drop (ly_size (PAGES n2)) v).
rewrite /heap_mapsto_own_state heap_mapsto_app.
iDestruct "Hp" as "[Hp Hp+n2]".
iSplitL "Hp".
- iExists _. iFrame. iSplit; iPureIntro.
+ rewrite /has_layout_val in Hly1.
rewrite /has_layout_val take_length Hly1.
rewrite /PAGES /PAGE_SIZE /ly_with_align /ly_size /=.
rewrite min_l //=. lia.
+ move: Hly2. by rewrite /has_layout_loc /aligned_to /PAGES /ly_with_align /ly_align.
- iApply ("HT" with "[Hp+n2]").
rewrite /has_layout_val in Hly1.
rewrite take_length min_l; last first.
{ rewrite Hly1 /PAGES /PAGE_SIZE /ly_with_align /ly_size /=. lia. }
iExists _. iFrame. iSplit; iPureIntro.
+ rewrite /has_layout_val drop_length Hly1.
rewrite /PAGES /PAGE_SIZE /ly_with_align /ly_size /=. lia.
+ move: Hly2. rewrite /has_layout_loc /aligned_to /ly_align /ly_size /=.
rewrite /PAGE_SIZE. move => Hly2. apply Z.divide_add_r => //.
rewrite Nat2Z.inj_mul. apply Z.divide_mul_r. rewrite Z2Nat.id => //.
Qed.
(* Global Instance subsume_uninit_uninit_PAGES_inst p n1 n2: *)
(* Subsume (p ◁ₗ uninit (PAGES n1))%I (p ◁ₗ uninit (PAGES n2))%I := *)
(* λ T, i2p (subsume_uninit_uninit_PAGES p n1 n2 T). *)
Lemma ly_offset_PAGES n m:
(ly_offset (PAGES n) (ly_size (PAGES m))) = PAGES (n - m).
Proof. Admitted.
Proof.
rewrite ly_size_PAGES /ly_offset /PAGES /ly_with_align /ly_size /PAGE_SIZE /=.
f_equal; first lia. rewrite min_l // /factor2 /factor2' /=. case_match => //=.
assert (p = Pos.of_nat m * (2 ^ 12))%positive as ->. { simpl. lia. }
rewrite Pos_factor2_mult Pos_factor2_pow. lia.
Qed.
(*
Lemma subsume_zeroed_zeroed_PAGES p n1 n2 (T : iProp Σ) `{!CanSolve (n1 n2)%nat}:
((p + ly_size (PAGES n2)) ◁ₗ zeroed (PAGES (n1 - n2)) - T) -
subsume (p ◁ₗ zeroed (PAGES n1))%I (p ◁ₗ zeroed (PAGES n2))%I T.
......@@ -216,24 +184,11 @@ Section instances.
Global Instance subsume_zeroed_zeroed_PAGES_lt_inst p n1 n2 `{!CanSolve (n2 n1)%nat}:
Subsume (p ◁ₗ zeroed (PAGES n1))%I (p ◁ₗ zeroed (PAGES n2))%I :=
λ T, i2p (subsume_zeroed_zeroed_PAGES_lt p n1 n2 T).
Lemma subsume_uninit_zeroed_0 p ly1 ly2 T:
⌜ly_align ly1 = ly_align ly2⌝ ∗ ⌜ly_size ly2 = 0%nat⌝ ∗ (p ◁ₗ uninit ly1 -∗ T) -∗
subsume (p ◁ₗ uninit ly1)%I (p ◁ₗ zeroed ly2)%I T.
Proof.
iIntros "HT Hp".
iDestruct (ty_aligned with "Hp") as %Hal.
iDestruct (loc_in_bounds_in_bounds with "Hp") as "#Hlib".
rewrite /ty_own /= /has_layout_loc. rewrite /has_layout_loc /= in Hal.
iDestruct "HT" as "(<-&->&HT)". iSplitR; last by iApply "HT".
iSplit; first done. rewrite /zero_val heap_mapsto_eq. iSplit; last done.
rewrite replicate_length. iApply (loc_in_bounds_shorten with "Hlib"). lia.
Qed.
Global Instance subsume_uninit_zeroed_0_inst p ly1 ly2:
Subsume (p ◁ₗ uninit ly1)%I (p ◁ₗ zeroed ly2)%I :=
λ T, i2p (subsume_uninit_zeroed_0 p ly1 ly2 T).
*)
End instances.
Typeclasses Opaque FindLocInBounds.
Typeclasses Opaque PAGES.
Global Opaque PAGES.
(* Typeclasses Opaque PAGE_SIZE PAGE_SHIFT. *)
......@@ -196,6 +196,7 @@ Section proofs.
iSplitL "Hcases".
{ iDestruct "Hcases" as "[[H %]|H]"; [iLeft | iRight] => //. iSplitL => //. iPureIntro. lia. }
iDestruct (ty_ref (t := uninit u16) with "[] Hnext+1 []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
iRename select (local_ticket _)%I into "Hticket".
iRename select (local_got_it ◁ₗ _)%I into "Hgot_it".
iDestruct (ty_ref (t := next @ int u16) with "[] Hticket []") as "$" => //.
......@@ -240,6 +241,7 @@ Section proofs.
iDestruct select (ticket_range _ _ _) as "$".
iDestruct select (_ _)%I as "$".
iDestruct (ty_ref (t := uninit u16) with "[] Hi+1 []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
iRename select (local_ticket _)%I into "Hticket".
iDestruct (ty_ref (t := next @ int u16) with "[] Hticket []") as "$" => //.
iRename select (local_got_it ◁ₗ _)%I into "Hgot_it".
......@@ -311,6 +313,7 @@ Section proofs.
iRename select (local_next _)%I into "Hlocal_next".
iDestruct (ty_ref (t := next @ int u16) with "[] Hlocal_ticket []") as "$" => //.
iDestruct (ty_ref (t := uninit u16) with "[] Hlocal_next []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
** iRename select (_ ◁ₗ next @ int u16)%I into "Hnext".
iDestruct (ty_aligned with "Hnext") as %?.
iDestruct (ty_deref with "Hnext") as (?) "[Hnext Hv]".
......@@ -344,6 +347,7 @@ Section proofs.
iRename select (local_next _)%I into "Hlocal_next".
iDestruct (ty_ref (t := next @ int u16) with "[] Hlocal_ticket []") as "$" => //.
iDestruct (ty_ref (t := uninit u16) with "[] Hlocal_next []") as "$" => //.
{ iPureIntro. split => //. by apply Forall_forall. }
- (* #4 Final loop: checking if we are the owner. *)
destruct s.
+ repeat liRStep; liShow.
......
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 fixpoint.
From refinedc.typing Require Import programs function bytes globals int fixpoint.
From refinedc.lang Require Import heap.
From iris.program_logic Require Export language.
Set Default Proof Using "Type".
......
From iris.algebra Require Import list.
From refinedc.typing Require Export type.
From refinedc.typing Require Import programs singleton uninit int.
From refinedc.typing Require Import programs singleton bytes int.
Set Default Proof Using "Type".
Section array.
......@@ -135,17 +135,21 @@ Section array.
l ◁ₗ{β} array ly (replicate n (uninit ly)) l ◁ₗ{β} uninit (mk_array_layout ly n).
Proof.
rewrite /ty_own/= => ?. iSplit.
- rewrite heap_mapsto_own_state_layout_alt. iDestruct 1 as (Hl) "[Hb Ha]". iSplit => //. clear Hl.
iInduction n as [|n] "IH" forall (l) => /=.
{ iExists []. rewrite heap_mapsto_own_state_nil mult_0_r.
iFrame. iPureIntro. rewrite /has_layout_val/ly_size/=. lia. }
- iInduction n as [|n] "IH" forall (l) => /=; iIntros "(%&Hlib&Htys)".
{ iExists []. rewrite heap_mapsto_own_state_nil mult_0_r Forall_nil.
iFrame "Hlib". iPureIntro. rewrite /has_layout_val/ly_size/=. naive_solver lia. }
setoid_rewrite offset_loc_S. setoid_rewrite offset_loc_1. rewrite offset_loc_0.
iDestruct "Ha" as "[Hl Ha]". iDestruct (loc_in_bounds_split_mul_S with "Hb") as "[#Hb1 Hb2]".
iDestruct ("IH" with "Hb2 Ha") as (v2 Hv2) "Hv2".
iDestruct "Hl" as (v1 Hv1 Hl1) "Hv1".
iExists (v1 ++ v2). rewrite heap_mapsto_own_state_app Hv1 /has_layout_val app_length Hv1 Hv2. iFrame.
iPureIntro. rewrite {2 3}/ly_size/=. lia.
- iDestruct 1 as (v Hv Hl) "Hl". iSplit => //.
iDestruct "Htys" as "[Hty Htys]".
iDestruct (loc_in_bounds_split_mul_S with "Hlib") as "[#Hlib1 Hlib2]".
iDestruct ("IH" with "[Hlib2 Htys]") as (v2 Hv2 ? _) "Hv2".
{ iFrame. iPureIntro. revert select (layout_wf _). revert select (_ `has_layout_loc` _).
rewrite /has_layout_loc /layout_wf /aligned_to. destruct l as [? a].
move => /= [? ->] [? ->]. eexists. by rewrite -Z.mul_add_distr_r. }
rewrite {2}/ty_own/=. iDestruct "Hty" as (v1 Hv1 Hl1 _) "Hv1".
iExists (v1 ++ v2). rewrite heap_mapsto_own_state_app Hv1 /has_layout_val app_length Hv1 Hv2.
iFrame. rewrite Forall_forall. iPureIntro. split_and! => //.
rewrite {2 3}/ly_size/=. lia.
- iDestruct 1 as (v Hv Hl _) "Hl". iSplit => //.
iInduction n as [|n] "IH" forall (v l Hv Hl) => /=.
{ rewrite mult_0_r right_id.
iApply loc_in_bounds_shorten; last by iApply heap_mapsto_own_state_loc_in_bounds. lia. }
......@@ -164,7 +168,7 @@ Section array.
iFrame "Hbl". rewrite replicate_length drop_length Hv.
destruct ly as [k?]. repeat unfold ly_size => /=.
have ->: (k * n = k * S n - k)%nat by lia. done.
+ iSplitL "Hl"; last done. iExists _. iFrame. iPureIntro. split => //.
+ iSplitL "Hl"; last done. iExists _. iFrame. iPureIntro. rewrite Forall_forall. split_and! => //.
rewrite /has_layout_val take_length_le ?Hv; repeat unfold ly_size => /=; lia.
Qed.
......
......@@ -2,7 +2,7 @@ From iris.proofmode Require Import coq_tactics reduction.
From refinedc.typing Require Export type.
From refinedc.lithium Require Export tactics.
From refinedc.typing.automation Require Export normalize solvers simplification proof_state.
From refinedc.typing Require Import programs function singleton own struct uninit int.
From refinedc.typing Require Import programs function singleton own struct bytes int.
Set Default Proof Using "Type".
(** * Registering extensions *)
......
From refinedc.typing Require Export type.
From refinedc.typing Require Import programs int own.
Set Default Proof Using "Type".
(* NOTE: we might want to have a type [bytes : list mbyte → type] one day,
and the [bytewise] abstraction could be encoded on top of it. *)
Section bytewise.
Context `{!typeG Σ}.
Implicit Types P : mbyte Prop.
Program Definition bytewise (P : mbyte Prop) (ly : layout) : type := {|
ty_own β l :=
v, v `has_layout_val` ly
l `has_layout_loc` ly
Forall P v
l [β] v;
|}%I.
Next Obligation.
iIntros (?????). iDestruct 1 as (?) "(?&?&?&Hl)".
iMod (heap_mapsto_own_state_share with "Hl") as "Hl".
eauto with iFrame.
Qed.
Global Program Instance movable_bytewise ly P : Movable (bytewise P ly) := {|
ty_layout := ly;
ty_own_val v := v `has_layout_val` ly Forall P v;
|}%I.
Next Obligation. iIntros (???). by iDestruct 1 as (????) "_". Qed.
Next Obligation. by iIntros (??? [??]). Qed.
Next Obligation. iIntros (???). iDestruct 1 as (????) "?". by eauto. Qed.
Next Obligation. iIntros (??? v ?) "? [%%]". iExists v. by iFrame. Qed.
Lemma bytewise_weaken l β P1 P2 ly:
( b, P1 b P2 b)
l ◁ₗ{β} bytewise P1 ly - l ◁ₗ{β} bytewise P2 ly.
Proof.
iIntros (?). iDestruct 1 as (????) "H". iExists _; iFrame.
iPureIntro; split_and! => //. by eapply Forall_impl.
Qed.
Lemma split_bytewise n l β P ly:
(n ly.(ly_size))%nat
l ◁ₗ{β} bytewise P ly -
l ◁ₗ{β} bytewise P (ly_set_size ly n)
(l + n) ◁ₗ{β} bytewise P (ly_offset ly n).
Proof.
iIntros (?). iDestruct 1 as (v Hv Hl HP) "Hl".
rewrite -[v](take_drop n) heap_mapsto_own_state_app.
iDestruct "Hl" as "[Hl1 Hl2]". iSplitL "Hl1".
- iExists _. iFrame.
eapply Forall_take in HP. rewrite /has_layout_val in Hv.
by rewrite /has_layout_val take_length min_l // Hv.
- rewrite take_length_le ?Hv //. iExists _. iFrame.
eapply Forall_drop in HP. eapply has_layout_ly_offset in Hl.
by rewrite /has_layout_val drop_length Hv.
Qed.
Lemma merge_bytewise l β P ly1 ly2:
(ly1.(ly_size) ly2.(ly_size))%nat
(ly_align ly2 ly_align ly1)%nat
l ◁ₗ{β} bytewise P ly1 -
(l + ly1.(ly_size)) ◁ₗ{β} (bytewise P (ly_offset ly2 ly1.(ly_size))) -
l ◁ₗ{β} bytewise P ly2.
Proof.
iIntros (??).
iDestruct 1 as (v1 Hv1 Hl1 HP1) "Hl1".
iDestruct 1 as (v2 Hv2 Hl2 HP2) "Hl2".
iExists (v1 ++ v2).
rewrite heap_mapsto_own_state_app Hv1 /has_layout_val app_length Hv1 Hv2.
iFrame. iPureIntro. split_and!.
- rewrite {2}/ly_size/=. lia.
- by apply: has_layout_loc_trans'.
- by apply Forall_app.
Qed.
Lemma bytewise_loc_in_bounds l β P ly:
l ◁ₗ{β} bytewise P ly - loc_in_bounds l (ly_size ly).
Proof.
iDestruct 1 as (v <-) "(_&_&?)".
by iApply heap_mapsto_own_state_loc_in_bounds.
Qed.
Global Instance loc_in_bounds_bytewise β P ly:
LocInBounds (bytewise P ly) β (ly_size ly).
Proof. constructor. iIntros (?). by iApply bytewise_loc_in_bounds. Qed.
Lemma subsume_bytewise_eq l β P1 P2 ly1 ly2
`{!CanSolve (ly1.(ly_size) = ly2.(ly_size))} T:
b, P1 b P2 b
(l `has_layout_loc` ly1 - l `has_layout_loc` ly2 T) -
subsume (l ◁ₗ{β} bytewise P1 ly1) (l ◁ₗ{β} bytewise P2 ly2) T.
Proof.
revert select (CanSolve _) => Hsz. unfold CanSolve in *.
iDestruct 1 as (HPs) "HT". iDestruct 1 as (??? HP) "?".
apply (Forall_impl _ _ _ HP) in HPs.
iDestruct ("HT" with "[//]") as (?) "$".
iExists _. iFrame. by rewrite /has_layout_val -Hsz.
Qed.
Global Instance subsume_bytewise_eq_inst l β P1 P2 ly1 ly2
`{!CanSolve (ly1.(ly_size) = ly2.(ly_size))}:
SubsumePlace l β (bytewise P1 ly1) (bytewise P2 ly2) | 10 :=
λ T, i2p (subsume_bytewise_eq l β P1 P2 ly1 ly2 T).
Lemma subsume_bytewise_merge l β P1 P2 ly1 ly2
`{!CanSolve (ly1.(ly_size) ly2.(ly_size))%nat} T:
b, P1 b P2 b
ly_align ly2 ly_align ly1%nat
((l + ly1.(ly_size)) ◁ₗ{β} bytewise P2 (ly_offset ly2 ly1.(ly_size)) T) -
subsume (l ◁ₗ{β} bytewise P1 ly1) (l ◁ₗ{β} bytewise P2 ly2) T.
Proof.
unfold CanSolve in *.
iIntros "(%&%&?&$) Hl".
iDestruct (bytewise_weaken with "Hl") as "Hl" => //.
iApply (merge_bytewise with "Hl") => //.
Qed.
Global Instance subsume_bytewise_merge_inst l β P1 P2 ly1 ly2
`{!CanSolve (ly1.(ly_size) ly2.(ly_size))%nat}:
SubsumePlace l β (bytewise P1 ly1) (bytewise P2 ly2) | 20 :=
λ T, i2p (subsume_bytewise_merge l β P1 P2 ly1 ly2 T).
Lemma subsume_bytewise_split l β P1 P2 ly1 ly2
`{!CanSolve (ly2.(ly_size) ly1.(ly_size))%nat} T:
b, P1 b P2 b
ly_align ly2 ly_align ly1%nat
((l + ly2.(ly_size)) ◁ₗ{β} bytewise P1 (ly_offset ly1 ly2.(ly_size)) - T) -
subsume (l ◁ₗ{β} bytewise P1 ly1) (l ◁ₗ{β} bytewise P2 ly2) T.
Proof.
unfold CanSolve in *.
iIntros "(%&%&HT) Hl".
iDestruct (split_bytewise with "Hl") as "[Hl1 Hl2]" => //.
iDestruct (bytewise_weaken with "Hl1") as "Hl1" => //.
iDestruct ("HT" with "Hl2") as "$".
iDestruct "Hl1" as (????) "Hl1".
iExists _; iFrame. iPureIntro; split_and! => //.
by apply: has_layout_loc_trans'.
Qed.
Global Instance subsume_bytewise_split_inst l β P1 P2 ly1 ly2
`{!CanSolve (ly2.(ly_size) ly1.(ly_size))%nat}:
SubsumePlace l β (bytewise P1 ly1) (bytewise P2 ly2) | 15 :=
λ T, i2p (subsume_bytewise_split l β P1 P2 ly1 ly2 T).
Lemma type_add_bytewise v2 β P ly (p : loc) n it T:
(n it -
0 n
Z.to_nat n ly.(ly_size)%nat
(p ◁ₗ{β} bytewise P (ly_set_size ly (Z.to_nat n)) - v2 ◁ᵥ n @ int it -
T (val_of_loc (p + n)) (t2mt ((p + n) @ &frac{β} (bytewise P (ly_offset ly (Z.to_nat n))))))) -
typed_bin_op v2 (v2 ◁ᵥ n @ int it) p (p ◁ₗ{β} bytewise P ly) (PtrOffsetOp u8) (IntOp it) PtrOp T.
Proof.
iIntros "HT" (Hint) "Hp". iIntros (Φ) "HΦ".
move: (Hint) => /val_of_int_in_range?.
iDestruct ("HT" with "[//]") as (??) "HT".
iDestruct (split_bytewise (Z.to_nat n) with "Hp") as "[H1 H2]"; [lia..|].
iApply wp_ptr_offset. by apply val_to_of_loc. by apply val_to_of_int. done.
iModIntro. rewrite offset_loc_sz1//.
iApply ("HΦ" with "[H2]"). 2: iApply ("HT" with "H1 []"). rewrite Z2Nat.id; [|lia]. by iFrame.
by iPureIntro.
Qed.
Global Instance type_add_bytewise_inst v2 β P ly (p : loc) n it:
TypedBinOp v2 (v2 ◁ᵥ n @ int it)%I p (p ◁ₗ{β} bytewise P ly) (PtrOffsetOp u8) (IntOp it) PtrOp :=
λ T, i2p (type_add_bytewise v2 β P ly p n it T).
End bytewise.
Notation "bytewise< P , ly >" := (bytewise P ly)
(only printing, format "'bytewise<' P ',' ly '>'") : printing_sugar.
Typeclasses Opaque bytewise.
Notation uninit := (bytewise (λ _, True)).
Section uninit.
Context `{!typeG Σ}.
Lemma uninit_own_spec l ly:
(l ◁ₗ uninit ly)%I (l |ly|)%I.
Proof.
rewrite /ty_own/=; iSplit.
- iDestruct 1 as (??? _) "Hl". iExists _; by iFrame.
- iDestruct 1 as (v ??) "Hl". iExists v; iFrame. by rewrite Forall_forall.
Qed.
(* This only works for [Own] since [ty] might have interior mutability. *)
Lemma uninit_mono l ty ly `{!Movable ty} `{!FastDone (ty.(ty_layout) = ly)} T:
( v, v ◁ᵥ ty - T) -
subsume (l ◁ₗ ty) (l ◁ₗ uninit ly) T.
Proof.