Declarations with indexing on the left-hand side

[brianhuffman]

I thought it might be nice to be able to write declarations like this:

sbox : [256][8]
sbox @ i = gf28Inverse (xformByte i)

The idea is that like defining a function by writing an argument on the left-hand side, we should also be able to define lists by writing an indexing operator on the left-hand side. The index variable is then in scope on the right-hand side, so the element value can be defined in terms of the index.

I think this feature would let us write Cryptol specs that more obviously match the official reference spec, because sequence-indexing notation is commonly used in papers that describe crypto algorithms.

Currently our usual approach when translating a spec to Cryptol is to define sequences of values using recursive list comprehensions. The problem is that this makes all the indexing implicit, when it is usually explicit in the original paper, so it's harder to see that the two are the same. Making the indexing explicit in Cryptol should make our specs more obviously correct.

Implementation should be a straightforward desugaring. Basically f @ i = expr would be translated as f = generate (\i -> expr), where generate is a new prelude function or primitive:

generate : {n, ix, a} (fin ix, fin n, n >= 1, ix >= width (n - 1)) => ([ix] -> a) -> [n]a
generate f = [ f i | i <- [0 .. n-1] ]

[yav]

Since I was just looking at this stuff: if we implement this, we should probably add it to record construction too (maybe update, not sure). Here is an example of what I mean:

// Currently we support this:
type T = { fun1  : [8] -> [8], fun2 : [16] -> [16] }

funs : T
funs = { fun1 x = x + 1, fun2 x = x - 1 }
// special notation for defining function fields

// With what you propose above we should probably allow it in records also:
type S = { vals1 : [8][8], vals2 : [16][8] }

lists : S
lists = { vals1 @ i = 3, vals2 @ i = i + 1 }
// special notation for defining sequnce fields

[atomb]

I like this idea.

[atomb]

Not only do I like this idea in the abstract, I'm now implementing an algorithm that's specified in a way that would line up very nicely with this notation. It would make the Cryptol and the PDF match very closely.

[brianhuffman]

This feature is implemented in pull request #609.