From 2fc53e340fcd75ab7a112211817ac94259d52c67 Mon Sep 17 00:00:00 2001 From: Petros Markopoulos Date: Mon, 6 Oct 2025 09:31:11 -0700 Subject: [PATCH 1/3] Mark theorems as proven externally and prove them --- arch/cortex-m/src/tcb/theorems.rs | 10 +- .../.github/workflows/lean_action_ci.yml | 14 ++ lean_proofs/.gitignore | 1 + lean_proofs/LeanProofs.lean | 3 + lean_proofs/LeanProofs/Basic.lean | 1 + lean_proofs/LeanProofs/SharedLemmas.lean | 143 ++++++++++++++++++ ...heoremAlignedValueGe32LowestFiveBits0.lean | 11 ++ ...mAlignedValueGe32LowestFiveBits0Proof.lean | 37 +++++ .../TcbTheoremsTheoremDiv2Pow2.lean | 8 + .../TcbTheoremsTheoremDiv2Pow2Proof.lean | 20 +++ .../TcbTheoremsTheoremPow2Div2Pow2.lean | 8 + .../TcbTheoremsTheoremPow2Div2Pow2Proof.lean | 51 +++++++ .../TcbTheoremsTheoremPow2LeAligned.lean | 11 ++ .../TcbTheoremsTheoremPow2LeAlignedProof.lean | 57 +++++++ .../TcbTheoremsTheoremPow2Octet.lean | 11 ++ .../TcbTheoremsTheoremPow2OctetProof.lean | 41 +++++ lean_proofs/README.md | 1 + lean_proofs/lake-manifest.json | 5 + lean_proofs/lakefile.toml | 6 + lean_proofs/lean-toolchain | 1 + 20 files changed, 435 insertions(+), 5 deletions(-) create mode 100644 lean_proofs/.github/workflows/lean_action_ci.yml create mode 100644 lean_proofs/.gitignore create mode 100644 lean_proofs/LeanProofs.lean create mode 100644 lean_proofs/LeanProofs/Basic.lean create mode 100644 lean_proofs/LeanProofs/SharedLemmas.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean create mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean create mode 100644 lean_proofs/README.md create mode 100644 lean_proofs/lake-manifest.json create mode 100644 lean_proofs/lakefile.toml create mode 100644 lean_proofs/lean-toolchain diff --git a/arch/cortex-m/src/tcb/theorems.rs b/arch/cortex-m/src/tcb/theorems.rs index 0a12808c8a..1363e29c00 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) {} @@ -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) {} 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..99415d9d9f --- /dev/null +++ b/lean_proofs/LeanProofs/Basic.lean @@ -0,0 +1 @@ +def hello := "world" diff --git a/lean_proofs/LeanProofs/SharedLemmas.lean b/lean_proofs/LeanProofs/SharedLemmas.lean new file mode 100644 index 0000000000..35cff7b46b --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean new file mode 100644 index 0000000000..7f1becc6b4 --- /dev/null +++ b/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 ≤ 18446744073709551615) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 18446744073709551615) -> ((BitVec.and (BitVec.ofInt 32 reftgen_x_0) 31#32) = 0#32))))))))))))) + diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean new file mode 100644 index 0000000000..27d9ebd61d --- /dev/null +++ b/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] diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean new file mode 100644 index 0000000000..cb8fa06dfb --- /dev/null +++ b/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 ≤ 18446744073709551615) -> (((reftgen_n_0 / 2) * 2) = reftgen_n_0)))))))) + diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean new file mode 100644 index 0000000000..6d0005462c --- /dev/null +++ b/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 diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean new file mode 100644 index 0000000000..180232e139 --- /dev/null +++ b/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 ≤ 18446744073709551615) -> (f_pow2_0 (reftgen_n_0 / 2))))))))) + diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean new file mode 100644 index 0000000000..a8b613e66e --- /dev/null +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean @@ -0,0 +1,51 @@ +import LeanProofs.TcbTheoremsTheoremPow2Div2Pow2 +import LeanProofs.SharedLemmas + +theorem f_pow2_eq_i_pow2 : f_pow2_0 = i_pow2 := by + funext x; unfold f_pow2_0 i_pow2; simp + +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] + +theorem four_is_pow2 : pow2 4 := by simp + +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 + + +def tcb_theorems_theorem_pow2_div2_pow2_proof : tcb_theorems_theorem_pow2_div2_pow2 := by + unfold tcb_theorems_theorem_pow2_div2_pow2 + intro n _ h _ n_ge0 _ n_in_bounds + obtain ⟨n_pow2, n_ge4⟩ := h + rw [f_pow2_eq_i_pow2] at * + have ntwo_in_bounds: (n.toNat / 2) < 2 ^ 32 := by omega + have nnat_in_bounds: n.toNat < 2 ^ 32 := by omega + have res_n: f_pow2_0 (n.toNat / 2) = true := by + apply (i_pow2_eq_pow2 (n.toNat / 2) ntwo_in_bounds).mpr + apply pow2_div2_pow2 + apply (i_pow2_eq_pow2 n.toNat nnat_in_bounds).mp + rw [Int.toNat_of_nonneg] + assumption + assumption + omega + rw [Int.toNat_of_nonneg] at res_n + assumption + assumption diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean new file mode 100644 index 0000000000..4ee2f35a73 --- /dev/null +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean @@ -0,0 +1,11 @@ +-- GENERATED; DO NOT EDIT -- +-- FUNCTIONS -- +def f_aligned_0 (a0 : Int) (a1 : Int) : Bool := + ((a0 % a1) = 0) + +def f_pow2_1 (a2 : Int) : Bool := + (let a3 := (BitVec.ofInt 32 a2); ((a2 > 0) && ((BitVec.and a3 (BitVec.sub a3 1#32)) = 0#32))) + +-- THEOREM -- +def tcb_theorems_theorem_pow2_le_aligned : Prop := (∀ (reftgen_x_0 : Int), (∀ (reftgen_y_1 : Int), (∀ (reftgen_z_2 : Int), (∀ (__ : Int), (((f_aligned_0 reftgen_x_0 reftgen_y_1) ∧ (reftgen_z_2 ≤ reftgen_y_1) ∧ (f_pow2_1 reftgen_y_1) ∧ (f_pow2_1 reftgen_z_2)) -> (∀ (__ : Int), ((reftgen_x_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_x_0 ≤ 18446744073709551615) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 18446744073709551615) -> (∀ (__ : Int), ((reftgen_z_2 ≥ 0) -> (∀ (__ : Int), ((reftgen_z_2 ≤ 18446744073709551615) -> (f_aligned_0 reftgen_x_0 reftgen_z_2)))))))))))))))))) + diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean new file mode 100644 index 0000000000..8b0318c2c1 --- /dev/null +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean @@ -0,0 +1,57 @@ +import LeanProofs.TcbTheoremsTheoremPow2LeAligned +import LeanProofs.SharedLemmas + +theorem f_pow2_1_eq_i_pow2 : f_pow2_1 = i_pow2 := by + funext x; unfold f_pow2_1 i_pow2; simp + +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 + +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 + +def tcb_theorems_theorem_pow2_le_aligned_proof : tcb_theorems_theorem_pow2_le_aligned := by + unfold tcb_theorems_theorem_pow2_le_aligned + intros x y z _ h _ x_ge0 _ x_in_bounds _ y_ge0 _ y_in_bounds _ z_ge0 _ z_in_bounds + obtain ⟨x_aligned_y, ⟨z_le_y, ⟨y_pow2, z_pow2⟩⟩⟩ := h + rw [f_pow2_1_eq_i_pow2] at * + unfold f_aligned_0 at * + simp at x_aligned_y + simp + 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 (i_pow2_eq_pow2 y.toNat _).mp + rw [Int.toNat_of_nonneg] + assumption + assumption + omega + · apply (i_pow2_eq_pow2 z.toNat _).mp + rw [Int.toNat_of_nonneg] + assumption + assumption + omega + rw [←Int.toNat_of_nonneg x_ge0, ←Int.toNat_of_nonneg z_ge0] + omega diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean new file mode 100644 index 0000000000..3bdfc63e7b --- /dev/null +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean @@ -0,0 +1,11 @@ +-- GENERATED; DO NOT EDIT -- +-- FUNCTIONS -- +def f_octet_1 (a2 : Int) : Bool := + ((a2 % 8) = 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_pow2_octet : Prop := (∀ (reftgen_r_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_r_0) ∧ (reftgen_r_0 ≥ 8)) -> (∀ (__ : Int), ((reftgen_r_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_r_0 ≤ 18446744073709551615) -> (f_octet_1 reftgen_r_0)))))))) + diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean new file mode 100644 index 0000000000..8fd6d21ff1 --- /dev/null +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean @@ -0,0 +1,41 @@ +import LeanProofs.TcbTheoremsTheoremPow2Octet +import LeanProofs.SharedLemmas + +theorem f_pow2_1_eq_i_pow2 : f_pow2_0 = i_pow2 := by + funext x; unfold f_pow2_0 i_pow2; simp + +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 + +def tcb_theorems_theorem_pow2_octet_proof : tcb_theorems_theorem_pow2_octet := by + unfold tcb_theorems_theorem_pow2_octet + intro r0 _ h1 _ r0_ge0 _ r0_in_bounds + obtain ⟨r0_pow2, r0_ge8⟩ := h1 + rw [f_pow2_1_eq_i_pow2] at * + unfold f_octet_1 + simp + have nat_res : r0.toNat % 8 = 0 := by + apply power_of_2_ge_8_octet + case _ => + apply (i_pow2_0_is_power_of_2 r0.toNat _).mp + case _ => + rw [Int.toNat_of_nonneg] + assumption + assumption + case _ => + omega + case _ => + omega + omega 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 From 3c0c9727ce97b0c322362a27d9839ad579203892 Mon Sep 17 00:00:00 2001 From: Petros Markopoulos Date: Mon, 6 Oct 2025 09:32:26 -0700 Subject: [PATCH 2/3] Fix pointer-width related type errors --- arch/cortex-m/src/mpu.rs | 5 ++-- flux_support/src/flux_ptr.rs | 2 +- kernel/src/allocator.rs | 23 +++++++++++++++++-- kernel/src/platform/mpu.rs | 6 +++-- ...heoremAlignedValueGe32LowestFiveBits0.lean | 2 +- .../TcbTheoremsTheoremDiv2Pow2.lean | 2 +- .../TcbTheoremsTheoremPow2Div2Pow2.lean | 2 +- .../TcbTheoremsTheoremPow2LeAligned.lean | 2 +- .../TcbTheoremsTheoremPow2Octet.lean | 2 +- 9 files changed, 34 insertions(+), 12 deletions(-) diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs index 339a49522b..90000b199b 100644 --- a/arch/cortex-m/src/mpu.rs +++ b/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; } 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/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean index 7f1becc6b4..214f9521ca 100644 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean @@ -7,5 +7,5 @@ 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 ≤ 18446744073709551615) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 18446744073709551615) -> ((BitVec.and (BitVec.ofInt 32 reftgen_x_0) 31#32) = 0#32))))))))))))) +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))))))))))))) diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean index cb8fa06dfb..09d4386ce8 100644 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean @@ -4,5 +4,5 @@ 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 ≤ 18446744073709551615) -> (((reftgen_n_0 / 2) * 2) = reftgen_n_0)))))))) +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)))))))) diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean index 180232e139..d1421ac0a0 100644 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean @@ -4,5 +4,5 @@ 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 ≤ 18446744073709551615) -> (f_pow2_0 (reftgen_n_0 / 2))))))))) +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))))))))) diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean index 4ee2f35a73..c333f67c41 100644 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean @@ -7,5 +7,5 @@ def f_pow2_1 (a2 : Int) : Bool := (let a3 := (BitVec.ofInt 32 a2); ((a2 > 0) && ((BitVec.and a3 (BitVec.sub a3 1#32)) = 0#32))) -- THEOREM -- -def tcb_theorems_theorem_pow2_le_aligned : Prop := (∀ (reftgen_x_0 : Int), (∀ (reftgen_y_1 : Int), (∀ (reftgen_z_2 : Int), (∀ (__ : Int), (((f_aligned_0 reftgen_x_0 reftgen_y_1) ∧ (reftgen_z_2 ≤ reftgen_y_1) ∧ (f_pow2_1 reftgen_y_1) ∧ (f_pow2_1 reftgen_z_2)) -> (∀ (__ : Int), ((reftgen_x_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_x_0 ≤ 18446744073709551615) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 18446744073709551615) -> (∀ (__ : Int), ((reftgen_z_2 ≥ 0) -> (∀ (__ : Int), ((reftgen_z_2 ≤ 18446744073709551615) -> (f_aligned_0 reftgen_x_0 reftgen_z_2)))))))))))))))))) +def tcb_theorems_theorem_pow2_le_aligned : Prop := (∀ (reftgen_x_0 : Int), (∀ (reftgen_y_1 : Int), (∀ (reftgen_z_2 : Int), (∀ (__ : Int), (((f_aligned_0 reftgen_x_0 reftgen_y_1) ∧ (reftgen_z_2 ≤ reftgen_y_1) ∧ (f_pow2_1 reftgen_y_1) ∧ (f_pow2_1 reftgen_z_2)) -> (∀ (__ : Int), ((reftgen_x_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_x_0 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_z_2 ≥ 0) -> (∀ (__ : Int), ((reftgen_z_2 ≤ 4294967295) -> (f_aligned_0 reftgen_x_0 reftgen_z_2)))))))))))))))))) diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean index 3bdfc63e7b..8546d24636 100644 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean +++ b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean @@ -7,5 +7,5 @@ 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_octet : Prop := (∀ (reftgen_r_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_r_0) ∧ (reftgen_r_0 ≥ 8)) -> (∀ (__ : Int), ((reftgen_r_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_r_0 ≤ 18446744073709551615) -> (f_octet_1 reftgen_r_0)))))))) +def tcb_theorems_theorem_pow2_octet : Prop := (∀ (reftgen_r_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_r_0) ∧ (reftgen_r_0 ≥ 8)) -> (∀ (__ : Int), ((reftgen_r_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_r_0 ≤ 4294967295) -> (f_octet_1 reftgen_r_0)))))))) From 1809fb9943600fc20f7af0c0a5ef4093e606e3b3 Mon Sep 17 00:00:00 2001 From: Petros Markopoulos Date: Mon, 15 Jun 2026 16:31:34 -0700 Subject: [PATCH 3/3] update proofs to work with current version of flux-lean --- arch/cortex-m/src/mpu.rs | 3 + arch/cortex-m/src/tcb/theorems.rs | 1 + lean_proofs/LeanProofs/Basic.lean | 7 ++- ...heoremAlignedValueGe32LowestFiveBits0.lean | 4 ++ .../Checking/TcbTheoremsTheoremDiv2Pow2.lean | 4 ++ .../TcbTheoremsTheoremPow2Div2Pow2.lean | 4 ++ .../TcbTheoremsTheoremPow2LeAligned.lean | 4 ++ .../Checking/TcbTheoremsTheoremPow2Octet.lean | 4 ++ .../LeanProofs/Flux/Fun/TcbDefsAligned.lean | 12 ++++ .../LeanProofs/Flux/Fun/TcbDefsOctet.lean | 12 ++++ .../LeanProofs/Flux/Fun/TcbDefsPow2.lean | 12 ++++ lean_proofs/LeanProofs/Flux/Prelude.lean | 15 +++++ ...heoremAlignedValueGe32LowestFiveBits0.lean | 21 +++++++ .../Flux/VC/TcbTheoremsTheoremDiv2Pow2.lean | 17 ++++++ .../VC/TcbTheoremsTheoremPow2Div2Pow2.lean | 17 ++++++ .../VC/TcbTheoremsTheoremPow2LeAligned.lean | 24 ++++++++ .../Flux/VC/TcbTheoremsTheoremPow2Octet.lean | 18 ++++++ lean_proofs/LeanProofs/SharedLemmas.lean | 14 ++--- ...heoremAlignedValueGe32LowestFiveBits0.lean | 11 ---- ...mAlignedValueGe32LowestFiveBits0Proof.lean | 37 ------------ .../TcbTheoremsTheoremDiv2Pow2.lean | 8 --- .../TcbTheoremsTheoremDiv2Pow2Proof.lean | 20 ------- .../TcbTheoremsTheoremPow2Div2Pow2.lean | 8 --- .../TcbTheoremsTheoremPow2Div2Pow2Proof.lean | 51 ----------------- .../TcbTheoremsTheoremPow2LeAligned.lean | 11 ---- .../TcbTheoremsTheoremPow2LeAlignedProof.lean | 57 ------------------- .../TcbTheoremsTheoremPow2Octet.lean | 11 ---- .../TcbTheoremsTheoremPow2OctetProof.lean | 41 ------------- ...mAlignedValueGe32LowestFiveBits0Proof.lean | 38 +++++++++++++ .../TcbTheoremsTheoremDiv2Pow2Proof.lean | 23 ++++++++ .../TcbTheoremsTheoremPow2Div2Pow2Proof.lean | 53 +++++++++++++++++ .../TcbTheoremsTheoremPow2LeAlignedProof.lean | 46 +++++++++++++++ .../TcbTheoremsTheoremPow2OctetProof.lean | 34 +++++++++++ 33 files changed, 378 insertions(+), 264 deletions(-) create mode 100644 lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean create mode 100644 lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremDiv2Pow2.lean create mode 100644 lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Div2Pow2.lean create mode 100644 lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2LeAligned.lean create mode 100644 lean_proofs/LeanProofs/Flux/Checking/TcbTheoremsTheoremPow2Octet.lean create mode 100644 lean_proofs/LeanProofs/Flux/Fun/TcbDefsAligned.lean create mode 100644 lean_proofs/LeanProofs/Flux/Fun/TcbDefsOctet.lean create mode 100644 lean_proofs/LeanProofs/Flux/Fun/TcbDefsPow2.lean create mode 100644 lean_proofs/LeanProofs/Flux/Prelude.lean create mode 100644 lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean create mode 100644 lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremDiv2Pow2.lean create mode 100644 lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Div2Pow2.lean create mode 100644 lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2LeAligned.lean create mode 100644 lean_proofs/LeanProofs/Flux/VC/TcbTheoremsTheoremPow2Octet.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean delete mode 100644 lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean create mode 100644 lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean create mode 100644 lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremDiv2Pow2Proof.lean create mode 100644 lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2Div2Pow2Proof.lean create mode 100644 lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2LeAlignedProof.lean create mode 100644 lean_proofs/LeanProofs/User/Proof/TcbTheoremsTheoremPow2OctetProof.lean diff --git a/arch/cortex-m/src/mpu.rs b/arch/cortex-m/src/mpu.rs index 90000b199b..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, @@ -574,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, @@ -683,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 1363e29c00..33d28ca41c 100644 --- a/arch/cortex-m/src/tcb/theorems.rs +++ b/arch/cortex-m/src/tcb/theorems.rs @@ -39,6 +39,7 @@ 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) {} diff --git a/lean_proofs/LeanProofs/Basic.lean b/lean_proofs/LeanProofs/Basic.lean index 99415d9d9f..669ff15704 100644 --- a/lean_proofs/LeanProofs/Basic.lean +++ b/lean_proofs/LeanProofs/Basic.lean @@ -1 +1,6 @@ -def hello := "world" +-- 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 index 35cff7b46b..d519ca37b9 100644 --- a/lean_proofs/LeanProofs/SharedLemmas.lean +++ b/lean_proofs/LeanProofs/SharedLemmas.lean @@ -1,3 +1,4 @@ +import LeanProofs.Flux.Fun.TcbDefsPow2 namespace Nat def bit (b : Bool) : Nat → Nat := cond b (2 * · + 1) (2 * ·) @@ -47,11 +48,8 @@ theorem le_max_of_nat_eq_of_nat {w : Nat} (x y : Nat) : 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 +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 @@ -128,16 +126,16 @@ theorem pow2_isPowerOfTwo (x : Nat) : pow2 x <-> x.isPowerOfTwo := by · 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 +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 (i_pow2_eq_pow2 x x_in_bounds).mp + apply (tcb_defs_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 + apply (tcb_defs_pow2_eq_pow2 x x_in_bounds).mpr rw [pow2_isPowerOfTwo] exact x_pow2 diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean deleted file mode 100644 index 214f9521ca..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0.lean +++ /dev/null @@ -1,11 +0,0 @@ --- 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))))))))))))) - diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean deleted file mode 100644 index 27d9ebd61d..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremAlignedValueGe32LowestFiveBits0Proof.lean +++ /dev/null @@ -1,37 +0,0 @@ -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] diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean deleted file mode 100644 index 09d4386ce8..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2.lean +++ /dev/null @@ -1,8 +0,0 @@ --- 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)))))))) - diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean deleted file mode 100644 index 6d0005462c..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremDiv2Pow2Proof.lean +++ /dev/null @@ -1,20 +0,0 @@ -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 diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean deleted file mode 100644 index d1421ac0a0..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2.lean +++ /dev/null @@ -1,8 +0,0 @@ --- 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))))))))) - diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean deleted file mode 100644 index a8b613e66e..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Div2Pow2Proof.lean +++ /dev/null @@ -1,51 +0,0 @@ -import LeanProofs.TcbTheoremsTheoremPow2Div2Pow2 -import LeanProofs.SharedLemmas - -theorem f_pow2_eq_i_pow2 : f_pow2_0 = i_pow2 := by - funext x; unfold f_pow2_0 i_pow2; simp - -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] - -theorem four_is_pow2 : pow2 4 := by simp - -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 - - -def tcb_theorems_theorem_pow2_div2_pow2_proof : tcb_theorems_theorem_pow2_div2_pow2 := by - unfold tcb_theorems_theorem_pow2_div2_pow2 - intro n _ h _ n_ge0 _ n_in_bounds - obtain ⟨n_pow2, n_ge4⟩ := h - rw [f_pow2_eq_i_pow2] at * - have ntwo_in_bounds: (n.toNat / 2) < 2 ^ 32 := by omega - have nnat_in_bounds: n.toNat < 2 ^ 32 := by omega - have res_n: f_pow2_0 (n.toNat / 2) = true := by - apply (i_pow2_eq_pow2 (n.toNat / 2) ntwo_in_bounds).mpr - apply pow2_div2_pow2 - apply (i_pow2_eq_pow2 n.toNat nnat_in_bounds).mp - rw [Int.toNat_of_nonneg] - assumption - assumption - omega - rw [Int.toNat_of_nonneg] at res_n - assumption - assumption diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean deleted file mode 100644 index c333f67c41..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAligned.lean +++ /dev/null @@ -1,11 +0,0 @@ --- GENERATED; DO NOT EDIT -- --- FUNCTIONS -- -def f_aligned_0 (a0 : Int) (a1 : Int) : Bool := - ((a0 % a1) = 0) - -def f_pow2_1 (a2 : Int) : Bool := - (let a3 := (BitVec.ofInt 32 a2); ((a2 > 0) && ((BitVec.and a3 (BitVec.sub a3 1#32)) = 0#32))) - --- THEOREM -- -def tcb_theorems_theorem_pow2_le_aligned : Prop := (∀ (reftgen_x_0 : Int), (∀ (reftgen_y_1 : Int), (∀ (reftgen_z_2 : Int), (∀ (__ : Int), (((f_aligned_0 reftgen_x_0 reftgen_y_1) ∧ (reftgen_z_2 ≤ reftgen_y_1) ∧ (f_pow2_1 reftgen_y_1) ∧ (f_pow2_1 reftgen_z_2)) -> (∀ (__ : Int), ((reftgen_x_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_x_0 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_y_1 ≥ 0) -> (∀ (__ : Int), ((reftgen_y_1 ≤ 4294967295) -> (∀ (__ : Int), ((reftgen_z_2 ≥ 0) -> (∀ (__ : Int), ((reftgen_z_2 ≤ 4294967295) -> (f_aligned_0 reftgen_x_0 reftgen_z_2)))))))))))))))))) - diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean deleted file mode 100644 index 8b0318c2c1..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2LeAlignedProof.lean +++ /dev/null @@ -1,57 +0,0 @@ -import LeanProofs.TcbTheoremsTheoremPow2LeAligned -import LeanProofs.SharedLemmas - -theorem f_pow2_1_eq_i_pow2 : f_pow2_1 = i_pow2 := by - funext x; unfold f_pow2_1 i_pow2; simp - -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 - -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 - -def tcb_theorems_theorem_pow2_le_aligned_proof : tcb_theorems_theorem_pow2_le_aligned := by - unfold tcb_theorems_theorem_pow2_le_aligned - intros x y z _ h _ x_ge0 _ x_in_bounds _ y_ge0 _ y_in_bounds _ z_ge0 _ z_in_bounds - obtain ⟨x_aligned_y, ⟨z_le_y, ⟨y_pow2, z_pow2⟩⟩⟩ := h - rw [f_pow2_1_eq_i_pow2] at * - unfold f_aligned_0 at * - simp at x_aligned_y - simp - 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 (i_pow2_eq_pow2 y.toNat _).mp - rw [Int.toNat_of_nonneg] - assumption - assumption - omega - · apply (i_pow2_eq_pow2 z.toNat _).mp - rw [Int.toNat_of_nonneg] - assumption - assumption - omega - rw [←Int.toNat_of_nonneg x_ge0, ←Int.toNat_of_nonneg z_ge0] - omega diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean deleted file mode 100644 index 8546d24636..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2Octet.lean +++ /dev/null @@ -1,11 +0,0 @@ --- GENERATED; DO NOT EDIT -- --- FUNCTIONS -- -def f_octet_1 (a2 : Int) : Bool := - ((a2 % 8) = 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_pow2_octet : Prop := (∀ (reftgen_r_0 : Int), (∀ (__ : Int), (((f_pow2_0 reftgen_r_0) ∧ (reftgen_r_0 ≥ 8)) -> (∀ (__ : Int), ((reftgen_r_0 ≥ 0) -> (∀ (__ : Int), ((reftgen_r_0 ≤ 4294967295) -> (f_octet_1 reftgen_r_0)))))))) - diff --git a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean b/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean deleted file mode 100644 index 8fd6d21ff1..0000000000 --- a/lean_proofs/LeanProofs/TcbTheoremsTheoremPow2OctetProof.lean +++ /dev/null @@ -1,41 +0,0 @@ -import LeanProofs.TcbTheoremsTheoremPow2Octet -import LeanProofs.SharedLemmas - -theorem f_pow2_1_eq_i_pow2 : f_pow2_0 = i_pow2 := by - funext x; unfold f_pow2_0 i_pow2; simp - -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 - -def tcb_theorems_theorem_pow2_octet_proof : tcb_theorems_theorem_pow2_octet := by - unfold tcb_theorems_theorem_pow2_octet - intro r0 _ h1 _ r0_ge0 _ r0_in_bounds - obtain ⟨r0_pow2, r0_ge8⟩ := h1 - rw [f_pow2_1_eq_i_pow2] at * - unfold f_octet_1 - simp - have nat_res : r0.toNat % 8 = 0 := by - apply power_of_2_ge_8_octet - case _ => - apply (i_pow2_0_is_power_of_2 r0.toNat _).mp - case _ => - rw [Int.toNat_of_nonneg] - assumption - assumption - case _ => - omega - case _ => - omega - omega 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