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

Start verifying a new version of [early_alloc.c].

parent 2e18054e
No related branches found
No related tags found
No related merge requests found
Pipeline #41377 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 578 additions and 0 deletions
_CoqProject
+ 1
− 0
View file @ 42414135
......@@ -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
linux/pkvm/early_alloc.c 0 → 100644
+ 101
− 0
View file @ 42414135
// 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;
}
linux/pkvm/include/asm/page-def.h 0 → 100644
+ 24
− 0
View file @ 42414135
/* 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 */
linux/pkvm/proofs/early_alloc/dune 0 → 100644
+ 5
− 0
View file @ 42414135
; 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))
linux/pkvm/proofs/early_alloc/generated_code.v 0 → 100644
+ 220
− 0
View file @ 42414135
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.
linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_contig.v 0 → 100644
+ 1
− 0
View file @ 42414135
(* Let's skip that, you seem to have some faith. *)
linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v 0 → 100644
+ 28
− 0
View file @ 42414135
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.
linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_init.v.bk 0 → 100644
+ 32
− 0
View file @ 42414135
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.
linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_nr_pages.v 0 → 100644
+ 1
− 0
View file @ 42414135
(* Let's skip that, you seem to have some faith. *)
linux/pkvm/proofs/early_alloc/generated_proof_hyp_early_alloc_page.v 0 → 100644
+ 28
− 0
View file @ 42414135
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.
linux/pkvm/proofs/early_alloc/generated_spec.v 0 → 100644
+ 105
− 0
View file @ 42414135
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.
linux/pkvm/proofs/early_alloc/instances.v 0 → 100644
+ 27
− 0
View file @ 42414135
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.
linux/pkvm/proofs/early_alloc/proof_files 0 → 100644
+ 5
− 0
View file @ 42414135
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
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