verify: secs4j cross-validation (independent Java implementation)

20 cross-validation checks PASS against [secs4java8] (Apache 2.0,
kenta-shimizu) — an independent SECS/HSMS implementation in Java by
a different author from a different language ecosystem.  Distinct
implementer = independent spec interpretation.  Two libraries
agreeing on wire bytes is much stronger evidence of spec-correctness
than either alone.

Coverage targets the gap the secsgem-py interop deliberately skipped
(secsgem-py's SFDL grammar couldn't easily express GEM 300 bodies
with variable lists of named scalars):

  - S1F1/F13/F17/F19/F21/F23 — establish comms + namelists
  - S2F17 — clock
  - S2F23 — trace init (5-field body)
  - S2F49 — enhanced remote command (DATAID + OBJSPEC + RCMD + params)
  - S3F17/F19/F25/F27 — full E87 carrier surface (action, slot map
                        verify, transfer with port pair, cancel)
  - S5F13/F17 — exception recovery (EXID + EXRECVRA)
  - S14F9/F11 — E94 CJ create with prjobids list, CJ delete
  - S16F5/F27 — E40 PJ command, E94 CJ command
  - S1F15 — offline cleanup

20/20 PASS against the demo equipment.  Reply S/F matches the spec
for every transaction; specific ACK values vary by equipment state
(CarrierIDUnknown for an unknown carrier is just as valid as Accept
for a known one) so we assert on the wire shape, not the result.

Ship layout:
  interop/secs4j/Dockerfile          — eclipse-temurin:21-jdk + clone
                                       + build of secs4java8 → Export.jar
  interop/secs4j/Secs4jHostHarness.java
                                     — 20 round_trip assertions; uses
                                       Secs2.list/uint4/ascii to build
                                       full GEM 300 bodies; comm.send()
                                       for arbitrary S/F pairs
  interop/secs4j_validate.sh         — orchestrator: builds image,
                                       compiles harness, starts compose
                                       server, runs Java container on
                                       the secs network against it
  .gitea/workflows/ci.yml            — secs4j-interop job in CI
  README.md                          — proof table grows to 7 commands
  .gitignore                         — *.class

After this commit our proof chain has:
  - SEMI E5 KAT          (standards body's own arithmetic)
  - tshark dissector     (Wireshark's HSMS impl)
  - secsgem-py interop   (Python reference impl)
  - **secs4j interop**   (independent Java impl)
  + 426 unit tests, 47 conformance harness checks, 100k random ops,
    YAML validation

Four independent external proofs, three of them on overlapping wire
surface from independent angles.

Plan: VERIFICATION.md §3.

[secs4java8]: https://github.com/kenta-shimizu/secs4java8

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
This commit is contained in:
2026-06-09 16:12:44 +02:00
parent 5baf3f4dc7
commit 2fce2fad0c
6 changed files with 358 additions and 0 deletions
+33
View File
@@ -0,0 +1,33 @@
FROM eclipse-temurin:21-jdk
# secs4java8 (kenta-shimizu) is a second independent SECS/HSMS
# implementation in Java. We use it as a third-party peer to
# cross-validate our C++ server against — distinct author, distinct
# language ecosystem, distinct interpretation of the SEMI standards.
# If both libraries agree on wire bytes, that's much stronger evidence
# of spec-correctness than either alone.
ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update && apt-get install -y --no-install-recommends \
git \
ca-certificates \
bash \
&& rm -rf /var/lib/apt/lists/*
WORKDIR /opt
# Pin to a tagged release if/when one becomes available; until then,
# pin to a known-working commit via depth=1 + checkout. Replace with
# a SHA in CI for full reproducibility.
RUN git clone --depth 1 https://github.com/kenta-shimizu/secs4java8.git secs4java8
WORKDIR /opt/secs4java8
# secs4java8 ships a compile.sh that builds Export.jar. Run it once
# at image build so the harness can just include the resulting jar.
RUN bash compile.sh
# The harness source lives outside this image and is mounted at /work
# when the container runs (so editing the harness doesn't require a
# rebuild).
WORKDIR /work