microsoft/qdk
Publicmirrored fromhttps://github.com/microsoft/qdkAvailable
library/fixed_point/src/Facts.qs
65lines · modecode
| 1 | // Copyright (c) Microsoft Corporation. All rights reserved. |
| 2 | // Licensed under the MIT License. |
| 3 | |
| 4 | import Types.FixedPoint; |
| 5 | import Std.Diagnostics.Fact; |
| 6 | import Std.Arrays.IsEmpty, Std.Arrays.Rest, Std.Arrays.Unzipped; |
| 7 | |
| 8 | /// # Summary |
| 9 | /// Asserts that a quantum fixed-point number is |
| 10 | /// initialized to zero. |
| 11 | /// |
| 12 | /// # Description |
| 13 | /// This assertion succeeds when all qubits are in state $\ket{0}$, |
| 14 | /// representing that the register encodes the fixed-point number $0.0$. |
| 15 | @Config(Unrestricted) |
| 16 | operation AssertAllZeroFxP(fp : FixedPoint) : Unit { |
| 17 | import Std.Diagnostics.CheckAllZero; |
| 18 | Fact(CheckAllZero(fp::Register), "Quantum fixed-point number was not zero."); |
| 19 | } |
| 20 | |
| 21 | /// # Summary |
| 22 | /// Assert that all fixed-point numbers in the provided array |
| 23 | /// have identical point positions and qubit numbers. |
| 24 | /// |
| 25 | /// # Input |
| 26 | /// ## fixedPoints |
| 27 | /// Array of quantum fixed-point numbers that will be checked for |
| 28 | /// compatibility (using assertions). |
| 29 | function AssertFormatsAreIdenticalFxP(fixedPoints : FixedPoint[]) : Unit { |
| 30 | |
| 31 | if IsEmpty(fixedPoints) { |
| 32 | return (); |
| 33 | } |
| 34 | let (position, register) = fixedPoints[0]!; |
| 35 | Fact(position > 0, "Point position must be greater than zero."); |
| 36 | let n = Length(register); |
| 37 | for fp in Rest(fixedPoints) { |
| 38 | Fact(fp::IntegerBits == position, "FixedPoint numbers must have identical binary point position."); |
| 39 | Fact(Length(fp::Register) == n, "FixedPoint numbers must have identical number of qubits."); |
| 40 | } |
| 41 | } |
| 42 | |
| 43 | /// # Summary |
| 44 | /// Assert that all fixed-point numbers in the provided array |
| 45 | /// have identical point positions when counting from the least- |
| 46 | /// significant bit. I.e., number of bits minus point position must |
| 47 | /// be constant for all fixed-point numbers in the array. |
| 48 | /// |
| 49 | /// # Input |
| 50 | /// ## fixedPoints |
| 51 | /// Array of quantum fixed-point numbers that will be checked for |
| 52 | /// compatibility (using assertions). |
| 53 | function AssertPointPositionsIdenticalFxP(fixedPoints : FixedPoint[]) : Unit { |
| 54 | if IsEmpty(fixedPoints) { |
| 55 | return (); |
| 56 | } |
| 57 | let (position, register) = fixedPoints[0]!; |
| 58 | Fact(position > 0, "Point position must be greater than zero."); |
| 59 | let n = Length(register); |
| 60 | for fp in Rest(fixedPoints) { |
| 61 | Fact((Length(fp::Register) - fp::IntegerBits) == (n - position), "FixedPoint numbers must have identical point alignment."); |
| 62 | } |
| 63 | } |
| 64 | |
| 65 | export AssertAllZeroFxP, AssertFormatsAreIdenticalFxP, AssertPointPositionsIdenticalFxP; |