Ignore dynamic Fact (#3098)

When performing codgen, partial evaluation will ignore calls to
`Std.Diagnostics.Fact` when the condition is dynamic (ie: not known at
compile time). This is more permissive than the current behavior, where
any `Fact` that is not provable true at compile time triggers a failure.

Author: swernli

library/std/src/Std/Diagnostics.qs

@@ -154,17 +154,18 @@ operation CheckAllZero(qubits : Qubit[]) : Bool {
 }
 
 /// # Summary
-/// Checks whether a given condition is true, failing with a message if it is not.
+/// Checks whether a given condition is false, failing with a message if it is.
 ///
 /// # Description
-/// This function checks whether a given condition is true. If the condition is false, the operation fails with the given message,
+/// This function checks the given condition. If the condition is false, the operation fails with the given message,
 /// terminating the program.
 ///
 /// # Input
 /// ## actual
 /// The condition to check.
 /// ## message
 /// The message to use in the failure if the condition is false.
+@SimulatableIntrinsic()
 function Fact(actual : Bool, message : String) : Unit {
     if (not actual) {
         fail message;

source/compiler/qsc_partial_eval/src/lib.rs

@@ -1777,7 +1777,8 @@ impl<'a> PartialEvaluator<'a> {
             | "ApplyIdleNoise"
             | "GlobalPhase"
             | "Message"
-            | "PostSelectZ" => Ok(Value::unit()),
+            | "PostSelectZ"
+            | "Fact" => Ok(Value::unit()),
             "CheckZero" => Err(Error::UnsupportedSimulationIntrinsic(
                 "CheckZero".to_string(),
                 callee_expr_span,

source/compiler/qsc_partial_eval/src/tests/debug_metadata.rs

@@ -58,10 +58,10 @@ fn one_gate() {
 
             dbg_scopes:
                 0 = SubProgram name=Main location=(2-40)
-                1 = SubProgram name=H location=(1-111218)
+                1 = SubProgram name=H location=(1-111225)
             dbg_locations:
                 [1]: scope=0 location=(2-99)
-                [2]: scope=1 location=(1-111290) inlined_at=1"#]],
+                [2]: scope=1 location=(1-111297) inlined_at=1"#]],
     );
 }
 
@@ -93,15 +93,15 @@ fn one_measurement() {
 
             dbg_scopes:
                 0 = SubProgram name=Main location=(2-40)
-                1 = SubProgram name=H location=(1-111218)
-                2 = SubProgram name=M location=(1-112927)
-                3 = SubProgram name=Measure location=(1-113843)
+                1 = SubProgram name=H location=(1-111225)
+                2 = SubProgram name=M location=(1-112934)
+                3 = SubProgram name=Measure location=(1-113850)
             dbg_locations:
                 [1]: scope=0 location=(2-103)
-                [2]: scope=1 location=(1-111290) inlined_at=1
+                [2]: scope=1 location=(1-111297) inlined_at=1
                 [3]: scope=0 location=(2-126)
-                [4]: scope=2 location=(1-112969) inlined_at=3
-                [6]: scope=3 location=(1-114156) inlined_at=4"#]],
+                [4]: scope=2 location=(1-112976) inlined_at=3
+                [6]: scope=3 location=(1-114163) inlined_at=4"#]],
     );
 }
 
@@ -136,14 +136,14 @@ fn calls_to_other_callables() {
             dbg_scopes:
                 0 = SubProgram name=Main location=(2-40)
                 1 = SubProgram name=Foo location=(2-138)
-                2 = SubProgram name=H location=(1-111218)
-                3 = SubProgram name=MResetZ location=(1-182267)
+                2 = SubProgram name=H location=(1-111225)
+                3 = SubProgram name=MResetZ location=(1-182274)
             dbg_locations:
                 [1]: scope=0 location=(2-99)
                 [2]: scope=1 location=(2-179) inlined_at=1
-                [3]: scope=2 location=(1-111290) inlined_at=2
+                [3]: scope=2 location=(1-111297) inlined_at=2
                 [4]: scope=0 location=(2-115)
-                [5]: scope=3 location=(1-182316) inlined_at=4"#]],
+                [5]: scope=3 location=(1-182323) inlined_at=4"#]],
     );
 }
 
@@ -189,27 +189,27 @@ fn classical_for_loop() {
                 0 = SubProgram name=Main location=(2-40)
                 1 = LexicalBlockFile location=(2-99) discriminator=1
                 2 = SubProgram name=Foo location=(2-156)
-                3 = SubProgram name=X location=(1-134016)
-                4 = SubProgram name=Y location=(1-135238)
+                3 = SubProgram name=X location=(1-134023)
+                4 = SubProgram name=Y location=(1-135245)
                 5 = LexicalBlockFile location=(2-99) discriminator=2
                 6 = LexicalBlockFile location=(2-99) discriminator=3
             dbg_locations:
                 [1]: scope=0 location=(2-99)
                 [2]: scope=1 location=(2-127) inlined_at=1
                 [3]: scope=2 location=(2-197) inlined_at=2
-                [4]: scope=3 location=(1-134088) inlined_at=3
+                [4]: scope=3 location=(1-134095) inlined_at=3
                 [5]: scope=2 location=(2-211) inlined_at=2
-                [6]: scope=4 location=(1-135310) inlined_at=5
+                [6]: scope=4 location=(1-135317) inlined_at=5
                 [7]: scope=5 location=(2-127) inlined_at=1
                 [8]: scope=2 location=(2-197) inlined_at=7
-                [9]: scope=3 location=(1-134088) inlined_at=8
+                [9]: scope=3 location=(1-134095) inlined_at=8
                 [10]: scope=2 location=(2-211) inlined_at=7
-                [11]: scope=4 location=(1-135310) inlined_at=10
+                [11]: scope=4 location=(1-135317) inlined_at=10
                 [12]: scope=6 location=(2-127) inlined_at=1
                 [13]: scope=2 location=(2-197) inlined_at=12
-                [14]: scope=3 location=(1-134088) inlined_at=13
+                [14]: scope=3 location=(1-134095) inlined_at=13
                 [15]: scope=2 location=(2-211) inlined_at=12
-                [16]: scope=4 location=(1-135310) inlined_at=15"#]],
+                [16]: scope=4 location=(1-135317) inlined_at=15"#]],
     );
 }
 
@@ -280,7 +280,7 @@ fn nested_classical_for_loop() {
                 5 = LexicalBlockFile location=(2-101) discriminator=1
                 6 = LexicalBlockFile location=(2-129) discriminator=1
                 7 = SubProgram name=Foo location=(2-208)
-                8 = SubProgram name=X location=(1-134016)
+                8 = SubProgram name=X location=(1-134023)
                 9 = LexicalBlockFile location=(2-129) discriminator=2
                 10 = LexicalBlockFile location=(2-129) discriminator=3
                 11 = LexicalBlockFile location=(2-101) discriminator=2
@@ -290,33 +290,33 @@ fn nested_classical_for_loop() {
                 [6]: scope=5 location=(2-129) inlined_at=5
                 [7]: scope=6 location=(2-161) inlined_at=6
                 [8]: scope=7 location=(2-249) inlined_at=7
-                [9]: scope=8 location=(1-134088) inlined_at=8
+                [9]: scope=8 location=(1-134095) inlined_at=8
                 [10]: scope=9 location=(2-161) inlined_at=6
                 [11]: scope=7 location=(2-249) inlined_at=10
-                [12]: scope=8 location=(1-134088) inlined_at=11
+                [12]: scope=8 location=(1-134095) inlined_at=11
                 [13]: scope=10 location=(2-161) inlined_at=6
                 [14]: scope=7 location=(2-249) inlined_at=13
-                [15]: scope=8 location=(1-134088) inlined_at=14
+                [15]: scope=8 location=(1-134095) inlined_at=14
                 [16]: scope=11 location=(2-129) inlined_at=5
                 [17]: scope=6 location=(2-161) inlined_at=16
                 [18]: scope=7 location=(2-249) inlined_at=17
-                [19]: scope=8 location=(1-134088) inlined_at=18
+                [19]: scope=8 location=(1-134095) inlined_at=18
                 [20]: scope=9 location=(2-161) inlined_at=16
                 [21]: scope=7 location=(2-249) inlined_at=20
-                [22]: scope=8 location=(1-134088) inlined_at=21
+                [22]: scope=8 location=(1-134095) inlined_at=21
                 [23]: scope=10 location=(2-161) inlined_at=16
                 [24]: scope=7 location=(2-249) inlined_at=23
-                [25]: scope=8 location=(1-134088) inlined_at=24
+                [25]: scope=8 location=(1-134095) inlined_at=24
                 [26]: scope=12 location=(2-129) inlined_at=5
                 [27]: scope=6 location=(2-161) inlined_at=26
                 [28]: scope=7 location=(2-249) inlined_at=27
-                [29]: scope=8 location=(1-134088) inlined_at=28
+                [29]: scope=8 location=(1-134095) inlined_at=28
                 [30]: scope=9 location=(2-161) inlined_at=26
                 [31]: scope=7 location=(2-249) inlined_at=30
-                [32]: scope=8 location=(1-134088) inlined_at=31
+                [32]: scope=8 location=(1-134095) inlined_at=31
                 [33]: scope=10 location=(2-161) inlined_at=26
                 [34]: scope=7 location=(2-249) inlined_at=33
-                [35]: scope=8 location=(1-134088) inlined_at=34"#]],
+                [35]: scope=8 location=(1-134095) inlined_at=34"#]],
     );
 }
 
@@ -345,11 +345,11 @@ fn lambda() {
             dbg_scopes:
                 0 = SubProgram name=Main location=(2-1)
                 1 = SubProgram name=<lambda> location=(2-65)
-                2 = SubProgram name=H location=(1-111218)
+                2 = SubProgram name=H location=(1-111225)
             dbg_locations:
                 [1]: scope=0 location=(2-99)
                 [2]: scope=1 location=(2-82) inlined_at=1
-                [3]: scope=2 location=(1-111290) inlined_at=2"#]],
+                [3]: scope=2 location=(1-111297) inlined_at=2"#]],
     );
 }
 
@@ -392,22 +392,22 @@ fn result_comparison_to_literal() {
 
             dbg_scopes:
                 0 = SubProgram name=Main location=(2-22)
-                1 = SubProgram name=H location=(1-111218)
-                2 = SubProgram name=M location=(1-112927)
-                3 = SubProgram name=Measure location=(1-113843)
-                4 = SubProgram name=X location=(1-134016)
-                5 = SubProgram name=Reset location=(1-117316)
+                1 = SubProgram name=H location=(1-111225)
+                2 = SubProgram name=M location=(1-112934)
+                3 = SubProgram name=Measure location=(1-113850)
+                4 = SubProgram name=X location=(1-134023)
+                5 = SubProgram name=Reset location=(1-117323)
             dbg_locations:
                 [1]: scope=0 location=(2-86)
-                [2]: scope=1 location=(1-111290) inlined_at=1
+                [2]: scope=1 location=(1-111297) inlined_at=1
                 [3]: scope=0 location=(2-110)
-                [4]: scope=2 location=(1-112969) inlined_at=3
-                [6]: scope=3 location=(1-114156) inlined_at=4
+                [4]: scope=2 location=(1-112976) inlined_at=3
+                [6]: scope=3 location=(1-114163) inlined_at=4
                 [8]: scope=0 location=(2-154)
-                [9]: scope=4 location=(1-134088) inlined_at=8
+                [9]: scope=4 location=(1-134095) inlined_at=8
                 [10]: scope=0 location=(2-125)
                 [11]: scope=0 location=(2-179)
-                [12]: scope=5 location=(1-117360) inlined_at=11"#]],
+                [12]: scope=5 location=(1-117367) inlined_at=11"#]],
     );
 }
 
@@ -457,25 +457,25 @@ fn if_else() {
 
             dbg_scopes:
                 0 = SubProgram name=Main location=(2-22)
-                1 = SubProgram name=H location=(1-111218)
-                2 = SubProgram name=M location=(1-112927)
-                3 = SubProgram name=Measure location=(1-113843)
-                4 = SubProgram name=X location=(1-134016)
-                5 = SubProgram name=Y location=(1-135238)
+                1 = SubProgram name=H location=(1-111225)
+                2 = SubProgram name=M location=(1-112934)
+                3 = SubProgram name=Measure location=(1-113850)
+                4 = SubProgram name=X location=(1-134023)
+                5 = SubProgram name=Y location=(1-135245)
             dbg_locations:
                 [2]: scope=0 location=(2-112)
-                [3]: scope=1 location=(1-111290) inlined_at=2
+                [3]: scope=1 location=(1-111297) inlined_at=2
                 [4]: scope=0 location=(2-135)
-                [5]: scope=2 location=(1-112969) inlined_at=4
-                [7]: scope=3 location=(1-114156) inlined_at=5
+                [5]: scope=2 location=(1-112976) inlined_at=4
+                [7]: scope=3 location=(1-114163) inlined_at=5
                 [9]: scope=0 location=(2-176)
-                [10]: scope=4 location=(1-134088) inlined_at=9
+                [10]: scope=4 location=(1-134095) inlined_at=9
                 [11]: scope=0 location=(2-212)
-                [12]: scope=5 location=(1-135310) inlined_at=11
+                [12]: scope=5 location=(1-135317) inlined_at=11
                 [13]: scope=0 location=(2-150)
                 [14]: scope=0 location=(2-246)
-                [15]: scope=2 location=(1-112969) inlined_at=14
-                [17]: scope=3 location=(1-114156) inlined_at=15"#]],
+                [15]: scope=2 location=(1-112976) inlined_at=14
+                [17]: scope=3 location=(1-114163) inlined_at=15"#]],
     );
 }
 
