From 4cd8fc2ecd1d312b1da602075965c2ea033e40df Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Mon, 1 Apr 2024 12:46:05 -0400
Subject: [PATCH] merge Group.Scalarmult into MontgomeryLadder, use in
 x25519_base (#1843)

---
 src/Bedrock/End2End/X25519/Field25519.v       |  14 +-
 src/Bedrock/End2End/X25519/GarageDoor.v       |  25 +-
 src/Bedrock/End2End/X25519/GarageDoorTop.v    |   1 -
 src/Bedrock/End2End/X25519/MontgomeryLadder.v | 112 ++++---
 .../X25519/MontgomeryLadderProperties.v       | 182 ----------
 .../End2End/X25519/MontgomeryLadderRISCV.v    |  59 ++++
 src/Bedrock/Group/AdditionChains.v            |   5 +-
 .../Group/ScalarMult/MontgomeryLadder.v       |  85 ++++-
 src/Bedrock/Group/ScalarMult/ScalarMult.v     | 313 ------------------
 src/Curves/Montgomery/Affine.v                |   8 +-
 src/Curves/Montgomery/XZProofs.v              | 121 +++----
 src/Spec/Curve25519.v                         |  29 ++
 src/Spec/MontgomeryCurve.v                    |  16 +
 src/Spec/Test/X25519.v                        |  11 +-
 14 files changed, 302 insertions(+), 679 deletions(-)
 delete mode 100644 src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
 create mode 100644 src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v
 delete mode 100644 src/Bedrock/Group/ScalarMult/ScalarMult.v

diff --git a/src/Bedrock/End2End/X25519/Field25519.v b/src/Bedrock/End2End/X25519/Field25519.v
index d60f0bb6e4..5ff884eb16 100644
--- a/src/Bedrock/End2End/X25519/Field25519.v
+++ b/src/Bedrock/End2End/X25519/Field25519.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Spec.Curve25519.
 Require Import Coq.Strings.String. Local Open Scope string_scope.
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
@@ -38,17 +39,8 @@ Section Field.
   Instance translation_parameters_ok : Types.ok.
   Proof using ext_spec_ok. constructor; try exact _; apply prefix_name_gen_unique. Qed.
 
-  (* Define Curve25519 field *)
-  Instance field_parameters : FieldParameters.
-  Proof using Type.
-    let M := (eval vm_compute in (Z.to_pos (UnsaturatedSolinas.m s c))) in
-    (* curve 'A' parameter *)
-    let a := constr:(F.of_Z M 486662) in
-    let prefix := constr:("fe25519_"%string) in
-    eapply
-      (field_parameters_prefixed
-         M ((a - F.of_Z _ 2) / F.of_Z _ 4)%F prefix).
-  Defined.
+  Instance field_parameters : FieldParameters :=
+    field_parameters_prefixed Curve25519.p Curve25519.M.a24 "fe25519_"%string.
 
   (* Call fiat-crypto pipeline on all field operations *)
   Instance fe25519_ops : unsaturated_solinas_ops (ext_spec:=ext_spec) n s c.
diff --git a/src/Bedrock/End2End/X25519/GarageDoor.v b/src/Bedrock/End2End/X25519/GarageDoor.v
index 1b5d202965..a77054bdef 100644
--- a/src/Bedrock/End2End/X25519/GarageDoor.v
+++ b/src/Bedrock/End2End/X25519/GarageDoor.v
@@ -40,10 +40,25 @@ Local Open Scope string_scope.
 Import Syntax Syntax.Coercions NotationsCustomEntry.
 Import ListNotations.
 Import Coq.Init.Byte.
+Import Tuple LittleEndianList.
+Local Coercion F.to_Z : F >-> Z.
 
 Definition garageowner : list byte :=
   [x7b; x06; x18; x0c; x54; x0c; xca; x9f; xa3; x16; x0b; x2f; x2b; x69; x89; x63; x77; x4c; xc1; xef; xdc; x04; x91; x46; x76; x8b; xb2; xbf; x43; x0e; x34; x34].
 
+Definition garageowner_P : Curve25519.M.point.
+refine (
+  let x := F.of_Z _ (le_combine garageowner) in
+  let y2 := (x*x*x + Curve25519.M.a*x*x +x)%F in
+  let sqrtm1 := (F.pow (F.of_Z _ 2) ((N.pos p-1)/4)) in
+  let y := F.sqrt_5mod8 sqrtm1 y2 in
+  exist _ (inl (x, y)) _).
+Decidable.vm_decide.
+Defined.
+
+Lemma garageowner_P_correct : le_split 32 (Curve25519.M.X0 garageowner_P) = garageowner.
+Proof. vm_compute. reflexivity. Qed.
+
 Local Notation ST := 0x80000000.
 Local Notation PK := 0x80000040.
 Local Notation BUF:= 0x80000060.
@@ -164,7 +179,6 @@ Qed.
 
 Local Open Scope list_scope.
 Require Crypto.Bedrock.End2End.RupicolaCrypto.Spec.
-Import Tuple LittleEndianList.
 Local Definition be2 z := rev (le_split 2 z).
 Local Coercion to_list : tuple >-> list.
 Local Coercion Z.b2z : bool >-> Z.
@@ -200,7 +214,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -
       (TracePredicate.one ("st", lightbulb_spec.GPIO_DATA_ADDR _, action))) ioh
    /\ (
     let m := firstn 16 garagedoor_payload in
-    let v := le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (Field.feval_bytes(FieldRepresentation:=frep25519) garageowner))) in
+    let v := le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) garageowner_P)) in
     exists set0 set1 : Naive.word32,
     (word.unsigned set0 = 1 <-> firstn 16 v = m) /\
     (word.unsigned set1 = 1 <->  skipn 16 v = m) /\
@@ -220,7 +234,7 @@ Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -
      udp_local ++ udp_remote ++
      be2 udp_length ++ be2 0 ++
      garagedoor_header ++
-     le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z _ 9)))))
+     le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) Curve25519.M.B))))
   ioh /\ SEED=seed /\ SK=sk.
 
 Local Instance spec_of_recvEthernet : spec_of "recvEthernet" := spec_of_recvEthernet.
@@ -363,6 +377,7 @@ Proof.
     repeat straightline.
     straightline_call; ssplit; try ecancel_assumption; try trivial; try ZnWords.
     { cbv. inversion 1. }
+    { instantiate (1:=garageowner_P). Decidable.vm_decide. }
 
     rename Lppp into Lihl; assert (List.length ppp = 40)%nat as Lppp by ZnWords.
 
@@ -387,7 +402,7 @@ Proof.
     subst pPPP.
     seprewrite_in_by (Array.bytearray_append cmp1) H33 SepAutoArray.listZnWords.
 
-    set (k := (Field.feval_bytes _)); remember (le_split 32 (F.to_Z (x25519_gallina (le_combine sk) k))) as vv; subst k.
+    remember (le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) garageowner_P))) as vv.
     repeat straightline.
     pose proof (List.firstn_skipn 16 vv) as Hvv.
     pose proof (@firstn_length_le _ vv 16 ltac:(subst vv; rewrite ?length_le_split; ZnWords)).
@@ -852,7 +867,7 @@ Optimize Proof. Optimize Heap.
   { rewrite ?app_length, ?length_le_split. SepAutoArray.listZnWords. }
   { ZnWords. }
 
-  pose proof length_le_split 32 (F.to_Z (x25519_gallina (le_combine sk) (F.of_Z _ 9))) as Hpkl.
+  pose proof length_le_split 32 (F.to_Z (M.X0 (Curve25519.M.scalarmult (le_combine sk mod 2^255) Curve25519.M.B))) as Hpkl.
   seprewrite_in_by (fun xs ys=>@bytearray_address_merge _ _ _ _ _ xs ys buf) H37 SepAutoArray.listZnWords.
   seprewrite_in_by (fun xs ys=>@bytearray_address_merge _ _ _ _ _ xs ys buf) H37 SepAutoArray.listZnWords.
 
diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v
index 030a84604a..5d27632c9b 100644
--- a/src/Bedrock/End2End/X25519/GarageDoorTop.v
+++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v
@@ -24,7 +24,6 @@ Require Import bedrock2Examples.memswap.
 Require Import bedrock2Examples.memconst.
 Require Import Rupicola.Examples.Net.IPChecksum.IPChecksum.
 Require Import Crypto.Bedrock.End2End.X25519.GarageDoor.
-Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadderProperties.
 Import Crypto.Bedrock.End2End.RupicolaCrypto.ChaCha20.
 Local Open Scope string_scope.
 Import Syntax Syntax.Coercions NotationsCustomEntry.
diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadder.v b/src/Bedrock/End2End/X25519/MontgomeryLadder.v
index bd86664336..fcf467ee29 100644
--- a/src/Bedrock/End2End/X25519/MontgomeryLadder.v
+++ b/src/Bedrock/End2End/X25519/MontgomeryLadder.v
@@ -1,6 +1,8 @@
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Spec.MontgomeryCurve.
 Require Import Crypto.Spec.Curve25519.
 Require Import bedrock2.Map.Separation.
 Require Import bedrock2.Syntax.
@@ -53,25 +55,29 @@ Require Import coqutil.Map.OfListWord Coq.Init.Byte coqutil.Byte.
 Import ProgramLogic.Coercions.
 Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Definition x25519_gallina K U : F (2^255-19) := 
-  @XZ.M.montladder _ F.zero F.one F.add F.sub F.mul F.inv (F.div (F.of_Z _ 486662 - F.of_Z _ 2) (F.of_Z _ 4))
-  (Z.to_nat (Z.log2 (Z.pos order))) (Z.testbit K) U.
+
 Global Instance spec_of_x25519 : spec_of "x25519" :=
-  fnspec! "x25519" out sk pk / (o s p : list Byte.byte) (R : _ -> Prop),
+  fnspec! "x25519" out sk pk / (o s p : list Byte.byte) P (R : _ -> Prop),
   { requires t m := m =* s$@sk * p$@pk * o$@out * R /\
-      length s = 32%nat /\ length p = 32%nat /\ length o = 32%nat /\ byte.unsigned (nth 31 p x00) <= 0x7f;
+      length s = 32%nat /\ length p = 32%nat /\ length o = 32%nat /\
+      byte.unsigned (nth 31 p x00) <= 0x7f /\ Field.feval_bytes(field_parameters:=field_parameters) p = Curve25519.M.X0 P;
     ensures t' m := t=t' /\ m=* s$@sk ⋆ p$@pk ⋆ R ⋆
-      (le_split 32 (x25519_gallina (le_combine s) (Field.feval_bytes p)))$@out }.
+      (le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine s mod 2^255) P))$@out) }.
 
 Local Instance spec_of_fe25519_from_word : spec_of "fe25519_from_word" := Field.spec_of_from_word.
 Local Instance spec_of_fe25519_from_bytes : spec_of "fe25519_from_bytes" := Field.spec_of_from_bytes.
 Local Instance spec_of_fe25519_to_bytes : spec_of "fe25519_to_bytes" := Field.spec_of_to_bytes.
-Local Instance spec_of_montladder : spec_of "montladder" := spec_of_montladder(Z.to_nat (Z.log2 Curve25519.order)).
+Local Instance spec_of_montladder : spec_of "montladder" :=
+  spec_of_montladder
+    (Z.to_nat (Z.log2 Curve25519.order))
+    Crypto.Spec.Curve25519.field
+    Curve25519.M.a Curve25519.M.b Curve25519.M.b_nonzero (char_ge_3:=Curve25519.char_ge_3).
 
 Local Arguments word.rep : simpl never.
 Local Arguments word.wrap : simpl never.
 Local Arguments word.unsigned : simpl never.
 Local Arguments word.of_Z : simpl never.
+
 Lemma x25519_ok : program_logic_goal_for_function! x25519.
 Proof.
   repeat straightline.
@@ -94,10 +100,10 @@ Proof.
     eapply byte.unsigned_range. }
   repeat straightline.
 
-  seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H15. { transitivity 40%nat; trivial. }
+  seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H16. { transitivity 40%nat; trivial. }
 
   straightline_call; ssplit.
