diff options
Diffstat (limited to 'src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v')
| -rw-r--r-- | src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v | 77 |
1 files changed, 0 insertions, 77 deletions
diff --git a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v deleted file mode 100644 index d4a05dec1..000000000 --- a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v +++ /dev/null @@ -1,77 +0,0 @@ -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.SpecificGen.GF25519_64. -Require Import Crypto.SpecificGen.GF25519_64BoundedCommon. -Require Import Crypto.Reflection.Reify. -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Map. -Require Import Crypto.Reflection.Z.Interpretations128. -Require Crypto.Reflection.Z.Interpretations128.Relations. -Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations. -Require Import Crypto.Reflection.Z.Reify. -Require Import Crypto.Reflection.Z.Syntax. -Require Import Crypto.SpecificGen.GF25519_64Reflective.Common. -Require Import Crypto.SpecificGen.GF25519_64Reflective.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_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W - 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 word128ize - 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_fe25519_64W curry_unop_fe25519_64W curry_unop_wire_digitsW curry_9op_fe25519_64W - 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 word128ize - Interp interp interp_flat_type interpf interp_flat_type fst snd]. - -(* -Time Definition interp_radd_coordinates : SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W - -> Tuple.tuple SpecificGen.GF25519_64BoundedCommon.fe25519_64W 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. -*) |