Enable sqrt* intrinsics

Requires fixes in CBMC's sqrt* implementations.

docs/src/rust-feature-support/intrinsics.md

@@ -211,8 +211,8 @@ sinf32 | Partial | Results are overapproximated; [this test](https://github.com/
 sinf64 | Partial | Results are overapproximated; [this test](https://github.com/model-checking/kani/blob/main/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs) explains how |
 size_of | Yes | |
 size_of_val | Yes | |
-sqrtf32 | No | |
-sqrtf64 | No | |
+sqrtf32 | Partial | Results are overapproximated |
+sqrtf64 | Partial | Results are overapproximated |
 sub_with_overflow | Yes | |
 transmute | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/nomicon/transmutes.html) |
 truncf32 | Yes | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -555,8 +555,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_xor" => codegen_intrinsic_binop!(bitxor),
             "size_of" => unreachable!(),
             "size_of_val" => codegen_size_align!(size),
-            "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)),
-            "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)),
+            "sqrtf32" => codegen_simple_intrinsic!(Sqrtf),
+            "sqrtf64" => codegen_simple_intrinsic!(Sqrt),
             "sub_with_overflow" => self.codegen_op_with_overflow(
                 BinaryOperator::OverflowResultMinus,
                 fargs,

tests/kani/Intrinsics/Math/Arith/sqrt.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_sqrt32() {
+    let positive = 4.0_f32;
+    let negative = -4.0_f32;
+    let negative_zero = -0.0_f32;
+
+    let abs_difference = (positive.sqrt() - 2.0).abs();
+
+    assert!(abs_difference <= f32::EPSILON);
+    assert!(negative.sqrt().is_nan());
+    assert!(negative_zero.sqrt() == negative_zero);
+}
+
+#[kani::proof]
+fn verify_sqrt64() {
+    let positive = 4.0_f64;
+    let negative = -4.0_f64;
+    let negative_zero = -0.0_f64;
+
+    let abs_difference = (positive.sqrt() - 2.0).abs();
+
+    assert!(abs_difference <= 1e-10);
+    assert!(negative.sqrt().is_nan());
+    assert!(negative_zero.sqrt() == negative_zero);
+}