move bit macros to a seperate file

linux/casestudies/bits.c

+#include "bits.h"
+
+// #define BIT(i) (1UL << (i))
+[[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::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))));
+}
+
+#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::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::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);
+}

linux/casestudies/bits.h

+#include <refinedc.h>
+
+#ifndef LINUX_BITS_H
+#define LINUX_BITS_H
+
+typedef uint64_t u64;
+typedef uint32_t u32;
+
+#define BITS_PER_LONG     (sizeof(long) * 8)
+
+[[rc::parameters("i : Z")]]
+[[rc::args("i @ int<i32>")]]
+[[rc::requires("{0 ≤ i < 64}")]]
+[[rc::returns("{bf_mask_cons i 1 bf_nil} @ bitfield_raw<u64>")]]
+u64 BIT(int i);
+
+[[rc::parameters("h : Z", "l : Z")]]
+[[rc::args("h @ int<i32>", "l @ int<i32>")]]
+[[rc::requires("{0 ≤ l}", "{l < h < 64}")]]
+[[rc::returns("{bf_mask_cons l (h - l + 1) bf_nil} @ bitfield_raw<u64>")]]
+u64 GENMASK(int h, int l);
+
+[[rc::parameters("r : Z", "a : Z", "k : Z", "res : Z")]]
+[[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
+[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
+[[rc::requires("{normalize_bitfield (bf_slice a k r) res}")]]
+[[rc::returns("res @ int<u64>")]]
+u64 FIELD_GET(u64 _mask, u64 _reg);
+
+[[rc::parameters("a : Z", "k : Z", "v : Z")]]
+[[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw<u64>", "v @ int<u64>")]]
+[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}", "{0 ≤ v < 2^k}")]]
+[[rc::returns("{bf_cons a k v bf_nil} @ bitfield_raw<u64>")]]
+u64 FIELD_PREP(u64 _mask, u64 _val);
+
+#endif

linux/casestudies/pgtable.c

 //@rc::import pgtable_lemmas from refinedc.linux.casestudies.pgtable
 
-#include <stddef.h>
-#include <stdint.h>
 #include <stdbool.h>
-#include <refinedc.h>
-
-typedef uint64_t u64;
-typedef uint32_t u32;
+#include "bits.h"
 
 #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<i32>")]]
-[[rc::requires("{0 ≤ i < 64}")]]
-[[rc::returns("{bf_mask_cons i 1 bf_nil} @ bitfield_raw<u64>")]]
-[[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<i32>", "l @ int<i32>")]]
-[[rc::requires("{0 ≤ l}", "{l < h < 64}")]]
-[[rc::returns("{bf_mask_cons l (h - l + 1) bf_nil} @ bitfield_raw<u64>")]]
-[[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<u64>", "r @ bitfield_raw<u64>")]]
-[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
-[[rc::requires("{normalize_bitfield (bf_slice a k r) res}")]]
-[[rc::returns("res @ int<u64>")]]
-[[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<u64>", "v @ int<u64>")]]
-[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}", "{0 ≤ v < 2^k}")]]
-[[rc::returns("{bf_cons a k v bf_nil} @ bitfield_raw<u64>")]]
-[[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;