separate freeze into two parts

1 files changed, 58 insertions, 8 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 2c0365fd2..de6a47c01 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -499,8 +499,37 @@ Proof.
   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)) }.
+Definition prefreeze_sig (f : fe25519) :
+  { f' : fe25519 | f' = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)) }.
+Proof.
+  cbv [fe25519] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  eexists.
+  cbv - [from_list_default].
+  (* TODO(jgross,jadep): use Reflective linearization here? *)
+  repeat (
+       set_evars; rewrite app_Let_In_nd; subst_evars;
+       eapply Proper_Let_In_nd_changebody; [reflexivity|intro]).
+  cbv [from_list_default from_list_default'].
+  reflexivity.
+Defined.
+
+Definition prefreeze (f : fe25519) : fe25519 :=
+  Eval cbv beta iota delta [proj1_sig prefreeze_sig] in
+    let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in
+    proj1_sig (prefreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
+
+Definition prefreeze_correct (f : fe25519)
+  : prefreeze f = from_list_default 0 10 (carry_full_3_opt c_ (to_list 10 f)).
+Proof.
+  pose proof (proj2_sig (prefreeze_sig f)).
+  cbv [fe25519] in *.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
+  assumption.
+Defined.
+
+Definition postfreeze_sig (f : fe25519) :
+  { f' : fe25519 | f' = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)) }.
 Proof.
   cbv [fe25519] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
@@ -517,20 +546,41 @@ Proof.
   reflexivity.
 Defined.
 
-Definition freeze (f : fe25519) : fe25519 :=
-  Eval cbv beta iota delta [proj1_sig freeze_sig] in
+Definition postfreeze (f : fe25519) : fe25519 :=
+  Eval cbv beta iota delta [proj1_sig postfreeze_sig] in
     let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in
-    proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
+    proj1_sig (postfreeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)).
 
-Definition freeze_correct (f : fe25519)
-  : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)).
+Definition postfreeze_correct (f : fe25519)
+  : postfreeze f = from_list_default 0 10 (conditional_subtract_modulus_opt (int_width := int_width) (to_list 10 f)).
 Proof.
-  pose proof (proj2_sig (freeze_sig f)).
+  pose proof (proj2_sig (postfreeze_sig f)).
   cbv [fe25519] in *.
   repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   assumption.
 Defined.
 
+Definition freeze (f : fe25519) : fe25519 :=
+  dlet x := prefreeze f in
+  postfreeze x.
+
+Local Transparent Let_In.
+Definition freeze_correct (f : fe25519)
+  : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)).
+Proof.
+  cbv [freeze_opt freeze Let_In].
+  rewrite prefreeze_correct.
+  rewrite postfreeze_correct.
+  Check from_list_default_eq.
+  match goal with
+    |- appcontext [to_list _ (from_list_default _ ?n ?xs)] =>
+    assert (length xs = n) as pf; [ | rewrite from_list_default_eq with (pf0 := pf) ] end.
+  { rewrite carry_full_3_opt_correct; repeat rewrite ModularBaseSystemListProofs.length_carry_full; auto using length_to_list. }
+  rewrite to_list_from_list.
+  reflexivity.
+Qed.
+Local Opaque Let_In.
+
 Definition fieldwiseb_sig (f g : fe25519) :
   { b | b = @fieldwiseb Z Z 10 Z.eqb f g }.
 Proof.