-  3: { unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
+  { unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
        { use_sep_assumption. cancel; repeat ecancel_step.
        cancel_seps_at_indices 0%nat 0%nat; trivial. cbn; reflexivity. }
     all : eauto.
@@ -106,7 +112,7 @@ Proof.
   { rewrite H3. vm_compute. inversion 1. }
   repeat straightline.
 
-  cbv [FElem] in H22. extract_ex1_and_emp_in H22.
+  specialize (H23 P ltac:(assumption)). cbv [FElem] in H23. extract_ex1_and_emp_in H23.
   straightline_call; ssplit.
   { ecancel_assumption. }
   { transitivity 32%nat; auto. }
@@ -116,21 +122,20 @@ Proof.
   repeat straightline.
 
   cbv [Field.FElem] in *.
-  seprewrite_in @Bignum.Bignum_to_bytes H25.
-  seprewrite_in @Bignum.Bignum_to_bytes H25.
-  extract_ex1_and_emp_in H25.
+  seprewrite_in @Bignum.Bignum_to_bytes H26.
+  seprewrite_in @Bignum.Bignum_to_bytes H26.
+  extract_ex1_and_emp_in H26.
 
   repeat straightline; intuition eauto.
-  rewrite H29 in *. cbv [x25519_gallina].
-  use_sep_assumption; cancel. eapply RelationClasses.reflexivity.
+  rewrite H30 in *.
+  use_sep_assumption; cancel. reflexivity.
 Qed.
 
 Global Instance spec_of_x25519_base : spec_of "x25519_base" :=
   fnspec! "x25519_base" out sk / (o s : list Byte.byte) (R : _ -> Prop),
-  { requires t m := m =* s$@sk * o$@out * R /\
-      length s = 32%nat /\ length o = 32%nat;
+  { requires t m := m =* s$@sk * o$@out * R /\ length s = 32%nat /\ length o = 32%nat;
     ensures t' m := t=t' /\ m=* s$@sk ⋆ R ⋆
-      (le_split 32 (x25519_gallina (le_combine s) (F.of_Z _ 9)))$@out }.
+      le_split 32 (M.X0 (Curve25519.M.scalarmult (le_combine s mod 2^255) Curve25519.M.B))$@out }.
 
 Lemma x25519_base_ok : program_logic_goal_for_function! x25519_base.
 Proof.
@@ -143,7 +148,7 @@ Proof.
   seprewrite_in (@Bignum.Bignum_of_bytes _ _ _ _ _ _ 10 a2) H13. { transitivity 40%nat; trivial. }
 
   straightline_call; ssplit.
-  3: { unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
+  { unfold FElem, Field.FElem in *; extract_ex1_and_emp_in_goal; ssplit.
        { use_sep_assumption. cancel; repeat ecancel_step.
        cancel_seps_at_indices 0%nat 0%nat; trivial. cbn; reflexivity. }
     all : eauto.
@@ -152,6 +157,7 @@ Proof.
   { rewrite H3. vm_compute. inversion 1. }
   repeat straightline.
 
+  specialize (H20 Curve25519.M.B eq_refl).
   unfold FElem in H20. extract_ex1_and_emp_in H20.
   straightline_call; ssplit.
   { ecancel_assumption. }
@@ -167,8 +173,8 @@ Proof.
   extract_ex1_and_emp_in H23.
 
   repeat straightline; intuition eauto.
-  rewrite H27 in *. cbv [x25519_gallina].
-  use_sep_assumption; cancel. eapply RelationClasses.reflexivity.
+  rewrite H27 in *.
+  use_sep_assumption; cancel. reflexivity.
 Qed.
 
 Require Import coqutil.Word.Naive.
@@ -196,36 +202,38 @@ Definition funcs :=
 Require Import bedrock2.ToCString.
 Definition montladder_c_module := list_byte_of_string (ToCString.c_module funcs).
 
-#[export]
-Instance BWM_RV32IM : FlatToRiscvCommon.bitwidth_iset 32 Decode.RV32IM := eq_refl.
-
-Derive montladder_compiler_result SuchThat
-       (compile
-         (compile_ext_call (funname_env:=SortedListString.map))
-         funcs = Success montladder_compiler_result)
-       As montladder_compiler_result_ok.
+Lemma link_montladder : spec_of_montladder (map.of_list funcs).
 Proof.
-  match goal with x := _ |- _ => cbv delta [x]; clear x end.
-  match goal with |- ?a = _ => set a end.
-  vm_compute.
-  match goal with |- @Success ?A ?x = Success ?e => is_evar e;
-    exact (@eq_refl (result A) (@Success A x)) end.
+  unfold spec_of_montladder, ScalarMult.MontgomeryLadder.spec_of_montladder.
+  unfold funcs.
+  (* use montladder correctness proof *)
+  rewrite montladder_defn.
+  eapply @montladder_correct; try (typeclasses eauto).
+  { reflexivity. }
+  { Decidable.vm_decide. }
+  { Decidable.vm_decide. }
+  { Decidable.vm_decide. }
+  { eapply M.a2m4_nonsq. }
+  { exact I. }
+  { reflexivity. }
+  { eapply CSwap.cswap_body_correct; [|exact I|reflexivity].
+    unfold field_representation, Signature.field_representation, Representation.frep; cbn; unfold n; cbv; trivial. }
+  { eapply fe25519_copy_correct. reflexivity. }
+  { eapply fe25519_from_word_correct. reflexivity. }
+  {
+    cbv [LadderStep.spec_of_ladderstep]; intros.
+    rewrite ladderstep_defn.
+    eapply @LadderStep.ladderstep_correct; try (typeclasses eauto).
+    { cbv [Core.__rupicola_program_marker]; tauto. }
+    { reflexivity. }
+    { apply fe25519_mul_correct. reflexivity. }
+    { apply fe25519_add_correct. reflexivity. }
+    { apply fe25519_sub_correct. reflexivity. }
+    { apply fe25519_square_correct. reflexivity. }
+    { apply fe25519_scmula24_correct. reflexivity. }
+    { ecancel_assumption. } }
+  { unshelve eapply AdditionChains.fe25519_inv_correct_exp; [exact I|reflexivity| | ].
+    { apply fe25519_square_correct. reflexivity. }
+    { apply fe25519_mul_correct. reflexivity. } }
+  { apply fe25519_mul_correct. reflexivity. }
 Qed.
-
-Definition montladder_stack_size := snd montladder_compiler_result.
-Definition montladder_finfo := snd (fst montladder_compiler_result).
-Definition montladder_insns := fst (fst montladder_compiler_result).
-Definition montladder_bytes := Pipeline.instrencode montladder_insns.
-Definition montladder_symbols : list byte := Symbols.symbols montladder_finfo.
-
-
-Require riscv.Utility.InstructionNotations.
-Require riscv.Utility.InstructionCoercions.
-Module PrintAssembly.
-  Import riscv.Utility.InstructionNotations.
-  Import riscv.Utility.InstructionCoercions.
-  Unset Printing Coercions.
-
-  (* Compute garagedoor_finfo. (* fe25519_mul is more than 10KB in just one function *) *)
-  Goal True. let r := eval cbv in montladder_insns in idtac (* r *). Abort.
-End PrintAssembly.
diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v b/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
deleted file mode 100644
index 5e44c09f16..0000000000
--- a/src/Bedrock/End2End/X25519/MontgomeryLadderProperties.v
+++ /dev/null
@@ -1,182 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import bedrock2.Map.Separation.
-Require Import bedrock2.Map.SeparationLogic.
-Require Import bedrock2.Syntax.
-Require Import compiler.Pipeline.
-Require Import compiler.MMIO.
-Require Import compiler.NaiveRiscvWordProperties.
-Require Import coqutil.Map.SortedListWord.
-Require Import coqutil.Map.Z_keyed_SortedListMap.
-Require Import coqutil.Word.Bitwidth32.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Bedrock.End2End.X25519.Field25519.
-Require Import Crypto.Bedrock.Field.Synthesis.New.UnsaturatedSolinas.
-Require Import Crypto.Bedrock.Specs.Field.
-Require Import Crypto.Bedrock.Field.Interface.Compilation2.
-Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.
-Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadder.
-
-Local Arguments map.rep: clear implicits.
-
-Definition f_rel_pos : Z := ltac:(
-  let y := eval vm_compute in (List.find (fun '(name, pos) => String.eqb name "montladder") montladder_finfo) in
-  match y with Some (_, ?pos) => exact pos end).
-
-Local Instance mem : map.map (word.rep (width:=32)) Init.Byte.byte := SortedListWord.map _ _.
-Local Existing Instance BW32.
-
-(* Postcondition extracted from spec_of_montladder *)
-Definition montladder_post (pOUT pK pU : word.rep (word:=Naive.word32))
-          (Kbytes : list Byte.byte) (K : Z)
-          (U : F (Field.M_pos (FieldParameters:=field_parameters)))
-          (OUT : F (Field.M_pos (FieldParameters:=field_parameters)))
-          (R : map.rep word.rep Init.Byte.byte mem -> Prop)
-          (tr : Semantics.trace) :
-  Semantics.trace -> map.rep _ _ mem -> list (word.rep (word:=Naive.word32)) -> Prop :=
-   (fun (tr' : Semantics.trace)
-        (mem' : map.rep word.rep Init.Byte.byte mem)
-        (rets : list word.rep) =>
-      rets = [] /\
-      tr' = tr /\
-      (FElem
-         (BW:=BW32)
-         (field_representaton:=field_representation n s c)
-         (Some Field.tight_bounds) pOUT
-         (@XZ.M.montladder _ F.zero F.one F.add F.sub F.mul F.inv a24 (Z.log2 Curve25519.order) (Z.testbit K) U)
-         ⋆ Array.array ptsto (word.of_Z 1) pK Kbytes
-         ⋆ FElem (BW:=BW32)
-                 (field_representaton:=field_representation n s c)
-                 (Some Field.tight_bounds) pU U ⋆ R)%sep
-        mem').
-
-Local Instance Registers : map.map Z (@word.rep 32 Naive.word32)
-  := Zkeyed_map _.
-
-Require Import riscv.Spec.Decode.
-
-Local Instance naive_word_riscv_ok :
-  RiscvWordProperties.word.riscv_ok Naive.word32 := naive_word_riscv_ok 5.
-
-Lemma link_montladder : spec_of_montladder (map.of_list funcs).
-Proof.
-    unfold spec_of_montladder, ScalarMult.MontgomeryLadder.spec_of_montladder.
-    unfold funcs.
-    (* use montladder correctness proof *)
-    rewrite montladder_defn.
-    eapply @montladder_correct; try (typeclasses eauto).
-    { reflexivity. }
-    { cbv [Core.__rupicola_program_marker]. tauto. }
-    { exact I. }
-    { reflexivity. }
-    { eapply CSwap.cswap_body_correct; [|exact I|reflexivity].
-      unfold field_representation, Signature.field_representation, Representation.frep; cbn; unfold n; cbv; trivial. }
-    { eapply fe25519_copy_correct. reflexivity. }
-    { eapply fe25519_from_word_correct. reflexivity. }
-    {
-      cbv [LadderStep.spec_of_ladderstep]; intros.
-      rewrite ladderstep_defn.
-      eapply @LadderStep.ladderstep_correct; try (typeclasses eauto).
-      { cbv [Core.__rupicola_program_marker]; tauto. }
-      { reflexivity. }
-      { apply fe25519_mul_correct. reflexivity. }
-      { apply fe25519_add_correct. reflexivity. }
-      { apply fe25519_sub_correct. reflexivity. }
-      { apply fe25519_square_correct. reflexivity. }
-      { apply fe25519_scmula24_correct. reflexivity. }
-      { ecancel_assumption. } }
-    { unshelve eapply AdditionChains.fe25519_inv_correct_exp; [exact I|reflexivity| | ].
-      { apply fe25519_square_correct. reflexivity. }
-      { apply fe25519_mul_correct. reflexivity. } }
-    { apply fe25519_mul_correct. reflexivity. }
-Qed.
-
-Lemma montladder_compiles_correctly :
-  forall (t : Semantics.trace)
-         (mH : map.rep word.rep Init.Byte.byte mem)
-         (pOUT pK pU : word.rep) (out_bound : option Field.bounds)
-         (OUT U: F Field.M_pos) (Kbytes : list Byte.byte) (K : Z)
-         (initial : MetricRiscvMachine)
-         (stack_lo stack_hi ret_addr p_funcs : word.rep)
-         (R Rdata Rexec : map.rep word.rep Init.Byte.byte mem -> Prop),
-         LittleEndianList.le_combine Kbytes = K ->
-         length Kbytes = 32%nat ->
-         (FElem (BW:=BW32)
-                (field_representaton:=field_representation n s c)
-                out_bound pOUT OUT
-          ⋆ Array.array ptsto (word.of_Z 1) pK Kbytes
-          ⋆  FElem (BW:=BW32)
-                   (field_representaton:=field_representation n s c)
-                   (Some Field.tight_bounds) pU U
-          ⋆ R)%sep mH ->
-         montladder_stack_size <=
-         word.unsigned (word.sub stack_hi stack_lo) /
-         SeparationLogic.bytes_per_word ->
-         word.unsigned (word.sub stack_hi stack_lo)
-         mod SeparationLogic.bytes_per_word = 0 ->
-         getPc (getMachine initial) = word.add p_funcs (word.of_Z f_rel_pos) ->
-         map.get (getRegs (getMachine initial)) RegisterNames.ra =
-         Some ret_addr ->
-         word.unsigned ret_addr mod 4 = 0 ->
-         LowerPipeline.arg_regs_contain (getRegs (getMachine initial)) [pOUT; pK; pU] ->
-         getLog (getMachine initial) = t ->
-         LowerPipeline.machine_ok p_funcs stack_lo stack_hi montladder_insns
-           mH Rdata Rexec initial ->
-         FlatToRiscvCommon.runsTo initial
-           (fun final : MetricRiscvMachine =>
-            exists
-              (mH' : map.rep word.rep Init.Byte.byte mem)
-            (retvals : list word.rep),
-              LowerPipeline.arg_regs_contain (getRegs (getMachine final)) retvals /\
-              montladder_post pOUT pK pU Kbytes K U OUT R t
-                 (getLog (getMachine final)) mH' retvals /\
-              map.only_differ (getRegs (getMachine initial))
-                              reg_class.caller_saved
-                              (getRegs (getMachine final)) /\
-              getPc (getMachine final) = ret_addr /\
-              LowerPipeline.machine_ok p_funcs stack_lo stack_hi
-                montladder_insns mH' Rdata Rexec final).
-Proof.
-  intros.
-  eapply (compiler_correct_wp
-            (ext_spec:=FE310CSemantics.ext_spec)
-            (string_keyed_map := SortedListString.map)
-            (string_keyed_map_ok := SortedListString.ok))
-    with (fname:="montladder"%string).
-  all:cbn [montladder fst snd].
-
-  (* fill in easy subgoals that instantiate evars *)
-  all:lazymatch goal with
-      | |- compile _ _ = Success _ =>
-        rewrite montladder_compiler_result_ok;
-        transitivity (Success (montladder_insns,
-                               montladder_finfo,
-                               montladder_stack_size));
-        [ | reflexivity ]; reflexivity
-      | _ => idtac
-      end.
-  all:lazymatch goal with
-      | |- getPc (getMachine _) = _ => eassumption
-      | |- getLog (getMachine _) = _ => eassumption
-      | |- map.get (getRegs (getMachine _)) _ = Some _ => eassumption
-      | |- LowerPipeline.arg_regs_contain _ _ => eassumption
-      | |- context [LowerPipeline.machine_ok] => eassumption
-      | |- map.get _ "montladder"%string = Some _ => reflexivity
-      | _ => idtac
-      end.
-
-  (* solve remaining goals one by one *)
-  { eapply (compile_ext_call_correct (funname_env_ok:=SortedListString.ok)). }
-  { intros. cbv [compile_ext_call compile_interact].
-    repeat (destruct_one_match; try reflexivity). }
-  { vm_compute. reflexivity. }
-  { lazy. repeat constructor; cbn [In]; intuition idtac; congruence. }
-  { eapply link_montladder.
-    ssplit; try eassumption; [ ].
-    lazymatch goal with H : length Kbytes = _ |- _ => rewrite H end.
-    lazy; congruence. }
-  { assumption. }
-  { assumption. }
-  { assumption. }
-Qed.
-
-(* Print Assumptions montladder_compiles_correctly. *)
diff --git a/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v b/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v
new file mode 100644
index 0000000000..642472ac88
--- /dev/null
+++ b/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v
@@ -0,0 +1,59 @@
+Require Import Coq.ZArith.ZArith.
+Require Import bedrock2.Map.Separation.
+Require Import bedrock2.Map.SeparationLogic.
+Require Import bedrock2.Syntax.
+Require Import compiler.Pipeline.
+Require Import compiler.MMIO.
+Require Import compiler.NaiveRiscvWordProperties.
+Require Import coqutil.Map.SortedListWord.
+Require Import coqutil.Map.Z_keyed_SortedListMap.
+Require Import coqutil.Word.Bitwidth32.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
+Require Import Crypto.Bedrock.End2End.X25519.Field25519.
+Require Import Crypto.Bedrock.Field.Synthesis.New.UnsaturatedSolinas.
+Require Import Crypto.Bedrock.Specs.Field.
+Require Import Crypto.Bedrock.Field.Interface.Compilation2.
+Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.
+Require Import Crypto.Bedrock.End2End.X25519.MontgomeryLadder.
+
+Local Arguments map.rep: clear implicits.
+
+#[export]
+Instance BWM_RV32IM : FlatToRiscvCommon.bitwidth_iset 32 Decode.RV32IM := eq_refl.
+
+Derive montladder_compiler_result SuchThat
+       (compile
+         (compile_ext_call (funname_env:=SortedListString.map))
+         funcs = Success montladder_compiler_result)
+       As montladder_compiler_result_ok.
+Proof.
+  match goal with x := _ |- _ => cbv delta [x]; clear x end.
+  match goal with |- ?a = _ => set a end.
+  vm_compute.
+  match goal with |- @Success ?A ?x = Success ?e => is_evar e;
+    exact (@eq_refl (result A) (@Success A x)) end.
+Qed.
+
+Definition montladder_stack_size := snd montladder_compiler_result.
+Definition montladder_finfo := snd (fst montladder_compiler_result).
+Definition montladder_insns := fst (fst montladder_compiler_result).
+Definition montladder_bytes := Pipeline.instrencode montladder_insns.
+Definition montladder_symbols : list _ := Symbols.symbols montladder_finfo.
+
+Require riscv.Utility.InstructionNotations.
+Require riscv.Utility.InstructionCoercions.
+Module PrintAssembly.
+  Import riscv.Utility.InstructionNotations.
+  Import riscv.Utility.InstructionCoercions.
+  Unset Printing Coercions.
+
+  (* Compute garagedoor_finfo. (* fe25519_mul is more than 10KB in just one function *) *)
+  Goal True. let r := eval cbv in montladder_insns in idtac (* r *). Abort.
+End PrintAssembly.
+
+Definition f_rel_pos : Z := ltac:(
+  let y := eval vm_compute in (List.find (fun '(name, pos) => String.eqb name "montladder") montladder_finfo) in
+  match y with Some (_, ?pos) => exact pos end).
+
+Local Instance mem : map.map (word.rep (width:=32)) Init.Byte.byte := SortedListWord.map _ _.
+Local Existing Instance BW32.
diff --git a/src/Bedrock/Group/AdditionChains.v b/src/Bedrock/Group/AdditionChains.v
index a96432a515..1393770f55 100644
--- a/src/Bedrock/Group/AdditionChains.v
+++ b/src/Bedrock/Group/AdditionChains.v
@@ -1,3 +1,4 @@
+Require Crypto.Spec.Curve25519.
 Require Import Rupicola.Lib.Api.
 Require Import Rupicola.Lib.Loops.
 Require Import Rupicola.Lib.ControlFlow.DownTo.
@@ -457,9 +458,6 @@ Section FElems.
         compile.
       Qed.
 
-      Print Assumptions exp_6_body. (* does not depend on [width] or [word] *)
-      Print Assumptions exp_97_body. (* depends on [width] and  [word] :/ *)
-
       Derive fe25519_inv SuchThat
              (defn! "fe25519_inv" ("res", "x") { fe25519_inv },
               implements (exp (2^255-21)) using [square; mul])
@@ -469,7 +467,6 @@ Section FElems.
       Qed.
 
       Context { F_M_pos : Z.pos M_pos = 2^255-19 }.
-      Require Import Crypto.Spec.Curve25519.
 
       Lemma compile_inv : forall m l tr functions x,
             let v := F.inv x in
diff --git a/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v b/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
index 7f389934e6..70f9847cf5 100644
--- a/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
+++ b/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v
@@ -1,5 +1,6 @@
 Require Crypto.Bedrock.Group.Loops.
 Require Import Crypto.Curves.Montgomery.XZ.
+Require Import Crypto.Curves.Montgomery.XZProofs.
 Require Import Rupicola.Lib.Api.
 Require Import Rupicola.Lib.Alloc.
 Require Import Rupicola.Lib.SepLocals.
@@ -45,7 +46,7 @@ Notation "'let/n' ( v , w , x , y , z ) := val 'in' body" :=
 
 Section Gallina.
   Local Open Scope F_scope.
-  Context (m : positive) (a24 : F m) (count : nat).
+  Context {m : positive} (a24 : F m) (count : nat).
   Definition montladder_gallina (k : Z) (u : F m)
     : F m :=
     let/n X1 := stack 1 in
@@ -128,6 +129,32 @@ Section Gallina.
       cbn [fst snd to_pair] in Heqp0; inversion_clear Heqp0; trivial. }
     { reflexivity. }
   Qed.
+
+  Context
+    (field : @Hierarchy.field (F m) eq F.zero F.one F.opp F.add F.sub F.mul F.inv F.div)
+    (Hm' : (28 <= m)%positive)
+     a (a24_correct : (1 + 1 + 1 + 1) * a24 = a - (1 + 1))
+    (a2m4_nonsq : ~(exists r, F.mul r r = F.sub (F.mul a a) (F.of_Z _ 4)))
+    (b : F m) (b_nonzero : b <> 0).
+  
+  Local Instance char_ge_28 : @Ring.char_ge (F m) eq 0 1 F.opp F.add F.sub F.mul 28.
+  Proof. eapply Algebra.Hierarchy.char_ge_weaken; try eapply F.char_gt; trivial. Qed.
+
+  Context {char_ge_3 : @Ring.char_ge (F m) eq 0 1 F.opp F.add F.sub F.mul 3}. (* appears in statement *)
+  Import MontgomeryCurve Montgomery.Affine.
+  Local Notation X0 := (@M.X0 _ eq F.zero F.add F.mul a b).
+  Local Notation add := (M.add(field:=field)(char_ge_3:=char_ge_3)(a:=a)(b_nonzero:=b_nonzero)).
+  Local Notation opp := (M.opp(field:=field)(a:=a)(b_nonzero:=b_nonzero)).
+  Local Notation scalarmult := (@ScalarMult.scalarmult_ref _ add M.zero opp).
+  Add Ring Private_ring : (F.ring_theory m) (morphism (F.ring_morph m), constants [F.is_constant]).
+
+  Lemma montladder_gallina_equiv_affine n P :
+    montladder_gallina n (X0 P) = X0 (scalarmult (n mod 2^Z.of_nat count) P).
+  Proof.
+    unshelve erewrite montladder_gallina_equiv, M.montladder_correct;
+      try lia; try exact _; trivial using F.inv_0.
+   { intros r Hr. apply a2m4_nonsq; exists r. rewrite Hr. f_equal. ring. }
+  Qed.
 End Gallina.
 
 Section __.
@@ -146,7 +173,19 @@ Section __.
   Section MontLadder.
     Context scalarbits (scalarbits_small : word.wrap (Z.of_nat scalarbits) = Z.of_nat scalarbits).
     Local Notation "bs $@ a" := (array ptsto (word.of_Z 1) a bs) (at level 20).
-
+    Let m : positive := M_pos.
+    Context
+      (field : @Hierarchy.field (F m) eq F.zero F.one F.opp F.add F.sub F.mul F.inv F.div) (Hm' : (28 <= m)%positive)
+      (a : F m) (b : F m) (b_nonzero : b <> F.zero).
+
+    Context {char_ge_3 : @Ring.char_ge (F m) eq F.zero F.one F.opp F.add F.sub F.mul 3}. (* appears in statement *)
+    Import MontgomeryCurve Montgomery.Affine.
+    Local Notation X0 := (@M.X0 _ eq F.zero F.add F.mul a b).
+    Local Notation add := (M.add(field:=field)(char_ge_3:=char_ge_3)(a:=a)(b_nonzero:=b_nonzero)).
+    Local Notation opp := (M.opp(field:=field)(a:=a)(b_nonzero:=b_nonzero)).
+    Local Notation scalarmult := (@ScalarMult.scalarmult_ref _ add M.zero opp).
+
+    Import MontgomeryCurve.
     Instance spec_of_montladder : spec_of "montladder" :=
       fnspec! "montladder"
             (pOUT pK pU : word)
@@ -154,13 +193,13 @@ Section __.
             out_bound OUT
             R,
       { requires tr mem :=
+          mem =* FElem out_bound pOUT OUT * Kbytes$@pK * FElem (Some tight_bounds) pU U *  R /\
           LittleEndianList.le_combine Kbytes = K /\
-          Z.of_nat scalarbits <= 8*Z.of_nat (length Kbytes) /\
-          (FElem out_bound pOUT OUT * Kbytes$@pK * FElem (Some tight_bounds) pU U
-           *  R)%sep mem;
+          Z.of_nat scalarbits <= 8*Z.of_nat (length Kbytes);
         ensures tr' mem' :=
-          tr' = tr
-          /\ (let OUT := @M.montladder _ F.zero F.one F.add F.sub F.mul F.inv a24 (Z.of_nat scalarbits) (Z.testbit K) U in
+          tr' = tr /\ (
+          forall P, U = MontgomeryCurve.M.X0 (Fzero:=F.zero) P ->
+          let OUT := MontgomeryCurve.M.X0 (Fzero:=F.zero) (scalarmult (K mod 2^Z.of_nat scalarbits) P) in 
               (FElem (Some tight_bounds) pOUT OUT * Kbytes$@pK
                * FElem (Some tight_bounds) pU U
                * R)%sep mem') }.
@@ -204,6 +243,7 @@ Section __.
      bedrock_cmd:($out_var = (load1($x_var+$i_var>>coq:(3))>>($i_var&coq:(7)))&coq:(1); coq:(k_impl))
      <{ pred (nlet_eq [out_var] v k) }>.
  Proof using mem_ok scalarbits word_ok.
+   clear dependent m.
    repeat straightline.
    repeat (eexists; split; repeat straightline'; eauto); cbn [Semantics.interp_binop].
 
@@ -255,15 +295,16 @@ Section __.
   Existing Instance felem_alloc.
 
 
-  Lemma cswap_same {A} b (a : A): cswap b a a = \<a,a\>.
+  Lemma cswap_same {A} : forall b (a : A), cswap b a a = \<a,a\>.
   Proof using Type.
-    destruct b; reflexivity.
+    intros b0; destruct b0; reflexivity.
   Qed.
 
   Local Ltac ecancel_assumption ::= ecancel_assumption_impl.
 
   Lemma scalarbits_bound : Z.of_nat scalarbits < 2 ^ width.
   Proof using scalarbits_small.
+    clear dependent m.
     rewrite <- scalarbits_small.
     unfold word.wrap.
     apply Z_mod_lt.
@@ -309,23 +350,23 @@ Section __.
   simple eapply word_unsigned_of_Z_eq; [ ZnWords |] : compiler.
 
   (*TODO: should this go in core rupicola?*)
-  Lemma compile_copy_bool {tr m l functions} (x: bool) :
+  Lemma compile_copy_bool {tr _m l functions} (x: bool) :
     let v := x in
     forall P (pred: P v -> predicate)
            (k: nlet_eq_k P v) k_impl
            x_expr var,
 
-      WeakestPrecondition.dexpr m l x_expr (word.of_Z (Z.b2z v)) ->
+      WeakestPrecondition.dexpr _m l x_expr (word.of_Z (Z.b2z v)) ->
 
       (let v := v in
        <{ Trace := tr;
-          Memory := m;
+          Memory := _m;
           Locals := map.put l var (word.of_Z (Z.b2z v));
           Functions := functions }>
        k_impl
        <{ pred (k v eq_refl) }>) ->
       <{ Trace := tr;
-         Memory := m;
+         Memory := _m;
          Locals := l;
          Functions := functions }>
       cmd.seq (cmd.set var x_expr) k_impl
@@ -356,7 +397,9 @@ Section __.
     | cons _ ?xs => let i := find_implication xs y in constr:(S i)
     end.
 
-  Context { F_M_pos : Z.pos M_pos = 2^255-19 }.
+  Context { F_M_pos : M_pos = (2^255-19)%positive }.
+  Context (a24_correct : F.mul (1 + 1 + 1 + 1) Field.a24 = F.sub a (1 + 1))
+          (Ha : ~(exists r, F.mul r r = F.sub (F.mul a a) (F.of_Z _ 4))).
 
   Hint Extern 1 (spec_of "fe25519_inv") => (simple refine (spec_of_exp_large)) : typeclass_instances.
   Hint Extern 1 (spec_of "felem_cswap") => (simple refine (spec_of_cswap)) : typeclass_instances.
@@ -364,23 +407,29 @@ Section __.
     Derive montladder_body SuchThat
            (defn! "montladder" ("OUT", "K", "U")
                 { montladder_body },
-             implements montladder_gallina
+             implements (montladder_gallina(m:=M_pos))
                         using ["felem_cswap"; felem_copy; from_word;
                                "ladderstep"; "fe25519_inv"; mul])
            As montladder_correct.
     Proof.
       pose proof scalarbits_bound.
-      cbv [spec_of_montladder]; intros; eapply Semantics.weaken_call; cycle 1; intros.
-      { rewrite <-montladder_gallina_equiv. match goal with H : ?e t' m' rets |- _ => exact H end. }
+      cbv [spec_of_montladder]; intros; eapply Semantics.weaken_call with
+        (post1:=fun t' m' rets => rets = [] /\ t' = tr /\
+           ((FElem (Some tight_bounds) pOUT (montladder_gallina a24 scalarbits K U)
+            ⋆ Kbytes $@ pK ⋆ FElem (Some tight_bounds) pU U ⋆ R) m')); cycle 1; intros.
+      { DestructHead.destruct_head and; Tactics.ssplit; trivial; intros.
+        pose proof LittleEndianList.le_combine_bound Kbytes. subst U.
+        erewrite montladder_gallina_equiv_affine in *; eauto; try lia. }
 
       compile_setup.
-      repeat compile_step.
+      repeat compile_step; shelve_unifiable.
       eapply compile_nlet_as_nlet_eq.
       eapply compile_felem_cswap; repeat compile_step.
 
       eapply compile_nlet_as_nlet_eq.
       eapply compile_felem_cswap; repeat compile_step.
 
+      lia. (* m = 2^255-19 *)
       compile_step.
     Qed.
 
diff --git a/src/Bedrock/Group/ScalarMult/ScalarMult.v b/src/Bedrock/Group/ScalarMult/ScalarMult.v
deleted file mode 100644
index ab26c0b28b..0000000000
--- a/src/Bedrock/Group/ScalarMult/ScalarMult.v
+++ /dev/null
@@ -1,313 +0,0 @@
-(* NOTE: broken, fix after Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder. *)
-Require Import Rupicola.Lib.Api. (* for helpful tactics + notations *)
-Require Import coqutil.Byte.
-Require Import Crypto.Algebra.Hierarchy.
-Require Import Crypto.Algebra.ScalarMult.
-Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.
-Require Import Crypto.Bedrock.Specs.Field.
-Require Import Crypto.Bedrock.Specs.Group.
-Require Import Crypto.Curves.Montgomery.AffineInstances.
-Require Import Crypto.Curves.Montgomery.XZ.
-Require Import Crypto.Curves.Montgomery.XZProofs.
-Require Import Crypto.Spec.MontgomeryCurve.
-
-Module M.
-  Section __.
-    Context {width: Z} {BW: Bitwidth width} {word: word.word width} {mem: map.map word Byte.byte}.
-    Context {locals: map.map String.string word}.
-    Context {ext_spec: bedrock2.Semantics.ExtSpec}.
-    Context {word_ok : word.ok word} {mem_ok : map.ok mem}.
-    Context {locals_ok : map.ok locals}.
-    Context {ext_spec_ok : Semantics.ext_spec.ok ext_spec}.
-    Context {field_parameters : FieldParameters}
-            {field_parameters_ok : FieldParameters_ok}
-            {field_representation : FieldRepresentation}
-            {field_representation_ok : FieldRepresentation_ok}
-            {scalarbits : nat}.
-    Context (char_ge_3 :
-               @Ring.char_ge (F M_pos) Logic.eq F.zero F.one F.opp F.add
-                             F.sub F.mul 3)
-            (char_ge_5 :
-               @Ring.char_ge (F M_pos) Logic.eq F.zero F.one F.opp F.add
-                             F.sub F.mul 5)
-            (char_ge_12 :
-               @Ring.char_ge (F M_pos) Logic.eq F.zero F.one F.opp F.add
-                              F.sub F.mul 12)
-            (char_ge_28 :
-               @Ring.char_ge (F M_pos) Logic.eq F.zero F.one F.opp F.add
-                             F.sub F.mul 28)
-            (a b : F M_pos) (scmul : string).
-    Context
-      (b_nonzero : b <> F.zero)
-      (discriminant_nonzero : (a * a - (1 + 1 + 1 + 1) <> 0)%F)
-      (a24_correct : ((1 + 1 + 1 + 1) * a24)%F = (a - (1 + 1))%F)
-      (a2m4_nonsquare :
-         forall r : F M_pos,
-           (r * r)%F <> (a * a - (1 + 1 + 1 + 1))%F).
-
-    Local Notation to_xz := (M.to_xz (F:=F M_pos) (Feq:=Logic.eq)
-                                     (Fzero:=F.zero) (Fone:=F.one)
-                                     (Fadd:=F.add) (Fmul:=F.mul)
-                                     (a:=a) (b:=b)).
-    Local Notation to_x := (M.to_x (F:=F M_pos) (Feq:=Logic.eq)
-                                   (Fzero:=F.zero) (Fdiv:=F.div)
-                                   (Feq_dec:=F.eq_dec)).
-
-    Global Instance group_parameters
-      : GroupParameters :=
-      { G := @M.point (F M_pos) Logic.eq F.add F.mul a b;
-        eq := @M.eq (F M_pos) Logic.eq F.add F.mul a b;
-        add := @M.add (F M_pos) Logic.eq F.zero F.one F.opp F.add F.sub
-                      F.mul F.inv F.div (@F.field_modulo M_pos M_prime)
-                      F.eq_dec char_ge_3 a b b_nonzero;
-        zero := @M.zero (F M_pos) Logic.eq F.add F.mul a b;
-        opp := @Affine.M.opp _ _ _ _ _ _ _ _ _ _ (@F.field_modulo M_pos M_prime) F.eq_dec a b b_nonzero;
-        scalarmult :=
-          @scalarmult_ref _
-                          (M.add
-                             (field := @F.field_modulo M_pos M_prime)
-                             (char_ge_3 := char_ge_3)
-                             (b_nonzero := b_nonzero))
-                          M.zero
-                          (Affine.M.opp
-                             (field := @F.field_modulo M_pos M_prime)
-                             (b_nonzero := b_nonzero));
-        scmul := scmul;
-      }.
-
-    Global Instance group_parameters_ok : GroupParameters_ok.
-    Proof.
-      constructor.
-      { apply M.MontgomeryWeierstrassIsomorphism; auto. }
-      { apply @scalarmult_ref_is_scalarmult.
-        apply M.MontgomeryWeierstrassIsomorphism; auto. }
-    Qed.
-
-    Definition xrepresents (x : list byte) (P : G) : Prop :=
-      feval_bytes x = to_x (to_xz P) /\ bytes_in_bounds x.
-
-    Global Instance x_representation : GroupRepresentation :=
-      { gelem := list byte; (* x only, as bytes *)
-        grepresents := xrepresents;
-        GElem := FElemBytes;
-      }.
-
-    Section Implementation.
-      Local Instance spec_of_montladder : spec_of "montladder" := spec_of_montladder scalarbits.
-
-      (* redeclaration plugs in implicits so [enter] works *)
-      Definition spec_of_scmul : spec_of scmul :=
-        Eval cbv [spec_of_scmul] in
-          (@spec_of_scmul _ _ _ _ _ _  group_parameters x_representation (Nat.div_up scalarbits 8)).
-      Definition spec_of_from_bytes : spec_of from_bytes := spec_of_from_bytes.
-      Definition spec_of_to_bytes : spec_of to_bytes := spec_of_to_bytes.
-      Existing Instances spec_of_scmul spec_of_from_bytes spec_of_to_bytes.
-
-      Fixpoint repeat_stackalloc
-               (size : Z) (names : list string)
-        : cmd.cmd -> cmd.cmd :=
-        match names with
-        | [] => fun post => post
-        | n :: names' =>
-          fun post =>
-            cmd.stackalloc n size (repeat_stackalloc size names' post)
-        end.
-
-      Import NotationsCustomEntry.
-      Definition scmul_func := func! (out, x_bytes, k) {
-        (* TODO: remove stack allocation of temporaries, it is no longer needed for Rupicola *)
-                 $(repeat_stackalloc
-                   felem_size_in_bytes
-                   ["X1"; "Z1"; "X2"; "Z2"; "A"; "AA"; "B"; "BB"; "E"; "C"; "D"; "DA"; "CB"; "x"; "r"]
-                   (cmd.seq
-                      (cmd.call [] from_bytes [expr.var "x"; expr.var "x_bytes"])
-                      (cmd.seq
-                         (cmd.call [] "montladder"
-                                   [expr.var "r"; expr.var "k"; expr.var "x"; expr.var "X1";
-                                      expr.var "Z1"; expr.var "X2"; expr.var "Z2"; expr.var "A";
-                                        expr.var "AA"; expr.var "B"; expr.var "BB"; expr.var "E";
-                                          expr.var "C"; expr.var "D"; expr.var "DA"; expr.var "CB"])
-                         (cmd.call [] to_bytes [expr.var "out"; expr.var "r"]))))}.
-
-      Lemma and_iff1_l (X : Prop) (P : mem -> Prop) :
-        X ->
-        Lift1Prop.iff1 (fun m => X /\ P m) P.
-      Proof.
-        repeat intro.
-        split; intros; sepsimpl; eauto.
-      Qed.
-
-      (* TODO: generalize this tactic and upstream to bedrock2 *)
-      Ltac extract_pred' pred P :=
-        lazymatch P with
-        | (pred ?X * ?Q)%sep => constr:(pair X Q)
-        | (?Q * pred ?X)%sep => constr:(pair X Q)
-        | (?P * ?Q)%sep =>
-          lazymatch P with
-          | context [pred] =>
-            match extract_pred' pred P with
-            | pair ?X ?P' => constr:(pair X (P' * Q)%sep)
-            end
-          | _ => lazymatch Q with
-                 | context [pred] =>
-                   match extract_pred' pred Q with
-                   | pair ?X ?Q' => constr:(pair X (P * Q')%sep)
-                   end
-                 | _ => fail "No emp found in" P Q
-                 end
-          end
-        | _ => fail "expected a separation-logic conjunct with at least 2 terms, got" P
-        end.
-      Ltac extract_pred pred :=
-        match goal with
-        | |- context [pred] =>
-          match goal with
-          | |- sep ?P ?Q ?m =>
-            let r := extract_pred' pred (sep P Q) in
-            match r with
-            | pair ?X ?Y =>
-              let H := fresh in
-              assert (sep (pred X) Y m) as H;
-              [ | clear - H; ecancel_assumption ]
-            end
-          end
-        end.
-      Ltac extract_emp :=
-        let pred := constr:(emp (map:=mem)) in
-        extract_pred pred.
-      Ltac extract_ex1 :=
-        lazymatch goal with
-        | |- context [@Lift1Prop.ex1 ?A ?B] =>
-            let pred := constr:(@Lift1Prop.ex1 A B) in
-            extract_pred pred
-        | _ => fail "extract_ex1 : no ex1 found in goal!"
-        end.
-
-      Ltac prove_anybytes_postcondition :=
-        repeat lazymatch goal with
-               | |- exists m mS,
-                   Memory.anybytes ?p ?n mS
-                   /\ map.split ?mC m mS
-                   /\ ?K =>
-                 let H := fresh in
-                 let mp := fresh in
-                 let mq := fresh in
-                 assert (sep (fun m => K) (Placeholder p) mC) as H;
-                 [ | clear - H; cbv [sep] in H; cbv [Placeholder];
-                     destruct H as [mp [mq [? [? ?]]]];
-                     exists mp, mq; ssplit; solve [eauto] ]
-               | |- sep (fun mC =>
-                           exists m mS,
-                             Memory.anybytes ?p ?n mS
-                             /\ map.split mC m mS
-                             /\ ?K) ?Q ?mem =>
-                 let H := fresh in
-                 let H' := fresh in
-                 let mp := fresh in
-                 let mq := fresh in
-                 let mp2 := fresh in
-                 let mq2 := fresh in
-                 assert (sep (sep (fun m => K) (Placeholder p)) Q mem) as H;
-                 [ eapply sep_assoc
-                 | clear - H; cbv [sep] in H; cbv [Placeholder];
-                   destruct H as [mp [mq [? [H' ?] ] ] ];
-                   exists mp, mq; ssplit; eauto; [ ];
-                   destruct H' as [mp2 [mq2 [? [? ?] ] ] ];
-                   exists mp2, mq2; ssplit; solve [eauto] ]
-               end.
-
-      (* speedier proof if straightline doesn't try to compute the stack
-         allocation sizes *)
-      Local Opaque felem_size_in_bytes.
-      Lemma scmul_func_correct : forall functions,
-          map.get functions scmul = Some scmul_func ->
-          spec_of_scmul functions.
-      Proof.
-        (* straightline doesn't work properly for setup, so the first step
-           is inlined and changed here *)
-        enter scmul_func. intros.
-        eapply start_func. 1: eassumption.
-        cbv beta match delta [WeakestPrecondition.func].
-
-        cbv [GElem x_representation grepresents xrepresents] in *.
-        sepsimpl.
-        (* plain straightline should do this but doesn't (because locals
-           representation is abstract?); using enhanced version from
-           rupicola (straightline') *)
-        repeat lazymatch goal with
-               | |- (felem_size_in_bytes mod _ = 0)%Z /\ _ =>
-                 split; [ solve [apply felem_size_in_bytes_mod] | ]
-               | Hb : Memory.anybytes ?p ?n ?mS,
-                      Hs : map.split ?mC ?m ?mS,
-                           Hm : ?P ?m |- _ =>
-                   assert (sep P (Placeholder p) mC)
-                     by (remember P; cbv [sep]; exists m, mS;
-                         ssplit; solve [eauto]);
-                   clear Hb Hs
-               | _ => clear_old_seps; straightline'
-               end.
-
-(* NOTE: broken, fix after Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder. *)
-(*
-        (* call from_bytes *)
-        handle_call; [ solve [eauto] .. | ].
-        sepsimpl; repeat straightline'.
-
-        (* call montladder *)
-        handle_call; [ solve [eauto] .. | ].
-        sepsimpl; repeat straightline'.
-
-        (* clean up *)
-        cbv [MontLadderResult] in *.
-        clear_old_seps. sepsimpl.
-
-        (* call to_bytes *)
-        handle_call; [ solve [eauto] .. | ].
-        sepsimpl; subst. clear_old_seps.
-
-        (* prove postcondition, including dealloc *)
-        repeat straightline'.
-        prove_anybytes_postcondition.
-        cbn [WeakestPrecondition.list_map
-               WeakestPrecondition.list_map_body].
-        seprewrite and_iff1_l; [ reflexivity | ].
-        sepsimpl; [ reflexivity .. | ].
-        lift_eexists; sepsimpl.
-
-        extract_emp.
-
-        extract_emp.
-
-        sepsimpl; [ | | ].
-        {
-          pose proof scalarbits_pos.
-          match goal with
-          | H : context [montladder_gallina] |- _ =>
-            erewrite montladder_gallina_equiv in H
-              by (reflexivity || lia)
-          end.
-          cbv [grepresents xrepresents] in *.
-          cbn [scalarmult group_parameters].
-          match goal with
-          | H : M.montladder _ _ _ = feval ?x
-            |- feval_bytes ?y = _ =>
-            let H' := fresh in
-            assert (feval x = feval_bytes y) as H' by eauto;
-              rewrite <-H', <-H; clear H H'
-          end.
-          apply @M.montladder_correct with (Feq := Logic.eq);
-            eauto using F.inv_0, sceval_range with lia; try congruence. }
-        { eauto. }
-        { repeat match goal with
-                 | H : context [FElem ?p] |- context [Placeholder ?p] =>
-                   seprewrite (FElem_from_bytes p)
-                 end.
-          sepsimpl. lift_eexists.
-          ecancel_assumption. }
-      Qed.
- *)
-      Abort.
-    End Implementation.
-  End __.
-End M.
diff --git a/src/Curves/Montgomery/Affine.v b/src/Curves/Montgomery/Affine.v
index dd3ae84cd2..0bcf46b6c3 100644
--- a/src/Curves/Montgomery/Affine.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -27,13 +27,7 @@ Module M.
 
     Context {a b: F} {b_nonzero:b <> 0}.
 
-    Program Definition opp (P:@M.point F Feq Fadd Fmul a b) : @M.point F Feq Fadd Fmul a b :=
-      match P return F*F+∞ with
-      | (x, y) => (x, -y)
-      | ∞ => ∞
-      end.
-    Next Obligation. Proof. destruct_head @M.point; cbv; break_match; trivial; fsatz. Qed.
-
+    Local Notation opp := (M.opp(a:=a)(b_nonzero:=b_nonzero)).
     Local Notation add := (M.add(b_nonzero:=b_nonzero)).
     Local Notation point := (@M.point F Feq Fadd Fmul a b).
 
diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v
index 495c249a36..1b74dc98e9 100644
--- a/src/Curves/Montgomery/XZProofs.v
+++ b/src/Curves/Montgomery/XZProofs.v
@@ -24,10 +24,15 @@ Module M.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
-            {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3}
-            {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}
-            {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12}
             {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
+
+    Lemma Private_char_ge_3:  @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
+    Proof. clear -char_ge_28; eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
+    Context {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3}. (* appears in statement *)
+    Local Instance char_ge_5:  @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5.
+    Proof. clear -char_ge_28; eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
+    Local Instance char_ge_12:  @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
+    Proof. clear -char_ge_28; eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
@@ -40,6 +45,7 @@ Module M.
     Local Notation Madd := (M.add(a:=a)(b_nonzero:=b_nonzero)(char_ge_3:=char_ge_3)).
     Local Notation Mopp := (M.opp(a:=a)(b_nonzero:=b_nonzero)).
     Local Notation Mpoint := (@M.point F Feq Fadd Fmul a b).
+    Local Notation X0 := (M.X0(Fzero:=Fzero)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)).
     Local Notation to_xz := (M.to_xz(Fzero:=Fzero)(Fone:=Fone)(Feq:=Feq)(Fadd:=Fadd)(Fmul:=Fmul)(a:=a)(b:=b)).
     Local Notation xzladderstep := (M.xzladderstep(a24:=a24)(Fadd:=Fadd)(Fsub:=Fsub)(Fmul:=Fmul)).
 
@@ -226,10 +232,7 @@ Module M.
       if dec (snd xz = 0) then 0 else fst xz / snd xz.
     Hint Unfold to_x : points_as_coordinates.
 
-    Lemma to_x_to_xz Q : to_x (to_xz Q) = match M.coordinates Q with
-                                          | ∞ => 0
-                                          | (x,y) => x
-                                          end.
+    Lemma to_x_to_xz Q : to_x (to_xz Q) = X0 Q.
     Proof. t. Qed.
 
     Lemma proper_to_x_projective xz x'z'
@@ -269,17 +272,11 @@ Module M.
     Lemma Z_shiftr_testbit_1 n i: Logic.eq (n>>i)%Z (Z.div2 (n >> i) + Z.div2 (n >> i) + Z.b2z (Z.testbit n i))%Z.
     Proof. rewrite ?Z.testbit_odd, ?Z.add_diag, <-?Z.div2_odd; reflexivity. Qed.
 
+    Context (HFinv : Finv 0 = 0) (scalarbits : Z) (Hscalarbits : (0 <= scalarbits)%Z).
+
     (* We prove montladder correct by considering the zero and non-zero case
        separately. *)
-
-    Lemma montladder_correct_0
-          (HFinv : Finv 0 = 0)
-          (n : Z)
-          (scalarbits : Z) (point : F)
-          (Hz : point = 0)
-          (Hn : (0 <= n < 2^scalarbits)%Z)
-          (Hscalarbits : (0 <= scalarbits)%Z)
-      : montladder scalarbits (Z.testbit n) point = 0.
+    Lemma montladder_correct_0 n x (Hx : Feq x 0) : montladder scalarbits (Z.testbit n) x = 0.
     Proof.
       cbv beta delta [M.montladder].
       (* [while.by_invariant] expects a goal like [?P (while _ _ _ _)], make it so: *)
@@ -292,7 +289,7 @@ Module M.
                 (fun s => Z.to_nat (Z.succ (snd s)))).
       { split.
         (* invariant holds in the beginning *)
-        { cbn; split; [lia|split;[reflexivity|t]]. }
+        { cbn; split; [lia|split;[reflexivity|try t]]. }
         { (* fuel <= measure *) cbn. rewrite Z.succ_pred. reflexivity. } }
       { intros [ [ [ [ [x2 z2] x3] z3] swap] i] [Hi [Hz2 Hx3z3]].
         destruct (i >=? 0)%Z eqn:Hbranch; (* did the loop continue? *)
@@ -313,15 +310,8 @@ Module M.
           cbv [M.cswap]; break_match; break_match_hyps; setoid_subst_rel Feq; fsatz. } }
     Qed.
 
-    Lemma montladder_correct_nz
-          (HFinv : Finv 0 = 0)
-          (n : Z) (P : M.point)
-          (scalarbits : Z) (point : F)
-          (Hnz : point <> 0)
-          (Hn : (0 <= n < 2^scalarbits)%Z)
-          (Hscalarbits : (0 <= scalarbits)%Z)
-          (Hpoint : point = to_x (to_xz P))
-      : montladder scalarbits (Z.testbit n) point = to_x (to_xz (scalarmult n P)).
+    Lemma montladder_correct_nz n P (Hnz : X0 P <> 0)
+      : montladder scalarbits (Z.testbit n) (X0 P) = X0 (scalarmult (n mod 2^scalarbits) P).
     Proof.
       pose proof (let (_, h, _, _) := AffineInstances.M.MontgomeryWeierstrassIsomorphism b_nonzero (a:=a) a2m4_nz in h) as commutative_group.
       cbv beta delta [M.montladder].
@@ -329,28 +319,31 @@ Module M.
       lazymatch goal with |- context [while ?t ?b ?l ?i] => pattern (while t b l i) end.
       eapply (while.by_invariant_fuel
                 (fun '(x2, z2, x3, z3, swap, i) =>
-                   (i >= -1)%Z /\
+                   (-1 <= i < scalarbits)%Z /\
                    projective (pair x2 z2) /\
                    projective (pair x3 z3) /\
                    let q := if (swap:bool) then (pair x3 z3) else (pair x2 z2) in
                    let q' := if (swap:bool) then (pair x2 z2) else (pair x3 z3) in
-                   let r := (n >> Z.succ i)%Z in
+                   let r := ((n mod 2^scalarbits) >> Z.succ i)%Z in
                    eq q (to_xz (scalarmult r P)) /\
                    eq q' (to_xz (scalarmult (Z.succ r) P)) /\
-                   ladder_invariant point (scalarmult r P) (scalarmult (Z.succ r) P))
+                   ladder_invariant (X0 P) (scalarmult r P) (scalarmult (Z.succ r) P))
                 (fun s => Z.to_nat (Z.succ (snd s))) (* decreasing measure *) ).
       { split; cbn.
         { (* invariant holds in the beginning *)
-          rewrite ?Z.succ_pred, ?Z.lt_pow_2_shiftr, <-?Z.one_succ by tauto.
-          repeat split; [lia|t..]. }
+          rewrite ?Z.succ_pred, ?Z.lt_pow_2_shiftr, <-?Z.one_succ by (apply Z.mod_pos_bound; lia).
+          repeat split; [lia|lia|t..]. }
         { (* sufficient fuel *) rewrite Z.succ_pred. reflexivity. } }
       { intros [ [ [ [ [x2 z2] x3] z3] swap] i] [Hi [Hx2z2 [Hx3z3 [Hq [Hq' Hladder]]]]].
         destruct (i >=? 0)%Z eqn:Hbranch; (* did the loop continue? *)
           rewrite Z.geb_ge_iff in Hbranch.
         split.
         { (* if loop continued, invariant is preserved *)
+          remember (Z.testbit n i) as bit eqn:Hbit; symmetry in Hbit.
+          erewrite <-(Z.mod_pow2_bits_low _ scalarbits) in Hbit by tauto.
+          set (n mod 2 ^ scalarbits)%Z as n' in *.
           let group _ := ltac:(repeat rewrite ?scalarmult_add_l, ?scalarmult_0_l, ?scalarmult_1_l, ?Hierarchy.left_identity, ?Hierarchy.right_identity, ?Hierarchy.associative, ?(Hierarchy.commutative _ P); reflexivity) in
-          destruct (Z.testbit n i) eqn:Hbit in *;
+          destruct bit in *;
             destruct swap eqn:Hswap in *;
             repeat match goal with
                    | _ => solve [ congruence | assumption | lia ]
@@ -367,8 +360,8 @@ Module M.
                      => let pf := constr:(to_xz_add p xz x'z' _ _ H G HQ HQ' ltac:(auto using ladder_invariant_swap)) in
                         unique pose proof (proj1 pf); destruct (proj2 pf) as [? [? [? ?]]] (* because there is no unique destruct *)
                    | _ => progress rewrite ?Z.succ_pred, ?Z.shiftr_succ, <-?Z.div2_spec, <-?Z.add_1_r in *
-                   | |- context [scalarmult (n>>i) ] => rewrite (Z_shiftr_testbit_1 n i), Hbit; cbn [Z.b2z]
-                   | |- context [scalarmult (n>>i+1) ] => rewrite (Z_shiftr_testbit_1 n i), Hbit; cbn [Z.b2z]
+                   | |- context [scalarmult (n'>>i) ] => rewrite (Z_shiftr_testbit_1 n' i), Hbit; cbn [Z.b2z]
+                   | |- context [scalarmult (n'>>i+1) ] => rewrite (Z_shiftr_testbit_1 n' i), Hbit; cbn [Z.b2z]
                    | |- ?P => match type of P with Prop => split end
                    | H: eq (?f _) (to_xz ?LHS) |- eq (?f _) (to_xz ?RHS)
                      => eapply (transitive_eq (to_xz LHS) ltac:(auto using projective_to_xz) H); f_equiv; group ()
@@ -381,11 +374,11 @@ Module M.
         { (* measure decreases *)
           cbv [Let_In]; break_match; cbn; rewrite Z.succ_pred; apply Znat.Z2Nat.inj_lt; lia. }
         { (* if loop exited, invariant implies postcondition *)
-          destruct_head' @and; autorewrite with cancel_pair in *.
           replace i with ((-(1))%Z) in * by lia; clear Hi Hbranch.
           rewrite Z.succ_m1, Z.shiftr_0_r in *.
           cbv [M.cswap];
           destruct swap eqn:Hswap; rewrite <-!to_x_inv00 by assumption;
+            etransitivity; try eapply to_x_to_xz; f_equal;
             eauto using projective_to_xz, proper_to_x_projective. } }
     Qed.
 
@@ -393,59 +386,29 @@ Module M.
        additionally showing that the right-hand-side is 0. This comes from there
        being two points such that to_x gives 0: infinity and (0, 0). *)
 
-    Lemma opp_to_x_to_xz_0
-          (P : M.point)
-          (H : 0 = to_x (to_xz P))
-      : 0 = to_x (to_xz (Mopp P)).
+    Lemma X0_opp_0 (P : M.point) (H : X0 P = 0) : X0 (Mopp P) = 0.
     Proof. t. Qed.
 
-    Lemma add_to_x_to_xz_0
-          (P Q : M.point)
-          (HP : 0 = to_x (to_xz P))
-          (HQ : 0 = to_x (to_xz Q))
-      : 0 = to_x (to_xz (Madd P Q)).
-    Proof. t. Qed.
+    Lemma X0_add_0 (P Q : M.point) (HP : X0 P = 0) (HQ : X0 Q = 0) : X0(Madd P Q) = 0.
+    Proof. cbv [X0] in *; t. Qed.
 
-    Lemma scalarmult_to_x_to_xz_0
-          (n : Z) (P : M.point)
-          (H : 0 = to_x (to_xz P))
-      : 0 = to_x (to_xz (scalarmult n P)).
+    Lemma X0_scalarmult_0 (n : Z) (P : M.point) (H : X0 P = 0) : X0 (scalarmult n P) = 0.
     Proof.
-      induction n using Z.peano_rect_strong.
-      { cbn. t. }
-      { (* Induction case from n to Z.succ n. *)
-        unfold scalarmult_ref.
-        rewrite Z.peano_rect_succ by lia.
-        fold (scalarmult n P).
-        apply add_to_x_to_xz_0; trivial. }
-      { (* Induction case from n to Z.pred n. *)
-        unfold scalarmult_ref.
-        rewrite Z.peano_rect_pred by lia.
-        fold (scalarmult n P).
-        apply add_to_x_to_xz_0.
-        { apply opp_to_x_to_xz_0; trivial. }
-        { trivial. } }
+      clear dependent scalarbits.
+      induction n using Z.peano_rect_strong; try t.
+      { unfold scalarmult_ref. rewrite Z.peano_rect_succ by lia. fold (scalarmult n P).
+        auto using X0_add_0. }
+      { unfold scalarmult_ref. rewrite Z.peano_rect_pred by lia. fold (scalarmult n P).
+        auto using X0_add_0, X0_opp_0. }
     Qed.
 
     (* Combine the two cases together. *)
 
-    Lemma montladder_correct
-          (HFinv : Finv 0 = 0)
-          (n : Z) (P : M.point)
-          (scalarbits : Z) (point : F)
-          (Hn : (0 <= n < 2^scalarbits)%Z)
-          (Hscalarbits : (0 <= scalarbits)%Z)
-          (Hpoint : point = to_x (to_xz P))
-      : montladder scalarbits (Z.testbit n) point = to_x (to_xz (scalarmult n P)).
+    Lemma montladder_correct n P :
+      montladder scalarbits (Z.testbit n) (X0 P) = X0 (scalarmult (n mod 2^scalarbits) P).
     Proof.
-      destruct (dec (point = 0)) as [Hz|Hnz].
-      { rewrite (montladder_correct_0 HFinv _ _ _ Hz Hn Hscalarbits).
-        setoid_subst_rel Feq.
-        apply scalarmult_to_x_to_xz_0.
-        trivial. }
-      { apply (montladder_correct_nz HFinv _ _ _ _ Hnz Hn Hscalarbits).
-        trivial. }
+      destruct (dec (X0 P = 0)) as [Hz|?]; auto using montladder_correct_nz .
+      rewrite montladder_correct_0, X0_scalarmult_0 by trivial; reflexivity.
     Qed.
-
   End MontgomeryCurve.
 End M.
diff --git a/src/Spec/Curve25519.v b/src/Spec/Curve25519.v
index 56b0488ccb..fa4e3e8252 100644
--- a/src/Spec/Curve25519.v
+++ b/src/Spec/Curve25519.v
@@ -68,3 +68,32 @@ Proof.
   Proof_certif 2 prime_2] _).
   native_cast_no_check (@eq_refl bool true).
 Time Qed. (* 1s *)
+
+Local Notation F := (F p).
+
+Require PrimeFieldTheorems.
+
+Lemma field : @Hierarchy.field F eq F.zero F.one F.opp F.add F.sub F.mul F.inv F.div.
+Proof. apply PrimeFieldTheorems.F.field_modulo, prime_p. Qed.
+Lemma char_ge_3 : @Ring.char_ge F eq F.zero F.one F.opp F.add F.sub F.mul 3.
+Proof. eapply Hierarchy.char_ge_weaken; try apply ModularArithmeticTheorems.F.char_gt; Decidable.vm_decide. Qed.
+
+Require Import Spec.MontgomeryCurve.
+Module M.
+  Definition a : F := F.of_Z _ 486662.
+  Definition b : F := F.one.
+  Definition a24 : F := ((a - F.of_Z _ 2) / F.of_Z _ 4)%F.
+  Definition point := @M.point F eq F.add F.mul a F.one.
+  Definition B : point :=
+    exist _ (inl (F.of_Z _ 9, F.of_Z _ 14781619447589544791020593568409986887264606134616475288964881837755586237401)) eq_refl.
+
+  Lemma a2m4_nonzero : F.sub (F.mul a a) (F.of_Z _ 4) <> F.zero. Decidable.vm_decide. Qed.
+  Lemma a2m4_nonsq : ~(exists r, F.mul r r = F.sub (F.mul a a) (F.of_Z _ 4)).
+  Proof. epose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); Decidable.vm_decide. Qed.
+  Lemma b_nonzero : b <> F.zero. Decidable.vm_decide. Qed.
+
+  Definition add := (M.add(field:=field)(char_ge_3:=char_ge_3)(a:=a)(b_nonzero:=b_nonzero)).
+  Definition opp := (M.opp(field:=field)(a:=a)(b_nonzero:=b_nonzero)).
+  Definition X0 := (M.X0(Feq:=eq)(Fzero:=F.zero)(Fadd:=F.add)(Fmul:=F.mul)(a:=a)(b:=b)).
+  Definition scalarmult := (@ScalarMult.scalarmult_ref _ add M.zero opp).
+End M.
diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v
index 55c73c7fd2..3f16a312e7 100644
--- a/src/Spec/MontgomeryCurve.v
+++ b/src/Spec/MontgomeryCurve.v
@@ -61,5 +61,21 @@ Module M.
     Proof.
       cbv [coordinates]; BreakMatch.break_match; trivial; Field.fsatz.
     Qed.
+
+    Program Definition opp (P : point) : point :=
+      match P return F*F+∞ with
+      | (x, y) => (x, -y)
+      | ∞ => ∞
+      end.
+    Next Obligation.
+    Proof. 
+      DestructHead.destruct_head @point; cbv; BreakMatch.break_match; trivial; Field.fsatz.
+    Qed.
+    
+    Definition X0 (P : point) : F :=
+      match coordinates P with
+      | (x, y) => x
+      | _ => Fzero
+      end.
   End MontgomeryCurve.
 End M.
diff --git a/src/Spec/Test/X25519.v b/src/Spec/Test/X25519.v
index 8390fffdc7..934b20a39c 100644
--- a/src/Spec/Test/X25519.v
+++ b/src/Spec/Test/X25519.v
@@ -5,11 +5,8 @@ Require Import Coq.NArith.BinNatDef.
 Require Import Coq.ZArith.BinIntDef.
 Require Import Coq.PArith.BinPosDef.
 Require Import Spec.ModularArithmetic Spec.Curve25519 Spec.MxDH Crypto.Util.Decidable.
-Definition F := F Curve25519.p.
-Definition a : F := F.of_Z _ 486662.
-Definition a24 : F := ((a - F.of_Z _ 2) / F.of_Z _ 4)%F.
 Definition cswap {T} (swap:bool) (a b:T) := if swap then (b, a) else (a, b).
-Definition monty s : F -> F := @MxDH.montladder F F.zero F.one F.add F.sub F.mul F.inv a24 cswap 255 (BinNat.N.testbit_nat s).
+Definition monty s : F p -> F p := @MxDH.montladder _ F.zero F.one F.add F.sub F.mul F.inv M.a24 cswap 255 (BinNat.N.testbit_nat s).
 
 Example one_basepoint : F.to_Z (monty 1 (F.of_Z _ 9)) = 9%Z.
 Proof. vm_decide_no_check. Qed.
@@ -28,7 +25,7 @@ Example order_basepoint : F.to_Z (monty (N.pos l) (F.of_Z _ 9)) = 0%Z.
 Proof. vm_decide_no_check. Qed. (* note: ideally we'd check that z=0 *)
 
 Definition double x := (* takes as input affine x, returns projective x/z *)
-  fst (@MxDH.ladderstep F F.add F.sub F.mul a24 (F.of_Z _ 0) (x, F.of_Z _ 1) (x, F.of_Z _ 1)).
+  fst (@MxDH.ladderstep _ F.add F.sub F.mul M.a24 (F.of_Z _ 0) (x, F.of_Z _ 1) (x, F.of_Z _ 1)).
 (* EllipticCurve(GF(2^255 - 19), [0,486662,0,1,0]).torsion_polynomial(8).roots(multiplicities=False) *)
 (* Point of order 2: *)
 Lemma double_zero : snd (double (F.of_Z _ 0)) = F.of_Z _ 0. vm_decide_no_check. Qed.
@@ -36,7 +33,7 @@ Lemma double_zero : snd (double (F.of_Z _ 0)) = F.of_Z _ 0. vm_decide_no_check.
 Lemma double_one  : fst (double (F.of_Z _ 1)) = F.of_Z _ 0. vm_decide_no_check. Qed.
 Lemma double_minusone:fst(double(F.of_Z _(-1)))=F.of_Z _ 0. vm_decide_no_check. Qed.
 (* Points of order 8: *)
-Definition order8_x1 : F := F.of_Z _ 39382357235489614581723060781553021112529911719440698176882885853963445705823.
-Definition order8_x2 : F := F.of_Z _ 325606250916557431795983626356110631294008115727848805560023387167927233504.
+Definition order8_x1 := F.of_Z p 39382357235489614581723060781553021112529911719440698176882885853963445705823.
+Definition order8_x2 := F.of_Z p 325606250916557431795983626356110631294008115727848805560023387167927233504.
 Lemma double_order8_x1 : fst (double order8_x1) = snd (double order8_x1). vm_decide_no_check. Qed.
 Lemma double_order8_x2 : fst (double order8_x2) = snd (double order8_x2). vm_decide_no_check. Qed.