Structured programs and exact execution costs

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

definition

Loading review…

Natural Language Statement

Definition

The imperative language used to construct the algorithms: finite programs, procedure calls, memory, word and stack limits, and an exact step-counted execution relation. The upstream compiler proves that these programs run on the word RAM with constant-factor overhead.

Concept map

1 concept; 8 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	/-
2	Copyright (c) 2026 Anthropic, PBC. All rights reserved.
3	Released under Apache 2.0 license as described in the file LICENSE.
4	SPDX-License-Identifier: Apache-2.0
5	-/
6	/-
7	Modified for the independent Lax packaging by Édouard Bonnet, 2026.
8	Derived from 3sum-apsp/ThreeSumApsp/Lang/Syntax.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
9	Changes: Lax module/namespace layout, separated concepts and proofs, archive
10	annotations, and compatibility with the archive Lean/mathlib environment.
11	See NOTICE and README.md in the submission root for provenance and scope.
12	-/
13
14	import Mathlib.Algebra.MvPolynomial.Basic
15	import Mathlib.Analysis.SpecialFunctions.Log.Base
16	import Mathlib.Analysis.SpecialFunctions.Log.Basic
17	import Mathlib.Analysis.SpecialFunctions.Pow.Real
18	import Mathlib.Combinatorics.SimpleGraph.Basic
19	import Mathlib.Data.Finset.Sort
20	import Mathlib.LinearAlgebra.Matrix.Notation
21	import Mathlib.MeasureTheory.Integral.Bochner.Basic
22	import Mathlib.NumberTheory.PrimeCounting
23	import Mathlib.Probability.Independence.Basic
24	import Mathlib.Tactic.DeriveFintype
25
26	/-!
27	---
28	title: Structured programs and exact execution costs
29	type: definition
30	---
31	The imperative language used to construct the algorithms: finite programs, procedure calls, memory, word and stack limits, and an exact step-counted execution relation. The upstream compiler proves that these programs run on the word RAM with constant-factor overhead.
32	-/
33
34	namespace Lax350013.StructuredPrograms
35
36	open Finset
37
38	/-- The operations on two words. -/
39	inductive Op : Type
40	\| add \| sub \| mul
41	deriving DecidableEq, Repr
42
43	/-- The result of an operation. -/
44	def Op.eval : Op → ℤ → ℤ → ℤ
45	\| .add, a, b => a + b
46	\| .sub, a, b => a - b
47	\| .mul, a, b => a * b
48
49	/-- Expressions: constants, local variables, operations, and the content of the memory cell at an
50	address. -/
51	inductive Expr : Type
52	\| const (n : ℕ)
53	\| var (x : ℕ)
54	\| op (o : Op) (a b : Expr)
55	\| load (a : Expr)
56	deriving Repr
57
58	/-- Tests. -/
59	inductive Cond : Type
60	\| lt (a b : Expr)
61	\| eq (a b : Expr)
62	deriving Repr
63
64	/-- Statements. `call p args x` runs procedure number p on the values of args and puts its result
65	into x. -/
66	inductive Stmt : Type
67	\| skip
68	\| set (x : ℕ) (e : Expr)
69	\| store (a e : Expr)
70	\| seq (s₁ s₂ : Stmt)
71	\| ite (c : Cond) (s₁ s₂ : Stmt)
72	\| while (c : Cond) (s : Stmt)
73	\| call (p : ℕ) (args : List Expr) (x : ℕ)
74	deriving Repr
75
76	/-- A program: the bodies of its procedures, numbered from 0. -/
77	abbrev Program : Type := List Stmt
78
79	/-- What a running procedure sees: its local variables and the memory. -/
80	structure State : Type where
81	loc : ℕ → ℤ
82	mem : ℕ → ℤ
83
84	/-- The limits on a run: largest absolute value of a word, number of memory cells, nesting depth of
85	calls. -/
86	structure Limits : Type where
87	word : ℤ
88	space : ℕ
89	depth : ℕ
90
91	/-- The value of an expression. -/
92	def Expr.val (s : State) : Expr → ℤ
93	\| .const n => n
94	\| .var x => s.loc x
95	\| .op o a b => o.eval (a.val s) (b.val s)
96	\| .load a => s.mem (a.val s).toNat
97
98	/-- The number of steps that evaluating an expression takes: one for each of its constants,
99	variables, operations, loads. -/
100	def Expr.cost : Expr → ℕ
101	\| .const _ => 1
102	\| .var _ => 1
103	\| .op _ a b => a.cost + b.cost + 1
104	\| .load a => a.cost + 1
105
106	/-- An address within the limits. -/
107	def Limits.Addr (lim : Limits) (a : ℤ) : Prop := 0 ≤ a ∧ a < lim.space
108
109	/-- The evaluation of an expression stays within the limits: every value that is formed fits in a
110	word, and every address that is read is within the memory. -/
111	def Expr.Safe (lim : Limits) (s : State) : Expr → Prop
112	\| .const n => (n : ℤ) ≤ lim.word
113	\| .var _ => True
114	\| .op o a b => a.Safe lim s ∧ b.Safe lim s ∧ \|o.eval (a.val s) (b.val s)\| ≤ lim.word
115	\| .load a => a.Safe lim s ∧ lim.Addr (a.val s)
116
117	/-- Whether a test holds. -/
118	def Cond.Holds (s : State) : Cond → Prop
119	\| .lt a b => a.val s < b.val s
120	\| .eq a b => a.val s = b.val s
121
122	/-- The number of steps of a test: its two sides and the comparison. -/
123	def Cond.cost : Cond → ℕ
124	\| .lt a b => a.cost + b.cost + 1
125	\| .eq a b => a.cost + b.cost + 1
126
127	/-- The evaluation of a test stays within the limits. -/
128	def Cond.Safe (lim : Limits) (s : State) : Cond → Prop
129	\| .lt a b => a.Safe lim s ∧ b.Safe lim s
130	\| .eq a b => a.Safe lim s ∧ b.Safe lim s
131
132	/-- The local variables of a procedure that has just been called: the arguments in 0, 1, …, and 0 in
133	all others. -/
134	def frame (args : List ℤ) : ℕ → ℤ := fun i => args.getD i 0
135
136	/-- The memory that holds the list ws in the cells 0, 1, 2, … and 0 elsewhere. -/
137	def memOf (ws : List ℤ) : ℕ → ℤ := fun a => ws.getD a 0
138
139	/-- `Exec lim P d s σ σ' c`: within the limits lim, and at nesting depth d of calls, the statement
140	s of the program P, started in the state σ, ends in the state σ' after exactly c steps. -/
141	inductive Exec (lim : Limits) (P : Program) : ℕ → Stmt → State → State → ℕ → Prop
142	\| skip {d σ} : Exec lim P d .skip σ σ 0
143	\| set {d σ x e} : e.Safe lim σ →
144	Exec lim P d (.set x e) σ { σ with loc := Function.update σ.loc x (e.val σ) } (e.cost + 1)
145	\| store {d σ a e} : a.Safe lim σ → e.Safe lim σ → lim.Addr (a.val σ) →
146	Exec lim P d (.store a e) σ { σ with mem := Function.update σ.mem (a.val σ).toNat (e.val σ) }
147	(a.cost + e.cost + 1)
148	\| seq {d σ σ' σ'' s₁ s₂ c₁ c₂} : Exec lim P d s₁ σ σ' c₁ → Exec lim P d s₂ σ' σ'' c₂ →
149	Exec lim P d (.seq s₁ s₂) σ σ'' (c₁ + c₂)
150	\| iteTrue {d σ σ' c s₁ s₂ k} : c.Safe lim σ → c.Holds σ → Exec lim P d s₁ σ σ' k →
151	Exec lim P d (.ite c s₁ s₂) σ σ' (c.cost + 1 + k)
152	\| iteFalse {d σ σ' c s₁ s₂ k} : c.Safe lim σ → ¬ c.Holds σ → Exec lim P d s₂ σ σ' k →
153	Exec lim P d (.ite c s₁ s₂) σ σ' (c.cost + 1 + k)
154	\| whileFalse {d σ c s} : c.Safe lim σ → ¬ c.Holds σ → Exec lim P d (.while c s) σ σ (c.cost + 1)
155	\| whileTrue {d σ σ' σ'' c s k₁ k₂} : c.Safe lim σ → c.Holds σ → Exec lim P d s σ σ' k₁ →
156	Exec lim P d (.while c s) σ' σ'' k₂ → Exec lim P d (.while c s) σ σ'' (c.cost + 1 + k₁ + k₂)
157	\| call {d σ σ' p args x body k} : (∀ e ∈ args, e.Safe lim σ) → P[p]? = some body → d < lim.depth →
158	Exec lim P (d + 1) body ⟨frame (args.map (·.val σ)), σ.mem⟩ σ' k →
159	Exec lim P d (.call p args x) σ ⟨Function.update σ.loc x (σ'.loc 0), σ'.mem⟩
160	((args.map Expr.cost).sum + 2 + k)
161
162	/-- Everything held in a variable or in a cell fits in a word. -/
163	def State.Bounded (lim : Limits) (σ : State) : Prop :=
164	(∀ x, \|σ.loc x\| ≤ lim.word) ∧ ∀ a, \|σ.mem a\| ≤ lim.word
165
166	end Lax350013.StructuredPrograms
167

Builds on

none

Used by

Lax350013.ProcedureContracts

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

Structured programs and exact execution costs

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments