diff options
Diffstat (limited to 'src/Specific/NISTP256')
5 files changed, 26 insertions, 34 deletions
diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log index 3c47f3fc9..1dc1b7ba3 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256Display.log @@ -104,12 +104,11 @@ Interp-η uint64_t x308, uint8_t x309 = subborrow_u64(x306, x295, 0xffffffff); uint64_t x311, uint8_t x312 = subborrow_u64(x309, x298, 0x0); uint64_t x314, uint8_t x315 = subborrow_u64(x312, x301, 0xffffffff00000001L); - ℤ x316 = Op (Syntax.Opp (Syntax.TWord 3) Syntax.TZ) (Return x315); - uint64_t _, ℤ x319 = addcarryx_u64ℤ(0x0, x316, x303); - uint64_t x320 = x319 == 0 ? x314 : x301; - uint64_t x321 = x319 == 0 ? x311 : x298; - uint64_t x322 = x319 == 0 ? x308 : x295; - uint64_t x323 = x319 == 0 ? x305 : x292; - return (x320, x321, x322, x323)) + uint64_t _, uint8_t x318 = subborrow_u64(x315, x303, 0x0); + uint64_t x319 = x318 == 0 ? x314 : x301; + uint64_t x320 = x318 == 0 ? x311 : x298; + uint64_t x321 = x318 == 0 ? x308 : x295; + uint64_t x322 = x318 == 0 ? x305 : x292; + return (x319, x320, x321, x322)) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log index 0f46e27f6..e6498cf83 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_AddDisplay.log @@ -10,12 +10,11 @@ Interp-η uint64_t x32, uint8_t x33 = subborrow_u64(x30, x20, 0xffffffff); uint64_t x35, uint8_t x36 = subborrow_u64(x33, x23, 0x0); uint64_t x38, uint8_t x39 = subborrow_u64(x36, x26, 0xffffffff00000001L); - ℤ x40 = Op (Syntax.Opp (Syntax.TWord 3) Syntax.TZ) (Return x39); - uint64_t _, ℤ x43 = addcarryx_u64ℤ(0x0, x40, x27); - uint64_t x44 = x43 == 0 ? x38 : x26; - uint64_t x45 = x43 == 0 ? x35 : x23; - uint64_t x46 = x43 == 0 ? x32 : x20; - uint64_t x47 = x43 == 0 ? x29 : x17; - return (x44, x45, x46, x47)) + uint64_t _, uint8_t x42 = subborrow_u64(x39, x27, 0x0); + uint64_t x43 = x42 == 0 ? x38 : x26; + uint64_t x44 = x42 == 0 ? x35 : x23; + uint64_t x45 = x42 == 0 ? x32 : x20; + uint64_t x46 = x42 == 0 ? x29 : x17; + return (x43, x44, x45, x46)) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log index 0b94a81ce..b76a34a56 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_OppDisplay.log @@ -8,15 +8,12 @@ Interp-η uint64_t x17, uint8_t x18 = subborrow_u64(x15, 0x0, x5); uint64_t x19 = (uint64_t) (x18 == 0 ? 0x0 : 0xffffffffffffffffL); uint64_t x20 = x19 & 0xffffffffffffffffL; - uint64_t x22, uint8_t x23 = addcarryx_u64(0x0, x8, x20); + uint64_t x22, uint8_t x23 = subborrow_u64(0x0, x8, x20); uint64_t x24 = x19 & 0xffffffff; - uint64_t x26, uint8_t x27 = addcarryx_u64(x23, x11, x24); - uint64_t x29, uint8_t x30 = addcarryx_u64(x27, x14, 0x0); + uint64_t x26, uint8_t x27 = subborrow_u64(x23, x11, x24); + uint64_t x29, uint8_t x30 = subborrow_u64(x27, x14, 0x0); uint64_t x31 = x19 & 0xffffffff00000001L; - uint128_t x32 = 0x10000000000000000L * x18; - ℤ x33 = Op (Syntax.Opp (Syntax.TWord 7) Syntax.TZ) (Return x32); - uint64_t x35, ℤ _ = addcarryx_u64ℤ(x17, x33, x31); - uint64_t x38, uint8_t _ = addcarryx_u64(0x0, x30, x35); - (Return x38, Return x29, Return x26, Return x22)) + uint64_t x33, uint8_t _ = subborrow_u64(x30, x17, x31); + (Return x33, Return x29, Return x26, Return x22)) x : word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log index 9b301c678..de068350b 100644 --- a/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log +++ b/src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256_SubDisplay.log @@ -8,15 +8,12 @@ Interp-η uint64_t x26, uint8_t x27 = subborrow_u64(x24, x8, x14); uint64_t x28 = (uint64_t) (x27 == 0 ? 0x0 : 0xffffffffffffffffL); uint64_t x29 = x28 & 0xffffffffffffffffL; - uint64_t x31, uint8_t x32 = addcarryx_u64(0x0, x17, x29); + uint64_t x31, uint8_t x32 = subborrow_u64(0x0, x17, x29); uint64_t x33 = x28 & 0xffffffff; - uint64_t x35, uint8_t x36 = addcarryx_u64(x32, x20, x33); - uint64_t x38, uint8_t x39 = addcarryx_u64(x36, x23, 0x0); + uint64_t x35, uint8_t x36 = subborrow_u64(x32, x20, x33); + uint64_t x38, uint8_t x39 = subborrow_u64(x36, x23, 0x0); uint64_t x40 = x28 & 0xffffffff00000001L; - uint128_t x41 = 0x10000000000000000L * x27; - ℤ x42 = Op (Syntax.Opp (Syntax.TWord 7) Syntax.TZ) (Return x41); - uint64_t x44, ℤ _ = addcarryx_u64ℤ(x26, x42, x40); - uint64_t x47, uint8_t _ = addcarryx_u64(0x0, x39, x44); - (Return x47, Return x38, Return x35, Return x31)) + uint64_t x42, uint8_t _ = subborrow_u64(x39, x26, x40); + (Return x42, Return x38, Return x35, Return x31)) (x, x0)%core : word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v index d90a63bfb..ae5a3cb43 100644 --- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v +++ b/src/Specific/NISTP256/AMD64/MontgomeryP256.v @@ -34,7 +34,7 @@ Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. (* cbv [ r wt sz p256 @@ -139,7 +139,7 @@ Definition add' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. @@ -150,7 +150,7 @@ Definition sub' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. @@ -161,7 +161,7 @@ Definition opp' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz }. Proof. eapply (lift1_sig (fun A c => c = _)); eexists. - cbv -[Definitions.Z.add_get_carry Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. reflexivity. Defined. |