Make it easier to extract word64

This makes syntax trees not rely on WS and WO in extraction

(cc @andres-erbsen)

3 files changed, 95 insertions, 11 deletions

diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index b0a3f512a..1352d57cc 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -45,7 +45,7 @@ Local Ltac define_unop_WireToFE f opW blem :=
   abstract bounded_wire_digits_t opW blem.
 
 Local Opaque Let_In.
-Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb.
+Local Opaque Z.add Z.sub Z.mul Z.shiftl Z.shiftr Z.land Z.lor Z.eqb NToWord64.
 Local Arguments interp_radd / _ _.
 Local Arguments interp_rsub / _ _.
 Local Arguments interp_rmul / _ _.
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index 648a27f55..c012d6d90 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -25,6 +25,12 @@ Definition word64 := Word.word 64.
 Coercion word64ToZ (x : word64) : Z
   := Z.of_N (wordToN x).
 Coercion ZToWord64 (x : Z) : word64 := NToWord _ (Z.to_N x).
+Definition NToWord64 : N -> word64 := NToWord _.
+Global Arguments NToWord64 : simpl never.
+Definition word64ize (x : word64) : word64
+  := Eval cbv [wordToN N.succ_double N.double] in NToWord64 (wordToN x).
+Lemma word64ize_id x : word64ize x = x.
+Proof. apply NToWord_wordToN. Qed.
 Definition w64eqb (x y : word64) := weqb x y.
 
 Lemma word64eqb_Zeqb x y : (word64ToZ x =? word64ToZ y)%Z = w64eqb x y.
@@ -131,6 +137,27 @@ Definition wire_digitsWToZ (x : wire_digitsW) : Specific.GF25519.wire_digits
 Definition wire_digitsZToW (x : Specific.GF25519.wire_digits) : wire_digitsW
   := let '(x0, x1, x2, x3, x4, x5, x6, x7) := x in
      (x0 : word64, x1 : word64, x2 : word64, x3 : word64, x4 : word64, x5 : word64, x6 : word64, x7 : word64).
+Definition fe25519W_word64ize (x : fe25519W) : fe25519W
+  := Eval cbv [word64ize] in
+      let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
+      (word64ize x0, word64ize x1, word64ize x2, word64ize x3, word64ize x4, word64ize x5, word64ize x6, word64ize x7, word64ize x8, word64ize x9).
+Definition wire_digitsW_word64ize (x : wire_digitsW) : wire_digitsW
+  := Eval cbv [word64ize] in
+      let '(x0, x1, x2, x3, x4, x5, x6, x7) := x in
+      (word64ize x0, word64ize x1, word64ize x2, word64ize x3, word64ize x4, word64ize x5, word64ize x6, word64ize x7).
+
+Lemma fe25519W_word64ize_id x : fe25519W_word64ize x = x.
+Proof.
+  hnf in x; destruct_head' prod.
+  cbv [fe25519W_word64ize];
+    repeat apply f_equal2; apply word64ize_id.
+Qed.
+Lemma wire_digitsW_word64ize_id x : wire_digitsW_word64ize x = x.
+Proof.
+  hnf in x; destruct_head' prod.
+  cbv [wire_digitsW_word64ize];
+    repeat apply f_equal2; apply word64ize_id.
+Qed.
 
 Definition app_7 {T} (f : wire_digitsW) (P : wire_digitsW -> T) : T.
 Proof.
@@ -268,7 +295,7 @@ Ltac unfold_is_bounded_in H :=
 Definition Pow2_64 := Eval compute in 2^64.
 Definition unfold_Pow2_64 : 2^64 = Pow2_64 := eq_refl.
 
-Definition exist_fe25519W (x : fe25519W) : is_bounded (fe25519WToZ x) = true -> fe25519.
+Definition exist_fe25519W' (x : fe25519W) : is_bounded (fe25519WToZ x) = true -> fe25519.
 Proof.
   refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return is_bounded (fe25519WToZ x) = true -> fe25519 in
           fun H => (fun H' => (Build_bounded_word x0 _, Build_bounded_word x1 _, Build_bounded_word x2 _, Build_bounded_word x3 _, Build_bounded_word x4 _,
@@ -284,6 +311,20 @@ Proof.
       rewrite_hyp !*; reflexivity.
 Defined.
 
+Definition exist_fe25519W (x : fe25519W) : is_bounded (fe25519WToZ x) = true -> fe25519.
+Proof.
+  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) as x := x return is_bounded (fe25519WToZ x) = true -> fe25519 in
+          fun H => _).
+  let v := constr:(exist_fe25519W' (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) H) in
+  let rec do_refine v :=
+      first [ let v' := (eval cbv [exist_fe25519W' fe25519ZToW proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word v)) in
+              refine (Build_bounded_word v' _); abstract exact (word_bounded v)
+            | let v' := (eval cbv [exist_fe25519W' fe25519ZToW proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word (snd v))) in
+              refine (_, Build_bounded_word v' _);
+              [ do_refine (fst v) | abstract exact (word_bounded (snd v)) ] ] in
+  do_refine v.
+Defined.
+
 Definition exist_fe25519' (x : Specific.GF25519.fe25519) : is_bounded x = true -> fe25519.
 Proof.
   intro H; apply (exist_fe25519W (fe25519ZToW x)).
@@ -339,7 +380,7 @@ Proof.
   reflexivity.
 Qed.
 