@@ -517,20 +517,20 @@ fn branch_due_to_binop_short_circuit() {
 
             dbg_scopes:
                 0 = SubProgram name=Main location=(2-1)
-                1 = SubProgram name=H location=(1-111218)
-                2 = SubProgram name=M location=(1-112927)
-                3 = SubProgram name=Measure location=(1-113843)
+                1 = SubProgram name=H location=(1-111225)
+                2 = SubProgram name=M location=(1-112934)
+                3 = SubProgram name=Measure location=(1-113850)
             dbg_locations:
                 [2]: scope=0 location=(2-75)
-                [3]: scope=1 location=(1-111290) inlined_at=2
+                [3]: scope=1 location=(1-111297) inlined_at=2
                 [4]: scope=0 location=(2-86)
-                [5]: scope=1 location=(1-111290) inlined_at=4
+                [5]: scope=1 location=(1-111297) inlined_at=4
                 [6]: scope=0 location=(2-107)
-                [7]: scope=2 location=(1-112969) inlined_at=6
-                [9]: scope=3 location=(1-114156) inlined_at=7
+                [7]: scope=2 location=(1-112976) inlined_at=6
+                [9]: scope=3 location=(1-114163) inlined_at=7
                 [11]: scope=0 location=(2-129)
-                [12]: scope=2 location=(1-112969) inlined_at=11
-                [14]: scope=3 location=(1-114156) inlined_at=12
+                [12]: scope=2 location=(1-112976) inlined_at=11
+                [14]: scope=3 location=(1-114163) inlined_at=12
                 [16]: scope=0 location=(2-127)"#]],
     );
 }

