added forgotten file

linux/.editorconfig

+[*.c]
+indent_style = tab
+indent_size = tab
+tab_size = 4

linux/early_alloc.c

@@ -43,7 +43,7 @@ void hyp_early_alloc_init(unsigned long virt, unsigned long size)
 	_end = virt + size;
 	cur = virt;
 
-  /* hyp_early_alloc_mm_ops.zalloc_page = hyp_early_alloc_page; */
+	/* hyp_early_alloc_mm_ops.zalloc_page = hyp_early_alloc_page; */
 	/* hyp_early_alloc_mm_ops.phys_to_virt = hyp_phys_to_virt; */
 	/* hyp_early_alloc_mm_ops.virt_to_phys = hyp_virt_to_phys; */
 }
@@ -72,9 +72,9 @@ static unsigned char * cur1;
 [[rc::ensures("[global_with_type \"cur1\" Own (&own (uninit (ly_set_size PAGE_LAYOUT m)))]")]]
 void * hyp_early_alloc_page1(void *arg)
 {
-  if (size1 <= (unsigned long) PAGE_SIZE) {
-    return NULL;
-  }
+	if (size1 <= (unsigned long) PAGE_SIZE) {
+		return NULL;
+	}
 
 	unsigned char *ret = cur1;
 	cur1 += PAGE_SIZE;
@@ -98,7 +98,7 @@ void hyp_early_alloc_init1(unsigned char *virt, unsigned long size)
 	size1 = size;
 	cur1 = virt;
 
-  /* hyp_early_alloc_mm_ops.zalloc_page = hyp_early_alloc_page; */
+	/* hyp_early_alloc_mm_ops.zalloc_page = hyp_early_alloc_page; */
 	/* hyp_early_alloc_mm_ops.phys_to_virt = hyp_phys_to_virt; */
 	/* hyp_early_alloc_mm_ops.virt_to_phys = hyp_virt_to_phys; */
 }

theories/typing/zeroed.v

+From refinedc.typing Require Export type.
+From refinedc.typing Require Import programs.
+Set Default Proof Using "Type".
+
+Section zeroed.
+  Context `{!typeG Σ}.
+
+  Program Definition zeroed (ly : layout) : type := {|
+    ty_own β l := (⌜l `has_layout_loc` ly⌝ ∗ l ↦[β] zero_val ly.(ly_size))%I;
+  |}.
+  Next Obligation. iIntros (????) "[% ?]". iSplitR => //. by iApply heap_mapsto_own_state_share. Qed.
+
+  Global Program Instance movable_zeroed ly : Movable (zeroed ly) := {|
+    ty_layout := ly;
+    ty_own_val v := ⌜v = zero_val ly.(ly_size)⌝%I;
+  |}.
+  Next Obligation. iIntros (ly l). by iDestruct 1 as (?) "?". Qed.
+  Next Obligation. iIntros (ly v ->). by rewrite /has_layout_val replicate_length. Qed.
+  Next Obligation. iIntros (ly l) "[% Hl]". eauto with iFrame. Qed.
+  Next Obligation. iIntros (ly l v ?) "Hl ->". by iFrame. Qed.
+
+  Lemma zeroed_loc_in_bounds l β ly :
+    l ◁ₗ{β} zeroed ly -∗ loc_in_bounds l (ly_size ly).
+  Proof.
+    iIntros "[% Hl]". iDestruct (heap_mapsto_own_state_loc_in_bounds with "Hl") as "Hl".
+    by rewrite replicate_length.
+  Qed.
+
+  Global Instance loc_in_bounds_zeroed ly β: LocInBounds (zeroed ly) β.
+  Proof.
+    constructor. iIntros (l) "Hl".
+    iDestruct (zeroed_loc_in_bounds with "Hl") as "#Hb".
+    iApply loc_in_bounds_shorten; last done. lia.
+  Qed.
+End zeroed.