From 953278fc66486a33dd345c9fbd887487fb95d86c Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 08:30:22 -0400 Subject: [PATCH] Reuse Aeneas rules for views and indexed loops Use upstream checked-arithmetic and specification registrations to compose proofs through mathematical projections. Add an indexed-loop adapter that carries a prefix computation and representation invariant, with length minus index as the decreasing termination measure. Examples exercise successful and overflowing arithmetic, caller reuse, partial contracts and loop progress. Independently written outcome expectations keep the intended guarantees observable without maintaining a second execution logic. gherrit-pr-id: Gfbj3enqrcenbe76pfvmdhbt2b3h3j5fj Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/lean/Loops.lean | 57 +++++++++ verification/aeneas/lean/Proofs.lean | 1 + verification/aeneas/lean/SupportTests.lean | 141 +++++++++++++++++++++ 3 files changed, 199 insertions(+) create mode 100644 verification/aeneas/lean/Loops.lean create mode 100644 verification/aeneas/lean/SupportTests.lean diff --git a/verification/aeneas/lean/Loops.lean b/verification/aeneas/lean/Loops.lean new file mode 100644 index 0000000000..300d1bc5a0 --- /dev/null +++ b/verification/aeneas/lean/Loops.lean @@ -0,0 +1,57 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Aeneas +public section + +/-! +Aeneas already proves loop reasoning rules. This adapter specializes its +decreasing-natural rule to the indexed loops used by layout construction. The +caller supplies a prefix model and proves one body step. The adapter uses +length minus index as the termination measure and carries both the model +relation and the caller's representation invariant across every step. This +avoids reproving termination separately for each indexed operation. +-/ +open Aeneas Aeneas.Std + +namespace AeneasContracts + +/-- An indexed Rust loop refines a mathematical prefix computation. The +caller proves one body step: continue advances the index by one, while done +occurs at the length. This rule supplies the index bounds and termination +measure, and carries an arbitrary representation invariant. -/ +theorem indexed_loop_spec {State Model : Type} + (length : Nat) (view : State → Model) (prefixValue : Nat → Model) + (valid : State → Prop) + (body : State × Usize → Result (ControlFlow (State × Usize) State)) + (hbody : ∀ state i, i.val ≤ length → view state = prefixValue i.val → valid state → + body (state, i) ⦃ r => match r with + | .cont (next, j) => i.val < length ∧ j.val = i.val + 1 ∧ + view next = prefixValue j.val ∧ valid next + | .done out => i.val = length ∧ view out = prefixValue i.val ∧ valid out ⦄) + (state : State) (i : Usize) + (hi : i.val ≤ length) (hv : view state = prefixValue i.val) (hc : valid state) : + loop body (state, i) ⦃ out => view out = prefixValue length ∧ valid out ⦄ := by + apply loop.spec_decr_nat + (fun s : State × Usize => length - s.2.val) + (fun s => s.2.val ≤ length ∧ view s.1 = prefixValue s.2.val ∧ valid s.1) + · rintro ⟨state, i⟩ ⟨hi, hv, hc⟩ + apply WP.spec_mono (hbody state i hi hv hc) + intro r hr + cases r with + | done out => + obtain ⟨hend, hv, hc⟩ := hr + exact ⟨hend ▸ hv, hc⟩ + | cont s => + rcases s with ⟨next, j⟩ + obtain ⟨hlt, hj, hv, hc⟩ := hr + exact ⟨⟨by scalar_tac, hv, hc⟩, by scalar_tac⟩ + · exact ⟨hi, hv, hc⟩ + +end AeneasContracts diff --git a/verification/aeneas/lean/Proofs.lean b/verification/aeneas/lean/Proofs.lean index fc494fe6b0..1dbd3c3835 100644 --- a/verification/aeneas/lean/Proofs.lean +++ b/verification/aeneas/lean/Proofs.lean @@ -10,6 +10,7 @@ module public import Specs public import Proofs.Util public import Aeneas +public import Loops import all Mathlib.Data.Nat.Log import all Init.Data.Nat.Power2.Basic @[expose] public section diff --git a/verification/aeneas/lean/SupportTests.lean b/verification/aeneas/lean/SupportTests.lean new file mode 100644 index 0000000000..3d00b1ac35 --- /dev/null +++ b/verification/aeneas/lean/SupportTests.lean @@ -0,0 +1,141 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Aeneas +public import Loops +public import RequiredContracts +@[expose] public section + +/-! +These examples exercise arithmetic, mathematical-view composition, and +indexed-loop reasoning as ordinary consumers of the shared proof support. +They test how the abstractions are used together, rather than merely +repeating their definitions. The independently written expectations keep +termination, returned values, and loop-state preservation observable. +-/ +open Aeneas Aeneas.Std AeneasContracts AeneasSpecs +namespace SupportTests + +-- Use upstream checked-operation registrations, including overflow branches. +theorem add_spec (x y : Usize) : + lift (x.checked_add y) + ⦃ out => out.map UScalar.val = + if x.val + y.val ≤ Usize.max then some (x.val + y.val) else none ⦄ := by + step as ⟨out, hout⟩ + cases out <;> simp_all only [Option.map_none, Option.map_some] + all_goals scalar_tac +split + +theorem sub_spec (x y : Usize) : + lift (x.checked_sub y) + ⦃ out => out.map UScalar.val = + if y ≤ x then some (x.val - y.val) else none ⦄ := by + step as ⟨out, hout⟩ + cases out <;> simp_all only [Option.map_none, Option.map_some] + all_goals scalar_tac +split + +theorem mul_spec (x y : Usize) : + lift (x.checked_mul y) + ⦃ out => out.map UScalar.val = + if x.val * y.val ≤ Usize.max then some (x.val * y.val) else none ⦄ := by + step as ⟨out, hout⟩ + cases out <;> simp_all only [Option.map_none, Option.map_some] + all_goals scalar_tac +split + +def pair (n : Nat) : Result (Nat × Nat) := .ok (n, n + 1) + +theorem pair_view_spec (n : Nat) : + pair n + ⦃ r => Prod.fst r = n ∧ r.2 = n + 1 ⦄ := by + exact WP.spec.ret ⟨rfl, rfl⟩ + +attribute [step] pair_view_spec + +-- A caller uses the view theorem through Aeneas's existing spec registry. +theorem pair_caller_spec (n : Nat) : + (do let r ← pair n; Result.ok r.1) + ⦃ r => id r = n ⦄ := by + step* + simp_all + +theorem diverging_view_spec : + (Result.div : Result Nat) + ⦃ r => Nat.succ r = 0 ∧ r = 9 ⦄div := by + exact WP.dspec.div _ + +theorem partial_view_spec (n : Nat) : + Result.ok n + ⦃ r => Nat.succ r = n + 1 ⦄div := by + exact WP.dspec.ret rfl + +-- The independent family compares every outcome, even though `pair` itself +-- happens to return the expected pair for every input. +spec pair_inline for pair with 0 type parameters + ensures (first, second) => first = n ∧ second = n + 1 + +theorem pair_inline_proof : pair_inline := by + intro n math decoded + change some n = some math at decoded + cases decoded + exact ⟨(n, n + 1), rfl, rfl, rfl⟩ + +def pair_required_contract (n : Nat) (run : Result (Nat × Nat)) : Prop := + ∃ r, run = .ok r ∧ r.1 = n ∧ r.2 = n + 1 + +def pair_required : Prop := ∀ n : Nat, pair_required_contract n (pair n) + +@[contract_simps] theorem pair_required_bridge (n : Nat) (run : Result (Nat × Nat)) + (provided : pair_inline_contract n run) : pair_required_contract n run := by + obtain ⟨out, success, math, decoded, first, second⟩ := + (WP.spec_equiv_exists _ _).mp (provided n rfl) + have same : out = math := by + simpa [RustModel.decode, modelProd] using decoded + cases same + exact ⟨out, success, first, second⟩ + +check_contract pair_required using pair_inline_proof + +-- An alias still names its own independent family and canonical inline proof. +def pair_required_again_contract := pair_required_contract +def pair_required_again : Prop := pair_required +@[contract_simps] theorem pair_required_again_bridge + (n : Nat) (run : Result (Nat × Nat)) (provided : pair_inline_contract n run) : + pair_required_again_contract n run := pair_required_bridge n run provided +check_contract pair_required_again using pair_inline_proof + +example : ∀ n : Nat, WP.spec (do let r ← pair n; Result.ok r.1) + (fun r => r = n) := pair_caller_spec +example : WP.dspec (Result.div : Result Nat) + (fun r => Nat.succ r = 0 ∧ r = 9) := diverging_view_spec +example : ∀ n : Nat, WP.dspec (Result.ok n) + (fun r => Nat.succ r = n + 1) := partial_view_spec + +def counterBody (n : Usize) (s : Nat × Usize) : + Result (ControlFlow (Nat × Usize) Nat) := do + if s.2 < n then + let j ← s.2 + 1#usize + .ok (.cont (s.1 + 1, j)) + else .ok (.done s.1) + +theorem counter_spec (n i : Usize) (hi : i ≤ n) : + loop (counterBody n) (i.val, i) ⦃ out => out = n.val ∧ True ⦄ := by + apply indexed_loop_spec n.val id (fun i => i) (fun _ => True) + · intro state idx hidx hv _ + unfold counterBody + simp only [UScalar.lt_equiv] + split + · rename_i hlt + step as ⟨j, hj⟩ + simp_all [id] + · rename_i hdone + exact WP.spec.ret ⟨by scalar_tac, hv, trivial⟩ + · exact (UScalar.le_equiv _ _).mp hi + · rfl + · trivial + +end SupportTests