Constraint fails to be proven

[mariosge]

The following function definition is not accepted:

id : {k} (fin k, k > 0) => [2^^k] -> [2^^k]
id x = join(split`{2,2^^(k-1)}x)

The corresponding error is:

[error] at test.cry:2:1--2:33:
  Failed to validate user-specified signature.
    in the definition of 'Main::id', at test.cry:2:1--2:3,
    we need to show that
      for any type k
      assuming
        • fin k
        • k > 0
      the following constraints hold:
        • 2 ^^ k == 2 * 2 ^^ (k - 1)
            arising from
            matching types
            at test.cry:2:8--2:12
        • 2 * 2 ^^ (k - 1) == 2 ^^ k
            arising from
            matching types
            at test.cry:2:31--2:32

I encountered this in version:

 ✗ cryptol --version
Cryptol 2.13.0.99

[weaversa]

The quick answer is to add one of the constraints to the type definition --

id : {k} (fin k, k > 0, 2 ^^ k == 2 * 2 ^^ (k - 1)) => [2^^k] -> [2^^k]
id x = join (split`{2,2^^(k-1)} x)

And now this type checks appropriately.

The long answer is that Cryptol's type inference engine doesn't know enough about exponentiation to know that the constraints it is suggesting are the ones you actually want. For instance, see #704 and #1381. I think your example is included in the discussion already in #704.

[rod-chapman]

This kind of constraint also crops up in algorithms like the MLKEM NTT, which recursively splits a sequence in 2, works on the sub-sequences, then catenates the results. It would be good if the solver could see that 2 ^^ k == 2 * 2 ^^ (k - 1) really is OK.

[andrew-bivin]

We will be addressing this issue in our next dev cycle - updates soon!