[Verifpal] Matryoshka

[Nadim Kobeissi]

Oh, looks like we're not doing internal rewrites. Thanks a lot Mike, fixing
now.

Nadim Kobeissi
Symbolic Software • https://symbolic.software
Sent from office


On Wed, Sep 11, 2019 at 8:41 PM Mike via Verifpal
<verifpal at lists.symbolic.software> wrote:

> 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)
>
> _______________________________________________
> Verifpal mailing list
> Verifpal at lists.symbolic.software
> https://lists.symbolic.software/mailman/listinfo/verifpal
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20190911/511fc9fc/attachment.htm>