Normalize Cryptol types on import

[samcowger]

Cryptol has a normalization procedure for types. One of the things this procedure does is to put constants in types on the left. For example, if partial instantiation leads to a type that looks like n * 3, the type will be rewritten to 3 * n. Consider partially instantiating split:

Cryptol> :t split
split : {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a
Cryptol> :t split`{parts=4}
split`{parts = 4} : {n, a} (fin n) => [4 * n]a -> [4][n]a
Cryptol> :t split`{each=3}
split`{each = 3} : {n, a} [3 * n]a -> [n][3]a

Now consider the Cryptol term \x -> split`{each=3} x - in particular, consider importing this term into SAWCore. Cryptol typechecking and type normalization is performed on the term at large. SAW then steps in to convert this expression to a term in Core, which involves lightweight interaction with the type environment Cryptol has built.

When SAW sees split`{each=10} and needs its type, it uses Cryptol.TypeCheck.TypeOf.fastTypeOf, which reports that it is [parts * each]a -> [parts][each]a instantiated where each maps to 3. That instantiation is performed without normalization (via Cryptol.TypeCheck.TypeOf.simpleSubst), leading to a type that looks like [parts * 3]a -> [parts][3]a.

When SAW sees x in argument or value position, it uses fastTypeOf again, which delegates to the typing environment that Cryptol has built with normalization, and reports that x's type is [3 * parts]a.

Since these terms are not "the same", SAW resorts to type coercion to construct its Core representation, and ends up with something that looks like this:

\(u1229 : Num) ->
  \(u1230 : isort 0) ->
    \(x : seq (tcMul (TCNum 3) u1229) u1230) ->
      ecSplit 
        u1229 
        (TCNum 3) 
        u1230
        (coerce 
          (seq (tcMul (TCNum 3) u1229) u1230) 
          (seq (tcMul u1229 (TCNum 3)) u1230)
          (seq_cong1 
            (tcMul (TCNum 3) u1229) 
            (tcMul u1229 (TCNum 3)) 
            u1230 
            (unsafeAssert 
              Num 
              (tcMul (TCNum 3) u1229) 
              (tcMul u1229 (TCNum 3))))
          x)

These coercions are plainly unnecessary, though not technically unsound. Whether or not this constitutes a bug, it is certainly unexpected behavior, and impacts usability of conducting Cryptol proofs in SAW. I see two ways to fix this.

The first, which I've done here, is to apply Cryptol's type normalization procedure (via Cryptol.TypeCheck.SimpType.tRebuild) when SAW imports Cryptol types as Core terms. This doesn't actually avoid generating coercions during the conversion process, but causes coercions to cite Refl as evidence for their validity, which (it seems) lets them be eliminated automatically elsewhere in the conversion process. With this fix in place, SAW now generates Core for \x -> split`{each=3} x that looks like:

\(u1229 : Num) ->
  \(u1230 : isort 0) ->
    \(x : seq (tcMul (TCNum 3) u1229) u1230) -> 
      ecSplit u1229 (TCNum 3) u1230 x

The second is to apply the same normalization in fastTypeOf, within Cryptol. I didn't do this for fear that it would subvert the "fast" nature of that function, and because I don't have a good sense of the ripple effect that change might produce, but it may be better at encapsulating Cryptol's notion of type normalization than my fix here.

(Forgive the amount of text accompanying such a small change - writing this helped me better understand SAWCore and Cryptol, and I hope it may do the same for others.)

[RyanGlScott]

This seems plausible, and the fact that all of the tests continue to pass is encouraging. @chameco, can you think of any downside of doing this?

One request: it sounds like you have a proof that was made difficult without this feature. Can you add that proof as a test case?

[chameco]

This seems like a good change to me - I think our existing large SAW proofs almost exclusively work with monomorphic Cryptol functions, and the tests passing is encouraging.

[samcowger]

One request: it sounds like you have a proof that was made difficult without this feature. Can you add that proof as a test case?

I've done so, though the test is a little contrived.

[eddywestbrook]

@samcowger this seems like a useful change. Please don't forget to get it merged!