From 463fd14f266da2908b7991035e359f3c29d0b671 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Thu, 28 Dec 2023 14:57:18 -0500
Subject: [PATCH] Statics can also have ensures clauses

---
 examples/wip.rs            | 11 +----------
 src/lib.rs                 |  3 +--
 src/verus.pest             |  2 +-
 tests/verus-consistency.rs |  9 +++++++++
 4 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/examples/wip.rs b/examples/wip.rs
index ae29cb7..ed44a8b 100644
--- a/examples/wip.rs
+++ b/examples/wip.rs
@@ -1,15 +1,6 @@
-/*
-
-  This file models the abstraction of an infinite log that our log
-  implementation is supposed to implement.
-
-*/
-use vstd::set::*;
 
 verus! {
 
-pub struct AbstractInfiniteLogState {
-    pub head: int,
-}
+exec static LAZY_X: Lazy<X> ensures LAZY_X.wf() { Lazy::<X>::new() }
 
 } // verus!
diff --git a/src/lib.rs b/src/lib.rs
index bbe4d00..28bd9e1 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -846,7 +846,7 @@ fn to_doc<'a>(
         Rule::variant => map_to_doc(ctx, arena, pair),
         Rule::union => unsupported(pair),
         //Rule::initializer => soft_indent(arena, map_to_doc(ctx, arena, pair)),
-        Rule::r#const =>
+        Rule::r#const | Rule::r#static =>
         // In this context, if there's an ensures clause, we need to add a line
         {
             arena.concat(pair.into_inner().map(|p| match p.as_rule() {
@@ -854,7 +854,6 @@ fn to_doc<'a>(
                 _ => to_doc(ctx, p, arena),
             }))
         }
-        Rule::r#static => map_to_doc(ctx, arena, pair),
         Rule::r#trait => map_to_doc(ctx, arena, pair),
         Rule::trait_alias => unsupported(pair),
         Rule::assoc_items => map_to_doc_lines(ctx, arena, pair),
diff --git a/src/verus.pest b/src/verus.pest
index c8a5c2c..64bc3e3 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -706,7 +706,7 @@ const = {
 static = {
     attr* ~ visibility? ~ fn_mode? ~
     static_str ~ mut_str? ~ name ~ colon_str ~ type ~
-    (eq_str ~ expr)? ~ semi_str
+    (((eq_str ~ expr)? ~ semi_str) | (ensures_clause ~ fn_block_expr))
 }
 
 trait = {
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index 54d2630..1789cc9 100644
--- a/tests/verus-consistency.rs
+++ b/tests/verus-consistency.rs
@@ -1277,6 +1277,8 @@ verus! {
 
 exec static THREAD_COUNT: core::sync::atomic::AtomicUsize = core::sync::atomic::AtomicUsize::new(0);
 
+exec static LAZY_X: Lazy<X> ensures LAZY_X.wf() { Lazy::<X>::new() }
+
 } // verus!
 "#;
 
@@ -1285,6 +1287,13 @@ exec static THREAD_COUNT: core::sync::atomic::AtomicUsize = core::sync::atomic::
 
     exec static THREAD_COUNT: core::sync::atomic::AtomicUsize = core::sync::atomic::AtomicUsize::new(0);
 
+    exec static LAZY_X: Lazy<X>
+        ensures
+            LAZY_X.wf(),
+    {
+        Lazy::<X>::new()
+    }
+
     } // verus!
     "###);
 }