Add tool: VeriFast

[btj]

Remi Delmas recently suggested that I participate in the challenges using VeriFast. I went ahead and had a go at Challenge 5 (linked_list.rs); today I reached a state where I consider the challenge solved. I used VeriFast 24.12 (released today). I guess I should get the tool accepted now. Here is the tool application form:

The following form is designed to provide information for your tool that should be included in the effort to verify the Rust standard library. Please note that the tool will need to be supported if it is to be included.

Tool Name

VeriFast

Description

VeriFast is a tool for modularly verifying absence of undefined behavior as well as functional correctness properties of single-threaded and multithreaded C, Java, or Rust programs. It takes as input the source code for a module (object file/jar file/crate) with function/method preconditions and postconditions and other specification and proof hint constructs (such as loop invariants) included as special comments, and verifies each function/method separately by symbolically executing it, starting from a symbolic state that represents an arbitrary state that satisfies the precondition, and checking that the state upon return satisfies the postcondition. It uses a separation logic representation of memory.

Tool Information

• [Y] Does the tool perform Rust verification?
• [Y] Does the tool deal with unsafe Rust code?
• [Y] Does the tool run independently in CI?
• [Y] Is the tool open source?
• [Y] Is the tool under development?
• [Y] Will you or your team be able to provide support for the tool?

Licenses

Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s).
MIT license

Steps to Use the Tool

1. Download the tool distribution for your platform (MacOS, Windows, Linux) from https://github.com/verifast/verifast/releases .
2. Extract the archive to anywhere on your machine
3. Run /path/to/verifast/bin/verifast -c /path/to/the/file.rs

Extra command-line options may be required; see tests/rust/testsuite.mysh to see the command lines used for the Rust examples.

Artifacts

VeriFast has been used by Nathan Chong at AWS to verify the core concurrent queue data structure used for task scheduling in FreeRTOS: https://nchong.github.io/talks/CAVLightning-23July2020.pdf https://nchong.github.io/papers/ewc21.pdf , and then by Tobias Reinhard while interning with Mark Tuttle at AWS to verify the same in Multicore FreeRTOS. We have also used it for other small "industrial case studies": https://people.cs.kuleuven.be/~bart.jacobs/verifast/vf-case-studies-scp2012.pdf We have won several verification competitions with VeriFast: VerifyThis 2012 and VerifyThis 2016. But VeriFast has mostly been a vehicle for developing new ideas in modular verification. See references in https://arxiv.org/pdf/1507.07697 and at https://distrinet.cs.kuleuven.be/people/BartJacobs .

CI & Versioning

I mostly use the nightly builds; I create named releases only irregularly, when the need arises. I created a new release today: VeriFast 24.12.

[remi-delmas-3000]

Hi Bart !

Thanks a lot for submitting the application !

