Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.RecordArray

Free interleaving of two record arrays #

Two global circuits may compute different fields for every record. Running them once each and interleaving their outputs by fixed wiring combines those fields without duplicating either computation.

source
def Algebraic.MassProduction.Nonuniform.RecordArray.outputWire (records leftWidth rightWidth : ℕ) (output : Fin (records * (leftWidth + rightWidth))) :
Fin (records * leftWidth + records * rightWidth)

Interleave the left and right field blocks within every record.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.MassProduction.Nonuniform.RecordArray.combine {signature : Signature} {inputs records leftWidth rightWidth : ℕ} (left : Circuit signature inputs (records * leftWidth)) (right : Circuit signature inputs (records * rightWidth)) :
    Circuit signature inputs (records * (leftWidth + rightWidth))

    Compute both field arrays once, then interleave by free output wiring.

    Equations
    Instances For
      source
      @[simp]
      theorem Algebraic.MassProduction.Nonuniform.RecordArray.combine_size {signature : Signature} {inputs records leftWidth rightWidth : ℕ} (left : Circuit signature inputs (records * leftWidth)) (right : Circuit signature inputs (records * rightWidth)) :
      (combine left right).size = left.size + right.size

      The exact gate count of combine.

      source
      theorem Algebraic.MassProduction.Nonuniform.RecordArray.combine_eval {signature : Signature} {inputs records leftWidth rightWidth : ℕ} {Value : Type u_2} (left : Circuit signature inputs (records * leftWidth)) (right : Circuit signature inputs (records * rightWidth)) (interpretation : Interpretation signature Value) (input : Fin inputs → Value) (record : Fin records) (bit : Fin (leftWidth + rightWidth)) :
      (combine left right).eval interpretation input (finProdFinEquiv (record, bit)) = Fin.append (fun (field : Fin leftWidth) => left.eval interpretation input (finProdFinEquiv (record, field))) (fun (field : Fin rightWidth) => right.eval interpretation input (finProdFinEquiv (record, field))) bit

      Each combined record is the concatenation of the two computed fields.

      source
      theorem Algebraic.MassProduction.Nonuniform.RecordArray.combine_cost {signature : Signature} {inputs records leftWidth rightWidth : ℕ} (left : Circuit signature inputs (records * leftWidth)) (right : Circuit signature inputs (records * rightWidth)) (cost : OperationCost signature) :
      (combine left right).cost cost = left.cost cost + right.cost cost

      Interleaving adds no cost to the two global computations.