Skip to content

candor-java v0.35.0

Latest

Choose a tag to compare

@tombaldwin tombaldwin released this 03 Sep 19:21
· 4 commits to main since this release

⚠️ ADVISORY CORRECTION — 2026-09-03, supersedes the advisory on the v0.34.0 release

The v0.34.0 advisory said blanket deny <Effect> gates were not affected. Retract that. It was
true of the four defects then in hand, it was never a property of the engines, and it is falsified in
all four. In those first cases the caller vanished while the callee stayed independently reported,
so an unscoped deny caught the effect incidentally. That rescue is not a guarantee. In the findings
below, isolated reproductions have nothing anywhere in the report carrying the effect, and the blanket
gate exits 0.

None of this was introduced by 0.34.0. Everything named predates that tag, so downgrading does not
help. All of it is fixed in 0.35.0 unless stated otherwise.

In candor-java, fixed in 0.35.0. A read through an InputStream held in a field lost the Net that
the socket it came from had charged — the classifier had no rule for the abstract java.io types, and
an earlier fabrication had been masking the gap, so removing that over-charge exposed it. A method
reference passed to a functional interface's own abstract method (ifPresent(Runnable::run),
forEach(Runnable::run), new Thread(task::run)) was silent while the lambda spelling disclosed
correctly.

Note the direction of the first one. On 0.34.0 a scoped deny Net over such a read was red for the
wrong reason and would have gone green on upgrade; it is charged again in 0.35.0, at the acquisition.
Still open: a method reference to a primitive-specialised java.util.function interface
(IntSupplier::getAsInt and its siblings) is silent in 0.34.0 and 0.35.0 alike.

What to do

  1. Upgrade to 0.35.0. None of these fixes are available any other way.
  2. Re-baseline. Do not diff future scans against a 0.34.0 report; re-scan on 0.35.0 and start there.
  3. Diff in both directions. An upgrade can also remove a charge that was never real, and the
    baseline diff in AS-EFF-005 flags gains only, by design. A disappearing row is not automatically
    good news or bad; check losses separately if one matters to you.
  4. Re-run your scoped gates specifically. This note exists because policies naming a function, a
    path, callers, path, gains or tour were blind in cases an unscoped deny still caught.
    Passing on 0.34.0 did not mean the rule was checking what you thought.

This is a snapshot, not the register. SOUNDNESS.md in candor-spec is the register; read it for
anything not summarised here and for whatever closes after this note. The fix list is not a
completeness claim — the finding rate has not saturated.


