Skip to content

[router] use mce on-demand #415

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
jcp19 wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

[router] use mce on-demand #415

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
50f2c52
[router] use mce on-demand
jcp19 Apr 27, 2026
aaf76b9
Update scion.go
jcp19 Apr 27, 2026
7039b31
Update ghost-mutex.gobra
jcp19 Apr 27, 2026
4a33257
Use MCE on-demand
jcp19 Apr 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/gobra.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -489,7 +489,7 @@ jobs:
conditionalizePermissions: '1'
moreJoins: 'impure'
imageVersion: ${{ env.imageVersion }}
mceMode: 'on'
mceMode: 'on' # maybe change to od
Comment thread
jcp19 marked this conversation as resolved.
Outdated
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
Expand Down
2 changes: 0 additions & 2 deletions pkg/slayers/scion.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1028,7 +1028,6 @@ func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (res uint32, er
// @ invariant 0 <= i && i <= len(s.RawSrcAddr)
// @ decreases len(s.RawSrcAddr) - i
for i := 0; i < len(s.RawSrcAddr); i += 2 {
// @ preserves err == nil
// @ requires acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
// @ requires 0 <= i && i < len(s.RawSrcAddr) && i % 2 == 0 && len(s.RawSrcAddr) % 2 == 0
// @ ensures acc(&s.RawSrcAddr, R20) && acc(sl.Bytes(s.RawSrcAddr, 0, len(s.RawSrcAddr)), R20)
Expand All @@ -1049,7 +1048,6 @@ func (s *SCION) pseudoHeaderChecksum(length int, protocol uint8) (res uint32, er
// @ invariant 0 <= i && i <= len(s.RawDstAddr)
// @ decreases len(s.RawDstAddr) - i
for i := 0; i < len(s.RawDstAddr); i += 2 {
// @ preserves err == nil
// @ requires acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
// @ requires 0 <= i && i < len(s.RawDstAddr) && i % 2 == 0 && len(s.RawDstAddr) % 2 == 0
// @ ensures acc(&s.RawDstAddr, R20) && acc(sl.Bytes(s.RawDstAddr, 0, len(s.RawDstAddr)), R20)
Expand Down
4 changes: 2 additions & 2 deletions verification/utils/ghost_sync/ghost-mutex.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,13 +44,13 @@ pure func (m gpointer[GhostMutex]) LockInv() pred()
ghost
requires inv() && acc(m) && *m == GhostMutex{}
ensures m.LockP() && m.LockInv() == inv
decreases
decreases _
func (m gpointer[GhostMutex]) SetInv(inv pred())

ghost
requires acc(m.LockP(), _)
ensures m.LockP() && m.UnlockP() && m.LockInv()()
decreases _ if sync.IgnoreBlockingForTermination()
decreases _
func (m gpointer[GhostMutex]) Lock()

ghost
Expand Down
Loading