Bug in Retypd Proofs Related to Contravariant Rules Over Interesting Variables

[2over12]

x <= a
x.store <= y
y <= b

The retypd github impl prints the empty set when your interesting variables are [a,b]

But consider that an elementary proof exists for the subtyping constraint a.store <= b

x <= a and x.store exists based on the proof rule InheritL subtypes should inherit fields to the left of a subtyping constraint: a.store
x <= a and a.store exists .store is contravariant so by the contravariant field rule a.store <= x.store
a.store <= x.store and x.store <= y so by transitivity a.store <= y
a.store <= y and y<= b so a.store <= b QED 

The proof graph demonstrates that the proof connections exist, however, the initial variable is contravariant. We only explore covariant paths (ie. initial cov, end cov). Observationally the path a.store <= b and b<= a.store both exist but only the first path is a valid proof.

The first thing to check is wether the above is provable in normalized form. If it is, what is the graph representation of the normal form proof and why is it not represented. The issue appears to be with proofs that have an initial contravariant field rule.

[2over12]

This is fixed in 5885449 by using the variance of the stack when linking up start edges rather than the variance of the rule. There still may be some issues here, ie. rules for uninteresting variables and issues in saturation. Negation may not be a closed operation on the graph anymore.

[2over12]

A simpler regression test case for this is can we start with y <= x.store and prove y <= x.store

[2over12]

The root of this issue seems to be that InheritL cant be simulated by S-Field like claimed. As far as i can tell only InheritR can be

[2over12]

Both of these testcases are fixed in 00971943276f973ef72555d0ad85087f9582fbe7 . The trick to admit InheritL by S-Fields is to allow proofs that begin with a covariant constraint. ie. let us start with an assumption speculatively:

assume a <= x then by S-field a <=x /\ x.store: x.store < a.store: (since we were contravariant fix to cov) a.store < x.store then apply trans.

The way we support this in the transducer is to fixup how we filter explored paths. Originally we would require that the variable we start and end with is a covariant state. Instead we now check if the starting variance multiplied by the variance of the path is covariant. This allows us to start in a contravariant state as long as we fix it up to covariant before we exit.