bernardladenthin · bernardladenthin · Sep 13, 2026 · Sep 12, 2026 · Sep 12, 2026
@@ -0,0 +1,82 @@
+# SPDX-FileCopyrightText: 2014-2026 Bernard Ladenthin <bernard.ladenthin@gmail.com>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+name: Set up OpenJML
+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 392 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.
+
+inputs:
+  version:
+    description: OpenJML release version (GitHub release tag)
+    required: true
+  sha256:
+    description: Expected SHA-256 of the openjml-ubuntu-24.04-<version>.zip release asset
+    required: true
+
+runs:
+  using: composite
+  steps:
+    - name: Restore OpenJML from cache
+      id: cache
+      uses: actions/cache@v6
+      with:
+        path: ${{ runner.temp }}/openjml
+        # spec-fixups-v1: 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
+
+    - name: Download pinned OpenJML (checksum-verified)
+      if: steps.cache.outputs.cache-hit != 'true'
+      shell: bash
+      run: |
+        set -euo pipefail
+        curl --fail --location --retry 3 -o "$RUNNER_TEMP/openjml.zip" \
+          "https://github.com/OpenJML/OpenJML/releases/download/${{ inputs.version }}/openjml-ubuntu-24.04-${{ inputs.version }}.zip"
+        echo "${{ inputs.sha256 }}  $RUNNER_TEMP/openjml.zip" | sha256sum --check --strict
+        mkdir -p "$RUNNER_TEMP/openjml"
+        unzip -q "$RUNNER_TEMP/openjml.zip" -d "$RUNNER_TEMP/openjml"
+        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)
+      if: steps.cache.outputs.cache-hit != 'true'
+      shell: bash
+      # Both files ship broken in OpenJML 21.0.27 and break 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
+      # 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".
+      #   - 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.
+      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)
+      if: steps.cache.outputs.cache-hit != 'true'
+      shell: bash
+      # OpenJML 21.0.27's bundled jdk/release omits the JAVA_VERSION key. 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.
+      run: |
+        set -euo pipefail
+        rel="$RUNNER_TEMP/openjml/jdk/release"
+        grep -q '^JAVA_VERSION=' "$rel" || printf 'JAVA_VERSION="21"\n' >> "$rel"
+
+    - name: Export OPENJML_HOME and print version
+      shell: bash
+      run: |
+        set -euo pipefail
+        echo "OPENJML_HOME=$RUNNER_TEMP/openjml" >> "$GITHUB_ENV"
+        "$RUNNER_TEMP/openjml/openjml" --version
@@ -25,6 +25,16 @@
 
 # virtual machine crash logs, see http://www.java.com/en/download/help/error_hotspot.xml
 hs_err_pid*
+# heap dumps (HeapDumpOnOutOfMemoryError, surefire -Xmx cap, ad-hoc RAC/test forks)
+*.hprof
+
+# JPF interleaving check — build outputs assembled next to src/test/jpf/StreamBuffer.jpf at run
+# time, plus a locally cloned jpf-core. None of it is checked in.
+/jpf-core/
+src/test/jpf/out/
+src/test/jpf/streambuffer-classes/
+src/test/jpf/lib/
+src/test/jpf/jpf-output.log
 
 /target/
 /bin/

