feat: Bitstring encodings

Complexitylib.lean

@@ -6,6 +6,7 @@ Authors: Samuel Schlesinger
 
 module
 public import Complexitylib.Models
+public import Complexitylib.Encoding
 public import Complexitylib.Asymptotics
 public import Complexitylib.TimeConstructible
 public import Complexitylib.Classes

Complexitylib/Classes/NP/Internal/PairBuildTM.lean

@@ -1023,7 +1023,7 @@ private theorem pairBuild_copyY_loop {k : ℕ} (yIdx pIdx : Fin k)
 /-- Helper: `pair (b :: xs) y = b :: b :: pair xs y`. -/
 private theorem pair_build_cons_eq (b : Bool) (xs y : List Bool) :
     pair (b :: xs) y = b :: b :: pair xs y := by
-  simp [pair, List.append_assoc]
+  simp [pair]
 
 /-- Shift lemma: accessing `pair (b :: xs) y` at index `k+2` is the same as
     accessing `pair xs y` at index `k`. -/

Complexitylib/Classes/PPoly/Advice.lean

@@ -45,7 +45,7 @@ namespace Advice
 input. -/
 theorem fixedPrefix_append (a : Advice) (x : List Bool) :
     a.fixedPrefix x.length ++ x = advisedInput a x := by
-  simp [fixedPrefix, advisedInput, pair, List.append_assoc]
+  simp [fixedPrefix, advisedInput, pair]
 
 /-- The fixed-prefix bit string serializes to the self-delimiting advised
 machine input. -/

Complexitylib/Encoding.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2026 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+module
+public import Complexitylib.Encoding.Delimit
+public import Complexitylib.Encoding.Pairing
+public import Complexitylib.Encoding.Data
+public import Complexitylib.Encoding.DataEncode
+
+/-!
+# Encodings
+
+Aggregation module for the machine-independent encoding layer: the shared
+self-delimiting block framing and its parsers
+(`Complexitylib.Encoding.Delimit`), the pairing codec used by machine inputs
+(`Complexitylib.Encoding.Pairing`), and the rose-tree `Data` type
+(`Complexitylib.Encoding.Data`) together with the `DataEncode` typeclass and its
+derived bitstring encoding (`Complexitylib.Encoding.DataEncode`).
+-/

Complexitylib/Encoding/Data.lean

@@ -7,6 +7,7 @@ Authors: Christian Reitwiessner
 module
 public import Aesop.BuiltinRules
 public import Mathlib.Data.Nat.Notation
+public import Mathlib.Data.List.Basic
 public import Mathlib.Tactic.Finiteness.Attr
 public import Mathlib.Tactic.Push
 public import Mathlib.Tactic.ToAdditive
@@ -22,6 +23,8 @@ This file contains the main internal data structure for the RTM, `Data`, a rose
 - `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.toBits` - a parenthesized (balanced-bracket) serialization into `List Bool`, with length
+  equal to `Data.size`, and injective (`Data.toBits_injective`).
 - `Data.recL` - the main recursion principle for `Data`
 - `Data.inductionL` - the main induction principle for `Data`
 
@@ -32,8 +35,6 @@ 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
@@ -100,6 +101,16 @@ lemma Data.cons_size {h : Data} {t : List Data} :
   simp [Data.size]
   grind
 
+lemma Data.size_lt_of_mem {c : Data} {xs : List Data} (hc : c ∈ xs) :
+    c.size < (Data.l xs).size := by
+  induction xs with
+  | nil => simp at hc
+  | cons a as ih =>
+    rw [Data.cons_size]
+    rcases List.mem_cons.1 hc with h | h
+    · subst h; have := @Data.size_le (Data.l as); omega
+    · have := ih h; omega
+
 /-- Recursion principle for `Data`. -/
 @[elab_as_elim]
 def Data.recL {motive : Data → Sort*}
