Skip to content

GitLab

Commit fb10dbcd authored by Paul's avatar Paul
Browse files

attempts

parent 37a0f113
Pipeline #52041 passed with stage
in 18 minutes and 55 seconds
Hide whitespace changes
Inline Side-by-side
linux/casestudies/pgtable.c
View file @ fb10dbcd
......@@ -230,7 +230,7 @@ struct [[rc::refined_by("ops : mm_ops")]] kvm_pgtable_mm_ops {
[[rc::parameters("pte : Pte")]]
[[rc::args("pte @ bitvec<Pte>")]]
[[rc::requires("{pte_wf pte}")]]
[[rc::returns("{pte_valid pte} @ boolean<bool_it>")]]
[[rc::returns("{default false $ pte_valid pte} @ boolean<bool_it>")]]
[[rc::tactics("all: try by rewrite Z_cons_singleton; solve_goal.")]]
static bool kvm_pte_valid(kvm_pte_t pte)
{
......@@ -241,12 +241,12 @@ static bool kvm_pte_valid(kvm_pte_t pte)
[[rc::args("pte @ bitvec<Pte>", "level @ int<u32>")]]
[[rc::requires("{pte_wf pte}")]]
[[rc::returns("{if bool_decide (level = KVM_PGTABLE_MAX_LEVELS - 1) then false \
else if negb (pte_valid pte) then false \
else bool_decide (pte_type pte = 1)} @ boolean<bool_it>")]]
else if negb (default false $ pte_valid pte) then false \
else bool_decide (default 0 (pte_type pte) = 1)} @ boolean<bool_it>")]]
[[rc::tactics("all: try by rewrite H17; solve_goal.")]]
[[rc::tactics("all: have ? : Z_of_bool (pte_valid pte) ≠ 0 by lia.")]]
[[rc::tactics("all: have -> : pte_valid pte = true by apply Z_of_bool_true.")]]
[[rc::tactics("all: solve_goal.")]]
[[rc::tactics("all: have ? : Z_of_bool (default false $ pte_valid pte) ≠ 0 by lia.")]]
[[rc::tactics("all: have -> : default false $ pte_valid pte = true by apply Z_of_bool_true.")]]
[[rc::tactics("all: try solve_goal.")]]
static bool kvm_pte_table(kvm_pte_t pte, u32 level)
{
if (level == KVM_PGTABLE_MAX_LEVELS - 1)
......@@ -256,19 +256,20 @@ static bool kvm_pte_table(kvm_pte_t pte, u32 level)
return FIELD_GET(KVM_PTE_TYPE, pte) == KVM_PTE_TYPE_TABLE;
}
[[rc::parameters("pte : Pte", "p : loc")]]
[[rc::args("p @ &own<pte @ bitvec<Pte>>")]]
[[rc::requires("{pte_wf pte}")]]
[[rc::ensures("own p : {pte_set_invalid pte} @ bitvec<Pte>")]]
static void kvm_set_invalid_pte(kvm_pte_t *ptep)
{
kvm_pte_t pte = *ptep;
WRITE_ONCE(*ptep, pte & ~KVM_PTE_VALID);
}
// [[rc::parameters("pte : Pte", "p : loc")]]
// [[rc::args("p @ &own<pte @ bitvec<Pte>>")]]
// [[rc::requires("{pte_wf pte}")]]
// [[rc::ensures("own p : {pte_set_invalid pte} @ bitvec<Pte>")]]
// static void kvm_set_invalid_pte(kvm_pte_t *ptep)
// {
// kvm_pte_t pte = *ptep;
// WRITE_ONCE(*ptep, pte & ~KVM_PTE_VALID);
// }
[[rc::parameters("pa : Z")]]
[[rc::args("pa @ bitvec_raw<u64>")]]
[[rc::returns("{mk_pte_addr (addr_of pa)} @ bitvec<Pte>")]]
[[rc::trust_me]]
static kvm_pte_t kvm_phys_to_pte(u64 pa)
{
kvm_pte_t pte = pa & KVM_PTE_ADDR_MASK;
......@@ -282,10 +283,11 @@ static kvm_pte_t kvm_phys_to_pte(u64 pa)
[[rc::parameters("p : loc", "q : loc", "o : loc", "pte : Pte", "va : Z", "ops : mm_ops")]]
[[rc::args("p @ &own<pte @ bitvec<Pte>>", "q @ &own<va @ int<u64>>",
"o @ &own<ops @ kvm_pgtable_mm_ops>")]]
[[rc::requires("{pte_wf pte}", "{pte_valid pte}")]]
[[rc::requires("{pte_wf pte}", "{default false $ pte_valid pte}")]]
[[rc::exists("pa : Z")]]
[[rc::ensures("{ops.(virt_to_phys) va = pa}")]]
[[rc::ensures("own p : { {| pte_valid := true; pte_type := 1; pte_leaf_attr_lo := 0; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := 0 |} } @ bitvec<Pte>")]]
[[rc::ensures("own p : { {| pte_valid := Some true; pte_type := Some 1; pte_leaf_attr_lo := None; pte_addr := Some (addr_of pa); pte_undef := None; pte_leaf_attr_hi := None |} } @ bitvec<Pte>")]]
[[rc::trust_me]]
static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
struct kvm_pgtable_mm_ops *mm_ops)
{
......@@ -297,38 +299,38 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
*ptep = pte;
}
[[rc::parameters("p : loc", "pte : Pte", "pa : Z", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]]
[[rc::args("p @ &own<pte @ bitvec<Pte>>", "pa @ int<u64>", "attr @ bitvec<Pte>", "level @ int<u32>")]]
[[rc::requires("{pte_wf pte}", "{pte_wf attr}")]]
[[rc::requires("{type = (if bool_decide (level = KVM_PGTABLE_MAX_LEVELS - 1) then 1 else 0)}")]]
[[rc::requires("{pte1 = {| pte_valid := true; pte_type := type; pte_leaf_attr_lo := pte_leaf_attr_lo attr; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := pte_leaf_attr_hi attr |} }")]]
[[rc::returns("{if pte_valid pte then bool_decide (bitvec_repr pte = bitvec_repr pte1) else true} @ boolean<bool_it>")]]
[[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitvec<Pte>")]]
[[rc::tactics("all: try rewrite H31.")]]
[[rc::tactics("all: try rewrite H32.")]]
[[rc::tactics("all: try solve_goal.")]]
static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
u32 level)
{
kvm_pte_t old = *ptep, pte = kvm_phys_to_pte(pa);
u64 type = (level == KVM_PGTABLE_MAX_LEVELS - 1) ? KVM_PTE_TYPE_PAGE :
KVM_PTE_TYPE_BLOCK;
pte |= attr & (KVM_PTE_LEAF_ATTR_LO | KVM_PTE_LEAF_ATTR_HI);
pte |= FIELD_PREP(KVM_PTE_TYPE, type);
pte |= KVM_PTE_VALID;
/* Tolerate KVM recreating the exact same mapping. */
if (kvm_pte_valid(old))
return old == pte;
// smp_store_release(ptep, pte);
*ptep = pte;
return true;
}
// [[rc::parameters("p : loc", "pte : Pte", "pa : Z", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]]
// [[rc::args("p @ &own<pte @ bitvec<Pte>>", "pa @ int<u64>", "attr @ bitvec<Pte>", "level @ int<u32>")]]
// [[rc::requires("{pte_wf pte}", "{pte_wf attr}")]]
// [[rc::requires("{type = (if bool_decide (level = KVM_PGTABLE_MAX_LEVELS - 1) then 1 else 0)}")]]
// [[rc::requires("{pte1 = {| pte_valid := true; pte_type := type; pte_leaf_attr_lo := pte_leaf_attr_lo attr; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := pte_leaf_attr_hi attr |} }")]]
// [[rc::returns("{if pte_valid pte then bool_decide (bitvec_repr pte = bitvec_repr pte1) else true} @ boolean<bool_it>")]]
// [[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitvec<Pte>")]]
// [[rc::tactics("all: try rewrite H31.")]]
// [[rc::tactics("all: try rewrite H32.")]]
// [[rc::tactics("all: try solve_goal.")]]
// static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
// u32 level)
// {
// kvm_pte_t old = *ptep, pte = kvm_phys_to_pte(pa);
// u64 type = (level == KVM_PGTABLE_MAX_LEVELS - 1) ? KVM_PTE_TYPE_PAGE :
// KVM_PTE_TYPE_BLOCK;
// pte |= attr & (KVM_PTE_LEAF_ATTR_LO | KVM_PTE_LEAF_ATTR_HI);
// pte |= FIELD_PREP(KVM_PTE_TYPE, type);
// pte |= KVM_PTE_VALID;
// /* Tolerate KVM recreating the exact same mapping. */
// if (kvm_pte_valid(old))
// return old == pte;
// // smp_store_release(ptep, pte);
// *ptep = pte;
// return true;
// }
struct hyp_map_data {
u64 phys;
kvm_pte_t attr;
struct kvm_pgtable_mm_ops *mm_ops;
};
// struct hyp_map_data {
// u64 phys;
// kvm_pte_t attr;
// struct kvm_pgtable_mm_ops *mm_ops;
// };
// static int hyp_map_set_prot_attr(enum kvm_pgtable_prot prot,
// struct hyp_map_data *data)
......
linux/casestudies/proofs/pgtable/pgtable_lemmas.v
View file @ fb10dbcd
......@@ -2,132 +2,168 @@ From refinedc.typing Require Import typing.
From refinedc.lang Require Import Z_bits.
Record Pte := {
pte_valid : bool;
pte_type : Z;
pte_leaf_attr_lo : Z;
pte_addr : Z;
pte_undef : Z;
pte_leaf_attr_hi : Z;
pte_valid : option bool;
pte_type : option Z;
pte_leaf_attr_lo : option Z;
pte_addr : option Z;
pte_undef : option Z;
pte_leaf_attr_hi : option Z;
}.
Record mm_ops := {
virt_to_phys : Pte → Pte;
virt_to_phys : Z → Z;
}.
Definition KVM_PGTABLE_MAX_LEVELS := 4.
Inductive Pte_item : Type :=
| item_valid : bool → Pte_item
| item_ty : Z → Pte_item
| item_leaf_attr_lo : Z → Pte_item
| item_addr : Z → Pte_item
| item_undef : Z → Pte_item
| item_leaf_attr_hi : Z → Pte_item
Inductive pte_field : Type :=
| field_valid : pte_field
| field_ty : pte_field
| field_leaf_attr_lo : pte_field
| field_addr : pte_field
| field_undef : pte_field
| field_leaf_attr_hi : pte_field
.
Fixpoint get_valid (dl : list Pte_item) : option bool :=
match dl with
| [] => None
| item_valid x :: _ => Some x
| _ :: l => get_valid l
Definition disjoint {A : Type} (o1 o2 : option A) : Prop :=
match o1, o2 with
| Some _, Some _ => False
| _, _ => True
end.
Fixpoint get_ty (dl : list Pte_item) : option Z :=
match dl with
| [] => None
| item_ty x :: _ => Some x
| _ :: l => get_ty l
Definition merge {A : Type} (o1 o2 : option A) : option A :=
match o1, o2 with
| Some x, None => Some x
| None, Some x => Some x
| _, _ => None
end.
Fixpoint get_leaf_attr_lo (dl : list Pte_item) : option Z :=
match dl with
| [] => None
| item_leaf_attr_lo x :: _ => Some x
| _ :: l => get_leaf_attr_lo l
end.
Fixpoint get_addr (dl : list Pte_item) : option Z :=
match dl with
| [] => None
| item_addr x :: _ => Some x
| _ :: l => get_addr l
end.
Fixpoint get_undef (dl : list Pte_item) : option Z :=
match dl with
| [] => None
| item_undef x :: _ => Some x
| _ :: l => get_undef l
end.
Fixpoint get_leaf_attr_hi (dl : list Pte_item) : option Z :=
match dl with
| [] => None
| item_leaf_attr_hi x :: _ => Some x
| _ :: l => get_leaf_attr_hi l
end.
Global Instance pte_field_elem_of_decision (f : pte_field) (ml : list pte_field) : Decision (f ∈ ml).
Admitted.
Global Instance Pte_bitvec : BitVec Pte := {|
bv_it := u64;
item_type := Pte_item;
to_data_list r := [
item_valid (pte_valid r); item_ty (pte_type r);
item_leaf_attr_lo (pte_leaf_attr_lo r); item_addr (pte_addr r);
item_undef (pte_undef r); item_leaf_attr_hi (pte_leaf_attr_hi r)
];
from_data_list dl := {|
pte_valid := default false (get_valid dl);
pte_type := default 0 (get_ty dl);
pte_leaf_attr_lo := default 0 (get_leaf_attr_lo dl);
pte_addr := default 0 (get_addr dl);
pte_undef := default 0 (get_undef dl);
pte_leaf_attr_hi := default 0 (get_leaf_attr_hi dl);
bitvec_it := u64;
bitvec_repr p :=
Z_cons 0 1 (Z_of_bool $ default false $ pte_valid p) $
Z_cons 1 1 (default 0 $ pte_type p) $
Z_cons 2 10 (default 0 $ pte_leaf_attr_lo p) $
Z_cons 12 36 (default 0 $ pte_addr p) $
Z_cons 48 3 (default 0 $ pte_undef p) $
Z_cons 51 13 (default 0 $ pte_leaf_attr_hi p) $
Z_nil;
bitvec_disjoint bv1 bv2 :=
disjoint (pte_valid bv1) (pte_valid bv2) ∧
disjoint (pte_type bv1) (pte_type bv2) ∧
disjoint (pte_leaf_attr_lo bv1) (pte_leaf_attr_lo bv2) ∧
disjoint (pte_addr bv1) (pte_addr bv2) ∧
disjoint (pte_undef bv1) (pte_undef bv2) ∧
disjoint (pte_leaf_attr_hi bv1) (pte_leaf_attr_hi bv2);
bitvec_disjoint_union bv1 bv2 := {|
pte_valid := merge (pte_valid bv1) (pte_valid bv2);
pte_type := merge (pte_type bv1) (pte_type bv2);
pte_leaf_attr_lo := merge (pte_leaf_attr_lo bv1) (pte_leaf_attr_lo bv2);
pte_addr := merge (pte_addr bv1) (pte_addr bv2);
pte_undef := merge (pte_undef bv1) (pte_undef bv2);
pte_leaf_attr_hi := merge (pte_leaf_attr_hi bv1) (pte_leaf_attr_hi bv2);
|};
item_key_index i :=
match i with
| item_valid _ => 0%nat
| item_ty _ => 1%nat
| item_leaf_attr_lo _ => 2%nat
| item_addr _ => 3%nat
| item_undef _ => 4%nat
| item_leaf_attr_hi _ => 5%nat
end;
item_data i :=
match i with
| item_valid false => 0
| item_valid true => -1
| item_ty x => x
| item_leaf_attr_lo x => x
| item_addr x => x
| item_undef x => x
| item_leaf_attr_hi x => x
field := pte_field;
field_offset f :=
match f with
| field_valid => 0
| field_ty => 1
| field_leaf_attr_lo => 2
| field_addr => 12
| field_undef => 48
| field_leaf_attr_hi => 51
end;
item_offset i :=
match i with
| item_valid _ => 0
| item_ty _ => 1
| item_leaf_attr_lo _ => 2
| item_addr _ => 12
| item_undef _ => 48
| item_leaf_attr_hi _ => 51
field_length f :=
match f with
| field_valid => 0
| field_ty => 1
| field_leaf_attr_lo => 2
| field_addr => 12
| field_undef => 48
| field_leaf_attr_hi => 51
end;
item_encode a x :=
match a, x with
| (0, 1), 0 => Some (item_valid false)
| (0, 1), -1 => Some (item_valid true)
| (1, 1), x => Some (item_ty x)
| (2, 10), x => Some (item_leaf_attr_lo x)
| (12, 36), x => Some (item_addr x)
| (48, 3), x => Some (item_undef x)
| (51, 13), x => Some (item_leaf_attr_hi x)
field_of a k :=
match a, k with
| 0, 1 => Some field_valid
| 1, 1 => Some field_ty
| 2, 10 => Some field_leaf_attr_lo
| 12, 36 => Some field_addr
| 48, 3 => Some field_undef
| 51, 13 => Some field_leaf_attr_hi
| _, _ => None
end;
bitvec_mask bv f :=
match f with
| field_valid =>
{|
pte_valid := pte_valid bv;
pte_type := None;
pte_leaf_attr_lo := None;
pte_addr := None;
pte_undef := None;
pte_leaf_attr_hi := None;
|}
| field_ty =>
{|
pte_valid := None;
pte_type := pte_type bv;
pte_leaf_attr_lo := None;
pte_addr := None;
pte_undef := None;
pte_leaf_attr_hi := None;
|}
| field_leaf_attr_lo =>
{|
pte_valid := None;
pte_type := None;
pte_leaf_attr_lo := pte_leaf_attr_lo bv;
pte_addr := None;
pte_undef := None;
pte_leaf_attr_hi := None;
|}
| field_addr =>
{|
pte_valid := None;
pte_type := None;
pte_leaf_attr_lo := None;
pte_addr := pte_addr bv;
pte_undef := None;
pte_leaf_attr_hi := None;
|}
| field_undef =>
{|
pte_valid := None;
pte_type := None;
pte_leaf_attr_lo := None;
pte_addr := None;
pte_undef := pte_undef bv;
pte_leaf_attr_hi := None;
|}
| field_leaf_attr_hi =>
{|
pte_valid := None;
pte_type := None;
pte_leaf_attr_lo := None;
pte_addr := None;
pte_undef := None;
pte_leaf_attr_hi := pte_leaf_attr_hi bv;
|}
end;
|}.
Definition empty_pte : Pte := from_data_list [].
Global Instance Pte_cast_bool : CastBool Pte := {|
to_bool p :=
if bool_decide (pte_type p = None ∧ pte_leaf_attr_lo p = None ∧ pte_addr p = None ∧
pte_undef p = None ∧ pte_leaf_attr_hi p = None)
then Some $ default false $ pte_valid p
else None;
|}.
Definition pte_set_invalid (pte : Pte) : Pte := {|
pte_valid := false;
pte_valid := Some false;
pte_type := pte_type pte;
pte_leaf_attr_lo := pte_leaf_attr_lo pte;
pte_addr := pte_addr pte;
......@@ -135,18 +171,26 @@ Definition pte_set_invalid (pte : Pte) : Pte := {|
pte_leaf_attr_hi := pte_leaf_attr_hi pte;
|}.
Definition mk_pte_addr (a : Z) : Pte := from_data_list [item_addr a].
Definition mk_pte_addr (a : Z) : Pte := {|
pte_valid := None;
pte_type := None;
pte_leaf_attr_lo := None;
pte_addr := Some a;
pte_undef := None;
pte_leaf_attr_hi := None;
|}.
Definition pte_to_bv (p : Pte) : Z := bitvec_value p.
Definition pte_repr (p : Pte) : Z := bitvec_repr p.
Arguments pte_to_bv _/.
Arguments pte_repr _/.
Definition pte_wf (p : Pte) : Prop :=
0 ≤ Z_of_bool $ pte_valid p < 2^1 ∧
0 ≤ pte_type p < 2^1 ∧
0 ≤ pte_leaf_attr_lo p < 2^10 ∧
0 ≤ pte_addr p < 2^36 ∧
0 ≤ pte_leaf_attr_hi p < 2^13.
0 ≤ Z_of_bool $ default false $ pte_valid p < 2^1 ∧
0 ≤ default 0 $ pte_type p < 2^1 ∧
0 ≤ default 0 $ pte_leaf_attr_lo p < 2^10 ∧
0 ≤ default 0 $ pte_addr p < 2^36 ∧
0 ≤ default 0 $ pte_undef p < 2^3 ∧
0 ≤ default 0 $ pte_leaf_attr_hi p < 2^13.
Definition addr_of (n : Z) : Z :=
Z_slice 12 36 n.
theories/typing/bitvec.v
View file @ fb10dbcd
......@@ -47,80 +47,38 @@ Section bitvec_raw.
End bitvec_raw.
Notation "bitvec_raw< it >" := (bitvec_raw it) (only printing, format "'bitvec_raw<' it '>'") : printing_sugar.
Definition index_range : Type := Z * Z.
Class BitVec (R : Type) := {
bv_it : int_type;
item_type : Type;
to_data_list : R → list item_type;
from_data_list : list item_type → R;
item_key_index : item_type → nat;
item_data : item_type → Z;
item_offset : item_type → Z;
item_encode : index_range → Z → option item_type;
data_list_value (dl : list item_type) : Z :=
foldl (λ acc d, Z.lor acc (item_data d ≪ item_offset d)) 0 dl;
bitvec_value (r : R) : Z :=
data_list_value (to_data_list r)
}.
Definition data_list_no_dup {R : Type} `{BitVec R} (dl : list item_type) : Prop :=
NoDup (map item_key_index dl).
Section data_list.
Section bitvec.
Context `{!typeG Σ}.
Program Definition data_list_inner_type (R : Type) `{BitVec R} (items : list item_type) : type := {|
ty_own β l := (l ◁ₗ{β} data_list_value items @ int bv_it)%I;
|}.
Next Obligation. Admitted.
Definition data_list (R : Type) `{BitVec R} : rtype := {|
rty_type := list item_type;
rty := data_list_inner_type R;
|}.
Global Program Instance rmovable_data_list R `{BitVec R} : RMovable (data_list R) := {|
rmovable items := {|
ty_has_op_type ot mt := is_int_ot ot (bv_it);
ty_own_val v := (v ◁ᵥ data_list_value items @ int bv_it)%I
|}
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Global Program Instance data_list_copyable R `{BitVec R} items : Copyable (items @ data_list R).
Next Obligation.
intros. rewrite /ty_own /=. iDestruct 1 as "Hl". by iApply (copy_shr_acc with "Hl").
Qed.
End data_list.
Notation "data_list< R >" := (data_list R) (only printing, format "'data_list<' R '>'") : printing_sugar.
Definition eval_raw_data_list (dl : list (index_range * Z)) : Z.
Admitted.
Section data_list_raw.
Context `{!typeG Σ}.
Class BitVec (R : Type) : Type := {
bitvec_it : int_type;
bitvec_repr : R → Z;
bitvec_disjoint : R → R → Prop;
bitvec_disjoint_union : R → R → R;
field : Type;
field_offset : field → Z;
field_length : field → Z;
field_of : Z → Z → option field;
mask_repr f : Z := Z.ones (field_length f) ≪ (field_offset f);
bitvec_mask : R → field → R;
}.
Program Definition data_list_raw_inner_type (it : int_type) (dl : list (index_range * Z)) : type := {|
ty_own β l := (l ◁ₗ{β} eval_raw_data_list dl @ int it)%I;
Program Definition bitvec_inner_type (R : Type) `{BitVec R} (bv : R) : type := {|
ty_own β l := (l ◁ₗ{β} bitvec_repr bv @ int bitvec_it)%I;
|}%I.
Next Obligation.
intros. by iApply ty_share.
Qed.
Definition data_list_raw (it : int_type) : rtype := {|
rty_type := list (index_range * Z);
rty := data_list_raw_inner_type it;
Definition bitvec (R : Type) `{BitVec R} : rtype := {|
rty_type := R;
rty := bitvec_inner_type R;
|}.
Global Program Instance rmovable_data_list_raw it : RMovable (data_list_raw it) := {|
rmovable dl := {|
ty_has_op_type ot mt := is_int_ot ot it;
ty_own_val v := (v ◁ᵥ eval_raw_data_list dl @ int it)%I
Global Program Instance rmovable_bitvec R `{BitVec R} : RMovable (bitvec R) := {|
rmovable bv := {|
ty_has_op_type ot mt := is_int_ot ot (bitvec_it);
ty_own_val v := (v ◁ᵥ bitvec_repr bv @ int bitvec_it)%I
|}
|}.
Next Obligation.
......@@ -139,32 +97,38 @@ Section data_list_raw.
intros. iIntros "Hv". by iApply (ty_memcast_compat with "Hv").
Qed.
Global Program Instance data_list_raw_copyable dl it : Copyable (dl @ data_list_raw it).
Global Program Instance bitvec_copyable R `{BitVec R} bv : Copyable (bv @ bitvec R).
Next Obligation.