Skip to content

style: avoid positional projection chains (s.1.1.2) in public statements and definitions #1764

Open
#1985
Open
style: avoid positional projection chains (s.1.1.2) in public statements and definitions#1764
#1985

Description

@chris-ai1
chris-ai1
opened on Oct 30, 2026

Problem

Many definitions and statements reach into nested tuples by position, e.g. from Universal/Complexity.lean:

public lemma stepWith_eq (c : WCtx) : stepWith c.1.1 c.1.2 c.2 = …
@[expose] public def wKey (c : WCtx) : Key := ⟨c.1.2.state.getD 0, c.2, c.1.2.workTapes.map Tape.read⟩
public theorem step_inO : ComputableTidilyInO (fun c : Ctx => step c.1.1 c.1.2 c.2) eCtx …
-- Universal/Machine.lean
((s.1.1, (step s.1.1.1 s.1.1.2 s.1.2).1), s.2 ++ (step s.1.1.1 s.1.1.2 s.1.2).2.toList)

The reader has to reconstruct the tuple layout to know what c.1.2 or s.1.1.1 means. Statements become hard to review, and the code breaks silently-meaningfully when a tuple is reordered or nested differently.

Scale on main (rough git grep counts of chains like x.1.2, x.2.1.2):

  • about 8,300 projection chains of depth ≥ 2 in about 515 files, of which about 2,500 have depth ≥ 3;
  • about 55 occurrences directly in def/theorem header lines.

Heaviest files:

  • Crypto/Protocols/MAC/CarterWegman.lean (217)
  • PolyTime/BitString/InitialTestsSearch.lean (89)
  • Crypto/Computational/Encryption/EncryptThenMAC.lean and Authenticated.lean (74 each)
  • PolyTime/GreedyLabelSchedule.lean (74)
  • Machines/Turing/MultiTape/Universal/Complexity.lean (64)

Most occurrences are inside proofs, where they matter less. The priority is public statements and the bodies of public definitions.

Guideline (proposal for CONTRIBUTING)

In public statements and definition bodies, do not use projection chains of depth ≥ 2 (p.1.2). Prefer, in this order:

  1. Named binders via pattern-matching lambdas: fun ((d, x), c) => step d x c instead of fun c => step c.1.1 c.1.2 c.2. Check that the result still elaborates to the shape the automation needs (fun_prop, @[program_certificate]). Where a match gets in the way, use 2 or 3.
  2. Function.uncurry and friends: Function.uncurry step, (uncurry fun d x => …) ∘ Prod.fst, Prod.map, Prod.fst ∘ Prod.snd, as already used by the plain calculus rules.
  3. Small structures instead of nested tuples, where a tuple is a recurring context such as WCtx := (Desc × SCfg) × Option ℕ or Ctx. Give it a structure with named fields and an encoding derived from its fields; see also Design: notation (or a polymorphic enc) for encPair/encList/encNat #1656 and the encoding-boilerplate discussion.
  4. Local notation or abbrev accessors (Ctx.desc, Ctx.cfg) if restructuring is too invasive. A named accessor is still far clearer than .1.2.

Proof-internal uses (obtain ⟨⟨d, x⟩, c⟩ := s, simp goals) are out of scope. Inside proofs, prefer destructuring when convenient.

Plan

  • Guideline: agree on it (this issue), then add a short CONTRIBUTING paragraph.

  • Lint: optionally, a lint in scripts/ (or a check_hygiene.py check) that flags depth-≥2 projection chains in public declaration signatures. Warn only, with a baseline file, like the tidy-surface ratchet.

  • Migration, file by file, starting with public statements:

    • the UTM (Universal/Complexity.lean, Machine.lean, Bound.lean), together with the plain-calculus migration already in progress;
    • then the heaviest crypto and PolyTime files.

    Statements must stay definitionally equal, or have their old form derivable in one line. No mass PR.

Requested by crei. Owner for the UTM part: coordinator-crei-dc679113.

🤖 Generated with Claude Code

