Mulit tape sim

.github/workflows/lean_action_ci.yml

@@ -34,6 +34,6 @@ jobs:
         run: |
           set -e
           lake exe checkInitImports
-      - uses: leanprover-community/lint-style-action@main
+      - uses: leanprover-community/lint-style-action@e6128ab22cb03b509075ae46c33727e3952ffab7 # 2026-05-12
         with:
           mode: check

.github/workflows/report_failures_nightly-testing.yml

@@ -21,7 +21,7 @@ jobs:
         api-key: ${{ secrets.ZULIP_API_KEY }}
         email: 'github-mathlib4-bot@leanprover.zulipchat.com'
         organization-url: 'https://leanprover.zulipchat.com'
-        to: 'nightly-testing'
+        to: 'nightly-testing-cslib'
         type: 'stream'
         topic: 'Cslib status updates'
         content: |
@@ -101,7 +101,7 @@ jobs:
           'num_before': 1,
           'num_after': 0,
           'narrow': [
-            {'operator': 'stream', 'operand': 'nightly-testing'},
+            {'operator': 'stream', 'operand': 'nightly-testing-cslib'},
             {'operator': 'topic', 'operand': 'Cslib status updates'},
             {'operator': 'sender', 'operand': bot_email}
           ],
@@ -113,7 +113,7 @@ jobs:
             # Post the success message
             request = {
                 'type': 'stream',
-                'to': 'nightly-testing',
+                'to': 'nightly-testing-cslib',
                 'topic': 'Cslib status updates',
                 'content': f"✅ The latest CI for Cslib's [nightly-testing branch](https://github.com/leanprover/cslib/tree/nightly-testing) has succeeded! ([{os.getenv('SHA')}](https://github.com/${{ github.repository }}/commit/{os.getenv('SHA')}))"
             }
@@ -250,7 +250,7 @@ jobs:
         api-key: ${{ secrets.ZULIP_API_KEY }}
         email: 'github-mathlib4-bot@leanprover.zulipchat.com'
         organization-url: 'https://leanprover.zulipchat.com'
-        to: 'nightly-testing'
+        to: 'nightly-testing-cslib'
         type: 'stream'
         topic: 'Cslib status updates'
         content: |
@@ -350,7 +350,7 @@ jobs:
               'num_before': 1,
               'num_after': 0,
               'narrow': [
-                {'operator': 'stream', 'operand': 'nightly-testing'},
+                {'operator': 'stream', 'operand': 'nightly-testing-cslib'},
                 {'operator': 'topic', 'operand': 'Cslib bump branch reminders'},
                 {'operator': 'sender', 'operand': bot_email}
               ],
@@ -388,7 +388,7 @@ jobs:
                 # Post the reminder message
                 request = {
                     'type': 'stream',
-                    'to': 'nightly-testing',
+                    'to': 'nightly-testing-cslib',
                     'topic': 'Cslib bump branch reminders',
                     'content': payload
                 }

.github/workflows/weekly-lints.yml

@@ -58,6 +58,7 @@ jobs:
         SHA=${{ github.sha }} \
         REPO=${{ github.repository }} \
         RUN_ID=${{ github.run_id }} \
+        INFO=true \
           "${CI_SCRIPTS_DIR}/reporting/zulip_build_report.sh" "${lean_outfile}" > "${GITHUB_OUTPUT}"
 
     - name: Post output to Zulip

CONTRIBUTING.md

