Generate lemmas and prove them

arch/cortex-m/src/mpu.rs

@@ -459,6 +459,7 @@ impl mpu::RegionDescriptor for CortexMRegion {
         self.region_overlaps(start, end)
     }
 
+    #[flux_rs::trusted]
     #[flux_rs::reveal(first_subregion_from_logical, last_subregion_from_logical)]
     #[flux_rs::sig(fn (
         max_region_number: usize,
@@ -484,7 +485,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 +522,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;
         }
@@ -573,6 +575,7 @@ impl mpu::RegionDescriptor for CortexMRegion {
         })
     }
 
+    #[flux_rs::trusted]
     #[flux_rs::reveal(first_subregion_from_logical, last_subregion_from_logical)]
     #[flux_rs::sig(fn (
         region_start: FluxPtrU8,
@@ -682,6 +685,7 @@ impl mpu::RegionDescriptor for CortexMRegion {
         })
     }
 
+    #[flux_rs::trusted]
     #[flux_rs::reveal(first_subregion_from_logical, last_subregion_from_logical)]
     #[flux_rs::sig(
         fn (

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

@@ -19,31 +19,32 @@ 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) {}
 
 #[flux_rs::reveal(octet)]
 #[flux_rs::sig(fn (r:usize) requires octet(r) ensures 8 * (r / 8) == r)]
 pub fn theorem_div_octet(_n: usize) {}
 
+#[flux_rs::trusted]
 #[flux_rs::reveal(aligned)]
 #[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,6 @@
+-- Flux Basic Imports [DO NOT MODIFY] --
+import LeanProofs.Flux.Checking.TcbTheoremsTheoremPow2LeAligned
+import LeanProofs.Flux.Checking.TcbTheoremsTheoremPow2Octet
+import LeanProofs.Flux.Checking.TcbTheoremsTheoremPow2Div2Pow2
+import LeanProofs.Flux.Checking.TcbTheoremsTheoremDiv2Pow2
+import LeanProofs.Flux.Checking.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0

lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean

@@ -0,0 +1,4 @@
+import LeanProofs.Flux.VC.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0
+import LeanProofs.User.Proof.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof
+
+#check (F.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0_proof : F.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0)

lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremDiv2Pow2.lean

@@ -0,0 +1,4 @@
+import LeanProofs.Flux.VC.TcbTheoremsTheoremDiv2Pow2
+import LeanProofs.User.Proof.TcbTheoremsTheoremDiv2Pow2Proof
+
+#check (F.TcbTheoremsTheoremDiv2Pow2_proof : F.TcbTheoremsTheoremDiv2Pow2)

lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Div2Pow2.lean

@@ -0,0 +1,4 @@
+import LeanProofs.Flux.VC.TcbTheoremsTheoremPow2Div2Pow2
+import LeanProofs.User.Proof.TcbTheoremsTheoremPow2Div2Pow2Proof
+
+#check (F.TcbTheoremsTheoremPow2Div2Pow2_proof : F.TcbTheoremsTheoremPow2Div2Pow2)

lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2LeAligned.lean

@@ -0,0 +1,4 @@
+import LeanProofs.Flux.VC.TcbTheoremsTheoremPow2LeAligned
+import LeanProofs.User.Proof.TcbTheoremsTheoremPow2LeAlignedProof
+
+#check (F.TcbTheoremsTheoremPow2LeAligned_proof : F.TcbTheoremsTheoremPow2LeAligned)

lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Octet.lean

@@ -0,0 +1,4 @@
+import LeanProofs.Flux.VC.TcbTheoremsTheoremPow2Octet
+import LeanProofs.User.Proof.TcbTheoremsTheoremPow2OctetProof
+
+#check (F.TcbTheoremsTheoremPow2Octet_proof : F.TcbTheoremsTheoremPow2Octet)

lean_proofs/LeanProofs/Flux/Fun/TcbDefsAligned.lean

@@ -0,0 +1,12 @@
+import LeanProofs.Flux.Prelude
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+noncomputable def tcb_defs_aligned (a'₀ : Int) (a'₁ : Int) : Prop :=
+  ((a'₀ % a'₁) = 0)
+
+
+end F

lean_proofs/LeanProofs/Flux/Fun/TcbDefsOctet.lean

