Commit e452bbeb authored by Michael Sammler's avatar Michael Sammler
Browse files

find buddy

parent cddada8b
Pipeline #49867 passed with stage
in 16 minutes and 46 seconds
......@@ -52,3 +52,4 @@
-Q _build/default/examples/proofs/quick_sort refinedc.examples.quick_sort
-Q _build/default/examples/proofs/tagged_ptr refinedc.examples.tagged_ptr
-Q _build/default/examples/proofs/ocaml_runtime refinedc.examples.ocaml_runtime
-Q _build/default/linux/casestudies/proofs/page_alloc_find_buddy refinedc.linux.casestudies.page_alloc_find_buddy
// SPDX-License-Identifier: GPL-2.0-only
/*
* Copyright (C) 2020 Google LLC
* Author: Quentin Perret <qperret@google.com>
*/
// #include <asm/kvm_hyp.h>
// #include <nvhe/gfp.h>
#include <stddef.h>
#include <stdint.h>
#include <stdbool.h>
#include <limits.h>
#include <refinedc.h>
//@rc::import page_alloc_def from refinedc.linux.casestudies.page_alloc_find_buddy
typedef unsigned long long u64;
typedef signed long long s64;
typedef u64 phys_addr_t;
typedef u64 gfp_t;
#define PAGE_SIZE 4096
#define PAGE_SHIFT 12
/* SPDX-License-Identifier: GPL-2.0-only */
#ifndef __KVM_HYP_MEMORY_H
#define __KVM_HYP_MEMORY_H
/* #include <asm/page.h> */
/* #include <linux/types.h> */
#define HYP_MEMBLOCK_REGIONS 128
struct [[rc::refined_by("refcount : Z", "order : Z")]]
hyp_page {
[[rc::field("refcount @ int<u16>")]]
unsigned short refcount;
[[rc::field("order @ int<u16>")]]
unsigned short order;
};
extern s64 hyp_physvirt_offset;
// TODO: frontend seems to get confused by having both [extern u64 x]
// and [u64 x] in the same file: rc::global does not seem to work anymore
// extern u64 __hyp_vmemmap;
[[rc::parameters("vmemmap : loc")]]
[[rc::global("vmemmap @ intptr<u64>")]]
u64 __hyp_vmemmap;
#define hyp_vmemmap ((struct hyp_page *)__hyp_vmemmap)
/* #define hyp_vmemmap ((struct hyp_page *)__hyp_vmemmap) */
#define __hyp_pa(virt) ((phys_addr_t)(virt) + hyp_physvirt_offset)
#define __hyp_va(phys) ((void *)((phys_addr_t)(phys) - hyp_physvirt_offset))
static inline void *hyp_phys_to_virt(phys_addr_t phys)
{
return __hyp_va(phys);
}
static inline phys_addr_t hyp_virt_to_phys(void *addr)
{
return __hyp_pa(addr);
}
#define hyp_phys_to_pfn(phys) ((phys) >> PAGE_SHIFT)
#define hyp_pfn_to_phys(pfn) ((phys_addr_t)((pfn) << PAGE_SHIFT))
/* #define hyp_phys_to_page(phys) (&hyp_vmemmap[hyp_phys_to_pfn(phys)]) */
#define hyp_phys_to_page(phys) (hyp_vmemmap + hyp_phys_to_pfn(phys))
#define hyp_virt_to_page(virt) hyp_phys_to_page(__hyp_pa(virt))
#define hyp_virt_to_pfn(virt) hyp_phys_to_pfn(__hyp_pa(virt))
#define hyp_page_to_pfn(page) ((struct hyp_page *)(page) - hyp_vmemmap)
#define hyp_page_to_phys(page) hyp_pfn_to_phys((hyp_page_to_pfn(page)))
#define hyp_page_to_virt(page) __hyp_va(hyp_page_to_phys(page))
#define hyp_page_to_pool(page) (((struct hyp_page *)page)->pool)
#endif /* __KVM_HYP_MEMORY_H */
/* SPDX-License-Identifier: GPL-2.0-only */
#ifndef __KVM_HYP_GFP_H
#define __KVM_HYP_GFP_H
/* #include <linux/list.h> */
/* #include <nvhe/memory.h> */
/* #include <nvhe/spinlock.h> */
#define HYP_MAX_ORDER 11U
//@rc::inlined Definition HYP_MAX_ORDER : nat := Z.to_nat 11.
#define HYP_NO_ORDER UINT_MAX
//@rc::inlined Definition HYP_NO_ORDER : Z := max_int u32.
struct [[rc::refined_by("pages : {list (Z * Z)}",
"npages : nat",
"vmemmap : loc",
"range_start_idx : Z",
"max_order : Z")]]
[[rc::exists("range_start : Z", "range_end : Z")]]
[[rc::constraints("[initialized \"__hyp_vmemmap\" vmemmap]")]]
[[rc::constraints("{(length pages =@{Z} range_start_idx + npages)%Z}")]]
[[rc::constraints("{(range_start = range_start_idx ≪ PAGE_SHIFT)%Z}")]]
[[rc::constraints("{(range_end = range_start + npages ≪ PAGE_SHIFT)%Z}")]]
[[rc::constraints("{(0 <= range_start_idx)%Z}")]]
hyp_pool {
/* hyp_spinlock_t lock; */
/* struct list_head free_area[HYP_MAX_ORDER + 1]; */
[[rc::field("own_constrained<nonshr_constraint<{vmemmap ◁ₗ !{ array<struct_hyp_page, {pages `at_type` hyp_page}> } }>, range_start @ int<u64>>")]]
phys_addr_t range_start;
[[rc::field("range_end @ int<u64>")]]
phys_addr_t range_end;
[[rc::field("max_order @ int<u16>")]]
unsigned short max_order;
};
/* GFP flags */
#define HYP_GFP_NONE 0
#define HYP_GFP_ZERO 1
/* Allocation */
void *hyp_alloc_pages(struct hyp_pool *pool, gfp_t mask, unsigned int order);
void hyp_get_page(void *addr);
void hyp_put_page(void *addr);
/* Used pages cannot be freed */
int hyp_pool_init(struct hyp_pool *pool, phys_addr_t phys,
unsigned int nr_pages, unsigned int used_pages);
#endif /* __KVM_HYP_GFP_H */
//u64 __hyp_vmemmap;
/* [[rc::parameters("vmemmap : loc")]] */
/* [[rc::global("&own<place<vmemmap>>")]] */
/* void *__hyp_vmemmap; */
/*
* Example buddy-tree for a 4-pages physically contiguous pool:
*
* o : Page 3
* /
* o-o : Page 2
* /
* / o : Page 1
* / /
* o---o-o : Page 0
* Order 2 1 0
*
* Example of requests on this zon:
* __find_buddy(pool, page 0, order 0) => page 1
* __find_buddy(pool, page 0, order 1) => page 2
* __find_buddy(pool, page 1, order 0) => page 0
* __find_buddy(pool, page 2, order 0) => page 3
*/
[[rc::parameters("pool : loc", "pageloc : loc", "page : Z", "vmemmap : loc", "pages : {list (Z * Z)}", "npages : nat", "range_start_idx : Z", "order : Z", "max_order : Z")]]
[[rc::args("pool @ &own<{(pages, npages, vmemmap, range_start_idx, max_order)} @ hyp_pool>",
"pageloc @ &own<array_ptr<struct_hyp_page, vmemmap, page, {length pages}>>", "order @ int<u32>")]]
[[rc::requires("{0 <= page ≪ 12 <= max_int ptrdiff_t}", "{0 < length pages}", "{0 <= order <= HYP_MAX_ORDER}")]]
[[rc::returns("{range_start_idx <= find_buddy vmemmap order page < range_start_idx + npages} @ optional<&own<array_ptr<struct_hyp_page, vmemmap, {find_buddy vmemmap order page}, {length pages}>>, null>")]]
[[rc::ensures("own pool : {(pages, npages, vmemmap, range_start_idx, max_order)} @ hyp_pool")]]
[[rc::ensures("own pageloc : array_ptr<struct_hyp_page, vmemmap, page, {length pages}>")]]
[[rc::tactics("all: unfold find_buddy, PAGE_SHIFT, PAGE_SIZE in *.")]]
[[rc::tactics("all: repeat match goal with | H : _ = Lt |- _ => rewrite -/(Z.lt _ _) in H end.")]]
[[rc::tactics("all: try by etrans; [|done]; rewrite Z.shiftl_mul_pow2 //; lia.")]]
[[rc::tactics("all: try by rewrite Z.shiftl_mul_pow2 //; etrans; [ apply: Z.mul_le_mono_nonneg_l; [done| ]; apply: (Z.pow_le_mono_r _ _ 11) |].")]]
[[rc::tactics("all: try by move =>/find_buddy_result_eq; solve_goal.")]]
[[rc::tactics("all: try by apply: (find_buddy_result' page range_start_idx order npages); solve_goal.")]]
[[rc::tactics("all: try by apply/find_buddy_result_eq; solve_goal.")]]
static struct hyp_page *__find_buddy(struct hyp_pool *pool, struct hyp_page *p,
unsigned int order)
{
rc_unfold(pool->range_start);
phys_addr_t addr = hyp_page_to_phys(p);
addr ^= (PAGE_SIZE << order);
if (addr < pool->range_start || addr >= pool->range_end)
return NULL;
return hyp_phys_to_page(addr);
}
; Generated by [refinedc], do not edit.
(coq.theory
(flags -w -notation-overridden -w -redundant-canonical-projection)
(name refinedc.linux.casestudies.page_alloc_find_buddy)
(theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))
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/casestudies/page_alloc_find_buddy.c]. *)
Section code.
Definition file_0 : string := "linux/casestudies/page_alloc_find_buddy.c".
Definition loc_2 : location_info := LocationInfo file_0 59 1 59 62.
Definition loc_3 : location_info := LocationInfo file_0 59 8 59 61.
Definition loc_4 : location_info := LocationInfo file_0 59 17 59 60.
Definition loc_5 : location_info := LocationInfo file_0 59 18 59 37.
Definition loc_6 : location_info := LocationInfo file_0 59 31 59 37.
Definition loc_7 : location_info := LocationInfo file_0 59 31 59 37.
Definition loc_8 : location_info := LocationInfo file_0 59 40 59 59.
Definition loc_9 : location_info := LocationInfo file_0 59 40 59 59.
Definition loc_12 : location_info := LocationInfo file_0 64 1 64 52.
Definition loc_13 : location_info := LocationInfo file_0 64 8 64 51.
Definition loc_14 : location_info := LocationInfo file_0 64 9 64 28.
Definition loc_15 : location_info := LocationInfo file_0 64 22 64 28.
Definition loc_16 : location_info := LocationInfo file_0 64 22 64 28.
Definition loc_17 : location_info := LocationInfo file_0 64 31 64 50.
Definition loc_18 : location_info := LocationInfo file_0 64 31 64 50.
Definition loc_21 : location_info := LocationInfo file_0 171 1 171 22.
Definition loc_22 : location_info := LocationInfo file_0 171 22 171 2.
Definition loc_23 : location_info := LocationInfo file_0 172 1 172 109.
Definition loc_24 : location_info := LocationInfo file_0 174 1 174 25.
Definition loc_25 : location_info := LocationInfo file_0 175 1 176 24.
Definition loc_26 : location_info := LocationInfo file_0 178 1 178 62.
Definition loc_27 : location_info := LocationInfo file_0 178 8 178 61.
Definition loc_28 : location_info := LocationInfo file_0 178 9 178 43.
Definition loc_29 : location_info := LocationInfo file_0 178 29 178 42.
Definition loc_30 : location_info := LocationInfo file_0 178 29 178 42.
Definition loc_31 : location_info := LocationInfo file_0 178 46 178 60.
Definition loc_32 : location_info := LocationInfo file_0 178 47 178 53.
Definition loc_33 : location_info := LocationInfo file_0 178 47 178 53.
Definition loc_34 : location_info := LocationInfo file_0 178 57 178 59.
Definition loc_35 : location_info := LocationInfo file_0 176 2 176 24.
Definition loc_36 : location_info := LocationInfo file_0 176 9 176 23.
Definition loc_39 : location_info := LocationInfo file_0 175 5 175 29.
Definition loc_40 : location_info := LocationInfo file_0 175 5 175 9.
Definition loc_41 : location_info := LocationInfo file_0 175 5 175 9.
Definition loc_42 : location_info := LocationInfo file_0 175 12 175 29.
Definition loc_43 : location_info := LocationInfo file_0 175 12 175 29.
Definition loc_44 : location_info := LocationInfo file_0 175 12 175 16.
Definition loc_45 : location_info := LocationInfo file_0 175 12 175 16.
Definition loc_46 : location_info := LocationInfo file_0 175 33 175 56.
Definition loc_47 : location_info := LocationInfo file_0 175 33 175 37.
Definition loc_48 : location_info := LocationInfo file_0 175 33 175 37.
Definition loc_49 : location_info := LocationInfo file_0 175 41 175 56.
Definition loc_50 : location_info := LocationInfo file_0 175 41 175 56.
Definition loc_51 : location_info := LocationInfo file_0 175 41 175 45.
Definition loc_52 : location_info := LocationInfo file_0 175 41 175 45.
Definition loc_53 : location_info := LocationInfo file_0 174 1 174 5.
Definition loc_54 : location_info := LocationInfo file_0 174 1 174 24.
Definition loc_55 : location_info := LocationInfo file_0 174 1 174 5.
Definition loc_56 : location_info := LocationInfo file_0 174 1 174 5.
Definition loc_57 : location_info := LocationInfo file_0 174 9 174 24.
Definition loc_58 : location_info := LocationInfo file_0 174 10 174 14.
Definition loc_59 : location_info := LocationInfo file_0 174 18 174 23.
Definition loc_60 : location_info := LocationInfo file_0 174 18 174 23.
Definition loc_61 : location_info := LocationInfo file_0 172 20 172 108.
Definition loc_62 : location_info := LocationInfo file_0 172 34 172 107.
Definition loc_63 : location_info := LocationInfo file_0 172 35 172 100.
Definition loc_64 : location_info := LocationInfo file_0 172 38 172 60.
Definition loc_65 : location_info := LocationInfo file_0 172 57 172 60.
Definition loc_66 : location_info := LocationInfo file_0 172 57 172 60.
Definition loc_67 : location_info := LocationInfo file_0 172 63 172 97.
Definition loc_68 : location_info := LocationInfo file_0 172 83 172 96.
Definition loc_69 : location_info := LocationInfo file_0 172 83 172 96.
Definition loc_70 : location_info := LocationInfo file_0 172 104 172 106.
Definition loc_73 : location_info := LocationInfo file_0 171 1 171 21.
Definition loc_74 : location_info := LocationInfo file_0 171 2 171 21.
Definition loc_75 : location_info := LocationInfo file_0 171 3 171 7.
Definition loc_76 : location_info := LocationInfo file_0 171 3 171 7.
(* Definition of struct [hyp_page]. *)
Program Definition struct_hyp_page := {|
sl_members := [
(Some "refcount", it_layout u16);
(Some "order", it_layout u16)
];
|}.
Solve Obligations with solve_struct_obligations.
(* Definition of struct [hyp_pool]. *)
Program Definition struct_hyp_pool := {|
sl_members := [
(Some "range_start", it_layout u64);
(Some "range_end", it_layout u64);
(Some "max_order", it_layout u16);
(None, Layout 6%nat 0%nat)
];
|}.
Solve Obligations with solve_struct_obligations.
(* Definition of function [hyp_phys_to_virt]. *)
Definition impl_hyp_phys_to_virt (global_hyp_physvirt_offset : loc): function := {|
f_args := [
("phys", it_layout u64)
];
f_local_vars := [
];
f_init := "#0";
f_code := (
<[ "#0" :=
locinfo: loc_2 ;
Return (LocInfoE loc_3 (UnOp (CastOp $ PtrOp) (IntOp u64) (LocInfoE loc_4 ((LocInfoE loc_5 (UnOp (CastOp $ IntOp u64) (IntOp u64) (LocInfoE loc_6 (use{it_layout u64} (LocInfoE loc_7 ("phys")))))) -{IntOp u64, IntOp u64} (LocInfoE loc_8 (UnOp (CastOp $ IntOp u64) (IntOp i64) (LocInfoE loc_8 (use{it_layout i64} (LocInfoE loc_9 (global_hyp_physvirt_offset))))))))))
]> $
)%E
|}.
(* Definition of function [hyp_virt_to_phys]. *)
Definition impl_hyp_virt_to_phys (global_hyp_physvirt_offset : loc): function := {|
f_args := [
("addr", void*)
];
f_local_vars := [
];
f_init := "#0";
f_code := (
<[ "#0" :=
locinfo: loc_12 ;
Return (LocInfoE loc_13 ((LocInfoE loc_14 (UnOp (CastOp $ IntOp u64) (PtrOp) (LocInfoE loc_15 (use{void*} (LocInfoE loc_16 ("addr")))))) +{IntOp u64, IntOp u64} (LocInfoE loc_17 (UnOp (CastOp $ IntOp u64) (IntOp i64) (LocInfoE loc_17 (use{it_layout i64} (LocInfoE loc_18 (global_hyp_physvirt_offset))))))))
]> $
)%E
|}.
(* Definition of function [__find_buddy]. *)
Definition impl___find_buddy (global___hyp_vmemmap : loc): function := {|
f_args := [
("pool", void*);
("p", void*);
("order", it_layout u32)
];
f_local_vars := [
("addr", it_layout u64)
];
f_init := "#0";
f_code := (
<[ "#0" :=
locinfo: loc_21 ;
expr: (LocInfoE loc_73 (&(LocInfoE loc_74 ((LocInfoE loc_75 (!{void*} (LocInfoE loc_76 ("pool")))) at{struct_hyp_pool} "range_start")))) ;
"addr" <-{ it_layout u64 }
LocInfoE loc_61 (UnOp (CastOp $ IntOp u64) (IntOp ptrdiff_t) (LocInfoE loc_62 ((LocInfoE loc_63 ((LocInfoE loc_64 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_65 (use{void*} (LocInfoE loc_66 ("p")))))) sub_ptr{layout_of struct_hyp_page, PtrOp, PtrOp} (LocInfoE loc_67 (UnOp (CastOp $ PtrOp) (IntOp u64) (LocInfoE loc_68 (use{it_layout u64} (LocInfoE loc_69 (global___hyp_vmemmap)))))))) <<{IntOp ptrdiff_t, IntOp ptrdiff_t} (LocInfoE loc_70 (UnOp (CastOp $ IntOp ptrdiff_t) (IntOp i32) (LocInfoE loc_70 (i2v 12 i32))))))) ;
locinfo: loc_24 ;
LocInfoE loc_53 ("addr") <-{ it_layout u64 }
LocInfoE loc_54 ((LocInfoE loc_55 (use{it_layout u64} (LocInfoE loc_56 ("addr")))) ^{IntOp u64, IntOp u64} (LocInfoE loc_57 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_57 ((LocInfoE loc_58 (i2v 4096 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_59 (UnOp (CastOp $ IntOp i32) (IntOp u32) (LocInfoE loc_59 (use{it_layout u32} (LocInfoE loc_60 ("order"))))))))))) ;
locinfo: loc_39 ;
if: LocInfoE loc_39 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_39 ((LocInfoE loc_40 (use{it_layout u64} (LocInfoE loc_41 ("addr")))) <{IntOp u64, IntOp u64} (LocInfoE loc_42 (use{it_layout u64} (LocInfoE loc_43 ((LocInfoE loc_44 (!{void*} (LocInfoE loc_45 ("pool")))) at{struct_hyp_pool} "range_start")))))))
then
locinfo: loc_35 ;
Goto "#2"
else
Goto "#4"
]> $
<[ "#1" :=
locinfo: loc_26 ;
Return (LocInfoE loc_27 ((LocInfoE loc_28 (UnOp (CastOp $ PtrOp) (IntOp u64) (LocInfoE loc_29 (use{it_layout u64} (LocInfoE loc_30 (global___hyp_vmemmap)))))) at_offset{layout_of struct_hyp_page, PtrOp, IntOp u64} (LocInfoE loc_31 ((LocInfoE loc_32 (use{it_layout u64} (LocInfoE loc_33 ("addr")))) >>{IntOp u64, IntOp u64} (LocInfoE loc_34 (UnOp (CastOp $ IntOp u64) (IntOp i32) (LocInfoE loc_34 (i2v 12 i32))))))))
]> $
<[ "#2" :=
locinfo: loc_35 ;
Return (LocInfoE loc_36 (NULL))
]> $
<[ "#3" :=
locinfo: loc_26 ;
Goto "#1"
]> $
<[ "#4" :=
locinfo: loc_46 ;
if: LocInfoE loc_46 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_46 ((LocInfoE loc_47 (use{it_layout u64} (LocInfoE loc_48 ("addr")))) {IntOp u64, IntOp u64} (LocInfoE loc_49 (use{it_layout u64} (LocInfoE loc_50 ((LocInfoE loc_51 (!{void*} (LocInfoE loc_52 ("pool")))) at{struct_hyp_pool} "range_end")))))))
then
locinfo: loc_35 ;
Goto "#2"
else
locinfo: loc_26 ;
Goto "#3"
]> $
)%E
|}.
End code.
From refinedc.typing Require Import typing.
From refinedc.linux.casestudies.page_alloc_find_buddy Require Import generated_code.
From refinedc.linux.casestudies.page_alloc_find_buddy Require Import generated_spec.
From refinedc.linux.casestudies.page_alloc_find_buddy Require Import page_alloc_def.
Set Default Proof Using "Type".
(* Generated from [linux/casestudies/page_alloc_find_buddy.c]. *)
Section proof___find_buddy.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [__find_buddy]. *)
Lemma type___find_buddy (global___hyp_vmemmap : loc) :
global_locs !! "__hyp_vmemmap" = Some global___hyp_vmemmap
global_initialized_types !! "__hyp_vmemmap" = Some (GT loc (λ 'vmemmap, (vmemmap @ (intptr (u64))) : type)%I)
typed_function (impl___find_buddy global___hyp_vmemmap) type_of___find_buddy.
Proof.
Open Scope printing_sugar.
start_function "__find_buddy" ([[[[[[[[pool pageloc] page] vmemmap] pages] npages] range_start_idx] order] max_order]) => arg_pool arg_p arg_order local_addr.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "__find_buddy" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: unfold find_buddy, PAGE_SHIFT, PAGE_SIZE in *.
all: repeat match goal with | H : _ = Lt |- _ => rewrite -/(Z.lt _ _) in H end.
all: try by etrans; [|done]; rewrite Z.shiftl_mul_pow2 //; lia.
all: try by rewrite Z.shiftl_mul_pow2 //; etrans; [ apply: Z.mul_le_mono_nonneg_l; [done| ]; apply: (Z.pow_le_mono_r _ _ 11) |].
all: try by move =>/find_buddy_result_eq; solve_goal.
all: try by apply: (find_buddy_result' page range_start_idx order npages); solve_goal.
all: try by apply/find_buddy_result_eq; solve_goal.
all: print_sidecondition_goal "__find_buddy".
Qed.
End proof___find_buddy.
(* You were too lazy to even write a spec for this function. *)
(* You were too lazy to even write a spec for this function. *)
From refinedc.typing Require Import typing.
From refinedc.linux.casestudies.page_alloc_find_buddy Require Import generated_code.
From refinedc.linux.casestudies.page_alloc_find_buddy Require Import page_alloc_def.
Set Default Proof Using "Type".
(* Generated from [linux/casestudies/page_alloc_find_buddy.c]. *)
Section spec.
Context `{!typeG Σ} `{!globalG Σ}.
(* Inlined code. *)
Definition HYP_MAX_ORDER : nat := Z.to_nat 11.
Definition HYP_NO_ORDER : Z := max_int u32.
(* Definition of type [hyp_page]. *)
Definition hyp_page_rec : (Z * Z -d> typeO) (Z * Z -d> typeO) := (λ self patt__,
let refcount := patt__.1 in
let order := patt__.2 in
struct struct_hyp_page [@{type}
(refcount @ (int (u16))) ;
(order @ (int (u16)))
]
)%I.
Typeclasses Opaque hyp_page_rec.
Global Instance hyp_page_rec_ne : Contractive hyp_page_rec.
Proof. solve_type_proper. Qed.
Definition hyp_page : rtype := {|
rty_type := Z * Z;
rty r__ := fixp hyp_page_rec r__
|}.
Lemma hyp_page_unfold (patt__ : Z * Z):
(patt__ @ hyp_page)%I @{type} (
let refcount := patt__.1 in
let order := patt__.2 in
struct struct_hyp_page [@{type}
(refcount @ (int (u16))) ;
(order @ (int (u16)))
]
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
Global Program Instance hyp_page_rmovable : RMovable hyp_page :=
{| rmovable patt__ := movable_eq _ _ (hyp_page_unfold patt__) |}.
Next Obligation. solve_ty_layout_eq. Qed.
Global Instance hyp_page_simplify_hyp_place_inst_generated l_ β_ patt__:
SimplifyHypPlace l_ β_ (patt__ @ hyp_page)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_place_eq l_ β_ _ _ T (hyp_page_unfold _)).
Global Instance hyp_page_simplify_goal_place_inst_generated l_ β_ patt__:
SimplifyGoalPlace l_ β_ (patt__ @ hyp_page)%I (Some 100%N) :=
λ T, i2p (simplify_goal_place_eq l_ β_ _ _ T (hyp_page_unfold _)).
Global Program Instance hyp_page_simplify_hyp_val_inst_generated v_ patt__:
SimplifyHypVal v_ (patt__ @ hyp_page)%I (Some 100%N) :=
λ T, i2p (simplify_hyp_val_eq v_ _ _ (hyp_page_unfold _) T _).
Next Obligation. done. Qed.
Global Program Instance hyp_page_simplify_goal_val_inst_generated v_ patt__:
SimplifyGoalVal v_ (patt__ @ hyp_page)%I (Some 100%N) :=
λ T, i2p (simplify_goal_val_eq v_ _ _ (hyp_page_unfold _) T _).
Next Obligation. done. Qed.
(* Definition of type [hyp_pool]. *)
Definition hyp_pool_rec : ((list (Z * Z)) * nat * loc * Z * Z -d> typeO) ((list (Z * Z)) * nat * loc * Z * Z -d> typeO) := (λ self patt__,
let pages := patt__.1.1.1.1 in
let npages := patt__.1.1.1.2 in
let vmemmap := patt__.1.1.2 in
let range_start_idx := patt__.1.2 in
let max_order := patt__.2 in
tyexists (λ range_start : Z,
tyexists (λ range_end : Z,
constrained (struct struct_hyp_pool [@{type}
(own_constrained (nonshr_constraint (vmemmap ◁ₗ (array (struct_hyp_page) (pages `at_type` hyp_page)) )) (range_start @ (int (u64)))) ;
(range_end @ (int (u64))) ;
(max_order @ (int (u16)))
]) (
(initialized "__hyp_vmemmap" vmemmap)
(length pages =@{Z} range_start_idx + npages)%Z
(range_start = range_start_idx PAGE_SHIFT)%Z
(range_end = range_start + npages PAGE_SHIFT)%Z
(0 <= range_start_idx)%Z
)))
)%I.
Typeclasses Opaque hyp_pool_rec.
Global Instance hyp_pool_rec_ne : Contractive hyp_pool_rec.
Proof. solve_type_proper. Qed.
Definition hyp_pool : rtype := {|
rty_type := (list (Z * Z)) * nat * loc * Z * Z;
rty r__ := fixp hyp_pool_rec r__
|}.
Lemma hyp_pool_unfold (patt__ : (list (Z * Z)) * nat * loc * Z * Z):
(patt__ @ hyp_pool)%I @{type} (
let pages := patt__.1.1.1.1 in
let npages := patt__.1.1.1.2 in
let vmemmap := patt__.1.1.2 in
let range_start_idx := patt__.1.2 in
let max_order := patt__.2 in
tyexists (λ range_start : Z,
tyexists (λ range_end : Z,
constrained (struct struct_hyp_pool [@{type}
(own_constrained (nonshr_constraint (vmemmap ◁ₗ (array (struct_hyp_page) (pages `at_type` hyp_page)) )) (range_start @ (int (u64)))) ;
(range_end @ (int (u64))) ;
(max_order @ (int (u16)))
]) (
(initialized "__hyp_vmemmap" vmemmap)
(length pages =@{Z} range_start_idx + npages)%Z
(range_start = range_start_idx PAGE_SHIFT)%Z
(range_end = range_start + npages PAGE_SHIFT)%Z