Skip to content
Snippets Groups Projects
Commit b0a28e4a authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Use Z in early_alloc.

parent cb702f79
No related branches found
No related tags found
No related merge requests found
Pipeline #41520 passed
......@@ -12,12 +12,13 @@
//@rc::import instances from refinedc.linux.pkvm.early_alloc (for proofs only)
struct
[[rc::refined_by("base : loc", "given : nat", "remaining : nat")]]
[[rc::refined_by("base : loc", "given : Z", "remaining : Z")]]
[[rc::let("z_cur : Z = {(base.2 + given * PAGE_SIZE)%Z}")]]
[[rc::let("z_end : Z = {(base.2 + (given + remaining) * PAGE_SIZE)%Z}")]]
[[rc::constraints("{0 ≤ given}", "{0 ≤ remaining}")]]
region {
[[rc::field("own_constrained<nonshr_constraint<"
"{(base.1, z_cur) ◁ₗ uninit (PAGES remaining)}>, "
"{(base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining))}>, "
"value<void*, base>>")]] unsigned char* base;
[[rc::field("z_end @ int<uintptr_t>")]] uintptr_t end;
[[rc::field("z_cur @ int<uintptr_t>")]] uintptr_t cur;
......@@ -29,7 +30,7 @@ static struct region mem;
#define end (mem.end)
#define cur (mem.cur)
[[rc::parameters("base : loc", "given : nat", "remaining : nat")]]
[[rc::parameters("base : loc", "given : Z", "remaining : Z")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::returns("given @ int<size_t>")]]
[[rc::ensures("global mem : {(base, given, remaining)} @ region")]]
......@@ -43,11 +44,12 @@ size_t hyp_early_alloc_nr_pages(void){
[[rc::ensures("own p : zeroed<PAGE>")]]
extern void clear_page(void *to);
[[rc::parameters("base : loc", "given : nat", "remaining : nat", "n : nat")]]
[[rc::parameters("base : loc", "given : Z", "remaining : Z", "n : Z")]]
[[rc::args("n @ int<u32>")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region", "{0%nat < n ≤ remaining}")]]
[[rc::returns("&own<uninit<PAGES<n>>>")]]
[[rc::ensures("global mem : {(base, given + n, remaining - n)%nat} @ region")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::requires("{0 < n ≤ remaining}")]]
[[rc::returns("&own<uninit<PAGES<{Z.to_nat n}>>>")]]
[[rc::ensures("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::trust_me]] // FIXME
void *hyp_early_alloc_contig(unsigned int nr_pages){
uintptr_t ret = cur, p;
......@@ -71,20 +73,22 @@ void *hyp_early_alloc_contig(unsigned int nr_pages){
return rc_copy_alloc_id((void *) ret, base);
}
[[rc::parameters("base : loc", "given : nat", "remaining : nat")]]
[[rc::parameters("base : loc", "given : Z", "remaining : Z")]]
[[rc::args("uninit<void*>")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region", "{remaining ≠ 0%nat}")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::requires("{0 < remaining}")]]
[[rc::returns("&own<uninit<PAGE>>")]]
[[rc::ensures("global mem : {(base, given + 1, remaining - 1)%nat} @ region")]]
[[rc::ensures("global mem : {(base, given + 1, remaining - 1)} @ region")]]
void *hyp_early_alloc_page(void *arg){
return hyp_early_alloc_contig(1);
}
[[rc::parameters("l : loc", "n : nat", "s : Z")]]
[[rc::args("l @ &own<uninit<PAGES<n>>>", "s @ int<u32>")]]
[[rc::parameters("l : loc", "n : Z", "s : Z")]]
[[rc::args("l @ &own<uninit<PAGES<{Z.to_nat n}>>>", "s @ int<u32>")]]
[[rc::requires("{s = (n * PAGE_SIZE)%Z}")]]
[[rc::requires("global mem : uninit<struct_region>")]]
[[rc::ensures("global mem : {(l, 0%nat, n)} @ region")]]
[[rc::ensures("global mem : {(l, 0, n)} @ region")]]
[[rc::tactics("all: unfold PAGES, 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);
......
......@@ -6,88 +6,88 @@ Set Default Proof Using "Type".
(* Generated from [linux/pkvm/early_alloc.c]. *)
Section code.
Definition file_0 : string := "linux/pkvm/early_alloc.c".
Definition loc_2 : location_info := LocationInfo file_0 38 2 38 52.
Definition loc_3 : location_info := LocationInfo file_0 38 9 38 51.
Definition loc_4 : location_info := LocationInfo file_0 38 9 38 45.
Definition loc_5 : location_info := LocationInfo file_0 38 10 38 19.
Definition loc_6 : location_info := LocationInfo file_0 38 10 38 19.
Definition loc_7 : location_info := LocationInfo file_0 38 11 38 14.
Definition loc_8 : location_info := LocationInfo file_0 38 22 38 44.
Definition loc_9 : location_info := LocationInfo file_0 38 34 38 44.
Definition loc_10 : location_info := LocationInfo file_0 38 34 38 44.
Definition loc_11 : location_info := LocationInfo file_0 38 35 38 38.
Definition loc_12 : location_info := LocationInfo file_0 38 49 38 51.
Definition loc_15 : location_info := LocationInfo file_0 53 2 53 31.
Definition loc_16 : location_info := LocationInfo file_0 56 2 57 26.
Definition loc_17 : location_info := LocationInfo file_0 59 2 59 30.
Definition loc_18 : location_info := LocationInfo file_0 60 2 63 3.
Definition loc_19 : location_info := LocationInfo file_0 71 2 71 67.
Definition loc_20 : location_info := LocationInfo file_0 71 9 71 66.
Definition loc_21 : location_info := LocationInfo file_0 71 35 71 47.
Definition loc_22 : location_info := LocationInfo file_0 71 35 71 47.
Definition loc_23 : location_info := LocationInfo file_0 71 37 71 40.
Definition loc_24 : location_info := LocationInfo file_0 71 51 71 65.
Definition loc_25 : location_info := LocationInfo file_0 71 61 71 64.
Definition loc_26 : location_info := LocationInfo file_0 71 61 71 64.
Definition loc_27 : location_info := LocationInfo file_0 60 29 63 3.
Definition loc_28 : location_info := LocationInfo file_0 61 4 61 20.
Definition loc_29 : location_info := LocationInfo file_0 62 4 62 26.
Definition loc_30 : location_info := LocationInfo file_0 62 11 62 25.
Definition loc_31 : location_info := LocationInfo file_0 61 4 61 13.
Definition loc_32 : location_info := LocationInfo file_0 61 5 61 8.
Definition loc_33 : location_info := LocationInfo file_0 61 16 61 19.
Definition loc_34 : location_info := LocationInfo file_0 61 16 61 19.
Definition loc_36 : location_info := LocationInfo file_0 60 6 60 27.
Definition loc_37 : location_info := LocationInfo file_0 60 6 60 15.
Definition loc_38 : location_info := LocationInfo file_0 60 6 60 15.
Definition loc_39 : location_info := LocationInfo file_0 60 7 60 10.
Definition loc_40 : location_info := LocationInfo file_0 60 18 60 27.
Definition loc_41 : location_info := LocationInfo file_0 60 18 60 27.
Definition loc_42 : location_info := LocationInfo file_0 60 19 60 22.
Definition loc_43 : location_info := LocationInfo file_0 59 2 59 11.
Definition loc_44 : location_info := LocationInfo file_0 59 3 59 6.
Definition loc_45 : location_info := LocationInfo file_0 59 2 59 29.
Definition loc_46 : location_info := LocationInfo file_0 59 2 59 11.
Definition loc_47 : location_info := LocationInfo file_0 59 2 59 11.
Definition loc_48 : location_info := LocationInfo file_0 59 3 59 6.
Definition loc_49 : location_info := LocationInfo file_0 59 15 59 29.
Definition loc_50 : location_info := LocationInfo file_0 59 15 59 23.
Definition loc_51 : location_info := LocationInfo file_0 59 15 59 23.
Definition loc_52 : location_info := LocationInfo file_0 59 27 59 29.
Definition loc_53 : location_info := LocationInfo file_0 57 4 57 26.
Definition loc_54 : location_info := LocationInfo file_0 57 11 57 25.
Definition loc_56 : location_info := LocationInfo file_0 56 6 56 15.
Definition loc_58 : location_info := LocationInfo file_0 56 7 56 15.
Definition loc_59 : location_info := LocationInfo file_0 56 7 56 15.
Definition loc_60 : location_info := LocationInfo file_0 53 18 53 27.
Definition loc_61 : location_info := LocationInfo file_0 53 18 53 27.
Definition loc_62 : location_info := LocationInfo file_0 53 19 53 22.
Definition loc_67 : location_info := LocationInfo file_0 80 2 80 35.
Definition loc_68 : location_info := LocationInfo file_0 80 9 80 34.
Definition loc_69 : location_info := LocationInfo file_0 80 9 80 31.
Definition loc_70 : location_info := LocationInfo file_0 80 9 80 31.
Definition loc_71 : location_info := LocationInfo file_0 80 32 80 33.
Definition loc_74 : location_info := LocationInfo file_0 89 2 89 20.
Definition loc_75 : location_info := LocationInfo file_0 90 2 90 52.
Definition loc_76 : location_info := LocationInfo file_0 91 2 91 31.
Definition loc_77 : location_info := LocationInfo file_0 91 2 91 11.
Definition loc_78 : location_info := LocationInfo file_0 91 3 91 6.
Definition loc_79 : location_info := LocationInfo file_0 91 14 91 30.
Definition loc_80 : location_info := LocationInfo file_0 91 26 91 30.
Definition loc_81 : location_info := LocationInfo file_0 91 26 91 30.
Definition loc_82 : location_info := LocationInfo file_0 90 2 90 11.
Definition loc_83 : location_info := LocationInfo file_0 90 3 90 6.
Definition loc_84 : location_info := LocationInfo file_0 90 14 90 51.
Definition loc_85 : location_info := LocationInfo file_0 90 26 90 51.
Definition loc_86 : location_info := LocationInfo file_0 90 27 90 43.
Definition loc_87 : location_info := LocationInfo file_0 90 39 90 43.
Definition loc_88 : location_info := LocationInfo file_0 90 39 90 43.
Definition loc_89 : location_info := LocationInfo file_0 90 46 90 50.
Definition loc_90 : location_info := LocationInfo file_0 90 46 90 50.
Definition loc_91 : location_info := LocationInfo file_0 89 2 89 12.
Definition loc_92 : location_info := LocationInfo file_0 89 3 89 6.
Definition loc_93 : location_info := LocationInfo file_0 89 15 89 19.
Definition loc_94 : location_info := LocationInfo file_0 89 15 89 19.
Definition loc_2 : location_info := LocationInfo file_0 39 2 39 52.
Definition loc_3 : location_info := LocationInfo file_0 39 9 39 51.
Definition loc_4 : location_info := LocationInfo file_0 39 9 39 45.
Definition loc_5 : location_info := LocationInfo file_0 39 10 39 19.
Definition loc_6 : location_info := LocationInfo file_0 39 10 39 19.
Definition loc_7 : location_info := LocationInfo file_0 39 11 39 14.
Definition loc_8 : location_info := LocationInfo file_0 39 22 39 44.
Definition loc_9 : location_info := LocationInfo file_0 39 34 39 44.
Definition loc_10 : location_info := LocationInfo file_0 39 34 39 44.
Definition loc_11 : location_info := LocationInfo file_0 39 35 39 38.
Definition loc_12 : location_info := LocationInfo file_0 39 49 39 51.
Definition loc_15 : location_info := LocationInfo file_0 55 2 55 31.
Definition loc_16 : location_info := LocationInfo file_0 58 2 59 26.
Definition loc_17 : location_info := LocationInfo file_0 61 2 61 30.
Definition loc_18 : location_info := LocationInfo file_0 62 2 65 3.
Definition loc_19 : location_info := LocationInfo file_0 73 2 73 67.
Definition loc_20 : location_info := LocationInfo file_0 73 9 73 66.
Definition loc_21 : location_info := LocationInfo file_0 73 35 73 47.
Definition loc_22 : location_info := LocationInfo file_0 73 35 73 47.
Definition loc_23 : location_info := LocationInfo file_0 73 37 73 40.
Definition loc_24 : location_info := LocationInfo file_0 73 51 73 65.
Definition loc_25 : location_info := LocationInfo file_0 73 61 73 64.
Definition loc_26 : location_info := LocationInfo file_0 73 61 73 64.
Definition loc_27 : location_info := LocationInfo file_0 62 29 65 3.
Definition loc_28 : location_info := LocationInfo file_0 63 4 63 20.
Definition loc_29 : location_info := LocationInfo file_0 64 4 64 26.
Definition loc_30 : location_info := LocationInfo file_0 64 11 64 25.
Definition loc_31 : location_info := LocationInfo file_0 63 4 63 13.
Definition loc_32 : location_info := LocationInfo file_0 63 5 63 8.
Definition loc_33 : location_info := LocationInfo file_0 63 16 63 19.
Definition loc_34 : location_info := LocationInfo file_0 63 16 63 19.
Definition loc_36 : location_info := LocationInfo file_0 62 6 62 27.
Definition loc_37 : location_info := LocationInfo file_0 62 6 62 15.
Definition loc_38 : location_info := LocationInfo file_0 62 6 62 15.
Definition loc_39 : location_info := LocationInfo file_0 62 7 62 10.
Definition loc_40 : location_info := LocationInfo file_0 62 18 62 27.
Definition loc_41 : location_info := LocationInfo file_0 62 18 62 27.
Definition loc_42 : location_info := LocationInfo file_0 62 19 62 22.
Definition loc_43 : location_info := LocationInfo file_0 61 2 61 11.
Definition loc_44 : location_info := LocationInfo file_0 61 3 61 6.
Definition loc_45 : location_info := LocationInfo file_0 61 2 61 29.
Definition loc_46 : location_info := LocationInfo file_0 61 2 61 11.
Definition loc_47 : location_info := LocationInfo file_0 61 2 61 11.
Definition loc_48 : location_info := LocationInfo file_0 61 3 61 6.
Definition loc_49 : location_info := LocationInfo file_0 61 15 61 29.
Definition loc_50 : location_info := LocationInfo file_0 61 15 61 23.
Definition loc_51 : location_info := LocationInfo file_0 61 15 61 23.
Definition loc_52 : location_info := LocationInfo file_0 61 27 61 29.
Definition loc_53 : location_info := LocationInfo file_0 59 4 59 26.
Definition loc_54 : location_info := LocationInfo file_0 59 11 59 25.
Definition loc_56 : location_info := LocationInfo file_0 58 6 58 15.
Definition loc_58 : location_info := LocationInfo file_0 58 7 58 15.
Definition loc_59 : location_info := LocationInfo file_0 58 7 58 15.
Definition loc_60 : location_info := LocationInfo file_0 55 18 55 27.
Definition loc_61 : location_info := LocationInfo file_0 55 18 55 27.
Definition loc_62 : location_info := LocationInfo file_0 55 19 55 22.
Definition loc_67 : location_info := LocationInfo file_0 83 2 83 35.
Definition loc_68 : location_info := LocationInfo file_0 83 9 83 34.
Definition loc_69 : location_info := LocationInfo file_0 83 9 83 31.
Definition loc_70 : location_info := LocationInfo file_0 83 9 83 31.
Definition loc_71 : location_info := LocationInfo file_0 83 32 83 33.
Definition loc_74 : location_info := LocationInfo file_0 93 2 93 20.
Definition loc_75 : location_info := LocationInfo file_0 94 2 94 52.
Definition loc_76 : location_info := LocationInfo file_0 95 2 95 31.
Definition loc_77 : location_info := LocationInfo file_0 95 2 95 11.
Definition loc_78 : location_info := LocationInfo file_0 95 3 95 6.
Definition loc_79 : location_info := LocationInfo file_0 95 14 95 30.
Definition loc_80 : location_info := LocationInfo file_0 95 26 95 30.
Definition loc_81 : location_info := LocationInfo file_0 95 26 95 30.
Definition loc_82 : location_info := LocationInfo file_0 94 2 94 11.
Definition loc_83 : location_info := LocationInfo file_0 94 3 94 6.
Definition loc_84 : location_info := LocationInfo file_0 94 14 94 51.
Definition loc_85 : location_info := LocationInfo file_0 94 26 94 51.
Definition loc_86 : location_info := LocationInfo file_0 94 27 94 43.
Definition loc_87 : location_info := LocationInfo file_0 94 39 94 43.
Definition loc_88 : location_info := LocationInfo file_0 94 39 94 43.
Definition loc_89 : location_info := LocationInfo file_0 94 46 94 50.
Definition loc_90 : location_info := LocationInfo file_0 94 46 94 50.
Definition loc_91 : location_info := LocationInfo file_0 93 2 93 12.
Definition loc_92 : location_info := LocationInfo file_0 93 3 93 6.
Definition loc_93 : location_info := LocationInfo file_0 93 15 93 19.
Definition loc_94 : location_info := LocationInfo file_0 93 15 93 19.
(* Definition of struct [region]. *)
Program Definition struct_region := {|
......
......@@ -23,6 +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: print_sidecondition_goal "hyp_early_alloc_init".
Qed.
End proof_hyp_early_alloc_init.
......@@ -16,17 +16,20 @@ Section spec.
Notation PAGE := (PAGES 1).
(* Definition of type [region]. *)
Definition region_rec : (loc * nat * nat -d> typeO) (loc * nat * nat -d> typeO) := (λ self patt__,
Definition region_rec : (loc * Z * Z -d> typeO) (loc * Z * Z -d> typeO) := (λ self patt__,
let base := patt__.1.1 in
let given := patt__.1.2 in
let remaining := patt__.2 in
let z_cur : Z := (base.2 + given * PAGE_SIZE)%Z in
let z_end : Z := (base.2 + (given + remaining) * PAGE_SIZE)%Z in
struct struct_region [@{type}
(own_constrained (nonshr_constraint ((base.1, z_cur) uninit (PAGES remaining))) (value (void*) (base))) ;
constrained (struct struct_region [@{type}
(own_constrained (nonshr_constraint ((base.1, z_cur) uninit (PAGES (Z.to_nat remaining)))) (value (void*) (base))) ;
(z_end @ (int (uintptr_t))) ;
(z_cur @ (int (uintptr_t)))
]
]) (
0 given
0 remaining
)
)%I.
Typeclasses Opaque region_rec.
......@@ -34,22 +37,25 @@ Section spec.
Proof. solve_type_proper. Qed.
Definition region : rtype := {|
rty_type := loc * nat * nat;
rty_type := loc * Z * Z;
rty r__ := fixp region_rec r__
|}.
Lemma region_unfold (patt__ : loc * nat * nat):
Lemma region_unfold (patt__ : loc * Z * Z):
(patt__ @ region)%I ≡@{type} (
let base := patt__.1.1 in
let given := patt__.1.2 in
let remaining := patt__.2 in
let z_cur : Z := (base.2 + given * PAGE_SIZE)%Z in
let z_end : Z := (base.2 + (given + remaining) * PAGE_SIZE)%Z in
struct struct_region [@{type}
(own_constrained (nonshr_constraint ((base.1, z_cur) uninit (PAGES remaining))) (value (void*) (base))) ;
constrained (struct struct_region [@{type}
(own_constrained (nonshr_constraint ((base.1, z_cur) uninit (PAGES (Z.to_nat remaining)))) (value (void*) (base))) ;
(z_end @ (int (uintptr_t))) ;
(z_cur @ (int (uintptr_t)))
]
]) (
0 given
0 remaining
)
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
......@@ -78,7 +84,7 @@ Section spec.
(* Specifications for function [hyp_early_alloc_nr_pages]. *)
Definition type_of_hyp_early_alloc_nr_pages :=
fn( (base, given, remaining) : loc * nat * nat; (global_with_type "mem" Own (((base, given, remaining)) @ (region))))
fn( (base, given, remaining) : loc * Z * Z; (global_with_type "mem" Own (((base, given, remaining)) @ (region))))
() : (), (given @ (int (size_t))); (global_with_type "mem" Own (((base, given, remaining)) @ (region))).
(* Specifications for function [clear_page]. *)
......@@ -88,18 +94,18 @@ Section spec.
(* Specifications for function [hyp_early_alloc_contig]. *)
Definition type_of_hyp_early_alloc_contig :=
fn( (base, given, remaining, n) : loc * nat * nat * nat; (n @ (int (u32))); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) 0%nat < n remaining)
() : (), (&own (uninit (PAGES (n)))); (global_with_type "mem" Own (((base, given + n, remaining - n)%nat) @ (region))).
fn( (base, given, remaining, n) : loc * Z * Z * Z; (n @ (int (u32))); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) 0 < n remaining)
() : (), (&own (uninit (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 * nat * nat; (uninit (void*)); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) remaining 0%nat)
() : (), (&own (uninit (PAGE))); (global_with_type "mem" Own (((base, given + 1, remaining - 1)%nat) @ (region))).
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))).
(* Specifications for function [hyp_early_alloc_init]. *)
Definition type_of_hyp_early_alloc_init :=
fn( (l, n, s) : loc * nat * Z; (l @ (&own (uninit (PAGES (n))))), (s @ (int (u32))); s = (n * PAGE_SIZE)%Z (global_with_type "mem" Own (uninit (struct_region))))
() : (), (void); (global_with_type "mem" Own (((l, 0%nat, n)) @ (region))).
fn( (l, n, s) : loc * Z * Z; (l @ (&own (uninit (PAGES (Z.to_nat n))))), (s @ (int (u32))); s = (n * PAGE_SIZE)%Z (global_with_type "mem" Own (uninit (struct_region))))
() : (), (void); (global_with_type "mem" Own (((l, 0, n)) @ (region))).
End spec.
Typeclasses Opaque region_rec.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment