bernardladenthin · Oct 21, 2026 · Oct 20, 2026
@@ -7,9 +7,9 @@ description: >
   Installs a pinned, checksum-verified OpenJML release (Ubuntu x64 build) into
   $RUNNER_TEMP/openjml and exposes the location as the OPENJML_HOME environment
   variable. The unzipped distribution (~1 GB, zip ~490 MB) is cached keyed on
-  version + checksum + fixup revision. Known-broken bundled JDK specification
-  files are deleted on install (see the fixup step below); because the deletion
-  happens before the cache is saved, cache hits already contain the fixed tree.
+  version + checksum + fixup revision. The bundled jdk/release is repaired on
+  install if needed (see the fixup step below); because the repair happens before
+  the cache is saved, cache hits already contain the fixed tree.
 
 inputs:
   version:
@@ -27,9 +27,12 @@ runs:
       uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6
       with:
         path: ${{ runner.temp }}/openjml
-        # spec-fixups-v2: bump this suffix whenever the fixup step below changes,
+        # spec-fixups-v3: bump this suffix whenever the fixup step below changes,
         # otherwise cached installs keep the previous fixup state.
-        key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v2
+        # v3 deletes no bundled spec any more: OpenJML 21.0.29 ships the RAC fixes for
+        # ArrayDeque.jml (dropped in v3, OpenJML/OpenJML#1012) and AtomicLong.jml (dropped in v2,
+        # OpenJML/Specs#29); the RAC suite passes against both bundled files (285/285).
+        key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v3
 
     - name: Download pinned OpenJML (checksum-verified)
       if: steps.cache.outputs.cache-hit != 'true'
@@ -44,27 +47,7 @@ runs:
         rm "$RUNNER_TEMP/openjml.zip"
         chmod +x "$RUNNER_TEMP/openjml/openjml" "$RUNNER_TEMP/openjml/openjml-java"
 
-    - name: Delete known-broken bundled JDK specs (fixups v2)
-      if: steps.cache.outputs.cache-hit != 'true'
-      shell: bash
-      # The file ships broken in OpenJML 21.0.27 to 21.0.29 and breaks the RAC layer; deleting a
-      # bundled spec degrades the affected JDK class to default (empty) contracts, which
-      # is exactly what this repo needs — StreamBuffer's own contracts are the ones being
-      # checked. `rm` without -f: if an upgrade removes/fixes the file upstream, this
-      # step fails loudly and the fixup (plus the cache-key suffix) must be revisited.
-      #   - ArrayDeque.jml: references the undeclared model variable `containsNull`;
-      #     `openjml --rac` fails with "cannot find symbol: containsNull".
-      #     Still open upstream (comment on OpenJML/OpenJML#806, closed issue).
-      # Dropped in v2: concurrent/atomic/AtomicLong.jml, whose RAC-generated checks read the
-      # private field AtomicLong.value across the module boundary (IllegalAccessError in every
-      # test touching the statistics counters). The upstream fix (OpenJML/Specs#29 +
-      # OpenJML/OpenJML#982) shipped in 21.0.29 -- its contracts are `//-RAC@` there -- and the
-      # suite passes against the bundled file (285/285, measured 2026-10-20).
-      run: |
-        set -euo pipefail
-        rm "$RUNNER_TEMP/openjml/specs/java/util/ArrayDeque.jml"
-
-    - name: Repair the bundled JDK release file (fixups v2)
+    - name: Repair the bundled JDK release file (fixups v3)
       if: steps.cache.outputs.cache-hit != 'true'
       shell: bash
       # OpenJML 21.0.27's and 21.0.28's bundled jdk/release omit the JAVA_VERSION key (21.0.29 has

@@ -17,6 +17,11 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Cancellable pipeline start-gate via a `startgate` GitHub Environment with configurable wait timer.
 
 ### Changed