@@ -2,6 +2,7 @@
 
 - [Contributing to CSLib](#contributing-to-cslib)
 - [Contribution model](#contribution-model)
+- [The role of AI](#the-role-of-ai)
 - [Style and documentation](#style-and-documentation)
   - [Variable names](#variable-names)
   - [Proof style and golfing :golf:](#proof-style-and-golfing-golf)
@@ -38,8 +39,6 @@
       - [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
 
@@ -57,6 +56,11 @@ If you are adding something new to CSLib and are in doubt about it, you are very
 
 If you are unfamiliar with CSLib as a whole and want to understand how to get started, please see [Getting started](#getting-started).
 
+# The role of AI
+
+CSLib in general follows the Mathlib policy on [use of AI](https://leanprover-community.github.io/contribute/index.html#use-of-ai). In particular, take note of:
+> If you use artificial intelligence [...] please explain this in the PR description. Explain which tool(s) you used and how you used it. This provides useful context for reviewers: tools make different mistakes than humans, so knowing this makes it easier to spot common errors.
+
 # 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 CSLib are explained next.
@@ -322,12 +326,3 @@ The formal methods community has a wide range of verification techniques that co
 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

@@ -1,4 +1,4 @@
-module  -- shake: keep-all
+module  -- shake: keep-all --deprecated_module: ignore
 
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
@@ -22,13 +22,16 @@ public import Cslib.Computability.Automata.NA.Prod
 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.Distributed.FLP.Algorithm
+public import Cslib.Computability.Distributed.FLP.Consensus
 public import Cslib.Computability.Languages.Congruences.BuchiCongruence
 public import Cslib.Computability.Languages.Congruences.RightCongruence
 public import Cslib.Computability.Languages.ExampleEventuallyZero
 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.Basic
 public import Cslib.Computability.Machines.SingleTapeTuring.Basic
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
@@ -42,7 +45,10 @@ public import Cslib.Crypto.Protocols.PerfectSecrecy.Encryption
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.OneTimePad
 public import Cslib.Crypto.Protocols.PerfectSecrecy.Internal.PerfectSecrecy
 public import Cslib.Crypto.Protocols.PerfectSecrecy.OneTimePad
-public import Cslib.Crypto.Protocols.PerfectSecrecy.PMFUtilities
+public import Cslib.Crypto.Protocols.SecretSharing.Defs
+public import Cslib.Crypto.Protocols.SecretSharing.Scheme
+public import Cslib.Crypto.Protocols.SecretSharing.Shamir
+public import Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial
 public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
@@ -113,6 +119,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Congruence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBetaEtaConfluence
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEta
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullEtaConfluence
@@ -129,5 +136,12 @@ public import Cslib.Logics.LinearLogic.CLL.CutElimination
 public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
 public import Cslib.Logics.LinearLogic.CLL.MLL
 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.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.MachineLearning.PACLearning.Defs
+public import Cslib.MachineLearning.PACLearning.VCDimension
+public import Cslib.MachineLearning.PACLearning.VersionSpace
+public import Cslib.Probability.PMF

Cslib/Computability/Automata/DA/Congr.lean

@@ -62,7 +62,7 @@ theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a})
   /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
   constructor <;>
   · intro h
-    simpa [mem_language, Accepts, congr_mtr_eq] using h
+    simpa [mem_language, Accepts, congr_mtr_eq] using! h
 
 end FinAcc
 

Cslib/Computability/Automata/DA/ToNA.lean

@@ -30,14 +30,17 @@ def toNA (a : DA State Symbol) : NA State Symbol :=
 instance : Coe (DA State Symbol) (NA State Symbol) where
   coe := toNA
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 open scoped FLTS NA NA.Run LTS in
 @[simp, scoped grind =]
 theorem toNA_run {a : DA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} :
     a.toNA.Run xs ss ↔ a.run xs = ss := by
   constructor
   · rintro _
     ext n
-    induction n <;> grind [NA.Run]
+    induction n
+    · grind only [NA.Run, toNA, = run_zero, = Set.mem_singleton_iff]
+    · grind only [NA.Run, toNA, = run_succ, = LTS.OmegaExecution, = FLTS.toLTS_tr]
   · grind [NA.Run]
 
 namespace FinAcc

Cslib/Computability/Automata/NA/BuchiInter.lean

@@ -93,6 +93,7 @@ lemma inter_freq_comp_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((
   apply leadsTo_cases_or (q := {⟨_, b⟩ | b = false}) <;>
   grind [until_frequently_leadsTo_and, univ_inter]
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- The language accepted by the intersection automaton is the intersection of
 the languages accepted by the two component automata. -/
 @[simp, scoped grind =]
@@ -122,7 +123,8 @@ theorem inter_language_eq :
   · intro h
     choose ss_i h_ss_i using h
     let ss_p : ωSequence (Π i, State i) := fun k i ↦ ss_i i k
-    have h_ss_p : (iProd na).Run xs ss_p := by grind [Run]
+    have h_ss_p : (iProd na).Run xs ss_p := by
+      grind only [Run, = iProd_run_iff, = get_fun, = LTS.OmegaExecution, = get_map]
     have (k : ℕ) (i : Bool) : ss_p k i = ss_i i k := rfl
     obtain ⟨ss, h_run, _⟩ := hist_run_exists h_ss_p
     use ss, h_run

Cslib/Computability/Automata/NA/Concat.lean

@@ -90,22 +90,29 @@ theorem concat_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State1 ⊕ St
     · grind [concat_run_left_right]
   · exact concat_run_right hc n hl (Nat.find_spec hr')
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- Given an accepting finite run of `na1` and a run of `na2`, there exists a run of
 `concat na1 na2` that is the concatenation of the two runs. -/
 theorem concat_run_exists {xs1 : List Symbol} {xs2 : ωSequence Symbol} {ss2 : ωSequence State2}
     (h1 : xs1 ∈ language na1) (h2 : na2.Run xs2 ss2) :
     ∃ ss, (concat na1 na2).Run (xs1 ++ω xs2) ss ∧ ss.drop xs1.length = ss2.map inr := by
   by_cases h_xs1 : xs1.length = 0
   · obtain ⟨rfl⟩ : xs1 = [] := List.eq_nil_iff_length_eq_zero.mpr h_xs1
-    refine ⟨ss2.map inr, by simp only [concat]; grind [Run, LTS.OmegaExecution], by simp⟩
+    use ss2.map inr
+    split_ands
+    · simp [concat]
+      grind only [LTS.OmegaExecution, = Set.mem_union, = get_map, = Set.mem_image, Run]
+    · simp
   · obtain ⟨s0, _, _, _, h_mtr⟩ := h1
     obtain ⟨ss1, _, _, _, _⟩ := LTS.Execution.of_mTr h_mtr
     let ss := (ss1.map inl).take xs1.length ++ω ss2.map inr
     refine ⟨ss, Run.mk ?_ ?_, ?_⟩
     · grind [concat, get_append_left]
     · have (k) (h_k : ¬ k < xs1.length) : k + 1 - xs1.length = k - xs1.length + 1 := by grind
       simp only [concat]
-      grind [Run, LTS.OmegaExecution, get_append_right', get_append_left, LTS.Execution]
+      grind only [Run, LTS.OmegaExecution, get_append_right', get_append_left,
+        = List.length_take, = get_map, = List.length_map, = min_def, = List.getElem_take,
+        = List.getElem_map]
     · grind [drop_append_of_le_length]
 
 namespace Buchi
@@ -138,20 +145,20 @@ namespace FinAcc
 
 /-- `finConcat na1 na2` is the concatenation of the "totalized" versions of `na1` and `na2`. -/
 def finConcat (na1 : FinAcc State1 Symbol) (na2 : FinAcc State2 Symbol)
-  : NA ((State1 ⊕ Unit) ⊕ (State2 ⊕ Unit)) Symbol :=
-  concat ⟨na1.totalize, inl '' na1.accept⟩ na2.totalize
+  : NA (Option State1 ⊕ Option State2) Symbol :=
+  concat ⟨na1.totalize, some '' na1.accept⟩ na2.totalize
 
 variable {na1 : FinAcc State1 Symbol} {na2 : FinAcc State2 Symbol}
 
 /-- `finConcat na1 na2` is total. -/
 instance : (finConcat na1 na2).Total where
   total s x := match s with
-    | inl _ => ⟨inl (inr ()), by grind [finConcat, concat, NA.totalize, LTS.totalize]⟩
-    | inr _ => ⟨inr (inr ()), by grind [finConcat, concat, NA.totalize, LTS.totalize]⟩
+    | inl _ => ⟨inl none, by grind [finConcat, concat, NA.totalize, LTS.totalize]⟩
+    | inr _ => ⟨inr none, by grind [finConcat, concat, NA.totalize, LTS.totalize]⟩
 
 /-- `finConcat na1 na2` accepts the concatenation of the languages of `na1` and `na2`. -/
 theorem finConcat_language_eq [Inhabited Symbol] :
-    language (FinAcc.mk (finConcat na1 na2) (inr '' (inl '' na2.accept))) =
+    language (FinAcc.mk (finConcat na1 na2) (inr '' (some '' na2.accept))) =
     language na1 * language na2 := by
   ext xl
   constructor
@@ -166,7 +173,7 @@ theorem finConcat_language_eq [Inhabited Symbol] :
       #adaptation_note
       /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
       have : ss xl.length = inr (ss2 (xl.length - n)) := by grind
-      have hl : (ss2 (xl.length - n)).isLeft := by grind
+      have hl : (ss2 (xl.length - n)).isSome := by grind
       obtain ⟨s2, t2, h_mtr2, _, _, _⟩ := totalize_run_mtr h_run2 hl
       refine ⟨s2, ?_, t2, ?_, ?_⟩ <;> grind [drop_append_of_le_length, take_append_of_le_length]
     · exact xl.take_append_drop n
@@ -177,7 +184,7 @@ theorem finConcat_language_eq [Inhabited Symbol] :
     obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2
     #adaptation_note
     /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-    have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length))
+    have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (a := xl1.length + xl2.length))
     simp [← append_append_ωSequence, extract_eq_drop_take,
       take_append_of_le_length, ← List.length_append] at h_mtr
     have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind

Cslib/Computability/Automata/NA/Hist.lean

@@ -49,14 +49,15 @@ def makeHist (start' : State → Hist) (tr' : State × Hist → Symbol → State
   | 0 => start' (ss 0)
   | n + 1 => tr' (ss n, makeHist start' tr' xs ss n) (xs n) (ss (n + 1))
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- For every run `ss` of the original automaton, there exists a run `ss'` of the history automaton
 which projects back onto `ss`. -/
 theorem hist_run_exists {xs : ωSequence Symbol} {ss : ωSequence State}
     (h_run : na.Run xs ss) : ∃ ss', (na.addHist start' tr').Run xs ss' ∧ ss'.map fst = ss := by
   use ⟨fun n ↦ (ss n, makeHist start' tr' xs ss n)⟩
   constructor
   · simp only [addHist]
-    grind [Run]
+    grind only [Run, usr Set.mem_setOf_eq, = get_fun, = LTS.OmegaExecution, makeHist]
   · grind
 
 end Cslib.Automata.NA

Cslib/Computability/Automata/NA/Loop.lean

@@ -92,6 +92,7 @@ theorem loop_run_one_iter {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ St
     exact neq.imp (congrArg List.length)
   · grind [loop_run_from_left]
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 open List in
 /-- For any finite word in `language na`, there is a corresponding finite run of `na.loop`. -/
 theorem loop_fin_run_exists {xl : List Symbol} (h : xl ∈ language na) :
@@ -127,7 +128,8 @@ theorem loop_run_exists [Inhabited Symbol] {xls : ωSequence (List Symbol)}
     ∃ ss, na.loop.Run xls.flatten ss ∧ ∀ k, ss (xls.cumLen k) = inl () := by
   let ts := ωSequence.const (inl () : Unit ⊕ State)
   have h_mtr (k : ℕ) : na.loop.MTr (ts k) (xls k) (ts (k + 1)) := by grind [loop_fin_run_mtr]
-  have h_pos (k : ℕ) : (xls k).length > 0 := by grind
+  have (k : ℕ) : xls k ≠ [] := by grind
+  have h_pos (k : ℕ) : (xls k).length > 0 := List.length_pos_iff.mpr (this k)
   obtain ⟨ss, _, _⟩ := LTS.OmegaExecution.flatten_mTr h_mtr h_pos
   use ss
   grind [Run.mk, FinAcc.loop, cumLen_zero (ls := xls)]
@@ -158,7 +160,10 @@ theorem loop_language_eq [Inhabited Symbol] :
     use ss, h_run
     apply frequently_iff_strictMono.mpr
     use xls.cumLen, ?_, by grind
-    grind [cumLen_strictMono, List.eq_nil_iff_length_eq_zero]
+    apply cumLen_strictMono
+    intro k
+    apply List.length_pos_iff.mpr
+    grind
 
 end Buchi
 
@@ -167,14 +172,14 @@ namespace FinAcc
 open scoped Computability
 
 /-- `finLoop na` is the loop construction applied to the "totalized" version of `na`. -/
-def finLoop (na : FinAcc State Symbol) : NA (Unit ⊕ (State ⊕ Unit)) Symbol :=
-  FinAcc.loop ⟨na.totalize, inl '' na.accept⟩
+def finLoop (na : FinAcc State Symbol) : NA (Unit ⊕ Option State) Symbol :=
+  FinAcc.loop ⟨na.totalize, some '' na.accept⟩
 
 /-- `finLoop na` is total, assuming that `na` has at least one start state. -/
 instance [h : Nonempty na.start] : na.finLoop.Total where
   total s x := match s with
-    | inl _ => ⟨inr (inr ()), by simpa [finLoop, loop, NA.totalize, LTS.totalize] using h⟩
-    | inr _ => ⟨inr (inr ()), by grind [finLoop, loop, NA.totalize, LTS.totalize]⟩
+    | inl _ => ⟨inr none, by simpa [finLoop, loop, NA.totalize, LTS.totalize] using h⟩
+    | inr _ => ⟨inr none, by grind [finLoop, loop, NA.totalize, LTS.totalize]⟩
 
 /-- `finLoop na` accepts the Kleene star of the language of `na`, assuming that
 the latter is nonempty. -/

Cslib/Computability/Automata/NA/Pair.lean

@@ -99,6 +99,7 @@ namespace Automata.NA.Buchi
 
 open Set Filter ωSequence ωLanguage ωAcceptor
 
+set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- The ω-language accepted by a finite-state Büchi automaton is the finite union of ω-languages
 of the form `L * M^ω`, where all `L`s and `M`s are regular languages. -/
 theorem language_eq_fin_iSup_hmul_omegaPow
@@ -110,11 +111,11 @@ theorem language_eq_fin_iSup_hmul_omegaPow
   constructor
   · rintro ⟨ss, h_run, h_inf⟩
     obtain ⟨t, h_acc, h_t⟩ := frequently_in_finite_type.mp h_inf
-    use ss 0, by grind [NA.Run], t, h_acc
+    use ss 0, by grind only [NA.Run], t, h_acc
     obtain ⟨f, h_mono, h_f⟩ := frequently_iff_strictMono.mp h_t
     refine ⟨xs.take (f 0), ?_, xs.drop (f 0), ?_, by grind⟩
     · have : na.MTr (ss 0) (xs.extract 0 (f 0)) (ss (f 0)) := by
-        grind [LTS.OmegaExecution.extract_mTr, NA.Run]
+        grind only [LTS.OmegaExecution.extract_mTr, NA.Run]
       grind [extract_eq_drop_take]
     · simp only [omegaPow_seq_prop, LTS.mem_pairLang]
       use (f · - f 0)
@@ -131,7 +132,7 @@ theorem language_eq_fin_iSup_hmul_omegaPow
     have h_mtr (n : ℕ) : na.MTr (ts n) (zls n) (ts (n + 1)) := by
       grind [Language.mem_sub_one, LTS.mem_pairLang]
     have h_pos (n : ℕ) : (zls n).length > 0 := by
-      grind [Language.mem_sub_one, List.eq_nil_iff_length_eq_zero]
+      grind only [Language.mem_sub_one, List.eq_nil_iff_length_eq_zero]
     obtain ⟨zss, h_zss, _⟩ := LTS.OmegaExecution.flatten_mTr h_mtr h_pos
     have (n : ℕ) : zss (zls.cumLen n) = t := by grind
     obtain ⟨xss, _, _, _, _⟩ := LTS.OmegaExecution.append h_yl h_zss