start removing macros

frontend/ail_to_coq.ml

@@ -204,6 +204,11 @@ let is_macro_annot e =
   | MacroString("rc_macro") :: _ -> true
   | _ -> false
 
+let is_expr_annot e =
+  match macro_annot_to_list e with
+  | MacroString("rc_annot") :: _ -> true
+  | _ -> false
+
 
 (* Getting return and argument types for a function. *)
 let rec get_function_type loc Ctype.(Ctype(_, c_ty)) =
@@ -533,6 +538,14 @@ let rec translate_expr : bool -> op_type option -> ail_expr -> expr =
           locate (Macro(name, args, es, e3))
        | _ -> not_impl loc "wrong macro"
        end
+    | AilEcond(e1,e2,e3) when is_const_0 e1 && is_expr_annot e2 ->
+       begin
+       match macro_annot_to_list e2 with
+       | _ :: MacroString(name) :: _ ->
+         let e3 = translate e3 in
+         locate (AnnotExpr(1, Coq_ident(name), e3))
+       | _ -> not_impl loc "wrong annot expr"
+       end
     | AilEcond(e1,e2,e3)           ->
        let ty = op_type_of_tc (loc_of e1) (tc_of e1) in
        let e1 = translate_expr lval None e1 in

include/refinedc.h

@@ -26,6 +26,8 @@
     [[rc::annot(__VA_ARGS__)]] &(e);                     \
     _Pragma("GCC diagnostic pop")
 
+#define rc_annot_expr(e, ...) (0 ? ("rc_annot", __VA_ARGS__, (e)) : (e))
+
 #define rc_unlock(e) rc_annot(e, "UnlockA")
 #define rc_to_uninit(e) rc_annot(e, "ToUninit")
 #define rc_stop(e) rc_annot(e, "StopAnnot")
@@ -33,6 +35,7 @@
 #define rc_unfold_once(e) rc_annot(e, "UnfoldOnceAnnot")
 #define rc_learn(e) rc_annot(e, "LearnAnnot")
 #define rc_learn_alignment(e) rc_annot(e, "LearnAlignmentAnnot")
+#define rc_reduce_expr(e) rc_annot_expr(e, "ReduceAnnot")
 
 #ifdef RC_ENABLE_FOCUS
 #define RC_FOCUS ,rc::trust_me

linux/casestudies/bits.h

@@ -10,34 +10,78 @@ typedef uint8_t u8;
 
 #define BITS_PER_LONG     (sizeof(long) * 8)
 
