Lax Lean Archive

Structured stack programs with black-box calls

Lax218471.Programs · concepts/Lax218471/Programs.lean · lax-218471

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

    Programs use stack operations, finite control, sequencing, conditionals, while loops, and calls to a fixed library of contracts. A call replaces one stack with its result and preserves every other stack and the caller's control. The execution relation records the number of source instructions and a bound on all call argument and result lengths. In particular, a polynomial bound on the number of iterations alone does not assert polynomial time.

    Concept map
    3 concepts; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Lax218471.Subroutine
    2import Lax218471.PolynomialTime
    3
    4/-!
    5---
    6title: Structured stack programs with black-box calls
    7type: definition
    8---
    9Programs use stack operations, finite control, sequencing, conditionals,
    10while loops, and calls to a fixed library of contracts. A call replaces one
    11stack with its result and preserves every other stack and the caller's control.
    12The execution relation records the number of source instructions and a bound
    13on all call argument and result lengths. In particular, a polynomial bound
    14on the number of iterations alone does not assert polynomial time.
    15-/
    16
    17namespace Lax218471.Programs
    18
    19open Subroutine
    20
    21variable {K A σ I : Type}
    22
    23/-- One local operation; the control type is finite when programs are compiled. -/
    24inductive Op (K A σ : Type)
    25 | push (k : K) (f : σ → A)
    26 | pop (k : K) (f : σ → Option A → σ)
    27 | peek (k : K) (f : σ → Option A → σ)
    28 | load (f : σ → σ)
    29
    30/-- A finite program with named library calls. Loops retain their body as finite code. -/
    31inductive Program (K A σ I : Type)
    32 | atom (o : Op K A σ)
    33 | call (i : I) (port : K)
    34 | seq (p q : Program K A σ I)
    35 | branch (b : σ → Bool) (p q : Program K A σ I)
    36 | loop (b : σ → Bool) (p : Program K A σ I)
    37
    38def Op.apply [DecidableEq K] (o : Op K A σ) (s : Store (fun _ : K => A) σ) :
    39 Store (fun _ : K => A) σ :=
    40 match o with
    41 | .push k f => ⟨s.state, Function.update s.stk k (f s.state :: s.stk k)⟩
    42 | .pop k f => ⟨f s.state (s.stk k).head?, Function.update s.stk k (s.stk k).tail⟩
    43 | .peek k f => ⟨f s.state (s.stk k).head?, s.stk⟩
    44 | .load f => ⟨f s.state, s.stk⟩
    45
    46/-- Source execution, with a bound on the length of every argument and reply. -/
    47inductive Executes [DecidableEq K] (R : I → List A → List A → Prop) (size : ℕ) :
    48 Program K A σ I → Store (fun _ : K => A) σ → Store (fun _ : K => A) σ → ℕ → Prop
    49 | atom (o) (s) : Executes R size (.atom o) s (o.apply s) 1
    50 | call (i) (port) (s) (y) : R i (s.stk port) y →
    51 (s.stk port).length ≤ size → y.length ≤ size →
    52 Executes R size (.call i port) s ⟨s.state, Function.update s.stk port y⟩ 1
    53 | seq {p q s u t a b} : Executes R size p s u a → Executes R size q u t b →
    54 Executes R size (.seq p q) s t (a + b)
    55 | branch_true {p q s t a} {b : σ → Bool} : b s.state = true →
    56 Executes R size p s t a → Executes R size (.branch b p q) s t (a + 1)
    57 | branch_false {p q s t a} {b : σ → Bool} : b s.state = false →
    58 Executes R size q s t a → Executes R size (.branch b p q) s t (a + 1)
    59 | loop_false {p s} {b : σ → Bool} : b s.state = false →
    60 Executes R size (.loop b p) s s 1
    61 | loop_true {p s u t a c} {b : σ → Bool} : b s.state = true →
    62 Executes R size p s u a → Executes R size (.loop b p) u t c →
    63 Executes R size (.loop b p) s t (a + c + 1)
    64
    65end Lax218471.Programs
    66
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…