-
Notifications
You must be signed in to change notification settings - Fork 3
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.
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
Prove three of the four assumptions in parsePath
#316
Changes from all commits
0aa5841
8525b7c
2eaf7a4
e9d31ae
6b77cb6
e9631e0
bd062dc
3246a2b
35ff392
f925f10
6a19edf
3d90011
6e8f884
afe9e52
de241b5
8a0452e
4540095
bf2c331
53cadc9
790e842
ca581db
0d3cc57
01eade7
bfd6c2f
8c7b6c1
89997c6
f1cf0b1
4343478
715fa51
b051f09
7cbe9d6
689e9da
24d19e1
e923c40
45b432e
8f15113
503b0e0
c292a84
a68a3e7
ff00b89
4e85c1f
cd887c9
81b951a
8d468b8
b92ee32
2f250fb
95af227
00d92c5
8c57264
1c1850b
4ccdab1
3161a68
92b4a1a
9680dd6
50beee9
8300ead
468fab7
cdd2ce8
7eca4dc
67a4d5d
de48fa1
f892030
9258b54
7df48b8
1560668
1a9daf3
0160b2c
465553b
71866b2
0a4c77d
ea7c499
f07073e
d6b8d33
384661e
8514223
c27a66a
71aadfe
88db3fd
8383408
ab5e91f
2c08fb3
39330b5
ac2c877
99bd1e6
7d13caf
e733dc8
005fa2a
98a867b
ebf95fb
baa1bb6
72a5aec
c9c16c7
ae39655
7b8bcd8
b1618cd
736ad9b
56f6348
e40741a
2c509cc
bc7494b
6706d80
7db3c5b
7bb5140
1daa00b
4178d7c
5071a38
0f1ca2d
f2815c9
b3f97b7
4b26ae0
431a897
8d516c8
bb5d531
3b634c3
5344c79
6b24fca
a86a357
12c1164
ebc8fd7
f784cf5
0e7c3bd
794c8a6
045d57e
c72d66e
fc4311f
e49b959
46ccc35
aedb06b
60bbbf8
e335546
fd58c74
b72658a
0d81fc7
1349d7a
638bffc
5b661f1
1866cfd
f80c201
9b69830
cfd34d7
5ae6bfd
7ea708c
3fa6c88
e58d0e6
5ac52d6
d5689e5
33268e9
003bb51
5eea132
d512053
f3ff7a0
5b658be
97e4ac7
f03cb47
24b0577
d8fb8f1
c3a42c4
41a220b
d052e36
9e47938
deefc2c
b8bc232
12616a6
5a54b5d
e0fed36
6247842
396b9ac
574089d
5a0f43c
c7cee59
cb9ab37
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -43,13 +43,12 @@ pure func IO_ifsToIfs(ifs option[io.IO_ifs]) uint16{ | |
ghost | ||
requires 0 <= start && start <= middle | ||
requires middle + HopLen <= end && end <= len(raw) | ||
requires acc(slices.AbsSlice_Bytes(raw, start, end), _) | ||
requires forall i int :: { &raw[i] } start <= i && i < end ==> acc(&raw[i], _) | ||
decreases | ||
pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) { | ||
pure func BytesToIO_HF_Helper(raw [] byte, start int, middle int, end int) (io.IO_HF) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. These names are getting more and more unidiomatic :D I think calling these functions |
||
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+6][k]} 0 <= k && k < 4 ==> &raw[middle+4:middle+6][k] == &raw[middle + 4 + k]) in | ||
let _ := Asserting(forall k int :: {&raw[middle+6:middle+6+MacLen][k]} 0 <= k && k < MacLen ==> &raw[middle+6:middle+6+MacLen][k] == &raw[middle + 6 + k]) in | ||
unfolding acc(slices.AbsSlice_Bytes(raw, start, end), _) in | ||
let inif2 := binary.BigEndian.Uint16(raw[middle+2:middle+4]) in | ||
let egif2 := binary.BigEndian.Uint16(raw[middle+4:middle+6]) in | ||
let op_inif2 := ifsToIO_ifs(inif2) in | ||
|
@@ -61,6 +60,15 @@ pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) { | |
}) | ||
} | ||
|
||
ghost | ||
requires 0 <= start && start <= middle | ||
requires middle + HopLen <= end && end <= len(raw) | ||
requires acc(slices.AbsSlice_Bytes(raw, start, end), _) | ||
decreases | ||
pure func BytesToIO_HF(raw [] byte, start int, middle int, end int) (io.IO_HF) { | ||
return unfolding acc(slices.AbsSlice_Bytes(raw, start, end), _) in BytesToIO_HF_Helper(raw, start, middle, end) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I know that you still will refine the code, but as a heads-up, please try to keep lines shorter (e.g., by introducing line-breaks after |
||
} | ||
|
||
ghost | ||
decreases | ||
pure func (h HopField) ToIO_HF() (io.IO_HF) { | ||
|
@@ -70,3 +78,71 @@ pure func (h HopField) ToIO_HF() (io.IO_HF) { | |
HVF : AbsMac(h.Mac), | ||
}) | ||
} | ||
|
||
ghost | ||
opaque | ||
requires 0 <= start && start <= middle | ||
requires middle + HopLen <= end && end <= len(raw) | ||
requires acc(slices.AbsSlice_Bytes(raw, start, end), R50) | ||
requires h.Mem() | ||
decreases | ||
pure func (h *HopField) CorrectlyDecodedHF(raw []byte, start int, middle int, end int) bool { | ||
return unfolding h.Mem() in unfolding acc(slices.AbsSlice_Bytes(raw, start, end), R51) in BytesToIO_HF(raw, start, middle, end) == h.ToIO_HF() | ||
} | ||
|
||
ghost | ||
opaque | ||
requires 0 <= start && start <= middle | ||
requires middle + HopLen <= end && end <= len(raw) | ||
requires acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R50) | ||
decreases | ||
pure func CorrectlyDecodedHF_FullBuf(h HopField, raw []byte, start int, middle int, end int) bool { | ||
return unfolding acc(slices.AbsSlice_Bytes(raw, 0, len(raw)), R51) in | ||
let hop := BytesToIO_HF_Helper(raw, start, middle, end) in | ||
hop == h.ToIO_HF() | ||
} | ||
|
||
ghost | ||
requires 0 <= start && start <= middle | ||
requires middle + HopLen <= end && end <= slice_end-slice_start | ||
requires 0 <= slice_start && slice_start < slice_end && slice_end <= len(raw) | ||
requires slice_start + HopLen <= slice_end | ||
requires acc(slices.AbsSlice_Bytes(raw[slice_start : slice_end], start, end), R45) | ||
requires acc(slices.AbsSlice_Bytes(raw, start+slice_start, end+slice_start), R45) | ||
requires h.Mem() | ||
requires h.CorrectlyDecodedHF(raw[slice_start : slice_end], start, middle, end) | ||
ensures acc(slices.AbsSlice_Bytes(raw[slice_start : slice_end], start, end), R45) | ||
ensures acc(slices.AbsSlice_Bytes(raw, start+slice_start, end+slice_start), R45) | ||
ensures h.Mem() | ||
ensures h.CorrectlyDecodedHF(raw, start+slice_start, middle+slice_start, end+slice_start) | ||
decreases | ||
func (h *HopField) CorrectlyDecodedHF_Lemma(raw []byte, slice_start int, slice_end int, start int, middle int, end int) bool { | ||
assert reveal h.CorrectlyDecodedHF(raw[slice_start : slice_end], start, middle, end) | ||
unfold acc(slices.AbsSlice_Bytes(raw[slice_start : slice_end], start, end), R46) | ||
unfold acc(slices.AbsSlice_Bytes(raw, start+slice_start, end+slice_start), R46) | ||
assert BytesToIO_HF(raw[slice_start : slice_end], start, middle, end) == BytesToIO_HF(raw, start+slice_start, middle+slice_start, end+slice_start) | ||
assert reveal h.CorrectlyDecodedHF(raw, start+slice_start, middle+slice_start, end+slice_start) | ||
fold acc(slices.AbsSlice_Bytes(raw[slice_start : slice_end], start, end), R46) | ||
fold acc(slices.AbsSlice_Bytes(raw, start+slice_start, end+slice_start), R46) | ||
} | ||
|
||
ghost | ||
requires 0 <= start && start <= middle | ||
requires middle + HopLen <= end && end <= len(raw) | ||
requires acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R45) | ||
requires acc(slices.AbsSlice_Bytes(raw, start, end), R45) | ||
requires h.Mem() | ||
requires len(ubuf) >= len(raw) | ||
requires raw === ubuf[:len(raw)] | ||
requires h.CorrectlyDecodedHF(raw, start, middle, end) | ||
ensures acc(slices.AbsSlice_Bytes(raw, start, end), R45) | ||
ensures acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R45) | ||
ensures h.Mem() | ||
ensures CorrectlyDecodedHF_FullBuf(unfolding h.Mem() in *h, ubuf, start, middle, end) | ||
decreases | ||
func (h *HopField) CorrectlyDecodedHF_WidenLemma(raw []byte, start int, middle int, end int, ubuf []byte) bool { | ||
assert reveal h.CorrectlyDecodedHF(raw, start, middle, end) | ||
assert (unfolding h.Mem() in h.ToIO_HF()) == (unfolding h.Mem() in *h).ToIO_HF() | ||
assert unfolding acc(slices.AbsSlice_Bytes(ubuf, 0, len(ubuf)), R46) in unfolding acc(slices.AbsSlice_Bytes(raw, start, end), R46) in forall i int :: { &ubuf[i] } 0 <= i && i < len(raw) ==> raw[i] == ubuf[i] | ||
assert reveal CorrectlyDecodedHF_FullBuf(unfolding h.Mem() in *h, ubuf, start, middle, end) | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Considering all the effort that went into making Gobra/silicon faster in the last few months, I think that these outline blocks are now unnecessary because