diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-14 21:46:40 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-14 21:46:40 -0500 |
| commit | 43c5265c24bd1df125f8de00d1f89379a920659a (patch) | |
| tree | fdb435c27c7fa1fdc22c9ca8cf107e52dc094a5c /src/Specific/GF25519Reflective.v | |
| parent | 4faedd36b571f6c07eab1e348d1df655e1123eda (diff) | |
Support for 128-bit words
I haven't found a good way to genericize the proofs of relatedness
things, mostly because Modules and functors are annoying.
Diffstat (limited to 'src/Specific/GF25519Reflective.v')
| -rw-r--r-- | src/Specific/GF25519Reflective.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v index 5e306d61d..a7ca684fb 100644 --- a/src/Specific/GF25519Reflective.v +++ b/src/Specific/GF25519Reflective.v @@ -10,9 +10,9 @@ Require Import Crypto.Specific.GF25519BoundedCommon. Require Import Crypto.Reflection.Reify. Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.MapInterp. -Require Import Crypto.Reflection.Z.Interpretations. -Require Crypto.Reflection.Z.Interpretations.Relations. -Require Import Crypto.Reflection.Z.Interpretations.RelationsCombinations. +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. @@ -50,10 +50,10 @@ Declare Reduction asm_interp interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE radd rsub rmul ropp rprefreeze rge_modulus rpack runpack curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW - Word64.interp_op Word64.interp_base_type + 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 map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type map_interp WordW.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 @@ -61,10 +61,10 @@ Ltac asm_interp interp_bexpr interp_uexpr interp_uexpr_FEToWire interp_uexpr_FEToZ interp_uexpr_WireToFE radd rsub rmul ropp rprefreeze rge_modulus rpack runpack curry_binop_fe25519W curry_unop_fe25519W curry_unop_wire_digitsW - Word64.interp_op Word64.interp_base_type + 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 map_interp Word64.interp_base_type MapInterp mapf_interp word64ize rword64ize + mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize Interp interp interp_flat_type interpf interp_flat_type fst snd]. |