more early alloc

5f88f4c4 · Michael Sammler · 3730c601 · 5f88f4c4 · 5f88f4c4 · 5f88f4c4
Commit 5f88f4c4 authored 4 years ago by Michael Sammler
--- a/linux/pkvm/early_alloc.c
+++ b/linux/pkvm/early_alloc.c
@@ -58,6 +58,7 @@ extern void clear_page(void *to);
              "rewrite Z.shiftl_mul_pow2 -?Z.add_assoc => //=; apply -> Z.add_le_mono_l; lia.")]]
 [[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.")]]
 void *hyp_early_alloc_contig(unsigned int nr_pages){
  uintptr_t ret = cur, p;
  unsigned int i;

--- a/linux/pkvm/proofs/early_alloc/generated_code.v
+++ b/linux/pkvm/proofs/early_alloc/generated_code.v
@@ -17,87 +17,87 @@ Section code.
  Definition loc_10 : location_info := LocationInfo file_0 41 34 41 44.
  Definition loc_11 : location_info := LocationInfo file_0 41 35 41 38.
  Definition loc_12 : location_info := LocationInfo file_0 41 49 41 51.
-  Definition loc_15 : location_info := LocationInfo file_0 62 2 62 31.
-  Definition loc_16 : location_info := LocationInfo file_0 65 2 66 26.
-  Definition loc_17 : location_info := LocationInfo file_0 68 2 68 16.
-  Definition loc_18 : location_info := LocationInfo file_0 68 16 68 3.
-  Definition loc_19 : location_info := LocationInfo file_0 69 2 69 30.
-  Definition loc_20 : location_info := LocationInfo file_0 70 2 73 3.
-  Definition loc_21 : location_info := LocationInfo file_0 81 2 81 67.
-  Definition loc_22 : location_info := LocationInfo file_0 81 9 81 66.
-  Definition loc_23 : location_info := LocationInfo file_0 81 35 81 47.
-  Definition loc_24 : location_info := LocationInfo file_0 81 35 81 47.
-  Definition loc_25 : location_info := LocationInfo file_0 81 37 81 40.
-  Definition loc_26 : location_info := LocationInfo file_0 81 51 81 65.
-  Definition loc_27 : location_info := LocationInfo file_0 81 61 81 64.
-  Definition loc_28 : location_info := LocationInfo file_0 81 61 81 64.
-  Definition loc_29 : location_info := LocationInfo file_0 70 29 73 3.
-  Definition loc_30 : location_info := LocationInfo file_0 71 4 71 20.
-  Definition loc_31 : location_info := LocationInfo file_0 72 4 72 26.
-  Definition loc_32 : location_info := LocationInfo file_0 72 11 72 25.
-  Definition loc_33 : location_info := LocationInfo file_0 71 4 71 13.
-  Definition loc_34 : location_info := LocationInfo file_0 71 5 71 8.
-  Definition loc_35 : location_info := LocationInfo file_0 71 16 71 19.
-  Definition loc_36 : location_info := LocationInfo file_0 71 16 71 19.
-  Definition loc_38 : location_info := LocationInfo file_0 70 6 70 27.
-  Definition loc_39 : location_info := LocationInfo file_0 70 6 70 15.
-  Definition loc_40 : location_info := LocationInfo file_0 70 6 70 15.
-  Definition loc_41 : location_info := LocationInfo file_0 70 7 70 10.
-  Definition loc_42 : location_info := LocationInfo file_0 70 18 70 27.
-  Definition loc_43 : location_info := LocationInfo file_0 70 18 70 27.
-  Definition loc_44 : location_info := LocationInfo file_0 70 19 70 22.
-  Definition loc_45 : location_info := LocationInfo file_0 69 2 69 11.
-  Definition loc_46 : location_info := LocationInfo file_0 69 3 69 6.
-  Definition loc_47 : location_info := LocationInfo file_0 69 2 69 29.
-  Definition loc_48 : location_info := LocationInfo file_0 69 2 69 11.
-  Definition loc_49 : location_info := LocationInfo file_0 69 2 69 11.
-  Definition loc_50 : location_info := LocationInfo file_0 69 3 69 6.
-  Definition loc_51 : location_info := LocationInfo file_0 69 15 69 29.
-  Definition loc_52 : location_info := LocationInfo file_0 69 15 69 23.
-  Definition loc_53 : location_info := LocationInfo file_0 69 15 69 23.
-  Definition loc_54 : location_info := LocationInfo file_0 69 27 69 29.
-  Definition loc_55 : location_info := LocationInfo file_0 68 2 68 15.
-  Definition loc_56 : location_info := LocationInfo file_0 68 3 68 15.
-  Definition loc_57 : location_info := LocationInfo file_0 68 5 68 8.
-  Definition loc_58 : location_info := LocationInfo file_0 66 4 66 26.
-  Definition loc_59 : location_info := LocationInfo file_0 66 11 66 25.
-  Definition loc_61 : location_info := LocationInfo file_0 65 6 65 15.
-  Definition loc_63 : location_info := LocationInfo file_0 65 7 65 15.
-  Definition loc_64 : location_info := LocationInfo file_0 65 7 65 15.
-  Definition loc_65 : location_info := LocationInfo file_0 62 18 62 27.
-  Definition loc_66 : location_info := LocationInfo file_0 62 18 62 27.
-  Definition loc_67 : location_info := LocationInfo file_0 62 19 62 22.
-  Definition loc_72 : location_info := LocationInfo file_0 91 2 91 16.
-  Definition loc_73 : location_info := LocationInfo file_0 91 16 91 3.
-  Definition loc_74 : location_info := LocationInfo file_0 92 2 92 35.
-  Definition loc_75 : location_info := LocationInfo file_0 92 9 92 34.
-  Definition loc_76 : location_info := LocationInfo file_0 92 9 92 31.
-  Definition loc_77 : location_info := LocationInfo file_0 92 9 92 31.
-  Definition loc_78 : location_info := LocationInfo file_0 92 32 92 33.
-  Definition loc_79 : location_info := LocationInfo file_0 91 2 91 15.
-  Definition loc_80 : location_info := LocationInfo file_0 91 3 91 15.
-  Definition loc_81 : location_info := LocationInfo file_0 91 5 91 8.
-  Definition loc_84 : location_info := LocationInfo file_0 102 2 102 20.
-  Definition loc_85 : location_info := LocationInfo file_0 103 2 103 52.
-  Definition loc_86 : location_info := LocationInfo file_0 104 2 104 31.
-  Definition loc_87 : location_info := LocationInfo file_0 104 2 104 11.
-  Definition loc_88 : location_info := LocationInfo file_0 104 3 104 6.
-  Definition loc_89 : location_info := LocationInfo file_0 104 14 104 30.
-  Definition loc_90 : location_info := LocationInfo file_0 104 26 104 30.
-  Definition loc_91 : location_info := LocationInfo file_0 104 26 104 30.
-  Definition loc_92 : location_info := LocationInfo file_0 103 2 103 11.
-  Definition loc_93 : location_info := LocationInfo file_0 103 3 103 6.
-  Definition loc_94 : location_info := LocationInfo file_0 103 14 103 51.
-  Definition loc_95 : location_info := LocationInfo file_0 103 26 103 51.
-  Definition loc_96 : location_info := LocationInfo file_0 103 27 103 43.
-  Definition loc_97 : location_info := LocationInfo file_0 103 39 103 43.
-  Definition loc_98 : location_info := LocationInfo file_0 103 39 103 43.
-  Definition loc_99 : location_info := LocationInfo file_0 103 46 103 50.
-  Definition loc_100 : location_info := LocationInfo file_0 103 46 103 50.
-  Definition loc_101 : location_info := LocationInfo file_0 102 2 102 12.
-  Definition loc_102 : location_info := LocationInfo file_0 102 3 102 6.
-  Definition loc_103 : location_info := LocationInfo file_0 102 15 102 19.
-  Definition loc_104 : location_info := LocationInfo file_0 102 15 102 19.
+  Definition loc_15 : location_info := LocationInfo file_0 63 2 63 31.
+  Definition loc_16 : location_info := LocationInfo file_0 66 2 67 26.
+  Definition loc_17 : location_info := LocationInfo file_0 69 2 69 16.
+  Definition loc_18 : location_info := LocationInfo file_0 69 16 69 3.
+  Definition loc_19 : location_info := LocationInfo file_0 70 2 70 30.
+  Definition loc_20 : location_info := LocationInfo file_0 71 2 74 3.
+  Definition loc_21 : location_info := LocationInfo file_0 82 2 82 67.
+  Definition loc_22 : location_info := LocationInfo file_0 82 9 82 66.
+  Definition loc_23 : location_info := LocationInfo file_0 82 35 82 47.
+  Definition loc_24 : location_info := LocationInfo file_0 82 35 82 47.
+  Definition loc_25 : location_info := LocationInfo file_0 82 37 82 40.
+  Definition loc_26 : location_info := LocationInfo file_0 82 51 82 65.
+  Definition loc_27 : location_info := LocationInfo file_0 82 61 82 64.
+  Definition loc_28 : location_info := LocationInfo file_0 82 61 82 64.
+  Definition loc_29 : location_info := LocationInfo file_0 71 29 74 3.
+  Definition loc_30 : location_info := LocationInfo file_0 72 4 72 20.
+  Definition loc_31 : location_info := LocationInfo file_0 73 4 73 26.
+  Definition loc_32 : location_info := LocationInfo file_0 73 11 73 25.
+  Definition loc_33 : location_info := LocationInfo file_0 72 4 72 13.
+  Definition loc_34 : location_info := LocationInfo file_0 72 5 72 8.
+  Definition loc_35 : location_info := LocationInfo file_0 72 16 72 19.
+  Definition loc_36 : location_info := LocationInfo file_0 72 16 72 19.
+  Definition loc_38 : location_info := LocationInfo file_0 71 6 71 27.
+  Definition loc_39 : location_info := LocationInfo file_0 71 6 71 15.
+  Definition loc_40 : location_info := LocationInfo file_0 71 6 71 15.
+  Definition loc_41 : location_info := LocationInfo file_0 71 7 71 10.
+  Definition loc_42 : location_info := LocationInfo file_0 71 18 71 27.
+  Definition loc_43 : location_info := LocationInfo file_0 71 18 71 27.
+  Definition loc_44 : location_info := LocationInfo file_0 71 19 71 22.
+  Definition loc_45 : location_info := LocationInfo file_0 70 2 70 11.
+  Definition loc_46 : location_info := LocationInfo file_0 70 3 70 6.
+  Definition loc_47 : location_info := LocationInfo file_0 70 2 70 29.
+  Definition loc_48 : location_info := LocationInfo file_0 70 2 70 11.
+  Definition loc_49 : location_info := LocationInfo file_0 70 2 70 11.
+  Definition loc_50 : location_info := LocationInfo file_0 70 3 70 6.
+  Definition loc_51 : location_info := LocationInfo file_0 70 15 70 29.
+  Definition loc_52 : location_info := LocationInfo file_0 70 15 70 23.
+  Definition loc_53 : location_info := LocationInfo file_0 70 15 70 23.
+  Definition loc_54 : location_info := LocationInfo file_0 70 27 70 29.
+  Definition loc_55 : location_info := LocationInfo file_0 69 2 69 15.
+  Definition loc_56 : location_info := LocationInfo file_0 69 3 69 15.
+  Definition loc_57 : location_info := LocationInfo file_0 69 5 69 8.
+  Definition loc_58 : location_info := LocationInfo file_0 67 4 67 26.
+  Definition loc_59 : location_info := LocationInfo file_0 67 11 67 25.
+  Definition loc_61 : location_info := LocationInfo file_0 66 6 66 15.
+  Definition loc_63 : location_info := LocationInfo file_0 66 7 66 15.
+  Definition loc_64 : location_info := LocationInfo file_0 66 7 66 15.
+  Definition loc_65 : location_info := LocationInfo file_0 63 18 63 27.
+  Definition loc_66 : location_info := LocationInfo file_0 63 18 63 27.
+  Definition loc_67 : location_info := LocationInfo file_0 63 19 63 22.
+  Definition loc_72 : location_info := LocationInfo file_0 92 2 92 16.
+  Definition loc_73 : location_info := LocationInfo file_0 92 16 92 3.
+  Definition loc_74 : location_info := LocationInfo file_0 93 2 93 35.
+  Definition loc_75 : location_info := LocationInfo file_0 93 9 93 34.
+  Definition loc_76 : location_info := LocationInfo file_0 93 9 93 31.
+  Definition loc_77 : location_info := LocationInfo file_0 93 9 93 31.
+  Definition loc_78 : location_info := LocationInfo file_0 93 32 93 33.
+  Definition loc_79 : location_info := LocationInfo file_0 92 2 92 15.
+  Definition loc_80 : location_info := LocationInfo file_0 92 3 92 15.
+  Definition loc_81 : location_info := LocationInfo file_0 92 5 92 8.
+  Definition loc_84 : location_info := LocationInfo file_0 103 2 103 20.
+  Definition loc_85 : location_info := LocationInfo file_0 104 2 104 52.
+  Definition loc_86 : location_info := LocationInfo file_0 105 2 105 31.
+  Definition loc_87 : location_info := LocationInfo file_0 105 2 105 11.
+  Definition loc_88 : location_info := LocationInfo file_0 105 3 105 6.
+  Definition loc_89 : location_info := LocationInfo file_0 105 14 105 30.
+  Definition loc_90 : location_info := LocationInfo file_0 105 26 105 30.
+  Definition loc_91 : location_info := LocationInfo file_0 105 26 105 30.
+  Definition loc_92 : location_info := LocationInfo file_0 104 2 104 11.
+  Definition loc_93 : location_info := LocationInfo file_0 104 3 104 6.
+  Definition loc_94 : location_info := LocationInfo file_0 104 14 104 51.
+  Definition loc_95 : location_info := LocationInfo file_0 104 26 104 51.
+  Definition loc_96 : location_info := LocationInfo file_0 104 27 104 43.
+  Definition loc_97 : location_info := LocationInfo file_0 104 39 104 43.
+  Definition loc_98 : location_info := LocationInfo file_0 104 39 104 43.
+  Definition loc_99 : location_info := LocationInfo file_0 104 46 104 50.
+  Definition loc_100 : location_info := LocationInfo file_0 104 46 104 50.
+  Definition loc_101 : location_info := LocationInfo file_0 103 2 103 12.
+  Definition loc_102 : location_info := LocationInfo file_0 103 3 103 6.
+  Definition loc_103 : location_info := LocationInfo file_0 103 15 103 19.
+  Definition loc_104 : location_info := LocationInfo file_0 103 15 103 19.

  (* Definition of struct [region]. *)
  Program Definition struct_region := {|

--- a/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_contig.v
+++ b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_contig.v
@@ -28,6 +28,7 @@ Section proof_hyp_early_alloc_contig.
    + 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.
--- a/linux/pkvm/proofs/early_alloc/instances.v
+++ b/linux/pkvm/proofs/early_alloc/instances.v
@@ -10,6 +10,7 @@ Section instances.
  Global Instance simpl_to_NULL_val_of_loc (l : loc) : SimplAndRel (=) NULL (l) (λ T, False).
  Proof. split; naive_solver. Qed.

+  (*** location normalization rules *)
  Lemma simplify_goal_place_shift_loc_0nat_times l n β ty T:
    T (l ◁ₗ{β} ty) -∗ simplify_goal ((l +ₗ 0%nat * n) ◁ₗ{β} ty) T.
  Proof. iIntros "HT". assert (0%nat * n = 0) as -> by lia. rewrite shift_loc_0. iExists _. eauto with iFrame. Qed.
@@ -106,6 +107,22 @@ 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.
@@ -133,9 +150,14 @@ Section instances.
        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).
+  (* 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.
 End instances.

 Typeclasses Opaque FindLocInBounds.
+(* Typeclasses Opaque PAGE_SIZE PAGE_SHIFT. *)