See trailofbits/sv_circuit#13

This should be another one of our export formats.

For right now, our pipeline is required to pass though a tiny86.blif. BLIF compilation places reasonable constraints on the input HDL, is useful for CI verification, and as a common "interchange format". However, JSON ingestion is preferred for debugging because it includes source information, e.g.:

# ...
"syscall_x": {
  # ...
  "instr_len": {
    # ...
    "attributes": {
      "src": "circuit/tiny86.v:69.6-69.17",
      # ...
    }
  }
}
# ...

If ingesting yosys-produced JSON parses to the same impl Parser<T: WireValue>, this could feasibly be used to propagate Verilog source-level information to lower pipeline artifacts.

First question r.e. the circuit you provided us. It looks like it's missing the metadata of # inputs and # outputs (as specified here: https://homes.esat.kuleuven.be/~nsmart/MPC/). Is that something you could augment the circuit to support?

Right now, the internal representation of our gates/operations is a big enum, with value variants that look like this:

/// Defines the individual logic gate operations we can support
#[derive(Clone, Copy, Debug, Serialize, Deserialize, PartialEq, Eq, VariantCount)]
pub enum Operation<T: WireValue> {
    /// Read a value from input and emit it on the wire
    Input(usize),
    /// Emit a random value on the wire
    Random(usize),
    /// Add the two wires together
    Add(usize, usize, usize),
    /// Add the wire and the constant
    AddConst(usize, usize, T),
    /// Subtract the final wire from the second wire
    Sub(usize, usize, usize),
    /// Subtract the constant value from the wire
    SubConst(usize, usize, T),
    /// Multiply the two wires together
    Mul(usize, usize, usize),
    /// Multiply the first wire by the constant value
    MulConst(usize, usize, T),
    /// Assert that the wire has the const value zero
    AssertZero(usize),
    /// Emit the const value on the wire
    Const(usize, T),
}

...where each usize is an identified wire. This is unambiguous in the current context (since constant values are represented by the T bound), but it's not ideal from a design perspective -- enumerated wires should instead by newtyped as Wire.

Low priority, since this will require a great deal of refactoring.

I removed some comments in e706805 - these suggestions should be implemented given the latest IR0+ spec.

Right now, the Bristol-fashion exporter API is just a collection of functions. We should make it a trait, so that different formats can implement it.

A rough sketch:

pub trait ExportFormat<T: WireValue> {
  fn export_gate(gate: &Operation<T>, sink: &mut impl Write) -> Result<()>;

  fn export_circuit(gates: &[Operation<T>], witness: &[T], sink: &mut impl Write) -> Result<()>;
}

Right now this functionality is marked as "private":

We should support some kind of JSON export, for debugging/golden testing.

          > LGTM after changes for DISTAR compliance. Thanks!

Should these DISTAR compliance quotes be backported to sholva? They don't fully match.

Originally posted by @jleightcap in trailofbits/sv_circuit#27 (comment)