candor-java v0.41.3

[0.41.3] — 2026-11-06

• ⚠ A dispatch over a JDK collection type no longer charges a project implementor whose type argument cannot match
  the receiver's; it discloses Unknown[dispatch:<owner>.<member>] on that site instead (SOUNDNESS R1461).
  for (Integer x : Collection<Integer>) used to be charged the Fs of the program's only Iterator<Span>, because
  class-hierarchy analysis over Iterator.next() reaches every project implementor whatever its element type. The edge
  cannot simply be dropped: generics are not enforced by the JVM, and a raw iterator() override or an unchecked
  (Collection) upcast really does run that implementor (executed). The bare charge is ALSO lost where the wrong-type
  edge was the only thing covering a real one: a for (String s : list) over a project AbstractList<String> whose
  get writes, where the list arrives as a List<String> parameter or field. That write runs through
  AbstractList$Itr.next, which the engine does not edge at a JDK-typed receiver (R1462's residual). The argument
  contract still charges a caller that passes the project list, and the iterating function now reads Unknown. So the
  edge is replaced by the disclosure where the
  class files PROVE both of these: the receiver's declared type argument (from the LocalVariableTypeTable, the method
  or field Signature, or a call's generic return type such as c.iterator() over a Collection<Integer>), and the
  implementor's. Both must be resolved classes, and neither may be a subtype of the other. Anything not resolved that
  way keeps today's edge: raw types, missing signatures, wildcards, type variables, Object, casts and dependency
  classes. The disclosure is decided after the fixpoint, and only where the demoted body carries something the site
  lacks (an effect, any Unknown, or an invisible package). Where the body carried Unknown, the site also carries
  one reason per reason class the body reached (reflect, callback, native, …), so a reason-scoped
  deny Unknown[reflect] that failed before still fails. "Raw types keep the edge" means raw DECLARATIONS: a raw value
  stored into a generic local is judged by the local's declared type.

  Scope. The owners covered are java.lang.Iterable and the java.util types that reach Iterable, Map,
  Iterator or Map.Entry. Other generic JDK owners keep their edges: java.util.function, java.util.concurrent,
  Enumeration, Spliterator.

  Pinned JDK facts. The JDK's generic signatures come from a new pinned index, candor/jdk-generics.idx.gz, built
  by soundness/jdk_index/derive.sh. The jar and the native image therefore give the same answer.

  What moves. A bare deny <E> (without Unknown) on such a site, and on its callers, goes from failing to
  passing. This is the price of the hedge. deny <E> Unknown keeps failing on every one of them.

  Measured against published 0.41.1 over 452 corpus jars:

  • 5,374 rows lose a concrete effect (8,740 row/effect pairs). Every one carries the new Unknown and reaches a site
    whose demoted body carried that effect.
  • 0 deny <E> Unknown gates move.
  • 794 rows newly carry Unknown; 499 of them were pure.
  • The two false bare-deny Log failures that the R1462 entry below measured (kafka KerberosShortNamer.shortName,
    AddPartitionsToTxnTopic.toString) return to their 0.41.1 verdict.

  -Dcandor.r1461=off or CANDOR_R1461=off restores the previous edges.