Some proofs are broken with modern SAW and Cryptol

[sauclovian-g]

First, some background: the SAW repository runs some of the proofs from this repo as part of its CI tests. This led us to notice when the ancient nightly SAW build that it had been using finally disappeared.

Updating the Docker container to download the latest SAW release (1.2, see pull request #78) instead revealed that while some of the proofs (including the ones used in the SAW CI) work with modern SAW and Cryptol, some don't.

We are merging that change anyway on the grounds that having 2/5 of the CI jobs broken beats having all of them broken because there's no SAW download.

For reference, since the build results in the pull request may not remain available, there are five jobs in this repo's CI:

• Proofs / proofs (proof/memory_safety.saw), which succeeds
• Proofs / proofs (proof/functional_proofs.saw), which fails as described below
• Proofs / proofs (proof/correctness_add.saw), which succeeds
• Proofs / proofs (check), which succeeds
• Proofs / proofs (proof/bulk_addition.saw), which fails as described below.

Beware, also, that proof/correctness_add takes nearly six and a half hours to run, though it does run to completion successfully.

The observed failure is:

[05:48:33.368] Loading file "/workdir/proof/cryptol_imports.saw"
[05:48:34.092] Stack trace:
"include" (/workdir/proof/functional_proofs.saw:22:1-22:8)
Cryptol error:
Error:  at :1:1--1:1
    Type not in scope: validHMACSizes

Verification failed in proof/functional_proofs.saw
Error: Process completed with exit code 2.

This is not a SAW issue; it appears to be bitrot related to changes in the import semantics from Cryptol 2.x to 3.x. It can be replicated with a current Cryptol as follows:

% cd spec
% CRYPTOLPATH=../cryptol-specs cryptol KeyGen.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.2.0.99 (0985325)
https://cryptol.net  :? for help

Loading module Cryptol
Loading module Common::Set
Loading module Common::Morphism
Loading module Common::Field
Loading module Polynomial
Loading module Common::ModDivZ
Loading module Common::bv
Loading module Common::mod_arith
Loading module PrimeField
Loading module ExtensionField
Loading module ShortWeierstrassCurve
Loading module Parameters
Loading module `where` argument of Primitive::Keyless::Hash::SHA256
Loading interface module `parameter` interface of Primitive::Keyless::Hash::SHA
Loading module Primitive::Keyless::Hash::SHA
Loading module Primitive::Keyless::Hash::SHA256
Loading interface module `parameter` interface of Primitive::Symmetric::KDF::HKDF
[error] at :1:1--1:1
    Type not in scope: validHMACSizes
Loading module Cryptol
Cryptol> 

It is not clear how much work or finagling it would take to fix this, or how many other further problems there might be. The module that validHMACSizes is supposed to come from is in the cryptol-specs tree; the version of cryptol-specs used here is very old and updating it is likely a can of worms.

It is possible that changing the SAW download to an earlier release might make things run again without needing actual work in the specs; we haven't explored that. You can change the downloaded version around freely without worrying about breaking the SAW CI -- the SAW CI always tests with current SAW.

[sauclovian-g]

I should also note that we currently don't know if correctness_add taking six and a half hours is expected or represents a performance regression in SAW or some other problem. (It is not one six-hour proof; it's a lot of proofs, of which the longest two take about 75 minutes each.) If anyone seeing this does know/remember, get in touch...