From b38a703308a2030393ca23631461628b8caf4195 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 19 Jun 2017 17:59:31 -0400 Subject: No small in MP256 spec (wrong place), s/native/vm/ The native compiler was giving anomalies on travis. --- src/Specific/MontgomeryP256.v | 11 +++++------ src/Specific/MontgomeryP256_128.v | 11 +++++------ 2 files changed, 10 insertions(+), 12 deletions(-) (limited to 'src/Specific') diff --git a/src/Specific/MontgomeryP256.v b/src/Specific/MontgomeryP256.v index ad37ed02b..bdbcd6fd7 100644 --- a/src/Specific/MontgomeryP256.v +++ b/src/Specific/MontgomeryP256.v @@ -16,7 +16,7 @@ Definition m : positive := 2^256-2^224+2^192+2^96-1. Definition p256 := Eval vm_compute in ((Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m))). -Definition r' := Eval native_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m). +Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m). Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z. Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)). Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z. @@ -135,17 +135,16 @@ Definition montgomery_to_F (v : Z) : F m Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz | forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A) (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B), - Saturated.small (Z.pos r) (f A B) - /\ (let eval := Saturated.eval (Z.pos r) in - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) }. + let eval := Saturated.eval (Z.pos r) in + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }. Proof. exists (proj1_sig mulmod_256''). abstract ( intros A Asm B Bsm; pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H; cbv zeta in *; - split; try solve [ destruct_head'_and; assumption ]; + (*split; try solve [ destruct_head'_and; assumption ];*) rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H; unfold montgomery_to_F; destruct H as [H1 [H2 H3]]; diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v index 71df829e6..503c97572 100644 --- a/src/Specific/MontgomeryP256_128.v +++ b/src/Specific/MontgomeryP256_128.v @@ -16,7 +16,7 @@ Definition m : positive := 2^256-2^224+2^192+2^96-1. Definition p256 := Eval vm_compute in ((Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m))). -Definition r' := Eval native_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m). +Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m). Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z. Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)). Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z. @@ -144,17 +144,16 @@ Definition montgomery_to_F (v : Z) : F m Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz | forall (A : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) A) (B : Tuple.tuple Z sz) (_ : Saturated.small (Z.pos r) B), - Saturated.small (Z.pos r) (f A B) - /\ (let eval := Saturated.eval (Z.pos r) in - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) }. + let eval := Saturated.eval (Z.pos r) in + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }. Proof. exists (proj1_sig mulmod_256''). abstract ( intros A Asm B Bsm; pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H; cbv zeta in *; - split; try solve [ destruct_head'_and; assumption ]; + (*split; try solve [ destruct_head'_and; assumption ];*) rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H; unfold montgomery_to_F; destruct H as [H1 [H2 H3]]; -- cgit v1.2.3