diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs index 339a49522b..87a2a24fe6 100644 --- a/arch/cortex-m/src/mpu.rs +++ b/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 ( diff --git a/arch/cortex-m/src/tcb/theorems.rs b/arch/cortex-m/src/tcb/theorems.rs index 0a12808c8a..33d28ca41c 100644 --- a/arch/cortex-m/src/tcb/theorems.rs +++ b/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) {} @@ -39,11 +39,12 @@ pub fn theorem_div2_pow2(_n: usize) {} #[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) {} diff --git a/flux_support/src/flux_ptr.rs b/flux_support/src/flux_ptr.rs index ec2af946ee..a1fce9d68c 100644 --- a/flux_support/src/flux_ptr.rs +++ b/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 diff --git a/kernel/src/allocator.rs b/kernel/src/allocator.rs index e29c280e23..e15c76a701 100644 --- a/kernel/src/allocator.rs +++ b/kernel/src/allocator.rs @@ -411,7 +411,8 @@ impl AppMemoryAllocator { 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 AppMemoryAllocator { 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, @@ -578,10 +583,24 @@ impl AppMemoryAllocator { 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, diff --git a/kernel/src/platform/mpu.rs b/kernel/src/platform/mpu.rs index e973fc9d7d..cd9b8501a7 100644 --- a/kernel/src/platform/mpu.rs +++ b/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( diff --git a/lean_proofs/.github/workflows/lean_action_ci.yml b/lean_proofs/.github/workflows/lean_action_ci.yml new file mode 100644 index 0000000000..09cd4ca6df --- /dev/null +++ b/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 diff --git a/lean_proofs/.gitignore b/lean_proofs/.gitignore new file mode 100644 index 0000000000..bfb30ec8c7 --- /dev/null +++ b/lean_proofs/.gitignore @@ -0,0 +1 @@ +/.lake diff --git a/lean_proofs/LeanProofs.lean b/lean_proofs/LeanProofs.lean new file mode 100644 index 0000000000..a5b5ef0d61 --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Basic.lean b/lean_proofs/LeanProofs/Basic.lean new file mode 100644 index 0000000000..669ff15704 --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean b/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean new file mode 100644 index 0000000000..6ebaac8dd0 --- /dev/null +++ b/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) diff --git a/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremDiv2Pow2.lean b/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremDiv2Pow2.lean new file mode 100644 index 0000000000..d1bb9b8101 --- /dev/null +++ b/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) diff --git a/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Div2Pow2.lean b/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Div2Pow2.lean new file mode 100644 index 0000000000..d291c8304f --- /dev/null +++ b/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) diff --git a/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2LeAligned.lean b/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2LeAligned.lean new file mode 100644 index 0000000000..e604af799b --- /dev/null +++ b/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) diff --git a/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Octet.lean b/lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Octet.lean new file mode 100644 index 0000000000..45eca2c586 --- /dev/null +++ b/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) diff --git a/lean_proofs/LeanProofs/Flux/Fun/TcbDefsAligned.lean b/lean_proofs/LeanProofs/Flux/Fun/TcbDefsAligned.lean new file mode 100644 index 0000000000..879a3d8212 --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/Fun/TcbDefsOctet.lean b/lean_proofs/LeanProofs/Flux/Fun/TcbDefsOctet.lean new file mode 100644 index 0000000000..8ddf5f69b3 --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/Fun/TcbDefsPow2.lean b/lean_proofs/LeanProofs/Flux/Fun/TcbDefsPow2.lean new file mode 100644 index 0000000000..07428f0d1d --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/Prelude.lean b/lean_proofs/LeanProofs/Flux/Prelude.lean new file mode 100644 index 0000000000..f8ca64f09e --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean b/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean new file mode 100644 index 0000000000..72de7d392b --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremDiv2Pow2.lean b/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremDiv2Pow2.lean new file mode 100644 index 0000000000..15700269af --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Div2Pow2.lean b/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Div2Pow2.lean new file mode 100644 index 0000000000..8775f86c54 --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2LeAligned.lean b/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2LeAligned.lean new file mode 100644 index 0000000000..30ec39e23c --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Octet.lean b/lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Octet.lean new file mode 100644 index 0000000000..95f9a7dbcf --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/SharedLemmas.lean b/lean_proofs/LeanProofs/SharedLemmas.lean new file mode 100644 index 0000000000..d519ca37b9 --- /dev/null +++ b/lean_proofs/LeanProofs/SharedLemmas.lean @@ -0,0 +1,141 @@ +import LeanProofs.Flux.Fun.TcbDefsPow2 +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) + +theorem tcb_defs_pow2_eq_pow2 (x: Nat) : (x < 2 ^ 32) -> (F.tcb_defs_pow2 x <-> pow2 x) := by + unfold F.tcb_defs_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 tcb_defs_pow2_0_is_power_of_2 (x: Nat) : (x < 2 ^ 32) -> (F.tcb_defs_pow2 x <-> x.isPowerOfTwo) := by + intro x_in_bounds + apply Iff.intro + case _ => + intro x_pow2 + rw [← pow2_isPowerOfTwo x] + apply (tcb_defs_pow2_eq_pow2 x x_in_bounds).mp + exact x_pow2 + case _ => + intro x_pow2 + apply (tcb_defs_pow2_eq_pow2 x x_in_bounds).mpr + rw [pow2_isPowerOfTwo] + exact x_pow2 diff --git a/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean new file mode 100644 index 0000000000..27ef5a263f --- /dev/null +++ b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean @@ -0,0 +1,38 @@ +import LeanProofs.Flux.Prelude +import LeanProofs.Flux.VC.TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0 +import LeanProofs.SharedLemmas +import Init.Data.BitVec.Lemmas +open Classical +set_option linter.unusedVariables false + +namespace F + +def TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0_proof : TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0 := by + unfold TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0 + intro x₀ y₀ ⟨y_ge32, y_pow2, x_aligned_y⟩ x_ge0 x_in_bounds y_ge0 y_in_bounds + unfold tcb_defs_aligned 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 := (tcb_defs_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] + +end F diff --git a/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremDiv2Pow2Proof.lean b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremDiv2Pow2Proof.lean new file mode 100644 index 0000000000..f0c9be3d33 --- /dev/null +++ b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremDiv2Pow2Proof.lean @@ -0,0 +1,23 @@ +import LeanProofs.Flux.Prelude +import LeanProofs.Flux.VC.TcbTheoremsTheoremDiv2Pow2 +import LeanProofs.SharedLemmas +open Classical +set_option linter.unusedVariables false + +namespace F + +def TcbTheoremsTheoremDiv2Pow2_proof : TcbTheoremsTheoremDiv2Pow2 := by + unfold TcbTheoremsTheoremDiv2Pow2 + intro n ⟨n_pow2, n_ge2⟩ n_ge0 n_in_bounds + have nnat_in_bounds : n.toNat < 2 ^ 32 := by omega + rw [← Int.toNat_of_nonneg n_ge0] at n_pow2 + have nnat_pow2 := (tcb_defs_pow2_0_is_power_of_2 n.toNat nnat_in_bounds).mp n_pow2 + rcases nnat_pow2 with ⟨k, hy⟩ + cases k with + | zero => omega + | succ k' => + have hdvd : 2 ∣ n.toNat := ⟨2 ^ k', by omega⟩ + have hnat := Nat.div_mul_cancel hdvd + omega + +end F diff --git a/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2Div2Pow2Proof.lean b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2Div2Pow2Proof.lean new file mode 100644 index 0000000000..11104e8b92 --- /dev/null +++ b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2Div2Pow2Proof.lean @@ -0,0 +1,53 @@ +import LeanProofs.Flux.Prelude +import LeanProofs.Flux.VC.TcbTheoremsTheoremPow2Div2Pow2 +import LeanProofs.SharedLemmas +open Classical +set_option linter.unusedVariables false + +private theorem pow_right_inj (ha : 1 < a) : a ^ m = a ^ n ↔ m = n := by + simp [Nat.le_antisymm_iff, Nat.pow_le_pow_iff_right ha] + +private theorem four_is_pow2 : pow2 4 := by simp + +private theorem pow2_div2_pow2 (x : Nat) : pow2 x → x ≥ 4 → pow2 (x / 2) := by + intros h1 h2 + rcases (pow2_isPowerOfTwo x).mp h1 with ⟨n, hy⟩ + rcases (pow2_isPowerOfTwo 4).mp four_is_pow2 with ⟨m, hz⟩ + apply (pow2_isPowerOfTwo (x / 2)).mpr + simp_all + simp [Nat.isPowerOfTwo] + exists (n - 1) + have hn : n ≥ 1 := by + simp_all [Nat.pow_le_pow_iff_right] + have h_eq : 2 ^ 2 = 2 ^ m := by rw [← hz] + have hm : m = 2 := by + rw [pow_right_inj] at h_eq; simp_all; omega + simp_all; omega + rw [Nat.div_eq_iff_eq_mul_left] + rw [← Nat.pow_pred_mul] <;> omega + omega + have h3 : (2 ∣ 2 ^ n) = (2 ^ 1 ∣ 2 ^ n) := by simp + simp [h3] + apply Nat.pow_dvd_pow <;> omega + +namespace F + +def TcbTheoremsTheoremPow2Div2Pow2_proof : TcbTheoremsTheoremPow2Div2Pow2 := by + unfold TcbTheoremsTheoremPow2Div2Pow2 + intro n ⟨n_pow2, n_ge4⟩ n_ge0 n_in_bounds + have nnat_in_bounds : n.toNat < 2 ^ 32 := by omega + have ntwo_in_bounds : n.toNat / 2 < 2 ^ 32 := by omega + rw [← Int.toNat_of_nonneg n_ge0] at n_pow2 + have nnat_pow2 : pow2 n.toNat := + (tcb_defs_pow2_eq_pow2 n.toNat nnat_in_bounds).mp n_pow2 + have half_pow2 : pow2 (n.toNat / 2) := + pow2_div2_pow2 n.toNat nnat_pow2 (by omega) + have half_i_pow2 : F.tcb_defs_pow2 (↑(n.toNat / 2)) := + (tcb_defs_pow2_eq_pow2 (n.toNat / 2) ntwo_in_bounds).mpr half_pow2 + have key : n / 2 = ↑(n.toNat / 2) := by + have := Int.toNat_of_nonneg n_ge0 + omega + rw [key] + exact half_i_pow2 + +end F diff --git a/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2LeAlignedProof.lean b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2LeAlignedProof.lean new file mode 100644 index 0000000000..7dfe50cf24 --- /dev/null +++ b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2LeAlignedProof.lean @@ -0,0 +1,46 @@ +import LeanProofs.Flux.Prelude +import LeanProofs.Flux.VC.TcbTheoremsTheoremPow2LeAligned +import LeanProofs.SharedLemmas +open Classical +set_option linter.unusedVariables false + +private theorem mod_pow2_le {x n m : Nat} : m ≤ n → x % 2 ^ n = 0 → x % 2 ^ m = 0 := by + intros h1 h2 + simp_all [Nat.mod_eq_iff] + rcases h2 with ⟨a, ⟨k, _⟩⟩ + case _ => + apply And.intro + · apply Nat.pow_pos; simp + · exists (2 ^ (n - m) * k) + conv => right; rw [← Nat.mul_assoc]; left; rw [Nat.mul_comm, Nat.pow_sub_mul_pow 2 h1] + assumption + +private theorem pow2_le_aligned (x y z : Nat) : + x % y = 0 → z ≤ y → pow2 y → pow2 z → x % z = 0 := by + intros h1 h2 h3 h4 + rcases (pow2_isPowerOfTwo y).mp h3 with ⟨n, hy⟩ + rcases (pow2_isPowerOfTwo z).mp h4 with ⟨m, hz⟩ + simp_all + have h := (Nat.pow_le_pow_iff_right (a := 2) (by simp)).mp h2 + apply mod_pow2_le h + assumption + +namespace F + +def TcbTheoremsTheoremPow2LeAligned_proof : TcbTheoremsTheoremPow2LeAligned := by + unfold TcbTheoremsTheoremPow2LeAligned + intro x₀ y₀ z₀ ⟨x_aligned_y, z_le_y, y_pow2, z_pow2⟩ x_ge0 x_in_bounds y_ge0 y_in_bounds z_ge0 z_in_bounds + unfold tcb_defs_aligned at * + have nat_res : x₀.toNat % z₀.toNat = 0 := by + apply pow2_le_aligned x₀.toNat y₀.toNat z₀.toNat + · rw [← Int.toNat_of_nonneg x_ge0, ← Int.toNat_of_nonneg y_ge0] at x_aligned_y + omega + · omega + · apply (tcb_defs_pow2_eq_pow2 y₀.toNat (by omega)).mp + rw [Int.toNat_of_nonneg y_ge0]; exact y_pow2 + · apply (tcb_defs_pow2_eq_pow2 z₀.toNat (by omega)).mp + rw [Int.toNat_of_nonneg z_ge0]; exact z_pow2 + rw [← Int.toNat_of_nonneg x_ge0, ← Int.toNat_of_nonneg z_ge0] + omega + +end F diff --git a/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2OctetProof.lean b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2OctetProof.lean new file mode 100644 index 0000000000..e52541bc44 --- /dev/null +++ b/lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2OctetProof.lean @@ -0,0 +1,34 @@ +import LeanProofs.Flux.Prelude +import LeanProofs.Flux.VC.TcbTheoremsTheoremPow2Octet +import LeanProofs.SharedLemmas +open Classical +set_option linter.unusedVariables false + +private theorem power_of_2_ge_8_octet (x : Nat) : x.isPowerOfTwo → x ≥ 8 → x % 8 = 0 := by + intro x_pow2 x_ge8 + apply Nat.mod_eq_zero_of_dvd + unfold Nat.isPowerOfTwo at x_pow2 + cases x_pow2 with + | intro k hk => + have h : (8 = 2 ^ 3) := by simp + rw [hk, h, Nat.pow_dvd_pow_iff_le_right] + case _ => + rw [hk, h] at x_ge8 + rw [← (@Nat.pow_le_pow_iff_right 2 3 k)] + exact x_ge8 + simp + case _ => simp + +namespace F + +def TcbTheoremsTheoremPow2Octet_proof : TcbTheoremsTheoremPow2Octet := by + unfold TcbTheoremsTheoremPow2Octet + intro r₀ ⟨r₀_pow2, r₀_ge8⟩ r₀_ge0 r₀_in_bounds + unfold tcb_defs_octet + have nnat_in_bounds : r₀.toNat < 2 ^ 32 := by omega + rw [← Int.toNat_of_nonneg r₀_ge0] at r₀_pow2 + have nat_pow2 := (tcb_defs_pow2_0_is_power_of_2 r₀.toNat nnat_in_bounds).mp r₀_pow2 + have nat_res : r₀.toNat % 8 = 0 := power_of_2_ge_8_octet r₀.toNat nat_pow2 (by omega) + omega + +end F diff --git a/lean_proofs/README.md b/lean_proofs/README.md new file mode 100644 index 0000000000..b8429d6ecb --- /dev/null +++ b/lean_proofs/README.md @@ -0,0 +1 @@ +# lean_proofs \ No newline at end of file diff --git a/lean_proofs/lake-manifest.json b/lean_proofs/lake-manifest.json new file mode 100644 index 0000000000..49f8bbbb47 --- /dev/null +++ b/lean_proofs/lake-manifest.json @@ -0,0 +1,5 @@ +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "lean_proofs", + "lakeDir": ".lake"} diff --git a/lean_proofs/lakefile.toml b/lean_proofs/lakefile.toml new file mode 100644 index 0000000000..4fe9f7cc84 --- /dev/null +++ b/lean_proofs/lakefile.toml @@ -0,0 +1,6 @@ +name = "lean_proofs" +version = "0.1.0" +defaultTargets = ["LeanProofs"] + +[[lean_lib]] +name = "LeanProofs" diff --git a/lean_proofs/lean-toolchain b/lean_proofs/lean-toolchain new file mode 100644 index 0000000000..7f254a98f3 --- /dev/null +++ b/lean_proofs/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.23.0