Support Logical Intermediate Representation

[DavePearce]

The goal here is to support a simplistic "logical intermediate representation" (LIR). This would compete with MIR and, eventually, replace it. The representation needs only to support logical or (∨), logical and (∧), logical not (¬) and arithmetic equality (=, ≠). Potentially, we could extend this to support syntactic sugar, such as <, ≤, etc.

Notes

• (HIR) We should be able to "recover" logical primitives from HIR and, hence, translate from HIR => LIR. This would then mean that existing Corset constraints could be shown in LIR form.

• (Readability) We might desire to support logical implication (⇒) to enhance readability. This would make sense when compiling down from if conditions. We could have some kind of output format which looked like this:

Heartbeat:
  (I) ...
 (II) ...

• (Types) We need a way to define types, and we might want to support more complex datatypes, such as structs and arrays. Do we want to distinguish public inputs from computed witnesses?

• (Computation) Do we want a general mechanism for describing the computation for computed columns? We could just have a simple imperative language for this.

Example

This illustrates what a complete example might look like. Generating it fully from HIR might be challenging, such as for the column constructors.

module u256_lt {
   in ARG_1 : u256 
   in ARG_2 : u256 
   out RES : bool 
   // witnesses
   var STAMP : u32
   var CT : u5
   var CT_MAX : u5
   var DIFF : u256 
   var BYTE : u8
   var ACC : u256

   constraint first(0) { STAMP=0 }

   constraint stamp-inc(i) { STAMP==0 || STAMP == STAMP'+1 }

   constraint ct-reset(i) { STAMP == STAMP' || CT==0 }

   constraint heartbeat(i) {
      if CT == CT_MAX { 
        STAMP' == STAMP + 1 
      } else {
        CT^ = CT + 1
      }
   }  

   ...

   // Arbitrary computation which initialises the `BYTE` column.
   constructor(BYTE) {
     ...
   }
}

Here, X' refers to X on the previous row. For an arbitrary shift, we could have syntax like X'2 to say backwards 2 rows. Likewise, say X^ to represent X on the next row.