Below is a recap of the (requirements)[https://model-checking.github.io/verify-rust-std/general-rules.html] to get a tool integrated:

Any new tool that participants want to enable will require an application using the tool application template.

We are good on this one.

The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS

I’m going to assemble a group to audit verifast’s recently intoduced support for Rust and lifetime logic. However any supporting documents you can provide (papers, documentation etc), pointers to relevant code in the Verifast repository, etc. would be immensely helpful to help us get started.

A new tool application should clearly specify the differences to existing techniques and provide sufficient background of why this is needed.

No need to elaborate too much on the core principles underlying Verifast (you've already published a lot on Verifast), but you could at least elaborate a little bit on the approach you took to porting the liftetime logic from RustBelt to Verifast, and the classes of UB and even functional properties this allows to cover when verifying Rust.

The tool application should also include mechanisms to audit its implementation and correctness.

Here you could perhaps give links to Verifast’s own regression tests suite, specifically for Rust, and CI checks/status if you have any CI checks automated via github.

Examples of negative tests (failing proofs due to known bugs) would also be good to help confirm the tool can detect bugs when they are present.

Once the tool is approved, the participant needs to create a PR that creates a new action that runs the std library verification using the new tool, as well as an entry to the “Approved Tools” section of this book.

This point requires some precision: The PR must effectively provide a github action that runs your tool against the current version of the verify-std-lib repository.

The CI integration via a github action is a very (if not the most) important part of the tool integration, since we ultimately want the proofs to be performed at each release of the rust std library, and not just be one-off events.

For reference, this is the github action that runs Kani against the repo: https://github.com/model-checking/verify-rust-std/blob/main/.github/workflows/kani.yml

Setting up something similar for Verifast might require you to package Verifast and its dependencies in a format that can be executed via a github action (docket container, etc.). This also may require a mechanism to identify which files need to be analyzed by Verifast (unless Verifast can quickly scan the repository and analyze relevant files). Ultimately the goal is to be able to block a CI pipeline on proof failure.

Once the PR is merged, the tool is considered integrated.

The repository will be updated periodically, which can impact the tool capacity to analyze the new version of the repository. I.e., the action may no longer pass after an update. This will not impact the approval status of the tool, however, new solutions that want to employ the tool may need to ensure the action is passing first.

This means that modifications made to the code repo and break the github action will not cause the tool to lose approval, but will most likely trigger a support request from people who try to use the tool to complete some verification task and issue a PR that relies on Verifast.

[btj]

Many thanks for your guidance, Remi!! I will provide all of the requested information asap. Here is a first batch:

Architecture of VeriFast for Rust

I first explain the architecture of VeriFast for C, which existed first and which VeriFast for Rust extends.

Architecture of VeriFast for C

Frontend

• Abstract Syntax Trees for annotated programs (also used by VeriFast for Rust and VeriFast for Java) (this is used both for the raw parse tree and for the typechecked AST; node types that differ have a W in front to denote "well-typed")
• lexer used by VeriFast for Rust for tokenizing annotations
• parser for annotated C and Java (not used by VeriFast for Rust)

Core engine

• verifast1.ml: typechecking of struct definitions, inductive type definitions, expression, assertions, fixpoint function definitions, predicate definitions; building the symbol tables
• assertions.ml: producing and consuming assertions; auto-opening and closing of predicates and other automation
• verify_expr.ml: symbolic evaluation of expressions, including function calls, loads, and stores
• verifast.ml: symbolic execution of statements, verification of functions

For some more details, see the README.

Rust frontend

The Rust frontend essentially provides an alternative parser, providing the same kind of raw parse tree to verifast1.ml that the C parser provides. It gets called in verifast.ml for .rs files.

• rust_fe.ml launches bin/vf-rust-mir-exporter, a separate process written in Rust that uses rustc_driver to run the rustc frontend to obtain the drop-elaborated MIR for all function bodies, as well as the struct, enum, trait definitions, impl clauses, etc. and export it to stdout in a binary Cap'n Proto format. Before the .rs file is given to rustc, it is preprocessed to turn VeriFast ghost commands into VeriFast_ghost_command() calls so that we can tell where the ghost commands belong in the MIR.
• rust_fe.ml then hands the Cap'n Proto message to vf_mir_translator.ml which translates it into a VeriFast parse tree which is then verified by the core engine.
• vf_mir_translator.ml calls into rust_parser.ml to parse annotations.

Notable functions in vf_mir_translator.ml include:

• translate_adt_def which translates Rust structs into VeriFast (C) structs but, if the user declares a custom type interpretation (i.e. custom OWN and/or SHR predicates) for a struct, also generates the proof obligations required by RustBelt: Ty-Share and Ty-Shr-Mono, as well as a few other ones (see the help page).
• gen_contract generates the precondition and postcondition for a Rust function not marked as unsafe that is implied by its Rust parameter types and return type, as prescribed by RustBelt

If the user provides an explicit spec for a Rust function that is not marked as unsafe, VeriFast will check that the provided spec implies the generated spec. Since this implication check does only very limited logical reasoning, both specs mostly have to match syntactically. Therefore, look at the provided specs in linked_list.rs (grep for @ req) to get an idea of what the generated specs look like.

Prelude and standard library specs

Besides the source code for VeriFast for Rust, the other important ingredient is the prelude (the set of definitions always implicitly imported) and the specifications used for the standard library.

• prelude.rsspec is the prelude. It include!s the following:
• prelude_core.rsspec: core memory model definitions
• aliasing.rsspec: definitions for modeling shared references and mutable references, i.e. the aliasing restrictions. Note: this is work in progress; VeriFast is not yet fully sound in this regard.
• rust_belt/general.rsspec: some Iris and RustBelt definitions
• rust_belt/lifetime_logic.rsspec: the axioms of the lifetime logic, as published in Ralfs thesis, with some additions by ourselves whose soundness we consider plausible but have not yet proven formally.
• std/lib.rsspec provides specs for a few standard library constructs

Test suite

The VeriFast CI runs testsuite.mysh, which runs most of the examples in examples and tests. All of the Rust examples and test cases are in tests/rust; the command lines are in tests/rust/testsuite.mysh. See the README for more info.

The test suite has only a few negative test cases (look for -allow_should_fail on the command line), but VeriFast does report dead code as an error, so if an unsoundness were to cause it to think incorrectly that some code was unreachable, that would be detected. One way to get some assurance of soundness is to do mutation testing: tweak a test case and observe that VeriFast fails.

Soundness of VeriFast for Rust

The soundness property we are targeting with VeriFast for Rust is that if verifast -c lib.rs exits with exit code 0, then no purely safe (i.e. containing no unsafe blocks) Rust program that links against library crate lib.rs has undefined behavior. (This is called soundness of a library.) The following caveats apply:

• Any assume calls in lib.rs must be audited carefully; incorrect assume calls will of course break soundness. Fixed
• VeriFast for Rust does not yet check that lemma functions have a body. A lemma function without a body is an axiom. Fixed
• VeriFast for Rust should currently check all requirements in the Rust reference, except for the aliasing restrictions ("the pointer aliasing rules"). Since it currently treats mutable references like raw pointers, it also does not yet check that mutable references are always properly aligned and non-dangling. (It does check that loads and stores are properly aligned.)
• There are some known unsoundnesses. There are also probably some unknown unsoundnesses, since unlike some other tools, such as RefinedRust, VeriFast is not foundational. A bug anywhere in the codebase or in the prelude or standard library specs could lead to unsoundness. Any unsoundnesses that become known should be documented as issues with the unsoundness label.
• Since VeriFast for Rust uses the rustc frontend, which assumes a particular compilation target architecture, VeriFast for Rust's result will only hold for the current target architecture.

[btj]

For the GitHub action, one approach would be to have a parallel source tree below a verifast directory, containing for each file path/to/file.rs in the codebase for which a VeriFast proof has been done, a file verifast/path/to/file.verifast.orig.rs which is initially just an exact copy of path/to/file.rs, and a file verifast/path/to/file.verifast.rs which is an annotated version of verifast/path/to/file.verifast.orig.rs. The GitHub action would run VeriFast on verifast/path/to/file.verifast.rs and would also do one of two things:

• Option A: fail if path/to/file.rs is not exactly equal to verifast/path/to/file.verifast.orig.rs.
• Option B: compute the diff from verifast/path/to/file.verifast.orig.rs to verifast/path/to/file.verifast.rs, try to apply this patch to path/to/file.rs, and run VeriFast on the resulting file.

Option A is simpler but causes more CI failures; Option B will allow the action to succeed in case changes occur that do not affect the annotated/verified parts of the file.

It's not clear that option B is worth the trouble. Perhaps it is best if we simply do Option A for now; if it turns out this causes too much noise, we can still move to Option B later?

[btj]

The fact that verifast/path/to/file.verifast.rs is an annotated version of verifast/path/to/file.verifast.orig.rs cannot be checked fully automatically, for now, unfortunately, because some minor changes to the code are generally necessary. Maintainers should check that the code changes are safe. To keep them from forgetting to do that, we could also check in verifast/path/to/file.code-changes.diff, which is checked to be the diff from verifast/path/to/file.verifast.orig.rs to a version of verifast/path/to/file.verifast.rs from which the VeriFast annotations have been stripped using the vfstrip utility that ships with VeriFast. Any changes to the code changes would then show up clearly in the PR and could be reviewed easily.

[btj]

Running VeriFast in CI is as simple as downloading the Linux binary release, extracting it to anywhere, and running bin/verifast; no need for a Docker container.

I'm afraid there are no papers or other documentation specifically on VeriFast for Rust yet; a tutorial is in preparation.

I think this addresses your questions. If you need anything else, just let me know.

[btj]

I thought I'd add the following guide to the reader of the core engine source code:

• the core engine is parameterized by the type typenode of SMT solver type nodes (either type_bool, type_int, type_real, or type_inductive), the type symbol of SMT solver function (or constant) symbols, the type termnode of SMT solver terms, and the value ctxt, of type context, giving access to the SMT solver itself. The default SMT solver is Redux (a partial re-implementation of the venerable Simplify SMT solver), which uses simplex.ml to deal with linear inequalities, but the user can select Z3 version 4.5 by specifying -prover z3v4.5 on the command line.
• In verifast1.ml, the various symbol tables (called "the maps") are built, including the structmap of C/Rust structs, the inductivemap of inductive types, the predfammap of predicate family definitions, the predinstmap of predicate family instance definitions (a regular predicate definition defines both a predicate family of zero indices and the family's sole predicate instance), etc. Their types are here.
• I try to use particular variable names for particular things. In particular:
  • h: a symbolic heap, of type termnode heap = termnode chunk list
  • env: a symbolic store, of type termnode env, an association list mapping the name of each local variable name in scope to its symbolic value
  • tenv: a type environment, of type ( string * type_ ) list, mapping the name of each local variable in scope to its type
  • ghostenv: of type string list, the list of the names of the ghost variables in scope. Used to check that ghost code does not perform assignments to real variables.
  • l: a source location, of type loc
  • cont: a continuation (type varies). The symbolic execution engine is written in continuation-passing style so that symbolic execution can be forked when multiple branches need to be considered
• Some notable functions:
  • check_pure_type_core: resolution of type expressions (of type type_expr) to types (of type type_)
  • expect_type_core: subtyping check
  • check_expr_core_core: type checking of expressions
  • check_asn_core: type checking of assertions
  • eval_core_cps0: symbolic evaluation of pure (i.e. non-heap-dependent non-side-effecting) expressions
  • produce_asn_core_with_post: production of assertions
  • consume_asn_core_with_post: consumption of assertions
  • verify_call: symbolic execution of function calls
  • verify_expr: symbolic evaluation of expressions. It has the following notable nested functions:
    • lhs_to_lvalue: symbolically evaluating a place expression to a place
    • read_lvalue: loading a value from an lvalue (i.e. a place)
    • write_lvalue: storing a value to a place
  • verify_stmt: symbolic execution of statements
  • verify_func: verification of functions

[remi-delmas-3000]

@btj thanks a lot for all the leads. Currently looking for auditors, will post updates here.

[remi-delmas-3000]

@btj I'm posting the outcome of the Verifast code audit here for visibility. A big thank you to Rob Dockins (https://github.com/robdockins), Jason Hu (https://hustmphrrr.github.io/), @thanhnguyen-aws , @markrtuttle for conducting the audit !

Audit of Rust datatype layout assumptions

1. Verifast assumes C layout in all cases, even if no repr(C) attribute is present:

fixed by verifast/verifast#665, VeriFast no longer makes any assumptions about Rust struct layout except that in single-field structs, the field is at offset zero and the struct has no padding

Audit of lifetime_logic.rsspec (Thank you Thanh Nguyen, Jason Hu)

1. For each derivation rule in the paper, there are two corresponding lemmas: one for atomic and one for non-atomic. The non-atomic version is consistent with what described in the paper. The atomic version includes some requirements about atomic_mask, which I don’t understand clearly, but everything else is consistent with the non-atomic version.

The 'atomic_mask' corresponds to Iris' notion of masks. (Iris is the logic that the lifetime logic and RustBelt are built on top of.) Notice that most of the lifetime logic rules are viewshifts at mask Nlft. The nonatomic versions are marked as 'nonghost_callers_only' which means they can only be called from real code, which implies the mask is Top.

2. Verifast's lifetime logic defines some open/close_borrow lemmas that cannot be found in the Rustbelt paper. It seems these lemmas are applied when we access the data through the borrowing references.

Lemma open_full_borrow corresponds to LftL-bor-acc (Fig. 11.1 on p142 in Ralfs PhD thesis https://research.ralfj.de/phd/thesis-screen.pdf). Note: this rule uses accessor syntax, defined in Sec. 5.6 on p73. Notice that an accessor is a magic wand that yields another magic wand. The first magic wand is open_full_borrow, the second one is represented by the close_full_borrow_token and is applied by calling close_full_borrow. Notice, by the way, that in LftL-bor-acc, on the right-hand side of the accessor P is under a 'later' modality (\triangleright P). In VeriFast, this modality is not needed because ghost statements can be thought of as 'taking a step', so the step of opening the borrow gets rid of the later. (The same is true in F* https://fstar-lang.org/ .)

3. In general, the separation logic implemented in Verifast simplified compared to the IRIS version. For example, in IRIS, there are various modalities due to step indexing and different implication connectives like magic wands, classical implications, and view shifts. It is a little bit unclear whether these simplifications are problematic, or they are there for the technical reasons to make Coq happy. Given that Iris is obviously sound, are simplifications in Verifast also sound? Do we have a clear understanding about this or do we have a separate semantic model for this simplified separation logic somewhere?

See my comment about the later modality above. I can go into more detail if desired. I will include a discussion of this in the linked_list.rs paper that I'm working on. A viewshift is encoded into VeriFast as a lemma. But yes, it would be good if there was a document that went into detail on the soundness of VeriFast's separation logic. While various aspects of it have been formalized in various papers (and even mechanized in Coq) (such as https://people.cs.kuleuven.be/~bart.jacobs/finegrained/ and https://people.cs.kuleuven.be/~bart.jacobs/unload/ ) no thorough, comprehensive account of VeriFast's separation logic exists yet. It's high on my TODO list.

4. In Verifast, I see that there are two way of defining a predicate: the pred keyword and a fix that returns a bool. I imagine that the latter approach is for computable predicates, expect that often the fix is not undefined. Meanwhile, in lambda rust, everything is defined uniformly as iProp, which I believe correspond to pred in Verifast. I think this distinction should be sorted out.

'pred' defines a separation logic predicate which may assert ownership of resources (like an Iris iProp). 'fix' is a pure function (like a Coq Fixpoint); it cannot assert ownership of resources. A fix returning bool is like a Coq Prop.

5. In liftime_logic.rsspec, many lemmas use && instead of &*&. I believe the former is conjunction and the latter is separating conjunction. According to Ralf Jung’s thesis, it should be the latter because life time is a resource. I am not sure whether it matters in the context of Verifast or not. This bullet is related to the previous one.

That is correct. First of all, note that && binds more weakly than &&. Secondly, && operates on spatial assertions (iProps) and && operates on pure bool expressions (Props). (bool expressions can be used where spatial assertions are expected but not the other way around.)

6. In liftime_logic.rsspec also defines the strong versions of those lemmas, which involves opening/closing a borrow for a lifetime, which is included in another lifetime, and some lemmas for converting the predicates after closing a borrow.

open_full_borrow_strong corresponds to LftL-bor-acc-strong (Fig. 11.8 on p155).

7. Many updates/view shifts are captured by close_tokens, due to the lack of an internal representation of view shifts, I assume.

That is correct.

8. is_full_borrow_convert_strong is not defined? Looks like a typo of full_borrow_convert_strong. (maybe due to lem_type?)

Yes. For each definition of a lemma type T, VeriFast automatically introduces a predicate is_T that asserts that a given lemma has type T.

3. There are some extra lemmas that are trivially correct: lifetime_inclusion_trans, lifetime_inclusion_glb, full_borrow_mono, ...
4. There are lemmas for the “&*&” operators, which are not in RustBelt paper.

Audit of the underlying logical framework (Thank you Rob Dockins)

1. One of the allowed termination criteria is “induction on heap size.” This seems to assume that the “subheap” order has no infinite descending chains. Given that verifast has a model of fractional permissions, I don’t think this is true, and I wonder about the soundness of this. My first attempt to exploit this is rejected, so perhaps this is sound, after all. The error message seems to indicate that only “full field chunks” are acceptable for termination. For the record here is my attempt:

/*@

lemma void junk(int* p, real n)
  requires [n]integer(p,0);
  ensures false;
{
  assert [n/2]integer(p,0) &*& [n/2]integer(p,0);
  junk(p, n/2);
}

@*/

Indeed; for purposes of lemma termination, heap size is defined as the number of full/whole fields (i.e. with coefficient 1) present in the heap.

2. Looking into the Rust translator front-end (mostly in verifast/src/rust_frontend/vf_mir_translator), the code suffers from a very low comment:code ratio (common in OCaml projects for reasons I have never understood), and the main source file vm_mir_translator.ml is a quite large, mostly-monolithic module. This makes it pretty difficult to suss out the organizational structure. That said, the overall code seems reasonably well-engineered. I don’t see lots of skipped cases or horrible kludges.

Indeed; some technical debt has built up. I should go through and split some large functions up, and otherwise make the code more self-documenting and/or add comments.

3. There isn’t much in the way of unit tests, but the integration tests seem to do a reasonable job of exercising features and incorporate some negative tests as well (something I always look for in a formal reasoning tool). I echo Remi’s concern about struct/enum layout. It isn’t clear to me where/if struct layout information from rustc is incorporated. Rust can (and actually will, in some cases) do clever things to use less space for layouts, including collapsing nested enum types into a single representation and reordering struct fields to reduce padding. Overall, this appears to be in significantly better shape than what one generally expects of “research” software. I’d like to see some more modular refactoring and an overall better effort to maintain internal comments, but I don’t see any obvious soundness red flags. It’s difficult to get a complete picture of a project of this scale in a short time, but I’m mostly happy with what I see.

SMT solvers

1. @btj Could Verifast work with more recent versions of z3 than v4.5 (there's been a some soundness fixes in z3 between v4.5 and the current v4.13.4) ?

Main TODOs and takeaways

1. Produce a document (preferably a peer-reviewed publication) that gives a comprehensive account of VeriFast's logic, argues its soundness, and compares it to Iris.
2. Make the VeriFast codebase, and vf_mir_translator.ml in particular, easier to audit, by improving modularity, adding comments, etc.

[remi-delmas-3000]

@btj About the CI workflow, summarizing my understanding in this diagram:

+---------+    +----------------------+    +----------------+    +---------------------+
| lib.rs  |    | lib.verifast.orig.rs |    | lib.verifast.rs|    | code_changes.diff.  |
+---------+    +----------------------+    +----------------+    +---------------------+
    |                 |                           |                          |
    |    +------------+                           |                          |
    |    |            |                           |                          |
    |    v            |                           v                          |
+----------+          |                     +----------+                     |
| diff     |          |                     | vfstrip  |                     |
+----------+          |                     +----------+                     |
       |              |                           |                          |
       v              |                           |                          |
     FAIL             |                           v                          |
                      |                     +-------------------------+      |
                      |                     | lib.verifast.stripped.rs|      |      
                      |                     +-------------------------+      |
                      |                           |                          |
                      |                           |                          |
                      +----------------------+    |     +--------------------+
                                             v    v     v
                                       +------------------+  
                                       | Compare diff     |----> FAIL if unexpected code diff
                                       | with lib.rs     |     
                                       +------------------+
                                             |
                                             | (if no diff)
                                             v
                                       +------------------+
                                       | Run VeriFast     |
                                       | verification     |
                                       +------------------+
                                             |
                                             v
                                       +------------------+
                                       | Success/Failure  |
                                       | based on         |
                                       | verification     |
                                       +------------------+

I get that right now and in the near future verifast annotations are not going to be part of the upstream code, but how hard/easy do you think it will be to propagate upstream changes from lib.rs to lib.verifast.rs ?

• lib.rs is the upstream standard library source code
• lib.verifast.orig.rs is a copy of lib.rs
  • a non-empty diff between this file and lib.rs indicates that the proof artifacts are outdated.
• lib.verifast.rs: lib.rs + verifast proof annotations + verifast-specific code changes
  • if after stripping annotations with vfstrip we have an empty diff with lib.verifast.orig.rs, we can proceed with the proofs;
    • I don't really see the usefulness of lib.verifast.orig.rs, why not diff directly lib.verifast.rs with lib.rs ?
  • if after stripping annotations we have a code diff with lib.verifast.orig.rs, we check that differences are the one we expect by comparing the diff with code_changes.diff. which contains expected code changes.
    • looking at diffs of diffs is way too cumbersome for potential users/maintainers.

The checking done here seems sound in principle, but I think it is going to be very hard for users to propagate upstream changes from lib.rs to lib.verifast.rs.

Admitting the proof artifact consists of an fully annotated copy of the upstream lib.rs file, we need to at least support a practical way to git pull from the latest lib.rs into lib.verifast.rs or to git rebase the file lib.verifast.rs on top of the latest lib.rs without having to look at diffs of diffs.

We also cannot ask upstream developers to change their code solely for compatibility single verification tool, if this could be avoided by updating to tool itself.

[btj]

Produce a document (preferably a peer-reviewed publication) that gives a comprehensive account of VeriFast's logic, argues its soundness, and compares it to Iris.

A draft paper is here.

[remi-delmas-3000]

Update: @btj is now working on a CI check using semantic refinement checking instead of textual code diffs:

• the proof-annotated may (and most likely will) still contain code changes needed to open new scopes, desugar expressions to insert proof annotations where needed
• a verifast will check that the upstream file refines the proof-annotated file, i.e. that all behaviours of the upstream file are also behaviours of the proof-annotated file.
• This will make CI check robust to upstream source modifications that don't change program semantics, and allows to apply semantics preserving (or introduce abstraction) to conduct proofs.

[btj]

Update: my refinement-checker tool is now capable of verifying(*) refinement of original and verified versions of linked_list.rs's unlink_node function. I prepared a version of the linked_list.rs proof that retains only the proof of unlink_node, i.e. where the entire verified file (after collapsing comments) is identical to the original file, except for function unlink_node. refinement-checker checks for each function that the original version and the verified version either have identical source code or that one refines the other. It also checks that, apart from the refinement-checked functions and comments, the files are identical. As a result, I believe refinement-checker is sound.

I will do some finishing touches and then update the PR to include this refinement-checked unlink_node proof, probably tomorrow.

(*) refinement-checker, like VeriFast itself, is non-foundational, so bugs may exist that impact soundness. Any soundness bugs that are discovered should be recorded in the VeriFast issue tracker as issues with label unsoundness.