Bryan Parno

Has this been resolved at this point? If so, shall we close the issue?

Ah, I misinterpreted that comment. I think EverCrypt now exposes an API for AES-CTR. Not sure about AES on its own. @protz would know. Same for ChaCha and Poly as...

@protz Do you mean IVs of non-standard length? I recall talking about that. I don't remember discussing key expansion.

Regarding maximum input length, for AES-GCM, I believe @R1kM has a branch where he's working on increasing that to the NIST spec's limit. I'm not sure how far along he...

Thanks very much! I'm happy to hop onto Zoom if that's helpful. Just ping me on the AutoLab Slack.

I don't speak Ruby, unfortunately, but it seems like this line: https://github.com/autolab/Autolab/blob/6cad6d1f4cd638c470ed373c34c5908dec5ebd09/app/controllers/extensions_controller.rb#L31 should have included the course user datum ID in the error message, no? I can update the code...

I applied https://github.com/cg2v/Autolab/commit/057493b3e518376d54fa62dc74b4ac7ba46353a5 and https://github.com/cg2v/Autolab/commit/752a44f942fe65168de0de003060d073c09817ea, and that seems to have done the trick. Thanks for the pointers @cg2v!

In `NextRefinesNext`, I think you could move the `Inv(s')` into the `ensures` clause, no? It should be provable directly from `NextPreservesInv`. I assume it's necessary in the signature of `NextRefinesNext`...

As written, any caller of `NextRefinesNext` will need to invoke `NextPreservesInv`, whereas if you make the adjustment I suggested, that wouldn't be necessary.

> Do you remember why you introduced this extra check? No, at this point it looks mysterious (and redundant) to me as well. Sorry!