From 217b00d6cee3647f5c5a3587b2f52e4b8fc8cecb Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 21 Jun 2026 01:59:42 +0000 Subject: [PATCH] docs(verification): state no-formal-proof stance; add registry data-integrity invariants MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit gv-clade-index has no ABI/FFI surface, so there are no formal proofs to maintain here (the template Idris2 ABI proofs were removed earlier; see PROOF-NEEDS.md). Make that stance explicit and promote the registry's checkable invariants to executable "proofs". - verification/README.adoc + proofs/safety_case/traceability READMEs: document that formal proofs are N/A for this JS data/edge project and that correctness is assured by worker/test/ + the worker-ci gate; Idris2 proofs deferred until a native surface exists. - .machine_readable/6a2/STATE.a2ml: add [verification] section recording the stance. - worker/test/data.test.js: add invariants — prefixed == "-", valid secondary codes, github primary-key uniqueness, uuid present/well-formed/unique (now 37 tests). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01UCnxjXkN6uDj9YSANuGEgR --- .machine_readable/6a2/STATE.a2ml | 5 +++++ verification/README.adoc | 30 ++++++++++++++++++++++++- verification/proofs/README.adoc | 6 +++++ verification/safety_case/README.adoc | 8 ++++++- verification/traceability/README.adoc | 6 +++++ worker/test/data.test.js | 32 +++++++++++++++++++++++++++ 6 files changed, 85 insertions(+), 2 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 4f64da5..5fe6d7a 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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", diff --git a/verification/README.adoc b/verification/README.adoc index f07e7f3..0341434 100644 --- a/verification/README.adoc +++ b/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 == "-"`; 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. diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index 1ae324d..7b440d1 100644 --- a/verification/proofs/README.adoc +++ b/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. diff --git a/verification/safety_case/README.adoc b/verification/safety_case/README.adoc index 47c8e36..95f9680 100644 --- a/verification/safety_case/README.adoc +++ b/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`. diff --git a/verification/traceability/README.adoc b/verification/traceability/README.adoc index ff23dd7..5b1aed6 100644 --- a/verification/traceability/README.adoc +++ b/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`. diff --git a/worker/test/data.test.js b/worker/test/data.test.js index 7d24d58..dd1c65f 100644 --- a/worker/test/data.test.js +++ b/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 "-"', () => { + 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); + }); +});