type fiatScalarUint1 … type fiatScalarInt1 … type fiatScalarMontgomeryDomainFieldElement … type fiatScalarNonMontgomeryDomainFieldElement … // fiatScalarCmovznzU64 is a single-word conditional move. // // Postconditions: // // out1 = (if arg1 = 0 then arg2 else arg3) // // Input Bounds: // // arg1: [0x0 ~> 0x1] // arg2: [0x0 ~> 0xffffffffffffffff] // arg3: [0x0 ~> 0xffffffffffffffff] // // Output Bounds: // // out1: [0x0 ~> 0xffffffffffffffff] func fiatScalarCmovznzU64(out1 *uint64, arg1 fiatScalarUint1, arg2 uint64, arg3 uint64) { … } // fiatScalarMul multiplies two field elements in the Montgomery domain. // // Preconditions: // // 0 ≤ eval arg1 < m // 0 ≤ eval arg2 < m // // Postconditions: // // eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) * eval (from_montgomery arg2)) mod m // 0 ≤ eval out1 < m func fiatScalarMul(out1 *fiatScalarMontgomeryDomainFieldElement, arg1 *fiatScalarMontgomeryDomainFieldElement, arg2 *fiatScalarMontgomeryDomainFieldElement) { … } // fiatScalarAdd adds two field elements in the Montgomery domain. // // Preconditions: // // 0 ≤ eval arg1 < m // 0 ≤ eval arg2 < m // // Postconditions: // // eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) + eval (from_montgomery arg2)) mod m // 0 ≤ eval out1 < m func fiatScalarAdd(out1 *fiatScalarMontgomeryDomainFieldElement, arg1 *fiatScalarMontgomeryDomainFieldElement, arg2 *fiatScalarMontgomeryDomainFieldElement) { … } // fiatScalarSub subtracts two field elements in the Montgomery domain. // // Preconditions: // // 0 ≤ eval arg1 < m // 0 ≤ eval arg2 < m // // Postconditions: // // eval (from_montgomery out1) mod m = (eval (from_montgomery arg1) - eval (from_montgomery arg2)) mod m // 0 ≤ eval out1 < m func fiatScalarSub(out1 *fiatScalarMontgomeryDomainFieldElement, arg1 *fiatScalarMontgomeryDomainFieldElement, arg2 *fiatScalarMontgomeryDomainFieldElement) { … } // fiatScalarOpp negates a field element in the Montgomery domain. // // Preconditions: // // 0 ≤ eval arg1 < m // // Postconditions: // // eval (from_montgomery out1) mod m = -eval (from_montgomery arg1) mod m // 0 ≤ eval out1 < m func fiatScalarOpp(out1 *fiatScalarMontgomeryDomainFieldElement, arg1 *fiatScalarMontgomeryDomainFieldElement) { … } // fiatScalarNonzero outputs a single non-zero word if the input is non-zero and zero otherwise. // // Preconditions: // // 0 ≤ eval arg1 < m // // Postconditions: // // out1 = 0 ↔ eval (from_montgomery arg1) mod m = 0 // // Input Bounds: // // arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff]] // // Output Bounds: // // out1: [0x0 ~> 0xffffffffffffffff] func fiatScalarNonzero(out1 *uint64, arg1 *[4]uint64) { … } // fiatScalarFromMontgomery translates a field element out of the Montgomery domain. // // Preconditions: // // 0 ≤ eval arg1 < m // // Postconditions: // // eval out1 mod m = (eval arg1 * ((2^64)⁻¹ mod m)^4) mod m // 0 ≤ eval out1 < m func fiatScalarFromMontgomery(out1 *fiatScalarNonMontgomeryDomainFieldElement, arg1 *fiatScalarMontgomeryDomainFieldElement) { … } // fiatScalarToMontgomery translates a field element into the Montgomery domain. // // Preconditions: // // 0 ≤ eval arg1 < m // // Postconditions: // // eval (from_montgomery out1) mod m = eval arg1 mod m // 0 ≤ eval out1 < m func fiatScalarToMontgomery(out1 *fiatScalarMontgomeryDomainFieldElement, arg1 *fiatScalarNonMontgomeryDomainFieldElement) { … } // fiatScalarToBytes serializes a field element NOT in the Montgomery domain to bytes in little-endian order. // // Preconditions: // // 0 ≤ eval arg1 < m // // Postconditions: // // out1 = map (λ x, ⌊((eval arg1 mod m) mod 2^(8 * (x + 1))) / 2^(8 * x)⌋) [0..31] // // Input Bounds: // // arg1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1fffffffffffffff]] // // Output Bounds: // // out1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1f]] func fiatScalarToBytes(out1 *[32]uint8, arg1 *[4]uint64) { … } // fiatScalarFromBytes deserializes a field element NOT in the Montgomery domain from bytes in little-endian order. // // Preconditions: // // 0 ≤ bytes_eval arg1 < m // // Postconditions: // // eval out1 mod m = bytes_eval arg1 mod m // 0 ≤ eval out1 < m // // Input Bounds: // // arg1: [[0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0xff], [0x0 ~> 0x1f]] // // Output Bounds: // // out1: [[0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0xffffffffffffffff], [0x0 ~> 0x1fffffffffffffff]] func fiatScalarFromBytes(out1 *[4]uint64, arg1 *[32]uint8) { … }