[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]

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]

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)) {
  ...
} 

...