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

Jump to bottom

Drop Assumption in SetInfoField #350

Merged
merged 17 commits into from
Jun 13, 2024
Merged

Drop Assumption in SetInfoField #350

Show file tree
Hide file tree
Changes from 14 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
1b16d0c
proof setInfoField
mlimbeck Jun 4, 2024
f1b567c
fix verification errors
mlimbeck Jun 4, 2024
75a8042
fix syntax error
mlimbeck Jun 4, 2024
af94ea7
fix verification errors
mlimbeck Jun 4, 2024
e25b08c
formatting
mlimbeck Jun 11, 2024
b7aa914
simplification attempt
mlimbeck Jun 11, 2024
0290bc5
Merge branch 'master' into markus-io-spec-setInfoField-proof
mlimbeck Jun 11, 2024
84e8edc
Apply suggestions from code review
mlimbeck Jun 11, 2024
40d7e38
refactoring
mlimbeck Jun 12, 2024
70f0cfe
fix verification error
mlimbeck Jun 12, 2024
d84e9fc
fixed LeftSegEquality()
mlimbeck Jun 12, 2024
fa6ffa7
formatting
mlimbeck Jun 12, 2024
33a26b0
Apply suggestions from code review
mlimbeck Jun 12, 2024
6b8d86d
feedback
mlimbeck Jun 12, 2024
4d5eb49
Merge branch 'master' into markus-io-spec-setInfoField-proof
mlimbeck Jun 13, 2024
58e42f0
renaming AbsSlice_Bytes to Bytes
mlimbeck Jun 13, 2024
85e97e0
adding documentation
mlimbeck Jun 13, 2024
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
34 changes: 19 additions & 15 deletions pkg/slayers/path/infofield.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,55 +62,57 @@ type InfoField struct {
// path.InfoLen.
// @ requires len(raw) >= InfoLen
// @ preserves acc(inf)
// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R45)
// @ preserves acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R45)
// @ ensures err == nil
// @ ensures BytesToIntermediateAbsInfoField(raw, 0, 0, InfoLen) ==
// @ inf.ToIntermediateAbsInfoField()
// @ ensures BytesToAbsInfoField(raw, 0) ==
// @ inf.ToAbsInfoField()
// @ decreases
func (inf *InfoField) DecodeFromBytes(raw []byte) (err error) {
if len(raw) < InfoLen {
return serrors.New("InfoField raw too short", "expected", InfoLen, "actual", len(raw))
}
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R50)
//@ unfold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R50)
inf.ConsDir = raw[0]&0x1 == 0x1
inf.Peer = raw[0]&0x2 == 0x2
//@ assert &raw[2:4][0] == &raw[2] && &raw[2:4][1] == &raw[3]
inf.SegID = binary.BigEndian.Uint16(raw[2:4])
//@ assert &raw[4:8][0] == &raw[4] && &raw[4:8][1] == &raw[5]
//@ assert &raw[4:8][2] == &raw[6] && &raw[4:8][3] == &raw[7]
inf.Timestamp = binary.BigEndian.Uint32(raw[4:8])
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, InfoLen), R50)
//@ fold acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R50)
//@ assert reveal BytesToAbsInfoField(raw, 0) ==
//@ inf.ToAbsInfoField()
return nil
}

