feat: support persistent ghosts

src/lib.rs

@@ -75,12 +75,14 @@ pub enum Ast {
         definition: String,
     },
     GhostFunction {
+        persistent: bool,
         name: String,
         ty_list: Vec<String>,
         returns: String,
         axioms: Option<String>,
     },
     GhostMapping {
+        persistent: bool,
         name: String,
         mapping: String,
         axioms: Option<String>,

src/parse.rs

@@ -92,28 +92,40 @@ fn decl_parser() -> impl Parser<Token, Intermediate, Error = Simple<Token>> {
     };
 
     let ghost_decl = {
-        let with_mapping = just(Token::Ghost)
-            .ignore_then(ty())
+        let persistent_ghost = just(Token::Persistent).then(just(Token::Ghost)).to(true);
+        let regular_ghost = just(Token::Ghost).to(false);
+
+        let opening_tokens = persistent_ghost.or(regular_ghost);
+
+        let with_mapping = opening_tokens
+            .clone()
+            .then(ty())
             .then(ident())
             .then(optional_code_block())
-            .map(|((mapping, name), block)| Intermediate::GhostMapping {
-                mapping,
-                name,
-                axioms: block,
-            })
+            .map(
+                |(((persistent, mapping), name), axioms)| Intermediate::GhostMapping {
+                    persistent,
+                    mapping,
+                    name,
+                    axioms,
+                },
+            )
             .labelled("ghost declaration (with mapping)");
 
-        let without_mapping = just(Token::Ghost)
-            .ignore_then(ident())
+        let without_mapping = opening_tokens
+            .then(ident())
             .then(unnamed_param_list())
             .then(returns_type())
             .then(optional_code_block())
-            .map(|(((name, ty_list), returns), block)| Intermediate::Ghost {
-                name,
-                ty_list,
-                returns,
-                axioms: block,
-            })
+            .map(
+                |((((persistent, name), ty_list), returns), axioms)| Intermediate::GhostFunction {
+                    persistent,
+                    name,
+                    ty_list,
+                    returns,
+                    axioms,
+                },
+            )
             .labelled("ghost declaration (without mapping)");
 
         with_mapping.or(without_mapping)

src/parse/builder.rs

@@ -261,27 +261,31 @@ impl<'src> Builder<'src> {
                 DocOrAst::Ast(ast)
             }
             Intermediate::GhostMapping {
+                persistent,
                 mapping,
                 name,
                 axioms,
             } => {
                 let axioms = axioms.map(|c| self.owned_slice(c));
                 let ast = Ast::GhostMapping {
+                    persistent,
                     name,
                     mapping,
                     axioms,
                 };
 
                 DocOrAst::Ast(ast)
             }
-            Intermediate::Ghost {
+            Intermediate::GhostFunction {
+                persistent,
                 name,
                 ty_list,
                 returns,
                 axioms,
             } => {
                 let axioms = axioms.map(|c| self.owned_slice(c));
                 let ast = Ast::GhostFunction {
+                    persistent,
                     name,
                     ty_list,
                     returns,

src/parse/lexer.rs

@@ -127,6 +127,7 @@ pub fn cvl_lexer() -> impl Parser<char, Vec<(Token, Span)>, Error = Simple<char>
         "sig" => Token::Sig,
         "description" => Token::Description,
         "old" => Token::Old,
+        "persistent" => Token::Persistent,
         _ => Token::Ident(ident),
     });
     let other = {

src/parse/tests/cvl2.rs

@@ -546,3 +546,30 @@ fn unrecognized_tags() {
     assert_matches!(tag3.kind, TagKind::Formula);
     assert_eq!(tag3.description, "hello@withrevert(world)"); // @withrevert should not parse to a new tag
 }
+
+#[test]
+fn persistent_ghosts() {
+    let src = indoc! {"
+        persistent ghost int pers;
+        ghost            int non_pers;
+    "};
+
+    let parsed = Builder::new(src).build().unwrap();
+
+    let check_ghost = |element: &CvlElement, expected_name, expected_persistent| match &element.ast
+    {
+        Ast::GhostMapping {
+            persistent, name, ..
+        } => {
+            assert_eq!(name, expected_name);
+            assert_eq!(*persistent, expected_persistent);
+        }
+
+        ast => panic!("got unexpected ast: ${ast:?}"),
+    };
+
+    assert_eq!(parsed.len(), 2);
+
+    check_ghost(&parsed[0], "pers", true);
+    check_ghost(&parsed[1], "non_pers", false);
+}

src/parse/types.rs

@@ -59,6 +59,7 @@ pub enum Token {
     Old,
     Offset,
     Slot,
+    Persistent,
 }
 
 impl Display for Token {
@@ -108,6 +109,7 @@ impl Display for Token {
             Token::Index => write!(f, "INDEX"),
             Token::Slot => write!(f, "slot"),
             Token::Offset => write!(f, "offset"),
+            Token::Persistent => write!(f, "persistent"),
 
             Token::Ident(data) | Token::Other(data) | Token::Number(data) | Token::String(data) => {
                 write!(f, "{data}")
@@ -141,11 +143,13 @@ pub enum Intermediate {
         block: Span,
     },
     GhostMapping {
+        persistent: bool,
         name: String,
         mapping: String,
         axioms: Option<Span>,
     },
-    Ghost {
+    GhostFunction {
+        persistent: bool,
         name: String,
         ty_list: Vec<String>,
         returns: String,