README: the "Present so far" status list is stale

[daira]

The "Present so far" list under "Status" in README.md has fallen behind the tree. It stops at the fast Vesta arithmetic and does not mention the group-hash work (the simplified SWU mapping, the 3-isogenies, the character-sum and Weil-bound analysis), the curve-order proofs, the Jubjub scalar field, the higher-power residue criterion, the spec's encoding primitives, or the census tooling. Two nearby paragraphs are stale in the same way: the trust paragraph says the compiler-trust axiom is confined "chiefly [to] the order of the Tonelli–Shanks roots of unity", while TrustBoundary.lean now also pins the prime-order witnesses behind the group orders and the concrete hash-to-curve facts (isogeny bijectivity, oddness, character-sum, fibre, and Weil-bound instances); and "Uses of sorry are kept minimal" could say that there are none.

Suggested replacement for the list (every bullet checked against the module docs; the last one is on the aarch64-pasta-mul branch and belongs in only once that lands):

Early work in progress. Present so far:

- the Pasta (Pallas/Vesta) base and scalar prime fields and the Jubjub scalar field, each with a
  machine-verified Pratt primality certificate (`CompElliptic/Fields/Pasta.lean`,
  `CompElliptic/Fields/Jubjub.lean`);
- a computable short-Weierstrass affine group law with correct-by-construction `SWCurve` /
  `SWPoint` types — closure, commutativity, associativity, and the full `AddCommGroup (SWPoint E)`
  instance, with associativity by transport to Mathlib's `WeierstrassCurve.Affine.Point` group
  (`CompElliptic/CurveForms/ShortWeierstrass.lean`), and scalar multiplication by binary
  double-and-add supplying the `nsmul` field in `O(log n)` group operations
  (`CompElliptic/ScalarMul.lean`);
- Pallas and Vesta as concrete `SWCurve` instances (`CompElliptic/Curves/Pasta.lean`), with their
  group orders pinned without point-counting — a prime-order witness plus the elementary fibre
  bound `#E(F) ≤ 2·#F + 1`, no Hasse (`CompElliptic/CurveOrder.lean`,
  `CompElliptic/Curves/PastaOrder.lean`);
- a curve-form-agnostic `CoordinateSystem` abstraction — a carrier with a validity predicate, an
  equivalence on representatives, and computable operations — yielding a derived `AddCommGroup` on
  the quotient, with affine as the `Rel = Eq` instance (`CompElliptic/CoordinateSystem.lean`);
- an `Encoding` abstraction distinguishing `CanonicalEncoding` from `LenientEncoding` over a shared
  `EncodingClass` interface, with encoded values ("depictions") tagged `Raw` / `Decodable` /
  `Canonical`, the bijection `G ≃ Canonical e`, and the canonical-versus-decodable distinction
  (`CompElliptic/Encoding.lean`); the protocol specification's integer / bit-sequence / octet-string
  primitives with lengths in the types and endianness in the names (`CompElliptic/Encodings/Common.lean`);
  and the compressed Pasta point encoding (`toBytes`) for Pallas and Vesta
  (`CompElliptic/Encodings/Pasta.lean`);
- a computable Tonelli–Shanks square root for prime fields, soundness and completeness proved, with
  `pallasBase` / `vestaBase` instances (`CompElliptic/Fields/Sqrt.lean`), and the easy direction of
  the n'th-power residue criterion, used for the concrete non-residue facts about the Pasta fields
  and for RFC 9380's irreducibility criterion (`CompElliptic/Fields/Residue.lean`);
- degree-3 isogenies from Vélu's formulae, with the homomorphism property on rational points proved
  from polynomial certificates rather than assumed (`CompElliptic/Isogenies/`), and the iso-Pasta
  curves with their isogenies to Pallas and Vesta, each stated both as the Vélu derivation and as
  the specification's `iso_map` (`CompElliptic/Curves/IsoPasta.lean`);
- the group hash: the simplified SWU mapping as specified in §5.4.9.8, including `sqrt_ratio`
  (`CompElliptic/Hashing/SimplifiedSWU.lean`), with the deployed Pasta parameters tied to
  `pasta_curves` and `hashtocurve.sage` (`CompElliptic/Hashing/PastaSSWU.lean`); the signed lift
  and the oddness of the mapping (`SignedLift.lean`); character sums of odd mappings
  (`CharacterSum.lean`) and two-term uniformity from the `WeilBounded` hypothesis
  (`TwoTermUniformity.lean`); the Weil bound itself as an external input (`WellDistributed.lean`,
  `WeilInstance.lean`), whose algebraic inputs are machine-checked (`WeilSupport.lean`,
  `BranchCovers.lean`) and whose two geometric steps are cited from
  `design/weil-constant-derivation.md` (#28, #30); and the per-point fibre bound the
  indifferentiability sampler consumes (`FibreBound.lean`, #25);
- fast Vesta group arithmetic for computing with points rather than only reasoning about them —
  complete Renes–Costello–Batina projective addition, a windowed Pippenger multi-scalar
  multiplication (also run entirely in projective coordinates) and a scalar ladder, each proven to
  compute the affine group operation it replaces, together with a natively compilable
  Montgomery-limb kernel proven against them (`CompElliptic/Curves/Pasta/Fast/`, not imported by
  `CompElliptic.lean`). These interfaces are provisional: they are not guaranteed to remain public,
  and may be folded into the existing API or otherwise changed incompatibly;
- the build-checked trust census: `assert_axioms` / `assert_computable`
  (`CompElliptic/Meta/AxiomCheck.lean`) pinning every representative declaration's trusted base in
  `CompElliptic/TrustBoundary.lean`, with CI re-checking the whole library under nanoda, an
  independent implementation of the kernel;
- a transcription of the AArch64 Pasta Montgomery routines that pasta_curves vendors from
  Semolina, generated from the assembly over a small instruction-semantics module, with
  reference vectors from the real routines checked by the kernel (`CompElliptic/Asm/AArch64/`;
  `design/aarch64-pasta-mul-verification.md` states the intended correctness theorems).

And for the two paragraphs that follow the list:

The library's general theorems depend only on the standard `propext` / `Classical.choice` /
`Quot.sound` axioms. Facts specific to concrete fields and curves additionally depend on
`native_decide`'s per-declaration compiler-trust axiom, confined —per the *Independently
re-checkable trust* principle— to checks the kernel cannot feasibly run: the order of the
Tonelli–Shanks roots of unity, the prime-order witnesses behind the group orders, and the concrete
hash-to-curve facts (isogeny bijectivity, oddness, and the character-sum, fibre, and Weil-bound
instances). The tier of each is pinned in `CompElliptic/TrustBoundary.lean`.

There are currently no uses of `sorry`, and, as stated above under "Trust discipline", no uses of
`@[csimp]` replacement.

The "Acknowledgements" line names only Claude Opus 4.8; the commit trailers also credit Claude Fable 5 and Claude Fable 5.1.

🤖 Claude Fable 5.1