final touches/fixes for freeze restructuring

3 files changed, 10 insertions, 13 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 96c63adc7..dd6d4d4b8 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -103,7 +103,7 @@ Definition feEnc (x : GF25519.fe25519) : Word.word 255 :=
           (Word.combine (ZNWord 32 x4)
             (Word.combine (ZNWord 32 x5)
               (Word.combine (ZNWord 32 x6) (ZNWord 31 x7))))))).
-
+Check GF25519.ge_modulus.
 Definition feDec (w : Word.word 255) : option GF25519.fe25519 :=
   let w0 := Word.split1 32 _ w in
   let a0 := Word.split2 32 _ w in
@@ -120,7 +120,7 @@ Definition feDec (w : Word.word 255) : option GF25519.fe25519 :=
   let w6 := Word.split1 32 _ a5 in
   let w7 := Word.split2 32 _ a5 in
   let result := (GF25519.unpack (WordNZ w0, WordNZ w1, WordNZ w2, WordNZ w3, WordNZ w4, WordNZ w5, WordNZ w6, WordNZ w7)) in
-  if GF25519.ge_modulus result
+  if Z.eqb (GF25519.ge_modulus result) 1
   then None else (Some result).
 
 Let ERepEnc :=
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index d0af83e11..1117229d1 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -979,9 +979,9 @@ Section Canonicalization.
     induction i; intros; simpl; cbv [Let_In]; break_if; try reflexivity;
       apply IHi.
   Qed.
-(*
-  Definition ge_modulus'_opt_sig {A} (f : Z -> A) (us : list Z) b i :
-    { a : A | a = ModularBaseSystemList.ge_modulus' f us b i}.
+
+  Definition ge_modulus_opt_sig (us : list Z) :
+    { a : Z | a = ge_modulus us}.
   Proof.
     eexists.
     cbv [ge_modulus ge_modulus'].
@@ -991,13 +991,12 @@ Section Canonicalization.
     reflexivity.
   Defined.
 
-  Definition ge_modulus'_opt {A} f us b i : Z
-    := Eval cbv [proj1_sig ge_modulus'_opt_sig] in proj1_sig (@ge_modulus'_opt_sig A f us b i).
+  Definition ge_modulus_opt us : Z
+    := Eval cbv [proj1_sig ge_modulus_opt_sig] in proj1_sig (ge_modulus_opt_sig us).
 
-  Definition ge_modulus'_opt_correct {A} f us :
-    @ge_modulus'_opt A f us b i = @ge_modulus' A f us b i
-    := Eval cbv [proj2_sig ge_modulus_opt_sig] in proj2_sig (@ge_modulus'_opt_sig A f 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
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 3ea794435..e89615dde 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -460,7 +460,6 @@ Proof.
   + reflexivity.
 Qed.
 
-(*
 Definition ge_modulus_sig (f : fe25519) :
   { b : Z | b = ge_modulus_opt (to_list 10 f) }.
 Proof.
@@ -485,7 +484,6 @@ Proof.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
-*)
 
 Definition freeze_sig (f : fe25519) :
   { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }.