From 057ea9d3895a911df3eb0bc1911c41b591f1b483 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 19 Jul 2026 14:49:59 +0000 Subject: [PATCH 01/16] feat(Models): add rose tree machine data model and program semantics Introduce the RoseTreeMachine module: `Data`, a rose-tree structure for encoding Lean data (with decidable equality, size measure, and recursion/ induction principles), `DataEncode` instances for encoding `Bool`, `List`, and other types into `Data`, and `Prog`/`ProgSem` defining the RTM programming language along with its time/space complexity notions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- Complexitylib/Models.lean | 3 + .../Models/RoseTreeMachine/Data.lean | 123 ++++++ .../Models/RoseTreeMachine/DataEncode.lean | 107 +++++ .../Models/RoseTreeMachine/Prog.lean | 396 ++++++++++++++++++ 4 files changed, 629 insertions(+) create mode 100644 Complexitylib/Models/RoseTreeMachine/Data.lean create mode 100644 Complexitylib/Models/RoseTreeMachine/DataEncode.lean create mode 100644 Complexitylib/Models/RoseTreeMachine/Prog.lean diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean index 7bd2abd6..65814c56 100644 --- a/Complexitylib/Models.lean +++ b/Complexitylib/Models.lean @@ -56,6 +56,9 @@ import Complexitylib.Models.TuringMachine.UTM.ClockedUtm import Complexitylib.Models.TuringMachine.UTM.HierarchySupport import Complexitylib.Models.TuringMachine.UTM.Diagonal import Complexitylib.Models.RandomAccessMachine +import Complexitylib.Models.RoseTreeMachine.Data +import Complexitylib.Models.RoseTreeMachine.DataEncode +import Complexitylib.Models.RoseTreeMachine.Prog /-! # Computation models diff --git a/Complexitylib/Models/RoseTreeMachine/Data.lean b/Complexitylib/Models/RoseTreeMachine/Data.lean new file mode 100644 index 00000000..3430c6bf --- /dev/null +++ b/Complexitylib/Models/RoseTreeMachine/Data.lean @@ -0,0 +1,123 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Mathlib.Data.Part + +/-! +# Main internal data type for the rose tree machine (RTM) + +This file contains the main internal data structure for the RTM, `Data`, a rose tree. + +## Main definitions and notations + +- `Data` - the main data structure +- `Data.size` - the size of a `Data` object when encoded using parentheses, complexity results + use this size as the main measure. +- `Data.recL` - the main recursion principle for `Data` +- `Data.inductionL` - the main induction principle for `Data` + +-/ + +@[expose] public section + +namespace Complexity + +namespace RoseTreeMachine + +/-- Rose-tree data structure, it allows us to encode most of Lean's data structures in a +"natural" manner -/ +inductive Data where + | l : List Data → Data +deriving Repr + +mutual + /-- Decidable equality for `Data`, defined jointly with `Data.listDecEq`. -/ + def Data.decEq : ∀ (a b : Data), Decidable (a = b) + | .l xs, .l ys => + match Data.listDecEq xs ys with + | isTrue h => isTrue (congrArg Data.l h) + | isFalse h => isFalse fun heq => h (Data.l.inj heq) + /-- Decidable equality for `List Data`, defined jointly with `Data.decEq`. -/ + def Data.listDecEq : ∀ (xs ys : List Data), Decidable (xs = ys) + | [], [] => isTrue rfl + | [], _ :: _ => isFalse (by simp) + | _ :: _, [] => isFalse (by simp) + | x :: xs, y :: ys => + match Data.decEq x y, Data.listDecEq xs ys with + | isTrue hxy, isTrue hxys => isTrue (congrArg₂ List.cons hxy hxys) + | isFalse hxy, _ => isFalse fun h => hxy (List.cons.inj h).1 + | _, isFalse hxys => isFalse fun h => hxys (List.cons.inj h).2 +end + +instance : DecidableEq Data := Data.decEq +instance : BEq Data := inferInstance +instance : LawfulBEq Data := inferInstance + +/-- The empty `Data` node, `Data.l []`. -/ +abbrev Data.empty := Data.l [] + + +/-- The list of children of a `Data` node. -/ +@[scoped grind =] +def Data.asList + | Data.l xs => xs + +@[scoped grind =] +lemma Data.asList_empty : Data.empty.asList = [] := by rfl + +@[simp, scoped grind =] +lemma Data.asList_l (d : Data) : Data.l d.asList = d := by simp [Data.asList]; grind + +@[simp, scoped grind =] +lemma Data.l_asList (xs : List Data) : (Data.l xs).asList = xs := by simp [Data.asList] + +/-- The encoding length of `d`, relevant for complexity. +This is the encoded size assuming an encoding into parenthesized expressions. -/ +def Data.size : Data → ℕ + | Data.l xs => 2 + (xs.map Data.size |>.sum) + +@[simp] +lemma Data.size_le {d : Data} : 0 < d.size := by + obtain ⟨xs⟩ := d + grind [Data.size] + +@[simp, scoped grind =] +lemma Data.size_empty : Data.empty.size = 2 := by simp [Data.empty, Data.size] + +@[simp, scoped grind =] +lemma Data.cons_size {h : Data} {t : List Data} : + (Data.l (h :: t)).size = h.size + (Data.l t).size := by + simp [Data.size] + grind + +/-- Recursion principle for `Data`. -/ +@[elab_as_elim] +def Data.recL {motive : Data → Sort*} + (nil : motive (Data.l [])) + (cons : ∀ (x : Data) (xs : List Data), + motive x → motive (Data.l xs) → motive (Data.l (x :: xs))) : + ∀ d, motive d + | .l [] => nil + | .l (x :: xs) => + cons x xs (Data.recL nil cons x) (Data.recL nil cons (.l xs)) + +/-- Induction principle for `Data`, the `Prop`-valued companion to `Data.recL`. -/ +@[elab_as_elim] +theorem Data.inductionL {motive : Data → Prop} + (nil : motive (Data.l [])) + (cons : ∀ (x : Data) (xs : List Data), + motive x → motive (Data.l xs) → motive (Data.l (x :: xs))) + (d : Data) : motive d := + Data.recL nil cons d + +/-- Index of a tape cell used by the rose tree machine's execution model. -/ +abbrev TapeIndex := ℕ + +end RoseTreeMachine + +end Complexity diff --git a/Complexitylib/Models/RoseTreeMachine/DataEncode.lean b/Complexitylib/Models/RoseTreeMachine/DataEncode.lean new file mode 100644 index 00000000..3d06b0f9 --- /dev/null +++ b/Complexitylib/Models/RoseTreeMachine/DataEncode.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Complexitylib.Models.RoseTreeMachine.Data +public import Mathlib.Data.Nat.Bits +public import Mathlib.Data.List.Basic + +/-! +# Encodings into `Data` + +This file defines the class that is used to encode arbitrary data structures into `Data`, +so that RTMs (rose tree machines) can operate on them. + +Instances are provided for convenience for `Data` itself, `Bool`, `List α`, `Option α`, `α × β`, +and `ℕ` (binary encoding via `List Bool`) + +-/ + +@[expose] public section + +namespace Complexity + +namespace RoseTreeMachine + +/-- Encoding of types into `Data`. -/ +class DataEncode (α : Type) where + /-- Encode a value of `α` as `Data`. -/ + encode : α → Data + /-- The encoding is injective, so distinct values never collide. -/ + h_inj : encode.Injective + +instance : DataEncode Data where + encode b := b + h_inj := by intros a b h_eq; grind + +@[simp, scoped grind =] +lemma DataEncode_encode_data (d : Data) : DataEncode.encode d = d := rfl + +instance : DataEncode Bool where + encode b := if b then Data.l [ Data.l [] ] else Data.l [] + h_inj := by intros a b h_eq; grind + +instance (α : Type) [DataEncode α] : DataEncode (List α) where + encode xs := Data.l (xs.map DataEncode.encode) + h_inj := by + intro a b h + exact List.map_injective_iff.mpr DataEncode.h_inj (Data.l.inj h) + +@[simp, scoped grind =] +lemma DataEncode_list_nil {α : Type} [DataEncode α] : + DataEncode.encode ([] : List α) = Data.l [] := by + simp [DataEncode.encode] + +@[simp, scoped grind =] +lemma DataEncode_list_eq_nil_iff_nil {α : Type} [DataEncode α] (xs : List α) : + DataEncode.encode xs = Data.empty ↔ xs = [] := by + simp [DataEncode.encode] + +@[simp, scoped grind =] +lemma DataEncode_list_tail {α : Type} [DataEncode α] (xs : List α) : + (DataEncode.encode xs).asList.tail = (DataEncode.encode xs.tail).asList := by + simp [DataEncode.encode] + +instance (α : Type) [DataEncode α] : DataEncode (Option α) where + encode := fun + | none => Data.l [] + | some x => Data.l [DataEncode.encode x] + h_inj := by + intro a b h + grind [DataEncode.h_inj] + +@[simp] +lemma DataEncode_Option_empty {α : Type} [DataEncode α] (x : Option α) : + (DataEncode.encode x == Data.empty) = x.isNone := by + cases x <;> simp [DataEncode.encode, Data.empty] + +instance (α β : Type) [DataEncode α] [DataEncode β] : DataEncode (α × β) where + encode := fun (a, b) => Data.l [DataEncode.encode a, DataEncode.encode b] + h_inj := by + intro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h + grind [DataEncode.h_inj] + +lemma DataEncode_pair {α β : Type} [DataEncode α] [DataEncode β] (a : α) (b : β) : + DataEncode.encode (a, b) = Data.l [DataEncode.encode a, DataEncode.encode b] := by + simp [DataEncode.encode] + +instance : DataEncode ℕ where + encode x := DataEncode.encode (Nat.bits x) + h_inj := by + intro a b h + have hb : a.bits = b.bits := DataEncode.h_inj h + have hrec : ∀ n : ℕ, n.bits.foldr (fun b acc => Nat.bit b acc) 0 = n := by + intro n + induction n using Nat.binaryRec' with + | zero => simp + | bit b n hn ih => rw [Nat.bits_append_bit n b hn]; simp [ih] + have := congrArg (List.foldr (fun b acc => Nat.bit b acc) 0) hb + simpa [hrec] using this + +end RoseTreeMachine + +end Complexity diff --git a/Complexitylib/Models/RoseTreeMachine/Prog.lean b/Complexitylib/Models/RoseTreeMachine/Prog.lean new file mode 100644 index 00000000..f6494672 --- /dev/null +++ b/Complexitylib/Models/RoseTreeMachine/Prog.lean @@ -0,0 +1,396 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Complexitylib.Models.RoseTreeMachine.Data +public import Complexitylib.Models.RoseTreeMachine.DataEncode + + +/-! +# Programs in a rose tree machine (RTM) + +This file contains the main definition of the rose tree machine, its programs including +semantics and time and space resource consumption. + +## Main definitions and notations + +- `Prog` - the program +- `ProgSem` - semantics and resource consumption +- `InPlace` - a fragment of the language that can be easily simulated using multi-tape Turing + machines. +- `Prog.ComputesInTimeAndSpace` - this defines the complexity notion for the RTM computation model, + based on `Data` values. +- `Prog.ComputesBoolFunInTimeAndSpace` - the complexity notion transferred to functions on binary + strings, this making it compatible to all other computation models. +- `ComputableInOTime` - generic time-complexity in the RTM model +- `ComputableInOSpace` - generic space-complexity in the RTM model +-/ + +@[expose] public section + +namespace Complexity + +namespace RoseTreeMachine + +/-- +Prog is the syntax representation of a functional language that has a resource consumption +model which is compatible to that of a Turing machine. +The data structure it operates on is a rose tree (`Data`). The advantage of this data structure +is that the majority of lean data types have a direct encoding. +-/ +inductive Prog where + /-- Variable reference at de Bruijn level `id`. -/ + | var (id : ℕ) + /-- The empty constructor of `Data`. -/ + | empty + /-- The `cons` constructor of `Data`: prepend the value of `h` to the list value of `t`. -/ + | cons (h t : Prog) + /-- Destructor of `Data`: evaluate `v`; if it is `empty`, run `emp`; otherwise destructure into + `head` and `tail` and apply the function `cs` to `head` and then to `tail`. -/ + | elim (v emp cs : Prog) + /-- Equality comparison: If `x` evaluates to the same data as `y`, run `then_`, else + run `else_`. + This can be simulated using `while_` below, but it is useful to have. -/ + | ifEq (x y then_ else_ : Prog) + /-- While loop: evaluate `init` to the starting accumulator; `body` must evaluate + to a one-argument function which is applied to the current accumulator on each + iteration. Return the accumulator if its head is empty. -/ + | while_ (init body : Prog) + /-- Abstraction / closure in one variable. -/ + | fn (body : Prog) + /-- Function application. -/ + | app (fn arg : Prog) +deriving Repr + +/-- Runtime values for the semantics predicate `ProgSem`. -/ +inductive Value where + | data (d : Data) + | closure (body : Prog) (env : List Value) +deriving Repr + +/-- The empty `Value`, wrapping the empty `Data` node. -/ +abbrev Value.empty : Value := .data (Data.l []) + +/-- Whether the program `Prog` refers to the variable at de Bruijn index `i`. -/ +def Prog.hasVar (i : ℕ) : Prog → Bool + | .var j => i = j + | .empty => false + | .cons h t => h.hasVar i || t.hasVar i + | .elim v emp cs => v.hasVar i || emp.hasVar i || cs.hasVar i + | .ifEq x y then_ else_ => + x.hasVar i || y.hasVar i || then_.hasVar i || else_.hasVar i + | .while_ init body => init.hasVar i || body.hasVar i + | .fn body => body.hasVar i + | .app f arg => f.hasVar i || arg.hasVar i + + +mutual + /-- The size of a closure's environment, restricted to variables that `body` actually + references. -/ + def closureSize (body : Prog) (env : List Value) : ℕ := + let rec go (depth : ℕ) (env : List Value) : ℕ := + match env with + | [] => 0 + | hd :: tl => go (depth + 1) tl + if body.hasVar depth then hd.size else 0 + go 0 env + + /-- The size of a `Value`. The size of data is the length of its encoding and the size + of a closure is the sum of the sizes of the referenced variables. -/ + @[simp] + def Value.size : Value → ℕ + | .data d => d.size + | .closure p env => closureSize p env +end + +-- `closureSize.go` is an internal helper generated from the `let rec` inside `closureSize`; +-- doc comments cannot be placed directly on `let rec` definitions (doing so breaks +-- elaboration), so the docBlame lint is suppressed here instead. +attribute [nolint docBlame] closureSize.go + +@[simp, scoped grind =] +lemma closureSize_of_noVar {body : Prog} {env : List Value} (h : ∀ i, ¬body.hasVar i) : + closureSize body env = 0 := by + have (depth : ℕ) : closureSize.go body depth env = 0 := by + induction env generalizing depth with + | nil => simp [closureSize.go] + | cons hd tl ih => simp [closureSize.go, h depth, ih] + simp [closureSize, this] + +@[simp, scoped grind =] +lemma closureSize_of_var {env : List Value} : + closureSize (.var i) env = (env[i]?.map fun v => v.size).getD 0 := by + unfold closureSize + have (d : ℕ) : closureSize.go (.var i) d env = + if h : d ≤ i ∧ i - d < env.length then (env[i - d]'(by grind)).size else 0 := by + induction env generalizing d with + | nil => simp [closureSize.go] + | cons hd tl ih => + grind [closureSize.go, List.length_cons, Prog.hasVar] + grind + + +@[scoped grind =] +lemma Value.size_data {d : Data} : (Value.data d).size = d.size := by simp [Value.size] + +/-- Splitting the environment of a closure size computation across an append. -/ +lemma closureSize.go_append (body : Prog) (depth : ℕ) (l1 l2 : List Value) : + closureSize.go body depth (l1 ++ l2) + = closureSize.go body depth l1 + closureSize.go body (depth + l1.length) l2 := by + induction l1 generalizing depth with + | nil => simp [closureSize.go] + | cons hd tl ih => + have he : depth + 1 + tl.length = depth + (tl.length + 1) := by omega + simp only [List.cons_append, closureSize.go, List.length_cons, ih (depth + 1), he] + omega + +/-- The closure size over an appended environment splits into the size over the prefix plus the +contribution of the suffix (counted starting at depth `l1.length`). -/ +lemma closureSize_append (body : Prog) (l1 l2 : List Value) : + closureSize body (l1 ++ l2) + = closureSize body l1 + closureSize.go body l1.length l2 := by + simp only [closureSize, closureSize.go_append, Nat.zero_add] + +/-- `closureSize.go` is monotone in the set of accessed variables. -/ +lemma closureSize.go_mono {body1 body2 : Prog} (env : List Value) + (h : ∀ i, body1.hasVar i → body2.hasVar i) (depth : ℕ) : + closureSize.go body1 depth env ≤ closureSize.go body2 depth env := by + induction env generalizing depth with + | nil => simp [closureSize.go] + | cons hd tl ih => + simp only [closureSize.go] + have hb : (if body1.hasVar depth then hd.size else 0) + ≤ (if body2.hasVar depth then hd.size else 0) := by + by_cases hv : body1.hasVar depth + · simp [hv, h depth hv] + · simp [hv] + have := ih (depth + 1) + omega + +/-- If every variable accessed by `body1` is also accessed by `body2`, then `body1` has a smaller +closure size over any environment. -/ +lemma closureSize_mono {body1 body2 : Prog} (env : List Value) + (h : ∀ i, body1.hasVar i → body2.hasVar i) : + closureSize body1 env ≤ closureSize body2 env := by + have := closureSize.go_mono env h 0 + simpa only [closureSize] using this + +/-- The closure size is bounded by the total size of the environment. -/ +lemma closureSize.go_le_sum (body : Prog) (depth : ℕ) (env : List Value) : + closureSize.go body depth env ≤ (env.map Value.size).sum := by + induction env generalizing depth with + | nil => simp [closureSize.go] + | cons hd tl ih => + simp only [closureSize.go, List.map_cons, List.sum_cons] + have h1 := ih (depth + 1) + have h2 : (if body.hasVar depth then hd.size else 0) ≤ hd.size := by + by_cases hv : body.hasVar depth <;> simp [hv] + omega + +mutual +/-- Semantics of `Prog` including time and space resource bounds. +`ProgSem σ p x t s` means that on environment `σ`, the program `p` evaluates to the value +`x` and uses `t` time and `s` space. -/ +inductive ProgSem : (List Value) → Prog → Value → ℕ → ℕ → Prop + | var : + ProgSem σ (.var i) (σ[i]?.getD Value.empty) + (σ[i]?.getD Value.empty).size (σ[i]?.getD Value.empty).size + | empty : ProgSem σ .empty Value.empty 2 2 + | cons (h₁ : ProgSem σ head (.data hd) hd_t hd_s) (h₂ : ProgSem σ tail (.data tl) tl_t tl_s) : + ProgSem σ (.cons head tail) (.data (Data.l (hd :: tl.asList))) (hd_t + tl_t) (hd_s + tl_s) + /-- `elim`, empty branch: `v` is the empty list, so run `emp` in the current environment. -/ + | elim_nil + (h₁ : ProgSem σ val (.data (Data.l [])) t_v s_v) + (h₂ : ProgSem σ emp r t_emp s_emp) : + ProgSem σ (.elim val emp cs) r (t_v + t_emp) (s_v + s_emp) + /-- `elim`, cons branch: `v` destructures to `hd :: tl`; evaluate the function `cs` to a + closure and apply it first to `hd` and then to `tl` (so `cs` is a curried + two-argument function). -/ + | elim_cons + (h_v : ProgSem σ val (.data (Data.l (hd :: tl))) t_v s_v) + (h_cs : ProgSem σ cs cv t_cs s_cs) + (h_app₁ : AppSem cv (.data hd) cv' t₁ s₁) + (h_app₂ : AppSem cv' (.data (Data.l tl)) r t₂ s₂) : + ProgSem σ (.elim val emp cs) r (t_v + t_cs + t₁ + t₂) (s_v + s_cs + s₁ + s₂) + | ifEq_then + (h_x : ProgSem σ x (.data vx) t_x s_x) + (h_y : ProgSem σ y (.data vx) t_y s_y) + (h_then : ProgSem σ then_ r t_then s_then) : + ProgSem σ (.ifEq x y then_ else_) r (t_x + t_y + t_then) (s_x + s_y + s_then) + | ifEq_else + (h_x : ProgSem σ x (.data vx) t_x s_x) + (h_y : ProgSem σ y (.data vy) t_y s_y) + (h_neq : vx ≠ vy) + (h_else : ProgSem σ else_ r t_else s_else) : + ProgSem σ (.ifEq x y then_ else_) r (t_x + t_y + t_else) (s_x + s_y + s_else) + /-- `while_ init body`: evaluate `init` to the starting accumulator and `body` to a + one-argument closure, then iterate the closure via `WhileSem` until it halts. -/ + | while_ + (h_init : ProgSem σ init (.data acc) t_init s_init) + (h_body : ProgSem σ body bodyVal t_body s_body) + (h_while : WhileSem bodyVal acc r t_w s_w) : + ProgSem σ (.while_ init body) (.data r) (t_init + t_body + t_w) (s_init + s_body + s_w) + /-- `fn body`: evaluate to a closure capturing the current environment `σ`. The cost is the + size of the resulting closure (mirroring `var`, which charges the size of the value it + produces). -/ + | fn : ProgSem σ (.fn body) (.closure body σ) + (Value.closure body σ).size (Value.closure body σ).size + /-- `app fn arg`: evaluate `fn` to a closure, evaluate `arg` to a value, then run the + closure's body in the *captured* environment extended with the argument (static + scoping). -/ + | app + (h_fn : ProgSem σ fn fv t_f s_f) + (h_arg : ProgSem σ arg v t_a s_a) + (h_app : AppSem fv v r t_b s_b) : + ProgSem σ (.app fn arg) r (t_f + t_a + t_b) (s_f + s_a + s_b) + +/-- Application of a value to an argument value. `AppSem f v r t s` means that applying the +closure `f` to the argument `v` yields `r` using `t` time and `s` space. Only closures can be +applied; applying a first-order value has no derivation (the program is stuck). -/ +inductive AppSem : Value → Value → Value → ℕ → ℕ → Prop + | mk (h_body : ProgSem (σ ++ [v]) body r t s) : + AppSem (.closure body σ) v r t s + +/-- Iterates the closure `bodyVal` of a `while_` loop, threading the accumulator. +`WhileSem bodyVal acc r t s` means that, starting from accumulator `acc`, repeatedly applying +`bodyVal` to the current accumulator eventually yields result `r` using `t` time and `s` space. +Before each iteration the halting condition is checked on the current accumulator: iteration +terminates (with the accumulator as result) when `acc` is empty or its head is empty. +Otherwise `bodyVal` is applied and its result becomes the new accumulator. Non-terminating +loops simply have no derivation. -/ +inductive WhileSem : Value → Data → Data → ℕ → ℕ → Prop + | halt + (h_stop : acc.asList.head?.getD (Data.l []) = Data.l []) : + WhileSem bodyVal acc acc acc.size acc.size + | step + (h_cont : acc.asList.head?.getD (Data.l []) ≠ Data.l []) + (h_app : AppSem bodyVal (.data acc) (.data v) t_b s_b) + (h_rest : WhileSem bodyVal v r t_r s_r) : + WhileSem bodyVal acc r (t_b + t_r) (max s_b s_r) +end + +/-- Producing a value costs at least its size, in both time and space. This holds because every +`ProgSem` derivation either reads/builds the value directly (charging its size) or returns a +value produced by a sub-derivation whose cost it includes. Provable by mutual induction over +`ProgSem`/`AppSem`/`WhileSem`. -/ +lemma ProgSem.size_le {σ : List Value} {p : Prog} {v : Value} {t s : ℕ} + (h : ProgSem σ p v t s) : v.size ≤ t ∧ v.size ≤ s := by + induction h using ProgSem.rec + (motive_2 := fun _ _ r t s _ => r.size ≤ t ∧ r.size ≤ s) + (motive_3 := fun _ _ r t s _ => (Value.data r).size ≤ t ∧ (Value.data r).size ≤ s) with + | empty => exact ⟨by simp, by simp⟩ + | var | cons | elim_nil | elim_cons | ifEq_then | ifEq_else + | while_ | fn | app | mk | halt | step + => grind [Value.size_data, Data.cons_size, Data.asList_l] + +/-- Value-determinism of the relational semantics: a program evaluates to at most one value in a +given environment. The mutually-defined `AppSem`/`WhileSem` relations are value-deterministic too. +The potential branch overlaps (`elim_nil`/`elim_cons`, `ifEq_then`/`ifEq_else`) are ruled out by +value-determinism of the scrutinee / compared values, supplied by the induction hypotheses. -/ +theorem ProgSem.value_det {σ : List Value} {p : Prog} {v₁ : Value} {t₁ s₁ : ℕ} + (h₁ : ProgSem σ p v₁ t₁ s₁) : + ∀ (v₂ : Value) (t₂ s₂ : ℕ), ProgSem σ p v₂ t₂ s₂ → v₁ = v₂ := by + induction h₁ using ProgSem.rec + (motive_2 := fun f a r₁ _ _ _ => + ∀ (r₂ : Value) (t₂ s₂ : ℕ), AppSem f a r₂ t₂ s₂ → r₁ = r₂) + (motive_3 := fun b acc r₁ _ _ _ => + ∀ (r₂ : Data) (t₂ s₂ : ℕ), WhileSem b acc r₂ t₂ s₂ → r₁ = r₂) with + | var | empty | fn => rintro _ _ _ h₂; cases h₂; rfl + | cons _ _ ih₁ ih₂ => + rintro _ _ _ h₂; cases h₂ with + | cons h₁' h₂' => have := ih₁ _ _ _ h₁'; have := ih₂ _ _ _ h₂'; grind + | elim_nil _ _ ih_v _ => + rintro _ _ _ h₂; cases h₂ with + | elim_nil h_v' _ => grind + | elim_cons h_v' _ _ _ => have := ih_v _ _ _ h_v'; grind + | elim_cons _ _ _ _ ih_v ih_cs ih₁ ih₂ => + rintro _ _ _ h₂; cases h₂ with + | elim_nil h_v' _ => have := ih_v _ _ _ h_v'; grind + | elim_cons h_v' h_cs' h_a₁' h_a₂' => + have := ih_v _ _ _ h_v'; have := ih_cs _ _ _ h_cs' + grind + | ifEq_then _ _ _ ih_x ih_y ih_then => + rintro _ _ _ h₂; cases h₂ with + | ifEq_then h_x' _ h_then' => have := ih_then _ _ _ h_then'; grind + | ifEq_else h_x' h_y' h_neq _ => + have := ih_x _ _ _ h_x'; have := ih_y _ _ _ h_y'; grind + | ifEq_else _ _ _ _ ih_x ih_y ih_else => + rintro _ _ _ h₂; cases h₂ with + | ifEq_then h_x' h_y' _ => have := ih_x _ _ _ h_x'; have := ih_y _ _ _ h_y'; grind + | ifEq_else _ _ _ h_else' => have := ih_else _ _ _ h_else'; grind + | while_ _ _ _ ih_init ih_body ih_while => + rintro _ _ _ h₂; cases h₂ with + | while_ h_init' h_body' h_while' => + have := ih_init _ _ _ h_init'; have := ih_body _ _ _ h_body'; grind + | app _ _ _ ih_fn ih_arg ih_app => + rintro _ _ _ h₂; cases h₂ with + | app h_fn' h_arg' h_app' => + have := ih_fn _ _ _ h_fn'; have := ih_arg _ _ _ h_arg'; grind + | mk _ ih_body => + rename_i h₂; cases h₂ with + | mk h_body' => exact ih_body _ _ _ h_body' + | halt _ + | step _ _ _ ih_app ih_rest => + rename_i h₂; cases h₂ with + | halt h_stop => grind + | step _ h_app' h_rest' => grind + +/-- The program `p` computes the value `y` from the value `x` in time `t` and space `s`. -/ +def Prog.ComputesInTimeAndSpace (p : Prog) (x y : Data) (t : ℕ) (s : ℕ) : Prop := + ProgSem [.data x] p (.data y) t s + + +/-- The program `p` computes the function `f` (on binary strings) in time `t` and space `s`. +This is the main definition that defines complexity for this computation model. -/ +def Prog.ComputesBoolFunInTimeAndSpace + (p : Prog) (f : List Bool → List Bool) (t : ℕ → ℕ) (s : ℕ → ℕ) : Prop := + ∀ x, ∃ t' ≤ t x.length, ∃ s' ≤ s x.length, + Prog.ComputesInTimeAndSpace p (DataEncode.encode x) (DataEncode.encode (f x)) t' s' + +/-- The function `f` is computable in time `t` in the RTM model, up to constant factors -/ +def ComputableInOTime (f : List Bool → List Bool) (t : ℕ → ℕ) : Prop := + ∃ p a s, Prog.ComputesBoolFunInTimeAndSpace p f (fun n => a * (t n) + a) s + +/-- The function `f` is computable in space `s` in the RTM model, up to constant factors -/ +def ComputableInOSpace (f : List Bool → List Bool) (s : ℕ → ℕ) : Prop := + ∃ p a t, Prog.ComputesBoolFunInTimeAndSpace p f t (fun n => a * (s n) + a) + +/-- The *in-place* (first-order) fragment of the functional language. + +`InPlace p` holds when every `fn` in `p` occurs in an immediately-consumed position — as the +operator of an `app`, or as the (curried) branch of an `elim`/`while_`. Consequently no +closure ever escapes: every abstraction is created and used on the spot, so all values that +flow through the environment are first-order `Data`. This is exactly the fragment a +defunctionalising compiler targets, and it is closed under the operational semantics. + +A Turing machine can directly implement this fragment without the need for closures: +One tape is used for each "node" in the syntax tree. +-/ +inductive InPlace : Prog → Prop + | var : InPlace (.var i) + | empty : InPlace .empty + | cons (hh : InPlace h) (ht : InPlace t) : InPlace (.cons h t) + /-- `elim` over an in-place value, empty branch, and a curried two-argument function + branch `fn (fn body)` binding `head` and `tail`. -/ + | elim (hv : InPlace v) (hemp : InPlace emp) (hbody : InPlace body) : + InPlace (.elim v emp (.fn (.fn body))) + | ifEq (hx : InPlace x) (hy : InPlace y) (hthen : InPlace then_) (helse : InPlace else_) : + InPlace (.ifEq x y then_ else_) + /-- `while_` whose body is a literal one-argument function `fn body` binding the + accumulator. -/ + | while_ (hinit : InPlace init) (hbody : InPlace body) : + InPlace (.while_ init (.fn body)) + /-- `app` whose operator is a literal one-argument function `fn body`: this is a `let`, + binding the value of `arg` and running `body` on the spot. The abstraction is consumed + immediately, so no closure escapes. Nested applications of this form give multi-argument + `let`-chains; arbitrary arities follow by repeated use of this constructor. -/ + | app (hbody : InPlace body) (harg : InPlace arg) : + InPlace (.app (.fn body) arg) + + +end RoseTreeMachine + +end Complexity From 293e1bde83884e84d13a33f54f5b0ff67ade3cf1 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 19 Jul 2026 15:25:21 +0000 Subject: [PATCH 02/16] feat(Models): compile in-place RTM programs to Turing machines Add `Complexitylib.Models.RoseTreeMachine.Compile`, the first verified slice of the InPlace rose tree machine to Turing machine compiler. It relates the RTM `ProgSem` cost model to Turing-machine time and space up to a constant factor (the notion the RTM's own `ComputableInOTime`/`ComputableInOSpace` already use). Provides: - `InPlaceRealizedByTM`, the per-program correspondence predicate: same binary function, with TM time/space bounds dominated by the program's RTM bounds. - `dataSize_encode_listBool`, the reusable bridge showing the binary encoding of a `List Bool` has `Data.size` linear in the list length. - `emptyOutputTM` plus its time and space correctness, and `empty_realized`: the `empty` program is realized with matching time and space. - `identity_time_matches`: the `var 0` program and `copyInputToOutputTM` both compute the identity, with matching linear time. The inductive constructors remain tracked as future work in ROADMAP.md. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- Complexitylib/Models.lean | 1 + .../Models/RoseTreeMachine/Compile.lean | 228 ++++++++++++++++++ ROADMAP.md | 10 + 3 files changed, 239 insertions(+) create mode 100644 Complexitylib/Models/RoseTreeMachine/Compile.lean diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean index 65814c56..b725c85d 100644 --- a/Complexitylib/Models.lean +++ b/Complexitylib/Models.lean @@ -59,6 +59,7 @@ import Complexitylib.Models.RandomAccessMachine import Complexitylib.Models.RoseTreeMachine.Data import Complexitylib.Models.RoseTreeMachine.DataEncode import Complexitylib.Models.RoseTreeMachine.Prog +import Complexitylib.Models.RoseTreeMachine.Compile /-! # Computation models diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean new file mode 100644 index 00000000..06d0fe32 --- /dev/null +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -0,0 +1,228 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexitylib.Models.RoseTreeMachine.Prog +import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput + +/-! +# Compiling in-place rose tree machine programs to Turing machines + +This file constructs equivalent Turing machines for programs in the first-order +(`InPlace`) fragment of the rose tree machine (RTM) and relates their resource +consumption to the RTM `ProgSem` cost model. + +## What "match" means here + +The RTM cost model is faithful to Turing machines only *up to a constant +factor* — this is the same notion the RTM's own `ComputableInOTime` / +`ComputableInOSpace` already use, and it is the standard notion for +cross-model simulation. Concretely, a compiled machine computes the *same* +binary function as the source program and its time (resp. space) bound is +*dominated by* the program's RTM time (resp. space) bound. + +Two structural facts make this achievable for the `InPlace` fragment: + +- **Result materialization is already paid for.** `ProgSem.size_le` shows every + derivation charges at least the size of the value it produces, in both time + and space. So the O(size) traversal/assembly/copy work a Turing machine must + perform to build a `Data` result is always absorbed (up to a constant) by the + sub-costs the RTM already charges. +- **Space is charged generously.** Most `ProgSem` rules *add* the space of + sequential sub-computations (`s₁ + s₂ + …`) where a Turing machine reuses + space and pays only their `max`. The RTM figure is therefore a valid upper + bound for the machine's actual space. (`WhileSem` already uses `max`, matching + the loop's space reuse exactly.) + +## Main definitions + +- `RoseTreeMachine.InPlaceRealizedByTM` — the correspondence predicate: an + `InPlace` program computing a binary function `f` is realized by some Turing + machine that computes `f` with time and space bounds dominated by the + program's RTM bounds. +- `RoseTreeMachine.emptyOutputTM` — the one-state machine that halts immediately + with empty output. + +## Main results + +- `RoseTreeMachine.dataSize_encode_bool`, `dataSize_encode_listBool` — the binary + encoding of a `List Bool` has `Data.size` linear in the list length; the + reusable bridge between input length and RTM cost. +- `RoseTreeMachine.emptyOutputTM_computesInTime` / + `emptyOutputTM_computesInSpace` — the trivial machine computes `fun _ => []` + in zero time and zero auxiliary space. +- `RoseTreeMachine.empty_realized` — the `InPlace` program `empty` is realized by + a Turing machine with matching time *and* space. +- `RoseTreeMachine.identity_time_matches` — the `InPlace` program `var 0` and the + input-to-output copy machine both compute the identity, with the machine's + exact time bound `n + 2` dominated by the program's RTM bound `4·n + 2`. + +## Scope + +This is the first verified slice of the `InPlace`-RTM → TM compiler. The +inductive constructors (`cons`, `elim`, `ifEq`, `while_`, and the immediately +consumed `app`/`fn` let-binding) require concrete data-manipulation +subroutines over the `Data` encoding and are tracked as future work in +`ROADMAP.md` (track N0). The framework here — the `InPlaceRealizedByTM` +predicate, the encoding-size bridge, and the two proven base cases — fixes the +interface those constructors will compose through. +-/ + +namespace Complexity + +namespace RoseTreeMachine + +open Complexity.TM + +-- ════════════════════════════════════════════════════════════════════════ +-- Encoding-size bridge: `Data.size` of a binary encoding is linear +-- ════════════════════════════════════════════════════════════════════════ + +/-- Each `Bool` encodes to a `Data` value of size at most `4` (`false ↦ 2`, +`true ↦ 4`). -/ +lemma dataSize_encode_bool (b : Bool) : Data.size (DataEncode.encode b) ≤ 4 := by + cases b <;> simp [DataEncode.encode] + +/-- The binary encoding of a `List Bool` has `Data.size` bounded linearly by the +list length: `Data.size (encode x) ≤ 4·|x| + 2`. This is the bridge between a +Turing machine's input length `n` and the RTM cost of manipulating `encode x`. -/ +lemma dataSize_encode_listBool (x : List Bool) : + Data.size (DataEncode.encode x) ≤ 4 * x.length + 2 := by + induction x with + | nil => simp [DataEncode.encode] + | cons b bs ih => + have hrw : DataEncode.encode (b :: bs) + = Data.l (DataEncode.encode b :: bs.map DataEncode.encode) := by + simp [DataEncode.encode] + have hbs : Data.l (bs.map DataEncode.encode) = DataEncode.encode bs := by + simp [DataEncode.encode] + rw [hrw, Data.cons_size, hbs] + have hb := dataSize_encode_bool b + simp only [List.length_cons] + omega + +-- ════════════════════════════════════════════════════════════════════════ +-- A halted configuration only reaches itself +-- ════════════════════════════════════════════════════════════════════════ + +/-- A configuration whose state is the halt state has no successors, so the only +configuration it reaches is itself. -/ +private theorem reaches_eq_of_halted {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} + (hh : c.state = tm.qhalt) (h : tm.reaches c c') : c' = c := by + rcases Relation.ReflTransGen.cases_head h with heq | ⟨d, hstep, _⟩ + · exact heq.symm + · exact absurd hstep (by + have hnone : tm.step c = none := step_eq_none_iff_halted.mpr hh + simp [TM.stepRel, hnone]) + +-- ════════════════════════════════════════════════════════════════════════ +-- The trivial machine: halt immediately with empty output +-- ════════════════════════════════════════════════════════════════════════ + +/-- The one-state Turing machine that is halted from the start. Its output tape +is the initial (empty) tape, so it computes the constant empty-string function +in zero steps and zero auxiliary space. All transition directions are `right`, +satisfying `δ_right_of_start` and the transducer discipline vacuously (the +machine never steps). -/ +def emptyOutputTM (n : ℕ) : TM n where + Q := Unit + qstart := () + qhalt := () + δ := fun _ _ _ _ => ((), fun _ => Γw.blank, Γw.blank, .right, fun _ => .right, .right) + δ_right_of_start := by + intro q iHead wHeads oHead + exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ + +/-- The initial (empty) output tape holds the empty output string. -/ +private theorem hasOutput_init_nil : (Tape.init []).HasOutput ([] : List Bool) := by + refine ⟨fun i h => absurd h (by simp), ?_⟩ + exact Tape.init_nil_cells_succ 0 + +/-- `emptyOutputTM` computes the constant empty-string function in zero time. -/ +theorem emptyOutputTM_computesInTime (n : ℕ) : + (emptyOutputTM n).ComputesInTime (fun _ => []) (fun _ => 0) := by + intro x + refine ⟨(emptyOutputTM n).initCfg x, 0, le_refl _, reachesIn.zero, rfl, ?_⟩ + exact hasOutput_init_nil + +/-- `emptyOutputTM` computes the constant empty-string function in zero auxiliary +space: it is a transducer, every reachable configuration is the (halted) initial +one, and that configuration trivially respects the space bound. -/ +theorem emptyOutputTM_computesInSpace (n : ℕ) : + (emptyOutputTM n).ComputesInSpace (fun _ => []) (fun _ => 0) := by + refine ⟨?_, ?_, ?_⟩ + · intro q iHead wHeads oHead + simp [emptyOutputTM] + · intro x c' hreach + have hc' : c' = (emptyOutputTM n).initCfg x := reaches_eq_of_halted rfl hreach + subst hc' + refine ⟨fun i => ?_, ?_⟩ + · simp + · simp + · intro x + exact ⟨(emptyOutputTM n).initCfg x, Relation.ReflTransGen.refl, rfl, hasOutput_init_nil⟩ + +-- ════════════════════════════════════════════════════════════════════════ +-- The correspondence predicate and the proven base cases +-- ════════════════════════════════════════════════════════════════════════ + +/-- An `InPlace` rose tree machine program `p` computing the binary function `f` +is *realized by a Turing machine* when some machine computes the same `f` with +time and space bounds dominated by `p`'s RTM `ProgSem` bounds. This is the +compiler's per-program correctness-and-resource contract. -/ +def InPlaceRealizedByTM (p : Prog) (f : List Bool → List Bool) : Prop := + InPlace p ∧ + ∃ tR sR : ℕ → ℕ, p.ComputesBoolFunInTimeAndSpace f tR sR ∧ + ∃ (k : ℕ) (M : TM k) (tT sT : ℕ → ℕ), + M.ComputesInTime f tT ∧ M.ComputesInSpace f sT ∧ + (∀ n, tT n ≤ tR n) ∧ (∀ n, sT n ≤ sR n) + +/-- **The `empty` program is realized by a Turing machine with matching time and +space.** The `InPlace` program `empty` computes the constant empty-string +function in RTM time and space `2`, and `emptyOutputTM` computes the same +function in `0` time and `0` auxiliary space, both dominated by `2`. -/ +theorem empty_realized : InPlaceRealizedByTM Prog.empty (fun _ => []) := by + refine ⟨InPlace.empty, (fun _ => 2), (fun _ => 2), ?_, 0, emptyOutputTM 0, + (fun _ => 0), (fun _ => 0), emptyOutputTM_computesInTime 0, + emptyOutputTM_computesInSpace 0, fun _ => by dsimp only; omega, + fun _ => by dsimp only; omega⟩ + intro x + refine ⟨2, le_refl _, 2, le_refl _, ?_⟩ + show ProgSem [Value.data (DataEncode.encode x)] Prog.empty + (Value.data (DataEncode.encode ([] : List Bool))) 2 2 + rw [DataEncode_list_nil] + exact ProgSem.empty + +/-- The `InPlace` program `var 0` computes the identity binary function in RTM +time and space `4·n + 2` (the `Data.size` of the encoded input, bounded via +`dataSize_encode_listBool`). -/ +theorem var0_computesBoolFun_id : + (Prog.var 0).ComputesBoolFunInTimeAndSpace id + (fun n => 4 * n + 2) (fun n => 4 * n + 2) := by + intro x + refine ⟨Data.size (DataEncode.encode x), dataSize_encode_listBool x, + Data.size (DataEncode.encode x), dataSize_encode_listBool x, ?_⟩ + show ProgSem [Value.data (DataEncode.encode x)] (Prog.var 0) + (Value.data (DataEncode.encode (id x))) _ _ + have h : ProgSem [Value.data (DataEncode.encode x)] (Prog.var 0) _ _ _ := ProgSem.var + simpa using h + +/-- **The `var 0` program and the copy machine both compute the identity, with +matching (linear) time.** The `InPlace` program `var 0` computes the identity in +RTM time `4·n + 2`, and `copyInputToOutputTM` computes the identity in the exact +time bound `n + 2 ≤ 4·n + 2`. (The copy machine also uses only its fixed, +here empty, work-tape bank; a formal `ComputesInSpace` certificate is tracked +with the remaining constructors.) -/ +theorem identity_time_matches : + InPlace (Prog.var 0) ∧ + (Prog.var 0).ComputesBoolFunInTimeAndSpace id (fun n => 4 * n + 2) + (fun n => 4 * n + 2) ∧ + ∃ (k : ℕ) (M : TM k) (T : ℕ → ℕ), + M.ComputesInTime id T ∧ ∀ n, T n ≤ 4 * n + 2 := + ⟨InPlace.var, var0_computesBoolFun_id, 0, copyInputToOutputTM (n := 0), + (fun m => m + 2), copyInputToOutputTM_computesInTime 0, fun n => by dsimp only; omega⟩ + +end RoseTreeMachine + +end Complexity diff --git a/ROADMAP.md b/ROADMAP.md index 214fa757..b4c96158 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -153,6 +153,16 @@ another controller-local proof. deferred and optional, not implemented. It is not a dependency of the named-tape/effect work; revisit only when a real construction needs recursive Data-valued syntax and the bounded slice can meet all promotion gates. + - [ ] Compile the `InPlace` (first-order) RTM fragment to Turing machines with + resource consumption matching the `ProgSem` cost model up to a constant + factor. `Complexitylib.Models.RoseTreeMachine.Compile` lands the first + verified slice: the `InPlaceRealizedByTM` correspondence predicate, the + linear `Data`-encoding-size bridge (`dataSize_encode_listBool`), and two + proven base cases — `empty` (matching time *and* space via `emptyOutputTM`) + and `var 0`/identity (matching time via `copyInputToOutputTM`). The inductive + constructors (`cons`, `elim`, `ifEq`, `while_`, and the immediately consumed + `app`/`fn` let-binding) need concrete `Data`-manipulation subroutines and + remain to be composed through the same interface. - [x] Audit proof-engineering mechanics across representative machine and circuit constructions: inventory repeated state/tape/wire bookkeeping, run or trace stitching, semantic transport, and resource accounting, then prototype the From 1453ce754b9fa84c3a91227606921de69e0b6db8 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 19 Jul 2026 17:05:07 +0000 Subject: [PATCH 03/16] feat(Models): state full InPlace RTM to TM compiler theorem Add `inPlace_compilesToTM`: for every InPlace rose tree machine program `p` there is a single Turing machine `M` (with constants `a`, `b` depending only on `p`) that, whenever `p` computes a binary function `f` within RTM time `tR`/space `sR`, computes the same `f` within TM time `a*tR+a` and auxiliary space `b*sR+b`. The `ComputesInTime`/`ComputesInSpace` certificates make `M` usable as a subroutine (e.g. via `seqTM`/`compositionTM`). The statement is provided now to fix the subroutine interface; the proof is a `sorry` pending the inductive constructors' data-manipulation subroutines (tracked in ROADMAP.md). Note: this makes `lake build --wfail` and the axiom guard report the declaration until the proof lands. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 57 +++++++++++++++++-- 1 file changed, 52 insertions(+), 5 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index 06d0fe32..30344bc6 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -46,6 +46,10 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Main results +- `RoseTreeMachine.inPlace_compilesToTM` — **the full compiler theorem** (stated + now; proof deferred, see *Scope*): every `InPlace` program compiles to a single + Turing machine, usable as a subroutine, whose time and space are within a + constant factor of the program's RTM bounds. - `RoseTreeMachine.dataSize_encode_bool`, `dataSize_encode_listBool` — the binary encoding of a `List Bool` has `Data.size` linear in the list length; the reusable bridge between input length and RTM cost. @@ -61,12 +65,18 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Scope This is the first verified slice of the `InPlace`-RTM → TM compiler. The -inductive constructors (`cons`, `elim`, `ifEq`, `while_`, and the immediately -consumed `app`/`fn` let-binding) require concrete data-manipulation +headline `inPlace_compilesToTM` is stated but its proof is currently `sorry`: +the inductive constructors (`cons`, `elim`, `ifEq`, `while_`, and the +immediately consumed `app`/`fn` let-binding) require concrete data-manipulation subroutines over the `Data` encoding and are tracked as future work in -`ROADMAP.md` (track N0). The framework here — the `InPlaceRealizedByTM` -predicate, the encoding-size bridge, and the two proven base cases — fixes the -interface those constructors will compose through. +`ROADMAP.md` (track N0). The base cases are already proven (`empty_realized`, +`identity_time_matches`). The framework here — the `InPlaceRealizedByTM` +predicate, the encoding-size bridge, the two proven base cases, and the fixed +statement of `inPlace_compilesToTM` — pins down the interface those constructors +will compose through. + +> Note: `inPlace_compilesToTM` uses `sorry`, so `lake build --wfail` and the +> axiom guard will report it until the proof is supplied. -/ namespace Complexity @@ -223,6 +233,43 @@ theorem identity_time_matches : ⟨InPlace.var, var0_computesBoolFun_id, 0, copyInputToOutputTM (n := 0), (fun m => m + 2), copyInputToOutputTM_computesInTime 0, fun n => by dsimp only; omega⟩ +-- ════════════════════════════════════════════════════════════════════════ +-- The full compiler theorem (statement; proof is tracked future work) +-- ════════════════════════════════════════════════════════════════════════ + +/-- **The full in-place RTM → Turing-machine compiler theorem.** + +For every first-order (`InPlace`) rose tree machine program `p`, there is a +Turing machine `M` and constants `a`, `b` such that, whenever `p` computes a +binary function `f` within RTM time `tR` and space `sR`, the *single* machine +`M` computes the same `f` within Turing-machine time `a·tR + a` and auxiliary +space `b·sR + b`. + +The machine `M` and constants `a`, `b` depend only on `p` (they are produced by +compiling `p`), not on the function `f` being analyzed; by value-determinism of +`ProgSem` there is at most one such `f`. The constants capture the "match up to +a constant factor" convention documented at the top of this file. + +Because `M` carries ordinary `ComputesInTime` / `ComputesInSpace` certificates, +it is directly usable as a **subroutine** — for instance composed with other +machines through `TM.seqTM` or `TM.compositionTM`. + +The proof compiles `p` by structural recursion on the `InPlace` derivation, +implementing each constructor with `Data`-manipulation subroutines over the +binary encoding and accumulating the resource bounds compositionally. The base +cases `empty` and `var 0` are already discharged by `empty_realized` and +`identity_time_matches`; the inductive constructors (`cons`, `elim`, `ifEq`, +`while_`, and the immediately consumed `app`/`fn` let-binding) remain to be +built (tracked in `ROADMAP.md`, track N0). The statement is provided now so the +subroutine interface is fixed; the proof is deferred. -/ +theorem inPlace_compilesToTM (p : Prog) (hp : InPlace p) : + ∃ (k : ℕ) (M : TM k) (a b : ℕ), + ∀ (f : List Bool → List Bool) (tR sR : ℕ → ℕ), + p.ComputesBoolFunInTimeAndSpace f tR sR → + M.ComputesInTime f (fun n => a * tR n + a) ∧ + M.ComputesInSpace f (fun n => b * sR n + b) := by + sorry + end RoseTreeMachine end Complexity From 54276272b755e851fd4d654c6b6786a052465c74 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 19 Jul 2026 17:25:21 +0000 Subject: [PATCH 04/16] feat(Models): add layout-relative multi-tape compiler interface for RTM Introduce the internal, layout-relative compiler contract so an InPlace program's multiple arguments map to distinct Turing-machine work tapes, while keeping the public inPlace_compilesToTM theorem on the standard single-input / single-output subroutine interface. - Data.toBits / toBitsList: balanced-parenthesis serialization of a Data value to List Bool, with Data.toBits_length : length = Data.size (bridges RTM Data.size space to physical tape cells). - LoadedStart: multi-tape analogue of Cfg.init placing argument j on work tape slot j via Data.toBits. - CompilesUnder M slot res p a b: the layout-relative correctness-and-resource contract the InPlace recursion is proved against (time a*t+a, work-head space b*s+b). - compilesUnder_of_inPlace: internal recursion statement (sorry); the public inPlace_compilesToTM is its m=1 wrapper (prologue unpacks input tape onto the argument tape, epilogue copies the result tape to output; renumbering via the existing Lift/RetargetCompute/Placement combinators). Both headline statements remain sorry, so lake build --wfail and the axiom guard report them until proved. Style lint, full build, and env linter pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 121 +++++++++++++++--- .../Models/RoseTreeMachine/Data.lean | 34 +++++ ROADMAP.md | 20 ++- 3 files changed, 152 insertions(+), 23 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index 30344bc6..bfb25c50 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -37,19 +37,32 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Main definitions -- `RoseTreeMachine.InPlaceRealizedByTM` — the correspondence predicate: an - `InPlace` program computing a binary function `f` is realized by some Turing - machine that computes `f` with time and space bounds dominated by the - program's RTM bounds. +- `RoseTreeMachine.CompilesUnder` — the internal, **layout-relative** compiler + contract: a machine implements a program for an environment layout that places + one program argument per work tape (`slot : Fin m → Fin k`) and deposits the + result on a chosen tape, with time/space matched to the RTM `ProgSem` bounds. + This is where "multiple inputs map to tapes" lives. +- `RoseTreeMachine.LoadedStart` — the multi-tape analogue of `Cfg.init`: the + starting configuration for `CompilesUnder`, with each argument serialized onto + its designated tape via `Data.toBits`. +- `RoseTreeMachine.InPlaceRealizedByTM` — the (single-input) correspondence + predicate: an `InPlace` program computing a binary function `f` is realized by + some Turing machine that computes `f` with time and space bounds dominated by + the program's RTM bounds. - `RoseTreeMachine.emptyOutputTM` — the one-state machine that halts immediately with empty output. ## Main results -- `RoseTreeMachine.inPlace_compilesToTM` — **the full compiler theorem** (stated - now; proof deferred, see *Scope*): every `InPlace` program compiles to a single - Turing machine, usable as a subroutine, whose time and space are within a - constant factor of the program's RTM bounds. +- `RoseTreeMachine.inPlace_compilesToTM` — **the full public compiler theorem** + (stated now; proof deferred, see *Scope*): every `InPlace` program compiles to + a single Turing machine, usable as a subroutine, whose time and space are + within a constant factor of the program's RTM bounds. +- `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion** + (statement only): every `InPlace` program compiles, for a fixed argument + arity, to a machine plus a tape layout satisfying `CompilesUnder`. This is the + theorem proved by structural recursion; `inPlace_compilesToTM` is its + single-argument wrapper. - `RoseTreeMachine.dataSize_encode_bool`, `dataSize_encode_listBool` — the binary encoding of a `List Bool` has `Data.size` linear in the list length; the reusable bridge between input length and RTM cost. @@ -65,18 +78,21 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Scope This is the first verified slice of the `InPlace`-RTM → TM compiler. The -headline `inPlace_compilesToTM` is stated but its proof is currently `sorry`: +headline `inPlace_compilesToTM` and the internal recursion +`compilesUnder_of_inPlace` are stated but their proofs are currently `sorry`: the inductive constructors (`cons`, `elim`, `ifEq`, `while_`, and the immediately consumed `app`/`fn` let-binding) require concrete data-manipulation subroutines over the `Data` encoding and are tracked as future work in `ROADMAP.md` (track N0). The base cases are already proven (`empty_realized`, -`identity_time_matches`). The framework here — the `InPlaceRealizedByTM` -predicate, the encoding-size bridge, the two proven base cases, and the fixed -statement of `inPlace_compilesToTM` — pins down the interface those constructors -will compose through. - -> Note: `inPlace_compilesToTM` uses `sorry`, so `lake build --wfail` and the -> axiom guard will report it until the proof is supplied. +`identity_time_matches`). The framework here — the `CompilesUnder` / +`LoadedStart` layout-relative interface, the `InPlaceRealizedByTM` predicate, +the `Data.toBits` tape serialization, the encoding-size bridge, the two proven +base cases, and the fixed statements of both theorems — pins down the interface +those constructors will compose through. + +> Note: `compilesUnder_of_inPlace` and `inPlace_compilesToTM` use `sorry`, so +> `lake build --wfail` and the axiom guard will report them until the proofs are +> supplied. -/ namespace Complexity @@ -237,6 +253,69 @@ theorem identity_time_matches : -- The full compiler theorem (statement; proof is tracked future work) -- ════════════════════════════════════════════════════════════════════════ +/-- A *loaded start configuration* for the internal, layout-relative compiler +interface. The environment of an in-place program is a list of first-order +`Data` values `env : Fin m → Data`; a `LoadedStart` places entry `j` on the +designated work tape `slot j` (as its balanced-parenthesis serialization +`Data.toBits`) and leaves every other tape blank, with the machine in its start +state. This is the multi-tape analogue of `Cfg.init`: one work tape per program +argument, chosen by the caller through `slot`. -/ +structure LoadedStart {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) + (env : Fin m → Data) (c : Cfg k M.Q) : Prop where + /-- The machine is in its start state. -/ + state : c.state = M.qstart + /-- The dedicated input tape is unused (blank). -/ + input : c.input = Tape.init [] + /-- The output tape starts blank. -/ + output : c.output = Tape.init [] + /-- Environment entry `j` sits on tape `slot j`, serialized via `Data.toBits`. -/ + envTape : ∀ j, c.work (slot j) = Tape.init ((env j).toBits.map Γ.ofBool) + /-- Every non-environment work tape starts blank. -/ + cleanTape : ∀ i, (∀ j, i ≠ slot j) → c.work i = Tape.init [] + +/-- **The internal, layout-relative compiler contract.** `CompilesUnder M slot +res p a b` says the machine `M` implements program `p` for the environment +layout `slot` (argument `j` on work tape `slot j`) with the result deposited on +work tape `res`: for every first-order environment `env` and every RTM +derivation `ProgSem … p (.data result) t s`, starting from any `LoadedStart`, +the machine halts within `a·t + a` steps having written `result.toBits` on tape +`res`, and no reachable configuration moves any work head past cell `b·s + b`. + +Because `Data.toBits` has length `Data.size` (`Data.toBits_length`), the tape +space charged here is exactly the RTM `Data.size` measure, so the space bound +`b·s + b` matches the RTM space `s` up to the constant `b`. This is the +predicate the structural recursion over `InPlace` is proved against; the public +`inPlace_compilesToTM` is the single-argument (`m = 1`) specialization wrapped +with a fixed input-tape ↦ argument-tape prologue and a result-tape ↦ output-tape +epilogue. -/ +def CompilesUnder {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) (res : Fin k) + (p : Prog) (a b : ℕ) : Prop := + ∀ (env : Fin m → Data) (result : Data) (t s : ℕ), + ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → + ∀ c : Cfg k M.Q, LoadedStart M slot env c → + (∃ (c' : Cfg k M.Q) (t' : ℕ), t' ≤ a * t + a ∧ M.reachesIn t' c c' ∧ + M.halted c' ∧ (c'.work res).HasOutput result.toBits) ∧ + (∀ c'', M.reaches c c'' → ∀ i, (c''.work i).head ≤ b * s + b) + +/-- **The internal compiler recursion (statement only; proof deferred).** For a +fixed argument arity `m`, every first-order (`InPlace`) program compiles to a +Turing machine together with a tape layout (`slot`, `res`) and constant factors +`a`, `b` satisfying the layout-relative contract `CompilesUnder`. + +This is the workhorse proved by structural recursion on the `InPlace` +derivation: `var i` reads tape `slot i`; `empty` writes the empty node; `cons` +runs its two sub-machines on disjoint tape banks and concatenates; `elim`, +`ifEq`, and `while_` branch/loop over the sub-machines; and the immediately +consumed `app`/`fn` let-binding allocates one fresh environment tape (extending +`slot` for the `σ ++ [v]` body). Each constructor composes the sub-machines' +`CompilesUnder` certificates, accumulating `a`, `b` additively — matching the +`ProgSem` cost rules up to a constant. The base cases mirror `empty_realized` +and `identity_time_matches`. -/ +theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : + ∃ (k : ℕ) (M : TM k) (slot : Fin m → Fin k) (res : Fin k) (a b : ℕ), + CompilesUnder M slot res p a b := by + sorry + /-- **The full in-place RTM → Turing-machine compiler theorem.** For every first-order (`InPlace`) rose tree machine program `p`, there is a @@ -254,6 +333,16 @@ Because `M` carries ordinary `ComputesInTime` / `ComputesInSpace` certificates, it is directly usable as a **subroutine** — for instance composed with other machines through `TM.seqTM` or `TM.compositionTM`. +This public statement keeps the standard single-input / single-output interface +of the whole subroutine ecosystem; the multi-tape flexibility (one work tape per +program argument) lives in the internal layout-relative contract +`CompilesUnder` / `compilesUnder_of_inPlace`. The plan is to derive this theorem +as the `m = 1` specialization of `compilesUnder_of_inPlace`, wrapping the +resulting machine with a prologue that unpacks the single input tape onto the +one environment tape and an epilogue that copies the result tape to the output +tape. Tape *renumbering* for arbitrary call sites is then handled externally by +the existing `Lift` / `RetargetCompute` / `Placement` combinators. + The proof compiles `p` by structural recursion on the `InPlace` derivation, implementing each constructor with `Data`-manipulation subroutines over the binary encoding and accumulating the resource bounds compositionally. The base diff --git a/Complexitylib/Models/RoseTreeMachine/Data.lean b/Complexitylib/Models/RoseTreeMachine/Data.lean index 3430c6bf..6aeadcf2 100644 --- a/Complexitylib/Models/RoseTreeMachine/Data.lean +++ b/Complexitylib/Models/RoseTreeMachine/Data.lean @@ -115,6 +115,40 @@ theorem Data.inductionL {motive : Data → Prop} (d : Data) : motive d := Data.recL nil cons d +mutual +/-- Serialize a `Data` value to a balanced-parenthesis bit string: a node +`Data.l xs` becomes `false` (open bracket), the concatenated serializations of +its children, then `true` (close bracket). This is the physical layout used to +store a `Data` value on a Turing-machine tape; its length equals `Data.size` +(see `Data.toBits_length`), so the tape uses exactly `d.size` cells. -/ +def Data.toBits : Data → List Bool + | .l xs => false :: Data.toBitsList xs ++ [true] +/-- Concatenated serializations of a list of `Data` nodes; the recursive helper +of `Data.toBits`. -/ +def Data.toBitsList : List Data → List Bool + | [] => [] + | x :: xs => Data.toBits x ++ Data.toBitsList xs +end + +@[simp] lemma Data.toBits_l (xs : List Data) : + (Data.l xs).toBits = false :: Data.toBitsList xs ++ [true] := rfl + +@[simp] lemma Data.toBitsList_nil : Data.toBitsList [] = [] := rfl + +@[simp] lemma Data.toBitsList_cons (x : Data) (xs : List Data) : + Data.toBitsList (x :: xs) = x.toBits ++ Data.toBitsList xs := rfl + +/-- The serialization length equals `Data.size`: a tape holding `d.toBits` uses +exactly `d.size` cells. This is the bridge between RTM space (`Data.size`) and +the Turing-machine tape space that stores the value. -/ +@[simp] lemma Data.toBits_length (d : Data) : d.toBits.length = d.size := by + induction d using Data.inductionL with + | nil => simp + | cons x xs ihx ihxs => + simp only [Data.toBits_l, Data.toBitsList_cons, Data.cons_size, + List.length_append, List.length_cons, List.length_nil] at * + omega + /-- Index of a tape cell used by the rose tree machine's execution model. -/ abbrev TapeIndex := ℕ diff --git a/ROADMAP.md b/ROADMAP.md index b4c96158..baf121bd 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -156,13 +156,19 @@ another controller-local proof. - [ ] Compile the `InPlace` (first-order) RTM fragment to Turing machines with resource consumption matching the `ProgSem` cost model up to a constant factor. `Complexitylib.Models.RoseTreeMachine.Compile` lands the first - verified slice: the `InPlaceRealizedByTM` correspondence predicate, the - linear `Data`-encoding-size bridge (`dataSize_encode_listBool`), and two - proven base cases — `empty` (matching time *and* space via `emptyOutputTM`) - and `var 0`/identity (matching time via `copyInputToOutputTM`). The inductive - constructors (`cons`, `elim`, `ifEq`, `while_`, and the immediately consumed - `app`/`fn` let-binding) need concrete `Data`-manipulation subroutines and - remain to be composed through the same interface. + verified slice: the public `inPlace_compilesToTM` theorem statement (single + input/output, subroutine-ready), the internal layout-relative contract + `CompilesUnder` / `LoadedStart` (one work tape per program argument via + `slot : Fin m → Fin k`) with its recursion `compilesUnder_of_inPlace`, the + `Data.toBits` balanced-parenthesis tape serialization (length `= Data.size`), + the `InPlaceRealizedByTM` correspondence predicate, the linear + `Data`-encoding-size bridge (`dataSize_encode_listBool`), and two proven base + cases — `empty` (matching time *and* space via `emptyOutputTM`) and + `var 0`/identity (matching time via `copyInputToOutputTM`). The two headline + statements are `sorry` for now. The inductive constructors (`cons`, `elim`, + `ifEq`, `while_`, and the immediately consumed `app`/`fn` let-binding) need + concrete `Data`-manipulation subroutines and remain to be composed through + the `CompilesUnder` interface. - [x] Audit proof-engineering mechanics across representative machine and circuit constructions: inventory repeated state/tape/wire bookkeeping, run or trace stitching, semantic transport, and resource accounting, then prototype the From d0c6a79664723f0173cc38060ad39d3d8b622e23 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 19 Jul 2026 17:44:55 +0000 Subject: [PATCH 05/16] feat(Models): decompose RTM compiler into per-constructor parts Split the monolithic compilesUnder_of_inPlace obligation into one lemma per InPlace constructor, and complete the recursion assembly with no sorry. - Compiled m p: shared codomain (exists a machine + layout satisfying CompilesUnder at argument arity m). - compiled_var, compiled_empty, compiled_cons, compiled_elim, compiled_ifEq, compiled_while, compiled_app: the individual compiler parts, each turning compiled sub-programs into the compiled composite. Arities follow the operational semantics' environment extension (elim body at m+2, while/app body at m+1). Statements only (sorry). - compilesUnder_of_inPlace: now proved by induction on the InPlace derivation, dispatching each case to its part. This assembly is sorry-free. Only the seven compiled_* parts (and the public inPlace_compilesToTM wrapper) remain sorry. Style lint, build, and env linter pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 154 +++++++++++++----- ROADMAP.md | 6 +- 2 files changed, 122 insertions(+), 38 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index bfb25c50..c2c11d27 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -58,11 +58,15 @@ Two structural facts make this achievable for the `InPlace` fragment: (stated now; proof deferred, see *Scope*): every `InPlace` program compiles to a single Turing machine, usable as a subroutine, whose time and space are within a constant factor of the program's RTM bounds. -- `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion** - (statement only): every `InPlace` program compiles, for a fixed argument - arity, to a machine plus a tape layout satisfying `CompilesUnder`. This is the - theorem proved by structural recursion; `inPlace_compilesToTM` is its - single-argument wrapper. +- `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every + `InPlace` program compiles, for any argument arity, to a machine plus a tape + layout satisfying `CompilesUnder`. The recursion *assembly* is complete (no + `sorry`); it dispatches each program constructor to its individual part. +- `RoseTreeMachine.compiled_var`, `compiled_empty`, `compiled_cons`, + `compiled_elim`, `compiled_ifEq`, `compiled_while`, `compiled_app` — the + **individual compiler parts**, one per `InPlace` constructor, each turning + compiled sub-programs into the compiled composite (statements only; these are + the remaining `Data`-manipulation obligations). - `RoseTreeMachine.dataSize_encode_bool`, `dataSize_encode_listBool` — the binary encoding of a `List Bool` has `Data.size` linear in the list length; the reusable bridge between input length and RTM cost. @@ -78,21 +82,22 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Scope This is the first verified slice of the `InPlace`-RTM → TM compiler. The -headline `inPlace_compilesToTM` and the internal recursion -`compilesUnder_of_inPlace` are stated but their proofs are currently `sorry`: -the inductive constructors (`cons`, `elim`, `ifEq`, `while_`, and the -immediately consumed `app`/`fn` let-binding) require concrete data-manipulation -subroutines over the `Data` encoding and are tracked as future work in -`ROADMAP.md` (track N0). The base cases are already proven (`empty_realized`, -`identity_time_matches`). The framework here — the `CompilesUnder` / -`LoadedStart` layout-relative interface, the `InPlaceRealizedByTM` predicate, -the `Data.toBits` tape serialization, the encoding-size bridge, the two proven -base cases, and the fixed statements of both theorems — pins down the interface -those constructors will compose through. - -> Note: `compilesUnder_of_inPlace` and `inPlace_compilesToTM` use `sorry`, so -> `lake build --wfail` and the axiom guard will report them until the proofs are -> supplied. +compiler recursion is now fully decomposed: `compilesUnder_of_inPlace` assembles +the per-constructor parts `compiled_var`, `compiled_empty`, `compiled_cons`, +`compiled_elim`, `compiled_ifEq`, `compiled_while`, and `compiled_app` by +induction on the `InPlace` derivation — this assembly is complete, with no +`sorry`. Each individual part is stated but still `sorry`: it needs concrete +`Data`-manipulation subroutines over the tape serialization, tracked as future +work in `ROADMAP.md` (track N0). The `List Bool`-level base cases are separately +proven (`empty_realized`, `identity_time_matches`). The framework here — the +`CompilesUnder` / `LoadedStart` layout-relative interface, the `Data.toBits` +tape serialization, the `InPlaceRealizedByTM` predicate, the encoding-size +bridge, and the fixed part/assembly/wrapper statements — pins down the interface +those subroutines will compose through. + +> Note: the `compiled_*` parts and `inPlace_compilesToTM` use `sorry` (and +> `compilesUnder_of_inPlace` depends on the parts), so `lake build --wfail` and +> the axiom guard will report them until the parts are proved. -/ namespace Complexity @@ -297,25 +302,100 @@ def CompilesUnder {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) (res : Fin k) M.halted c' ∧ (c'.work res).HasOutput result.toBits) ∧ (∀ c'', M.reaches c c'' → ∀ i, (c''.work i).head ≤ b * s + b) -/-- **The internal compiler recursion (statement only; proof deferred).** For a -fixed argument arity `m`, every first-order (`InPlace`) program compiles to a -Turing machine together with a tape layout (`slot`, `res`) and constant factors -`a`, `b` satisfying the layout-relative contract `CompilesUnder`. - -This is the workhorse proved by structural recursion on the `InPlace` -derivation: `var i` reads tape `slot i`; `empty` writes the empty node; `cons` -runs its two sub-machines on disjoint tape banks and concatenates; `elim`, -`ifEq`, and `while_` branch/loop over the sub-machines; and the immediately -consumed `app`/`fn` let-binding allocates one fresh environment tape (extending -`slot` for the `σ ++ [v]` body). Each constructor composes the sub-machines' -`CompilesUnder` certificates, accumulating `a`, `b` additively — matching the -`ProgSem` cost rules up to a constant. The base cases mirror `empty_realized` -and `identity_time_matches`. -/ -theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : - ∃ (k : ℕ) (M : TM k) (slot : Fin m → Fin k) (res : Fin k) (a b : ℕ), - CompilesUnder M slot res p a b := by +/-- `Compiled m p`: the first-order program `p` compiles, for argument arity +`m`, to *some* Turing machine and tape layout satisfying the layout-relative +contract `CompilesUnder`. This is the codomain of the compiler recursion +`compilesUnder_of_inPlace`, and the shared shape of the per-constructor building +blocks below. -/ +def Compiled (m : ℕ) (p : Prog) : Prop := + ∃ (k : ℕ) (M : TM k) (slot : Fin m → Fin k) (res : Fin k) (a b : ℕ), + CompilesUnder M slot res p a b + +/-- **Compiler part — `var i`** (statement only). A variable read compiles: the +machine copies the argument tape `slot i` (when `i < m`, else the empty node) to +the result tape. Matches `ProgSem.var`, whose time and space are the size of the +read value. -/ +theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by + sorry + +/-- **Compiler part — `empty`** (statement only). The empty constructor compiles +to a machine that writes the empty node `Data.empty.toBits = [false, true]` on +the result tape. Matches `ProgSem.empty` (time and space `2`). -/ +theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by + sorry + +/-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines +for `h` and `t`, `cons` runs them on disjoint tape banks and prepends the head +value to the tail list on the result tape. Matches `ProgSem.cons` +(time/space add). -/ +theorem compiled_cons {m : ℕ} {h t : Prog} + (ih_h : Compiled m h) (ih_t : Compiled m t) : Compiled m (Prog.cons h t) := by + sorry + +/-- **Compiler part — `elim v emp (fn (fn body))`** (statement only). Given +compiled sub-machines for the scrutinee `v` and the empty branch `emp` at arity +`m`, and for the cons branch `body` at arity `m + 2` (the two fresh tapes hold +the destructured head and tail), `elim` branches on whether `v` is the empty +node. Matches `ProgSem.elim_nil` / `ProgSem.elim_cons`. -/ +theorem compiled_elim {m : ℕ} {v emp body : Prog} + (ih_v : Compiled m v) (ih_emp : Compiled m emp) (ih_body : Compiled (m + 2) body) : + Compiled m (Prog.elim v emp (.fn (.fn body))) := by sorry +/-- **Compiler part — `ifEq x y then_ else_`** (statement only). Given compiled +sub-machines for all four arguments at arity `m`, `ifEq` compares the values of +`x` and `y` and runs the matching branch. Matches `ProgSem.ifEq_then` / +`ProgSem.ifEq_else`. -/ +theorem compiled_ifEq {m : ℕ} {x y then_ else_ : Prog} + (ih_x : Compiled m x) (ih_y : Compiled m y) + (ih_then : Compiled m then_) (ih_else : Compiled m else_) : + Compiled m (Prog.ifEq x y then_ else_) := by + sorry + +/-- **Compiler part — `while_ init (fn body)`** (statement only). Given a +compiled sub-machine for `init` at arity `m` and for the loop `body` at arity +`m + 1` (the fresh tape holds the accumulator), `while_` iterates the body on the +accumulator tape until its head is empty. Matches `ProgSem.while_` / +`WhileSem` (which already uses `max` for space, exactly the loop's reuse). -/ +theorem compiled_while {m : ℕ} {init body : Prog} + (ih_init : Compiled m init) (ih_body : Compiled (m + 1) body) : + Compiled m (Prog.while_ init (.fn body)) := by + sorry + +/-- **Compiler part — `app (fn body) arg`** (the in-place `let`; statement only). +Given a compiled sub-machine for `arg` at arity `m` and for `body` at arity +`m + 1`, `app` evaluates `arg` onto a fresh environment tape and then runs +`body`. Matches `ProgSem.app` composed with `AppSem.mk` (running `body` in +`σ ++ [v]`). Nested uses give multi-argument `let`-chains, hence arbitrary +arities. -/ +theorem compiled_app {m : ℕ} {body arg : Prog} + (ih_body : Compiled (m + 1) body) (ih_arg : Compiled m arg) : + Compiled m (Prog.app (.fn body) arg) := by + sorry + +/-- **The internal compiler recursion.** For every argument arity `m`, every +first-order (`InPlace`) program compiles to a Turing machine together with a tape +layout satisfying the layout-relative contract `CompilesUnder`. + +The recursion structure is fully assembled here: induction on the `InPlace` +derivation dispatches each program constructor to its compiler part +(`compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`, +`compiled_ifEq`, `compiled_while`, `compiled_app`), threading the argument arity +so that `elim`/`while_`/`app` compile their body at the extended arity (`m + 2`, +`m + 1`, `m + 1`) that the `σ`-extension of the operational semantics uses. Only +the individual parts carry `sorry`; the assembly below is complete. -/ +theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : + Compiled m p := by + induction hp generalizing m with + | var => exact compiled_var m _ + | empty => exact compiled_empty m + | cons _ _ ih_h ih_t => exact compiled_cons ih_h ih_t + | elim _ _ _ ih_v ih_emp ih_body => exact compiled_elim ih_v ih_emp ih_body + | ifEq _ _ _ _ ih_x ih_y ih_then ih_else => + exact compiled_ifEq ih_x ih_y ih_then ih_else + | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body + | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg + /-- **The full in-place RTM → Turing-machine compiler theorem.** For every first-order (`InPlace`) rose tree machine program `p`, there is a diff --git a/ROADMAP.md b/ROADMAP.md index baf121bd..8189a7e5 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -168,7 +168,11 @@ another controller-local proof. statements are `sorry` for now. The inductive constructors (`cons`, `elim`, `ifEq`, `while_`, and the immediately consumed `app`/`fn` let-binding) need concrete `Data`-manipulation subroutines and remain to be composed through - the `CompilesUnder` interface. + the `CompilesUnder` interface. The compiler recursion is fully decomposed: + `compilesUnder_of_inPlace` assembles the per-constructor parts + (`compiled_var`/`compiled_empty`/`compiled_cons`/`compiled_elim`/ + `compiled_ifEq`/`compiled_while`/`compiled_app`) by induction with no + `sorry`; the parts themselves are the remaining obligations. - [x] Audit proof-engineering mechanics across representative machine and circuit constructions: inventory repeated state/tape/wire bookkeeping, run or trace stitching, semantic transport, and resource accounting, then prototype the From 13f309e74c1e4d892d006c7f05e0d3bd911d989c Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 19 Jul 2026 21:45:05 +0000 Subject: [PATCH 06/16] feat(rtm): prove compiled_empty RTM compiler part MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the `sorry` in `compiled_empty` with a full, machine-checked proof. Introduce `emptyNodeTM`, a 4-state multi-tape machine that materializes the empty node's serialization `[false, true]` on the result tape in three rightward steps, and prove it satisfies the layout-relative `CompilesUnder` contract for `Prog.empty`: the run has length 3 ≤ 2·2+2 and every reachable work head stays within 2·2+2, matching `ProgSem.empty` (time/space 2). Add supporting helpers `emptyStepOut`/`emptyStep` (one-step characterization), the write-and-move tape lemmas `writeAndMove_right_head`/`_cells` and `write_cells_of_ne_zero`, and `Γ.toΓwId` (write-back symbol map). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 160 +++++++++++++++++- 1 file changed, 156 insertions(+), 4 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index c2c11d27..698f8f49 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -102,6 +102,15 @@ those subroutines will compose through. namespace Complexity +/-- Map a read symbol to a writable symbol, sending the start marker `▷` to +blank. Used by the compiler's machines to write back a symbol they just read +without ever emitting `▷` (which is not a member of the write alphabet). -/ +def Γ.toΓwId : Γ → Γw + | .zero => .zero + | .one => .one + | .blank => .blank + | .start => .blank + namespace RoseTreeMachine open Complexity.TM @@ -311,6 +320,62 @@ def Compiled (m : ℕ) (p : Prog) : Prop := ∃ (k : ℕ) (M : TM k) (slot : Fin m → Fin k) (res : Fin k) (a b : ℕ), CompilesUnder M slot res p a b +/-- The empty-node writer: a 4-state machine over `m + 1` work tapes. From the +start state it steps all heads right off the left marker, then writes `0` and +`1` on the last (result) work tape, preserving all other tapes by writing back +what they read. This realizes `Prog.empty`, materializing `[false, true]` (the +`Data.toBits` of the empty node) on the result tape in three steps. -/ +def emptyNodeTM (m : ℕ) : TM (m + 1) where + Q := Fin 4 + qstart := 0 + qhalt := 3 + δ := fun q _ wHeads _ => + ( (if q = 0 then 1 else if q = 1 then 2 else 3), + (fun i => if i = Fin.last m + then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) + else (wHeads i).toΓwId), + Γw.blank, + Dir3.right, + (fun _ => Dir3.right), + Dir3.right ) + δ_right_of_start := by + intro q iHead wHeads oHead + exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ + +/-- The configuration reached by one step of `emptyNodeTM` from a state `q`. -/ +def emptyStepOut (m : ℕ) (cc : Cfg (m + 1) (Fin 4)) (q : Fin 4) : Cfg (m + 1) (Fin 4) := + { state := if q = 0 then 1 else if q = 1 then 2 else 3 + input := cc.input.move .right + work := fun i => (cc.work i).writeAndMove + ((if i = Fin.last m + then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) + else ((cc.work i).read).toΓwId) : Γ) .right + output := cc.output.writeAndMove ((Γw.blank : Γ)) .right } + +/-- One step of `emptyNodeTM` from a non-halted state matches `emptyStepOut`. -/ +theorem emptyStep (m : ℕ) (cc : Cfg (m + 1) (emptyNodeTM m).Q) (q : Fin 4) + (hq : cc.state = q) (hq3 : q ≠ 3) : + (emptyNodeTM m).step cc = some (emptyStepOut m cc q) := by + unfold TM.step + rw [if_neg (by rw [hq]; exact hq3)] + subst hq + simp only [emptyNodeTM, emptyStepOut, apply_ite Γw.toΓ] + +/-- One rightward write-and-move advances the head by one. -/ +theorem writeAndMove_right_head (t : Tape) (s : Γ) : + (t.writeAndMove s Dir3.right).head = t.head + 1 := by + simp [Tape.writeAndMove, Tape.move, Tape.write_head] + +/-- A rightward write-and-move leaves the same cells as writing in place. -/ +theorem writeAndMove_right_cells (t : Tape) (s : Γ) : + (t.writeAndMove s Dir3.right).cells = (t.write s).cells := by + simp [Tape.writeAndMove, Tape.move_cells] + +/-- Writing at a nonzero head updates exactly that cell. -/ +theorem write_cells_of_ne_zero {t : Tape} (h : t.head ≠ 0) (s : Γ) : + (t.write s).cells = Function.update t.cells t.head s := by + simp [Tape.write, h] + /-- **Compiler part — `var i`** (statement only). A variable read compiles: the machine copies the argument tape `slot i` (when `i < m`, else the empty node) to the result tape. Matches `ProgSem.var`, whose time and space are the size of the @@ -318,11 +383,98 @@ read value. -/ theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by sorry -/-- **Compiler part — `empty`** (statement only). The empty constructor compiles -to a machine that writes the empty node `Data.empty.toBits = [false, true]` on -the result tape. Matches `ProgSem.empty` (time and space `2`). -/ +/-- **Compiler part — `empty`.** The empty constructor compiles to `emptyNodeTM`, +a 4-state machine that writes the empty node `Data.empty.toBits = [false, true]` +on the result tape in three steps (all heads advance rightward each step). +Matches `ProgSem.empty` (time and space `2`): the run has length `3 ≤ 2·2 + 2` +and every reachable work head stays within `2·2 + 2`. -/ theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by - sorry + refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ + intro env result t s hsem c hstart + cases hsem + have hstate : c.state = (0 : Fin 4) := hstart.state + have hres0 : c.work (Fin.last m) = Tape.init [] := + hstart.cleanTape (Fin.last m) (fun j => (Fin.castSucc_lt_last j).ne') + have hheads0 : ∀ i, (c.work i).head = 0 := by + intro i + refine Fin.lastCases ?_ ?_ i + · rw [hres0]; rfl + · intro j; rw [hstart.envTape j]; rfl + set c1 := emptyStepOut m c 0 with hc1 + set c2 := emptyStepOut m c1 1 with hc2 + set c3 := emptyStepOut m c2 2 with hc3 + have hs0 : (emptyNodeTM m).step c = some c1 := emptyStep m c 0 hstate (by decide) + have hc1state : c1.state = 1 := by rw [hc1]; simp [emptyStepOut] + have hs1 : (emptyNodeTM m).step c1 = some c2 := emptyStep m c1 1 hc1state (by decide) + have hc2state : c2.state = 2 := by rw [hc2]; simp [emptyStepOut] + have hs2 : (emptyNodeTM m).step c2 = some c3 := emptyStep m c2 2 hc2state (by decide) + have hc3state : c3.state = 3 := by rw [hc3]; simp [emptyStepOut] + have htrace : (emptyNodeTM m).reachesIn 3 c c3 := .step hs0 (.step hs1 (.step hs2 .zero)) + -- The result tape after three steps. + set t0 : Tape := Tape.init [] with ht0 + set t1 : Tape := t0.writeAndMove ((Γw.blank : Γ)) Dir3.right with ht1 + set t2 : Tape := t1.writeAndMove ((Γw.zero : Γ)) Dir3.right with ht2 + set t3 : Tape := t2.writeAndMove ((Γw.one : Γ)) Dir3.right with ht3 + have rres : c3.work (Fin.last m) = t3 := by + simp only [hc3, hc2, hc1, emptyStepOut, ht3, ht2, ht1, ht0, hres0] + simp + have hh1 : t1.head = 1 := by rw [ht1, writeAndMove_right_head]; rfl + have hh2 : t2.head = 2 := by rw [ht2, writeAndMove_right_head, hh1] + -- Cells of the result tape. + have hc2cells : t2.cells = Function.update t0.cells 1 ((Γw.zero : Γ)) := by + rw [ht2, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh1]; decide), + hh1, ht1, writeAndMove_right_cells, Tape.write, ht0] + simp + have hc3cells : t3.cells = + Function.update (Function.update t0.cells 1 ((Γw.zero : Γ))) 2 ((Γw.one : Γ)) := by + rw [ht3, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh2]; decide), + hh2, hc2cells] + have hle : (3 : ℕ) ≤ 2 * 2 + 2 := by omega + refine ⟨⟨c3, 3, hle, htrace, ?_, ?_⟩, ?_⟩ + · -- halted + show c3.state = (emptyNodeTM m).qhalt + rw [hc3state]; rfl + · -- the result tape holds `[false, true]` + rw [rres] + have htb : (Data.l []).toBits = [false, true] := by simp + rw [htb, Tape.HasOutput] + refine ⟨?_, ?_⟩ + · intro i hi + rcases i with _ | _ | i + · rw [hc3cells, Function.update_of_ne (by decide), Function.update_self]; rfl + · rw [hc3cells, Function.update_self]; rfl + · simp only [List.length_cons, List.length_nil] at hi; omega + · rw [hc3cells, Function.update_of_ne (by decide), Function.update_of_ne (by decide), ht0] + simp + · -- space bound: every reachable configuration keeps work heads within `2·2 + 2` + have head_c1 : ∀ i, (c1.work i).head = (c.work i).head + 1 := by + intro i; rw [hc1]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ + have head_c2 : ∀ i, (c2.work i).head = (c1.work i).head + 1 := by + intro i; rw [hc2]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ + have head_c3 : ∀ i, (c3.work i).head = (c2.work i).head + 1 := by + intro i; rw [hc3]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ + have B0 : ∀ i, (c.work i).head ≤ 2 * 2 + 2 := fun i => by rw [hheads0 i]; omega + have B1 : ∀ i, (c1.work i).head ≤ 2 * 2 + 2 := fun i => by + rw [head_c1 i, hheads0 i]; omega + have B2 : ∀ i, (c2.work i).head ≤ 2 * 2 + 2 := fun i => by + rw [head_c2 i, head_c1 i, hheads0 i]; omega + have B3 : ∀ i, (c3.work i).head ≤ 2 * 2 + 2 := fun i => by + rw [head_c3 i, head_c2 i, head_c1 i, hheads0 i]; omega + have hc3h : c3.state = (emptyNodeTM m).qhalt := hc3state + have hnone : (emptyNodeTM m).step c3 = none := step_eq_none_iff_halted.mpr hc3h + intro c'' hreach i + rcases Relation.ReflTransGen.cases_head hreach with rfl | ⟨d1, hd1, hr1⟩ + · exact B0 i + · simp only [TM.stepRel] at hd1; rw [hs0] at hd1; injection hd1 with hd1; subst hd1 + rcases Relation.ReflTransGen.cases_head hr1 with rfl | ⟨d2, hd2, hr2⟩ + · exact B1 i + · simp only [TM.stepRel] at hd2; rw [hs1] at hd2; injection hd2 with hd2; subst hd2 + rcases Relation.ReflTransGen.cases_head hr2 with rfl | ⟨d3, hd3, hr3⟩ + · exact B2 i + · simp only [TM.stepRel] at hd3; rw [hs2] at hd3; injection hd3 with hd3; subst hd3 + rcases Relation.ReflTransGen.cases_head hr3 with rfl | ⟨d4, hd4, _⟩ + · exact B3 i + · simp only [TM.stepRel] at hd4; rw [hnone] at hd4; exact absurd hd4 (by simp) /-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines for `h` and `t`, `cons` runs them on disjoint tape banks and prepends the head From e2ca82a22ed39097c2a03f4f8811f6360ad4a62e Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Jul 2026 14:52:30 +0000 Subject: [PATCH 07/16] refactor(rtm): reframe compiler theorem over Data.toBits inputs Restate `inPlace_compilesToTM` to quantify over source values `d : Data` and use their balanced-parenthesis serialization `d.toBits` as the physical tape I/O encoding, constraining only well-formed inputs. This makes the Turing-machine space charge coincide exactly with the RTM `Data.size` measure via `Data.toBits_length` (no constant blow-up) and aligns the public statement with the internal `LoadedStart`/`CompilesUnder` layer, which already serializes via `Data.toBits`. Drop the obsolete encode-based framing: the `DataEncode`-bridge lemmas `dataSize_encode_bool`/`dataSize_encode_listBool`, the `InPlaceRealizedByTM` correspondence predicate, and its base cases `empty_realized`/ `var0_computesBoolFun_id`/`identity_time_matches`. Update the module docstring accordingly. Proof remains `sorry` (deferred). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 200 +++++------------- 1 file changed, 55 insertions(+), 145 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index 698f8f49..c58db493 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -45,10 +45,6 @@ Two structural facts make this achievable for the `InPlace` fragment: - `RoseTreeMachine.LoadedStart` — the multi-tape analogue of `Cfg.init`: the starting configuration for `CompilesUnder`, with each argument serialized onto its designated tape via `Data.toBits`. -- `RoseTreeMachine.InPlaceRealizedByTM` — the (single-input) correspondence - predicate: an `InPlace` program computing a binary function `f` is realized by - some Turing machine that computes `f` with time and space bounds dominated by - the program's RTM bounds. - `RoseTreeMachine.emptyOutputTM` — the one-state machine that halts immediately with empty output. @@ -56,8 +52,12 @@ Two structural facts make this achievable for the `InPlace` fragment: - `RoseTreeMachine.inPlace_compilesToTM` — **the full public compiler theorem** (stated now; proof deferred, see *Scope*): every `InPlace` program compiles to - a single Turing machine, usable as a subroutine, whose time and space are - within a constant factor of the program's RTM bounds. + a single Turing machine that, on any well-formed input `d.toBits` (the + balanced-parenthesis serialization of a first-order value `d`), halts with + `result.toBits` on its output tape and stays within the RTM time/space bounds + up to a constant factor. Because the physical tape encoding is `Data.toBits`, + `Data.toBits_length` makes the space charge coincide exactly with the RTM + `Data.size` measure. Ill-formed (non-`d.toBits`) inputs are left unconstrained. - `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every `InPlace` program compiles, for any argument arity, to a machine plus a tape layout satisfying `CompilesUnder`. The recursion *assembly* is complete (no @@ -65,19 +65,11 @@ Two structural facts make this achievable for the `InPlace` fragment: - `RoseTreeMachine.compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`, `compiled_ifEq`, `compiled_while`, `compiled_app` — the **individual compiler parts**, one per `InPlace` constructor, each turning - compiled sub-programs into the compiled composite (statements only; these are - the remaining `Data`-manipulation obligations). -- `RoseTreeMachine.dataSize_encode_bool`, `dataSize_encode_listBool` — the binary - encoding of a `List Bool` has `Data.size` linear in the list length; the - reusable bridge between input length and RTM cost. + compiled sub-programs into the compiled composite. `compiled_empty` is proven; + the rest are stated only (the remaining `Data`-manipulation obligations). - `RoseTreeMachine.emptyOutputTM_computesInTime` / `emptyOutputTM_computesInSpace` — the trivial machine computes `fun _ => []` in zero time and zero auxiliary space. -- `RoseTreeMachine.empty_realized` — the `InPlace` program `empty` is realized by - a Turing machine with matching time *and* space. -- `RoseTreeMachine.identity_time_matches` — the `InPlace` program `var 0` and the - input-to-output copy machine both compute the identity, with the machine's - exact time bound `n + 2` dominated by the program's RTM bound `4·n + 2`. ## Scope @@ -86,14 +78,13 @@ compiler recursion is now fully decomposed: `compilesUnder_of_inPlace` assembles the per-constructor parts `compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`, `compiled_ifEq`, `compiled_while`, and `compiled_app` by induction on the `InPlace` derivation — this assembly is complete, with no -`sorry`. Each individual part is stated but still `sorry`: it needs concrete -`Data`-manipulation subroutines over the tape serialization, tracked as future -work in `ROADMAP.md` (track N0). The `List Bool`-level base cases are separately -proven (`empty_realized`, `identity_time_matches`). The framework here — the -`CompilesUnder` / `LoadedStart` layout-relative interface, the `Data.toBits` -tape serialization, the `InPlaceRealizedByTM` predicate, the encoding-size -bridge, and the fixed part/assembly/wrapper statements — pins down the interface -those subroutines will compose through. +`sorry`. Of the individual parts, `compiled_empty` is proven; each remaining +part is stated but still `sorry`: it needs concrete `Data`-manipulation +subroutines over the tape serialization, tracked as future work in `ROADMAP.md` +(track N0). The framework here — the `CompilesUnder` / `LoadedStart` +layout-relative interface, the `Data.toBits` tape serialization, and the fixed +part/assembly/wrapper statements — pins down the interface those subroutines +will compose through. > Note: the `compiled_*` parts and `inPlace_compilesToTM` use `sorry` (and > `compilesUnder_of_inPlace` depends on the parts), so `lake build --wfail` and @@ -115,33 +106,6 @@ namespace RoseTreeMachine open Complexity.TM --- ════════════════════════════════════════════════════════════════════════ --- Encoding-size bridge: `Data.size` of a binary encoding is linear --- ════════════════════════════════════════════════════════════════════════ - -/-- Each `Bool` encodes to a `Data` value of size at most `4` (`false ↦ 2`, -`true ↦ 4`). -/ -lemma dataSize_encode_bool (b : Bool) : Data.size (DataEncode.encode b) ≤ 4 := by - cases b <;> simp [DataEncode.encode] - -/-- The binary encoding of a `List Bool` has `Data.size` bounded linearly by the -list length: `Data.size (encode x) ≤ 4·|x| + 2`. This is the bridge between a -Turing machine's input length `n` and the RTM cost of manipulating `encode x`. -/ -lemma dataSize_encode_listBool (x : List Bool) : - Data.size (DataEncode.encode x) ≤ 4 * x.length + 2 := by - induction x with - | nil => simp [DataEncode.encode] - | cons b bs ih => - have hrw : DataEncode.encode (b :: bs) - = Data.l (DataEncode.encode b :: bs.map DataEncode.encode) := by - simp [DataEncode.encode] - have hbs : Data.l (bs.map DataEncode.encode) = DataEncode.encode bs := by - simp [DataEncode.encode] - rw [hrw, Data.cons_size, hbs] - have hb := dataSize_encode_bool b - simp only [List.length_cons] - omega - -- ════════════════════════════════════════════════════════════════════════ -- A halted configuration only reaches itself -- ════════════════════════════════════════════════════════════════════════ @@ -204,65 +168,6 @@ theorem emptyOutputTM_computesInSpace (n : ℕ) : exact ⟨(emptyOutputTM n).initCfg x, Relation.ReflTransGen.refl, rfl, hasOutput_init_nil⟩ -- ════════════════════════════════════════════════════════════════════════ --- The correspondence predicate and the proven base cases --- ════════════════════════════════════════════════════════════════════════ - -/-- An `InPlace` rose tree machine program `p` computing the binary function `f` -is *realized by a Turing machine* when some machine computes the same `f` with -time and space bounds dominated by `p`'s RTM `ProgSem` bounds. This is the -compiler's per-program correctness-and-resource contract. -/ -def InPlaceRealizedByTM (p : Prog) (f : List Bool → List Bool) : Prop := - InPlace p ∧ - ∃ tR sR : ℕ → ℕ, p.ComputesBoolFunInTimeAndSpace f tR sR ∧ - ∃ (k : ℕ) (M : TM k) (tT sT : ℕ → ℕ), - M.ComputesInTime f tT ∧ M.ComputesInSpace f sT ∧ - (∀ n, tT n ≤ tR n) ∧ (∀ n, sT n ≤ sR n) - -/-- **The `empty` program is realized by a Turing machine with matching time and -space.** The `InPlace` program `empty` computes the constant empty-string -function in RTM time and space `2`, and `emptyOutputTM` computes the same -function in `0` time and `0` auxiliary space, both dominated by `2`. -/ -theorem empty_realized : InPlaceRealizedByTM Prog.empty (fun _ => []) := by - refine ⟨InPlace.empty, (fun _ => 2), (fun _ => 2), ?_, 0, emptyOutputTM 0, - (fun _ => 0), (fun _ => 0), emptyOutputTM_computesInTime 0, - emptyOutputTM_computesInSpace 0, fun _ => by dsimp only; omega, - fun _ => by dsimp only; omega⟩ - intro x - refine ⟨2, le_refl _, 2, le_refl _, ?_⟩ - show ProgSem [Value.data (DataEncode.encode x)] Prog.empty - (Value.data (DataEncode.encode ([] : List Bool))) 2 2 - rw [DataEncode_list_nil] - exact ProgSem.empty - -/-- The `InPlace` program `var 0` computes the identity binary function in RTM -time and space `4·n + 2` (the `Data.size` of the encoded input, bounded via -`dataSize_encode_listBool`). -/ -theorem var0_computesBoolFun_id : - (Prog.var 0).ComputesBoolFunInTimeAndSpace id - (fun n => 4 * n + 2) (fun n => 4 * n + 2) := by - intro x - refine ⟨Data.size (DataEncode.encode x), dataSize_encode_listBool x, - Data.size (DataEncode.encode x), dataSize_encode_listBool x, ?_⟩ - show ProgSem [Value.data (DataEncode.encode x)] (Prog.var 0) - (Value.data (DataEncode.encode (id x))) _ _ - have h : ProgSem [Value.data (DataEncode.encode x)] (Prog.var 0) _ _ _ := ProgSem.var - simpa using h - -/-- **The `var 0` program and the copy machine both compute the identity, with -matching (linear) time.** The `InPlace` program `var 0` computes the identity in -RTM time `4·n + 2`, and `copyInputToOutputTM` computes the identity in the exact -time bound `n + 2 ≤ 4·n + 2`. (The copy machine also uses only its fixed, -here empty, work-tape bank; a formal `ComputesInSpace` certificate is tracked -with the remaining constructors.) -/ -theorem identity_time_matches : - InPlace (Prog.var 0) ∧ - (Prog.var 0).ComputesBoolFunInTimeAndSpace id (fun n => 4 * n + 2) - (fun n => 4 * n + 2) ∧ - ∃ (k : ℕ) (M : TM k) (T : ℕ → ℕ), - M.ComputesInTime id T ∧ ∀ n, T n ≤ 4 * n + 2 := - ⟨InPlace.var, var0_computesBoolFun_id, 0, copyInputToOutputTM (n := 0), - (fun m => m + 2), copyInputToOutputTM_computesInTime 0, fun n => by dsimp only; omega⟩ - -- ════════════════════════════════════════════════════════════════════════ -- The full compiler theorem (statement; proof is tracked future work) -- ════════════════════════════════════════════════════════════════════════ @@ -551,44 +456,49 @@ theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : /-- **The full in-place RTM → Turing-machine compiler theorem.** For every first-order (`InPlace`) rose tree machine program `p`, there is a -Turing machine `M` and constants `a`, `b` such that, whenever `p` computes a -binary function `f` within RTM time `tR` and space `sR`, the *single* machine -`M` computes the same `f` within Turing-machine time `a·tR + a` and auxiliary -space `b·sR + b`. +Turing machine `M` and constants `a`, `b` such that, on any *well-formed* input +— the balanced-parenthesis serialization `d.toBits` of a first-order value `d` +(`(` ↦ `false`, `)` ↦ `true`) — `M` reproduces the program's behaviour: whenever +`p` maps `d` to `result` in RTM time `t` and space `s` +(`ProgSem [.data d] p (.data result) t s`, i.e. `p.ComputesInTimeAndSpace`), the +*single* machine `M` halts on input `d.toBits` within `a·t + a` steps with +`result.toBits` on its output tape, and every reachable configuration keeps its +work heads (and input-head travel) within `b·s + b`. + +Inputs that are *not* of the form `d.toBits` — the ill-formed bit strings — are +left unconstrained: the statement quantifies over the source values `d` +directly, so it speaks only about well-formed inputs. This uses `Data.toBits` as +the physical tape encoding, so `Data.toBits_length : d.toBits.length = d.size` +makes the Turing-machine space charge coincide exactly with the RTM `Data.size` +space measure (no constant blow-up), and the statement lines up directly with +the internal `LoadedStart` / `CompilesUnder` layout, which already serializes +values via `Data.toBits`. The machine `M` and constants `a`, `b` depend only on `p` (they are produced by -compiling `p`), not on the function `f` being analyzed; by value-determinism of -`ProgSem` there is at most one such `f`. The constants capture the "match up to -a constant factor" convention documented at the top of this file. - -Because `M` carries ordinary `ComputesInTime` / `ComputesInSpace` certificates, -it is directly usable as a **subroutine** — for instance composed with other -machines through `TM.seqTM` or `TM.compositionTM`. - -This public statement keeps the standard single-input / single-output interface -of the whole subroutine ecosystem; the multi-tape flexibility (one work tape per -program argument) lives in the internal layout-relative contract -`CompilesUnder` / `compilesUnder_of_inPlace`. The plan is to derive this theorem -as the `m = 1` specialization of `compilesUnder_of_inPlace`, wrapping the -resulting machine with a prologue that unpacks the single input tape onto the -one environment tape and an epilogue that copies the result tape to the output -tape. Tape *renumbering* for arbitrary call sites is then handled externally by -the existing `Lift` / `RetargetCompute` / `Placement` combinators. - -The proof compiles `p` by structural recursion on the `InPlace` derivation, -implementing each constructor with `Data`-manipulation subroutines over the -binary encoding and accumulating the resource bounds compositionally. The base -cases `empty` and `var 0` are already discharged by `empty_realized` and -`identity_time_matches`; the inductive constructors (`cons`, `elim`, `ifEq`, -`while_`, and the immediately consumed `app`/`fn` let-binding) remain to be -built (tracked in `ROADMAP.md`, track N0). The statement is provided now so the -subroutine interface is fixed; the proof is deferred. -/ +compiling `p`). `M.IsTransducer` records the one-way output discipline required +of a space-bounded transducer, so `M` is directly usable as a **subroutine** — +composed with other machines through `TM.seqTM` or `TM.compositionTM`. The +multi-tape flexibility (one work tape per program argument) lives in the +internal layout-relative contract `CompilesUnder` / `compilesUnder_of_inPlace`. +The plan is to derive this theorem as the `m = 1` specialization of +`compilesUnder_of_inPlace`, wrapping the resulting machine with a prologue that +unpacks the single input tape onto the one environment tape and an epilogue that +copies the result tape to the output tape. Tape *renumbering* for arbitrary call +sites is then handled externally by the existing `Lift` / `RetargetCompute` / +`Placement` combinators. + +The base case `empty` is discharged by `compiled_empty`; the remaining +constructors are tracked in `ROADMAP.md`, track N0. The statement is provided +now so the subroutine interface is fixed; the proof is deferred. -/ theorem inPlace_compilesToTM (p : Prog) (hp : InPlace p) : - ∃ (k : ℕ) (M : TM k) (a b : ℕ), - ∀ (f : List Bool → List Bool) (tR sR : ℕ → ℕ), - p.ComputesBoolFunInTimeAndSpace f tR sR → - M.ComputesInTime f (fun n => a * tR n + a) ∧ - M.ComputesInSpace f (fun n => b * sR n + b) := by + ∃ (k : ℕ) (M : TM k) (a b : ℕ), M.IsTransducer ∧ + ∀ (d result : Data) (t s : ℕ), + p.ComputesInTimeAndSpace d result t s → + (∃ (c' : Cfg k M.Q) (t' : ℕ), t' ≤ a * t + a ∧ + M.reachesIn t' (M.initCfg d.toBits) c' ∧ M.halted c' ∧ + c'.output.HasOutput result.toBits) ∧ + (∀ c', M.reaches (M.initCfg d.toBits) c' → + c'.WithinAuxSpace d.toBits.length (b * s + b)) := by sorry end RoseTreeMachine From 1f87b3e1d7b05379aaaeed797d8b20cdb80308b3 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Jul 2026 15:08:14 +0000 Subject: [PATCH 08/16] refactor(rtm): restate compiler theorem as tape-indexed subroutine MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reframe `inPlace_compilesToTM` in the style of the binary-arithmetic subroutines (`binaryAddIntoTM` etc.): the caller runs the compiled program at tape indices of their choosing rather than on the dedicated input/output tapes. The theorem now exposes a scratch-tape count `sc` and constants `a`, `b` (all depending only on the program and arity `m`), then quantifies over a caller-owned tape bank `Fin k` with: - `argIdx : Fin m → Fin k` — variable `j` read from tape `argIdx j`; - `resIdx : Fin k` — result tape; - `scratchIdx : Fin sc → Fin k` — the auxiliary tapes to reserve; required pairwise disjoint. Inputs sit on the argument work tapes as their `Data.toBits` serialization (the input tape stays blank). Correctness/resources are stated as a `HoareTimeSpace` contract: the machine halts within `a·t + a` steps with `HasOutput result.toBits` on `resIdx`, leaves every other tape exactly as it started (arguments preserved read-only, scratch restored blank, untouched tapes untouched), and stays within `b·s + b` auxiliary space. Add the `Hoare.Space.Defs` import and update the module docstring. Proof remains `sorry` (deferred). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 126 +++++++++++------- 1 file changed, 78 insertions(+), 48 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index c58db493..b6f8d042 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -5,6 +5,7 @@ Authors: Christian Reitwiessner -/ import Complexitylib.Models.RoseTreeMachine.Prog import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput +import Complexitylib.Models.TuringMachine.Hoare.Space.Defs /-! # Compiling in-place rose tree machine programs to Turing machines @@ -51,13 +52,18 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Main results - `RoseTreeMachine.inPlace_compilesToTM` — **the full public compiler theorem** - (stated now; proof deferred, see *Scope*): every `InPlace` program compiles to - a single Turing machine that, on any well-formed input `d.toBits` (the - balanced-parenthesis serialization of a first-order value `d`), halts with - `result.toBits` on its output tape and stays within the RTM time/space bounds - up to a constant factor. Because the physical tape encoding is `Data.toBits`, + (stated now; proof deferred, see *Scope*): every `InPlace` program of arity + `m` compiles to a subroutine that the caller runs at tape indices of their + choosing — argument tapes `argIdx : Fin m → Fin k`, a result tape `resIdx`, + and `sc` scratch tapes `scratchIdx : Fin sc → Fin k` (the scratch count `sc` + is exposed) — in the style of `binaryAddIntoTM`. Inputs live on the chosen + argument work tapes (not the dedicated input tape) as their `Data.toBits` + serialization; the machine halts within `a·t + a` steps with + `HasOutput result.toBits` on the result tape, leaves **every other tape + exactly as it started** (arguments preserved, scratch restored blank), and + stays within `b·s + b` auxiliary space. Because the encoding is `Data.toBits`, `Data.toBits_length` makes the space charge coincide exactly with the RTM - `Data.size` measure. Ill-formed (non-`d.toBits`) inputs are left unconstrained. + `Data.size` measure. - `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every `InPlace` program compiles, for any argument arity, to a machine plus a tape layout satisfying `CompilesUnder`. The recursion *assembly* is complete (no @@ -453,52 +459,76 @@ theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg -/-- **The full in-place RTM → Turing-machine compiler theorem.** - -For every first-order (`InPlace`) rose tree machine program `p`, there is a -Turing machine `M` and constants `a`, `b` such that, on any *well-formed* input -— the balanced-parenthesis serialization `d.toBits` of a first-order value `d` -(`(` ↦ `false`, `)` ↦ `true`) — `M` reproduces the program's behaviour: whenever -`p` maps `d` to `result` in RTM time `t` and space `s` -(`ProgSem [.data d] p (.data result) t s`, i.e. `p.ComputesInTimeAndSpace`), the -*single* machine `M` halts on input `d.toBits` within `a·t + a` steps with -`result.toBits` on its output tape, and every reachable configuration keeps its -work heads (and input-head travel) within `b·s + b`. - -Inputs that are *not* of the form `d.toBits` — the ill-formed bit strings — are -left unconstrained: the statement quantifies over the source values `d` -directly, so it speaks only about well-formed inputs. This uses `Data.toBits` as -the physical tape encoding, so `Data.toBits_length : d.toBits.length = d.size` -makes the Turing-machine space charge coincide exactly with the RTM `Data.size` -space measure (no constant blow-up), and the statement lines up directly with -the internal `LoadedStart` / `CompilesUnder` layout, which already serializes -values via `Data.toBits`. - -The machine `M` and constants `a`, `b` depend only on `p` (they are produced by -compiling `p`). `M.IsTransducer` records the one-way output discipline required -of a space-bounded transducer, so `M` is directly usable as a **subroutine** — -composed with other machines through `TM.seqTM` or `TM.compositionTM`. The -multi-tape flexibility (one work tape per program argument) lives in the -internal layout-relative contract `CompilesUnder` / `compilesUnder_of_inPlace`. -The plan is to derive this theorem as the `m = 1` specialization of -`compilesUnder_of_inPlace`, wrapping the resulting machine with a prologue that -unpacks the single input tape onto the one environment tape and an epilogue that -copies the result tape to the output tape. Tape *renumbering* for arbitrary call -sites is then handled externally by the existing `Lift` / `RetargetCompute` / -`Placement` combinators. +/-- **The full in-place RTM → Turing-machine compiler theorem (subroutine +form).** + +For every first-order (`InPlace`) rose tree machine program `p` of argument +arity `m`, there is a scratch-tape count `sc` and constants `a`, `b`, all +depending only on `p`, such that the program can be run *at tape indices the +caller chooses*, in the style of the binary-arithmetic subroutines +(`binaryAddIntoTM` etc.): + +* The caller owns a tape bank `Fin k` and picks the tapes freely: + - `argIdx : Fin m → Fin k` — variable `j` is read from work tape `argIdx j` + (the "variable index → tape index" map is caller-supplied, not fixed); + - `resIdx : Fin k` — the result is deposited here; + - `scratchIdx : Fin sc → Fin k` — the `sc` auxiliary tapes the machine needs. + These must be pairwise disjoint (`argIdx`/`scratchIdx` injective and their + ranges disjoint from each other and from `resIdx`). +* Inputs live on the chosen work tapes — **not** on the dedicated input tape, + which stays blank — each serialized via its balanced-parenthesis form + `Data.toBits` (`(` ↦ `false`, `)` ↦ `true`). The result-tape and every + scratch tape start blank. + +Then a machine `M : TM k` (built from the chosen indices) satisfies a +space-aware Hoare contract: whenever `p` maps the environment `env` to `result` +in RTM time `t` and space `s` +(`ProgSem (List.ofFn (Value.data ∘ env)) p (.data result) t s`), starting from +that loaded configuration `M` halts within `a·t + a` steps in a configuration +where + +* the result tape `resIdx` satisfies `HasOutput result.toBits`, and +* **every other tape is exactly as it started** (`∀ i ≠ resIdx, work i = + work₀ i`): the argument tapes are preserved read-only, the scratch tapes are + restored to blank, and any tape the machine never touched is untouched; + +and every reachable configuration keeps its work heads (and input-head travel) +within `b·s + b` auxiliary space. Because the physical encoding is `Data.toBits` +and `Data.toBits_length : d.toBits.length = d.size`, this space charge coincides +exactly with the RTM `Data.size` measure up to the constant `b`. + +Exposing `sc` tells the caller how many auxiliary tapes to reserve; the +"only the result tape changes" frame makes `M` freely reusable as a +**subroutine**, composable with the other tape-indexed machines. This is the +public face of the internal layout-relative contract `CompilesUnder` / +`compilesUnder_of_inPlace`, which serializes environments the same way. The base case `empty` is discharged by `compiled_empty`; the remaining constructors are tracked in `ROADMAP.md`, track N0. The statement is provided now so the subroutine interface is fixed; the proof is deferred. -/ -theorem inPlace_compilesToTM (p : Prog) (hp : InPlace p) : - ∃ (k : ℕ) (M : TM k) (a b : ℕ), M.IsTransducer ∧ - ∀ (d result : Data) (t s : ℕ), - p.ComputesInTimeAndSpace d result t s → - (∃ (c' : Cfg k M.Q) (t' : ℕ), t' ≤ a * t + a ∧ - M.reachesIn t' (M.initCfg d.toBits) c' ∧ M.halted c' ∧ - c'.output.HasOutput result.toBits) ∧ - (∀ c', M.reaches (M.initCfg d.toBits) c' → - c'.WithinAuxSpace d.toBits.length (b * s + b)) := by +theorem inPlace_compilesToTM (m : ℕ) (p : Prog) (hp : InPlace p) : + ∃ (sc a b : ℕ), + ∀ (k : ℕ) (argIdx : Fin m → Fin k) (resIdx : Fin k) + (scratchIdx : Fin sc → Fin k), + Function.Injective argIdx → Function.Injective scratchIdx → + (∀ j, argIdx j ≠ resIdx) → (∀ l, scratchIdx l ≠ resIdx) → + (∀ j l, argIdx j ≠ scratchIdx l) → + ∃ M : TM k, + ∀ (env : Fin m → Data) (result : Data) (t s : ℕ) + (work₀ : Fin k → Tape), + ProgSem (List.ofFn (fun j => Value.data (env j))) p + (Value.data result) t s → + (∀ j, work₀ (argIdx j) = Tape.init ((env j).toBits.map Γ.ofBool)) → + work₀ resIdx = Tape.init [] → + (∀ l, work₀ (scratchIdx l) = Tape.init []) → + M.HoareTimeSpace + (fun inp work out => + inp = Tape.init [] ∧ work = work₀ ∧ out = Tape.init []) + (fun inp work out => + inp = Tape.init [] ∧ out = Tape.init [] ∧ + (work resIdx).HasOutput result.toBits ∧ + (∀ i, i ≠ resIdx → work i = work₀ i)) + (a * t + a) 0 (b * s + b) := by sorry end RoseTreeMachine From 2542e66b92fe4a015b116ad0972ad2b25f03a85f Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Jul 2026 15:12:12 +0000 Subject: [PATCH 09/16] refactor(rtm): bundle compiler theorem into layout + contract defs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Simplify the public `inPlace_compilesToTM` statement, which had grown to a deeply nested block of index arguments, disjointness hypotheses, loading premises, and inline Hoare pre/post predicates. Factor it into two named, individually documented abstractions so the theorem collapses to one line: - `SubroutineLayout m sc k` — bundles the caller-chosen argument/result/scratch tape indices together with their pairwise-distinctness proofs, plus a `SubroutineLayout.Loaded` predicate for the expected starting tapes. - `Prog.RunsAsSubroutine p m` — the full subroutine correctness-and-resource contract (scratch count, time/space constants, per-layout machine, and the `HoareTimeSpace` frame). `inPlace_compilesToTM` is now `p.RunsAsSubroutine m`. Behaviour is unchanged; this is purely a readability refactor. Update the module docstring. Proof remains `sorry` (deferred). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 167 ++++++++++-------- 1 file changed, 92 insertions(+), 75 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index b6f8d042..7c6a3da6 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -38,6 +38,15 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Main definitions +- `RoseTreeMachine.SubroutineLayout` — a caller-chosen tape layout (argument + tapes `argIdx`, result tape `resIdx`, `sc` scratch tapes `scratchIdx`, all + pairwise distinct) for running an in-place program at tape indices of the + caller's choosing, in the style of the binary-arithmetic subroutines. +- `RoseTreeMachine.Prog.RunsAsSubroutine` — the **public subroutine contract**: + the compiled machine, run from a `SubroutineLayout.Loaded` start, halts with + the result on the result tape, frames every other tape (arguments preserved, + scratch restored blank), and matches the RTM time/space bounds up to a + constant. This is what `inPlace_compilesToTM` establishes. - `RoseTreeMachine.CompilesUnder` — the internal, **layout-relative** compiler contract: a machine implements a program for an environment layout that places one program argument per work tape (`slot : Fin m → Fin k`) and deposits the @@ -53,15 +62,13 @@ Two structural facts make this achievable for the `InPlace` fragment: - `RoseTreeMachine.inPlace_compilesToTM` — **the full public compiler theorem** (stated now; proof deferred, see *Scope*): every `InPlace` program of arity - `m` compiles to a subroutine that the caller runs at tape indices of their - choosing — argument tapes `argIdx : Fin m → Fin k`, a result tape `resIdx`, - and `sc` scratch tapes `scratchIdx : Fin sc → Fin k` (the scratch count `sc` - is exposed) — in the style of `binaryAddIntoTM`. Inputs live on the chosen - argument work tapes (not the dedicated input tape) as their `Data.toBits` - serialization; the machine halts within `a·t + a` steps with - `HasOutput result.toBits` on the result tape, leaves **every other tape - exactly as it started** (arguments preserved, scratch restored blank), and - stays within `b·s + b` auxiliary space. Because the encoding is `Data.toBits`, + `m` compiles to a reusable tape-indexed subroutine + (`Prog.RunsAsSubroutine m`). The caller runs it at tape indices of their + choosing (a `SubroutineLayout`); inputs live on the chosen argument work tapes + (not the dedicated input tape) as their `Data.toBits` serialization; the + machine halts with `HasOutput result.toBits` on the result tape, leaves every + other tape exactly as it started, and matches the RTM time/space bounds up to + a constant. Because the encoding is `Data.toBits`, `Data.toBits_length` makes the space charge coincide exactly with the RTM `Data.size` measure. - `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every @@ -459,76 +466,86 @@ theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg -/-- **The full in-place RTM → Turing-machine compiler theorem (subroutine -form).** - -For every first-order (`InPlace`) rose tree machine program `p` of argument -arity `m`, there is a scratch-tape count `sc` and constants `a`, `b`, all -depending only on `p`, such that the program can be run *at tape indices the -caller chooses*, in the style of the binary-arithmetic subroutines -(`binaryAddIntoTM` etc.): - -* The caller owns a tape bank `Fin k` and picks the tapes freely: - - `argIdx : Fin m → Fin k` — variable `j` is read from work tape `argIdx j` - (the "variable index → tape index" map is caller-supplied, not fixed); - - `resIdx : Fin k` — the result is deposited here; - - `scratchIdx : Fin sc → Fin k` — the `sc` auxiliary tapes the machine needs. - These must be pairwise disjoint (`argIdx`/`scratchIdx` injective and their - ranges disjoint from each other and from `resIdx`). -* Inputs live on the chosen work tapes — **not** on the dedicated input tape, - which stays blank — each serialized via its balanced-parenthesis form - `Data.toBits` (`(` ↦ `false`, `)` ↦ `true`). The result-tape and every - scratch tape start blank. - -Then a machine `M : TM k` (built from the chosen indices) satisfies a -space-aware Hoare contract: whenever `p` maps the environment `env` to `result` -in RTM time `t` and space `s` -(`ProgSem (List.ofFn (Value.data ∘ env)) p (.data result) t s`), starting from -that loaded configuration `M` halts within `a·t + a` steps in a configuration -where - -* the result tape `resIdx` satisfies `HasOutput result.toBits`, and -* **every other tape is exactly as it started** (`∀ i ≠ resIdx, work i = - work₀ i`): the argument tapes are preserved read-only, the scratch tapes are - restored to blank, and any tape the machine never touched is untouched; - -and every reachable configuration keeps its work heads (and input-head travel) -within `b·s + b` auxiliary space. Because the physical encoding is `Data.toBits` -and `Data.toBits_length : d.toBits.length = d.size`, this space charge coincides -exactly with the RTM `Data.size` measure up to the constant `b`. - -Exposing `sc` tells the caller how many auxiliary tapes to reserve; the -"only the result tape changes" frame makes `M` freely reusable as a -**subroutine**, composable with the other tape-indexed machines. This is the -public face of the internal layout-relative contract `CompilesUnder` / -`compilesUnder_of_inPlace`, which serializes environments the same way. +/-- **A caller-chosen tape layout** for running an `m`-argument in-place RTM +program as a subroutine on a `Fin k` tape bank using `sc` scratch tapes. As with +the binary-arithmetic subroutines, the caller picks every index; the fields +record that they are pairwise distinct so the machine can treat them as +independent registers. + +- `argIdx j` — the tape variable `j` is read from; +- `resIdx` — the tape the result is written to; +- `scratchIdx l` — the `l`-th auxiliary tape the machine may use. -/ +structure SubroutineLayout (m sc k : ℕ) where + /-- Variable `j` is read from work tape `argIdx j`. -/ + argIdx : Fin m → Fin k + /-- The result is deposited on work tape `resIdx`. -/ + resIdx : Fin k + /-- The `sc` auxiliary work tapes the machine may use. -/ + scratchIdx : Fin sc → Fin k + /-- Distinct variables use distinct tapes. -/ + argIdx_inj : Function.Injective argIdx + /-- Distinct scratch slots use distinct tapes. -/ + scratchIdx_inj : Function.Injective scratchIdx + /-- No argument tape coincides with the result tape. -/ + arg_ne_res : ∀ j, argIdx j ≠ resIdx + /-- No scratch tape coincides with the result tape. -/ + scratch_ne_res : ∀ l, scratchIdx l ≠ resIdx + /-- Argument tapes and scratch tapes are disjoint. -/ + arg_ne_scratch : ∀ j l, argIdx j ≠ scratchIdx l + +/-- The starting tape assignment expected by a `SubroutineLayout`: environment +entry `j` sits on its argument tape as the balanced-parenthesis serialization +`Data.toBits`, and the result and scratch tapes start blank. Tapes outside the +layout are unconstrained (and preserved as a frame). -/ +def SubroutineLayout.Loaded {m sc k : ℕ} (L : SubroutineLayout m sc k) + (env : Fin m → Data) (work : Fin k → Tape) : Prop := + (∀ j, work (L.argIdx j) = Tape.init ((env j).toBits.map Γ.ofBool)) ∧ + work L.resIdx = Tape.init [] ∧ + (∀ l, work (L.scratchIdx l) = Tape.init []) + +/-- **The public subroutine contract.** `p.RunsAsSubroutine m` says the +`m`-argument in-place program `p` compiles to a reusable Turing-machine +subroutine: there is a scratch-tape count `sc` and constants `a`, `b` +(depending only on `p`), so that for *any* caller layout `L : SubroutineLayout +m sc k` there is a machine `M : TM k` that, whenever `p` maps `env` to `result` +in RTM time `t` and space `s`, run from a `Loaded` start + +* halts within `a·t + a` steps with `result.toBits` on the result tape + (`HasOutput`), +* leaves **every other tape exactly as it started** (`∀ i ≠ resIdx`): arguments + preserved read-only, scratch restored blank, untouched tapes untouched, and +* keeps all work heads within `b·s + b` auxiliary space. + +Inputs live on the chosen argument work tapes, *not* the dedicated input tape +(which stays blank), so the space charge is over `Data.toBits`; by +`Data.toBits_length` it matches the RTM `Data.size` measure up to `b`. Exposing +`sc` tells the caller how many auxiliary tapes to reserve, and the +"only the result tape changes" frame makes `M` freely composable. -/ +def Prog.RunsAsSubroutine (p : Prog) (m : ℕ) : Prop := + ∃ sc a b : ℕ, ∀ {k : ℕ} (L : SubroutineLayout m sc k), + ∃ M : TM k, ∀ (env : Fin m → Data) (result : Data) (t s : ℕ) + (work₀ : Fin k → Tape), + ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → + L.Loaded env work₀ → + M.HoareTimeSpace + (fun inp work out => inp = Tape.init [] ∧ work = work₀ ∧ out = Tape.init []) + (fun inp work out => inp = Tape.init [] ∧ out = Tape.init [] ∧ + (work L.resIdx).HasOutput result.toBits ∧ + (∀ i, i ≠ L.resIdx → work i = work₀ i)) + (a * t + a) 0 (b * s + b) + +/-- **The full in-place RTM → Turing-machine compiler theorem.** Every +first-order (`InPlace`) rose tree machine program compiles, at any argument +arity `m`, to a reusable tape-indexed Turing-machine subroutine +(`Prog.RunsAsSubroutine`): the caller runs it at tape indices of their choosing, +inputs are serialized via `Data.toBits`, and time/space match the RTM `ProgSem` +bounds up to a constant. See `Prog.RunsAsSubroutine` for the precise contract. The base case `empty` is discharged by `compiled_empty`; the remaining constructors are tracked in `ROADMAP.md`, track N0. The statement is provided now so the subroutine interface is fixed; the proof is deferred. -/ -theorem inPlace_compilesToTM (m : ℕ) (p : Prog) (hp : InPlace p) : - ∃ (sc a b : ℕ), - ∀ (k : ℕ) (argIdx : Fin m → Fin k) (resIdx : Fin k) - (scratchIdx : Fin sc → Fin k), - Function.Injective argIdx → Function.Injective scratchIdx → - (∀ j, argIdx j ≠ resIdx) → (∀ l, scratchIdx l ≠ resIdx) → - (∀ j l, argIdx j ≠ scratchIdx l) → - ∃ M : TM k, - ∀ (env : Fin m → Data) (result : Data) (t s : ℕ) - (work₀ : Fin k → Tape), - ProgSem (List.ofFn (fun j => Value.data (env j))) p - (Value.data result) t s → - (∀ j, work₀ (argIdx j) = Tape.init ((env j).toBits.map Γ.ofBool)) → - work₀ resIdx = Tape.init [] → - (∀ l, work₀ (scratchIdx l) = Tape.init []) → - M.HoareTimeSpace - (fun inp work out => - inp = Tape.init [] ∧ work = work₀ ∧ out = Tape.init []) - (fun inp work out => - inp = Tape.init [] ∧ out = Tape.init [] ∧ - (work resIdx).HasOutput result.toBits ∧ - (∀ i, i ≠ resIdx → work i = work₀ i)) - (a * t + a) 0 (b * s + b) := by +theorem inPlace_compilesToTM {m : ℕ} (p : Prog) (hp : InPlace p) : + p.RunsAsSubroutine m := by sorry end RoseTreeMachine From 930ee1123143bb0e68fb1f552ad96efd77065833 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 20 Jul 2026 15:17:07 +0000 Subject: [PATCH 10/16] refactor(rtm): unify subroutine layout into one injective placement MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the three separate tape maps (`argIdx`/`resIdx`/`scratchIdx`) and five pairwise-distinctness fields of `SubroutineLayout` with a single injective placement `place : SubroutineSlot m sc → Fin k`, where `SubroutineSlot m sc := Fin m ⊕ Unit ⊕ Fin sc` enumerates the argument, result, and scratch slots. The five distinctness conditions are exactly injectivity of `place`. Role accessors `argIdx`/`resIdx`/`scratchIdx` and the derived distinctness lemmas (`argIdx_inj`, `scratchIdx_inj`, `arg_ne_res`, `scratch_ne_res`, `arg_ne_scratch`) are recovered from `place_inj`, so `Loaded` and `Prog.RunsAsSubroutine` are unchanged. Update the module docstring. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 83 ++++++++++++------- 1 file changed, 54 insertions(+), 29 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index 7c6a3da6..75ad5d48 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -38,10 +38,12 @@ Two structural facts make this achievable for the `InPlace` fragment: ## Main definitions -- `RoseTreeMachine.SubroutineLayout` — a caller-chosen tape layout (argument - tapes `argIdx`, result tape `resIdx`, `sc` scratch tapes `scratchIdx`, all - pairwise distinct) for running an in-place program at tape indices of the - caller's choosing, in the style of the binary-arithmetic subroutines. +- `RoseTreeMachine.SubroutineLayout` — a caller-chosen tape layout: a single + injective `place` map assigning each slot (an argument, the result, or a + scratch tape) a distinct physical tape in the caller's bank, for running an + in-place program at tape indices of the caller's choosing, in the style of the + binary-arithmetic subroutines. Role accessors `argIdx`/`resIdx`/`scratchIdx` + and their pairwise-distinctness follow from injectivity of `place`. - `RoseTreeMachine.Prog.RunsAsSubroutine` — the **public subroutine contract**: the compiled machine, run from a `SubroutineLayout.Loaded` start, halts with the result on the result tape, frames every other tape (arguments preserved, @@ -466,43 +468,66 @@ theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg +/-- The tapes a subroutine occupies, indexed uniformly by role: `m` argument +slots, one result slot, and `sc` scratch slots. A `SubroutineLayout` maps this +slot space injectively into the caller's tape bank. -/ +abbrev SubroutineSlot (m sc : ℕ) := Fin m ⊕ Unit ⊕ Fin sc + /-- **A caller-chosen tape layout** for running an `m`-argument in-place RTM program as a subroutine on a `Fin k` tape bank using `sc` scratch tapes. As with -the binary-arithmetic subroutines, the caller picks every index; the fields -record that they are pairwise distinct so the machine can treat them as -independent registers. - -- `argIdx j` — the tape variable `j` is read from; -- `resIdx` — the tape the result is written to; -- `scratchIdx l` — the `l`-th auxiliary tape the machine may use. -/ +the binary-arithmetic subroutines, the caller picks the tapes; a single +injective `place` assigns each slot (argument, result, or scratch) a distinct +physical tape, so the machine can treat them as independent registers. -/ structure SubroutineLayout (m sc k : ℕ) where - /-- Variable `j` is read from work tape `argIdx j`. -/ - argIdx : Fin m → Fin k - /-- The result is deposited on work tape `resIdx`. -/ - resIdx : Fin k - /-- The `sc` auxiliary work tapes the machine may use. -/ - scratchIdx : Fin sc → Fin k - /-- Distinct variables use distinct tapes. -/ - argIdx_inj : Function.Injective argIdx - /-- Distinct scratch slots use distinct tapes. -/ - scratchIdx_inj : Function.Injective scratchIdx - /-- No argument tape coincides with the result tape. -/ - arg_ne_res : ∀ j, argIdx j ≠ resIdx - /-- No scratch tape coincides with the result tape. -/ - scratch_ne_res : ∀ l, scratchIdx l ≠ resIdx - /-- Argument tapes and scratch tapes are disjoint. -/ - arg_ne_scratch : ∀ j l, argIdx j ≠ scratchIdx l + /-- The physical tape each slot occupies. -/ + place : SubroutineSlot m sc → Fin k + /-- Distinct slots occupy distinct tapes. -/ + place_inj : Function.Injective place + +namespace SubroutineLayout + +variable {m sc k : ℕ} (L : SubroutineLayout m sc k) + +/-- The tape variable `j` is read from. -/ +def argIdx (j : Fin m) : Fin k := L.place (.inl j) + +/-- The tape the result is written to. -/ +def resIdx : Fin k := L.place (.inr (.inl ())) + +/-- The `l`-th auxiliary tape the machine may use. -/ +def scratchIdx (l : Fin sc) : Fin k := L.place (.inr (.inr l)) + +/-- Distinct variables use distinct tapes. -/ +theorem argIdx_inj : Function.Injective L.argIdx := fun _ _ h => + Sum.inl_injective (L.place_inj h) + +/-- Distinct scratch slots use distinct tapes. -/ +theorem scratchIdx_inj : Function.Injective L.scratchIdx := fun _ _ h => + Sum.inr_injective (Sum.inr_injective (L.place_inj h)) + +/-- No argument tape coincides with the result tape. -/ +theorem arg_ne_res (j : Fin m) : L.argIdx j ≠ L.resIdx := fun h => by + simpa using L.place_inj h + +/-- No scratch tape coincides with the result tape. -/ +theorem scratch_ne_res (l : Fin sc) : L.scratchIdx l ≠ L.resIdx := fun h => by + simpa using L.place_inj h + +/-- Argument tapes and scratch tapes are disjoint. -/ +theorem arg_ne_scratch (j : Fin m) (l : Fin sc) : L.argIdx j ≠ L.scratchIdx l := + fun h => by simpa using L.place_inj h /-- The starting tape assignment expected by a `SubroutineLayout`: environment entry `j` sits on its argument tape as the balanced-parenthesis serialization `Data.toBits`, and the result and scratch tapes start blank. Tapes outside the layout are unconstrained (and preserved as a frame). -/ -def SubroutineLayout.Loaded {m sc k : ℕ} (L : SubroutineLayout m sc k) - (env : Fin m → Data) (work : Fin k → Tape) : Prop := +def Loaded (env : Fin m → Data) (work : Fin k → Tape) : Prop := (∀ j, work (L.argIdx j) = Tape.init ((env j).toBits.map Γ.ofBool)) ∧ work L.resIdx = Tape.init [] ∧ (∀ l, work (L.scratchIdx l) = Tape.init []) +end SubroutineLayout + /-- **The public subroutine contract.** `p.RunsAsSubroutine m` says the `m`-argument in-place program `p` compiles to a reusable Turing-machine subroutine: there is a scratch-tape count `sc` and constants `a`, `b` From e5ede5462211937ba07b03f7b200aa1662945eef Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 22 Jul 2026 09:06:16 +0000 Subject: [PATCH 11/16] feat(rtm): add emptyTM subroutine for the empty constructor MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Build the Turing machine that the rose tree `empty` constructor compiles to, targeting a caller-chosen work tape. - `emitBitsWorkTM idx w` — a reusable work-tape analogue of the output-tape `emitBitsTM`, appending a fixed word `w` to work tape `idx` one cell per step. Comes with `HoareTime` and `IsTransducer` contracts. - `emptyTM idx` — clears work tape `idx` first (so it works from any prior canonical Boolean content) then writes the empty node's serialization `[false, true]`. Proven `HoareTime` (linear time), `HoareTimeSpace` (additive space) and `IsTransducer` contracts. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- Complexitylib/Models.lean | 1 + .../Models/RoseTreeMachine/EmptyTM.lean | 278 ++++++++++++++++++ 2 files changed, 279 insertions(+) create mode 100644 Complexitylib/Models/RoseTreeMachine/EmptyTM.lean diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean index b725c85d..eccd1e84 100644 --- a/Complexitylib/Models.lean +++ b/Complexitylib/Models.lean @@ -60,6 +60,7 @@ import Complexitylib.Models.RoseTreeMachine.Data import Complexitylib.Models.RoseTreeMachine.DataEncode import Complexitylib.Models.RoseTreeMachine.Prog import Complexitylib.Models.RoseTreeMachine.Compile +import Complexitylib.Models.RoseTreeMachine.EmptyTM /-! # Computation models diff --git a/Complexitylib/Models/RoseTreeMachine/EmptyTM.lean b/Complexitylib/Models/RoseTreeMachine/EmptyTM.lean new file mode 100644 index 00000000..263d283e --- /dev/null +++ b/Complexitylib/Models/RoseTreeMachine/EmptyTM.lean @@ -0,0 +1,278 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexitylib.Models.TuringMachine.Registers.Emit +import Complexitylib.Models.TuringMachine.Subroutines.ClearWork +import Complexitylib.Models.TuringMachine.Hoare +import Complexitylib.Models.TuringMachine.Hoare.Space + +/-! +# The `empty` constructor as a tape-indexed Turing-machine subroutine + +The rose tree machine `empty` constructor produces the empty node, whose +balanced-parenthesis serialization is the two-bit word `[false, true]` +(an open followed by a close parenthesis). This module builds the Turing +machine that materializes that word on a **caller-chosen work tape**, so it can +serve as the machine the compiler maps `Prog.empty` to. + +The construction is deliberately parameterized only by the target tape index: + +- `TM.emitBitsWorkTM idx w` — a reusable subroutine that appends a *fixed* word + `w` to work tape `idx` (the work-tape analogue of the output-tape + `TM.emitBitsTM`), one cell per step. +- `TM.emptyTM idx` — clears work tape `idx` first (reusing `TM.clearWorkTM`, so + the machine works regardless of the tape's prior contents), then writes + `[false, true]`. Running the clear first costs only linear extra time and + does not increase the space footprint. + +## Main results + +- `TM.emitBitsWorkTM_hoareTime` — `emitBitsWorkTM idx w` writes `w` onto work + tape `idx` in `|w|` steps, framing every other tape. +- `TM.emitBitsWorkTM_isTransducer` — the writer never moves the output head left. +- `TM.emptyTM_hoareTime` — from any canonical Boolean target tape, `emptyTM idx` + leaves `[false, true]` on tape `idx` (`OutAcc`/`HasOutput`), framing the rest, + in time linear in the tape's prior length. +- `TM.emptyTM_hoareTimeSpace` — the corresponding additive space contract. +- `TM.emptyTM_isTransducer` — `emptyTM` never moves the output head left. +-/ + +namespace Complexity + +namespace TM + +variable {n : ℕ} + +-- ════════════════════════════════════════════════════════════════════════ +-- emitBitsWorkTM: append a fixed word to a work tape +-- ════════════════════════════════════════════════════════════════════════ + +/-- **Append the fixed word `w` to work tape `idx`** and halt. State `k` = the +number of bits already written; each step writes bit `k` on tape `idx`, moves +that head right, and leaves the input, output, and every other work tape parked +and untouched. This is the work-tape analogue of `emitBitsTM`. -/ +def emitBitsWorkTM (idx : Fin n) (w : List Bool) : TM n where + Q := Fin (w.length + 1) + qstart := ⟨0, by omega⟩ + qhalt := ⟨w.length, by omega⟩ + δ := fun k iHead wHeads oHead => + if h : k.val < w.length then + (⟨k.val + 1, by omega⟩, + fun i => if i = idx then Γw.ofBool w[k.val] else readBackWrite (wHeads i), + readBackWrite oHead, + idleDir iHead, + fun i => if i = idx then Dir3.right else idleDir (wHeads i), + idleDir oHead) + else + allIdle k iHead wHeads oHead + δ_right_of_start := by + intro k iHead wHeads oHead + by_cases h : k.val < w.length + · simp only [h, ↓reduceDIte] + refine ⟨idleDir_right_of_start, ?_, idleDir_right_of_start⟩ + intro i hi + split + · rfl + · exact idleDir_right_of_start hi + · simp only [h, ↓reduceDIte] + exact rightOfStart_allIdle iHead wHeads oHead + +/-- One write step: from state `k < |w|`, the machine writes bit `k` on tape +`idx`, advances the accumulator, and leaves the parked input, output, and other +work tapes unchanged. -/ +private theorem emitBitsWorkTM_step (idx : Fin n) (w : List Bool) + (c : Cfg n (emitBitsWorkTM (n := n) idx w).Q) (k : ℕ) (hk : k < w.length) + (hst : c.state = ⟨k, by omega⟩) + (hinp : Parked c.input) (hout : Parked c.output) + (hother : ∀ i, i ≠ idx → Parked (c.work i)) : + (emitBitsWorkTM (n := n) idx w).step c = some + { state := ⟨k + 1, by omega⟩, input := c.input, + work := Function.update c.work idx + ((c.work idx).writeAndMove (Γ.ofBool w[k]) .right), + output := c.output } := by + have hne : ¬ c.state = (emitBitsWorkTM (n := n) idx w).qhalt := by + rw [hst] + simp only [emitBitsWorkTM, Fin.mk.injEq] + omega + rw [TM.step, if_neg hne] + simp only [emitBitsWorkTM, hst, hk, ↓reduceDIte] + refine congrArg some ((Cfg.mk.injEq ..).mpr ⟨rfl, ?_, ?_, ?_⟩) + · exact hinp.move_idle + · funext i + by_cases hi : i = idx + · subst hi + simp only [if_true, Function.update_self, Γw.ofBool_toΓ] + · simp only [if_neg hi, Function.update_of_ne hi] + exact (hother i hi).writeAndMove_readBack_idle + · exact hout.writeAndMove_readBack_idle + +/-- The write loop: from state `k` with `|w| = k + m`, the machine reaches the +halt state in exactly `m` steps, appending `w.drop k` to tape `idx` and +preserving the input, output, and other work tapes. -/ +private theorem emitBitsWorkTM_run (idx : Fin n) (w : List Bool) (m : ℕ) : + ∀ (k : ℕ) (hk : w.length = k + m), + ∀ (c : Cfg n (emitBitsWorkTM (n := n) idx w).Q) (ys : List Bool), + c.state = ⟨k, by omega⟩ → Parked c.input → Parked c.output → + (∀ i, i ≠ idx → Parked (c.work i)) → OutAcc ys (c.work idx) → + ∃ c', (emitBitsWorkTM (n := n) idx w).reachesIn m c c' ∧ + c'.state = ⟨w.length, by omega⟩ ∧ c'.input = c.input ∧ + c'.output = c.output ∧ (∀ i, i ≠ idx → c'.work i = c.work i) ∧ + OutAcc (ys ++ w.drop k) (c'.work idx) := by + induction m with + | zero => + intro k hk c ys hst _ _ _ hacc + refine ⟨c, .zero, ?_, rfl, rfl, fun _ _ => rfl, ?_⟩ + · rw [hst]; congr 1; omega + · rw [List.drop_of_length_le (by omega), List.append_nil] + exact hacc + | succ m ih => + intro k hk c ys hst hinp hout hother hacc + have hklt : k < w.length := by omega + have hstep := emitBitsWorkTM_step idx w c k hklt hst hinp hout hother + set c₁ : Cfg n (emitBitsWorkTM (n := n) idx w).Q := + { state := ⟨k + 1, by omega⟩, input := c.input, + work := Function.update c.work idx + ((c.work idx).writeAndMove (Γ.ofBool w[k]) .right), + output := c.output } with hc₁ + have hother₁ : ∀ i, i ≠ idx → Parked (c₁.work i) := by + intro i hi + show Parked (Function.update c.work idx _ i) + rw [Function.update_of_ne hi] + exact hother i hi + have hacc₁ : OutAcc (ys ++ [w[k]]) (c₁.work idx) := by + show OutAcc _ (Function.update c.work idx _ idx) + rw [Function.update_self] + exact outAcc_append_bit hacc w[k] + obtain ⟨c', hreach, hst', hinp', hout', hwork', hacc'⟩ := + ih (k + 1) (by omega) c₁ (ys ++ [w[k]]) rfl hinp hout hother₁ hacc₁ + refine ⟨c', .step hstep hreach, hst', hinp', hout', ?_, ?_⟩ + · intro i hi + rw [hwork' i hi] + show Function.update c.work idx _ i = c.work i + rw [Function.update_of_ne hi] + · rwa [List.append_assoc, List.singleton_append, + List.getElem_cons_drop] at hacc' + +/-- **`emitBitsWorkTM` Hoare specification.** Writes the word `w` onto work tape +`idx` in `|w|` steps, leaving the input, output, and every other (parked) work +tape literally unchanged. Ghost-parametrized by the initial tapes so it composes +through `seqTM_hoareTime`. The starting tape `idx` is the empty accumulator (a +blank tape rewound to cell 1). -/ +theorem emitBitsWorkTM_hoareTime (idx : Fin n) (w : List Bool) + (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) + (hinp₀ : Parked inp₀) (hout₀ : Parked out₀) + (hother₀ : ∀ i, i ≠ idx → Parked (work₀ i)) + (hidx₀ : OutAcc [] (work₀ idx)) : + (emitBitsWorkTM (n := n) idx w).HoareTime + (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀) + (fun inp work out => + inp = inp₀ ∧ (∀ i, i ≠ idx → work i = work₀ i) ∧ + OutAcc w (work idx) ∧ out = out₀) + w.length := by + rintro inp work out ⟨rfl, rfl, rfl⟩ + obtain ⟨c', hreach, hst', hinp', hout', hwork', hacc'⟩ := + emitBitsWorkTM_run idx w w.length 0 (by omega) + { state := ⟨0, by omega⟩, input := inp, work := work, output := out } + [] rfl hinp₀ hout₀ hother₀ (by simpa using hidx₀) + refine ⟨c', w.length, le_refl _, hreach, hst', hinp', hwork', ?_, hout'⟩ + rwa [List.nil_append, List.drop_zero] at hacc' + +/-- Fixed-word work-tape emission never moves the output head left. -/ +theorem emitBitsWorkTM_isTransducer (idx : Fin n) (w : List Bool) : + (emitBitsWorkTM (n := n) idx w).IsTransducer := by + intro k iHead wHeads oHead + by_cases h : k.val < w.length + · simp [emitBitsWorkTM, h, idleDir] + split <;> decide + · simp [emitBitsWorkTM, h, allIdle, idleDir] + split <;> decide + +-- ════════════════════════════════════════════════════════════════════════ +-- emptyTM: clear then materialize the empty node's serialization +-- ════════════════════════════════════════════════════════════════════════ + +/-- **The Turing machine for the rose tree `empty` constructor.** Clears work +tape `idx` (so it works from any prior canonical Boolean content), then writes +the two-bit serialization `[false, true]` of the empty node onto it. -/ +def emptyTM (idx : Fin n) : TM n := + seqTM (clearWorkTM idx) (emitBitsWorkTM idx [false, true]) + +/-- The empty accumulator is exactly a rewound blank work tape. -/ +private theorem outAcc_nil_move_right : + OutAcc [] ((Tape.init []).move Dir3.right) := + outAcc_nil_init + +/-- **`emptyTM` Hoare specification.** Starting from any canonical Boolean +target tape `idx`, `emptyTM idx` produces the empty node's serialization +`[false, true]` on tape `idx`, leaves the input, output, and every other work +tape unchanged, and runs in `clearWorkTimeBound bits.length + 3` steps — +linear in the tape's prior length. -/ +theorem emptyTM_hoareTime (idx : Fin n) (bits : List Bool) + (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) + (htarget : work₀ idx = (Tape.init (bits.map Γ.ofBool)).move Dir3.right) + (hinp : Parked inp₀) (hother : ∀ i, i ≠ idx → Parked (work₀ i)) + (hout : Parked out₀) : + (emptyTM idx).HoareTime + (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀) + (fun inp work out => + inp = inp₀ ∧ (∀ i, i ≠ idx → work i = work₀ i) ∧ + (work idx).HasOutput [false, true] ∧ out = out₀) + (clearWorkTimeBound bits.length + 1 + 2) := by + set wc := Function.update work₀ idx ((Tape.init []).move Dir3.right) with hwc_def + have hidx0 : OutAcc [] (wc idx) := by + rw [hwc_def, Function.update_self]; exact outAcc_nil_move_right + have hwcParked : ∀ i, Parked (wc i) := by + intro i + by_cases hi : i = idx + · subst hi; exact hidx0.parked + · rw [hwc_def, Function.update_of_ne hi]; exact hother i hi + refine (seqTM_hoareTime (clearWorkTM idx) (emitBitsWorkTM idx [false, true]) + (clearWorkTM_hoareTime_frame idx bits inp₀ work₀ out₀ htarget hinp hother hout) + ?htrans + (emitBitsWorkTM_hoareTime idx [false, true] inp₀ wc out₀ hinp hout + (fun i _ => hwcParked i) hidx0)).strengthen_post ?hpost + · rintro inp work out ⟨rfl, rfl, rfl⟩ + exact ⟨hinp.transitionInput_eq_self, + funext fun i => (hwcParked i).transitionTape_eq_self, + hout.transitionTape_eq_self⟩ + · rintro inp work out ⟨hi, hframe, hacc, ho⟩ + refine ⟨hi, fun i hi' => ?_, hacc.hasOutput, ho⟩ + rw [hframe i hi', hwc_def, Function.update_of_ne hi'] + +/-- `emptyTM` never moves the output head left. -/ +theorem emptyTM_isTransducer (idx : Fin n) : + (emptyTM idx).IsTransducer := + (clearWorkTM_isTransducer idx).seqTM (emitBitsWorkTM_isTransducer idx [false, true]) + +/-- **Time-and-space form of `emptyTM_hoareTime`.** Starting within an +`initialSpace` budget, materializing the empty node stays within +`initialSpace + (clearWorkTimeBound bits.length + 3)` — the standard additive +over-approximation (one cell per step). Since the running time is linear in the +target tape's prior length, so is the extra space charged here. -/ +theorem emptyTM_hoareTimeSpace (idx : Fin n) (bits : List Bool) + (inputLength initialSpace : ℕ) + (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) + (htarget : work₀ idx = (Tape.init (bits.map Γ.ofBool)).move Dir3.right) + (hinp : Parked inp₀) (hother : ∀ i, i ≠ idx → Parked (work₀ i)) + (hout : Parked out₀) + (hinitial : + ({ state := (emptyTM idx).qstart + input := inp₀ + work := work₀ + output := out₀ } : + Cfg n (emptyTM idx).Q).WithinAuxSpace inputLength initialSpace) : + (emptyTM idx).HoareTimeSpace + (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀) + (fun inp work out => + inp = inp₀ ∧ (∀ i, i ≠ idx → work i = work₀ i) ∧ + (work idx).HasOutput [false, true] ∧ out = out₀) + (clearWorkTimeBound bits.length + 1 + 2) inputLength + (initialSpace + (clearWorkTimeBound bits.length + 1 + 2)) := + (emptyTM_hoareTime idx bits inp₀ work₀ out₀ htarget hinp hother hout).toHoareTimeSpace + (by rintro inp work out ⟨rfl, rfl, rfl⟩; exact hinitial) + +end TM + +end Complexity From 195b9a22a9735cfc6b3df600ceb23a8ea2458cc5 Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 22 Jul 2026 09:33:08 +0000 Subject: [PATCH 12/16] refactor(rtm): split RTM-to-TM compiler into Defs/Internal/surface MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reorganize the RTM → TM simulation code into a `Compile/` directory following the repo's three-layer architecture: - `Compile.lean` (surface) — keeps only the final theorem `inPlace_compilesToTM`. - `Compile/Defs.lean` — the human-auditable contract: `SubroutineSlot`, `SubroutineLayout` (+ accessors/distinctness lemmas, `Loaded`) and `Prog.RunsAsSubroutine`. - `Compile/Internal.lean` — all proof machinery (`Γ.toΓwId`, `emptyOutputTM`, `LoadedStart`/`CompilesUnder`/`Compiled`, the concrete per-constructor machines and `compiled_*` parts, `compilesUnder_of_inPlace`). - `Compile/Internal/EmptyTM.lean` — the empty-constructor machine (`emitBitsWorkTM`/`emptyTM`), moved from `RoseTreeMachine/EmptyTM.lean`. No definitions change; `Models.lean` now imports `Compile` transitively. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- Complexitylib/Models.lean | 1 - .../Models/RoseTreeMachine/Compile.lean | 566 +----------------- .../Models/RoseTreeMachine/Compile/Defs.lean | 148 +++++ .../RoseTreeMachine/Compile/Internal.lean | 413 +++++++++++++ .../{ => Compile/Internal}/EmptyTM.lean | 0 5 files changed, 586 insertions(+), 542 deletions(-) create mode 100644 Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean create mode 100644 Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean rename Complexitylib/Models/RoseTreeMachine/{ => Compile/Internal}/EmptyTM.lean (100%) diff --git a/Complexitylib/Models.lean b/Complexitylib/Models.lean index eccd1e84..b725c85d 100644 --- a/Complexitylib/Models.lean +++ b/Complexitylib/Models.lean @@ -60,7 +60,6 @@ import Complexitylib.Models.RoseTreeMachine.Data import Complexitylib.Models.RoseTreeMachine.DataEncode import Complexitylib.Models.RoseTreeMachine.Prog import Complexitylib.Models.RoseTreeMachine.Compile -import Complexitylib.Models.RoseTreeMachine.EmptyTM /-! # Computation models diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index 75ad5d48..d201a59a 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -3,562 +3,46 @@ Copyright (c) 2026 Christian Reitwiessner. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Christian Reitwiessner -/ -import Complexitylib.Models.RoseTreeMachine.Prog -import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput -import Complexitylib.Models.TuringMachine.Hoare.Space.Defs +import Complexitylib.Models.RoseTreeMachine.Compile.Defs +import Complexitylib.Models.RoseTreeMachine.Compile.Internal /-! # Compiling in-place rose tree machine programs to Turing machines -This file constructs equivalent Turing machines for programs in the first-order -(`InPlace`) fragment of the rose tree machine (RTM) and relates their resource -consumption to the RTM `ProgSem` cost model. +This is the **surface** of the RTM → TM compiler: it states the single public +theorem `inPlace_compilesToTM`. The human-auditable contract it establishes +(`SubroutineLayout` / `Prog.RunsAsSubroutine`) lives in +`Complexitylib.Models.RoseTreeMachine.Compile.Defs`, and all proof machinery +lives in `Complexitylib.Models.RoseTreeMachine.Compile.Internal`. -## What "match" means here +## Main result -The RTM cost model is faithful to Turing machines only *up to a constant -factor* — this is the same notion the RTM's own `ComputableInOTime` / -`ComputableInOSpace` already use, and it is the standard notion for -cross-model simulation. Concretely, a compiled machine computes the *same* -binary function as the source program and its time (resp. space) bound is -*dominated by* the program's RTM time (resp. space) bound. - -Two structural facts make this achievable for the `InPlace` fragment: - -- **Result materialization is already paid for.** `ProgSem.size_le` shows every - derivation charges at least the size of the value it produces, in both time - and space. So the O(size) traversal/assembly/copy work a Turing machine must - perform to build a `Data` result is always absorbed (up to a constant) by the - sub-costs the RTM already charges. -- **Space is charged generously.** Most `ProgSem` rules *add* the space of - sequential sub-computations (`s₁ + s₂ + …`) where a Turing machine reuses - space and pays only their `max`. The RTM figure is therefore a valid upper - bound for the machine's actual space. (`WhileSem` already uses `max`, matching - the loop's space reuse exactly.) - -## Main definitions - -- `RoseTreeMachine.SubroutineLayout` — a caller-chosen tape layout: a single - injective `place` map assigning each slot (an argument, the result, or a - scratch tape) a distinct physical tape in the caller's bank, for running an - in-place program at tape indices of the caller's choosing, in the style of the - binary-arithmetic subroutines. Role accessors `argIdx`/`resIdx`/`scratchIdx` - and their pairwise-distinctness follow from injectivity of `place`. -- `RoseTreeMachine.Prog.RunsAsSubroutine` — the **public subroutine contract**: - the compiled machine, run from a `SubroutineLayout.Loaded` start, halts with - the result on the result tape, frames every other tape (arguments preserved, - scratch restored blank), and matches the RTM time/space bounds up to a - constant. This is what `inPlace_compilesToTM` establishes. -- `RoseTreeMachine.CompilesUnder` — the internal, **layout-relative** compiler - contract: a machine implements a program for an environment layout that places - one program argument per work tape (`slot : Fin m → Fin k`) and deposits the - result on a chosen tape, with time/space matched to the RTM `ProgSem` bounds. - This is where "multiple inputs map to tapes" lives. -- `RoseTreeMachine.LoadedStart` — the multi-tape analogue of `Cfg.init`: the - starting configuration for `CompilesUnder`, with each argument serialized onto - its designated tape via `Data.toBits`. -- `RoseTreeMachine.emptyOutputTM` — the one-state machine that halts immediately - with empty output. - -## Main results - -- `RoseTreeMachine.inPlace_compilesToTM` — **the full public compiler theorem** - (stated now; proof deferred, see *Scope*): every `InPlace` program of arity - `m` compiles to a reusable tape-indexed subroutine - (`Prog.RunsAsSubroutine m`). The caller runs it at tape indices of their - choosing (a `SubroutineLayout`); inputs live on the chosen argument work tapes - (not the dedicated input tape) as their `Data.toBits` serialization; the +- `RoseTreeMachine.inPlace_compilesToTM` — **the full public compiler theorem**: + every `InPlace` program of arity `m` compiles to a reusable tape-indexed + subroutine (`Prog.RunsAsSubroutine m`). The caller runs it at tape indices of + their choosing (a `SubroutineLayout`); inputs live on the chosen argument work + tapes (not the dedicated input tape) as their `Data.toBits` serialization; the machine halts with `HasOutput result.toBits` on the result tape, leaves every other tape exactly as it started, and matches the RTM time/space bounds up to - a constant. Because the encoding is `Data.toBits`, - `Data.toBits_length` makes the space charge coincide exactly with the RTM - `Data.size` measure. -- `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every - `InPlace` program compiles, for any argument arity, to a machine plus a tape - layout satisfying `CompilesUnder`. The recursion *assembly* is complete (no - `sorry`); it dispatches each program constructor to its individual part. -- `RoseTreeMachine.compiled_var`, `compiled_empty`, `compiled_cons`, - `compiled_elim`, `compiled_ifEq`, `compiled_while`, `compiled_app` — the - **individual compiler parts**, one per `InPlace` constructor, each turning - compiled sub-programs into the compiled composite. `compiled_empty` is proven; - the rest are stated only (the remaining `Data`-manipulation obligations). -- `RoseTreeMachine.emptyOutputTM_computesInTime` / - `emptyOutputTM_computesInSpace` — the trivial machine computes `fun _ => []` - in zero time and zero auxiliary space. + a constant. Because the encoding is `Data.toBits`, `Data.toBits_length` makes + the space charge coincide exactly with the RTM `Data.size` measure. ## Scope This is the first verified slice of the `InPlace`-RTM → TM compiler. The -compiler recursion is now fully decomposed: `compilesUnder_of_inPlace` assembles -the per-constructor parts `compiled_var`, `compiled_empty`, `compiled_cons`, -`compiled_elim`, `compiled_ifEq`, `compiled_while`, and `compiled_app` by -induction on the `InPlace` derivation — this assembly is complete, with no -`sorry`. Of the individual parts, `compiled_empty` is proven; each remaining -part is stated but still `sorry`: it needs concrete `Data`-manipulation -subroutines over the tape serialization, tracked as future work in `ROADMAP.md` -(track N0). The framework here — the `CompilesUnder` / `LoadedStart` -layout-relative interface, the `Data.toBits` tape serialization, and the fixed -part/assembly/wrapper statements — pins down the interface those subroutines -will compose through. - -> Note: the `compiled_*` parts and `inPlace_compilesToTM` use `sorry` (and -> `compilesUnder_of_inPlace` depends on the parts), so `lake build --wfail` and -> the axiom guard will report them until the parts are proved. +compiler recursion `Compile.Internal.compilesUnder_of_inPlace` is fully +decomposed into per-constructor parts; of those, `compiled_empty` is proven and +each remaining part is stated but still `sorry` (it needs concrete +`Data`-manipulation subroutines over the tape serialization, tracked in +`ROADMAP.md`, track N0). The final theorem below is therefore also `sorry` for +now, so `lake build --wfail` and the axiom guard will report it until the parts +are proved. -/ namespace Complexity -/-- Map a read symbol to a writable symbol, sending the start marker `▷` to -blank. Used by the compiler's machines to write back a symbol they just read -without ever emitting `▷` (which is not a member of the write alphabet). -/ -def Γ.toΓwId : Γ → Γw - | .zero => .zero - | .one => .one - | .blank => .blank - | .start => .blank - namespace RoseTreeMachine -open Complexity.TM - --- ════════════════════════════════════════════════════════════════════════ --- A halted configuration only reaches itself --- ════════════════════════════════════════════════════════════════════════ - -/-- A configuration whose state is the halt state has no successors, so the only -configuration it reaches is itself. -/ -private theorem reaches_eq_of_halted {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} - (hh : c.state = tm.qhalt) (h : tm.reaches c c') : c' = c := by - rcases Relation.ReflTransGen.cases_head h with heq | ⟨d, hstep, _⟩ - · exact heq.symm - · exact absurd hstep (by - have hnone : tm.step c = none := step_eq_none_iff_halted.mpr hh - simp [TM.stepRel, hnone]) - --- ════════════════════════════════════════════════════════════════════════ --- The trivial machine: halt immediately with empty output --- ════════════════════════════════════════════════════════════════════════ - -/-- The one-state Turing machine that is halted from the start. Its output tape -is the initial (empty) tape, so it computes the constant empty-string function -in zero steps and zero auxiliary space. All transition directions are `right`, -satisfying `δ_right_of_start` and the transducer discipline vacuously (the -machine never steps). -/ -def emptyOutputTM (n : ℕ) : TM n where - Q := Unit - qstart := () - qhalt := () - δ := fun _ _ _ _ => ((), fun _ => Γw.blank, Γw.blank, .right, fun _ => .right, .right) - δ_right_of_start := by - intro q iHead wHeads oHead - exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ - -/-- The initial (empty) output tape holds the empty output string. -/ -private theorem hasOutput_init_nil : (Tape.init []).HasOutput ([] : List Bool) := by - refine ⟨fun i h => absurd h (by simp), ?_⟩ - exact Tape.init_nil_cells_succ 0 - -/-- `emptyOutputTM` computes the constant empty-string function in zero time. -/ -theorem emptyOutputTM_computesInTime (n : ℕ) : - (emptyOutputTM n).ComputesInTime (fun _ => []) (fun _ => 0) := by - intro x - refine ⟨(emptyOutputTM n).initCfg x, 0, le_refl _, reachesIn.zero, rfl, ?_⟩ - exact hasOutput_init_nil - -/-- `emptyOutputTM` computes the constant empty-string function in zero auxiliary -space: it is a transducer, every reachable configuration is the (halted) initial -one, and that configuration trivially respects the space bound. -/ -theorem emptyOutputTM_computesInSpace (n : ℕ) : - (emptyOutputTM n).ComputesInSpace (fun _ => []) (fun _ => 0) := by - refine ⟨?_, ?_, ?_⟩ - · intro q iHead wHeads oHead - simp [emptyOutputTM] - · intro x c' hreach - have hc' : c' = (emptyOutputTM n).initCfg x := reaches_eq_of_halted rfl hreach - subst hc' - refine ⟨fun i => ?_, ?_⟩ - · simp - · simp - · intro x - exact ⟨(emptyOutputTM n).initCfg x, Relation.ReflTransGen.refl, rfl, hasOutput_init_nil⟩ - --- ════════════════════════════════════════════════════════════════════════ --- ════════════════════════════════════════════════════════════════════════ --- The full compiler theorem (statement; proof is tracked future work) --- ════════════════════════════════════════════════════════════════════════ - -/-- A *loaded start configuration* for the internal, layout-relative compiler -interface. The environment of an in-place program is a list of first-order -`Data` values `env : Fin m → Data`; a `LoadedStart` places entry `j` on the -designated work tape `slot j` (as its balanced-parenthesis serialization -`Data.toBits`) and leaves every other tape blank, with the machine in its start -state. This is the multi-tape analogue of `Cfg.init`: one work tape per program -argument, chosen by the caller through `slot`. -/ -structure LoadedStart {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) - (env : Fin m → Data) (c : Cfg k M.Q) : Prop where - /-- The machine is in its start state. -/ - state : c.state = M.qstart - /-- The dedicated input tape is unused (blank). -/ - input : c.input = Tape.init [] - /-- The output tape starts blank. -/ - output : c.output = Tape.init [] - /-- Environment entry `j` sits on tape `slot j`, serialized via `Data.toBits`. -/ - envTape : ∀ j, c.work (slot j) = Tape.init ((env j).toBits.map Γ.ofBool) - /-- Every non-environment work tape starts blank. -/ - cleanTape : ∀ i, (∀ j, i ≠ slot j) → c.work i = Tape.init [] - -/-- **The internal, layout-relative compiler contract.** `CompilesUnder M slot -res p a b` says the machine `M` implements program `p` for the environment -layout `slot` (argument `j` on work tape `slot j`) with the result deposited on -work tape `res`: for every first-order environment `env` and every RTM -derivation `ProgSem … p (.data result) t s`, starting from any `LoadedStart`, -the machine halts within `a·t + a` steps having written `result.toBits` on tape -`res`, and no reachable configuration moves any work head past cell `b·s + b`. - -Because `Data.toBits` has length `Data.size` (`Data.toBits_length`), the tape -space charged here is exactly the RTM `Data.size` measure, so the space bound -`b·s + b` matches the RTM space `s` up to the constant `b`. This is the -predicate the structural recursion over `InPlace` is proved against; the public -`inPlace_compilesToTM` is the single-argument (`m = 1`) specialization wrapped -with a fixed input-tape ↦ argument-tape prologue and a result-tape ↦ output-tape -epilogue. -/ -def CompilesUnder {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) (res : Fin k) - (p : Prog) (a b : ℕ) : Prop := - ∀ (env : Fin m → Data) (result : Data) (t s : ℕ), - ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → - ∀ c : Cfg k M.Q, LoadedStart M slot env c → - (∃ (c' : Cfg k M.Q) (t' : ℕ), t' ≤ a * t + a ∧ M.reachesIn t' c c' ∧ - M.halted c' ∧ (c'.work res).HasOutput result.toBits) ∧ - (∀ c'', M.reaches c c'' → ∀ i, (c''.work i).head ≤ b * s + b) - -/-- `Compiled m p`: the first-order program `p` compiles, for argument arity -`m`, to *some* Turing machine and tape layout satisfying the layout-relative -contract `CompilesUnder`. This is the codomain of the compiler recursion -`compilesUnder_of_inPlace`, and the shared shape of the per-constructor building -blocks below. -/ -def Compiled (m : ℕ) (p : Prog) : Prop := - ∃ (k : ℕ) (M : TM k) (slot : Fin m → Fin k) (res : Fin k) (a b : ℕ), - CompilesUnder M slot res p a b - -/-- The empty-node writer: a 4-state machine over `m + 1` work tapes. From the -start state it steps all heads right off the left marker, then writes `0` and -`1` on the last (result) work tape, preserving all other tapes by writing back -what they read. This realizes `Prog.empty`, materializing `[false, true]` (the -`Data.toBits` of the empty node) on the result tape in three steps. -/ -def emptyNodeTM (m : ℕ) : TM (m + 1) where - Q := Fin 4 - qstart := 0 - qhalt := 3 - δ := fun q _ wHeads _ => - ( (if q = 0 then 1 else if q = 1 then 2 else 3), - (fun i => if i = Fin.last m - then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) - else (wHeads i).toΓwId), - Γw.blank, - Dir3.right, - (fun _ => Dir3.right), - Dir3.right ) - δ_right_of_start := by - intro q iHead wHeads oHead - exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ - -/-- The configuration reached by one step of `emptyNodeTM` from a state `q`. -/ -def emptyStepOut (m : ℕ) (cc : Cfg (m + 1) (Fin 4)) (q : Fin 4) : Cfg (m + 1) (Fin 4) := - { state := if q = 0 then 1 else if q = 1 then 2 else 3 - input := cc.input.move .right - work := fun i => (cc.work i).writeAndMove - ((if i = Fin.last m - then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) - else ((cc.work i).read).toΓwId) : Γ) .right - output := cc.output.writeAndMove ((Γw.blank : Γ)) .right } - -/-- One step of `emptyNodeTM` from a non-halted state matches `emptyStepOut`. -/ -theorem emptyStep (m : ℕ) (cc : Cfg (m + 1) (emptyNodeTM m).Q) (q : Fin 4) - (hq : cc.state = q) (hq3 : q ≠ 3) : - (emptyNodeTM m).step cc = some (emptyStepOut m cc q) := by - unfold TM.step - rw [if_neg (by rw [hq]; exact hq3)] - subst hq - simp only [emptyNodeTM, emptyStepOut, apply_ite Γw.toΓ] - -/-- One rightward write-and-move advances the head by one. -/ -theorem writeAndMove_right_head (t : Tape) (s : Γ) : - (t.writeAndMove s Dir3.right).head = t.head + 1 := by - simp [Tape.writeAndMove, Tape.move, Tape.write_head] - -/-- A rightward write-and-move leaves the same cells as writing in place. -/ -theorem writeAndMove_right_cells (t : Tape) (s : Γ) : - (t.writeAndMove s Dir3.right).cells = (t.write s).cells := by - simp [Tape.writeAndMove, Tape.move_cells] - -/-- Writing at a nonzero head updates exactly that cell. -/ -theorem write_cells_of_ne_zero {t : Tape} (h : t.head ≠ 0) (s : Γ) : - (t.write s).cells = Function.update t.cells t.head s := by - simp [Tape.write, h] - -/-- **Compiler part — `var i`** (statement only). A variable read compiles: the -machine copies the argument tape `slot i` (when `i < m`, else the empty node) to -the result tape. Matches `ProgSem.var`, whose time and space are the size of the -read value. -/ -theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by - sorry - -/-- **Compiler part — `empty`.** The empty constructor compiles to `emptyNodeTM`, -a 4-state machine that writes the empty node `Data.empty.toBits = [false, true]` -on the result tape in three steps (all heads advance rightward each step). -Matches `ProgSem.empty` (time and space `2`): the run has length `3 ≤ 2·2 + 2` -and every reachable work head stays within `2·2 + 2`. -/ -theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by - refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ - intro env result t s hsem c hstart - cases hsem - have hstate : c.state = (0 : Fin 4) := hstart.state - have hres0 : c.work (Fin.last m) = Tape.init [] := - hstart.cleanTape (Fin.last m) (fun j => (Fin.castSucc_lt_last j).ne') - have hheads0 : ∀ i, (c.work i).head = 0 := by - intro i - refine Fin.lastCases ?_ ?_ i - · rw [hres0]; rfl - · intro j; rw [hstart.envTape j]; rfl - set c1 := emptyStepOut m c 0 with hc1 - set c2 := emptyStepOut m c1 1 with hc2 - set c3 := emptyStepOut m c2 2 with hc3 - have hs0 : (emptyNodeTM m).step c = some c1 := emptyStep m c 0 hstate (by decide) - have hc1state : c1.state = 1 := by rw [hc1]; simp [emptyStepOut] - have hs1 : (emptyNodeTM m).step c1 = some c2 := emptyStep m c1 1 hc1state (by decide) - have hc2state : c2.state = 2 := by rw [hc2]; simp [emptyStepOut] - have hs2 : (emptyNodeTM m).step c2 = some c3 := emptyStep m c2 2 hc2state (by decide) - have hc3state : c3.state = 3 := by rw [hc3]; simp [emptyStepOut] - have htrace : (emptyNodeTM m).reachesIn 3 c c3 := .step hs0 (.step hs1 (.step hs2 .zero)) - -- The result tape after three steps. - set t0 : Tape := Tape.init [] with ht0 - set t1 : Tape := t0.writeAndMove ((Γw.blank : Γ)) Dir3.right with ht1 - set t2 : Tape := t1.writeAndMove ((Γw.zero : Γ)) Dir3.right with ht2 - set t3 : Tape := t2.writeAndMove ((Γw.one : Γ)) Dir3.right with ht3 - have rres : c3.work (Fin.last m) = t3 := by - simp only [hc3, hc2, hc1, emptyStepOut, ht3, ht2, ht1, ht0, hres0] - simp - have hh1 : t1.head = 1 := by rw [ht1, writeAndMove_right_head]; rfl - have hh2 : t2.head = 2 := by rw [ht2, writeAndMove_right_head, hh1] - -- Cells of the result tape. - have hc2cells : t2.cells = Function.update t0.cells 1 ((Γw.zero : Γ)) := by - rw [ht2, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh1]; decide), - hh1, ht1, writeAndMove_right_cells, Tape.write, ht0] - simp - have hc3cells : t3.cells = - Function.update (Function.update t0.cells 1 ((Γw.zero : Γ))) 2 ((Γw.one : Γ)) := by - rw [ht3, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh2]; decide), - hh2, hc2cells] - have hle : (3 : ℕ) ≤ 2 * 2 + 2 := by omega - refine ⟨⟨c3, 3, hle, htrace, ?_, ?_⟩, ?_⟩ - · -- halted - show c3.state = (emptyNodeTM m).qhalt - rw [hc3state]; rfl - · -- the result tape holds `[false, true]` - rw [rres] - have htb : (Data.l []).toBits = [false, true] := by simp - rw [htb, Tape.HasOutput] - refine ⟨?_, ?_⟩ - · intro i hi - rcases i with _ | _ | i - · rw [hc3cells, Function.update_of_ne (by decide), Function.update_self]; rfl - · rw [hc3cells, Function.update_self]; rfl - · simp only [List.length_cons, List.length_nil] at hi; omega - · rw [hc3cells, Function.update_of_ne (by decide), Function.update_of_ne (by decide), ht0] - simp - · -- space bound: every reachable configuration keeps work heads within `2·2 + 2` - have head_c1 : ∀ i, (c1.work i).head = (c.work i).head + 1 := by - intro i; rw [hc1]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ - have head_c2 : ∀ i, (c2.work i).head = (c1.work i).head + 1 := by - intro i; rw [hc2]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ - have head_c3 : ∀ i, (c3.work i).head = (c2.work i).head + 1 := by - intro i; rw [hc3]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ - have B0 : ∀ i, (c.work i).head ≤ 2 * 2 + 2 := fun i => by rw [hheads0 i]; omega - have B1 : ∀ i, (c1.work i).head ≤ 2 * 2 + 2 := fun i => by - rw [head_c1 i, hheads0 i]; omega - have B2 : ∀ i, (c2.work i).head ≤ 2 * 2 + 2 := fun i => by - rw [head_c2 i, head_c1 i, hheads0 i]; omega - have B3 : ∀ i, (c3.work i).head ≤ 2 * 2 + 2 := fun i => by - rw [head_c3 i, head_c2 i, head_c1 i, hheads0 i]; omega - have hc3h : c3.state = (emptyNodeTM m).qhalt := hc3state - have hnone : (emptyNodeTM m).step c3 = none := step_eq_none_iff_halted.mpr hc3h - intro c'' hreach i - rcases Relation.ReflTransGen.cases_head hreach with rfl | ⟨d1, hd1, hr1⟩ - · exact B0 i - · simp only [TM.stepRel] at hd1; rw [hs0] at hd1; injection hd1 with hd1; subst hd1 - rcases Relation.ReflTransGen.cases_head hr1 with rfl | ⟨d2, hd2, hr2⟩ - · exact B1 i - · simp only [TM.stepRel] at hd2; rw [hs1] at hd2; injection hd2 with hd2; subst hd2 - rcases Relation.ReflTransGen.cases_head hr2 with rfl | ⟨d3, hd3, hr3⟩ - · exact B2 i - · simp only [TM.stepRel] at hd3; rw [hs2] at hd3; injection hd3 with hd3; subst hd3 - rcases Relation.ReflTransGen.cases_head hr3 with rfl | ⟨d4, hd4, _⟩ - · exact B3 i - · simp only [TM.stepRel] at hd4; rw [hnone] at hd4; exact absurd hd4 (by simp) - -/-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines -for `h` and `t`, `cons` runs them on disjoint tape banks and prepends the head -value to the tail list on the result tape. Matches `ProgSem.cons` -(time/space add). -/ -theorem compiled_cons {m : ℕ} {h t : Prog} - (ih_h : Compiled m h) (ih_t : Compiled m t) : Compiled m (Prog.cons h t) := by - sorry - -/-- **Compiler part — `elim v emp (fn (fn body))`** (statement only). Given -compiled sub-machines for the scrutinee `v` and the empty branch `emp` at arity -`m`, and for the cons branch `body` at arity `m + 2` (the two fresh tapes hold -the destructured head and tail), `elim` branches on whether `v` is the empty -node. Matches `ProgSem.elim_nil` / `ProgSem.elim_cons`. -/ -theorem compiled_elim {m : ℕ} {v emp body : Prog} - (ih_v : Compiled m v) (ih_emp : Compiled m emp) (ih_body : Compiled (m + 2) body) : - Compiled m (Prog.elim v emp (.fn (.fn body))) := by - sorry - -/-- **Compiler part — `ifEq x y then_ else_`** (statement only). Given compiled -sub-machines for all four arguments at arity `m`, `ifEq` compares the values of -`x` and `y` and runs the matching branch. Matches `ProgSem.ifEq_then` / -`ProgSem.ifEq_else`. -/ -theorem compiled_ifEq {m : ℕ} {x y then_ else_ : Prog} - (ih_x : Compiled m x) (ih_y : Compiled m y) - (ih_then : Compiled m then_) (ih_else : Compiled m else_) : - Compiled m (Prog.ifEq x y then_ else_) := by - sorry - -/-- **Compiler part — `while_ init (fn body)`** (statement only). Given a -compiled sub-machine for `init` at arity `m` and for the loop `body` at arity -`m + 1` (the fresh tape holds the accumulator), `while_` iterates the body on the -accumulator tape until its head is empty. Matches `ProgSem.while_` / -`WhileSem` (which already uses `max` for space, exactly the loop's reuse). -/ -theorem compiled_while {m : ℕ} {init body : Prog} - (ih_init : Compiled m init) (ih_body : Compiled (m + 1) body) : - Compiled m (Prog.while_ init (.fn body)) := by - sorry - -/-- **Compiler part — `app (fn body) arg`** (the in-place `let`; statement only). -Given a compiled sub-machine for `arg` at arity `m` and for `body` at arity -`m + 1`, `app` evaluates `arg` onto a fresh environment tape and then runs -`body`. Matches `ProgSem.app` composed with `AppSem.mk` (running `body` in -`σ ++ [v]`). Nested uses give multi-argument `let`-chains, hence arbitrary -arities. -/ -theorem compiled_app {m : ℕ} {body arg : Prog} - (ih_body : Compiled (m + 1) body) (ih_arg : Compiled m arg) : - Compiled m (Prog.app (.fn body) arg) := by - sorry - -/-- **The internal compiler recursion.** For every argument arity `m`, every -first-order (`InPlace`) program compiles to a Turing machine together with a tape -layout satisfying the layout-relative contract `CompilesUnder`. - -The recursion structure is fully assembled here: induction on the `InPlace` -derivation dispatches each program constructor to its compiler part -(`compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`, -`compiled_ifEq`, `compiled_while`, `compiled_app`), threading the argument arity -so that `elim`/`while_`/`app` compile their body at the extended arity (`m + 2`, -`m + 1`, `m + 1`) that the `σ`-extension of the operational semantics uses. Only -the individual parts carry `sorry`; the assembly below is complete. -/ -theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : - Compiled m p := by - induction hp generalizing m with - | var => exact compiled_var m _ - | empty => exact compiled_empty m - | cons _ _ ih_h ih_t => exact compiled_cons ih_h ih_t - | elim _ _ _ ih_v ih_emp ih_body => exact compiled_elim ih_v ih_emp ih_body - | ifEq _ _ _ _ ih_x ih_y ih_then ih_else => - exact compiled_ifEq ih_x ih_y ih_then ih_else - | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body - | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg - -/-- The tapes a subroutine occupies, indexed uniformly by role: `m` argument -slots, one result slot, and `sc` scratch slots. A `SubroutineLayout` maps this -slot space injectively into the caller's tape bank. -/ -abbrev SubroutineSlot (m sc : ℕ) := Fin m ⊕ Unit ⊕ Fin sc - -/-- **A caller-chosen tape layout** for running an `m`-argument in-place RTM -program as a subroutine on a `Fin k` tape bank using `sc` scratch tapes. As with -the binary-arithmetic subroutines, the caller picks the tapes; a single -injective `place` assigns each slot (argument, result, or scratch) a distinct -physical tape, so the machine can treat them as independent registers. -/ -structure SubroutineLayout (m sc k : ℕ) where - /-- The physical tape each slot occupies. -/ - place : SubroutineSlot m sc → Fin k - /-- Distinct slots occupy distinct tapes. -/ - place_inj : Function.Injective place - -namespace SubroutineLayout - -variable {m sc k : ℕ} (L : SubroutineLayout m sc k) - -/-- The tape variable `j` is read from. -/ -def argIdx (j : Fin m) : Fin k := L.place (.inl j) - -/-- The tape the result is written to. -/ -def resIdx : Fin k := L.place (.inr (.inl ())) - -/-- The `l`-th auxiliary tape the machine may use. -/ -def scratchIdx (l : Fin sc) : Fin k := L.place (.inr (.inr l)) - -/-- Distinct variables use distinct tapes. -/ -theorem argIdx_inj : Function.Injective L.argIdx := fun _ _ h => - Sum.inl_injective (L.place_inj h) - -/-- Distinct scratch slots use distinct tapes. -/ -theorem scratchIdx_inj : Function.Injective L.scratchIdx := fun _ _ h => - Sum.inr_injective (Sum.inr_injective (L.place_inj h)) - -/-- No argument tape coincides with the result tape. -/ -theorem arg_ne_res (j : Fin m) : L.argIdx j ≠ L.resIdx := fun h => by - simpa using L.place_inj h - -/-- No scratch tape coincides with the result tape. -/ -theorem scratch_ne_res (l : Fin sc) : L.scratchIdx l ≠ L.resIdx := fun h => by - simpa using L.place_inj h - -/-- Argument tapes and scratch tapes are disjoint. -/ -theorem arg_ne_scratch (j : Fin m) (l : Fin sc) : L.argIdx j ≠ L.scratchIdx l := - fun h => by simpa using L.place_inj h - -/-- The starting tape assignment expected by a `SubroutineLayout`: environment -entry `j` sits on its argument tape as the balanced-parenthesis serialization -`Data.toBits`, and the result and scratch tapes start blank. Tapes outside the -layout are unconstrained (and preserved as a frame). -/ -def Loaded (env : Fin m → Data) (work : Fin k → Tape) : Prop := - (∀ j, work (L.argIdx j) = Tape.init ((env j).toBits.map Γ.ofBool)) ∧ - work L.resIdx = Tape.init [] ∧ - (∀ l, work (L.scratchIdx l) = Tape.init []) - -end SubroutineLayout - -/-- **The public subroutine contract.** `p.RunsAsSubroutine m` says the -`m`-argument in-place program `p` compiles to a reusable Turing-machine -subroutine: there is a scratch-tape count `sc` and constants `a`, `b` -(depending only on `p`), so that for *any* caller layout `L : SubroutineLayout -m sc k` there is a machine `M : TM k` that, whenever `p` maps `env` to `result` -in RTM time `t` and space `s`, run from a `Loaded` start - -* halts within `a·t + a` steps with `result.toBits` on the result tape - (`HasOutput`), -* leaves **every other tape exactly as it started** (`∀ i ≠ resIdx`): arguments - preserved read-only, scratch restored blank, untouched tapes untouched, and -* keeps all work heads within `b·s + b` auxiliary space. - -Inputs live on the chosen argument work tapes, *not* the dedicated input tape -(which stays blank), so the space charge is over `Data.toBits`; by -`Data.toBits_length` it matches the RTM `Data.size` measure up to `b`. Exposing -`sc` tells the caller how many auxiliary tapes to reserve, and the -"only the result tape changes" frame makes `M` freely composable. -/ -def Prog.RunsAsSubroutine (p : Prog) (m : ℕ) : Prop := - ∃ sc a b : ℕ, ∀ {k : ℕ} (L : SubroutineLayout m sc k), - ∃ M : TM k, ∀ (env : Fin m → Data) (result : Data) (t s : ℕ) - (work₀ : Fin k → Tape), - ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → - L.Loaded env work₀ → - M.HoareTimeSpace - (fun inp work out => inp = Tape.init [] ∧ work = work₀ ∧ out = Tape.init []) - (fun inp work out => inp = Tape.init [] ∧ out = Tape.init [] ∧ - (work L.resIdx).HasOutput result.toBits ∧ - (∀ i, i ≠ L.resIdx → work i = work₀ i)) - (a * t + a) 0 (b * s + b) - /-- **The full in-place RTM → Turing-machine compiler theorem.** Every first-order (`InPlace`) rose tree machine program compiles, at any argument arity `m`, to a reusable tape-indexed Turing-machine subroutine @@ -566,9 +50,9 @@ arity `m`, to a reusable tape-indexed Turing-machine subroutine inputs are serialized via `Data.toBits`, and time/space match the RTM `ProgSem` bounds up to a constant. See `Prog.RunsAsSubroutine` for the precise contract. -The base case `empty` is discharged by `compiled_empty`; the remaining -constructors are tracked in `ROADMAP.md`, track N0. The statement is provided -now so the subroutine interface is fixed; the proof is deferred. -/ +The base case `empty` is discharged by `Compile.Internal.compiled_empty`; the +remaining constructors are tracked in `ROADMAP.md`, track N0. The statement is +provided now so the subroutine interface is fixed; the proof is deferred. -/ theorem inPlace_compilesToTM {m : ℕ} (p : Prog) (hp : InPlace p) : p.RunsAsSubroutine m := by sorry diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean new file mode 100644 index 00000000..5a69ffa6 --- /dev/null +++ b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean @@ -0,0 +1,148 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexitylib.Models.RoseTreeMachine.Prog +import Complexitylib.Models.TuringMachine.Hoare.Space.Defs + +/-! +# Compiling in-place rose tree machine programs to Turing machines — contract + +This module holds the **human-auditable contract** the RTM → TM compiler +establishes: the caller-chosen tape layout and the public subroutine +specification. The proof machinery that discharges the contract lives in +`Complexitylib.Models.RoseTreeMachine.Compile.Internal`, and the final theorem +`inPlace_compilesToTM` lives in `Complexitylib.Models.RoseTreeMachine.Compile`. + +## What "match" means here + +The RTM cost model is faithful to Turing machines only *up to a constant +factor* — the standard notion for cross-model simulation. A compiled machine +computes the *same* binary function as the source program and its time (resp. +space) bound is *dominated by* the program's RTM time (resp. space) bound. + +Two structural facts make this achievable for the `InPlace` fragment: + +- **Result materialization is already paid for.** `ProgSem.size_le` shows every + derivation charges at least the size of the value it produces, in both time + and space, so the O(size) traversal/assembly/copy work a Turing machine must + perform to build a `Data` result is always absorbed (up to a constant). +- **Space is charged generously.** Most `ProgSem` rules *add* the space of + sequential sub-computations (`s₁ + s₂ + …`) where a Turing machine reuses + space and pays only their `max`, so the RTM figure is a valid upper bound. + +## Main definitions + +- `RoseTreeMachine.SubroutineLayout` — a caller-chosen tape layout: a single + injective `place` map assigning each slot (an argument, the result, or a + scratch tape) a distinct physical tape in the caller's bank. Role accessors + `argIdx`/`resIdx`/`scratchIdx` and their pairwise-distinctness follow from + injectivity of `place`. +- `RoseTreeMachine.Prog.RunsAsSubroutine` — the **public subroutine contract**: + the compiled machine, run from a `SubroutineLayout.Loaded` start, halts with + the result on the result tape, frames every other tape (arguments preserved, + scratch restored blank), and matches the RTM time/space bounds up to a + constant. This is what `inPlace_compilesToTM` establishes. +-/ + +namespace Complexity + +namespace RoseTreeMachine + +open Complexity.TM + +/-- The tapes a subroutine occupies, indexed uniformly by role: `m` argument +slots, one result slot, and `sc` scratch slots. A `SubroutineLayout` maps this +slot space injectively into the caller's tape bank. -/ +abbrev SubroutineSlot (m sc : ℕ) := Fin m ⊕ Unit ⊕ Fin sc + +/-- **A caller-chosen tape layout** for running an `m`-argument in-place RTM +program as a subroutine on a `Fin k` tape bank using `sc` scratch tapes. As with +the binary-arithmetic subroutines, the caller picks the tapes; a single +injective `place` assigns each slot (argument, result, or scratch) a distinct +physical tape, so the machine can treat them as independent registers. -/ +structure SubroutineLayout (m sc k : ℕ) where + /-- The physical tape each slot occupies. -/ + place : SubroutineSlot m sc → Fin k + /-- Distinct slots occupy distinct tapes. -/ + place_inj : Function.Injective place + +namespace SubroutineLayout + +variable {m sc k : ℕ} (L : SubroutineLayout m sc k) + +/-- The tape variable `j` is read from. -/ +def argIdx (j : Fin m) : Fin k := L.place (.inl j) + +/-- The tape the result is written to. -/ +def resIdx : Fin k := L.place (.inr (.inl ())) + +/-- The `l`-th auxiliary tape the machine may use. -/ +def scratchIdx (l : Fin sc) : Fin k := L.place (.inr (.inr l)) + +/-- Distinct variables use distinct tapes. -/ +theorem argIdx_inj : Function.Injective L.argIdx := fun _ _ h => + Sum.inl_injective (L.place_inj h) + +/-- Distinct scratch slots use distinct tapes. -/ +theorem scratchIdx_inj : Function.Injective L.scratchIdx := fun _ _ h => + Sum.inr_injective (Sum.inr_injective (L.place_inj h)) + +/-- No argument tape coincides with the result tape. -/ +theorem arg_ne_res (j : Fin m) : L.argIdx j ≠ L.resIdx := fun h => by + simpa using L.place_inj h + +/-- No scratch tape coincides with the result tape. -/ +theorem scratch_ne_res (l : Fin sc) : L.scratchIdx l ≠ L.resIdx := fun h => by + simpa using L.place_inj h + +/-- Argument tapes and scratch tapes are disjoint. -/ +theorem arg_ne_scratch (j : Fin m) (l : Fin sc) : L.argIdx j ≠ L.scratchIdx l := + fun h => by simpa using L.place_inj h + +/-- The starting tape assignment expected by a `SubroutineLayout`: environment +entry `j` sits on its argument tape as the balanced-parenthesis serialization +`Data.toBits`, and the result and scratch tapes start blank. Tapes outside the +layout are unconstrained (and preserved as a frame). -/ +def Loaded (env : Fin m → Data) (work : Fin k → Tape) : Prop := + (∀ j, work (L.argIdx j) = Tape.init ((env j).toBits.map Γ.ofBool)) ∧ + work L.resIdx = Tape.init [] ∧ + (∀ l, work (L.scratchIdx l) = Tape.init []) + +end SubroutineLayout + +/-- **The public subroutine contract.** `p.RunsAsSubroutine m` says the +`m`-argument in-place program `p` compiles to a reusable Turing-machine +subroutine: there is a scratch-tape count `sc` and constants `a`, `b` +(depending only on `p`), so that for *any* caller layout `L : SubroutineLayout +m sc k` there is a machine `M : TM k` that, whenever `p` maps `env` to `result` +in RTM time `t` and space `s`, run from a `Loaded` start + +* halts within `a·t + a` steps with `result.toBits` on the result tape + (`HasOutput`), +* leaves **every other tape exactly as it started** (`∀ i ≠ resIdx`): arguments + preserved read-only, scratch restored blank, untouched tapes untouched, and +* keeps all work heads within `b·s + b` auxiliary space. + +Inputs live on the chosen argument work tapes, *not* the dedicated input tape +(which stays blank), so the space charge is over `Data.toBits`; by +`Data.toBits_length` it matches the RTM `Data.size` measure up to `b`. Exposing +`sc` tells the caller how many auxiliary tapes to reserve, and the +"only the result tape changes" frame makes `M` freely composable. -/ +def Prog.RunsAsSubroutine (p : Prog) (m : ℕ) : Prop := + ∃ sc a b : ℕ, ∀ {k : ℕ} (L : SubroutineLayout m sc k), + ∃ M : TM k, ∀ (env : Fin m → Data) (result : Data) (t s : ℕ) + (work₀ : Fin k → Tape), + ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → + L.Loaded env work₀ → + M.HoareTimeSpace + (fun inp work out => inp = Tape.init [] ∧ work = work₀ ∧ out = Tape.init []) + (fun inp work out => inp = Tape.init [] ∧ out = Tape.init [] ∧ + (work L.resIdx).HasOutput result.toBits ∧ + (∀ i, i ≠ L.resIdx → work i = work₀ i)) + (a * t + a) 0 (b * s + b) + +end RoseTreeMachine + +end Complexity diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean new file mode 100644 index 00000000..79e37f59 --- /dev/null +++ b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean @@ -0,0 +1,413 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ +import Complexitylib.Models.RoseTreeMachine.Compile.Defs +import Complexitylib.Models.RoseTreeMachine.Compile.Internal.EmptyTM +import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput + +/-! +# Compiling in-place rose tree machine programs to Turing machines — internals + +This module holds the **proof machinery** for the RTM → TM compiler: the trivial +empty-output machine, the layout-relative compiler interface +(`LoadedStart` / `CompilesUnder` / `Compiled`), the concrete per-constructor +machines and their compiler parts, and the structural recursion +`compilesUnder_of_inPlace` that assembles them. Correctness is established by the +type checker; the human-auditable contract it discharges lives in +`Complexitylib.Models.RoseTreeMachine.Compile.Defs`, and the final theorem +`inPlace_compilesToTM` in `Complexitylib.Models.RoseTreeMachine.Compile`. + +## Contents + +- `RoseTreeMachine.emptyOutputTM` — the one-state machine that halts immediately + with empty output, with its time/space computation lemmas. +- `RoseTreeMachine.LoadedStart` — the multi-tape analogue of `Cfg.init`: the + starting configuration for `CompilesUnder`, with each argument serialized onto + its designated tape via `Data.toBits`. +- `RoseTreeMachine.CompilesUnder` — the internal, **layout-relative** compiler + contract: a machine implements a program for an environment layout that places + one program argument per work tape (`slot : Fin m → Fin k`) and deposits the + result on a chosen tape, with time/space matched to the RTM `ProgSem` bounds. +- `RoseTreeMachine.compiled_var`, `compiled_empty`, `compiled_cons`, + `compiled_elim`, `compiled_ifEq`, `compiled_while`, `compiled_app` — the + **individual compiler parts**, one per `InPlace` constructor. `compiled_empty` + is proven; each remaining part is stated but still `sorry`: it needs concrete + `Data`-manipulation subroutines over the tape serialization, tracked as future + work in `ROADMAP.md` (track N0). +- `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every + `InPlace` program compiles, for any argument arity, to a machine plus a tape + layout satisfying `CompilesUnder`. The assembly is complete (no `sorry`); it + dispatches each program constructor to its individual part. + +> Note: the `compiled_*` parts use `sorry` (and `compilesUnder_of_inPlace` +> depends on the parts), so `lake build --wfail` and the axiom guard will report +> them until the parts are proved. +-/ + +namespace Complexity +/-- Map a read symbol to a writable symbol, sending the start marker `▷` to +blank. Used by the compiler's machines to write back a symbol they just read +without ever emitting `▷` (which is not a member of the write alphabet). -/ +def Γ.toΓwId : Γ → Γw + | .zero => .zero + | .one => .one + | .blank => .blank + | .start => .blank + +namespace RoseTreeMachine + +open Complexity.TM + +-- ════════════════════════════════════════════════════════════════════════ +-- A halted configuration only reaches itself +-- ════════════════════════════════════════════════════════════════════════ + +/-- A configuration whose state is the halt state has no successors, so the only +configuration it reaches is itself. -/ +private theorem reaches_eq_of_halted {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} + (hh : c.state = tm.qhalt) (h : tm.reaches c c') : c' = c := by + rcases Relation.ReflTransGen.cases_head h with heq | ⟨d, hstep, _⟩ + · exact heq.symm + · exact absurd hstep (by + have hnone : tm.step c = none := step_eq_none_iff_halted.mpr hh + simp [TM.stepRel, hnone]) + +-- ════════════════════════════════════════════════════════════════════════ +-- The trivial machine: halt immediately with empty output +-- ════════════════════════════════════════════════════════════════════════ + +/-- The one-state Turing machine that is halted from the start. Its output tape +is the initial (empty) tape, so it computes the constant empty-string function +in zero steps and zero auxiliary space. All transition directions are `right`, +satisfying `δ_right_of_start` and the transducer discipline vacuously (the +machine never steps). -/ +def emptyOutputTM (n : ℕ) : TM n where + Q := Unit + qstart := () + qhalt := () + δ := fun _ _ _ _ => ((), fun _ => Γw.blank, Γw.blank, .right, fun _ => .right, .right) + δ_right_of_start := by + intro q iHead wHeads oHead + exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ + +/-- The initial (empty) output tape holds the empty output string. -/ +private theorem hasOutput_init_nil : (Tape.init []).HasOutput ([] : List Bool) := by + refine ⟨fun i h => absurd h (by simp), ?_⟩ + exact Tape.init_nil_cells_succ 0 + +/-- `emptyOutputTM` computes the constant empty-string function in zero time. -/ +theorem emptyOutputTM_computesInTime (n : ℕ) : + (emptyOutputTM n).ComputesInTime (fun _ => []) (fun _ => 0) := by + intro x + refine ⟨(emptyOutputTM n).initCfg x, 0, le_refl _, reachesIn.zero, rfl, ?_⟩ + exact hasOutput_init_nil + +/-- `emptyOutputTM` computes the constant empty-string function in zero auxiliary +space: it is a transducer, every reachable configuration is the (halted) initial +one, and that configuration trivially respects the space bound. -/ +theorem emptyOutputTM_computesInSpace (n : ℕ) : + (emptyOutputTM n).ComputesInSpace (fun _ => []) (fun _ => 0) := by + refine ⟨?_, ?_, ?_⟩ + · intro q iHead wHeads oHead + simp [emptyOutputTM] + · intro x c' hreach + have hc' : c' = (emptyOutputTM n).initCfg x := reaches_eq_of_halted rfl hreach + subst hc' + refine ⟨fun i => ?_, ?_⟩ + · simp + · simp + · intro x + exact ⟨(emptyOutputTM n).initCfg x, Relation.ReflTransGen.refl, rfl, hasOutput_init_nil⟩ + +-- ════════════════════════════════════════════════════════════════════════ +-- ════════════════════════════════════════════════════════════════════════ +-- The full compiler theorem (statement; proof is tracked future work) +-- ════════════════════════════════════════════════════════════════════════ + +/-- A *loaded start configuration* for the internal, layout-relative compiler +interface. The environment of an in-place program is a list of first-order +`Data` values `env : Fin m → Data`; a `LoadedStart` places entry `j` on the +designated work tape `slot j` (as its balanced-parenthesis serialization +`Data.toBits`) and leaves every other tape blank, with the machine in its start +state. This is the multi-tape analogue of `Cfg.init`: one work tape per program +argument, chosen by the caller through `slot`. -/ +structure LoadedStart {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) + (env : Fin m → Data) (c : Cfg k M.Q) : Prop where + /-- The machine is in its start state. -/ + state : c.state = M.qstart + /-- The dedicated input tape is unused (blank). -/ + input : c.input = Tape.init [] + /-- The output tape starts blank. -/ + output : c.output = Tape.init [] + /-- Environment entry `j` sits on tape `slot j`, serialized via `Data.toBits`. -/ + envTape : ∀ j, c.work (slot j) = Tape.init ((env j).toBits.map Γ.ofBool) + /-- Every non-environment work tape starts blank. -/ + cleanTape : ∀ i, (∀ j, i ≠ slot j) → c.work i = Tape.init [] + +/-- **The internal, layout-relative compiler contract.** `CompilesUnder M slot +res p a b` says the machine `M` implements program `p` for the environment +layout `slot` (argument `j` on work tape `slot j`) with the result deposited on +work tape `res`: for every first-order environment `env` and every RTM +derivation `ProgSem … p (.data result) t s`, starting from any `LoadedStart`, +the machine halts within `a·t + a` steps having written `result.toBits` on tape +`res`, and no reachable configuration moves any work head past cell `b·s + b`. + +Because `Data.toBits` has length `Data.size` (`Data.toBits_length`), the tape +space charged here is exactly the RTM `Data.size` measure, so the space bound +`b·s + b` matches the RTM space `s` up to the constant `b`. This is the +predicate the structural recursion over `InPlace` is proved against; the public +`inPlace_compilesToTM` is the single-argument (`m = 1`) specialization wrapped +with a fixed input-tape ↦ argument-tape prologue and a result-tape ↦ output-tape +epilogue. -/ +def CompilesUnder {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) (res : Fin k) + (p : Prog) (a b : ℕ) : Prop := + ∀ (env : Fin m → Data) (result : Data) (t s : ℕ), + ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → + ∀ c : Cfg k M.Q, LoadedStart M slot env c → + (∃ (c' : Cfg k M.Q) (t' : ℕ), t' ≤ a * t + a ∧ M.reachesIn t' c c' ∧ + M.halted c' ∧ (c'.work res).HasOutput result.toBits) ∧ + (∀ c'', M.reaches c c'' → ∀ i, (c''.work i).head ≤ b * s + b) + +/-- `Compiled m p`: the first-order program `p` compiles, for argument arity +`m`, to *some* Turing machine and tape layout satisfying the layout-relative +contract `CompilesUnder`. This is the codomain of the compiler recursion +`compilesUnder_of_inPlace`, and the shared shape of the per-constructor building +blocks below. -/ +def Compiled (m : ℕ) (p : Prog) : Prop := + ∃ (k : ℕ) (M : TM k) (slot : Fin m → Fin k) (res : Fin k) (a b : ℕ), + CompilesUnder M slot res p a b + +/-- The empty-node writer: a 4-state machine over `m + 1` work tapes. From the +start state it steps all heads right off the left marker, then writes `0` and +`1` on the last (result) work tape, preserving all other tapes by writing back +what they read. This realizes `Prog.empty`, materializing `[false, true]` (the +`Data.toBits` of the empty node) on the result tape in three steps. -/ +def emptyNodeTM (m : ℕ) : TM (m + 1) where + Q := Fin 4 + qstart := 0 + qhalt := 3 + δ := fun q _ wHeads _ => + ( (if q = 0 then 1 else if q = 1 then 2 else 3), + (fun i => if i = Fin.last m + then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) + else (wHeads i).toΓwId), + Γw.blank, + Dir3.right, + (fun _ => Dir3.right), + Dir3.right ) + δ_right_of_start := by + intro q iHead wHeads oHead + exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ + +/-- The configuration reached by one step of `emptyNodeTM` from a state `q`. -/ +def emptyStepOut (m : ℕ) (cc : Cfg (m + 1) (Fin 4)) (q : Fin 4) : Cfg (m + 1) (Fin 4) := + { state := if q = 0 then 1 else if q = 1 then 2 else 3 + input := cc.input.move .right + work := fun i => (cc.work i).writeAndMove + ((if i = Fin.last m + then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) + else ((cc.work i).read).toΓwId) : Γ) .right + output := cc.output.writeAndMove ((Γw.blank : Γ)) .right } + +/-- One step of `emptyNodeTM` from a non-halted state matches `emptyStepOut`. -/ +theorem emptyStep (m : ℕ) (cc : Cfg (m + 1) (emptyNodeTM m).Q) (q : Fin 4) + (hq : cc.state = q) (hq3 : q ≠ 3) : + (emptyNodeTM m).step cc = some (emptyStepOut m cc q) := by + unfold TM.step + rw [if_neg (by rw [hq]; exact hq3)] + subst hq + simp only [emptyNodeTM, emptyStepOut, apply_ite Γw.toΓ] + +/-- One rightward write-and-move advances the head by one. -/ +theorem writeAndMove_right_head (t : Tape) (s : Γ) : + (t.writeAndMove s Dir3.right).head = t.head + 1 := by + simp [Tape.writeAndMove, Tape.move, Tape.write_head] + +/-- A rightward write-and-move leaves the same cells as writing in place. -/ +theorem writeAndMove_right_cells (t : Tape) (s : Γ) : + (t.writeAndMove s Dir3.right).cells = (t.write s).cells := by + simp [Tape.writeAndMove, Tape.move_cells] + +/-- Writing at a nonzero head updates exactly that cell. -/ +theorem write_cells_of_ne_zero {t : Tape} (h : t.head ≠ 0) (s : Γ) : + (t.write s).cells = Function.update t.cells t.head s := by + simp [Tape.write, h] + +/-- **Compiler part — `var i`** (statement only). A variable read compiles: the +machine copies the argument tape `slot i` (when `i < m`, else the empty node) to +the result tape. Matches `ProgSem.var`, whose time and space are the size of the +read value. -/ +theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by + sorry + +/-- **Compiler part — `empty`.** The empty constructor compiles to `emptyNodeTM`, +a 4-state machine that writes the empty node `Data.empty.toBits = [false, true]` +on the result tape in three steps (all heads advance rightward each step). +Matches `ProgSem.empty` (time and space `2`): the run has length `3 ≤ 2·2 + 2` +and every reachable work head stays within `2·2 + 2`. -/ +theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by + refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ + intro env result t s hsem c hstart + cases hsem + have hstate : c.state = (0 : Fin 4) := hstart.state + have hres0 : c.work (Fin.last m) = Tape.init [] := + hstart.cleanTape (Fin.last m) (fun j => (Fin.castSucc_lt_last j).ne') + have hheads0 : ∀ i, (c.work i).head = 0 := by + intro i + refine Fin.lastCases ?_ ?_ i + · rw [hres0]; rfl + · intro j; rw [hstart.envTape j]; rfl + set c1 := emptyStepOut m c 0 with hc1 + set c2 := emptyStepOut m c1 1 with hc2 + set c3 := emptyStepOut m c2 2 with hc3 + have hs0 : (emptyNodeTM m).step c = some c1 := emptyStep m c 0 hstate (by decide) + have hc1state : c1.state = 1 := by rw [hc1]; simp [emptyStepOut] + have hs1 : (emptyNodeTM m).step c1 = some c2 := emptyStep m c1 1 hc1state (by decide) + have hc2state : c2.state = 2 := by rw [hc2]; simp [emptyStepOut] + have hs2 : (emptyNodeTM m).step c2 = some c3 := emptyStep m c2 2 hc2state (by decide) + have hc3state : c3.state = 3 := by rw [hc3]; simp [emptyStepOut] + have htrace : (emptyNodeTM m).reachesIn 3 c c3 := .step hs0 (.step hs1 (.step hs2 .zero)) + -- The result tape after three steps. + set t0 : Tape := Tape.init [] with ht0 + set t1 : Tape := t0.writeAndMove ((Γw.blank : Γ)) Dir3.right with ht1 + set t2 : Tape := t1.writeAndMove ((Γw.zero : Γ)) Dir3.right with ht2 + set t3 : Tape := t2.writeAndMove ((Γw.one : Γ)) Dir3.right with ht3 + have rres : c3.work (Fin.last m) = t3 := by + simp only [hc3, hc2, hc1, emptyStepOut, ht3, ht2, ht1, ht0, hres0] + simp + have hh1 : t1.head = 1 := by rw [ht1, writeAndMove_right_head]; rfl + have hh2 : t2.head = 2 := by rw [ht2, writeAndMove_right_head, hh1] + -- Cells of the result tape. + have hc2cells : t2.cells = Function.update t0.cells 1 ((Γw.zero : Γ)) := by + rw [ht2, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh1]; decide), + hh1, ht1, writeAndMove_right_cells, Tape.write, ht0] + simp + have hc3cells : t3.cells = + Function.update (Function.update t0.cells 1 ((Γw.zero : Γ))) 2 ((Γw.one : Γ)) := by + rw [ht3, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh2]; decide), + hh2, hc2cells] + have hle : (3 : ℕ) ≤ 2 * 2 + 2 := by omega + refine ⟨⟨c3, 3, hle, htrace, ?_, ?_⟩, ?_⟩ + · -- halted + show c3.state = (emptyNodeTM m).qhalt + rw [hc3state]; rfl + · -- the result tape holds `[false, true]` + rw [rres] + have htb : (Data.l []).toBits = [false, true] := by simp + rw [htb, Tape.HasOutput] + refine ⟨?_, ?_⟩ + · intro i hi + rcases i with _ | _ | i + · rw [hc3cells, Function.update_of_ne (by decide), Function.update_self]; rfl + · rw [hc3cells, Function.update_self]; rfl + · simp only [List.length_cons, List.length_nil] at hi; omega + · rw [hc3cells, Function.update_of_ne (by decide), Function.update_of_ne (by decide), ht0] + simp + · -- space bound: every reachable configuration keeps work heads within `2·2 + 2` + have head_c1 : ∀ i, (c1.work i).head = (c.work i).head + 1 := by + intro i; rw [hc1]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ + have head_c2 : ∀ i, (c2.work i).head = (c1.work i).head + 1 := by + intro i; rw [hc2]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ + have head_c3 : ∀ i, (c3.work i).head = (c2.work i).head + 1 := by + intro i; rw [hc3]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ + have B0 : ∀ i, (c.work i).head ≤ 2 * 2 + 2 := fun i => by rw [hheads0 i]; omega + have B1 : ∀ i, (c1.work i).head ≤ 2 * 2 + 2 := fun i => by + rw [head_c1 i, hheads0 i]; omega + have B2 : ∀ i, (c2.work i).head ≤ 2 * 2 + 2 := fun i => by + rw [head_c2 i, head_c1 i, hheads0 i]; omega + have B3 : ∀ i, (c3.work i).head ≤ 2 * 2 + 2 := fun i => by + rw [head_c3 i, head_c2 i, head_c1 i, hheads0 i]; omega + have hc3h : c3.state = (emptyNodeTM m).qhalt := hc3state + have hnone : (emptyNodeTM m).step c3 = none := step_eq_none_iff_halted.mpr hc3h + intro c'' hreach i + rcases Relation.ReflTransGen.cases_head hreach with rfl | ⟨d1, hd1, hr1⟩ + · exact B0 i + · simp only [TM.stepRel] at hd1; rw [hs0] at hd1; injection hd1 with hd1; subst hd1 + rcases Relation.ReflTransGen.cases_head hr1 with rfl | ⟨d2, hd2, hr2⟩ + · exact B1 i + · simp only [TM.stepRel] at hd2; rw [hs1] at hd2; injection hd2 with hd2; subst hd2 + rcases Relation.ReflTransGen.cases_head hr2 with rfl | ⟨d3, hd3, hr3⟩ + · exact B2 i + · simp only [TM.stepRel] at hd3; rw [hs2] at hd3; injection hd3 with hd3; subst hd3 + rcases Relation.ReflTransGen.cases_head hr3 with rfl | ⟨d4, hd4, _⟩ + · exact B3 i + · simp only [TM.stepRel] at hd4; rw [hnone] at hd4; exact absurd hd4 (by simp) + +/-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines +for `h` and `t`, `cons` runs them on disjoint tape banks and prepends the head +value to the tail list on the result tape. Matches `ProgSem.cons` +(time/space add). -/ +theorem compiled_cons {m : ℕ} {h t : Prog} + (ih_h : Compiled m h) (ih_t : Compiled m t) : Compiled m (Prog.cons h t) := by + sorry + +/-- **Compiler part — `elim v emp (fn (fn body))`** (statement only). Given +compiled sub-machines for the scrutinee `v` and the empty branch `emp` at arity +`m`, and for the cons branch `body` at arity `m + 2` (the two fresh tapes hold +the destructured head and tail), `elim` branches on whether `v` is the empty +node. Matches `ProgSem.elim_nil` / `ProgSem.elim_cons`. -/ +theorem compiled_elim {m : ℕ} {v emp body : Prog} + (ih_v : Compiled m v) (ih_emp : Compiled m emp) (ih_body : Compiled (m + 2) body) : + Compiled m (Prog.elim v emp (.fn (.fn body))) := by + sorry + +/-- **Compiler part — `ifEq x y then_ else_`** (statement only). Given compiled +sub-machines for all four arguments at arity `m`, `ifEq` compares the values of +`x` and `y` and runs the matching branch. Matches `ProgSem.ifEq_then` / +`ProgSem.ifEq_else`. -/ +theorem compiled_ifEq {m : ℕ} {x y then_ else_ : Prog} + (ih_x : Compiled m x) (ih_y : Compiled m y) + (ih_then : Compiled m then_) (ih_else : Compiled m else_) : + Compiled m (Prog.ifEq x y then_ else_) := by + sorry + +/-- **Compiler part — `while_ init (fn body)`** (statement only). Given a +compiled sub-machine for `init` at arity `m` and for the loop `body` at arity +`m + 1` (the fresh tape holds the accumulator), `while_` iterates the body on the +accumulator tape until its head is empty. Matches `ProgSem.while_` / +`WhileSem` (which already uses `max` for space, exactly the loop's reuse). -/ +theorem compiled_while {m : ℕ} {init body : Prog} + (ih_init : Compiled m init) (ih_body : Compiled (m + 1) body) : + Compiled m (Prog.while_ init (.fn body)) := by + sorry + +/-- **Compiler part — `app (fn body) arg`** (the in-place `let`; statement only). +Given a compiled sub-machine for `arg` at arity `m` and for `body` at arity +`m + 1`, `app` evaluates `arg` onto a fresh environment tape and then runs +`body`. Matches `ProgSem.app` composed with `AppSem.mk` (running `body` in +`σ ++ [v]`). Nested uses give multi-argument `let`-chains, hence arbitrary +arities. -/ +theorem compiled_app {m : ℕ} {body arg : Prog} + (ih_body : Compiled (m + 1) body) (ih_arg : Compiled m arg) : + Compiled m (Prog.app (.fn body) arg) := by + sorry + +/-- **The internal compiler recursion.** For every argument arity `m`, every +first-order (`InPlace`) program compiles to a Turing machine together with a tape +layout satisfying the layout-relative contract `CompilesUnder`. + +The recursion structure is fully assembled here: induction on the `InPlace` +derivation dispatches each program constructor to its compiler part +(`compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`, +`compiled_ifEq`, `compiled_while`, `compiled_app`), threading the argument arity +so that `elim`/`while_`/`app` compile their body at the extended arity (`m + 2`, +`m + 1`, `m + 1`) that the `σ`-extension of the operational semantics uses. Only +the individual parts carry `sorry`; the assembly below is complete. -/ +theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : + Compiled m p := by + induction hp generalizing m with + | var => exact compiled_var m _ + | empty => exact compiled_empty m + | cons _ _ ih_h ih_t => exact compiled_cons ih_h ih_t + | elim _ _ _ ih_v ih_emp ih_body => exact compiled_elim ih_v ih_emp ih_body + | ifEq _ _ _ _ ih_x ih_y ih_then ih_else => + exact compiled_ifEq ih_x ih_y ih_then ih_else + | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body + | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg + + +end RoseTreeMachine + +end Complexity diff --git a/Complexitylib/Models/RoseTreeMachine/EmptyTM.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Internal/EmptyTM.lean similarity index 100% rename from Complexitylib/Models/RoseTreeMachine/EmptyTM.lean rename to Complexitylib/Models/RoseTreeMachine/Compile/Internal/EmptyTM.lean From e785e2a8cfcdffc3fcaccd6cdd40bb8d1400671e Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 22 Jul 2026 10:20:19 +0000 Subject: [PATCH 13/16] refactor(rtm): park subroutine tapes at head 1 in compile contract Switch the RTM->TM subroutine contract to the head-1 parked convention. A TM step applies a direction to every tape and idleDir moves a head reading the start marker rightward, so a head-0 Tape.init tape cannot be required to stay unchanged across a step. Loaded now places every layout tape parked at cell 1, and RunsAsSubroutine frames the (unused) input and output tapes as Parked and literally unchanged (inp = inp0, out = out0), with the input head at cell 1 so it fits the input-space allowance. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile/Defs.lean | 38 ++++-- RTM_to_TM.lean | 123 ++++++++++++++++++ 2 files changed, 148 insertions(+), 13 deletions(-) create mode 100644 RTM_to_TM.lean diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean index 5a69ffa6..d115de19 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean @@ -5,6 +5,7 @@ Authors: Christian Reitwiessner -/ import Complexitylib.Models.RoseTreeMachine.Prog import Complexitylib.Models.TuringMachine.Hoare.Space.Defs +import Complexitylib.Models.TuringMachine.Registers /-! # Compiling in-place rose tree machine programs to Turing machines — contract @@ -103,12 +104,17 @@ theorem arg_ne_scratch (j : Fin m) (l : Fin sc) : L.argIdx j ≠ L.scratchIdx l /-- The starting tape assignment expected by a `SubroutineLayout`: environment entry `j` sits on its argument tape as the balanced-parenthesis serialization -`Data.toBits`, and the result and scratch tapes start blank. Tapes outside the -layout are unconstrained (and preserved as a frame). -/ +`Data.toBits`, and the result and scratch tapes start blank. Every layout tape +is **parked** (head at cell 1, just past the `▷` marker): a parked head is +fixed by `idleDir`, so tapes the machine does not touch stay literally +unchanged, and the convention matches the binary-arithmetic subroutines +(e.g. `clearWorkTM`). Tapes outside the layout are unconstrained (and preserved +as a frame). -/ def Loaded (env : Fin m → Data) (work : Fin k → Tape) : Prop := - (∀ j, work (L.argIdx j) = Tape.init ((env j).toBits.map Γ.ofBool)) ∧ - work L.resIdx = Tape.init [] ∧ - (∀ l, work (L.scratchIdx l) = Tape.init []) + (∀ j, work (L.argIdx j) = + (Tape.init ((env j).toBits.map Γ.ofBool)).move Dir3.right) ∧ + work L.resIdx = (Tape.init []).move Dir3.right ∧ + (∀ l, work (L.scratchIdx l) = (Tape.init []).move Dir3.right) end SubroutineLayout @@ -125,20 +131,26 @@ in RTM time `t` and space `s`, run from a `Loaded` start preserved read-only, scratch restored blank, untouched tapes untouched, and * keeps all work heads within `b·s + b` auxiliary space. -Inputs live on the chosen argument work tapes, *not* the dedicated input tape -(which stays blank), so the space charge is over `Data.toBits`; by -`Data.toBits_length` it matches the RTM `Data.size` measure up to `b`. Exposing -`sc` tells the caller how many auxiliary tapes to reserve, and the -"only the result tape changes" frame makes `M` freely composable. -/ +The dedicated input and output tapes are not used by the compiler: the caller +supplies them **parked** (`Parked inp₀`, `Parked out₀`) so the machine leaves +them literally unchanged (`inp = inp₀ ∧ out = out₀`), and the input head starts +at cell 1 (`inp₀.head ≤ 1`) so it fits the `0 + space + 1` input allowance. + +Inputs live on the chosen argument work tapes, *not* the dedicated input tape, +so the space charge is over `Data.toBits`; by `Data.toBits_length` it matches +the RTM `Data.size` measure up to `b`. Exposing `sc` tells the caller how many +auxiliary tapes to reserve, and the "only the result tape changes" frame makes +`M` freely composable. -/ def Prog.RunsAsSubroutine (p : Prog) (m : ℕ) : Prop := ∃ sc a b : ℕ, ∀ {k : ℕ} (L : SubroutineLayout m sc k), ∃ M : TM k, ∀ (env : Fin m → Data) (result : Data) (t s : ℕ) - (work₀ : Fin k → Tape), + (work₀ : Fin k → Tape) (inp₀ out₀ : Tape), ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → L.Loaded env work₀ → + Parked inp₀ → inp₀.head ≤ 1 → Parked out₀ → M.HoareTimeSpace - (fun inp work out => inp = Tape.init [] ∧ work = work₀ ∧ out = Tape.init []) - (fun inp work out => inp = Tape.init [] ∧ out = Tape.init [] ∧ + (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀) + (fun inp work out => inp = inp₀ ∧ out = out₀ ∧ (work L.resIdx).HasOutput result.toBits ∧ (∀ i, i ≠ L.resIdx → work i = work₀ i)) (a * t + a) 0 (b * s + b) diff --git a/RTM_to_TM.lean b/RTM_to_TM.lean new file mode 100644 index 00000000..cee4d48c --- /dev/null +++ b/RTM_to_TM.lean @@ -0,0 +1,123 @@ +/-- + +Sketch of how to simulate an RTM with a TM. + +First we describe how to simulate the RTM with a multi-tape TM. + +From each Prog, we can determine a number of tapes required: + +def tape_count (p : Prog) : ℕ := + match p with + | .var _ => 1 + | .letin val rest => 1 + tape_count val + tape_count rest + | .empty => 1 + | .cons h t => 1 + tape_count h + tape_count t + | .elim v em cs => 5 + tape_count v + tape_count em + tape_count cs + | .eq a b => 1 + tape_count a + tape_count b + | .fold body init list => 5 + tape_count body + tape_count init + tape_count list + | .while_ init body => 5 + tape_count init + tape_count body + +From these tape counts, we can allocate distinct tapes for each Prog. Each prog has a designated +output tape and potentially some helper tapes. We also maintain a mapping from +variable indices to tapes. + +This is how we simulate. Whenever we write to a tape, we first clear it, because it might +still contain data from previous loop iterations. + +var : copy from the tape of the variable to the output tape of the Prog. This should take linear time in the size of the copied data and also linear space in that. + +letin : simulate 'val'. add a new variable to the environment and let it point at the output + tape of 'val'. Then simulate 'rest'. Copy its output to the output tape. + +empty: write '(', ')' to the output tape. + +cons: simulate h and t. write '(' to the output tape, then copy the contents of the output tape +of h, then copy the contents of the output tape of t (but ignore the first symbol). + +elim: simulate v. check if the output take is exactly "()". If yes, simulate em and copy its +output to the output tape of elim. Otherwise, use three auxiliary tapes: We nede to copy +the head and the tail of the output tape of v to two separate tapes. For that, we need to +analyze the parentheses-nesting structure. Prepare an auxiliary tape to count the current nesting +level in unary (you can put single '(' that do not match a closing one). skip the first '(' on +the output tape of v. Then do the following in a loop: copy the current symbol to the head auxiliary tape +and update the nesting level (add a '(' for '(', remove a '(' for ')'). If the nesting level reaches 0 (the tape head on the nesting level tape reads "empty"), we are at the end of the head, so we switch to copying to the tail auxiliary tape: put a `(` on hte tail auxiliary tape and copy over the rest of the 'v' autput tape. After this, we have the head and tail on separate tapes, so we can simulate cs with these tapes added to the variable mapping. After rest terminates, copy its output tape to the outpuut tape of elim. + +eq : simulate a and b. We compare the tape contents by moving over them in parallel. If we find a mismatch, write (()), otherwise write () to the output tape. + +fold: simulate init and list. We maintain an auxiliary tape for the accumulator, which we initialize with the output of init. We also maintain an auxiliary tape for the current element of the list. TODO + +Then we can simulate each Prog on the TM by using the tapes to store the environment and intermediate results. The TM will have a fixed number of tapes equal to the maximum number of tapes needed for any Prog we want to simulate. + +Finally, we can use the fact that multi-tape TMs can be simulated by single-tape TMs with only a polynomial slowdown, to conclude that we can simulate the RTM with a single-tape TM. + +-/ +inductive Prog where + | var (id : Var) + /-- `letin val rest`: evaluate `val`, append the result to `env`, then evaluate `rest`. -/ + | letin (val : Prog) (rest : Prog) + | empty + | cons (h t : Prog) + /-- `elim v em cs`: if `v` evaluates to `empty`, run `em`; otherwise destructure into + `head` and `tail` (both appended to `env`, in that order) and run `cs`. -/ + | elim (v : Prog) (em : Prog) (cs : Prog) + | eq (a b : Prog) + /-- `fold body init list`: `init` and `list` produce starting accumulator and the input + list; `body` runs once per element with `env` extended by `[acc, x]`. -/ + | fold (body : Prog) (init list : Prog) + /-- `while_ init body`: `init` produces the starting accumulator; `body` runs with + `env` extended by the current accumulator. -/ + | while_ (init body : Prog) +deriving Repr + +/-- Evaluates `p` on `env` and returns the result, the time and the space consumption. -/ +def Prog.meteredEval (env : List Data) (p : Prog) : Part (Data × ℕ × ℕ) := + match p with + -- TODO charge for copy? + | .var id => .some (env[(show ℕ from id)]?.getD (Data.l []), 1, 1) + | .letin val rest => do + let (v, t, s) ← val.meteredEval env + let (r, t', s') ← rest.meteredEval (env ++ [v]) + -- TODO charge for copy? + return (r, 1 + t + t', max s s') + | .empty => .some (Data.empty, 1, 1) + | .cons h t => do + let (head, h_t, h_s) ← h.meteredEval env + let (tail, t_t, t_s) ← t.meteredEval env + return (Data.l (head :: tail.asList), 1 + h_t + t_t, max h_s t_s) + | .elim v em cs => do + let (v', t, s) ← v.meteredEval env + match v' with + | Data.l [] => + let (r, t', s') ← em.meteredEval env + return (r, 1 + t + t', max s s') + | Data.l (head :: tail) => + let (r, t', s') ← cs.meteredEval (env ++ [head, Data.l tail]) + return (r, 1 + t + t', max s s') + | .eq a b => do + let (a, a_t, a_s) ← a.meteredEval env + let (b, b_t, b_s) ← b.meteredEval env + (if a == b then Data.l [ Data.l [] ] else Data.l [], 1 + a_t + b_t, 1 + max a_s b_s) + | .fold body init list => do + let (i, i_t, i_s) ← init.meteredEval env + let (l, l_t, l_s) ← list.meteredEval env + l.asList.foldlM + (fun (acc, t, s) el => do + let (acc', b_t, b_s) ← body.meteredEval (env ++ [acc, el]) + return (acc', 1 + t + b_t, max s b_s)) + (i, 1 + i_t + l_t, max i_s l_s) + | .while_ init body => do + let (i, i_t, i_s) ← init.meteredEval env + -- Real while loop: check the halt condition on the current accumulator first. + -- If `acc.asList.headD = []` (empty head), halt and return `acc`. + -- Otherwise run `body` on the accumulator and loop with its result. + let F : ((Data × ℕ × ℕ) → Part (Data × ℕ × ℕ)) → + (Data × ℕ × ℕ) → Part (Data × ℕ × ℕ) := + fun rec d_ts => + let (acc, t, s) := d_ts + if acc.asList.headD (Data.l []) = Data.l [] then + .some (acc, t, s) + else + (body.meteredEval (env ++ [acc])).bind fun (r, b_t, b_s) => + rec (r, t + 1 + b_t, max s b_s) + Part.fix F (i, 1 + i_t, max 1 i_s) + termination_by (sizeOf p, 0) From e8f62d72988e273bb3ba083e9ac7d926c520e4da Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 22 Jul 2026 10:41:39 +0000 Subject: [PATCH 14/16] feat(rtm): prove compiled_var compiler part MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove the var-read compiler part of the RTM->TM compiler. When the de Bruijn index is in range (i < m) the argument value is already serialized on tape i, so the identity layout with res = slot i lets the trivial emptyOutputTM halt immediately with the value in place; when i >= m the read falls off the environment and yields the empty node, produced by emptyNodeTM. Factor the empty-node machine's run into a shared emptyNode_compilesUnder lemma (generalized to time/space bounds t,s >= 2 via ProgSem.size_le) now used by both compiled_empty and compiled_var, and add hasOutput_init_map (a tape initialized from w.map Γ.ofBool holds w as output). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../RoseTreeMachine/Compile/Internal.lean | 110 ++++++++++++++---- 1 file changed, 88 insertions(+), 22 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean index 79e37f59..754ea311 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean @@ -97,6 +97,14 @@ private theorem hasOutput_init_nil : (Tape.init []).HasOutput ([] : List Bool) : refine ⟨fun i h => absurd h (by simp), ?_⟩ exact Tape.init_nil_cells_succ 0 +/-- A tape initialized from the serialization `w.map Γ.ofBool` holds `w` as its +output: cell `i + 1` reads back bit `i`, and the cell past the end is blank. -/ +private theorem hasOutput_init_map (w : List Bool) : + (Tape.init (w.map Γ.ofBool)).HasOutput w := by + refine ⟨fun i hi => ?_, ?_⟩ + · simp [Tape.init_cells_succ, List.getElem?_map, List.getElem?_eq_getElem hi] + · simp [Tape.init_cells_succ] + /-- `emptyOutputTM` computes the constant empty-string function in zero time. -/ theorem emptyOutputTM_computesInTime (n : ℕ) : (emptyOutputTM n).ComputesInTime (fun _ => []) (fun _ => 0) := by @@ -235,22 +243,19 @@ theorem write_cells_of_ne_zero {t : Tape} (h : t.head ≠ 0) (s : Γ) : (t.write s).cells = Function.update t.cells t.head s := by simp [Tape.write, h] -/-- **Compiler part — `var i`** (statement only). A variable read compiles: the -machine copies the argument tape `slot i` (when `i < m`, else the empty node) to -the result tape. Matches `ProgSem.var`, whose time and space are the size of the -read value. -/ -theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by - sorry - -/-- **Compiler part — `empty`.** The empty constructor compiles to `emptyNodeTM`, -a 4-state machine that writes the empty node `Data.empty.toBits = [false, true]` -on the result tape in three steps (all heads advance rightward each step). -Matches `ProgSem.empty` (time and space `2`): the run has length `3 ≤ 2·2 + 2` -and every reachable work head stays within `2·2 + 2`. -/ -theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by - refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ - intro env result t s hsem c hstart - cases hsem +/-- **The empty-node machine's contract.** For any loaded start, `emptyNodeTM m` +runs three steps to leave the empty node `Data.empty.toBits = [false, true]` on +the result tape (`Fin.last m`) and keeps every reachable work head within +`2·s + 2` (resp. finishes within `2·t + 2` steps) whenever the RTM time and +space bounds `t`, `s` are at least the empty node's size `2`. This is shared by +`compiled_empty` and the empty-node case of `compiled_var`. -/ +private theorem emptyNode_compilesUnder {m t s : ℕ} (ht : 2 ≤ t) (hs : 2 ≤ s) + {env : Fin m → Data} {c : Cfg (m + 1) (emptyNodeTM m).Q} + (hstart : LoadedStart (emptyNodeTM m) Fin.castSucc env c) : + (∃ (c' : Cfg (m + 1) (emptyNodeTM m).Q) (t' : ℕ), t' ≤ 2 * t + 2 ∧ + (emptyNodeTM m).reachesIn t' c c' ∧ (emptyNodeTM m).halted c' ∧ + (c'.work (Fin.last m)).HasOutput (Data.l []).toBits) ∧ + (∀ c'', (emptyNodeTM m).reaches c c'' → ∀ i, (c''.work i).head ≤ 2 * s + 2) := by have hstate : c.state = (0 : Fin 4) := hstart.state have hres0 : c.work (Fin.last m) = Tape.init [] := hstart.cleanTape (Fin.last m) (fun j => (Fin.castSucc_lt_last j).ne') @@ -288,7 +293,7 @@ theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by Function.update (Function.update t0.cells 1 ((Γw.zero : Γ))) 2 ((Γw.one : Γ)) := by rw [ht3, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh2]; decide), hh2, hc2cells] - have hle : (3 : ℕ) ≤ 2 * 2 + 2 := by omega + have hle : (3 : ℕ) ≤ 2 * t + 2 := by omega refine ⟨⟨c3, 3, hle, htrace, ?_, ?_⟩, ?_⟩ · -- halted show c3.state = (emptyNodeTM m).qhalt @@ -305,19 +310,19 @@ theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by · simp only [List.length_cons, List.length_nil] at hi; omega · rw [hc3cells, Function.update_of_ne (by decide), Function.update_of_ne (by decide), ht0] simp - · -- space bound: every reachable configuration keeps work heads within `2·2 + 2` + · -- space bound: every reachable configuration keeps work heads within `2·s + 2` have head_c1 : ∀ i, (c1.work i).head = (c.work i).head + 1 := by intro i; rw [hc1]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ have head_c2 : ∀ i, (c2.work i).head = (c1.work i).head + 1 := by intro i; rw [hc2]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ have head_c3 : ∀ i, (c3.work i).head = (c2.work i).head + 1 := by intro i; rw [hc3]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ - have B0 : ∀ i, (c.work i).head ≤ 2 * 2 + 2 := fun i => by rw [hheads0 i]; omega - have B1 : ∀ i, (c1.work i).head ≤ 2 * 2 + 2 := fun i => by + have B0 : ∀ i, (c.work i).head ≤ 2 * s + 2 := fun i => by rw [hheads0 i]; omega + have B1 : ∀ i, (c1.work i).head ≤ 2 * s + 2 := fun i => by rw [head_c1 i, hheads0 i]; omega - have B2 : ∀ i, (c2.work i).head ≤ 2 * 2 + 2 := fun i => by + have B2 : ∀ i, (c2.work i).head ≤ 2 * s + 2 := fun i => by rw [head_c2 i, head_c1 i, hheads0 i]; omega - have B3 : ∀ i, (c3.work i).head ≤ 2 * 2 + 2 := fun i => by + have B3 : ∀ i, (c3.work i).head ≤ 2 * s + 2 := fun i => by rw [head_c3 i, head_c2 i, head_c1 i, hheads0 i]; omega have hc3h : c3.state = (emptyNodeTM m).qhalt := hc3state have hnone : (emptyNodeTM m).step c3 = none := step_eq_none_iff_halted.mpr hc3h @@ -335,6 +340,67 @@ theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by · exact B3 i · simp only [TM.stepRel] at hd4; rw [hnone] at hd4; exact absurd hd4 (by simp) +/-- **Compiler part — `var i`.** A variable read compiles with the value already +serialized on a tape: when `i < m` the argument tape `slot i` holds +`(env i).toBits`, so the identity layout (`res = slot i`) lets the trivial +`emptyOutputTM` halt immediately with the value in place; when `i ≥ m` the read +falls off the environment and yields the empty node, produced by `emptyNodeTM`. +Matches `ProgSem.var`, whose time and space are the size of the read value. -/ +theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by + by_cases hi : i < m + · -- `i < m`: the value is already on tape `i`; halt immediately with `res = i`. + refine ⟨m, emptyOutputTM m, id, ⟨i, hi⟩, 0, 0, ?_⟩ + intro env result t s hsem c hstart + have hval := hsem.value_det _ _ _ + (ProgSem.var (σ := List.ofFn (fun j => Value.data (env j))) (i := i)) + have hσ : (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty + = Value.data (env ⟨i, hi⟩) := by + simp [hi] + rw [hσ] at hval + have hres : result = env ⟨i, hi⟩ := by injection hval + have hhalt : (emptyOutputTM m).halted c := hstart.state + refine ⟨⟨c, 0, by omega, reachesIn.zero, hhalt, ?_⟩, ?_⟩ + · show (c.work (⟨i, hi⟩ : Fin m)).HasOutput result.toBits + have he := hstart.envTape ⟨i, hi⟩ + simp only [id_eq] at he + rw [hres, he] + exact hasOutput_init_map _ + · intro c'' hreach i' + have hc'' : c'' = c := reaches_eq_of_halted hhalt hreach + subst hc'' + have he := hstart.envTape i' + simp only [id_eq] at he + rw [he]; simp + · -- `i ≥ m`: the read falls off the environment, yielding the empty node. + push Not at hi + refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ + intro env result t s hsem c hstart + have hval := hsem.value_det _ _ _ + (ProgSem.var (σ := List.ofFn (fun j => Value.data (env j))) (i := i)) + have hσ : (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty + = Value.empty := by + simp [Nat.not_lt.mpr hi] + rw [hσ] at hval + have hres : result = Data.l [] := by simpa [Value.empty] using hval + subst hres + have hsize := hsem.size_le + exact emptyNode_compilesUnder (by simpa using hsize.1) (by simpa using hsize.2) hstart + +/-- **Compiler part — `empty`.** The empty constructor compiles to `emptyNodeTM`, +a 4-state machine that writes the empty node `Data.empty.toBits = [false, true]` +on the result tape in three steps (all heads advance rightward each step). +Matches `ProgSem.empty` (time and space `2`): the run has length `3 ≤ 2·2 + 2` +and every reachable work head stays within `2·2 + 2`. -/ +theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by + refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ + intro env result t s hsem c hstart + have hres : result = Data.l [] := by + have hval := hsem.value_det _ _ _ ProgSem.empty + simpa [Value.empty] using hval + subst hres + have hsize := hsem.size_le + exact emptyNode_compilesUnder (by simpa using hsize.1) (by simpa using hsize.2) hstart + /-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines for `h` and `t`, `cons` runs them on disjoint tape banks and prepends the head value to the tail list on the result tape. Matches `ProgSem.cons` From 8d64bef7acd1816ab2425a6e8b2190c55eb740e5 Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 22 Jul 2026 14:07:16 +0000 Subject: [PATCH 15/16] refactor(rtm): reframe compiler recursion onto RunsAsSubroutine MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Retarget the InPlace RTM to TM compiler recursion at the composable public subroutine contract `Prog.RunsAsSubroutine`, replacing the reaches-based `CompilesUnder`/`LoadedStart` machinery. `Compiled` is now a thin alias for `RunsAsSubroutine`, so the per-constructor part signatures and the recursion `compilesUnder_of_inPlace` are unchanged, and the surface theorem `inPlace_compilesToTM` is now wired to that recursion instead of an independent `sorry`. Prove `compiled_empty` in the new contract via `TM.emptyTM` (the parked-tape layout subroutine), with `HoareTimeSpace.consequence` fitting its constant time/additive space into the `a*t+a` / `b*s+b` budget. Strengthen `SubroutineLayout.Loaded` so every bank tape is parked at head 1 (`Parked ∧ head ≤ 1`), not just the layout tapes: parkedness is required for the "every non-result tape is preserved" frame to hold across idle steps, and the head-1 bound keeps non-layout tapes inside the `b*s+b` space budget from the initial configuration. Layout tapes already sit at head 1, so this only pins down the caller's spare tapes. `compiled_var`/`cons`/`elim`/`ifEq`/`while`/`app` remain `sorry` pending the `Data`-manipulation subroutines (copy-with-rewind, merge, equality comparator). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../Models/RoseTreeMachine/Compile.lean | 16 +- .../Models/RoseTreeMachine/Compile/Defs.lean | 13 +- .../RoseTreeMachine/Compile/Internal.lean | 437 +++--------------- 3 files changed, 80 insertions(+), 386 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile.lean b/Complexitylib/Models/RoseTreeMachine/Compile.lean index d201a59a..b361ae1c 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile.lean @@ -31,12 +31,12 @@ lives in `Complexitylib.Models.RoseTreeMachine.Compile.Internal`. This is the first verified slice of the `InPlace`-RTM → TM compiler. The compiler recursion `Compile.Internal.compilesUnder_of_inPlace` is fully -decomposed into per-constructor parts; of those, `compiled_empty` is proven and -each remaining part is stated but still `sorry` (it needs concrete -`Data`-manipulation subroutines over the tape serialization, tracked in -`ROADMAP.md`, track N0). The final theorem below is therefore also `sorry` for -now, so `lake build --wfail` and the axiom guard will report it until the parts -are proved. +decomposed into per-constructor parts and `inPlace_compilesToTM` is wired to it; +of those parts, `compiled_empty` is proven and each remaining part is stated but +still `sorry` (it needs concrete `Data`-manipulation subroutines over the tape +serialization, tracked in `ROADMAP.md`, track N0). The final theorem below +therefore transitively depends on `sorry`, so `lake build --wfail` and the axiom +guard will report it until the parts are proved. -/ namespace Complexity @@ -54,8 +54,8 @@ The base case `empty` is discharged by `Compile.Internal.compiled_empty`; the remaining constructors are tracked in `ROADMAP.md`, track N0. The statement is provided now so the subroutine interface is fixed; the proof is deferred. -/ theorem inPlace_compilesToTM {m : ℕ} (p : Prog) (hp : InPlace p) : - p.RunsAsSubroutine m := by - sorry + p.RunsAsSubroutine m := + compilesUnder_of_inPlace p hp end RoseTreeMachine diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean index d115de19..fa7d39fe 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile/Defs.lean @@ -108,13 +108,20 @@ entry `j` sits on its argument tape as the balanced-parenthesis serialization is **parked** (head at cell 1, just past the `▷` marker): a parked head is fixed by `idleDir`, so tapes the machine does not touch stay literally unchanged, and the convention matches the binary-arithmetic subroutines -(e.g. `clearWorkTM`). Tapes outside the layout are unconstrained (and preserved -as a frame). -/ +(e.g. `clearWorkTM`). Tapes outside the layout carry no prescribed contents, but +they too must be **parked at head 1** (`Parked ∧ head ≤ 1`): parkedness makes the +machine leave them literally unchanged (a head resting past a stray `▷` could be +mutated across an idle step), and the head-1 bound keeps them inside the `b·s+b` +auxiliary-space budget from the very first configuration. Every layout tape +already sits at head 1, so this constrains only the caller's spare tapes. This +makes the "every non-result tape is preserved" frame in `RunsAsSubroutine` hold +for the whole bank, not just the layout tapes. -/ def Loaded (env : Fin m → Data) (work : Fin k → Tape) : Prop := (∀ j, work (L.argIdx j) = (Tape.init ((env j).toBits.map Γ.ofBool)).move Dir3.right) ∧ work L.resIdx = (Tape.init []).move Dir3.right ∧ - (∀ l, work (L.scratchIdx l) = (Tape.init []).move Dir3.right) + (∀ l, work (L.scratchIdx l) = (Tape.init []).move Dir3.right) ∧ + (∀ i, Parked (work i) ∧ (work i).head ≤ 1) end SubroutineLayout diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean index 754ea311..03e4f5ac 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean @@ -5,404 +5,92 @@ Authors: Christian Reitwiessner -/ import Complexitylib.Models.RoseTreeMachine.Compile.Defs import Complexitylib.Models.RoseTreeMachine.Compile.Internal.EmptyTM -import Complexitylib.Models.TuringMachine.Subroutines.CopyOutput /-! # Compiling in-place rose tree machine programs to Turing machines — internals -This module holds the **proof machinery** for the RTM → TM compiler: the trivial -empty-output machine, the layout-relative compiler interface -(`LoadedStart` / `CompilesUnder` / `Compiled`), the concrete per-constructor -machines and their compiler parts, and the structural recursion -`compilesUnder_of_inPlace` that assembles them. Correctness is established by the -type checker; the human-auditable contract it discharges lives in +This module holds the **proof machinery** for the RTM → TM compiler: the +per-constructor compiler parts and the structural recursion +`compilesUnder_of_inPlace` that assembles them into the public subroutine +contract `Prog.RunsAsSubroutine`. Correctness is established by the type checker; +the human-auditable contract it discharges lives in `Complexitylib.Models.RoseTreeMachine.Compile.Defs`, and the final theorem `inPlace_compilesToTM` in `Complexitylib.Models.RoseTreeMachine.Compile`. ## Contents -- `RoseTreeMachine.emptyOutputTM` — the one-state machine that halts immediately - with empty output, with its time/space computation lemmas. -- `RoseTreeMachine.LoadedStart` — the multi-tape analogue of `Cfg.init`: the - starting configuration for `CompilesUnder`, with each argument serialized onto - its designated tape via `Data.toBits`. -- `RoseTreeMachine.CompilesUnder` — the internal, **layout-relative** compiler - contract: a machine implements a program for an environment layout that places - one program argument per work tape (`slot : Fin m → Fin k`) and deposits the - result on a chosen tape, with time/space matched to the RTM `ProgSem` bounds. +- `RoseTreeMachine.Compiled` — a thin alias for `Prog.RunsAsSubroutine`, the + shared codomain of the compiler recursion and the per-constructor parts. - `RoseTreeMachine.compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`, `compiled_ifEq`, `compiled_while`, `compiled_app` — the **individual compiler parts**, one per `InPlace` constructor. `compiled_empty` - is proven; each remaining part is stated but still `sorry`: it needs concrete - `Data`-manipulation subroutines over the tape serialization, tracked as future - work in `ROADMAP.md` (track N0). + is proven (it reuses `TM.emptyTM`, the parked-tape layout subroutine that + materializes the empty node's serialization `[false, true]`); each remaining + part is stated but still `sorry`: it needs concrete `Data`-manipulation + subroutines over the tape serialization, tracked as future work in + `ROADMAP.md` (track N0). - `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every - `InPlace` program compiles, for any argument arity, to a machine plus a tape - layout satisfying `CompilesUnder`. The assembly is complete (no `sorry`); it - dispatches each program constructor to its individual part. + `InPlace` program compiles, for any argument arity, to a subroutine satisfying + `Prog.RunsAsSubroutine`. The assembly is complete (no `sorry`); it dispatches + each program constructor to its individual part. -> Note: the `compiled_*` parts use `sorry` (and `compilesUnder_of_inPlace` -> depends on the parts), so `lake build --wfail` and the axiom guard will report -> them until the parts are proved. +> Note: the `compiled_*` parts other than `compiled_empty` use `sorry` (and +> `compilesUnder_of_inPlace` depends on them), so `lake build --wfail` and the +> axiom guard will report them until the parts are proved. -/ namespace Complexity -/-- Map a read symbol to a writable symbol, sending the start marker `▷` to -blank. Used by the compiler's machines to write back a symbol they just read -without ever emitting `▷` (which is not a member of the write alphabet). -/ -def Γ.toΓwId : Γ → Γw - | .zero => .zero - | .one => .one - | .blank => .blank - | .start => .blank namespace RoseTreeMachine open Complexity.TM --- ════════════════════════════════════════════════════════════════════════ --- A halted configuration only reaches itself --- ════════════════════════════════════════════════════════════════════════ - -/-- A configuration whose state is the halt state has no successors, so the only -configuration it reaches is itself. -/ -private theorem reaches_eq_of_halted {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} - (hh : c.state = tm.qhalt) (h : tm.reaches c c') : c' = c := by - rcases Relation.ReflTransGen.cases_head h with heq | ⟨d, hstep, _⟩ - · exact heq.symm - · exact absurd hstep (by - have hnone : tm.step c = none := step_eq_none_iff_halted.mpr hh - simp [TM.stepRel, hnone]) - --- ════════════════════════════════════════════════════════════════════════ --- The trivial machine: halt immediately with empty output --- ════════════════════════════════════════════════════════════════════════ - -/-- The one-state Turing machine that is halted from the start. Its output tape -is the initial (empty) tape, so it computes the constant empty-string function -in zero steps and zero auxiliary space. All transition directions are `right`, -satisfying `δ_right_of_start` and the transducer discipline vacuously (the -machine never steps). -/ -def emptyOutputTM (n : ℕ) : TM n where - Q := Unit - qstart := () - qhalt := () - δ := fun _ _ _ _ => ((), fun _ => Γw.blank, Γw.blank, .right, fun _ => .right, .right) - δ_right_of_start := by - intro q iHead wHeads oHead - exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ - -/-- The initial (empty) output tape holds the empty output string. -/ -private theorem hasOutput_init_nil : (Tape.init []).HasOutput ([] : List Bool) := by - refine ⟨fun i h => absurd h (by simp), ?_⟩ - exact Tape.init_nil_cells_succ 0 - -/-- A tape initialized from the serialization `w.map Γ.ofBool` holds `w` as its -output: cell `i + 1` reads back bit `i`, and the cell past the end is blank. -/ -private theorem hasOutput_init_map (w : List Bool) : - (Tape.init (w.map Γ.ofBool)).HasOutput w := by - refine ⟨fun i hi => ?_, ?_⟩ - · simp [Tape.init_cells_succ, List.getElem?_map, List.getElem?_eq_getElem hi] - · simp [Tape.init_cells_succ] - -/-- `emptyOutputTM` computes the constant empty-string function in zero time. -/ -theorem emptyOutputTM_computesInTime (n : ℕ) : - (emptyOutputTM n).ComputesInTime (fun _ => []) (fun _ => 0) := by - intro x - refine ⟨(emptyOutputTM n).initCfg x, 0, le_refl _, reachesIn.zero, rfl, ?_⟩ - exact hasOutput_init_nil - -/-- `emptyOutputTM` computes the constant empty-string function in zero auxiliary -space: it is a transducer, every reachable configuration is the (halted) initial -one, and that configuration trivially respects the space bound. -/ -theorem emptyOutputTM_computesInSpace (n : ℕ) : - (emptyOutputTM n).ComputesInSpace (fun _ => []) (fun _ => 0) := by - refine ⟨?_, ?_, ?_⟩ - · intro q iHead wHeads oHead - simp [emptyOutputTM] - · intro x c' hreach - have hc' : c' = (emptyOutputTM n).initCfg x := reaches_eq_of_halted rfl hreach - subst hc' - refine ⟨fun i => ?_, ?_⟩ - · simp - · simp - · intro x - exact ⟨(emptyOutputTM n).initCfg x, Relation.ReflTransGen.refl, rfl, hasOutput_init_nil⟩ - --- ════════════════════════════════════════════════════════════════════════ --- ════════════════════════════════════════════════════════════════════════ --- The full compiler theorem (statement; proof is tracked future work) --- ════════════════════════════════════════════════════════════════════════ - -/-- A *loaded start configuration* for the internal, layout-relative compiler -interface. The environment of an in-place program is a list of first-order -`Data` values `env : Fin m → Data`; a `LoadedStart` places entry `j` on the -designated work tape `slot j` (as its balanced-parenthesis serialization -`Data.toBits`) and leaves every other tape blank, with the machine in its start -state. This is the multi-tape analogue of `Cfg.init`: one work tape per program -argument, chosen by the caller through `slot`. -/ -structure LoadedStart {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) - (env : Fin m → Data) (c : Cfg k M.Q) : Prop where - /-- The machine is in its start state. -/ - state : c.state = M.qstart - /-- The dedicated input tape is unused (blank). -/ - input : c.input = Tape.init [] - /-- The output tape starts blank. -/ - output : c.output = Tape.init [] - /-- Environment entry `j` sits on tape `slot j`, serialized via `Data.toBits`. -/ - envTape : ∀ j, c.work (slot j) = Tape.init ((env j).toBits.map Γ.ofBool) - /-- Every non-environment work tape starts blank. -/ - cleanTape : ∀ i, (∀ j, i ≠ slot j) → c.work i = Tape.init [] - -/-- **The internal, layout-relative compiler contract.** `CompilesUnder M slot -res p a b` says the machine `M` implements program `p` for the environment -layout `slot` (argument `j` on work tape `slot j`) with the result deposited on -work tape `res`: for every first-order environment `env` and every RTM -derivation `ProgSem … p (.data result) t s`, starting from any `LoadedStart`, -the machine halts within `a·t + a` steps having written `result.toBits` on tape -`res`, and no reachable configuration moves any work head past cell `b·s + b`. - -Because `Data.toBits` has length `Data.size` (`Data.toBits_length`), the tape -space charged here is exactly the RTM `Data.size` measure, so the space bound -`b·s + b` matches the RTM space `s` up to the constant `b`. This is the -predicate the structural recursion over `InPlace` is proved against; the public -`inPlace_compilesToTM` is the single-argument (`m = 1`) specialization wrapped -with a fixed input-tape ↦ argument-tape prologue and a result-tape ↦ output-tape -epilogue. -/ -def CompilesUnder {k m : ℕ} (M : TM k) (slot : Fin m → Fin k) (res : Fin k) - (p : Prog) (a b : ℕ) : Prop := - ∀ (env : Fin m → Data) (result : Data) (t s : ℕ), - ProgSem (List.ofFn (fun j => Value.data (env j))) p (Value.data result) t s → - ∀ c : Cfg k M.Q, LoadedStart M slot env c → - (∃ (c' : Cfg k M.Q) (t' : ℕ), t' ≤ a * t + a ∧ M.reachesIn t' c c' ∧ - M.halted c' ∧ (c'.work res).HasOutput result.toBits) ∧ - (∀ c'', M.reaches c c'' → ∀ i, (c''.work i).head ≤ b * s + b) - /-- `Compiled m p`: the first-order program `p` compiles, for argument arity -`m`, to *some* Turing machine and tape layout satisfying the layout-relative -contract `CompilesUnder`. This is the codomain of the compiler recursion -`compilesUnder_of_inPlace`, and the shared shape of the per-constructor building -blocks below. -/ -def Compiled (m : ℕ) (p : Prog) : Prop := - ∃ (k : ℕ) (M : TM k) (slot : Fin m → Fin k) (res : Fin k) (a b : ℕ), - CompilesUnder M slot res p a b - -/-- The empty-node writer: a 4-state machine over `m + 1` work tapes. From the -start state it steps all heads right off the left marker, then writes `0` and -`1` on the last (result) work tape, preserving all other tapes by writing back -what they read. This realizes `Prog.empty`, materializing `[false, true]` (the -`Data.toBits` of the empty node) on the result tape in three steps. -/ -def emptyNodeTM (m : ℕ) : TM (m + 1) where - Q := Fin 4 - qstart := 0 - qhalt := 3 - δ := fun q _ wHeads _ => - ( (if q = 0 then 1 else if q = 1 then 2 else 3), - (fun i => if i = Fin.last m - then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) - else (wHeads i).toΓwId), - Γw.blank, - Dir3.right, - (fun _ => Dir3.right), - Dir3.right ) - δ_right_of_start := by - intro q iHead wHeads oHead - exact ⟨fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩ - -/-- The configuration reached by one step of `emptyNodeTM` from a state `q`. -/ -def emptyStepOut (m : ℕ) (cc : Cfg (m + 1) (Fin 4)) (q : Fin 4) : Cfg (m + 1) (Fin 4) := - { state := if q = 0 then 1 else if q = 1 then 2 else 3 - input := cc.input.move .right - work := fun i => (cc.work i).writeAndMove - ((if i = Fin.last m - then (if q = 1 then Γw.zero else if q = 2 then Γw.one else Γw.blank) - else ((cc.work i).read).toΓwId) : Γ) .right - output := cc.output.writeAndMove ((Γw.blank : Γ)) .right } - -/-- One step of `emptyNodeTM` from a non-halted state matches `emptyStepOut`. -/ -theorem emptyStep (m : ℕ) (cc : Cfg (m + 1) (emptyNodeTM m).Q) (q : Fin 4) - (hq : cc.state = q) (hq3 : q ≠ 3) : - (emptyNodeTM m).step cc = some (emptyStepOut m cc q) := by - unfold TM.step - rw [if_neg (by rw [hq]; exact hq3)] - subst hq - simp only [emptyNodeTM, emptyStepOut, apply_ite Γw.toΓ] - -/-- One rightward write-and-move advances the head by one. -/ -theorem writeAndMove_right_head (t : Tape) (s : Γ) : - (t.writeAndMove s Dir3.right).head = t.head + 1 := by - simp [Tape.writeAndMove, Tape.move, Tape.write_head] - -/-- A rightward write-and-move leaves the same cells as writing in place. -/ -theorem writeAndMove_right_cells (t : Tape) (s : Γ) : - (t.writeAndMove s Dir3.right).cells = (t.write s).cells := by - simp [Tape.writeAndMove, Tape.move_cells] - -/-- Writing at a nonzero head updates exactly that cell. -/ -theorem write_cells_of_ne_zero {t : Tape} (h : t.head ≠ 0) (s : Γ) : - (t.write s).cells = Function.update t.cells t.head s := by - simp [Tape.write, h] - -/-- **The empty-node machine's contract.** For any loaded start, `emptyNodeTM m` -runs three steps to leave the empty node `Data.empty.toBits = [false, true]` on -the result tape (`Fin.last m`) and keeps every reachable work head within -`2·s + 2` (resp. finishes within `2·t + 2` steps) whenever the RTM time and -space bounds `t`, `s` are at least the empty node's size `2`. This is shared by -`compiled_empty` and the empty-node case of `compiled_var`. -/ -private theorem emptyNode_compilesUnder {m t s : ℕ} (ht : 2 ≤ t) (hs : 2 ≤ s) - {env : Fin m → Data} {c : Cfg (m + 1) (emptyNodeTM m).Q} - (hstart : LoadedStart (emptyNodeTM m) Fin.castSucc env c) : - (∃ (c' : Cfg (m + 1) (emptyNodeTM m).Q) (t' : ℕ), t' ≤ 2 * t + 2 ∧ - (emptyNodeTM m).reachesIn t' c c' ∧ (emptyNodeTM m).halted c' ∧ - (c'.work (Fin.last m)).HasOutput (Data.l []).toBits) ∧ - (∀ c'', (emptyNodeTM m).reaches c c'' → ∀ i, (c''.work i).head ≤ 2 * s + 2) := by - have hstate : c.state = (0 : Fin 4) := hstart.state - have hres0 : c.work (Fin.last m) = Tape.init [] := - hstart.cleanTape (Fin.last m) (fun j => (Fin.castSucc_lt_last j).ne') - have hheads0 : ∀ i, (c.work i).head = 0 := by - intro i - refine Fin.lastCases ?_ ?_ i - · rw [hres0]; rfl - · intro j; rw [hstart.envTape j]; rfl - set c1 := emptyStepOut m c 0 with hc1 - set c2 := emptyStepOut m c1 1 with hc2 - set c3 := emptyStepOut m c2 2 with hc3 - have hs0 : (emptyNodeTM m).step c = some c1 := emptyStep m c 0 hstate (by decide) - have hc1state : c1.state = 1 := by rw [hc1]; simp [emptyStepOut] - have hs1 : (emptyNodeTM m).step c1 = some c2 := emptyStep m c1 1 hc1state (by decide) - have hc2state : c2.state = 2 := by rw [hc2]; simp [emptyStepOut] - have hs2 : (emptyNodeTM m).step c2 = some c3 := emptyStep m c2 2 hc2state (by decide) - have hc3state : c3.state = 3 := by rw [hc3]; simp [emptyStepOut] - have htrace : (emptyNodeTM m).reachesIn 3 c c3 := .step hs0 (.step hs1 (.step hs2 .zero)) - -- The result tape after three steps. - set t0 : Tape := Tape.init [] with ht0 - set t1 : Tape := t0.writeAndMove ((Γw.blank : Γ)) Dir3.right with ht1 - set t2 : Tape := t1.writeAndMove ((Γw.zero : Γ)) Dir3.right with ht2 - set t3 : Tape := t2.writeAndMove ((Γw.one : Γ)) Dir3.right with ht3 - have rres : c3.work (Fin.last m) = t3 := by - simp only [hc3, hc2, hc1, emptyStepOut, ht3, ht2, ht1, ht0, hres0] - simp - have hh1 : t1.head = 1 := by rw [ht1, writeAndMove_right_head]; rfl - have hh2 : t2.head = 2 := by rw [ht2, writeAndMove_right_head, hh1] - -- Cells of the result tape. - have hc2cells : t2.cells = Function.update t0.cells 1 ((Γw.zero : Γ)) := by - rw [ht2, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh1]; decide), - hh1, ht1, writeAndMove_right_cells, Tape.write, ht0] - simp - have hc3cells : t3.cells = - Function.update (Function.update t0.cells 1 ((Γw.zero : Γ))) 2 ((Γw.one : Γ)) := by - rw [ht3, writeAndMove_right_cells, write_cells_of_ne_zero (by rw [hh2]; decide), - hh2, hc2cells] - have hle : (3 : ℕ) ≤ 2 * t + 2 := by omega - refine ⟨⟨c3, 3, hle, htrace, ?_, ?_⟩, ?_⟩ - · -- halted - show c3.state = (emptyNodeTM m).qhalt - rw [hc3state]; rfl - · -- the result tape holds `[false, true]` - rw [rres] - have htb : (Data.l []).toBits = [false, true] := by simp - rw [htb, Tape.HasOutput] - refine ⟨?_, ?_⟩ - · intro i hi - rcases i with _ | _ | i - · rw [hc3cells, Function.update_of_ne (by decide), Function.update_self]; rfl - · rw [hc3cells, Function.update_self]; rfl - · simp only [List.length_cons, List.length_nil] at hi; omega - · rw [hc3cells, Function.update_of_ne (by decide), Function.update_of_ne (by decide), ht0] - simp - · -- space bound: every reachable configuration keeps work heads within `2·s + 2` - have head_c1 : ∀ i, (c1.work i).head = (c.work i).head + 1 := by - intro i; rw [hc1]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ - have head_c2 : ∀ i, (c2.work i).head = (c1.work i).head + 1 := by - intro i; rw [hc2]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ - have head_c3 : ∀ i, (c3.work i).head = (c2.work i).head + 1 := by - intro i; rw [hc3]; simp only [emptyStepOut]; exact writeAndMove_right_head _ _ - have B0 : ∀ i, (c.work i).head ≤ 2 * s + 2 := fun i => by rw [hheads0 i]; omega - have B1 : ∀ i, (c1.work i).head ≤ 2 * s + 2 := fun i => by - rw [head_c1 i, hheads0 i]; omega - have B2 : ∀ i, (c2.work i).head ≤ 2 * s + 2 := fun i => by - rw [head_c2 i, head_c1 i, hheads0 i]; omega - have B3 : ∀ i, (c3.work i).head ≤ 2 * s + 2 := fun i => by - rw [head_c3 i, head_c2 i, head_c1 i, hheads0 i]; omega - have hc3h : c3.state = (emptyNodeTM m).qhalt := hc3state - have hnone : (emptyNodeTM m).step c3 = none := step_eq_none_iff_halted.mpr hc3h - intro c'' hreach i - rcases Relation.ReflTransGen.cases_head hreach with rfl | ⟨d1, hd1, hr1⟩ - · exact B0 i - · simp only [TM.stepRel] at hd1; rw [hs0] at hd1; injection hd1 with hd1; subst hd1 - rcases Relation.ReflTransGen.cases_head hr1 with rfl | ⟨d2, hd2, hr2⟩ - · exact B1 i - · simp only [TM.stepRel] at hd2; rw [hs1] at hd2; injection hd2 with hd2; subst hd2 - rcases Relation.ReflTransGen.cases_head hr2 with rfl | ⟨d3, hd3, hr3⟩ - · exact B2 i - · simp only [TM.stepRel] at hd3; rw [hs2] at hd3; injection hd3 with hd3; subst hd3 - rcases Relation.ReflTransGen.cases_head hr3 with rfl | ⟨d4, hd4, _⟩ - · exact B3 i - · simp only [TM.stepRel] at hd4; rw [hnone] at hd4; exact absurd hd4 (by simp) - -/-- **Compiler part — `var i`.** A variable read compiles with the value already -serialized on a tape: when `i < m` the argument tape `slot i` holds -`(env i).toBits`, so the identity layout (`res = slot i`) lets the trivial -`emptyOutputTM` halt immediately with the value in place; when `i ≥ m` the read -falls off the environment and yields the empty node, produced by `emptyNodeTM`. -Matches `ProgSem.var`, whose time and space are the size of the read value. -/ -theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by - by_cases hi : i < m - · -- `i < m`: the value is already on tape `i`; halt immediately with `res = i`. - refine ⟨m, emptyOutputTM m, id, ⟨i, hi⟩, 0, 0, ?_⟩ - intro env result t s hsem c hstart - have hval := hsem.value_det _ _ _ - (ProgSem.var (σ := List.ofFn (fun j => Value.data (env j))) (i := i)) - have hσ : (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty - = Value.data (env ⟨i, hi⟩) := by - simp [hi] - rw [hσ] at hval - have hres : result = env ⟨i, hi⟩ := by injection hval - have hhalt : (emptyOutputTM m).halted c := hstart.state - refine ⟨⟨c, 0, by omega, reachesIn.zero, hhalt, ?_⟩, ?_⟩ - · show (c.work (⟨i, hi⟩ : Fin m)).HasOutput result.toBits - have he := hstart.envTape ⟨i, hi⟩ - simp only [id_eq] at he - rw [hres, he] - exact hasOutput_init_map _ - · intro c'' hreach i' - have hc'' : c'' = c := reaches_eq_of_halted hhalt hreach - subst hc'' - have he := hstart.envTape i' - simp only [id_eq] at he - rw [he]; simp - · -- `i ≥ m`: the read falls off the environment, yielding the empty node. - push Not at hi - refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ - intro env result t s hsem c hstart - have hval := hsem.value_det _ _ _ - (ProgSem.var (σ := List.ofFn (fun j => Value.data (env j))) (i := i)) - have hσ : (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty - = Value.empty := by - simp [Nat.not_lt.mpr hi] - rw [hσ] at hval - have hres : result = Data.l [] := by simpa [Value.empty] using hval - subst hres - have hsize := hsem.size_le - exact emptyNode_compilesUnder (by simpa using hsize.1) (by simpa using hsize.2) hstart - -/-- **Compiler part — `empty`.** The empty constructor compiles to `emptyNodeTM`, -a 4-state machine that writes the empty node `Data.empty.toBits = [false, true]` -on the result tape in three steps (all heads advance rightward each step). -Matches `ProgSem.empty` (time and space `2`): the run has length `3 ≤ 2·2 + 2` -and every reachable work head stays within `2·2 + 2`. -/ +`m`, to a reusable tape-indexed Turing-machine subroutine. This is a thin alias +for the public contract `Prog.RunsAsSubroutine`; it names the shared codomain of +the compiler recursion `compilesUnder_of_inPlace` and the per-constructor +building blocks below. -/ +def Compiled (m : ℕ) (p : Prog) : Prop := p.RunsAsSubroutine m + +/-- **Compiler part — `empty`.** The empty constructor compiles to `TM.emptyTM`, +the parked-tape layout subroutine that clears the result tape and writes the +empty node's serialization `[false, true] = (Data.l []).toBits` onto it, leaving +every other tape literally unchanged. `ProgSem.empty` fixes the RTM cost at +`t = s = 2`, so the machine's constant time and additive space fit the +`a·t + a` / `b·s + b` budget with `a = clearWorkTimeBound 0 + 3` and `b = a + 1`. -/ theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by - refine ⟨m + 1, emptyNodeTM m, Fin.castSucc, Fin.last m, 2, 2, ?_⟩ - intro env result t s hsem c hstart - have hres : result = Data.l [] := by - have hval := hsem.value_det _ _ _ ProgSem.empty - simpa [Value.empty] using hval - subst hres - have hsize := hsem.size_le - exact emptyNode_compilesUnder (by simpa using hsize.1) (by simpa using hsize.2) hstart + refine ⟨0, clearWorkTimeBound 0 + 1 + 2, 1 + (clearWorkTimeBound 0 + 1 + 2), ?_⟩ + intro k L + refine ⟨emptyTM L.resIdx, ?_⟩ + intro env result t s work₀ inp₀ out₀ hsem hloaded hinpP hinpHead houtP + obtain ⟨_, hres, _, hpark⟩ := hloaded + cases hsem + have htarget : + work₀ L.resIdx = (Tape.init (([] : List Bool).map Γ.ofBool)).move Dir3.right := by + simpa using hres + have hinitial : + ({ state := (emptyTM L.resIdx).qstart + input := inp₀ + work := work₀ + output := out₀ } : + Cfg k (emptyTM L.resIdx).Q).WithinAuxSpace 0 1 := + ⟨fun i => (hpark i).2, by show inp₀.head ≤ 0 + 1 + 1; omega⟩ + have key := emptyTM_hoareTimeSpace L.resIdx [] 0 1 inp₀ work₀ out₀ htarget + hinpP (fun i _ => (hpark i).1) houtP hinitial + simp only [List.length_nil] at key + refine key.consequence (fun _ _ _ h => h) ?_ (by omega) (le_refl _) (by omega) + rintro inp work out ⟨hi, hframe, hacc, ho⟩ + exact ⟨hi, ho, by simpa using hacc, hframe⟩ + +/-- **Compiler part — `var i`** (statement only). Reading environment variable +`i` copies the value on argument tape `i` (for `i < m`) to the result tape, or +materializes the empty node (for `i ≥ m`, where the read falls off the +environment). Matches `ProgSem.var`. -/ +theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by + sorry /-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines -for `h` and `t`, `cons` runs them on disjoint tape banks and prepends the head +for `h` and `t`, `cons` runs them on a shared tape bank and prepends the head value to the tail list on the result tape. Matches `ProgSem.cons` (time/space add). -/ theorem compiled_cons {m : ℕ} {h t : Prog} @@ -451,8 +139,8 @@ theorem compiled_app {m : ℕ} {body arg : Prog} sorry /-- **The internal compiler recursion.** For every argument arity `m`, every -first-order (`InPlace`) program compiles to a Turing machine together with a tape -layout satisfying the layout-relative contract `CompilesUnder`. +first-order (`InPlace`) program compiles to a reusable tape-indexed Turing +machine subroutine satisfying `Prog.RunsAsSubroutine`. The recursion structure is fully assembled here: induction on the `InPlace` derivation dispatches each program constructor to its compiler part @@ -473,7 +161,6 @@ theorem compilesUnder_of_inPlace {m : ℕ} (p : Prog) (hp : InPlace p) : | while_ _ _ ih_init ih_body => exact compiled_while ih_init ih_body | app _ _ ih_body ih_arg => exact compiled_app ih_body ih_arg - end RoseTreeMachine end Complexity From c9dc27dc41b6c19d8d698c97a8ec31594544b4d9 Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 22 Jul 2026 14:56:26 +0000 Subject: [PATCH 16/16] feat(rtm): prove compiled_var compiler part MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove the `var i` case of the RTM→TM compiler. For `i < m` the machine copies argument tape `i` to the result tape via `copyWorkToWorkTM` and restores the argument tape with `rewindWorkTM`; for `i ≥ m` it falls back to `emptyTM` to materialize the empty node. The copy/rewind pair adds only linear time and no extra space beyond the copied value, so the composed Hoare time/space contract fits the `a·t + a` / `b·s + b` subroutine budget with `a = clearWorkTimeBound 0 + 5`, `b = a + 1`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .../RoseTreeMachine/Compile/Internal.lean | 175 ++++++++++++++++-- 1 file changed, 162 insertions(+), 13 deletions(-) diff --git a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean index 03e4f5ac..6eb42750 100644 --- a/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean +++ b/Complexitylib/Models/RoseTreeMachine/Compile/Internal.lean @@ -5,6 +5,7 @@ Authors: Christian Reitwiessner -/ import Complexitylib.Models.RoseTreeMachine.Compile.Defs import Complexitylib.Models.RoseTreeMachine.Compile.Internal.EmptyTM +import Complexitylib.Models.TuringMachine.Subroutines.CopyWorkOutput /-! # Compiling in-place rose tree machine programs to Turing machines — internals @@ -24,19 +25,22 @@ the human-auditable contract it discharges lives in - `RoseTreeMachine.compiled_var`, `compiled_empty`, `compiled_cons`, `compiled_elim`, `compiled_ifEq`, `compiled_while`, `compiled_app` — the **individual compiler parts**, one per `InPlace` constructor. `compiled_empty` - is proven (it reuses `TM.emptyTM`, the parked-tape layout subroutine that - materializes the empty node's serialization `[false, true]`); each remaining - part is stated but still `sorry`: it needs concrete `Data`-manipulation - subroutines over the tape serialization, tracked as future work in - `ROADMAP.md` (track N0). + and `compiled_var` are proven: `compiled_empty` reuses `TM.emptyTM` (the + parked-tape layout subroutine that materializes the empty node's serialization + `[false, true]`), and `compiled_var` copies argument tape `i` to the result + tape via `TM.copyWorkToWorkTM` then restores it with `TM.rewindWorkTM` (falling + back to `TM.emptyTM` when `i ≥ m`). Each remaining part is stated but still + `sorry`: it needs concrete `Data`-manipulation subroutines over the tape + serialization, tracked as future work in `ROADMAP.md` (track N0). - `RoseTreeMachine.compilesUnder_of_inPlace` — **the internal recursion**: every `InPlace` program compiles, for any argument arity, to a subroutine satisfying `Prog.RunsAsSubroutine`. The assembly is complete (no `sorry`); it dispatches each program constructor to its individual part. -> Note: the `compiled_*` parts other than `compiled_empty` use `sorry` (and -> `compilesUnder_of_inPlace` depends on them), so `lake build --wfail` and the -> axiom guard will report them until the parts are proved. +> Note: the `compiled_*` parts other than `compiled_empty` and `compiled_var` +> use `sorry` (and `compilesUnder_of_inPlace` depends on them), so +> `lake build --wfail` and the axiom guard will report them until the parts are +> proved. -/ namespace Complexity @@ -82,12 +86,157 @@ theorem compiled_empty (m : ℕ) : Compiled m Prog.empty := by rintro inp work out ⟨hi, hframe, hacc, ho⟩ exact ⟨hi, ho, by simpa using hacc, hframe⟩ -/-- **Compiler part — `var i`** (statement only). Reading environment variable -`i` copies the value on argument tape `i` (for `i < m`) to the result tape, or -materializes the empty node (for `i ≥ m`, where the read falls off the -environment). Matches `ProgSem.var`. -/ +/-- **Compiler part — `var i`.** Reading environment variable `i` copies the +value on argument tape `i` (for `i < m`) to the result tape via +`TM.copyWorkToWorkTM`, then restores the argument tape with `TM.rewindWorkTM`; +for `i ≥ m` (where the read falls off the environment) it materializes the empty +node with `TM.emptyTM`. Matches `ProgSem.var`. The copy/rewind pair adds only +linear time and no extra space beyond the copied value, fitting the `a·t + a` / +`b·s + b` budget with `a = clearWorkTimeBound 0 + 5` and `b = a + 1`. -/ theorem compiled_var (m i : ℕ) : Compiled m (Prog.var i) := by - sorry + refine ⟨0, clearWorkTimeBound 0 + 5, clearWorkTimeBound 0 + 6, ?_⟩ + intro k L + by_cases hi : i < m + · -- copy argument tape i to the result tape, then rewind the argument tape + set src := L.argIdx ⟨i, hi⟩ with hsrc + set dst := L.resIdx with hdst + have hne : src ≠ dst := L.arg_ne_res ⟨i, hi⟩ + refine ⟨seqTM (copyWorkToWorkTM src dst) (rewindWorkTM src), ?_⟩ + intro env result t s work₀ inp₀ out₀ hsem hloaded hinpP hinpHead houtP + obtain ⟨hargs, hres, hscratch, hpark⟩ := hloaded + -- identify the result value with argument `i` + have hval : Value.data result + = (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty := + hsem.value_det _ _ _ ProgSem.var + simp only [List.getElem?_ofFn, hi, dif_pos, Option.getD_some] at hval + have hresult : result = env ⟨i, hi⟩ := by + simpa using hval + subst hresult + set x := (env ⟨i, hi⟩).toBits with hx + set source := (Tape.init (x.map Γ.ofBool)).move Dir3.right with hsource + have hsrc_source : work₀ src = source := by rw [hsrc, hargs, hsource, hx] + have hsource_head : source.head = 1 := by rw [hsource]; simp [Tape.move] + have hsource_out : source.HasOutput x := by + have := Tape.init_move_right_hasBinaryString x + exact ⟨this.2.1, this.2.2 x.length le_rfl⟩ + have hsource_cells0 : source.cells 0 = Γ.start := by + rw [hsource]; simp [Tape.move, Tape.init] + have hsource_nostart : ∀ j, j ≥ 1 → source.cells j ≠ Γ.start := by + intro j hj + obtain ⟨p, rfl⟩ : ∃ p, j = p + 1 := ⟨j - 1, by omega⟩ + have hbs := Tape.init_move_right_hasBinaryString x + rw [hsource] + by_cases hp : p < x.length + · rw [hbs.2.1 p hp]; cases (x[p]'hp) <;> simp [Γ.ofBool] + · rw [hbs.2.2 p (by omega)]; simp + -- copy-phase frame predicate + set Pc : Tape → (Fin k → Tape) → Tape → Prop := + fun inp work out => inp = inp₀ ∧ out = out₀ ∧ + (∀ j, j ≠ src → j ≠ dst → work j = work₀ j) with hPc + have hcopy := copyWorkToWorkTM_hoareTime_frame_of_hasOutput src dst hne x source + (P := Pc) + (by + rintro inp work out inp' work' out' ⟨hi1, hi2, hi3⟩ _ _ _ _ _ hii hoo hframe + exact ⟨by rw [hii, hi1], by rw [hoo, hi2], + fun j hj1 hj2 => by rw [hframe j hj1 hj2]; exact hi3 j hj1 hj2⟩) + -- rewind-phase frame predicate + set Pr : Tape → (Fin k → Tape) → Tape → Prop := + fun inp work out => inp = inp₀ ∧ out = out₀ ∧ + (work dst).HasOutput x ∧ (work src).cells = source.cells ∧ + (∀ j, j ≠ src → j ≠ dst → work j = work₀ j) with hPr + have hrewind := rewindWorkTM_hoareTime_frame src (x.length + 1) + (P := Pr) + (by + rintro inp work out inp' work' out' ⟨hi1, hi2, hi3, hi4, hi5⟩ + hcells hhead hframe hii houtc houth + refine ⟨by rw [hii, hi1], ?_, ?_, ?_, ?_⟩ + · rw [hi2] at houtc houth; exact Tape.ext houth houtc + · rw [hframe dst hne.symm]; exact hi3 + · rw [hcells]; exact hi4 + · intro j hj1 hj2; rw [hframe j hj1]; exact hi5 j hj1 hj2) + -- compose + have hcomp := seqTM_hoareTime (copyWorkToWorkTM src dst) (rewindWorkTM src) + hcopy ?_ hrewind + · -- convert to time-space and fit the budget + have hsize := hsem.size_le + rw [Value.size_data] at hsize + obtain ⟨hst, hss⟩ := hsize + have hxlen : x.length = (env ⟨i, hi⟩).size := by rw [hx]; exact (env ⟨i, hi⟩).toBits_length + have hHT : (seqTM (copyWorkToWorkTM src dst) (rewindWorkTM src)).HoareTime + (fun inp work out => inp = inp₀ ∧ work = work₀ ∧ out = out₀) + (fun inp work out => inp = inp₀ ∧ out = out₀ ∧ + (work L.resIdx).HasOutput (env ⟨i, hi⟩).toBits ∧ + (∀ j, j ≠ L.resIdx → work j = work₀ j)) + (x.length + 1 + 1 + (x.length + 1 + 2)) := by + refine hcomp.consequence ?_ ?_ le_rfl + · rintro inp work out ⟨rfl, rfl, rfl⟩ + exact ⟨hsrc_source, hsource_head, hsource_out, + by rw [hdst]; exact hres, hinpP.read_ne_start, houtP.read_ne_start, + houtP.1, fun j _ _ => ⟨(hpark j).1.read_ne_start, (hpark j).1.1⟩, + rfl, rfl, fun _ _ _ => rfl⟩ + · rintro inp work out ⟨hhead1, hpr1, hpr2, hpr3, hpr4, hpr5⟩ + refine ⟨hpr1, hpr2, by rw [← hdst]; exact hpr3, ?_⟩ + intro j hj + by_cases hjs : j = src + · subst hjs + rw [hsrc_source] + exact Tape.ext (hhead1.trans hsource_head.symm) hpr4 + · exact hpr5 j hjs (by rw [hdst]; exact hj) + have hHTS := hHT.toHoareTimeSpace (inputLength := 0) (initialSpace := 1) + (by rintro inp work out ⟨rfl, rfl, rfl⟩ + exact ⟨fun j => (hpark j).2, by show inp.head ≤ 0 + 1 + 1; omega⟩) + refine hHTS.consequence (fun _ _ _ h => h) (fun _ _ _ h => h) ?_ (le_refl _) ?_ + · have hPt : 2 * t ≤ (clearWorkTimeBound 0 + 5) * t := by gcongr; omega + omega + · have hPs : 2 * s ≤ (clearWorkTimeBound 0 + 6) * s := by gcongr; omega + omega + · -- boundary transition: all reads ≠ start, so the transition is the identity + rintro inp work out ⟨hc1, hc2, hc3, hc4, hc5, hpc1, hpc2, hpc3⟩ + have hwork_ns : ∀ j, (work j).read ≠ Γ.start := by + intro j + by_cases hjs : j = src + · subst hjs; rw [Tape.read, hc2, hc3.2]; decide + · by_cases hjd : j = dst + · subst hjd; rw [hc4.read_blank]; decide + · rw [hpc3 j hjs hjd]; exact (hpark j).1.read_ne_start + have hinp_ns : inp.read ≠ Γ.start := by rw [hpc1]; exact hinpP.read_ne_start + have hout_ns : out.read ≠ Γ.start := by rw [hpc2]; exact houtP.read_ne_start + obtain ⟨hti, htw, hto⟩ := + phaseTransition_eq_self_of_reads_ne_start hinp_ns hwork_ns hout_ns + rw [hti, htw, hto] + refine ⟨by rw [hc1]; exact hsource_cells0, + fun j hj => by rw [hc1]; exact hsource_nostart j hj, hc2.le, hinp_ns, hout_ns, + by rw [hpc2]; exact houtP.1, ?_, hpc1, hpc2, hc4.hasOutput, hc1, hpc3⟩ + intro j hjs + by_cases hjd : j = dst + · subst hjd; exact ⟨by rw [hc4.read_blank]; decide, by rw [hc4.1]; omega⟩ + · rw [hpc3 j hjs hjd]; exact ⟨(hpark j).1.read_ne_start, (hpark j).1.1⟩ + · -- i ≥ m : the read falls off the environment; materialize the empty node + refine ⟨emptyTM L.resIdx, ?_⟩ + intro env result t s work₀ inp₀ out₀ hsem hloaded hinpP hinpHead houtP + obtain ⟨_, hres, _, hpark⟩ := hloaded + have hval : Value.data result + = (List.ofFn (fun j => Value.data (env j)))[i]?.getD Value.empty := + hsem.value_det _ _ _ ProgSem.var + rw [List.getElem?_ofFn, dif_neg hi, Option.getD_none] at hval + injection hval with hresult + subst hresult + have htarget : + work₀ L.resIdx = (Tape.init (([] : List Bool).map Γ.ofBool)).move Dir3.right := by + simpa using hres + have hinitial : + ({ state := (emptyTM L.resIdx).qstart + input := inp₀ + work := work₀ + output := out₀ } : + Cfg k (emptyTM L.resIdx).Q).WithinAuxSpace 0 1 := + ⟨fun i => (hpark i).2, by show inp₀.head ≤ 0 + 1 + 1; omega⟩ + have key := emptyTM_hoareTimeSpace L.resIdx [] 0 1 inp₀ work₀ out₀ htarget + hinpP (fun i _ => (hpark i).1) houtP hinitial + simp only [List.length_nil] at key + refine key.consequence (fun _ _ _ h => h) ?_ (by omega) (le_refl _) (by omega) + rintro inp work out ⟨hi', hframe, hacc, ho⟩ + exact ⟨hi', ho, by simpa using hacc, hframe⟩ /-- **Compiler part — `cons h t`** (statement only). Given compiled sub-machines for `h` and `t`, `cons` runs them on a shared tape bank and prepends the head