Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Reusable procedures and memory preservation

Lax350013.ProcedureContracts · concepts/Lax350013/ProcedureContracts.lean · lax-350013

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    A solver remains correct when other procedures are appended to its program. Its contract specifies inputs, outputs, preserved memory, time, and polynomial bounds on words, scratch space and call depth. These guarantees make the algorithmic reductions compositional.

    Concept map
    2 concepts; 7 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1/-
    2Copyright (c) 2026 Anthropic, PBC. All rights reserved.
    3Released under Apache 2.0 license as described in the file LICENSE.
    4SPDX-License-Identifier: Apache-2.0
    5-/
    6/-
    7Modified for the independent Lax packaging by Édouard Bonnet, 2026.
    8Derived from 3sum-apsp/ThreeSumApsp/Lang and Util/List.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
    9Changes: Lax module/namespace layout, separated concepts and proofs, archive
    10annotations, and compatibility with the archive Lean/mathlib environment.
    11See NOTICE and README.md in the submission root for provenance and scope.
    12-/
    13
    14import Mathlib.Algebra.MvPolynomial.Basic
    15import Mathlib.Analysis.SpecialFunctions.Log.Base
    16import Mathlib.Analysis.SpecialFunctions.Log.Basic
    17import Mathlib.Analysis.SpecialFunctions.Pow.Real
    18import Mathlib.Combinatorics.SimpleGraph.Basic
    19import Mathlib.Data.Finset.Sort
    20import Mathlib.LinearAlgebra.Matrix.Notation
    21import Mathlib.MeasureTheory.Integral.Bochner.Basic
    22import Mathlib.NumberTheory.PrimeCounting
    23import Mathlib.Probability.Independence.Basic
    24import Mathlib.Tactic.DeriveFintype
    25import Lax350013.StructuredPrograms
    26
    27/-!
    28---
    29title: Reusable procedures and memory preservation
    30type: definition
    31---
    32A solver remains correct when other procedures are appended to its program. Its contract specifies inputs, outputs, preserved memory, time, and polynomial bounds on words, scratch space and call depth. These guarantees make the algorithmic reductions compositional.
    33-/
    34
    35namespace Lax350013.ProcedureContracts
    36
    37open Finset
    38open Lax350013.StructuredPrograms
    39
    40/-- The statement s, started in σ, ends within T steps in a state that satisfies Q. -/
    41def Ends (lim : Limits) (P : Program) (d : ℕ) (s : Stmt) (σ : State) (T : ℕ) (Q : State → Prop) :
    42 Prop :=
    43 ∃ σ' c, Exec lim P d s σ σ' c ∧ c ≤ T ∧ Q σ'
    44
    45/-- The bound 2^s · ((p₁ + 1) (p₂ + 1) ⋯)^k in the parameters of an instance. -/
    46def polyBound (s k : ℕ) (params : List ℕ) : ℕ := 2 ^ s * ((params.map (· + 1)).prod) ^ k
    47
    48/-- The cell `b` is among the `n` cells from address `a`. -/
    49abbrev Inside (a n b : ℕ) : Prop := a ≤ b ∧ b < a + n
    50
    51/-- The cell `b` is not among the `n` cells from address `a`. -/
    52abbrev Outside (a n b : ℕ) : Prop := b < a ∨ a + n ≤ b
    53
    54/-- Two regions of the memory, of `n` cells from `a` and of `n'` cells from `a'`, do not meet. -/
    55abbrev Apart (a n a' n' : ℕ) : Prop := a + n ≤ a' ∨ a' + n' ≤ a
    56
    57/-- The memory `μ'` agrees with `μ` on every cell that satisfies `K`. -/
    58def SameOn (K : ℕ → Prop) (μ μ' : ℕ → ℤ) : Prop := ∀ b, K b → μ' b = μ b
    59
    60/-- No cell below the free pointer has changed. -/
    61abbrev Kept (μ μ' : ℕ → ℤ) (fr : ℕ) : Prop := SameOn (· < fr) μ μ'
    62
    63/-- No cell below the free pointer has changed, except the `len` cells from `out`. -/
    64abbrev KeptBut (μ μ' : ℕ → ℤ) (fr out len : ℕ) : Prop :=
    65 SameOn (fun x => x < fr ∧ Outside out len x) μ μ'
    66
    67/-- The cells a, a + 1, … of the memory μ hold the list l. -/
    68def Seg (μ : ℕ → ℤ) (a : ℕ) (l : List ℤ) : Prop := ∀ i (h : i < l.length), μ (a + i) = l[i]
    69
    70/-- The cells a, a + 1, … hold a list of natural numbers. -/
    71abbrev SegN (μ : ℕ → ℤ) (a : ℕ) (l : List ℕ) : Prop := Seg μ a (l.map fun x : ℕ => (x : ℤ))
    72
    73/-- All members of the list `l` have absolute value at most `U`. -/
    74def AbsLe (l : List ℤ) (U : ℤ) : Prop := ∀ x ∈ l, |x| ≤ U
    75
    76/-- What a run needs: the largest absolute value it forms, the number of cells it uses from the free
    77pointer on, and the number of levels of calls below the procedure. -/
    78structure Need : Type where
    79 word : ℕ
    80 cells : ℕ
    81 depth : ℕ
    82
    83/-- The limits allow for the need of a procedure that is called at depth `d` with the free pointer
    84`fr`. An address always fits in a word. -/
    85structure Need.Ok (r : Need) (lim : Limits) (fr d : ℕ) : Prop where
    86 word : (r.word : ℤ) ≤ lim.word
    87 cells : fr + r.cells ≤ lim.space
    88 space : (lim.space : ℤ) ≤ lim.word
    89 depth : d + r.depth ≤ lim.depth
    90
    91/-- A need that depends on a size and a bound is polynomially bounded in the two: by
    92`2^s ((n + 1) (U + 1))^k`. -/
    93def PolyNeed (need : ℕ → ℕ → Need) : Prop :=
    94 ∃ s k : ℕ, ∀ n U : ℕ, (need n U).word ≤ polyBound s k [n, U] ∧ (need n U).cells ≤
    95 polyBound s k [n, U] ∧
    96 (need n U).depth ≤ polyBound s k [n, U]
    97
    98/-- A problem with a calling convention. -/
    99structure Task : Type 1 where
    100 /-- The instances, as they lie in the memory: sizes, bound, addresses, contents. -/
    101 Inst : Type
    102 /-- The size of an instance. -/
    103 size : Inst → ℕ
    104 /-- The bound on the absolute values of its numbers that is handed to the solver. -/
    105 bound : Inst → ℕ
    106 /-- The arguments of the call, without the free pointer, which comes last. -/
    107 args : Inst → List ℤ
    108 /-- The instance is valid, and it lies in the memory below the free pointer. -/
    109 Pre : Inst → (ℕ → ℤ) → ℕ → Prop
    110 /-- The result and the final memory are right. (That the cells below the free pointer are
    111 otherwise unchanged is part of this.) -/
    112 Post : Inst → (ℕ → ℤ) → ℕ → ℤ → (ℕ → ℤ) → Prop
    113
    114/-- **Procedure `p` of the program `P` solves the task** within `T (size) (bound)` steps, whenever
    115the limits allow for `need (size) (bound)`; and so it does in every program that begins with `P`. -/
    116def Solves (task : Task) (P : Program) (p : ℕ) (T : ℕ → ℕ → ℕ) (need : ℕ → ℕ → Need) : Prop :=
    117 ∃ body, P[p]? = some body ∧
    118 ∀ (R : Program) (lim : Limits) (d : ℕ) (x : task.Inst) (μ : ℕ → ℤ) (fr : ℕ), task.Pre x μ fr →
    119 (need (task.size x) (task.bound x)).Ok lim fr d →
    120 Ends lim (P ++ R) d body ⟨frame (task.args x ++ [(fr : ℤ)]), μ⟩
    121 (T (task.size x) (task.bound x))
    122 fun σ' => task.Post x μ fr (σ'.loc 0) σ'.mem
    123
    124/-- "The task is solved in time `T`", for a real-valued `T` whose second argument is an upper bound
    125on the numbers: some solver with a polynomially bounded need takes at most `T n u` steps on every
    126instance of size `n ≥ 1` with a bound `1 ≤ U ≤ u`. -/
    127def SolvedIn (task : Task) (T : ℕ → ℝ → ℝ) : Prop :=
    128 ∃ (P : Program) (p : ℕ) (Tn : ℕ → ℕ → ℕ) (need : ℕ → ℕ → Need), PolyNeed need ∧
    129 Solves task P p Tn need ∧
    130 ∀ (n U : ℕ) (u : ℝ), 1 ≤ n → 1 ≤ U → (U : ℝ) ≤ u → (Tn n U : ℝ) ≤ T n u
    131
    132/-- A problem with a calling convention and a list of parameters. -/
    133structure TaskN : Type 1 where
    134 /-- The instances, as they lie in the memory. -/
    135 Inst : Type
    136 /-- The parameters on which time and need depend. -/
    137 pars : Inst → List ℕ
    138 /-- The arguments of the call, without the free pointer, which comes last. -/
    139 args : Inst → List ℤ
    140 /-- The instance is valid, and it lies in the memory below the free pointer. -/
    141 Pre : Inst → (ℕ → ℤ) → ℕ → Prop
    142 /-- The result and the final memory are right. -/
    143 Post : Inst → (ℕ → ℤ) → ℕ → ℤ → (ℕ → ℤ) → Prop
    144
    145/-- Procedure `p` of the program `P` solves the task within `T pars` steps, whenever the limits
    146allow for `need pars`; and so it does in every program that begins with `P`. -/
    147def SolvesN (task : TaskN) (P : Program) (p : ℕ) (T : List ℕ → ℕ) (need : List ℕ → Need) : Prop :=
    148 ∃ body, P[p]? = some body ∧
    149 ∀ (R : Program) (lim : Limits) (d : ℕ) (x : task.Inst) (μ : ℕ → ℤ) (fr : ℕ), task.Pre x μ fr →
    150 (need (task.pars x)).Ok lim fr d →
    151 Ends lim (P ++ R) d body ⟨frame (task.args x ++ [(fr : ℤ)]), μ⟩ (T (task.pars x))
    152 fun σ' => task.Post x μ fr (σ'.loc 0) σ'.mem
    153
    154/-- A need that is polynomially bounded in the parameters. -/
    155def PolyNeedN (need : List ℕ → Need) : Prop :=
    156 ∃ s k : ℕ, ∀ ps : List ℕ, (need ps).word ≤ polyBound s k ps ∧ (need ps).cells ≤ polyBound s k ps ∧
    157 (need ps).depth ≤ polyBound s k ps
    158
    159end Lax350013.ProcedureContracts
    160
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…