Cryptol translation is broken for terms using Arith and Cmp operations

[brianhuffman]

In the saw-script REPL, simple prove commands are now failing:

prove z3 {{ \(x:[8]) -> x == x }}
prove: 1 unsolved subgoal(s)
Invalid: [x = 255, _ = 0]
sawscript> prove z3 {{ \(x:[8]) -> x != x + 1 }}
"prove" (<stdin>:1:1):
"z3" (<stdin>:1:7):
valRecordSelect: Not a record value: ("add",<<bitvector>>)

It turns out that terms involving Arith and Cmp are now being translated incorrectly, as we can see:

sawscript> print_term (rewrite (cryptol_ss()) {{ \(x:[8]) -> x == x }})
let { x0 = Prelude.Vec 8 Prelude.Bool;
    }
 in \(x::x0) -> Prelude.eq x0 x
sawscript> print_term (rewrite (cryptol_ss()) {{ \(x:[8]) -> x + 1 }})
\(x::Prelude.Vec 8 Prelude.Bool) ->
  x.add (Prelude.bvNat 8 1)

The current translator maps Cryptol props Arith and Cmp to dictionaries (i.e. records of functions) in SAW. (Other props like "m >= n" that have no computational content are erased.) This worked before, but since the merge of the wip/solver branch of Cryptol, type substitution automatically rewrites e.g. "Cmp [8]" to "True", so the translator doesn't know to create the dictionaries it needs.

[brianhuffman]

I have an idea for a fix that only involves the cryptol-verifier package (no modifications to Cryptol will be required). Basically, we will have a single dictionary type that includes all of the Arith, Cmp, and logical operations; we will construct and apply an appropriate dictionary on every type application.