Generate lemmas and prove them

arch/cortex-m/src/mpu.rs

@@ -484,7 +484,8 @@ impl mpu::RegionDescriptor for CortexMRegion {
                     Self::start(p.fst),
                     Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
                     permissions
-                )
+                ) &&
+                valid_size(Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd))
             )
         }> requires valid_size(available_start + available_size) && max_region_number > 0 && max_region_number < 8
     )]
@@ -520,7 +521,7 @@ impl mpu::RegionDescriptor for CortexMRegion {
         // region size must be aligned to start
         start = align(start, region_size);
         // RJ: start = u32::MAX, region_size = u32::MAX/2 --> start + region_size overflows!
-         if start > overflow_bound {
+         if start > overflow_bound || size > (u32::MAX as usize) - start {
             // RJ: defensively adding check as otherwise `start + region_size` can overflow?
             return None;
         }

arch/cortex-m/src/tcb/theorems.rs

@@ -19,19 +19,19 @@ pub fn theorem_to_pow2_gt1(x: usize) {}
 #[flux_rs::sig(fn (usize[@n]) requires n < 32 ensures pow2(to_pow2(n)))]
 pub fn theorem_to_pow2_is_pow2(_n: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (usize[@x], usize[@y], usize[@z]) requires aligned(x, y) && z <= y && pow2(y) && pow2(z) ensures aligned(x, z))]
 pub fn theorem_pow2_le_aligned(x: usize, y: usize, z: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (r:usize) requires pow2(r) && r >= 8 ensures octet(r))]
 pub fn theorem_pow2_octet(_n: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (n:usize) requires pow2(n) && n >= 4 ensures pow2(n / 2))]
 pub fn theorem_pow2_div2_pow2(_n: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (n:usize) requires pow2(n) && n >= 2 ensures (n / 2) * 2 == n)]
 pub fn theorem_div2_pow2(_n: usize) {}
 
@@ -43,7 +43,7 @@ pub fn theorem_div_octet(_n: usize) {}
 #[flux_rs::sig(fn (x: usize, y: usize) requires aligned(x, y) ensures aligned(x + y, y))]
 pub fn theorem_aligned_plus_aligned_to_is_aligned(_x: usize, _y: usize) {}
 
-#[flux_rs::trusted(reason = "math")]
+#[flux_rs::proven_externally]
 #[flux_rs::sig(fn (x: usize, y: usize) requires y >= 32 && pow2(y) && aligned(x, y) ensures least_five_bits(bv32(x)) == 0)]
 pub fn theorem_aligned_value_ge32_lowest_five_bits0(x: usize, y: usize) {}
 

flux_support/src/flux_ptr.rs

@@ -157,7 +157,7 @@ impl FluxPtr {
         let n = self.as_usize();
         if offset <= u32::MAX as usize {
             // offset in bounds; test addition
-            n + offset <= (u32::MAX as usize)
+            n <= (u32::MAX as usize) - offset
         } else {
             // offset itself is out of bounds
             false

kernel/src/allocator.rs

@@ -411,7 +411,8 @@ impl<R: RegionDescriptor + Display + Copy> AppMemoryAllocator<R> {
                     R::start(p.fst),
                     R::start(p.fst) + R::size(p.fst) + R::size(p.snd),
                     mpu::Permissions { r: true, w: true, x: false }
-                )
+                ) &&
+                valid_size(R::start(p.fst) + R::size(p.fst) + R::size(p.snd))
             )
         }, ()>
     )]
