Conversation
LinoTelschow
force-pushed
the
tlino-msc-io-spec-2
branch
from
af1b959 to
b0db60c
Compare
| pure func ToAbsIA(ia addr.IA) AbsIA | ||
|
|
||
| ghost | ||
| requires acc(path.HopFieldInv(hop), _) |
There was a problem hiding this comment.
we are not establishing any functional relation between the result and the original hop (e.g., that they have the same egressID). Is the plan to change that
There was a problem hiding this comment.
I think we can do this, at the moment it is a bit tricky to relate the current hop to its abstraction within the processSCION method. But i think it can be done by adding a absHop entry to the scionPacketProcessor struct and keep their relation with help of the Mem predicate of scionPacketProcessor
There was a problem hiding this comment.
But I first need to know if the rest of the code is fine before proceeding
* added helper functons to speedup verification * added additional ghost state to distinguish address sources * improved performance of processOHP2 * defined addrFromSCIONPkt as non ghost * outlined another method * added comments * adapted some comments
jcp19
left a comment
jcp19
left a comment
There was a problem hiding this comment.
I'm still going through it, but I have some comments already
gobra/pkg/router/io_types.gobra
Outdated
| ghost | ||
| requires verifyutils.BytesAcc(b) | ||
| decreases _ | ||
| pure func ToAbsBytes2(b []byte) (res AbsBytes) |
There was a problem hiding this comment.
you can specify here that the result of this operation is equal to the result of calling ToAbsBytes with b
There was a problem hiding this comment.
Yes, this was my first idea, but this significantly increases the verification time.
There was a problem hiding this comment.
Hmm, how big was the increase in verification time?
There was a problem hiding this comment.
I stopped after 20 minutes
Before it was around 90 seconds
gobra/pkg/router/io_types.gobra
Outdated
| // lemmas | ||
| ghost | ||
| requires acc(verifyutils.BytesAcc(b), _) | ||
| requires absBytes == unfolding acc(verifyutils.BytesAcc(b), _) in ToAbsBytes(b) | ||
| ensures absBytes == ToAbsBytes2(b) | ||
| decreases _ | ||
| pure func relateByteAccess(b []byte, absBytes AbsBytes) bool No newline at end of file |
There was a problem hiding this comment.
this is probably not necessary, look at my comment for the ToAbsBytes2 function
gobra/pkg/router/io_spec.gobra
Outdated
| ghost | ||
| requires scn.Mem() | ||
| requires data == unfolding scn.Mem() in scn.RawPkt | ||
| ensures absBytes == GetAbsSCIONRawPkt(ToAbsSCION(scn)) |
There was a problem hiding this comment.
You could probably move this postcondition (with some editing) to the ToAbsSCION function. Is there any reason to not do so?
There was a problem hiding this comment.
You can probably do something similar for the other lemmas here
There was a problem hiding this comment.
Maybe i can move this postcondtion, but we have to be very careful.
Like in the case for the ToAbsBytes2 method, an unfolding in the contract can increase the verification time.
And the SCION type requires a lot of nested unfoldings.
Thus, I have decided to use only lemma methods to specify the getter methods of abstract types
There was a problem hiding this comment.
Ok, it is also fine to keep the lemma methods. However, they are currently implemented as pure functions which means that they introduce new axioms, and we cannot control very well when they are brought into context. Let's use non-pure functions for that
There was a problem hiding this comment.
I have tested it with non-pure functions,
It is about 3 minutes slower, but I guess its still ok.
Btw, what do you mean exactly by "they introduce new axioms, and we cannot control very well when they are brought into context."?
2 participants
No description provided.