Check label well-formedness

[dz333]

Implement a well-formedness check for the following:

• All labels are dependent only upon variables whose labels flow to the target label (in any context)
• The lower bound of all erasure labels flow to the upper bound.
• All variables appearing in dependent types are sequential, wires, or inputs

[dz333]

This is a sub-issue of https://github.com/dz333/secverilog/issues/8

[dz333]

Ok new rule! It turns out that we don't need these well-formedness checks on seq variables. So we would like to enforce the following:

• For seq variables and wires: no restrictions or well-formedness.
• For com type regs (i.e., non-registers assigned in always blocks).
  • Use the well-formedness typing condition from the original secverilog paper: $\forall v' \in FV(\Gamma(v)). \Gamma(v') \sqsubseteq \Gamma(v)$ and $v' \neq v \implies FV(v') = \emptyset$
  • Also use the typing rules from the original SecVerilog paper (if non recursive, simple label check - if recursive then replace all instances of $v$ with interpretation of new expression and check -- also do NSU check (pc flows to current label without replacement)