Checking sharing with `for` loops

[rachitnigam]

Checking sharing with `for` loops

[gabizon103]

@rachitnigam question about (1): I don't think the loop guarantees that each use of A is separated from other uses by i cycles; the way this loop is written, each use of A is separated only by 1 cycle. So if A has a delay of 2, we would want to throw an error here because we can only use it every 2 cycles, but we would have a bunch of uses like A<G>, A<G+1>, A<G+2>, and so on. A correct program should have uses A<G>, A<G+2>, A<G+4>, and so on. In the above example, if we check i >= delay, we would only catch this because the loop starts at 0, which doesn't seem rigorous enough because if the loop were to start at 3 (for example), we would generate uses A<G+3>, A<G+4>, .... These uses conflict with each other but would pass the i >= delay constraint.

This makes me think if it would make things easier to tweak the for loop syntax to be something along the lines of
for (i in 0..N, i = i+2) so we can do something like require that the increment to i be greater than the delay of the component being invoked, because the increment is what actually determines if the uses are separated by enough time. Of course, the example above can also be tweaked to invoke A at <G+2*i> but this initially seems (1) less readable and (2) harder to generalize into a concise compile-time check, since in my head this check on invocations makes the most sense only in relation to other invocations. If we do this, we might have to impose some more restrictions on the event offsets that can be used in invocations.

A bit lower level, but for (1) I figure that we want to add constraints saying i >= delay of A - but doesn't this run into the problem we talked about earlier about how Facts get hoisted? I'm not familiar with the specifics of the discharge pass, but if we generate a bunch of constraints saying i >= some d, I have a feeling they won't ever get meaningfully discharged (with i having the right binding) with the current setup

[rachitnigam]

Yup! You’re absolutely right about this! Some sort of structured “step” syntax seems useful because it keeps the constraints simple/tractable. I think I have an idea on how we can generalize this a bit more. Let’s schedule some time to talk?

[gabizon103]

Cool! When would be a good time to talk?