Proposal: lawful lenses for verified state access

Problem

Verified computer-science developments often need structured state updates over records. When modeling interpreters, simulators, or incremental transformations, authors repeatedly write the same pattern: read a field from a state record, compute an updated value, and write it back while preserving unrelated fields. Without a shared abstraction, each project reimplements getters, setters, and the algebraic laws that make those updates composable and trustworthy.

Proposed minimal API

A small lawful lens core for verified state access (not category theory or profunctor optics):

structure Lens (S A : Type u) where
  get : S → A
  set : S → A → S

structure LawfulLens (S A : Type u) extends Lens S A where
  get_set : ∀ s a, get (set s a) = a
  set_get : ∀ s, set s (get s) = s
  set_set : ∀ s a b, set (set s a) b = set s b

Plus:

• over — update the focused component with a function
• compose — chain nested field access

Example: interpreter state

structure MachineState where
  pc : Nat
  memory : List Nat
  halted : Bool

A lawful lens for pc, a step function that increments pc when not halted, and proofs that step preserves memory and halted.

This pattern is exercised in lean-optics (Optics.Examples.MachineState) as an extraction candidate; see also docs/upstream/CSLIB_LENS_PROPOSAL.md in that repo.

Why CSLib

CSLib is the right venue for executable state semantics and verified transformations without tactic automation. The API should be small enough to review in one sitting and strong enough to support verified record updates in algorithms, semantics, and systems formalizations.

Explicitly out of scope (for this first PR)

• Profunctor hierarchy and optic generalizations
• Prisms, traversals, and other optic variants
• Macros (lens!, field-syntax sugar)
• optic_laws! and other tactic automation
• Telemetry and benchmarks

Suggested placement

Cslib/Foundations/Data/Lens/ (or similar under Foundations), with one self-contained example module.

Mathlib

Not proposed for this slice. Mathlib optimizes for mathematical structure; the immediate need is a tiny, law-carrying API for executable state in CS developments.

Next step

Happy to open a draft PR with only the minimal API + MachineState example if maintainers agree with the framing. Feedback welcome on naming, placement, and whether composition laws should ship in v1.

Start by reading docs/upstream/CSLIB_LENS_PROPOSAL.md and the Optics.Examples.MachineState example in lean-optics, then compare the proposed placement under Cslib/Foundations/Data/Lens/. A complete contribution would need maintainer agreement on naming and composition scope, followed by the minimal lens API and one self-contained MachineState example with its stated laws.