Cannot type-check floating point parameters.

[UnsignedByte]

Putting a short writeup here of some issues highlighted in comments on #325.

The following test case fails:

import "primitives/comb.fil";

comp main<'G: 1>(
  in: ['G, 'G+1] 1,
) -> (
  out: ['G, 'G+1] 1,
  floor_test: ['G, 'G+1] 32,
) {
  floor := new Const[32, floor(1.5)]<'G>();
  floor_test = floor.out;

  out = in;
}

with the following error:

thread 'main' panicked at 'called `Result::unwrap()` on an `Err` value: Custom { kind: Other, error: "Unexpected result from solver: (error \"Invalid sort of function body ' (/ 3 2) ' , expected 'Int ' \")" }', src/ir_passes/discharge.rs:424:18

The issue (in model.smt) seems to be that the expression (define-fun e6 () Int 1.5) is added because every single expr in comp is added to the solver. As the solver works only with integers, this causes the solver to error.

I think we should instead only add expressions as necessary (I.E. if they are used in a time expression or proposition somewhere).

[UnsignedByte]

This still likely won't solve the issue though, because, for example, if Const has requirements for its parameter values, we have to find a binding that satisfies these constraints, and thus floor(1.5) must somehow contain information about being > 0, and would still be needed in the type checker somewhere.

[rachitnigam]

This is even more tricky because we can't even encode the axioms for floor because it is a function over reals and not integers. It would require us to reason explicitly about Real values which will make typechecking untenable.

The restriction here probably should be that we can immediately evaluate the value of floor(1.5) before we hit the type checker. Out of curiousity, can you explain what this code is actually trying to do/being used for?

[UnsignedByte]

This is just a test using floor, but we can imagine that in the FFT with twiddle factors that we would want to do something similar but with f32_bits(sin(1/n)) to define a constant wire, which would also undergo the same problems.

Immediate evaluation doesn't solve the problem in its entirety either because we could technically want to pass floating point parameters across components, which would render them non-evaluatable, so it would only be a stopgap solution.

FWIW, it might not be worth it to create typed parameters at all; maybe we could do something like verilog's LOCALPARAM and only implement floats there that are evaluated during precompile, so that PARAMs that we actually pass around are all integers by typechecking stage.

[UnsignedByte]

Spoke to @rachitnigam about this in a meeting. We decided that in order to have a working solution, floating point parameters can never appear in typechecking expressions. This means expressions can be Clean or Dirty depending on whether they use expressions that are Clean or `Dirty. Thus, this requires a few new features:

• Parameters needed to instantiate components must also carry with them information on whether they are used in typechecking constraints. This means can either only accept Clean expressions and will be treated as such internally, or they can accept either Clean or Dirty expressions and internally are treated as Dirty.
• When instantiating, the component doing the instantiation is responsible for checking this.

In essense, a Dirtied expression will always stay so, and must be one that can be entirely ignored by the typechecker so that we can pass Dirty values around with no issue. This means that it cannot appear in constraints on parameters in the signature, nor in any liveness information.

This also allows for a third possible type: Const. Because constant values (like floor(1.5)) can be evaluated explicitely into a certain integer value, they can be used in typechecking constraints, provided they are evaluated away at runtime. This would be useful if complex calculations required intermediate floating point values, but evaluate to an integer (not sure exactly what examples there are of this).

• We could discuss how using floating point expressions in for-loops with constant length could maybe be eliminated, but that is even less important.

Because this will end up being a much bigger change than we initially anticipated, we are tabling this implementation for now and going back to the sinbits integer functions that can be implemented easily but are not chainable/super useful. I will be closing #325 for now.