diff --git a/_CoqProject b/_CoqProject index 5d6cafb553bca932a2c4a0ef1367a85fa09f98d3..a540fad5d13758205de4e3d89e4c200d73c942fe 100644 --- a/_CoqProject +++ b/_CoqProject @@ -54,3 +54,4 @@ -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 -Q _build/default/examples/proofs/pointers refinedc.examples.pointers +-Q _build/default/linux/casestudies/proofs/pgtable refinedc.linux.casestudies.pgtable diff --git a/include/dune b/include/dune index 2cf2dedb47dc3e62b567ab9c6363fd167cc53b4d..4c906bcca3da9d2223bcd646b0c42980a7fb0741 100644 --- a/include/dune +++ b/include/dune @@ -1,4 +1,5 @@ (install - (files (refinedc.h as include/refinedc.h)) + (files (refinedc.h as include/refinedc.h) + (refinedc_builtins_specs.h as include/refinedc_builtins_specs.h)) (section lib) (package refinedc)) diff --git a/include/refinedc.h b/include/refinedc.h index bd8784befb1d2c1cab71d7042c640edb9e4ed002..5b6b72444a2da4d54bfd588aa1cbc93bd43780a3 100644 --- a/include/refinedc.h +++ b/include/refinedc.h @@ -4,6 +4,10 @@ // Required for copy_alloc_id. #include +#if defined (__cerb__) +#include "refinedc_builtins_specs.h" +#endif + #define rc_unfold(e) \ _Pragma("GCC diagnostic push") \ _Pragma("GCC diagnostic ignored \"-Wunused-value\"") \ diff --git a/include/refinedc_builtins_specs.h b/include/refinedc_builtins_specs.h new file mode 100644 index 0000000000000000000000000000000000000000..00671a2d35607795b3d8bded07500ede50e053f2 --- /dev/null +++ b/include/refinedc_builtins_specs.h @@ -0,0 +1,22 @@ +//@rc::import builtins_specs from refinedc.lang + +/** + * GCC-builtins declaration. + */ +#ifndef REFINEDC_BUILTINS_SPECS_H +#define REFINEDC_BUILTINS_SPECS_H + +/** + * https://gcc.gnu.org/onlinedocs/gcc/Other-Builtins.html + * + * This built-in function returns one plus the index of the least significant 1-bit of x, + * or if x is zero, returns zero. + * + * Reference implementation: return log2(x & -x); + */ +[[rc::parameters("x : Z")]] +[[rc::args("x @ int")]] +[[rc::returns("{(Z_least_significant_one x + 1)%Z} @ int")]] +int __builtin_ffsll(unsigned long long x); + +#endif diff --git a/linux/casestudies/pgtable.c b/linux/casestudies/pgtable.c new file mode 100644 index 0000000000000000000000000000000000000000..66474e9ff578e3f5d38791144beee4b05ce2eedf --- /dev/null +++ b/linux/casestudies/pgtable.c @@ -0,0 +1,334 @@ +//@rc::import pgtable_lemmas from refinedc.linux.casestudies.pgtable + +#include +#include +#include +#include + +typedef uint64_t u64; +typedef uint32_t u32; + +#define PAGE_SHIFT 12 +#define WRITE_ONCE(a, b) ((a) = (b)) +#define BITS_PER_LONG (sizeof(long) * 8) +#define EINVAL 22 /* Invalid argument */ +#define WARN_ON(b) (assert(b)) + +/* linux/bits.h */ + +// #define BIT(i) (1UL << (i)) +[[rc::parameters("i : Z")]] +[[rc::args("i @ int")]] +[[rc::requires("{0 ≤ i < 64}")]] +[[rc::returns("{bf_mask_cons i 1 bf_nil} @ bitfield_raw")]] +[[rc::tactics("all: have ? := Z_shiftl_1_range i 64; try solve_goal.")]] +[[rc::lemmas("bf_mask_bit")]] +u64 BIT(int i) +{ + return (1UL << (i)); +} + +/* + * Create a contiguous bitmask starting at bit position @l and ending at + * position @h. For example + * GENMASK_ULL(39, 21) gives us the 64bit vector 0x000000ffffe00000. + */ +// #define GENMASK(h, l) \ + (((~0UL) - (1UL << (l)) + 1) & (~0UL >> (BITS_PER_LONG - 1 - (h)))) +[[rc::parameters("h : Z", "l : Z")]] +[[rc::args("h @ int", "l @ int")]] +[[rc::requires("{0 ≤ l}", "{l < h < 64}")]] +[[rc::returns("{bf_mask_cons l (h - l + 1) bf_nil} @ bitfield_raw")]] +[[rc::tactics("all: have [??] : 1 ≤ 1 ≪ l ≤ 2^64 - 1 by apply Z_shiftl_1_range; solve_goal.")]] +[[rc::tactics("all: try have -> : max_int u64 = 2^64 - 1 by solve_goal.")]] +[[rc::tactics("all: try have -> : ly_size i64 * 8 = bits_per_int u64 by solve_goal.")]] +[[rc::tactics("all: try have -> : bits_per_int u64 = 64 by solve_goal.")]] +[[rc::tactics("all: try have -> : Z_lunot 64 0 = 2^64 - 1 by solve_goal.")]] +[[rc::tactics("all: try solve_goal.")]] +[[rc::lemmas("bf_mask_gen")]] +u64 GENMASK(int h, int l) +{ + return (((~0UL) - (1UL << (l)) + 1) & (~0UL >> (BITS_PER_LONG - 1 - (h)))); +} + +/* linux/bitfield.h */ +#define __bf_shf(x) (__builtin_ffsll(x) - 1) + +/** + * FIELD_GET() - extract a bitfield element + * @_mask: shifted mask defining the field's length and position + * @_reg: value of entire bitfield + * + * FIELD_GET() extracts the field specified by @_mask from the + * bitfield passed in as @_reg by masking and shifting it down. + */ +/* +#define FIELD_GET(_mask, _reg) \ + ({ \ + __BF_FIELD_CHECK(_mask, _reg, 0U, "FIELD_GET: "); \ + (typeof(_mask))(((_reg) & (_mask)) >> __bf_shf(_mask)); \ + }) +*/ +[[rc::parameters("r : Z", "a : Z", "k : Z", "res : Z")]] +[[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw", "r @ bitfield_raw")]] +[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]] +[[rc::requires("{normalize_bitfield (bf_slice a k r) res}")]] +[[rc::returns("res @ int")]] +[[rc::tactics("all: unfold normalize_bitfield in *; subst.")]] +[[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask.")]] +[[rc::tactics("all: try solve_goal.")]] +[[rc::lemmas("bf_mask_cons_singleton_nonempty", "bf_shr_singleton")]] +u64 FIELD_GET(u64 _mask, u64 _reg) +{ + return (((_reg) & (_mask)) >> __bf_shf(_mask)); +} + +/** + * FIELD_PREP() - prepare a bitfield element + * @_mask: shifted mask defining the field's length and position + * @_val: value to put in the field + * + * FIELD_PREP() masks and shifts up the value. The result should + * be combined with other fields of the bitfield using logical OR. + */ +/* +#define FIELD_PREP(_mask, _val) \ + ({ \ + __BF_FIELD_CHECK(_mask, 0ULL, _val, "FIELD_PREP: "); \ + ((typeof(_mask))(_val) << __bf_shf(_mask)) & (_mask); \ + }) +*/ +[[rc::parameters("a : Z", "k : Z", "v : Z")]] +[[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw", "v @ int")]] +[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}", "{0 ≤ v < 2^k}")]] +[[rc::returns("{bf_cons a k v bf_nil} @ bitfield_raw")]] +[[rc::tactics("all: have [??] : v ≤ v ≪ a ≤ 2^64 - 1 by apply (Z_shl_bound k _ _ _); solve_goal.")]] +[[rc::tactics("all: try have -> : max_int u64 = 2^64 - 1 by solve_goal.")]] +[[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask ?bf_slice_shl.")]] +[[rc::tactics("all: try solve_goal.")]] +[[rc::lemmas("bf_mask_cons_singleton_nonempty")]] +u64 FIELD_PREP(u64 _mask, u64 _val) +{ + return ((_val) << __bf_shf(_mask)) & (_mask); +} + +/* asm/kvm_pgtable.h */ + +typedef u64 kvm_pte_t; +typedef u64 phys_addr_t; + +/** + * enum kvm_pgtable_prot - Page-table permissions and attributes. + * @KVM_PGTABLE_PROT_X: Execute permission. + * @KVM_PGTABLE_PROT_W: Write permission. + * @KVM_PGTABLE_PROT_R: Read permission. + * @KVM_PGTABLE_PROT_DEVICE: Device attributes. + */ +// enum kvm_pgtable_prot { +// KVM_PGTABLE_PROT_X = BIT(0), +// KVM_PGTABLE_PROT_W = BIT(1), +// KVM_PGTABLE_PROT_R = BIT(2), +// KVM_PGTABLE_PROT_DEVICE = BIT(3), +// }; +typedef u64 kvm_pgtable_prot; +#define KVM_PGTABLE_PROT_X BIT(0) +#define KVM_PGTABLE_PROT_W BIT(1) +#define KVM_PGTABLE_PROT_R BIT(2) +#define KVM_PGTABLE_PROT_DEVICE BIT(3) + +/** + * struct kvm_pgtable_mm_ops - Memory management callbacks. + * @zalloc_page: Allocate a zeroed memory page. + * @zalloc_pages_exact: Allocate an exact number of zeroed memory pages. + * @free_pages_exact: Free an exact number of memory pages. + * @get_page: Increment the refcount on a page. + * @put_page: Decrement the refcount on a page. + * @page_count: Returns the refcount of a page. + * @phys_to_virt: Convert a physical address into a virtual address. + * @virt_to_phys: Convert a virtual address into a physical address. + */ +struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops { + // void* (*zalloc_page)(void *arg); + // void* (*zalloc_pages_exact)(size_t size); + // void (*free_pages_exact)(void *addr, size_t size); + // void (*get_page)(void *addr); + // void (*put_page)(void *addr); + // int (*page_count)(void *addr); + // void* (*phys_to_virt)(phys_addr_t phys); + [[rc::field("function_ptr<{fn(∀ (p, a) : loc * Z; p @ &own (a @ int u64); True) → ∃ () : (), (mm_ops.(virt_to_phys) a) @ bitfield_raw u64; True}>")]] + phys_addr_t (*virt_to_phys)(void *addr); +}; + +/* asm/memory.h */ + +#define MT_NORMAL 0 +#define MT_DEVICE_nGnRE 5 + +// pgtable.c + +#define KVM_PGTABLE_MAX_LEVELS 4U +#define KVM_PTE_VALID BIT(0) +#define KVM_PTE_TYPE BIT(1) +#define KVM_PTE_TYPE_BLOCK 0 +#define KVM_PTE_TYPE_PAGE 1 +#define KVM_PTE_TYPE_TABLE 1 +#define KVM_PTE_ADDR_MASK GENMASK(47, PAGE_SHIFT) +#define KVM_PTE_ADDR_51_48 GENMASK(15, 12) +#define KVM_PTE_LEAF_ATTR_LO GENMASK(11, 2) +#define KVM_PTE_LEAF_ATTR_LO_S1_ATTRIDX GENMASK(4, 2) +#define KVM_PTE_LEAF_ATTR_LO_S1_AP GENMASK(7, 6) +#define KVM_PTE_LEAF_ATTR_LO_S1_AP_RO 3 +#define KVM_PTE_LEAF_ATTR_LO_S1_AP_RW 1 +#define KVM_PTE_LEAF_ATTR_LO_S1_SH GENMASK(9, 8) +#define KVM_PTE_LEAF_ATTR_LO_S1_SH_IS 3 +#define KVM_PTE_LEAF_ATTR_LO_S1_AF BIT(10) +// #define KVM_PTE_LEAF_ATTR_LO_S2_MEMATTR GENMASK(5, 2) +// #define KVM_PTE_LEAF_ATTR_LO_S2_S2AP_R BIT(6) +// #define KVM_PTE_LEAF_ATTR_LO_S2_S2AP_W BIT(7) +// #define KVM_PTE_LEAF_ATTR_LO_S2_SH GENMASK(9, 8) +// #define KVM_PTE_LEAF_ATTR_LO_S2_SH_IS 3 +// #define KVM_PTE_LEAF_ATTR_LO_S2_AF BIT(10) +#define KVM_PTE_LEAF_ATTR_HI GENMASK(63, 51) +#define KVM_PTE_LEAF_ATTR_HI_S1_XN BIT(54) +// #define KVM_PTE_LEAF_ATTR_HI_S2_XN BIT(54) + +[[rc::parameters("pte : Pte")]] +[[rc::args("pte @ bitfield")]] +[[rc::requires("{bitfield_wf pte}")]] +[[rc::returns("{pte_valid pte} @ boolean")]] +static bool kvm_pte_valid(kvm_pte_t pte) +{ + // TODO: remove 0 != once issue #45 is fixed + return 0 != (pte & KVM_PTE_VALID); +} + +[[rc::parameters("pte : Pte", "level : Z")]] +[[rc::args("pte @ bitfield", "level @ int")]] +[[rc::requires("{bitfield_wf pte}")]] +[[rc::returns("{if bool_decide (level = max_level - 1) then false \ + else if negb (pte_valid pte) then false \ + else bool_decide (pte_type pte = pte_type_table)} @ boolean")]] +[[rc::tactics("all: simpl_bool_hyp.")]] +static bool kvm_pte_table(kvm_pte_t pte, u32 level) +{ + if (level == KVM_PGTABLE_MAX_LEVELS - 1) + return false; + if (!kvm_pte_valid(pte)) + return false; + return FIELD_GET(KVM_PTE_TYPE, pte) == KVM_PTE_TYPE_TABLE; +} + +[[rc::parameters("pte : Pte", "p : loc")]] +[[rc::args("p @ &own>")]] +[[rc::requires("{bitfield_wf pte}")]] +[[rc::ensures("own p : {pte_set_invalid pte} @ bitfield")]] +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 @ int")]] +[[rc::returns("{mk_pte_addr (addr_of pa)} @ bitfield")]] +static kvm_pte_t kvm_phys_to_pte(u64 pa) +{ + kvm_pte_t pte = pa & KVM_PTE_ADDR_MASK; + + if (PAGE_SHIFT == 16) // always false given PAGE_SHIFT == 12 + pte |= FIELD_PREP(KVM_PTE_ADDR_51_48, pa >> 48); + + return pte; +} + +[[rc::parameters("p : loc", "q : loc", "o : loc", "pte : Pte", "va : Z", "mm_ops : mm_callbacks")]] +[[rc::args("p @ &own>", "q @ &own>", + "o @ &own")]] +[[rc::requires("{bitfield_wf pte}", "{pte_valid pte}")]] +[[rc::exists("pa : Z")]] +[[rc::ensures("{mm_ops.(virt_to_phys) va = pa}")]] +[[rc::ensures("own p : { {| pte_valid := true; pte_type := pte_type_table; pte_leaf_attr_lo := 0; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := 0 |} } @ bitfield")]] +static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp, + struct kvm_pgtable_mm_ops *mm_ops) +{ + kvm_pte_t old = *ptep, pte = kvm_phys_to_pte(mm_ops->virt_to_phys(childp)); + pte |= FIELD_PREP(KVM_PTE_TYPE, KVM_PTE_TYPE_TABLE); + pte |= KVM_PTE_VALID; + WARN_ON(kvm_pte_valid(old)); + // smp_store_release(ptep, pte); + *ptep = pte; +} + +[[rc::parameters("p : loc", "pte : Pte", "pa : Z", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]] +[[rc::args("p @ &own>", "pa @ int", "attr @ bitfield", "level @ int")]] +[[rc::requires("{bitfield_wf pte}", "{bitfield_wf attr}")]] +[[rc::requires("{type = (if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block)}")]] +[[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 (bitfield_repr pte = bitfield_repr pte1) else true} @ boolean")]] +[[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitfield")]] +[[rc::tactics("all: simpl_bool_hyp.")]] +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 [[rc::refined_by("phys : Z", "attr : Attr", "mm_ops : mm_callbacks", "o : loc")]] hyp_map_data { + [[rc::field("phys @ int")]] + u64 phys; + [[rc::field("attr @ bitfield")]] + kvm_pte_t attr; + [[rc::field("o @ &own")]] + struct kvm_pgtable_mm_ops *mm_ops; +}; + +[[rc::parameters("prot : Prot", "phys : Z", "a : Attr", "attr : Attr", + "mtype : Z", "ap : Z", "xn : bool", "err : bool", + "mm_ops : mm_callbacks", "o : loc", "d : loc")]] +[[rc::args("prot @ bitfield", "d @ &own<{(phys, a, mm_ops, o)} @ hyp_map_data>")]] +[[rc::requires("{bitfield_wf prot}")]] +[[rc::requires("{mtype = (if prot_device prot then mtype_device else mtype_normal)}")]] +[[rc::requires("{ap = (if prot_w prot then ap_rw else ap_ro)}")]] +[[rc::requires("{xn = negb (prot_x prot)}")]] +[[rc::requires("{err = negb (prot_r prot) || (prot_x prot && (prot_w prot || prot_device prot))}")]] +[[rc::requires("{attr = {| attr_lo_s1_attridx := mtype; attr_lo_s1_ap := ap; attr_lo_s1_sh := sh_is; attr_lo_s1_af := true; attr_hi_s1_xn := xn |} }")]] +[[rc::returns("{if err then -err_code else 0} @ int")]] +[[rc::ensures("own d : {if err then (phys, a, mm_ops, o) else (phys, attr, mm_ops, o)} @ hyp_map_data")]] +[[rc::tactics("all: try congruence.")]] +[[rc::tactics("all: simpl_bool_hyp.")]] +static int hyp_map_set_prot_attr(kvm_pgtable_prot prot, struct hyp_map_data *data) +{ + // TODO: remove 0 != once issue #45 is fixed + bool device = 0 != (prot & KVM_PGTABLE_PROT_DEVICE); + u32 mtype = device ? MT_DEVICE_nGnRE : MT_NORMAL; + kvm_pte_t attr = FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_ATTRIDX, mtype); + u32 sh = KVM_PTE_LEAF_ATTR_LO_S1_SH_IS; + u32 ap = (prot & KVM_PGTABLE_PROT_W) ? KVM_PTE_LEAF_ATTR_LO_S1_AP_RW : + KVM_PTE_LEAF_ATTR_LO_S1_AP_RO; + if (!(prot & KVM_PGTABLE_PROT_R)) + return -EINVAL; + if (prot & KVM_PGTABLE_PROT_X) { + if (prot & KVM_PGTABLE_PROT_W) + return -EINVAL; + if (device) + return -EINVAL; + } else { + attr |= KVM_PTE_LEAF_ATTR_HI_S1_XN; + } + attr |= FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_AP, ap); + attr |= FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_SH, sh); + attr |= KVM_PTE_LEAF_ATTR_LO_S1_AF; + data->attr = attr; + return 0; +} diff --git a/linux/casestudies/proofs/pgtable/pgtable_lemmas.v b/linux/casestudies/proofs/pgtable/pgtable_lemmas.v new file mode 100644 index 0000000000000000000000000000000000000000..107c6f45b520d4db23ca548be8d6ca3b0c8bde3c --- /dev/null +++ b/linux/casestudies/proofs/pgtable/pgtable_lemmas.v @@ -0,0 +1,158 @@ +From refinedc.typing Require Import typing. + +(* pte *) + +Record Pte := { + pte_valid : bool; + pte_type : Z; + pte_leaf_attr_lo : Z; + pte_addr : Z; + pte_undef : Z; + pte_leaf_attr_hi : Z; +}. + +Definition pte_set_invalid (pte : Pte) : Pte := {| + pte_valid := false; + pte_type := pte_type pte; + pte_leaf_attr_lo := pte_leaf_attr_lo pte; + pte_addr := pte_addr pte; + pte_undef := pte_undef pte; + pte_leaf_attr_hi := pte_leaf_attr_hi pte; +|}. + +Definition mk_pte_addr (a : Z) : Pte := {| + pte_valid := false; + pte_type := 0; + pte_leaf_attr_lo := 0; + pte_addr := a; + pte_undef := 0; + pte_leaf_attr_hi := 0; +|}. + +Definition pte_repr (p : Pte) : Z := + bf_cons 0 1 (Z_of_bool $ pte_valid p) $ + bf_cons 1 1 (pte_type p) $ + bf_cons 2 10 (pte_leaf_attr_lo p) $ + bf_cons 12 36 (pte_addr p) $ + bf_cons 48 3 (pte_undef p) $ + bf_cons 51 13 (pte_leaf_attr_hi p) $ + bf_nil. + +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_undef p < 2^3 ∧ + 0 ≤ pte_leaf_attr_hi p < 2^13. + +Global Instance Pte_BitfieldDesc : BitfieldDesc Pte := {| + bitfield_it := u64; + bitfield_repr := pte_repr; + bitfield_wf := pte_wf; +|}. + +Definition addr_of (n : Z) : Z := + bf_slice 12 36 n. + +(* pte attr *) + +Record Attr := { + attr_lo_s1_attridx : Z; + attr_lo_s1_ap : Z; + attr_lo_s1_sh : Z; + attr_lo_s1_af : bool; + attr_hi_s1_xn : bool; +}. + +Definition attr_repr (a : Attr) : Z := + bf_cons 2 2 (attr_lo_s1_attridx a) $ + bf_cons 6 2 (attr_lo_s1_ap a) $ + bf_cons 8 2 (attr_lo_s1_sh a) $ + bf_cons 10 1 (Z_of_bool $ attr_lo_s1_af a) $ + bf_cons 54 1 (Z_of_bool $ attr_hi_s1_xn a) + bf_nil. + +Arguments attr_repr _/. + +Definition attr_wf (a : Attr) : Prop := + 0 ≤ attr_lo_s1_attridx a < 2^2 ∧ + 0 ≤ attr_lo_s1_ap a < 2^2 ∧ + 0 ≤ attr_lo_s1_sh a < 2^2 ∧ + 0 ≤ Z_of_bool $ attr_lo_s1_af a < 2^1 ∧ + 0 ≤ Z_of_bool $ attr_hi_s1_xn a < 2^1. + +Global Instance Attr_BitfieldDesc : BitfieldDesc Attr := {| + bitfield_it := u64; + bitfield_repr := attr_repr; + bitfield_wf := attr_wf; +|}. + +(* pte prot *) + +Record Prot := { + prot_x : bool; + prot_w : bool; + prot_r : bool; + prot_device : bool; +}. + +Definition prot_repr (p : Prot) : Z := + bf_cons 0 1 (Z_of_bool $ prot_x p) $ + bf_cons 1 1 (Z_of_bool $ prot_w p) $ + bf_cons 2 1 (Z_of_bool $ prot_r p) $ + bf_cons 3 1 (Z_of_bool $ prot_device p) $ + bf_nil. + +Arguments prot_repr _/. + +Definition prot_wf (p : Prot) : Prop := + 0 ≤ Z_of_bool $ prot_x p < 2^1 ∧ + 0 ≤ Z_of_bool $ prot_w p < 2^1 ∧ + 0 ≤ Z_of_bool $ prot_r p < 2^1 ∧ + 0 ≤ Z_of_bool $ prot_device p < 2^1. + +Global Instance Prot_BitfieldDesc : BitfieldDesc Prot := {| + bitfield_it := u64; + bitfield_repr := prot_repr; + bitfield_wf := prot_wf; +|}. + +(* struct, const *) + +Record mm_callbacks := { + virt_to_phys : Z → Z; +}. + +Definition max_level : Z := 4. +Definition mtype_device : Z := 5. +Definition mtype_normal : Z := 0. +Definition pte_type_block : Z := 0. +Definition pte_type_page : Z := 1. +Definition pte_type_table : Z := 1. +Definition ap_rw : Z := 1. +Definition ap_ro : Z := 3. +Definition sh_is : Z := 3. +Definition err_code : Z := 22. + +(* tactics TODO: SimplImpl *) + +Ltac simpl_bool_hyp := + repeat (match goal with + | [ H : negb ?b = true |- _ ] => + assert (b = false) by apply negb_true_iff; clear H + | [ H : negb ?b = false |- _ ] => + assert (b = true) by apply negb_false_iff; clear H + | [ H : 0 = Z_of_bool ?b |- _ ] => + assert (b = false) by (by apply Z_of_bool_false); clear H + | [ H : 0 ≠ Z_of_bool ?b |- _ ] => + assert (b = true) by (by apply Z_of_bool_true); clear H + | [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil = 0 |- _ ] => + assert (b = false) by (by apply (bf_cons_bool_singleton_false_iff a b)); clear H + | [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil ≠ 0 |- _ ] => + assert (b = true) by (by apply (bf_cons_bool_singleton_true_iff a b)); clear H + | [ H : ?b = false |- _ ] => try (rewrite !H; clear H) + | [ H : ?b = true |- _ ] => try (rewrite !H; clear H) + end; try solve_goal). diff --git a/theories/lang/bitfield.v b/theories/lang/bitfield.v new file mode 100644 index 0000000000000000000000000000000000000000..0dd61d6cbba908061ef79b0391830a54ae2d19a7 --- /dev/null +++ b/theories/lang/bitfield.v @@ -0,0 +1,403 @@ +From refinedc.lang Require Import base int_type builtins_specs. +From refinedc.lithium Require Import simpl_classes tactics_extend infrastructure Z_bitblast. + +(* raw bit vector constructors *) + +Definition bf_nil : Z := 0. + +Definition bf_cons (a k x : Z) (l : Z) := + Z.lor (x ≪ a) l. + +Definition bf_mask_cons (a k : Z) (l : Z) : Z := + Z.lor (Z.ones k ≪ a) l. + +Definition bf_slice (a k : Z) (bv : Z) : Z := + Z.land (bv ≫ a) (Z.ones k). + +Definition bf_update (a k x : Z) (bv : Z) : Z := + Z.lor (Z.land bv (Z.lnot (Z.ones k ≪ a))) (x ≪ a). + +(* singleton list *) + +Lemma bf_shr_singleton a k x : + 0 ≤ a → (bf_cons a k x bf_nil) ≫ a = x. +Proof. + rewrite /bf_cons /bf_nil => ?. + bitblast. +Qed. + +Lemma bf_cons_bool_singleton_false_iff a b : + 0 ≤ a → + bf_cons a 1 (Z_of_bool b) bf_nil = 0 ↔ b = false. +Proof. + intros. rewrite /bf_cons /bf_nil Z.lor_0_r. + split. + - destruct b; last done. + simplify_eq/=. rewrite Z.shiftl_1_l. + have ? : 2 ^ a ≠ 0 by apply Z.pow_nonzero. + contradiction. + - move => ->. simplify_eq/=. by rewrite Z.shiftl_0_l. +Qed. + +Lemma bf_cons_bool_singleton_true_iff a b : + 0 ≤ a → + bf_cons a 1 (Z_of_bool b) bf_nil ≠ 0 ↔ b = true. +Proof. + intros. rewrite /not bf_cons_bool_singleton_false_iff //. + destruct b; naive_solver. +Qed. + +Lemma bf_mask_cons_singleton a k : + bf_mask_cons a k bf_nil = (Z.ones k) ≪ a. +Proof. + rewrite /bf_mask_cons /bf_nil. + bitblast. +Qed. + +Lemma bf_mask_cons_singleton_nonempty a k : + 0 ≤ a → 0 < k → bf_mask_cons a k bf_nil > 0. +Proof. + intros. + rewrite bf_mask_cons_singleton Z.ones_equiv Z.shiftl_mul_pow2; last lia. + apply Zmult_gt_0_compat. + - suff : 2 ^ 0 < 2 ^ k by lia. + apply Z.pow_lt_mono_r. all: lia. + - suff : 0 < 2 ^ a by lia. + by apply Z.pow_pos_nonneg. +Qed. + +(* Rewriting rules *) + +Lemma bf_land_nil bv : + Z.land bv bf_nil = bf_nil. +Proof. + by rewrite Z.land_0_r. +Qed. + +Lemma bf_land_mask_cons bv a k l : + 0 ≤ a → 0 ≤ k → + Z.land bv (bf_mask_cons a k l) = bf_cons a k (bf_slice a k bv) (Z.land bv l). +Proof. + rewrite /bf_cons /bf_mask_cons /bf_slice => ??. + bitblast. +Qed. + +Lemma bf_land_mask_flip bv a k N : + 0 ≤ a → 0 ≤ k → a + k ≤ N → + 0 ≤ bv < 2 ^ N → + Z.land bv (Z_lunot N (bf_mask_cons a k bf_nil)) = bf_update a k 0 bv. +Proof. + rewrite /bf_mask_cons /bf_update /bf_nil /Z_lunot => ????. + rewrite -Z.land_ones; last lia. + bitblast. + symmetry. apply (Z_bounded_iff_bits_nonneg N bv); lia. +Qed. + +Lemma bf_lor_nil_l bv : + Z.lor bf_nil bv = bv. +Proof. done. Qed. + +Lemma bf_lor_nil_r bv : + Z.lor bv bf_nil = bv. +Proof. + by rewrite Z.lor_0_r. +Qed. + +Lemma bf_lor_update a k x x' dl1 dl2 : + 0 ≤ a → 0 ≤ k → + x = 0 → + Z.lor (bf_cons a k x dl1) (bf_cons a k x' dl2) = bf_cons a k x' (Z.lor dl1 dl2). +Proof. + move => ? ? ->. + rewrite /bf_cons. + bitblast. +Qed. + +Lemma bf_lor_update_ne a1 k1 x1 a2 k2 x2 dl1 dl2 : + 0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 → + (a1 + k1 ≤ a2 ∨ a2 + k2 ≤ a1) → + Z.lor (bf_cons a1 k1 x1 dl1) (bf_cons a2 k2 x2 dl2) = bf_cons a1 k1 x1 (Z.lor dl1 (bf_cons a2 k2 x2 dl2)). +Proof. + rewrite /bf_cons => ?????. + bitblast. +Qed. + +Lemma bf_lor_mask_cons_l a k x dl1 dl2 : + 0 ≤ a → 0 ≤ k → + x = 0 → + Z.lor (bf_mask_cons a k dl1) (bf_cons a k x dl2) = bf_cons a k (Z.ones k) (Z.lor dl1 dl2). +Proof. + move => ? ? ->. + rewrite /bf_cons /bf_mask_cons. + bitblast. +Qed. + +Lemma bf_lor_mask_cons_ne_l a1 k1 x1 a2 k2 dl1 ml : + 0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 → + (a1 + k1 ≤ a2 ∨ a2 + k2 ≤ a1) → + Z.lor (bf_mask_cons a1 k1 ml) (bf_cons a2 k2 x1 dl1) = bf_cons a2 k2 x1 (Z.lor dl1 (bf_mask_cons a1 k1 ml)). +Proof. + rewrite /bf_cons /bf_mask_cons => ?????. + bitblast. +Qed. + +Lemma bf_lor_mask_cons_r a k x dl1 dl2 : + 0 ≤ a → 0 ≤ k → + x = 0 → + Z.lor (bf_cons a k x dl1) (bf_mask_cons a k dl2) = bf_cons a k (Z.ones k) (Z.lor dl1 dl2). +Proof. + move => ? ? ->. + rewrite /bf_cons /bf_mask_cons. + bitblast. +Qed. + +Lemma bf_lor_mask_cons a1 k1 dl1 a2 k2 dl2 : + 0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 → + (a1 + k1 ≤ a2 ∨ a2 + k2 ≤ a1) → + Z.lor (bf_mask_cons a1 k1 dl1) (bf_mask_cons a2 k2 dl2) = bf_mask_cons a1 k1 (Z.lor dl1 (bf_mask_cons a2 k2 dl2)). +Proof. + rewrite /bf_cons /bf_mask_cons => ?????. + bitblast. +Qed. + +Lemma bf_lor_mask_cons_ne_r a1 k1 x1 a2 k2 dl1 ml : + 0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 → + (a1 + k1 ≤ a2 ∨ a2 + k2 ≤ a1) → + Z.lor (bf_cons a1 k1 x1 dl1) (bf_mask_cons a2 k2 ml) = bf_cons a1 k1 x1 (Z.lor dl1 (bf_mask_cons a2 k2 ml)). +Proof. + rewrite /bf_cons /bf_mask_cons => ?????. + bitblast. +Qed. + +Lemma bf_slice_nil a k : + bf_slice a k bf_nil = 0. +Proof. + rewrite /bf_slice /bf_nil. + bitblast. +Qed. + +Definition bf_range_empty a k bv : Prop := + ∀ i, a ≤ i < a + k → Z.testbit bv i = false. + +Lemma bf_range_empty_nil a k : + bf_range_empty a k bf_nil. +Proof. + rewrite /bf_range_empty /bf_nil => i ?. + by rewrite Z.bits_0. +Qed. + +Lemma bf_range_empty_cons a k x l a' k' : + 0 ≤ a → 0 ≤ k → 0 ≤ a' → 0 ≤ k' → + 0 ≤ x < 2^k → + (a + k ≤ a' ∨ a' + k' ≤ a) → + bf_range_empty a' k' (bf_cons a k x l) ↔ bf_range_empty a' k' l. +Proof. + rewrite /bf_range_empty /bf_cons => ???? [??] Hor. + split. + - move => Hl i [??]. + have : Z.testbit (Z.lor (x ≪ a) l) i = false by apply Hl. + rewrite Z.lor_spec Z.shiftl_spec ?Hl; [|lia..]. + by apply orb_false_elim. + - move => Hl i [??]. + rewrite Z.lor_spec Z.shiftl_spec ?Hl; [|lia..]. + simplify_bool_eq. destruct Hor. + + apply (Z_bounded_iff_bits_nonneg k x); lia. + + rewrite Z.testbit_neg_r //. lia. +Qed. + +Lemma bf_slice_cons a k x l : + 0 ≤ a → 0 ≤ k → + 0 ≤ x < 2^k → + bf_range_empty a k l → + bf_slice a k (bf_cons a k x l) = x. +Proof. + rewrite /bf_slice /bf_cons => ??? Hi. + bitblast. + rewrite Hi; [by simplify_bool_eq | lia]. + symmetry. apply (Z_bounded_iff_bits_nonneg k x); lia. +Qed. + +Lemma bf_slice_cons_ne a k x a' k' l : + 0 ≤ a → 0 ≤ k → 0 ≤ a' → 0 ≤ k' → + 0 ≤ x < 2^k → + (a + k ≤ a' ∨ a' + k' ≤ a) → + bf_slice a' k' (bf_cons a k x l) = bf_slice a' k' l. +Proof. + rewrite /bf_slice /bf_cons => ????? [?|?]. + all: bitblast. + have -> : Z.testbit x (i + a' - a) = false + by apply (Z_bounded_iff_bits_nonneg k x); lia. + by simplify_bool_eq. +Qed. + +Lemma bf_update_nil a k x : + bf_update a k x bf_nil = bf_cons a k x bf_nil. +Proof. + rewrite /bf_update /bf_nil /bf_cons. + bitblast. +Qed. + +Lemma bf_update_cons a k x x' dl : + 0 ≤ a → 0 ≤ k → + 0 ≤ x < 2^k → + bf_range_empty a k dl → + bf_update a k x' (bf_cons a k x dl) = bf_cons a k x' dl. +Proof. + rewrite /bf_update /bf_nil /bf_cons => ??? Hi. + bitblast. + + rewrite Hi; [by simplify_bool_eq | lia]. + + have -> : Z.testbit x (i - a) = false + by apply (Z_bounded_iff_bits_nonneg k x); lia. + simplify_bool_eq. by apply orb_comm. +Qed. + +Lemma bf_update_cons_ne a k x a' k' x' dl : + 0 ≤ a → 0 ≤ k → 0 ≤ a' → 0 ≤ k' → + 0 ≤ x < 2^k → + (a + k ≤ a' ∨ a' + k' ≤ a) → + bf_update a' k' x' (bf_cons a k x dl) = bf_cons a k x (bf_update a' k' x' dl). +Proof. + rewrite /bf_update /bf_nil /bf_cons => ????? [?|?]. + all: bitblast. + have -> : Z.testbit x (i - a) = false + by apply (Z_bounded_iff_bits_nonneg k x); lia. + by simplify_bool_eq. +Qed. + +(* rewrite & simpl rules *) +Create HintDb bitfield_rewrite discriminated. + +Hint Rewrite bf_land_nil : bitfield_rewrite. +Hint Rewrite bf_land_mask_cons using can_solve_tac : bitfield_rewrite. +Hint Rewrite bf_land_mask_flip using can_solve_tac : bitfield_rewrite. + +Hint Rewrite bf_lor_nil_l : bitfield_rewrite. +Hint Rewrite bf_lor_nil_r : bitfield_rewrite. +Hint Rewrite bf_lor_update using lia : bitfield_rewrite. +Hint Rewrite bf_lor_update_ne using lia : bitfield_rewrite. +Hint Rewrite bf_lor_mask_cons_l using lia : bitfield_rewrite. +Hint Rewrite bf_lor_mask_cons_ne_l using lia : bitfield_rewrite. +Hint Rewrite bf_lor_mask_cons_r using lia : bitfield_rewrite. +Hint Rewrite bf_lor_mask_cons_ne_r using lia : bitfield_rewrite. +Hint Rewrite bf_lor_mask_cons using lia : bitfield_rewrite. + +Hint Rewrite bf_slice_nil : bitfield_rewrite. +Hint Rewrite bf_slice_cons using can_solve_tac : bitfield_rewrite. +Hint Rewrite bf_slice_cons_ne using lia : bitfield_rewrite. + +Hint Rewrite bf_update_nil : bitfield_rewrite. +Hint Rewrite bf_update_cons using can_solve_tac : bitfield_rewrite. +Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite. + +Definition normalize_bitfield (bv norm : Z) : Prop := bv = norm. +Typeclasses Opaque normalize_bitfield. + +Class NormalizeBitfield (bv norm : Z) : Prop := + normalize_bitfield_proof : bv = norm. + +Global Instance simpl_and_normalize_bitfield bv norm `{!NormalizeBitfield bv norm'} `{!IsProtected norm} : + SimplAnd (normalize_bitfield bv norm) (λ T, norm' = norm ∧ T). +Proof. erewrite normalize_bitfield_proof. done. Qed. + +Global Hint Extern 10 (NormalizeBitfield _ _) => + autorewrite with bitfield_rewrite; exact: eq_refl : typeclass_instances. + +(* Side cond: ∀ i ∈ I, Z.testbit bv i = false. *) +Global Instance bf_range_empty_nil_inst a k : + SimplAnd (bf_range_empty a k bf_nil) (λ T, T). +Proof. + have ? := bf_range_empty_nil. + split; naive_solver. +Qed. + +Global Instance bf_range_empty_cons_inst a k x l a' k' + `{!CanSolve (0 ≤ a ∧ 0 ≤ k ∧ 0 ≤ a' ∧ 0 ≤ k')} + `{!CanSolve (0 ≤ x < 2^k)} + `{!CanSolve (a + k ≤ a' ∨ a' + k' ≤ a)} : + SimplAnd (bf_range_empty a' k' (bf_cons a k x l)) (λ T, bf_range_empty a' k' l ∧ T). +Proof. + unfold CanSolve in *. + have ? := bf_range_empty_cons. + split; naive_solver. +Qed. + +(* Linux macros for bits *) + +Lemma Z_shl_bound a k x N : + 0 ≤ a → 0 ≤ k → a + k ≤ N → + 0 ≤ x < 2 ^ a → + x ≤ x ≪ k ≤ 2 ^ N - 1. +Proof. + intros. rewrite Z.shiftl_mul_pow2; last lia. + destruct (decide (x = 0)) as [->|]. + - rewrite Z.mul_0_l. + have ? : 0 < 2 ^ N. { apply Z.pow_pos_nonneg. all: lia. } + lia. + - split. + + apply Z.le_mul_diag_r; first lia. + suff : 0 < 2 ^ k by lia. + by apply Z.pow_pos_nonneg. + + suff : (x * 2 ^ k) < 2 ^ N by lia. + apply Z.log2_lt_cancel. + rewrite Z.log2_mul_pow2 ?Z.log2_pow2; [|lia..]. + have ? : Z.log2 x < a. { apply Z.log2_lt_pow2. all: lia. } + lia. +Qed. + +Lemma Z_shiftl_1_range i N : + 0 ≤ i < N → 1 ≤ 1 ≪ i ≤ 2 ^ N - 1. +Proof. + intros. + apply (Z_shl_bound 1 _ _ _). all: lia. +Qed. + +Lemma bf_mask_bit i : + 1 ≪ i = bf_mask_cons i 1 bf_nil. +Proof. + rewrite /bf_mask_cons /bf_nil. + bitblast. +Qed. + +Lemma bf_mask_high N k : + 0 ≤ k ≤ N → 2 ^ N - 1 - 1 ≪ k + 1 = bf_mask_cons k (N - k) bf_nil. +Proof. + intros. + rewrite bf_mask_cons_singleton Z.ones_equiv !Z.shiftl_mul_pow2; [|lia..]. + rewrite Z.mul_pred_l -Z.pow_add_r ?Z.sub_add; lia. +Qed. + +Lemma bf_mask_gen h l N : + 0 ≤ l → l < h < N → + Z.land (2 ^ N - 1 - 1 ≪ l + 1) ((2 ^ N - 1) ≫ (N - 1 - h)) = bf_mask_cons l (h - l + 1) bf_nil. +Proof. + intros. + rewrite bf_mask_high /bf_mask_cons /bf_nil; last lia. + have -> : 2 ^ N - 1 = Z.pred (2 ^ N) by lia. + rewrite -Z.ones_equiv. + bitblast. +Qed. + +Lemma Z_least_significant_one_nonempty_mask (a k : Z) : + 0 ≤ a → 0 < k → + Z_least_significant_one (bf_mask_cons a k bf_nil) = a. +Proof. + intros. + apply Z_least_significant_one_sound => //. + rewrite bf_mask_cons_singleton. + split. + - rewrite Z.shiftl_spec ?Z.ones_spec_low //. lia. + - intros. rewrite Z.shiftl_spec ?Z.testbit_neg_r //; lia. +Qed. + +Lemma bf_slice_shl a k x : + 0 ≤ a → 0 < k → + 0 ≤ x < 2^k → + bf_slice a k (x ≪ a) = x. +Proof. + rewrite /bf_slice => ???. + bitblast. + symmetry. apply (Z_bounded_iff_bits_nonneg k x); lia. +Qed. + +(* opaque *) +Global Opaque bf_nil bf_cons bf_mask_cons bf_slice bf_update. diff --git a/theories/lang/builtins_specs.v b/theories/lang/builtins_specs.v new file mode 100644 index 0000000000000000000000000000000000000000..4966f7ac0f50d8161cf58c5ec24543fe0ed1d5e9 --- /dev/null +++ b/theories/lang/builtins_specs.v @@ -0,0 +1,41 @@ +From refinedc.lang Require Import base int_type. +From refinedc.lithium Require Import Z_bitblast. + +(* least significant 1-bit *) + +Definition is_least_significant_one (k n : Z) : Prop := + Z.testbit n k = true ∧ ∀ i, 0 ≤ i < k → Z.testbit n i = false. + +Definition Z_least_significant_one (n : Z) : Z := + if bool_decide (n = 0) then -1 else Z.log2 (Z.land n (-n)). + +Lemma Z_least_significant_one_sound k n : + 0 ≤ k → + is_least_significant_one k n → + Z_least_significant_one n = k. +Proof. + rewrite /is_least_significant_one /Z_least_significant_one => ? [Heq Hlt]. + case_bool_decide; first by + subst; have ? := Z.bits_0 k; congruence. + suff : Z.land n (- n) = 1 ≪ k. + { move => ->. rewrite Z.shiftl_1_l Z.log2_pow2. all: lia. } + apply Z.bits_inj' => i ?. + rewrite Z.land_spec ?Z.shiftl_spec //. + destruct (decide (i = k)) as [->|]; last destruct (decide (i < k)). + - (* i = k *) + have ? : n `mod` 2 ^ k = 0 by apply Z_mod_pow2_zero_iff. + rewrite Z_bits_opp_z ?Heq ?Z_bits_1_0 //; lia. + - (* i < k *) + have ? : n `mod` 2 ^ i = 0. + { apply Z_mod_pow2_zero_iff. + 2: intros; apply Hlt. + all: lia. } + rewrite Z_bits_opp_z ?Hlt ?Z.testbit_neg_r //; lia. + - (* i > k *) + have ? : n `mod` 2 ^ i ≠ 0. + { move => /Z_mod_pow2_zero_iff He. + have Hcontra : Z.testbit n k = false by apply He; lia. + congruence. } + rewrite Z_bits_opp_nz ?Z_bits_1_above //; [|lia..]. + by rewrite andb_negb_r. +Qed. diff --git a/theories/lithium/base.v b/theories/lithium/base.v index 771fdc5134a53cc7239e670da622abdb46ad7ca7..6a6e7106c050774aa960fb1b529f1a911421d9f2 100644 --- a/theories/lithium/base.v +++ b/theories/lithium/base.v @@ -38,6 +38,9 @@ Notation "'[@{' A '}' x ; y ; .. ; z ]" := (@cons A x (@cons A y .. (@cons A z Notation "'[@{' A '}' x ]" := (@cons A x nil) (only parsing) : list_scope. Notation "'[@{' A '}' ]" := (@nil A) (only parsing) : list_scope. +(** More automation for modular arithmetics. *) +Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. + (** * tactics *) Lemma rel_to_eq {A} (R : A → A → Prop) `{!Reflexive R} x y: x = y → R x y. @@ -840,6 +843,12 @@ Proof. by rewrite Z.mod_pow2_bits_low ?Z.lnot_spec. Qed. +Lemma Z_lunot_spec_high bits n k: + (0 ≤ bits ≤ k)%Z → Z.testbit (Z_lunot bits n) k = false. +Proof. + move => ?. by rewrite Z.mod_pow2_bits_high. +Qed. + Lemma Z_lunot_range bits n: (0 ≤ bits → 0 ≤ Z_lunot bits n < 2 ^ bits)%Z. Proof. @@ -847,3 +856,42 @@ Proof. apply: Z.mod_pos_bound. by apply: Z.pow_pos_nonneg. Qed. + +(* bits for `- n` *) +Lemma Z_bits_opp_z n i : + (0 ≤ i)%Z → + (n `mod` 2 ^ i = 0)%Z → + Z.testbit (- n) i = Z.testbit n i. +Proof. + intros. + rewrite !Z.testbit_eqb; [|lia..]. + have ? : (0 < 2 ^ i)%Z by apply Z.pow_pos_nonneg; lia. + rewrite Z.div_opp_l_z; lia. +Qed. + +Lemma Z_bits_opp_nz n i : + (0 ≤ i)%Z → + (n `mod` 2 ^ i ≠ 0)%Z → + Z.testbit (-n) i = negb (Z.testbit n i). +Proof. + intros. + rewrite !Z.testbit_eqb; [|lia..]. + rewrite Z.div_opp_l_nz; lia. +Qed. + +Lemma Z_mod_pow2_zero_iff n k : + (0 ≤ k)%Z → + (n `mod` 2 ^ k = 0)%Z ↔ ∀ i, (0 ≤ i < k)%Z → Z.testbit n i = false. +Proof. + intros. + rewrite -Z.land_ones; last lia. + split. + - move => Hz i ?. + have <- : Z.testbit (Z.land n (Z.ones k)) i = false + by rewrite Hz Z.bits_0. + rewrite Z.land_spec Z.ones_spec_low //. + by simplify_bool_eq. + - move => Hf. + bitblast. + by rewrite Hf. +Qed. diff --git a/theories/typing/automation.v b/theories/typing/automation.v index 909679e52441db454f92e75f146e31f21a99698b..e2e8b09b26022280257225c786eaaecde48cd494 100644 --- a/theories/typing/automation.v +++ b/theories/typing/automation.v @@ -6,9 +6,6 @@ From refinedc.typing Require Import programs function singleton own struct bytes Set Default Proof Using "Type". (** * Registering extensions *) -(** More automation for modular arithmetics. *) -Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations. - (** We use autorewrite for the moment. *) Ltac normalize_tac ::= normalize_autorewrite. (* Goal ∀ l i (x : Z), *) diff --git a/theories/typing/bitfield.v b/theories/typing/bitfield.v new file mode 100644 index 0000000000000000000000000000000000000000..e6d9f2fefeda966f418305a6c7d7d5d95c198bb8 --- /dev/null +++ b/theories/typing/bitfield.v @@ -0,0 +1,322 @@ +From refinedc.lithium Require Import simpl_classes. +From refinedc.lang Require Export bitfield. +From refinedc.typing Require Import programs int. +From refinedc.typing Require Export type. +Set Default Proof Using "Type". + +Section bitfield_raw. + Context `{!typeG Σ}. + + Program Definition bitfield_raw_inner_type (it : int_type) (bv : Z) : type := {| + ty_own β l := (l ◁ₗ{β} bv @ int it)%I; + |}%I. + Next Obligation. + intros. by iApply ty_share. + Qed. + + Definition bitfield_raw (it : int_type) : rtype := {| + rty_type := Z; + rty := bitfield_raw_inner_type it; + |}. + + Global Program Instance rmovable_bitfield_raw it : RMovable (bitfield_raw it) := {| + rmovable bv := {| + ty_has_op_type ot mt := is_int_ot ot it; + ty_own_val v := (v ◁ᵥ bv @ int it)%I + |} + |}. + Next Obligation. + intros. rewrite /ty_own /=. iIntros "Hl". by iApply (ty_aligned with "Hl"). + Qed. + Next Obligation. + intros. iIntros "Hv". by iApply (ty_size_eq with "Hv"). + Qed. + Next Obligation. + intros. rewrite /ty_own /=. iIntros "Hl". by iApply (ty_deref with "Hl"). + Qed. + Next Obligation. + intros. iIntros "Hly Hl Hv". by iApply (ty_ref with "Hly Hl Hv"). + Qed. + Next Obligation. + intros. iIntros "Hv". by iApply (ty_memcast_compat with "Hv"). + Qed. + + Global Program Instance bitfield_raw_copyable bv it : Copyable (bv @ bitfield_raw it). + Next Obligation. + intros. rewrite /ty_own /=. iIntros "Hl". by iApply (copy_shr_acc with "Hl"). + Qed. + +End bitfield_raw. +Notation "bitfield_raw< it >" := (bitfield_raw it) (only printing, format "'bitfield_raw<' it '>'") : printing_sugar. + +Typeclasses Opaque bitfield_raw_inner_type. + +Section bitfield. + + Class BitfieldDesc (R : Type) : Type := { + bitfield_it : int_type; + bitfield_repr : R → Z; + bitfield_wf : R → Prop; + }. + + Context `{!typeG Σ}. + + Program Definition bitfield_inner_type (R : Type) `{BitfieldDesc R} (bv : R) : type := {| + ty_own β l := (l ◁ₗ{β} bitfield_repr bv @ bitfield_raw bitfield_it)%I; + |}%I. + Next Obligation. + intros. by iApply ty_share. + Qed. + + Definition bitfield (R : Type) `{BitfieldDesc R} : rtype := {| + rty_type := R; + rty := bitfield_inner_type R; + |}. + + Global Program Instance rmovable_bitfield R `{BitfieldDesc R} : RMovable (bitfield R) := {| + rmovable bv := {| + ty_has_op_type ot mt := is_int_ot ot bitfield_it; + ty_own_val v := (v ◁ᵥ bitfield_repr bv @ int bitfield_it)%I + |} + |}. + Next Obligation. + intros. rewrite /ty_own /=. iIntros "Hl". by iApply (ty_aligned with "Hl"). + Qed. + Next Obligation. + intros. iIntros "Hv". by iApply (ty_size_eq with "Hv"). + Qed. + Next Obligation. + intros. rewrite /ty_own /=. iIntros "Hl". by iApply (ty_deref with "Hl"). + Qed. + Next Obligation. + intros. iIntros "Hly Hl Hv". by iApply (ty_ref with "Hly Hl Hv"). + Qed. + Next Obligation. + intros. iIntros "Hv". by iApply (ty_memcast_compat with "Hv"). + Qed. + + Global Program Instance bitfield_copyable R `{BitfieldDesc R} bv : Copyable (bv @ bitfield R). + Next Obligation. + intros. rewrite /ty_own /=. iIntros "Hl". by iApply (copy_shr_acc with "Hl"). + Qed. +End bitfield. +Notation "bitfield< R >" := (bitfield R) (only printing, format "'bitfield<' R '>'") : printing_sugar. + +Typeclasses Opaque bitfield_inner_type. + +Section programs. + Context `{!typeG Σ}. + + (* int ↔ bitfield_raw *) + + Lemma subsume_val_int_bitfield_raw T it v n bv : + (⌜n = bv⌝ ∗ T) -∗ subsume (v ◁ᵥ n @ int it) (v ◁ᵥ bv @ bitfield_raw it) T. + Proof. + by iIntros "[-> $] ?". + Qed. + Global Instance subsume_val_int_bitfield_raw_inst it v n bv : SubsumeVal v (n @ int it) (bv @ bitfield_raw it) := + λ T, i2p (subsume_val_int_bitfield_raw T it v n bv). + + Lemma subsume_val_bitfield_raw_int T it v n bv : + (⌜bv = n⌝ ∗ T) -∗ subsume (v ◁ᵥ bv @ bitfield_raw it) (v ◁ᵥ n @ int it) T. + Proof. + by iIntros "[-> $] ?". + Qed. + Global Instance subsume_val_bitfield_raw_int_inst it v n bv : SubsumeVal v (bv @ bitfield_raw it) (n @ int it) := + λ T, i2p (subsume_val_bitfield_raw_int T it v n bv). + + (* typing rules for bitfield_raw *) + + Lemma type_arithop_bitfield_raw it v1 bv1 v2 bv2 T bv op: + arith_op_result it bv1 bv2 op = Some bv → + (⌜bv1 ∈ it⌝ -∗ ⌜bv2 ∈ it⌝ -∗ ⌜arith_op_sidecond it bv1 bv2 bv op⌝ ∗ ∃ norm, + (⌜normalize_bitfield bv norm⌝ ∗ T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -∗ + typed_bin_op v1 (v1 ◁ᵥ bv1 @ bitfield_raw it) v2 (v2 ◁ᵥ bv2 @ bitfield_raw it) op (IntOp it) (IntOp it) T. + Proof. + iIntros "%Hop HT Hv1 Hv2". + iApply type_val_expr_mono_strong. + iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //. + iIntros "Hbv1 Hbv2". + iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]". + iSplitR => //. + iExists _. by iFrame. + Qed. + Global Program Instance type_and_bitfield_raw_inst it v1 bv1 v2 bv2: + TypedBinOpVal v1 (bv1 @ bitfield_raw it)%I v2 (bv2 @ bitfield_raw it)%I AndOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_bitfield_raw it v1 bv1 v2 bv2 T (Z.land bv1 bv2) _ _). + Next Obligation. done. Qed. + Global Program Instance type_or_bitfield_raw_inst it v1 bv1 v2 bv2: + TypedBinOpVal v1 (bv1 @ bitfield_raw it)%I v2 (bv2 @ bitfield_raw it)%I OrOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_bitfield_raw it v1 bv1 v2 bv2 T (Z.lor bv1 bv2) _ _). + Next Obligation. done. Qed. + Global Program Instance type_xor_bitfield_raw_inst it v1 bv1 v2 bv2: + TypedBinOpVal v1 (bv1 @ bitfield_raw it)%I v2 (bv2 @ bitfield_raw it)%I XorOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_bitfield_raw it v1 bv1 v2 bv2 T (Z.lxor bv1 bv2) _ _). + Next Obligation. done. Qed. + Global Program Instance type_shl_bitfield_raw_inst it v1 bv1 v2 bv2: + TypedBinOpVal v1 (bv1 @ bitfield_raw it)%I v2 (bv2 @ bitfield_raw it)%I ShlOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_bitfield_raw it v1 bv1 v2 bv2 T (bv1 ≪ bv2) _ _). + Next Obligation. done. Qed. + Global Program Instance type_shr_bitfield_raw_inst it v1 bv1 v2 bv2: + TypedBinOpVal v1 (bv1 @ bitfield_raw it)%I v2 (bv2 @ bitfield_raw it)%I ShrOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_bitfield_raw it v1 bv1 v2 bv2 T (bv1 ≫ bv2) _ _). + Next Obligation. done. Qed. + + Lemma type_not_bitfield_raw bv it v T: + let bv' := if it_signed it then Z.lnot bv else Z_lunot (bits_per_int it) bv in + (⌜bv ∈ it⌝ -∗ T (i2v bv' it) (t2mt (bv' @ bitfield_raw it))) -∗ + typed_un_op v (v ◁ᵥ bv @ bitfield_raw it)%I (NotIntOp) (IntOp it) T. + Proof. + iIntros "HT Hv". + iApply type_val_expr_mono_strong. + iApply (type_not_int with "[HT] Hv") => //. + iIntros "Hbv". + iDestruct ("HT" with "Hbv") as "?". + iExists _. by iFrame. + Qed. + Global Instance type_not_bitfield_raw_inst bv it v: + TypedUnOpVal v (bv @ bitfield_raw it)%I NotIntOp (IntOp it) := + λ T, i2p (type_not_bitfield_raw bv it v T). + + Lemma type_relop_bitfield_raw it v1 bv1 v2 bv2 T b op : + match op with + | EqOp rit => Some (bool_decide (bv1 = bv2), rit) + | NeOp rit => Some (bool_decide (bv1 ≠ bv2), rit) + | LtOp rit => Some (bool_decide (bv1 < bv2), rit) + | GtOp rit => Some (bool_decide (bv1 > bv2), rit) + | LeOp rit => Some (bool_decide (bv1 <= bv2), rit) + | GeOp rit => Some (bool_decide (bv1 >= bv2), rit) + | _ => None + end = Some (b, i32) → + (⌜bv1 ∈ it⌝ -∗ ⌜bv2 ∈ it⌝ -∗ T (i2v (Z_of_bool b) i32) (t2mt (b @ boolean i32))) -∗ + typed_bin_op v1 (v1 ◁ᵥ bv1 @ bitfield_raw it) v2 (v2 ◁ᵥ bv2 @ bitfield_raw it) op (IntOp it) (IntOp it) T. + Proof. + iIntros "%Hop HT Hv1 Hv2". + iApply type_val_expr_mono_strong. + iApply (type_relop_int_int with "[HT] Hv1 Hv2") => //. + iIntros "Hbv1 Hbv2". + iDestruct ("HT" with "Hbv1 Hbv2") as "?". + iExists _. by iFrame. + Qed. + Global Program Instance type_eq_bitfield_raw_inst it v1 bv1 v2 bv2: + TypedBinOpVal v1 (bv1 @ bitfield_raw it)%I v2 (bv2 @ bitfield_raw it)%I (EqOp i32) (IntOp it) (IntOp it) := + λ T, i2p (type_relop_bitfield_raw it v1 bv1 v2 bv2 T (bool_decide (bv1 = bv2)) _ _). + Next Obligation. done. Qed. + Global Program Instance type_ne_bitfield_raw_inst it v1 bv1 v2 bv2: + TypedBinOpVal v1 (bv1 @ bitfield_raw it)%I v2 (bv2 @ bitfield_raw it)%I (NeOp i32) (IntOp it) (IntOp it) := + λ T, i2p (type_relop_bitfield_raw it v1 bv1 v2 bv2 T (bool_decide (bv1 ≠ bv2)) _ _). + Next Obligation. done. Qed. + + (* bitfield_raw with int *) + + Lemma type_arithop_bitfield_raw_int it v1 bv v2 n T bv' op: + arith_op_result it bv n op = Some bv' → + (⌜bv ∈ it⌝ -∗ ⌜n ∈ it⌝ -∗ ⌜arith_op_sidecond it bv n bv' op⌝ ∗ ∃ norm, + (⌜normalize_bitfield bv' norm⌝ ∗ T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -∗ + typed_bin_op v1 (v1 ◁ᵥ bv @ bitfield_raw it) v2 (v2 ◁ᵥ n @ int it) op (IntOp it) (IntOp it) T. + Proof. + iIntros "%Hop HT Hv1 Hv2". + iApply type_val_expr_mono_strong. + iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //. + iIntros "Hbv1 Hbv2". + iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]". + iSplitR => //. + iExists _. by iFrame. + Qed. + Global Program Instance type_shl_bitfield_raw_int_inst it v1 bv v2 n : + TypedBinOpVal v1 (bv @ bitfield_raw it)%I v2 (n @ int it)%I ShlOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_bitfield_raw_int it v1 bv v2 n T (bv ≪ n) _ _). + Next Obligation. done. Qed. + Global Program Instance type_shr_bitfield_raw_int_inst it v1 bv v2 n : + TypedBinOpVal v1 (bv @ bitfield_raw it)%I v2 (n @ int it)%I ShrOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_bitfield_raw_int it v1 bv v2 n T (bv ≫ n) _ _). + Next Obligation. done. Qed. + + Lemma type_arithop_int_bitfield_raw it v1 n v2 bv T bv' op: + arith_op_result it n bv op = Some bv' → + (⌜n ∈ it⌝ -∗ ⌜bv ∈ it⌝ -∗ ⌜arith_op_sidecond it n bv bv' op⌝ ∗ ∃ norm, + (⌜normalize_bitfield bv' norm⌝ ∗ T (i2v norm it) (t2mt (norm @ bitfield_raw it)))) -∗ + typed_bin_op v1 (v1 ◁ᵥ n @ int it) v2 (v2 ◁ᵥ bv @ bitfield_raw it) op (IntOp it) (IntOp it) T. + Proof. + iIntros "%Hop HT Hv1 Hv2". + iApply type_val_expr_mono_strong. + iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //. + iIntros "Hbv1 Hbv2". + iDestruct ("HT" with "Hbv1 Hbv2") as "[% [%norm [<- ?]]]". + iSplitR => //. + iExists _. by iFrame. + Qed. + Global Program Instance type_and_int_bitfield_raw_inst it v1 n v2 bv : + TypedBinOpVal v1 (n @ int it)%I v2 (bv @ bitfield_raw it)%I AndOp (IntOp it) (IntOp it) := λ T, i2p (type_arithop_int_bitfield_raw it v1 n v2 bv T (Z.land n bv) _ _). + Next Obligation. done. Qed. + + Lemma type_bitfield_raw_is_false it v1 v2 bv T : + (∃ a b, ⌜bv = bf_cons a 1 (Z_of_bool b) bf_nil⌝ ∗ ⌜0 ≤ a⌝ ∗ T (i2v (Z_of_bool (negb b)) i32) (t2mt ((Z_of_bool (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 _. by iFrame. + 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 (Z_of_bool b) bf_nil⌝ ∗ ⌜0 ≤ a⌝ ∗ T (i2v (Z_of_bool b) i32) (t2mt ((Z_of_bool b) @ int i32))) -∗ + typed_bin_op v1 (v1 ◁ᵥ 0 @ int it) v2 (v2 ◁ᵥ bv @ bitfield_raw it) (NeOp 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 -> : 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 _. 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). + + (* typing rules for bitfield: unfold to bitfield_raw *) + + Lemma simplify_hyp_place_bitfield l β R `{BitfieldDesc R} bv T : + (l ◁ₗ{β} bitfield_repr bv @ bitfield_raw bitfield_it -∗ T) -∗ + simplify_hyp (l ◁ₗ{β} bv @ bitfield R) T. + Proof. done. Qed. + Global Instance simplify_hyp_place_bitfield_inst l β R `{BitfieldDesc R} bv : + SimplifyHyp (l ◁ₗ{β} bv @ bitfield R)%I (Some 0%N) := + λ T, i2p (simplify_hyp_place_bitfield l β R bv T). + + Lemma simplify_goal_place_bitfield l β R `{BitfieldDesc R} bv T : + T (l ◁ₗ{β} bitfield_repr bv @ bitfield_raw bitfield_it) -∗ + simplify_goal (l ◁ₗ{β} bv @ bitfield R) T. + Proof. + iIntros "HT". iExists _. iFrame. by iIntros "?". + Qed. + Global Instance simplify_goal_place_bitfield_inst l β R `{BitfieldDesc R} bv : + SimplifyGoal (l ◁ₗ{β} bv @ bitfield R)%I (Some 0%N) := + λ T, i2p (simplify_goal_place_bitfield l β R bv T). + + Lemma simplify_hyp_val_bitfield v R `{BitfieldDesc R} bv T : + (v ◁ᵥ bitfield_repr bv @ bitfield_raw bitfield_it -∗ T) -∗ + simplify_hyp (v ◁ᵥ bv @ bitfield R) T. + Proof. done. Qed. + Global Instance simplify_hyp_val_bitfield_inst v R `{BitfieldDesc R} bv : + SimplifyHypVal v (bv @ bitfield R)%I (Some 0%N) := + λ T, i2p (simplify_hyp_val_bitfield v R bv T). + + Lemma simplify_goal_val_bitfield v R `{BitfieldDesc R} bv T : + T (v ◁ᵥ bitfield_repr bv @ bitfield_raw bitfield_it) -∗ + simplify_goal (v ◁ᵥ bv @ bitfield R) T. + Proof. + iIntros "HT". iExists _. iFrame. by iIntros "?". + Qed. + Global Instance simplify_goal_val_bitfield_inst v R `{BitfieldDesc R} bv : + SimplifyGoalVal v (bv @ bitfield R)%I (Some 0%N) := + λ T, i2p (simplify_goal_val_bitfield v R bv T). + +End programs. diff --git a/theories/typing/programs.v b/theories/typing/programs.v index 6c8331dbf14ea0f839fdb7ca2863046e1ed19db6..0b0f10dd932a76d22112d8e0457a7def81ebfd62 100644 --- a/theories/typing/programs.v +++ b/theories/typing/programs.v @@ -446,6 +446,18 @@ Section proper. iIntros "H Hw HP". iApply "H". by iApply "Hw". Qed. + Lemma type_val_expr_mono_strong e T : + typed_val_expr e (λ v ty, + ∃ (ty' : mtype), subsume (v ◁ᵥ ty) (v ◁ᵥ ty') (T v ty'))%I + -∗ typed_val_expr e T. + Proof. + iIntros "HT". iIntros (Φ) "HΦ". + iApply "HT". iIntros (v ty) "Hv HT". + iDestruct "HT" as (ty') "HT". + iPoseProof ("HT" with "Hv") as "[Hv HT']". + iApply ("HΦ" with "Hv HT'"). + Qed. + (** typed_read_end *) Lemma typed_read_end_mono_strong (a : bool) E1 E2 l β ty ot T: (if a then ∅ else E2) = (if a then ∅ else E1) → diff --git a/theories/typing/typing.v b/theories/typing/typing.v index aa5333716befba018d3ce8bd7456fdc6bb5ec526..b1b43cc9cec1eb8dbfc84b180402285a2e91128d 100644 --- a/theories/typing/typing.v +++ b/theories/typing/typing.v @@ -1,3 +1,3 @@ -From refinedc.typing Require Export programs type int intptr function bytes own struct optional singleton fixpoint automation padded exist immovable constrained union array wand globals tyfold atomic_bool locked tagged_ptr. +From refinedc.typing Require Export programs type int intptr function bytes own struct optional singleton fixpoint automation padded exist immovable constrained union array wand globals tyfold atomic_bool locked tagged_ptr bitfield. Notation "'block{' n }" := (typed_block _ n _ _ _ _) (only printing, format "'block{' n }") : bi_scope.