some coq refactoring

Signed-off-by: Lennard Gäher <l.gaeher@posteo.de>

security-monitor/src/core/architecture/riscv/mmu/page_size.rs

@@ -1,7 +1,7 @@
 // SPDX-FileCopyrightText: 2023 IBM Corporation
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
-#![rr::import("ace.theories.page", "page_extra")]
+#![rr::import("ace.theories.page_allocator", "page")]
 #![rr::include("option")]
 
 // The order of page size in this enum must follow the increasing sizes of page to guarantee that the Ord/PartialOrd are correctly derived

security-monitor/src/core/memory_layout/confidential_memory_address.rs

@@ -1,7 +1,6 @@
 // SPDX-FileCopyrightText: 2023 IBM Corporation
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
-#![rr::import("ace.theories.result", "result")]
 use crate::error::Error;
 use pointers_utility::{ptr_byte_add_mut, ptr_byte_offset};
 

security-monitor/src/core/page_allocator/allocator.rs

@@ -6,7 +6,7 @@
 #![rr::include("btreemap")]
 #![rr::include("vec")]
 #![rr::include("spin")]
-#![rr::import("ace.theories.page_allocator", "page_allocator_extra")]
+#![rr::import("ace.theories.page_allocator", "page_allocator")]
 use super::page::{Page, UnAllocated};
 use crate::core::architecture::PageSize;
 use crate::core::memory_layout::{ConfidentialMemoryAddress, MemoryLayout};

security-monitor/src/core/page_allocator/page.rs

@@ -1,7 +1,7 @@
 // SPDX-FileCopyrightText: 2023 IBM Corporation
 // SPDX-FileContributor: Wojciech Ozga <woz@zurich.ibm.com>, IBM Research - Zurich
 // SPDX-License-Identifier: Apache-2.0
-#![rr::import("ace.theories.page", "page_extra")]
+#![rr::import("ace.theories.page_allocator", "page")]
 use crate::core::architecture::PageSize;
 use crate::core::control_data::{DigestType, MeasurementDigest};
 use crate::core::memory_layout::{ConfidentialMemoryAddress, MemoryLayout, NonConfidentialMemoryAddress};

verification/theories/base/base.v

@@ -0,0 +1,12 @@
+From refinedrust Require Import typing.
+
+(** * Lemmas that should probably be upstreamed *)
+
+Lemma aligned_to_mul_inv l al num :
+  l `aligned_to` al * num →
+  l `aligned_to` al.
+Proof.
+  rewrite /aligned_to.
+  destruct caesium_config.enforce_alignment; last done.
+  intros (k & Heq). intros. exists (k * num). lia.
+Qed.

verification/theories/result/dune → verification/theories/base/dune

@@ -1,6 +1,6 @@
 (coq.theory
- (name ace.theories.result)
+ (name ace.theories.base)
  (package ace)
  (flags -w -notation-overridden -w -redundant-canonical-projection)
- (synopsis "core::result::Result")
+ (synopsis "Basic lemmas")
  (theories stdpp iris Ltac2 caesium lithium lrust RecordUpdate Equations refinedrust))

verification/theories/memory_layout/memory_layout.v

@@ -1,5 +1,7 @@
 From refinedrust Require Import typing.
 
+(** * Additional definitions for the security monitor's global memory layout *)
+
 Record memory_layout : Type := mk_memory_layout {
   conf_start : loc;
   conf_end : loc;

verification/theories/memory_tracker/page_allocator/dune → verification/theories/page_allocator/dune

@@ -2,5 +2,5 @@
  (name ace.theories.page_allocator)
  (package ace)
  (flags -w -notation-overridden -w -redundant-canonical-projection)
- (synopsis "Manual proofs for ACE Security Monitor page")
- (theories stdpp iris Ltac2 caesium lithium lrust RecordUpdate Equations refinedrust ace.theories.page))
+ (synopsis "Manual proofs for ACE Security Monitor page allocator")
+ (theories stdpp iris Ltac2 caesium lithium lrust RecordUpdate Equations refinedrust ace.theories.base))

verification/theories/memory_tracker/page/page_extra.v → verification/theories/page_allocator/page.v

@@ -1,7 +1,9 @@
 From refinedrust Require Import typing.
+From ace.theories.base Require Import base.
 
+(** * Extra theories for page sizes and pages *)
 
-(* This reflects the page sizes in [core/mmu/page_size.rs] *)
+(* This reflects the page sizes in [core/architecture/riscv/mmu/page_size.rs] *)
 Inductive page_size : Set :=
   | Size4KiB
   | Size16KiB
@@ -16,9 +18,29 @@ Global Instance page_size_eqdec : EqDecision page_size.
 Proof. solve_decision. Defined.
 Global Instance page_size_countable : Countable page_size.
 Proof.
-  (* TODO *)
-Admitted.
+  refine (inj_countable (λ sz,
+    match sz with
+    | Size4KiB => 0
+    | Size16KiB => 1
+    | Size2MiB => 2
+    | Size1GiB => 3
+    | Size512GiB => 4
+    | Size128TiB => 5
+    end)
+    (λ a,
+    match a with
+    | 0 => Some Size4KiB
+    | 1 => Some Size16KiB
+    | 2 => Some Size2MiB
+    | 3 => Some Size1GiB 
+    | 4 => Some Size512GiB 
+    | 5 => Some Size128TiB
+    | _ => None
+    end) _).
+  intros []; naive_solver.
+Qed.
 
