verification: state no-formal-proof stance + add registry data-integrity invariants

.machine_readable/6a2/STATE.a2ml

@@ -31,6 +31,11 @@ milestones = [
   { name = "Phase 8: Repo lockdown (visibility management)", completion = 0 },
 ]
 
+[verification]
+formal-proofs = "none — no ABI/FFI surface to verify (see PROOF-NEEDS.md, verification/README.adoc)"
+correctness-evidence = "worker/test/ — Worker test suite + data-integrity invariants; gated by worker-ci.yml"
+idris2-proofs = "deferred until/unless a native ABI surface is introduced"
+
 [blockers-and-issues]
 blockers = [
   "Phase 3 deploy: CLOUDFLARE_API_TOKEN repo secret required to enable automated Worker deploys",

verification/README.adoc

@@ -1 +1,29 @@
-= Verification Pillar
+// SPDX-License-Identifier: MPL-2.0
+= Verification Pillar — gv-clade-index
+
+== Status: no formal-proof surface
+
+gv-clade-index is a `gv`/`db` project — a JavaScript Cloudflare Worker over a
+VeriSimDB/KV registry. It has *no native ABI/FFI surface*, so there are no Idris2 /
+Lean / Coq / Agda proofs to maintain here, and none are outstanding. The template
+ABI proofs that once implied otherwise were removed; see `PROOF-NEEDS.md`.
+
+== What stands in for "proofs" here
+
+Correctness is assured by executable evidence appropriate to a data/edge service:
+
+* *Worker test suite* — `worker/test/worker.test.js`: routing, input validation,
+  security headers, CORS, error paths, and a fuzz sweep (no uncontrolled 5xx).
+* *Data-integrity invariants* — `worker/test/data.test.js` asserts the registry's
+  "theorems": the 12-clade invariant; count consistency
+  (`total_repos == |by_name| == Σ member_count`); every clade member resolves;
+  `prefixed == "<clade>-<name>"`; valid secondary codes; and forge primary-key
+  (`github`) + `uuid` uniqueness.
+* *CI gate* — `.github/workflows/worker-ci.yml` runs these on every PR.
+
+== When real proofs would apply
+
+Only if a native/compiled ABI surface is introduced. At that point, add
+domain-specific Idris2 proofs per the pattern referenced in `PROOF-NEEDS.md`
+(e.g. `proven`, `typed-wasm`, `echidna`). The `proofs/`, `safety_case/`, and
+`traceability/` units are retained for RSR structure until then.

verification/proofs/README.adoc

@@ -1 +1,7 @@
+// SPDX-License-Identifier: MPL-2.0
 = Proofs Unit
+
+No formal proofs: gv-clade-index has no ABI/FFI surface to verify (see
+`../README.adoc` and the repo-root `PROOF-NEEDS.md`). Correctness evidence for this
+data/edge service lives in the Worker test suite and the data-integrity invariants
+under `worker/test/`. Add Idris2 proofs here only if a native surface is introduced.

verification/safety_case/README.adoc

@@ -1 +1,7 @@
-= Safety case Unit
+// SPDX-License-Identifier: MPL-2.0
+= Safety Case Unit
+
+Not applicable as a high-assurance safety case: this is a read-only governance
+registry (JavaScript Worker + VeriSimDB), not safety-critical software. Operational
+assurance is provided by the test suite, the CI gate, structured logging, and the
+`/v1/health` + `/v1/ready` probes. See `../README.adoc`.

verification/traceability/README.adoc

@@ -1 +1,7 @@
+// SPDX-License-Identifier: MPL-2.0
 = Traceability Unit
+
+No requirements-to-proof traceability matrix: there are no formal proofs to trace
+(see `../README.adoc`). Phase/requirement tracking lives in
+`.machine_readable/6a2/STATE.a2ml` and `ROADMAP.adoc`; the registry's data invariants
+are traced by `worker/test/data.test.js`.

worker/test/data.test.js

@@ -56,3 +56,35 @@ describe('index.json consistency', () => {
     }
   });
 });
+
+// Registry data-integrity invariants — the "proofs" a governance/registry repo can
+// actually guarantee (this project has no formal ABI/FFI surface; see
+// verification/README.adoc and PROOF-NEEDS.md).
+describe('registry invariants', () => {
+  it('every repo prefixed name is "<clade>-<name>"', () => {
+    for (const r of repos) {
+      expect(r.prefixed).toBe(`${r.clade}-${r.name}`);
+    }
+  });
+
+  it('secondary clade codes are valid and exclude the primary', () => {
+    for (const r of repos) {
+      for (const code of r.secondary || []) {
+        expect(VALID_CLADES).toContain(code);
+        expect(code).not.toBe(r.clade);
+      }
+    }
+  });
+
+  it('forge primary keys (github slugs) are unique', () => {
+    const slugs = repos.map((r) => r.github);
+    expect(new Set(slugs).size).toBe(slugs.length);
+  });
+
+  it('uuids are present, well-formed and unique', () => {
+    const uuidRe = /^[0-9a-f]{8}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{4}-[0-9a-f]{12}$/i;
+    const uuids = repos.map((r) => r.uuid);
+    for (const u of uuids) expect(u).toMatch(uuidRe);
+    expect(new Set(uuids).size).toBe(uuids.length);
+  });
+});