Reuse Aeneas rules for views and indexed loops

verification/aeneas/README.md

@@ -645,6 +645,44 @@ its generated proposition. Edit its proof directly in Lean. No proof copying
 back to Rust is required. This development cache is for iteration; CI always
 regenerates specifications and builds both models in fresh isolated projects.
 
+## Mathematical views and indexed loops
+
+### Arithmetic, mathematical views, and indexed loops
+
+Checked addition, subtraction, and multiplication already have upstream
+`step_pure` specifications. Use `step as ⟨result, facts⟩` and split the `Option`
+result to obtain both the exact successful value and the overflow condition.
+`SupportTests.lean` exercises all inputs, including overflow.
+
+A contract may express equality through a pure mathematical view:
+
+```lean
+theorem operation_spec (input : Input) (h : valid input) :
+    operation input ⦃ result =>
+      view result = mathematicalOperation (view input) ∧ canonical result ⦄ := by
+  ...
+```
+
+This ordinary theorem states the existing total WP postcondition directly.
+A view-only theorem states just the view equality. Partial correctness uses
+`⦄div` in place of `⦄`: it explicitly permits divergence and still excludes
+failure. These are Aeneas's existing specification operators. Use `WP.spec_mono`
+to adapt an existing result specification to a view, and register useful caller
+specifications with `attribute [step] operation_spec`. The existing Aeneas
+registry then lets callers use `step` without specifying the theorem manually.
+
+`AeneasContracts.indexed_loop_spec` specializes Aeneas's `loop.spec_decr_nat`
+to a state and `Usize` index. Supply a view, the mathematical value of each
+prefix, and a representation invariant. Each continuing body step must advance
+the index by exactly one and establish the next prefix; a completed step must
+be at the length. The adapter supplies bounds and the decreasing `length - index`
+termination measure. `SupportTests.lean` contains an independent example.
+
+The specification syntax, examples, and required-contract proof terms
+participate in the axiom audit. Failure controls challenge an incorrect view,
+divergence under a total view contract, a stationary loop index, an incorrect
+prefix step, and continuing past the loop bound.
+
 ## Updating models and fuzzy comparison
 
 `golden/` stores all four complete generated Aeneas modules, including types,

verification/aeneas/lean/Loops.lean

@@ -0,0 +1,57 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, 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

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

verification/aeneas/lean/SupportTests.lean

@@ -0,0 +1,141 @@
+/- Copyright 2026 The Fuchsia Authors
+
+Licensed under a BSD-style license <LICENSE-BSD>, Apache License, Version 2.0
+<LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+license <LICENSE-MIT or https://opensource.org/licenses/MIT>, 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