Change circuit translation to tuple the state instead of adding it to a record type

[eddywestbrook]

The way circuits are translated into SAW is that each circuit is translated into a SAW core term for a function from a Cryptol record of all the inputs, keyed by name, to a Cryptol record of all the outputs. For sequential circuits (i.e., circuits with state, such as flip-flops), the old value of the state is considered an input, with name "__state__", and the new value of the state is considered an output, with the same name.

E.g., a sequential circuit with inputs a and b and outputs x and y, all of 8 bits, that also has an 8-bit internal state, would have a Cryptol type that looks something like this, noting that the elements of the state type are assigned numeric names that are generated from internal details of the circuit:

{ __state__ : { z25 : [8] }, a : [8], b : [8] }  ->  { __state__ : { z25 : [8] }, x : [8], y : [8] }

The problem with this approach is that it does not allow a user to define operations over circuit representations where the operations are polymorphic in the input and output types. For instance, if we want to define a Cryptol function that maps a circuit to property of that circuit, we have to define one instance of that function for each list of input and output fields.

To solve this problem, the current PR changes the circuit translation to tuple the state with the inputs and outputs, rather than add it as a field in the records of the inputs and outputs. For instance, the above described circuit now has a Cryptol type that looks like this:

({ z25 : [8] }, { a : [8], b : [8] }  ->  ({ z25 : [8] }, { x : [8], y : [8] })

This makes it possible to write Cryptol functions that are polymorphic in the input, output, and state type of a circuit. And, indeed, there is a new example of doing this in concert with the prove_bisim command to verify circuits in the newly added intTests/test_comp_bisim test case added in this PR.

[RyanGlScott]

I have only performed a very shallow review of the PR, but this looks sensible. My only request: could you leave a high-level comment somewhere in SAWScript.Yosys.CompositionalTranslation (perhaps in the module Haddocks) saying what the new state type should be? That is helpful context to know when reading the code.

Even better would be to document the new state type conventions in the SAW manual, assuming that you have the time for that.

[eddywestbrook]

@RyanGlScott Your request for docs is reasonable, but I'd like to make that a separate PR, for reasons I'll discuss offline.