Price the OVMX-EXECUTIVE claim on which code a defect edits, not on what an assertion says (vms-ecf, vms-f26)

.github/workflows/ci.yml

@@ -23,19 +23,49 @@ jobs:
         uses: actions/cache@v4
         with:
           path: /var/cache/apt/archives
-          # Cache-key hygiene, not a correctness fix (vms-fb9 r7): strace was
-          # added to the install list below. restore-keys already falls back
-          # to any apt-${{ runner.os }}- prefix, so apt-get install would
-          # still succeed and fetch strace on a stale-key cache hit -- this
-          # bump only avoids re-downloading it every run.
-          key: apt-${{ runner.os }}-cmake-gcc-readline-strace
+          # Cache-key hygiene, not a correctness fix (vms-fb9 r7, vms-ecf r5):
+          # strace, then libssh-dev, were added to the install list below.
+          # restore-keys already falls back to any apt-${{ runner.os }}-
+          # prefix, so apt-get install would still succeed and fetch them on a
+          # stale-key cache hit -- this bump only avoids re-downloading them
+          # every run.
+          key: apt-${{ runner.os }}-cmake-gcc-readline-strace-libssh
           restore-keys: apt-${{ runner.os }}-
 
+      # libssh-dev IS NOT OPTIONAL FOR THIS JOB, and the reason is a gate
+      # rather than a feature (vms-ecf r5). This job runs ctest, which runs
+      # tests/integration/test_userspace_service_register.sh. That gate derives
+      # the universe of sys$ services from WHAT THE PRODUCT EXPORTS: it
+      # compiles every product .c file and reads the sys$ symbols out of the
+      # objects with nm, because both source-text readings of the universe were
+      # escaped together by one asm-label rename (vms-f26). src/vmsssh/vmssshd.c
+      # is a product source and includes <libssh/libssh.h>, so without this
+      # package the scan compiles 126 of 127 files and the gate REFUSES TO
+      # CERTIFY -- "a service could hide behind a build error", its own words.
+      #
+      # THAT REFUSAL IS CORRECT AND MUST NOT BE WEAKENED. It is the same
+      # property as the -Wno-* flag probe next to it: a price that cannot be
+      # computed must refuse, not certify. The legal fixes are to make the
+      # condition unreachable (this line) or to declare the exclusion in the
+      # gate's header; silently skipping the file, allowlisting it, or
+      # tolerating a short count are not among them. Removing libssh-dev here
+      # does not "skip an optional component" -- it turns the register red.
+      #
+      # WHAT IT DOES NOT DO, measured rather than assumed because the
+      # expectation going in was wrong: it does NOT add test entries. ctest -N
+      # reports 53 with libssh-dev and 53 without -- identical. src/vmsssh
+      # (the daemon) is the part CMake skips when libssh is missing and it
+      # registers no tests; tests/vmsssh (the term_mapping unit test) has no
+      # libssh dependency and is configured either way, deliberately
+      # (CMakeLists.txt:171). So this package changes exactly one thing that
+      # ctest can see: the register gate can compile 127 of 127 product
+      # sources instead of 126, and stops refusing.
       - name: Install build dependencies
         run: |
           sudo apt-get update -qq
           sudo apt-get install -y --no-install-recommends \
-            cmake gcc make libc6-dev libreadline-dev strace libcap2-bin
+            cmake gcc make libc6-dev libreadline-dev strace libcap2-bin \
+            libssh-dev
 
       - name: Cache CMake build
         uses: actions/cache@v4

CMakeLists.txt

@@ -235,21 +235,32 @@ if(BUILD_TESTS)
     # ask "is there another implementation of the same public service the
     # product reaches INSTEAD" — a facade is invisible to a gate that only
     # counts calls to the real thing. Source scan.
+    #
+    # NOT a pure source scan any more (vms-f26): it COMPILES every product .c
+    # file it scans and reads the exported sys$ symbols out of the objects with
+    # nm, because the source-text readings of the universe were all escaped
+    # together by an asm-label rename that left the object symbol-identical.
+    # One compile per product .c file per run, hence the raised timeout.
     add_test(NAME userspace_service_register
         COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/tests/integration/test_userspace_service_register.sh
                 ${CMAKE_CURRENT_SOURCE_DIR})
     set_tests_properties(userspace_service_register PROPERTIES
-        LABELS "integration;authenticity" TIMEOUT 120)
+        LABELS "integration;authenticity" TIMEOUT 300)
 
     # ...and the evasions, on a sandbox copy of the tree. The GREEN controls
     # carry as much weight as the RED ones here: the register's design rests on
     # firing for an undeclared impostor and NOT for legitimate pure computation,
     # and on leaving Rule 10's second answer (delete the service outright) open.