[0.35.0] — 2026-09-03

  • ⚠ SOUNDNESS R179 — a method reference to a functional interface's own SAM, handed to a higher-order
    function, read SILENT-PURE.
    Optional.ofNullable(task).ifPresent(Runnable::run),
    Stream.of(task).forEach(Runnable::run), queue.forEach(Runnable::run), es.submit(task::run) and
    new Thread(task::run) were ABSENT from the report — while the LAMBDA spelling of the same call,
    ifPresent(r -> r.run()), discloses Unknown with callback:java.lang.Runnable.run. One variable: the
    spelling. PUBLISHED — identical on 0.34.0 and on the 0.35.0 candidate. Ground truth EXECUTED: every
    spelling really writes the file. deny Unknown app.Widget.viaOptional / viaStream / viaList all go
    exit 0 → 1; the lambda control was already 1 on all three arms, and blanket deny Unknown was 1 on
    all three (it passes only INCIDENTALLY, via another method).

    The mechanism is a comment asserting its own correctness. ProvValue.fromIndy suppresses
    Candor.opaqueTaskHandoff's Unknown on the stated ground that a lambda's "body is edged at
    creation"
    . For a reference to a functional interface's own SAM that ground does not exist: the
    LambdaMetafactory handle names an ABSTRACT method (REF_invokeInterface java/lang/Runnable.run:()V),
    so handleInvokeDynamic's project branch never runs — the owner is java/lang/Runnable, not a project
    class — and its external branch finds nothing to classify or inherit. The body that really runs belongs
    to whatever receiver the HOF supplies. The site got neither an edge nor an Unknown. Not R84: that is
    the same false premise one site over (indyLambdaTarget accepting an abstract PROJECT method-ref for a
    FIELD-BOUND dispatch); it fixed the project branch and left this suppression untouched — §F1 q3 crossed
    with q2.

    Keyed on the SAM table, not on "is the target abstract", and that choice is a control rather than a
    preference.
    handleTargetConcrete fails CLOSED for every non-project owner (it can only read
    ACC_ABSTRACT off a loaded project class), so reusing it here would call System.out::println bodiless
    too and disclose Unknown over provably pure code. Candor.SAM_OF — the engine's existing authority for
    "this interface method is the abstract SAM a hand-off invokes" — is asked instead, and
    aConcreteJdkMethodReferenceIsStillPure is the row that would have caught the wrong fix.

    Found in real code by the corpus A/B, not by enumeration. spring-web 5.3.39's
    StandardServletAsyncWebRequest.onTimeout and .onComplete are literally
    this.timeoutHandlers.forEach(Runnable::run) — confirmed from the class file's own BootstrapMethods
    table, not from candor's report — and both are ENTRY POINTS (servlet AsyncListener callbacks), so
    a user's registered timeout handler ran through a method certified pure.

    A/B over the same 395 gradle-cache jars, isolated from R147 by A/B-ing against a jar built with R147
    and nothing else, 577,790 common rows: ADDED 46, REMOVED 0, CHANGED(wide) 9, CHANGED(inferred) 6 — all
    six are Unknown GAINS, zero effects lost on any field.
    Two rows changed DIRECTLY (the two spring
    entry points above); four more inherit transitively through the AsyncListener.onComplete/onTimeout
    CHA fan-out. The 46 ADDED rows are all in that one spring class's nested LifecyclePrintWriter /
    LifecycleHttpServletResponse, all with inferred: [] and overdeclared: ['Unknown'] — the
    pre-existing AS-EFF-002 report rule ("a class that declares a capability stays visible") admitting a
    unit that now carries a class-level effect. They claim nothing new about any method and no deny reads
    them.

    THE BOUNDARY, MEASURED — AND IT LEAVES A DIFFERENT SILENT UNDER-REPORT OPEN, WHICH IS SAID HERE
    RATHER THAN IMPLIED.
    This fix corrects fromIndy's false premise. It does NOT widen
    Rules.SYNC_CALLBACK_INVOKERS / FOR_EACH_FAMILY, the allowlist of higher-order functions known to
    INVOKE their callback. So a HOF outside those tables is still silent in the method-reference spelling:
    Optional.ofNullable(sup).map(Supplier::get) reports nothing, while map(s -> s.get()) discloses.
    Both arms measured; the asymmetry is real, published, and one HOF over from the trigger. It belongs
    to a different question — which HOFs invoke, where the allowlist deliberately excludes STORE and LAZY
    sinks — and widening it has its own fabrication risk, so it is filed rather than folded in here.
    theHofTableBoundaryThisRowDoesNotWiden pins it, so closing it turns that test red.

    Teeth, revert-tested BY REVERTING: 2 of the 6 rows in SamForwarderHandoffTest go RED — the
    sync-callback arm and the executor/Thread arm. The other four pass in BOTH arms by construction and
    are NOT claimed to discriminate the fix: the lambda-spelling and plain-loop control, the concrete-JDK
    method-ref over-charge control, the bound-project-method-ref resolution control (PART 87's field-stored
    toggle must stay Fs, not regress to a disclosure), and the residual above. Fixture names are chosen so
    that no name is a prefix of another — the 0.35.0 panel recorded a cell contaminated by scope
    prefix-matching, and a scoped policy here would inherit exactly that.

    The in-code comment beside the fix names the test that proves it (5dae0ca, comment only).

  • ⚠ SOUNDNESS R147 — a read through a stream handle STORED IN A FIELD was silent; deny Net over a
    socket read went exit 1 → 0 on this upgrade until now.
    this.in = sock.getInputStream() charges
    Net in the constructor; in.read() in another method charged NOTHING, because the receiver's static
    type is the abstract java.io.InputStream and the classifier has no rule for it — so the method that
    actually moves the bytes was reported pure. PRE-EXISTING AND PUBLISHED: absent at 2dd1600, at
    d8e953c and at 81f4ceb. Until 81f4ceb the surrounding method kept a Net that came ENTIRELY from
    the fabricated get/setSoTimeout pair — a correct verdict produced by an incorrect mechanism — so
    removing that over-charge UNMASKED this, and the 0.35.0 release panel measured the consequence as a
    RED→GREEN FLIP on upgrade. Three arms, one variable, published jar vs release candidate vs this fix,
    on s.setSoTimeout(100); return in.read(); over a stored socket stream:

    policy published 0.34.0 0.35.0 candidate this fix
    deny Net SockRead.poll 1 0 1
    pure SockRead.poll 1 0 1
    deny Net Unknown SockRead.poll 1 0 1
    deny Net SockRead.tune (options only — the correct removal) 1 0 0
    deny Net (blanket) 1 1 1 — passes INCIDENTALLY, via the acquisition in <init>

    Ground truth EXECUTED over real loopback TCP: poll() returns byte 65 written by the peer, tune()
    moves none.

    The fix is keyed on the ACQUISITION, not on the socket (§G). A whole-program pre-pass records, per
    stream field, the effect of what was written into it — asking Classifier.classify what the producing
    call already charges — so Socket/SSLSocket/URLConnection (Net), Process (Exec),
    Files.newOutputStream/new FileInputStream (Fs) all fall out of ONE rule and none can drift from the
    classifier's own answer at the acquisition site. A field declared with a CONCRETE stream type needed no
    pass at all (FileInputStream in; in.read() already emits owner java/io/FileInputStream); the blind
    spot was exactly the four abstract java.io bases. Static fields and cross-class writes are covered —
    the real-world instance below binds the field from a SUBCLASS. The consuming verbs are
    Candor.isAbstractStreamIo's, reused rather than re-listed, so this and R17 cannot answer "is this a
    stream read" two ways (§F1 q3).

    A/B over 395 gradle-cache jars, keyed on EVERY field (18 of them), 577,790 common rows:
    ADDED 0, REMOVED 0, CHANGED(wide) 271, CHANGED(inferred) 255 — every one a GAIN (Fs 250, Net 5),
    ZERO effects lost on any field.
    The 25 rows that changed DIRECTLY were audited in FULL from javap,
    never from candor's own report — four mechanisms, all confirmed real I/O:
    commons-io LockableFileWriter.write(×5, three jar versions) (out = initWriter(File,…), which really
    returns an OutputStreamWriter over a FileOutputStream on that file); commons-compress
    FileBasedScatterGatherBackingStore.writeOut (Files.newOutputStream(target)); guava and its
    checkerframework shade, FileBackedOutputStream.write(int) / write(byte[],int,int)
    (out = new FileOutputStream(temp) inside update(), i.e. a capability that only appears past the
    threshold); and bsf 2.3.0 SocketConnection.listen / sendPacket, which is the R147 shape verbatim
    in real third-party code
    fInputStream = fSocket.getInputStream() written by the SUBCLASS
    ClientConnection, read by the superclass, deny Net exit 0 before. The remaining 230 rows are the
    engine's existing CHA propagation of those 25 (direct moved on 25, inferred on 255); two were
    traced end-to-end and both land on LockableFileWriter.write. The corpus therefore REACHES both new
    branches on real code, so this is a RECALL measurement, not a safety-only one.

    THE BOUNDARY, PINNED RATHER THAN ASSERTED. Two shapes are deliberately NOT closed and are measured
    as residuals in StoredStreamProvenanceTest.theTwoResidualsThisRowDoesNotClose, so closing either turns
    that test red instead of quietly widening the claim: a field bound from a PARAM (the caller's concrete
    stream — the pre-existing external-stream question, answered with Unknown today only where the stream
    is an ARGUMENT to a stream-consuming utility, or is an entry point's own param), and a field holding a
    FILTER constructed over an acquisition (new InputStreamReader(sock.getInputStream())). close() is
    outside isAbstractStreamIo and so outside this fix.

    Teeth, revert-tested BY REVERTING (git stash of src/main, suite re-run): 4 of the 7 rows in
    StoredStreamProvenanceTest go RED — the socket read/write, the static field, the four-effect
    acquisition sweep, and the branch-merged join. The other three pass in BOTH arms by construction and are
    NOT claimed to discriminate the fix: the socket-option over-charge control, the two residuals, and the
    §E2 row that MEASURES (rather than asserts) the one assumption in the new code — that every
    SELF_SOURCING_STREAMS rule is whole-owner, so a synthetic ()V probe can stand in for the real
    constructor descriptor. The branch-merged row was RED against the first cut of this fix and is why the
    origin rides on the VALUE at the NEW rather than being re-derived from newType at the store:
    newType correctly collapses at a control-flow join, and a store-side re-derivation lost the Fs half
    of net ? sock.getInputStream() : new FileInputStream(f) in silence.

    The new index is a body-derived whole-program pre-pass output, so it is folded into
    Refresh.wholeProgramDigest — R163's reflective guard over AnalysisContext.inputNames() requires
    exactly that, and it is the reason this could not be forgotten.

  • SOUNDNESS R155 — AGENTS.md never named the effect VOCABULARY. Nine of the eleven SPEC §1
    effects had zero mentions in candor-java's agent contract, and the embedded --agents copy an agent
    actually reads had none either — including Llm, which the classifier has policed since ⟨0.13⟩. The
    drift gate could not see it: test/smoke.sh pins the repo doc to the embedded copy, so the two drift
    TOGETHER and stay green; nothing pinned either to SPEC §1. candor-spec's new
    scripts/check_agents_vocabulary.py derives the vocabulary from SPEC.md's own table and now passes
    for candor-java in both copies (it named candor-java as the only failing engine before this change).

  • ⚠ SOUNDNESS R163 — a whole-program pre-pass index built from other classes' BODIES was not in the
    refresh digest.
    R151's class, one field over. ⟨0.35⟩ added fieldLambdaBindings to
    AnalysisContext: Cha.collectFieldLambdaBindings walks every method's INSTRUCTIONS to bind each
    functional-interface field to the lambdas/method-refs written into it, and Cha.fieldBoundImplementors
    reads it during per-class analyze. So class A's cached delta depends on class B's BODY — exactly what
    Refresh.wholeProgramDigest deliberately does not cover structurally — and the field reached that
    digest by no route at all. Unpublished: the defect is post-v0.34.0, so no released binary carries it.

    Reproduced first, executed, one variable. Widget.bindSecondary() goes from a no-op to
    this.task = Effector::act — a bound METHOD REFERENCE, chosen so javac emits no new synthetic member
    and javap -p Widget is byte-identical either way; Caller.class, Effector.class and Main.class
    are sha256-identical across the two arms, and the programs were RUN (v1 writes nothing, v2 writes the
    witness file through Caller.go's field dispatch). Matrix on the pre-fix HEAD, pure Caller.go:

    arm exit reuse Caller.go
    cold v1 0 0 of 4 absent (pure — correct)
    cold v2 1 0 of 4 Fs, calls:[Effector.act]
    warm: primed v1, rerun v2 0 3 of 4 absent — report byte-identical to cold v1
    control: primed v2, rerun v2 1 4 of 4 Fs (ordinary reuse intact)

    After the fix the warm arm is exit 1, reused 0 of 4, byte-identical to cold v2, and the control
    still reuses 4 of 4. analyzed.digest is d7608ec5a5adc4c4 in all four arms, and
    CANDOR_REFRESH_DEBUG's digest-input dump was byte-identical between v1 and v2 with no occurrence of
    task, Effector or lambda.

    The sweep, not just the instance (§9). AnalysisContext.inputNames() — the engine's own authority
    for the shared-input set — lists 47 fields. Perturbed one at a time against wholeProgramDigest on the
    pre-fix build, exactly one failed to move it: fieldLambdaBindings. The other 26 perturbable
    inputs move the digest; the remaining 20 are excused in writing, in three categories: structure-derived
    (ALL, byName, projectClasses, subtypeIndex, overloadDescs, classHash — the per-class loop
    already hashes the bytes they are functions of), dep-derived memos (depFnsByOwner,
    depFnsByOwnerName, depOwnersBySigBuilt — pure functions of crossDeps, folded value-by-value by
    R151), and after-analyze-only (vocabularySource, netPartnersSource, unanalyzed, excluded,
    archives, sourceFiles, classpathRoots, scanRoot, outOfScope, scannedUnder, peekedClasses
    — written and read by the peek/scope/report-write phases, which run after the analyze loop). R151's
    audit reached the same verdict on the remainder and still missed this one, because it was added in the
    release that audit was run against; a prose audit cannot see a field that appears after it.

    Teeth, all revert-tested BY REVERTING. RefreshFieldLambdaDigestTest — an end-to-end arm on the
    fixture above (compiled AND executed, with the one-variable and cache-engaged controls), plus a
    reflective arm requiring every name in AnalysisContext.inputNames() to be either perturbable-into-the
    -digest or carry a written excuse, so a field added tomorrow is in neither list and fails BY NAME.
    Reverting only the digest fold turns both red, naming fieldLambdaBindings.
    bin/refresh-equiv.sh gains a field-binding axis in the style of R151's CANDOR_DEPS one: it
    compiles its own fixture, refuses to pass unless the body change moved a COLD report, the two arms
    differ in exactly one class, and the cache engaged — and it FAILS against the pre-fix jar and
    passes against the fixed one. RefreshBodyIndependenceTest is structurally blind to this class (it
    runs prepareScan over the real bodies in BOTH arms, so every pre-pass output is identical by
    construction); its doc justified that with "those are already in the digest", which was true when
    written and false the moment ⟨0.35⟩ landed. That sentence and Refresh's matching class-doc clause are
    now corrected rather than left standing.

    COST: none measurable. guava-33.6.0-jre (1,969 classes), three warm runs each: cache-digest
    14.8/16.8/15.4 ms before vs 12.1/14.4/15.3 ms after, whole warm scan ~1.0 s both, reuse 1,969 of 1,969
    both, reports byte-identical. candor's own build/classes/java/main (87 classes): digest 2.3 ms both,
    warm scan 0.26–0.28 s both, reuse 87 of 87 both. The fold is small because the index is: 3 bound
    fields on guava, 1 on candor's own classes
    — counted from the digest-input dump, so the cost figure
    is not a zero over a branch that never ran.

  • ⚠ SOUNDNESS R151 — a CHAINED DEPENDENCY that kept its key and changed its VALUE was replayed from
    the refresh cache.
    Refresh.wholeProgramDigest folded in crossDeps.keySet() and none of the
    DepFn VALUES, while Candor.inheritDepFn writes those values — effects, hosts/cmds/paths/
    tables, netClass, incomplete, unknownWhy — straight into the per-class accumulators the cache
    stores. The class comment claiming that "a change to … chained dependencies discards the whole cache"
    was false, and bin/refresh-equiv.sh, which calls itself "the refresh's entire safety case", never
    perturbed CANDOR_DEPS at all. It needs only a warm cache, which is the normal CI configuration.

    Reproduced on the published 0.34.0 jar, one variable, app bytecode byte-identical across the two
    arms (shasum equal), dep v1 and v2 both compiled and EXECUTED first so the effect was observed
    present and absent (a listener on 127.0.0.1:19151 saw NO CONNECTION under v1 and
    CONNECTION RECEIVED under v2). Warm cache primed under a dep reporting ['Db'], rerun under the
    same dep reporting ['Db','Net']: exit 0, no violations, "reused 1 of 1", where the fresh-cache
    and no-cache controls both exit 1 with ['Db','Net'].

    Ten axes measured, each on its own fixture, each with its cold and fresh-cache controls; the six
    marked ⚑ flip a configured gate from exit 1 to exit 0:

    axis policy stale cold
    effects deny Net 0 1
    hosts allow Net a.example.com 0 1
    paths allow Fs /tmp/alpha 0 1
    cmds allow Exec ls 0 1
    tables allow Db users 0 1
    netClass / incomplete allow Net a.example.com 0 1
    unknownWhy deny Net Unknown[reflect] stale reason class, both directions
    fn + calls (depCallsByFn/depWhyByFn) deny Net Unknown[reflect] same, one hop further
    stale (§2.1 distrust) already caught, via depCoveredPkgs

    The boundary: the pre-fix digest DID cover a dep entry appearing or disappearing (the key set); what
    it missed was a value change on an existing key. Every non-final, non-memo AnalysisContext field was
    audited against the digest — the remaining uncovered ones are all derived from the scanned class bytes
    (projectClasses, subtypeIndex, overloadDescs, byName, classHash, classpathRoots) or are
    recomputed per run at report-write time (vocabularySource, netPartnersSource, outOfScope), and
    only a shared input read during per-class analyze can go stale in a per-class cache.

    Fixed by folding every DepFn field, plus the dep call graph, into the digest. The DepFn
    rendering is REFLECTIVE over that record's own fields and raises on a type it does not recognise,
    because the hole opened by hand-written omission: four fields were added after the digest was written
    (unknownWhy ⟨0.19⟩, netClass ⟨0.20⟩, fn ⟨0.24⟩, incomplete ⟨0.29⟩) and every one escaped it.

    Corpus A/B, guava-33.5.0-jre chained into six real third-party jars, refresh on, keyed on fifteen
    fields (not just inferred), with hit counters: 45,150 executions of the changed branch (7,525 per
    consumer, counted from the digest's own CANDOR_REFRESH_DEBUG dump). Under an UNCHANGED dep report
    pre-fix and post-fix agree +0/-0/~0 on all six with identical reuse counts (1666/878/1912/131/704/413)
    — no over-invalidation. Under a dep report perturbed in one field, the post-fix warm scan equals the
    cold scan on all six, while the PRE-FIX warm scan diverges on 3,809 / 2,799 / 1,379 / 523 rows in
    error_prone_core, dagger-compiler, dagger-spi and google-java-format — 5,825 rows LOST an effect and
    0 gained one
    , which is the cardinal sin at corpus scale. caffeine and commons-lang3 join nothing from
    guava, so their rows are a SAFETY measurement only, and are recorded as such.

    Cost, measured rather than assumed (guava + hibernate-core chained, 23,624 joined entries, candor's
    own classes as the consumer, three warm runs each): cache-digest 218 ms → 269 ms, whole warm scan
    6.79s → 6.88s — against 6.7s that both arms spend just PARSING those dep reports. Reuse stays 87 of 87
    and the reports are byte-identical. With no deps chained, the ordinary agent-loop case, the digest goes
    4.8 ms → 2.5 ms. The refresh is not made worthless; it is not measurably slower.

  • The refresh digest's identity-hash guard was quadratic, and had no test at all. Sizing R151 showed
    the guard, not the rendering, was the cost: [\w.$\[;]+@[0-9a-f]{6,8}\b retries the run from every
    position inside it, so the 15.4 MB the chained entries render to cost 1.19s of a 1.46s digest.
    Anchored to the start of a run and made possessive it is 0.05s and finds exactly the same thing (a
    leftmost match always began at a run start). RefreshIdentityHashGuardTest pins the equivalence on
    seven positives and seven near-misses, and pins the linearity — that last one fails at 1,262 ms against
    the old pattern.

  • bin/refresh-equiv.sh gained a CANDOR_DEPS axis, and CI gained bin/refresh-equiv.sh. The
    script had no caller anywhere: not ci.yml, not test/smoke.sh, not any gate. The new arm compiles
    its own two-package fixture and generates both dep reports with the jar under test, then requires the
    perturbation to move a cold report and the cache to have engaged before it will call anything a pass.
    It FAILS against the pre-fix jar (a CHANGED dependency report was replayed from cache) and passes
    against this one; the whole script is 4s on this repo's own classes.

  • ⚠ SOUNDNESS R130 — one rule, one spelling: THIRTEEN JDK routes to an already-modelled effect were
    silent.
    The question came from candor-rust, where std::fs:: turned out to be the entire filesystem
    rule and every platform module under it read PURE. Re-asked of this engine and answered by
    measurement, not by reading the classifier. Each route below was put in a class of its own with no
    ordinary-spelling call in it, COMPILED AND EXECUTED so the real-world effect was observed, and then
    scanned: every one came back functions: [], excluded: [], and exit 0 under all five policy
    forms
    deny <E>, deny Unknown, deny <E> Unknown, scoped deny <E> <pkg>, and pure <pkg>.
    In every case the control — the ordinary spelling of the same operation, same jar, same compile,
    differing only in the route — charged the effect and exited 1.

    • java.nio.file.spi.FileSystemProvider — the SPI every Files.* method is defined as a call
      to, handed to user code by FileSystems.getDefault().provider(). A real file, a real directory and
      a real symlink created on disk through it, silently. Now whole-owner Fs with a tested denylist
      (getScheme, <init>, and — found by auditing this fix's own corpus diff — getPath(URI) and
      getFileSystem(URI), both specified by the SPI as non-I/O).
    • java.nio.file.FileSystem getFileStores/getRootDirectories/newWatchService/close
      Fs. Verb-gated: the type is mostly path algebra.
    • java.nio.file.attribute.*AttributeViewFs. chmod, chown, utimes, setxattr and the ACL/DOS
      equivalents, through a view received as a PARAMETER — the acquisition (Files.getFileAttributeView)
      was charged, but acquisition and mutation routinely live in different methods. A 0400 chmod and a
      user.candor xattr were both verified on disk while the scan said nothing.
      Plus UserPrincipalLookupService.lookupPrincipalByName.
    • java.awt.Desktop.moveToTrashFs. The Desktop rule enumerated the LAUNCH verbs; this is the
      one member that is not a launch — it deletes the named file. The fixture's file really was removed.
    • java.lang.Process and java.lang.ProcessHandle → whole-owner Exec with a tested denylist,
      replacing two verb ALLOWLISTS that had each forgotten members: onExit() (the async twin of the
      charged waitFor), the Java 17 inputReader()/errorReader()/outputWriter(), and
      allProcesses()/children()/descendants()/parent()/of(pid), every one of which hands back a
      destroy-capable handle. The fixture really enumerated 807 live OS processes. exitValue/isAlive/
      pid/toHandle/info/supportsNormalTermination/current/<init> stay pure, each pinned.
    • java.util.random.RandomGenerator$*GeneratorRand. The rule matched the root interface
      exactly, under a comment asserting that the sub-interfaces "extend it" — true of the type system and
      false of bytecode, since the classifier is keyed on the STATIC RECEIVER TYPE. Real entropy drawn
      through SplittableGenerator/JumpableGenerator/StreamableGenerator, silently. Now
      $-anchored, so the sibling top-level RandomGeneratorFactory stays pure (pinned).
    • new InetSocketAddress(String,int)Net — it performs the identical resolver lookup the
      already-charged InetAddress.getByName exists for. Proven by execution: localhost resolved,
      a .invalid name came back isUnresolved(). Descriptor-gated, so createUnresolved and the
      (InetAddress,int) / (int) forms stay pure. Plus InetAddress.getHostName (the REVERSE lookup,
      omitted because it does not look like one), and Inet4Address/Inet6Address-typed receivers.
    • javax.net.ssl.SSLServerSocketNet (with a full pure-config carve-out), the acceptor twin of
      the SSLSocket carve-in; ServerSocketFactory/SSLServerSocketFactory.createServerSocket
      Net; java.net.JarURLConnectionNet, the fourth URLConnection subclass.
    • GregorianCalendar.getInstance()Clock. javac emits the QUALIFYING type for a static call.

    A/B over 395 third-party jars (gradle cache), PRE built from HEAD 2dd1600 in a clean worktree,
    diffed on every field and not just inferred: 577,547 common rows, ADDED 107, REMOVED 0, and
    zero losses on any field (inferred, incomplete, declared, invisible, unknownWhy,
    unresolved, netClass) — the movement is entirely in the reporting direction. Gains: Net 180,
    Fs 21, Exec 12, Clock 4, each bucketed by mechanism and ground-truthed from javap, never from
    candor's own report. Hit counters in every changed branch (an instrumented twin of the shipped
    jar) prove the corpus REACHED 11 of the 14 new branches — clock.calendar 279, exec.process 111,
    net.sockaddr 90, fs.filesystem 61, fs.provider 57, net.gethostname 34, fs.attrview 33, net.jarurl 14,
    net.ssfactory 11, fs.principal 7, net.inetsub 4 — so this is a RECALL measurement, not a safety-only
    one. Three branches (Desktop.moveToTrash, the RandomGenerator sub-interfaces, SSLServerSocket) got
    zero corpus hits and are safety-only over this corpus; each is backed by an executed fixture
    instead. Real code newly reported includes httpcore5's DefaultAddressResolver.resolve, okhttp's
    Util.peerName, jackson's InetSocketAddressSerializer, and IntelliJ's split-mode process tracker.

    The audit found two fabrications in its own first cut (FileSystemProvider.getPath/
    getFileSystem, over-charging four real rows in jetbrains verifier-cli) and one near-miss:
    ServerSocketFactory.createServerSocket first read as already-covered because the fixture also called
    ServerSocket.close(), which is charged — re-run with the bind ALONE, both arms reported
    functions: []. A mixed fixture cannot answer this question.

  • ⚠ SOUNDNESS R130 follow-up — the over-charge column of that fix: three fabrications it introduced,
    and one silent under-report it sat next to.
    An adversarial review of the entry above found three
    members newly charged for effects they do not perform, each absent at 2dd1600, charged at
    d8e953c, and each flipping a deny <E> gate from exit 0 to exit 1 on code that performs nothing.
    All three were reproduced before being fixed, with the real-world behaviour EXECUTED.

    • FileSystemProvider.getFileAttributeView was charged Fs and performs no I/O. Executed: on a
      path that does not exist it returns a live BasicFileAttributeView and throws nothing, while
      view.readAttributes() on that same view throws NoSuchFileException. The syscall is in the view,
      and the view's whole surface is already charged by the *AttributeView rule, so carving the
      acquisition out loses no capability. The defect was the audit boundary, not the member: the two
      carve-outs d8e953c shipped (getPath, getFileSystem) were derived from what its 395-jar corpus
      happened to contain, so the member the corpus lacked was missed by exactly the reasoning that
      produced them. The replacement boundary is the SPI itself — every I/O member of
      java.nio.file.spi.FileSystemProvider declares throws IOException and exactly five do not
      (<init>, getScheme, getFileSystem, getPath, getFileAttributeView), plus the static
      installedProviders(), which is deliberately still charged because it runs a ServiceLoader over
      META-INF/services. That the discriminator has a counterexample is why the rule stays a denylist:
      JDK 20's exists(Path,…) also declares no IOException and really does call checkAccess, and it
      keeps firing.
    • The socket-option protocol was charged Net and moves no byte, on all six socket owners.
      Executed on an UNBOUND SSLServerSocketFactory.getDefault().createServerSocket(): setSoTimeout,
      setReuseAddress, setReceiveBufferSize, setPerformancePreferences and
      setOption(SO_REUSEADDR) all succeed and leave it isBound()==false, getLocalPort()==-1 — a socket
      with no local address cannot have touched the wire — while the getters round-trip what was set. The
      engine had already ruled that option access is not network I/O by exempting getSoTimeout/
      getReuseAddress for many rounds (getReuseAddress() is a real getsockopt), so charging the
      matching setters answered one syscall class two ways. d8e953c made that visible by giving
      javax.net.ssl.SSLServerSocket a whole-owner Net rule; the asymmetry itself was pre-existing on
      the other five owners.
    • …and the two ACCEPTOR arms had drifted. The SSLServerSocket list d8e953c added carved out
      getReceiveBufferSize where the java.net.ServerSocket list it was copied from does not, so one
      program got two answers for one operation depending only on the receiver's declared type. Fixed by
      replacing five hand-copied method.equals(...) chains with three predicates defined once
      isPureSocketHandleState, isPureSocketOptionAccessor, isPureTlsHandshakeConfig — shared by
      Socket, ServerSocket, DatagramSocket, MulticastSocket, SSLSocket and SSLServerSocket.
      Fixing the TLS acceptor alone would have converged one pair of arms by splitting another. The wire
      boundary (connect/bind/accept/close/getInputStream/getOutputStream/sendUrgentData/
      shutdown*/send/receive/joinGroup/leaveGroup/disconnect/startHandshake/getSession)
      is unchanged and pinned by a 17-member control.
    • new GregorianCalendar(TimeZone) / (Locale) / (TimeZone,Locale) read the wall clock and were
      certified pure
      — the opposite direction, PRE-EXISTING, and one line from the code d8e953c
      edited. Missed because the adjacent comment asserts "ARITY-PRECISE: new Date(long) /
      new GregorianCalendar(y,m,d) take a value and are pure"
      ; three valued constructors take a value
      and read the clock. Arity was never the discriminator — the argument KIND is: every pure
      GregorianCalendar ctor takes only ints, every clock-reading one takes only TimeZone/Locale.
      Executed: two calls 1.1s apart returned millis differing by 1110–1111 through each of the three,
      and by 0 through the (y,m,d) control.

    NOT narrowed, and the measurement is why. A project class extending java.lang.Process is charged
    Exec on the INHERITED CONCRETE members it does not override, because the supertype walk in
    handleMethodInsn re-classifies them against java.lang.Process. On a test double that spawns
    nothing that is a fabrication (onExit/inputReader go absent → ['Exec'] across the two commits,
    deny Exec 0 → 1, on a program whose own output shows zero child processes). Removing the walk would
    be worse: a wrapper over a REAL child reaches its capability through that walk and through nothing
    else
    (calls: None, because the JDK body that would call back into the subclass is never scanned),
    so the narrowing would trade a loud over-charge for a silent under-report. Both directions are now
    pinned by tests instead of argued in a comment, and the comment that claimed a user subclass's
    "own methods are analysed as project code" — false for inherited concrete members — now says what
    it assumes. The general mechanism is R131. The same shape reaches FileSystemProvider (ten concrete
    inheritable members) and RandomGenerator (~30 defaults over one abstract nextLong);
    ProcessHandle is unaffected — its only concrete inheritable member is default compareTo(Object),
    already exempt.

    A/B — the same 395 third-party jars, three arms in one run, keyed on EVERY field. The
    2dd1600 → d8e953c arm reproduces that fix's published numbers exactly (577,547 common rows, ADDED
    107, REMOVED 0), which is what calibrates the instrument. d8e953c → HEAD: 577,536 common, ADDED
    254, REMOVED 118, CHANGED(wide) 1,839
    — declared 806, overdeclared 716, undeclared 506, inferred
    382, calls 208, incomplete 82, direct 63, netClass 57. Two mechanisms, not one: +117 rows gained
    Clock
    (37 of them with the constructor in their own bytecode, all 37 confirmed by javap, zero
    unexplained, across gson, jackson, okhttp, postgresql, joda-time, poi, log4j and 12 more) and +137
    appeared only because their class's field types now declare Clock; −118 rows plus the field-level
    losses
    are the socket narrowing and the two FileSystemProvider rows.

    Every removal was audited in FULL from javap, never from candor's own report — 146 rows losing
    Net or Fs: 102 direct with every changed-owner call in the exempt set, 44 explained transitively,
    0 suspicious, 0 unexplained.
    Hit counters in an instrumented twin (proven byte-identical to the
    shipped jar over all 395 jars: ADDED 0 REMOVED 0 CHANGED 0) show the corpus reaches every changed
    branch — 400 socket-option hits across 6 owners, 41 GregorianCalendar ctor hits, 2
    getFileAttributeView hits — so this is a recall measurement. SSLServerSocket itself still gets
    zero corpus hits and remains safety-only, exactly as d8e953c recorded.

    The near-miss, reported rather than buried. Removing an over-charge un-masks whatever it was
    accidentally covering. Screening all 146 lost rows for a co-located read/write found 8, and exactly
    one leaf loses its row with no disclosure at all: httpcore 4.4.13's
    BHttpConnectionBase.fillInputBuffer, which really does read the socket — through
    SessionInputBufferImpl.fillBuffer on a plain java.io.InputStream stored at bind time. Its Net
    came entirely from the get/setSoTimeout pair; SessionInputBufferImpl.fillBuffer is absent from the
    report at 2dd1600, at d8e953c and at HEAD, so the blind spot is socket-STREAM PROVENANCE and
    is not introduced here — it was masked by the fabrication. ~13 rows in that one jar follow it
    transitively (awaitInput, isStale, isResponseAvailable, BasicConnPool.validate, …). The other
    seven keep a disclosure (invisible: ['okio'] on okhttp's Util.isHealthy) or keep Net from
    another route. The wire boundary in the same jar is untouched: getSocketInputStream,
    getSocketOutputStream, close, shutdown and ensureOpen all still read Net. Filed as its own
    question rather than answered by keeping a known fabrication as accidental coverage.

  • ⚠ SPEC ⟨0.35⟩ §4 / conformance PART 87 — A NON-EMPTY CANDIDATE SET IS NOT A COMPLETE ONE, part 1
    of 3 (a294b86).
    A lambda stored in a field and invoked later was attributed to NOTHING the moment
    the functional interface had any declared implementor. Measured on the PUBLISHED 0.34.0 jar, one
    variable: with zero implementors App.go reads Unknown, unresolved:true, callback:java.lang.Runnable.run; add ONE pure unrelated class Repaint implements Runnable and
    change nothing else, and App.go VANISHES from functions[]deny Unknown exit 1 → 0.
    The engine
    parsed the metafactory (it named the target interface in its own callback: detail) and analysed the
    lambda body as its own unit; it simply never registered that body as an implementor. Fixed by
    COMPLETING the candidate set — SPEC ⟨0.35⟩ was written as a disjunction precisely so that the effects
    may flow rather than be hedged, and binding it to unresolved:true alone would have outlawed this fix.
    Published-jar A/B on the engine's own 1,636-function corpus: ADDED 0, REMOVED 0, CHANGED 0 — zero blast
    radius, because this source does not contain the shape; the over-charge control (a PURE lambda through
    the identical shape) gains no Fs.

  • ⚠ PART 87 was HALF-CLOSED: the STATIC and INHERITED field shapes (5fa3417). Two ordinary Java
    spellings of the identical property were still live, both reproducing on published 0.34.0 (they predate
    a294b86, so this is not a regression). Static fields: private static Runnable taskGETSTATIC
    was never tagged with fieldOrigin, only GETFIELD was, and the pass's own doc called that "inert,
    not wrong"
    ; measurement said otherwise (Widget.fire ABSENT, deny Unknown 1 → 0). Inherited
    fields
    : Base.install's PUTFIELD names owner=Base while Sub.fire's GETFIELD of the same
    storage names owner=Sub (confirmed with javap -v), so the write key and the read's fieldOrigin
    never matched and the lookup fell through to the unfixed CHA path (deny Fs Sub.fire 1 → 0). Fixed
    with Cha.fieldKey, which normalises a field access to its DECLARING class through the same
    resolution-order walk CHA already trusts for methods — one mechanism, not a second hand-rolled walk —
    after an enumeration of nine field-access spellings, each with its own revert-tested fixture. A/B over
    325 real third-party jars vs the published jar: ADDED 2, REMOVED 66, CHANGED 318. Also closed, and
    also measured rather than assumed:
    the pre-existing OVER-CHARGE this vein produces when a field falls
    through to CHA beside exactly one unrelated effectful implementor (a false deny Fs on a provably-pure
    lambda, on the published jar too) — closed for a CLEAN write-set, and explicitly NOT closed for a
    tainted one, which is recorded in BACKLOG.md rather than left standing as a fixed claim. So is the
    larger gap that field provenance does not survive a call through a GETTER at all.

  • ⚠ PART 87, part 3: the binding pass read CONTROL FLOW as LINEAR ADJACENCY (8599ec0). The
    field-lambda pass decided whether a PUTFIELD/PUTSTATIC's write-set was a clean project lambda by
    inspecting only the single bytecode instruction physically preceding the store. That is a linear check
    answering a dataflow question. this.x = supplied != null ? supplied : defaultLambda; — the
    default-or-caller-supplied-callback idiom, shipped by the AWS S3 SDK, HttpCore5, Spring Data Redis and
    Netflix Eureka — compiles to ONE putfield fed by TWO merging predecessors, and javac places the
    default arm adjacent, so an arbitrary caller-supplied callback was recorded as if it could only ever
    be the safe default
    : the exact inverse of that method's own documented taint contract. Fixed by
    reusing the engine's existing whole-method dataflow (Interp.ProvInterpreter via
    Candor.cachedProvFrames), whose merge already collapses lambdaTarget to null the moment two
    incoming paths disagree — correct and free, since the stream-origin pre-pass shares the same per-method
    memo. 325-jar A/B: of the 386 rows a294b86+5fa3417 had moved off the published value, 42 revert
    exactly to it and 344 stay exactly where they were; zero landed on a third value.

  • ⚠ SOUNDNESS R84 — an ABSTRACT method reference was accepted as a clean lambda body (a1bbd92).
    A CARDINAL SIN introduced by a294b86 and untouched by both 5fa3417 and 8599ec0, caught and
    fixed inside this release, so no published artifact carries it.
    indyLambdaTarget called a
    LambdaMetafactory handle a recognisable project lambda whenever its owner was a project class and its
    tag was >= H_INVOKEVIRTUAL, without checking the target was CONCRETE — so this.op = Shape::render
    where Shape.render has no body bound the field to a phantom method id with zero instructions, and the
    real implementor's effect never reached the caller. Where published 0.34.0 disclosed Unknown, the
    intermediate build read certified pure. Fixed by handleTargetConcrete(Handle), which enumerates all
    six MethodHandle kinds — the three that can never be abstract are accepted unconditionally, the two
    that can are walked through Cha.resolutionOrder and their ACC_ABSTRACT bit read, and an
    unresolvable declaration FAILS CLOSED. "interface" is deliberately not used as a proxy for "abstract":
    a default method is concrete and must still bind, and it has its own control. deny Unknown and
    deny Fs Unknown Main.main both restored 0 → 1; deny Fs 1 → 1 and the pre-existing scoped gap
    deny Fs Main.main 0 → 0 untouched. 325-jar A/B isolated by rebuilding a pre-R84 jar: ADDED 3,
    REMOVED 0, CHANGED 93, all in the disclosure direction; the two rows that lost a label were
    ground-truthed from javap.

  • ⚠ SOUNDNESS R86 — every backward literal walker captured the WRONG ternary branch (1abc71d,
    regression teeth in 2dd1600).
    Each instruction-window walker in Literals.java bounded its walk at
    a call/jump/NEW/store but never at a control-flow JOIN, so a ternary or switch-expression feeding a
    literal into a call argument had whichever branch sat physically adjacent captured. That is a
    POSITIVE claim about the wrong destination, not an omission
    :
    new Socket(cond ? "danger.example.net" : "safe-partner.example.com", 443) with
    net-partner safe-partner.example.com configured reported ONLY the safe partner, and
    deny Net[unknown-host] exited 0. Fixed with Literals.joinLabels(mn) — computed once per method —
    so a merged literal becomes "no literal captured" and takes the existing fail-closed/incomplete path
    rather than one chosen by bytecode order. Measured: the repro now reports no hosts and
    incomplete:["Net"], and both deny Net[unknown-host] and deny Net exit 1; switch-expression was
    confirmed vulnerable pre-fix in BOTH branch orders and fixed in both. Try/catch-via-local and
    loop-carried reassignment were BUILT and measured already safe through an unrelated pre-existing
    ambiguity check — the brief's inference that they shared the vulnerable path was wrong, and saying so
    is the point. Every consumer inherits the fix: Net host, Fs path, Exec program head, Db tables,
    and the reflection method-name and receiver class.

  • ⚠ SOUNDNESS R87 — an entry-point marker without an explicit @Retention(RUNTIME) was never seen
    (1abc71d).
    Candor.markEntryPoints matched Rules.ROOT_ANNOTATIONS against
    mn.visibleAnnotations ONLY. Java's DEFAULT retention is CLASS, so a custom lifecycle / scheduler /
    container marker declared without an explicit @Retention(RUNTIME) lands in invisibleAnnotations and
    was never read. Measured with retention as the only variable: CLASSentryPoint:false and
    candor reachable answers 0 entry points over a method that genuinely writes a file; RUNTIME
    correct. impact shares the same filter and moved identically (0 downstream entry points pre-fix, 1
    post-fix). --policy scan gates were confirmed UNAFFECTED — a direct-effect deny fires regardless
    of entry-point status — so the ⚠ here is about the entryPoint REPORT field and the query verbs that
    read it, not about a gate flip. Fixed with anyDeclAnnoMatches(visible, invisible, markers), which is
    the pattern anyParamAnnoMatches was already using one level down (the CDI @Observes path always
    checked both lists): two independent implementations of one question that had already drifted, now one
    authority (§F1 q3). Controls measured in all three directions: CLASS → now true; RUNTIME → still
    true; no marker at all → still false, 0 entry points, no fabrication.