This PR brings together the work of the past weeks into a top-level type+memory safety proof of crypto_kem_keypair_derand() -- with only NTT and SHA3 axiomatized, but all other lower level functions specified and proved.
A few changes had to be made to the existing lower level proofs -- see the individual commit messages for details.
This PR brings together the work of the past weeks into a top-level type+memory safety proof of
crypto_kem_keypair_derand()-- with only NTT and SHA3 axiomatized, but all other lower level functions specified and proved.A few changes had to be made to the existing lower level proofs -- see the individual commit messages for details.