// SerializeTo writes the fields into the provided buffer. The buffer must be of length >=
// path.InfoLen.
// @ requires len(b) >= InfoLen
// @ preserves acc(inf, R10)
// @ preserves slices.AbsSlice_Bytes(b, 0, InfoLen)
// @ preserves slices.AbsSlice_Bytes(b, 0, len(b))
// @ ensures err == nil
// @ ensures inf.ToIntermediateAbsInfoField() ==
// @ BytesToIntermediateAbsInfoField(b, 0, 0, InfoLen)
// @ ensures inf.ToAbsInfoField() ==
// @ BytesToAbsInfoField(b, 0)
// @ decreases
func (inf *InfoField) SerializeTo(b []byte) (err error) {
if len(b) < InfoLen {
return serrors.New("buffer for InfoField too short", "expected", InfoLen,
"actual", len(b))
}
//@ ghost targetAbsInfo := inf.ToIntermediateAbsInfoField()
//@ unfold slices.AbsSlice_Bytes(b, 0, InfoLen)
//@ ghost targetAbsInfo := inf.ToAbsInfoField()
//@ unfold slices.AbsSlice_Bytes(b, 0, len(b))
b[0] = 0
if inf.ConsDir {
b[0] |= 0x1
}
//@ ghost tmpInfo1 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
//@ ghost tmpInfo1 := BytesToAbsInfoFieldHelper(b, 0)
//@ bits.InfoFieldFirstByteSerializationLemmas()
//@ assert tmpInfo1.ConsDir == targetAbsInfo.ConsDir
//@ ghost firstByte := b[0]
if inf.Peer {
b[0] |= 0x2
}
//@ tmpInfo2 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
//@ tmpInfo2 := BytesToAbsInfoFieldHelper(b, 0)
//@ assert tmpInfo2.Peer == (b[0] & 0x2 == 0x2)
//@ assert tmpInfo2.ConsDir == (b[0] & 0x1 == 0x1)
//@ assert tmpInfo2.Peer == targetAbsInfo.Peer
Expand All @@ -119,14 +121,16 @@ func (inf *InfoField) SerializeTo(b []byte) (err error) {
b[1] = 0 // reserved
//@ assert &b[2:4][0] == &b[2] && &b[2:4][1] == &b[3]
binary.BigEndian.PutUint16(b[2:4], inf.SegID)
//@ ghost tmpInfo3 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
//@ ghost tmpInfo3 := BytesToAbsInfoFieldHelper(b, 0)
//@ assert tmpInfo3.UInfo == targetAbsInfo.UInfo
//@ assert &b[4:8][0] == &b[4] && &b[4:8][1] == &b[5]
//@ assert &b[4:8][2] == &b[6] && &b[4:8][3] == &b[7]
binary.BigEndian.PutUint32(b[4:8], inf.Timestamp)
//@ ghost tmpInfo4 := BytesToIntermediateAbsInfoFieldHelper(b, 0, InfoLen)
//@ ghost tmpInfo4 := BytesToAbsInfoFieldHelper(b, 0)
//@ assert tmpInfo4.AInfo == targetAbsInfo.AInfo
//@ fold slices.AbsSlice_Bytes(b, 0, InfoLen)
//@ fold slices.AbsSlice_Bytes(b, 0, len(b))
//@ assert inf.ToAbsInfoField() ==
//@ reveal BytesToAbsInfoField(b, 0)
return nil
}

Expand Down
36 changes: 13 additions & 23 deletions pkg/slayers/path/infofield_spec.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,39 +75,29 @@ pure func AbsUinfo(raw []byte, currINF int, headerOffset int) set[io.IO_msgterm]
AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[idx:idx+2]))
}

// This type simplifies the infoField, making it easier
// to use than the IO_seg3 from the IO-spec.
type IntermediateAbsInfoField adt {
IntermediateAbsInfoField_ {
AInfo io.IO_ainfo
UInfo set[io.IO_msgterm]
ConsDir bool
Peer bool
}
}

ghost
requires 0 <= start && start <= middle
requires middle+InfoLen <= end && end <= len(raw)
requires acc(sl.AbsSlice_Bytes(raw, start, end), _)
opaque
requires 0 <= middle
requires middle+InfoLen <= len(raw)
requires acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _)
decreases
pure func BytesToIntermediateAbsInfoField(raw [] byte, start int, middle int, end int) (IntermediateAbsInfoField) {
return unfolding acc(sl.AbsSlice_Bytes(raw, start, end), _) in
BytesToIntermediateAbsInfoFieldHelper(raw, middle, end)
pure func BytesToAbsInfoField(raw [] byte, middle int) (io.AbsInfoField) {
return unfolding acc(sl.AbsSlice_Bytes(raw, 0, len(raw)), _) in
BytesToAbsInfoFieldHelper(raw, middle)
}

ghost
requires 0 <= middle
requires middle+InfoLen <= end && end <= len(raw)
requires forall i int :: { &raw[i] } middle <= i && i < end ==>
requires middle+InfoLen <= len(raw)
requires forall i int :: { &raw[i] } middle <= i && i < len(raw) ==>
acc(&raw[i], _)
decreases
pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int) (IntermediateAbsInfoField) {
pure func BytesToAbsInfoFieldHelper(raw [] byte, middle int) (io.AbsInfoField) {
return let _ := Asserting(forall k int :: {&raw[middle+2:middle+4][k]} 0 <= k && k < 2 ==>
&raw[middle+2:middle+4][k] == &raw[middle+2 + k]) in
let _ := Asserting(forall k int :: {&raw[middle+4:middle+8][k]} 0 <= k && k < 4 ==>
&raw[middle+4:middle+8][k] == &raw[middle+4 + k]) in
IntermediateAbsInfoField(IntermediateAbsInfoField_{
io.AbsInfoField(io.AbsInfoField_{
AInfo : io.IO_ainfo(binary.BigEndian.Uint32(raw[middle+4:middle+8])),
UInfo : AbsUInfoFromUint16(binary.BigEndian.Uint16(raw[middle+2:middle+4])),
ConsDir : raw[middle] & 0x1 == 0x1,
Expand All @@ -117,8 +107,8 @@ pure func BytesToIntermediateAbsInfoFieldHelper(raw [] byte, middle int, end int

ghost
decreases
pure func (inf InfoField) ToIntermediateAbsInfoField() (IntermediateAbsInfoField) {
return IntermediateAbsInfoField(IntermediateAbsInfoField_{
pure func (inf InfoField) ToAbsInfoField() (io.AbsInfoField) {
return io.AbsInfoField(io.AbsInfoField_{
AInfo : io.IO_ainfo(inf.Timestamp),
UInfo : AbsUInfoFromUint16(inf.SegID),
ConsDir : inf.ConsDir,
Expand Down
Loading
Loading