+    # Each control runs the whole gate, and the gate now compiles the tree for
+    # its symbol scan, so the wall clock is (controls x compiles). Measured on
+    # an 8-core box: 99s for 34 controls before the symbol scan, 180s for 39
+    # after. The timeout is set well clear of that because a CI runner has
+    # fewer cores and the compiles are what parallelise.
     add_test(NAME userspace_service_register_negctl
         COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/tests/integration/test_userspace_service_register_negctl.sh
                 ${CMAKE_CURRENT_SOURCE_DIR})
     set_tests_properties(userspace_service_register_negctl PROPERTIES
-        LABELS "integration;authenticity" TIMEOUT 300)
+        LABELS "integration;authenticity" TIMEOUT 900)
 
     # Rule 10/11 standing gate (vms-fb9): a process does not name its own
     # terminal, and SHOW DEVICE does not invent device rows. Keeps the

src/libvms/syssvc/sys_lock.c

@@ -31,17 +31,32 @@
  * OVMX service register (rd vms-d89) -- gate:
  * tests/integration/test_userspace_service_register.sh
  *
- * OVMX-EXECUTIVE: sys$enq (vms-ci.7) proof=tests/qemu/test_syssvc_lock.c -- there is
- *     no userspace lock table and no flock() fallback; the grant decision, the lock
- *     id and the value block all come back from the kernel lock manager.
- * OVMX-EXECUTIVE: sys$enqw (vms-ci.7) proof=tests/qemu/test_syssvc_lock.c -- the same
- *     request as $ENQ with the wait taken in the executive.
- * OVMX-EXECUTIVE: sys$deq (vms-ci.7) proof=tests/qemu/test_syssvc_lock.c -- one-line
- *     pass-through to vms_kif_deq.
+ * OVMX-PARTIAL: sys$enq (vms-ci.7) -- exec: the grant decision, the lock id and the
+ *     value block all come back from the kernel lock manager. There is no userspace
+ *     lock table and no flock() fallback; tests/qemu/test_syssvc_lock.c is the
+ *     A-writes/B-reads proof, and lock-compat-cr-ex mutates the executive code that
+ *     answers it.
+ * OVMX-LOCAL: sys$enq -- the ssdef.h SPELLING of the status. kstat_to_ss() below runs
+ *     in the calling process and maps the kernel numbering onto the public SS$_xxx
+ *     constants; the executive never sees an ssdef.h value.
+ * OVMX-PARTIAL: sys$enqw (vms-ci.7) -- exec: the same request as $ENQ with the wait
+ *     taken in the executive.
+ * OVMX-LOCAL: sys$enqw -- the same userspace status mapping as $ENQ.
+ * OVMX-PARTIAL: sys$deq (vms-ci.7) -- exec: a pass-through to vms_kif_deq; the release
+ *     decision is entirely the kernel lock manager's.
+ * OVMX-LOCAL: sys$deq -- the same userspace status mapping as $ENQ.
  *
- * kstat_to_ss() below translates the kernel's status numbering into the public
- * ssdef.h values. That is a translation of the executive's answer, not a
- * substitute for it: it changes how the answer is spelled, never what it says.
+ * THESE THREE WERE OVMX-EXECUTIVE UNTIL vms-ecf ROUND 4, AND THE DOWNGRADE IS A
+ * MEASUREMENT, NOT A LOSS OF CONFIDENCE IN THE LOCK MANAGER. What sat here was the
+ * hand-written defence "kstat_to_ss() is a translation of the executive's answer, not
+ * a substitute for it: it changes how the answer is spelled, never what it says."
+ * That is exactly the kind of prose the register is not allowed to read, and the
+ * manifest contradicts it: kstat-deadlock-mismapped, kstat-ivlockid-mismapped and
+ * kstat-cvtungrant-mismapped each mutate THIS FILE ONLY -- no executive code at all --
+ * and each changes what a public-API caller observes (SS$_DEADLOCK, SS$_IVLOCKID,
+ * SS$_CVTUNGRANT). A part of the answer a caller receives is therefore computed in
+ * the calling process, which is what OVMX-PARTIAL + OVMX-LOCAL is for. The executive
+ * facts the old lines asserted are all still asserted above, under exec:.
  */
 
 #include <stdint.h>