for i in *.json; do ./copy_bounds.sh $i; done

6 files changed, 42 insertions, 24 deletions

diff --git a/src/SpecificGen/GF2213_32Bounded.v b/src/SpecificGen/GF2213_32Bounded.v
index 9a35ce124..f304eb648 100644
--- a/src/SpecificGen/GF2213_32Bounded.v
+++ b/src/SpecificGen/GF2213_32Bounded.v
@@ -83,9 +83,11 @@ Definition postfreezeW : fe2213_32W -> fe2213_32W :=
 Definition freezeW (f : fe2213_32W) : fe2213_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
-Definition powW (f : fe2213_32W) chain := fold_chain_opt (proj1_fe2213_32W one) mulW chain [f].
+(* Wrapper to allow extracted code to not unfold [mulW] *)
+Definition mulW_noinline := mulW.
+Definition powW (f : fe2213_32W) chain := fold_chain_opt (proj1_fe2213_32W one) mulW_noinline chain [f].
 Definition invW (f : fe2213_32W) : fe2213_32W
-  := Eval cbv -[Let_In fe2213_32W mulW] in powW f (chain inv_ec).
+  := Eval cbv -[Let_In fe2213_32W 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 fe2213_32W mulW]; reflexivity).
+    by abstract (cbv -[Let_In fe2213_32W mulW_noinline]; reflexivity).
   rewrite H.
   rewrite inv_correct.
   cbv [inv_opt].
@@ -300,7 +302,7 @@ Definition sqrt_m1W : fe2213_32W :=
 
 Definition GF2213_32sqrt x : GF2213_32.fe2213_32 :=
   dlet powx := powW (fe2213_32ZToW x) (chain GF2213_32.sqrt_ec) in
-  GF2213_32.sqrt (fe2213_32WToZ powx) (fe2213_32WToZ (mulW powx powx)) x.
+  GF2213_32.sqrt (fe2213_32WToZ powx) (fe2213_32WToZ (mulW_noinline powx powx)) x.
 
 Definition sqrtW_sig
   : { sqrtW | iunop_correct_and_bounded sqrtW GF2213_32sqrt }.
