bernardladenthin · Oct 20, 2026 · Oct 20, 2026 · Oct 20, 2026
@@ -27,9 +27,9 @@ runs:
       uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6
       with:
         path: ${{ runner.temp }}/openjml
-        # spec-fixups-v1: bump this suffix whenever the fixup step below changes,
+        # spec-fixups-v2: 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-v1
+        key: openjml-ubuntu-x64-${{ inputs.version }}-${{ inputs.sha256 }}-spec-fixups-v2
 
     - name: Download pinned OpenJML (checksum-verified)
       if: steps.cache.outputs.cache-hit != 'true'
@@ -44,31 +44,31 @@ 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 v1)
+    - name: Delete known-broken bundled JDK specs (fixups v2)
       if: steps.cache.outputs.cache-hit != 'true'
       shell: bash
-      # Both files ship broken in OpenJML 21.0.27 and 21.0.28 and break the RAC layer; deleting a
+      # 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 these files upstream, this
+      # 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).
-      #   - concurrent/atomic/AtomicLong.jml: RAC-generated checks read the private field
-      #     AtomicLong.value across the module boundary; every test touching the
-      #     statistics counters then dies with java.lang.IllegalAccessError.
-      #     Upstream fix: OpenJML/Specs#29 + OpenJML/OpenJML#982, merged into dev-21 on
-      #     2026-10-05, NOT in 21.0.28 (built from Specs 1a91cb6); drop this rm once released.
+      # 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"
-        rm "$RUNNER_TEMP/openjml/specs/java/util/concurrent/atomic/AtomicLong.jml"
 
-    - name: Repair the bundled JDK release file (fixups v1)
+    - name: Repair the bundled JDK release file (fixups v2)
       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. maven-surefire-plugin
+      # OpenJML 21.0.27's and 21.0.28's bundled jdk/release omit the JAVA_VERSION key (21.0.29 has
+      # it again, so this is a no-op there, kept as a guard against a regression). maven-surefire-plugin
       # reads that key to fingerprint a forked <jvm> (SystemUtils.toJdkVersionFromReleaseFile);
       # without it the RAC job — which forks this exact JVM so the org.jmlspecs bigint runtime
       # class resolves — dies before any test with an NPE. Add the key if it is missing.

@@ -55,18 +55,18 @@ e8f444ef851bd134330f1505f52b4b0970ef9a62dd76e4c25829241814ba5c73  .github/ISSUE_
 9a24b2a67ab8e6f52016093e9b6a89796adea29887b7820accede06cc0c0d170  .github/workflows/publish.yml#code-style
 6e2ae11dad0616f66bbb2b6e6556f580bb987fd911d7132aa6bee2bfc7cc7b52  .java-version
 71ec85b7a30e80b18a9ab1fac0199cc50d68548e6f00dd116ab0f904ad63aa50  .java-version.license
-3f73b87c4675376cbe80f1fb914bd7020062dcdb9a7ee503d3ef787fd462358a  .github/workflows/claude.yml
-085f19495d9e0812dc90268ea7917579bd6eaf749c669a9f01922272a5cdf06f  .github/workflows/claude-code-review.yml
-463c34f6244675ee5bee3d28c28c84f5eb3c8bea4f45de3f6ce477348d29589c  .github/workflows/scorecard.yml
+30b3bed932fd05a34d79af0155166b548a7597e5ee4913aa105dd82a41d1936d  .github/workflows/claude.yml
+de1479c5c1e662c0f01d6afd0d18b4a71e8d8168b377287ca6e93285eef63358  .github/workflows/claude-code-review.yml
+fe768632e9abc1a8cd39b038a77c1a79dbfd036129bb7f0d84b393251b369be6  .github/workflows/scorecard.yml
 480afc0c1e41f3997b195d7297750b43599ba71a7471657aa32bfc9662b6fd30  .github/workflows/reuse.yml
