Multi tape turing machine - ongoing PR

.github/workflows/lean_action_ci.yml

@@ -15,8 +15,8 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
-        with:
-          build-args: "--wfail --iofail"
+        # with:
+        #   build-args: "--iofail"
       - name: "lake exe mk_all --check --module"
         run: |
           set -e

.github/workflows/pr-title.yml

@@ -17,7 +17,3 @@ jobs:
         with:
           script: |
             const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message;
-            console.log(`Message: ${msg}`)
-            if (!/^(ci|feat|fix|doc|style|refactor|test|chore|perf)(\(.*\))?: .*[^.]($|\n\n)/.test(msg)) {
-              core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
-            }

CONTRIBUTING.md

@@ -1,3 +1,46 @@
+**Table of Contents**
+
+- [Contributing to CSLib](#contributing-to-cslib)
+- [Contribution model](#contribution-model)
+- [Style and documentation](#style-and-documentation)
+  - [Variable names](#variable-names)
+  - [Proof style and golfing :golf:](#proof-style-and-golfing-golf)
+  - [Notation](#notation)
+  - [Documentation](#documentation)
+- [Design principles](#design-principles)
+  - [Reuse](#reuse)
+- [Continuous Integration](#continuous-integration)
+  - [Pull Request Titles](#pull-request-titles)
+  - [Testing](#testing)
+  - [Linting](#linting)
+  - [Imports](#imports)
+- [Getting started](#getting-started)
+  - [Before you start: coordination to avoid rework](#before-you-start-coordination-to-avoid-rework)
+  - [Finding tasks](#finding-tasks)
+  - [Working groups](#working-groups)
+    - [Proposing a new working group](#proposing-a-new-working-group)
+  - [Examples of welcome contributions](#examples-of-welcome-contributions)
+    - [Pillar 1: Formalising Computer Science in Lean](#pillar-1-formalising-computer-science-in-lean)
+      - [Algorithms and Data Structures](#algorithms-and-data-structures)
+        - [Verified data structures with time complexity (Batteries + Time Monad)](#verified-data-structures-with-time-complexity-batteries--time-monad)
+        - [Graph algorithms and graph foundations](#graph-algorithms-and-graph-foundations)
+        - [APIs for algorithmic paradigms](#apis-for-algorithmic-paradigms)
+      - [Programming Languages, Models of Computation and Interaction](#programming-languages-models-of-computation-and-interaction)
+      - [Logics](#logics)
+      - [Semantics and program equivalences](#semantics-and-program-equivalences)
+        - [Semantic frameworks](#semantic-frameworks)
+        - [Program equivalences](#program-equivalences)
+    - [Pillar 2: Code reasoning](#pillar-2-code-reasoning)
+      - [Contributing Boole examples](#contributing-boole-examples)
+      - [Boole specifications](#boole-specifications)
+      - [Issue labels for Boole](#issue-labels-for-boole)
+      - [Front ends for Boole](#front-ends-for-boole)
+      - [Back ends for Boole](#back-ends-for-boole)
+      - [Implementing verification paradigms](#implementing-verification-paradigms)
+      - [Lean automation](#lean-automation)
+      - [The role of AI](#the-role-of-ai)
+
+
 # Contributing to CSLib
 
 It's great that you're interested in contributing to CSLib! :tada:
@@ -12,9 +55,11 @@ Each PR needs to be approved by at least one relevant maintainer. You can read t
 
 If you are adding something new to CSLib and are in doubt about it, you are very welcome to contact us on the [Lean prover Zulip chat](https://leanprover.zulipchat.com/).
 
+If you are unfamiliar with CSLib as a whole and want to understand how to get started, please see [Getting started](#getting-started).
+
 # Style and documentation
 
-We generally follow the [mathlib style for coding and documentation](https://leanprover-community.github.io/contribute/style.html), so please read that as well. Some things worth mentioning and conventions specific to this library are explained next.
+We generally follow the [mathlib style for coding and documentation](https://leanprover-community.github.io/contribute/style.html), so please read that as well. Some things worth mentioning and conventions specific to CSLib are explained next.
 
 ## Variable names
 
@@ -79,3 +124,208 @@ CSLib uses a number of linters, mostly inherited from Batteries and Mathlib. The
 
 There is a also a test that [Cslib.lean](/Cslib.lean) imports all files. You can ensure this by
 running `lake exe mk_all --module` locally, which will make the required changes.
+
+# Getting started
+
+CSLib is a community effort. To understand its scope and vision, please read the [CSLib whitepaper](https://arxiv.org/abs/2602.04846).
+For an overview of its technical approach to reuse, continuous integration, and proof automation, please read the [Computer Science as Infrastructure paper](https://arxiv.org/abs/2602.15078).
+
+Key project links include:
+
+- Website: https://www.cslib.io/
+- GitHub issues + PRs: https://github.com/leanprover/cslib
+- Open contribution board: https://github.com/leanprover/cslib/projects?query=is%3Aopen
+- Community discussion (Lean Community Zulip): https://leanprover.zulipchat.com/
+  - CSLib channels are the recommended place to coordinate and ask questions.
+
+## Before you start: coordination to avoid rework
+
+Most contributions are welcome as straightforward PRs. However, **for any major development**, it is strongly recommended to discuss first on Zulip (or via a GitHub issue) so that the scope, dependencies, and placement in the library are aligned.
+
+Examples of work that should be discussed first:
+
+- New cross-cutting abstractions / typeclasses / notation schemes.
+- New foundational frameworks.
+- Major refactorings.
+- New frontend or backend components for CSLib's verification infrastructure.
+- Proposals for new working groups (see below).
+
+## Finding tasks
+
+If you are looking for a concrete starting point, please look at:
+
+- The CSLib Zulip channels.
+- Our [GitHub issues](https://github.com/leanprover/cslib/issues).
+
+
+## Working groups
+
+CSLib is structured to support multiple topic-focused efforts. We organise sustained work via **working groups** (informal or formal), which typically have a topic scope and a Zulip topic/channel for coordination.
+
+If you want to **join** a working group, start by posting on the relevant CSLib Zulip channel describing your background and what you want to contribute.
+
+### Proposing a new working group
+
+If you want to propose a new working group, write a short proposal (Zulip message or GitHub issue is fine) that includes:
+
+- **Topic**: What do you want to do?
+- **Execution plan**: What is your execution plan?
+- **Collaborators**: If some group or people are already planning to work on the topic, write them.
+
+The goal is to keep proposals lightweight while ensuring CSLib remains coherent and reusable.
+
+## Examples of welcome contributions
+
+Here you can find some (non-exhaustive) examples of topics looking for contributions.
+
+### Pillar 1: Formalising Computer Science in Lean
+
+Pillar 1 is about the formalisation of Computer Science as reusable infrastructure. This includes, but is not limited to, models of computation, semantics, logics, algorithms, data structures, metatheory, and supporting mathematics.
+
+#### Algorithms and Data Structures
+
+##### Verified data structures with time complexity (Batteries + Time Monad)
+
+A concrete and high-impact track is to verify implementations and time complexity bounds for [data structures from Batteries](https://github.com/leanprover-community/batteries/tree/main/Batteries/Data).
+
+Examples of candidate targets:
+
+- List and Array developments
+- Binary heap
+- Binomial heap
+- Union find
+- Red-black trees
+
+##### Graph algorithms and graph foundations
+
+- Foundational definitions (directed/undirected simple graphs, etc.)
+- Core algorithms and their correctness proofs:
+  - DFS, topological sorting, SCC
+  - shortest paths, APSP
+  - max-flow
+  - minimum spanning tree
+  - spanners
+  - Gomory–Hu trees
+
+##### APIs for algorithmic paradigms
+
+Reusable APIs that support many concrete algorithms.
+
+- Divide-and-conquer
+  - Master theorem
+- Dynamic programming
+  - generic DP API patterns
+  - quadrangle inequality (Yao ’80)
+  - SMAWK algorithm
+
+#### Programming Languages, Models of Computation and Interaction
+
+- Automata (on finite and infinite words)
+- Choreographic languages
+- Lambda calculi
+- Petri Nets
+- Process calculi, like CCS and pi-calculus
+- Frameworks for language encodings (compilers, etc.).
+- Proof techniques for the correctness of encodings.
+
+#### Logics
+
+We aim at formalising a number of logics of different kinds, including linear logic, modal logics, etc.
+
+We welcome proofs of logical equivalences and metatheoretical results such as identity expansion, cut elimiation, etc.
+
+Examples of interesting logics include:
+- Linear logic
+- Temporal logic
+- Separation logic
+
+#### Semantics and program equivalences
+
+##### Semantic frameworks
+- Denotational semantics
+- Operational semantics, including results on labelled transition systems and reduction systems
+
+##### Program equivalences
+
+- Bisimulation
+- May/Must testing
+- Trace equivalence
+
+### Pillar 2: Code reasoning
+
+Pillar 2 is about infrastructure for reasoning about code in mainstream programming languages via intermediate representations, VC generation, and automation.
+
+We are interested in collecting a large number of programs in Boole (see the [CSLib whitepaper](https://arxiv.org/abs/2602.04846) for Boole's vision).
+
+You can try the Boole sandbox examples at <https://github.com/leanprover/cslib/tree/Boole-sandbox/Cslib/Languages/Boole>.
+
+#### Contributing Boole examples
+
+We are interested in collecting a large number of programs in Boole.
+
+If you'd like to contribute examples, please propose and coordinate on the [Zulip channel for code reasoning](https://leanprover.zulipchat.com/#narrow/channel/563135-CSLib.3A-Code-Reasoning) first (especially if the example requires new features).
+
+We separate Boole examples into two directories:
+
+- examples that work with the current Boole back end
+- examples that are broken or contain features not yet implemented
+
+Contributions to both sets are valuable: working examples demonstrate capabilities; 'broken' examples identify missing features and bottlenecks.
+
+#### Boole specifications
+
+Currently, Boole specifications are based on Strata Core: <https://strata-org.github.io/Strata/>
+
+A key long-term goal is to support specifications that reference arbitrary Lean concepts, especially those formalised as part of CSLib Pillar 1. Designing this cleanly within the Strata framework is a challenging and valuable project.
+
+#### Issue labels for Boole
+
+If you have feature requests for Boole, file an issue with title `feat(Boole): <feature request title here>`.
+
+For bugs, errors, or other issues, file an issue with label `Boole`.
+
+#### Front ends for Boole
+
+We are interested in developing translations from real-world programming languages to Boole.
+
+- Prototype translations are welcome to explore feasibility and identify design constraints.
+- If you want to propose a translation for inclusion in CSLib, coordinate on Zulip.
+
+We expect initial translations will be ad hoc and trusted. The eventual goal is to formalize the semantics of front ends and prove (as a Lean metatheorem) that translations preserve semantics.
+
+#### Back ends for Boole
+
+We are interested in building Boole back ends that take as input Boole programs with formal specifications and construct proof obligations in Lean, which, if proved, ensure that the program meets its specification.
+
+- A prototype translation based on a deep embedding in Strata exists, but is not fully foundational.
+- A major long-term goal is to prove Lean meta-theorems showing that proving the verification conditions ensures correctness of the Boole program.
+
+Alternative directions are welcome, e.g.:
+
+- Exploring a shallow embedding approach
+- Leveraging Loom for more foundational pipelines
+
+A back end for **time complexity analysis** is also of interest.
+
+#### Implementing verification paradigms
+
+The formal methods community has a wide range of verification techniques that could be valuable in the Boole ecosystem, e.g.:
+
+- proof by refinement
+- techniques for program equivalence
+- other deductive verification paradigms
+
+#### Lean automation
+
+Since Boole back ends reduce correctness questions to Lean conjectures, automation is central.
+
+We already rely on key techniques such as `grind` and `lean-smt`. Additional work on automation for conjectures generated from Boole is welcome, including domain-specific automation that remains performant and readable.
+
+#### The role of AI
+
+There are two primary areas where generative AI can help:
+
+- generating/refining specifications (at the front-end or Boole level)
+- helping to prove Lean conjectures
+
+Other creative uses of AI are welcome, but contributions should remain reviewable and maintainable.

Cslib.lean

@@ -29,6 +29,26 @@ public import Cslib.Computability.Languages.Language
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
+public import Cslib.Computability.Machines.MultiTapeTuring.AddRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.Basic
+public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.EqualRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.GraphReachability
+public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats
+public import Cslib.Computability.Machines.MultiTapeTuring.IsZeroRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.IteCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding
+public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.MoveRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.MulRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.SuccRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.TapeExtension
+public import Cslib.Computability.Machines.MultiTapeTuring.WhileCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
+public import Cslib.Computability.Machines.SingleTapeTuring.Basic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
@@ -39,6 +59,7 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.FinFun
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
@@ -50,6 +71,7 @@ public import Cslib.Foundations.Data.OmegaSequence.Temporal
 public import Cslib.Foundations.Data.RelatesInSteps
 public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
+public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

@@ -17,7 +17,7 @@ public import Mathlib.Data.Nat.Log
 # MergeSort on a list
 
 In this file we introduce `merge` and `mergeSort` algorithms that returns a time monad
-over the list `TimeM (List α)`. The time complexity of `mergeSort` is the number of comparisons.
+over the list `TimeM ℕ (List α)`. The time complexity of `mergeSort` is the number of comparisons.
 
 --
 ## Main results
@@ -34,8 +34,8 @@ namespace Cslib.Algorithms.Lean.TimeM
 variable {α : Type} [LinearOrder α]
 
 /-- Merges two lists into a single list, counting comparisons as time cost.
-Returns a `TimeM (List α)` where the time represents the number of comparisons performed. -/
-def merge :  List α → List α → TimeM (List α)
+Returns a `TimeM ℕ (List α)` where the time represents the number of comparisons performed. -/
+def merge :  List α → List α → TimeM ℕ (List α)
   | [], ys => return ys
   | xs, [] => return xs
   | x::xs', y::ys' => do
@@ -48,8 +48,8 @@ def merge :  List α → List α → TimeM (List α)
       return (y :: rest)
 
 /-- Sorts a list using the merge sort algorithm, counting comparisons as time cost.
-Returns a `TimeM (List α)` where the time represents the total number of comparisons. -/
-def mergeSort (xs : List α) : TimeM (List α) :=  do
+Returns a `TimeM ℕ (List α)` where the time represents the total number of comparisons. -/
+def mergeSort (xs : List α) : TimeM ℕ (List α) :=  do
   if xs.length < 2 then return xs
   else
     let half  := xs.length / 2