+(** Number of 64-bit machine words in a page size *)
 Definition page_size_in_words_nat (sz : page_size) : nat :=
   match sz with
   | Size4KiB => 512
@@ -34,7 +56,7 @@ Definition page_size_in_bytes_nat (sz : page_size) : nat :=
 Definition page_size_in_bytes_Z (sz : page_size) : Z :=
   page_size_in_bytes_nat sz.
 
-
+(** The next smaller page size *)
 Definition page_size_smaller (sz : page_size) : option page_size :=
   match sz with
   | Size4KiB => None
@@ -44,6 +66,7 @@ Definition page_size_smaller (sz : page_size) : option page_size :=
   | Size512GiB => Some Size1GiB
   | Size128TiB => Some Size512GiB
   end.
+(** The next larger page size *)
 Definition page_size_larger (sz : page_size) : option page_size :=
   match sz with
   | Size4KiB => Some Size16KiB
@@ -54,7 +77,8 @@ Definition page_size_larger (sz : page_size) : option page_size :=
   | Size128TiB => None
   end.
 
-(* Pages should be aligned to the size of the page *)
+(** Pages should be aligned to the size of the page; 
+  compute the log2 of this page's alignment *)
 Definition page_size_align_log (sz : page_size) : nat :=
   match sz with
   | Size4KiB => 12
@@ -85,9 +109,14 @@ Definition MAX_PAGE_ADDR_unfold : MAX_PAGE_ADDR = MAX_PAGE_ADDR_def :=
   seal_eq MAX_PAGE_ADDR_aux.
 
 (** * Pages *)
+(** Page containing zeroes *)
 Definition zero_page (sz : page_size) : list Z :=
   replicate (page_size_in_words_nat sz) 0.
 
+(** Logical representation of a page, consisting of:
+   - its location in memory
+   - its size
+   - its list of words, represented as integers *)
 Record page : Type := mk_page {
   page_loc : loc;
   page_sz : page_size;
@@ -99,9 +128,12 @@ Global Instance page_eqdec : EqDecision page.
 Proof. solve_decision. Defined.
 Global Instance page_countable : Countable page.
 Proof.
-  (* TODO *)
-Admitted.
+  refine (inj_countable' (λ p, (p.(page_loc), p.(page_sz), p.(page_val)))
+    (λ p, mk_page p.1.1 p.1.2 p.2) _).
+  intros []; done.
+Qed.
 
+(** One-past-the-end location of this page *)
 Definition page_end_loc (p : page) : loc :=
   p.(page_loc) +ₗ (page_size_in_bytes_Z p.(page_sz)).
 
@@ -114,7 +146,9 @@ Infix "≤ₚ" := page_size_le (at level 50).
 
 (** Well-formedness of a page *)
 Definition page_wf (p : page) : Prop :=
+  (** The value has the right size *)
   page_size_in_words_nat p.(page_sz) = length p.(page_val) ∧
+  (** The location has the right alignment *)
   p.(page_loc) `aligned_to` page_size_align p.(page_sz).
 
 (** The list of [pages] forms a contiguous region of memory, one page after another. *)
@@ -143,7 +177,7 @@ Proof.
 Qed.
 
 
-(* How many pages of the next smaller page size are there in this page size? *)
+(** How many pages of the next smaller page size are there in this page size? *)
 Definition page_size_multiplier_log (sz : page_size) : nat :=
   match sz with
   | Size4KiB => 0
@@ -183,7 +217,7 @@ Proof.
   f_equiv. by apply page_size_multiplier_align_log.
 Qed.
 
-(* Divide a page into pages of the next smaller page size *)
+(** Divide a page into pages of the next smaller page size *)
 Definition subdivide_page (p : page) : list page :=
   match page_size_smaller p.(page_sz) with
   | None => [p]
@@ -225,16 +259,6 @@ Proof.
   apply (IH (S start)).
 Qed.
 
-(* TODO move *)
-Lemma aligned_to_mul_inv l al num :
-  l `aligned_to` al * num →
-  l `aligned_to` al.
-Proof.
-  rewrite /aligned_to.
-  destruct caesium_config.enforce_alignment; last done.
-  intros (k & Heq). intros. exists (k * num). lia.
-Qed.
-
 Lemma subdivide_page_wf p :
   page_wf p →
   Forall page_wf (subdivide_page p).

verification/theories/memory_tracker/page_allocator/page_allocator_extra.v → verification/theories/page_allocator/page_allocator.v

@@ -1,6 +1,6 @@
 From refinedrust Require Import typing.
 From refinedrust Require Import ghost_var_dfrac.
-From ace.theories.page Require Import page_extra.
+From ace.theories.page_allocator Require Import page.
 
 (** * Page allocator ghost state *)
 Record memory_region := {

verification/theories/page_table/dune

@@ -3,4 +3,4 @@
  (package ace)
  (flags -w -notation-overridden -w -redundant-canonical-projection)
  (synopsis "Manual proofs for ACE Security Monitor page table")
- (theories stdpp iris Ltac2 caesium lithium lrust RecordUpdate Equations refinedrust ace.theories.page))
+ (theories stdpp iris Ltac2 caesium lithium lrust RecordUpdate Equations refinedrust ace.theories.page_allocator))

verification/theories/page_table/page_table.v

@@ -1,5 +1,5 @@
 From refinedrust Require Import typing.
-From ace.theories.page Require Import page_extra.
+From ace.theories.page_allocator Require Import page.
 From stdpp Require Import bitvector.
 
 (* Based on Release riscv-isa-release-7b8ddc9-2024-05-07 *)