2 files changed, 37 insertions, 1 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index d1bd49a55..3b50662a6 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -892,6 +892,24 @@ Section Canonicalization.
     : conditional_subtract_modulus_opt f cond = conditional_subtract_modulus f cond
     := Eval cbv [proj2_sig conditional_subtract_modulus_opt_sig] in proj2_sig (conditional_subtract_modulus_opt_sig f cond).
 
+  Definition ge_modulus_opt_sig (us : list Z) :
+    { b : bool | b = ModularBaseSystemList.ge_modulus us }.
+  Proof.
+    eexists.
+    cbv beta iota delta [ge_modulus ge_modulus'].
+    change length with length_opt.
+    change nth_default with @nth_default_opt.
+    change minus with minus_opt.
+    reflexivity.
+  Defined.
+
+  Definition ge_modulus_opt us : bool
+    := Eval cbv [proj1_sig ge_modulus_opt_sig] in proj1_sig (ge_modulus_opt_sig us).
+
+  Definition ge_modulus_opt_correct us :
+    ge_modulus_opt us = ge_modulus us
+    := Eval cbv [proj2_sig ge_modulus_opt_sig] in proj2_sig (ge_modulus_opt_sig us).
+
   Definition freeze_opt_sig (us : list Z) :
     { b : list Z | length us = length limb_widths
                    -> b = ModularBaseSystemList.freeze us }.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index ebaa54080..8f9e1bc59 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -129,7 +129,7 @@ Definition zero_subst : zero = zero_ := eq_refl zero_.
 Definition modulus_digits_ := Eval compute in ModularBaseSystemList.modulus_digits.
 Definition modulus_digits_subst : ModularBaseSystemList.modulus_digits = modulus_digits_ := eq_refl modulus_digits_.
 
-Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb andb.
+Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb andb.
 
 Definition app_7 {T} (f : wire_digits) (P : wire_digits -> T) : T.
 Proof.
@@ -361,6 +361,24 @@ Proof.
   + reflexivity.
 Qed.
 
+Definition ge_modulus_sig (f : fe25519) :
+  { b : bool | b = ge_modulus_opt (to_list 10 f) }.
+Proof.
+  cbv [fe25519] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists; cbv [ge_modulus_opt].
+  rewrite !modulus_digits_subst.
+  cbv.
+  reflexivity.
+Defined.
+
+Definition ge_modulus (f : fe25519) : bool
+  := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in proj1_sig (ge_modulus_sig f).
+
+Definition ge_modulus_correct (f : fe25519) :
+  ge_modulus f = ge_modulus_opt (to_list 10 f)
+  := Eval cbv beta iota delta [proj2_sig ge_modulus_sig] in proj2_sig (ge_modulus_sig f).
+
 Definition freeze_sig (f : fe25519) :
   { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt c_ (to_list 10 f)) }.
 Proof.