Add mulW_noinline

2 files changed, 16 insertions, 8 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 5c107eb39..2cd70a3b4 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -1382,6 +1382,10 @@ Local Ltac prove_bounded_by :=
            => apply GF25519Bounded.mulW_correct_and_bounded
          | [ |- GF25519BoundedCommon.is_bounded
                   (GF25519BoundedCommon.fe25519WToZ
+                     (GF25519Bounded.mulW_noinline _ _)) = true ]
+           => apply GF25519Bounded.mulW_correct_and_bounded
+         | [ |- GF25519BoundedCommon.is_bounded
+                  (GF25519BoundedCommon.fe25519WToZ
                      (GF25519Bounded.powW _ _)) = true ]
            => apply GF25519Bounded.powW_correct_and_bounded
          | [ |- context[GF25519BoundedCommon.fe25519WToZ (GF25519BoundedCommon.fe25519ZToW _)] ]
@@ -1410,7 +1414,7 @@ Proof.
   rewrite ModularBaseSystemProofs.encode_rep.
   symmetry.
   eapply @ModularBaseSystemProofs.sqrt_5mod8_correct;
-    eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; prove_bounded_by; eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519; [ reflexivity | 
+    eauto using GF25519.freezePreconditions25519, ModularBaseSystemProofs.encode_rep, bounded_by_freeze, bounded_by_encode_freeze; prove_bounded_by; eauto using GF25519BoundedCommon.is_bounded_proj1_fe25519; [ reflexivity |
   lazymatch goal with
     | |- appcontext[GF25519Bounded.powW ?a ?ch] =>
       let A := fresh "H" in
@@ -1420,8 +1424,9 @@ Proof.
         | rewrite A;
           rewrite GF25519.pow_correct, ModularBaseSystemOpt.pow_opt_correct
             by reflexivity]
-    end..]; 
+    end..];
     [ rewrite GF25519BoundedCommon.fe25519WToZ_ZToW by (eapply GF25519BoundedCommon.is_bounded_proj1_fe25519); reflexivity | ].
+  unfold GF25519Bounded.mulW_noinline.
   match goal with
   | |- appcontext[GF25519Bounded.mulW ?a ?b] =>
     let A := fresh "H" in
@@ -1456,7 +1461,7 @@ Proof.
   intros. pose proof sqrt_correct' (GF25519BoundedCommon.encode x) as H.
   rewrite GF25519BoundedCommon.decode_encode in H; exact H.
 Qed.
-  
+
 
 Local Instance Proper_sqrt :
   Proper (GF25519BoundedCommon.eq ==> GF25519BoundedCommon.eq) GF25519Bounded.sqrt.
@@ -1620,4 +1625,4 @@ Print Assumptions three_correct.
 (* [B_order_l] is proven above in this file, just replace Admitted with Qed, start the build and wait for a couple of hours *)
 (* [prime_q] and [prime_l] have been proven in Coq exactly as stated here, see <https://github.com/andres-erbsen/safecurves-primes> for the (lengthy) proofs *)
 (* [SHA512] is outside the scope of this project, but its type is satisfied by [(fun n bits => Word.wzero 512)] *)
-Definition __check_SHA512_type := [(fun n bits => Word.wzero 512); SHA512].
\ No newline at end of file
+Definition __check_SHA512_type := [(fun n bits => Word.wzero 512); SHA512].
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index d79e413a4..66de326b2 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -83,9 +83,11 @@ Definition postfreezeW : fe25519W -> fe25519W :=
 Definition freezeW (f : fe25519W) : fe25519W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
-Definition powW (f : fe25519W) chain := fold_chain_opt (proj1_fe25519W one) mulW chain [f].
+(* Wrapper to allow extracted code to not unfold [mulW] *)
+Definition mulW_noinline := mulW.
+Definition powW (f : fe25519W) chain := fold_chain_opt (proj1_fe25519W one) mulW_noinline chain [f].
 Definition invW (f : fe25519W) : fe25519W
-  := Eval cbv -[Let_In fe25519W mulW] in powW f (chain inv_ec).
+  := Eval cbv -[Let_In fe25519W mulW_noinline] in powW f (chain inv_ec).
 
 Local Ltac port_correct_and_bounded pre_rewrite opW interp_rop rop_cb :=
   change opW with (interp_rop);
@@ -229,7 +231,7 @@ Lemma invW_correct_and_bounded : iunop_correct_and_bounded invW inv.
 Proof.
   intro f.
   assert (H : forall f, invW f = powW f (chain inv_ec))
-    by abstract (cbv -[Let_In fe25519W mulW]; reflexivity).
+    by abstract (cbv -[Let_In fe25519W mulW_noinline]; reflexivity).
   rewrite H.
   rewrite inv_correct.
   cbv [inv_opt].
@@ -300,7 +302,7 @@ Definition sqrt_m1W : fe25519W :=
 
 Definition GF25519sqrt x : GF25519.fe25519 :=
   dlet powx := powW (fe25519ZToW x) (chain GF25519.sqrt_ec) in
-  GF25519.sqrt (fe25519WToZ powx) (fe25519WToZ (mulW powx powx)) x.
+  GF25519.sqrt (fe25519WToZ powx) (fe25519WToZ (mulW_noinline powx powx)) x.
 
 Definition sqrtW_sig
   : { sqrtW | iunop_correct_and_bounded sqrtW GF25519sqrt }.
@@ -325,6 +327,7 @@ Proof.
                   | [ |- is_bounded (fe25519WToZ ?op) = true ]
                     => lazymatch op with
                        | mulW _ _ => apply mulW_correct_and_bounded
+                       | mulW_noinline _ _ => apply mulW_correct_and_bounded
                        | powW _ _ => apply powW_correct_and_bounded
                        | sqrt_m1W => vm_compute; reflexivity
                        | _ => assumption