-cf75cdc06e5ab02359c12b6a8eecb97f2dd3d95502cd2b397d539584cefa56c3  .github/workflows/osv-scanner.yml
+93aedaf67af1c4d63b2502107a51f2f454f2b3b4bc5f2fe892561e12363e57a9  .github/workflows/osv-scanner.yml
 52182fe4073eb696606813d768ff9444e6b751978f9d27a8d84cc269e9f6cb3a  .github/workflows/codeql.yml
 c9e757f2d0a2f456a08791697a94161c776d9b008a8aa75890da4133c81a99e9  .github/dependabot.yml
 f26d05f25a154b84d8f281bb92857811749e2225cdbc167362de930c48b532d1  .github/workflows/publish.yml#startgate
 e3dde66089fd568f03caeefee86ea36a9f6eb7f47e5dc6d053e0e5784fd7a208  .github/workflows/publish.yml#shared-files
 3ef45f189f4419e0d4087f572b3c1b6085c0fe39ac7979b07deb2e882f7ffe8c  .github/workflows/publish.yml#verify-signing-key
 09230b04c5f14bdda50a0c862152ff197a656cbc3fd0d110899c5f8150f8aa9a  .github/workflows/publish.yml#check-snapshot
 51e987d59efd9887b43e345edc0e0f3db21686879e3ca6ea9f0fdbc493d37121  .github/workflows/publish.yml#check-tag
-06f0af70ed125dc5cc1506e27970059fb831971d3faaee56f868789f3282fdf9  .github/workflows/publish.yml#verify-signing-key-gradle
+a4f42a0bfa9b14ca937675052b990e5f1dda238d762f9d0268ac282cd7030c0d  .github/workflows/publish.yml#verify-signing-key-gradle
 c2684a3f93aaf552c13f845307536c2a14dda315c7d7b1e416bc66951b811dc1  .github/workflows/publish.yml#github-snapshot
 c09a030706dbea4221851ca0fcbfa6fc686165b408724724ade61724da6e123b  .github/workflows/publish.yml#github-release
@@ -25,7 +25,7 @@ jobs:
 
       - name: Run Claude Code Review
         id: claude-review
-        uses: anthropics/claude-code-action@f27be6b65a4652f08a2ba3cff79114829b588967 # v1
+        uses: anthropics/claude-code-action@e4a6faad497d33dbc7144135c75e41f82f0bf6c0 # v1
         with:
           anthropic_api_key: ${{ secrets.ANTHROPIC_API_KEY }}
           prompt: |

@@ -36,7 +36,7 @@ jobs:
 
       - name: Run Claude Code
         id: claude
-        uses: anthropics/claude-code-action@f27be6b65a4652f08a2ba3cff79114829b588967 # v1
+        uses: anthropics/claude-code-action@e4a6faad497d33dbc7144135c75e41f82f0bf6c0 # v1
         with:
           anthropic_api_key: ${{ secrets.ANTHROPIC_API_KEY }}
 

@@ -62,13 +62,13 @@ permissions:
   contents: read
 
 env:
-  OPENJML_VERSION: "21.0.28"
-  # SHA-256 of openjml-ubuntu-24.04-21.0.28.zip, taken from the GitHub release asset digest
-  # (https://github.com/OpenJML/OpenJML/releases/tag/21.0.28). ubuntu-latest is ubuntu-24.04,
+  OPENJML_VERSION: "21.0.29"
+  # SHA-256 of openjml-ubuntu-24.04-21.0.29.zip, taken from the GitHub release asset digest
+  # (https://github.com/OpenJML/OpenJML/releases/tag/21.0.29). ubuntu-latest is ubuntu-24.04,
   # matching the asset. When bumping the version: update both values, re-test the RAC spec
   # fixups in .github/actions/setup-openjml/action.yml, and re-try the class invariants noted
   # in src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml.
-  OPENJML_SHA256: "0a151820c4e680e32cb2e399a02615182c748fc24e308865b317783d4836df8a"
+  OPENJML_SHA256: "4fd633e1f555399e47bad8bbbe5ee1f4ae682dab74511ae9e4d7f0a10eeb914b"
   # The ESC scope: the complete static, sequential core of StreamBuffer. Every method listed
   # here MUST prove — and the count guard below additionally fails the job if the number of
   # completed proofs is not exactly ESC_EXPECTED_PROOFS, so a typo here (or a rename in the

@@ -153,7 +153,7 @@ jobs:
           distribution: temurin
       - uses: gradle/actions/setup-gradle@3f5f9adaf7d9fecd50b5935e54106014257a94e6 # v6
         with:
-          gradle-version: "9.8.1"
+          gradle-version: "9.8.2"
       - name: Sign a throwaway artifact via useInMemoryPgpKeys (BouncyCastle)
         shell: bash
         env:

