Skip to content

Verify pkg/addr#3

Closed
henriman wants to merge 20 commits into
sif-private-topologyfrom
sif-pkg-addr
Closed

Verify pkg/addr#3
henriman wants to merge 20 commits into
sif-private-topologyfrom
sif-pkg-addr

Conversation

@henriman

@henriman henriman commented Apr 14, 2025

Copy link
Copy Markdown
Owner

Still contains workarounds for bugs:

  • (832) String of low byte slice is low; see LowSliceImpliesLowString in verification/utils/sif/assumptions.gobra
  • (835/890) Slice created from low values is low

TODO before merge:

  • Align contract clauses (I haven't done so yet in order to make the diff more useful)
  • Rebase to sif-io-spec
  • Open issue regarding possibly insufficient sensitivity preconditions for serrors

@henriman

henriman commented Jul 31, 2025

Copy link
Copy Markdown
Owner Author

I have added some improvements to sif-pkg-addr-rework beyond how to handle sensitivity with interfaces. For this reason, I will close this PR (and PR #4) and open a new PR (#5) for merging sif-pkg-addr-rework into sif-private-topology.

@henriman henriman closed this Jul 31, 2025
@henriman
henriman deleted the sif-pkg-addr branch July 31, 2025 17:22
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.

1 participant