secs-gem/VERIFICATION.md

# External verification plan

The five proofs in [README.md](README.md#proof-of-feature-completeness)
are mostly **us testing us**:

| Proof                          | Independence                                                 |
|--------------------------------|--------------------------------------------------------------|
| 426 unit/integration tests     | Internal — our code testing our code                         |
| 47 conformance harness checks  | Internal — our host driving our server                       |
| 24 secsgem-py interop checks   | **External**, but covers ~15–20 % of the claimed wire surface |
| 100 k random tool ops          | Internal — property test of our model                        |
| YAML validation                | Internal — our validator on our YAML                         |

Only the secsgem-py row is external, and it's thin: it skips most of
GEM 300 (E40 multi-create, E94 CJ-create, E87 slot map / transfer /
cancel, E116, E120, E148, E157), HSMS-GS, S5F9–F18 exception
recovery, S12 wafer maps, S2F49 enhanced commands, and every
wire-level edge case that isn't message-shaped (frame framing, T-timer
expiry behaviours, auto-S9F path).  That's an enormous footprint to
leave on "we both interpret the spec the same way" trust.

This document plans the work to plug that gap with **four independent
external validators**.  None of them is a GEM RTS (that costs money
and needs hardware); none replaces a real-MES integration sweep
([MES_INTEROP.md](MES_INTEROP.md)).  But together they convert the
proof-of-completeness from "trust the unit-test count" to "four
independent codecs, two independent implementations, the standards
body's own bytes, and one fuzzer all agree."

---

## 1.  SEMI E5 known-answer tests (KAT)

**Goal.** Assert our encoder produces the exact bytes the SEMI E5
encoding rules require, and our decoder reverses any spec-conformant
byte stream to the original Item.  Hex-string fixtures, no peer
implementation involved.

**Why it's the strongest single test.** Every other validator is one
implementer's interpretation of the spec.  KAT is the *spec's own
arithmetic*.  If our codec matches the format-byte construction rules
(§9.2-§9.5), it is wire-compatible with anything else that obeys
those rules.

**Method.** A new `tests/test_e5_kat.cpp` with hex-string fixtures
covering every format code:

| Format | Code   | KAT fixture content                                           |
|--------|--------|---------------------------------------------------------------|
| List   | `0x00` | empty list `<L[0]>`, nested list, list with mixed-type items  |
| Binary | `0x20` | empty, 1-byte, 256-byte (length-byte count = 2), 65 536-byte (length-byte count = 3) |
| Boolean| `0x24` | TRUE, FALSE, multi-element vector                             |
| ASCII  | `0x40` | empty, single char, "Hello", 255-byte string, 256-byte string |
| JIS-8  | `0x44` | empty, non-ASCII bytes                                        |
| C2     | `0x48` | empty, ASCII subset, BMP code points                          |
| U1     | `0xA4` | 0, 1, 0x7F, 0xFF, multi-element                               |
| U2     | `0xA8` | 0, 0x0102 big-endian, 0xFFFF, multi-element                   |
| U4     | `0xAC` | 0, 0x01020304, 0xFFFFFFFF, multi-element                      |
| U8     | `0xA0` | 0, 0x0102030405060708, multi-element                          |
| I1     | `0x64` | 0, 1, -1 (0xFF), -128 (0x80), 127 (0x7F)                      |
| I2     | `0x68` | 0, 1, -1, INT16_MIN, INT16_MAX                                |
| I4     | `0x6C` | 0, 1, -1, INT32_MIN, INT32_MAX                                |
| I8     | `0x60` | 0, 1, -1, INT64_MIN, INT64_MAX                                |
| F4     | `0x84` | 0.0, 1.0, -1.0, NaN, +Inf, -Inf, subnormal                    |
| F8     | `0x80` | 0.0, 1.0, -1.0, NaN, +Inf, -Inf                               |

Plus the format-byte length-count cases:

- `length_bytes = 1` (body ≤ 255 bytes)
- `length_bytes = 2` (body 256 – 65 535 bytes)
- `length_bytes = 3` (body 65 536 – 16 777 215 bytes)

Each row in the test is a `(canonical_hex, expected_item)` pair.
`encode(expected_item)` must produce `canonical_hex`; `decode(canonical_hex)`
must produce a value equal to `expected_item`.

