[Verifpal] Matryoshka

[Nadim Kobeissi]

042c063fd8 (latest commit) should fix this. I'm annoyed I didn't think
about this sooner, it's a significant oversight on my part. We weren't
doing internal rewrites!

Keep them coming, Mike!

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


On Wed, Sep 11, 2019 at 8:55 PM Nadim Kobeissi <nadim at symbolic.software>
wrote:

> 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/e49feded/attachment.htm>