From c7067cf9dc35f48c6d1e7ac20ab2be107f3c4021 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 19 Apr 2024 13:41:28 -0700
Subject: [PATCH] Stabilize cover statement and update contracts RFC (#3091)

I would like to propose that we stabilize the cover statement as is. Any
further improvements or changes can be done separately, with or without
an RFC.

I am also updating the contracts RFC status since parts of it have been
integrated to Kani, but it is still unstable.

### Call-out

This PR requires at least 2 approvals.
---
 library/kani/src/mem.rs                 |  2 +-
 rfc/src/rfcs/0003-cover-statement.md    | 12 ++++++++----
 rfc/src/rfcs/0009-function-contracts.md |  7 ++++---
 scripts/build-docs.sh                   |  4 +++-
 4 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
index 203eae2229c4..43062ebed6a1 100644
--- a/library/kani/src/mem.rs
+++ b/library/kani/src/mem.rs
@@ -44,7 +44,7 @@ use std::ptr::{DynMetadata, NonNull, Pointee};
 /// Note that an unaligned pointer is still considered valid.
 ///
 /// TODO: Kani should automatically add those checks when a de-reference happens.
-/// https://github.com/model-checking/kani/issues/2975
+/// <https://github.com/model-checking/kani/issues/2975>
 ///
 /// This function will either panic or return `true`. This is to make it easier to use it in
 /// contracts.
diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md
index 6839af22f929..de452654392b 100644
--- a/rfc/src/rfcs/0003-cover-statement.md
+++ b/rfc/src/rfcs/0003-cover-statement.md
@@ -1,8 +1,8 @@
 - **Feature Name:** Cover statement (`cover-statement`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/696>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1906>
-- **Status:** Unstable
-- **Version:** 1
+- **Status:** Stable
+- **Version:** 2
 
 -------------------
 
@@ -138,8 +138,12 @@ However, if the condition can indeed be covered, verification would fail due to
 
 ## Open questions
 
-Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`?
-Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time.
+- ~Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`?
+Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time.~
+  - For now, this macro will not accept format arguments, since this
+    is not well handled by Kani.
+    This is an extesion to this API that can be easily added later on if Kani
+    ever supports runtime formatting.
 
 ## Other Considerations
 
diff --git a/rfc/src/rfcs/0009-function-contracts.md b/rfc/src/rfcs/0009-function-contracts.md
index e26592080822..dae805a7db72 100644
--- a/rfc/src/rfcs/0009-function-contracts.md
+++ b/rfc/src/rfcs/0009-function-contracts.md
@@ -1,8 +1,8 @@
 - **Feature Name:** Function Contracts
 - **Feature Request Issue:** [#2652](https://github.com/model-checking/kani/issues/2652) and [Milestone](https://github.com/model-checking/kani/milestone/31)
 - **RFC PR:** [#2620](https://github.com/model-checking/kani/pull/2620)
-- **Status:** Under Review 
-- **Version:** 0
+- **Status:** Unstable
+- **Version:** 1
 - **Proof-of-concept:** [features/contracts](https://github.com/model-checking/kani/tree/features/contracts)
 - **Feature Gate:** `-Zfunction-contracts`, enforced by compile time error[^gate]
 
@@ -893,4 +893,5 @@ times larger than what they expect the function will touch).
 
 [^stubcheck]: Kani cannot report the occurrence of a contract function to check
     in abstracted functions as errors, because the mechanism is needed to verify
-    mutually recursive functions.
\ No newline at end of file
+    mutually recursive functions.
+
diff --git a/scripts/build-docs.sh b/scripts/build-docs.sh
index cd40a2edabad..2e2c10b052f6 100755
--- a/scripts/build-docs.sh
+++ b/scripts/build-docs.sh
@@ -28,8 +28,10 @@ else
       curl -sSL -o "$FILE" "$URL"
       echo "$EXPECTED_HASH $FILE" | sha256sum -c -
       tar zxf $FILE
+      MDBOOK=${SCRIPT_DIR}/mdbook
+  else
+      MDBOOK=mdbook
   fi
-  MDBOOK=${SCRIPT_DIR}/mdbook
 fi
 
 KANI_DIR=$SCRIPT_DIR/..