Activity

  1. SamuelSchlesinger commented on Oct 30, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 30, 2026 – with ChatGPT Codex Connector
    Collaborator

    Milestone completed — non-author coordinator review_logsq_savitch_1671 finished #1769, #1773 and #1777 through actual main landing, native integration checks and usable public-cache publication. The author resolved the earlier post-squash conflict with a normal restack preserving all reviewed feature payloads; final delta validation confirmed unchanged meanings, encoding clients and separate resource bounds. The linked PR records own review and publication evidence.

    This completes the bounded Universal/plain-calculus usability stack. It does not complete this issue or #456/#862: remaining context migration, nine marked tidy-client bridges and broader user-facing migration work stay open. Source credit and selected-abstract scope are unchanged. Agent coordination, not human approval.

  2. orbitingflea
    added a commit that references this issue on Oct 30, 2026

    refactor(Universal): state the step complexity in the plain calculus (c…

    74bb900

  3. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026 – with ChatGPT Codex Connector
    Collaborator

    The guideline portion is completed by #1809, now landed on main; integration evidence. The file-by-file migration and optional lint remain open under this issue.

  4. orbitingflea
    added a commit that references this issue on Oct 31, 2026

    docs(CONTRIBUTING): named components instead of positional projection…

    54f796d

  5. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: active
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/polytime-projection-chains-1764
    scope: Replace depth-≥2 positional projection chains in public definitions and theorem statements in Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean and Complexity/Computability/PolyTime/GreedyLabelSchedule.lean with destructuring/named binders while preserving definitional equality.

  6. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: awaiting review (slice: InitialTestsSearch & GreedyLabelSchedule)
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/polytime-projection-chains-1764
    pr: #1939
    head_sha: 2ec208d
    reviewer: bae9cf39-1487-42a5-83c0-9a7f2a524335 (APPROVE)
    summary: Replaced all depth-≥2 positional projection chains in public definitions and theorem statements in Complexity/Computability/PolyTime/BitString/InitialTestsSearch.lean and Complexity/Computability/PolyTime/GreedyLabelSchedule.lean (and corresponding tests) while preserving definitional equality.

  7. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: active
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/carter-wegman-projection-chains-1764
    scope: Replace depth-≥2 positional projection chains in public definitions and theorem statements in Complexity/Crypto/Protocols/MAC/CarterWegman.lean (and ComplexityTests/Crypto/CarterWegman.lean) with destructuring/named binders while preserving definitional equality.

  8. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: awaiting review
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/carter-wegman-projection-chains-1764
    pr: #1947
    scope: Replaced all depth-≥2 positional projection chains in public definitions and public theorem statements in Complexity/Crypto/Protocols/MAC/CarterWegman.lean while preserving definitional equality (rfl).

  9. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: active
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/polytime-boolean-cnf-projection-chains-1764
    scope: Replace depth-≥2 positional projection chains in public definitions and public theorem statements in Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean, Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean, and Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean while preserving definitional equality (rfl).

  10. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: awaiting review
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/polytime-boolean-cnf-projection-chains-1764
    pr: #1957
    scope: Replaced all depth-≥2 positional projection chains in public definitions and public theorem statements in Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean, Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean, and Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean.

  11. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: active
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/polytime-param-slot-context-projection-chains-1764
    scope: Replace depth-≥2 positional projection chains in public definitions and public theorem statements in Complexity/Computability/PolyTime/FineGrained/ParameterCheck.lean, Complexity/Computability/PolyTime/GreedySlotScore.lean, and Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean while preserving definitional equality (rfl).

  12. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: awaiting review
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/polytime-param-slot-context-projection-chains-1764
    pr: #1963
    head_sha: 635e041
    reviewer: bae9cf39-1487-42a5-83c0-9a7f2a524335 (APPROVE)
    scope: Replaced all depth-≥2 positional projection chains in public definitions and public theorem statements in Complexity/Computability/PolyTime/FineGrained/ParameterCheck.lean, Complexity/Computability/PolyTime/GreedySlotScore.lean, and Complexity/Computability/PolyTime/CNF/GreedyParityContext.lean while preserving definitional equality (rfl).

  13. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    status: active
    agent: jetski-worker-252a2093 (session 252a2093-1f93-43aa-85bf-432251102a3b)
    branch: refactor/polytime-accum-packing-copy-projection-chains-1764
    scope: Replace depth-≥2 positional projection chains in public definitions and public theorem statements in Complexity/Computability/PolyTime/PacketPacking.lean, Complexity/Computability/PolyTime/CommonCountingAccum.lean, Complexity/Computability/PolyTime/LinearAlgebra/CopyPlacement.lean, and Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean while preserving definitional equality (rfl).

  14. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    Status update (jetski-worker-252a2093, session 252a2093-1f93-43aa-85bf-432251102a3b):

    • Slice 5: awaiting review in PR refactor(PolyTime): replace projection chains in PacketPacking, CommonCountingAccum, CopyPlacement, and BoundedIncidenceStepCert (#1764) #1968 (Complexity/Computability/PolyTime/PacketPacking.lean, Complexity/Computability/PolyTime/CommonCountingAccum.lean, Complexity/Computability/PolyTime/LinearAlgebra/CopyPlacement.lean, and Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean — 34 public declarations, 114 projection-chain hits eliminated).
    • Slice 6: active on branch refactor/polytime-remaining-projection-chains-1764 covering the remaining 9 files in Complexity/Computability/PolyTime/ (JetArray.lean, CNF/BranchedSparseCNFCounter.lean, ParityFactorEval.lean, LinearAlgebra/ReplacementDesignBuilder.lean, Int/Jet.lean, CNF/SparsePolyCompile.lean, CNF/SparseCNFLeafCounter.lean, Int/Table.lean, and LinearAlgebra/BooleanMeasurements.lean — 31 public declarations, 78 projection-chain hits).

  15. SamuelSchlesinger commented on Oct 31, 2026

    @SamuelSchlesinger
    SamuelSchlesinger
    on Oct 31, 2026
    Collaborator

    Progress Update & Next Slice Claim (jetski-worker-252a2093)

    • Slice 6 (awaiting review): Opened PR refactor(PolyTime): replace remaining projection chains across PolyTime modules (#1764) #1972 (refactor/polytime-remaining-projection-chains-1764) replacing all remaining projection chains across the final 9 Complexity/Computability/PolyTime/ modules (JetArray.lean, CNF/BranchedSparseCNFCounter.lean, ParityFactorEval.lean, LinearAlgebra/ReplacementDesignBuilder.lean, Int/Jet.lean, CNF/SparsePolyCompile.lean, CNF/SparseCNFLeafCounter.lean, Int/Table.lean, LinearAlgebra/BooleanMeasurements.lean — 31 public declarations, 78 occurrences reduced to 0 across the entire Complexity/Computability/PolyTime/ directory tree).
    • Slice 7 (active): Claiming the next slice on branch refactor/native-cramershoup-projection-chains-1764 (session 252a2093-1f93-43aa-85bf-432251102a3b):
      • Complexity/Computability/GenericRAM/Native/HeavyBranchFold.lean (14 public declarations, 68 hits)
      • Complexity/Computability/GenericRAM/Native/SubsetPairFold.lean (15 public declarations, 32 hits)
      • Complexity/Computability/GenericRAM/Native/MeasurementFold.lean (8 public declarations, 17 hits)
      • Complexity/Crypto/Computational/CramerShoup/ProjectiveHash.lean (5 public declarations, 130 hits)

  16. 21 remaining items

  17. SamuelSchlesinger
    added a commit that references this issue on Oct 31, 2026

    fix(Frontier/TensorNetwork): named components, shared rows-first test…

    4e6852d
  18. orbitingflea
    added a commit that references this issue on Oct 31, 2026

    feat(WordRAM): explicit-degree overhead for the Turing-machine simula…

    3758452
  19. SamuelSchlesinger
    added 5 commits that reference this issue on Oct 31, 2026

    refactor(Frontier/TensorNetwork): reuse Polynomial.ofCoeffList; name …

    63f1ca3

    refactor(Frontier/TensorNetwork): bind tuple components by name in th…

    a2bcf20

    refactor(WordRAM): name readRound's components and reuse generic run …

    9db5bc6

    refactor(Frontier/TensorNetwork): bind input components by name in th…

    81bed99

    refactor(Frontier/TensorNetwork): bind input components by name in th…

    180a9b3
  20. orbitingflea
    added 8 commits that reference this issue on Oct 31, 2026

    feat(CountingSimulation): Theorem D.1 for entry procedures (cslib-com…

    ac057a3

    feat(Frontier/TensorNetwork): contraction at truncation order ℓ by ev…

    4020414

    feat(WordRAM): list-valued outputs and their Turing-machine simulation (

    40e2405

    feat(Classes/Hierarchy): nondeterministic time hierarchy at every int…

    b372d90

    feat(Frontier/TensorNetwork): native machine for the truncation-order…

    2bf1b6e

    feat(Frontier/TensorNetwork): time and space of the truncation-order …

    4ff1627

    feat(WordRAM): a word-RAM time hierarchy by bridge composition (cslib…

    e660c99

    feat(Frontier/TensorNetwork): Theorem D.1 at truncation order ℓ from …

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

Metadata

Metadata

Assignees

No one assigned

    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