1 files changed, 65 insertions, 2 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 37e0c08db..2ec338625 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -32,11 +32,30 @@ Defined.
 (* Precompute k and c *)
 Definition k_ := Eval compute in k.
 Definition c_ := Eval compute in c.
+Definition base_ := Eval compute in base.
+Definition limb_widths_ := Eval compute in limb_widths.
+
+Definition c_subst : c = c_ := eq_refl c_.
+
+Lemma c_reduce1 : (c * Z.ones (32 - log_cap (pred (length base))) < max_bound 0 + 1)%Z.
+Proof.
+  cbv; congruence.
+Qed.
+
+Lemma c_reduce2 : c <= max_bound 0 - c.
+Proof.
+  cbv; congruence.
+Qed.
+
+Lemma two_pow_k_le_2modulus : (2 ^ k <= 2 * modulus)%Z.
+Proof.
+  cbv; congruence.
+Qed.
 
 (* Makes Qed not take forever *)
 Opaque Z.shiftr Pos.iter Z.div2 Pos.div2 Pos.div2_up Pos.succ Z.land
   Z.of_N Pos.land N.ldiff Pos.pred_N Pos.pred_double Z.opp Z.mul Pos.mul
-  Let_In digits Z.add Pos.add Z.pos_sub.
+  Let_In digits Z.add Pos.add Z.pos_sub andb Z.eqb Z.ltb.
 
 Local Open Scope nat_scope.
 Lemma GF25519Base25Point5_mul_reduce_formula :
@@ -47,7 +66,7 @@ Lemma GF25519Base25Point5_mul_reduce_formula :
                       -> rep ls (f*g)%F}.
 Proof.
   eexists; intros ? ? Hf Hg.
-  pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg.
+  pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) c_subst _ _ _ _ Hf Hg) as Hfg.
   compute_formula.
 Time Defined.
 
@@ -84,6 +103,50 @@ Proof.
   compute_formula.
 Defined.
 
+Lemma GF25519Base25Point5_freeze_formula :
+  forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9,
+    {ls | forall x, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] x
+                 -> rep ls x}.
+Proof.
+  eexists.
+  intros x Hf.
+  assert (1 < length base)%nat as lt_1_length_base by (cbv; repeat constructor).
+  assert (0 < 32)%Z by omega.
+  assert (forall w : Z, In w limb_widths -> (w <= 32)%Z) by
+    (cbv [limb_widths params25519 limb_widths_from_len In]; intros w w_cases;
+     repeat (destruct w_cases as  [ ? | w_cases]; [ subst; omega | ]); exfalso; assumption).
+  assert (0 < c)%Z by (change c with c_; cbv; congruence).
+  pose proof c_reduce1.
+  pose proof c_reduce2.
+  pose proof two_pow_k_le_2modulus.
+  pose proof (@freeze_opt_preserves_rep modulus params25519 subCoeff c_ (eq_refl c_) lt_1_length_base 32) as Hfreeze_rep.
+  repeat match goal with H : ?P, H' : ?P -> _ |- _ => specialize (H' H) end.
+  specialize (Hfreeze_rep _ _ Hf).
+  change ModularBaseSystem.rep with rep in Hfreeze_rep.
+  match goal with H : @rep ?M ?P (?f ?l) ?result |- _ =>
+    let m := fresh "m" in
+        set (m := M) in H at 1; change M with m in |- * at 1;
+         (let p := fresh "p" in
+          set (p := P) in H at 1; change P with p in |- * at 1;
+           (let r := fresh "r" in
+            set (r := result) in H |- *))
+  end.
+  cbv [freeze_opt] in Hfreeze_rep.
+  cbv [carry_full_3_opt_cps] in Hfreeze_rep.
+  cbv -[m p r rep] in Hfreeze_rep.
+  exact Hfreeze_rep.
+Defined.
+
+(* Uncomment the below to see pretty-printed freeze function *)
+(*
+Local Transparent Let_In.
+Infix "<<" := Z.shiftr (at level 50).
+Infix "&" := Z.land (at level 50).
+Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_freeze_formula Let_In] in
+  fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 => proj1_sig (
+    GF25519Base25Point5_freeze_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9).
+*)
+
 Definition F25519Rep := (Z * Z * Z * Z * Z  *  Z * Z * Z * Z * Z)%type.
 
 Definition F25519toRep (x:F (2^255 - 19)) : F25519Rep := (0, 0, 0, 0, 0,  0, 0, 0, 0, FieldToZ x)%Z.