**Success criterion.** Every fixture round-trips byte-identical.
Failure on any single one is a spec-deviation bug — fix the codec,
not the fixture.

**Effort.** ~3 hours.  Most of it is constructing the byte sequences
correctly the first time (a one-byte error in a fixture invalidates
the proof).

**Scope limits.** KAT proves byte-level encoding only.  It does not
prove higher-level message structure (S1F3 body has these fields in
this order) — that's covered by `test_messages.cpp`.

---

## 2.  tshark / Wireshark HSMS dissector

**Goal.** Validate our HSMS framing against an independent third
codec — Wireshark's built-in HSMS dissector (in tree since ~2017).

**Why.** Wireshark's dissector is written by network-protocol
authors who don't read our code, didn't talk to us, and don't share
implementation details with secsgem-py.  If they parse our pcap
without warnings, our HSMS framing is wire-correct independently of
both our internal tests and the secsgem-py path.

**Method.** A new script `interop/tshark_dissector_check.sh` that:

1. Starts the C++ server.
2. Captures a pcap of the demo flow via `tcpdump -i any -w trace.pcap 'tcp port 5000'`.
3. Runs the two-container demo client to generate ~24 transactions.
4. Stops the server.
5. Parses `trace.pcap` with `tshark -V -r trace.pcap -d tcp.port==5000,hsms`.
6. Greps the parsed output for `Malformed Packet`, `Dissector bug`,
   or `Unknown PType/SType` and asserts none appear.
7. Greps for known good frames (`Select.req`, `Linktest.req`,
   `S1F13`, `S6F11`) and asserts they appear at least once each.

Wired into `.gitea/workflows/ci.yml` as an additional CI job
(installs `tshark` from apt, runs the script, fails on grep
mismatches).

**Success criterion.** tshark dissects every captured HSMS frame
without errors or warnings.

**Effort.** ~3 hours including CI wiring.

**Scope limits.** Validates HSMS *framing* (4-byte length prefix +
10-byte header) and *control message* shapes (Select / Deselect /
Linktest / Separate / Reject).  Does NOT validate SECS-II body
structure beyond the dissector's depth (which is shallow — Wireshark
displays bodies as hex blobs, doesn't decode S/F semantics).  That's
where KAT and secs4j pick up.

---

## 3.  secs4j cross-validation

