Constant space machines

.github/CODEOWNERS

@@ -12,6 +12,9 @@
 ### Area access
 # Each area maintainer has access to parts that pertain them. They get automatically asked for
 # reviewing new PRs that touch those areas.
-/Cslib/Languages/LambdaCalculus/ @chenson2018
+/Cslib/Algorithms/ @fmontesi @sorrachai @chenson2018
+/Cslib/Foundations/Logic/ @arademaker @fmontesi @chenson2018
+/Cslib/Logics/ @arademaker @fmontesi @chenson2018
+/Cslib/Languages/LambdaCalculus/ @chenson2018 @fmontesi
 /.github/workflows @kim-em @fmontesi @chenson2018
 /scripts @kim-em @fmontesi @chenson2018

.github/workflows/lake-update.yml

@@ -25,6 +25,7 @@ on:
 jobs:
   bump:
     runs-on: ubuntu-latest
+    if: github.repository == 'leanprover/cslib'
     steps:
       - name: Generate app token
         id: app-token
@@ -52,6 +53,7 @@ jobs:
 
   open-issue:
     runs-on: ubuntu-latest
+    if: github.repository == 'leanprover/cslib'
     permissions:
       issues: write
     steps:

.github/workflows/lean_action_ci.yml

@@ -22,10 +22,10 @@ jobs:
         with:
           build-args: "--wfail --iofail"
           test-args: "--wfail --iofail"
-      - name: "lake exe mk_all --check --module"
+      - name: "lake exe mk_all --check"
         run: |
           set -e
-          lake exe mk_all --check --module
+          lake exe mk_all --check
       #- name: "lake shake"
       #  run: |
       #    set -e

.github/copilot-instructions.md → AGENTS.md

@@ -1,4 +1,4 @@
-# Copilot Instructions for CSLib
+# Project Instructions
 
 ## Repository Overview
 
@@ -18,20 +18,20 @@
 | Command | Purpose | When to Use |
 |---------|---------|-------------|
 | `lake build` | Build the library | After any code change |
-| `lake build --wfail --iofail` | Build with CI strictness (fails on warnings) | **Always use before committing** |
+| `lake build --wfail --iofail` | Build with CI strictness (fails on warnings) | Before committing |
 | `lake test` | Run all tests (builds CslibTests + checks init imports) | After changes to verify correctness |
 | `lake lint` | Run environment linters (Batteries/Mathlib) | Before committing |
 | `lake exe lint-style` | Run text-based style linters | Before committing |
-| `lake exe mk_all --module --check` | Verify Cslib.lean imports all modules | After adding new files |
-| `lake exe mk_all --module` | Auto-update Cslib.lean imports | After adding new files |
+| `lake exe mk_all --check` | Verify Cslib.lean imports all modules | After adding new files |
+| `lake exe mk_all` | Auto-update Cslib.lean imports | After adding new files |
 
 ### Full CI Validation Sequence
 
 Run these commands **in order** to replicate CI checks locally:
 
 ```bash
 lake build --wfail --iofail
-lake exe mk_all --module --check
+lake exe mk_all --check
 lake test
 lake lint
 lake exe lint-style
@@ -64,8 +64,7 @@ lake exe lint-style
 │   └── Logics/          # Logic formalisations (e.g., Linear Logic, Hennessy-Milner Logic)
 ├── CslibTests/          # Test files
 ├── scripts/             # Build and maintenance scripts
-│   ├── noshake.json     # Import exceptions for shake tool
-│   └── nolints.json     # Lint exceptions
+│   └── noshake.json     # Import exceptions for shake tool
 └── .github/workflows/   # CI workflows
 ```
 
@@ -79,9 +78,9 @@ Every file in `Cslib/` must transitively import `Cslib/Init.lean`. This sets up
 - `Cslib.Init` itself
 
 ### 2. New Files Must Be Added to Cslib.lean
-When creating a new `.lean` file in `Cslib/`, add its import to `Cslib.lean`. Run:
+When creating a new `.lean` file in `Cslib/`, add its import to `Cslib.lean` by running:
 ```bash
-lake exe mk_all --module
+lake exe mk_all
 ```
 
 ### 3. PR Title Convention
