Add VeriFast CI

[btj]

Adds a GitHub Actions workflow that downloads VeriFast and runs verifast-proofs/check-verifast-proofs.mysh. (mysh is a simple tool that ships with VeriFast for running simple scripts. It is optimized for running test suites (and used to run VeriFast's test suite. Works on Linux, Mac, and Windows.)

See #238 to see how this can be used to verify the linked_list.rs (Challenge 5) solution.

Resolves#213

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[remi-delmas-3000]

@btj do you think you could add a simple proof example in ./verifast-proofs and implement the diff and tool invocation logic in check-verifast-proofs.mysh ? We'd like to be able to check that the action runs/fails/succeeds at least once. A positive and a negative example would be great

[btj]

I'm developing a "refinement checker", a simple tool that checks that one .rs file F1 is a "refinement" of another one F2. This means that for every function f in F1, and for every execution of F1, function f in F2 has a matching execution. It follows that if F2 has been verified to have no "bad"/unsafe executions, F1 also has no bad executions. This tool should support the kinds of changes that I have made in linked_list.rs. If this works, this solves the diff problem: there will no longer be a need for maintainers to manually check diffs for "soundness". Instead, it will suffice to run this tool on the original file and the verified file.

[btj]

I just pushed a first version of the refinement checker: test suitesource code. For now, it supports only a tiny subset of MIR constructs: just function calls and local-to-local assignments.

[btj]

Hi @remi-delmas-3000 , I think I addressed all of the issues you raised. I'll leave it to you to resolve the conversations or otherwise follow up.

[remi-delmas-3000]

@btj Tthanks a lot for all the modifications !
We may just want to separate negative tests and positive tests in two separate actions to avoid systematically failing CI with negative tests.

• The positive test action succeeds on proof success, fails otherwise,
• The negative tests action succeeds on diff or verification failure, fails otherwise.

Need to split action into expect success/expect failure actions

[remi-delmas-3000]

@btj This repository is already a copy of the upstream repository, so we'd like to avoid extra copies that are not strictly necessary. That's the last request we have for this PR. We could avoid making a full copy of the library file, and instead use a git command to diff library.rs at the current HEAD and at some previous commit hash ? The annotated file could store the hash commit of its corresponding upstream file instead:

/* UPSTREAM "path/to/file.rs" "abc123...." */

And we run something like that to diff that reference hash with the current head.

#!/bin/bash# Function to check if a test file's referenced source matches its specified commit# Parameters:# $1: test file path# Returns:# 0 if source file matches the committed version# 1 if differences found or any error occurscheck_test_source() {
local annotated_file="$1"# Check if test file existsif [ !-f"$annotated_file" ];thenecho"Error: Test file $annotated_file not found"return 1
}
# Extract source file and hash from UPSTREAM commentlocal pattern='/\* UPSTREAM "\([^"]*\)" "\([^"]*\)" \*/'local extraction=$(sed -n "s|$pattern|\1 \2|p""$test_file"| head -1)# Check if extraction succeededif [ -z"$extraction" ];thenecho"Error: Could not find UPSTREAM comment with file and hash in $annotated_file"return 1
}
# Split extraction into source_file and hashread -r source_file hash<<<"$extraction"# Check if source file existsif [ !-f"$source_file" ];thenecho"Error: Source file $source_file not found"return 1
}
# Check if the hash exists in git historyif! git rev-parse --quiet --verify "$hash">/dev/null;thenecho"Error: Commit $hash not found in repository"return 1
}
# Compare the file between the hash and HEADif git diff "$hash" HEAD -- "$source_file">/dev/null;thenecho"WARNING: $source_file has changed since commit $hash"return 1
elseecho"OK: $source_file matches the version at commit $hash"return 0
fi
}

The refinement check could then directly run against the upstream file ?

@carolynzech does that match your idea?

[carolynzech]

@carolynzech does that match your idea?

Yes. Any solution that avoids adding extra copies is fine--the proof-annotated copies are okay, since those require actual code changes to insert ghost code. But there shouldn't be any need to copy the original files; we should be able to reference those from git history alone. The git solution 1) prevents the size of this repository from exploding and 2) provides a record of how the verified files fit into the history of the upstream repo. I recommend looking at Kani's setup for how to organize it--you could add a script of your own to scripts/ with this logic, and add the configuration file with the commit hashes to the tool_config/ folder. You could reference the upstream/master branch of this repository, which mirrors the upstream master branch of Rust.

I had a few other comments as well:

1. Why do these empty tests.rs files exist? It seems like this is another thing that could be created as a temporary file during CI and then deleted; I don't see a reason to merge empty files into the repo.
2. As long as you're implementing the git-based approach Remi outlined, I recommend decoupling the CI from a particular version of Verifast / Rust toolchain, and instead having configuration files with the versions in tool_config/ that the CI workflow reads from. You can also use logic like this to read the toolchain date from the rust-toolchain file instead of hardcoding it. But this is optional and a non-blocker for this PR.

[btj]

Let me try to understand. The current file structure of the example linked_list.rs proof in verifast-proofs/alloc/collections is as follows:

linked_list.rs
original
lib.rs
linked_list.rs
linked_list
tests.rs
verified
lib.rs
linked_list.rs
linked_list
tests.rs

Here, lib.rs serves as a crate root for verification. (I want to avoid passing the entire alloc crate to rustc and to VeriFast's MIR exporter; this alternative crate root has linked_list as its only module.) original/lib.rs and verified/lib.rs are identical; this is important because refinement-checker checks that the two crate source trees are entirely identical, apart from comments and apart from the functions that are refinement-checked. Also, original/linked_list.rs is identical to the real file in library/alloc/src/collections. Since that file has a tests module, we need a tests module here too, hence the tests.rs file.

Now, if I understand correctly, you are objecting to the presence of original/linked_list.rs in the repo, given that it is an exact copy from library/alloc/src/collections/linked_list.rs. You are proposing that this file instead be retrieved from git history at CI time? Similarly, you are proposing that tests.rs be generated at CI time.

While this is definitely feasible, I would like to double-check if you really think this is better than the current approach. A big advantage of the current approach, IMHO, is simplicity: fewer moving parts. The file structure that you get from checking out the repo is immediately ready for running VeriFast (which needs verified/linked_list/tests.rs) and for running refinement-checker (which needs all of the files). If some of the files are generated, someone who wants to run VeriFast or refinement-checker manually will also first need to generate the files.

While I applaud your optimism regarding how fast verifast-proofs will grow, I don't expect that the size of this subtree will be at all significant in the near term. (Note also that since git's object store is content-addressed, the copies do not take extra space in the git repo. They do, however, indeed take extra space in the checked-out working copy.)

Having said all this, I will of course implement the requested changes if confirmed.

[carolynzech]

@btj Your comment was helpful--I think I got a bit confused trying to map the abstract examples in the README to the actual files you're adding here. I think I understand the reason for the copies now, and I'm okay with them.

I added an "Example" section to the README inspired by your comment; I think a more explicit example is useful here. Feel free to make any changes as you see fit, then I'm good to merge.

[btj]

Many thanks, @carolynzech ! The edits to the README you suggested will indeed be very useful to readers; I applied them almost verbatim.