**Goal.** Add a second independent SECS implementation as a peer:
[`secs4j`](https://github.com/kenta-shimizu/secs4j), Apache-2.0 Java.

**Why.** secsgem-py and secs4j were written by different authors,
from different language ecosystems, against the same SEMI standards.
Disagreements between them mark spec ambiguities; agreement marks
genuine wire-correctness.  Our secsgem-py interop is *one* peer; this
adds a second.  Most likely to surface GEM 300 issues — secs4j
historically covers E40/E94/E87/E116 more thoroughly than secsgem-py.

**Method.**

1. Add a Docker sidecar `interop/secs4j/` with `eclipse-temurin:21-jdk`,
   maven, and a copy of secs4j cloned + built.
2. Write a `Secs4jHostHarness.java` that:
   - Connects as active HSMS host to our C++ server.
   - Runs the same ~24 checks as `host_vs_cpp_server.py` (S1, S2, S5,
     S6, S7, S10) so we have a like-for-like comparison.
   - Plus the GEM 300 streams secs4j covers natively (S3 carrier
     actions, S14 CJ create, S16 PJ create/command including the full
     variable-list bodies that defeated secsgem-py's SFDL).
   - Asserts each transaction's response code is in the spec-defined
     range.  Exits 0 on success.
3. Cron the harness into `interop/run-secs4j.sh` and add a CI job
   that runs it.

**Survey step (do this first).** Before committing, build secs4j and
catalog which streams/functions it actually supports.  If it covers
strictly less than secsgem-py, the value drops.  Estimated 30 min to
clone + build + list functions.

**Success criterion.** Every check the harness defines exits PASS
against the C++ server, AND secs4j's output for at least 3 streams
secsgem-py couldn't drive (S14, S16 full bodies, S3 slot map) lands
clean.

**Effort.** ~6 hours, with risk:
- Build / dependency problems (Java, maven, secs4j build)
- Coverage gaps (secs4j may not cover what we hoped)
- API differences requiring a different harness structure

If at the survey step secs4j proves unhelpful, we'll write up what we
learned and skip the rest.

**Scope limits.** Same as secsgem-py — peer-implementation comparison
catches "we both got it wrong the same way" but not "we both got it
wrong differently."  Three peers (KAT, secsgem-py, secs4j) covering
overlapping subsets together approach the asymptote.

---

## 4.  libFuzzer over codec + SML parser

**Goal.** Catch crashes, out-of-bounds reads, integer overflows, and
infinite loops on arbitrary input to `secs2::decode` and
`secs2::from_sml`.

**Why.** The 26-line `test_fuzz.cpp` exists but is one-shot — it
runs a fixed handful of malformed inputs.  Real fuzzing runs millions
of inputs guided by coverage feedback.  Catches the class of bug
where a malicious or buggy peer sends a frame designed to crash us.

**Method.**

1. Add a `SECSGEM_FUZZ=ON` CMake option that:
   - Sets compiler to clang (libFuzzer is a clang feature).
   - Adds `-fsanitize=fuzzer,address,undefined` to the fuzzer
     targets.
   - Adds two new executables, `fuzz_secs2_decode` and
     `fuzz_sml_parse`, each with a `LLVMFuzzerTestOneInput` entry
     point that calls the respective decoder on the input bytes.
2. Wire a CI job that builds with `SECSGEM_FUZZ=ON` and runs each
   fuzzer for **5 minutes** (long enough to cover the easy bugs;
   short enough to fit a PR cycle).  Stores any crashing inputs as
   CI artifacts.
3. Seed corpus with the SEMI E5 KAT fixtures from (1) plus the
   wire payloads our `interop/` runs produce.  Coverage-guided
   fuzzing starts from a known-good baseline and explores edges.

**Success criterion.** 5-minute run finds no crashes; coverage map
shows growth over time (proving the fuzzer is actually exploring,
not stuck).

**Effort.** ~4 hours including the corpus seed + CI wiring.

**Scope limits.** Catches *crashes and UB*, not *semantic
mismatches*.  A decoder that returns the wrong value silently is
invisible to libFuzzer; KAT and interop catch that.  Combined, they
cover both axes.

---

## Order of execution

Plan: **(1) KAT → (2) tshark → (3) secs4j → (4) libFuzzer.**

Rationale:
- KAT first because it's the highest-leverage individual test (the
  standard's own arithmetic), is cheap, and produces fixtures that
  later seed libFuzzer's corpus.
- tshark second because it's cheap and gives us a third independent
  framing codec.
- secs4j third because it has the largest variance — could be huge
  win, could be a dud.  Worth de-risking with the survey step.
- libFuzzer last because it benefits from the KAT corpus and its
  CI wiring is mostly orthogonal to everything else.

After all four:

| Proof channel                  | Independence                                         |
|--------------------------------|------------------------------------------------------|
| 426 unit/integration tests     | Internal                                             |
| 47 conformance harness checks  | Internal                                             |
| **SEMI E5 KAT**                | **External — standards body's own encoding rules**   |
| **tshark dissector**           | **External — independent network-protocol authors**  |
| **secs4j interop**             | **External — second independent SECS implementation**|
| secsgem-py interop             | External — Python reference impl                     |
| **libFuzzer 5-min run**        | **External — coverage-guided structural search**     |
| 100 k random tool ops          | Internal — property test                             |
| YAML validation                | Internal                                             |

That's **four external proofs**, three of them validating overlapping
slices of the same surface from independent angles.  An adversarial
review can no longer say "you wrote the tests, of course they pass."

---

## What this plan does NOT replace

- **A GEM RTS run.**  Still required for certification; still costs
  money + needs hardware.  Documented in
  [MES_INTEROP.md](MES_INTEROP.md) §10.
- **Per-MES interop sweeps** against the customer's actual MES
  (Camstar, FactoryWorks, etc.).  Still required for any production
  deployment.  See [MES_INTEROP.md](MES_INTEROP.md).
- **Real-fab wire traces.**  No public corpus exists; fabs treat
  their captures as IP.

Those three remain customer-side work.  But the validators in this
plan move "we claim feature completeness" from one external proof
(thin secsgem-py interop) to five (KAT + tshark + secsgem-py +
secs4j + libFuzzer), and that's worth doing.