Skip to content

GitLab

Commit a77f55f9 authored by Paul's avatar Paul
Browse files

more typing rules to handle it cast

parent 8a7d451a
Hide whitespace changes
Inline Side-by-side
linux/casestudies/proofs/pgtable/pgtable_lemmas.v
View file @ a77f55f9
......@@ -58,9 +58,8 @@ Global Program Instance Pte_BitfieldDesc : BitfieldDesc Pte := {|
(range_of 48 3); (range_of 51 13)];
|}
|}.
Next Obligation. by repeat econstructor. Qed.
Next Obligation. Admitted. (* derivable from the first *)
Next Obligation. Admitted.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
(*
Example pte_repr_sound p :
......@@ -127,9 +126,8 @@ Global Program Instance Attr_BitfieldDesc : BitfieldDesc Attr := {|
(range_of 54 1)]
|}
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
(* pte prot *)
......@@ -165,9 +163,8 @@ Global Program Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
sig_ranges := [# range_of 0 1; range_of 1 1; range_of 2 1; range_of 3 1]
|}
|}.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. Admitted.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Global Instance simpl_exist_Prot P : SimplExist Prot P (∃ x w r device,
......
linux/casestudies/proofs/tcp_input/tcp_input_lemmas.v
View file @ a77f55f9
......@@ -10,11 +10,11 @@ Record tcp_ecn_flags := mk_tcp_ecn_flags {
Global Instance tcp_ecn_flags_settable : Settable _ := settable! mk_tcp_ecn_flags
<ecn_ok; ecn_queue_cwr; ecn_demand_cwr; ecn_seen>.
Definition tcp_ecn_flags_repr (f : tcp_ecn_flags) : Z :=
bf_cons 0 1 (Z_of_bool $ ecn_ok f) $
bf_cons 1 1 (Z_of_bool $ ecn_queue_cwr f) $
bf_cons 2 1 (Z_of_bool $ ecn_demand_cwr f) $
bf_cons 3 1 (Z_of_bool $ ecn_seen f) $
Definition tcp_ecn_flags_repr (f : tcp_ecn_flags) : tm :=
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ ecn_ok f) $
bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ ecn_queue_cwr f) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ ecn_demand_cwr f) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ ecn_seen f) $
bf_nil.
Arguments tcp_ecn_flags_repr _/.
......@@ -25,11 +25,18 @@ Definition tcp_ecn_flags_wf (f : tcp_ecn_flags) : Prop :=
0 ≤ Z_of_bool $ ecn_demand_cwr f < 2^1 ∧
0 ≤ Z_of_bool $ ecn_seen f < 2^1.
Global Instance tcp_ecn_flags_BitFieldDesc : BitfieldDesc tcp_ecn_flags := {|
Global Program Instance tcp_ecn_flags_BitFieldDesc : BitfieldDesc tcp_ecn_flags := {|
bitfield_it := u8;
bitfield_repr := tcp_ecn_flags_repr;
bitfield_wf := tcp_ecn_flags_wf;
bitfield_sig := {|
sig_bits := 8;
sig_ranges := [# (range_of 0 1); (range_of 1 1); (range_of 2 1); (range_of 3 1)]
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Global Instance simpl_exist_tcp_ecn_flags P : SimplExist tcp_ecn_flags P
(∃ ok queue_cwr demand_cwr seen,
......@@ -61,12 +68,12 @@ Record inet_csk_ack_state := mk_inet_csk_ack_state {
Global Instance inet_csk_ack_state_settable : Settable _ := settable! mk_inet_csk_ack_state
<ack_sched; ack_timer; ack_pushed; ack_pushed_2; ack_now>.
Definition inet_csk_ack_state_repr (f : inet_csk_ack_state) : Z :=
bf_cons 0 1 (Z_of_bool $ ack_sched f) $
bf_cons 1 1 (Z_of_bool $ ack_timer f) $
bf_cons 2 1 (Z_of_bool $ ack_pushed f) $
bf_cons 3 1 (Z_of_bool $ ack_pushed_2 f) $
bf_cons 4 1 (Z_of_bool $ ack_now f) $
Definition inet_csk_ack_state_repr (f : inet_csk_ack_state) : tm :=
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ ack_sched f) $
bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ ack_timer f) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ ack_pushed f) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ ack_pushed_2 f) $
bf_cons (range_of 4 1) (bf_val $ Z_of_bool $ ack_now f) $
bf_nil.
Arguments inet_csk_ack_state_repr _/.
......@@ -78,11 +85,18 @@ Definition inet_csk_ack_state_wf (f : inet_csk_ack_state) : Prop :=
0 ≤ Z_of_bool $ ack_pushed_2 f < 2^1 ∧
0 ≤ Z_of_bool $ ack_now f < 2^1.
Global Instance inet_csk_ack_state_BitFieldDesc : BitfieldDesc inet_csk_ack_state := {|
Global Program Instance inet_csk_ack_state_BitFieldDesc : BitfieldDesc inet_csk_ack_state := {|
bitfield_it := u8;
bitfield_repr := inet_csk_ack_state_repr;
bitfield_wf := inet_csk_ack_state_wf;
bitfield_sig := {|
sig_bits := 8;
sig_ranges := [# (range_of 0 1); (range_of 1 1); (range_of 2 1); (range_of 3 1); (range_of 4 1)]
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Global Instance simpl_exist_inet_csk_ack_state P : SimplExist inet_csk_ack_state P
(∃ sched timer pushed pushed_2 now,
......
linux/casestudies/proofs/x86_pgtable/x86_pgtable_lemmas.v
View file @ a77f55f9
......@@ -24,25 +24,25 @@ Global Instance pte_settable : Settable _ := settable! mk_pte
pg_uffd_wp; pg_soft_dirty;
pg_dev_map; pg_no_exec>.
Definition pte_repr (f : pte) : Z :=
bf_cons 0 1 (Z_of_bool $ pg_present f) $
bf_cons 1 1 (Z_of_bool $ pg_write f) $
bf_cons 2 1 (Z_of_bool $ pg_user f) $
bf_cons 3 1 (Z_of_bool $ pg_pwt f) $
bf_cons 4 1 (Z_of_bool $ pg_pcd f) $
bf_cons 5 1 (Z_of_bool $ pg_accessed f) $
bf_cons 6 1 (Z_of_bool $ pg_dirty f) $
bf_cons 7 1 (Z_of_bool $ pg_pse f) $
bf_cons 8 1 (Z_of_bool $ pg_global f) $
bf_cons 9 1 (Z_of_bool $ pg_special f) $
bf_cons 10 1 (Z_of_bool $ pg_uffd_wp f) $
bf_cons 11 1 (Z_of_bool $ pg_soft_dirty f) $
bf_cons 58 1 (Z_of_bool $ pg_dev_map f) $
bf_cons 63 1 (Z_of_bool $ pg_no_exec f) $
Definition pte_repr (f : pte) : tm :=
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ pg_present f) $
bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ pg_write f) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ pg_user f) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ pg_pwt f) $
bf_cons (range_of 4 1) (bf_val $ Z_of_bool $ pg_pcd f) $
bf_cons (range_of 5 1) (bf_val $ Z_of_bool $ pg_accessed f) $
bf_cons (range_of 6 1) (bf_val $ Z_of_bool $ pg_dirty f) $
bf_cons (range_of 7 1) (bf_val $ Z_of_bool $ pg_pse f) $
bf_cons (range_of 8 1) (bf_val $ Z_of_bool $ pg_global f) $
bf_cons (range_of 9 1) (bf_val $ Z_of_bool $ pg_special f) $
bf_cons (range_of 10 1) (bf_val $ Z_of_bool $ pg_uffd_wp f) $
bf_cons (range_of 11 1) (bf_val $ Z_of_bool $ pg_soft_dirty f) $
bf_cons (range_of 58 1) (bf_val $ Z_of_bool $ pg_dev_map f) $
bf_cons (range_of 63 1) (bf_val $ Z_of_bool $ pg_no_exec f) $
bf_nil.
Arguments pte_repr _/.
Coercion pte_repr : pte >-> Z.
Coercion pte_repr : pte >-> tm.
Definition pte_wf (f : pte) : Prop :=
0 ≤ Z_of_bool $ pg_present f < 2^1 ∧
......@@ -58,14 +58,23 @@ Definition pte_wf (f : pte) : Prop :=
0 ≤ Z_of_bool $ pg_uffd_wp f < 2^1 ∧
0 ≤ Z_of_bool $ pg_soft_dirty f < 2^1 ∧
0 ≤ Z_of_bool $ pg_dev_map f < 2^1 ∧
0 ≤ Z_of_bool $ pg_no_exec f < 2^1 ∧
0 ≤ f < 2^64.
0 ≤ Z_of_bool $ pg_no_exec f < 2^1.
(* 0 ≤ f < 2^64. *)
Global Instance pte_Bitfield_Desc : BitfieldDesc pte := {|
Global Program Instance pte_Bitfield_Desc : BitfieldDesc pte := {|
bitfield_it := u64;
bitfield_repr := pte_repr;
bitfield_wf := pte_wf;
bitfield_sig := {|
sig_bits := 64;
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 58 1); (range_of 63 1)];
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Definition pte_present (p : pte) : bool := pg_present p || pg_global p.
......
linux/casestudies/x86_pgtable.c
View file @ a77f55f9
......@@ -20,7 +20,7 @@ typedef u64 phys_addr_t;
// arch/x86/include/asm/pgtable_64_types.h
typedef unsigned long pteval_t;
typedef struct [[rc::refined_by("v : Z")]] pte_t {
typedef struct [[rc::refined_by("v : tm")]] pte_t {
[[rc::field("v @ bitfield_raw<u64>")]]
pteval_t pte;
} pte_t;
......@@ -35,7 +35,7 @@ static inline pteval_t native_pte_val(pte_t pte)
return pte.pte;
}
[[rc::parameters("v : Z")]]
[[rc::parameters("v : tm")]]
[[rc::args("v @ bitfield_raw<u64>")]]
[[rc::returns("v @ pte_t")]]
static inline pte_t native_make_pte(pteval_t val)
......@@ -189,20 +189,19 @@ static inline bool pte_special(pte_t pte)
return 0 != (pte_flags(pte) & _PAGE_SPECIAL);
}
[[rc::parameters("p : pte", "m : Z", "res : Z")]]
[[rc::parameters("p : pte", "m : tm")]]
[[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]]
[[rc::requires("{normalize_bitfield_eq (Z.lor p m) res}")]]
[[rc::returns("res @ pte_t")]]
[[rc::returns("{bf_or p m} @ pte_t")]]
static inline pte_t pte_set_flags(pte_t pte, pteval_t set)
{
pteval_t v = native_pte_val(pte);
return native_make_pte(v | set);
}
[[rc::parameters("p : pte", "m : Z", "res : Z")]]
[[rc::parameters("p : pte", "m : tm")]]
[[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]]
[[rc::requires("{normalize_bitfield_eq (Z.land p (Z_lunot 64 m)) res}")]]
[[rc::returns("res @ pte_t")]]
// [[rc::requires("{normalize_bitfield_eq (Z.land p (Z_lunot 64 m)) res}")]]
[[rc::returns("{bf_and_neg p m} @ pte_t")]]
static inline pte_t pte_clear_flags(pte_t pte, pteval_t clear)
{
pteval_t v = native_pte_val(pte);
......@@ -217,131 +216,131 @@ static inline bool pte_uffd_wp(pte_t pte)
return 0 != (pte_flags(pte) & _PAGE_UFFD_WP);
}
INPUT_PTE
[[rc::returns("{p <| pg_uffd_wp := true |>} @ pte_t")]]
static inline pte_t pte_mkuffd_wp(pte_t pte)
{
return pte_set_flags(pte, _PAGE_UFFD_WP);
}
INPUT_PTE
[[rc::returns("{p <| pg_uffd_wp := false |>} @ pte_t")]]
static inline pte_t pte_clear_uffd_wp(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_UFFD_WP);
}
// #endif
INPUT_PTE
[[rc::returns("{p <| pg_dirty := false |>} @ pte_t")]]
static inline pte_t pte_mkclean(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_accessed := false |>} @ pte_t")]]
static inline pte_t pte_mkold(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_ACCESSED);
}
INPUT_PTE
[[rc::returns("{p <| pg_write := false |>} @ pte_t")]]
static inline pte_t pte_wrprotect(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_RW);
}
INPUT_PTE
[[rc::returns("{p <| pg_no_exec := false |>} @ pte_t")]]
static inline pte_t pte_mkexec(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_NX);
}
INPUT_PTE
[[rc::returns("{p <| pg_dirty := true |> <| pg_soft_dirty := true |>} @ pte_t")]]
static inline pte_t pte_mkdirty(pte_t pte)
{
return pte_set_flags(pte, _PAGE_DIRTY | _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_accessed := true |>} @ pte_t")]]
static inline pte_t pte_mkyoung(pte_t pte)
{
return pte_set_flags(pte, _PAGE_ACCESSED);
}
INPUT_PTE
[[rc::returns("{p <| pg_write := true |>} @ pte_t")]]
static inline pte_t pte_mkwrite(pte_t pte)
{
return pte_set_flags(pte, _PAGE_RW);
}
INPUT_PTE
[[rc::returns("{p <| pg_pse := true |>} @ pte_t")]]
static inline pte_t pte_mkhuge(pte_t pte)
{
return pte_set_flags(pte, _PAGE_PSE);
}
INPUT_PTE
[[rc::returns("{p <| pg_pse := false |>} @ pte_t")]]
static inline pte_t pte_clrhuge(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_PSE);
}
INPUT_PTE
[[rc::returns("{p <| pg_global := true |>} @ pte_t")]]
static inline pte_t pte_mkglobal(pte_t pte)
{
return pte_set_flags(pte, _PAGE_GLOBAL);
}
INPUT_PTE
[[rc::returns("{p <| pg_global := false |>} @ pte_t")]]
static inline pte_t pte_clrglobal(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_GLOBAL);
}
INPUT_PTE
[[rc::returns("{p <| pg_special := true |>} @ pte_t")]]
static inline pte_t pte_mkspecial(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SPECIAL);
}
INPUT_PTE
[[rc::returns("{p <| pg_special := true |> <| pg_dev_map := true |>} @ pte_t")]]
static inline pte_t pte_mkdevmap(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SPECIAL | _PAGE_DEVMAP);
}
// #ifdef CONFIG_HAVE_ARCH_SOFT_DIRTY
INPUT_PTE
[[rc::returns("{pg_soft_dirty p} @ boolean<bool_it>")]]
static inline bool pte_soft_dirty(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_soft_dirty := true |>} @ pte_t")]]
static inline pte_t pte_mksoft_dirty(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pg_soft_dirty := false |>} @ pte_t")]]
static inline pte_t pte_clear_soft_dirty(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_SOFT_DIRTY);
}
// #endif
// INPUT_PTE
// [[rc::returns("{p <| pg_uffd_wp := true |>} @ pte_t")]]
// static inline pte_t pte_mkuffd_wp(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_UFFD_WP);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_uffd_wp := false |>} @ pte_t")]]
// static inline pte_t pte_clear_uffd_wp(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_UFFD_WP);
// }
// // #endif
// INPUT_PTE
// [[rc::returns("{p <| pg_dirty := false |>} @ pte_t")]]
// static inline pte_t pte_mkclean(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_accessed := false |>} @ pte_t")]]
// static inline pte_t pte_mkold(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_ACCESSED);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_write := false |>} @ pte_t")]]
// static inline pte_t pte_wrprotect(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_RW);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_no_exec := false |>} @ pte_t")]]
// static inline pte_t pte_mkexec(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_NX);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_dirty := true |> <| pg_soft_dirty := true |>} @ pte_t")]]
// static inline pte_t pte_mkdirty(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_DIRTY | _PAGE_SOFT_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_accessed := true |>} @ pte_t")]]
// static inline pte_t pte_mkyoung(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_ACCESSED);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_write := true |>} @ pte_t")]]
// static inline pte_t pte_mkwrite(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_RW);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_pse := true |>} @ pte_t")]]
// static inline pte_t pte_mkhuge(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_PSE);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_pse := false |>} @ pte_t")]]
// static inline pte_t pte_clrhuge(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_PSE);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_global := true |>} @ pte_t")]]
// static inline pte_t pte_mkglobal(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_GLOBAL);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_global := false |>} @ pte_t")]]
// static inline pte_t pte_clrglobal(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_GLOBAL);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_special := true |>} @ pte_t")]]
// static inline pte_t pte_mkspecial(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_SPECIAL);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_special := true |> <| pg_dev_map := true |>} @ pte_t")]]
// static inline pte_t pte_mkdevmap(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_SPECIAL | _PAGE_DEVMAP);
// }
// // #ifdef CONFIG_HAVE_ARCH_SOFT_DIRTY
// INPUT_PTE
// [[rc::returns("{pg_soft_dirty p} @ boolean<bool_it>")]]
// static inline bool pte_soft_dirty(pte_t pte)
// {
// return 0 != (pte_flags(pte) & _PAGE_SOFT_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_soft_dirty := true |>} @ pte_t")]]
// static inline pte_t pte_mksoft_dirty(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_SOFT_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_soft_dirty := false |>} @ pte_t")]]
// static inline pte_t pte_clear_soft_dirty(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_SOFT_DIRTY);
// }
// // #endif
theories/lithium/normalize.v
View file @ a77f55f9
......@@ -31,7 +31,7 @@ Ltac normalize_autorewrite :=
#[export] Hint Rewrite keep_factor2_min_1 keep_factor2_twice : lithium_rewrite.
(* basic boolean simplification *)
#[export] Hint Rewrite andb_false_r andb_true_r orb_true_r orb_false_r negb_involutive : lithium_rewrite.
#[export] Hint Rewrite andb_false_r andb_true_r orb_true_r orb_false_r negb_involutive negb_andb negb_orb : lithium_rewrite.
Lemma bool_decide_Z_of_bool_z b :
bool_decide (Z_of_bool b = 0) = negb b.
......
theories/mask_core/calculus.v
View file @ a77f55f9
......@@ -62,8 +62,8 @@ Record signature := {
sig_ranges : vec range sig_length;
sig_mono : ranges_monotone sig_ranges;
(* properties on ranges *)
sig_disjoint : ∀ f1 f2, f1 ≠ f2 →
(sig_ranges !!! f1 ≺ sig_ranges !!! f2) ∨ (sig_ranges !!! f2 ≺ sig_ranges !!! f1);
(* sig_disjoint : ∀ f1 f2, f1 ≠ f2 →
(sig_ranges !!! f1 ≺ sig_ranges !!! f2) ∨ (sig_ranges !!! f2 ≺ sig_ranges !!! f1); *)
field_width f := width (sig_ranges !!! f);
recognize (r : range) : option (fin sig_length) :=
match filter (λ f, sig_ranges !!! f = r) (enum (fin sig_length)) with
......@@ -72,10 +72,34 @@ Record signature := {
end;
(* total bits *)
sig_bits : nat;
sig_ranges_bounded : ∀ f,
Z.of_nat (offset (sig_ranges !!! f)) + Z.of_nat (width (sig_ranges !!! f)) ≤ sig_bits
sig_max_range_bounded : ∃ r, last sig_ranges = Some r ∧
offset r + width r ≤ sig_bits
}.
Lemma sig_disjoint σ f1 f2 :
f1 ≠ f2 →
(sig_ranges σ !!! f1 ≺ sig_ranges σ !!! f2) ∨
(sig_ranges σ !!! f2 ≺ sig_ranges σ !!! f1).
Proof.
Admitted.
Lemma sig_ranges_bounded σ f :
Z.of_nat (offset (sig_ranges σ !!! f)) + Z.of_nat (width (sig_ranges σ !!! f)) ≤ sig_bits σ.
Proof.
Admitted.
Ltac solve_ranges_monotone := by repeat econstructor.
Ltac sig_max_range_bounded := eexists; split; [done | simpl; lia].
Module example.
Program Definition Pte_signature := {|
sig_bits := 64;
sig_ranges := [# (range_of 0 1); (range_of 1 1); (range_of 2 10); (range_of 12 36); (range_of 48 3); (range_of 51 13)];
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
End example.
(* This is reasonable, because in practice signature is more like a nominal type,
which means we can directly know if two signatures are eq by checking if their names are eq,
and the record signature is more like a definition of that nominal type *)
......
theories/mask_core/total_merge.v
View file @ a77f55f9
......@@ -16,6 +16,14 @@ Section total_merge.
Context {A : Type} `{EqDecision A} (R : relation A) `{∀ x y, Decision (R x y)}.
Lemma Sorted_lookup_mono (l : list A) i j x y :
Sorted R l →
l !! i = Some x →
l !! j = Some y →
i < j →
R x y.
Admitted.
Fixpoint total_merge (l1 : list A) : list A → list A :=
fix total_merge_aux l2 :=
match l1, l2 with
......
theories/mask_core/typecheck.v
View file @ a77f55f9
......@@ -27,7 +27,7 @@ Admitted.
Fixpoint check_has_ty (t : tm) (τ : ty) : bool :=
match t, τ with
| bf_val n, val σ f =>
(* bool_decide (0 ≤ n < 2 ^ (field_width σ f)) *)
(* (0 <=? n) && (n <? 2 ^ (field_width σ f)) *)
true
| bf_mask k, val σ f =>
k =? field_width σ f
......@@ -76,7 +76,7 @@ Ltac destruct_option :=
Lemma check_has_ty_spec t τ :
check_has_ty t τ = true → ⊢ t : τ.
Proof.
induction t; destruct τ; try case_match.