SHA3: Explicitly name the underlying Keccak instance

[glguy]

This enables external verification in to access the underlying Keccak primitives as used in a SHA3 instantiation. In particular this support compositional verification activities against refined specifications.

[glguy]

This allows me to relate internal functions of the the cryptol-specs version of SHA3 to my refined one which allows efficient compositional verification. Here's an example of what that looks like:

thm_pi <- prove_pretty "π equivalent"
    rme
    {{ Spec::pi === Ref::Keccak::π }};

for [0, 1, 20, 81, 1024, 1025] (\N ->
    prove_pretty (str_concat "Reference equivalent " (show N))
        do {
            goal_eval_unint ["Spec::pi", "Ref::Keccak::π"];
            simplify (addsimp thm_pi empty_ss);
            w4_unint_rme ["Ref::Keccak::π"];
        }
        {{ Spec::hash`{N} === Ref::hash }}
);

π equivalent
Time: 0.004215s

OK
Reference equivalent 0
Starting RME
Time: 2.228779s

OK
Reference equivalent 1
Starting RME
Time: 2.297238s

OK
Reference equivalent 20
Starting RME
Time: 2.341336s

OK
Reference equivalent 81
Starting RME
Time: 2.46238s

OK
Reference equivalent 1024
Starting RME
Time: 4.893666s

OK
Reference equivalent 1025
Starting RME
Time: 4.884365s

[glguy]

This pattern would also be relevant in: AES_GCM_SIV, SHAKE128, and SHAKE256

[marsella]

I'm fine with this change. Do you want me to rewrite the others similarly?

[marsella]

I'm merging despite CI failures because I do not think those are related.

[glguy]

I'm fine with this change. Do you want me to rewrite the others similarly?

I think it's probably a good practice to always name these imports; I just didn't want to make the change any harder to get merged than necessary.