feat(tocslib): add polynomial-time single-tape toolkit

.github/workflows/ci.yml

@@ -92,7 +92,9 @@ jobs:
         run: lake build --wfail
 
       - name: Run environment linters
-        run: lake lint
+        run: |
+          lake build ToCslib
+          lake lint
 
   test:
     name: Test

AGENTS.md

@@ -112,6 +112,10 @@ and depend on this library.
 - `PolyFun/Control/LTS/Trace.lean`: generic finite visible traces over the
   silent/visible `Control.LTS` layer and preservation by weak simulation.
 - `PolyFun/Logic/`: small logic helpers (`HEq`).
+- `ToCslib/`: a separate low-level Lake library of reusable extensions to the
+  pinned cslib machine API. It imports cslib and Mathlib but never PolyFun,
+  oracle semantics, probability, or cryptography. Concrete PolyFun backend
+  adapters may import it explicitly; the generated `PolyFun` umbrella does not.
 - `PolyFunTest/`: separate test / worked-example library (glob
   `PolyFunTest.+`), built by `lake test` and kept out of the `lake lint`
   scope. Holds the dynamical / interaction worked examples and the

PolyFunTest/ToCslib/Basic.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma, Elias Judin, Quang Dao
+-/
+
+module
+
+public import ToCslib
+
+/-!
+# Direct canaries for the ToCslib substrate
+
+These examples pin bit order, finite-table semantic orientation, overwrite
+selection, and the cardinality used by the machine-counting argument.
+-/
+
+open ToCslib.Computability
+
+example : natToBits 3 5 = [true, false, true] := by decide
+
+example (bit : Bool) :
+    let encoding : Bool → List Bool := fun value => [value]
+    let witness := EncPolyTime.ofFintype encoding (by
+      intro left right equality
+      have headEquality := congrArg List.head? equality
+      simpa [encoding] using headEquality) encoding (!·)
+    witness.toFun (encoding bit) = encoding (!bit) := by
+  dsimp only
+  exact EncPolyTime.map_encode _ bit
+
+example {n index : ℕ} (hindex : index < n) (bit : Bool) (value : BitVec n) :
+    (value.overwriteBit index bit).getLsbD index = bit := by
+  exact BitVec.getLsbD_overwriteBit_self hindex bit value
+
+example : Fintype.card (BitVec 2 → Bool) = 16 := by
+  simpa using card_bitVec_fun 2
+
+example (state : StrEncFam fun _ ↦ Bool) (parameter : ℕ) (value : Bool) :
+    state.option.enc parameter none ≠ state.option.enc parameter (some value) := by
+  simp
+
+example (input : List Bool) :
+    (EncPolyTime.appendBit id true).toFun input = input ++ [true] := rfl
+
+/-! Mixed-universe canaries: encoding products and machine families do not require
+their source and target families to live in the same universe. -/
+
+noncomputable example (lower : BitEncFam fun _ ↦ Bool)
+    (higher : BitEncFam fun _ ↦ ULift.{1} Bool) :
+    BitEncFam (fun _ ↦ Bool × ULift.{1} Bool) :=
+  lower.pair higher
+
+noncomputable example (lower : StrEncFam fun _ ↦ Bool)
+    (higher : BitEncFam fun _ ↦ ULift.{1} Bool) :
+    StrEncFam (fun _ ↦ Bool × ULift.{1} Bool) :=
+  lower.pairVar higher
+
+example {α : ℕ → Type} {β : ℕ → Type 1}
+    {ea : (n : ℕ) → α n → List Bool} {eb : (n : ℕ) → β n → List Bool}
+    {f : (n : ℕ) → α n → β n} (witness : EncPolyTimeFam ea eb f) :
+    EncPolyTimeFam ea eb f :=
+  witness

ToCslib.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2026 PolyFun Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma, Elias Judin
+-/
+
+module
+
+public import ToCslib.Computability.BitEncoding
+public import ToCslib.Computability.SingleTape.Counting
+public import ToCslib.Computability.SingleTape.Snoc
+public import ToCslib.Data.BitVec
+
+/-!
+# Extensions of the pinned cslib machine library
+
+This library contains reusable facts and constructions about cslib machines. It
+does not import PolyFun's realizability theory or any downstream oracle or
+cryptographic semantics. Optional backend libraries may import these modules
+explicitly without making cslib a dependency of generic PolyFun.
+-/