@@ -466,7 +467,11 @@ impl<R: RegionDescriptor + Display + Copy> AppMemoryAllocator<R> {
                 unallocated_memory_start + unallocated_memory_size <= u32::MAX &&
                 unallocated_memory_start > 0 &&
                 initial_kernel_memory_size > 0 &&
-                flash_start + flash_size < unallocated_memory_start
+                flash_start + flash_size < unallocated_memory_start &&
+                valid_size(R::start(ram_regions.fst) + R::size(ram_regions.fst) + initial_kernel_memory_size) &&
+                (R::is_set(ram_regions.snd) => (
+                    valid_size(initial_kernel_memory_size + R::start(ram_regions.fst) + R::size(ram_regions.fst) + R::size(ram_regions.snd))
+                ))
     )]
     fn get_app_breaks(
         ram_regions: Pair<R, R>,
@@ -578,10 +583,24 @@ impl<R: RegionDescriptor + Display + Copy> AppMemoryAllocator<R> {
         let Some(ram0_size) = ram_regions.fst.size() else {
             return Err(AllocateAppMemoryError::HeapError);
         };
+        let Some(ram0_start) = ram_regions.fst.start() else {
+            return Err(AllocateAppMemoryError::HeapError);
+        };
         if ram0_size > (u32::MAX as usize) - initial_kernel_memory_size {
             return Err(AllocateAppMemoryError::HeapError);
         }
 
+        if ram0_size + initial_kernel_memory_size
+                > (u32::MAX as usize) - ram0_start.as_usize() {
+                    return Err(AllocateAppMemoryError::HeapError);   
+                }
+        if ram_regions.snd.is_set()
+            && ram0_size + initial_kernel_memory_size
+                > (u32::MAX as usize) - ram_regions.snd.size().unwrap() - ram0_start.as_usize()
+        {
+            return Err(AllocateAppMemoryError::HeapError);
+        }
+
         // Get the app breaks using the RAM region
         let breaks = Self::get_app_breaks(
             ram_regions,

kernel/src/platform/mpu.rs

@@ -183,7 +183,8 @@ pub trait RegionDescriptor: core::marker::Sized {
                     Self::start(p.fst),
                     Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
                     permissions
-                )
+                ) &&
+                valid_size(Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd))
             )
         }> requires valid_size(available_start + available_size) && max_region_number > 0 && max_region_number < 8
     )]
@@ -387,7 +388,8 @@ impl RegionDescriptor for MpuRegionDefault {
                     Self::start(p.fst),
                     Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd),
                     permissions
