diff --git a/_CoqProject b/_CoqProject
index 6e1ea9b46464243cca8b48feab7aef1fd14e29e0..7779623b40e26bb230df913f0da18a8d1ccf42ea 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -46,3 +46,4 @@
-Q _build/default/examples/proofs/tests refinedc.examples.tests
-Q _build/default/linux/proofs/page_alloc refinedc.linux.page_alloc
-Q _build/default/linux/pkvm/proofs/spinlock refinedc.linux.pkvm.spinlock
+-Q _build/default/linux/pkvm/proofs/early_alloc refinedc.linux.pkvm.early_alloc
diff --git a/linux/pkvm/early_alloc.c b/linux/pkvm/early_alloc.c
new file mode 100644
index 0000000000000000000000000000000000000000..77d5c45fbf2ae3f5cc34c2366c0c66efbcce3542
--- /dev/null
+++ b/linux/pkvm/early_alloc.c
@@ -0,0 +1,101 @@
+// SPDX-License-Identifier: GPL-2.0-only
+/*
+ * Copyright (C) 2020 Google LLC
+ * Author: Quentin Perret <qperret@google.com>
+ */
+
+#include <asm/page-def.h>
+#include <stddef.h>
+#include <stdint.h>
+#include <refinedc.h>
+
+//@rc::import instances from refinedc.linux.pkvm.early_alloc (for proofs only)
+
+struct
+[[rc::refined_by("base : loc", "given : nat", "remaining : nat")]]
+[[rc::let("z_cur : Z = {(base.2 + given * PAGE_SIZE)%Z}")]]
+[[rc::let("z_end : Z = {(base.2 + (given + remaining) * PAGE_SIZE)%Z}")]]
+region {
+ [[rc::field("own_constrained<nonshr_constraint<"
+ "{(base.1, z_cur) â—â‚— uninit (PAGES 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;
+};
+
+static struct region mem;
+
+#define base (mem.base)
+#define end (mem.end)
+#define cur (mem.cur)
+
+[[rc::parameters("base : loc", "given : nat", "remaining : nat")]]
+[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
+[[rc::returns("given @ int<size_t>")]]
+[[rc::ensures("global mem : {(base, given, remaining)} @ region")]]
+[[rc::trust_me]] // FIXME
+size_t hyp_early_alloc_nr_pages(void){
+ return (cur - (uintptr_t) base) >> PAGE_SHIFT;
+}
+
+[[rc::parameters("p : loc")]]
+[[rc::args("p @ &own<uninit<PAGE>>")]]
+[[rc::ensures("own p : zeroed<PAGE>")]]
+extern void clear_page(void *to);
+
+[[rc::parameters("base : loc", "given : nat", "remaining : nat", "n : nat")]]
+[[rc::args("n @ int<u32>")]]
+[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
+[[rc::returns("{0%nat < n ≤ remaining} @ optional<&own<uninit<PAGES<n>>>>")]]
+[[rc::ensures("global mem : {if bool_decide (0%nat < n ≤ remaining) then "
+ "(base, given + n, remaining - n)%nat else "
+ "(base, given, remaining)} @ region")]]
+[[rc::trust_me]] // FIXME
+void *hyp_early_alloc_contig(unsigned int nr_pages){
+ uintptr_t ret = cur, p;
+ unsigned int i;
+
+ if (!nr_pages)
+ return NULL;
+
+ cur += nr_pages << PAGE_SHIFT;
+ if (cur > end) {
+ cur = ret;
+ return NULL;
+ }
+
+ // FIXME change spec with zeroed.
+ //for (i = 0; i < nr_pages; i++) {
+ // p = ret + (i << PAGE_SHIFT);
+ // clear_page((void *)(p));
+ //}
+
+ return rc_copy_alloc_id((void *) ret, base);
+}
+
+//[[rc::parameters("n : nat")]]
+//[[rc::args("uninit<void*>")]]
+//[[rc::requires("global mem : n @ region")]]
+//[[rc::returns("{n ≠0%nat} @ optional<&own<uninit<PAGE>>>")]]
+//[[rc::ensures("global mem : {if bool_decide (n ≠0%nat) then (n - 1)%nat else n} @ region")]]
+[[rc::parameters("base : loc", "given : nat", "remaining : nat")]]
+[[rc::args("uninit<void*>")]]
+[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
+[[rc::returns("{remaining ≠0%nat} @ optional<&own<uninit<PAGE>>>")]]
+[[rc::ensures("global mem : {if bool_decide (remaining ≠0%nat) then "
+ "(base, given + 1, remaining - 1)%nat else "
+ "(base, given, remaining)} @ 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::requires("{s = (n * PAGE_SIZE)%Z}")]]
+[[rc::requires("global mem : uninit<struct_region>")]]
+[[rc::ensures("global mem : {(l, 0%nat, n)} @ region")]]
+void hyp_early_alloc_init(unsigned char* virt, unsigned int size){
+ base = virt;
+ end = (uintptr_t) ((uintptr_t) virt + size);
+ cur = (uintptr_t) virt;
+}
diff --git a/linux/pkvm/include/asm/page-def.h b/linux/pkvm/include/asm/page-def.h
new file mode 100644
index 0000000000000000000000000000000000000000..d548ec35aa68d4b3ea36c9a8f24788b53a95485f
--- /dev/null
+++ b/linux/pkvm/include/asm/page-def.h
@@ -0,0 +1,24 @@
+/* SPDX-License-Identifier: GPL-2.0-only */
+/*
+ * Based on arch/arm/include/asm/page.h
+ *
+ * Copyright (C) 1995-2003 Russell King
+ * Copyright (C) 2017 ARM Ltd.
+ */
+#ifndef __ASM_PAGE_DEF_H
+#define __ASM_PAGE_DEF_H
+
+#define PAGE_SHIFT 12
+#define PAGE_SIZE 4096
+#define PAGE_MASK (~(PAGE_SIZE-1))
+
+//@rc::inlined
+//@Definition PAGE_SIZE := (4096).
+//@
+//@Definition PAGES (n : nat) : layout :=
+//@ ly_with_align (n * Z.to_nat PAGE_SIZE) (Z.to_nat PAGE_SIZE).
+//@
+//@Notation PAGE := (PAGES 1).
+//@rc::end
+
+#endif /* __ASM_PAGE_DEF_H */
diff --git a/linux/pkvm/proofs/early_alloc/dune b/linux/pkvm/proofs/early_alloc/dune
new file mode 100644
index 0000000000000000000000000000000000000000..f710fd6a72ea2f3855c401b5fa597be96946861d
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/dune
@@ -0,0 +1,5 @@
+; Generated by [refinedc], do not edit.
+(coq.theory
+ (flags -w -notation-overridden -w -redundant-canonical-projection)
+ (name refinedc.linux.pkvm.early_alloc)
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
diff --git a/linux/pkvm/proofs/early_alloc/generated_code.v b/linux/pkvm/proofs/early_alloc/generated_code.v
new file mode 100644
index 0000000000000000000000000000000000000000..4f4f6cdde543a359a21df09fb499af54c11496e4
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/generated_code.v
@@ -0,0 +1,220 @@
+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+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 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 89 2 89 35.
+ Definition loc_68 : location_info := LocationInfo file_0 89 9 89 34.
+ Definition loc_69 : location_info := LocationInfo file_0 89 9 89 31.
+ Definition loc_70 : location_info := LocationInfo file_0 89 9 89 31.
+ Definition loc_71 : location_info := LocationInfo file_0 89 32 89 33.
+ Definition loc_74 : location_info := LocationInfo file_0 98 2 98 20.
+ Definition loc_75 : location_info := LocationInfo file_0 99 2 99 52.
+ Definition loc_76 : location_info := LocationInfo file_0 100 2 100 31.
+ Definition loc_77 : location_info := LocationInfo file_0 100 2 100 11.
+ Definition loc_78 : location_info := LocationInfo file_0 100 3 100 6.
+ Definition loc_79 : location_info := LocationInfo file_0 100 14 100 30.
+ Definition loc_80 : location_info := LocationInfo file_0 100 26 100 30.
+ Definition loc_81 : location_info := LocationInfo file_0 100 26 100 30.
+ Definition loc_82 : location_info := LocationInfo file_0 99 2 99 11.
+ Definition loc_83 : location_info := LocationInfo file_0 99 3 99 6.
+ Definition loc_84 : location_info := LocationInfo file_0 99 14 99 51.
+ Definition loc_85 : location_info := LocationInfo file_0 99 26 99 51.
+ Definition loc_86 : location_info := LocationInfo file_0 99 27 99 43.
+ Definition loc_87 : location_info := LocationInfo file_0 99 39 99 43.
+ Definition loc_88 : location_info := LocationInfo file_0 99 39 99 43.
+ Definition loc_89 : location_info := LocationInfo file_0 99 46 99 50.
+ Definition loc_90 : location_info := LocationInfo file_0 99 46 99 50.
+ Definition loc_91 : location_info := LocationInfo file_0 98 2 98 12.
+ Definition loc_92 : location_info := LocationInfo file_0 98 3 98 6.
+ Definition loc_93 : location_info := LocationInfo file_0 98 15 98 19.
+ Definition loc_94 : location_info := LocationInfo file_0 98 15 98 19.
+
+ (* Definition of struct [region]. *)
+ Program Definition struct_region := {|
+ sl_members := [
+ (Some "base", void*);
+ (Some "end", it_layout size_t);
+ (Some "cur", it_layout size_t)
+ ];
+ |}.
+ Solve Obligations with solve_struct_obligations.
+
+ (* Definition of function [hyp_early_alloc_nr_pages]. *)
+ Definition impl_hyp_early_alloc_nr_pages (global_mem : loc): function := {|
+ f_args := [
+ ];
+ f_local_vars := [
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ locinfo: loc_2 ;
+ Return (LocInfoE loc_3 ((LocInfoE loc_4 ((LocInfoE loc_5 (use{it_layout size_t} (LocInfoE loc_6 ((LocInfoE loc_7 (global_mem)) at{struct_region} "cur")))) -{IntOp size_t, IntOp size_t} (LocInfoE loc_8 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_9 (use{void*} (LocInfoE loc_10 ((LocInfoE loc_11 (global_mem)) at{struct_region} "base")))))))) >>{IntOp size_t, IntOp size_t} (LocInfoE loc_12 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_12 (i2v 12 i32))))))
+ ]> $∅
+ )%E
+ |}.
+
+ (* Definition of function [hyp_early_alloc_contig]. *)
+ Definition impl_hyp_early_alloc_contig (global_mem : loc): function := {|
+ f_args := [
+ ("nr_pages", it_layout u32)
+ ];
+ f_local_vars := [
+ ("i", it_layout u32);
+ ("ret", it_layout size_t);
+ ("p", it_layout size_t)
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ "ret" <-{ it_layout size_t }
+ LocInfoE loc_60 (use{it_layout size_t} (LocInfoE loc_61 ((LocInfoE loc_62 (global_mem)) at{struct_region} "cur"))) ;
+ locinfo: loc_56 ;
+ if: LocInfoE loc_56 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_56 ((UnOp (CastOp $ IntOp u32) (IntOp i32) (i2v 0 i32)) ={IntOp u32, IntOp u32} (LocInfoE loc_58 (use{it_layout u32} (LocInfoE loc_59 ("nr_pages")))))))
+ then
+ locinfo: loc_53 ;
+ Goto "#5"
+ else
+ locinfo: loc_17 ;
+ Goto "#6"
+ ]> $
+ <[ "#1" :=
+ locinfo: loc_17 ;
+ LocInfoE loc_43 ((LocInfoE loc_44 (global_mem)) at{struct_region} "cur") <-{ it_layout size_t }
+ LocInfoE loc_45 ((LocInfoE loc_46 (use{it_layout size_t} (LocInfoE loc_47 ((LocInfoE loc_48 (global_mem)) at{struct_region} "cur")))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_49 (UnOp (CastOp $ IntOp size_t) (IntOp u32) (LocInfoE loc_49 ((LocInfoE loc_50 (use{it_layout u32} (LocInfoE loc_51 ("nr_pages")))) <<{IntOp u32, IntOp u32} (LocInfoE loc_52 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_52 (i2v 12 i32))))))))) ;
+ locinfo: loc_36 ;
+ if: LocInfoE loc_36 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_36 ((LocInfoE loc_37 (use{it_layout size_t} (LocInfoE loc_38 ((LocInfoE loc_39 (global_mem)) at{struct_region} "cur")))) >{IntOp size_t, IntOp size_t} (LocInfoE loc_40 (use{it_layout size_t} (LocInfoE loc_41 ((LocInfoE loc_42 (global_mem)) at{struct_region} "end")))))))
+ then
+ locinfo: loc_28 ;
+ Goto "#3"
+ else
+ locinfo: loc_19 ;
+ Goto "#4"
+ ]> $
+ <[ "#2" :=
+ locinfo: loc_19 ;
+ Return (LocInfoE loc_20 (CopyAllocId (LocInfoE loc_24 (UnOp (CastOp $ PtrOp) (IntOp size_t) (LocInfoE loc_25 (use{it_layout size_t} (LocInfoE loc_26 ("ret")))))) (LocInfoE loc_21 (use{void*} (LocInfoE loc_22 ((LocInfoE loc_23 (global_mem)) at{struct_region} "base"))))))
+ ]> $
+ <[ "#3" :=
+ locinfo: loc_28 ;
+ LocInfoE loc_31 ((LocInfoE loc_32 (global_mem)) at{struct_region} "cur") <-{ it_layout size_t }
+ LocInfoE loc_33 (use{it_layout size_t} (LocInfoE loc_34 ("ret"))) ;
+ locinfo: loc_29 ;
+ Return (LocInfoE loc_30 (NULL))
+ ]> $
+ <[ "#4" :=
+ locinfo: loc_19 ;
+ Goto "#2"
+ ]> $
+ <[ "#5" :=
+ locinfo: loc_53 ;
+ Return (LocInfoE loc_54 (NULL))
+ ]> $
+ <[ "#6" :=
+ locinfo: loc_17 ;
+ Goto "#1"
+ ]> $∅
+ )%E
+ |}.
+
+ (* Definition of function [hyp_early_alloc_page]. *)
+ Definition impl_hyp_early_alloc_page (global_hyp_early_alloc_contig : loc): function := {|
+ f_args := [
+ ("arg", void*)
+ ];
+ f_local_vars := [
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ locinfo: loc_67 ;
+ Return (LocInfoE loc_68 (Call (LocInfoE loc_70 (global_hyp_early_alloc_contig)) [@{expr} LocInfoE loc_71 (UnOp (CastOp $ IntOp u32) (IntOp i32) (LocInfoE loc_71 (i2v 1 i32))) ]))
+ ]> $∅
+ )%E
+ |}.
+
+ (* Definition of function [hyp_early_alloc_init]. *)
+ Definition impl_hyp_early_alloc_init (global_mem : loc): function := {|
+ f_args := [
+ ("virt", void*);
+ ("size", it_layout u32)
+ ];
+ f_local_vars := [
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ locinfo: loc_74 ;
+ LocInfoE loc_91 ((LocInfoE loc_92 (global_mem)) at{struct_region} "base") <-{ void* }
+ LocInfoE loc_93 (use{void*} (LocInfoE loc_94 ("virt"))) ;
+ locinfo: loc_75 ;
+ LocInfoE loc_82 ((LocInfoE loc_83 (global_mem)) at{struct_region} "end") <-{ it_layout size_t }
+ LocInfoE loc_84 (UnOp (CastOp $ IntOp size_t) (IntOp size_t) (LocInfoE loc_85 ((LocInfoE loc_86 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_87 (use{void*} (LocInfoE loc_88 ("virt")))))) +{IntOp size_t, IntOp size_t} (LocInfoE loc_89 (UnOp (CastOp $ IntOp size_t) (IntOp u32) (LocInfoE loc_89 (use{it_layout u32} (LocInfoE loc_90 ("size"))))))))) ;
+ locinfo: loc_76 ;
+ LocInfoE loc_77 ((LocInfoE loc_78 (global_mem)) at{struct_region} "cur") <-{ it_layout size_t }
+ LocInfoE loc_79 (UnOp (CastOp $ IntOp size_t) (PtrOp) (LocInfoE loc_80 (use{void*} (LocInfoE loc_81 ("virt"))))) ;
+ Return (VOID)
+ ]> $∅
+ )%E
+ |}.
+End code.
diff --git 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
new file mode 100644
index 0000000000000000000000000000000000000000..2cdc798bf3d07ebf3a8f460e9d2d8baac9986235
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_contig.v
@@ -0,0 +1 @@
+(* Let's skip that, you seem to have some faith. *)
diff --git a/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v
new file mode 100644
index 0000000000000000000000000000000000000000..dad59485f96a291acaf7ac7756e18589ce1e4abf
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v
@@ -0,0 +1,28 @@
+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_init.
+ Context `{!typeG Σ} `{!globalG Σ}.
+
+ (* Typing proof for [hyp_early_alloc_init]. *)
+ Lemma type_hyp_early_alloc_init (global_mem : loc) :
+ global_locs !! "mem" = Some global_mem →
+ ⊢ typed_function (impl_hyp_early_alloc_init global_mem) type_of_hyp_early_alloc_init.
+ Proof.
+ Open Scope printing_sugar.
+ start_function "hyp_early_alloc_init" ([[l n] s]) => arg_virt arg_size.
+ split_blocks ((
+ ∅
+ )%I : gmap label (iProp Σ)) ((
+ ∅
+ )%I : gmap label (iProp Σ)).
+ - 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: print_sidecondition_goal "hyp_early_alloc_init".
+ Qed.
+End proof_hyp_early_alloc_init.
diff --git a/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v.bk b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v.bk
new file mode 100644
index 0000000000000000000000000000000000000000..6d7bfb4ca994b9a1795218c456ff9839ec88a9ba
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v.bk
@@ -0,0 +1,32 @@
+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.
+Set Default Proof Using "Type".
+
+(* Generated from [linux/pkvm/early_alloc.c]. *)
+Section proof_hyp_early_alloc_init.
+ Context `{!typeG Σ} `{!globalG Σ}.
+
+ (* Typing proof for [hyp_early_alloc_init]. *)
+ Lemma type_hyp_early_alloc_init (global_mem : loc) :
+ global_locs !! "mem" = Some global_mem →
+ ⊢ typed_function (impl_hyp_early_alloc_init global_mem) type_of_hyp_early_alloc_init.
+ Proof.
+ Open Scope printing_sugar.
+ start_function "hyp_early_alloc_init" ([[l n] s]) => arg_virt arg_size.
+ split_blocks ((
+ ∅
+ )%I : gmap label (iProp Σ)) ((
+ ∅
+ )%I : gmap label (iProp Σ)).
+ - repeat liRStep; liShow.
+ liInst Hevar0 l.2. assert ((l.1, l.2) = l) as -> by by destruct l.
+ 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.
+ + by etransitivity.
+ + transitivity max_alloc_end; last done.
+ rewrite /ly_size /= in H1. lia.
+ all: print_sidecondition_goal "hyp_early_alloc_init".
+ Qed.
+End proof_hyp_early_alloc_init.
diff --git a/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_nr_pages.v b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_nr_pages.v
new file mode 100644
index 0000000000000000000000000000000000000000..2cdc798bf3d07ebf3a8f460e9d2d8baac9986235
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_nr_pages.v
@@ -0,0 +1 @@
+(* Let's skip that, you seem to have some faith. *)
diff --git a/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_page.v b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_page.v
new file mode 100644
index 0000000000000000000000000000000000000000..9c2fe03c1e10161b4795af7a428831226b20bcaf
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_page.v
@@ -0,0 +1,28 @@
+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_page.
+ Context `{!typeG Σ} `{!globalG Σ}.
+
+ (* Typing proof for [hyp_early_alloc_page]. *)
+ Lemma type_hyp_early_alloc_page (global_hyp_early_alloc_contig : loc) :
+ global_hyp_early_alloc_contig â—áµ¥ global_hyp_early_alloc_contig @ function_ptr type_of_hyp_early_alloc_contig -∗
+ typed_function (impl_hyp_early_alloc_page global_hyp_early_alloc_contig) type_of_hyp_early_alloc_page.
+ Proof.
+ Open Scope printing_sugar.
+ start_function "hyp_early_alloc_page" ([[base given] remaining]) => arg_arg.
+ split_blocks ((
+ ∅
+ )%I : gmap label (iProp Σ)) ((
+ ∅
+ )%I : gmap label (iProp Σ)).
+ - repeat liRStep; liShow.
+ all: print_typesystem_goal "hyp_early_alloc_page" "#0".
+ Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+ all: print_sidecondition_goal "hyp_early_alloc_page".
+ Qed.
+End proof_hyp_early_alloc_page.
diff --git a/linux/pkvm/proofs/early_alloc/generated_spec.v b/linux/pkvm/proofs/early_alloc/generated_spec.v
new file mode 100644
index 0000000000000000000000000000000000000000..34dff12bb93594c03fe9aad0d38230968d1ee6ed
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/generated_spec.v
@@ -0,0 +1,105 @@
+From refinedc.typing Require Import typing.
+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. *)
+
+ Definition PAGE_SIZE := (4096).
+
+ Definition PAGES (n : nat) : layout :=
+ ly_with_align (n * Z.to_nat PAGE_SIZE) (Z.to_nat PAGE_SIZE).
+
+ Notation PAGE := (PAGES 1).
+
+ (* Definition of type [region]. *)
+ Definition region_rec : (loc * nat * nat -d> typeO) → (loc * nat * nat -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))) ;
+ (z_end @ (int (uintptr_t))) ;
+ (z_cur @ (int (uintptr_t)))
+ ]
+ )%I.
+ Typeclasses Opaque region_rec.
+
+ Global Instance region_rec_ne : Contractive region_rec.
+ Proof. solve_type_proper. Qed.
+
+ Definition region : rtype := {|
+ rty_type := loc * nat * nat;
+ rty r__ := fixp region_rec r__
+ |}.
+
+ Lemma region_unfold (patt__ : loc * nat * nat):
+ (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))) ;
+ (z_end @ (int (uintptr_t))) ;
+ (z_cur @ (int (uintptr_t)))
+ ]
+ )%I.
+ Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
+
+
+ Global Program Instance region_rmovable : RMovable region :=
+ {| rmovable patt__ := movable_eq _ _ (region_unfold patt__) |}.
+ Next Obligation. solve_ty_layout_eq. Qed.
+
+ Global Instance region_simplify_hyp_place_inst l_ β_ patt__:
+ SimplifyHypPlace l_ β_ (patt__ @ region)%I (Some 100%N) :=
+ λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (region_unfold _)).
+ Global Instance region_simplify_goal_place_inst l_ β_ patt__:
+ SimplifyGoalPlace l_ β_ (patt__ @ region)%I (Some 100%N) :=
+ λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (region_unfold _)).
+
+ Global Program Instance region_simplify_hyp_val_inst v_ patt__:
+ SimplifyHypVal v_ (patt__ @ region)%I (Some 100%N) :=
+ λ T, i2p (simplify_hyp_val_eq v_ _ _ (region_unfold _) T _).
+ Next Obligation. done. Qed.
+ Global Program Instance region_simplify_goal_val_inst v_ patt__:
+ SimplifyGoalVal v_ (patt__ @ region)%I (Some 100%N) :=
+ λ T, i2p (simplify_goal_val_eq v_ _ _ (region_unfold _) T _).
+ Next Obligation. done. Qed.
+
+ (* Type definitions. *)
+
+ (* 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))))
+ → ∃ () : (), (given @ (int (size_t))); (global_with_type "mem" Own (((base, given, remaining)) @ (region))).
+
+ (* Specifications for function [clear_page]. *)
+ Definition type_of_clear_page :=
+ fn(∀ p : loc; (p @ (&own (uninit (PAGE)))); True)
+ → ∃ () : (), (void); (p â—â‚— (zeroed (PAGE))).
+
+ (* 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) @ (optional (&own (uninit (PAGES (n)))) null)); (global_with_type "mem" Own ((if bool_decide (0%nat < n ≤ remaining) then (base, given + n, remaining - n)%nat else (base, given, remaining)) @ (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) @ (optional (&own (uninit (PAGE))) null)); (global_with_type "mem" Own ((if bool_decide (remaining ≠0%nat) then (base, given + 1, remaining - 1)%nat else (base, given, remaining)) @ (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))).
+End spec.
+
+Typeclasses Opaque region_rec.
diff --git a/linux/pkvm/proofs/early_alloc/instances.v b/linux/pkvm/proofs/early_alloc/instances.v
new file mode 100644
index 0000000000000000000000000000000000000000..c048cf5a8e4e801efc764f098924df52da207699
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/instances.v
@@ -0,0 +1,27 @@
+From refinedc.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section instances.
+ Context `{!typeG Σ}.
+
+ 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.
+ Global Instance simplify_goal_place_shift_loc_0nat_times_inst l n β ty:
+ SimplifyGoalPlace (l +ₗ 0%nat * n) β ty (Some 0%N) :=
+ λ T, i2p (simplify_goal_place_shift_loc_0nat_times l n β ty T).
+
+ Lemma simplify_goal_place_combine l β ty T:
+ T (l â—â‚—{β} ty) -∗ simplify_goal ((l.1, l.2) â—â‚—{β} ty) T.
+ Proof. iIntros "HT". assert ((l.1, l.2) = l) as -> by by destruct l. iExists _. eauto with iFrame. Qed.
+ Global Instance simplify_goal_place_combine_inst l β ty:
+ SimplifyGoalPlace (l.1, l.2) β ty (Some 0%N) :=
+ λ T, i2p (simplify_goal_place_combine l β ty T).
+
+ Lemma simplify_goal_place_combine_offset l β n ty T:
+ T ((l +â‚— n) â—â‚—{β} ty) -∗ simplify_goal ((l.1, l.2 + n) â—â‚—{β} ty) T.
+ Proof. iIntros "HT". iExists _. eauto with iFrame. Qed.
+ Global Instance simplify_goal_place_combine_offset_inst l β n ty:
+ SimplifyGoalPlace (l.1, l.2 + n) β ty (Some 0%N) | 100 :=
+ λ T, i2p (simplify_goal_place_combine_offset l β n ty T).
+End instances.
diff --git a/linux/pkvm/proofs/early_alloc/proof_files b/linux/pkvm/proofs/early_alloc/proof_files
new file mode 100644
index 0000000000000000000000000000000000000000..0e4d13ab1148f010aaa6c64fdd82cdb21066728f
--- /dev/null
+++ b/linux/pkvm/proofs/early_alloc/proof_files
@@ -0,0 +1,5 @@
+generated_proof_clear_page.v
+generated_proof_hyp_early_alloc_contig.v
+generated_proof_hyp_early_alloc_init.v
+generated_proof_hyp_early_alloc_nr_pages.v
+generated_proof_hyp_early_alloc_page.v