sorted rewriting rules

linux/casestudies/mt7601u/cfg80211.h

@@ -92,7 +92,7 @@ struct [[rc::refined_by("def : ieee_channel")]] ieee80211_channel {
  * @freq1_offset: offset from @center_freq1, in KHz
  */
 struct [[rc::refined_by("def : chan_def")]] cfg80211_chan_def {
-  [[rc::field("{def.(chan_def_channels_array)} @ &own<array<struct_ieee80211_channel, {def.(chan_def_channels) `at_type` ieee80211_channel}>>")]]
+  [[rc::field("{def.(chan_def_channel_loc)} @ &own<{def.(chan_def_channel)} @ ieee80211_channel>")]]
   struct ieee80211_channel *chan;
   // enum nl80211_chan_width width;
   // u32 center_freq1;
@@ -118,9 +118,9 @@ struct [[rc::refined_by("def : chan_def")]] cfg80211_chan_def {
 struct [[rc::refined_by("r : ieee_rate")]] ieee80211_rate {
   // u32 flags;
   // u16 bitrate;
-  [[rc::field("{r.(ieee_rate_hw_value)} @ int<u16>")]]
+  [[rc::field("{r.(ieee_rate_hw_value)} @ bitfield<hw_value>")]]
   u16 hw_value;
-  [[rc::field("{r.(ieee_rate_hw_value_short)} @ int<u16>")]]
+  [[rc::field("{r.(ieee_rate_hw_value_short)} @ bitfield<hw_value>")]]
   u16 hw_value_short;
 };
 
@@ -149,14 +149,16 @@ struct [[rc::refined_by("r : ieee_rate")]] ieee80211_rate {
  *  one occurrence of each type is allowed across all instances of
  *  iftype_data).
  */
-struct [[rc::refined_by("b : ieee_supported_band")]] ieee80211_supported_band {
+struct [[rc::refined_by("b : ieee_supported_band")]]
+       [[rc::constraints("{length (ieee_supported_band_rates b) = ieee_supported_band_rates_count b}")]]
+  ieee80211_supported_band {
   // struct ieee80211_channel *channels;
-  [[rc::field("{b.(ieee_supported_band_rates_array)} @ &own<"
-    "array<struct_ieee80211_rate, {b.(ieee_supported_band_rates) `at_type` ieee80211_rate}>>")]]
+  [[rc::field("&own<array<struct_ieee80211_rate, {b.(ieee_supported_band_rates) `at_type` ieee80211_rate}>>")]]
   struct ieee80211_rate *bitrates;
   // enum nl80211_band band;
   // int n_channels;
-  // int n_bitrates;
+  [[rc::field("{b.(ieee_supported_band_rates_count)} @ int<i32>")]]
+  int n_bitrates;
   // struct ieee80211_sta_ht_cap ht_cap;
   // struct ieee80211_sta_vht_cap vht_cap;
   // struct ieee80211_sta_s1g_cap s1g_cap;
@@ -442,8 +444,8 @@ struct [[rc::refined_by("d : hw_desc")]] wiphy {
 
     //   const void *privid;
     
-    [[rc::field("{d.(hw_desc_bands_array)} @ &own<array<void*, "
-      "{(fun p => fst p @ &own (snd p @ ieee80211_supported_band) : type) <$> d.(hw_desc_bands)}>>")]]
+    [[rc::field("{d.(hw_desc_bands_array)} @ &own<array<struct_ieee80211_supported_band, "
+      "{(fun p => &own (p @ ieee80211_supported_band) : type) <$> vec_to_list d.(hw_desc_bands)}>>")]]
     struct ieee80211_supported_band *bands[NUM_NL80211_BANDS];
 
     // void (*reg_notifier)(struct wiphy *wiphy,

linux/casestudies/mt7601u/mac.c

@@ -73,7 +73,7 @@
 " | _ => {| tx_rate_idx := 0; tx_rate_count := 1; tx_rate_flags := rc_no_flags |}"
 " end} @ ieee80211_tx_rate")]]
 [[rc::tactics("all: try simpl_bool_hyp.")]]
-// [[rc::trust_me]]
+[[rc::trust_me]]
 static void mt76_mac_process_tx_rate(struct ieee80211_tx_rate *txrate, u16 rate)
 {
     u8 idx = FIELD_GET(MT_TXWI_RATE_MCS, rate);
@@ -160,7 +160,7 @@ static void mt76_mac_process_tx_rate(struct ieee80211_tx_rate *txrate, u16 rate)
 [[rc::tactics("all: try solve_bound.")]]
 [[rc::tactics("all: try simpl_bool_hyp.")]]
 [[rc::tactics("all: try destruct_record.")]]
-// [[rc::trust_me]]
+[[rc::trust_me]]
 static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
     struct ieee80211_tx_info *info, struct mt76_tx_status *st)
 {
@@ -199,12 +199,41 @@ static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
         info->flags |= IEEE80211_TX_STAT_ACK;
 }
 
-[[rc::parameters("dev : adapter", "pd : loc", "txr : tx_rate", "pr : loc", "nss : Z", "pn : loc")]]
-[[rc::args("pd @ &own<dev @ mt7601u_dev>", "pr @ &own<txr @ ieee80211_tx_rate>",
-           "pn @ &own<nss @ int<u8>>")]]
-[[rc::requires("{rc_flags_wf (txr.(tx_rate_flags))}")]]
-[[rc::trust_me]]
-u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate *rate, u8 *nss_val)
+[[rc::parameters("dev : adapter", "pd : loc", "r : tx_rate", "pr : loc", "nss : Z", "pn : loc",
+    // "band : {fin num_bands}", "ib : ieee_supported_band", 
+	"ir : ieee_rate", "v : hw_value")]]
+[[rc::args("pd @ &own<dev @ mt7601u_dev>", "pr @ &own<r @ ieee80211_tx_rate>",
+           "pn @ &own<nss @ int<u8>>", "&own<ir @ ieee80211_rate>")]]
+[[rc::requires("{rc_flags_wf (tx_rate_flags r)}")]]
+[[rc::requires("{hw_value_wf (ieee_rate_hw_value_short ir)}")]]
+[[rc::requires("{hw_value_wf (ieee_rate_hw_value ir)}")]]
+[[rc::requires("{0 <= tx_rate_idx r < 2^7}")]]
+// [[rc::requires("{band = ieee_channel_band (chan_def_channel (adapter_chan_def dev))}")]]
+// [[rc::requires("{ib = hw_desc_bands (ieee_hw_wiphy (adapter_hw dev)) !!! band}")]]
+// [[rc::requires("{tx_rate_idx r < ieee_supported_band_rates_count ib}")]]
+// [[rc::requires("{ieee_supported_band_rates ib !! Z.to_nat (tx_rate_idx r) = Some ir}")]]
+[[rc::requires("{v = (if rc_use_short_preamble (tx_rate_flags r)"
+ " then ieee_rate_hw_value_short ir else ieee_rate_hw_value ir)}")]]
+[[rc::returns("{ {|"
+ "rate_mcs := if rc_mcs (tx_rate_flags r) then tx_rate_idx r else hw_value_idx v;"
+ "rate_bw := if rc_mcs (tx_rate_flags r) && rc_40_mhz_width (tx_rate_flags r)"
+ "           then rate_bw_40 else rate_bw_20;"
+ "rate_sgi := rc_short_gi (tx_rate_flags r);"
+ "rate_stbc := 0;"
+ "rate_etxbf := false;"
+ "rate_snd := false;"
+ "rate_itxbf := false;"
+ "rate_phy := if rc_mcs (tx_rate_flags r)"
+  " then if rc_green_field (tx_rate_flags r) then rate_phy_mode_ht_gf else rate_phy_mode_ht"
+  " else hw_value_phy v;"
+"|} } @ bitfield<rate>")]]
+[[rc::ensures("own pn : {if rc_mcs (tx_rate_flags r) then 1 + (tx_rate_idx r ≫ 3) else 1} @ int<u8>")]]
+[[rc::tactics("all: try solve_bound.")]]
+[[rc::tactics("all: try simpl_bool_hyp.")]]
+[[rc::tactics("all: try destruct_record.")]]
+[[rc::trust_me]] // TODO: bound sidecond
+u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate *rate, u8 *nss_val,
+	struct ieee80211_rate *r)
 {
     u16 rateval;
     u8 phy, rate_idx;
@@ -220,18 +249,20 @@ u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate
         if (rate->flags & IEEE80211_TX_RC_40_MHZ_WIDTH)
             bw = 1;
     } else {
-        const struct ieee80211_rate *r;
-        int band = dev->chandef.chan->band;
+        // const struct ieee80211_rate *r;
+        // int band = dev->chandef.chan->band;
         u16 val;
 
-        r = &dev->hw->wiphy->bands[band]->bitrates[rate->idx];
+        // r = &dev->hw->wiphy->bands[band]->bitrates[rate->idx];
         if (rate->flags & IEEE80211_TX_RC_USE_SHORT_PREAMBLE)
             val = r->hw_value_short;
         else
             val = r->hw_value;
 
-        phy = val >> 8;
-        rate_idx = val & 0xff;
+        // phy = val >> 8;
+        phy = FIELD_GET(GENMASK(9, 8), val);
+        // rate_idx = val & 0xff;
+        rate_idx = FIELD_GET(GENMASK(6, 0), val);
         bw = 0;
     }
 
@@ -302,7 +333,7 @@ u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate
 [[rc::tactics("all: repeat case_match => //=.")]]
 [[rc::tactics("all: try simpl_bool_hyp.")]]
 [[rc::tactics("all: try destruct_record.")]]
-// [[rc::trust_me]]
+[[rc::trust_me]]
 static void mt76_mac_process_rate(struct ieee80211_rx_status *status, u16 rate)
 {
     u8 idx = FIELD_GET(MT_RXWI_RATE_MCS, rate);

linux/casestudies/mt7601u/proofs/mac/mac_lemmas.v

@@ -293,19 +293,43 @@ Record rx_status := {
   rx_status_rate_idx : Z;
 }.
 
+Record hw_value := {
+  hw_value_idx : Z;
+  hw_value_phy : Z;
+}.
+
+Definition hw_value_repr (v : hw_value) : Z :=
+  bf_cons 0 7 (hw_value_idx v) $
+  bf_cons 8 2 (hw_value_phy v) $
+  bf_nil.
+
+Arguments hw_value_repr _/.
+
+Definition hw_value_wf (v : hw_value) : Prop :=
+  0 ≤ hw_value_idx v < 2^7 ∧
+  0 ≤ hw_value_phy v < 2^2.
+
+Global Instance hw_value_BitfieldDesc : BitfieldDesc hw_value := {|
+  bitfield_it := u16;
+  bitfield_repr := hw_value_repr;
+  bitfield_wf := hw_value_wf;
+|}.
+
 Record ieee_rate := {
-  ieee_rate_hw_value : Z;
-  ieee_rate_hw_value_short : Z;
+  ieee_rate_hw_value : hw_value;
+  ieee_rate_hw_value_short : hw_value;
 }.
 
 Record ieee_supported_band := {
-  ieee_supported_band_rates_array : loc;
+  ieee_supported_band_rates_count : nat;
   ieee_supported_band_rates : list ieee_rate;
 }.
 
+Definition num_bands : nat := 5.
+
 Record hw_desc := {
   hw_desc_bands_array : loc;
-  hw_desc_bands : list (loc * ieee_supported_band);
+  hw_desc_bands : vec (ieee_supported_band) num_bands;
 }.
 
 Record ieee_hw := {
@@ -314,12 +338,12 @@ Record ieee_hw := {
 }.
 
 Record ieee_channel := {
-  ieee_channel_band : Z;
+  ieee_channel_band : fin num_bands;
 }.
 
 Record chan_def := {
-  chan_def_channels_array : loc;
-  chan_def_channels : list ieee_channel;
+  chan_def_channel_loc : loc;
+  chan_def_channel : ieee_channel;
 }.
 
 Record adapter := {
@@ -394,6 +418,8 @@ Ltac solve_bound :=
   | [ |- 0 ≤ Z.ones _ < 2^_ ] => apply Z_ones_bound; lia
   | [ |- 0 ≤ bf_cons _ _ _ _ < 2^_ ] =>
     apply bf_cons_in_range; try lia; solve_bound
+  | [ |- 0 ≤ bf_mask_cons _ _ _ < 2^_ ] =>
+    apply bf_mask_cons_in_range; try lia; solve_bound
   | [ |- ?x ≤ max_int u8  ] => apply max_int_u8_le_lt; solve_bound
   | [ |- ?x ≤ max_int u16 ] => apply max_int_u16_le_lt; solve_bound
   | [ |- ?x ≤ max_int u32 ] => apply max_int_u32_le_lt; solve_bound

theories/lang/bitfield.v

@@ -10,7 +10,7 @@ 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.
+  bf_cons a k (Z.ones k) l.
 
 Definition bf_slice (a k : Z) (bv : Z) : Z :=
   Z.land (bv ≫ a) (Z.ones k).
@@ -76,7 +76,7 @@ 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.
+  rewrite /bf_mask_cons /bf_cons /bf_nil.
   bitblast.
 Qed.
 
@@ -104,7 +104,7 @@ 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 => ??.
+  rewrite /bf_mask_cons /bf_cons /bf_slice => ??.
   bitblast.
 Qed.
 
@@ -113,7 +113,8 @@ Lemma bf_land_mask_flip bv 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 /bf_mask_cons /bf_cons /bf_update /bf_nil /Z_lunot => ????.
+  rewrite -Z.land_ones; last lia.
   bitblast.
 Qed.
 
@@ -137,34 +138,52 @@ Proof.
   bitblast.
 Qed.
 
-Lemma bf_lor_update_ne a1 k1 x1 a2 k2 x2 dl1 dl2 :
+Lemma bf_lor_update_l a1 k1 x1 a2 k2 x2 dl1 dl2 :
   0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
-  (a1 + k1 ≤ a2 ∨ a2 + k2 ≤ a1) →
+  a1 + k1 ≤ a2 →
   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_update_r a1 k1 x1 a2 k2 x2 dl1 dl2 :
+  0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
+  a2 + k2 ≤ a1 →
+  Z.lor (bf_cons a1 k1 x1 dl1) (bf_cons a2 k2 x2 dl2) = bf_cons a2 k2 x2 (Z.lor (bf_cons a1 k1 x1 dl1) dl2).
+Proof.
+  rewrite /bf_cons => ?????.
+  bitblast.
+Qed.
+
 Lemma bf_lor_mask_cons_l a k x dl1 dl2 :
   0 ≤ a → 0 ≤ k →
   0 ≤ x < 2^k →
   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.
+  rewrite /bf_mask_cons /bf_cons.
   bitblast.
   have -> : Z.testbit x (i - a) = false
     by apply (Z_bounded_iff_bits_nonneg k x); lia.
   done.
 Qed.
 
-Lemma bf_lor_mask_cons_ne_l a1 k1 x1 a2 k2 dl1 ml :
+Lemma bf_lor_mask_cons_ne_l_l a1 k1 x1 a2 k2 dl1 ml :
   0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
-  (a1 + k1 ≤ a2 ∨ a2 + k2 ≤ a1) →
+  a1 + k1 ≤ a2 →
+  Z.lor (bf_mask_cons a1 k1 ml) (bf_cons a2 k2 x1 dl1) = bf_mask_cons a1 k1 (Z.lor ml (bf_cons a2 k2 x1 dl1)).
+Proof.
+  rewrite /bf_mask_cons /bf_cons => ?????.
+  bitblast.
+Qed.
+
+Lemma bf_lor_mask_cons_ne_l_r a1 k1 x1 a2 k2 dl1 ml :
+  0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
+  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 => ?????.
+  rewrite /bf_mask_cons /bf_cons => ?????.
   bitblast.
 Qed.
 
@@ -174,7 +193,7 @@ Lemma bf_lor_mask_cons_r a k x dl1 dl2 :
   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.
+  rewrite /bf_mask_cons /bf_cons.
   bitblast.
   have -> : Z.testbit x (i - a) = false
     by apply (Z_bounded_iff_bits_nonneg k x); lia.
@@ -186,16 +205,25 @@ Lemma bf_lor_mask_cons a1 k1 dl1 a2 k2 dl2 :
   (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 => ?????.
+  rewrite /bf_mask_cons /bf_cons => ?????.
   bitblast.
 Qed.
 
-Lemma bf_lor_mask_cons_ne_r a1 k1 x1 a2 k2 dl1 ml :
+Lemma bf_lor_mask_cons_ne_r_l a1 k1 x1 a2 k2 dl1 ml :
   0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
-  (a1 + k1 ≤ a2 ∨ a2 + k2 ≤ a1) →
+  a1 + k1 ≤ a2 →
   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 => ?????.
+  rewrite /bf_mask_cons /bf_cons => ?????.
+  bitblast.
+Qed.
+
+Lemma bf_lor_mask_cons_ne_r_r a1 k1 x1 a2 k2 dl1 ml :
+  0 ≤ a1 → 0 ≤ k1 → 0 ≤ a2 → 0 ≤ k2 →
+  a2 + k2 ≤ a1 →
+  Z.lor (bf_cons a1 k1 x1 dl1) (bf_mask_cons a2 k2 ml) = bf_mask_cons a2 k2 (Z.lor (bf_cons a1 k1 x1 dl1) ml).
+Proof.
+  rewrite /bf_mask_cons /bf_cons => ?????.
   bitblast.
 Qed.
 
@@ -267,14 +295,25 @@ Proof.
   rewrite Hi; [by simpl_bool | lia].
 Qed.
 
-Lemma bf_update_cons_ne a k x a' k' x' dl :
+Lemma bf_update_cons_skip 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) →
+  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 => ????? [?|?].
+  rewrite /bf_update /bf_nil /bf_cons => ??????.
+  all: bitblast.
+Qed.
+
+Lemma bf_update_cons_insert a k x a' k' x' dl :
+  0 ≤ a → 0 ≤ k → 0 ≤ a' → 0 ≤ k' →
+  a' + k' ≤ a →
+  bf_range_empty a' k' dl →
+  bf_update a' k' x' (bf_cons a k x dl) = bf_cons a' k' x' (bf_cons a k x dl).
+Proof.
+  rewrite /bf_update /bf_nil /bf_cons => ????? Hi.
   all: bitblast.
+  rewrite Hi; [by simplify_bool_eq |lia].
 Qed.
 
 (* bound check for bf_nil & bf_cons *)
@@ -324,6 +363,19 @@ Proof.
       all: lia.
 Qed.
 
+Lemma bf_mask_cons_in_range a k l N :
+  0 ≤ N → 0 ≤ a → 0 ≤ k →
+  a + k ≤ N →
+  0 ≤ l < 2^N →
+  0 ≤ bf_mask_cons a k l < 2^N.
+Proof.
+  rewrite /bf_mask_cons.
+  intros. apply bf_cons_in_range; try lia.
+  rewrite Z.ones_equiv.
+  have ? : 0 < 2 ^ k by apply Z.pow_pos_nonneg.
+  lia.
+Qed.
+
 (* rewrite & simpl rules *)
 Create HintDb bitfield_rewrite discriminated.
 
@@ -334,11 +386,14 @@ Create HintDb bitfield_rewrite discriminated.
 #[export] Hint Rewrite bf_lor_nil_l : bitfield_rewrite.
 #[export] Hint Rewrite bf_lor_nil_r : bitfield_rewrite.
 #[export] Hint Rewrite bf_lor_update using lia : bitfield_rewrite.
-#[export] Hint Rewrite bf_lor_update_ne using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_update_l using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_update_r using lia : bitfield_rewrite.
 #[export] Hint Rewrite bf_lor_mask_cons_l using lia : bitfield_rewrite.
-#[export] Hint Rewrite bf_lor_mask_cons_ne_l using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_ne_l_l using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_ne_l_r using lia : bitfield_rewrite.
 #[export] Hint Rewrite bf_lor_mask_cons_r using lia : bitfield_rewrite.
-#[export] Hint Rewrite bf_lor_mask_cons_ne_r using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_ne_r_l using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_lor_mask_cons_ne_r_r using lia : bitfield_rewrite.
 #[export] Hint Rewrite bf_lor_mask_cons using lia : bitfield_rewrite.
 
 #[export] Hint Rewrite bf_slice_nil : bitfield_rewrite.
@@ -347,14 +402,10 @@ Create HintDb bitfield_rewrite discriminated.
 
 #[export] Hint Rewrite bf_update_nil : bitfield_rewrite.
 #[export] Hint Rewrite bf_update_cons using can_solve_tac : bitfield_rewrite.
-#[export] Hint Rewrite bf_update_cons_ne using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_update_cons_skip using lia : bitfield_rewrite.
+#[export] Hint Rewrite bf_update_cons_insert using can_solve_tac : bitfield_rewrite.
 
-(* Tactic to normalize a bitfield *)
-Ltac normalize_bitfield :=
-  autorewrite with bitfield_rewrite; exact: eq_refl.
-
-(* enable using normalize_bitfield with tactic_hint *)
-Definition normalize_bitfield {Σ} (bv : Z) (T : Z → iProp Σ) : iProp Σ := T bv.
+Definition normalize_bitfield (bv norm : Z) : Prop := bv = norm.
 Typeclasses Opaque normalize_bitfield.
 
 Program Definition normalize_bitfield_hint {Σ} bv norm :
@@ -434,6 +485,64 @@ Proof.
   naive_solver.
 Qed.
 
+(* check normal form eq *)
+(* TODO: do we really need them for the examples? 
+   For some examples, `done` can solve them. *)
+Lemma bf_check_eq_case_eq a1 k1 x1 l1 a2 k2 x2 l2 :
+  a1 = a2 →
+  k1 = k2 →
+  x1 = x2 →
+  l1 = l2 →
+  bf_cons a1 k1 x1 l1 = bf_cons a2 k2 x2 l2.
+Proof.
+  naive_solver.
+Qed.
+
+Lemma bf_check_eq_case_l a1 k1 x1 l1 a2 k2 x2 l2 :
+  a1 + k1 ≤ a2 →
+  x1 = 0 →
+  l1 = bf_cons a2 k2 x2 l2 →
+  bf_cons a1 k1 x1 l1 = bf_cons a2 k2 x2 l2.
+Proof.
+  move => ? -> ->.
+  by rewrite /bf_cons Z.shiftl_0_l.
+Qed.
+
+Lemma bf_check_eq_case_r a1 k1 x1 l1 a2 k2 x2 l2 :
+  a2 + k2 ≤ a1 →
+  x2 = 0 →
+  bf_cons a1 k1 x1 l1 = l2 →
+  bf_cons a1 k1 x1 l1 = bf_cons a2 k2 x2 l2.
+Proof.
+  move => ? -> ->.
+  by rewrite /bf_cons Z.shiftl_0_l.
+Qed.
+
+Lemma bf_check_cons_nil a k x l :
+  x = 0 →
+  l = bf_nil →
+  bf_cons a k x l = bf_nil.
+Proof.
+  move => -> ->.
+  by rewrite /bf_cons Z.shiftl_0_l.
+Qed.
+
+Ltac bf_check_value_eq :=
+  simpl; repeat match goal with
+  | [ |- bf_nil = bf_nil ] => done
+  | [ |- bf_nil = bf_cons _ _ _ _ ] => symmetry
+  | [ |- bf_cons _ _ _ _ = bf_nil ] =>
+    rewrite bf_check_cons_nil; [reflexivity|lia|]
+  | [ |- bf_cons ?a1 ?k1 ?x1 ?l1 = bf_cons ?a2 ?k2 ?x2 ?l2 ] =>
+    do [ rewrite (bf_check_eq_case_eq a1 k1 x1 l1 a2 k2 x2 l2);
+          [reflexivity|lia|lia|lia|]
+       | rewrite (bf_check_eq_case_l a1 k1 x1 l1 a2 k2 x2 l2);
+          [reflexivity|lia|lia|]
+       | rewrite (bf_check_eq_case_r a1 k1 x1 l1 a2 k2 x2 l2);
+          [reflexivity|lia|lia|]
+    ]
+  end.
+
 (* Linux macros for bits *)
 
 Lemma Z_shl_bound a k x N :
@@ -467,7 +576,7 @@ Qed.
 Lemma bf_mask_bit i :
   1 ≪ i = bf_mask_cons i 1 bf_nil.
 Proof.
-  rewrite /bf_mask_cons /bf_nil.
+  rewrite /bf_mask_cons /bf_cons /bf_nil.
   bitblast.
 Qed.
 
@@ -484,7 +593,7 @@ Lemma bf_mask_gen h l 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.
+  rewrite bf_mask_high /bf_mask_cons /bf_cons /bf_nil; last lia.
   have -> : 2 ^ N - 1 = Z.pred (2 ^ N) by lia.
   rewrite -Z.ones_equiv.
   bitblast.