Translation of Cryptol parallel comprehensions introduces unnecessary coercions

[robdockins]

Consider this definition from the Cryptol prelude

zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
zip xs ys = [(x,y) | x <- xs | y <- ys]

When translated to SAWCore we get:

\(n : Cryptol.Num) ->
  \(a : isort 0) ->
    \(b : isort 0) ->
      \(xs : Cryptol.seq n a) ->
        \(ys : Cryptol.seq n b) ->
          let { x@1 = a * b
                x@2 = Cryptol.tcMin n n
              }
           in Prelude.coerce (Cryptol.seq x@2 x@1) (Cryptol.seq n x@1)
                (Cryptol.seq_cong1 x@2 n x@1
                   (Prelude.unsafeAssert Cryptol.Num x@2 n))
                (Cryptol.seqMap x@1 x@1 x@2
                   (Prelude.uncurry a b x@1 (\(x : a) -> \(y : b) -> (x,y)))
                   (Cryptol.seqZip a b n n xs ys))

Notice we are coercing from seq (tcMin n n) (a*b) to seq n (a*b). This arises from the semantics of Cryptol's parallel comprehensions, where branches may be different lengths. However, it the fairly common case where they are actually the same length, this coercion is unnecessary and makes reasoning about the resulting term much harder (e.g., after extraction to Coq).

It would be nice if we could notice this situation and use a more direct SAWCore zipping primitive that unifies the input and output types, and avoid the need for coercions.

[brianhuffman]

So basically, what we need is a variant of Cryptol.seqZip that has a more specific type

seqZipSame : (a b : sort 0) -> (n : Num) -> seq n a -> seq n b -> seq n (a * b);

instead of

seqZip : (a b : sort 0) -> (m n : Num) -> seq m a -> seq n b -> seq (tcMin m n) (a * b);

and then make the translator use seqZipSame whenever the length types are obviously the same. Sounds reasonable to me.

(Actually, I'm really not a fan of how Cryptol allows comprehension branches to have different lengths, because in my experience the implicit truncation can lead to bugs. I'd prefer for Cryptol to require all comprehension branches to have the same length, which would simplify both Cryptol's typing rules and the SAW translation.)

[robdockins]

Indeed, that's basically what I had in mind.

As to restricting comprehensions to be the same length... I don't hate that idea, but I think it would break a lot of idiomatic Cryptol; lots of recursive stream definitions would need to add a take in various places.

[robdockins]

Is there a particular reason we made the SAWCore zip a primitive?

-- Zip together two lists (truncating the longer of the two).
primitive zip : (a b : sort 0) -> (m n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) (a * b);

It seems like we could just have easily defined it as:

zip : (a b : isort 0) -> (c : sort 0)
        -> (a -> b -> c)
        -> (m : Nat) -> (n : Nat) -> Vec m a -> Vec n b -> Vec (minNat m n) c;
zip a b c f m n x y = gen (minNat m n) c (\ (i : Nat) -> (at m a x i, at n b y i));

[brianhuffman]

I just dived into the git history, and I found that zip was originally introduced to the saw-core prelude under the name vZip back in 2014 (1f75778). The generate primitive already existed at that time, but it used type Fin n instead of Nat. So defining vZip in terms of generate would have required some gymnastics to make the indexing operations type check. That's probably why it's a primitive.

[brianhuffman]

The Fin-based function generate was superseded by the Nat-based gen in 2015 (6778846 and 89d7899).

[robdockins]

Do you think we should leave it as-is, or use the proposed defined version above?