@@ -325,6 +327,7 @@ Proof.
                   | [ |- is_bounded (fe2213_32WToZ ?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
diff --git a/src/SpecificGen/GF2519_32Bounded.v b/src/SpecificGen/GF2519_32Bounded.v
index 292ee9adb..a878292a2 100644
--- a/src/SpecificGen/GF2519_32Bounded.v
+++ b/src/SpecificGen/GF2519_32Bounded.v
@@ -83,9 +83,11 @@ Definition postfreezeW : fe2519_32W -> fe2519_32W :=
 Definition freezeW (f : fe2519_32W) : fe2519_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
-Definition powW (f : fe2519_32W) chain := fold_chain_opt (proj1_fe2519_32W one) mulW chain [f].
+(* Wrapper to allow extracted code to not unfold [mulW] *)
+Definition mulW_noinline := mulW.
+Definition powW (f : fe2519_32W) chain := fold_chain_opt (proj1_fe2519_32W one) mulW_noinline chain [f].
 Definition invW (f : fe2519_32W) : fe2519_32W
-  := Eval cbv -[Let_In fe2519_32W mulW] in powW f (chain inv_ec).
+  := Eval cbv -[Let_In fe2519_32W 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 fe2519_32W mulW]; reflexivity).
+    by abstract (cbv -[Let_In fe2519_32W mulW_noinline]; reflexivity).
   rewrite H.
   rewrite inv_correct.
   cbv [inv_opt].
@@ -300,7 +302,7 @@ Definition sqrt_m1W : fe2519_32W :=
 
 Definition GF2519_32sqrt x : GF2519_32.fe2519_32 :=
   dlet powx := powW (fe2519_32ZToW x) (chain GF2519_32.sqrt_ec) in
-  GF2519_32.sqrt (fe2519_32WToZ powx) (fe2519_32WToZ (mulW powx powx)) x.
+  GF2519_32.sqrt (fe2519_32WToZ powx) (fe2519_32WToZ (mulW_noinline powx powx)) x.
 
 Definition sqrtW_sig
   : { sqrtW | iunop_correct_and_bounded sqrtW GF2519_32sqrt }.
@@ -325,6 +327,7 @@ Proof.
                   | [ |- is_bounded (fe2519_32WToZ ?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
diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v
index 311001606..8a978fc6f 100644
--- a/src/SpecificGen/GF25519_32Bounded.v
+++ b/src/SpecificGen/GF25519_32Bounded.v
@@ -83,9 +83,11 @@ Definition postfreezeW : fe25519_32W -> fe25519_32W :=
 Definition freezeW (f : fe25519_32W) : fe25519_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
-Definition powW (f : fe25519_32W) chain := fold_chain_opt (proj1_fe25519_32W one) mulW chain [f].
+(* Wrapper to allow extracted code to not unfold [mulW] *)
+Definition mulW_noinline := mulW.
+Definition powW (f : fe25519_32W) chain := fold_chain_opt (proj1_fe25519_32W one) mulW_noinline chain [f].
 Definition invW (f : fe25519_32W) : fe25519_32W
-  := Eval cbv -[Let_In fe25519_32W mulW] in powW f (chain inv_ec).
+  := Eval cbv -[Let_In fe25519_32W 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 fe25519_32W mulW]; reflexivity).
+    by abstract (cbv -[Let_In fe25519_32W mulW_noinline]; reflexivity).
   rewrite H.
   rewrite inv_correct.
   cbv [inv_opt].
@@ -300,7 +302,7 @@ Definition sqrt_m1W : fe25519_32W :=
 
 Definition GF25519_32sqrt x : GF25519_32.fe25519_32 :=
   dlet powx := powW (fe25519_32ZToW x) (chain GF25519_32.sqrt_ec) in
-  GF25519_32.sqrt (fe25519_32WToZ powx) (fe25519_32WToZ (mulW powx powx)) x.
+  GF25519_32.sqrt (fe25519_32WToZ powx) (fe25519_32WToZ (mulW_noinline powx powx)) x.
 
 Definition sqrtW_sig
   : { sqrtW | iunop_correct_and_bounded sqrtW GF25519_32sqrt }.
@@ -325,6 +327,7 @@ Proof.
                   | [ |- is_bounded (fe25519_32WToZ ?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
diff --git a/src/SpecificGen/GF25519_64Bounded.v b/src/SpecificGen/GF25519_64Bounded.v
index e474eb2bc..528e536a0 100644
--- a/src/SpecificGen/GF25519_64Bounded.v
+++ b/src/SpecificGen/GF25519_64Bounded.v
@@ -83,9 +83,11 @@ Definition postfreezeW : fe25519_64W -> fe25519_64W :=
 Definition freezeW (f : fe25519_64W) : fe25519_64W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
-Definition powW (f : fe25519_64W) chain := fold_chain_opt (proj1_fe25519_64W one) mulW chain [f].
+(* Wrapper to allow extracted code to not unfold [mulW] *)
+Definition mulW_noinline := mulW.
+Definition powW (f : fe25519_64W) chain := fold_chain_opt (proj1_fe25519_64W one) mulW_noinline chain [f].
 Definition invW (f : fe25519_64W) : fe25519_64W
-  := Eval cbv -[Let_In fe25519_64W mulW] in powW f (chain inv_ec).
+  := Eval cbv -[Let_In fe25519_64W 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 fe25519_64W mulW]; reflexivity).
+    by abstract (cbv -[Let_In fe25519_64W mulW_noinline]; reflexivity).
   rewrite H.
   rewrite inv_correct.
   cbv [inv_opt].
@@ -300,7 +302,7 @@ Definition sqrt_m1W : fe25519_64W :=
 
 Definition GF25519_64sqrt x : GF25519_64.fe25519_64 :=
   dlet powx := powW (fe25519_64ZToW x) (chain GF25519_64.sqrt_ec) in
-  GF25519_64.sqrt (fe25519_64WToZ powx) (fe25519_64WToZ (mulW powx powx)) x.
+  GF25519_64.sqrt (fe25519_64WToZ powx) (fe25519_64WToZ (mulW_noinline powx powx)) x.
 
 Definition sqrtW_sig
   : { sqrtW | iunop_correct_and_bounded sqrtW GF25519_64sqrt }.
@@ -325,6 +327,7 @@ Proof.
                   | [ |- is_bounded (fe25519_64WToZ ?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
diff --git a/src/SpecificGen/GF41417_32Bounded.v b/src/SpecificGen/GF41417_32Bounded.v
index af6a28421..d44c722b2 100644
--- a/src/SpecificGen/GF41417_32Bounded.v
+++ b/src/SpecificGen/GF41417_32Bounded.v
@@ -83,9 +83,11 @@ Definition postfreezeW : fe41417_32W -> fe41417_32W :=
 Definition freezeW (f : fe41417_32W) : fe41417_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
-Definition powW (f : fe41417_32W) chain := fold_chain_opt (proj1_fe41417_32W one) mulW chain [f].
+(* Wrapper to allow extracted code to not unfold [mulW] *)
+Definition mulW_noinline := mulW.
+Definition powW (f : fe41417_32W) chain := fold_chain_opt (proj1_fe41417_32W one) mulW_noinline chain [f].
 Definition invW (f : fe41417_32W) : fe41417_32W
-  := Eval cbv -[Let_In fe41417_32W mulW] in powW f (chain inv_ec).
+  := Eval cbv -[Let_In fe41417_32W 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 fe41417_32W mulW]; reflexivity).
+    by abstract (cbv -[Let_In fe41417_32W mulW_noinline]; reflexivity).
   rewrite H.
   rewrite inv_correct.
   cbv [inv_opt].
@@ -300,7 +302,7 @@ Definition sqrt_m1W : fe41417_32W :=
 
 Definition GF41417_32sqrt x : GF41417_32.fe41417_32 :=
   dlet powx := powW (fe41417_32ZToW x) (chain GF41417_32.sqrt_ec) in
-  GF41417_32.sqrt (fe41417_32WToZ powx) (fe41417_32WToZ (mulW powx powx)) x.
+  GF41417_32.sqrt (fe41417_32WToZ powx) (fe41417_32WToZ (mulW_noinline powx powx)) x.
 
 Definition sqrtW_sig
   : { sqrtW | iunop_correct_and_bounded sqrtW GF41417_32sqrt }.
@@ -325,6 +327,7 @@ Proof.
                   | [ |- is_bounded (fe41417_32WToZ ?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
diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v
index 3574afadc..d77609534 100644
--- a/src/SpecificGen/GF5211_32Bounded.v
+++ b/src/SpecificGen/GF5211_32Bounded.v
@@ -83,9 +83,11 @@ Definition postfreezeW : fe5211_32W -> fe5211_32W :=
 Definition freezeW (f : fe5211_32W) : fe5211_32W := Eval cbv beta delta [prefreezeW postfreezeW] in postfreezeW (prefreezeW f).
 
 Local Transparent Let_In.
-Definition powW (f : fe5211_32W) chain := fold_chain_opt (proj1_fe5211_32W one) mulW chain [f].
+(* Wrapper to allow extracted code to not unfold [mulW] *)
+Definition mulW_noinline := mulW.
+Definition powW (f : fe5211_32W) chain := fold_chain_opt (proj1_fe5211_32W one) mulW_noinline chain [f].
 Definition invW (f : fe5211_32W) : fe5211_32W
-  := Eval cbv -[Let_In fe5211_32W mulW] in powW f (chain inv_ec).
+  := Eval cbv -[Let_In fe5211_32W 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 fe5211_32W mulW]; reflexivity).
+    by abstract (cbv -[Let_In fe5211_32W mulW_noinline]; reflexivity).
   rewrite H.
   rewrite inv_correct.
   cbv [inv_opt].
@@ -300,7 +302,7 @@ Definition sqrt_m1W : fe5211_32W :=
 
 Definition GF5211_32sqrt x : GF5211_32.fe5211_32 :=
   dlet powx := powW (fe5211_32ZToW x) (chain GF5211_32.sqrt_ec) in
-  GF5211_32.sqrt (fe5211_32WToZ powx) (fe5211_32WToZ (mulW powx powx)) x.
+  GF5211_32.sqrt (fe5211_32WToZ powx) (fe5211_32WToZ (mulW_noinline powx powx)) x.
 
 Definition sqrtW_sig
   : { sqrtW | iunop_correct_and_bounded sqrtW GF5211_32sqrt }.
@@ -325,6 +327,7 @@ Proof.
                   | [ |- is_bounded (fe5211_32WToZ ?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