Base case for enumerations

[weaversa]

Cryptol> [1..3]
[1, 2, 3]
Cryptol> [2..3]
[2, 3]
Cryptol> [3..3]
[3]
Cryptol> [4..3]

[error] at <interactive>:1:1--1:7:
  Unsolvable constraints:
    • 3 >= 4
        arising from
        use of finite enumeration
        at <interactive>:1:1--1:7
    • Reason: It is not the case that 3 >= 4

I am advocating here that [4..3] should result in [] rather than an error. I'm fine if [5..3] gives an error, but I would like to be able to create an enumeration with no elements.

This comes from trying to create a Cryptol spec of RC2 (https://tools.ietf.org/html/rfc2268). Namely, this loop here:

   for i = T, T+1, ..., 127 do
     L[i] = PITABLE[L[i-1] + L[i-T]];

T is a type variable that ranges from 1 to 128 inclusive, and when T is 128 we don't enter the loop. It is possible to write this in Cryptol, but it's not as clean as it could be.

    L = K
      # [ PITABLE@(L@(i-1) + L@(i-`T))
        | i <- take [`T ... ] ] : [128][8]

I'd rather like to write something like:

    L = K
      # [ PITABLE@(L@(i-1) + L@(i-`T))
        | i <- [`T .. 127 ] ] : [128][8]

An alternative way to write it is like so:

    L = K # (drop`{T} L') : [128][8]
    L'@i = PITABLE@(L@(i-1) + L@(i-`T))

But even so I'd still like use the loop bounds from the spec, like so, but this doesn't work when T = 128:

    L = K # L'@@[T..127]
    L'@i = PITABLE@(L@(i-1) + L@(i-`T))

[weaversa]

In the same vein, the base case for enumerations using decimation actually is []

Cryptol> [2, 1 .. 2]
[2]
Cryptol> [2, 1 .. 3]
[]

But the type system won't allow it. Consider this from the same RC2 spec:

   for i = 127-T8, ..., 0 do
     L[i] = PITABLE[L[i+1] XOR L[i+T8]];

Here we would want to write something like [ ... | [127-T8, 127-T8 - 1 ... 0] ], but when we do the type inference engine asserts that T8 has to be big enough for the subtraction to stay positive (of course T8 also ranges in RC2 from 1 to 128 inclusive).

[robdockins]

Right now, the type for enumerations looks like:

/**
 * A finite sequence counting up from 'first' to 'last'.
 *
 * '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'.
 */
primitive fromTo : {first, last, a} (fin last, last >= first,
                                    Literal first a, Literal last a) =>
                                    [1 + (last - first)]a

If we change 1 + (last - first) to (1 + last) - first and last >= first to 1 + last >= first, things might just work out, at least for the [4 .. 3] case.

[brianhuffman]

I totally misread the example code as PITIABLE at first, which seemed like it might be an indirect comment on the state of the language :)

Anyway, I've also run into this problem of not being able to make enumerations of the form [0..n-1] or [1..n] that can also work at length 0. Some kind of language modification/extension to allow this would definitely be useful.

I have to say that I'm not a fan of [4..3], for two reasons: To the uninitiated it is not at all suggestive of what it is supposed to mean. One might reasonably expect [4..3] to mean [4,3], for example. Also, it doesn't work if you want your numbering to start at 0; we can't write [0 .. -1] (or [0..n-1] when n is 0) because we don't have negative natural numbers.

The Isabelle standard library defines a half-open interval notation [a..<b], which I think would be a nice option for Cryptol. Then if we want a list of length n starting with 0 or k we could write [0..<n] or [k..<n+k], and these would work even when n is 0. Also I think the meaning is pretty clear even for someone who hasn't seen the notation before.

[robdockins]

I like the idea of having a half-open interval; I've definitely wanted to write things like [0 .. n) before. I'm OK with the syntax, as long as we can get the lexer/parser to accept it without too much trouble.

I don't think it helps with the [ ... | i <- [127-T8, 127-T8 - 1 .. 0] ] form. That seems a lot harder to handle, though.

[yav]

One of the reasons we didn't do open intervals is that things get tricky if the upper bound is not representable in the same type as the elements in the enumeration (e.g., things like [0 .. 256)] : [256][8]).

I know this is not what @weaversa was asking for, and I am sure we could work something out, I am just mentioning it because I remember it being a bit tricky.

[robdockins]

The additional thing that might be nice is other options for specifying "down from" enumerations other than the current [n, n-1, ... 0 ] syntax. One problem with this is that n-1 requires n >= 1. Maybe something like [n .. 0 by -1 ], so you can explicitly set the stride, which is usually what you care about anyway.