@@ -59,6 +59,85 @@ mvn -Pvmlens test
 ```
 The `vmlens` profile pulls in `com.vmlens:api` and runs the `vmlens-maven-plugin` during the `test` phase. Tests using `com.vmlens.api.AllInterleavings` are then driven through every possible thread interleaving. The profile is off by default — vmlens overhead is too high for every build.
 
+## Formal Verification
+
+Two layers, run in a **separate** CI pipeline (`.github/workflows/formal-verification.yml` —
+deliberately not part of the synchronous Publish pipeline and never a required check):
+
+1. **OpenJML ESC** (deductive proof, Z3): the 14 static sequential-core methods (2 validators +
+   12 pure helpers) are proven against full functional contracts.
+2. **OpenJML RAC**: the existing JUnit suite runs against RAC-instrumented classes
+   (violations throw), checking the static contracts plus the instance/stream-adapter contracts.
+3. **JPF interleavings** (`src/test/jpf/`, scheduled/dispatch CI job `jpf-interleavings`): Java
+   PathFinder exhaustively model-checks the concurrent read/write/close protocol. Requires JDK 11;
+   builds jpf-core from a pinned commit with a one-file `AtomicLong` model patch; the harness is
+   compiled at `--release 8` and run under JPF. Local recipe (Docker+JDK 11) in
+   `src/test/jpf/README.md`. Never touches the shipped jar.
+
+The `@GuardedBy("bufferLock")` lock discipline is gated separately by Error Prone in the default
+build. The Checker Framework Lock Checker was evaluated as a further layer and deferred — see
+TODO.md "Formal verification".
+
+**Local commands** (OpenJML 21.0.27 — a native Windows build exists since this release;
+`<openjml>` = unzipped release dir, `<cp>` = output of
+`mvn dependency:build-classpath -Dmdep.outputFile=... -DincludeScope=compile`):
+
+```bash
+# ESC — the --method list is the verified scope; it is mirrored in ESC_METHODS in the workflow
+<openjml>/openjml --esc --progress --timeout 300 --spec-math=bigint \
+  --class-path "<cp>" --specs-path src/main/jml \
+  --method "<ESC_METHODS from the workflow>" \
+  src/main/java/net/ladenthin/streambuffer/StreamBuffer.java
+
+# RAC — compile instrumented classes (Java math both sides), then run the suite against them.
+# The suite MUST fork OpenJML's own JVM (it carries the org.jmlspecs bigint runtime class that
+# the bundled JDK specs reference); the profile does this via -Dopenjml.jdk.java.
+<openjml>/openjml --rac --code-math=java --spec-math=java --class-path "<cp>" \
+  --specs-path src/main/jml -d target/rac-classes \
+  src/main/java/net/ladenthin/streambuffer/StreamBuffer.java
+mvn -P jml-rac -Dopenjml.home=<openjml> -Dopenjml.jdk.java=<openjml>/jdk/bin/java test
+```
+
+**Rules that keep this sound — read before touching `StreamBuffer.java` or the specs:**
+
+- Specs live ONLY in `src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml`. A `.jml` file
+  **replaces** all class-level JML in the `.java` (which therefore stays JML-free), and OpenJML
+  errors on any signature mismatch — so every signature change in `StreamBuffer.java` must be
+  mirrored there, and the verification workflow catches drift.
+- The 12 pure helpers are `static` **because instance-method proof obligations are undecidable
+  for Z3 in this class** (the non-static inner stream classes poison the receiver context —
+  measured, not theorized). New pure helpers must be static or they cannot join the ESC scope.
+- The ESC scope is guarded by an exact proof COUNT in the workflow (`ESC_EXPECTED_PROOFS`);
+  adding/removing a method from the scope means updating `ESC_METHODS` + the count together.
+- `validateOffsetAndLengthToWrite` and `calculateResultingChunks` are marked `code_java_math`
+  in the spec file: both deliberately rely on wrap semantics (overflow-guard idiom; wrap-back
+  at the ceiling-division boundary). Everything else is proven overflow-free under safe math.
+- The exception-message builder `newInvalidOffsetOrLengthToWriteException` carries an ASSUMED
+  (unproven) contract — string concatenation defeats the SMT encoding. Do not inline it back.
+- NO class invariants in the `.jml`: OpenJML 21.0.27's RAC crashes on invariants combined with
+  non-static inner classes ("no enclosing instance" AssertionError). 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.
+  Non-null intent is still enforced where it matters via explicit `requires ... != null`.
+- `validateOffsetAndLengthToWrite` uses a manual `if (b == null) throw new NPE(...)` rather than
+  `Objects.requireNonNull`: under `nullable_by_default` the bundled `Objects.requireNonNull`
+  contract leaves ESC an unprovable ExceptionList goal. Behaviour is identical.
+- The stream logic lives in `private` OUTER methods (`availableClamped`, `readSingleByte`,
+  `readIntoArray`, `writeSingleByte`, `writeFromArray`); the inner `SBInputStream`/
+  `SBOutputStream` are pure delegating shells. Required: OpenJML RAC miscompiles outer-field
+  access from inside non-static inner classes (`NoSuchFieldError` at runtime). Do not move field
+  access back into the inner classes.
+- 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`).
+- 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.
+
 ## Architecture
 
 `StreamBuffer` is a single-class Java library (`net.ladenthin.streambuffer`) that connects an `OutputStream` and `InputStream` through a dynamic FIFO queue — solving the fixed-buffer and cross-thread-deadlock limitations of Java's `PipedInputStream`/`PipedOutputStream`.