-Definition exist_wire_digitsW (x : wire_digitsW) : wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits.
+Definition exist_wire_digitsW' (x : wire_digitsW) : wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits.
 Proof.
   refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits in
           fun H => (fun H' => (Build_bounded_word x0 _, Build_bounded_word x1 _, Build_bounded_word x2 _, Build_bounded_word x3 _, Build_bounded_word x4 _,
@@ -355,6 +396,20 @@ Proof.
       rewrite_hyp !*; reflexivity.
 Defined.
 
+Definition exist_wire_digitsW (x : wire_digitsW) : wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits.
+Proof.
+  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) as x := x return wire_digits_is_bounded (wire_digitsWToZ x) = true -> wire_digits in
+          fun H => _).
+  let v := constr:(exist_wire_digitsW' (x0, x1, x2, x3, x4, x5, x6, x7) H) in
+  let rec do_refine v :=
+      first [ let v' := (eval cbv [exist_wire_digitsW' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word v)) in
+              refine (Build_bounded_word v' _); abstract exact (word_bounded v)
+            | let v' := (eval cbv [exist_wire_digitsW' proj_word Build_bounded_word Build_bounded_word' snd fst] in (proj_word (snd v))) in
+              refine (_, Build_bounded_word v' _);
+              [ do_refine (fst v) | abstract exact (word_bounded (snd v)) ] ] in
+  do_refine v.
+Defined.
+
 Definition exist_wire_digits' (x : Specific.GF25519.wire_digits) : wire_digits_is_bounded x = true -> wire_digits.
 Proof.
   intro H; apply (exist_wire_digitsW (wire_digitsZToW x)).
@@ -410,6 +465,29 @@ Proof.
   reflexivity.
 Qed.
 
+Definition fe25519_word64ize (x : fe25519) : fe25519.
+Proof.
+  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) := x in
+          let x' : fe25519 := (x0, x1, x2, x3, x4, x5, x6, x7, x8, x9) in
+          _).
+  let lem := constr:(exist_fe25519W (fe25519W_word64ize (proj1_fe25519W x'))) in
+  let lem := (eval cbv [proj1_fe25519W x' fe25519W_word64ize proj_word exist_fe25519W Build_bounded_word Build_bounded_word'] in lem) in
+  refine (lem _);
+    change (is_bounded (fe25519WToZ (fe25519W_word64ize (proj1_fe25519W x'))) = true);
+    abstract (rewrite fe25519W_word64ize_id; apply is_bounded_proj1_fe25519).
+Defined.
+Definition wire_digits_word64ize (x : wire_digits) : wire_digits.
+Proof.
+  refine (let '(x0, x1, x2, x3, x4, x5, x6, x7) := x in
+          let x' : wire_digits := (x0, x1, x2, x3, x4, x5, x6, x7) in
+          _).
+  let lem := constr:(exist_wire_digitsW (wire_digitsW_word64ize (proj1_wire_digitsW x'))) in
+  let lem := (eval cbv [proj1_wire_digitsW x' wire_digitsW_word64ize proj_word exist_wire_digitsW Build_bounded_word Build_bounded_word'] in lem) in
+  refine (lem _);
+    change (wire_digits_is_bounded (wire_digitsWToZ (wire_digitsW_word64ize (proj1_wire_digitsW x'))) = true);
+    abstract (rewrite wire_digitsW_word64ize_id; apply is_bounded_proj1_wire_digits).
+Defined.
+
 (* END precomputation *)
 
 (* Precompute constants *)
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v
index f80bc492b..fedae291b 100644
--- a/src/Specific/GF25519Reflective.v
+++ b/src/Specific/GF25519Reflective.v
@@ -39,6 +39,9 @@ Definition rge_modulus : ExprUnOpFEToZ := Eval vm_compute in rge_modulusW.
 Definition rpack : ExprUnOpFEToWire := Eval vm_compute in rpackW.
 Definition runpack : ExprUnOpWireToFE := Eval vm_compute in runpackW.
 
+Definition rword64ize {t} (x : Expr t) : Expr t
+  := MapInterp (fun t => match t with TZ => word64ize end) x.
+
 Declare Reduction asm_interp
   := cbv beta iota delta
          [id
@@ -48,6 +51,7 @@ Declare Reduction asm_interp
             Word64.interp_op Word64.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -58,39 +62,41 @@ Ltac asm_interp
             Word64.interp_op Word64.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
+            mapf_interp_flat_type map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
+
 Definition interp_radd : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_bexpr radd.
+  := Eval asm_interp in interp_bexpr (rword64ize radd).
 (*Print interp_radd.*)
 Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
 Definition interp_rsub : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_bexpr rsub.
+  := Eval asm_interp in interp_bexpr (rword64ize rsub).
 (*Print interp_rsub.*)
 Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
 Definition interp_rmul : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_bexpr rmul.
+  := Eval asm_interp in interp_bexpr (rword64ize rmul).
 (*Print interp_rmul.*)
 Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
 Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_uexpr ropp.
+  := Eval asm_interp in interp_uexpr (rword64ize ropp).
 (*Print interp_ropp.*)
 Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
 Definition interp_rfreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_uexpr rfreeze.
+  := Eval asm_interp in interp_uexpr (rword64ize rfreeze).
 (*Print interp_rfreeze.*)
 Definition interp_rfreeze_correct : interp_rfreeze = interp_uexpr rfreeze := eq_refl.
 
 Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
-  := Eval asm_interp in interp_uexpr_FEToZ rge_modulus.
+  := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus).
 Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl.
 
 Definition interp_rpack : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
-  := Eval asm_interp in interp_uexpr_FEToWire rpack.
+  := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack).
 Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl.
 
 Definition interp_runpack : Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_uexpr_WireToFE runpack.
+  := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack).
 Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl.
 
 Local Notation binop_correct_and_bounded rop op