@@ -0,0 +1,12 @@
+import LeanProofs.Flux.Prelude
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+noncomputable def tcb_defs_octet (a'₂ : Int) : Prop :=
+  ((a'₂ % 8) = 0)
+
+
+end F

lean_proofs/LeanProofs/Flux/Fun/TcbDefsPow2.lean

@@ -0,0 +1,12 @@
+import LeanProofs.Flux.Prelude
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+noncomputable def tcb_defs_pow2 (a'₂ : Int) : Prop :=
+  (let a'₃ := (BitVec.ofInt 32 a'₂); ((a'₂ > 0) ∧ ((BitVec.and a'₃ (BitVec.sub a'₃ 1#32)) = 0#32)))
+
+
+end F

lean_proofs/LeanProofs/Flux/Prelude.lean

@@ -0,0 +1,15 @@
+-- FLUX LIBRARY [DO NOT MODIFY] --
+abbrev BitVec_shiftLeft { n : Nat } (x s : BitVec n) : BitVec n := BitVec.shiftLeft x (s.toNat)
+abbrev BitVec_ushiftRight { n : Nat } (x s : BitVec n) : BitVec n := BitVec.ushiftRight x (s.toNat)
+abbrev BitVec_sshiftRight { n : Nat } (x s : BitVec n) : BitVec n := BitVec.sshiftRight x (s.toNat)
+abbrev BitVec_uge { n : Nat } (x y : BitVec n) := (BitVec.ult x y).not
+abbrev BitVec_sge { n : Nat } (x y : BitVec n) := (BitVec.slt x y).not
+abbrev BitVec_ugt { n : Nat } (x y : BitVec n) := (BitVec.ule x y).not
+abbrev BitVec_sgt { n : Nat } (x y : BitVec n) := (BitVec.sle x y).not
+abbrev BitVec_zeroExtend {n : Nat} (extra : Nat) (x : BitVec n) : BitVec (n + extra) := BitVec.zeroExtend (n + extra) x
+abbrev BitVec_signExtend {n : Nat} (extra : Nat) (x : BitVec n) : BitVec (n + extra) := BitVec.signExtend (n + extra) x
+abbrev SmtMap (t0 t1 : Type) [Inhabited t0] [BEq t0] [Inhabited t1] : Type := t0 -> t1
+abbrev SmtMap_default { t0 t1: Type } (v : t1) [Inhabited t0] [BEq t0] [Inhabited t1] : SmtMap t0 t1 := fun _ => v
+abbrev SmtMap_store { t0 t1 : Type } [Inhabited t0] [BEq t0] [Inhabited t1] (m : SmtMap t0 t1) (k : t0) (v : t1) : SmtMap t0 t1 :=
+  fun x => if x == k then v else m x
+abbrev SmtMap_select { t0 t1 : Type } [Inhabited t0] [BEq t0] [Inhabited t1] (m : SmtMap t0 t1) (k : t0) := m k

lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean

@@ -0,0 +1,21 @@
+import LeanProofs.Flux.Prelude
+import LeanProofs.Flux.Fun.TcbDefsAligned
+import LeanProofs.Flux.Fun.TcbDefsPow2
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+
+
+def TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0 := 
+ ∀ (x₀ : Int),
+  ∀ (y₀ : Int),
+   ((y₀ ≥ 32) ∧ (tcb_defs_pow2 y₀) ∧ (tcb_defs_aligned x₀ y₀)) ->
+    (x₀ ≥ 0) ->
+     (x₀ ≤ 4294967295) ->
+      (y₀ ≥ 0) ->
+       (y₀ ≤ 4294967295) ->
+        ((BitVec.and (BitVec.ofInt 32 x₀) 31#32) = 0#32)
+end F

lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremDiv2Pow2.lean

@@ -0,0 +1,17 @@
+import LeanProofs.Flux.Prelude
+import LeanProofs.Flux.Fun.TcbDefsPow2
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+
+
+def TcbTheoremsTheoremDiv2Pow2 := 
+ ∀ (n₀ : Int),
+  ((tcb_defs_pow2 n₀) ∧ (n₀ ≥ 2)) ->
+   (n₀ ≥ 0) ->
+    (n₀ ≤ 4294967295) ->
+     (((n₀ / 2) * 2) = n₀)
+end F

lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Div2Pow2.lean

@@ -0,0 +1,17 @@
+import LeanProofs.Flux.Prelude
+import LeanProofs.Flux.Fun.TcbDefsPow2
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+
+
+def TcbTheoremsTheoremPow2Div2Pow2 := 
+ ∀ (n₀ : Int),
+  ((tcb_defs_pow2 n₀) ∧ (n₀ ≥ 4)) ->
+   (n₀ ≥ 0) ->
+    (n₀ ≤ 4294967295) ->
+     (tcb_defs_pow2 (n₀ / 2))
+end F

lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2LeAligned.lean

@@ -0,0 +1,24 @@
+import LeanProofs.Flux.Prelude
+import LeanProofs.Flux.Fun.TcbDefsAligned
+import LeanProofs.Flux.Fun.TcbDefsPow2
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+
+
+def TcbTheoremsTheoremPow2LeAligned := 
+ ∀ (x₀ : Int),
+  ∀ (y₀ : Int),
+   ∀ (z₀ : Int),
+    ((tcb_defs_aligned x₀ y₀) ∧ (z₀ ≤ y₀) ∧ (tcb_defs_pow2 y₀) ∧ (tcb_defs_pow2 z₀)) ->
+     (x₀ ≥ 0) ->
+      (x₀ ≤ 4294967295) ->
+       (y₀ ≥ 0) ->
+        (y₀ ≤ 4294967295) ->
+         (z₀ ≥ 0) ->
+          (z₀ ≤ 4294967295) ->
+           (tcb_defs_aligned x₀ z₀)
+end F

lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Octet.lean

@@ -0,0 +1,18 @@
+import LeanProofs.Flux.Prelude
+import LeanProofs.Flux.Fun.TcbDefsOctet
+import LeanProofs.Flux.Fun.TcbDefsPow2
+open Classical
+set_option linter.unusedVariables false
+
+
+namespace F
+
+
+
+def TcbTheoremsTheoremPow2Octet := 
+ ∀ (r₀ : Int),
+  ((tcb_defs_pow2 r₀) ∧ (r₀ ≥ 8)) ->
+   (r₀ ≥ 0) ->
+    (r₀ ≤ 4294967295) ->
+     (tcb_defs_octet r₀)
+end F