Skip to content

GitLab

Commit d4f568e7 authored by Paul's avatar Paul
Browse files

check more cases

parent a77f55f9
Hide whitespace changes
Inline Side-by-side
linux/casestudies/bits.h
View file @ d4f568e7
......@@ -29,6 +29,7 @@ u64 GENMASK(int h, int l);
[[rc::requires("{0 ≤ a}", "{0 < k}", "{a + k ≤ 64}")]]
[[rc::requires("{normalize (bf_slice (range_of a k) r) = norm}")]]
[[rc::returns("{bf_to_Z norm u64} @ int<u64>")]]
[[rc::ensures("{0 ≤ (bf_to_Z norm u64) < 2 ^ k}")]]
[[rc::trust_me]]
u64 FIELD_GET(u64 _mask, u64 _reg);
......
linux/casestudies/mt7601u/mac.c
View file @ d4f568e7
......@@ -34,6 +34,7 @@
[[rc::parameters("txr : tx_rate", "p : loc", "r : rate",
"idx : Z", "flags : rc_flags", "flags_with_gf : rc_flags")]]
[[rc::args("p @ &own<txr @ ieee80211_tx_rate>", "r @ bitfield<rate>")]]
[[rc::requires("{tx_rate_flags txr = rc_no_flags}")]]
[[rc::requires("{rate_wf r}")]]
[[rc::requires("{idx = rate_mcs r}")]]
[[rc::requires("{idx + 4 ≤ max_int i8}")]]
......@@ -50,13 +51,12 @@
" | 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::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);
txrate->idx = 0;
txrate->flags = 0;
// txrate->flags = 0;
txrate->count = 1;
switch (FIELD_GET(MT_TXWI_RATE_PHY_MODE, rate)) {
......@@ -107,7 +107,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::trust_me]]
static void mt76_mac_fill_tx_status(struct mt7601u_dev *dev,
struct ieee80211_tx_info *info, struct mt76_tx_status *st)
{
......@@ -244,7 +243,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::trust_me]]
static void mt76_mac_process_rate(struct ieee80211_rx_status *status, u16 rate)
{
u8 idx = FIELD_GET(MT_RXWI_RATE_MCS, rate);
......
linux/casestudies/mt7601u/proofs/mac/mac_lemmas.v
View file @ d4f568e7
From refinedc.typing Require Import typing.
From refinedc.mask_core Require Import typecheck.
Record rc_flags := mk_rc_flags {
rc_use_rts_cts : bool;
......@@ -33,18 +34,18 @@ Definition rc_no_flags : rc_flags := {|
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) $
bf_cons 2 1 (Z_of_bool $ rc_use_short_preamble f) $
bf_cons 3 1 (Z_of_bool $ rc_mcs f) $
bf_cons 4 1 (Z_of_bool $ rc_green_field f) $
bf_cons 5 1 (Z_of_bool $ rc_40_mhz_width f) $
bf_cons 6 1 (Z_of_bool $ rc_dup_data f) $
bf_cons 7 1 (Z_of_bool $ rc_short_gi f) $
bf_cons 8 1 (Z_of_bool $ rc_vht_mcs f) $
bf_cons 9 1 (Z_of_bool $ rc_80_mhz_width f) $
bf_cons 10 1 (Z_of_bool $ rc_160_mhz_width f) $
Definition rc_flags_repr (f : rc_flags) : tm :=
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ rc_use_rts_cts f) $
bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ rc_use_cts_protect f) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ rc_use_short_preamble f) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ rc_mcs f) $
bf_cons (range_of 4 1) (bf_val $ Z_of_bool $ rc_green_field f) $
bf_cons (range_of 5 1) (bf_val $ Z_of_bool $ rc_40_mhz_width f) $
bf_cons (range_of 6 1) (bf_val $ Z_of_bool $ rc_dup_data f) $
bf_cons (range_of 7 1) (bf_val $ Z_of_bool $ rc_short_gi f) $
bf_cons (range_of 8 1) (bf_val $ Z_of_bool $ rc_vht_mcs f) $
bf_cons (range_of 9 1) (bf_val $ Z_of_bool $ rc_80_mhz_width f) $
bf_cons (range_of 10 1) (bf_val $ Z_of_bool $ rc_160_mhz_width f) $
bf_nil.
Arguments rc_flags_repr _/.
......@@ -62,11 +63,24 @@ Definition rc_flags_wf (f : rc_flags) : Prop :=
0 ≤ Z_of_bool $ rc_80_mhz_width f < 2^1 ∧
0 ≤ Z_of_bool $ rc_160_mhz_width f < 2^1.
Global Instance rc_flags_BitfieldDesc : BitfieldDesc rc_flags := {|
Global Program Instance rc_flags_BitfieldDesc : BitfieldDesc rc_flags := {|
bitfield_it := u16;
bitfield_repr := rc_flags_repr;
bitfield_wf := rc_flags_wf;
bitfield_sig := {|
sig_bits := 16;
sig_ranges := [# (range_of 0 1); (range_of 1 1); (range_of 2 1); (range_of 3 1); (range_of 4 1);
(range_of 5 1); (range_of 6 1); (range_of 7 1); (range_of 8 1); (range_of 9 1); (range_of 10 1)
]
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma rc_flags_repr_tpd r :
check_has_ty (rc_flags_repr r) (bv bitfield_sig).
Proof. done. Qed.
Global Instance simpl_exist_rc_flags P : SimplExist rc_flags P
(∃ use_rts_cts use_cts_protect use_short_preamble mcs green_field
......@@ -161,15 +175,15 @@ Definition rate_phy_mode_ofdm : Z := 1.
Definition rate_phy_mode_ht : Z := 2.
Definition rate_phy_mode_ht_gf : Z := 3.
Definition rate_repr (r : rate) : Z :=
bf_cons 0 7 (rate_mcs r) $
bf_cons 7 1 (rate_bw r) $
bf_cons 8 1 (Z_of_bool $ rate_sgi r) $
bf_cons 9 2 (rate_stbc r) $
bf_cons 11 1 (Z_of_bool $ rate_etxbf r) $
bf_cons 12 1 (Z_of_bool $ rate_snd r) $
bf_cons 13 1 (Z_of_bool $ rate_itxbf r) $
bf_cons 14 2 (rate_phy r) $
Definition rate_repr (r : rate) : tm :=
bf_cons (range_of 0 7) (bf_val $ rate_mcs r) $
bf_cons (range_of 7 1) (bf_val $ rate_bw r) $
bf_cons (range_of 8 1) (bf_val $ Z_of_bool $ rate_sgi r) $
bf_cons (range_of 9 2) (bf_val $ rate_stbc r) $
bf_cons (range_of 11 1) (bf_val $ Z_of_bool $ rate_etxbf r) $
bf_cons (range_of 12 1) (bf_val $ Z_of_bool $ rate_snd r) $
bf_cons (range_of 13 1) (bf_val $ Z_of_bool $ rate_itxbf r) $
bf_cons (range_of 14 2) (bf_val $ rate_phy r) $
bf_nil.
Arguments rate_repr _/.
......@@ -184,11 +198,22 @@ Definition rate_wf (r : rate) : Prop :=
0 ≤ Z_of_bool $ rate_itxbf r < 2^1 ∧
0 ≤ rate_phy r < 2^2.
Global Instance rate_BitfieldDesc : BitfieldDesc rate := {|
Global Program Instance rate_BitfieldDesc : BitfieldDesc rate := {|
bitfield_it := u16;
bitfield_repr := rate_repr;
bitfield_wf := rate_wf;
bitfield_sig := {|
sig_bits := 16;
sig_ranges := [# (range_of 0 7); (range_of 7 1); (range_of 8 1); (range_of 9 2); (range_of 11 1); (range_of 12 1); (range_of 13 1); (range_of 14 2)]
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma rate_repr_typed r :
check_has_ty (rate_repr r) (bv bitfield_sig).
Proof. done. Qed.
Global Instance simpl_exist_rate P : SimplExist rate P
(∃ mcs bw sgi stbc etxbf snd itxbf phy,
......@@ -262,38 +287,38 @@ Global Instance info_flags_settable : Settable _ := settable! mk_info_flags
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) $
bf_cons 2 1 (Z_of_bool $ info_ctl_no_ack f) $
bf_cons 3 1 (Z_of_bool $ info_ctl_clear_ps_filt f) $
bf_cons 4 1 (Z_of_bool $ info_ctl_first_fragment f) $
bf_cons 5 1 (Z_of_bool $ info_ctl_send_after_dtim f) $
bf_cons 6 1 (Z_of_bool $ info_ctl_ampdu f) $
bf_cons 7 1 (Z_of_bool $ info_ctl_injected f) $
bf_cons 8 1 (Z_of_bool $ info_stat_tx_filtered f) $
bf_cons 9 1 (Z_of_bool $ info_stat_ack f) $
bf_cons 10 1 (Z_of_bool $ info_stat_ampdu f) $
bf_cons 11 1 (Z_of_bool $ info_stat_ampdu_no_back f) $
bf_cons 12 1 (Z_of_bool $ info_ctl_rate_ctrl_probe f) $
bf_cons 13 1 (Z_of_bool $ info_intfl_offchan_tx_ok f) $
bf_cons 14 1 (Z_of_bool $ info_ctl_hw_80211_encap f) $
bf_cons 15 1 (Z_of_bool $ info_intfl_retried f) $
bf_cons 16 1 (Z_of_bool $ info_intfl_dont_encrypt f) $
bf_cons 17 1 (Z_of_bool $ info_ctl_no_ps_buffer f) $
bf_cons 18 1 (Z_of_bool $ info_ctl_more_frames f) $
bf_cons 19 1 (Z_of_bool $ info_intfl_retransmission f) $
bf_cons 20 1 (Z_of_bool $ info_intfl_mlme_conn_tx f) $
bf_cons 21 1 (Z_of_bool $ info_intfl_nl80211_frame_tx f) $
bf_cons 22 1 (Z_of_bool $ info_ctl_ldpc f) $
bf_cons 23 2 (info_ctl_stbc f) $
bf_cons 25 1 (Z_of_bool $ info_ctl_tx_offchan f) $
bf_cons 26 1 (Z_of_bool $ info_intfl_tkip_mic_failure f) $
bf_cons 27 1 (Z_of_bool $ info_ctl_no_cck_rate f) $
bf_cons 28 1 (Z_of_bool $ info_status_eosp f) $
bf_cons 29 1 (Z_of_bool $ info_ctl_use_minrate f) $
bf_cons 30 1 (Z_of_bool $ info_ctl_dontfrag f) $
bf_cons 31 1 (Z_of_bool $ info_stat_noack_transmitted f) $
Definition info_flags_repr (f : info_flags) : tm :=
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ info_ctl_req_tx_status f) $
bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ info_ctl_assign_seq f) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ info_ctl_no_ack f) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ info_ctl_clear_ps_filt f) $
bf_cons (range_of 4 1) (bf_val $ Z_of_bool $ info_ctl_first_fragment f) $
bf_cons (range_of 5 1) (bf_val $ Z_of_bool $ info_ctl_send_after_dtim f) $
bf_cons (range_of 6 1) (bf_val $ Z_of_bool $ info_ctl_ampdu f) $
bf_cons (range_of 7 1) (bf_val $ Z_of_bool $ info_ctl_injected f) $
bf_cons (range_of 8 1) (bf_val $ Z_of_bool $ info_stat_tx_filtered f) $
bf_cons (range_of 9 1) (bf_val $ Z_of_bool $ info_stat_ack f) $
bf_cons (range_of 10 1) (bf_val $ Z_of_bool $ info_stat_ampdu f) $
bf_cons (range_of 11 1) (bf_val $ Z_of_bool $ info_stat_ampdu_no_back f) $
bf_cons (range_of 12 1) (bf_val $ Z_of_bool $ info_ctl_rate_ctrl_probe f) $
bf_cons (range_of 13 1) (bf_val $ Z_of_bool $ info_intfl_offchan_tx_ok f) $
bf_cons (range_of 14 1) (bf_val $ Z_of_bool $ info_ctl_hw_80211_encap f) $
bf_cons (range_of 15 1) (bf_val $ Z_of_bool $ info_intfl_retried f) $
bf_cons (range_of 16 1) (bf_val $ Z_of_bool $ info_intfl_dont_encrypt f) $
bf_cons (range_of 17 1) (bf_val $ Z_of_bool $ info_ctl_no_ps_buffer f) $
bf_cons (range_of 18 1) (bf_val $ Z_of_bool $ info_ctl_more_frames f) $
bf_cons (range_of 19 1) (bf_val $ Z_of_bool $ info_intfl_retransmission f) $
bf_cons (range_of 20 1) (bf_val $ Z_of_bool $ info_intfl_mlme_conn_tx f) $
bf_cons (range_of 21 1) (bf_val $ Z_of_bool $ info_intfl_nl80211_frame_tx f) $
bf_cons (range_of 22 1) (bf_val $ Z_of_bool $ info_ctl_ldpc f) $
bf_cons (range_of 23 2) (bf_val $ info_ctl_stbc f) $
bf_cons (range_of 25 1) (bf_val $ Z_of_bool $ info_ctl_tx_offchan f) $
bf_cons (range_of 26 1) (bf_val $ Z_of_bool $ info_intfl_tkip_mic_failure f) $
bf_cons (range_of 27 1) (bf_val $ Z_of_bool $ info_ctl_no_cck_rate f) $
bf_cons (range_of 28 1) (bf_val $ Z_of_bool $ info_status_eosp f) $
bf_cons (range_of 29 1) (bf_val $ Z_of_bool $ info_ctl_use_minrate f) $
bf_cons (range_of 30 1) (bf_val $ Z_of_bool $ info_ctl_dontfrag f) $
bf_cons (range_of 31 1) (bf_val $ Z_of_bool $ info_stat_noack_transmitted f) $
bf_nil.
Arguments info_flags_repr _/.
......@@ -331,11 +356,28 @@ Definition info_flags_wf (f : info_flags) : Prop :=
0 ≤ Z_of_bool $ info_ctl_dontfrag f < 2^1 ∧
0 ≤ Z_of_bool $ info_stat_noack_transmitted f < 2^1.
Global Instance info_flags_BitfieldDesc : BitfieldDesc info_flags := {|
Global Program Instance info_flags_BitfieldDesc : BitfieldDesc info_flags := {|
bitfield_it := u32;
bitfield_repr := info_flags_repr;
bitfield_wf := info_flags_wf;
bitfield_sig := {|
sig_bits := 32;
sig_ranges := [# (range_of 0 1); (range_of 1 1); (range_of 2 1); (range_of 3 1); (range_of 4 1);
(range_of 5 1); (range_of 6 1); (range_of 7 1); (range_of 8 1); (range_of 9 1); (range_of 10 1);
(range_of 11 1); (range_of 12 1); (range_of 13 1); (range_of 14 1);
(range_of 15 1); (range_of 16 1); (range_of 17 1); (range_of 18 1); (range_of 19 1); (range_of 20 1);
(range_of 21 1); (range_of 22 1); (range_of 23 2);
(range_of 25 1); (range_of 26 1); (range_of 27 1); (range_of 28 1); (range_of 29 1); (range_of 30 1);
(range_of 31 1)]
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma info_flags_repr_tpd r :
check_has_ty (info_flags_repr r) (bv bitfield_sig).
Proof. done. Qed.
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
......@@ -503,14 +545,14 @@ 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>.
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) $
bf_cons 3 1 (Z_of_bool $ enc_flag_ht_gf f) $
bf_cons 4 1 (Z_of_bool $ enc_flag_stbc_lo f) $
bf_cons 5 1 (Z_of_bool $ enc_flag_stbc_hi f) $
bf_cons 6 1 (Z_of_bool $ enc_flag_ldpc f) $
bf_cons 7 1 (Z_of_bool $ enc_flag_bf f) $
Definition enc_flags_repr (f : enc_flags) : tm :=
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ enc_flag_shortpre f) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ enc_flag_short_gi f) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ enc_flag_ht_gf f) $
bf_cons (range_of 4 1) (bf_val $ Z_of_bool $ enc_flag_stbc_lo f) $
bf_cons (range_of 5 1) (bf_val $ Z_of_bool $ enc_flag_stbc_hi f) $
bf_cons (range_of 6 1) (bf_val $ Z_of_bool $ enc_flag_ldpc f) $
bf_cons (range_of 7 1) (bf_val $ Z_of_bool $ enc_flag_bf f) $
bf_nil.
Arguments enc_flags_repr _/.
......@@ -524,11 +566,23 @@ Definition enc_flags_wf (f : enc_flags) : Prop :=
0 ≤ Z_of_bool $ enc_flag_ldpc f < 2^1 ∧
0 ≤ Z_of_bool $ enc_flag_bf f < 2^1.
Global Instance enc_flags_BitfieldDesc : BitfieldDesc enc_flags := {|
Global Program Instance enc_flags_BitfieldDesc : BitfieldDesc enc_flags := {|
bitfield_it := u8;
bitfield_repr := enc_flags_repr;
bitfield_wf := enc_flags_wf;
bitfield_sig := {|
sig_bits := 8;
sig_ranges := [# (range_of 0 1); (range_of 2 1); (range_of 3 1); (range_of 4 1);
(range_of 5 1); (range_of 6 1); (range_of 7 1)]
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma enc_flags_repr_tpd r :
check_has_ty (enc_flags_repr r) (bv bitfield_sig).
Proof. done. Qed.
Global Instance simpl_exist_enc_flags P : SimplExist enc_flags P
(∃ shortpre short_gi ht_gf stbc_lo stbc_hi ldpc bf,
......@@ -586,9 +640,9 @@ Record hw_value := {
hw_value_phy : Z;
}.
Definition hw_value_repr (v : hw_value) : Z :=
bf_cons 0 7 (hw_value_idx v) $
bf_cons 8 2 (hw_value_phy v) $
Definition hw_value_repr (v : hw_value) : tm :=
bf_cons (range_of 0 7) (bf_val $ hw_value_idx v) $
bf_cons (range_of 8 2) (bf_val $ hw_value_phy v) $
bf_nil.
Arguments hw_value_repr _/.
......@@ -597,11 +651,22 @@ Definition hw_value_wf (v : hw_value) : Prop :=
0 ≤ hw_value_idx v < 2^7 ∧
0 ≤ hw_value_phy v < 2^2.
Global Instance hw_value_BitfieldDesc : BitfieldDesc hw_value := {|
Global Program Instance hw_value_BitfieldDesc : BitfieldDesc hw_value := {|
bitfield_it := u16;
bitfield_repr := hw_value_repr;
bitfield_wf := hw_value_wf;
bitfield_sig := {|
sig_bits := 16;
sig_ranges := [# (range_of 0 7); (range_of 8 2)]
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma hw_value_repr_tpd r :
check_has_ty (hw_value_repr r) (bv bitfield_sig).
Proof. done. Qed.
Record ieee_rate := {
ieee_rate_hw_value : hw_value;
......
linux/casestudies/proofs/tcp_input/tcp_input_lemmas.v
View file @ d4f568e7
From refinedc.typing Require Import typing.
From refinedc.mask_core Require Import typecheck.
Record tcp_ecn_flags := mk_tcp_ecn_flags {
ecn_ok : bool;
......@@ -38,6 +39,10 @@ Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma tcp_ecn_flags_repr_tpd r :
check_has_ty (tcp_ecn_flags_repr r) (bv bitfield_sig).
Proof. done. Qed.
Global Instance simpl_exist_tcp_ecn_flags P : SimplExist tcp_ecn_flags P
(∃ ok queue_cwr demand_cwr seen,
P {|
......@@ -98,6 +103,10 @@ Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma inet_csk_ack_state_repr_tpd r :
check_has_ty (inet_csk_ack_state_repr r) (bv bitfield_sig).
Proof. done. Qed.
Global Instance simpl_exist_inet_csk_ack_state P : SimplExist inet_csk_ack_state P
(∃ sched timer pushed pushed_2 now,
P {|
......
linux/casestudies/proofs/x86_pgtable/x86_pgtable_lemmas.v
View file @ d4f568e7
From refinedc.typing Require Import typing.
From refinedc.mask_core Require Import typecheck.
Record pte := mk_pte {
pg_present : bool;
......@@ -76,6 +77,10 @@ Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma pte_repr_tpd r :
check_has_ty (pte_repr r) (bv bitfield_sig).
Proof. done. Qed.
Definition pte_present (p : pte) : bool := pg_present p || pg_global p.
Arguments pte_present _/.
linux/casestudies/x86_pgtable.c
View file @ d4f568e7
......@@ -216,6 +216,7 @@ static inline bool pte_uffd_wp(pte_t pte)
return 0 != (pte_flags(pte) & _PAGE_UFFD_WP);
}
// bitfield in struct: subsume val eq
// INPUT_PTE
// [[rc::returns("{p <| pg_uffd_wp := true |>} @ pte_t")]]
// static inline pte_t pte_mkuffd_wp(pte_t pte)
......
theories/lang/bitfield.v
View file @ d4f568e7
From refinedc.lang Require Import base int_type.
(* From refinedc.lithium Require Import simpl_classes tactics_extend infrastructure Z_bitblast classes. *)
From refinedc.mask_core Require Export calculus confluence provability.
From refinedc.mask_core Require Import semantics safety typecheck.
From refinedc.lithium Require Import simpl_classes.
From refinedc.mask_core Require Export calculus confluence provability typecheck.
From refinedc.mask_core Require Import semantics safety.
Local Open Scope Z_scope.
Local Open Scope bf_scope.
......@@ -9,6 +9,12 @@ Local Open Scope bf_scope.
Definition bf_to_Z (t : tm) (it : int_type) : Z :=
eval (bits_per_int it) t.
Lemma bf_to_Z_bf_val x it :
bf_to_Z (bf_val x) it = x.
Proof. done. Qed.
#[export] Hint Rewrite bf_to_Z_bf_val : lithium_rewrite.
Class BitfieldDesc (R : Type) : Type := {
bitfield_it : int_type;
bitfield_wf : R → Prop;
......@@ -205,3 +211,34 @@ Proof.
all: try by eapply normalize_spec.
rewrite !normalize_preserves_eval //.
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.
theories/typing/bitfield.v
View file @ d4f568e7
......@@ -206,6 +206,19 @@ Typeclasses Opaque bitfield_type.
Section programs.
Context `{!typeG Σ}.
(* it up casting *)
Definition it_le : relation int_type := λ it1 it2,
it_signed it1 = it_signed it2 ∧ it_byte_size_log it1 ≤ it_byte_size_log it2.
Lemma bitfield_raw_it_up_cast v t it1 it2 :
it_le it1 it2 →
bf_to_Z t it1 = bf_to_Z t it2 →
v ◁ᵥ t @ bitfield_raw it1 -∗ v ◁ᵥ t @ bitfield_raw it2.
Proof.
iIntros (Hle Heq) "Hv".
rewrite /ty_own_val /= Heq.
Admitted.
(* typing rules for bitwise operators *)
Lemma type_and_bitfield_tpd T R `{BitfieldDesc R} v1 v2 t1 t2 :
......@@ -417,16 +430,16 @@ Section programs.
(* tpd -> raw *)
(* TODO: sem t = sem t' *)
Lemma subsume_val_bitfield_tpd_raw T R `{BitfieldDesc R} v t t' :
(⌜bf_to_Z t bitfield_it = bf_to_Z t' bitfield_it⌝ ∗ T) -∗
subsume (v ◁ᵥ t @ bitfield_tpd R) (v ◁ᵥ t' @ bitfield_raw bitfield_it) T.
Lemma subsume_val_bitfield_tpd_raw T R `{BitfieldDesc R} it v t t' :
(⌜it_le bitfield_it it⌝ ∗ ⌜bf_to_Z t bitfield_it = bf_to_Z t it⌝ ∗ ⌜t = t'⌝ ∗ T) -∗
subsume (v ◁ᵥ t @ bitfield_tpd R) (v ◁ᵥ t' @ bitfield_raw it) T.
Proof.
iIntros "[%Heq $] [% Hv]". by rewrite /ty_own_val /= Heq.
iIntros "[%Hle [%Heq [<- $]]] [% Hv]".
iApply bitfield_raw_it_up_cast => //.
Qed.
Global Instance subsume_val_bitfield_tpd_raw_inst R `{BitfieldDesc R} v t t' :
SubsumeVal v (t @ bitfield_tpd R) (t' @ bitfield_raw bitfield_it) :=
λ T, i2p (subsume_val_bitfield_tpd_raw T R v t t').
Global Instance subsume_val_bitfield_tpd_raw_inst R `{BitfieldDesc R} it v t t' :
SubsumeVal v (t @ bitfield_tpd R) (t' @ bitfield_raw it) :=
λ T, i2p (subsume_val_bitfield_tpd_raw T R it v t t').
(* Lemma subsume_place_bitfield_tpd_raw T R `{BitfieldDesc R} l β t t' :
(⌜t = t'⌝ ∗ T) -∗ subsume (l ◁ₗ{β} t @ bitfield_tpd R) (l ◁ₗ{β} t' @ bitfield_raw bitfield_it) T.
......@@ -437,18 +450,18 @@ Section programs.
λ T, i2p (subsume_place_bitfield_tpd_raw T R l β t t'). *)
(* raw -> tpd *)
(* Lemma subsume_val_bitfield_raw_tpd T it R `{BitfieldDesc R} v t t' :
Lemma subsume_val_bitfield_raw_tpd T it R `{BitfieldDesc R} v t t' :
(tactic_hint (vm_compute_hint (ensure_bv R) t) (λ _,
⌜it = bitfield_it⌝ ∗ ⌜t = t'⌝ ∗ T)) -∗
⌜it = bitfield_it⌝ ∗ ⌜normalize t = t'⌝ ∗ T)) -∗
subsume (v ◁ᵥ t @ bitfield_raw it) (v ◁ᵥ t' @ bitfield_tpd R) T.
Proof.
unfold tactic_hint, vm_compute_hint.
iIntros "[% [% [-> [-> $]]]] Hv". iSplitR => //.
iPureIntro. by apply ensure_bv_spec.
Qed.
(* iIntros "[% [% [-> [-> $]]]] Hv". iSplitR => //. *)
(* iPureIntro. by apply ensure_bv_spec. *)
Admitted.
Global Instance subsume_val_bitfield_raw_tpd_inst it R `{BitfieldDesc R} v t t' :
SubsumeVal v (t @ bitfield_raw it) (t' @ bitfield_tpd R) :=
λ T, i2p (subsume_val_bitfield_raw_tpd T it R v t t'). *)
λ T, i2p (subsume_val_bitfield_raw_tpd T it R v t t').
Lemma subsume_place_bitfield_raw_tpd T it R `{BitfieldDesc R} l β t t' :
(tactic_hint (vm_compute_hint (ensure_bv R) t') (λ _,
......@@ -523,7 +536,7 @@ Section programs.
SimpleSubsumePlace (t1 @ bitfield_raw it) (t2 @ bitfield_raw it) (⌜bf_to_Z t1 it = bf_to_Z t2 it⌝) | 50.
Proof.
Admitted.
(* int ↔ bitfield_raw
Lemma subsume_val_int_bitfield_raw T it v n bv :
......