From 3d868717635b280773844a765ce4c60d5fd5c803 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Mon, 11 Dec 2023 10:31:22 -0500
Subject: [PATCH] update supported features list, add docs for static items

---
 source/docs/guide/src/SUMMARY.md  |  1 +
 source/docs/guide/src/features.md | 12 ++++++------
 source/docs/guide/src/static.md   | 20 ++++++++++++++++++++
 3 files changed, 27 insertions(+), 6 deletions(-)
 create mode 100644 source/docs/guide/src/static.md

diff --git a/source/docs/guide/src/SUMMARY.md b/source/docs/guide/src/SUMMARY.md
index a3981d2c6e..44198cab95 100644
--- a/source/docs/guide/src/SUMMARY.md
+++ b/source/docs/guide/src/SUMMARY.md
@@ -43,6 +43,7 @@
     - [broadcast_forall]() <!--- Chris --->
 - [Runtime `exec` Features]()
     - [Exec closures]()
+    - [Statics](./static.md)
 - [SMT solving, automation, and where automation fails](smt_failures.md) <!--- Chris --->
     - [What's decidable, what's undecidable, what's fast, what's slow]() <!--- Chris --->
     - [Integers: nonlinear arithmetic and bit vectors](nonlinear_bitvec.md) <!--- Chris and Chanhee --->
diff --git a/source/docs/guide/src/features.md b/source/docs/guide/src/features.md
index 156a17db43..64b4ae86e5 100644
--- a/source/docs/guide/src/features.md
+++ b/source/docs/guide/src/features.md
@@ -4,7 +4,7 @@ Quick reference for supported Rust features. Note that this list does not includ
 
 Note that Verus is in active development. If a feature is unsupported, it might be genuinely hard, or it might just be low priority. See the [github issues](https://github.com/verus-lang/verus/issues) or [discussions](https://github.com/verus-lang/verus/discussions) for information on planned features.
 
-**Last Updated: 2023-05-17**
+**Last Updated: 2023-12-11**
 
 <div class="table-wrapper"><table>
   <thead><tr><th colspan="2"><strong>Items</strong></th></tr></thead>
@@ -43,7 +43,7 @@ Note that Verus is in active development. If a feature is unsupported, it might
   </tr>
   <tr>
     <td>Static items</td>
-    <td>Not supported</td>
+    <td>[Partially supported](./statics.md)</td>
   </tr>
   <tr>
     <td>Unions</td>
@@ -141,11 +141,11 @@ Note that Verus is in active development. If a feature is unsupported, it might
   </tr>
   <tr>
     <td>Compound assigments (<code>+=</code>, etc.)</td>
-    <td>Not supported</td>
+    <td>Supported</td>
   </tr>
   <tr>
     <td>Array expressions</td>
-    <td>Not supported</td>
+    <td>Partially supported (no fill expressions)</td>
   </tr>
   <tr>
     <td>Range expressions</td>
@@ -239,7 +239,7 @@ Note that Verus is in active development. If a feature is unsupported, it might
   </tr>
   <tr>
     <td>Arrays</td>
-    <td>Not supported</td>
+    <td>Supported</td>
   </tr>
   <tr>
     <td>Pointers</td>
@@ -338,7 +338,7 @@ Note that Verus is in active development. If a feature is unsupported, it might
   </tr>
   <tr>
     <td><code>Sized</code> (<code>size_of</code>, <code>align_of</code>)</td>
-    <td>Not supported</td>
+    <td>Supported</td>
   </tr>
   <tr>
     <td><code>Deref</code>, <code>DerefMut</code></td>
diff --git a/source/docs/guide/src/static.md b/source/docs/guide/src/static.md
new file mode 100644
index 0000000000..3b1590aa9d
--- /dev/null
+++ b/source/docs/guide/src/static.md
@@ -0,0 +1,20 @@
+# Static items
+
+Verus supports static items, similar to `const` items. Unlike `const` items, though,
+`static` items are only usable in `exec` mode. Note that this requires them to be
+_explicitly_ marked as `exec`:
+
+```
+exec static x: u64 = 0;
+```
+
+The reason for this is consistency with `const`; for `const` items, the default mode
+for an unmarked const item is the [dual `spec`-`exec` mode](./const.md).
+However, this mode is not supported for `static` items; therefore, static items
+need to be explicitly marked `exec`.
+
+Note there are some **limitations** to the current support for `static` items.
+Currently, a static item cannot be referenced from a spec expression. This means, for example,
+that you can't prove that two uses of the same static item give the same value
+if those uses are in different functions. We expect this limitation will be lifted
+in the future.