Skip to content
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

Drop specific permission amounts in pure functions's preconditions #387

Open
wants to merge 27 commits into
base: master
Choose a base branch
from
Open

Drop specific permission amounts in pure functions's preconditions #387

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
70bb22d
test
jcp19 Dec 2, 2024
b8eefef
Apply suggestions from code review
jcp19 Dec 2, 2024
35ecbed
Update pkg/slayers/path/epic/epic_spec.gobra
jcp19 Dec 2, 2024
400ceb7
Update pkg/slayers/path/epic/epic_spec.gobra
jcp19 Dec 2, 2024
6a1b5b1
Merge branch 'master' into drop_fractions_functions
jcp19 Dec 19, 2024
00db763
drop unnecessary formalization of waitgroups
jcp19 Dec 20, 2024
8d6127a
tiny change
jcp19 Dec 20, 2024
bde15be
drop access predicates
jcp19 Dec 20, 2024
f27bbf1
stabilize verification conditions that now fail
jcp19 Jan 6, 2025
4b797ea
fix yet one more proof obligation; extract code into additional theorem
jcp19 Jan 6, 2025
2c0697c
yet another proof obligation fixed
jcp19 Jan 6, 2025
fd68775
refactor widen lemma for HopField to reuse a previous proof
jcp19 Jan 7, 2025
f27ca87
fix bad triggers generated by Gobra
jcp19 Jan 7, 2025
ced08ce
Refactor parts of scion_spec.gobra for proof stability (#389)
jcp19 Jan 7, 2025
11eada7
Merge branch 'master' into drop_fractions_functions
jcp19 Jan 7, 2025
b34f546
backup
jcp19 Jan 8, 2025
5176886
backup
jcp19 Jan 9, 2025
c837096
backup
jcp19 Jan 9, 2025
4ceaa78
backup
jcp19 Jan 16, 2025
351c43b
fix proof obligation in CurrSegEquality
jcp19 Jan 17, 2025
c113e18
drop Uncallable
jcp19 Jan 17, 2025
62d9a32
fix outstanding proof obligations
jcp19 Jan 17, 2025
127a291
drop unnecessary function
jcp19 Jan 17, 2025
590b417
backup
jcp19 Jan 17, 2025
0a874bc
restore old spec
jcp19 Jan 17, 2025
2e2b11b
merge with master
jcp19 Jan 17, 2025
7cd1d56
add gobra action cfg
jcp19 Jan 17, 2025
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
6 changes: 2 additions & 4 deletions pkg/slayers/path/empty/empty_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,16 +35,14 @@ func (e Path) DowngradePerm(buf []byte) {
}

ghost
pure
decreases
func (p Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
pure func (p Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
return true
}

ghost
pure
decreases
func (p Path) LenSpec(ghost ub []byte) (l int) {
pure func (p Path) LenSpec(ghost ub []byte) (l int) {
return PathLen
}

Expand Down
17 changes: 5 additions & 12 deletions pkg/slayers/path/epic/epic_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,10 +38,9 @@ pred (p *Path) Mem(ubuf []byte) {
}

ghost
pure
requires acc(p.Mem(ub), _)
decreases
func (p *Path) LenSpec(ghost ub []byte) (l int) {
pure func (p *Path) LenSpec(ghost ub []byte) (l int) {
return unfolding acc(p.Mem(ub), _) in
(p.ScionPath == nil ?
MetadataLen :
Expand All @@ -66,29 +65,24 @@ pure func (r *Path) GetBase(ub []byte) scion.Base {
}

ghost
pure
requires acc(p.Mem(buf), _)
ensures l == (unfolding acc(p.Mem(buf), _) in len(p.PHVF))
jcp19 marked this conversation as resolved.
Show resolved Hide resolved
decreases
func (p *Path) getPHVFLen(buf []byte) (l int) {
pure func (p *Path) getPHVFLen(buf []byte) (l int) {
return unfolding acc(p.Mem(buf), _) in len(p.PHVF)
}

ghost
pure
requires acc(p.Mem(buf), _)
ensures l == (unfolding acc(p.Mem(buf), _) in len(p.LHVF))
decreases
func (p *Path) getLHVFLen(buf []byte) (l int) {
pure func (p *Path) getLHVFLen(buf []byte) (l int) {
return unfolding acc(p.Mem(buf), _) in len(p.LHVF)
}

ghost
pure
requires acc(p.Mem(buf), _)
ensures r == (unfolding acc(p.Mem(buf), _) in p.ScionPath != nil)
decreases
func (p *Path) hasScionPath(buf []byte) (r bool) {
pure func (p *Path) hasScionPath(buf []byte) (r bool) {
return unfolding acc(p.Mem(buf), _) in p.ScionPath != nil
}

Expand All @@ -100,9 +94,8 @@ pure func (p *Path) GetUnderlyingScionPathBuf(buf []byte) []byte {
}

ghost
pure
decreases
func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
pure func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
return true
}

Expand Down
4 changes: 2 additions & 2 deletions pkg/slayers/path/hopfield_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,13 +30,13 @@ pred (h *HopField) Mem() {

ghost
decreases
pure func ifsToIO_ifs(ifs uint16) option[io.IO_ifs]{
pure func ifsToIO_ifs(ifs uint16) option[io.IO_ifs] {
return ifs == 0 ? none[io.IO_ifs] : some(io.IO_ifs(ifs))
}

ghost
decreases
pure func IO_ifsToIfs(ifs option[io.IO_ifs]) uint16{
pure func IO_ifsToIfs(ifs option[io.IO_ifs]) uint16 {
return ifs == none[io.IO_ifs] ? 0 : uint16(get(ifs))
}

Expand Down
16 changes: 8 additions & 8 deletions pkg/slayers/path/infofield_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,31 +32,31 @@ pure func InfoFieldOffset(currINF, headerOffset int) int {
ghost
requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) < len(raw)
requires acc(sl.Bytes(raw, 0, len(raw)), R56)
requires acc(sl.Bytes(raw, 0, len(raw)), _)
decreases
pure func ConsDir(raw []byte, currINF int, headerOffset int) bool {
return unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in
return unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
raw[InfoFieldOffset(currINF, headerOffset)] & 0x1 == 0x1
}

ghost
requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) < len(raw)
requires acc(sl.Bytes(raw, 0, len(raw)), R56)
requires acc(sl.Bytes(raw, 0, len(raw)), _)
decreases
pure func Peer(raw []byte, currINF int, headerOffset int) bool {
return unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in
return unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
raw[InfoFieldOffset(currINF, headerOffset)] & 0x2 == 0x2
}

ghost
requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
requires acc(sl.Bytes(raw, 0, len(raw)), R56)
requires acc(sl.Bytes(raw, 0, len(raw)), _)
decreases
pure func Timestamp(raw []byte, currINF int, headerOffset int) io.IO_ainfo {
return let idx := InfoFieldOffset(currINF, headerOffset) + 4 in
unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in
unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
let _ := Asserting(forall i int :: { &raw[idx+i] } { &raw[idx:idx+4][i] } 0 <= i && i < 4 ==>
&raw[idx+i] == &raw[idx:idx+4][i]) in
io.IO_ainfo(binary.BigEndian.Uint32(raw[idx : idx + 4]))
Expand All @@ -65,11 +65,11 @@ pure func Timestamp(raw []byte, currINF int, headerOffset int) io.IO_ainfo {
ghost
requires 0 <= currINF && 0 <= headerOffset
requires InfoFieldOffset(currINF, headerOffset) + InfoLen < len(raw)
requires acc(sl.Bytes(raw, 0, len(raw)), R56)
requires acc(sl.Bytes(raw, 0, len(raw)), _)
decreases
pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.IO_msgterm] {
return let idx := InfoFieldOffset(currINF, headerOffset) + 2 in
unfolding acc(sl.Bytes(raw, 0, len(raw)), R56) in
unfolding acc(sl.Bytes(raw, 0, len(raw)), _) in
let _ := Asserting(forall k int :: {&raw[idx:idx+2][k]} 0 <= k && k < 2 ==>
&raw[idx:idx+4][k] == &raw[idx + k]) in
AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[idx:idx+2]))
Expand Down
6 changes: 2 additions & 4 deletions pkg/slayers/path/onehop/onehop_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -52,16 +52,14 @@ pure func (o *Path) InferSizeUb(ghost ub []byte) (b bool) {
}

ghost
pure
decreases
func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
pure func (p *Path) IsValidResultOfDecoding(b []byte, err error) (res bool) {
return true
}

ghost
pure
decreases
func (p *Path) LenSpec(ghost ub []byte) (l int) {
pure func (p *Path) LenSpec(ghost ub []byte) (l int) {
return PathLen
}

Expand Down
2 changes: 1 addition & 1 deletion pkg/slayers/path/path.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ type Path interface {
//@ ghost
//@ pure
//@ requires Mem(b)
//@ requires acc(sl.Bytes(b, 0, len(b)), R42)
//@ requires acc(sl.Bytes(b, 0, len(b)), _)
//@ decreases
//@ IsValidResultOfDecoding(b []byte, err error) (res bool)
// Reverse reverses a path such that it can be used in the reversed direction.
Expand Down
7 changes: 2 additions & 5 deletions pkg/slayers/path/path_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,18 +38,16 @@ func (p *rawPath) DowngradePerm(ghost buf []byte) {
}

ghost
pure
decreases
func (p *rawPath) IsValidResultOfDecoding(b []byte, err error) (res bool) {
pure func (p *rawPath) IsValidResultOfDecoding(b []byte, err error) (res bool) {
return true
}

ghost
pure
requires acc(p.Mem(ub), _)
ensures 0 <= l
decreases
func (p *rawPath) LenSpec(ghost ub []byte) (l int) {
pure func (p *rawPath) LenSpec(ghost ub []byte) (l int) {
return unfolding acc(p.Mem(ub), _) in len(p.raw)
}

Expand All @@ -69,7 +67,6 @@ pred PathPackageMem() {
ghost
requires 0 <= t && t < maxPathType
requires acc(PathPackageMem(), _)
ensures res == unfolding acc(PathPackageMem(), _) in registeredPaths[t].inUse
decreases
pure func Registered(t Type) (res bool) {
return unfolding acc(PathPackageMem(), _) in registeredPaths[t].inUse
Expand Down
2 changes: 1 addition & 1 deletion pkg/slayers/path/scion/base_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -304,7 +304,7 @@ pure func (m MetaHdr) SerializeToSpec(b []byte) bool {
}

ghost
requires acc(sl.Bytes(ub, 0, len(ub)), R56)
requires acc(sl.Bytes(ub, 0, len(ub)), _)
decreases
pure func (s Base) EqAbsHeader(ub []byte) bool {
// we compute the sublice ub[:MetaLen] inside this function instead
Expand Down
11 changes: 3 additions & 8 deletions pkg/slayers/path/scion/decoded_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,8 @@ import (
)

ghost
pure
decreases
func (p *Decoded) IsValidResultOfDecoding(b []byte, err error) (res bool) {
pure func (p *Decoded) IsValidResultOfDecoding(b []byte, err error) (res bool) {
return true
}

Expand Down Expand Up @@ -66,11 +65,9 @@ func (d *Decoded) Len(ghost ubuf []byte) (l int) {
}

ghost
pure
requires acc(d.Mem(ub), _)
ensures unfolding acc(d.Mem(ub), _) in l == d.Base.Len()
decreases
func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
pure func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
return unfolding acc(d.Mem(ub), _) in d.Base.Len()
}

Expand All @@ -80,11 +77,9 @@ func (d *Decoded) LenSpec(ghost ub []byte) (l int) {
* Unfortunately, Gobra does not fully support them yet, so we
* introduced this method which acts as a wrapper.
*/
pure
requires acc(d.Mem(ubuf), _)
ensures unfolding acc(d.Mem(ubuf), _) in t == d.Base.Type()
decreases
func (d *Decoded) Type(ghost ubuf []byte) (t path.Type) {
pure func (d *Decoded) Type(ghost ubuf []byte) (t path.Type) {
return unfolding acc(d.Mem(ubuf), _) in d.Base.Type()
}

Expand Down
34 changes: 17 additions & 17 deletions pkg/slayers/path/scion/info_hop_setter_lemmas.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,7 @@ opaque
requires 0 < SegLen
requires 0 <= currHfIdx && currHfIdx <= SegLen
requires SegLen * path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), R56)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
decreases
pure func CurrSegWithInfo(hopfields []byte, currHfIdx int, SegLen int, inf io.AbsInfoField) io.IO_seg3 {
return segment(hopfields, 0, currHfIdx, inf.AInfo, inf.UInfo, inf.ConsDir, inf.Peer, SegLen)
Expand All @@ -241,7 +241,7 @@ requires (currInfIdx == 1 && segs.Seg2Len > 0) ||
let end := HopfieldsEndIdx(currInfIdx, segs) in
inf != none[io.AbsInfoField] &&
len(hopfields) == end - start &&
acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
decreases
pure func LeftSegWithInfo(
hopfields []byte,
Expand All @@ -268,7 +268,7 @@ requires (currInfIdx == 0 && segs.Seg2Len > 0) ||
let end := HopfieldsEndIdx(currInfIdx, segs) in
inf != none[io.AbsInfoField] &&
len(hopfields) == end - start &&
acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
decreases
pure func RightSegWithInfo(
hopfields []byte,
Expand All @@ -295,7 +295,7 @@ requires (segs.Seg2Len > 0 && segs.Seg3Len > 0 &&
let end := HopfieldsEndIdx(currInfIdx, segs) in
inf != none[io.AbsInfoField] &&
len(hopfields) == end - start &&
acc(sl.Bytes(hopfields, 0, len(hopfields)), R49)
acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
decreases
pure func MidSegWithInfo(
hopfields []byte,
Expand Down Expand Up @@ -363,13 +363,13 @@ ghost
requires segs.Valid()
requires PktLen(segs, MetaLen) <= len(raw)
requires 1 <= currInfIdx && currInfIdx < 4
requires acc(sl.Bytes(raw, 0, len(raw)), R49)
requires acc(sl.Bytes(raw, 0, len(raw)), _)
requires (currInfIdx == 1 && segs.Seg2Len > 0) ||
(currInfIdx == 2 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ==>
let infoBytes := InfofieldByteSlice(raw, currInfIdx) in
let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in
acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) &&
acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49)
acc(sl.Bytes(infoBytes, 0, path.InfoLen), _) &&
acc(sl.Bytes(hopBytes, 0, len(hopBytes)), _)
decreases
pure func LeftSegEqualitySpec(raw []byte, currInfIdx int, segs io.SegLens) bool {
return (currInfIdx == 1 && segs.Seg2Len > 0) ||
Expand Down Expand Up @@ -424,13 +424,13 @@ ghost
requires segs.Valid()
requires PktLen(segs, MetaLen) <= len(raw)
requires -1 <= currInfIdx && currInfIdx < 2
requires acc(sl.Bytes(raw, 0, len(raw)), R49)
requires acc(sl.Bytes(raw, 0, len(raw)), _)
requires (currInfIdx == 0 && segs.Seg2Len > 0) ||
(currInfIdx == 1 && segs.Seg2Len > 0 && segs.Seg3Len > 0) ==>
let infoBytes := InfofieldByteSlice(raw, currInfIdx) in
let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in
acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) &&
acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49)
acc(sl.Bytes(infoBytes, 0, path.InfoLen), _) &&
acc(sl.Bytes(hopBytes, 0, len(hopBytes)), _)
decreases
pure func RightSegEqualitySpec(raw []byte, currInfIdx int, segs io.SegLens) bool {
return (currInfIdx == 0 && segs.Seg2Len > 0) ||
Expand Down Expand Up @@ -485,13 +485,13 @@ ghost
requires segs.Valid()
requires PktLen(segs, MetaLen) <= len(raw)
requires 2 <= currInfIdx && currInfIdx < 5
requires acc(sl.Bytes(raw, 0, len(raw)), R49)
requires acc(sl.Bytes(raw, 0, len(raw)), _)
requires (segs.Seg2Len > 0 && segs.Seg3Len > 0 &&
(currInfIdx == 2 || currInfIdx == 4)) ==>
let infoBytes := InfofieldByteSlice(raw, currInfIdx) in
let hopBytes := HopfieldsByteSlice(raw, currInfIdx, segs) in
acc(sl.Bytes(infoBytes, 0, path.InfoLen), R49) &&
acc(sl.Bytes(hopBytes, 0, len(hopBytes)), R49)
acc(sl.Bytes(infoBytes, 0, path.InfoLen), _) &&
acc(sl.Bytes(hopBytes, 0, len(hopBytes)), _)
decreases
pure func MidSegEqualitySpec(raw []byte, currInfIdx int, segs io.SegLens) bool {
return (segs.Seg2Len > 0 && segs.Seg3Len > 0 &&
Expand Down Expand Up @@ -551,12 +551,12 @@ func MidSegEquality(raw []byte, currInfIdx int, segs io.SegLens) {
ghost
requires 0 <= currHfIdx && currHfIdx < segLen
requires segLen * path.HopLen == len(hopfields)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), R50)
requires acc(sl.Bytes(hopfields, 0, len(hopfields)), _)
requires let currHfStart := currHfIdx * path.HopLen in
let currHfEnd := currHfStart + path.HopLen in
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), R50) &&
acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), R50) &&
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), R50)
acc(sl.Bytes(hopfields[:currHfStart], 0, currHfStart), _) &&
acc(sl.Bytes(hopfields[currHfStart:currHfEnd], 0, path.HopLen), _) &&
acc(sl.Bytes(hopfields[currHfEnd:], 0, (segLen - currHfIdx - 1) * path.HopLen), _)
decreases
pure func BytesStoreCurrSeg(hopfields []byte, currHfIdx int, segLen int, inf io.AbsInfoField) bool {
return let currseg := CurrSegWithInfo(hopfields, currHfIdx, segLen, inf) in
Expand Down
Loading
Loading