Commit 05431e20 authored by Paul's avatar Paul
Browse files

migrate TacticHint

parent 0f746427
......@@ -45,7 +45,7 @@ u64 GENMASK(int h, int l)
(typeof(_mask))(((_reg) & (_mask)) >> __bf_shf(_mask)); \
})
*/
[[rc::tactics("all: unfold normalize_bitfield in *; subst.")]]
[[rc::tactics("all: unfold normalize_bitfield_eq in *; subst.")]]
[[rc::tactics("all: try rewrite Z.add_simpl_r Z_least_significant_one_nonempty_mask.")]]
[[rc::tactics("all: try solve_goal.")]]
[[rc::lemmas("bf_mask_cons_singleton_nonempty", "bf_shr_singleton")]]
......
......@@ -25,7 +25,7 @@ u64 GENMASK(int h, int l);
[[rc::parameters("r : Z", "a : Z", "k : Z", "res : Z")]]
[[rc::args("{bf_mask_cons a k bf_nil} @ bitfield_raw<u64>", "r @ bitfield_raw<u64>")]]
[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
[[rc::requires("{normalize_bitfield (bf_slice a k r) res}")]]
[[rc::requires("{normalize_bitfield_eq (bf_slice a k r) res}")]]
[[rc::returns("res @ int<u64>")]]
u64 FIELD_GET(u64 _mask, u64 _reg);
......
//@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"
......
From refinedc.typing Require Import typing.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.
Record rc_flags := mk_rc_flags {
rc_use_rts_cts : bool;
......@@ -16,7 +14,7 @@ Record rc_flags := mk_rc_flags {
rc_160_mhz_width : bool;
}.
Instance rc_flags_settable : Settable _ := settable! mk_rc_flags
Global 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>.
......@@ -141,7 +139,7 @@ Record rate := mk_rate {
rate_phy : Z;
}.
Instance mk_rate_settable : Settable _ := settable! mk_rate
Global 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 := {|
......@@ -253,7 +251,7 @@ Record info_flags := mk_info_flags {
info_stat_noack_transmitted : bool;
}.
Instance info_flags_settable : Settable _ := settable! mk_info_flags
Global 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;
......@@ -501,7 +499,7 @@ Record enc_flags := mk_enc_flags {
enc_flag_bf : bool;
}.
Instance enc_flags_settable : Settable _ := settable! mk_enc_flags
Global 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>.
......
......@@ -451,7 +451,12 @@ Create HintDb bitfield_rewrite discriminated.
#[export] Hint Rewrite bf_update_cons_skip using lia : bitfield_rewrite.
#[export] Hint Rewrite bf_update_cons_insert using can_solve_tac : bitfield_rewrite.
Definition normalize_bitfield (bv norm : Z) : Prop := bv = norm.
(* 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.
Typeclasses Opaque normalize_bitfield.
Program Definition normalize_bitfield_hint {Σ} bv norm :
......
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