VeriFast for Rust Reference (verifast#674)

.github/workflows/gh-pages.yml

@@ -0,0 +1,47 @@
+name: Deploy Rust Reference to GitHub Pages
+
+on:
+  push:
+    branches:
+    - master
+
+permissions:
+  contents: read
+  pages: write
+  id-token: write
+
+concurrency:
+  group: "pages"
+  cancel-in-progress: false
+
+jobs:
+  build-gh-pages:
+    name: Deploy the VeriFast for Rust Reference to GitHub Pages
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Setup Pages
+      uses: actions/configure-pages@v5  
+
+    - name: Install mdbook
+      run: mkdir $HOME/mdbook && curl -sSL https://github.com/rust-lang/mdBook/releases/download/v0.4.43/mdbook-v0.4.43-x86_64-unknown-linux-gnu.tar.gz | tar -xz --directory=$HOME/mdbook
+
+    - name: Build the book
+      run: cd docs/rust-reference && $HOME/mdbook/mdbook build
+
+    - name: Set up the site
+      run: mkdir gh-pages && mv docs/rust-reference/book gh-pages/rust-reference
+
+    - name: Upload artifact
+      uses: actions/upload-pages-artifact@v3
+      with:
+        path: gh-pages
+
+    - name: Deploy to GitHub Pages
+      id: deployment
+      uses: actions/deploy-pages@v4

docs/rust-reference/.gitignore

@@ -0,0 +1 @@
+book

docs/rust-reference/book.toml

@@ -0,0 +1,6 @@
+[book]
+authors = ["Bart Jacobs"]
+language = "en"
+multilingual = false
+src = "src"
+title = "The VeriFast for Rust Reference"

docs/rust-reference/src/SUMMARY.md

@@ -0,0 +1,13 @@
+# The VeriFast for Rust Reference
+
+[Introduction](introduction.md)
+- [Symbolic execution states](states.md)
+- [Annotations](annotations.md)
+    - [Keywords](keywords.md)
+    - [Types](types.md)
+    - [Expressions](expressions.md)
+    - [Assertions](assertions.md)
+    - [Function specifications](func-specs.md)
+    - [Function body annotations](func-body-annots.md)
+    - [Ghost declarations](ghost-decls.md)
+- [Verifying non-\`unsafe\` functions](non-unsafe-funcs.md)

docs/rust-reference/src/annotations.md

@@ -0,0 +1,14 @@
+# Annotations
+
+This chapter defines the syntax and the semantics of the various contructs that may appear inside VeriFast annotations.
+
+- [Keywords](keywords.md)
+- [Types](types.md)
+- [Expressions](expressions.md)
+- [Assertions](assertions.md)
+- [Function specifications](func-specs.md)
+- [Function body annotations](func-body-annots.md)
+    - [Ghost commands](func-body-annots.md#ghost-commands)
+    - [Block annotations](func-body-annots.md#block-annotations)
+    - [Call annotations](func-body-annots.md#call-annotations)
+- [Ghost declarations](ghost-decls.md)

docs/rust-reference/src/assertions.md

@@ -0,0 +1,32 @@
+# Assertions
+
+> **<sup>Syntax</sup>**\
+> _Assertion_ :\
+> &nbsp;&nbsp; &nbsp;&nbsp; _PointsToAssertion_\
+> &nbsp;&nbsp; | _PredicateAssertion_\
+> &nbsp;&nbsp; | _TypePredicateAssertion_\
+> &nbsp;&nbsp; | _BooleanAssertion_\
+> &nbsp;&nbsp; | _PatternMatchingEqualityAssertion_\
+> &nbsp;&nbsp; | _ConditionalAssertion_\
+> &nbsp;&nbsp; | _MatchAssertion_\
+> &nbsp;&nbsp; | _Assertion_ `&*&` _Assertion_
+>
+> _PointsToAssertion_ : ( `[` _VFPattern_ `]` )<sup>?</sup> _Expression_ ( `|->` | `|-?->` ) _VFPattern_
+>
+> _VFPattern_ : `_` | `?` ( IDENTIFIER | `_` ) | Expression
+>
+> _PredicateAssertion_ : ( `[` _VFPattern_ `]` )<sup>?</sup> _Expression_ _VFPatternList_ <sup>?</sup> _VFPatternList_
+>
+> _VFPatternList_ : `(` (( _VFPattern_ `,` )<sup>\*</sup> _VFPattern_ )<sup>?</sup> `)`
+>
+> _TypePredicateAssertion_ : `<` _Type_ `>` `.` IDENTIFIER _VFPatternList_
+>
+> _BooleanAssertion_ : _Expression_
+>
+> _PatternMatchingEqualityAssertion_ : _Expression_ `==` _VFPattern_
+>
+> _ConditionalAssertion_ : `if` _Expression_ `{` _Assertion_ `}` `else` `{` _Assertion_ `}`
+>
+> _MatchAssertion_ : `match` _Scrutinee_ `{` ( _MatchAssertionArm_ `,`<sup>?</sup> )<sup>\*</sup> `}`
+>
+> _MatchAssertionArm_ : _Pattern_ `=>` _Assertion_

docs/rust-reference/src/expressions.md

@@ -0,0 +1,14 @@
+# Expressions
+
+> **<sup>Syntax</sup>**\
+> _Expression_ : ... | _Lifetime_ | `typeid` `(` _Type_ `)`
+
+The syntax of expressions in annotations is the same as in Rust code, with two additional supported forms:
+- A lifetime parameter in scope may be used as an expression. This denotes the RustBelt `lifetime_t` value corresponding to that lifetime parameter.
+- The expression `typeid(T)` denotes the typeid of type T.
+
+Also, certain Rust expressions are interpreted differently in annotations than in Rust code:
+- Array expressions are interpreted as `list<T>` values. For example, `[10, 20, 30]` is interpreted as `cons(10, cons(20, cons(30, nil)))`.
+- Arithmetic expressions on integer types are interpreted as operations on the mathematical set ℤ of all integers; they produce their mathematical result and never wrap around.
+
+Note that `match` expressions may be used to perform case analysis on values of VeriFast inductive types.

docs/rust-reference/src/func-body-annots.md

@@ -0,0 +1,43 @@
+# Function body annotations
+
+## Ghost commands
+
+VeriFast accepts the following *ghost commands* as annotations in positions where statements are allowed in Rust code.
+
+<div class="warning">
+
+> VeriFast preprocesses `.rs` files to replace annotations inside function bodies by dummy `VeriFast_ghost_command();` statements.
+> If an annotation inside a function body appears in a position where
+> such a call is not allowed, you may get a confusing Rust compiler error.
+
+</div>
+
+> **<sup>Syntax</sup>**\
+> _GhostCommandAnnotation_ : `/*@` _GhostCommand_ `@*/`
+>
+> _GhostCommand_ :\
+> &nbsp;&nbsp; &nbsp;&nbsp; `open` _PredicateAssertion_ `;`\
+> &nbsp;&nbsp; | `close` _PredicateAssertion_ `;`\
+> &nbsp;&nbsp; | `let` IDENTIFIER `=` _Expression_ `;`\
+> &nbsp;&nbsp; | `if` _Expression_ `{` _GhostCommand_ <sup>\*</sup> `}` ( `else` `{` _GhostCommand_ <sup>\*</sup> `}` )<sup>?</sup>\
+> &nbsp;&nbsp; | `match` _Scrutinee_ `{` _MatchGhostCommandArm_ <sup>\*</sup> `}`\
+> &nbsp;&nbsp; | `assert` _Assertion_ `;`\
+> &nbsp;&nbsp; | `leak` _Assertion_ `;`\
+> &nbsp;&nbsp; | `produce_lem_ptr_chunk` _TypePath_ `(` (( _Expression_ `,` )<sup>\*</sup> _Expression_ )<sup>?</sup> `)` `(` (( IDENTIFIER `,` )<sup>*</sup> IDENTIFIER )<sup>?</sup> `)` `{` _GhostCommand_ <sup>\*</sup> `}` ( `;` | `{` _GhostCommand_ <sup>\*</sup> `}` )\
+> &nbsp;&nbsp; | `produce_fun_ptr_chunk` _TypePath_ `(` _Expression_ `)` `(` (( _Expression_ `,` )<sup>\*</sup> _Expression_ )<sup>?</sup> `)` `(` (( IDENTIFIER `,` )<sup>*</sup> IDENTIFIER )<sup>?</sup> `)` `{` _GhostCommand_ <sup>\*</sup> `}`\
+> &nbsp;&nbsp; | `{` _GhostDeclaration_ <sup>\*</sup> _GhostCommand_ <sup>\*</sup> `}`\
+> &nbsp;&nbsp; | `return` _Expression_ <sup>?</sup> `;`\
+> &nbsp;&nbsp; | _Expression_ `;`
+
+A `return` ghost command may only appear in a lemma body, not in a ghost command annotation.
+
+## Block annotations
+
+Additionally, a Rust block may start with one of the following VeriFast annotations:
+- a loop invariant of the form `/*@` `inv` _Assertion_ `;` `@*/`
+- a loop specification of the form `/*@` `req` _Assertion_ `;` `ens` _Assertion_ `;` `@*/`. Notice that here, the requires clause and the ensures clause must be in the same annotation, whereas in the case of function specifications they must be in separate annotations.
+- a batch of ghost declarations of the form `/*@` _GhostDeclaration_ <sup>\*</sup> `@*/` The declarations supported in such batches are predicate definitions, lemma definitions, and local lifetime variable definitions (using `let_lft`).
+
+## Call annotations
+
+Furthermore, a *ghost generic argument list* annotation may be inserted between the function name and the argument list of a Rust function call, like so: `foo/*@::<'a, T>@*/`. This is necessary in cases where it is important to pass a particular lifetime as a generic argument to a function. If, for a function call, no ghost generic argument list is provided, VeriFast uses `'static` as the argument for each of the function's lifetime parameters.

docs/rust-reference/src/func-specs.md

@@ -0,0 +1,13 @@
+# Function specifications
+
+VeriFast accepts the following *specification clauses* between a function's header and its body:
+
+> **<sup>Syntax</sup>**\
+> _SpecificationClause_ :\
+> &nbsp;&nbsp; &nbsp;&nbsp; `/*@` `req` _Assertion_ `;` `@*/`\
+> &nbsp;&nbsp; | `/*@` `ens` _Assertion_ `;` `@*/` \
+> &nbsp;&nbsp; | `/*@` `assume_correct` `@*/`
+
+Note that VeriFast also support single-line annotations of the form `//@ ...annotation...`. Such an annotation is entirely equivalent to `/*@ ...annotation... @*/`.
+
+Notice that the requires clause and the ensures clause must be in separate annotations.

docs/rust-reference/src/ghost-decls.md

@@ -0,0 +1,33 @@
+# Ghost declarations
+
+A ghost declarations annotation may appear anywhere a Rust item may appear, except that only a few kinds of ghost declarations are supported inside function bodies (see [Block annotations](func-body-annots.md#block-annotations)).
+
+> **<sup>Syntax</sup>**\
+> _GhostDeclarationsAnnotation_ : `/*@` _GhostDeclaration_ <sup>\*</sup> `@*/`
+>
+> _GhostDeclaration_ :\
+> &nbsp;&nbsp; &nbsp;&nbsp; `pub` _GhostDeclaration_\
+> &nbsp;&nbsp; | `inductive` IDENTIFIER _GenericParams_ <sup>?</sup> `=` `|`<sup>?</sup> _InductiveConstructor_ ( `|` _InductiveConstructor_ )<sup>\*</sup> `;`\
+> &nbsp;&nbsp; | `fix` IDENTIFIER _GenericParams_ <sup>?</sup> `(` _Params_ `)` ( `->` _Type_ )<sup>?</sup> ( `{` _Expression_ `}` | `;` )\
+> &nbsp;&nbsp; | `pred` IDENTIFIER _GenericParams_ <sup>?</sup> `(` ( _Params_ `;` )<sup>?</sup> _Params_ `)` ( `=` _Assertion_ )<sup>?</sup> `;`\
+> &nbsp;&nbsp; | `pred_ctor` IDENTIFIER _GenericParams_ <sup>?</sup> `(` _Params_ `)` `(` ( _Params_ `;` )<sup>?</sup> _Params_ `)` `=` _Assertion_ `;`\
+> &nbsp;&nbsp; | `pred` _GenericParams_ <sup>?</sup> `<` _Type_ `>` `.` IDENTIFIER `(` ( _ParamNames_ `;` )<sup>?</sup> _ParamNames_ `)` `=` _Assertion_ `;`\
+> &nbsp;&nbsp; | `lem` IDENTIFIER _GenericParams_ <sup>?</sup> `(` _Params_ `)` ( `->` _Type_ )<sup>?</sup> _LemmaRest_\
+> &nbsp;&nbsp; | `fn_type` IDENTIFIER _GenericParams_ <sup>?</sup> `(` _Params_ `)` `=` `unsafe` `fn` `(` _Params_ `)` ( `->` _Type_ )<sup>?</sup> `;` `req` _Assertion_ `;` `ens` _Assertion_ `;`\
+> &nbsp;&nbsp; | `lem_type` IDENTIFIER _GenericParams_ <sup>?</sup> `(` _Params_ `)` `=` `lem` `(` _Params_ `)` ( `->` _Type_ )<sup>?</sup> `;` `req` _Assertion_ `;` `ens` _Assertion_ `;`\
+> &nbsp;&nbsp; | `let_lft` _Lifetime_ `=` _Expression_ `;`\
+> &nbsp;&nbsp; | `abstract_type` IDENTIFIER `;`
+>
+> _InductiveConstructor_ : IDENTIFIER ( `(` ( _ParamType_ `,` )<sup>*</sup> _ParamType_ `)` )<sup>?</sup>
+> 
+> _LemmaRest_ :\
+> &nbsp;&nbsp; &nbsp;&nbsp; _LemmaSpecification_ `{` _GhostCommand_ <sup>\*</sup> `}`\
+> &nbsp;&nbsp; | `;` _LemmaSpecification_
+>
+> _LemmaSpecification_ : `nonghost_callers_only`<sup>?</sup> `req` _Assertion_ `;` `ens` _Assertion_ `;`
+>
+> _Params_ : (( _Param_ `,` )<sup>\*</sup> _Param_ )<sup>?</sup>
+>
+> _Param_ : IDENTIFIER `:` _Type_
+>
+> _ParamNames_ : (( IDENTIFIER `,` )<sup>\*</sup> IDENTIFIER )<sup>?</sup>

docs/rust-reference/src/introduction.md

@@ -0,0 +1,74 @@
+# Introduction
+
+VeriFast is a tool for modular formal verification of the absence of [undefined
+behavior](https://doc.rust-lang.org/reference/behavior-considered-undefined.html)
+in Rust[^other-languages] programs that use `unsafe` blocks and the
+[soundness](https://doc.rust-lang.org/nomicon/working-with-unsafe.html) of Rust
+modules that use `unsafe` blocks. It works by _symbolically executing_ each
+function separately, using a _separation logic_ representation of memory,
+starting from a symbolic state that represents an arbitrary program state that
+satisfies the function's _precondition_, and checking that each state at which
+the function returns satisfies the function's _postcondition_. By using the
+callee's precondition and postcondition instead of its body when symbolically
+executing a function call, and by using the user-specified loop invariant when
+symbolically executing a loop so as to be able to symbolically execute the loop
+body only once, and by using _symbols_ to represent possibly infinitely many
+program states using a finite number of symbolic states, VeriFast covers all
+(usually infinitely many) possible executions of a function using a finite (and
+usually small) number of symbolic executions, allowing the verification of
+(small) programs to usually complete in a matter of seconds.
+
+For functions not declared as `unsafe`, VeriFast derives a precondition and
+postcondition from the function's parameter types and return type using the
+separation logic interpretation of Rust's types defined by
+[RustBelt](https://research.ralfj.de/thesis.html); for functions declared as
+`unsafe`, the user has to provide a precondition and postcondition by inserting
+specially marked comments called _annotations_ into the source code. Similarly, for each loop a loop
+invariant has to be provided in an annotation. To be able to
+express these conditions (called _assertions_), the user may generally also have
+to insert annotations defining mathematical recursive datatypes called
+_inductive datatypes_, mathematical recursive functions over these datatypes
+called _fixpoint functions_, recursive named separation logic assertions called
+_predicates_, and _type predicates_ defining a custom interpretation for some of the
+struct types defined by the current module (as well as some less common constructs
+such as _VeriFast named function types_, _lemma function types_, _predicate
+families_, and _predicate family instances_).
+
+In order for symbolic execution to succeed, the user may furthermore have to
+insert annotations containing _ghost commands_ such as `open` and `close`
+commands for unfolding and folding predicates and calls of _lemma functions_,
+possibly recursive functions defined inside annotations that are checked by
+VeriFast to terminate and to not have side-effects and that serve as possibly
+inductive proofs about fixpoint functions and predicates.
+
+This reference defines the syntax of the various kinds of annotations, and
+describes VeriFast's symbolic execution algorithm and the various checks that
+VeriFast performs.
+
+## The state of VeriFast
+
+VeriFast has been developed by Bart Jacobs, Jan Smans, and Frank Piessens at KU
+Leuven, Department of Computer Science, DistriNet research group since 2008,
+with many contributions from contributors inside and outside DistriNet. VeriFast
+for Rust has been developed by Nima Rahimi Foroushaani and Bart Jacobs at
+DistriNet since 2022. The lead developer and main maintainer is Bart Jacobs, an
+associate professor at DistriNet, who combines these activities with his usual
+research, education, and service duties. The largest verification performed so far with
+VeriFast for Rust, the verification of certain properties of certain functions
+of the Rust standard library's LinkedList data structure, was performed in
+December 2024. Its support for the Rust language is as of yet very incomplete[^other-languages-incomplete],
+so that for any new nontrivial use case, it is to be expected, for now, that the
+tool will have to be extended. Bart Jacobs is eager to support anyone interested
+in using VeriFast. However, despite his best intentions, he may get distracted
+by other occupations; in that case, please do not hesitate to remind him early
+and often---your continued showing of interest will only delight him and you may
+rest assured that, given sufficient prodding, your issue will be resolved eventually.
+
+## The state of this reference
+
+This reference is under construction; much material is still missing. Please
+bear with us! But if there are particular parts you're particularly eager to
+see, it always helps to let us know.
+
+[^other-languages]: VeriFast also supports (subsets of) C and Java.
+[^other-languages-incomplete]: as is its support for Java and, to a somewhat lesser extent, C

docs/rust-reference/src/keywords.md

@@ -0,0 +1,21 @@
+# Keywords
+
+In annotations, these words, in addition to Rust's keywords, are recognized as keywords and cannot be used as identifiers:
+
+> `_` `above` `abstract_type` `activating` `action` `and_fresh_handle`\
+> `and_handle` `any` `assert` `assume_correct` `below` `box_class` `by` `close`\
+> `consuming_box_pred` `consuming_handle_pred` `copred` `create_box`\
+> `create_fresh_handle` `create_handle` `decreases` `dispose_box`\
+> `dup_lem_ptr_chunk` `emp` `ens` `extends` `fix` `fix_auto` `fn_type`\
+> `forall_` `handle` `handle_pred` `import_module` `inductive` `inv` `leak`\
+> `lem` `lem_auto` `lem_type` `let_lft` `merge_fractions`\
+> `nonghost_callers_only` `open` `perform_action` `permbased` `pred`\
+> `pred_ctor` `pred_fam` `pred_fam_inst` `preserved_by` `produce_fn_ptr_chunk`\
+> `produce_lem_ptr_chunk` `producing_box_pred` `producing_fresh_handle_pred`\
+> `producing_handle_pred` `req` `require_module` `split_fraction` `terminates`\
+> `truncating` `type_pred_decl` `type_pred_def` `typedef` `typeid`\
+> `unloadable_module`
+
+These are the additional operators recognized inside annotations:
+
+>  `&*&` `|->` `|-?->` `@`