Use frontend-generated code for [pgtable.c].

linux/casestudies/pgtable.c

-//@rc::import pgtable_lemmas from refinedc.linux.casestudies.pgtable
-
 #include <stdbool.h>
 #include "bits.h"
 
@@ -88,6 +86,53 @@ struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops {
 #define KVM_PTE_LEAF_ATTR_HI_S1_XN          BIT(54)
 // #define KVM_PTE_LEAF_ATTR_HI_S2_XN          BIT(54)
 
+//@rc::bitfields Pte as u64
+//@  pte_valid       : bool[0]
+//@  pte_type        : integer[1]
+//@  pte_leaf_attr_lo: integer[2 ..11]
+//@  pte_addr        : integer[12..47]
+//@  pte_undef       : integer[48..50]
+//@  pte_leaf_attr_hi: integer[51..63]
+//@rc::end
+
+//@rc::bitfields Attr as u64
+//@  attr_lo_s1_attridx : integer[2..4]
+//@  attr_lo_s1_ap      : integer[6..7]
+//@  attr_lo_s1_sh      : integer[8..9]
+//@  attr_lo_s1_af      : bool[10]
+//@  attr_hi_s1_xn      : bool[54]
+//@rc::end
+
+//@rc::bitfields Prot as u64
+//@  prot_x      : bool[0]
+//@  prot_w      : bool[1]
+//@  prot_r      : bool[2]
+//@  prot_device : bool[3]
+//@rc::end
+
+//@rc::inlined_prelude
+//@Definition pte_from_addr (pa : Pte) : Pte :=
+//@  zero_Pte <| pte_addr := pte_addr pa |>.
+//@
+//@Definition pte_pa (pa : Pte) : tm :=
+//@  bf_cons (range_of 12 36) (bf_val $ pte_addr pa) bf_nil.
+//@
+//@Record mm_callbacks := {
+//@  virt_to_phys : Z → Pte;
+//@}.
+//@
+//@Definition max_level : Z := 4.
+//@Definition mtype_device : Z := 5.
+//@Definition mtype_normal : Z := 0.
+//@Definition pte_type_block : Z := 0.
+//@Definition pte_type_page : Z := 1.
+//@Definition pte_type_table : Z := 1.
+//@Definition ap_rw : Z := 1.
+//@Definition ap_ro : Z := 3.
+//@Definition sh_is : Z := 3.
+//@Definition err_code : Z := 22.
+//@rc::end
+
 [[rc::parameters("pte : Pte")]]
 [[rc::args("pte @ bitfield<Pte>")]]
 [[rc::requires("{bitfield_wf pte}")]]

linux/casestudies/proofs/pgtable/pgtable_lemmas.v

-From refinedc.typing Require Import typing.
-
-(* pte *)
-
-Record Pte := mk_pte {
-  pte_valid : bool;
-  pte_type : Z;
-  pte_leaf_attr_lo : Z;
-  pte_addr : Z;
-  pte_undef : Z;
-  pte_leaf_attr_hi : Z;
-}.
-
-Global Instance Pte_settable : Settable _ := settable! mk_pte
-  <pte_valid; pte_type; pte_leaf_attr_lo; pte_addr; pte_undef; pte_leaf_attr_hi>.
-
-Definition empty_pte := {|
-  pte_valid := false;
-  pte_type := 0;
-  pte_leaf_attr_lo := 0;
-  pte_addr := 0;
-  pte_undef := 0;
-  pte_leaf_attr_hi := 0;
-|}.
-
-Definition pte_from_addr (pa : Pte) : Pte :=
-  empty_pte <| pte_addr := pte_addr pa |>.
-
-Definition pte_pa (pa : Pte) : tm :=
-  bf_cons (range_of 12 36) (bf_val $ pte_addr pa) bf_nil.
-
-Definition pte_repr (p : Pte) : tm :=
-  bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ pte_valid p) $
-  bf_cons (range_of 1 1) (bf_val $ pte_type p) $
-  bf_cons (range_of 2 10) (bf_val $ pte_leaf_attr_lo p) $
-  bf_cons (range_of 12 36) (bf_val $ pte_addr p) $
-  bf_cons (range_of 48 3) (bf_val $ pte_undef p) $
-  bf_cons (range_of 51 13) (bf_val $ pte_leaf_attr_hi p) $
-  bf_nil.
-
-Arguments pte_repr _/.
-
-Definition pte_wf (p : Pte) : Prop :=
-  0 ≤ bool_to_Z $ pte_valid p < 2^1 ∧
-  0 ≤ pte_type p < 2^1 ∧
-  0 ≤ pte_leaf_attr_lo p < 2^10 ∧
-  0 ≤ pte_addr p < 2^36 ∧
-  0 ≤ pte_undef p < 2^3 ∧
-  0 ≤ pte_leaf_attr_hi p < 2^13.
-
-Global Program Instance Pte_BitfieldDesc : 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 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.
-Next Obligation. done. Qed.
-(* 
-Example pte_repr_sound p :
-  pte_wf p → check_has_ty (pte_repr p) (bv bitfield_sig).
-Admitted. *)
-
-Global Instance simpl_exist_Pte P : SimplExist Pte P
-  (∃ valid type leaf_attr_lo addr undef leaf_attr_hi,
-    P {|
-      pte_valid := valid;
-      pte_type := type;
-      pte_leaf_attr_lo := leaf_attr_lo;
-      pte_addr := addr;
-      pte_undef := undef;
-      pte_leaf_attr_hi := leaf_attr_hi;
-    |}).
-Proof. unfold SimplExist. naive_solver. Qed.
-Global Instance simpl_forall_Pte P : SimplForall Pte 6 P
-  (∀ valid type leaf_attr_lo addr undef leaf_attr_hi,
-    P {|
-      pte_valid := valid;
-      pte_type := type;
-      pte_leaf_attr_lo := leaf_attr_lo;
-      pte_addr := addr;
-      pte_undef := undef;
-      pte_leaf_attr_hi := leaf_attr_hi;
-    |}).
-Proof. unfold SimplForall => ? []. naive_solver. Qed.
-
-(* pte attr *)
-
-Record Attr := {
-  attr_lo_s1_attridx : Z;
-  attr_lo_s1_ap : Z;
-  attr_lo_s1_sh : Z;
-  attr_lo_s1_af : bool;
-  attr_hi_s1_xn : bool;
-}.
-
-Definition attr_repr (a : Attr) : tm :=
-  bf_cons (range_of 2 3) (bf_val $ attr_lo_s1_attridx a) $
-  bf_cons (range_of 6 2) (bf_val $ attr_lo_s1_ap a) $
-  bf_cons (range_of 8 2) (bf_val $ attr_lo_s1_sh a) $
-  bf_cons (range_of 10 1) (bf_val $ Z_of_bool $ attr_lo_s1_af a) $
-  bf_cons (range_of 54 1) (bf_val $ Z_of_bool $ attr_hi_s1_xn a)
-  bf_nil.
-
-Arguments attr_repr _/.
-
-Definition attr_wf (a : Attr) : Prop :=
-  0 ≤ attr_lo_s1_attridx a < 2^2 ∧
-  0 ≤ attr_lo_s1_ap a < 2^2 ∧
-  0 ≤ attr_lo_s1_sh a < 2^2 ∧
-  0 ≤ bool_to_Z $ attr_lo_s1_af a < 2^1 ∧
-  0 ≤ bool_to_Z $ attr_hi_s1_xn a < 2^1.
-
-Global Program Instance Attr_BitfieldDesc : BitfieldDesc Attr := {|
-  bitfield_it := u64;
-  bitfield_repr := attr_repr;
-  bitfield_wf := attr_wf;
-  bitfield_sig := {|
-    sig_bits := 64;
-    sig_ranges := [# (range_of 2 3); (range_of 6 2); (range_of 8 2); (range_of 10 1);
-      (range_of 54 1)]
-  |}
-|}.
-Next Obligation. solve_ranges_monotone. Qed.
-Next Obligation. sig_max_range_bounded. Qed.
-Next Obligation. done. Qed.
-
-(* pte prot *)
-
-Record Prot := {
-  prot_x : bool;
-  prot_w : bool;
-  prot_r : bool;
-  prot_device : bool;
-}.
-
-Definition prot_repr (p : Prot) : tm :=
-  bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ prot_x p) $
-  bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ prot_w p) $
-  bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ prot_r p) $
-  bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ prot_device p) $
-  bf_nil.
-
-Arguments prot_repr _/.
-
-Definition prot_wf (p : Prot) : Prop :=
-  0 ≤ bool_to_Z $ prot_x p < 2^1 ∧
-  0 ≤ bool_to_Z $ prot_w p < 2^1 ∧
-  0 ≤ bool_to_Z $ prot_r p < 2^1 ∧
-  0 ≤ bool_to_Z $ prot_device p < 2^1.
-
-Global Program Instance Prot_BitfieldDesc : BitfieldDesc Prot := {|
-  bitfield_it := u64;
-  bitfield_repr := prot_repr;
-  bitfield_wf := prot_wf;
-  bitfield_sig := {|
-    sig_bits := 64;
-    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_Prot P : SimplExist Prot P (∃ x w r device,
-  P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
-Proof. unfold SimplExist. naive_solver. Qed.
-Global Instance simpl_forall_Prot P : SimplForall Prot 4 P (∀ x w r device,
-  P {| prot_x := x; prot_w := w; prot_r := r; prot_device := device |}).
-Proof. unfold SimplForall => ? []. naive_solver. Qed.
-
-(* struct, const *)
-
-Record mm_callbacks := {
-  virt_to_phys : Z → Pte;
-}.
-
-Definition max_level : Z := 4.
-Definition mtype_device : Z := 5.
-Definition mtype_normal : Z := 0.
-Definition pte_type_block : Z := 0.
-Definition pte_type_page : Z := 1.
-Definition pte_type_table : Z := 1.
-Definition ap_rw : Z := 1.
-Definition ap_ro : Z := 3.
-Definition sh_is : Z := 3.
-Definition err_code : Z := 22.