Type Checker Regression on Primitive/Keyless/Hash/SHA.cry

[WeeknightMVP]

cryptol-specs> cryptol Primitive/Keyless/Hash/SHA.cry
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.6.1 (f96e1e4)

Loading module Cryptol
Loading module Primitive::Keyless::Hash::SHA
[error] at Primitive/Keyless/Hash/SHA.cry:74:3--74:40:
  Failed to validate user-specified signature.
    in the definition of 'Primitive::Keyless::Hash::SHA::pad', at Primitive/Keyless/Hash/SHA.cry:74:3--74:6,
    we need to show that
      for any type Primitive::Keyless::Hash::SHA::j,
                   Primitive::Keyless::Hash::SHA::w, L
      assuming
        • fin Primitive::Keyless::Hash::SHA::j
        • Primitive::Keyless::Hash::SHA::j >= 17
        • fin Primitive::Keyless::Hash::SHA::w
        • Primitive::Keyless::Hash::SHA::w >= 1
        • 2 * Primitive::Keyless::Hash::SHA::w >= width L
      the following constraints hold:
      • Primitive::Keyless::Hash::SHA::num_blocks L *
        Primitive::Keyless::Hash::SHA::block_size >= 1 +
                                                     (L + 2 * Primitive::Keyless::Hash::SHA::w)
          arising from
          matching types
          at Primitive/Keyless/Hash/SHA.cry:74:11--74:40

[yav]

Is it possible to have a look at the code that lead to this error somewhere?

[brianhuffman]

It's in the cryptol-specs repository: https://github.com/GaloisInc/cryptol-specs/blob/master/Primitive/Keyless/Hash/SHA.cry

[brianhuffman]

With d8b1a7a, GaloisInc/cryptol-specs@e27ea10, and z3 version 4.6.0, everything works for me:

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.6.1 (f96e1e4)

Loading module Cryptol
Loading module Primitive::Keyless::Hash::SHA
Primitive::Keyless::Hash::SHA (parameterized) >

[yav]

I have Z3 4.7.1 and it appears to work on my build too. Which version are you using?

[WeeknightMVP]

> z3 -version
Z3 version 4.8.3 - 64 bit

[WeeknightMVP]

This also works on my build if I use Z3 4.7.1.

> z3 -version
Z3 version 4.7.1 - 64 bit
> cryptol Primitive/Keyless/Hash/SHA.cry 
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.6.1 (f96e1e4)

Loading module Cryptol
Loading module Primitive::Keyless::Hash::SHA
Primitive::Keyless::Hash::SHA (parameterized) > 

[brianhuffman]

I tested a few different z3 releases: It works with 4.8.1, but fails with 4.8.3.

[yav]

This seems to be an issue with z3, which is being tracked here:

Z3Prover/z3#2079

[weaversa]

This works again with the z3 released yesterday.

[WeeknightMVP]

FYSA -- Primitive::Keyless::Hash::SHA stalls with Z3 4.8.9 but works again with Z3 4.8.10.