Skip to content

GitLab

Commit 0f746427 authored by Paul's avatar Paul
Browse files

enable coq-record-update

parent d91f7a57
Hide whitespace changes
Inline Side-by-side
linux/casestudies/mt7601u/mac.c
View file @ 0f746427
//@rc::import mac_lemmas from refinedc.linux.casestudies.mt7601u.mac
//@rc::import RecordSet from RecordUpdate
//@rc::inlined Import RecordSetNotations.
// NOTE: the include order affects the appearance order of generated struct definitions
#include "cfg80211.h"
......@@ -37,32 +39,10 @@
[[rc::requires("{rate_wf r}")]]
[[rc::requires("{idx = rate_mcs r}")]]
[[rc::requires("{idx + 4 ≤ max_int i8}")]]
[[rc::requires("{flags = {|"
"rc_use_rts_cts := false;"
"rc_use_cts_protect := false;"
"rc_use_short_preamble := false;"
"rc_mcs := true;"
"rc_green_field := false;"
"rc_40_mhz_width := bool_decide (rate_bw r = rate_bw_40);"
"rc_dup_data := false;"
"rc_short_gi := rate_sgi r;"
"rc_vht_mcs := false;"
"rc_80_mhz_width := false;"
"rc_160_mhz_width := false;"
"|} }")]]
[[rc::requires("{flags_with_gf = {|"
"rc_use_rts_cts := false;"
"rc_use_cts_protect := false;"
"rc_use_short_preamble := false;"
"rc_mcs := true;"
"rc_green_field := true;"
"rc_40_mhz_width := bool_decide (rate_bw r = rate_bw_40);"
"rc_dup_data := false;"
"rc_short_gi := rate_sgi r;"
"rc_vht_mcs := false;"
"rc_80_mhz_width := false;"
"rc_160_mhz_width := false;"
"|} }")]]
[[rc::requires("{flags = rc_no_flags <| rc_mcs := true |>"
" <| rc_40_mhz_width := bool_decide (rate_bw r = rate_bw_40) |>"
" <| rc_short_gi := rate_sgi r |>}")]]
[[rc::requires("{flags_with_gf = flags <| rc_green_field := true |>}")]]
// TODO: we could define an enum in Coq
[[rc::ensures("own p : {match rate_phy r with"
" | 1 => {| tx_rate_idx := idx + 4; tx_rate_count := 1; tx_rate_flags := rc_no_flags |}"
......@@ -115,39 +95,12 @@ static void mt76_mac_process_tx_rate(struct ieee80211_tx_rate *txrate, u16 rate)
[[rc::args("pd @ &own<dev @ mt7601u_dev>", "pi @ &own<info @ ieee80211_tx_info>",
"ps @ &own<st @ mt76_tx_status>")]]
[[rc::requires("{info_flags_wf (tx_info_flags info)}")]]
[[rc::requires("{flags = {|"
"info_ctl_req_tx_status := info_ctl_req_tx_status (tx_info_flags info);"
"info_ctl_assign_seq := info_ctl_assign_seq (tx_info_flags info);"
"info_ctl_no_ack := negb (tx_status_ack_req st) || info_ctl_no_ack (tx_info_flags info);"
"info_ctl_clear_ps_filt := info_ctl_clear_ps_filt (tx_info_flags info);"
"info_ctl_first_fragment := info_ctl_first_fragment (tx_info_flags info);"
"info_ctl_send_after_dtim := info_ctl_send_after_dtim (tx_info_flags info);"
"info_ctl_ampdu := tx_status_aggr st || info_ctl_ampdu (tx_info_flags info);"
"info_ctl_injected := info_ctl_injected (tx_info_flags info);"
"info_stat_tx_filtered := info_stat_tx_filtered (tx_info_flags info);"
"info_stat_ack := (tx_status_ack_req st && tx_status_success st) || info_stat_ack (tx_info_flags info);"
"info_stat_ampdu := tx_status_aggr st || info_stat_ampdu (tx_info_flags info);"
"info_stat_ampdu_no_back := info_stat_ampdu_no_back (tx_info_flags info);"
"info_ctl_rate_ctrl_probe := tx_status_is_probe st || info_ctl_rate_ctrl_probe (tx_info_flags info);"
"info_intfl_offchan_tx_ok := info_intfl_offchan_tx_ok (tx_info_flags info);"
"info_ctl_hw_80211_encap := info_ctl_hw_80211_encap (tx_info_flags info);"
"info_intfl_retried := info_intfl_retried (tx_info_flags info);"
"info_intfl_dont_encrypt := info_intfl_dont_encrypt (tx_info_flags info);"
"info_ctl_no_ps_buffer := info_ctl_no_ps_buffer (tx_info_flags info);"
"info_ctl_more_frames := info_ctl_more_frames (tx_info_flags info);"
"info_intfl_retransmission := info_intfl_retransmission (tx_info_flags info);"
"info_intfl_mlme_conn_tx := info_intfl_mlme_conn_tx (tx_info_flags info);"
"info_intfl_nl80211_frame_tx := info_intfl_nl80211_frame_tx (tx_info_flags info);"
"info_ctl_ldpc := info_ctl_ldpc (tx_info_flags info);"
"info_ctl_stbc := info_ctl_stbc (tx_info_flags info);"
"info_ctl_tx_offchan := info_ctl_tx_offchan (tx_info_flags info);"
"info_intfl_tkip_mic_failure := info_intfl_tkip_mic_failure (tx_info_flags info);"
"info_ctl_no_cck_rate := info_ctl_no_cck_rate (tx_info_flags info);"
"info_status_eosp := info_status_eosp (tx_info_flags info);"
"info_ctl_use_minrate := info_ctl_use_minrate (tx_info_flags info);"
"info_ctl_dontfrag := info_ctl_dontfrag (tx_info_flags info);"
"info_stat_noack_transmitted := info_stat_noack_transmitted (tx_info_flags info);"
"|} }")]]
[[rc::requires("{flags = (tx_info_flags info)"
"<| info_ctl_no_ack := negb (tx_status_ack_req st) || info_ctl_no_ack (tx_info_flags info) |>"
"<| info_ctl_ampdu := tx_status_aggr st || info_ctl_ampdu (tx_info_flags info) |>"
"<| info_stat_ack := (tx_status_ack_req st && tx_status_success st) || info_stat_ack (tx_info_flags info) |>"
"<| info_stat_ampdu := tx_status_aggr st || info_stat_ampdu (tx_info_flags info) |>"
"<| info_ctl_rate_ctrl_probe := tx_status_is_probe st || info_ctl_rate_ctrl_probe (tx_info_flags info) |>}")]]
[[rc::requires("{status = {|"
"info_status_rates := info_status_rates (tx_info_status info);"
"ampdu_ack_len := Z_of_bool (tx_status_success st);"
......@@ -210,19 +163,13 @@ static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
// [[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)"
[[rc::returns("{empty_rate <| rate_mcs := if rc_mcs (tx_rate_flags r) then tx_rate_idx r else hw_value_idx v |>"
"<| 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_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>")]]
" 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::trust_me]] // TODO: bound sidecond
u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate *rate, u8 *nss_val,
......@@ -270,8 +217,7 @@ u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate
}
[[rc::parameters("st : rx_status", "p : loc", "r : rate",
"idx : Z", "idx_cck : Z",
"flags_cck : enc_flags", "flags_ht : enc_flags", "flags_ht_gf : enc_flags")]]
"idx : Z", "idx_cck : Z", "flags_cck : enc_flags", "flags_ht : enc_flags", "flags_ht_gf : enc_flags")]]
[[rc::args("p @ &own<st @ ieee80211_rx_status>", "r @ bitfield<rate>")]]
[[rc::requires("{rate_wf r}")]]
[[rc::requires("{enc_flags_wf (rx_status_enc_flags st)}")]]
......@@ -281,33 +227,11 @@ u16 mt76_mac_tx_rate_val(struct mt7601u_dev *dev, const struct ieee80211_tx_rate
" else if bool_decide (idx >= 8) then idx - 8"
" else if bool_decide (idx >= 4) then 0"
" else idx)}")]]
[[rc::requires("{flags_cck = {|"
"enc_flag_shortpre := bool_decide (idx >= 8) || enc_flag_shortpre (rx_status_enc_flags st);"
"enc_flag_short_gi := enc_flag_short_gi (rx_status_enc_flags st);"
"enc_flag_ht_gf := enc_flag_ht_gf (rx_status_enc_flags st);"
"enc_flag_stbc_lo := enc_flag_stbc_lo (rx_status_enc_flags st);"
"enc_flag_stbc_hi := enc_flag_stbc_hi (rx_status_enc_flags st);"
"enc_flag_ldpc := enc_flag_ldpc (rx_status_enc_flags st);"
"enc_flag_bf := enc_flag_bf (rx_status_enc_flags st);"
"|} }")]]
[[rc::requires("{flags_ht = {|"
"enc_flag_shortpre := enc_flag_shortpre (rx_status_enc_flags st);"
"enc_flag_short_gi := rate_sgi r || enc_flag_short_gi (rx_status_enc_flags st);"
"enc_flag_ht_gf := enc_flag_ht_gf (rx_status_enc_flags st);"
"enc_flag_stbc_lo := bool_decide (rate_stbc r ≠ 0) || enc_flag_stbc_lo (rx_status_enc_flags st);"
"enc_flag_stbc_hi := enc_flag_stbc_hi (rx_status_enc_flags st);"
"enc_flag_ldpc := enc_flag_ldpc (rx_status_enc_flags st);"
"enc_flag_bf := enc_flag_bf (rx_status_enc_flags st);"
"|} }")]]
[[rc::requires("{flags_ht_gf = {|"
"enc_flag_shortpre := enc_flag_shortpre (rx_status_enc_flags st);"
"enc_flag_short_gi := rate_sgi r || enc_flag_short_gi (rx_status_enc_flags st);"
"enc_flag_ht_gf := true;"
"enc_flag_stbc_lo := bool_decide (rate_stbc r ≠ 0) || enc_flag_stbc_lo (rx_status_enc_flags st);"
"enc_flag_stbc_hi := enc_flag_stbc_hi (rx_status_enc_flags st);"
"enc_flag_ldpc := enc_flag_ldpc (rx_status_enc_flags st);"
"enc_flag_bf := enc_flag_bf (rx_status_enc_flags st);"
"|} }")]]
[[rc::requires("{flags_cck = (rx_status_enc_flags st) <| enc_flag_shortpre := bool_decide (idx >= 8) || enc_flag_shortpre (rx_status_enc_flags st) |>}")]]
[[rc::requires("{flags_ht = (rx_status_enc_flags st)"
"<| enc_flag_short_gi := rate_sgi r || enc_flag_short_gi (rx_status_enc_flags st) |>"
"<| enc_flag_stbc_lo := bool_decide (rate_stbc r ≠ 0) || enc_flag_stbc_lo (rx_status_enc_flags st) |>}")]]
[[rc::requires("{flags_ht_gf = flags_ht <| enc_flag_ht_gf := true |>}")]]
[[rc::ensures("own p : {match rate_phy r with"
" | 1 => {| rx_status_enc_flags := rx_status_enc_flags st;"
" rx_status_encoding := rx_status_encoding st; rx_status_bw := rx_status_bw st;"
......
linux/casestudies/mt7601u/proofs/mac/mac_lemmas.v
View file @ 0f746427
From refinedc.typing Require Import typing.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.
Record rc_flags := {
Record rc_flags := mk_rc_flags {
rc_use_rts_cts : bool;
rc_use_cts_protect : bool;
rc_use_short_preamble : bool;
......@@ -14,6 +16,25 @@ Record rc_flags := {
rc_160_mhz_width : bool;
}.
Instance rc_flags_settable : Settable _ := settable! mk_rc_flags
<rc_use_rts_cts; rc_use_cts_protect; rc_use_short_preamble; rc_mcs; rc_green_field;
rc_40_mhz_width; rc_dup_data; rc_short_gi; rc_vht_mcs; rc_80_mhz_width;
rc_160_mhz_width>.
Definition rc_no_flags : rc_flags := {|
rc_use_rts_cts := false;
rc_use_cts_protect := false;
rc_use_short_preamble := false;
rc_mcs := false;
rc_green_field := false;
rc_40_mhz_width := false;
rc_dup_data := false;
rc_short_gi := false;
rc_vht_mcs := false;
rc_80_mhz_width := false;
rc_160_mhz_width := false;
|}.
Definition rc_flags_repr (f : rc_flags) : Z :=
bf_cons 0 1 (Z_of_bool $ rc_use_rts_cts f) $
bf_cons 1 1 (Z_of_bool $ rc_use_cts_protect f) $
......@@ -86,20 +107,6 @@ Global Instance simpl_forall_rc_flags P : SimplForall rc_flags 11 P
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Definition rc_no_flags : rc_flags := {|
rc_use_rts_cts := false;
rc_use_cts_protect := false;
rc_use_short_preamble := false;
rc_mcs := false;
rc_green_field := false;
rc_40_mhz_width := false;
rc_dup_data := false;
rc_short_gi := false;
rc_vht_mcs := false;
rc_80_mhz_width := false;
rc_160_mhz_width := false;
|}.
Record tx_rate := {
tx_rate_idx : Z;
tx_rate_count : Z;
......@@ -123,7 +130,7 @@ Global Instance simpl_forall_tx_rate P : SimplForall tx_rate 3 P
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record rate := {
Record rate := mk_rate {
rate_mcs : Z;
rate_bw : Z;
rate_sgi : bool;
......@@ -134,6 +141,20 @@ Record rate := {
rate_phy : Z;
}.
Instance mk_rate_settable : Settable _ := settable! mk_rate
<rate_mcs; rate_bw; rate_sgi; rate_stbc; rate_etxbf; rate_snd; rate_itxbf; rate_phy>.
Definition empty_rate := {|
rate_mcs := 0;
rate_bw := 0;
rate_sgi := false;
rate_stbc := 0;
rate_etxbf := false;
rate_snd := false;
rate_itxbf := false;
rate_phy := 0;
|}.
Definition rate_bw_20 : Z := 0.
Definition rate_bw_40 : Z := 1.
......@@ -198,7 +219,7 @@ Global Instance simpl_forall_rate P : SimplForall rate 8 P
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record info_flags := {
Record info_flags := mk_info_flags {
info_ctl_req_tx_status : bool;
info_ctl_assign_seq : bool;
info_ctl_no_ack : bool;
......@@ -232,6 +253,17 @@ Record info_flags := {
info_stat_noack_transmitted : bool;
}.
Instance info_flags_settable : Settable _ := settable! mk_info_flags
< info_ctl_req_tx_status; info_ctl_assign_seq; info_ctl_no_ack; info_ctl_clear_ps_filt;
info_ctl_first_fragment; info_ctl_send_after_dtim; info_ctl_ampdu; info_ctl_injected;
info_stat_tx_filtered; info_stat_ack; info_stat_ampdu; info_stat_ampdu_no_back;
info_ctl_rate_ctrl_probe; info_intfl_offchan_tx_ok; info_ctl_hw_80211_encap;
info_intfl_retried; info_intfl_dont_encrypt; info_ctl_no_ps_buffer; info_ctl_more_frames;
info_intfl_retransmission; info_intfl_mlme_conn_tx; info_intfl_nl80211_frame_tx;
info_ctl_ldpc; info_ctl_stbc; info_ctl_tx_offchan; info_intfl_tkip_mic_failure;
info_ctl_no_cck_rate; info_status_eosp; info_ctl_use_minrate; info_ctl_dontfrag;
info_stat_noack_transmitted >.
Definition info_flags_repr (f : info_flags) : Z :=
bf_cons 0 1 (Z_of_bool $ info_ctl_req_tx_status f) $
bf_cons 1 1 (Z_of_bool $ info_ctl_assign_seq f) $
......@@ -459,7 +491,7 @@ Global Instance simpl_forall_tx_status P : SimplForall tx_status 9 P
|}).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
Record enc_flags := {
Record enc_flags := mk_enc_flags {
enc_flag_shortpre : bool;
enc_flag_short_gi : bool;
enc_flag_ht_gf : bool;
......@@ -469,6 +501,10 @@ Record enc_flags := {
enc_flag_bf : bool;
}.
Instance enc_flags_settable : Settable _ := settable! mk_enc_flags
<enc_flag_shortpre; enc_flag_short_gi; enc_flag_ht_gf; enc_flag_stbc_lo; enc_flag_stbc_hi;
enc_flag_ldpc; enc_flag_bf>.
Definition enc_flags_repr (f : enc_flags) : Z :=
bf_cons 0 1 (Z_of_bool $ enc_flag_shortpre f) $
bf_cons 2 1 (Z_of_bool $ enc_flag_short_gi f) $
......
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