experimental: add specifications to packages pkg/addr and pkg/slayers/path, verify them in the CI with Gobra
#4837
Conversation
jcp19
changed the title
pkg/addr package, verify it in the CI with Gobrapkg/addr and pkg/slayers/path packages, verify it in the CI with Gobra
jcp19
changed the title
pkg/addr and pkg/slayers/path packages, verify it in the CI with Gobrapkg/addr and pkg/slayers/path, verify the in the CI with Gobra
…package gobra/utils
jcp19
changed the title
pkg/addr and pkg/slayers/path, verify the in the CI with Gobrapkg/addr and pkg/slayers/path, verify them in the CI with Gobra
katyatitkova
changed the title
pkg/addr and pkg/slayers/path, verify them in the CI with Gobrapkg/addr and pkg/slayers/path, verify them in the CI with Gobra
katyatitkova
changed the title
pkg/addr and pkg/slayers/path, verify them in the CI with Gobrapkg/addr and pkg/slayers/path, verify them in the CI with Gobra
katyatitkova
changed the title
pkg/addr and pkg/slayers/path, verify them in the CI with Gobrapkg/addr and pkg/slayers/path, verify them in the CI with Gobra
|
I think what could be done is making this CI check optional: so it's still being run, but if it fails for any reason, it's still possible to merge the PR. Also, is there any link for Gobra 101? It could be useful if the check fails and the person seeing it is interested enough in fixing it |
Thank you for the idea, @katyatitkova. As suggested, I made the CI checks optional (with the option |
| func ParseFormattedAS(as string, opts ...FormatOption) (AS, error) { | ||
| // @ trusted | ||
| // @ requires false | ||
| func ParseFormattedAS(a string, opts ...FormatOption) (AS, error) { |
There was a problem hiding this comment.
as is currently a keyword of Gobra.
There was a problem hiding this comment.
Well, it's unfortunate considering that our code has a lot of variables called as... But it's OK I guess
| var ( | ||
| registeredPaths [maxPathType]metadata | ||
| strictDecoding bool = true | ||
| registeredPaths/*@@@*/ [maxPathType]metadata |
There was a problem hiding this comment.
There's another variable in this PR where the comment is added after a space. IMO, it looks better with a space, but I don't have a preference. But I think it's best to stick to one way to "style" this comment
There was a problem hiding this comment.
Good point, I agree! I added a space here :)
There was a problem hiding this comment.
Oops, turns out that this spacing is actually enforced by go-fmt. It looks like the comments after a variable identifier have different whitespacing depending on whether they occur in a single variable declaration or in declaration of multiple variables (https://go.dev/play/p/xhmKLzNbVtV).
| # (hopefully) informative error message, which identifies the parts of the code | ||
| # where the issues might lie. | ||
| # For more information on Gobra and its error messages, check the following: | ||
| # - The Gobra Book (WIP): viperproject.github.io/gobra-book/ |
There was a problem hiding this comment.
A feedback about the book itself, not this particular PR: the search there doesn't work with special characters, like @. Fortunately for me (a complete beginner with Gobra), I noticed that one chapter has @ in its name. But for people like me, the search bar might be a first place to go...
There was a problem hiding this comment.
Thank you! I added a feature request in the book repository (viperproject/gobra-book#43).
|
Looks good to me. I think we could try to merge these changes to see how it works in real life. Let's see what others will say |
2 participants
PR #4187 introduced Gobra to the SCION CI and added formal specifications to some files in the
pathpackage.Recently, in the context of an NGI Zero project, we have been looking at the possibility of adding more extensive formal specifications to the packages in the SCION repository, with the goal of bringing the specifications and proofs from the VerifiedSCION project, which formally verifies the router and its dependencies, to the upstream SCION implementation.
This PR makes more contributions in that direction. In particular, it introduces the following changes:
pkg/addrandpkg/slayers/paththat ensure memory safety and crash-freedom:pkg/addr: we specify and verify the functions and methods in filesaddr.go,host.go,isdas.goandsvc.go, except for functions that are used for testing purposes only (i.e., functions namedMustParseXXX). In addition, we specify and verifyfmtASin filefmt.go. A version of these annotations in an older version of SCION was useful in detecting a minor mistake (addr: missing bounds check #4080).pkg/slayers/path: it adds specifications topath.goto specify its functions and methods. Of interest, we add a specification to thePathinterface that over-approximates what all valid implementations ofPathmay do.We are aware that adding these annotations impose a high burden on developers, especially if these packages are expected to change often. Thus, we do not expect this PR to be merged as is. Nonetheless, we hope we can use it as a basis for continuing our discussion (@katyatitkova, @romshark) about strategies to progressively incorporate more formal methods in the SCION repository.