@@ -26,6 +26,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - **CI prints the runner's CPU** at the top of `test`, `vmlens` and the three formal-verification jobs
   (`.github/print-host-info.sh`, a shared file of the four repositories): Z3's proof times and the
   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
+  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.
 - Formal verification: OpenJML 21.0.28 (from 21.0.27; default solver z3 5.1.0). ESC 14/14 and RAC
   285/285 unchanged; the bundled-spec workarounds stay (the upstream fixes are not in 21.0.28).
 - **CI: shared files and the release gate are checked.** The files kept byte-identical with the sibling

@@ -78,7 +78,7 @@ The `@GuardedBy("bufferLock")` lock discipline is gated separately by Error Pron
 build. The Checker Framework Lock Checker was evaluated as a further layer and deferred — see
 TODO.md "Formal verification".
 
-**Local commands** (OpenJML 21.0.28, pinned in the workflow; native Windows builds exist since 21.0.27;
+**Local commands** (OpenJML 21.0.29, pinned in the workflow; native Windows builds exist since 21.0.27;
 `<openjml>` = unzipped release dir, `<cp>` = output of
 `mvn dependency:build-classpath -Dmdep.outputFile=... -DincludeScope=compile`):
 
@@ -118,7 +118,10 @@ 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. Re-test on upgrades.
+  ("no enclosing instance") was not reproduced. **21.0.29 changed the symptom, not the defect:**
+  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.
 - `//@ 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.
@@ -134,13 +137,14 @@ mvn -P jml-rac -Dopenjml.home=<openjml> -Dopenjml.jdk.java=<openjml>/jdk/bin/jav
 - RAC forks OpenJML's OWN JVM (`-Dopenjml.jdk.java`), because the bundled JDK library specs pull
   in `org.jmlspecs.lang.internal.bigint`, a class present only in OpenJML's patched JDK image.
   The setup action also patches `jdk/release` to add the `JAVA_VERSION` key surefire needs to
-  fork that JVM.
-- Two bundled OpenJML JDK specs are known-broken and deleted at install time by
-  `.github/actions/setup-openjml` (`ArrayDeque.jml`: undeclared `containsNull`;
-  `atomic/AtomicLong.jml`: RAC reads the private field `value` → `IllegalAccessError`;
-  upstream fix [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29) + test
-  [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982), merged into `dev-21`,
-  not yet released — still broken in 21.0.28).
+  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).
 - 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,16 +34,17 @@ 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** (pinned 21.0.28 still ships all of them; it was built from
-    Specs `1a91cb6`, before the fixes below). All three share one cause: a model field declared
+  - **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
     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):
-      **fixed upstream, unreleased.** [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29)
+      **fixed upstream, released in 21.0.29** (its contracts are `//-RAC@` there). [OpenJML/Specs#29](https://github.com/OpenJML/Specs/pull/29)
       (`4ebda9c`) + maintainer extension `c365293` on Specs `dev-21`; testspecs
       [OpenJML/OpenJML#982](https://github.com/OpenJML/OpenJML/pull/982) merged into `dev-21`
       (2026-10-05). Verified: streambuffer RAC 285/285 with the fixed spec, 258/285 without.
-      Once released: drop the `AtomicLong.jml` `rm` in `.github/actions/setup-openjml`.
+      **Done 2026-10-20:** the `AtomicLong.jml` `rm` is gone from `.github/actions/setup-openjml`
+      (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
@@ -53,11 +54,16 @@ annotated, so everything below is genuinely still open.
       [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`.
-    - Missing `JAVA_VERSION` key in the bundled `jdk/release`: still missing in 21.0.28
-      (reported in #1012).
+    - 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
     [OpenJML/OpenJML#1012](https://github.com/OpenJML/OpenJML/issues/1012).** RAC checks the outer class's invariant inside the inner class's constructor and
     reads the field on the inner class → `NoSuchFieldError` at runtime (21.0.27 and 21.0.28).
+    **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:
     ```java
     public class Outer {

@@ -88,6 +88,9 @@ public class StreamBuffer implements Closeable {
     // NoSuchFieldError ("SBInputStream does not have member field 'long availableBytes'");
     // 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.
     // The candidate invariants
     // (0 <= availableBytes, 0 <= positionAtCurrentBufferEntry, 1 <= maxAllocationSize,
     // 0 <= maxObservedBytes) would have been RAC-only value anyway — the ESC layer proves