Dilithium imports missing

[ramsdell]

: At root of cryptol-specs $ cryptol Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumRecommended.cry ┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃ ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹ ╹ ┗━┛┗━╸ version 2.12.0 https://cryptol.net :? for help

Loading module Cryptol Loading module Primitive::Keyless::Hash::keccak Loading module Common::utils Loading module Common::bv Loading module Common::mod_arith Loading module Primitive::Asymmetric::Signature::Dilithium::test::test_latest Loading module Primitive::Asymmetric::Signature::Dilithium::Round2::DilithiumParameterized [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:458:27--458:40 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:458:58--458:72 Value not in scope: SHA3::SHAKE128 [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:458:80--458:93 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:476:22--476:35 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:476:50--476:64 Value not in scope: SHA3::SHAKE256 [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:476:72--476:85 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:504:30--504:43 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:504:61--504:75 Value not in scope: SHA3::SHAKE256 [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:504:83--504:96 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:518:18--518:31 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:518:52--518:66 Value not in scope: SHA3::SHAKE256 [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:518:74--518:87 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:528:34--528:47 Value not in scope: SHA3::toBytes [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:528:62--528:76 Value not in scope: SHA3::SHAKE128 [error] at /Users/ramsdell/rep/cryptol-specs/Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumParameterized.cry:528:84--528:97 Value not in scope: SHA3::toBytes Loading module Cryptol Cryptol>

[RyanGlScott]

I'm fairly sure that this is due to a recent refactoring in d15c5d035266b6b68db44ff67a332885ff25be3d. That commit moved some definitions out of Primitive::Keyless::Hash::keccak, but DilithiumRecommended.cry appears not to have been updated in the process.

[ajayeeralla]

But I can compile without errors the version on the master branch though. I'm wondering which branch were you compiling?

[pnwamk]

I can reproduce the issues on a fresh master:HEAD with Cryptol 2.12.0 (specifically 3371266ed6dc614eeac1706d82e0caf6c67a9975 of this repository); I believe these issues should be fixed when we merge this PR: https://github.com/GaloisInc/cryptol-specs/pull/43

[mccleeary-galois]

We need to ensure this is still relevant and still a bug.

[marsella]

This loads fine for me.

[mccleeary-galois]

cryptol Primitive/Asymmetric/Signature/Dilithium/Round2/DilithiumRecommended.cry

This appears to no longer be an issue. Closing.