Crash when an override has fewer state refinements than the method it overrides #462

Impact: the verifier crashes on a valid program when an override has fewer @StateRefinements than the method it overrides.

Minimal reproducer

@StateSet({"off", "on"})
class A {
    @StateRefinement(to = "off(this)")
    A() {}

    @StateRefinement(from = "off(this)", to = "on(this)")
    @StateRefinement(from = "on(this)", to = "off(this)")
    void toggle() {}

    @StateRefinement(from = "on(this)")
    void use() {}
}

class B extends A {
    @Override
    @StateRefinement(from = "off(this)", to = "on(this)")
    void toggle() {}
}

class Client {
    static void f() {
        B b = new B();
        b.use();
    }
}

Actual: on main @ 19991d3:

Error while checking CtMethodImpl
  on toggle() {}
  at A.java:17
  with Index: 0
Caused by: java.lang.IndexOutOfBoundsException: Index: 0

That first crash comes from AuxHierarchyRefinementsPassage.transferStateRefinements indexing method.getParameters() with the index of the state refinement (toggle() has no parameters). The PR for #456 fixes it, and then the same example fails on the next line:

Caused by: java.lang.IndexOutOfBoundsException: Index 1 out of bounds for length 1
    at ...AuxHierarchyRefinementsPassage.transferStateRefinements (AuxHierarchyRefinementsPassage.java:139)

The loop goes over the superclass's state refinements and reads subStates.get(i) for each one, assuming that the override has the same number of refinements, in the same order.

Expected: no crash. A subclass's refinements should be checked against the superclass's as a whole, not pairwise by position: every state the superclass accepts should be accepted by the override, and the override's result should be one the superclass promises. If they are incompatible, the verifier should report the usual FROM/TO subtyping error instead of throwing.

Found while working on #456.