Constraints on Existential Parameters

One of the current limitations of existential parameters is the inability to describe relationships between two components' existential parameters. Currently in the type system (smt solver) we already represent (non-opaque) existential parameters as a result of a function on input parameters. Therefore, we could theoretically provide this information in existential parameter constraints.

For example, one of the cases where this issue pops up is when using floating point addition or negation.

We have something like the following:

comp FAdd[E, M]<'G:1>(
  X: ['G, 'G+1] W,
  Y: ['G, 'G+1] W,
) -> (
  R: ['G+L, 'G+L+1] W,
) with {
  some W where W == E + M + 1;
  some L where L >= 0;
} { ... }

comp FSub[E, M]<'G:1>(
  X: ['G, 'G+1] W,
  Y: ['G, 'G+1] W,
) -> (
  R: ['G+L, 'G+L+1] W,
) with {
  some W where W == E + M + 1;
  some L where L >= 0;
} { ... }

where subtraction has the same latency of an addition, only adding an inverter on Ys sign bit.

I propose being able to rewrite FSub's constraints on L as follows:

comp FSub[E, M]<'G:1>(
  X: ['G, 'G+1] W,
  Y: ['G, 'G+1] W,
) -> (
  R: ['G+L, 'G+L+1] W,
) with {
  some W where W == E + M + 1;
  some L where L == FAdd[E, M]::L;
} { ... }

Which will then allow us to place additions and subtractions in parallel without having to add assumptions or unused registers.

cucapra / filament

Constraints on Existential Parameters #450