Bedrock2 WordByWordMontgomery felem_copy_func_correct

src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v

@@ -55,6 +55,10 @@ Class word_by_word_Montgomery_ops
         (WordByWordMontgomery.square m width)
         Field.square
         list_unop_insizes list_unop_outsizes (list_unop_inlengths n);
+    felem_copy_op :
+      computed_op
+        (WordByWordMontgomery.copy m width) Field.felem_copy
+        list_unop_insizes list_unop_outsizes (list_unop_inlengths n);
     from_bytes_op :
       computed_op
         (WordByWordMontgomery.from_bytes m width)
@@ -165,13 +169,14 @@ Section WordByWordMontgomery.
           (to_mont : string)
           (ops : word_by_word_Montgomery_ops n m)
           mul_func add_func sub_func opp_func square_func
-          from_bytes_func to_bytes_func
+          felem_copy_func from_bytes_func to_bytes_func
           from_mont_func to_mont_func select_znz_func
           (mul_func_eq : mul_func = b2_func mul_op)
           (add_func_eq : add_func = b2_func add_op)
           (sub_func_eq : sub_func = b2_func sub_op)
           (opp_func_eq : opp_func = b2_func opp_op)
           (square_func_eq : square_func = b2_func square_op)
+          (felem_copy_func_eq : felem_copy_func = b2_func felem_copy_op)
           (from_bytes_func_eq : from_bytes_func = b2_func from_bytes_op)
           (to_bytes_func_eq : to_bytes_func = b2_func to_bytes_op)
           (from_mont_func_eq : from_mont_func = b2_func from_mont_op)
@@ -492,6 +497,41 @@ Qed.
       intros. apply Hcorrect; auto. }
   Qed.
 
+  Lemma list_Z_bounded_by_unsigned (xs : list (@Interface.word.rep _ word)) :
+    list_Z_bounded_by
+      (Primitives.saturated_bounds (List.length xs) width)
+      (map Interface.word.unsigned xs).
+  Proof using parameters_sentinel ok.
+    induction xs; cbn; [reflexivity|].
+    eapply list_Z_bounded_by_cons; split; [|assumption].
+    eapply Bool.andb_true_iff; split; eapply Z.leb_le;
+    cbv [Primitives.word_bound]; cbn.
+    { eapply Properties.word.unsigned_range. }
+    { eapply Le.Z.le_sub_1_iff, Properties.word.unsigned_range. }
+  Qed.
+
+  Lemma felem_copy_func_correct :
+    valid_func (res felem_copy_op _) ->
+    forall functions,
+      Interface.map.get functions Field.felem_copy = Some felem_copy_func ->
+      (@spec_of_felem_copy _ _ _ _ _ _ _ field_representation_raw) functions.
+  Proof using M_eq check_args_ok felem_copy_func_eq ok.
+    cbv [spec_of_felem_copy]. rewrite felem_copy_func_eq. intros.
+    pose proof copy_correct
+         _ _ _ ltac:(eassumption) _ (res_eq felem_copy_op)
+      as Hcorrect.
+
+    eapply felem_copy_correct; [ .. | eassumption | eassumption ];
+      repeat handle_side_conditions; [ | ]; intros.
+    { (* output *value* is correct *)
+      unshelve erewrite (proj1 (Hcorrect _ _)); cycle 1.
+      { rewrite map_map, List.map_ext_id; trivial; intros.
+        rewrite ?Word.Interface.word.of_Z_unsigned; trivial. }
+      { rewrite <- H2. exact (list_Z_bounded_by_unsigned x0). } }
+    { (* output *bounds* are correct *)
+      intros. apply Hcorrect; auto. }
+    Qed.
+
   Lemma from_bytes_func_correct :
     valid_func (res from_bytes_op _) ->
     forall functions,