@@ -120,9 +131,99 @@ theorem Data.inductionL {motive : Data → Prop}
     (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 := ℕ
+/-! ## Bitstring serialization
+
+`Data.toBits` serializes a `Data` value into a `List Bool` using a parenthesized
+(balanced-bracket) encoding: `false` opens a node, its children are serialized in order, and
+`true` closes the node. This matches `Data.size` exactly (`Data.length_toBits`) and is injective
+(`Data.toBits_injective`), so any `DataEncode` instance yields an injective bitstring encoding
+(see `Complexitylib.Encoding.DataEncode`). -/
+
+/-- Serialize `Data` into a bitstring with a parenthesized (balanced-bracket) encoding: `false`
+opens a node, the children are serialized in order, and `true` closes the node. -/
+def Data.toBits : Data → List Bool
+  | Data.l xs => false :: ((xs.map Data.toBits).flatten ++ [true])
 
-end RoseTreeMachine
+lemma Data.toBits_l (xs : List Data) :
+    (Data.l xs).toBits = false :: ((xs.map Data.toBits).flatten ++ [true]) := by
+  rw [Data.toBits]
+
+@[simp]
+lemma Data.length_toBits (d : Data) : d.toBits.length = d.size := by
+  induction d using Data.inductionL with
+  | nil => simp [Data.toBits]
+  | cons x xs ihx ihxs =>
+    simp only [Data.toBits, Data.size, List.map_cons, List.flatten_cons, List.length_cons,
+      List.length_append, List.length_flatten, List.map_map] at *
+    grind
+
+/-- One step of the stack-based `Data.fromBits` parser. The state is a stack of frames, each a
+list of the sibling nodes completed so far at that nesting depth (outermost frame at the bottom).
+Reading `false` opens a new (empty) frame; reading `true` closes the top frame into a `Data.l`
+node and appends it to its parent. `none` is a permanent failure state (an unmatched `true`). -/
+def Data.fromBitsStep : Option (List (List Data)) → Bool → Option (List (List Data))
+  | none, _ => none
+  | some stack, false => some ([] :: stack)
+  | some stack, true =>
+    match stack with
+    | kids :: parent :: rest => some ((parent ++ [Data.l kids]) :: rest)
+    | _ => none
+
+/-- Decode a bitstring produced by `Data.toBits` back into a `Data` value, or `none` if it is not
+a valid single serialization. This is a left inverse of `Data.toBits` (`Data.fromBits_toBits`). -/
+def Data.fromBits (bits : List Bool) : Option Data :=
+  match bits.foldl Data.fromBitsStep (some [[]]) with
+  | some [[d]] => some d
+  | _ => none
+
+/-- Running `Data.fromBitsStep` over `d.toBits` appends the decoded `d` to the top frame of the
+stack, leaving the rest of the stack untouched. This is the key lemma behind
+`Data.fromBits_toBits`. -/
+theorem Data.foldl_fromBitsStep_toBits :
+    ∀ (d : Data) (top : List Data) (rest : List (List Data)),
+      d.toBits.foldl Data.fromBitsStep (some (top :: rest)) = some ((top ++ [d]) :: rest) := by
+  -- Strong induction on the size of `d`, so that each child (strictly smaller) can appeal to the
+  -- inductive hypothesis while a plain list induction consumes the children in order.
+  have key : ∀ (n : ℕ) (d : Data) (top : List Data) (rest : List (List Data)),
+      d.size ≤ n →
+      d.toBits.foldl Data.fromBitsStep (some (top :: rest)) = some ((top ++ [d]) :: rest) := by
+    intro n
+    induction n using Nat.strongRecOn with
+    | ind n IH =>
+      rintro ⟨xs⟩ top rest hsz
+      -- Consuming the flattened children appends them, in order, to the current frame.
+      have L : ∀ (xs : List Data) (cur : List Data) (rest : List (List Data)),
+          (∀ c ∈ xs, c.size < n) →
+          (xs.map Data.toBits).flatten.foldl Data.fromBitsStep (some (cur :: rest))
+            = some ((cur ++ xs) :: rest) := by
+        intro xs
+        induction xs with
+        | nil => intro cur rest _; simp
+        | cons c cs ihcs =>
+          intro cur rest hlt
+          have hc : c.size < n := hlt c (List.mem_cons_self ..)
+          simp only [List.map_cons, List.flatten_cons, List.foldl_append]
+          rw [IH c.size hc c cur rest (Nat.le_refl _),
+            ihcs (cur ++ [c]) rest (fun c' hc' => hlt c' (List.mem_cons_of_mem _ hc'))]
+          simp
+      rw [Data.toBits_l]
+      simp only [List.foldl_cons, List.foldl_append, Data.fromBitsStep]
+      rw [L xs [] (top :: rest) (fun c hc => Nat.lt_of_lt_of_le (Data.size_lt_of_mem hc) hsz)]
+      simp
+  intro d top rest
+  exact key d.size d top rest (Nat.le_refl _)
+
+/-- `Data.fromBits` recovers any value serialized by `Data.toBits`. -/
+@[simp]
+theorem Data.fromBits_toBits (d : Data) : Data.fromBits d.toBits = some d := by
+  simp only [Data.fromBits, Data.foldl_fromBitsStep_toBits, List.nil_append]
+
+/-- `Data.toBits` is injective: the parenthesized serialization determines the value. This follows
+from `Data.fromBits` being a left inverse. -/
+theorem Data.toBits_injective : Function.Injective Data.toBits := by
+  intro a b h
+  have := Data.fromBits_toBits a
+  rw [h, Data.fromBits_toBits b] at this
+  exact Option.some.inj this.symm
 
 end Complexity

Complexitylib/Encoding/DataEncode.lean

@@ -18,15 +18,17 @@ 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`)
 
+Every `DataEncode` instance also yields a *bitstring* encoding `DataEncode.bitstringEncode`, by
+serializing the target `Data` value with `Data.toBits`. Since both the `DataEncode` instance and
+`Data.toBits` are injective, `bitstringEncode` is injective too
+(`DataEncode.bitstringEncode_injective`).
 -/
 
 
 public section
 
 namespace Complexity
 
-namespace RoseTreeMachine
-
 /-- Encoding of types into `Data`. -/
 class DataEncode (α : Type) where
   /-- Encode a value of `α` as `Data`. -/
@@ -102,6 +104,19 @@ instance : DataEncode ℕ where
     have := congrArg (List.foldr (fun b acc => Nat.bit b acc) 0) hb
     simpa [hrec] using this
 
-end RoseTreeMachine
+/-- Encode a value into a bitstring (`List Bool`) by first encoding it into `Data` and then
+serializing that with the parenthesized `Data.toBits`. This is the class-inferrable bitstring
+encoding available for any type with a `DataEncode` instance. -/
+@[expose] def DataEncode.bitstringEncode {α : Type} [DataEncode α] (a : α) : List Bool :=
+  (DataEncode.encode a).toBits
+
+lemma DataEncode.bitstringEncode_def {α : Type} [DataEncode α] (a : α) :
+    DataEncode.bitstringEncode a = (DataEncode.encode a).toBits := rfl
+
+/-- The bitstring encoding is injective: distinct values yield distinct bitstrings. This composes
+the injectivity of the `DataEncode` instance with that of `Data.toBits`. -/
+theorem DataEncode.bitstringEncode_injective {α : Type} [DataEncode α] :
+    Function.Injective (DataEncode.bitstringEncode (α := α)) :=
+  Data.toBits_injective.comp DataEncode.h_inj
 
 end Complexity