Instead of having the postcondition guarded by an assumption of
coprimality, there is now a precise case analysis in the specification
asserting that it returns zero in the degenerate cases. For now, this
is worked around in other proofs, but it gives scope for actually
avoiding the special-case reasoning about zero in many such
applications.

The ABI only requires preservation of the low 64-bit parts of
Q8,...,Q15, and MAYCHANGE_REGS_AND_FLAGS_PERMITTED_BY_ABI now
reflects that with new entries Q8 :> tophalf; ...; Q15 :> tophalf.
The subroutine boilerplate tactic ARM_ADD_RETURN_STACK_TAC is now
updated (somewhat crudely) to accept save/restore of D8,...,D15
in the prologue and epilogue of functions.

This completely changes the implementation of ARM curve25519_x25519
and curve25519_x25519_byte (not the _alt forms, which remain faster
on their target microarchitectures) to a base-25.5 unsaturated version
with interleaved integer and SIMD operations, the inner loop closely
following Emil Lenngren's implementation described in the paper

  https://github.com/Emill/X25519-AArch64/blob/master/X25519_AArch64.pdf

and available here:

  https://github.com/Emill/X25519-AArch64

A version of this code was generated by SLOTHY from the reorganized
implementation by Abdulrahman, Becker, Kannwischer and Klein here:

 https://github.com/slothy-optimizer/slothy/blob/main/paper/clean/neon/X25519-AArch64-simple.s

as described in the associated paper

  https://eprint.iacr.org/2022/1303.pdf

with some additional annotations for use in the formal proof. The
final modular inverse computation reverts to the usual saturated
representation and s2n-bignum's divstep-based inverse function.