[Formal][Property Annotation] Annotate Reconvergent-paths using flow variables

[Basmet0]

Each operation has local properties on how tokens are distributed between inputs and outputs. For example, a join operation expects the same number of tokens coming from each input, and sends them to its output. By extracting all of these local equations from a circuit, and then performing Gaussian elimination, one gets equations that describe properties of paths using only the internal states of the operations, rather than having to keep track of how many tokens are sent across each channel.

[Jiahui17]

APIs for accessing rows/cols

https://www.boost.org/doc/libs/latest/libs/numeric/ublas/doc/matrix_proxy.html

[Jiahui17]

using MatIntType = boost::numeric::ublas::matrix<int>;

[Jiahui17]

Maybe pull out the linear algebra stuff to dynamatic/Support/LinearAlgebra/Gaussian.h

[Jiahui17]

Add a bit more descriptions on this

https://en.wikipedia.org/wiki/Row_echelon_form

[Jiahui17]

Here we should describe the model that we assume:

every unit is a cascade of: merge/join/mux -(internal_channel1)-> [slot]* -(internal_channel2)-> fork

Rename i1 -> lambda_internal_channel1

[Jiahui17]

add a constructor: FlowVariable(...)

[Jiahui17]

Implement a separate DSL for writing flow equations

Add rationale for this:
Why don't we use CPVar from ConstraintProgramming.h:

1. Integer coefficients (int16 maybe is good enough), but CPVar always uses double
2. We can freely attach metadata type without confusing the users of ConstraintProgramming.h
3. We don't need to encode anything in the name (we don't actually need a name because we don't need any external solvers for our equations).
4. Dedicated conversion function to boost::...::matrix

struct FlowVarImpl {
std::shared_ptr<...> impl;
};

struct FlowVar {
std::shared_ptr<...> impl;
};

FlowEquation {

};

FlowExpression operator+(FlowExpression, FlowExpression);
FlowExpression operator-(FlowExpression, FlowExpression);
FlowExpression operator*(FlowExpression, FlowExpression);

[Jiahui17]

Split this function into multiple smaller ones:

• createFlowVariables
• addEquations
• solveGaussian
• ...

[Jiahui17]

We could do a separate PR for class HandshakeOpInternalState

- <forkOp> fork1 -> { fork1.sent1, fork1.sent2, ... }
- fork1.sent2 -> { "it is a sent", "the second one" }
- parse
- print
- write smv

struct HandshakeOpInternalState {
  StringRef writeSmv() virtual = 0;
  /// This is the same as the "handshake.name" of the operation
  std::string name;
  static std::optional<HandshakeOpInternalState> parse() virtual = 0;
  Operation * getOperation(NameAnalysis& namer) {
    namer.findOepration(this->name)
  }
};


struct EagerForkSent : public HandshakeOpInternalState {
  Operation * op;
  unsigned outputId;
  StringRef writeSmv() override {

  }

  // Validate that there is an op with a matching name
  std::optional<HandshakeOpInternalState> parse(NameAnalysis& namer) override {
    

  }
};

if (auto state = EagerForkSent::parse(name)) {
  ...
} else if (auto state = BufferFull::parse(name)) {
  ...
} 

...

[Jiahui17]

std::vector is better here

[Jiahui17]

We could unify Matrix and its index management as a single struct

class -> struct because we are not hiding anything

[Jiahui17]

Maybe add a link to some referneces