Signed bitvector primitives in specifications

[brianhuffman]

The following SAWCore primitives (mostly to do with signed bitvectors) appear in terms extracted from Java or LLVM, but are not expressible in Cryptol:

Prelude.bvUpd
Prelude.bvSDiv
Prelude.bvSRem
Prelude.bvSShr
Prelude.bvsgt
Prelude.bvsge
Prelude.bvslt
Prelude.bvsle
Prelude.bvTrunc
Prelude.bvUExt
Prelude.bvSExt

It would be very useful to be able to state theorems (especially rewrite rules) involving these operations, so we should provide some way for users to be able to express them. A possibility would be to provide a saw-script primitive of type Term for each; these could then be used within the {{ }} cryptol brackets.

[brianhuffman]

My latest idea is to provide a value of type CryptolModule (or maybe () -> CryptolModule if we need side-effects to construct it) that would contain each of the above-mentioned functions. Users could bind the module with e.g. let m = cryptol_extras() and then refer to the various primitive functions within cryptol brackets: {{ update }}, {{ bvsge }}, {{ bvsrem }}, etc.

let m = cryptol_extras();
type {{ (m::update, m::

[ntc2]

We want to do signed comparisons in the V2V project.

[brianhuffman]

To use the cryptol_prims primitive, first bind the CryptolModule result to a variable with let; then you can access the functions inside with qualified names inside the Cryptol brackets:

sawscript> let m = cryptol_prims ()
sawscript> print m
Symbols
=======
    trunc : {m, n} (fin m, fin n) => [m + n] -> [n]
    uext : {m, n} (fin m, fin n) => [n] -> [m + n]
    sgt : {n} (fin n) => [n] -> [n] -> Bit
    sge : {n} (fin n) => [n] -> [n] -> Bit
    slt : {n} (fin n) => [n] -> [n] -> Bit
    sle : {n} (fin n) => [n] -> [n] -> Bit

sawscript> print {{ m::sle 0xf 0x5 }}
True

I need to put a hint like this in the :help text for cryptol_prims.

[ntc2]

Thanks, exactly what I needed! I added your example to the tutorial (2291292). Yes, adding it the cryptol_prims help output would also be useful.

Should this issue be closed?

[brianhuffman]

The ticket is still open because cryptol_prims still doesn't include sdiv, srem, or sshr. The reason is that the corresponding prelude primitives have inconvenient types involving bitvector (Succ n), which don't match up well with types produced by the Cryptol-to-saw translation. So I'll have to fix that problem first.

[atomb]

Now that we have signed operators in Crypol for these, is there work left to do for this issue?

[brianhuffman]

I should probably remove everything from cryptol_prims that is a cryptol primitive now. And I need to make sure that cryptol_prims includes all the operators I listed above that still aren't cryptol primitives.

[brianhuffman]

Revision 514b712 adds a sign extension operator sext to cryptol_prims. I won't bother to add sdiv, srem, or sshr, since these are already Cryptol primitives. I'll keep trunc and uext because these were never Cryptol primitives. Even though there are Cryptol prelude operators for sge, sgt, and sle, they are not Cryptol primitives, so we should keep them, and we might as well keep all the signed comparisons.