Commit b82d8cfa authored by Paul's avatar Paul
Browse files

x86 pgtable case

parent 05431e20
......@@ -57,3 +57,4 @@
-Q _build/default/linux/casestudies/proofs/pgtable refinedc.linux.casestudies.pgtable
-Q _build/default/tutorial/proofs/lithium refinedc.tutorial.lithium
-Q _build/default/linux/casestudies/mt7601u/proofs/mac refinedc.linux.casestudies.mt7601u.mac
-Q _build/default/linux/casestudies/proofs/x86_pgtable refinedc.linux.casestudies.x86_pgtable
From refinedc.typing Require Import typing.
Record pte := mk_pte {
pg_present : bool;
pg_write : bool;
pg_user : bool;
pg_pwt : bool;
pg_pcd : bool;
pg_accessed : bool;
pg_dirty : bool;
pg_pse : bool;
pg_global : bool;
pg_special : bool;
pg_uffd_wp : bool;
pg_soft_dirty : bool;
(*****)
pg_dev_map : bool;
pg_no_exec : bool;
}.
Global Instance pte_settable : Settable _ := settable! mk_pte
<pg_present; pg_write; pg_user; pg_pwt; pg_pcd;
pg_accessed; pg_dirty; pg_pse; pg_global; pg_special;
pg_uffd_wp; pg_soft_dirty;
pg_dev_map; pg_no_exec>.
Definition pte_repr (f : pte) : Z :=
bf_cons 0 1 (Z_of_bool $ pg_present f) $
bf_cons 1 1 (Z_of_bool $ pg_write f) $
bf_cons 2 1 (Z_of_bool $ pg_user f) $
bf_cons 3 1 (Z_of_bool $ pg_pwt f) $
bf_cons 4 1 (Z_of_bool $ pg_pcd f) $
bf_cons 5 1 (Z_of_bool $ pg_accessed f) $
bf_cons 6 1 (Z_of_bool $ pg_dirty f) $
bf_cons 7 1 (Z_of_bool $ pg_pse f) $
bf_cons 8 1 (Z_of_bool $ pg_global f) $
bf_cons 9 1 (Z_of_bool $ pg_special f) $
bf_cons 10 1 (Z_of_bool $ pg_uffd_wp f) $
bf_cons 11 1 (Z_of_bool $ pg_soft_dirty f) $
bf_cons 58 1 (Z_of_bool $ pg_dev_map f) $
bf_cons 63 1 (Z_of_bool $ pg_no_exec f) $
bf_nil.
Arguments pte_repr _/.
Coercion pte_repr : pte >-> Z.
Definition pte_wf (f : pte) : Prop :=
0 Z_of_bool $ pg_present f < 2^1
0 Z_of_bool $ pg_write f < 2^1
0 Z_of_bool $ pg_user f < 2^1
0 Z_of_bool $ pg_pwt f < 2^1
0 Z_of_bool $ pg_pcd f < 2^1
0 Z_of_bool $ pg_accessed f < 2^1
0 Z_of_bool $ pg_dirty f < 2^1
0 Z_of_bool $ pg_pse f < 2^1
0 Z_of_bool $ pg_global f < 2^1
0 Z_of_bool $ pg_special f < 2^1
0 Z_of_bool $ pg_uffd_wp f < 2^1
0 Z_of_bool $ pg_soft_dirty f < 2^1
0 Z_of_bool $ pg_dev_map f < 2^1
0 Z_of_bool $ pg_no_exec f < 2^1
0 f < 2^64.
Global Instance pte_Bitfield_Desc : BitfieldDesc pte := {|
bitfield_it := u64;
bitfield_repr := pte_repr;
bitfield_wf := pte_wf;
|}.
Definition pte_present (p : pte) : bool := pg_present p || pg_global p.
Arguments pte_present _/.
//@rc::import x86_pgtable_lemmas from refinedc.linux.casestudies.x86_pgtable
#include <stdbool.h>
#include "bits.h"
// arch/x86/include/asm/page_64_types.h
#define __PHYSICAL_MASK_SHIFT 52
// arch/x86/include/asm/page_types.h
typedef u64 phys_addr_t;
// Z.ones 52
#define __PHYSICAL_MASK ((phys_addr_t)((1ULL << __PHYSICAL_MASK_SHIFT) - 1))
#define PAGE_SHIFT 12
#define PAGE_SIZE (1 << PAGE_SHIFT)
// ~Z.ones 12
#define PAGE_MASK (~(PAGE_SIZE-1))
// GENMASK(51, 12)
#define PHYSICAL_PAGE_MASK (((signed long)PAGE_MASK) & __PHYSICAL_MASK)
// arch/x86/include/asm/pgtable_64_types.h
typedef unsigned long pteval_t;
typedef struct [[rc::refined_by("v : Z")]] pte_t {
[[rc::field("v @ bitfield_raw<u64>")]]
pteval_t pte;
} pte_t;
// arch/x86/include/asm/pgtable_types.h
[[rc::parameters("p : pte")]]
[[rc::args("p @ pte_t")]]
[[rc::returns("p @ bitfield_raw<u64>")]]
static inline pteval_t native_pte_val(pte_t pte)
{
return pte.pte;
}
[[rc::parameters("v : Z")]]
[[rc::args("v @ bitfield_raw<u64>")]]
[[rc::returns("v @ pte_t")]]
static inline pte_t native_make_pte(pteval_t val)
{
return (pte_t) { .pte = val };
}
/* Extracts the PFN from a (pte|pmd|pud|pgd)val_t of a 4KB page */
#define PTE_PFN_MASK ((pteval_t)PHYSICAL_PAGE_MASK)
/*
* Extracts the flags from a (pte|pmd|pud|pgd)val_t
* This includes the protection key value.
*/
// GENMASK(0, 11) | GENMASK(52, 63)
#define PTE_FLAGS_MASK (~PTE_PFN_MASK)
[[rc::parameters("p : pte")]]
[[rc::args("p @ pte_t")]]
[[rc::returns("p @ bitfield<pte>")]]
[[rc::trust_me]]
static inline pteval_t pte_flags(pte_t pte)
{
return native_pte_val(pte) & PTE_FLAGS_MASK;
}
#define _PAGE_BIT_PRESENT 0 /* is present */
#define _PAGE_BIT_RW 1 /* writeable */
#define _PAGE_BIT_USER 2 /* userspace addressable */
#define _PAGE_BIT_PWT 3 /* page write through */
#define _PAGE_BIT_PCD 4 /* page cache disabled */
#define _PAGE_BIT_ACCESSED 5 /* was accessed (raised by CPU) */
#define _PAGE_BIT_DIRTY 6 /* was written to (raised by CPU) */
#define _PAGE_BIT_PSE 7 /* 4 MB (or 2MB) page */
#define _PAGE_BIT_GLOBAL 8 /* Global TLB entry PPro+ */
#define _PAGE_BIT_SOFTW1 9 /* available for programmer */
#define _PAGE_BIT_SOFTW2 10 /* " */
#define _PAGE_BIT_SOFTW3 11 /* " */
#define _PAGE_BIT_PAT_LARGE 12 /* On 2MB or 1GB pages */
#define _PAGE_BIT_SOFTW4 58 /* available for programmer */
#define _PAGE_BIT_PKEY_BIT0 59 /* Protection Keys, bit 1/4 */
#define _PAGE_BIT_PKEY_BIT1 60 /* Protection Keys, bit 2/4 */
#define _PAGE_BIT_PKEY_BIT2 61 /* Protection Keys, bit 3/4 */
#define _PAGE_BIT_PKEY_BIT3 62 /* Protection Keys, bit 4/4 */
#define _PAGE_BIT_NX 63 /* No execute: only valid after cpuid check */
#define _PAGE_BIT_SPECIAL _PAGE_BIT_SOFTW1
#define _PAGE_BIT_CPA_TEST _PAGE_BIT_SOFTW1
#define _PAGE_BIT_UFFD_WP _PAGE_BIT_SOFTW2 /* userfaultfd wrprotected */
#define _PAGE_BIT_SOFT_DIRTY _PAGE_BIT_SOFTW3 /* software dirty tracking */
#define _PAGE_BIT_DEVMAP _PAGE_BIT_SOFTW4
#define _PAGE_BIT_PROTNONE _PAGE_BIT_GLOBAL
// (_AT(pteval_t, 1) << k) = BIT(k)
#define _PAGE_PRESENT BIT(_PAGE_BIT_PRESENT)
#define _PAGE_RW BIT(_PAGE_BIT_RW)
#define _PAGE_USER BIT(_PAGE_BIT_USER)
#define _PAGE_PWT BIT(_PAGE_BIT_PWT)
#define _PAGE_PCD BIT(_PAGE_BIT_PCD)
#define _PAGE_ACCESSED BIT(_PAGE_BIT_ACCESSED)
#define _PAGE_DIRTY BIT(_PAGE_BIT_DIRTY)
#define _PAGE_PSE BIT(_PAGE_BIT_PSE)
#define _PAGE_GLOBAL BIT(_PAGE_BIT_GLOBAL)
#define _PAGE_SOFTW1 BIT(_PAGE_BIT_SOFTW1)
#define _PAGE_SOFTW2 BIT(_PAGE_BIT_SOFTW2)
#define _PAGE_SOFTW3 BIT(_PAGE_BIT_SOFTW3)
#define _PAGE_PAT BIT(_PAGE_BIT_PAT)
#define _PAGE_PAT_LARGE BIT(_PAGE_BIT_PAT_LARGE)
#define _PAGE_SPECIAL BIT(_PAGE_BIT_SPECIAL)
#define _PAGE_UFFD_WP BIT(_PAGE_BIT_UFFD_WP)
#define _PAGE_SOFT_DIRTY BIT(_PAGE_BIT_SOFT_DIRTY)
#define _PAGE_NX BIT(_PAGE_BIT_NX)
#define _PAGE_DEVMAP BIT(_PAGE_BIT_DEVMAP)
#define _PAGE_PROTNONE BIT(_PAGE_BIT_PROTNONE)
#define INPUT_PTE \
[[rc::parameters("p : pte")]] \
[[rc::args("p @ pte_t")]] \
[[rc::requires("{bitfield_wf p}")]]
INPUT_PTE
[[rc::returns("{pte_present p} @ boolean<bool_it>")]]
static inline bool pte_present(pte_t a)
{
// TODO: remove 0 != once issue #45 is fixed
return 0 != (pte_flags(a) & (_PAGE_PRESENT | _PAGE_PROTNONE));
}
/*
* The following only work if pte_present() is true.
* Undefined behaviour if not..
*/
#define IF_PTE_PRESENT \
[[rc::requires("{pte_present p}")]]
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_dirty p} @ boolean<bool_it>")]]
static inline bool pte_dirty(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_DIRTY);
}
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_accessed p} @ boolean<bool_it>")]]
static inline bool pte_young(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_ACCESSED);
}
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_write p} @ boolean<bool_it>")]]
static inline bool pte_write(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_RW);
}
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_pse p} @ boolean<bool_it>")]]
static inline bool pte_huge(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_PSE);
}
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_global p} @ boolean<bool_it>")]]
static inline bool pte_global(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_GLOBAL);
}
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{negb (pg_no_exec p)} @ boolean<bool_it>")]]
[[rc::trust_me]] // TODO: Z_of_bool (negb _) bound
static inline bool pte_exec(pte_t pte)
{
return !(pte_flags(pte) & _PAGE_NX);
}
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_special p} @ boolean<bool_it>")]]
static inline bool pte_special(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_SPECIAL);
}
[[rc::parameters("p : pte", "m : Z", "res : Z")]]
[[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]]
[[rc::requires("{normalize_bitfield_eq (Z.lor p m) res}")]]
[[rc::returns("res @ pte_t")]]
static inline pte_t pte_set_flags(pte_t pte, pteval_t set)
{
pteval_t v = native_pte_val(pte);
return native_make_pte(v | set);
}
[[rc::parameters("p : pte", "m : Z", "res : Z")]]
[[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]]
[[rc::requires("{normalize_bitfield_eq (Z.land p (Z_lunot 64 m)) res}")]]
[[rc::returns("res @ pte_t")]]
static inline pte_t pte_clear_flags(pte_t pte, pteval_t clear)
{
pteval_t v = native_pte_val(pte);
return native_make_pte(v & ~clear);
}
// #ifdef CONFIG_HAVE_ARCH_USERFAULTFD_WP
INPUT_PTE
[[rc::returns("{pg_uffd_wp p} @ boolean<bool_it>")]]
static inline bool pte_uffd_wp(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_UFFD_WP);
}
INPUT_PTE
[[rc::returns("{p <| pg_uffd_wp := true |>} @ pte_t")]]
static inline pte_t pte_mkuffd_wp(pte_t pte)
{
return pte_set_flags(pte, _PAGE_UFFD_WP);
}
INPUT_PTE
[[rc::returns("{p <| pg_uffd_wp := false |>} @ pte_t")]]
static inline pte_t pte_clear_uffd_wp(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_UFFD_WP);
}
// #endif
INPUT_PTE
[[rc::returns("{p <| pg_dirty := false |>} @ pte_t")]]
static inline pte_t pte_mkclean(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_accessed := false |>} @ pte_t")]]
static inline pte_t pte_mkold(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_ACCESSED);
}
INPUT_PTE
[[rc::returns("{p <| pg_write := false |>} @ pte_t")]]
static inline pte_t pte_wrprotect(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_RW);
}
INPUT_PTE
[[rc::returns("{p <| pg_no_exec := false |>} @ pte_t")]]
static inline pte_t pte_mkexec(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_NX);
}
INPUT_PTE
[[rc::returns("{p <| pg_dirty := true |> <| pg_soft_dirty := true |>} @ pte_t")]]
static inline pte_t pte_mkdirty(pte_t pte)
{
return pte_set_flags(pte, _PAGE_DIRTY | _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_accessed := true |>} @ pte_t")]]
static inline pte_t pte_mkyoung(pte_t pte)
{
return pte_set_flags(pte, _PAGE_ACCESSED);
}
INPUT_PTE
[[rc::returns("{p <| pg_write := true |>} @ pte_t")]]
static inline pte_t pte_mkwrite(pte_t pte)
{
return pte_set_flags(pte, _PAGE_RW);
}
INPUT_PTE
[[rc::returns("{p <| pg_pse := true |>} @ pte_t")]]
static inline pte_t pte_mkhuge(pte_t pte)
{
return pte_set_flags(pte, _PAGE_PSE);
}
INPUT_PTE
[[rc::returns("{p <| pg_pse := false |>} @ pte_t")]]
static inline pte_t pte_clrhuge(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_PSE);
}
INPUT_PTE
[[rc::returns("{p <| pg_global := true |>} @ pte_t")]]
static inline pte_t pte_mkglobal(pte_t pte)
{
return pte_set_flags(pte, _PAGE_GLOBAL);
}
INPUT_PTE
[[rc::returns("{p <| pg_global := false |>} @ pte_t")]]
static inline pte_t pte_clrglobal(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_GLOBAL);
}
INPUT_PTE
[[rc::returns("{p <| pg_special := true |>} @ pte_t")]]
static inline pte_t pte_mkspecial(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SPECIAL);
}
INPUT_PTE
[[rc::returns("{p <| pg_special := true |> <| pg_dev_map := true |>} @ pte_t")]]
static inline pte_t pte_mkdevmap(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SPECIAL | _PAGE_DEVMAP);
}
// #ifdef CONFIG_HAVE_ARCH_SOFT_DIRTY
INPUT_PTE
[[rc::returns("{pg_soft_dirty p} @ boolean<bool_it>")]]
static inline bool pte_soft_dirty(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_soft_dirty := true |>} @ pte_t")]]
static inline pte_t pte_mksoft_dirty(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_soft_dirty := false |>} @ pte_t")]]
static inline pte_t pte_clear_soft_dirty(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_SOFT_DIRTY);
}
// #endif
......@@ -505,7 +505,7 @@ Proof.
split; naive_solver.
Qed.
(* Simplify singleton data list =/≠ 0 *)
(* Simplify data list =/≠ 0 *)
Global Instance bf_cons_singleton_z a k x `{!CanSolve (0 a)} :
SimplBothRel (=) 0 (bf_cons a k x bf_nil) (x = 0).
......@@ -527,6 +527,75 @@ Proof.
split; naive_solver.
Qed.
Lemma bf_cons_z_iff a k x l :
0 a
bf_cons a k x l = 0 x = 0 l = 0.
Proof.
move => ?. rewrite /bf_cons Z.lor_eq_0_iff Z.shiftl_eq_0_iff //.
Qed.
Global Instance bf_cons_z a k x l `{!CanSolve (0 a)} :
SimplBothRel (=) 0 (bf_cons a k x l) (x = 0 l = 0).
Proof.
have := (bf_cons_z_iff a k x l).
split; naive_solver.
Qed.
Lemma bf_cons_nz_iff a k x l :
0 a
bf_cons a k x l 0 x 0 l 0.
Proof.
move => ?. rewrite not_iff_compat; last by apply bf_cons_z_iff. lia.
Qed.
Global Instance bf_cons_nz_1 a k x l `{!CanSolve (0 a)} :
SimplBoth (bf_cons a k x l 0) (x 0 l 0).
Proof.
have := (bf_cons_nz_iff a k x l).
split; naive_solver.
Qed.
Global Instance bf_cons_nz_2 a k x l `{!CanSolve (0 a)} :
SimplBoth (0 bf_cons a k x l) (x 0 l 0).
Proof.
have := (bf_cons_nz_iff a k x l).
split; naive_solver.
Qed.
Lemma bool_decide_or P Q `{Decision P} `{Decision Q} :
bool_decide (P Q) = bool_decide P || bool_decide Q.
Proof.
destruct (bool_decide P) eqn:HP;
[apply bool_decide_eq_true in HP | apply bool_decide_eq_false in HP].
all: destruct (bool_decide Q) eqn:HQ;
[apply bool_decide_eq_true in HQ | apply bool_decide_eq_false in HQ].
all: simpl.
all: try by apply bool_decide_eq_true; naive_solver.
apply bool_decide_eq_false; naive_solver.
Qed.
Lemma bool_decide_Z_of_bool b :
bool_decide (Z_of_bool b 0) = b.
Proof.
by destruct b.
Qed.
Global Instance bf_cons_bool_decide_eq_b a k b `{!CanSolve (0 a)} :
SimplAnd (bool_decide (0 bf_cons a k (Z_of_bool b) bf_nil) = b) (λ T, T).
Proof.
rewrite (bool_decide_iff _ (Z_of_bool b 0)); last by rewrite -bf_cons_singleton_nz_iff.
rewrite bool_decide_Z_of_bool.
split; naive_solver.
Qed.
Global Instance bf_cons_bool_decide_eq_orb a k l b b' `{!CanSolve (0 a)} :
SimplAndUnsafe true (bool_decide (0 bf_cons a k (Z_of_bool b) l) = b || b')
(λ T, bool_decide (0 l) = b' T).
Proof.
rewrite (bool_decide_iff _ (Z_of_bool b 0 l 0)); last by rewrite -bf_cons_nz_iff.
rewrite bool_decide_or bool_decide_Z_of_bool => ? [<- ?].
rewrite (bool_decide_iff _ (0 l)); naive_solver.
Qed.
(* Simplify data list eq *)
Global Instance bf_cons_eq a k x1 l1 x2 l2 :
......
......@@ -263,44 +263,34 @@ Section programs.
TypedBinOpVal v1 (n @ int it)%I v2 (bv @ bitfield_raw it)%I OrOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_bitfield_raw it v1 n v2 bv T (Z.lor n bv) _ _).
Next Obligation. done. Qed.
Lemma type_bitfield_raw_is_false it v1 v2 bv T :
( a b, bv = bf_cons a 1 (bool_to_Z b) bf_nil 0 a T (i2v (bool_to_Z (negb b)) i32) ((bool_to_Z (negb b) @ int i32))) -
typed_bin_op v1 (v1 ◁ᵥ 0 @ int it) v2 (v2 ◁ᵥ bv @ bitfield_raw it) (EqOp i32) (IntOp it) (IntOp it) T.
Proof.
iIntros "HT Hv1 Hv2".
iDestruct "HT" as (a b Hbv ?) "HT".
iApply type_val_expr_mono_strong.
iApply (type_relop_int_int with "[HT] Hv1 Hv2") => //.
iIntros "_ _".
have -> : negb b = bool_decide (0 = bv).
{ rewrite (bool_decide_iff _ (bv = 0)) //.
rewrite Hbv (bool_decide_iff _ (b = false)); last by apply bf_cons_bool_singleton_false_iff.
by destruct b. }
iExists _. iFrame. unfold boolean, int; simpl_type. iIntros "(%n&%&%Heq)". move: Heq => /= ?. subst n. done.
Qed.
Global Instance type_bitfield_raw_is_false_inst it v1 v2 bv :
TypedBinOpVal v1 (0 @ int it)%I v2 (bv @ bitfield_raw it)%I (EqOp i32) (IntOp it) (IntOp it) :=
λ T, i2p (type_bitfield_raw_is_false it v1 v2 bv T).
Lemma type_bitfield_raw_is_true it v1 v2 bv T :
( a b, bv = bf_cons a 1 (bool_to_Z b) bf_nil 0 a T (i2v (bool_to_Z b) i32) ((bool_to_Z b) @ int i32)) -
typed_bin_op v1 (v1 ◁ᵥ 0 @ int it) v2 (v2 ◁ᵥ bv @ bitfield_raw it) (NeOp i32) (IntOp it) (IntOp it) T.
Lemma type_relop_int_bitfield_raw it v1 n v2 bv T b op:
match op with
| EqOp rit => Some (bool_decide (n = bv), rit)
| NeOp rit => Some (bool_decide (n bv), rit)
| LtOp rit => Some (bool_decide (n < bv), rit)
| GtOp rit => Some (bool_decide (n > bv), rit)
| LeOp rit => Some (bool_decide (n <= bv), rit)
| GeOp rit => Some (bool_decide (n >= bv), rit)
| _ => None
end = Some (b, i32)
(n it - bv it - T (i2v (Z_of_bool b) i32) (t2mt (b @ boolean i32))) -
typed_bin_op v1 (v1 ◁ᵥ n @ int it) v2 (v2 ◁ᵥ bv @ bitfield_raw it) op (IntOp it) (IntOp it) T.
Proof.
iIntros "HT Hv1 Hv2".
iDestruct "HT" as (a b Hbv ?) "HT".
iIntros "%Hop HT Hv1 Hv2".
iApply type_val_expr_mono_strong.
iApply (type_relop_int_int with "[HT] Hv1 Hv2") => //.
iIntros "_ _".
have -> : b = bool_decide (0 bv).
{ rewrite (bool_decide_iff _ (bv 0)) //.
rewrite Hbv (bool_decide_iff _ (b = true)); last by apply bf_cons_bool_singleton_true_iff.
by destruct b. }
iExists _. iFrame. unfold boolean, int; simpl_type.
iIntros "(%n&%&%Heq)". move: Heq => /= ?. subst n. done.
iIntros "Hbv1 Hbv2".
iSpecialize ("HT" with "Hbv1 Hbv2").
iExists _. by iFrame.
Qed.
Global Instance type_bitfield_raw_is_true_inst it v1 v2 bv :
TypedBinOpVal v1 (0 @ int it)%I v2 (bv @ bitfield_raw it)%I (NeOp i32) (IntOp it) (IntOp it) :=
λ T, i2p (type_bitfield_raw_is_true it v1 v2 bv T).
Global Program Instance type_eq_int_bitfield_raw_inst it v1 n v2 bv :
TypedBinOpVal v1 (n @ (int it))%I v2 (bv @ (bitfield_raw it))%I (EqOp i32) (IntOp it) (IntOp it) :=
λ T, i2p (type_relop_int_bitfield_raw it v1 n v2 bv T (bool_decide (n = bv)) _ _).
Next Obligation. done. Qed.
Global Program Instance type_ne_int_bitfield_raw_inst it v1 n v2 bv :
TypedBinOpVal v1 (n @ (int it))%I v2 (bv @ (bitfield_raw it))%I (NeOp i32) (IntOp it) (IntOp it) :=
λ T, i2p (type_relop_int_bitfield_raw it v1 n v2 bv T (bool_decide (n bv)) _ _).
Next Obligation. done. Qed.