From 1051a52fb788a8f05d1f11b3da65389627c5c4a9 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Fri, 23 Jun 2023 14:41:17 +0000
Subject: [PATCH] Minor edits for all RFCs

---
 rfc/src/rfcs/0001-mir-linker.md              | 2 +-
 rfc/src/rfcs/0002-function-stubbing.md       | 6 ++++--
 rfc/src/rfcs/0003-cover-statement.md         | 7 ++++---
 rfc/src/rfcs/0004-loop-contract-synthesis.md | 4 +++-
 rfc/src/rfcs/0005-should-panic-attr.md       | 6 ++++--
 rfc/src/rfcs/0006-unstable-api.md            | 2 +-
 rfc/src/template.md                          | 2 ++
 7 files changed, 19 insertions(+), 10 deletions(-)

diff --git a/rfc/src/rfcs/0001-mir-linker.md b/rfc/src/rfcs/0001-mir-linker.md
index 1c12d8ee7b68..d951f6243809 100644
--- a/rfc/src/rfcs/0001-mir-linker.md
+++ b/rfc/src/rfcs/0001-mir-linker.md
@@ -1,4 +1,4 @@
-- **Feature Name:** MIR Linker (mir_linker)
+- **Feature Name:** MIR Linker (`mir_linker`)
 - **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/1588>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1600>
 - **Status:** Stable
diff --git a/rfc/src/rfcs/0002-function-stubbing.md b/rfc/src/rfcs/0002-function-stubbing.md
index 2103ad3b632c..e92e3c06178b 100644
--- a/rfc/src/rfcs/0002-function-stubbing.md
+++ b/rfc/src/rfcs/0002-function-stubbing.md
@@ -1,10 +1,12 @@
-- **Feature Name:** Function and method stubbing (`function_stubbing`)
+- **Feature Name:** Function and method stubbing (`function-stubbing`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/1695>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1723> 
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 1
 - **Proof-of-concept:** <https://github.com/aaronbembenek-aws/kani/tree/mir_transform>
 
+-------------------
+
 ## Summary
 
 Allow users to specify that certain functions and methods should be replaced with mock functions (stubs) during verification.
diff --git a/rfc/src/rfcs/0003-cover-statement.md b/rfc/src/rfcs/0003-cover-statement.md
index bbb7a8904e6e..59c99e42107b 100644
--- a/rfc/src/rfcs/0003-cover-statement.md
+++ b/rfc/src/rfcs/0003-cover-statement.md
@@ -1,9 +1,10 @@
-- **Feature Name:** Cover statement `cover_statement`
+- **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:** Under Review
+- **Status:** Unstable
 - **Version:** 0
-- **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here*
+
+-------------------
 
 ## Summary
 
diff --git a/rfc/src/rfcs/0004-loop-contract-synthesis.md b/rfc/src/rfcs/0004-loop-contract-synthesis.md
index 2ac828f06eec..0286dd71b2d2 100644
--- a/rfc/src/rfcs/0004-loop-contract-synthesis.md
+++ b/rfc/src/rfcs/0004-loop-contract-synthesis.md
@@ -1,10 +1,12 @@
-- **Feature Name:** Loop-contract synthesis
+- **Feature Name:** Loop-contract synthesis (`loop-contract-synthesis`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/2214>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2215>
 - **Status:** Under Review
 - **Version:** 0
 - **Proof-of-concept:** <https://github.com/qinheping/kani/tree/kani-synthesizer>
 
+-------------------
+
 ## Summary
 
 A new option that allows users to verify programs without unwinding loops by synthesizing loop contracts for those loops.
diff --git a/rfc/src/rfcs/0005-should-panic-attr.md b/rfc/src/rfcs/0005-should-panic-attr.md
index a5dcff085d2d..1f4aafb599e6 100644
--- a/rfc/src/rfcs/0005-should-panic-attr.md
+++ b/rfc/src/rfcs/0005-should-panic-attr.md
@@ -1,10 +1,12 @@
-- **Feature Name:** The `kani::should_panic` attribute (`should-panic-attr`)*
+- **Feature Name:** The `kani::should_panic` attribute (`should-panic-attr`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/600>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2272>
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 0
 - **Proof-of-concept:** <https://github.com/model-checking/kani/pull/2315>
 
+-------------------
+
 ## Summary
 
 Users may want to express that a verification harness should panic.
diff --git a/rfc/src/rfcs/0006-unstable-api.md b/rfc/src/rfcs/0006-unstable-api.md
index 2c055d4d9333..c964b050bfe1 100644
--- a/rfc/src/rfcs/0006-unstable-api.md
+++ b/rfc/src/rfcs/0006-unstable-api.md
@@ -1,7 +1,7 @@
 - **Feature Name:** Unstable APIs (`unstable-api`)
 - **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/2279>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2281>
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 0
 
 -------------------
diff --git a/rfc/src/template.md b/rfc/src/template.md
index 1ace8208d46e..4f50f7b72f0c 100644
--- a/rfc/src/template.md
+++ b/rfc/src/template.md
@@ -6,6 +6,8 @@
   Start with 0.*
 - **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here*
 
+-------------------
+
 ## Summary
 
 Short description of the feature, i.e.: the elevator pitch. What is this feature about?