source/compiler/qsc_partial_eval/src/tests/misc.rs

@@ -800,3 +800,54 @@ fn double_to_integer_conversion() {
                 Jump(1)"#]],
     );
 }
+
+#[test]
+fn dynamic_fact_call_ignored() {
+    let program = get_rir_program(indoc! {
+        r#"
+        namespace Test {
+            @EntryPoint()
+            operation Main() : Bool {
+                use q = Qubit();
+                let b = M(q) == One;
+                Std.Diagnostics.Fact(not b, "measurement should always be zero");
+                b
+            }
+        }
+        "#,
+    });
+
+    assert_blocks(
+        &program,
+        &expect![[r#"
+            Blocks:
+            Block 0:Block:
+                Call id(1), args( Pointer, )
+                Call id(2), args( Qubit(0), Result(0), )
+                Variable(0, Boolean) = Call id(3), args( Result(0), )
+                Variable(1, Boolean) = Store Variable(0, Boolean)
+                Variable(2, Boolean) = Store Variable(1, Boolean)
+                Variable(3, Boolean) = LogicalNot Variable(2, Boolean)
+                Variable(4, Boolean) = Store Variable(2, Boolean)
+                Call id(4), args( Variable(4, Boolean), Tag(0, 3), )
+                Return"#]],
+    );
+}
+
+#[test]
+fn static_fact_call_evaluated() {
+    let error = get_partial_evaluation_error(indoc! {
+        r#"
+        namespace Test {
+            @EntryPoint()
+            operation Main() : Unit {
+                Std.Diagnostics.Fact(false, "this should always fail");
+            }
+        }
+        "#,
+    });
+    // Note that we don't use `assert_error` with an `expect!` here because it includes
+    // a `PackageSpan` in the error message which is points to the stdlib and can be noisy when
+    // libraries are updated.
+    assert!(format!("{error:?}").contains("this should always fail"));
+}