From 0391a865bba524e802e1c3f9b95c2924362661ff Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 7 Apr 2022 19:13:35 +0000
Subject: [PATCH 1/2] Add a test for `discriminant_value`

---
 tests/kani/Intrinsics/discriminant_value.rs | 50 +++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 tests/kani/Intrinsics/discriminant_value.rs

diff --git a/tests/kani/Intrinsics/discriminant_value.rs b/tests/kani/Intrinsics/discriminant_value.rs
new file mode 100644
index 000000000000..66fca4c8b39b
--- /dev/null
+++ b/tests/kani/Intrinsics/discriminant_value.rs
@@ -0,0 +1,50 @@
+// 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 },
+}
+
+// An enum that assigns constant values to some variants
+enum Constants {
+    A = 2,
+    B = 5,
+    C,
+}
+
+// An enum that assigns constant values (one of them negative) to all variants
+enum Ordering {
+    Less = -1,
+    Equal = 0,
+    Greater = 1,
+}
+
+#[kani::proof]
+fn main() {
+    // 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
+    );
+    // 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);
+    // 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);
+    // Check that the value is 0 if the type has no discriminant
+    assert!(discriminant_value(&2) == 0);
+}

From 4aa9bceab98d532e91a11ecdec92210320f5e955 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Thu, 7 Apr 2022 21:38:00 +0000
Subject: [PATCH 2/2] Split into 4 proofs

---
 tests/kani/Intrinsics/discriminant_value.rs | 36 ++++++++++++++-------
 1 file changed, 24 insertions(+), 12 deletions(-)

diff --git a/tests/kani/Intrinsics/discriminant_value.rs b/tests/kani/Intrinsics/discriminant_value.rs
index 66fca4c8b39b..519bd5ac392a 100644
--- a/tests/kani/Intrinsics/discriminant_value.rs
+++ b/tests/kani/Intrinsics/discriminant_value.rs
@@ -13,6 +13,17 @@ enum MyError {
     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,
@@ -20,6 +31,14 @@ enum Constants {
     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,
@@ -28,23 +47,16 @@ enum Ordering {
 }
 
 #[kani::proof]
-fn main() {
-    // 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
-    );
-    // 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);
+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);
 }