Hi @jcp19, thank you for creating this PR, this is quite exciting!

Reviewable status: 0 of 4 files reviewed, 7 unresolved discussions (waiting on @jcp19 and @oncilla)

.github/workflows/gobra.yml, line 14 at r1 (raw file):

        uses: actions/checkout@v2
      - name: Verify the specified files
        uses: viperproject/gobra-action@main

Could we pin a specific version so that when there are breaking changes to the actions does not break our builds globally? And also pin imageVersion.
This would allow to keep using the older version until we explicitly update the version and update all the annotations.

.github/workflows/gobra.yml, line 15 at r1 (raw file):

      - name: Verify the specified files
        uses: viperproject/gobra-action@main
        with:

If a developer wants to run the verifier locally, either when adding new annotations or when changing annotated code, it would be helpful if there was a clear way to run the verifier with the same settings as this github action.
Is there an option to specify the settings in this block in a configuration file in the repository instead? Then we could e.g. add a make verify target to run the verifier locally, very similar to how we currently run golangci-lint.

Speaking of linters -- would it be at all reasonable to integrate this verifier into our build system by integrating it as a linter pass, e.g. in nogo? Not now, I mean, but for later.

.github/workflows/gobra.yml, line 25 at r1 (raw file):

          packages: 'path'
          # Gobra only verifies files annotated with the header "// +gobra"
          headerOnly: '1'

These settings appear redundant; if only // +gobra files are verified, why do we also need to specify srcDirectory, and packages?
FWIW, to me it would also work to just have an explicit list of files that are to be verified.

.github/workflows/gobra.yml, line 34 at r1 (raw file):

        with:
          name: cache
          path: ${{ runner.workspace }}/.gobra/cache.json

I'm not very familiar with github actions; my superficial understanding is that this only stores the cache artifact, but it never appears to be "consumed". Should this use actions/cache instead? Or how does this work?

.github/workflows/gobra.yml, line 34 at r1 (raw file):

        with:
          name: cache
          path: ${{ runner.workspace }}/.gobra/cache.json

Should we also upload the report?

pkg/slayers/path/hopfield.go, line 95 at r1 (raw file):

	//@ assert forall i int :: { h.Mac[:][i] } 0 <= i && i < len(h.Mac[:]) ==> acc(&h.Mac[:][i])
	//@ assert forall i int :: { raw[6:6+MacLen][i] } 0 <= i && i < len(raw[6:6+MacLen]) ==>
	//@     acc(&raw[6:6+MacLen][i], 1/2)

These asserts here and also in the simpler cases above just seem to describe the semantics of the slice syntax for every occurrence. Will gobra eventually be able to "understand" this on it's own? It looks entirely mechanical to me, and a comment block of this size is certainly distracting.

pkg/slayers/path/hopfield.go, line 96 at r1 (raw file):

	//@ assert forall i int :: { raw[6:6+MacLen][i] } 0 <= i && i < len(raw[6:6+MacLen]) ==>
	//@     acc(&raw[6:6+MacLen][i], 1/2)
	copy(h.Mac[:], raw[6:6+MacLen] /*@, perm(1/4)@*/)

I don't understand this fractional bookkeeping. What is the difference between 1/2 and 1/4? Why not just read?

Reviewable status: 0 of 4 files reviewed, 6 unresolved discussions (waiting on @jcp19, @matzf, and @oncilla)

.github/workflows/gobra.yml, line 34 at r1 (raw file):

Yes, you are totally correct. I fixed it in the meanwhile

.github/workflows/gobra.yml, line 34 at r1 (raw file):

Done

Reviewable status: 0 of 5 files reviewed, 6 unresolved discussions (waiting on @matzf and @oncilla)

.github/workflows/gobra.yml line 14 at r1 (raw file):

I have now fixed the version of the gobra-action used in the CI. Here, we don't need to pin the imageVersion, as the selected version for the gobra-action already uses a fixed version of Gobra if none is specified.

.github/workflows/gobra.yml line 15 at r1 (raw file):

Right now, there is no direct way to do this, although it is something that I would like to do in the near future. I really like your suggestion to try to integrate it as a linter pass in nogo. For the time being, I think that the easiest way to run gobra locally with the given configuration is to use something like act to run the Github action locally.

.github/workflows/gobra.yml line 25 at r1 (raw file):

Yes, they are redundant but they were required in a previous version of the action. In the time since the review, we made extensive improvement to the action and gobra, making it possible to not provide these options.

pkg/slayers/path/hopfield.go line 95 at r1 (raw file):

You are right that these assertions are distracting and can be obtained mechanically. However, they are still required for Gobra to verify these files. Addressing this in Gobra requires extensive changes to our encoding of the slices, which is on our mid-term plans. I will update these files as soon as these annotations are no longer required.

pkg/slayers/path/hopfield.go line 96 at r1 (raw file):

For practical purposes, the most crucial point is that both permission amounts (1/2 and 1/4) allow reading a value from a heap location, but not writing to it. For consistency, I now use the same fraction in all places where a "read" permission is required, when possible. Using read here though is not the same as using one of these fixed amounts. read stands for an existentially quantified positive value. Different occurrences of read in the spec of a method are thus not guaranteed to stand for the same permission value. Because of this, the following example fails to verify:

package f

// `_` here stands for the `read` permission
//@ requires acc(x, _)
//@ ensures  acc(x, _)
func getValue(x *int) int {
	return *x
}

func main() {
	x := new(int)
	//@ assert acc(x)
	_ = getValue(x)
	// The following assertion fails:
	// Gobra cannot guarantee that the
	// permission amount transferred back
	// from `getValue` is the same as the
	// amount transferred to it.
	//@ assert acc(x)
}

The same example succeeds when _ is replaced by a fixed permission amount:

package f

//@ requires acc(x, 1/2)
//@ ensures  acc(x, 1/2)
func getValue(x *int) int {
	return *x
}

func main() {
	x := new(int)
	//@ assert acc(x)
	_ = getValue(x)
	// The following assertion
	// is verified successfully
	// now.
	//@ assert acc(x)
}

Reviewed 1 of 4 files at r1, 1 of 2 files at r3, 3 of 3 files at r5, all commit messages.
Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @oncilla)

.github/workflows/gobra.yml line 15 at r1 (raw file):

Ok 👍

.github/workflows/gobra.yml line 34 at r1 (raw file):

The path does not seem to match the expected file:

No files were found with the provided path: /home/runner/work/scion/.gobra/stats.json. No artifacts will be uploaded.

Note: in the gobra-action's docker invocation I see -v "/home/runner/work/scion/scion":"/github/workspace" (mismatch scion/scion vs scion/.gobra).

Nit: trailing whitespace

pkg/slayers/path/hopfield.go line 95 at r1 (raw file):

All clear, thanks 👍

pkg/slayers/path/hopfield.go line 96 at r1 (raw file):

Thanks for the explanation. This example makes sense to me. What I still don't quite understand is why we care about different permission levels in the first place. Does this represent something like concurrent readers?

Anyway, I'm resolving the discussion -- this is probably not the best forum to ask beginner questions about gobra 😄

Reviewed 1 of 4 files at r1, 1 of 2 files at r3, 2 of 3 files at r5, 1 of 1 files at r6, all commit messages.
Reviewable status: all files reviewed, 2 unresolved discussions (waiting on @jcp19 and @oncilla)

a discussion (no related file):
Hi @jcp19 . Great to see this work. Would it be possible for you to add comments on the individual specifications that describe in human language what is going on. Most people looking at this won't be familiar with verification let alone Gobra. It would be helpful to still understand roughly what's going on.

pkg/private/serrors/errors_spec.gobra line 27 at r6 (raw file):

ensures err != nil
decreases
func New(msg string, errCtx ...interface{}) (err error)

nit - missing newline

Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @jcp19 and @oncilla)

pkg/slayers/path/hopfield.go line 96 at r1 (raw file):

This is a very good point. Unfortunately, these fractional permissions are an artifact of our verification approach. There are other approaches that do away with this fractional book-keeping (e.g., https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/krml225.pdf), essentially only requiring distinguishing between 'read' and 'write' permissions, but we do not support them in Gobra yet.

Reviewable status: 3 of 5 files reviewed, 1 unresolved discussion (waiting on @jcp19, @matzf, @oncilla, and @shitz)

.github/workflows/gobra.yml line 34 at r1 (raw file):

This was actually caused by a bug in our Github action that was causing the verification statistics to not be produced. It is now fixed :)

Reviewable status: 0 of 5 files reviewed, 1 unresolved discussion (waiting on @matzf, @oncilla, and @shitz)

a discussion (no related file):

Hey @shitz. I've incorporated small descriptions of the contracts of every specified method which hopefully will make it easier to understand what the specs mean. At the same time, I avoided deep descriptions of the features of Gobra (like the permission model) in order to make these comments easy to grasp. Feel free to let me know if you think that the comments should be more detailed. Additionally, I tried to interleave specification clauses with sentences describing their meaning. Let me know if this style works for you.

Reviewed 1 of 2 files at r7, 4 of 4 files at r8, all commit messages.
Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @jcp19 and @oncilla)

a discussion (no related file):

Very nice, thank you!

.gitignore line 95 at r8 (raw file):

*.vpr
tmp/
logger.log

Where does tmp/ and logger.log come from?

Reviewable status: all files reviewed, 1 unresolved discussion (waiting on @oncilla and @shitz)

.gitignore line 95 at r8 (raw file):

These are just some additional files generated by Gobra when you verify the code. tmp basically contains some .smt2 which correspond to the proof obligations that Gobra ends up passing to an smt solver, which is sometimes (although very rarely) useful for debugging. I can remove these files from the .gitignore if you think they should not be here.

Reviewable status: complete! all files reviewed, all discussions resolved (waiting on @oncilla)

.gitignore line 95 at r8 (raw file):

If gobra creates them we should ignore them (note beside I think it should use the designated temp folder based on the OS it's running on, but that's not something you can influence here)