Add a test for discriminant_value (model-checking#1021)

* Add a test for `discriminant_value`

* Split into 4 proofs

tests/kani/Intrinsics/discriminant_value.rs

@@ -0,0 +1,62 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `discriminant_value` returns the expected results
+// for different cases
+#![feature(core_intrinsics)]
+use std::intrinsics::discriminant_value;
+
+// A standard enum with variants containing fields
+enum MyError {
+    Error1(i32),
+    Error2(&'static str),
+    Error3 { description: String, code: u32 },
+}
+
+#[kani::proof]
+fn test_standard_enum() {
+    // Check that the values go from 0 to `num_variants - 1`
+    assert!(discriminant_value(&MyError::Error1) == 0);
+    assert!(discriminant_value(&MyError::Error2("bar")) == 1);
+    assert!(
+        discriminant_value(&MyError::Error3 { description: "some_error".to_string(), code: 3 })
+            == 2
+    );
+}
+
+// An enum that assigns constant values to some variants
+enum Constants {
+    A = 2,
+    B = 5,
+    C,
+}
+
+#[kani::proof]
+fn test_constants_enum() {
+    // Check that the values are equal to the constants assigned
+    assert!(discriminant_value(&Ordering::Less) == -1);
+    assert!(discriminant_value(&Ordering::Equal) == 0);
+    assert!(discriminant_value(&Ordering::Greater) == 1);
+}
+
+// An enum that assigns constant values (one of them negative) to all variants
+enum Ordering {
+    Less = -1,
+    Equal = 0,
+    Greater = 1,
+}
+
+#[kani::proof]
+fn test_ordering_enum() {
+    // Check that the values are equal to the constants assigned
+    // and the non-assigned value follows from the assigned ones
+    assert!(discriminant_value(&Constants::A) == 2);
+    assert!(discriminant_value(&Constants::B) == 5);
+    assert!(discriminant_value(&Constants::C) == 6);
+}
+
+#[kani::proof]
+fn test_no_enum() {
+    // Check that the value is 0 if the type has no discriminant
+    assert!(discriminant_value(&2) == 0);
+}