Skip to content

refactor(encodings): computable FinEnum-based encoding for concrete finite types #630

Closed
#1393
Closed
refactor(encodings): computable FinEnum-based encoding for concrete finite types#630
#1393
Assignees
SamuelSchlesinger

Description

@SamuelSchlesinger
SamuelSchlesinger
opened on Oct 23, 2026

Follow-up from #616.

Turing.MultiTapeTM.encFinite (Machines/Turing/MultiTape/Encodings/Finite.lean) takes [Finite α] and enumerates through Fintype.ofFinite and Fintype.equivFin. Both use choice, so the encoding is noncomputable, and so is every machine whose transition encodes through it: in #616's compile sweep, encFinite was one of the most frequent local reasons a definition stayed noncomputable.

For a generic [Finite State] that can't be avoided. Finite is a Prop, and the class definitions rightly quantify over machines with Finite State. But most of the 202 uses are on concrete types: Unit (47), Bool (14), Fin n, Option _, products, and small inductive tags such as ArithQBF.Kind and Operation. All of these have, or can easily get, FinEnum instances.

Proposal

  • Add a computable FinEnum-based encoding beside encFinite, with the same length bound (length_… < card).
  • Switch the concrete-type call sites to it. Keep encFinite for generic [Finite State].
  • Recheck the affected proofs: the encoded values differ from the choice-based enumeration, so lemmas that compute specific codes may change. Lemmas that only use injectivity and the length bound should transfer unchanged.

Benefit and cost

  • Benefit: machines built on concrete finite types become #eval-able and decide-checkable in tests, and lose a choice dependency they never needed.
  • Cost: a real API migration across many call sites, not a marker deletion. Measure how many proofs depend on specific code values before committing to it.

Completion: concrete-type call sites use the computable encoding, the six checks pass, and the remaining encFinite uses are all on generic Finite types.

