diff options
| -rw-r--r-- | curve25519_32.c | 2 | ||||
| -rw-r--r-- | curve25519_64.c | 2 | ||||
| -rw-r--r-- | p224_32.c | 2 | ||||
| -rw-r--r-- | p224_64.c | 2 | ||||
| -rw-r--r-- | p256_32.c | 2 | ||||
| -rw-r--r-- | p256_64.c | 2 | ||||
| -rw-r--r-- | p384_32.c | 2 | ||||
| -rw-r--r-- | p384_64.c | 2 | ||||
| -rw-r--r-- | p521_32.c | 2 | ||||
| -rw-r--r-- | p521_64.c | 2 | ||||
| -rw-r--r-- | secp256k1_32.c | 2 | ||||
| -rw-r--r-- | secp256k1_64.c | 2 | ||||
| -rw-r--r-- | src/Util/ZUtil/Morphisms.v | 21 |
13 files changed, 33 insertions, 12 deletions
diff --git a/curve25519_32.c b/curve25519_32.c index 5c3add9e9..5e6ee6486 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -90,7 +90,7 @@ static void fiat_25519_subborrowx_u25(uint32_t* out1, fiat_25519_uint1* out2, fi static void fiat_25519_cmovznz_u32(uint32_t* out1, fiat_25519_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_25519_uint1 x1 = (!(!arg1)); uint32_t x2 = ((fiat_25519_int1)(0x0 - x1) & UINT32_C(0xffffffff)); - uint32_t x3 = ((x2 & arg3) | (uint32_t)((uint64_t)(~x2) & arg2)); + uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } diff --git a/curve25519_64.c b/curve25519_64.c index 899f37e40..ed90d1ce3 100644 --- a/curve25519_64.c +++ b/curve25519_64.c @@ -58,7 +58,7 @@ static void fiat_25519_subborrowx_u51(uint64_t* out1, fiat_25519_uint1* out2, fi static void fiat_25519_cmovznz_u64(uint64_t* out1, fiat_25519_uint1 arg1, uint64_t arg2, uint64_t arg3) { fiat_25519_uint1 x1 = (!(!arg1)); uint64_t x2 = ((fiat_25519_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); - uint64_t x3 = ((x2 & arg3) | (uint64_t)((fiat_25519_uint128)(~x2) & arg2)); + uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -78,7 +78,7 @@ static void fiat_p224_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, ui static void fiat_p224_cmovznz_u32(uint32_t* out1, fiat_p224_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_p224_uint1 x1 = (!(!arg1)); uint32_t x2 = ((fiat_p224_int1)(0x0 - x1) & UINT32_C(0xffffffff)); - uint32_t x3 = ((x2 & arg3) | (uint32_t)((uint64_t)(~x2) & arg2)); + uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -80,7 +80,7 @@ static void fiat_p224_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui static void fiat_p224_cmovznz_u64(uint64_t* out1, fiat_p224_uint1 arg1, uint64_t arg2, uint64_t arg3) { fiat_p224_uint1 x1 = (!(!arg1)); uint64_t x2 = ((fiat_p224_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); - uint64_t x3 = ((x2 & arg3) | (uint64_t)((fiat_p224_uint128)(~x2) & arg2)); + uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -78,7 +78,7 @@ static void fiat_p256_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, ui static void fiat_p256_cmovznz_u32(uint32_t* out1, fiat_p256_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_p256_uint1 x1 = (!(!arg1)); uint32_t x2 = ((fiat_p256_int1)(0x0 - x1) & UINT32_C(0xffffffff)); - uint32_t x3 = ((x2 & arg3) | (uint32_t)((uint64_t)(~x2) & arg2)); + uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -80,7 +80,7 @@ static void fiat_p256_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui static void fiat_p256_cmovznz_u64(uint64_t* out1, fiat_p256_uint1 arg1, uint64_t arg2, uint64_t arg3) { fiat_p256_uint1 x1 = (!(!arg1)); uint64_t x2 = ((fiat_p256_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); - uint64_t x3 = ((x2 & arg3) | (uint64_t)((fiat_p256_uint128)(~x2) & arg2)); + uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -78,7 +78,7 @@ static void fiat_p384_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg1, ui static void fiat_p384_cmovznz_u32(uint32_t* out1, fiat_p384_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_p384_uint1 x1 = (!(!arg1)); uint32_t x2 = ((fiat_p384_int1)(0x0 - x1) & UINT32_C(0xffffffff)); - uint32_t x3 = ((x2 & arg3) | (uint32_t)((uint64_t)(~x2) & arg2)); + uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -80,7 +80,7 @@ static void fiat_p384_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg1, ui static void fiat_p384_cmovznz_u64(uint64_t* out1, fiat_p384_uint1 arg1, uint64_t arg2, uint64_t arg3) { fiat_p384_uint1 x1 = (!(!arg1)); uint64_t x2 = ((fiat_p384_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); - uint64_t x3 = ((x2 & arg3) | (uint64_t)((fiat_p384_uint128)(~x2) & arg2)); + uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -92,7 +92,7 @@ static void fiat_p521_subborrowx_u31(uint32_t* out1, fiat_p521_uint1* out2, fiat static void fiat_p521_cmovznz_u32(uint32_t* out1, fiat_p521_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_p521_uint1 x1 = (!(!arg1)); uint32_t x2 = ((fiat_p521_int1)(0x0 - x1) & UINT32_C(0xffffffff)); - uint32_t x3 = ((x2 & arg3) | (uint32_t)((uint64_t)(~x2) & arg2)); + uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } @@ -92,7 +92,7 @@ static void fiat_p521_subborrowx_u57(uint64_t* out1, fiat_p521_uint1* out2, fiat static void fiat_p521_cmovznz_u64(uint64_t* out1, fiat_p521_uint1 arg1, uint64_t arg2, uint64_t arg3) { fiat_p521_uint1 x1 = (!(!arg1)); uint64_t x2 = ((fiat_p521_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); - uint64_t x3 = ((x2 & arg3) | (uint64_t)((fiat_p521_uint128)(~x2) & arg2)); + uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } diff --git a/secp256k1_32.c b/secp256k1_32.c index 0bc344bd1..fb1ce688a 100644 --- a/secp256k1_32.c +++ b/secp256k1_32.c @@ -78,7 +78,7 @@ static void fiat_secp256k1_mulx_u32(uint32_t* out1, uint32_t* out2, uint32_t arg static void fiat_secp256k1_cmovznz_u32(uint32_t* out1, fiat_secp256k1_uint1 arg1, uint32_t arg2, uint32_t arg3) { fiat_secp256k1_uint1 x1 = (!(!arg1)); uint32_t x2 = ((fiat_secp256k1_int1)(0x0 - x1) & UINT32_C(0xffffffff)); - uint32_t x3 = ((x2 & arg3) | (uint32_t)((uint64_t)(~x2) & arg2)); + uint32_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } diff --git a/secp256k1_64.c b/secp256k1_64.c index 729a8a2c2..53487afa9 100644 --- a/secp256k1_64.c +++ b/secp256k1_64.c @@ -80,7 +80,7 @@ static void fiat_secp256k1_mulx_u64(uint64_t* out1, uint64_t* out2, uint64_t arg static void fiat_secp256k1_cmovznz_u64(uint64_t* out1, fiat_secp256k1_uint1 arg1, uint64_t arg2, uint64_t arg3) { fiat_secp256k1_uint1 x1 = (!(!arg1)); uint64_t x2 = ((fiat_secp256k1_int1)(0x0 - x1) & UINT64_C(0xffffffffffffffff)); - uint64_t x3 = ((x2 & arg3) | (uint64_t)((fiat_secp256k1_uint128)(~x2) & arg2)); + uint64_t x3 = ((x2 & arg3) | ((~x2) & arg2)); *out1 = x3; } diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v index d58b89c91..731219a6a 100644 --- a/src/Util/ZUtil/Morphisms.v +++ b/src/Util/ZUtil/Morphisms.v @@ -14,45 +14,66 @@ Module Z. [Local Existing Instances]. *) Lemma succ_le_Proper : Proper (Z.le ==> Z.le) Z.succ. Proof. repeat (omega || intro). Qed. + Hint Resolve succ_le_Proper : zarith. Lemma add_le_Proper : Proper (Z.le ==> Z.le ==> Z.le) Z.add. Proof. repeat (omega || intro). Qed. + Hint Resolve add_le_Proper : zarith. Lemma add_le_Proper' x : Proper (Z.le ==> Z.le) (Z.add x). Proof. repeat (omega || intro). Qed. + Hint Resolve add_le_Proper' : zarith. Lemma sub_le_ge_Proper : Proper (Z.le ==> Z.ge ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. + Hint Resolve sub_le_ge_Proper : zarith. Lemma sub_le_flip_le_Proper : Proper (Z.le ==> Basics.flip Z.le ==> Z.le) Z.sub. Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Hint Resolve sub_le_flip_le_Proper : zarith. Lemma sub_le_eq_Proper : Proper (Z.le ==> Logic.eq ==> Z.le) Z.sub. Proof. repeat (omega || intro). Qed. + Hint Resolve sub_le_eq_Proper : zarith. Lemma mul_Zpos_le_Proper p : Proper (Z.le ==> Z.le) (Z.mul (Z.pos p)). Proof. repeat (nia || intro). Qed. + Hint Resolve mul_Zpos_le_Proper : zarith. Lemma log2_up_le_Proper : Proper (Z.le ==> Z.le) Z.log2_up. Proof. intros ???; apply Z.log2_up_le_mono; assumption. Qed. + Hint Resolve log2_up_le_Proper : zarith. Lemma log2_le_Proper : Proper (Z.le ==> Z.le) Z.log2. Proof. intros ???; apply Z.log2_le_mono; assumption. Qed. + Hint Resolve log2_le_Proper : zarith. Lemma pow_Zpos_le_Proper x : Proper (Z.le ==> Z.le) (Z.pow (Z.pos x)). Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. + Hint Resolve pow_Zpos_le_Proper : zarith. Lemma lt_le_flip_Proper_flip_impl : Proper (Z.le ==> Basics.flip Z.le ==> Basics.flip Basics.impl) Z.lt. Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Hint Resolve lt_le_flip_Proper_flip_impl : zarith. Lemma le_Proper_ge_le_flip_impl : Proper (Z.le ==> Z.ge ==> Basics.flip Basics.impl) Z.le. Proof. intros ???????; omega. Qed. + Hint Resolve le_Proper_ge_le_flip_impl : zarith. Lemma add_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le ==> Basics.flip Z.le) Z.add. Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Hint Resolve add_le_Proper_flip : zarith. Lemma sub_le_ge_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.ge ==> Basics.flip Z.le) Z.sub. Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Hint Resolve sub_le_ge_Proper_flip : zarith. Lemma sub_flip_le_le_Proper_flip : Proper (Basics.flip Z.le ==> Z.le ==> Basics.flip Z.le) Z.sub. Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Hint Resolve sub_flip_le_le_Proper_flip : zarith. Lemma sub_le_eq_Proper_flip : Proper (Basics.flip Z.le ==> Logic.eq ==> Basics.flip Z.le) Z.sub. Proof. unfold Basics.flip; repeat (omega || intro). Qed. + Hint Resolve sub_le_eq_Proper_flip : zarith. Lemma log2_up_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le) Z.log2_up. Proof. intros ???; apply Z.log2_up_le_mono; assumption. Qed. + Hint Resolve log2_up_le_Proper_flip : zarith. Lemma log2_le_Proper_flip : Proper (Basics.flip Z.le ==> Basics.flip Z.le) Z.log2. Proof. intros ???; apply Z.log2_le_mono; assumption. Qed. + Hint Resolve log2_le_Proper_flip : zarith. Lemma pow_Zpos_le_Proper_flip x : Proper (Basics.flip Z.le ==> Basics.flip Z.le) (Z.pow (Z.pos x)). Proof. intros ???; apply Z.pow_le_mono_r; try reflexivity; try assumption. Qed. + Hint Resolve pow_Zpos_le_Proper_flip : zarith. Lemma add_with_carry_le_Proper : Proper (Z.le ==> Z.le ==> Z.le ==> Z.le) Z.add_with_carry. Proof. unfold Z.add_with_carry; repeat (omega || intro). Qed. + Hint Resolve add_with_carry_le_Proper : zarith. Lemma sub_with_borrow_le_Proper : Proper (Basics.flip Z.le ==> Z.le ==> Basics.flip Z.le ==> Z.le) Z.sub_with_borrow. Proof. unfold Z.sub_with_borrow, Z.add_with_carry, Basics.flip; repeat (omega || intro). Qed. + Hint Resolve sub_with_borrow_le_Proper : zarith. End Z. |