Commit 715a0e11 authored by Paul's avatar Paul
Browse files

remove simpl_bool_hyp; instead create SimplForall SimplExist instances

parent 93b59897
......@@ -72,8 +72,7 @@
" | 2 => {| tx_rate_idx := idx; tx_rate_count := 1; tx_rate_flags := flags |}"
" | _ => {| 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);
......@@ -158,9 +157,7 @@ static void mt76_mac_process_tx_rate(struct ieee80211_tx_rate *txrate, u16 rate)
[[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::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)
{
......@@ -229,8 +226,6 @@ static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
"|} } @ 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)
......@@ -330,10 +325,7 @@ u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate
" | _ => st"
" end} @ ieee80211_rx_status")]]
[[rc::tactics("all: try solve_bound.")]]
[[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);
......
......@@ -49,6 +49,43 @@ Global Instance rc_flags_BitfieldDesc : BitfieldDesc rc_flags := {|
bitfield_wf := rc_flags_wf;
|}.
Global Instance simpl_exist_rc_flags P : SimplExist rc_flags P
( use_rts_cts use_cts_protect use_short_preamble mcs green_field
width_40_mhz dup_data short_gi vht_mcs width_80_mhz
width_160_mhz,
P {|
rc_use_rts_cts := use_rts_cts;
rc_use_cts_protect := use_cts_protect;
rc_use_short_preamble := use_short_preamble;
rc_mcs := mcs;
rc_green_field := green_field;
rc_40_mhz_width := width_40_mhz;
rc_dup_data := dup_data;
rc_short_gi := short_gi;
rc_vht_mcs := vht_mcs;
rc_80_mhz_width := width_80_mhz;
rc_160_mhz_width := width_160_mhz;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_rc_flags P : SimplForall rc_flags 11 P
( use_rts_cts use_cts_protect use_short_preamble mcs green_field
width_40_mhz dup_data short_gi vht_mcs width_80_mhz
width_160_mhz,
P {|
rc_use_rts_cts := use_rts_cts;
rc_use_cts_protect := use_cts_protect;
rc_use_short_preamble := use_short_preamble;
rc_mcs := mcs;
rc_green_field := green_field;
rc_40_mhz_width := width_40_mhz;
rc_dup_data := dup_data;
rc_short_gi := short_gi;
rc_vht_mcs := vht_mcs;
rc_80_mhz_width := width_80_mhz;
rc_160_mhz_width := width_160_mhz;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Definition rc_no_flags : rc_flags := {|
rc_use_rts_cts := false;
rc_use_cts_protect := false;
......@@ -69,6 +106,23 @@ Record tx_rate := {
tx_rate_flags : rc_flags;
}.
Global Instance simpl_exist_tx_rate P : SimplExist tx_rate P
( idx count flags,
P {|
tx_rate_idx := idx;
tx_rate_count := count;
tx_rate_flags := flags;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_tx_rate P : SimplForall tx_rate 3 P
( idx count flags,
P {|
tx_rate_idx := idx;
tx_rate_count := count;
tx_rate_flags := flags;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record rate := {
rate_mcs : Z;
rate_bw : Z;
......@@ -117,6 +171,33 @@ Global Instance rate_BitfieldDesc : BitfieldDesc rate := {|
bitfield_wf := rate_wf;
|}.
Global Instance simpl_exist_rate P : SimplExist rate P
( mcs bw sgi stbc etxbf snd itxbf phy,
P {|
rate_mcs := mcs;
rate_bw := bw;
rate_sgi := sgi;
rate_stbc := stbc;
rate_etxbf := etxbf;
rate_snd := snd;
rate_itxbf := itxbf;
rate_phy := phy;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_rate P : SimplForall rate 8 P
( mcs bw sgi stbc etxbf snd itxbf phy,
P {|
rate_mcs := mcs;
rate_bw := bw;
rate_sgi := sgi;
rate_stbc := stbc;
rate_etxbf := etxbf;
rate_snd := snd;
rate_itxbf := itxbf;
rate_phy := phy;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record info_flags := {
info_ctl_req_tx_status : bool;
info_ctl_assign_seq : bool;
......@@ -226,6 +307,91 @@ Global Instance info_flags_BitfieldDesc : BitfieldDesc info_flags := {|
bitfield_wf := info_flags_wf;
|}.
Global Instance simpl_exist_info_flags P : SimplExist info_flags P
( ctl_req_tx_status ctl_assign_seq ctl_no_ack ctl_clear_ps_filt ctl_first_fragment
ctl_send_after_dtim ctl_ampdu ctl_injected stat_tx_filtered stat_ack
stat_ampdu stat_ampdu_no_back ctl_rate_ctrl_probe intfl_offchan_tx_ok ctl_hw_80211_encap
intfl_retried intfl_dont_encrypt ctl_no_ps_buffer ctl_more_frames intfl_retransmission
intfl_mlme_conn_tx intfl_nl80211_frame_tx ctl_ldpc ctl_stbc ctl_tx_offchan
intfl_tkip_mic_failure ctl_no_cck_rate status_eosp ctl_use_minrate ctl_dontfrag
stat_noack_transmitted,
P {|
info_ctl_req_tx_status := ctl_req_tx_status;
info_ctl_assign_seq := ctl_assign_seq;
info_ctl_no_ack := ctl_no_ack;
info_ctl_clear_ps_filt := ctl_clear_ps_filt;
info_ctl_first_fragment := ctl_first_fragment;
info_ctl_send_after_dtim := ctl_send_after_dtim;
info_ctl_ampdu := ctl_ampdu;
info_ctl_injected := ctl_injected;
info_stat_tx_filtered := stat_tx_filtered;
info_stat_ack := stat_ack;
info_stat_ampdu := stat_ampdu;
info_stat_ampdu_no_back := stat_ampdu_no_back;
info_ctl_rate_ctrl_probe := ctl_rate_ctrl_probe;
info_intfl_offchan_tx_ok := intfl_offchan_tx_ok;
info_ctl_hw_80211_encap := ctl_hw_80211_encap;
info_intfl_retried := intfl_retried;
info_intfl_dont_encrypt := intfl_dont_encrypt;
info_ctl_no_ps_buffer := ctl_no_ps_buffer;
info_ctl_more_frames := ctl_more_frames;
info_intfl_retransmission := intfl_retransmission;
info_intfl_mlme_conn_tx := intfl_mlme_conn_tx;
info_intfl_nl80211_frame_tx := intfl_nl80211_frame_tx;
info_ctl_ldpc := ctl_ldpc;
info_ctl_stbc := ctl_stbc;
info_ctl_tx_offchan := ctl_tx_offchan;
info_intfl_tkip_mic_failure := intfl_tkip_mic_failure;
info_ctl_no_cck_rate := ctl_no_cck_rate;
info_status_eosp := status_eosp;
info_ctl_use_minrate := ctl_use_minrate;
info_ctl_dontfrag := ctl_dontfrag;
info_stat_noack_transmitted := stat_noack_transmitted;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_info_flags P : SimplForall info_flags 31 P
( ctl_req_tx_status ctl_assign_seq ctl_no_ack ctl_clear_ps_filt ctl_first_fragment
ctl_send_after_dtim ctl_ampdu ctl_injected stat_tx_filtered stat_ack
stat_ampdu stat_ampdu_no_back ctl_rate_ctrl_probe intfl_offchan_tx_ok ctl_hw_80211_encap
intfl_retried intfl_dont_encrypt ctl_no_ps_buffer ctl_more_frames intfl_retransmission
intfl_mlme_conn_tx intfl_nl80211_frame_tx ctl_ldpc ctl_stbc ctl_tx_offchan
intfl_tkip_mic_failure ctl_no_cck_rate status_eosp ctl_use_minrate ctl_dontfrag
stat_noack_transmitted,
P {|
info_ctl_req_tx_status := ctl_req_tx_status;
info_ctl_assign_seq := ctl_assign_seq;
info_ctl_no_ack := ctl_no_ack;
info_ctl_clear_ps_filt := ctl_clear_ps_filt;
info_ctl_first_fragment := ctl_first_fragment;
info_ctl_send_after_dtim := ctl_send_after_dtim;
info_ctl_ampdu := ctl_ampdu;
info_ctl_injected := ctl_injected;
info_stat_tx_filtered := stat_tx_filtered;
info_stat_ack := stat_ack;
info_stat_ampdu := stat_ampdu;
info_stat_ampdu_no_back := stat_ampdu_no_back;
info_ctl_rate_ctrl_probe := ctl_rate_ctrl_probe;
info_intfl_offchan_tx_ok := intfl_offchan_tx_ok;
info_ctl_hw_80211_encap := ctl_hw_80211_encap;
info_intfl_retried := intfl_retried;
info_intfl_dont_encrypt := intfl_dont_encrypt;
info_ctl_no_ps_buffer := ctl_no_ps_buffer;
info_ctl_more_frames := ctl_more_frames;
info_intfl_retransmission := intfl_retransmission;
info_intfl_mlme_conn_tx := intfl_mlme_conn_tx;
info_intfl_nl80211_frame_tx := intfl_nl80211_frame_tx;
info_ctl_ldpc := ctl_ldpc;
info_ctl_stbc := ctl_stbc;
info_ctl_tx_offchan := ctl_tx_offchan;
info_intfl_tkip_mic_failure := intfl_tkip_mic_failure;
info_ctl_no_cck_rate := ctl_no_cck_rate;
info_status_eosp := status_eosp;
info_ctl_use_minrate := ctl_use_minrate;
info_ctl_dontfrag := ctl_dontfrag;
info_stat_noack_transmitted := stat_noack_transmitted;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record info_status := {
info_status_rates : list tx_rate;
ampdu_ack_len : Z;
......@@ -237,6 +403,21 @@ Record tx_info := {
tx_info_status : info_status;
}.
Global Instance simpl_exist_tx_info P : SimplExist tx_info P
( flags status,
P {|
tx_info_flags := flags;
tx_info_status := status;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_tx_info P : SimplForall tx_info 2 P
( flags status,
P {|
tx_info_flags := flags;
tx_info_status := status;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record tx_status := {
tx_status_valid : bool;
tx_status_success : bool;
......@@ -249,6 +430,35 @@ Record tx_status := {
tx_status_rate : Z;
}.
Global Instance simpl_exist_tx_status P : SimplExist tx_status P
( valid success aggr ack_req is_probe wcid pktid retry rate,
P {|
tx_status_valid := valid;
tx_status_success := success;
tx_status_aggr := aggr;
tx_status_ack_req := ack_req;
tx_status_is_probe := is_probe;
tx_status_wcid := wcid;
tx_status_pktid := pktid;
tx_status_retry := retry;
tx_status_rate := rate;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_tx_status P : SimplForall tx_status 9 P
( valid success aggr ack_req is_probe wcid pktid retry rate,
P {|
tx_status_valid := valid;
tx_status_success := success;
tx_status_aggr := aggr;
tx_status_ack_req := ack_req;
tx_status_is_probe := is_probe;
tx_status_wcid := wcid;
tx_status_pktid := pktid;
tx_status_retry := retry;
tx_status_rate := rate;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record enc_flags := {
enc_flag_shortpre : bool;
enc_flag_short_gi : bool;
......@@ -286,6 +496,31 @@ Global Instance enc_flags_BitfieldDesc : BitfieldDesc enc_flags := {|
bitfield_wf := enc_flags_wf;
|}.
Global Instance simpl_exist_enc_flags P : SimplExist enc_flags P
( shortpre short_gi ht_gf stbc_lo stbc_hi ldpc bf,
P {|
enc_flag_shortpre := shortpre;
enc_flag_short_gi := short_gi;
enc_flag_ht_gf := ht_gf;
enc_flag_stbc_lo := stbc_lo;
enc_flag_stbc_hi := stbc_hi;
enc_flag_ldpc := ldpc;
enc_flag_bf := bf;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_enc_flags P : SimplForall enc_flags 7 P
( shortpre short_gi ht_gf stbc_lo stbc_hi ldpc bf,
P {|
enc_flag_shortpre := shortpre;
enc_flag_short_gi := short_gi;
enc_flag_ht_gf := ht_gf;
enc_flag_stbc_lo := stbc_lo;
enc_flag_stbc_hi := stbc_hi;
enc_flag_ldpc := ldpc;
enc_flag_bf := bf;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record rx_status := {
rx_status_enc_flags : enc_flags;
rx_status_encoding : Z;
......@@ -293,6 +528,25 @@ Record rx_status := {
rx_status_rate_idx : Z;
}.
Global Instance simpl_exist_rx_status P : SimplExist rx_status P
( enc_flags encoding bw rate_idx,
P {|
rx_status_enc_flags := enc_flags;
rx_status_encoding := encoding;
rx_status_bw := bw;
rx_status_rate_idx := rate_idx;
|}).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_rx_status P : SimplForall rx_status 4 P
( enc_flags encoding bw rate_idx,
P {|
rx_status_enc_flags := enc_flags;
rx_status_encoding := encoding;
rx_status_bw := bw;
rx_status_rate_idx := rate_idx;
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record hw_value := {
hw_value_idx : Z;
hw_value_phy : Z;
......@@ -352,24 +606,6 @@ Record adapter := {
adapter_chan_def : chan_def;
}.
Ltac simpl_bool_hyp :=
repeat (match goal with
| [ H : negb ?b = true |- _ ] =>
assert (b = false) by apply negb_true_iff; clear H
| [ H : negb ?b = false |- _ ] =>
assert (b = true) by apply negb_false_iff; clear H
| [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil = 0 |- _ ] =>
assert (b = false) by (by apply (bf_cons_bool_singleton_false_iff a b)); clear H
| [ H : bf_cons ?a 1 (Z_of_bool ?b) bf_nil 0 |- _ ] =>
assert (b = true) by (by apply (bf_cons_bool_singleton_true_iff a b)); clear H
| [ H : bf_cons ?a ?k ?x bf_nil = 0 |- _ ] =>
assert (x = 0) by (by apply (bf_cons_singleton_z_iff a k x)); clear H
| [ H : bf_cons ?a ?k ?x bf_nil 0 |- _ ] =>
assert (x 0) by (by apply (bf_cons_singleton_nz_iff a k x)); clear H
| [ H : ?b = false |- _ ] => try (rewrite !H; clear H)
| [ H : ?b = true |- _ ] => try (rewrite !H; clear H)
end; try solve_goal).
Local Open Scope Z_scope.
Lemma max_int_unsigned_le_lt x (it : int_type) :
......@@ -424,8 +660,3 @@ Ltac 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.
Ltac destruct_record :=
match goal with
| [ |- ?r = _ ] => destruct r; solve_goal
end.
......@@ -58,21 +58,6 @@ Proof.
by destruct b.
Qed.
Lemma bf_cons_singleton_z_iff a k x :
0 a
bf_cons a k x bf_nil = 0 x = 0.
Proof.
intros. rewrite /bf_cons /bf_nil Z.lor_0_r.
by apply Z.shiftl_eq_0_iff.
Qed.
Lemma bf_cons_singleton_nz_iff a k x :
0 a
bf_cons a k x bf_nil 0 x 0.
Proof.
intros. rewrite /not bf_cons_singleton_z_iff //.
Qed.
Lemma bf_mask_cons_singleton a k :
bf_mask_cons a k bf_nil = (Z.ones k) a.
Proof.
......
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