-                )
+                ) &&
+                valid_size(Self::start(p.fst) + Self::size(p.fst) + Self::size(p.snd))
             )
         }> requires max_region_number > 0 && max_region_number < 8)]
     fn allocate_regions(

lean_proofs/.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

lean_proofs/.gitignore

@@ -0,0 +1 @@
+/.lake

lean_proofs/LeanProofs.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `LeanProofs` library.
+-- Import modules here that should be built as part of the library.
+import LeanProofs.Basic

lean_proofs/LeanProofs/Basic.lean

@@ -0,0 +1 @@
+def hello := "world"

lean_proofs/LeanProofs/SharedLemmas.lean

@@ -0,0 +1,143 @@
+namespace Nat
+
+def bit (b : Bool) : Nat → Nat := cond b (2 * · + 1) (2 * ·)
+
+theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl
+
+@[simp]
+theorem bit_decide_mod_two_eq_one_shiftRight_one (n : Nat) : bit (n % 2 = 1) (n >>> 1) = n := by
+  simp only [bit, shiftRight_one]
+  cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2
+
+theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by
+  simp
+
+/-- A recursion principle for `bit` representations of natural numbers.
+  For a predicate `motive : Nat → Sort u`, if instances can be
+  constructed for natural numbers of the form `bit b n`,
+  they can be constructed for all natural numbers. -/
+@[elab_as_elim, specialize]
+def binaryRec {motive : Nat → Sort u} (z : motive 0) (f : ∀ b n, motive n → motive (bit b n))
+    (n : Nat) : motive n :=
+  if n0 : n = 0 then congrArg motive n0 ▸ z
+  else
+    let x := f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))
+    congrArg motive n.bit_testBit_zero_shiftRight_one ▸ x
+decreasing_by exact bitwise_rec_lemma n0
+
+end Nat
+
+theorem le_max_of_nat_eq_of_nat {w : Nat} (x y : Nat) :
+    x < 2 ^ w → y < 2 ^ w → (BitVec.ofNat w x = BitVec.ofNat w y ↔ x = y) := by
+  intros hx hy
+  apply Iff.intro
+  case mp =>
+    intro bv_eq
+    have fin_eq := congrArg BitVec.toFin bv_eq
+    simp [BitVec.toFin_ofNat, Fin.ofNat] at fin_eq
+    rw [Nat.mod_eq_of_lt, Nat.mod_eq_of_lt] at fin_eq
+    exact fin_eq
+    exact hy
+    exact hx
+  case mpr =>
+    intro eq
+    rw [eq]
+
+@[simp]
+def pow2 (n : Nat) : Bool :=
+  (n > 0) && ((n &&& (n - 1)) == 0)
+
+def i_pow2 (n : Int) : Bool :=
+  (let a3 := (BitVec.ofInt 32 n); ((n > 0) && ((BitVec.and a3 (BitVec.sub a3 1#32)) = 0#32)))
+
+theorem i_pow2_eq_pow2 (x: Nat) : (x < 2 ^ 32) -> (i_pow2 x <-> pow2 x) := by
+  unfold i_pow2 pow2
+  simp
+  intros x_in_bounds xgt0
+  apply Iff.intro
+  case mp =>
+    intros bv_eq
+    rw [
+      BitVec.ofNat_sub_ofNat_of_le,
+      ← BitVec.ofNat_and,
+      le_max_of_nat_eq_of_nat
+    ] at bv_eq
+    exact bv_eq
+    case _ =>
+      apply Nat.lt_of_le_of_lt
+      exact @Nat.and_le_right x (x - 1)
+      apply Nat.lt_trans (by omega : (x - 1) < x)
+      simp; exact x_in_bounds
+    case _ =>
+      simp
+    case _ =>
+      simp
+    case _ =>
+      exact xgt0
+  case mpr =>
+    intros bv_eq
+    rw [
+      BitVec.ofNat_sub_ofNat_of_le,
+      ← BitVec.ofNat_and,
+      le_max_of_nat_eq_of_nat
+    ]
+    exact bv_eq
+    case _ =>
+      apply Nat.lt_of_le_of_lt
+      exact @Nat.and_le_right x (x - 1)
+      apply Nat.lt_trans (by omega : (x - 1) < x)
+      simp; exact x_in_bounds
+    case _ => simp
+    case _ => simp
+    case _ => exact xgt0
+
+theorem fold_land : (Nat.bitwise and x x) = x &&& x := by rfl
+
+theorem pow2_isPowerOfTwo (x : Nat) : pow2 x <-> x.isPowerOfTwo := by
+  apply Iff.intro
+  case mp =>
+    intro h
+    induction x using Nat.binaryRec
+    case z => simp_all!
+    case f b n ih =>
+      simp_all [Nat.bit]
+      cases b
+      · simp_all!
+        rcases h with ⟨_, h⟩
+        rw [Nat.mul_comm]
+        apply Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo
+        apply ih
+        simp_all [HAnd.hAnd, AndOp.and, Nat.land]
+        unfold Nat.bitwise at h
+        split at h ; omega
+        split at h ; omega
+        simp_all
+        have p : (2 * n - 1) /2 = n - 1 := by cases n ; trivial ; simp +arith [Nat.left_distrib, Nat.mul_add_div]
+        simp_all
+      · simp_all
+        simp [HAnd.hAnd, AndOp.and, Nat.land] at h
+        unfold Nat.bitwise at h
+        split at h ; simp_all
+        split at h ; simp_all ; exists 0
+        simp_all [Nat.mul_add_div, fold_land]
+  case mpr =>
+    intro h
+    rcases h with ⟨n, h⟩
+    simp
+    and_intros
+    · simp_all ; apply Nat.pow_pos ; simp
+    · induction n generalizing x <;> simp_all
+
+theorem i_pow2_0_is_power_of_2 (x: Nat) : (x < 2 ^ 32) -> (i_pow2 x <-> x.isPowerOfTwo) := by
+  intro x_in_bounds
+  apply Iff.intro
+  case _ =>
+    intro x_pow2
+    rw [← pow2_isPowerOfTwo x]
+    apply (i_pow2_eq_pow2 x x_in_bounds).mp
+    exact x_pow2
+  case _ =>
+    intro x_pow2
+    apply (i_pow2_eq_pow2 x x_in_bounds).mpr
+    rw [pow2_isPowerOfTwo]
+    exact x_pow2

lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean

@@ -0,0 +1,11 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_aligned_1 (a2 : Int) (a3 : Int) : Bool :=
+  ((a2 % a3) = 0)
+
+def f_pow2_0 (a0 : Int) : Bool :=
+  (let a1 := (BitVec.ofInt 32 a0); ((a0 > 0) && ((BitVec.and a1 (BitVec.sub a1 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0 : Prop := (∀ (reftgen_x_0 : Int), (∀ (reftgen_y_1 : Int), (∀ (__ : Int), (((reftgen_y_1 ≥ 32) ∧ (f_pow2_0 reftgen_y_1) ∧ (f_aligned_1 reftgen_x_0 reftgen_y_1)) -> (∀ (__ : Int), ((reftgen_x_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_x_0 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 4294967295) -> ((BitVec.and (BitVec.ofInt 32 reftgen_x_0) 31#32) = 0#32)))))))))))))
+

lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean

@@ -0,0 +1,37 @@
+import LeanProofs.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0
+import LeanProofs.SharedLemmas
+import Init.Data.BitVec.Lemmas
+
+
+theorem f_pow2_0_eq_i_pow2 : f_pow2_0 = i_pow2 := by
+  funext x ; unfold f_pow2_0 i_pow2 ; simp
+
+def tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0_proof : tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0 := by
+  unfold tcb_theorems_theorem_aligned_value_ge32_lowest_five_bits0
+  intro x y _ h _ x_ge0 _ x_in_bounds _ y_ge0 _ y_in_bounds
+  obtain ⟨y_ge32, y_pow2, x_aligned_y⟩ := h
+  rw [f_pow2_0_eq_i_pow2] at *
+  unfold f_aligned_1 at x_aligned_y; simp at x_aligned_y
+  rw [
+    ← Int.toNat_of_nonneg x_ge0,
+    BitVec.ofInt_natCast,
+    BitVec.and_eq,
+    ←BitVec.ofNat_and
+  ]
+  simp [Nat.and_two_pow_sub_one_eq_mod _ 5]
+  have xnat_aligned_ynat : x.toNat % y.toNat = 0 := by
+    rw [← Int.toNat_emod x_ge0 y_ge0, x_aligned_y]
+    simp
+  rw [← Int.toNat_of_nonneg y_ge0] at y_pow2
+  have ynat_pow2 := (i_pow2_0_is_power_of_2 y.toNat (by omega)).mp y_pow2
+  rcases ynat_pow2 with ⟨k, hk⟩
+  rw [hk] at xnat_aligned_ynat
+  have ynat_dvd_xnat := Nat.dvd_of_mod_eq_zero xnat_aligned_ynat
+  have thirty_two_dvd_x : 32 ∣ x.toNat := by
+    apply @Nat.pow_dvd_of_le_of_pow_dvd 2 5 k
+    · apply (@Nat.pow_le_pow_iff_right 2 5 k (by omega)).mp
+      rw [← hk]
+      omega
+    · assumption
+  have x_mod_32_eq_0 := Nat.mod_eq_zero_of_dvd thirty_two_dvd_x
+  rw [x_mod_32_eq_0]

lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean

@@ -0,0 +1,8 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_pow2_0 (a0 : Int) : Bool :=
+  (let a1 := (BitVec.ofInt 32 a0); ((a0 > 0) && ((BitVec.and a1 (BitVec.sub a1 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_div2_pow2 : Prop := (∀ (reftgen_n_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_n_0) ∧ (reftgen_n_0 ≥ 2)) -> (∀ (__ : Int), ((reftgen_n_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_n_0 ≤ 4294967295) -> (((reftgen_n_0 / 2) * 2) = reftgen_n_0))))))))
+

lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean

@@ -0,0 +1,20 @@
+import LeanProofs.TcbTheoremsTheoremDiv2Pow2
+import LeanProofs.SharedLemmas
+
+theorem f_pow2_0_eq_i_pow2 : f_pow2_0 = i_pow2 := by
+  funext x; unfold f_pow2_0 i_pow2; simp
+
+def tcb_theorems_theorem_div2_pow2_proof : tcb_theorems_theorem_div2_pow2 := by
+  unfold tcb_theorems_theorem_div2_pow2
+  intro n _ h _ n_ge0 _ n_in_bounds
+  obtain ⟨n_pow2, n_ge2⟩ := h
+  rw [f_pow2_0_eq_i_pow2] at *
+  have res_nat : (n.toNat / 2) * 2 = n.toNat := by
+    rw [Nat.div_mul_cancel]
+    rw [←Int.toNat_of_nonneg n_ge0] at n_pow2
+    have nnat_pow2 := (i_pow2_0_is_power_of_2 n.toNat (by omega)).mp n_pow2
+    rcases nnat_pow2 with ⟨k, hy⟩
+    cases k with
+    | zero => omega
+    | succ k' => omega
+  omega

lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean

@@ -0,0 +1,8 @@
+-- GENERATED; DO NOT EDIT --
+-- FUNCTIONS --
+def f_pow2_0 (a0 : Int) : Bool :=
+  (let a1 := (BitVec.ofInt 32 a0); ((a0 > 0) && ((BitVec.and a1 (BitVec.sub a1 1#32)) = 0#32)))
+
+-- THEOREM --
+def tcb_theorems_theorem_pow2_div2_pow2 : Prop := (∀ (reftgen_n_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_n_0) ∧ (reftgen_n_0 ≥ 4)) -> (∀ (__ : Int), ((reftgen_n_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_n_0 ≤ 4294967295) -> (f_pow2_0 (reftgen_n_0 / 2)))))))))
+