-[[rc::parameters("i : Z")]]
-[[rc::args("i @ int<i32>")]]
-[[rc::requires("{0 ≤ i < 64}")]]
-[[rc::returns("{bf_cons (range_of i 1) (bf_mask 1) bf_nil} @ bitfield_raw<u64>")]]
-[[rc::trust_me]]
-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_cons (range_of l (h - l + 1)) (bf_mask (h - l + 1)) bf_nil} @ bitfield_raw<u64>")]]
-[[rc::trust_me]]
-u64 GENMASK(int h, int l);
-
-[[rc::parameters("r : tm", "a : Z", "k : Z", "norm : tm")]]
-[[rc::args("{bf_cons (range_of a k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
-[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
-[[rc::requires("{normalize (bf_slice (range_of a k) r) = norm}")]]
-[[rc::returns("{bf_to_Z norm u64} @ int<u64>")]]
-[[rc::ensures("{0 ≤ (bf_to_Z norm u64) < 2 ^ k}")]]
-[[rc::trust_me]]
-u64 FIELD_GET(u64 _mask, u64 _reg);
-
-[[rc::parameters("a : Z", "k : Z", "v : Z")]]
-[[rc::args("{bf_cons (range_of a k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "v @ int<u64>")]]
-[[rc::requires("{a + k ≤ 64}", "{0 ≤ v < 2^k}")]]
-[[rc::returns("{bf_cons (range_of a k) (bf_val v) bf_nil} @ bitfield_raw<u64>")]]
-[[rc::trust_me]]
-u64 FIELD_PREP(u64 _mask, u64 _val);
+#define BIT(i) (1UL << (i))
+// [[rc::parameters("i : Z")]]
+// [[rc::args("i @ int<i32>")]]
+// [[rc::requires("{0 ≤ i < 64}")]]
+// [[rc::returns("{bf_cons (range_of i 1) (bf_mask 1) bf_nil} @ bitfield_raw<u64>")]]
+// [[rc::trust_me]]
+// u64 BIT(int 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) \
+    rc_reduce_expr(((~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_cons (range_of l (h - l + 1)) (bf_mask (h - l + 1)) bf_nil} @ bitfield_raw<u64>")]]
+// [[rc::trust_me]]
+// u64 GENMASK(int h, int l);
+
+#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)); \
+    })
+*/
+#define FIELD_GET(_mask, _reg)        \
+  (typeof(_mask))(((_reg) & (_mask)) >> __bf_shf(_mask))
+
+// [[rc::parameters("r : tm", "a : Z", "k : Z", "norm : tm")]]
+// [[rc::args("{bf_cons (range_of a k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
+// [[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
+// [[rc::requires("{normalize (bf_slice (range_of a k) r) = norm}")]]
+// [[rc::returns("{bf_to_Z norm u64} @ int<u64>")]]
+// [[rc::ensures("{0 ≤ (bf_to_Z norm u64) < 2 ^ k}")]]
+// [[rc::trust_me]]
+// u64 FIELD_GET(u64 _mask, u64 _reg);
+
+/**
+ * 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);    \
+    })
+*/
+#define FIELD_PREP(_mask, _val)                 \
+    ((typeof(_mask))(_val) << __bf_shf(_mask)) & (_mask)
+// [[rc::parameters("a : Z", "k : Z", "v : Z")]]
+// [[rc::args("{bf_cons (range_of a k) (bf_mask k) bf_nil} @ bitfield_raw<u64>", "v @ int<u64>")]]
+// [[rc::requires("{a + k ≤ 64}", "{0 ≤ v < 2^k}")]]
+// [[rc::returns("{bf_cons (range_of a k) (bf_val v) bf_nil} @ bitfield_raw<u64>")]]
+// [[rc::trust_me]]
+// u64 FIELD_PREP(u64 _mask, u64 _val);
 
 #endif

theories/lang/bitfield.v

 From refinedc.lang Require Import base int_type.
-From refinedc.lithium Require Import simpl_classes.
+From refinedc.lithium Require Import simpl_classes Z_bitblast.
 From refinedc.mask_core Require Export calculus confluence provability typecheck.
 From refinedc.mask_core Require Import semantics safety.
 
@@ -220,6 +220,90 @@ Proof.
   rewrite !normalize_preserves_eval //.
 Qed.
 
+(** * Typeclasses to convert integers to bitfields *)
+Class BfIsMask (n : Z) (it : int_type) (t : tm) : Prop := {
+    bf_is_mask_proof : n = bf_to_Z t it
+}.
+Global Hint Mode BfIsMask + + - : typeclass_instances.
+
+Lemma bf_is_mask_Z_to_bit_ranges n it s l:
+  Z_to_bit_ranges n = [(s, S l)] →
+  n = bf_to_Z (bf_cons (s, l) (bf_mask (S (s, l).2)) bf_nil) it.
+Proof.
+  rewrite /bf_to_Z/=/bitwise.rc.bf_cons/bitwise.rc.bf_nil => /Z_to_bit_ranges_singleton_spec Hbit.
+  bitblast; rewrite Hbit ?bool_decide_eq_true ?bool_decide_eq_false; naive_solver lia.
+Qed.
+
+Lemma bf_is_mask_Z_lor n1 n2 it t1 t2:
+  n1 = bf_to_Z t1 it →
+  n2 = bf_to_Z t2 it →
+  Z.lor n1 n2 = bf_to_Z (bf_or t1 t2) it.
+Proof. move => -> ->. done. Qed.
+
+Ltac solve_bf_is_mask :=
+  repeat match goal with
+         | |- Z.lor _ _ = _ => apply bf_is_mask_Z_lor
+         | |- _ => apply bf_is_mask_Z_to_bit_ranges; evar_safe_vm_compute
+         end.
+
+Global Hint Extern 10 (BfIsMask ?n _ _) =>
+   check_closed n; constructor; solve_bf_is_mask : typeclass_instances.
+
+Class BfIsNegMask (n : Z) (it : int_type) (t : tm) : Prop := {
+    bf_is_neg_mask_proof : n = Z_lunot (bits_per_int it) (bf_to_Z t it)
+}.
+Global Hint Mode BfIsNegMask + + - : typeclass_instances.
+
+Ltac solve_bf_is_neg_mask :=
+  lazymatch goal with
+  | |- Z_lunot _ _ = _ =>
+      apply f_equal_help; [reflexivity|];
+      solve_bf_is_mask
+  end.
+
+Global Hint Extern 10 (BfIsNegMask ?n _ _) =>
+   check_closed n; constructor; solve_bf_is_neg_mask : typeclass_instances.
+
+Class BfFromZ (n : Z) (it : int_type) (t : tm) : Prop := {
+    bf_from_Z_proof : n = bf_to_Z t it
+}.
+Global Hint Mode BfFromZ + + - : typeclass_instances.
+
+Lemma bf_from_Z_land_shiftl z m it s l (n : Z):
+  Z_to_bit_ranges m = [(s, S l)] →
+  n = s →
+  0 ≤ z < 2^(S l) →
+  Z.land (z ≪ n) m = bf_to_Z (bf_cons (s, l) (bf_val z) bf_nil) it.
+Proof. Admitted.
+
+Lemma bf_from_Z_shiftl_1 it (n : Z):
+  1 ≪ n = bf_to_Z (bf_cons (range_of n 1) (bf_val 1) bf_nil) it.
+Proof. Admitted.
+
+Ltac solve_bf_from_Z :=
+  constructor;
+  repeat (
+    match goal with
+    | |- Z.land (_ ≪ _) ?m = bf_to_Z _ _ =>
+        check_closed m; eapply bf_from_Z_land_shiftl; [evar_safe_vm_compute| by vm_compute|lia]
+    | |- _ ≪ ?m = bf_to_Z _ _ =>
+        check_closed m; eapply bf_from_Z_shiftl_1
+    | |- Z.lor _ _ = bf_to_Z _ _ =>
+        eapply bf_is_mask_Z_lor
+    end
+  ).
+
+Global Hint Extern 10 (BfFromZ _ _ _) => solve_bf_from_Z : typeclass_instances.
+
+Class BfEnsureMV (t : tm) (σ : signature) : Prop := {
+    bf_ensure_mv_proof : check_has_ty t (mv σ)
+}.
+Global Hint Mode BfEnsureMV + + : typeclass_instances.
+
+Global Hint Extern 10 (BfEnsureMV _ _) =>
+   constructor; vm_compute; exact: I : typeclass_instances.
+
+(** * Helper Lemmas *)
 (* simpl `_ ≤ max_int uN` to `_ < 2^N` *)
 
 Lemma max_int_unsigned_le_lt x (it : int_type) :

theories/lithium/base.v

@@ -593,6 +593,72 @@ End sep_list.
   Qed.
 End big_op.
 
+(** bitranges *)
+Fixpoint pos_to_bit_ranges (p : positive) (i s l : nat) : list (nat * nat) :=
+  match p with
+  | xH => [(s, S l)]
+  | xO p' => (if (l =? 0)%nat then [] else [(s, l)]) ++ pos_to_bit_ranges p' (S i) (S i) 0
+  | xI p' => pos_to_bit_ranges p' (S i) s (S l)
+  end.
+Definition Z_to_bit_ranges (z : Z) : list (nat * nat) :=
+  match z with
+  | Z0 => []
+  | Z.pos p => pos_to_bit_ranges p 0 0 0
+  | Z.neg _ => []
+  end.
+
+Lemma pos_to_bit_ranges_not_nil p i s l:
+  pos_to_bit_ranges p i s l ≠ [].
+Proof. elim: p i s l => //= ?????. by case_match => /=. Qed.
+
+Lemma pos_to_bit_ranges_singleton_spec_S p i s l r:
+  pos_to_bit_ranges p i s (S l) = [r] →
+  r.1 = s ∧ (S l < r.2)%nat ∧ (∀ n, Pos.testbit p n ↔ (n < N.of_nat r.2 - N.of_nat (S l))%N).
+Proof.
+  elim: p i s l r => //=.
+  - move => p IH i s l r /IH[?[? Hn]]; subst. split_and!; [done|lia|] => n.
+    destruct n.
+    + split; [|done] => ?. lia.
+    + rewrite Hn. lia.
+  - move => p IH i s l r [? /pos_to_bit_ranges_not_nil?//].
+  - move => ? s l r [<-]. split_and!; [done|simpl;lia|] => n. cbn [snd].
+    destruct n; split => //; lia.
+Qed.
+
+Lemma pos_to_bit_ranges_singleton_spec_0 p i r:
+  pos_to_bit_ranges p i i 0 = [r] →
+  i ≤ r.1 ∧ ∀ n, Pos.testbit p n ↔ (N.of_nat r.1 - N.of_nat i ≤ n ∧ n < N.of_nat r.1 + N.of_nat r.2 - N.of_nat i)%N.
+Proof.
+  elim: p i r => /=.
+  - move => p IH i r /pos_to_bit_ranges_singleton_spec_S[?[? Hn]]; subst. split; [done|] => n.
+    destruct n; rewrite ?Hn; split => //; lia.
+  - move => p IH i r /IH [? Hn]. split; [lia|] => n.
+    destruct n. { split => //; lia. }
+    rewrite Hn. lia.
+  - move => i r [<-]/=. split;[lia|] => n.
+    destruct n; split => //; lia.
+Qed.
+
+Lemma pos_to_bit_ranges_singleton_spec p r n:
+  pos_to_bit_ranges p 0 0 0 = [r] →
+  Pos.testbit p n ↔ (N.of_nat r.1 ≤ n ∧ n < N.of_nat r.1 + N.of_nat r.2)%N.
+Proof. move => /pos_to_bit_ranges_singleton_spec_0[? ->]. lia. Qed.
+
+Lemma Z_testbit_pos_testbit p n:
+  (0 ≤ n)%Z →
+  Z.testbit (Z.pos p) n = Pos.testbit p (Z.to_N n).
+Proof. by destruct n, p. Qed.
+
+Lemma Z_to_bit_ranges_singleton_spec z n r:
+  (0 ≤ n)%Z →
+  Z_to_bit_ranges z = [r] →
+  Z.testbit z n = bool_decide (r.1 ≤ n ∧ n < r.1 + r.2)%Z.
+Proof.
+  destruct z => //= ? /pos_to_bit_ranges_singleton_spec Hbit. apply eq_bool_prop_intro.
+  rewrite Z_testbit_pos_testbit // bool_decide_spec Hbit.
+  naive_solver lia.
+Qed.
+
 (** * power_of_two and factor2  *)
 Definition is_power_of_two (n : nat) := ∃ m : nat, n = (2^m)%nat.
 Arguments is_power_of_two : simpl never.

theories/typing/annotations.v

@@ -19,3 +19,6 @@ Inductive learn_alignment_annot : Type :=
   LearnAlignmentAnnot.
 
 Inductive LockAnnot : Type := LockA | UnlockA.
+
+Inductive reduce_annot : Type :=
+  ReduceAnnot.

theories/typing/bitfield.v

@@ -272,6 +272,54 @@ Section programs.
     TypedBinOpVal v1 (t1 @ bitfield_tpd R)%I v2 (t2 @ bitfield_raw it)%I AndOp (IntOp it) (IntOp it) :=
       λ T, i2p (type_and_bitfield_tpd_raw T R it v1 v2 t1 t2).
 
+  Lemma type_and_bitfield_tpd_int_mask T R `{BitfieldDesc R} n it t1 t2 `{!BfIsMask n it t2} `{!BfEnsureMV t2 bitfield_sig} v1 v2 :
+    (let norm := normalize (bf_and t1 t2) in
+      T (i2v (bf_to_Z norm bitfield_it) bitfield_it) (t2mt (norm @ bitfield_tpd R))) -∗
+    typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd R) v2 (v2 ◁ᵥ n @ int it) AndOp (IntOp it) (IntOp it) T.
+      Proof. Admitted.
+      (*
+    remember (normalize (bf_and t1 t2)) as n eqn:Heqn.
+    iIntros "[% [% HT]] [% Hv1] Hv2".
+    have Hty : has_ty (bf_and t1 t2) (bv bitfield_sig).
+    { econstructor; eauto. by apply ensure_mv_spec. }
+    have Hn : bf_to_Z n bitfield_it = Z.land (bf_to_Z t1 bitfield_it) (bf_to_Z t2 bitfield_it).
+    { rewrite Heqn. by rewrite normalize_preserves_bf_to_Z. }
+    iApply type_val_expr_mono_strong.
+*)
+    (* iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
+    iIntros "_ _". iSplitR => //. iExists _.
+    rewrite /ty_own_val /= Hn.
+    iIntros "?". iFrame. iSplitR.
+    { iPureIntro. rewrite Heqn; by apply normalize_preserves_type. }
+    by rewrite /ty_own_val /= Hn. *)
+  Global Instance type_and_bitfield_tpd_int_mask_inst R `{BitfieldDesc R} n it t1 t2 `{!BfIsMask n it t2} `{!BfEnsureMV t2 bitfield_sig} v1 v2 :
+    TypedBinOpVal v1 (t1 @ bitfield_tpd R)%I v2 (n @ int it)%I AndOp (IntOp it) (IntOp it) :=
+    λ T, i2p (type_and_bitfield_tpd_int_mask T R n it t1 t2 v1 v2).
+
+  Lemma type_and_neg_bitfield_tpd_int_mask T R `{BitfieldDesc R} n it t1 t2 `{!BfIsNegMask n it t2} `{!BfEnsureMV t2 bitfield_sig} v1 v2 :
+    (let norm := normalize (bf_and_neg t1 t2) in
+      T (i2v (bf_to_Z norm bitfield_it) bitfield_it) (t2mt (norm @ bitfield_tpd R))) -∗
+    typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd R) v2 (v2 ◁ᵥ n @ int it) AndOp (IntOp it) (IntOp it) T.
+      Proof. Admitted.
+      (*
+    remember (normalize (bf_and t1 t2)) as n eqn:Heqn.
+    iIntros "[% [% HT]] [% Hv1] Hv2".
+    have Hty : has_ty (bf_and t1 t2) (bv bitfield_sig).
+    { econstructor; eauto. by apply ensure_mv_spec. }
+    have Hn : bf_to_Z n bitfield_it = Z.land (bf_to_Z t1 bitfield_it) (bf_to_Z t2 bitfield_it).
+    { rewrite Heqn. by rewrite normalize_preserves_bf_to_Z. }
+    iApply type_val_expr_mono_strong.
+*)
+    (* iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
+    iIntros "_ _". iSplitR => //. iExists _.
+    rewrite /ty_own_val /= Hn.
+    iIntros "?". iFrame. iSplitR.
+    { iPureIntro. rewrite Heqn; by apply normalize_preserves_type. }
+    by rewrite /ty_own_val /= Hn. *)
+  Global Instance type_and_neg_bitfield_tpd_int_mask_inst R `{BitfieldDesc R} n it t1 t2 `{!BfIsNegMask n it t2} `{!BfEnsureMV t2 bitfield_sig} v1 v2 :
+    TypedBinOpVal v1 (t1 @ bitfield_tpd R)%I v2 (n @ int it)%I AndOp (IntOp it) (IntOp it) :=
+    λ T, i2p (type_and_neg_bitfield_tpd_int_mask T R n it t1 t2 v1 v2).
+
   Lemma type_not_bitfield_raw T it v t :
     (⌜it_signed it = false⌝ ∗ let n := Z_lunot (bits_per_int it) (bf_to_Z t it) in T (i2v n it) (t2mt (t @ bitfield_neg it))) -∗
     typed_un_op v (v ◁ᵥ t @ bitfield_raw it)%I (NotIntOp) (IntOp it) T.
@@ -385,6 +433,30 @@ Section programs.
     TypedBinOpVal v1 (t1 @ bitfield_raw it)%I v2 (t2 @ bitfield_raw it)%I OrOp (IntOp it) (IntOp it) :=
       λ T, i2p (type_or_bitfield_raw T it v1 v2 t1 t2).
 
+  Lemma type_or_bitfield_tpd_int T R `{BitfieldDesc R} n it t1 t2 `{!BfFromZ n it t2} v1 v2 :
+    (let norm := normalize (bf_or t1 t2) in
+      T (i2v (bf_to_Z norm bitfield_it) bitfield_it) (t2mt (norm @ bitfield_tpd R))) -∗
+    typed_bin_op v1 (v1 ◁ᵥ t1 @ bitfield_tpd R) v2 (v2 ◁ᵥ n @ int it) OrOp (IntOp it) (IntOp it) T.
+      Proof. Admitted.
+      (*
+    remember (normalize (bf_and t1 t2)) as n eqn:Heqn.
+    iIntros "[% [% HT]] [% Hv1] Hv2".
+    have Hty : has_ty (bf_and t1 t2) (bv bitfield_sig).
+    { econstructor; eauto. by apply ensure_mv_spec. }
+    have Hn : bf_to_Z n bitfield_it = Z.land (bf_to_Z t1 bitfield_it) (bf_to_Z t2 bitfield_it).
+    { rewrite Heqn. by rewrite normalize_preserves_bf_to_Z. }
+    iApply type_val_expr_mono_strong.
+*)
+    (* iApply (type_arithop_int_int with "[HT] Hv1 Hv2") => //.
+    iIntros "_ _". iSplitR => //. iExists _.
+    rewrite /ty_own_val /= Hn.
+    iIntros "?". iFrame. iSplitR.
+    { iPureIntro. rewrite Heqn; by apply normalize_preserves_type. }
+    by rewrite /ty_own_val /= Hn. *)
+  Global Instance type_or_bitfield_tpd_int_inst R `{BitfieldDesc R} n it t1 t2 `{!BfFromZ n it t2} v1 v2 :
+    TypedBinOpVal v1 (t1 @ bitfield_tpd R)%I v2 (n @ int it)%I OrOp (IntOp it) (IntOp it) :=
+    λ T, i2p (type_or_bitfield_tpd_int T R n it t1 t2 v1 v2).
+
   (* rel op *)
 
   Lemma type_eq_bitfield_tpd T R `{BitfieldDesc R} v1 v2 t1 t2 :
@@ -481,6 +553,17 @@ Section programs.
   Global Instance subsume_place_bitfield_raw_tpd_inst it R `{BitfieldDesc R} l β t t' : SubsumePlace l β (t @ bitfield_raw it) (t' @ bitfield_tpd R) :=
     λ T, i2p (subsume_place_bitfield_raw_tpd T it R l β t t').
 
+  (* TODO: add val instance *)
+  Lemma subsume_place_int_bitfield_tpd T it R `{BitfieldDesc R} l β n t t' `{!BfFromZ n it t}:
+    (tactic_hint (vm_compute_hint (ensure_bv R) t') (λ _,
+      ⌜Forall id (check_has_ty_conditions t' (bv bitfield_sig))⌝ ∗
+      ⌜it = bitfield_it⌝ ∗ ⌜bf_to_Z t bitfield_it = bf_to_Z t' bitfield_it⌝ ∗ T)) -∗
+    subsume (l ◁ₗ{β} n @ int it) (l ◁ₗ{β} t' @ bitfield_tpd R) T.
+  Proof. Admitted.
+  Global Instance subsume_place_int_bitfield_tpd_inst it R `{BitfieldDesc R} l β n t t' `{!BfFromZ n it t} :
+    SubsumePlace l β (n @ int it) (t' @ bitfield_tpd R) :=
+    λ T, i2p (subsume_place_int_bitfield_tpd T it R l β n t t').
+
   Lemma bool_decide_eq_swap {A} (x y : A) `{!Decision (x = y)} `{!Decision (y = x)} :
     bool_decide (x = y) = bool_decide (y = x).
   Proof. (* TODO: is there a simpler way? *)