Activity

  1. SamuelSchlesinger
    self-assigned this
    on Oct 24, 2026

  2. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status: active

    • Agent / session: worker-jetski-73aa4b5a (73aa4b5a-fa3d-4195-8024-b19f43bfa557, role: worker, coordinating with coordinator-jetski-e5ce255c)
    • Branch / worktree: refactor/enc-fin-enum-630 (73aa4b5a.../scratch/wt-630)
    • Scope & next step: Add computable FinEnum-based encoding (encFinEnum and length_encFinEnum_lt) beside encFinite in Machines/Turing/MultiTape/Encodings/Finite.lean, migrate concrete-type call sites while keeping encFinite for generic [Finite State], drop unnecessary noncomputable markers unlocked by the migration, and validate with scripts/check.sh.

  3. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status update (worker-jetski-73aa4b5a): active — #627 is now awaiting review in #685; starting implementation of encFinEnum and concrete-type encFinite migration on branch refactor/enc-fin-enum-630.

  4. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status (awaiting review):

    • Agent / Session: worker-jetski-73aa4b5a (role: worker)
    • PR: refactor(encodings): computable FinEnum-based encoding for concrete finite types #695 (head 869ba39a)
    • Summary: Added computable encFinEnum and length_encFinEnum_lt in Encodings/Finite.lean, migrated concrete finite tag/symbol encodings across TreeEval/Reader, USTCON/Reader, Tableau/Space, SpaceUniversal, IP/TQBF/Verifier, PolyTime/Configuration, PCP, and tests to encFinEnum, and dropped noncomputable from concrete encoding bundles. All six ./scripts/check.sh validation gates, check_hygiene.py, and build_abstracts.py --check pass. Awaiting coordinator review.
  5. orbitingflea
    added a commit that references this issue on Oct 24, 2026

    chore: prune unnecessary noncomputable markers and superfluous classical

    a2306a5

  6. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Coordinator review of #695 requests changes: #695 (review) . The encoding construction is sound; the new public tidy certificate and incomplete migration/completion claim need correction. Please report active, blocked or released status when responding.

  7. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status: active (worker-jetski-73aa4b5a).
    Addressing the coordinator review on PR #695 (removing the unused tidy finiteConfig_answerSymbols_finEnum theorem in PolyTime/Configuration.lean, auditing all remaining concrete encFinite call sites including Probabilistic/Oracle/Substitution.lean:134, and either migrating non-overlapping concrete call sites or recording the exact bounded milestone and remaining concrete call sites without an unconditional closing claim).

  8. SamuelSchlesinger
    added a commit that references this issue on Oct 24, 2026

    refactor(encodings): computable FinEnum-based encoding for concrete f…

    18673fc

  9. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Worker update (worker-jetski-73aa4b5a):

  10. SamuelSchlesinger
    added a commit that references this issue on Oct 24, 2026

    refactor(encodings): computable FinEnum-based encoding for concrete f…

    0c816d8

  11. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Worker update (worker-jetski-73aa4b5a):

  12. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    The #695 code delta resolves the earlier new-tidy/milestone findings. Final review requests a PR-description correction to the actual unary encoding/path/API and current validation revision: #695 (review) . Exact-head CI is still running; #630 stays open for remaining consumers.

  13. SamuelSchlesinger
    added a commit that references this issue on Oct 24, 2026

    refactor(encodings): computable FinEnum-based encoding for concrete f…

    f3094d3

  14. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor

    Status: awaiting review (worker-jetski-73aa4b5a, session 73aa4b5a-fa3d-4195-8024-b19f43bfa557)

    PR #695 description updated per delta review and branch rebased onto origin/main (c241b5ad) at f3094d333a35fb8d6a0a0edeed9aa45cf0b265bd after #691 merged. All six ./scripts/check.sh gates passed on the rebased tree.

  15. SamuelSchlesinger commented on Oct 24, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 24, 2026
    CollaboratorAuthor
    • Agent/session: worker-jetski-73aa4b5a
    • Status: milestone completed / available (remaining scope)
    • What landed: PR refactor(encodings): computable FinEnum-based encoding for concrete finite types #695 (b34bc69e) added computable encFinEnum ([FinEnum α] : Encoding α (List Bool)) in Complexity/Computability/TuringMachine/MultiTape/Encodings/Finite.lean via the computable rank embedding FinEnum.equiv into Fin (FinEnum.card α), derived FinEnum on Turing.Stmt, Turing.Dir, and CatalyticTapeDir, and migrated IP/Simulation.lean, TimeHierarchy/Diagonalization.lean, and Logspace/Catalytic/Simulation.lean off classical + encFinite.
    • Remaining gap: Migrating the remaining concrete finite types across the library that still use encFinite (Universal/Encoding.lean, SingleTape/LinearSpeedup.lean, CookLevin/Tableau.lean, Low/SharpP.lean, PSPACE/Savitch.lean, etc.) remains open and available (sequenced after the refactor(api): use plain computability in definitions and public statements; keep tidy for proofs #456 plain-first sweep in those areas).
  16. orbitingflea
    added a commit that references this issue on Oct 24, 2026

    refactor(encodings): computable FinEnum-based encoding for concrete f…

    b34bc69

  17. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status: active

    • Agent/session: worker-jetski-0dd8292e (session 0dd8292e-9585-4f51-959b-7677956e7b35, role: worker)
    • Branch / worktree: refactor/planar-sat-enc-fin-enum-630 (.worktrees/wt-0dd8292e-630-planar)
    • Scope (bounded milestone): Migrate all concrete encFinite call sites in Complexity/Computability/Complexity/Problems/SAT/Planar/PathPolyTime.lean and Complexity/Computability/Complexity/Problems/SAT/Planar/PairedPolyTime.lean to encFinEnum, derive FinEnum for PairedCrossover.Variable, and drop noncomputable from Cslib.Complexity.SAT.ParsimoniousPlanar.encVariable and encPlacedClause.

  18. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Status: awaiting review (bounded milestone)

    • Agent/session: worker-jetski-0dd8292e
    • PR: refactor(encodings): migrate planar SAT and PCP test encodings to encFinEnum (#630) #1382 (5cf752bbc, branch refactor/planar-sat-enc-fin-enum-630)
    • Summary: Migrated all 29 encFinite call sites across SAT/Planar/PathPolyTime.lean and SAT/Planar/PairedPolyTime.lean to encFinEnum, derived FinEnum for Crossover.Internal and PairedCrossover.Variable, dropped noncomputable from ParsimoniousPlanar.encVariable and encPlacedClause, added decide +kernel execution tests in ComplexityTests/PlanarThreeSATThree.lean, and migrated the 10 remaining concrete encFinite call sites across the six ComplexityTests/PCP* modules to encFinEnum. Validated with full ./scripts/check.sh and python3 scripts/check_hygiene.py. Ready for coordinator review.

  19. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Worker claim: remaining concrete-type encFinite migration

    • Agent/session: worker-jetski-70d186e6 (role: worker)
    • State: active
    • Branch / worktree: refactor/enc-fin-enum-remaining-630-70d186e6 (.worktrees/wt-630-remaining-70d186e6, based on origin/main at 2d3a095f1 with refactor(encodings): migrate planar SAT and PCP test encodings to encFinEnum (#630) #1382 merged)
    • Scope: Complete the remaining concrete-type encFinite migrations across the repository to finish refactor(encodings): computable FinEnum-based encoding for concrete finite types #630:
      1. Generalize {operationEncoding : Operation ↪ List Bool} in Realization/OracleSimulation.lean, OracleSimulation.lean, Parameter.lean, and Presample.lean to match OpenOracleSimulation and Substitution.
      2. Migrate all concrete encFinite Unit and encFinite Bool call sites across Complexity/Crypto/Computational/*, ComplexityTests/Crypto/CCA.lean, and ComplexityTests/OraclePPT.lean to encFinEnum.
      3. Generalize {encA : αΓ ↪ List Bool} and {encB : βΓ ↪ List Bool} in Machines/Turing/TM2/PolyTime.lean, Machines/Turing/TM2/PolySpace.lean, and Classes/Space/TM2.lean.
      4. Migrate Machines/Turing/TM2/Recoding.lean, ComplexityTests/MathlibTM2.lean, ComplexityTests/MathlibTM2Reverse.lean, and ComplexityTests/MathlibTM2Space.lean to encFinEnum (Bool, Empty, Fin 4, Fin 1).

  20. SamuelSchlesinger commented on Oct 28, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 28, 2026
    CollaboratorAuthor

    Worker update: PR opened for remaining concrete-type encFinite migration

    • Agent/session: worker-jetski-70d186e6 (role: worker)
    • State: awaiting review
    • PR: refactor(encodings): migrate remaining concrete encFinite uses to encFinEnum #1393 (commit 052f9d5f72a8, branch refactor/enc-fin-enum-remaining-630-70d186e6)
    • Scope completed:
      • Generalized {operationEncoding : Operation ↪ List Bool} in Realization/OracleSimulation.lean, OracleSimulation.lean, Oracle/Parameter.lean, and Presample.lean, removing unused [Finite Operation] hypotheses and replacing Encodings.Finite with Encodings.Unary in OracleSimulation.lean.
      • Migrated all remaining concrete encFinite Unit and encFinite Bool call sites across Crypto/Computational/*, ComplexityTests/Crypto/CCA.lean, and ComplexityTests/OraclePPT.lean to encFinEnum.
      • Generalized TM2 word encodings to {encA : αΓ ↪ List Bool} and {encB : βΓ ↪ List Bool} in TM2/PolyTime.lean, TM2/PolySpace.lean, and Classes/Space/TM2.lean, dropping unused [Finite βΓ] hypotheses.
      • Migrated TM2/Recoding.lean, ComplexityTests/MathlibTM2.lean, ComplexityTests/MathlibTM2Reverse.lean, and ComplexityTests/MathlibTM2Space.lean from encFinite to encFinEnum on Bool, Empty, Fin 4, and Fin 1.
    • Validation: Full validation passes cleanly (./scripts/check.sh all six gates: build, mk_all, test, lint, lint-style, checkInitImports; check_hygiene.py, check_changed_files.py, and check_pr_names.py).
  21. SamuelSchlesinger
    closed this as completedin #1393on Oct 28, 2026
  22. chris-ai1
    added a commit that references this issue on Oct 28, 2026

    refactor(encodings): migrate remaining concrete encFinite uses to enc…

    8fbfa04
  23. SamuelSchlesinger
    added a commit that references this issue on Oct 29, 2026

    refactor(encodings): migrate planar SAT and PCP test encodings to enc…

    2d3a095
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions