source HACL* https://github.com/hacl-star/hacl-star/blob/v0.3.0/specs/Spec.Curve25519.fst#L56
parameter am24
assume am24 = (a-2)/4
assume Z1 = 1
coords xz