update supported features list, add docs for static items

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 --->

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>

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.