Commit 093ce2fb authored by Paul's avatar Paul
Browse files

bf_cons bound check instances

parent 715a0e11
......@@ -156,7 +156,6 @@ static void mt76_mac_process_tx_rate(struct ieee80211_tx_rate *txrate, u16 rate)
[[rc::ensures("own pd : dev @ mt7601u_dev")]]
[[rc::ensures("own pi : { {| tx_info_flags := flags; tx_info_status := status |} } @ ieee80211_tx_info")]]
[[rc::ensures("own ps : st @ mt76_tx_status")]]
[[rc::tactics("all: try solve_bound.")]]
// [[rc::trust_me]]
static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
struct ieee80211_tx_info *info, struct mt76_tx_status *st)
......@@ -225,7 +224,6 @@ static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
" 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::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)
......@@ -324,7 +322,6 @@ u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate
" rx_status_bw := if bool_decide (rate_bw r ≠ 0) then 3 else rx_status_bw st |}"
" | _ => st"
" end} @ ieee80211_rx_status")]]
[[rc::tactics("all: try solve_bound.")]]
// [[rc::trust_me]]
static void mt76_mac_process_rate(struct ieee80211_rx_status *status, u16 rate)
{
......
......@@ -605,58 +605,3 @@ Record adapter := {
adapter_hw : ieee_hw;
adapter_chan_def : chan_def;
}.
Local Open Scope Z_scope.
Lemma max_int_unsigned_le_lt x (it : int_type) :
it_signed it = false
0 x < 2 ^ (bits_per_int it)
x max_int it.
Proof.
unfold max_int, int_modulus.
case_match; [done | lia].
Qed.
Lemma max_int_u8_le_lt x :
0 x < 2^8 x max_int u8.
Proof.
move => ?. by apply max_int_unsigned_le_lt.
Qed.
Lemma max_int_u16_le_lt x :
0 x < 2^16 x max_int u16.
Proof.
move => ?. by apply max_int_unsigned_le_lt.
Qed.
Lemma max_int_u32_le_lt x :
0 x < 2^32 x max_int u32.
Proof.
move => ?. by apply max_int_unsigned_le_lt.
Qed.
Lemma Z_ones_bound k N :
0 k N
0 Z.ones k < 2 ^ N.
Proof.
move => ?.
rewrite Z.ones_equiv.
split.
- suff : 0 < 2 ^ k by lia.
apply Z.pow_pos_nonneg; lia.
- apply Z.lt_le_trans with (m := 2^k); first lia.
apply Z.pow_le_mono_r; lia.
Qed.
Ltac solve_bound :=
match goal with
| [ |- 0 bf_nil < 2^_ ] => apply bf_nil_in_range; lia
| [ |- 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
end.
......@@ -301,64 +301,125 @@ Proof.
rewrite Hi; [by simplify_bool_eq |lia].
Qed.
(* bound check for bf_nil & bf_cons *)
(* bound check for bf_cons *)
Lemma bf_nil_in_range N :
0 N
0 bf_nil < 2^N.
Lemma Z_ones_bound k N :
0 k 0 N
Z.ones k < 2 ^ N k N.
Proof.
move => ? ?. rewrite Z.ones_equiv.
suff : 2^k 2^N k N by lia.
split; move => Hk.
- apply Z.log2_le_mono in Hk.
rewrite !Z.log2_pow2 in Hk; lia.
- apply Z.pow_le_mono_r; lia.
Qed.
Global Instance Z_ones_bound_inst k N `{!CanSolve (0 k 0 N)} :
SimplAnd (Z.ones k < 2 ^ N) (λ T, k N T).
Proof.
move => ?.
split; first done.
apply Z.pow_pos_nonneg; lia.
unfold CanSolve in *.
have ? := Z_ones_bound.
split; naive_solver.
Qed.
Lemma Z_lor_bound a b N :
Lemma Z_lor_bounded_nonneg a b N :
0 N
0 a < 2^N
0 b < 2^N
0 Z.lor a b < 2^N.
0 a
0 b
Z.lor a b < 2^N a < 2^N b < 2^N.
Proof.
move => HN [? /Z_bounded_iff_bits_nonneg Ha]
[? /Z_bounded_iff_bits_nonneg Hb].
have ? : 0 Z.lor a b by apply Z.lor_nonneg; lia.
split; first done.
apply Z_bounded_iff_bits_nonneg => //.
move => i ?. rewrite Z.lor_spec Ha ?Hb; lia.
move => ? ? ?.
rewrite !Z_bounded_iff_bits_nonneg //; last by apply Z.lor_nonneg.
setoid_rewrite Z.lor_spec.
setoid_rewrite orb_false_iff.
naive_solver.
Qed.
Lemma bf_cons_in_range a k x l N :
Lemma bf_cons_bounded a k x l N :
0 N 0 a 0 k
0 x < 2^k
a + k N
0 l < 2^N
0 bf_cons a k x l < 2^N.
bf_cons a k x l < 2^N l < 2^N.
Proof.
move => ? ? ? ? Hak. rewrite /bf_cons.
destruct (decide (0 l)).
- (* 0 ≤ l *)
rewrite Z.shiftl_mul_pow2 //.
rewrite Z_lor_bounded_nonneg //.
* suff : x * 2 ^ a < 2 ^ N by naive_solver.
apply Z.lt_le_trans with (m := 2^k * 2^a);
[ apply Z.mul_lt_mono_pos_r; [apply Z.pow_pos_nonneg|]; lia
| rewrite -Z.pow_add_r //; apply Z.pow_le_mono_r; lia
].
* apply Z.mul_nonneg_nonneg; first lia.
suff : 0 < 2 ^ a by lia. apply Z.pow_pos_nonneg; lia.
- (* l < 0 *)
have ? : 0 < 2 ^ N by apply Z.pow_pos_nonneg; lia.
suff : Z.lor (x a) l < 0 l < 0 by lia.
rewrite Z.lor_neg. lia.
Qed.
Global Instance bf_cons_bounded_inst a k x l N
`{!CanSolve (0 a 0 k 0 N a + k N)}
`{!CanSolve (0 x < 2^k)} :
SimplAnd (bf_cons a k x l < 2 ^ N) (λ T, l < 2 ^ N T).
Proof.
move => ? ? ? ? Hak ?.
rewrite /bf_cons.
apply Z_lor_bound => //.
rewrite Z.shiftl_mul_pow2; last done.
split.
- apply Z.mul_nonneg_nonneg; first lia.
suff : 0 < 2 ^ a by lia. apply Z.pow_pos_nonneg; lia.
- apply Z.lt_le_trans with (m := 2^k * 2^a).
+ apply Z.mul_lt_mono_pos_r; first apply Z.pow_pos_nonneg.
all: lia.
+ rewrite -Z.pow_add_r //.
apply Z.pow_le_mono_r.
all: lia.
unfold CanSolve in *.
have ? := bf_cons_bounded.
split; naive_solver.
Qed.
Lemma bf_mask_cons_in_range a k l N :
Lemma bf_mask_cons_bounded 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.
bf_mask_cons a k l < 2^N l < 2^N.
Proof.
intros. apply bf_cons_bounded => //. split.
- rewrite Z.ones_equiv.
suff : 0 < 2 ^ k by lia.
apply Z.pow_pos_nonneg; lia.
- by apply Z_ones_bound.
Qed.
Global Instance bf_mask_cons_bounded_inst a k l N
`{!CanSolve (0 a 0 k 0 N a + k N)} :
SimplAnd (bf_mask_cons a k l < 2 ^ N) (λ T, l < 2 ^ N T).
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.
unfold CanSolve in *.
have ? := bf_mask_cons_bounded.
split; naive_solver.
Qed.
(* simpl `_ ≤ max_int uN` to `_ < 2^N` *)
Lemma max_int_unsigned_le_lt x (it : int_type) :
it_signed it = false
x max_int it x < 2 ^ (bits_per_int it).
Proof.
unfold max_int, int_modulus.
case_match => ? //. lia.
Qed.
Global Instance max_int_u8_le_lt x :
SimplBoth (x max_int u8) (x < 2^8).
Proof.
unfold SimplBoth. by apply max_int_unsigned_le_lt.
Qed.
Global Instance max_int_u16_le_lt x :
SimplBoth (x max_int u16) (x < 2^16).
Proof.
unfold SimplBoth. by apply max_int_unsigned_le_lt.
Qed.
Global Instance max_int_u32_le_lt x :
SimplBoth (x max_int u32) (x < 2^32).
Proof.
unfold SimplBoth. by apply max_int_unsigned_le_lt.
Qed.
Global Instance max_int_u64_le_lt x :
SimplBoth (x max_int u64) (x < 2^64).
Proof.
unfold SimplBoth. by apply max_int_unsigned_le_lt.
Qed.
(* rewrite & simpl rules *)
......@@ -470,64 +531,6 @@ 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 :
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment