[david415]

Moves cryptlib to Lean v4.35.0, the latest stable release, with Mathlib, VCVio, cslib and Cli at their v4.35.0 tags and cborg at its 4.35.0 merge; the docs site (Verso) and API docs (doc-gen4) move to v4.35.0 too. The version becomes 0.2.0, since a new toolchain breaks dependents; the tag follows once every Katzenpost Lean package is on 4.35.0.

What VCVio v4.35.0 changed, and what follows here:

• Keccak moved from HashSig.SLHDSA.Concrete.Keccak to VCVio.Algorithms.Keccak, and sha3_256/sha3_512 are sha3Digest256/sha3Digest512, with the same definitions. ML-KEM and the group chat scenarios import the new module; the ML-KEM vectors and the 14 scenarios against katzenqt still pass, so no byte changed.
• Probability is measure-based: Pr[… | …], probOutput and NeverFail are gone in favour of Pr{let x ← mx}[p x] over Mathlib measures. VCVio's codemod (scripts/migrate-native-probability.py) converted the statements in Sphinx, BACAP and Sign/Blindable; the proofs it leaves were redone:
  • Util/UniformHit and Sphinx/Integrity with OracleComp.prEvent_bind_eq_tsum and SampleableType.prEvent_uniformSample_eq_singleton;
  • Sphinx/Indistinguishability with prEvent_bind_congr, OracleComp.prEvent_bind_bind_swap, ProbComp.evalDist_decide_eq_uniformBool_half, and a lemma prEvent_bind_unused for a draw whose result is unused. The DDH and PRG experiments were renamed (ddhExpReal → ddhRealExperiment, prgRealExp → prgRealExperiment, …) with unchanged definitions. ddhDistAdvantage is gone; advantage_le now states its DDH hypothesis as that definition read, |Pr[real] - Pr[random]| ≤ εDDH, as it already states the two PRG ones, so the theorem says what it said. NeverFail binders are dropped: a ProbComp never fails.
• Lean 4.35.0: List.eraseP_cons unfolds to if instead of bif, so one simp set in Member/ReaderProofs takes Bool.false_eq_true, ↓reduceIte.

Mathlib came from its cache throughout (lake exe cache get); nothing of it was compiled. Locally: lake build of the library and every CI target; all 15 CI test executables pass; scripts/check-axioms.sh finds every group chat theorem on Lean's own axioms; no sorry; bench builds (LeanBench unchanged); the Verso site and doc-gen4 build.