Open
Conversation
Also required some additional annotations to satisfy low control flow. This might require modifications to previous packages
This package verifies successfully except for `scion_test`. Furthermore, there are some problems with "surrounding" packages
Where possible implement as true, otherwise add proper TODO.
Before, some triggers contained `end-start`; however, this leads to invalid triggers in the Viper encoding. I replaced these by `len(s[start:end])`.
In the same vein, I resolved the remaining verification issues - I verified scion_test.gobra as this turned out simpler than expected - The other issues did not stem from Gobra issue #948, but rather from me adding postconditions to some methods of the `Path` interface which weren't satisfied by other implementing types
As `IsLowDecodingLayer` was more widely used and has a more general form, I decided to rename: - `SerializableLayer.IsLow` -> `SerializableLayer.IsLowSerializableLayer` - `DecodingLayer.IsLowDecodingLayer` -> `DecodingLayer.IsLow`
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
It turned out that verifying
pkg/slayers/scion_test.gobrawas fairly trivial, and that the failing implementation proofs were not related to Gobra issue 948 -- I just needed to re-verify the already verified packages considering the changes to thePathinterface. Thus, this should now verify completely.This PR still contains workarounds for Gobra issues 846, 888, 946, and 955.
scion_spec.gobra, I commented out apackageclause due to issue 946; in other cases, I tried to model the effect of the package clause by exhaling/inhaling the appropriate definitions. As explained in a TODO there, this has not been done here (yet), as I didn't deem this worth the effort here (considering it is just a workaround).IsLowSlicefunction andfix-846(cf. Usefix-846and implement hyper functions for abstracting over sensitivity #10).Furthermore, I added contracts in
pkg/slayers/path/scionwhich have not been verified yet (as the package has not been verified yet, either).