diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-10-21 18:47:26 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-10-22 00:10:53 -0400 |
| commit | 31d24dcb9e53cd21d619d403de8933b8fc451ed8 (patch) | |
| tree | e40c363a60cd861847f686535af6bd8801fff62d /src/Specific/GF25519.v | |
| parent | 1ec6ade7fa92912adffdb815eef5f6cac31ab078 (diff) | |
Modified [freeze] to be more reifyable
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 1ded72383..283f79974 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -129,7 +129,7 @@ Definition zero_subst : zero = zero_ := eq_refl zero_. Definition modulus_digits_ := Eval compute in ModularBaseSystemList.modulus_digits. Definition modulus_digits_subst : ModularBaseSystemList.modulus_digits = modulus_digits_ := eq_refl modulus_digits_. -Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb andb. +Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Z.lor Let_In Z.eqb Z.ltb Z.leb ModularBaseSystemList.neg. Definition app_7 {T} (f : wire_digits) (P : wire_digits -> T) : T. Proof. @@ -460,8 +460,9 @@ Proof. + reflexivity. Qed. +(* Definition ge_modulus_sig (f : fe25519) : - { b : bool | b = ge_modulus_opt (to_list 10 f) }. + { b : Z | b = ge_modulus_opt (to_list 10 f) }. Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -471,7 +472,7 @@ Proof. reflexivity. Defined. -Definition ge_modulus (f : fe25519) : bool := +Definition ge_modulus (f : fe25519) : Z := Eval cbv beta iota delta [proj1_sig ge_modulus_sig] in let '(f0, f1, f2, f3, f4, f5, f6, f7, f8, f9) := f in proj1_sig (ge_modulus_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). @@ -484,9 +485,10 @@ Proof. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. assumption. Defined. +*) Definition freeze_sig (f : fe25519) : - { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt c_ (to_list 10 f)) }. + { f' : fe25519 | f' = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)) }. Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -509,7 +511,7 @@ Definition freeze (f : fe25519) : fe25519 := proj1_sig (freeze_sig (f0, f1, f2, f3, f4, f5, f6, f7, f8, f9)). Definition freeze_correct (f : fe25519) - : freeze f = from_list_default 0 10 (freeze_opt c_ (to_list 10 f)). + : freeze f = from_list_default 0 10 (freeze_opt (int_width := int_width) c_ (to_list 10 f)). Proof. pose proof (proj2_sig (freeze_sig f)). cbv [fe25519] in *. |