Skip to content

Verify pkg/addr#5

Merged
henriman merged 42 commits into
sif-io-specfrom
sif-pkg-addr
Sep 19, 2025
Merged

Verify pkg/addr#5
henriman merged 42 commits into
sif-io-specfrom
sif-pkg-addr

Conversation

@henriman

@henriman henriman commented Jul 31, 2025

Copy link
Copy Markdown
Owner

Issues #13, #14 and #15 have been opened to keep track of the assumptions still present here.

There still remain a lot of assumptions due to Gobra issues
Most notably sensitivity requirements in interfaces have been made
uniform
Note that the way `strings.Builder` is annotated may not be final
... in `fmt.Stringer` and `flag.Value`
This also allowed the removal of several workarounds for bugs 835/890
@henriman
henriman requested a review from jcp19 July 31, 2025 17:41
Comment thread pkg/addr/fmt.go Outdated
Comment thread pkg/addr/host.go Outdated
Comment thread verification/dependencies/net/ip.gobra
Comment thread verification/dependencies/strings/strings.gobra Outdated
@henriman
henriman requested a review from jcp19 August 5, 2025 19:11
@henriman

Copy link
Copy Markdown
Owner Author

@jcp19: I have addressed all your feedback now. The removal of the restriction len(ip) == HostLenIPv6 ==> ... on the lowness of ip necessitated adding IsLow to the precondition of HostAddr.Pack and HostAddr.IP. I also added && low(i) ==> to quantified assertions where appropriate. (In PR #10, I also already replaced most of these quantified assertions with calls to the corresponding hyper functions.)

@jcp19 jcp19 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, please look at my comment

Comment thread pkg/addr/host.go
@henriman
henriman changed the base branch from sif-private-topology to sif-io-spec September 19, 2025 08:31
@henriman
henriman merged commit d43f141 into sif-io-spec Sep 19, 2025
@jcp19
jcp19 deleted the sif-pkg-addr branch September 19, 2025 09:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants