[Verifpal] Matryoshka

[Mike]

hi all,

0. I've checked *all* functions itself.
OK.
Now I'm checking the kernel by combinations. No crypto, no protocols.
Since you *handle* a lot of things already findings real bug(s) is like pure art.
1. Files attached (enc.vp, aead.vp) shows kernel understands functions inside functions as expected. 
Good.
2. If replace line by next two lines inside "principal B" in file fail.vp last ASSERT() will not fail.

(mike)
-------------- next part --------------
A non-text attachment was scrubbed...
Name: enc.vp
Type: application/octet-stream
Size: 102 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190911/62504a64/attachment.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: aead.vp
Type: application/octet-stream
Size: 123 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190911/62504a64/attachment-0001.obj>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: fail.vp
Type: application/octet-stream
Size: 354 bytes
Desc: not available
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190911/62504a64/attachment-0002.obj>