Refactor evopts

[robdockins]

Builds on PR #985

This refactors how evaluation options are piped into primitives, and makes them work in a less surprising way. Currently, this only affects the trace and traceVal functions. This change makes it pretty straightforward to have the symbolic and concrete evaluators work uniformly with the same implementation for trace.

[weaversa]

I don't know if this is the right place, but having trace work in the symbolic backends reminded me of a feature we used to have in Cryptol 1. It used to be that Cryptol could symbolically execute any valid expression vi a :fm command (which generated a formal model, either an sbv file or aig). If a trace statement was used in the expression, the trace value would be printed, and if the value was trivially concrete it would print the concrete values. If the value was symbolic, Cryptol would print #. This even worked at the bit level, so a partially symbolic value could be seen. There's an example below (Cryptol 1.8.27 still works!). This was useful for determining whether or not a function was symbolically terminating. This was also useful for determining how many steps were needed to flush out / initialize the internals of pipelined, hardware-based algorithms.

I don't know if this is something we could do atm, but thought I would bring it up in case stars align.

Cryptol> :fm (\x -> [| trace ("value", x << y, x << y : [10]) || y <- [0..10] |])
["command line", line 1, col 10] value: ##########
["command line", line 1, col 10] value: #########0
["command line", line 1, col 10] value: ########00
["command line", line 1, col 10] value: #######000
["command line", line 1, col 10] value: ######0000
["command line", line 1, col 10] value: #####00000
["command line", line 1, col 10] value: ####000000
["command line", line 1, col 10] value: ###0000000
["command line", line 1, col 10] value: ##00000000
["command line", line 1, col 10] value: #000000000
["command line", line 1, col 10] value: 0b0000000000

[robdockins]

Right now, the symbolic simulators print a dummy string [?] when they encounter symbolic values, but will otherwise print concrete values just as in the concrete simulator. We could probably extend that to bit-level (or maybe digit-level, depending on the base setting) values and get something pretty close to that.

[robdockins]

For example, on this branch, we currently get the following results:

Cryptol> :set base=2
Cryptol> let f x = [ traceVal "value" (x << y : [10]) | y <- [0..10] ]
Cryptol> :safe f
value [?]
value [?]
value [?]
value [?]
value [?]
value [?]
value [?]
value [?]
value [?]
value [?]
value 0b0000000000
Safe

[robdockins]

Turns out, it isn't too difficult to get this working. You'll get better results using the What4 provers in this case; SBV seems less able to figure out when individual slices of a bitvector are concrete.

Cryptol> :set prover=w4-z3
Cryptol> :set base=2
Cryptol> let f x = [ traceVal "value" (x << y : [10]) | y <- [0..10] ]
Cryptol> :safe f
value 0b??????????
value 0b?????????0
value 0b????????00
value 0b???????000
value 0b??????0000
value 0b?????00000
value 0b????000000
value 0b???0000000
value 0b??00000000
value 0b?000000000
value 0b0000000000
Safe

[weaversa]

🥳