@@ -103,15 +102,22 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: $LIST_OF_AUTHORS
 -/
 ```
+where $YEAR should be replaced with the current year, $AUTHOR_NAME with the name of the file creator, and $LIST_OF_AUTHORS with the list of authors (this is just the file creator if there are no additional authors).
+
+### 5. Always Read Local README.md Files
+
+Before working on any file or directory, **always read** all `README.md` files in all directories throughout the entire repository.
+
+These files contain essential context that must be understood before making changes.
 
 ## Code Style
 
 - Follow everything written in /CONTRIBUTING.md
-- Follow [Mathlib style guide](https://leanprover-community.github.io/contribute/style.html)
-- Use domain-specific variable names (e.g., `State` for state types, `μ` for transition labels)
-- Keep proofs readable; golfing is welcome if proofs remain clear
-- Use existing typeclasses for common concepts (transitions, reductions)
-- Use `module` keyword at the start of files with `public import` statements
+- Follow the [Mathlib code style](https://leanprover-community.github.io/contribute/style.html)
+- Use domain-specific variable names when dealing with APIs that have a clear intention (e.g., `State` for state types, `μ` for transition labels).
+- Keep proofs readable; golfing is welcome if proofs remain clear.
+- Use existing typeclasses for common concepts (`Congruence`, `Context`, etc.).
+- Use the `module` keyword at the start of files with `public import` statements.
 
 ## Linter Configuration
 
@@ -122,18 +128,11 @@ Linters are configured in `lakefile.toml`.
 ### Creating a New Module
 1. Create file in appropriate `Cslib/` subdirectory
 2. Add `import Cslib.Init` (or import a module that imports it)
-3. Run `lake exe mk_all --module`
+3. Run `lake exe mk_all`
 4. Run `lake build --wfail --iofail`
 5. Run `lake test` to verify init imports
 
 ### Adding Tests
 1. Create or modify a file in `CslibTests/`
-2. Add import to `CslibTests.lean` if new file
+2. Add import to `CslibTests.lean` if it is a new file
 3. Run `lake test`
-
-## Trust These Instructions
-
-Only search for additional information if:
-- A command fails with an unexpected error
-- You need details about a specific module's API
-- The instructions appear incomplete for your specific task

AUTHORS.md

@@ -0,0 +1,15 @@
+# CSLib Authors
+
+## Copyright and Authorship
+
+**Copyright in CSLib is held by the individual authors** who contributed to the code.
+
+Each file in CSLib includes a copyright header that lists the authors who contributed significantly to that specific file (in the opener and in the optional `Authors` field, when there are multiple significant authors). Examples of significant contributions are original creation, major refactoring, or important additions.
+
+To see more people who have contributed to CSLib and own copyright to parts of the codebase, please refer to its Git history (on a web browser, this can be accessed at <https://github.com/leanprover/cslib/commits/main>).
+
+**Note**: Git history may not always be fully comprehensive. In cases where code is co-written, commit messages and copyright headers in files may attribute additional authors beyond the single commit author.
+
+## Co-Authorship
+
+To ensure **all contributors are properly credited**, we strongly encourage the use of GitHub's [commit with multiple authors feature](https://docs.github.com/en/pull-requests/committing-changes-to-your-project/creating-and-editing-commits/creating-a-commit-with-multiple-authors) whenever code is co-written. This helps with maintaining accurate attribution in CSLib's Git history.

CONTRIBUTING.md

@@ -101,7 +101,7 @@ instructions on how to run these locally.
 
 ## Pull Request Titles
 
-It is required that pull request titles begun with one of the following categories followed by a
+It is required that pull request titles begin with one of the following categories followed by a
 colon: `feat`, `fix`, `doc`, `style`, `refactor`, `test`, `chore`, `perf`. These may optionally be followed by a
 parenthetical containing what area of the library the PR is working on.
 
@@ -125,8 +125,8 @@ CSLib uses a number of linters, mostly inherited from Batteries and Mathlib. The
 
 ## Imports
 
-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.
+There is also a test that [Cslib.lean](/Cslib.lean) imports all files. You can ensure this by
+running `lake exe mk_all` locally, which will make the required changes.
 
 CSLib tests for minimized imports using `lake shake --add-public --keep-implied --keep-prefix`, which also comes with a `--fix` option.
 See `lake shake --help` for the special comment syntax used to preserve imports required for tactics or typeclasses.

Cslib.lean

@@ -1,5 +1,6 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import Cslib.Algorithms.CCS.VendingMachine
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor
@@ -11,19 +12,29 @@ public import Cslib.Computability.Automata.DA.Prod
 public import Cslib.Computability.Automata.DA.ToNA
 public import Cslib.Computability.Automata.EpsilonNA.Basic
 public import Cslib.Computability.Automata.EpsilonNA.ToNA
+public import Cslib.Computability.Automata.EpsilonNA.ToSingleAccept
 public import Cslib.Computability.Automata.NA.Basic
 public import Cslib.Computability.Automata.NA.BuchiEquiv
 public import Cslib.Computability.Automata.NA.BuchiInter
 public import Cslib.Computability.Automata.NA.Concat
+public import Cslib.Computability.Automata.NA.EpsilonTransducer
 public import Cslib.Computability.Automata.NA.Hist
 public import Cslib.Computability.Automata.NA.Loop
 public import Cslib.Computability.Automata.NA.Pair
 public import Cslib.Computability.Automata.NA.Prod
+public import Cslib.Computability.Automata.NA.Reverse
 public import Cslib.Computability.Automata.NA.Sum
 public import Cslib.Computability.Automata.NA.ToDA
 public import Cslib.Computability.Automata.NA.Total
+public import Cslib.Computability.Automata.Transducers.Transducer
 public import Cslib.Computability.Distributed.FLP.Algorithm
+public import Cslib.Computability.Distributed.FLP.CanReachVia
 public import Cslib.Computability.Distributed.FLP.Consensus
+public import Cslib.Computability.Distributed.FLP.FairScheduler
+public import Cslib.Computability.Distributed.FLP.Impossibility
+public import Cslib.Computability.Distributed.FLP.OnePseudoConsensus
+public import Cslib.Computability.Distributed.FLP.PseudoConsensus
+public import Cslib.Computability.Distributed.FLP.ZeroConsensus
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
@@ -32,7 +43,13 @@ public import Cslib.Computability.Languages.MyhillNerode
 public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
-public import Cslib.Computability.Machines.SingleTapeTuring.Basic
+public import Cslib.Computability.Languages.SafetyLiveness
+public import Cslib.Computability.Machines.Turing.MultiTape.ConstantSpace
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
+public import Cslib.Computability.Machines.Turing.SingleTape.Defs
+public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
@@ -64,26 +81,37 @@ public import Cslib.Foundations.Data.OmegaSequence.Flatten
 public import Cslib.Foundations.Data.OmegaSequence.InfOcc
 public import Cslib.Foundations.Data.OmegaSequence.Init
 public import Cslib.Foundations.Data.OmegaSequence.Temporal
+public import Cslib.Foundations.Data.OmegaSequence.Topology
+public import Cslib.Foundations.Data.PFunctor.Free
 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.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
+public import Cslib.Foundations.Logic.Operators
+public import Cslib.Foundations.Relation.Attr
+public import Cslib.Foundations.Relation.Confluence
+public import Cslib.Foundations.Relation.Defs
+public import Cslib.Foundations.Relation.Domain
+public import Cslib.Foundations.Relation.Euclidean
+public import Cslib.Foundations.Relation.Restriction
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
 public import Cslib.Foundations.Semantics.FLTS.Prod
 public import Cslib.Foundations.Semantics.LTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Bisimulation
 public import Cslib.Foundations.Semantics.LTS.Divergence
+public import Cslib.Foundations.Semantics.LTS.ExampleTermination
 public import Cslib.Foundations.Semantics.LTS.Execution
 public import Cslib.Foundations.Semantics.LTS.HasTau
 public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic
+public import Cslib.Foundations.Semantics.LTS.MapLabel
 public import Cslib.Foundations.Semantics.LTS.Notation
 public import Cslib.Foundations.Semantics.LTS.OmegaExecution
 public import Cslib.Foundations.Semantics.LTS.Relation
+public import Cslib.Foundations.Semantics.LTS.Reverse
 public import Cslib.Foundations.Semantics.LTS.Simulation
 public import Cslib.Foundations.Semantics.LTS.Termination
 public import Cslib.Foundations.Semantics.LTS.Total
@@ -116,6 +144,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.StrongNorm
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.BetaAt
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.CallByName
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
@@ -124,11 +154,18 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LeftmostReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiApp
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.MultiSubst
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StandardReduction
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.StrongNorm
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
+public import Cslib.Languages.LambdaCalculus.Named.Untyped.Properties
+public import Cslib.Languages.Mech.Choreography.Basic
+public import Cslib.Languages.Mech.LocalComputation
+public import Cslib.Languages.StatefulProcesses.Basic
+public import Cslib.Languages.StatefulProcesses.Network
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.HML.LogicalEquivalence
 public import Cslib.Logics.LinearLogic.CLL.Basic
@@ -139,9 +176,12 @@ public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
 public import Cslib.Logics.Modal.Basic
 public import Cslib.Logics.Modal.Cube
 public import Cslib.Logics.Modal.Denotation
+public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.Logics.Propositional.NaturalDeduction.Theory
 public import Cslib.MachineLearning.PACLearning.Defs
 public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
+public import Cslib.MachineLearning.PACLearning.VersionSpaceLattice
 public import Cslib.Probability.PMF