Commit 58efddb9 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Improve the [early_alloc.c] example.

parent c84ba52e
Pipeline #42369 passed with stage
in 15 minutes and 11 seconds
......@@ -35,7 +35,7 @@ static struct region mem;
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::returns("given @ int<size_t>")]]
[[rc::ensures("global mem : {(base, given, remaining)} @ region")]]
[[rc::tactics("all: rewrite /PAGE_SIZE Z.add_simpl_l; try solve_goal.")]]
[[rc::tactics("all: rewrite Z.add_simpl_l; try solve_goal.")]]
[[rc::tactics("all: rewrite Z.shiftr_div_pow2 //= Z.div_mul //=.")]]
size_t hyp_early_alloc_nr_pages(void){
return (cur - (uintptr_t) base) >> PAGE_SHIFT;
......@@ -52,7 +52,6 @@ extern void clear_page(void *to);
[[rc::requires("{0 < n ≤ remaining}", "{n ≪ PAGE_SHIFT ≤ max_int u32}")]]
[[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("all: rewrite -> Z.shiftl_mul_pow2 in *; try lia.")]]
[[rc::tactics("all: try apply: has_layout_loc_trans' => //.")]]
[[rc::tactics("all: rewrite ?ly_offset_PAGES; try solve_goal.")]]
......@@ -106,7 +105,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: rewrite -> ly_size_PAGES in *; unfold PAGE_SIZE in *; solve_goal.")]]
[[rc::tactics("all: rewrite -> ly_size_PAGES in *; solve_goal.")]]
void hyp_early_alloc_init(unsigned char* virt, unsigned int size){
base = virt;
end = (uintptr_t) ((uintptr_t) virt + size);
......
......@@ -12,9 +12,9 @@
#define PAGE_SIZE 4096
#define PAGE_MASK (~(PAGE_SIZE-1))
//@rc::inlined
//@Definition PAGE_SHIFT := (12).
//@Definition PAGE_SIZE := (4096).
//@rc::inlined_prelude
//@Notation PAGE_SHIFT := (12).
//@Notation PAGE_SIZE := (4096).
//@
//@Definition PAGES (n : nat) : layout :=
//@ ly_with_align (n * Z.to_nat PAGE_SIZE) (Z.to_nat PAGE_SIZE).
......
......@@ -17,125 +17,125 @@ 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 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 84 2 88 3.
Definition loc_22 : location_info := LocationInfo file_0 84 7 84 12.
Definition loc_23 : location_info := LocationInfo file_0 84 2 88 3.
Definition loc_24 : location_info := LocationInfo file_0 90 2 90 67.
Definition loc_25 : location_info := LocationInfo file_0 90 9 90 66.
Definition loc_26 : location_info := LocationInfo file_0 90 35 90 47.
Definition loc_27 : location_info := LocationInfo file_0 90 35 90 47.
Definition loc_28 : location_info := LocationInfo file_0 90 37 90 40.
Definition loc_29 : location_info := LocationInfo file_0 90 51 90 65.
Definition loc_30 : location_info := LocationInfo file_0 90 61 90 64.
Definition loc_31 : location_info := LocationInfo file_0 90 61 90 64.
Definition loc_32 : location_info := LocationInfo file_0 84 33 88 3.
Definition loc_33 : location_info := LocationInfo file_0 85 4 85 18.
Definition loc_34 : location_info := LocationInfo file_0 85 18 85 5.
Definition loc_35 : location_info := LocationInfo file_0 86 4 86 24.
Definition loc_36 : location_info := LocationInfo file_0 87 4 87 73.
Definition loc_37 : location_info := LocationInfo file_0 84 2 88 3.
Definition loc_38 : location_info := LocationInfo file_0 84 28 84 31.
Definition loc_39 : location_info := LocationInfo file_0 84 28 84 29.
Definition loc_40 : location_info := LocationInfo file_0 87 4 87 14.
Definition loc_41 : location_info := LocationInfo file_0 87 4 87 14.
Definition loc_42 : location_info := LocationInfo file_0 87 15 87 71.
Definition loc_43 : location_info := LocationInfo file_0 87 41 87 53.
Definition loc_44 : location_info := LocationInfo file_0 87 41 87 53.
Definition loc_45 : location_info := LocationInfo file_0 87 43 87 46.
Definition loc_46 : location_info := LocationInfo file_0 87 57 87 70.
Definition loc_47 : location_info := LocationInfo file_0 87 66 87 69.
Definition loc_48 : location_info := LocationInfo file_0 87 66 87 69.
Definition loc_49 : location_info := LocationInfo file_0 86 4 86 5.
Definition loc_50 : location_info := LocationInfo file_0 86 8 86 23.
Definition loc_51 : location_info := LocationInfo file_0 86 8 86 11.
Definition loc_52 : location_info := LocationInfo file_0 86 8 86 11.
Definition loc_53 : location_info := LocationInfo file_0 86 14 86 23.
Definition loc_54 : location_info := LocationInfo file_0 86 15 86 16.
Definition loc_55 : location_info := LocationInfo file_0 86 15 86 16.
Definition loc_56 : location_info := LocationInfo file_0 86 20 86 22.
Definition loc_57 : location_info := LocationInfo file_0 85 4 85 17.
Definition loc_58 : location_info := LocationInfo file_0 85 5 85 17.
Definition loc_59 : location_info := LocationInfo file_0 85 7 85 10.
Definition loc_60 : location_info := LocationInfo file_0 84 14 84 26.
Definition loc_61 : location_info := LocationInfo file_0 84 14 84 15.
Definition loc_62 : location_info := LocationInfo file_0 84 14 84 15.
Definition loc_63 : location_info := LocationInfo file_0 84 18 84 26.
Definition loc_64 : location_info := LocationInfo file_0 84 18 84 26.
Definition loc_65 : location_info := LocationInfo file_0 84 7 84 8.
Definition loc_66 : location_info := LocationInfo file_0 84 11 84 12.
Definition loc_67 : location_info := LocationInfo file_0 71 29 74 3.
Definition loc_68 : location_info := LocationInfo file_0 72 4 72 20.
Definition loc_69 : location_info := LocationInfo file_0 73 4 73 26.
Definition loc_70 : location_info := LocationInfo file_0 73 11 73 25.
Definition loc_71 : location_info := LocationInfo file_0 72 4 72 13.
Definition loc_72 : location_info := LocationInfo file_0 72 5 72 8.
Definition loc_73 : location_info := LocationInfo file_0 72 16 72 19.
Definition loc_74 : location_info := LocationInfo file_0 72 16 72 19.
Definition loc_76 : location_info := LocationInfo file_0 71 6 71 27.
Definition loc_77 : location_info := LocationInfo file_0 71 6 71 15.
Definition loc_78 : location_info := LocationInfo file_0 71 6 71 15.
Definition loc_79 : location_info := LocationInfo file_0 71 7 71 10.
Definition loc_80 : location_info := LocationInfo file_0 71 18 71 27.
Definition loc_81 : location_info := LocationInfo file_0 71 18 71 27.
Definition loc_82 : location_info := LocationInfo file_0 71 19 71 22.
Definition loc_83 : location_info := LocationInfo file_0 70 2 70 11.
Definition loc_84 : location_info := LocationInfo file_0 70 3 70 6.
Definition loc_85 : location_info := LocationInfo file_0 70 2 70 29.
Definition loc_86 : location_info := LocationInfo file_0 70 2 70 11.
Definition loc_87 : location_info := LocationInfo file_0 70 2 70 11.
Definition loc_88 : location_info := LocationInfo file_0 70 3 70 6.
Definition loc_89 : location_info := LocationInfo file_0 70 15 70 29.
Definition loc_90 : location_info := LocationInfo file_0 70 15 70 23.
Definition loc_91 : location_info := LocationInfo file_0 70 15 70 23.
Definition loc_92 : location_info := LocationInfo file_0 70 27 70 29.
Definition loc_93 : location_info := LocationInfo file_0 69 2 69 15.
Definition loc_94 : location_info := LocationInfo file_0 69 3 69 15.
Definition loc_95 : location_info := LocationInfo file_0 69 5 69 8.
Definition loc_96 : location_info := LocationInfo file_0 67 4 67 26.
Definition loc_97 : location_info := LocationInfo file_0 67 11 67 25.
Definition loc_99 : location_info := LocationInfo file_0 66 6 66 15.
Definition loc_101 : location_info := LocationInfo file_0 66 7 66 15.
Definition loc_102 : location_info := LocationInfo file_0 66 7 66 15.
Definition loc_103 : location_info := LocationInfo file_0 63 18 63 27.
Definition loc_104 : location_info := LocationInfo file_0 63 18 63 27.
Definition loc_105 : location_info := LocationInfo file_0 63 19 63 22.
Definition loc_110 : location_info := LocationInfo file_0 100 2 100 16.
Definition loc_111 : location_info := LocationInfo file_0 100 16 100 3.
Definition loc_112 : location_info := LocationInfo file_0 101 2 101 35.
Definition loc_113 : location_info := LocationInfo file_0 101 9 101 34.
Definition loc_114 : location_info := LocationInfo file_0 101 9 101 31.
Definition loc_115 : location_info := LocationInfo file_0 101 9 101 31.
Definition loc_116 : location_info := LocationInfo file_0 101 32 101 33.
Definition loc_117 : location_info := LocationInfo file_0 100 2 100 15.
Definition loc_118 : location_info := LocationInfo file_0 100 3 100 15.
Definition loc_119 : location_info := LocationInfo file_0 100 5 100 8.
Definition loc_122 : location_info := LocationInfo file_0 111 2 111 20.
Definition loc_123 : location_info := LocationInfo file_0 112 2 112 52.
Definition loc_124 : location_info := LocationInfo file_0 113 2 113 31.
Definition loc_125 : location_info := LocationInfo file_0 113 2 113 11.
Definition loc_126 : location_info := LocationInfo file_0 113 3 113 6.
Definition loc_127 : location_info := LocationInfo file_0 113 14 113 30.
Definition loc_128 : location_info := LocationInfo file_0 113 26 113 30.
Definition loc_129 : location_info := LocationInfo file_0 113 26 113 30.
Definition loc_130 : location_info := LocationInfo file_0 112 2 112 11.
Definition loc_131 : location_info := LocationInfo file_0 112 3 112 6.
Definition loc_132 : location_info := LocationInfo file_0 112 14 112 51.
Definition loc_133 : location_info := LocationInfo file_0 112 26 112 51.
Definition loc_134 : location_info := LocationInfo file_0 112 27 112 43.
Definition loc_135 : location_info := LocationInfo file_0 112 39 112 43.
Definition loc_136 : location_info := LocationInfo file_0 112 39 112 43.
Definition loc_137 : location_info := LocationInfo file_0 112 46 112 50.
Definition loc_138 : location_info := LocationInfo file_0 112 46 112 50.
Definition loc_139 : location_info := LocationInfo file_0 111 2 111 12.
Definition loc_140 : location_info := LocationInfo file_0 111 3 111 6.
Definition loc_141 : location_info := LocationInfo file_0 111 15 111 19.
Definition loc_142 : location_info := LocationInfo file_0 111 15 111 19.
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 83 2 87 3.
Definition loc_22 : location_info := LocationInfo file_0 83 7 83 12.
Definition loc_23 : location_info := LocationInfo file_0 83 2 87 3.
Definition loc_24 : location_info := LocationInfo file_0 89 2 89 67.
Definition loc_25 : location_info := LocationInfo file_0 89 9 89 66.
Definition loc_26 : location_info := LocationInfo file_0 89 35 89 47.
Definition loc_27 : location_info := LocationInfo file_0 89 35 89 47.
Definition loc_28 : location_info := LocationInfo file_0 89 37 89 40.
Definition loc_29 : location_info := LocationInfo file_0 89 51 89 65.
Definition loc_30 : location_info := LocationInfo file_0 89 61 89 64.
Definition loc_31 : location_info := LocationInfo file_0 89 61 89 64.
Definition loc_32 : location_info := LocationInfo file_0 83 33 87 3.
Definition loc_33 : location_info := LocationInfo file_0 84 4 84 18.
Definition loc_34 : location_info := LocationInfo file_0 84 18 84 5.
Definition loc_35 : location_info := LocationInfo file_0 85 4 85 24.
Definition loc_36 : location_info := LocationInfo file_0 86 4 86 73.
Definition loc_37 : location_info := LocationInfo file_0 83 2 87 3.
Definition loc_38 : location_info := LocationInfo file_0 83 28 83 31.
Definition loc_39 : location_info := LocationInfo file_0 83 28 83 29.
Definition loc_40 : location_info := LocationInfo file_0 86 4 86 14.
Definition loc_41 : location_info := LocationInfo file_0 86 4 86 14.
Definition loc_42 : location_info := LocationInfo file_0 86 15 86 71.
Definition loc_43 : location_info := LocationInfo file_0 86 41 86 53.
Definition loc_44 : location_info := LocationInfo file_0 86 41 86 53.
Definition loc_45 : location_info := LocationInfo file_0 86 43 86 46.
Definition loc_46 : location_info := LocationInfo file_0 86 57 86 70.
Definition loc_47 : location_info := LocationInfo file_0 86 66 86 69.
Definition loc_48 : location_info := LocationInfo file_0 86 66 86 69.
Definition loc_49 : location_info := LocationInfo file_0 85 4 85 5.
Definition loc_50 : location_info := LocationInfo file_0 85 8 85 23.
Definition loc_51 : location_info := LocationInfo file_0 85 8 85 11.
Definition loc_52 : location_info := LocationInfo file_0 85 8 85 11.
Definition loc_53 : location_info := LocationInfo file_0 85 14 85 23.
Definition loc_54 : location_info := LocationInfo file_0 85 15 85 16.
Definition loc_55 : location_info := LocationInfo file_0 85 15 85 16.
Definition loc_56 : location_info := LocationInfo file_0 85 20 85 22.
Definition loc_57 : location_info := LocationInfo file_0 84 4 84 17.
Definition loc_58 : location_info := LocationInfo file_0 84 5 84 17.
Definition loc_59 : location_info := LocationInfo file_0 84 7 84 10.
Definition loc_60 : location_info := LocationInfo file_0 83 14 83 26.
Definition loc_61 : location_info := LocationInfo file_0 83 14 83 15.
Definition loc_62 : location_info := LocationInfo file_0 83 14 83 15.
Definition loc_63 : location_info := LocationInfo file_0 83 18 83 26.
Definition loc_64 : location_info := LocationInfo file_0 83 18 83 26.
Definition loc_65 : location_info := LocationInfo file_0 83 7 83 8.
Definition loc_66 : location_info := LocationInfo file_0 83 11 83 12.
Definition loc_67 : location_info := LocationInfo file_0 70 29 73 3.
Definition loc_68 : location_info := LocationInfo file_0 71 4 71 20.
Definition loc_69 : location_info := LocationInfo file_0 72 4 72 26.
Definition loc_70 : location_info := LocationInfo file_0 72 11 72 25.
Definition loc_71 : location_info := LocationInfo file_0 71 4 71 13.
Definition loc_72 : location_info := LocationInfo file_0 71 5 71 8.
Definition loc_73 : location_info := LocationInfo file_0 71 16 71 19.
Definition loc_74 : location_info := LocationInfo file_0 71 16 71 19.
Definition loc_76 : location_info := LocationInfo file_0 70 6 70 27.
Definition loc_77 : location_info := LocationInfo file_0 70 6 70 15.
Definition loc_78 : location_info := LocationInfo file_0 70 6 70 15.
Definition loc_79 : location_info := LocationInfo file_0 70 7 70 10.
Definition loc_80 : location_info := LocationInfo file_0 70 18 70 27.
Definition loc_81 : location_info := LocationInfo file_0 70 18 70 27.
Definition loc_82 : location_info := LocationInfo file_0 70 19 70 22.
Definition loc_83 : location_info := LocationInfo file_0 69 2 69 11.
Definition loc_84 : location_info := LocationInfo file_0 69 3 69 6.
Definition loc_85 : location_info := LocationInfo file_0 69 2 69 29.
Definition loc_86 : location_info := LocationInfo file_0 69 2 69 11.
Definition loc_87 : location_info := LocationInfo file_0 69 2 69 11.
Definition loc_88 : location_info := LocationInfo file_0 69 3 69 6.
Definition loc_89 : location_info := LocationInfo file_0 69 15 69 29.
Definition loc_90 : location_info := LocationInfo file_0 69 15 69 23.
Definition loc_91 : location_info := LocationInfo file_0 69 15 69 23.
Definition loc_92 : location_info := LocationInfo file_0 69 27 69 29.
Definition loc_93 : location_info := LocationInfo file_0 68 2 68 15.
Definition loc_94 : location_info := LocationInfo file_0 68 3 68 15.
Definition loc_95 : location_info := LocationInfo file_0 68 5 68 8.
Definition loc_96 : location_info := LocationInfo file_0 66 4 66 26.
Definition loc_97 : location_info := LocationInfo file_0 66 11 66 25.
Definition loc_99 : location_info := LocationInfo file_0 65 6 65 15.
Definition loc_101 : location_info := LocationInfo file_0 65 7 65 15.
Definition loc_102 : location_info := LocationInfo file_0 65 7 65 15.
Definition loc_103 : location_info := LocationInfo file_0 62 18 62 27.
Definition loc_104 : location_info := LocationInfo file_0 62 18 62 27.
Definition loc_105 : location_info := LocationInfo file_0 62 19 62 22.
Definition loc_110 : location_info := LocationInfo file_0 99 2 99 16.
Definition loc_111 : location_info := LocationInfo file_0 99 16 99 3.
Definition loc_112 : location_info := LocationInfo file_0 100 2 100 35.
Definition loc_113 : location_info := LocationInfo file_0 100 9 100 34.
Definition loc_114 : location_info := LocationInfo file_0 100 9 100 31.
Definition loc_115 : location_info := LocationInfo file_0 100 9 100 31.
Definition loc_116 : location_info := LocationInfo file_0 100 32 100 33.
Definition loc_117 : location_info := LocationInfo file_0 99 2 99 15.
Definition loc_118 : location_info := LocationInfo file_0 99 3 99 15.
Definition loc_119 : location_info := LocationInfo file_0 99 5 99 8.
Definition loc_122 : location_info := LocationInfo file_0 110 2 110 20.
Definition loc_123 : location_info := LocationInfo file_0 111 2 111 52.
Definition loc_124 : location_info := LocationInfo file_0 112 2 112 31.
Definition loc_125 : location_info := LocationInfo file_0 112 2 112 11.
Definition loc_126 : location_info := LocationInfo file_0 112 3 112 6.
Definition loc_127 : location_info := LocationInfo file_0 112 14 112 30.
Definition loc_128 : location_info := LocationInfo file_0 112 26 112 30.
Definition loc_129 : location_info := LocationInfo file_0 112 26 112 30.
Definition loc_130 : location_info := LocationInfo file_0 111 2 111 11.
Definition loc_131 : location_info := LocationInfo file_0 111 3 111 6.
Definition loc_132 : location_info := LocationInfo file_0 111 14 111 51.
Definition loc_133 : location_info := LocationInfo file_0 111 26 111 51.
Definition loc_134 : location_info := LocationInfo file_0 111 27 111 43.
Definition loc_135 : location_info := LocationInfo file_0 111 39 111 43.
Definition loc_136 : location_info := LocationInfo file_0 111 39 111 43.
Definition loc_137 : location_info := LocationInfo file_0 111 46 111 50.
Definition loc_138 : location_info := LocationInfo file_0 111 46 111 50.
Definition loc_139 : location_info := LocationInfo file_0 110 2 110 12.
Definition loc_140 : location_info := LocationInfo file_0 110 3 110 6.
Definition loc_141 : location_info := LocationInfo file_0 110 15 110 19.
Definition loc_142 : location_info := LocationInfo file_0 110 15 110 19.
(* Definition of struct [region]. *)
Program Definition struct_region := {|
......
......@@ -37,7 +37,6 @@ Section proof_hyp_early_alloc_contig.
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_contig" "#3".
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.
all: rewrite -> Z.shiftl_mul_pow2 in *; try lia.
all: try apply: has_layout_loc_trans' => //.
all: rewrite ?ly_offset_PAGES; try solve_goal.
......
......@@ -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: rewrite -> ly_size_PAGES in *; unfold PAGE_SIZE in *; solve_goal.
all: rewrite -> ly_size_PAGES in *; solve_goal.
all: print_sidecondition_goal "hyp_early_alloc_init".
Qed.
End proof_hyp_early_alloc_init.
......@@ -23,7 +23,7 @@ Section proof_hyp_early_alloc_nr_pages.
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_nr_pages" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: rewrite /PAGE_SIZE Z.add_simpl_l; try solve_goal.
all: rewrite Z.add_simpl_l; try solve_goal.
all: rewrite Z.shiftr_div_pow2 //= Z.div_mul //=.
all: print_sidecondition_goal "hyp_early_alloc_nr_pages".
Qed.
......
......@@ -3,18 +3,19 @@ From refinedc.linux.pkvm.early_alloc Require Import generated_code.
Set Default Proof Using "Type".
(* Generated from [linux/pkvm/early_alloc.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Inlined code. *)
(* Inlined code (prelude). *)
Notation PAGE_SHIFT := (12).
Notation PAGE_SIZE := (4096).
Definition PAGE_SHIFT := (12).
Definition PAGE_SIZE := (4096).
Definition PAGES (n : nat) : layout :=
ly_with_align (n * Z.to_nat PAGE_SIZE) (Z.to_nat PAGE_SIZE).
Definition PAGES (n : nat) : layout :=
ly_with_align (n * Z.to_nat PAGE_SIZE) (Z.to_nat PAGE_SIZE).
Notation PAGE := (PAGES 1).
Notation PAGE := (PAGES 1).
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Definition of type [region]. *)
Definition region_rec : (loc * Z * Z -d> typeO) (loc * Z * Z -d> typeO) := (λ self patt__,
......
......@@ -2,82 +2,15 @@ From refinedc.typing Require Import typing.
From refinedc.linux.pkvm.early_alloc Require Import generated_spec.
Set Default Proof Using "Type".
(*** Demonstration of FindHypEqual ***)
(* Instance simpl_loc_offset_0_times (l : loc) (n : Z): *)
(* SimplLoc (l +ₗ 0%nat * n) l. *)
(* Proof. assert (0%nat * n = 0) as -> by lia. by rewrite shift_loc_0. Qed. *)
(* TODO: move this to own.v or somewhere in the automation folder *)
Inductive FICLocSemantic : Set :=.
Global Instance find_in_context_type_loc_semantic_inst `{!typeG Σ} l :
FindInContext (FindLoc l) 2%nat FICLocSemantic :=
λ T, i2p (find_in_context_type_loc_id l T).
(* TODO: move this to somewhere in the automation folder *)
Lemma tac_solve_loc_eq `{!typeG Σ} l1 β1 ty1 l2 β2 ty2:
l1 = l2
FindHypEqual FICLocSemantic (l1 ◁ₗ{β1} ty1) (l2 ◁ₗ{β2} ty2) (l1 ◁ₗ{β2} ty2).
Proof. by move => ->. Qed.
(* TODO: move this to somewhere in the automation folder and implement
it properly. *)
Ltac solve_loc_eq :=
rewrite ?shift_loc_0; done.
(* TODO: move this to somewhere in the automation folder *)
Hint Extern 10 (FindHypEqual FICLocSemantic (_ ◁ₗ{_} _) (_ ◁ₗ{_} _) _) =>
(notypeclasses refine (tac_solve_loc_eq _ _ _ _ _ _ _); solve_loc_eq) : typeclass_instances.
(*** Simplification of locations ***)
Class SimplLoc (l1 l2 : loc) : Prop := simpl_loc : l1 = l2.
Instance simpl_loc_eta (l : loc):
SimplLoc (l.1, l.2) l.
Proof. by destruct l. Qed.
Instance simpl_loc_eta_with_offset (l : loc) (n : Z):
SimplLoc (l.1, l.2 + n) (l + n).
Proof. by destruct l. Qed.
Instance simpl_loc_shift_loc_assoc (l : loc) (n1 n2 : Z):
SimplLoc (l + n1 + n2) (l + (n1 + n2)).
Proof. by rewrite shift_loc_assoc. Qed.
Instance simpl_loc_offset_add_assoc id p n1 n2:
SimplLoc (id, p + n1 + n2) (id, p + (n1 + n2)).
Proof. by rewrite Z.add_assoc. Qed.
(* The following instances are probably over-specialized. *)
Instance simpl_loc_extra1 l n i j:
SimplLoc (l + (n + (i + j)%nat)) (l + (n + i + j)).
Proof. f_equal. lia. Qed.
Instance simpl_loc_extra2 l n i:
SimplLoc (l + (n * PAGE_SIZE + ly_size (PAGES i))) (l + (n + i) * PAGE_SIZE).
Proof. rewrite Z.mul_add_distr_r. repeat f_equal. rewrite /PAGES /ly_size /PAGE_SIZE /=. lia. Qed.
Instance simpl_loc_extra3 l n i:
SimplLoc (l + (n * PAGE_SIZE + i 12)) (l + (n + i) * PAGE_SIZE).
Proof. rewrite Z.mul_add_distr_r. repeat f_equal. rewrite Z.shiftl_mul_pow2 //. Qed.
Instance simpl_loc_extra4 l n1 n2:
SimplLoc (l + (n1 + 0%nat) * n2) (l + (n1 * n2)).
Proof. f_equal. lia. Qed.
Instance simpl_loc_extra5 l n1 n2 n3 n4:
SimplLoc (l + (n1 + (n2 + n3)%nat) * n4) (l + (n1 + n2 + n3) * n4).
Proof. f_equal. lia. Qed.
(*** Things about PAGES ***)
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.
Lemma ly_offset_PAGES n m:
(ly_offset (PAGES n) (ly_size (PAGES m))) = PAGES (n - m).
Proof.
rewrite ly_size_PAGES /ly_offset /PAGES /ly_with_align /ly_size /PAGE_SIZE /=.
rewrite ly_size_PAGES /ly_offset /PAGES /ly_with_align /ly_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.
......@@ -85,11 +18,11 @@ Qed.
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.
Proof. rewrite /PAGES /ly_with_align /ly_size /=. split; lia. Qed.
Global Instance simpl_ly_size_page_eq i j:
SimplBothRel (=) (PAGES i).(ly_size) (PAGES j).(ly_size) (i = j).
Proof. rewrite !ly_size_PAGES /PAGE_SIZE. split; lia. Qed.
Proof. rewrite !ly_size_PAGES. split; lia. Qed.
Global Instance simpl_extra1 k m n:
SimplBoth (k = ly_size (ly_offset (PAGES n) (ly_size (PAGES m)))) (k = ly_size (PAGES (n - m))).
......@@ -105,21 +38,6 @@ 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_simpl_loc l1 l2 β ty `{!SimplLoc l1 l2} T:
T (l2 ◁ₗ{β} ty) - simplify_goal (l1 ◁ₗ{β} ty) T.
Proof. revert select (SimplLoc _ _) => ->. iIntros "?". iExists _. eauto with iFrame. Qed.
Global Instance simplify_goal_place_simpl_loc_inst l1 l2 β ty `{!SimplLoc l1 l2}:
SimplifyGoalPlace l1 β ty (Some 0%N) :=
λ T, i2p (simplify_goal_place_simpl_loc l1 l2 β ty T).
Lemma simplify_hyp_place_simpl_loc l1 l2 β ty `{!SimplLoc l1 l2} T:
(l2 ◁ₗ{β} ty - T) - simplify_hyp (l1 ◁ₗ{β} ty) T.
Proof. revert select (SimplLoc _ _) => ->. eauto with iFrame. Qed.
Global Instance simplify_hyp_place_simpl_loc_inst l1 l2 β ty `{!SimplLoc l1 l2}:
SimplifyHypPlace l1 β ty (Some 0%N) :=
λ T, i2p (simplify_hyp_place_simpl_loc l1 l2 β ty T).
Lemma simplify_hyp_place_PAGES_stuff l β n1 n2 ty T:
0 n2 ((l + ((n1 + n2) * PAGE_SIZE)) ◁ₗ{β} ty - T) -
simplify_hyp ((l + (n1 * PAGE_SIZE + ly_size (PAGES (Z.to_nat n2)))) ◁ₗ{β} ty) T.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment