Verify private/topology#2
Merged
Merged
Conversation
As for private/topology/underlay, I have added these to make the contracts more precise, as I anticipate I will need this for further verification Note that at the moment, we still need a lot of `assume` statements due to Gobra issues #831 and #832. Also, `LinkType.String` doesn't have an appropriate postcondition yet, as I couldn't assert (nor assume) low(err.Error()) for a low `err`.
Together with the assumptions, I also moved `LowBytes` to a dedicated folder: `verification/util/sif`
…into sif-private-topology
…rifiedSCION into sif-private-topology
henriman
marked this pull request as ready for review
June 27, 2025 08:49
Due to the change in the contract of serrors, the workaround is not necessary anymore
jcp19
reviewed
Aug 6, 2025
Owner
Author
|
@jcp19: besides addressing your feedback, I have added |
jcp19
approved these changes
Aug 14, 2025
Collaborator
|
LGTM. Please address my comment and then you can merge this |
Issue 831 is fixed by PR 961
Collaborator
|
Is there any issue blocking the merging of this or the other PRs? |
henriman
changed the base branch from
sif-private-topology-underlay
to
sif-io-spec
September 19, 2025 08:16
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
2 participants
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.
Issue #13 has been opened to keep track of the assumption still present here.