IO spec

[LinoTelschow]

Changes:

• adds IO spec

[Felalolf]

where is the slicing of the buffer that we talked about today, or is this not necessary anymore?

[Felalolf]

Or is this coming in a later PR?

[LinoTelschow]

I want to do this next

[LinoTelschow]

Im currently trying this:

ghost
requires forall i int :: 0 <= i && i < cap(b) ==> acc(&b[i], _)
requires 0 <= n && n <= cap(b)
ensures res == ToAbsBytes(b[0:n])
decreases _
pure func ToAbsBytesBounded(b []byte, n int) (res AbsBytes)

requires token(t) && readBatch_p(t)
preserves acc(Mem(), _)
preserves msgs.Mem()
preserves forall i int :: 0 <= i && i < len(metas) ==> (&metas[i]).Mem()
ensures err == nil ==> 0 < n && n <= len(msgs) && n <= len(metas)
ensures err == nil ==> absMsgs == ToAbsMessages(msgs, n)
ensures err == nil ==> unfolding msgs.Mem() in (forall i int :: 0 <= i && i < n ==> GetAbsMessagePayload(absMsgs[i]) == unfolding (&msgs[i]).Mem() in ToAbsBytesBounded((msgs[i].Buffers)[0], msgs[i].N))
ensures err == nil ==> token(t1) && t1 == old(get_readBatch_t1(t)) && absMsgs == old(get_readBatch_msgs(t))
ensures err != nil ==> t1 == t && token(t1) && readBatch_p(t1) && get_readBatch_t1(t) == old(get_readBatch_t1(t)) && get_readBatch_msgs(t) == old(get_readBatch_msgs(t))
ReadBatch(msgs underlayconn.Messages, metas []underlayconn.ReadMeta, ghost t Place) (n int, err error, ghost absMsgs seq[AbsMessage], ghost t1 Place)

However after executing the readBatch method, I cannot assert GetAbsMessagePayload(absMsgs[i]) == ToAbsBytesBounded((msgs[i].Buffers)[0], msgs[i].N) property.

I also tried the approach with directly slicing, but again asserting the property afterwards fails.

Do you have an Idea how to make it work?

[Felalolf]

look like a triggering problem to me. Try adding triggers to the quantifier in the postcondition.

[LinoTelschow]

In the last days i tried to solve this issue, but I could not fix it.
What I found out is the following behavior:
If I used this postcondition:

ensures err == nil ==> forall i int :: { GetAbsMessagePayload(absMsgs[i]) } (0 <= i && i < n) ==> (unfolding msgs.Mem() in GetAbsMessagePayload(absMsgs[i]) == unfolding (&msgs[i]).Mem() in ToAbsBytes((msgs[i].Buffers)[0]))

with this ToAbsBytes method:

ghost
// requires forall i int :: 0 <= i && i < len(b) ==> acc(&b[i], _)
decreases _
pure func ToAbsBytes(b []byte) AbsBytes

Then i can assert the property.

But if I uncomment the requires clause in the ToAbsBytes method, then the assertion of the property fails.

[LinoTelschow]

OK, I think I found a solution for the problem:

I use this function:

ghost
requires msg.Mem()
ensures res == unfolding msg.Mem() in ToAbsBytes(msg.Buffers[0][0:msg.N])
decreases _
pure func MessageToAbsBytesBounded(msg *ipv4.Message) (res AbsBytes)

and this contract:

ensures err == nil ==> forall i int :: { GetAbsMessagePayload(absMsgs[i]) } (0 <= i && i < n) ==> (GetAbsMessagePayload(absMsgs[i]) == (unfolding msgs.Mem() in MessageToAbsBytesBounded(&msgs[i])))

[Felalolf]

This version looks good. With the previous version, which assertion failed?

[Felalolf]

I am not sure if I made this clear enough. The trigger should not be something that requires an unfold. I would expect that this is the reason why the previous version failed. A trigger that consists of a heap function is implicitly parameterized with a heap snapshot (see this as a mathematical abstraction of the footprint of the function). As such, if the heap snapshot is not well defined or not yet uncovered at the scope of the trigger, then I am not too surprised that there are issues. Since terms outside the forall cannot have the same heap snapshot as the trigger.

[LinoTelschow]

I couldn't really find out which assertion failed.
But what I noticed is that as soon as i use this this construct :

ensures err == nil ==> forall i int :: { GetAbsMessagePayload(absMsgs[i]) } (0 <= i && i < n) ==> (unfolding msgs.Mem() in GetAbsMessagePayload(absMsgs[i]) == unfolding (&msgs[i]).Mem() in foo((msgs[i].Buffers)[0]))

with a method foo:

requires forall i int :: { b[i] } 0 <= i && i < len(b) ==> acc(&b[i], _)
pure func foo(b []byte)

Then it fails

But with this foo:

pure func foo(b []byte)

It verifies

[Felalolf]

looks good to me.