Statics can also have ensures clauses

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!

src/lib.rs

@@ -846,15 +846,14 @@ 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() {
                 Rule::ensures_clause => to_doc(ctx, p, arena).append(arena.line()),
                 _ => 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),

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

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!
     "###);
 }