Require Import Crypto.BaseSystem.
Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
Require Import Crypto.ModularArithmetic.ModularBaseSystem.
Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs.
Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt.
Require Export Crypto.Specific.GF25519.
Require Import Crypto.Specific.GF25519BoundedCommon.
Require Import Crypto.Reflection.Reify.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Map.
Require Import Crypto.Reflection.Z.Interpretations64.
Require Crypto.Reflection.Z.Interpretations64.Relations.
Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
Require Import Crypto.Reflection.Z.Reify.
Require Import Crypto.Reflection.Z.Syntax.
Require Import Crypto.Specific.GF25519Reflective.Common.
Require Import Crypto.Specific.GF25519Reflective.Reified.AddCoordinates.
Require Import Bedrock.Word Crypto.Util.WordUtil.
Require Import Coq.Lists.List Crypto.Util.ListUtil.
Require Import Crypto.Tactics.VerdiTactics.
Require Import Crypto.Util.ZUtil.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Bool.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Algebra.
Import ListNotations.
Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
Local Open Scope Z.

Time Definition radd_coordinates : Expr _ := Eval vm_compute in radd_coordinatesW.

Declare Reduction asm_interp_add_coordinates
  := cbv beta iota delta
         [id
            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
            radd_coordinates
            curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W
            WordW.interp_op WordW.interp_base_type
            Z.interp_op Z.interp_base_type
            Z.Syntax.interp_op Z.Syntax.interp_base_type
            mapf_interp_flat_type WordW.interp_base_type word64ize
            Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
Ltac asm_interp_add_coordinates
  := cbv beta iota delta
         [id
            interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE interp_9_4expr
            radd_coordinates
            curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW curry_9op_fe25519W
            WordW.interp_op WordW.interp_base_type
            Z.interp_op Z.interp_base_type
            Z.Syntax.interp_op Z.Syntax.interp_base_type
            mapf_interp_flat_type WordW.interp_base_type word64ize
            Interp interp interp_flat_type interpf interp_flat_type fst snd].

(*
Time Definition interp_radd_coordinates : Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Specific.GF25519BoundedCommon.fe25519W
                                          -> Tuple.tuple Specific.GF25519BoundedCommon.fe25519W 4
  := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates.
(*Print interp_radd_coordinates.*)
Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.

Lemma radd_coordinates_correct_and_bounded : op9_4_correct_and_bounded radd_coordinates add_coordinates.
Proof. exact_no_check radd_coordinatesW_correct_and_bounded. Time Qed.
*)