hard-to-express postcondition for equals helper

5be5d3b0d71b4a9049c64e1678ae2cf6d0f836e6 recently improved the annotations for equals, to include the post-condition that if equals returns true its argument must have been non-null:

@EnsuresNonNullIf(expression="#1", result=true)

I ran into a problem with some equals methods that delegate to a helper method, e.g.:

  @Override
  public boolean equals(Object other) {
    return helper(this, other);
  }

 static boolean helper(@Nullable Object left, @Nullable Object right) {
    if (left == right) {
      return true;
    }
    if (left == null || right == null) {
      return false;
    }
    // TODO: eventually return true if the arguments are equal
  }

Is there a way to express the contract for the helper method? It seems tricky because the method can return true when right is null (as long as left is also null), so I don't see a way to use @EnsuresNonNullIf of @EnsuresNonNull.

Start with the equals helper example and the @EnsuresNonNullIf and @EnsuresNonNull annotations described in the issue. Investigate how the checker represents postconditions for delegated equals methods and whether the null-equality case can be expressed. Done means documenting or implementing a contract that handles both arguments and the true result correctly.