@@ -411,6 +411,13 @@ Test coverage includes:
 - Thread interruption during blocked reads (wraps `InterruptedException` in `IOException`)
 - Concurrent read/write stress tests
 - Parallel close without deadlock
+- Deadlock-freedom of every blocking entry point, stress-checked with jcstress `Mode.Termination`
+  (`-Pjcstress`): a thread parked in `read()`, in the second wait phase of `read(byte[], off, len)`,
+  or in `waitForAtLeast(...)` is always released by both a concurrent `write` and a concurrent
+  `close`
+- Exhaustive thread-interleaving model check of the read/write/close protocol with Java PathFinder
+  (`src/test/jpf/`, scheduled CI job + local Docker recipe) — the erschöpfende counterpart to the
+  jcstress stress tests
 - Signal/slot notification via external semaphores on write and all close paths
 - `removeSignal(null)` returning `false` without throwing
 - `addSignal(null)` throwing `NullPointerException`
@@ -426,6 +433,34 @@ Test coverage includes:
 - Concurrent close during active trim — no exceptions or deadlock
 - `decideTrimExecution` pure function — comprehensive table-driven tests covering all boundary conditions and the smart-skip edge case
 
+## Formal Verification
+
+`StreamBuffer` carries machine-checked JML specifications
+([`src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml`](./src/main/jml/net/ladenthin/streambuffer/StreamBuffer.jml)),
+verified in a separate CI pipeline
+([`formal-verification.yml`](./.github/workflows/formal-verification.yml)) in two layers:
+
+- **Deductive proof — OpenJML ESC (Z3).** The complete static, sequential core is *proven*
+  against full functional contracts: both offset/length validators — including the classic
+  `(off + len) < 0` integer-overflow guard, proven equivalent to the clean bounds condition
+  under Java wrap semantics — and the twelve static trim-decision/arithmetic helpers, among
+  them the ceiling division in `calculateResultingChunks` (proven against its multiplicative
+  characterization `m·(⌈a/m⌉−1) < a ≤ m·⌈a/m⌉`, including the wrap-around boundary
+  `a = Long.MAX_VALUE − m + 1`) and the full decision tree of `decideTrimExecution`.
+- **Runtime assertion checking — OpenJML RAC.** The entire JUnit suite additionally runs
+  against RAC-instrumented classes (`mvn -P jml-rac`); every JML contract — the proven static
+  ones plus runtime contracts on the instance API and the two stream adapters — is then
+  checked at runtime and a violation throws instead of scrolling by.
+
+Concurrency itself is outside the deductive scope by JML doctrine (JML specifies sequential
+behavior; OpenJML does not model `volatile` or monitors) and is covered empirically by the
+Lincheck, jcstress and vmlens suites listed above, plus an exhaustive Java PathFinder
+interleaving model check of the read/write/close protocol (`src/test/jpf/`); the lock-holding
+discipline on the FIFO deque is additionally gated by Error Prone's `@GuardedBy` check in the
+ordinary build. The scope rationale — with citations to the published case studies that made the
+same split (LinkedList/TACAS 2020, IdentityHashMap/iFM 2022) — lives in the header of the
+specification file.
+
 ### Contributors: do not upgrade jqwik past 1.9.3
 
 > ⚠️ **DO NOT UPGRADE jqwik past 1.9.3.** jqwik 1.10.0 added an anti-AI prompt-injection string to test stdout; the 1.10.1 user guide states the library "is not meant to be used by any 'AI' coding agents at all." 1.9.3 is the last pre-disclosure release and is the pinned version. See `CLAUDE.md` section "jqwik prompt-injection in test output" for the full context. Dependabot is configured to ignore **all** `net.jqwik` updates (every version, including patches) — see the `ignore` rule in [`.github/dependabot.yml`](./.github/dependabot.yml).