+- Formal verification: the last bundled-spec workaround is gone. OpenJML 21.0.29 also ships the RAC fix
+  for `ArrayDeque.jml` (OpenJML/OpenJML#1012), so the setup action no longer deletes any bundled spec
+  (fixups v3); RAC 285/285 against the unmodified 21.0.29 distribution. The class-invariant blocker is
+  narrowed down: RAC miscompiles an unqualified call from an inner-class method to an outer instance
+  method (`writeSingleByte(b)` in `SBOutputStream`), see TODO.md.
 - Build tooling: spotbugs-maven-plugin 4.10.4.1 -> 4.10.5.0 (SpotBugs 4.10.5, the first release that reads
   JSpecify; nothing to report here), in step with the sibling repositories.
 - Build and test tooling bumped in step with the sibling repositories: Spotless 3.10.4 and Checker
@@ -28,7 +33,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   Lincheck and jcstress runs depend on it.
 - Formal verification: OpenJML 21.0.29 (from 21.0.28). ESC 14/14 (1.7 s locally: SMT commands are now
   pipelined) and RAC 285/285 unchanged. The `AtomicLong.jml` workaround is gone -- the upstream fix
-  (OpenJML/Specs#29) shipped in 21.0.29 -- while `ArrayDeque.jml` is still deleted at install. Class
+  (OpenJML/Specs#29) shipped in 21.0.29 -- while `ArrayDeque.jml` was still deleted at install. Class
   invariants still break RAC (now `NoSuchMethodError` on the inner stream classes), so they stay out.
 - Build tooling: `anthropics/claude-code-action` v1.0.255 (from v1.0.252) and Gradle 9.8.2 in the shared
   `verify-signing-key-gradle` job, in step with the sibling repositories.

@@ -118,10 +118,13 @@ mvn -P jml-rac -Dopenjml.home=<openjml> -Dopenjml.jdk.java=<openjml>/jdk/bin/jav
   invariant inside the constructor of a non-static inner class and reads the field on the wrong
   class → `NoSuchFieldError` at runtime (14-line reproducer: private field + invariant + inner
   class). On this class every test fails (258/285). An earlier 21.0.27 compile crash
-  ("no enclosing instance") was not reproduced. **21.0.29 changed the symptom, not the defect:**
+  ("no enclosing instance") was not reproduced. **21.0.29 fixed that case but not this class:**
   the 14-line reproducer runs clean there, but the four candidate invariants on this class still
-  break RAC -- `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$<n>()` (RAC calls the
-  outer class's invariant check on the inner class), 106 errors (measured 2026-10-20). Re-test on upgrades.
+  break RAC -- `NoSuchMethodError` on `StreamBuffer$SBOutputStream.JML$INV$$<n>()`, 106 errors
+  (measured 2026-10-20). Cause (narrowed down 2026-10-21): an inner-class method calling an outer
+  instance method *without a qualifier* (`writeSingleByte(b)`); RAC checks the callee's receiver
+  invariant on `this` (the inner object) instead of `StreamBuffer.this`. `Outer.this.m()` runs clean.
+  Reproducer in TODO.md. Re-test on upgrades.
 - `//@ nullable_by_default` at the class head is load-bearing for RAC: without it JML's
   non-null-by-default inserts an implicit non-null precondition on every reference parameter, so
   the null-argument tests hit `JmlAssertionError.Precondition` instead of the specified NPE.
@@ -139,12 +142,13 @@ mvn -P jml-rac -Dopenjml.home=<openjml> -Dopenjml.jdk.java=<openjml>/jdk/bin/jav
   The setup action also patches `jdk/release` to add the `JAVA_VERSION` key surefire needs to
   fork that JVM (missing in 21.0.27/21.0.28, present again in 21.0.29; the guarded step is a no-op
   there and stays as a regression guard).
-- One bundled OpenJML JDK spec is known-broken and deleted at install time by
-  `.github/actions/setup-openjml` (`ArrayDeque.jml`: undeclared `containsNull`, still in 21.0.29).
-  The second one, `atomic/AtomicLong.jml` (RAC read the private field `value` →
-  `IllegalAccessError`), was fixed upstream by [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29)
-  + [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982), released in 21.0.29; its
-  `rm` is gone, and the suite passes against the bundled file (285/285).
+- No bundled OpenJML JDK spec is deleted at install any more (fixups v3). Up to 21.0.28 two were
+  broken under RAC and deleted by `.github/actions/setup-openjml`: `ArrayDeque.jml` (undeclared
+  `containsNull`, fixed via [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012))
+  and `atomic/AtomicLong.jml` (RAC read the private field `value` → `IllegalAccessError`, fixed by
+  [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) +
+  [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982)). Both fixes are in 21.0.29;
+  the suite passes against the unmodified distribution (285/285).
 - RAC classes are class-file 65 and live only under `target/rac-classes` — they never enter the
   shipped jar, so the Java 8 bytecode floor is unaffected.
 

@@ -34,8 +34,8 @@ annotated, so everything below is genuinely still open.
     reporting upstream (its native peer already implements the methods the stub model never
     declared). Possible extension: a second harness for the array-read / `waitForAtLeast` blocking
     paths (jcstress already covers those; JPF would make them exhaustive too).
-  - **OpenJML bundled-spec defects** (21.0.28 shipped all of them, built from Specs `1a91cb6`;
-    the pinned 21.0.29 carries the AtomicLong fix and still ships the ArrayDeque one). All three share one cause: a model field declared
+  - **OpenJML bundled-spec defects — all fixed in 21.0.29, no workaround left (fixups v3)**
+    (21.0.28 shipped all of them, built from Specs `1a91cb6`). All three share one cause: a model field declared
     only behind `-RAC` in `java/lang/Iterable.jml` (`values`, `containsNull`) or a private
     `java.base` field (`value`) used in a clause RAC compiles.
     - `atomic/Atomic{Long,Integer,Boolean}.jml` (`value` → `IllegalAccessError` at runtime):
@@ -47,13 +47,13 @@ annotated, so everything below is genuinely still open.
       (fixups v2); RAC 285/285 against the bundled 21.0.29 file.
     - `java/util/ArrayDeque.jml:30` (`containsNull` → RAC compile error) and
       `java/util/Collections.jml:116-117` (`singletonList`, `values` → RAC compile error):
-      **open.** Both are the original errors of the closed
+      **fixed upstream, released in 21.0.29** (`//-RAC@`, Specs `43ab561`). Both are the original errors of the closed
       [OpenJML/OpenJML#806](https://github.com/OpenJML/OpenJML/issues/806) ("repaired" there in
       2024 — true for ESC/check, never for RAC; neither file changed in that window).
       **Reported** with a sweep over all bundled specs (9 files fail `--rac`) and a proposed fix in
       [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012) (2026-10-07).
-      Fix + red/green testspecs cases prepared locally, offered as PRs. Once released: drop the
-      `ArrayDeque.jml` `rm`.
+      **Done 2026-10-21:** the `ArrayDeque.jml` `rm` is gone (fixups v3); RAC compile and 285/285
+      against the unmodified 21.0.29 distribution.
     - Missing `JAVA_VERSION` key in the bundled `jdk/release`: missing in 21.0.28 (reported in #1012),
       **present again in 21.0.29**; the guarded repair step is a no-op there and stays as a guard.
   - **Invariants + non-static inner classes break RAC — confirmed OpenJML bug, reported in
@@ -62,9 +62,27 @@ annotated, so everything below is genuinely still open.
     **21.0.29: the minimal reproducer below runs clean, the defect on this class does not go away** --
     with the four candidate invariants RAC throws `NoSuchMethodError` on
     `StreamBuffer$SBOutputStream.JML$INV$$<n>()` (the outer invariant check called on the inner
-    class), 106 errors (measured 2026-10-20). A reproducer for
-    #1012 therefore needs an inner class whose methods run while the outer invariant is checked.
-    Minimal reproducer:
+    class), 106 errors (measured 2026-10-20).
+    **Narrowed down 2026-10-21 (21.0.29):** the trigger is an inner-class method calling an outer
+    instance method *without a qualifier* -- exactly the delegation `SBOutputStream.write(int)` →
+    `writeSingleByte(b)` (and `writeFromArray`, `closeAll`, `readSingleByte`, `availableClamped`).
+    RAC checks the callee's receiver invariant on `this` (the inner object) instead of
+    `StreamBuffer.this`:
+    ```java
+    public class InvA {
+        private long x = 1;
+        //@ private invariant 0 <= x;
+        void inc() { x++; }
+        class Inner { void go() { inc(); } }
+        public static void main(String... a) { new InvA().new Inner().go(); }
+    }
+    ```
+    → `NoSuchMethodError: 'boolean InvA$Inner.JML$INV$$107()'`. Same with a `private` outer method.
+    Clean: `InvA.this.inc()`, `other.inc()` on another reference, outer → inner calls,
+    `synchronized (InvA.this) { x++; }` inside the inner class. To report on
+    [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012). Possible downstream
+    workaround to try: qualify the delegating calls as `StreamBuffer.this.writeSingleByte(b)`.
+    The 21.0.27/21.0.28 reproducer (fixed in 21.0.29):
     ```java
     public class Outer {
         private long x = 1;

@@ -89,8 +89,9 @@ public class StreamBuffer implements Closeable {
     // 258/285 tests fail. Minimal reproducer: private field + invariant + inner class (see
     // TODO.md). An earlier 21.0.27 compile crash ("no enclosing instance") was not reproduced.
     // 21.0.29: the minimal reproducer passes, but these four invariants on this class still break
-    // RAC with NoSuchMethodError on SBOutputStream.JML$INV$$<n>() (106 errors) -- the same
-    // defect with a different symptom.
+    // RAC with NoSuchMethodError on SBOutputStream.JML$INV$$<n>() (106 errors): the inner streams
+    // call outer instance methods without a qualifier (writeSingleByte(b)), and RAC checks the
+    // callee's invariant on the inner object instead of StreamBuffer.this (see TODO.md).
     // The candidate invariants
     // (0 <= availableBytes, 0 <= positionAtCurrentBufferEntry, 1 <= maxAllocationSize,
     // 0 <= maxObservedBytes) would have been RAC-only value anyway — the ESC layer proves