fix two trust_me, one remaining

linux/casestudies/mt7601u/mac.c

@@ -146,7 +146,7 @@ static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
 }
 
 [[rc::parameters("dev : adapter", "pd : loc", "r : tx_rate", "pr : loc", "nss : Z", "pn : loc",
-    // "band : {fin num_bands}", "ib : ieee_supported_band", 
+    // "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>")]]
@@ -168,7 +168,24 @@ static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
   " 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 by rewrite Z.shiftr_div_pow2; solve_goal.")]]
 [[rc::trust_me]] // TODO: bound sidecond
+/*
+      Global Instance simpl_goal_or_lt_pow2 z1 z2 n `{!CanSolve (0 ≤ n ∧ 0 ≤ z1 ∧ 0 ≤ z2)}:
+        SimplAnd (Z.lor z1 z2 < 2 ^ n) (λ T, z1 < 2 ^ n ∧ z2 < 2 ^ n ∧ T).
+      Proof.
+        unfold CanSolve in *. split.
+        - move => [/Z_bounded_iff_bits_nonneg Hz1 [/Z_bounded_iff_bits_nonneg Hz2 ?]]. split; [|done].
+          apply Z_bounded_iff_bits_nonneg; [lia| apply Z.lor_nonneg;lia |].
+          move => ??. rewrite Z.lor_spec Hz1 ?Hz2 //; lia.
+        - move => [/Z_bounded_iff_bits_nonneg? ?].
+      Admitted.
+      Global Instance simpl_goal_land_lt_pow2 z1 z2 n `{!TCDone (0 ≤ z2 < 2^n)} :
+        SimplAnd (Z.land z1 z2 < 2 ^ n) (λ T, T).
+      Proof.
+        unfold TCDone in *. split; [|naive_solver] => ?. split; [|done].
+      Admitted.
+*/
 u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate *rate, u8 *nss_val,
 	struct ieee80211_rate *r)
 {

linux/casestudies/x86_pgtable.c

@@ -15,6 +15,7 @@
 //@  pte_special       : bool[9]
 //@  pte_uffd_wp       : bool[10]
 //@  pte_soft_dirty       : bool[11]
+//@  pte_address       : integer[12..51]
 //@  pte_dev_map       : bool[58]
 //@  pte_no_exec       : bool[63]
 //@rc::end
@@ -35,11 +36,12 @@ typedef u64 phys_addr_t;
 #define __PHYSICAL_MASK     ((phys_addr_t)((1ULL << __PHYSICAL_MASK_SHIFT) - 1))
 
 #define PAGE_SHIFT          12
-#define PAGE_SIZE           (1 << PAGE_SHIFT)
+#define PAGE_SIZE           (1ULL << PAGE_SHIFT)
 // ~Z.ones 12
 #define PAGE_MASK           (~(PAGE_SIZE-1))
 // GENMASK(51, 12)
-#define PHYSICAL_PAGE_MASK  (((signed long)PAGE_MASK) & __PHYSICAL_MASK)
+// TODO: This cast originally goes to singed long but RefinedC currently does not handle sign extension
+#define PHYSICAL_PAGE_MASK  (((unsigned long)PAGE_MASK) & __PHYSICAL_MASK)
 
 // arch/x86/include/asm/pgtable_64_types.h
 typedef unsigned long pteval_t;
@@ -79,8 +81,7 @@ static inline pte_t native_make_pte(pteval_t val)
 
 [[rc::parameters("p : pte")]]
 [[rc::args("p @ pte_t")]]
-[[rc::returns("p @ bitfield<pte>")]]
-[[rc::trust_me]]
+[[rc::returns("{p <| pte_address := 0 |>} @ bitfield<pte>")]]
 static inline pteval_t pte_flags(pte_t pte)
 {
     return native_pte_val(pte) & PTE_FLAGS_MASK;
@@ -199,7 +200,6 @@ static inline bool pte_global(pte_t pte)
 INPUT_PTE
 IF_PTE_PRESENT
 [[rc::returns("{negb (pte_no_exec p)} @ boolean<bool_it>")]]
-[[rc::trust_me]] // TODO: Z_of_bool (negb _) bound
 static inline bool pte_exec(pte_t pte)
 {
     return !(pte_flags(pte) & _PAGE_NX);