Added top-level modulus comparison operation so field-element decoding can return None if input is greater than modulus

1 files changed, 19 insertions, 1 deletions

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.