Linearity check for port assignments about filament

[rachitnigam]

How to encode coverage constraints for Filament's linearity check?

For example:

bundle a{#K+1};
a{0} = 20
for #i in 0..#K-1 {
  a{#i+1} = 30
}
a{#K} = 10

The following asks whether there is any point that is not any of these indices:

exists #p. 
  #p \in [0, K] /\                   -- (1)
  (
    !(#p == 0) \/                    -- (2)
    !(#p >= 1 /\ #p < K) \/          -- (3)
    !(#p == #K)                      -- (4)
  )

Constraints are:

1. #p is a valid index into the bundle
2. #p is not {0} which is written to in the first write
3. #p is not in the range implied by [0, K-1) incremented by 1 because of the #i+1 expression
   1. It's not clear how to support a{2*#i} or other expressions which don't generate continuous sets.
4. Same as (1)

Since p is implicitly existentially quantified, we can just ask the solver to provide a model and there is a model, then we've found an index that is not assigned to.

[rachitnigam]

Another approach is using forall (😭 ):

exists #p. 
  #p \in [0, K] /\                         -- (1)
  (
    #p != 0) \/                            -- (2)
    (forall #i. 
	    #i >= 0 /\ #i < K-1 /\ #p != #i+1) -- (3)
	\/          
    #p != #K                               -- (4)
  )

While annoying, this does get around the problem of dealing with complex indexing expressions like 2*#i. The final approach is making this a best effort check and leave it to monomorphization to track if all locations in a bundle are assigned to.

[rachitnigam]

Subsumes #46

[rachitnigam]

Much like #85, this is not strictly required for Filament's type soundness guarantees. The type soundness guarantee only holds if all the ports are linearly assigned. However, I think it makes sense to keep this around if not for parametric modules then at least as a elaboration check