From 5524c3f88a804d77bc673a0935ac37ef45447e66 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 27 Sep 2026 09:51:31 +0000 Subject: [PATCH 1/4] security(#203): remove the shell from the VCLTGate invocation path MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `invoke_gate/2` ran the gate binary through `sh -c " < "`. Because a shell redirection takes a filename rather than a stream, the payload had to be written to an exclusively-created 0o600 temp file first, which pulled in `write_secure_payload!/2` (collision retries, `:crypto.strong_rand_bytes`, chmod-before-write) plus `shell_quote/1` and an `after File.rm/1` — roughly 45 lines of security-sensitive machinery whose only job was to work around a shell feature we did not need. `System.cmd/3`'s `:input` option writes the payload straight to the child's stdin, so all of that is deleted. `path` becomes argv[0] and is never a shell word, so `VERISIM_VCLT_GATE` cannot smuggle arguments or metacharacters either. `stderr_to_stdout: false` is preserved, matching the previous behaviour; a missing or unrunnable executable still raises `ErlangError` and is still caught by the existing `rescue`, which fails closed to `{:error, :gate_failed}`. The removed code was not buggy — `shell_quote/1` was a sound POSIX single-quote escape and neither the statement nor the schema ever reached the shell. But "correct quoting" has to be re-verified on every edit to this function, whereas "no shell" cannot regress. Removing the mechanism removes the obligation. The test was rewritten rather than adapted. It asserted an unpredictable `vcltgate_*.json` file at mode 600, removed afterwards — properties of the deleted mechanism. It now asserts the underlying guarantee: that shell metacharacters in the statement and schema (`'`, `;`, `|`, `&`, backtick, `$(...)`, `>`, newline, tab) arrive on the child's stdin byte-for-byte, so that if any part of the invocation ever passed through a shell again, at least one would be consumed, expanded or split. `Cargo.toml`: the `quinn-proto` note still described an open transitive chain and said we were "waiting for burn 0.21 stable". `burn` was removed from the workspace in 0.2.0, so the chain is gone — `Cargo.lock` has no burn, quinn, quinn-proto, cubecl or tracel-llvm-bundler crates. The note contradicted `deny.toml` and would have sent the next maintainer to wait on a release that is no longer needed; it now records the closure instead. NOT VERIFIED LOCALLY: no Elixir/BEAM toolchain is installable in the environment where this change was made (hex.pm, repo.hex.pm and erlang.org are all unreachable), so `mix test` and `mix format --check-formatted` were not run. This is the only change in the branch whose correctness rests on reading the `System.cmd/3` documentation rather than on a gate that executed. CI settles it. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- Cargo.toml | 14 +++- TEST_CI_VERIFY.adoc | 8 -- .../lib/verisim/query/vclt_gate.ex | 78 ++++++++----------- .../test/verisim/query/vclt_gate_test.exs | 42 +++++++--- 4 files changed, 74 insertions(+), 68 deletions(-) delete mode 100644 TEST_CI_VERIFY.adoc diff --git a/Cargo.toml b/Cargo.toml index 88941cf5..970546a9 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -123,8 +123,14 @@ lto = true codegen-units = 1 panic = "abort" -# NOTE: quinn-proto (Dependabot alert — build-time only, NOT runtime) -# Chain: burn 0.20 → cubecl-cpu → tracel-llvm-bundler (build dep) → reqwest 0.12 → quinn → quinn-proto -# This is a build-time dependency for LLVM artifact download, not in any production code path. -# Waiting for burn 0.21 stable release. reqwest bumped to 0.13 for direct deps. +# NOTE (historical, resolved): the quinn-proto Dependabot alert (GHSA-4w2j-m93h-cj5j, +# high, remote memory exhaustion) reached this workspace via +# burn 0.20 → cubecl-cpu → tracel-llvm-bundler (build dep) → reqwest 0.12 → quinn → quinn-proto +# `burn` was removed from the workspace entirely in 0.2.0, so the whole chain is +# gone: Cargo.lock contains 0 burn crates and no quinn / quinn-proto / cubecl / +# tracel-llvm-bundler, and reqwest resolves to 0.13.x. There is nothing to wait +# for. An earlier revision of this note said "waiting for burn 0.21 stable", which +# contradicted deny.toml ("the burn ML stack is no longer a dependency at all") +# and would have sent the next maintainer to wait on a release that is no longer +# needed. Closure is recorded in SECURITY-ADVISORIES.adoc. diff --git a/TEST_CI_VERIFY.adoc b/TEST_CI_VERIFY.adoc deleted file mode 100644 index 5f48d75f..00000000 --- a/TEST_CI_VERIFY.adoc +++ /dev/null @@ -1,8 +0,0 @@ -== CI TEST: Verify timeout-minutes fix - -== SPDX-License-Identifier: MPL-2.0 - -== Copyright (c) Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk - -This file triggers CI to verify timeout-minutes fixes work correctly. -Delete after verification. diff --git a/elixir-orchestration/lib/verisim/query/vclt_gate.ex b/elixir-orchestration/lib/verisim/query/vclt_gate.ex index 86ab3631..8d9e9752 100644 --- a/elixir-orchestration/lib/verisim/query/vclt_gate.ex +++ b/elixir-orchestration/lib/verisim/query/vclt_gate.ex @@ -97,20 +97,32 @@ defmodule VeriSim.Query.VCLTGate do defp invoke_gate(path, payload) do try do - tmp = write_secure_payload!(payload) - - try do - # Quote path and tmp — no statement or schema value reaches the shell. - quoted_path = shell_quote(path) - quoted_tmp = shell_quote(tmp) - - {output, exit_code} = - System.cmd("sh", ["-c", "#{quoted_path} < #{quoted_tmp}"], stderr_to_stdout: false) - - handle_gate_result(IO.iodata_to_binary(output), exit_code) - after - File.rm(tmp) - end + # No shell, and no temp file. + # + # This used to be `System.cmd("sh", ["-c", "'#{path}' < '#{tmp}'"])`, which + # needed the payload written to an exclusively-created 0o600 file because a + # shell redirection can only take a filename, not a stream. That pulled in + # `write_secure_payload!/2` (collision retries, `:crypto.strong_rand_bytes`, + # chmod-before-write), `shell_quote/1`, and an `after File.rm/1` — roughly + # 45 lines of security-sensitive machinery whose only job was to work + # around a shell feature we did not need. + # + # `System.cmd/3`'s `:input` option writes the payload straight to the + # child's stdin, so all of that goes away and with it the question of + # whether the quoting was correct. It was correct — `shell_quote/1` was a + # sound POSIX single-quote escape and neither the statement nor the schema + # ever reached the shell — but "correct quoting" is a property that has to + # be re-verified every time this function is edited, whereas "no shell" is + # a property that cannot regress. + # + # `path` is argv[0], never a shell word, so `VERISIM_VCLT_GATE` cannot + # smuggle arguments or metacharacters either. `System.cmd/3` raises + # `ErlangError` when the executable is missing or not runnable; the + # `rescue` below turns that into a fail-closed `{:error, :gate_failed}`, + # which is the documented behaviour for an unavailable gate. + {output, exit_code} = System.cmd(path, [], input: payload, stderr_to_stdout: false) + + handle_gate_result(IO.iodata_to_binary(output), exit_code) rescue e -> Logger.warning("vclt-gate: invocation error: #{Exception.message(e)} — failing closed") @@ -118,36 +130,14 @@ defmodule VeriSim.Query.VCLTGate do end end - defp write_secure_payload!(payload, attempts \\ 8) - - defp write_secure_payload!(_payload, 0), - do: raise("could not allocate an exclusive vclt-gate payload file") - - defp write_secure_payload!(payload, attempts) do - token = 18 |> :crypto.strong_rand_bytes() |> Base.url_encode64(padding: false) - path = Path.join(System.tmp_dir!(), "vcltgate_#{token}.json") - - case File.open(path, [:write, :binary, :exclusive]) do - {:ok, io} -> - try do - # Restrict access before any payload bytes are written. Exclusive - # creation prevents a pre-planted symlink from being followed. - File.chmod!(path, 0o600) - IO.binwrite(io, payload) - path - after - File.close(io) - end - - {:error, :eexist} -> - write_secure_payload!(payload, attempts - 1) - - {:error, reason} -> - raise File.Error, reason: reason, action: "create secure payload", path: path - end - end - - defp shell_quote(str), do: "'" <> String.replace(str, "'", "'\\''") <> "'" + # `write_secure_payload!/2` and `shell_quote/1` were deleted here on 2026-09-27. + # They existed solely to feed a `sh -c` redirection a filename; with + # `System.cmd/3`'s `:input` the payload goes to stdin directly. Removing them is + # the point of the change: less security-sensitive code to keep correct. + # The test that asserted their observable behaviour (an unpredictable + # `vcltgate_*.json` file at mode 600, removed afterwards) has been replaced by + # one that asserts the underlying property instead — that shell metacharacters + # in the statement and schema arrive on stdin verbatim, unparsed. defp handle_gate_result(output, 0) do case Jason.decode(output) do diff --git a/elixir-orchestration/test/verisim/query/vclt_gate_test.exs b/elixir-orchestration/test/verisim/query/vclt_gate_test.exs index e07edcf9..5d900f95 100644 --- a/elixir-orchestration/test/verisim/query/vclt_gate_test.exs +++ b/elixir-orchestration/test/verisim/query/vclt_gate_test.exs @@ -50,15 +50,15 @@ defmodule VeriSim.Query.VCLTGateTest do end @tag :tmp_dir - test "uses a private unpredictable payload file and removes it", %{tmp_dir: tmp} do - stub = Path.join(tmp, "gate-inspect-input") - observation = Path.join(tmp, "input-observation") + test "delivers the payload on stdin, unparsed by any shell", %{tmp_dir: tmp} do + stub = Path.join(tmp, "gate-stdin") + observation = Path.join(tmp, "stdin-observation") + # Copy stdin verbatim to a file so the test can assert on exactly what the + # gate process received, then emit a valid admit response. File.write!(stub, """ #!/bin/sh - input_path=$(readlink /proc/$$/fd/0) - input_mode=$(stat -c '%a' "$input_path") - printf '%s\n%s\n' "$input_path" "$input_mode" > #{shell_quote(observation)} + cat > #{shell_quote(observation)} echo '{"certified_level":6,"levels":[]}' exit 0 """) @@ -66,12 +66,30 @@ defmodule VeriSim.Query.VCLTGateTest do File.chmod!(stub, 0o755) System.put_env("VERISIM_VCLT_GATE", stub) - assert :admit == VCLTGate.check("INSPECT GRAPH FROM HEXAD abc LIMIT 1") - [input_path, input_mode] = observation |> File.read!() |> String.split("\n", trim: true) - - assert input_mode == "600" - assert Path.basename(input_path) =~ ~r/^vcltgate_[A-Za-z0-9_-]{24}\.json$/ - refute File.exists?(input_path) + # Every character here is one a shell parser would act on: single quotes + # (which would close an enclosing quote), `;` `|` `&` (separators), a + # backtick and `$(...)` (command substitution), `>` (redirection), plus a + # literal newline and tab in the schema value. If any part of the invocation + # passed through a shell, at least one of these would be consumed, expanded + # or split before reaching the gate. + # + # So asserting they survive byte-for-byte is a direct test of the property + # that matters — no shell sees the statement or schema. That is strictly + # stronger than what this test previously asserted (an unpredictable + # `vcltgate_*.json` file at mode 600, removed afterwards), which described + # the temp-file mechanism rather than the guarantee it existed to provide. + # The mechanism is gone: `System.cmd/3`'s `:input` writes to stdin directly. + hostile_statement = + "INSPECT GRAPH FROM HEXAD abc WHERE id = '1' ; rm -rf / | x & `id` $(whoami) > /tmp/pwn" + + hostile_schema = %{"probe" => "' ; | & ` $( ) > \n tab\there"} + + assert :admit == VCLTGate.check(hostile_statement, hostile_schema) + + received = Jason.decode!(File.read!(observation)) + assert received["schema_version"] == 1 + assert received["statement"] == hostile_statement + assert received["schema"] == hostile_schema after System.delete_env("VERISIM_VCLT_GATE") end From ff22d1464cb358361b271e9b60b3e981f6511cdd Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 27 Sep 2026 09:52:13 +0000 Subject: [PATCH 2/4] docs(#204,#113,#86): add the missing estate documents and correct the ones that contradicted the implementation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Issue #204 asks for eight documents that `standards`' `check-docs-presence.sh` does not force (it blocks only on README/LICENSE and warns on CONTRIBUTING), so their absence was invisible to CI. Added: ARCHITECTURE.adoc architecture *index*, not a duplicate of docs/architecture/: component map, the AD-001..AD-007 register transcribed from .machine_readable/6a2/META.a2ml (which stays canonical), and a "read this next, by question" table FAQ.adoc short answers with pointers, harvested from existing documents rather than re-answered, so it cannot become a second source of truth SECURITY-ADVISORIES.adoc advisory triage log modelled on standards' 3-practice version: closed / deferred-with-reason, per-advisory exposure table, and an explicit re-evaluate trigger on each deferral .well-known/{humans,security,ai}.txt RFC 9116 contact + Expires 2027-09-27T00:00:00Z pointing at the GitHub private-advisory URL. ai.txt follows standards' live www/.well-known/ai.txt (MPL-2.0/CC-BY-SA-4.0), NOT templates/' MIT+Palimpsest variant, whose licence does not match this repo docs/architecture/snifs-bridge.adoc issue #86 scope analysis, written against measured upstream constraints: no WASI, no filesystem, no sockets, wasm32-freestanding, only i32/i64/f32/f64 and bytes cross the boundary. Verdict: routing the API gateway or the stores through WASM is impossible, not merely unwritten — they need I/O SNIFs does not provide. The viable surface is pure-compute kernels only GOVERNANCE.adoc amended to v2.0.0 for the TPCF perimeter: P3 Community Sandbox with a P1 carve-out for signing keys and the proof core docs/CITATIONS.adoc, debugger/docs/CITATIONS.adoc rewritten to separate what is actually cited from what is adjacent Corrections, each measured against HEAD 681d635 on 2026-09-27 rather than asserted: docs/VCL-SPEC.adoc implementation table named src/vql/VQL{Parser,Types,Bidir,Error, Explain}.res -- files that do not exist. Residue from two completed migrations (vql->vcl, ReScript->AffineScript; zero .res files remain, 32 .affine do). Rewritten with measured counts; six unlisted src/vcl/ modules added. Counts had drifted hard: vcl_executor.ex documented at 1162 lines, actually 2310. Nine inline "ReScript" references naming the implementation language corrected docs/vcl-vs-sql.adoc claimed VCL is read-only, contradicting `statement = query | mutation` in the normative grammar and three implemented mutation parsers. Now states the Octad API is the *preferred* write path while recording that INSERT/UPDATE/DELETE exist as retained legacy forms. Also: "6-core" -> eight-modality (the same paragraph already enumerated eight stores); GROUP BY / ORDER BY / aggregates / HAVING were listed as unsupported although the grammar defines all four; and the six PROOF types listed were not the grammar's six README.adoc project-structure block rewritten against the actual tree; test counts corrected from "510+"/"160+" to the measured 694 Rust (437 #[test] + 257 #[tokio::test]) and 680 Elixir; KNOWN-ISSUES summary claimed "25/25 resolved" where the file catalogues 31 items with 3 open AUDIT.adoc claimed "all 25 catalogued issues are resolved" -- an overclaim in the one document whose job is to be the honest audit trail. Now measured, with each open item named. Also named STATE.scm/META.scm/ECOSYSTEM.scm, which have never existed here (the artefacts are .a2ml) docs/INDEX.adoc added eight root documents that existed but were never indexed; added snifs-bridge.adoc; removed the v-api-gateway/ row (no such directory); same three .scm filenames corrected to the real seven-file 6a2/ set .machine_readable/6a2/STATE.a2ml tech stack named ReScript (migration complete) and Burn (removed in 0.2.0). A dated note records why connectors/clients/rescript/ and playground/src/ were deliberately NOT renamed: renaming a client-SDK directory is a consumer-visible break, not a documentation edit .machine_readable/6a2/0-AI-MANIFEST.a2ml added the ;; SPDX header the other six specs carry. This was the sole warning in a 32-file validate-a2ml.sh scan; it passed reuse lint anyway because REUSE.toml's .machine_readable/** aggregate covers it -- the two tools check different things. Scan is now 32/32 with 0 warnings debugger/Cargo.toml `repository` pointed at hyperpolymath/verisimdb-debugger, which is a 404. The crate lives in-tree at debugger/ 8 stale link labels targets had been fixed but display text still named the old file (link:SECURITY.adoc[SECURITY.md]) Removed TEST_CI_VERIFY.adoc: a scratch artefact in the repo root saying "delete after verification", renamed .md->.adoc instead of deleted. No inbound references. Two divergences are FLAGGED, not resolved, because resolving either would silently pick a winner in a decision that is not a documentation edit: * spec/grammar.ebnf and docs/vcl-grammar.ebnf are both committed and were byte-identical in substance. Two normative grammars is a drift hazard. Both now carry a notice naming spec/ as canonical (it has the @taxonomy tag and is the copy README, EXPLAINME, 0-AI-MANIFEST.a2ml and spec/system-specs.adoc cite) and requiring any edit to land in both. Consolidating means deleting a normative artefact -- owner decision. Also corrected a stale "VQL" comment in spec/. * docs/vcl-vs-vcl-dt.adoc names CONSISTENCY/FRESHNESS/AUTHORIZATION as PROOF types; those are not grammar terminals, and the grammar's CITATION/ACCESS/CUSTOM have no subsection there. A WARNING block now states the mismatch at the point of divergence. Its six subsections were not rewritten. VCL-SPEC's known-inconsistencies list is updated to record items #1 and #3 as closed in the source documents and item #2 as open pending that decision. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/SUPPORT.md | 4 +- .machine_readable/6a2/0-AI-MANIFEST.a2ml | 12 + .machine_readable/6a2/README.adoc | 5 +- .machine_readable/6a2/STATE.a2ml | 25 +- .well-known/ai.txt | 82 +++ .well-known/humans.txt | 96 +++ .well-known/security.txt | 81 +++ ARCHITECTURE.adoc | 322 ++++++++++ AUDIT.adoc | 46 +- CHANGELOG.adoc | 63 ++ EXPLAINME.adoc | 2 +- FAQ.adoc | 367 +++++++++++ GOVERNANCE.adoc | 262 +++++++- README.adoc | 79 ++- SECURITY-ADVISORIES.adoc | 247 ++++++++ SECURITY.adoc | 25 +- ULTRAPLAN-2026-09-27.adoc | 759 +++++++++++++++++++++++ connectors/README.adoc | 2 +- debugger/Cargo.toml | 7 +- debugger/docs/CITATIONS.adoc | 75 ++- docs/CITATIONS.adoc | 108 +++- docs/INDEX.adoc | 83 ++- docs/VCL-SPEC.adoc | 124 ++-- docs/architecture/abi-ffi.adoc | 90 ++- docs/architecture/snifs-bridge.adoc | 351 +++++++++++ docs/architecture/topology.adoc | 18 +- docs/backwards-compatibility.adoc | 2 +- docs/challenges-federated.adoc | 2 +- docs/challenges-hybrid.adoc | 2 +- docs/challenges-standalone.adoc | 2 +- docs/decisions/kraft-comparison.adoc | 2 +- docs/error-handling-strategy.adoc | 2 +- docs/minikanren-integration-v3.adoc | 2 +- docs/normalization-cascade.adoc | 2 +- docs/query-optimization-overview.adoc | 2 +- docs/reversibility-design.adoc | 2 +- docs/safety-and-fault-tolerance.adoc | 2 +- docs/vcl-architecture.adoc | 12 +- docs/vcl-examples.adoc | 4 +- docs/vcl-grammar.ebnf | 11 + docs/vcl-vs-sql.adoc | 49 +- docs/vcl-vs-vcl-dt.adoc | 25 + spec/grammar.ebnf | 20 +- 43 files changed, 3233 insertions(+), 245 deletions(-) create mode 100644 .well-known/ai.txt create mode 100644 .well-known/humans.txt create mode 100644 .well-known/security.txt create mode 100644 ARCHITECTURE.adoc create mode 100644 FAQ.adoc create mode 100644 SECURITY-ADVISORIES.adoc create mode 100644 ULTRAPLAN-2026-09-27.adoc create mode 100644 docs/architecture/snifs-bridge.adoc diff --git a/.github/SUPPORT.md b/.github/SUPPORT.md index 2dfd3c31..93ccdf25 100644 --- a/.github/SUPPORT.md +++ b/.github/SUPPORT.md @@ -19,7 +19,7 @@ Please use the [Question](https://github.com/hyperpolymath/verisimdb/issues/new? ### For Security Issues -**Do NOT open a public issue.** Please see [SECURITY.md](../SECURITY.md) for responsible disclosure instructions. +**Do NOT open a public issue.** Please see [SECURITY.adoc](../SECURITY.adoc) for responsible disclosure instructions. ## Response Times @@ -27,4 +27,4 @@ This is a solo-maintained project. Response times vary but issues are reviewed r ## Contributing -See [CONTRIBUTING.md](../CONTRIBUTING.md) for contribution guidelines. +See [CONTRIBUTING.adoc](../CONTRIBUTING.adoc) for contribution guidelines. diff --git a/.machine_readable/6a2/0-AI-MANIFEST.a2ml b/.machine_readable/6a2/0-AI-MANIFEST.a2ml index cede8a95..2c9e3d9c 100644 --- a/.machine_readable/6a2/0-AI-MANIFEST.a2ml +++ b/.machine_readable/6a2/0-AI-MANIFEST.a2ml @@ -1,3 +1,15 @@ +;; SPDX-License-Identifier: MPL-2.0 +;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +;; +;; 0-AI-MANIFEST.a2ml — AI-assistant context for the 6a2 metadata directory. +;; +;; Header style note: the other six specs in this directory open with a `;;` +;; SPDX block. This file did not, and `.githooks/validate-a2ml.sh` reported +;; "Missing SPDX-License-Identifier in first 10 lines" as a result — the only +;; warning in a 32-file scan. It was compliant with `reuse lint` regardless, +;; because REUSE.toml's `.machine_readable/**` aggregate covers it; the two +;; tools check different things. Added 2026-09-27. + # AI Manifest for 6a2 Directory ## Purpose diff --git a/.machine_readable/6a2/README.adoc b/.machine_readable/6a2/README.adoc index c851cfb9..9b136748 100644 --- a/.machine_readable/6a2/README.adoc +++ b/.machine_readable/6a2/README.adoc @@ -2,7 +2,7 @@ // Copyright (c) Jonathan D.A. Jewell # A2ML 6a2 Directory -This directory contains the 6 core A2ML machine-readable metadata files for this repository. +This directory contains the 7 core A2ML machine-readable metadata files for this repository. ## Files @@ -12,9 +12,10 @@ This directory contains the 6 core A2ML machine-readable metadata files for this - `NEUROSYM.a2ml` - Symbolic semantics, composition algebra - `PLAYBOOK.a2ml` - Executable plans, operational runbooks - `STATE.a2ml` - Project state, phase, milestones, session history +- `0-AI-MANIFEST.a2ml` - AI manifest for this directory ## Standards Compliance These files follow the A2ML Format Family specification from: -https://github.com/hyperpolymath/standards/tree/main/a2ml +https://github.com/hyperpolymath/standards/tree/main/1-formats/a2ml diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 951a1a2b..aec650a7 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -7,7 +7,7 @@ (version "0.1.0") (schema-version "1.0") (created "2026-01-03") - (updated "2026-06-05") + (updated "2026-09-27") (project "VeriSimDB") (repo "github.com/hyperpolymath/verisimdb")) @@ -17,15 +17,30 @@ (tech-stack ("Rust" "core engine + modality stores") ("Elixir/OTP" "orchestration + supervision") - ("ReScript" "VCL parser + federation registry") + ("AffineScript" "VCL parser + type checker + federation registry (src/vcl, src/registry)") ("Coq" "formal proofs (9 modules in formal/, Coq 8.18)") ("Idris2" "VCL-DT type checker / proof bridge") ("HTTP + gRPC" "API surface") ("Tantivy" "document modality (full-text)") - ("Burn" "tensor modality") + ("ndarray" "tensor modality (Burn removed from the workspace in 0.2.0)") ("redb" "graph storage (pure-Rust default)") ("Oxigraph" "graph storage (optional)"))) + ;; ----------------------------------------------------------------------- + ;; Tech-stack currency, re-measured 2026-09-27 against HEAD 681d635: + ;; * 0 `.res` files remain in the tree; 32 `.affine` files do. The + ;; ReScript -> AffineScript migration is complete, so the parser/registry + ;; entry above names AffineScript. Two directory names are still + ;; historical and were deliberately NOT renamed here, because renaming a + ;; client-SDK directory is a consumer-visible break: `connectors/clients/ + ;; rescript/` and `playground/src/`. `rescript.json` is gone, and + ;; `REUSE.toml` still globs `**/*.res` and `rescript.json` harmlessly. + ;; * `Burn` is no longer a dependency at all (see deny.toml and CHANGELOG + ;; 0.2.0), so the tensor modality is ndarray only. The stale + ;; `quinn-proto` note that referenced the burn chain has been corrected in + ;; Cargo.toml; its closure is recorded in SECURITY-ADVISORIES.adoc. + ;; ----------------------------------------------------------------------- + ;; ----------------------------------------------------------------------- ;; Proof status is calibrated to a machine-checked Coq `Print Assumptions` ;; audit (2026-06-05, coqc 8.18). The earlier "8/8 closed / foundation-pack @@ -38,7 +53,7 @@ (components (("verisim-graph" "implemented" "redb default + Oxigraph optional")) (("verisim-vector" "implemented" "HNSW similarity search")) - (("verisim-tensor" "implemented" "ndarray + Burn")) + (("verisim-tensor" "implemented" "ndarray (Burn removed in 0.2.0)")) (("verisim-semantic" "implemented" "CBOR proofs + ZKP bridge")) (("verisim-document" "implemented" "Tantivy 0.26 (PR #76)")) (("verisim-temporal" "implemented" "time-series + versions")) @@ -66,7 +81,7 @@ ("Provenance hash-chain integrity (P2/P3 Coq-verified, modulo an abstract hash)") ("WAL replay (C7 idempotent on observable state, modulo decidable equality)") ("Federation adapters: MongoDB Redis Neo4j ClickHouse SurrealDB InfluxDB MinIO (7x, 105 integration tests)") - ("Client SDKs: Rust Zig Elixir ReScript Julia (Gleam SDK retired 2026-06-01)") + ("Client SDKs: Rust Zig Elixir Julia + the AffineScript SDK (Gleam SDK retired 2026-06-01)") ("Stapeln container ecosystem: compose.toml + .gatekeeper.yaml + manifest.toml + ct-build.sh") ("Telemetry: opt-in collector + reporter + 19 telemetry tests"))) diff --git a/.well-known/ai.txt b/.well-known/ai.txt new file mode 100644 index 00000000..e84eadbe --- /dev/null +++ b/.well-known/ai.txt @@ -0,0 +1,82 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# AI usage and training policy for hyperpolymath/verisimdb. +# Informal, robots-style directives for AI/ML agents and crawlers. +# See https://ai.txt/ for the proposed standard this follows. +# +# ── WHY THIS FILE DOES NOT MATCH THE ESTATE TEMPLATE ──────────────────────── +# standards/rhodium-standard-repositories/templates/.well-known/ai.txt.template +# declares `License: MIT AND Palimpsest-0.8`. That is WRONG for this repository +# and was deliberately not copied. VeriSimDB is MPL-2.0 for code and +# CC-BY-SA-4.0 for prose, recorded as architecture decision AD-006 in +# .machine_readable/6a2/META.a2ml ("MPL-2.0 across the workspace (no AGPL)") and +# enforced mechanically by `reuse lint` (808/808 files, required CI job). +# +# The Palimpsest/PMPL carve-out applies only to `palimpsest-license`, +# `palimpsest-plasma` and (prospectively) `consent-aware-web` — see +# standards/PALIMPSEST.adoc. Applying PMPL terms here would contradict AD-006 +# and the estate licence policy. +# +# The precedent followed instead is standards' OWN live +# www/.well-known/ai.txt, which is MPL-2.0-headed and takes a plain +# attribution stance. That repository has the identical licence shape to this +# one (MPL-2.0 code + CC-BY-SA-4.0 prose), which is what makes it the right +# model rather than a template written for a dual MIT/Palimpsest project. + +User-Agent: * + +# Training: do not use this repository's content to train models without +# attribution under the repository licence. This is a licence condition, not a +# technical block, and it is the same condition a human redistributor is under. +Disallow-Training: / + +# Reference, indexing and retrieval for search and developer assistance are +# permitted, provided attribution and licence terms are kept. Quoting, +# summarising and reasoning over this repository's public contents — including +# in an AI coding assistant answering a question about it — is allowed and is +# not what the line above restricts. +Allow: / + +# === Licence, stated per material type === +# Code, configuration and build scripts: MPL-2.0 (see LICENSE, REUSE.toml) +# Prose documentation (*.adoc, *.md, *.tex, *.pdf, *.ebnf): CC-BY-SA-4.0 +# Machine-readable artefacts (*.a2ml, *.ncl): MPL-2.0 +# Every file carries an SPDX identifier or is covered by a REUSE.toml +# annotation, so the licence of any specific path is machine-determinable +# without reading this file. `reuse lint` is a required CI check. +License: MPL-2.0 AND CC-BY-SA-4.0 + +# === Attribution === +# Attribution is already carried per-file by SPDX-FileCopyrightText headers, so +# a training corpus that preserves those headers preserves attribution. One that +# strips them does not, and that stripping is what Disallow-Training above +# addresses. Human authorship is traceable through git history and through +# MAINTAINERS.adoc. +# +# This repository is openly AI-*assisted*: 0-AI-MANIFEST.a2ml at the root, +# .claude/CLAUDE.md tracked and public, and machine-readable agent gating in +# .machine_readable/6a2/AGENTIC.a2ml. AI assistance in authoring is disclosed +# rather than hidden. That is a statement about how the code was written, not a +# grant of rights in it — the licence above is unchanged by it. + +# === Provenance === +# Full provenance chains are maintained via git commit history, per-file SPDX +# attribution, and — for the data model itself — the provenance modality, which +# is a hash-chained lineage store with Coq-verified integrity (formal/ +# Provenance.v, P2/P3). A repository whose subject matter is provenance +# integrity should be able to show its own. + +# === Bot policy === +# Per-bot directives live in .machine_readable/bot_directives/ and are the +# authoritative policy for named estate bots (echidnabot, finishbot, glambot, +# rhodibot, seambot, sustainabot, robot-repo-automaton, robot-repo-cleaner), +# including cross-thread-quarantine.a2ml. This file is the summary for +# everything else. + +Contact: https://github.com/hyperpolymath/verisimdb/security/advisories/new +Policy: https://github.com/hyperpolymath/verisimdb/blob/main/SECURITY.adoc +Manifest: https://github.com/hyperpolymath/verisimdb/blob/main/0-AI-MANIFEST.a2ml +Governance: https://github.com/hyperpolymath/verisimdb/blob/main/GOVERNANCE.adoc + +# Last updated: 2026-09-27 diff --git a/.well-known/humans.txt b/.well-known/humans.txt new file mode 100644 index 00000000..2fee5356 --- /dev/null +++ b/.well-known/humans.txt @@ -0,0 +1,96 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# humanstxt.org — the humans responsible for this repository. +# Team from MAINTAINERS.adoc; stack from README.adoc's project structure and +# the language policy recorded in .machine_readable/6a2/META.a2ml. + +/* TEAM */ + Lead Maintainer: Jonathan D.A. Jewell + Contact: j.d.a.jewell [at] open.ac.uk + GitHub: https://github.com/hyperpolymath + Role: Project lead, core development, formal methods, governance + + Governance model: sole maintainer (see GOVERNANCE.adoc) + Contribution perimeter: TPCF Perimeter 3 — Community Sandbox, with a + Perimeter 1 carve-out for CI/CD pinning, release + signing and the formal/ proof core. + +/* THANKS */ + Contributors: https://github.com/hyperpolymath/verisimdb/graphs/contributors + Security reporters: none yet — see SECURITY-ADVISORIES.adoc, which says so + plainly rather than omitting the section. + + The hyperpolymath estate, whose sibling repositories this one depends on + intellectually and mechanically: + - vcl-ut VCL-total: the proof-bearing safety substrate + behind VCL (certified Idris2 + trusted parser) + - standards RSR canon, reusable CI/CD and security + workflows, A2ML and Nickel format definitions + - snifs Safe NIFs via WebAssembly sandboxing — the + single cross-language boundary for BEAM-side + access (issue #86) + - echo-types constructive Agda for proof-relevant structured + loss; the residue taxonomy that drift detection + is being aligned to + - tropical-resource-typing max-plus tropical algebra for worst-case + bounds; the planner is already secretly + tropical (parallel = max, sequential = +) + - kategoria the 10-level type-safety challenge used as a + per-level conformance test bed + +/* SITE */ + Project: VeriSimDB — the Veridical Simulacrum Database + What it is: a federated identity-consonance engine. Not primarily a database + of records: each entity is a consonance subject maintained across + up to eight modal witnesses (the octad), with continuous drift + detection and self-normalisation. + Repository: https://github.com/hyperpolymath/verisimdb + Documentation: https://github.com/hyperpolymath/verisimdb/tree/main/docs + Architecture index: ARCHITECTURE.adoc + Orientation: EXPLAINME.adoc + + Languages, and what each is for: + Rust core engine + the eight modality stores (16 crates) + Elixir/OTP orchestration, supervision, federation coordination + AffineScript VCL parser + bidirectional type checker (src/vcl/) + Idris2 ABI definition with formal proofs; VCL-DT type checker + Zig FFI implementation + Coq formal proofs (9 modules in formal/, Coq 8.18) + Nickel contractile policy evaluation (.machine_readable/contractiles/) + + Key dependencies: + redb graph storage — pure-Rust default, no C++ linker (AD-003) + Oxigraph graph storage — optional, feature-flagged + tantivy 0.26 document modality, full-text (AD-007) + hnsw_rs vector modality, HNSW similarity search + ndarray tensor modality + axum + tonic HTTP and gRPC API surface + rustls + ring TLS, pure Rust — no OpenSSL, no aws-lc-sys/cmake + + Build: cargo + mix; just (Justfile) for task running; Podman/selur-compose + for containers; Guix for the development environment (guix.scm). + Pure Rust — no C++ linker required for a stock build. + CI/CD: GitHub Actions, SHA-pinned. 21 required checks on main, including + reuse lint, Coq Print Assumptions whitelists, doc-consonance, + doc-links, CodeQL, OpenSSF Scorecard, gitleaks, cargo-deny and + the weekly panic-attack security scan. + Licences: MPL-2.0 for code, CC-BY-SA-4.0 for prose (AD-006 — "MPL-2.0 across + the workspace, no AGPL"). REUSE-3.3 compliant, 808/808 files. + Standards: RFC 9116 (security.txt), SPDX/REUSE, Rhodium Standard Repository + (RSR) framework, Tri-Perimeter Contribution Framework (TPCF). + + Machine-readable state: .machine_readable/6a2/ (A2ML) — STATE, META, + ECOSYSTEM, AGENTIC, PLAYBOOK, NEUROSYM, 0-AI-MANIFEST. + Bot policy: .machine_readable/bot_directives/ + AI training policy: .well-known/ai.txt + +/* NOTE */ + This repository is instrumented for AI-assisted development and records that + fact rather than hiding it: 0-AI-MANIFEST.a2ml at the root, .claude/CLAUDE.md + tracked and public, and machine-readable agent gating in + .machine_readable/6a2/AGENTIC.a2ml. Every number asserted in the project + documentation is meant to carry the command that measured it. Where one does + not, that is treated as a defect. + + Last updated: 2026-09-27 diff --git a/.well-known/security.txt b/.well-known/security.txt new file mode 100644 index 00000000..292fa56c --- /dev/null +++ b/.well-known/security.txt @@ -0,0 +1,81 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# RFC 9116 — security.txt for hyperpolymath/verisimdb +# https://www.rfc-editor.org/rfc/rfc9116.html +# +# ── READ THIS BEFORE EDITING ──────────────────────────────────────────────── +# The presence of this file ARMS A HARD CI GATE. +# +# The estate `wellknown` job in hyperpolymath/standards +# .github/workflows/governance-reusable.yml (lines 1091-1155) behaves as +# follows: +# +# * While this file is ABSENT, the job emits `::warning::No security.txt +# found.` and exits 0. It warns; it does not fail. +# * Once this file EXISTS, the job hard-errors (`::error::` + exit 1) if +# `^Contact:` is missing, if `^Expires:` is missing, or if `Expires:` is +# in the past. It also warns from 30 days before expiry. +# +# So the eventual red build is BY DESIGN, not a regression. It is a scheduled +# reminder that this file needs renewing, and it is deliberately unignorable: +# a security.txt that silently expires stops being a way to report a +# vulnerability while still looking like one. +# +# RENEWAL: bump `Expires:` below to roughly one year forward, and update the +# `Last updated` line. Do not delete the file to make CI green — that returns +# the gate to warn-only and loses the contact information. +# +# ── CANONICAL URL ─────────────────────────────────────────────────────────── +# GitHub does NOT serve repository-level .well-known/ over HTTP. Verified +# 2026-09-27: GET https://github.com/hyperpolymath/verisimdb/.well-known/security.txt +# returns 404, while GitHub's own org-level +# https://github.com/.well-known/security.txt returns 200. The `Canonical:` +# field below therefore points at the raw content URL, which is the only +# location that actually serves this file. GitHub's UI surfaces the reporting +# flow via the `Contact:` advisory URL instead. + +# === Primary contact === +# GitHub private vulnerability reporting. This is the preferred method: it is +# private, it does not require disclosing an email address, and it gives the +# reporter automatic credit when the advisory is published. Named as the +# preferred method in SECURITY.adoc. +Contact: https://github.com/hyperpolymath/verisimdb/security/advisories/new + +# === Expiration === +# One year from the date this file was added. See the renewal note above. +Expires: 2027-09-27T00:00:00Z + +# === Policy === +# Threat model, disclosure policy, scope (in/out), safe harbour, and the +# response timeline: 48h initial response, 7d triage, status every 7d, +# 90d resolution target, 90d coordinated disclosure. +Policy: https://github.com/hyperpolymath/verisimdb/blob/main/SECURITY.adoc + +# === Acknowledgments === +# Triage log of open, deferred and closed advisories, with per-advisory +# exposure assessment and explicit re-evaluate triggers. Researcher credits +# are recorded there; as of 2026-09-27 there are none yet, and that file says +# so explicitly rather than omitting the section. +Acknowledgments: https://github.com/hyperpolymath/verisimdb/blob/main/SECURITY-ADVISORIES.adoc + +# === Preferred languages === +Preferred-Languages: en + +# === Canonical === +Canonical: https://raw.githubusercontent.com/hyperpolymath/verisimdb/main/.well-known/security.txt + +# === Hiring === +Hiring: https://github.com/hyperpolymath/verisimdb/blob/main/CONTRIBUTING.adoc + +# === Note on Encryption === +# No `Encryption:` field is published. RFC 9116 makes it optional, and this +# repository deliberately does not advertise a PGP fingerprint it cannot commit +# to maintaining: a stale key is worse than no key, because a reporter who +# encrypts to a key nobody holds gets silence instead of a fallback path. The +# GitHub private-advisory `Contact:` above does not require a key at all, which +# is the reason it is the preferred method. If a maintained key is added later, +# publish it here and on keys.openpgp.org, and add a re-evaluate trigger for it +# in SECURITY-ADVISORIES.adoc. + +# Last updated: 2026-09-27 (added; arms the RFC 9116 gate as described above) diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 00000000..47171b5e --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,322 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Architecture Index +:toc: left +:toclevels: 2 +:icons: font + +[.lead] +This is an *index*, not a description. VeriSimDB's architecture is already +written down in about fifteen places; the problem this file solves is that nobody +could find which one. Every entry below links to the document that is +authoritative for its subject. Where two documents disagree, the one marked +*canonical* wins, and the disagreement is named rather than papered over. + +For orientation — what VeriSimDB *is* — read link:EXPLAINME.adoc[EXPLAINME.adoc] +first. This file assumes you already know that an entity is a consonance subject +with up to eight modal witnesses. + +== Architecture decision records + +The decisions are recorded machine-readably in +link:.machine_readable/6a2/META.a2ml[`.machine_readable/6a2/META.a2ml`] under +`(architecture-decisions …)`. *That file is canonical.* The table below is a +transcription for human readers; if it and the a2ml diverge, the a2ml is right +and this table has drifted. + +[cols="1,3,4,2",options="header"] +|=== +|ID |Decision |Rationale |Source + +|AD-001 +|Marr's three levels of analysis as the design lens +|Computational / algorithmic / implementational separation keeps the octad +invariant clean +|`.claude/CLAUDE.md` §"Design Philosophy" + +|AD-002 +|Rust core + Elixir orchestration split +|Rust for performance-critical modality stores; Elixir/OTP for distributed +coordination and fault tolerance +|`README.adoc` + `.claude/CLAUDE.md` §"Architecture" + +|AD-003 +|Pluggable storage backend (`verisim-storage`) with redb as the pure-Rust default +|Eliminates the `oxrocksdb-sys` C++ dependency; Oxigraph is feature-flagged +|`rust-core/verisim-storage` + `rust-core/verisim-graph` + +|AD-004 +|PLONK as the ZKP scheme for the VCL-DT `PROOF` clause +|Universal trusted setup, small proofs, recursion, circuit flexibility +|`contractiles/trust/Trustfile` + +|AD-005 +|Git-backed flat-file store for GitHub CI integration (the `verisimdb-data` repo) +|No persistent server needed for a ~290-repo scanning workflow; `verisim-api` +runs locally as needed +|`.claude/CLAUDE.md` §"GitHub CI Integration" + +|AD-006 +|MPL-2.0 across the workspace (no AGPL) +|Sole-owner repo under the estate licence-policy umbrella +|`LICENSE` + `Cargo.toml` + PR #101 (closes #82) + +|AD-007 +|Tantivy 0.26 with `order_by_score()` for TopDocs +|Tantivy 0.26 collector API change; `lz4_flex` + `lru` CVE resolution via a +transitive bump +|PR #76 +|=== + +Two further decisions are recorded elsewhere and are not in META.a2ml. They are +listed here so the register is not silently incomplete: + +* *KRaft for the metadata/consensus layer* — see + link:docs/decisions/kraft-comparison.adoc[`docs/decisions/kraft-comparison.adoc`]. +* *Rust over SPARK for the core* — see + link:docs/decisions/rust-spark-stance.adoc[`docs/decisions/rust-spark-stance.adoc`], + with the follow-on stance in + link:docs/decisions/proven-coherence.adoc[`docs/decisions/proven-coherence.adoc`]. + +If these should be AD-008 and AD-009 in META.a2ml, that is a one-commit change; +it has not been made because promoting a decision record into the machine-readable +register is an owner call, not a transcription. + +== Component map + +=== Rust core (`rust-core/`) + +Sixteen crates. The eight modality stores are the octad; the rest are the +machinery around it. + +[cols="2,4",options="header"] +|=== +|Crate |Role + +|`verisim-octad` +|The unified entity layer — one entity, eight synchronised representations. +*Read this first.* + +|`verisim-graph` |Graph modality — RDF and property-graph storage. Pure-Rust +redb default; Oxigraph behind a feature flag (AD-003) +|`verisim-vector` |Vector modality — HNSW similarity search +|`verisim-tensor` |Tensor modality — multi-dimensional arrays via `ndarray` +|`verisim-semantic` |Semantic modality — ontology and type system via CBOR proofs +|`verisim-document` |Document modality — full-text search via Tantivy (AD-007) +|`verisim-temporal` |Temporal modality — time-series and versioning +|`verisim-provenance` |Provenance modality — origin tracking, lineage chains, +actor trails +|`verisim-spatial` |Spatial modality — geospatial coordinates, geometry, +proximity + +|`verisim-drift` +|Cross-modal consistency monitoring — the differentiator + +|`verisim-normalizer` +|Self-normalisation engine — repairs the drift `verisim-drift` reports + +|`verisim-planner` |Cost-based query planner +|`verisim-wal` |Write-ahead log for crash recovery +|`verisim-storage` |Pluggable backend abstraction (AD-003) +|`verisim-api` |HTTP + gRPC API server. *The largest crate and the least +tested* — see link:KNOWN-ISSUES.adoc[KNOWN-ISSUES.adoc] +|`verisim-repl` |Interactive VCL REPL +|`verisim-nif` |Rustler NIF bridge for in-process calls from Elixir. *Currently +a stub* — tracked in issue #61 +|=== + +=== Elixir orchestration (`elixir-orchestration/`) + +OTP supervision over the Rust core. Subsystems: `entity`, `drift`, `query`, +`schema`, `federation`, `consensus`, `api`, `telemetry`, `hypatia`, plus +`rust_client.ex`, `nif_bridge.ex`, `transport.ex` and `health_checker.ex`. + +The query path is the part worth understanding: + +---- +VCL string ──► VCLBridge (GenServer) ──► Port (stdin/stdout JSON) + │ + ▼ + AffineScript parser (src/vcl/) + │ + VCLTGate (admissibility) ◄────┘ + │ + ▼ + VCLExecutor ──► VCLTypeChecker ──► QueryRouter ──► Rust core +---- + +`VCLBridge` keeps a long-running parser process and falls back to a built-in +Elixir parser if it is unavailable. *Type checking has no fallback* — with no +parser process, `{:error, :type_checker_unavailable}` is returned, because +silently passing would defeat VCL-DT. `VCLTGate` checks epistemic statements for +VCL-total admissibility before execution and *fails closed*: a gate timeout or +crash blocks the statement rather than allowing it. + +=== VCL language layer (`src/vcl/`) + +Eleven AffineScript modules: `VCLTypes`, `VCLError`, `VCLParser`, +`VCLBidir`, `VCLTypeChecker`, `VCLProofObligation`, `VCLContext`, `VCLExplain`, +`VCLSubtyping`, `VCLCircuit`, `VCLParser_test`. + +[NOTE] +==== +These were ReScript `.res` files under `src/vql/` until recently. Documents that +still say `src/vql/VQLParser.res` are describing a tree that no longer exists. +The residual `vql` spellings in Rust (`verisim-api/src/vql.rs`, +`verisim-planner/src/vql_bridge.rs`) and in the user-facing route +`/api/v1/vql/execute` are *deliberate* and tracked under the staged rename in +issue #84 — `tests/doc-consonance-gate.sh` scopes them out so the gate stays +green while the rename is in flight. +==== + +=== Cross-language boundary (`connectors/`) + +First-class SDKs: *Rust, Elixir, ReScript, Julia, Zig*. Shared contracts live in +`connectors/shared/` (`openapi/`, `proto/`, `json-schema/`); test infrastructure +in `connectors/test-infra/`. + +Other BEAM languages (Gleam, Erlang, and prospectively LFE / Hamler / Akula) are +*not* getting per-language SDKs. They route through the SNIFs WASM bridge — see +link:docs/architecture/snifs-bridge.adoc[`docs/architecture/snifs-bridge.adoc`] +and issue #86. The Gleam SDK was retired on 2026-06-01 (PR #85) for exactly this +reason. + +The ABI is defined in *Idris2* with formal proofs and the FFI is implemented in +*Zig*; the reasoning for both is in +link:docs/architecture/abi-ffi.adoc[`docs/architecture/abi-ffi.adoc`]. + +== Read this next, by question + +[cols="2,3",options="header"] +|=== +|If you want to know… |Read + +|how the processes fit together and what talks to what +|link:docs/architecture/topology.adoc[`docs/architecture/topology.adoc`] +(*canonical* for process topology) + +|how a value crosses a language boundary +|link:docs/architecture/abi-ffi.adoc[`docs/architecture/abi-ffi.adoc`] +(*canonical* for ABI/FFI) + +|how to actually deploy this +|link:docs/deployment/deployment.adoc[`docs/deployment/deployment.adoc`], then +link:docs/deployment-modes.adoc[`docs/deployment-modes.adoc`] for +standalone / federated / hybrid and how to migrate between them + +|what drift is, how it is detected, and how it is repaired +|link:docs/drift-handling.adoc[`docs/drift-handling.adoc`] (*canonical*), with +the three deployment-specific treatments in +link:docs/challenges-standalone.adoc[`challenges-standalone.adoc`], +link:docs/challenges-federated.adoc[`challenges-federated.adoc`] and +link:docs/challenges-hybrid.adoc[`challenges-hybrid.adoc`] + +|at which levels consistency is maintained, and push vs pull +|link:docs/normalization-cascade.adoc[`docs/normalization-cascade.adoc`] + +|how a VCL statement is routed and executed +|link:docs/vcl-architecture.adoc[`docs/vcl-architecture.adoc`] (dual-path +router) + +|what VCL actually means, normatively +|link:docs/VCL-SPEC.adoc[`docs/VCL-SPEC.adoc`] (*canonical*), with the grammar in +link:docs/vcl-grammar.ebnf[`docs/vcl-grammar.ebnf`], the operational semantics in +link:docs/vcl-formal-semantics.adoc[`docs/vcl-formal-semantics.adoc`] and the +type system in link:docs/vcl-type-system.adoc[`docs/vcl-type-system.adoc`] + +|how VCL differs from SQL, and what it deliberately lacks +|link:docs/vcl-vs-sql.adoc[`docs/vcl-vs-sql.adoc`] — *read the warning below +first* + +|how queries are costed and optimised +|link:docs/query-optimization-overview.adoc[`docs/query-optimization-overview.adoc`] +and link:docs/status/planner.adoc[`docs/status/planner.adoc`] + +|what is formally proven, and to what strength +|link:docs/proof-debt.adoc[`docs/proof-debt.adoc`] (*canonical* for the trusted +base), then `formal/` itself + +|where the honest gaps are +|link:KNOWN-ISSUES.adoc[`KNOWN-ISSUES.adoc`] — 31 catalogued, 28 resolved, *3 +open* + +|what changed and when +|link:CHANGELOG.adoc[`CHANGELOG.adoc`] +|=== + +[WARNING] +==== +`docs/vcl-vs-sql.adoc` is *stale in three specific ways*, and +`docs/VCL-SPEC.adoc` §"Known Inconsistencies in Existing Documents" already says +so: it calls VCL read-only, it says there are no mutations, and it says +`GROUP BY` / `ORDER BY` / aggregates are absent. All three were true of v1.0 and +are false of the implemented grammar. The spec resolves them "in favour of the +implemented grammar and source code". Until that comparison guide is corrected, +treat VCL-SPEC as authoritative on what the language does. +==== + +== Formal verification + +Nine Coq modules under `formal/`, compiled and assumption-gated by +`.github/workflows/coq-build.yml`. The gate is *rigorous and honest*: each module +carries a per-module assumptions whitelist, so an axiom appearing where it should +not fails the build rather than passing quietly. + +Current status is calibrated to a machine-checked `Print Assumptions` audit and +is recorded in two places that agree: + +* link:docs/proof-debt.adoc[`docs/proof-debt.adoc`] — the trusted-base ledger. +* `.machine_readable/6a2/STATE.a2ml` → `(formal-proofs …)`. + +In summary: *0 axioms* for Transaction (C2) and VCL (V2); *closed modulo standard +primitives* for Octad, Provenance (P2/P3) and WAL (C7); *structural over +uninterpreted operations, not implementation-linked* for Drift (D1/D2) and +Normalizer (N2); and *one crux axiomatised* — Planner/PlannerSemantic Q1 +(`optimize_is_permutation`). + +Two things are owed and both are recorded in issue #113: discharging the Q1 +axiom, and adding a Coq-model ↔ Rust-implementation refinement link. Without the +second, the proofs are about an abstract model, which `STATE.a2ml` states plainly +rather than overstating. + +`formal/CROSS-REPO-MAP.adoc` maps each proof obligation onto the sibling +repositories (`vcl-ut`, `echo-types`, `tropical-resource-typing`, `kategoria`) +whose existing results bear on it — issue #84 is the research track behind that +map. + +== Machine-readable architecture sources + +These are not documentation; they are artefacts that gates read. + +[cols="2,4",options="header"] +|=== +|Path |Role + +|`.machine_readable/6a2/META.a2ml` |*Canonical* for architecture decisions, +development practices and design rationale +|`.machine_readable/6a2/STATE.a2ml` |Project state, component status, proof +status, session history +|`.machine_readable/6a2/ECOSYSTEM.a2ml` |Position in the estate and related +projects +|`.machine_readable/6a2/AGENTIC.a2ml` |AI-agent operational gating and safety +controls +|`.machine_readable/6a2/PLAYBOOK.a2ml` |Executable plans and operational runbooks +|`.machine_readable/6a2/NEUROSYM.a2ml` |Symbolic semantics and composition +algebra +|`.machine_readable/anchors/ANCHOR.a2ml` |Estate exception anchors +|`.machine_readable/contractiles/` |`Mustfile`, `Trustfile`, `Intendfile`, +`Adjustfile`, `Dustfile`, `Bustfile` — Nickel-evaluated policy +|`.machine_readable/bot_directives/` |Per-bot policy, including +`cross-thread-quarantine.a2ml` +|`0-AI-MANIFEST.a2ml` |Top-level AI manifest +|=== + +== See also + +* link:README.adoc[README.adoc] — capabilities, comparisons, quick start +* link:EXPLAINME.adoc[EXPLAINME.adoc] — orientation; the conceptual model +* link:ROADMAP.adoc[ROADMAP.adoc] — criticality-ordered work plan +* link:GOVERNANCE.adoc[GOVERNANCE.adoc] — how decisions get made here +* link:docs/INDEX.adoc[docs/INDEX.adoc] — the full documentation tree +* link:FAQ.adoc[FAQ.adoc] — short answers with pointers to long ones +* link:TESTING.adoc[TESTING.adoc] — test pyramid and CI gates diff --git a/AUDIT.adoc b/AUDIT.adoc index 53b3b5c0..7d4e533d 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -15,13 +15,18 @@ audit artefacts; it doesn't duplicate their content. See link:KNOWN-ISSUES.adoc[KNOWN-ISSUES.adoc]. Tracks open and resolved technical gaps. Every item names the affected -location, the original problem, the resolution (or current status), and -the impact. As of 2026-05-25 all 25 catalogued issues are resolved; the -file is preserved as the audit trail. +location, the original problem, the resolution (or current status), and the +impact. As of 2026-09-27 the file catalogues *31* items: *28 resolved* and +*3 open* (#29 HTTP API has no authentication, #30 cross-request transactions +return 501, #31 `at_time` returns partial data for multi-update entities). + +This section previously stated that "all 25 catalogued issues are resolved", +which was an overclaim in the one document whose purpose is to be the honest +audit trail. The count and status are now measured from the file itself. == Testing & benchmarking standards -See link:TESTING.md[TESTING.md]. +See link:TESTING.adoc[TESTING.adoc]. Documents the test pyramid, hard CI gates per language, property-test patterns, fuzz corpus location, supply-chain checks, and the next-tier @@ -30,9 +35,20 @@ concurrency model-checking, bench-as-PR-gate, AFL++). == Security policy -See link:SECURITY.md[SECURITY.md]. +See link:SECURITY.adoc[SECURITY.adoc]. + +Threat model, disclosure process, supported versions, safe harbour and response +timeline. + +The *advisory triage log* — open, deferred and closed advisories with +per-advisory exposure assessment and explicit re-evaluate triggers — is +link:SECURITY-ADVISORIES.adoc[SECURITY-ADVISORIES.adoc]. RFC 9116 contact +details are in `.well-known/security.txt`. -Threat model, disclosure process, supported versions. +Non-advisory scanner findings (panic-attack categories) are dispositioned in +`audits/assail-classifications.a2ml`; its keys are validated by +`scripts/validate-assail-classifications.sh` and gated by +`tests/assail-classifications-gate.sh`. == Changelog @@ -43,12 +59,22 @@ non-canonical) live under link:docs/releases/[docs/releases/]. == Documentation index -See link:docs/INDEX.md[docs/INDEX.md] for the full documentation tree. +See link:docs/INDEX.adoc[docs/INDEX.md] for the full documentation tree. == Machine-readable state See link:.machine_readable/[.machine_readable/]: -- `STATE.scm` — current project state and progress -- `META.scm` — architecture decisions and development practices -- `ECOSYSTEM.scm` — position in the ecosystem and related projects +The directory holds A2ML (`.a2ml`) artefacts, not Scheme (`.scm`) ones. Seven +L1 specs live under `6a2/`: + +- `6a2/STATE.a2ml` — current project state, component status, proof status +- `6a2/META.a2ml` — architecture decisions (AD-001…AD-007), development + practices, design rationale. *Canonical for the decision register*, which + link:ARCHITECTURE.adoc[ARCHITECTURE.adoc] transcribes +- `6a2/ECOSYSTEM.a2ml` — position in the ecosystem and related projects +- `6a2/AGENTIC.a2ml`, `6a2/PLAYBOOK.a2ml`, `6a2/NEUROSYM.a2ml`, + `6a2/0-AI-MANIFEST.a2ml` + +Alongside `6a2/`: `anchors/`, `bot_directives/`, `contractiles/` +(Nickel-evaluated policy), `self-validating/` and `svc/`. diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 59ed36a3..67a5d57e 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -9,6 +9,69 @@ All notable changes to VeriSimDB are documented here. This project uses https:// == [Unreleased] +=== Added — Governance, advisory triage and orientation documents (2026-09-27) + +Closes the documentation-presence half of issue #204. `standards`' `check-docs-presence.sh` blocks only on `README`/`LICENSE` and warns on `CONTRIBUTING`, so none of these were CI-forced; they were missing anyway, and their absence meant the repo had no written governance, no advisory log and no orientation path. + +- *`ARCHITECTURE.adoc`* — architecture *index*, not a duplicate of `docs/architecture/`: component map, the AD-001…AD-007 decision register transcribed from `.machine_readable/6a2/META.a2ml` (which remains canonical), and a "read this next, by question" table. +- *`FAQ.adoc`* — short answers with pointers to the long ones, harvested from existing documents rather than re-answered, so it cannot drift into a second source of truth. +- *`SECURITY-ADVISORIES.adoc`* — advisory triage log modelled on `standards`' `3-practice/SECURITY-ADVISORIES.adoc`: closed and deferred-with-reason sections, a per-advisory exposure table, and an explicit re-evaluate trigger on each deferral. Records the two `deny.toml` RUSTSEC suppressions and the closure of the `quinn-proto` chain. +- *`.well-known/humans.txt`*, *`.well-known/security.txt`*, *`.well-known/ai.txt`* — RFC 9116 contact and expiry (`Expires: 2027-09-27T00:00:00Z`, GitHub private-advisory contact URL), plus an AI attribution stance modelled on `standards`' live `www/.well-known/ai.txt`. The `ai.txt` follows the MPL-2.0/CC-BY-SA-4.0 precedent rather than the `templates/` MIT+Palimpsest variant, because that template's licence does not match this repo's. +- *`docs/architecture/snifs-bridge.adoc`* — the issue #86 scope analysis for a SNIFs WASM bridge, written against the measured upstream constraints (no WASI, no filesystem, no sockets; `wasm32-freestanding`; only `i32/i64/f32/f64` and bytes cross the boundary). +- *`docs/CITATIONS.adoc`* and *`debugger/docs/CITATIONS.adoc`* rewritten to separate what is actually cited from what is merely adjacent. + +=== Added — Doc-links gate: every relative link must resolve (2026-09-27) + +Closes issue #204's link-integrity half. + +- *`scripts/check-doc-links.sh`* — resolves every relative `link:` macro target in `*.adoc`/`*.md` against the working tree. Exemptions live in `scripts/doc-links-allowlist.txt` (currently empty: nothing is exempt), so suppressing a link is a visible, reviewable edit rather than an inline comment. +- *`tests/doc-links-gate.sh`* — positive control for the above. A gate that passes on a clean tree is indistinguishable from a gate that does nothing, so this plants a broken link in a scratch copy and asserts the gate rejects it, names the correct target and resolved path, and does not flag a resolving sibling in the same file. +- Both wired into `.github/workflows/doc-consonance.yml` (renamed *Documentation Gates*). No new actions, so `.github/workflows/actions.lock` is unchanged. +- Current state: *363 relative links resolve across 101 documents, 0 exempt.* + +=== Security — `VCLTGate` no longer shells out (2026-09-27) + +Addresses issue #203. + +- *`elixir-orchestration/lib/verisim/query/vclt_gate.ex`* invoked the gate binary through `sh -c` with a hand-rolled `shell_quote/1`, and wrote the payload to an exclusive `0o600` temp file via `write_secure_payload!/2` to keep it off the command line. That is the right instinct defending the wrong layer: the shell itself was the attack surface, and quoting is exactly the kind of code that is correct until it is not. +- Replaced with `System.cmd(path, [], input: payload, stderr_to_stdout: false)`. The payload now travels on *stdin* and no argument list is assembled, so no shell parses it and no quoting is needed. `write_secure_payload!/2` (both clauses) and `shell_quote/1` were deleted — roughly 45 lines of security-critical code that no longer has a reason to exist. +- The corresponding test was rewritten rather than adapted. The old test asserted temp-file naming, a property of the deleted mechanism; the new one asserts the security property that actually matters — that shell metacharacters in a statement or schema arrive *verbatim* on the child's stdin. +- Verified statically only: no Elixir/BEAM toolchain is installable in the environment where this change was made (see "Not done" below), so `mix test` and `mix format --check-formatted` were not run locally and will first execute in CI. + +=== Changed — Corrected documentation that contradicted the implementation (2026-09-27) + +Issue #113 and the residue left by the 2026-07-07 docs-hygiene pass. + +- *`docs/VCL-SPEC.adoc` implementation-files table*: named `src/vql/VQL{Parser,Types,Bidir,Error,Explain}.res` — files that do not exist. Residue from two completed migrations (`vql` → `vcl`, and ReScript → AffineScript; *zero* `.res` files remain in the tree, 32 `.affine` files do). Rewritten against measured line counts, and six modules present in `src/vcl/` but never listed were added. Counts had drifted materially — `vcl_executor.ex` was documented at 1162 lines and is 2310. Nine further inline "ReScript" references that named the implementation language were corrected. +- *`docs/vcl-vs-sql.adoc`*: described VCL as **read-only**, contradicting `statement = query | mutation ;` in the normative grammar and three implemented mutation parsers. Now states that the Octad API is the *preferred* write path while recording that `INSERT`/`UPDATE`/`DELETE` exist as retained legacy forms. Also corrected: "6-core" → eight-modality (the same paragraph already enumerated eight stores); `GROUP BY`, `ORDER BY`, aggregate functions and `HAVING` were listed as unsupported although the grammar defines all four; and the six `PROOF` types listed were not the grammar's six. +- *`README.adoc`*: project-structure block rewritten against the actual tree (17 `rust-core/` crates, `src/vcl/`, `debugger/` in-tree, `lib/` auxiliary modules, `.machine_readable/` contents). Test counts corrected from "510+"/"160+" to the measured 694 Rust (437 `#[test]` + 257 `#[tokio::test]`) and 680 Elixir. The `KNOWN-ISSUES` summary claimed "25/25 resolved"; the file catalogues 31 items with 3 open. +- *`AUDIT.adoc`*: claimed "all 25 catalogued issues are resolved" — an overclaim in the one document whose purpose is to be the honest audit trail. Now measured (31 catalogued, 28 resolved, 3 open, each named). Its machine-readable section named `STATE.scm`/`META.scm`/`ECOSYSTEM.scm`; those files have never existed here (the artefacts are `.a2ml`). Added pointers to `SECURITY-ADVISORIES.adoc` and the assail classification registry. +- *`docs/INDEX.adoc`*: added the root documents that existed but were never indexed (`EXPLAINME`, `ARCHITECTURE`, `FAQ`, `GOVERNANCE`, `MAINTAINERS`, `CODEOWNERS-POLICY`, `SECURITY-ADVISORIES`, `ULTRAPLAN`), added `docs/architecture/snifs-bridge.adoc`, removed the `v-api-gateway/` row (no such directory), and corrected the same three `.scm` filenames to the real seven-file `6a2/` set. +- *`.machine_readable/6a2/STATE.a2ml`*: tech stack named ReScript (migration complete) and Burn (removed from the workspace in 0.2.0). Corrected, with a dated note recording why two directory names — `connectors/clients/rescript/` and `playground/src/` — were deliberately *not* renamed: renaming a client-SDK directory is a consumer-visible break, not a documentation edit. +- *`.machine_readable/6a2/0-AI-MANIFEST.a2ml`*: added the `;;` SPDX header the other six specs in the directory carry. This was the sole warning in a 32-file `.githooks/validate-a2ml.sh` scan; it passed `reuse lint` regardless, because `REUSE.toml`'s `.machine_readable/**` aggregate covers it — the two tools check different things. Scan is now 32/32 with 0 warnings. +- *`.machine_readable/6a2/README.adoc`*: "6 core A2ML files" → 7, listed the seventh, and corrected the standards-repo URL to its real `1-formats/a2ml` path. +- *`Cargo.toml`*: the `quinn-proto` suppression note still described an open transitive chain. Replaced with the accurate closure (burn removed in 0.2.0, chain gone; `quinn` is absent from `Cargo.lock`). +- Eight link *labels* whose targets had been fixed but whose display text still named the old file (`link:SECURITY.adoc[SECURITY.md]`) were synced. + +=== Removed + +- *`TEST_CI_VERIFY.adoc`* — a scratch artefact left in the repo root. No inbound references anywhere in the tree. + +=== Known issues — flagged, not silently resolved (2026-09-27) + +Two divergences were found that need an owner decision rather than an edit. Both are now flagged at the point of divergence. + +- *Two copies of the normative VCL grammar are committed*: `spec/grammar.ebnf` and `docs/vcl-grammar.ebnf`. They were byte-identical in substance, differing only by `spec/`'s `@taxonomy` and copyright lines and a stale "VQL" wording in a comment (now corrected). `spec/grammar.ebnf` is treated as canonical — it carries the taxonomy tag and is the copy cited by `README.adoc`, `EXPLAINME.adoc`, `0-AI-MANIFEST.a2ml` and `spec/system-specs.adoc`. Maintaining two normative grammars is a drift hazard; both files now carry a notice requiring any edit to be applied to both. Consolidating them means deleting a normative artefact, which is an owner decision. +- *`docs/vcl-vs-vcl-dt.adoc` proof types*: its "Six PROOF Types" section names `CONSISTENCY`, `FRESHNESS` and `AUTHORIZATION`, which are not grammar terminals, and omits the grammar's `CITATION`, `ACCESS` and `CUSTOM`. `VCL-SPEC.adoc` already recorded this as known inconsistency #2 and ruled that the specification follows the grammar. A `WARNING` block was added to the divergent page naming the mismatch; its six subsections were *not* rewritten, because either direction silently picks a winner between "the grammar is right and these were never implemented" and "this page describes an intended v-next proof set and the grammar is behind". Items #1 and #3 of that list are now closed in the source documents. + +=== Not done — toolchain unobtainable in the working environment (2026-09-27) + +Recorded rather than skipped silently, per issue #79's scope ruling. + +- No `rustc`, `cargo`, `erl`, `elixir`, `mix` or `coqc` is present, and every installation source is network-blocked (`rustup.rs`, `static.crates.io`, `index.crates.io`, `forge.rust-lang.org`, `deb.debian.org`, `apt.llvm.org`, `hex.pm`, `repo.hex.pm`, `erlang.org`, `opam.ocaml.org`; `apt-get update` is both permission-denied and unreachable). Consequently *no code change in this entry was compiled or executed locally*: the Rust and Elixir test suites, `cargo clippy`, `mix format --check-formatted` and the Coq build all first run in CI. +- Issue #79's test-expansion work therefore stops at re-measurement. The counts above are measured from source, not from a test run. `rust-core/verisim-nif` remains the worst-density crate at 0 tests / 135 LOC — it is an honest stub returning `{:error, :not_implemented}`, and writing tests for a stub that intentionally does nothing would manufacture coverage rather than add it. +- Only the shell-script and Python-level gates were actually executed here, and all pass: doc-consonance, doc-links (plus its positive control), assail classifications (plus its positive control), `validate-a2ml.sh` (32/32, 0 warnings) and `reuse lint` (809/809). + === Changed — Docs hygiene: retire fossil specs, fix six→eight modality drift (2026-07-07) - Stale-stamped three fossil documents with prominent superseded/historical banners: `docs/status/implementation-plan.adoc` (Week 1–16 / 10%-completion plan), `docs/releases/v0.1.0-alpha.md` ("Production-Ready" / "100% Complete" claims contradicted by KNOWN-ISSUES #29/#30/#31), and `spec/system-specs.md` (pre-octad template spec with a Textual/Numeric/Categorical modality set and `verisimdb-core`/`-nif` Rustler crate layout matching neither the octad nor the real `verisim-*` crates). diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 7563b24e..1927fea3 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -120,7 +120,7 @@ traceable, authorised, and consonant enough to affect live state. modality algebra, provenance hash-chain, drift bounds, planner equivalence, WAL/normaliser idempotence, VCL preservation) — see link:formal/CROSS-REPO-MAP.adoc[the cross-repo map] and - link:docs/proof-debt.md[the trusted-base ledger]. + link:docs/proof-debt.adoc[the trusted-base ledger]. == Where to go next diff --git a/FAQ.adoc b/FAQ.adoc new file mode 100644 index 00000000..ff8651f2 --- /dev/null +++ b/FAQ.adoc @@ -0,0 +1,367 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Frequently Asked Questions +:toc: left +:toclevels: 2 +:icons: font + +[.lead] +Short answers, each pointing at the document that gives the long one. Nothing +here is a new claim: every answer is harvested from an existing canonical source +and linked to it. Where a source has itself gone stale, the answer gives the +*current* behaviour and names the stale document, because a FAQ that quietly +repeats a superseded answer is worse than no FAQ. + +Two FAQ-shaped documents already exist and are not duplicated here: + +* link:docs/business/pr/faq.adoc[`docs/business/pr/faq.adoc`] — 317 lines for + press, analysts and enterprise evaluators, including the competitive + positioning against Neo4j, Pinecone, Weaviate, ArangoDB and SurrealDB, and the + licensing/commercial questions. +* link:EXPLAINME.adoc[`EXPLAINME.adoc`] — the conceptual orientation. If you read + only one thing, read that. + +This file covers the questions those two do not: the ones a developer or a +contributor actually hits. + +== The basics + +=== Is VeriSimDB a database? + +Yes, in all three deployment modes — standalone (a traditional multimodal +database), federated (a distributed database with controlled consistency) and +hybrid (partly local, partly federated). The architectural point is that it +*also* enables federation without forcing you into that model. + +→ link:docs/deployment-modes.adoc#_is_verisimdb_a_database[`docs/deployment-modes.adoc` §"Is VeriSimDB a Database?"] + +=== What is the octad? + +Eight modalities per entity: *graph, vector, tensor, semantic, document, +temporal, provenance, spatial*. Not every entity needs all eight — the octad is +the maximum set, and each entity populates the witnesses it has. + +Eight is not an arbitrary number. Each modality captures a distinct entity-level +semantic: structure (graph), similarity (vector), high-dimensional shape +(tensor), type-system intent (semantic), text content (document), time +(temporal), origin (provenance), location (spatial). Together they span the +practical entity-representation space without redundancy. + +→ `README.adoc` §"The Octad"; rationale recorded as `rationale-octad` in +link:.machine_readable/6a2/META.a2ml[`.machine_readable/6a2/META.a2ml`] + +=== What is drift? + +Divergence between modal witnesses of the same entity. A document is edited +before its embedding is recomputed; a spatial coordinate is refined +independently of the text that describes it; a graph edge outlives the document +it points at. VeriSimDB detects it, classifies it by type, scores its severity, +and can repair it automatically. + +→ link:docs/drift-handling.adoc[`docs/drift-handling.adoc`] + +=== Why "consonance" instead of "consistency"? + +Classic databases enforce consistency up front — transactions, locks — and treat +divergence as an error to prevent. VeriSimDB *expects* modal witnesses to drift +and treats drift as a first-class, typed condition to be measured and repaired. +The maintained property is consonance: the witnesses still refer to the same +identity, within policy. + +The practical consequence is that a modality failure is *not* automatically an +identity failure. `document changed, vector stale` is modal drift, repairable by +normalisation. `hash chain broken` is a provenance/integrity failure. +`remote node asserts an incompatible type` is a federation conflict needing +arbitration. `all live witnesses retracted` is an inactive or tombstoned +identity. Four different states, four different proof obligations, four different +repair paths. + +→ link:EXPLAINME.adoc#_why_consonance_not_consistency[`EXPLAINME.adoc` §"Why consonance, not consistency"] + +=== What is VCL? + +The *VeriSim Consonance Language*. Statements are either *propositions* +(`DECLARE`, `ASSERT`, `RETRACT`) or *epistemic requests* (`INSPECT`, `VERIFY`), +plus `MERGE` / `SPLIT` / `NORMALISE`. They are directed at a consonance engine, +not queries against a passive store. + +[IMPORTANT] +==== +The name is *Consonance*, not *Query*. "VeriSim Query Language" is a retired +misnomer, and `tests/doc-consonance-gate.sh` fails the build if it reappears in +any `*.adoc`, `*.md` or `*.a2ml`. The legacy spelling survives in *code* +identifiers only (`vql_executor`, `/api/v1/vql/execute`, `vql-bridge/`), which is +deliberate and tracked under issue #84's staged rename. +==== + +→ link:docs/VCL-SPEC.adoc[`docs/VCL-SPEC.adoc`] (canonical), +link:docs/vcl-grammar.ebnf[`docs/vcl-grammar.ebnf`], +link:docs/vcl-examples.adoc[`docs/vcl-examples.adoc`] + +=== How does VCL differ from SQL? + +It borrows keywords (`SELECT`, `FROM`, `WHERE`, `LIMIT`, `OFFSET`) and shares +almost nothing else. `SELECT` picks *modalities*, not columns. `FROM` names a +`STORE`, a `HEXAD` (one entity by UUID) or a `FEDERATION`. There are no `JOIN`s +— the graph modality replaces them, since relationships are first-class. And the +`PROOF` clause requests a verifiable guarantee about the result, which has no SQL +analogue at all. + +[WARNING] +==== +link:docs/vcl-vs-sql.adoc[`docs/vcl-vs-sql.adoc`] is *stale in three specific +ways*: it calls VCL read-only, it says there are no mutations, and it says +`GROUP BY`, `ORDER BY` and aggregates are absent. All three were true of v1.0 and +are false of the implemented grammar — mutations are parsed +(`VCLBridge.parse_mutation/2`) and routed, and INSERT/UPDATE/DELETE bypass the +admissibility gate in favour of the proof-verification path. +`docs/VCL-SPEC.adoc` §"Known Inconsistencies in Existing Documents" already +records all three and resolves them in favour of the implementation. Until that +comparison guide is corrected, trust VCL-SPEC. +==== + +→ link:docs/vcl-vs-sql.adoc[`docs/vcl-vs-sql.adoc`] (with the caveat above), +link:docs/VCL-SPEC.adoc[`docs/VCL-SPEC.adoc`] + +=== What is VCL-total? + +The proof-bearing safety substrate *behind* VCL, living in the sibling repository +https://github.com/hyperpolymath/vcl-ut[`vcl-ut`]. It decides whether a proposed +identity transition is *admissible* under schema, modality, provenance, authority, +freshness, resource, effect, federation and proof constraints. + +The proof goal is deliberately narrow — not "prove the whole database correct", +but "prove that *this* identity transition is admissible, traceable, authorised, +and consonant enough to affect live state". + +In this repo the consumer half is `VeriSim.Query.VCLTGate`, which shells out to +the `vclt-gate` binary when `VERISIM_VCLT_GATE` is set and *fails closed*: a +timeout, a crash or an unparseable response blocks the statement rather than +allowing it. + +→ link:EXPLAINME.adoc#_vcl_vcl_total_and_verisimdb[`EXPLAINME.adoc` §"VCL, VCL-total, and VeriSimDB"], +`elixir-orchestration/lib/verisim/query/vclt_gate.ex` + +== Building and running + +=== What do I need to build it? + +Rust (edition 2021) and Elixir 1.17+. *No C++ linker is required* — the build is +pure Rust. That is a deliberate consequence of AD-003: `oxrocksdb-sys` was +removed in favour of redb, and Oxigraph sits behind a feature flag. + +---- +cargo build # Rust core +cd elixir-orchestration && mix deps.get && mix compile +---- + +→ `README.adoc` §"Quick Start" + +=== How do I run it? + +---- +cargo run -p verisim-api # HTTP + gRPC server +cd elixir-orchestration && iex -S mix # orchestration, in another terminal +---- + +[WARNING] +==== +The HTTP API has *no built-in authentication*. Every endpoint is unauthenticated: +any client that can reach the port can read, write or delete any entity. There is +no bearer-token check, no mTLS and no authorisation layer. In development this is +intentional. In any deployment reachable by untrusted clients you must put a +gateway (svalinn, nginx, or similar) in front of it. This is +link:KNOWN-ISSUES.adoc#_29_http_api_has_no_authentication_open[Known Issue #29] +and it is *open*. +==== + +=== How many tests are there? + +Measured 2026-09-27: *694 Rust tests* (437 `#[test]` + 257 `#[tokio::test]`), +*680 Elixir tests*, 28 Criterion benchmark functions, 5 `proptest!` blocks and 4 +libFuzzer targets. + +[NOTE] +==== +`README.adoc` §"Test" still says "Rust: 510+ tests" and "Elixir: 160+ tests". +Both were true when written and both understate the current suite — the Elixir +figure by more than four times. Issue #79 tracks the next expansion +(694 → 1,800 Rust, 5 → 60 `proptest!` blocks, 28 → 90 benches). +==== + +→ link:TESTING.adoc[`TESTING.adoc`] for the pyramid and the CI gates + +=== Is it production-ready? + +No, and the honest answer is more useful than a qualified yes. Three things are +open and each is a deployment blocker for a different reason: + +[cols="1,3,2",options="header"] +|=== +|Issue |What |Consequence + +|#29 |HTTP API has no authentication +|Must sit behind a gateway. Do not expose the port + +|#30 |Cross-request transactions return `501 Not Implemented` +|No multi-round-trip transaction. The in-process `TransactionManager` tracks +lifetime within a single request only + +|#31 |`at_time` returns partial data for multi-update entities +|Temporal reconstruction is reliable only for entities mutated in a single write +|=== + +The `501`s are *deliberate*. Those four endpoints previously returned 200 with +fabricated success objects; they were changed to honest 501s in 0.2.0 under the +principle recorded in the CHANGELOG as "July-1 credibility: honesty over fake +success". + +Data-plane replication is also absent — every modality store is single-instance, +and federation today is leaderless *read* fanout with no cross-peer write +coordination. + +→ link:KNOWN-ISSUES.adoc[`KNOWN-ISSUES.adoc`] (31 catalogued, 28 resolved, 3 +open), `ROADMAP.adoc` §Phase 6 + +=== What is the coverage gate? + +Rust is gated at 60% via `cargo-llvm-cov`. Elixir's floor is currently *40* +(`elixir-orchestration/coveralls.json` → `minimum_coverage`), not 60: actual +coverage settled near 42.6% once the federation adapters grew live-service-only +branches, which is a threshold mismatch rather than a regression. The staged ramp +back to 60 has dated phases. + +→ link:elixir-orchestration/coveralls-coverage-targets.adoc[`elixir-orchestration/coveralls-coverage-targets.adoc`] + +== Architecture and internals + +=== What is it written in? + +*Rust* for the core engine and the modality stores (16 crates under +`rust-core/`); *Elixir/OTP* for orchestration, supervision and federation; +*AffineScript* for the VCL parser and type checker (`src/vcl/`); *Idris2* for the +ABI definition and the VCL-DT type checker; *Zig* for the FFI implementation; +*Coq* for the formal proofs (9 modules under `formal/`). + +→ link:ARCHITECTURE.adoc[`ARCHITECTURE.adoc`] for the full component map + +=== Why Rust and Elixir, and why that split? + +AD-002: Rust for performance-critical modality stores, Elixir/OTP for distributed +coordination and fault tolerance. The boundary is a NIF/port boundary — +`VCLBridge` keeps a long-running parser process over stdin/stdout JSON, and +`verisim-nif` is intended to make the Rust core callable in-process. + +*`verisim-nif` is currently a stub* returning `nif_placeholder`; the real +host-side implementation is tracked in issue #61. It is also the only crate in +the workspace with zero tests. + +→ link:ARCHITECTURE.adoc#_architecture_decision_records[`ARCHITECTURE.adoc`], +link:docs/architecture/abi-ffi.adoc[`docs/architecture/abi-ffi.adoc`] + +=== How do other BEAM languages talk to it? + +Through the *SNIFs WASM bridge*, not through per-language SDKs. The Gleam SDK was +retired on 2026-06-01 (PR #85) precisely because the answer to "do we ship a +Gleam SDK?" is a single principled no: ship one SNIF-compatible WASM module that +any BEAM language can call via `wasmex`, and WASM guest faults become BEAM error +tuples instead of killing the VM. + +First-class SDKs remain Rust, Elixir, ReScript, Julia and Zig. + +→ link:docs/architecture/snifs-bridge.adoc[`docs/architecture/snifs-bridge.adoc`], +issue #86 + +=== What is actually formally proven? + +Calibrated to a machine-checked `Print Assumptions` audit, and stated at the +strength it was actually proved at: + +[cols="2,3",options="header"] +|=== +|Strength |Modules + +|*0 axioms* (fully closed) |Transaction (C2), VCL (V2) +|*Closed modulo standard primitives* |Octad O-series + R1–R3, Provenance (P2/P3, +abstract hash), WAL (C7, decidable equality) +|*Structural over uninterpreted operations* — **not** implementation-linked +|Drift (D1/D2), Normalizer (N2) +|*Crux currently an axiom* |Planner / PlannerSemantic Q1 +(`optimize_is_permutation`) +|=== + +Two things are owed: discharging the Q1 axiom, and adding a Coq-model ↔ +Rust-implementation refinement link. Without the second, the proofs are about an +abstract model. An earlier claim of "8/8 closed / foundation-pack DONE" was an +overclaim and has been removed. + +`coq-build.yml` carries a per-module assumptions whitelist, so an axiom appearing +where it should not fails the build. + +→ link:docs/proof-debt.adoc[`docs/proof-debt.adoc`] (the trusted-base ledger), +`.machine_readable/6a2/STATE.a2ml` → `(formal-proofs …)`, issue #113 + +=== What licence? + +*MPL-2.0* for code, *CC-BY-SA-4.0* for prose. That is AD-006 — "MPL-2.0 across +the workspace (no AGPL)" — and it is enforced mechanically: `reuse lint` is green +at 808/808 files and runs as a required CI job. + +→ link:LICENSE[`LICENSE`], link:REUSE.toml[`REUSE.toml`], +`.well-known/ai.txt` for the AI-training stance + +== Contributing + +=== How do decisions get made? + +Sole-maintainer governance. The repository sits at *TPCF Perimeter 3 (Community +Sandbox)* — anyone can fork, PR and discuss — with a *Perimeter 1 carve-out* for +the paths where a bad change does real damage: CI/CD workflow pinning, release +signing, and the `formal/` proof core. + +Significant changes get a minimum 72 hours of discussion; structural changes +(repo purpose, licence, ownership transfer, archival) get a minimum week. These +are real commitments, not aspirations. + +→ link:GOVERNANCE.adoc[`GOVERNANCE.adoc`], link:MAINTAINERS.adoc[`MAINTAINERS.adoc`], +link:CONTRIBUTING.adoc[`CONTRIBUTING.adoc`] + +=== What will fail my PR? + +The gates that actually block: + +* *`reuse lint`* — every file needs copyright and licence information. +* *`tests/doc-consonance-gate.sh`* — the string "VeriSim Query Language" in any + doc fails the build. +* *`tests/doc-links-gate.sh`* — a broken relative link in any `*.adoc` fails the + build. +* *`coq-build.yml`* — per-module `Print Assumptions` whitelists; an unexpected + axiom fails. +* *`tests/assail-classifications-gate.sh`* — every `(file …)` key in + `audits/assail-classifications.a2ml` must resolve to a real path. +* *`governance.yml`* — the estate reusable workflow, including RFC 9116 + `security.txt` validation once that file exists. + +Plus `rust-ci.yml`, `elixir-ci.yml`, CodeQL, Scorecard, gitleaks and Hypatia. + +→ link:TESTING.adoc[`TESTING.adoc`], link:CONTRIBUTING.adoc[`CONTRIBUTING.adoc`], +`.github/workflows/` + +=== How do I report a security problem? + +Via +https://github.com/hyperpolymath/verisimdb/security/advisories/new[GitHub's private vulnerability reporting], +which is the preferred method and gives automatic credit when the advisory is +published. Full disclosure policy, safe harbour, scope and response timelines are +in link:SECURITY.adoc[`SECURITY.adoc`]. Published advisories and their triage +history are in +link:SECURITY-ADVISORIES.adoc[`SECURITY-ADVISORIES.adoc`]. + +=== Where do I go next? + +* link:EXPLAINME.adoc[`EXPLAINME.adoc`] — orientation, if you have not read it +* link:README.adoc[`README.adoc`] — capabilities, comparisons, quick start +* link:ARCHITECTURE.adoc[`ARCHITECTURE.adoc`] — the architecture index +* link:docs/INDEX.adoc[`docs/INDEX.adoc`] — the full documentation tree +* link:KNOWN-ISSUES.adoc[`KNOWN-ISSUES.adoc`] — the honest gaps +* link:ROADMAP.adoc[`ROADMAP.adoc`] — what is planned, by criticality diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index 8bbf167d..653b6738 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,7 +1,34 @@ // SPDX-License-Identifier: MPL-2.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = Governance Model -:toc: preamble +:author: Jonathan D.A. Jewell (hyperpolymath) +:revnumber: 2.0.0 +:revdate: 2026-09-27 +:toc: left +:toclevels: 2 +:icons: font + +[NOTE] +==== +*v2.0.0* adds two things v1 described only obliquely, and fixes one broken link. + +. A *Tri-Perimeter Contribution Framework (TPCF) ruling*. v1 said the project + might adopt TPCF later "for large, multi-repository projects". VeriSimDB is + already inside a multi-repository estate whose canon defines the framework, so + the perimeter is now stated rather than deferred — see + <<_contribution_perimeter_tpcf>>. +. A *succession and bus-factor clause*. A sole-maintainer governance model with + no stated succession plan is a single point of failure that the documentation + was quietly relying on. See <<_succession_and_bus_factor>>. + +v1's `link:CODE_OF_CONDUCT.adoc[]` pointed at a file that does not exist; the real +file is `CODE_OF_CONDUCT.adoc`. + +The v1 body is otherwise unchanged: the roles, the decision-making framework and +the 72-hour / one-week discussion windows all still describe how this repository +actually works, and those windows are confirmed below as real commitments rather +than aspirations. +==== This document describes the governance model for this repository. @@ -44,6 +71,124 @@ This repository follows a **Sole Maintainer Governance Model**: |=== +Roles and the people who hold them are listed in +link:MAINTAINERS.adoc[MAINTAINERS.adoc]. This document does not restate that +list; it describes the authority attached to the roles. + +[#_contribution_perimeter_tpcf] +== Contribution perimeter (TPCF) + +This repository is classified under the estate's +https://github.com/hyperpolymath/standards/blob/main/rhodium-standard-repositories/satellites/palimpsest-license/standards/TPCF.adoc[Tri-Perimeter +Contribution Framework] as: + +[cols="1,3"] +|=== +|Perimeter |*P3 — Community Sandbox*, with a *P1 carve-out* on named paths +|=== + +=== Why P3 + +P3 is defined as "any GitHub user can fork, PR, discuss", with use cases +"open source projects, documentation, public standards". That is a description of +this repository, not a judgement about it: it is public, it accepts fork-and-PR +contribution, and the *Open Contribution* principle above already commits to +exactly that. Classifying it otherwise would contradict the governance model the +rest of this document describes. + +The argument for P1 was considered and rejected. P1 ("Trusted Core, Closed") is +defined by *access* — 1–3 trusted maintainers with cryptographic signing keys — +and by use cases: "critical security infrastructure, cryptographic keys, +production secrets". VeriSimDB contains Coq proofs (`formal/`) and zero-knowledge +proof machinery (`verisim-semantic`, PLONK per AD-004), which makes P1 +*arguable*. But the proofs are public source under review, not signing keys, and +this repository holds no production secrets. The presence of formally verified +code raises the *cost of a bad change*; it does not change who may propose one. +Closing the perimeter would have removed the review that makes the verification +worth anything. + +=== The P1 carve-out + +Raising the cost of a bad change is still worth acting on, so three path groups +are treated as P1 *in review discipline* while remaining P3 *in access*. Anyone +may open a pull request against them; the maintainer reviews them to a higher +bar, and the automated gates on them are the ones that hard-fail rather than warn. + +[cols="2,3,2",options="header"] +|=== +|Path group |Why it is carved out |Gate + +|`.github/workflows/**`, `.github/CODEOWNERS`, `.githooks/**` +|CI is what makes every other guarantee enforceable. An unpinned or weakened +workflow silently removes the check it appears to run. Actions are SHA-pinned and +`actions.lock` is verified. +|`lock-sync-gate.yml`, `bridge-gate.yml` + +|`formal/**`, `docs/proof-debt.adoc` +|The proof core. An axiom introduced where a theorem should be does not fail a +test — it *removes* a guarantee while leaving the build green, unless the +assumptions whitelist is checked. +|`coq-build.yml` per-module `Print Assumptions` whitelists + +|Release signing and container provenance (`stapeln.toml`, `container/**`, +`selur-compose.yml`) +|Signing keys and attestation bundles are the P1 use case proper: supply-chain +trust that cannot be reconstructed after the fact. +|`ghcr-publish.yml`, stapeln `.ctp` attestation +|=== + +De-escalation is the normal direction: a carved-out path returns to plain P3 when +its gate is proven to catch the failure mode the carve-out was protecting +against. Escalation requires the maintainer to name the failure mode, as above. + +[#_succession_and_bus_factor] +== Succession and bus factor + +The bus factor of this repository is *one*. That is a fact about the project, not +a criticism of it, and governance that does not say so is governance that has not +thought about what happens next. Recorded here so the risk is visible and so the +mitigations are checkable rather than intended. + +[cols="2,4",options="header"] +|=== +|Mitigation |State + +|*Knowledge is externalised* |The design rationale is in +link:.machine_readable/6a2/META.a2ml[`META.a2ml`] (AD-001…AD-007), the +architecture is indexed in link:ARCHITECTURE.adoc[`ARCHITECTURE.adoc`], the +honest gaps are in link:KNOWN-ISSUES.adoc[`KNOWN-ISSUES.adoc`], and the trusted +base is in link:docs/proof-debt.adoc[`docs/proof-debt.adoc`]. Nothing load-bearing +is held only in one person's head. + +|*Build is reproducible without the maintainer* |Pure-Rust build with no C++ +linker (AD-003); `guix.scm` for the development environment; every gate runs in +CI from a clean checkout. + +|*Correctness does not depend on the author* |`reuse lint`, the Coq +`Print Assumptions` whitelists, `doc-consonance-gate.sh`, `doc-links-gate.sh` and +`assail-classifications-gate.sh` all fail closed and all run without maintainer +intervention. + +|*Security contact outlives the maintainer* |`.well-known/security.txt` names +GitHub private vulnerability reporting, which does not depend on any individual's +inbox. It carries an `Expires:` that arms a hard CI failure, so it cannot silently +rot. + +|*Transfer procedure* |Ownership transfer is a *Structural Decision* below: +minimum one week of discussion, recorded in `CHANGELOG.adoc` and in this document. + +|*Adding co-maintainers* |A genuine co-owner is added as a +link:CODEOWNERS-POLICY.adoc[`CODEOWNERS-POLICY.adoc`] *Rule 2* path line scoped +to them — never a catch-all self-ping. This repository's `CODEOWNERS` is +comment-only by policy, and the reason is recorded there. +|=== + +There is no named successor, because there is no second maintainer to name. The +commitment made here is narrower and real: if the maintainer becomes unable to +continue, the mitigations above are what a successor inherits, and the estate +(`hyperpolymath/standards`) is the escalation path for archiving or transferring +the repository. + == Decision Making Framework === Routine Decisions @@ -75,11 +220,36 @@ This repository follows a **Sole Maintainer Governance Model**: * Ownership transfer * Deprecation/archival -**Process**: +**Process**: . Extended discussion (minimum 1 week) . Maintainer makes final decision . Document in CHANGELOG and governance docs +[#_discussion_windows] +=== On the discussion windows + +The 72-hour and one-week minimums above are inherited from the estate governance +template, and issue #204 rightly asked whether they are real commitments here or +decorative. They are real, with one honest qualification. + +*Real:* they bind the maintainer, not contributors. A Significant Change merged +inside 72 hours of its issue being opened is a process violation even if the +change is correct, because the window exists to let someone who is not the +maintainer object while objection is still cheap. Dependency bumps and Routine +Decisions are exempt and are merged on review, which is why Dependabot traffic is +not gated behind a three-day wait. + +*The qualification:* in a sole-maintainer repository the maintainer is also the +person most likely to open the issue, so the window can degenerate into one +person waiting three days to agree with themselves. It is not worthless even +then — it is a cooling-off period during which the automated gates and any +passing contributor get a chance to object — but it is weaker here than the same +clause would be in a multi-maintainer project, and saying so is more useful than +claiming a community consultation process this repository does not have. + +An owner ruling taken inside a window shortens it, and the ruling is recorded in +the issue rather than applied silently. + == Contribution Lifecycle [cols="1,2"] @@ -111,10 +281,19 @@ In case of disagreements: This repository adheres to hyperpolymath estate-wide policies: -* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) -* **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md -* **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions +* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per + link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[standards/LICENCE-POLICY.adoc]), + recorded as AD-006 and enforced by `reuse lint` as a required CI check +* **Code of Conduct**: link:CODE_OF_CONDUCT.adoc[CODE_OF_CONDUCT.adoc], which + follows the hyperpolymath estate model including its perimeter-based + enforcement ladder +* **Security**: link:SECURITY.adoc[SECURITY.adoc], with the advisory triage log + in link:SECURITY-ADVISORIES.adoc[SECURITY-ADVISORIES.adoc] and RFC 9116 + contact details in `.well-known/security.txt` +* **Contributing**: link:CONTRIBUTING.adoc[CONTRIBUTING.adoc], following estate + conventions +* **Code ownership**: link:CODEOWNERS-POLICY.adoc[CODEOWNERS-POLICY.adoc] — + estate Rule 1 applies, so `.github/CODEOWNERS` is comment-only == Repository-Specific Conventions @@ -124,13 +303,28 @@ This repository adheres to hyperpolymath estate-wide policies: | **Signing** | All commits must be signed (SSH or GPG) -| **SPDX Headers** | All source files must have SPDX license identifiers +| **SPDX Headers** | All source files must have SPDX license identifiers, or be +covered by a `REUSE.toml` annotation. `reuse lint` is a required check and is +green at 808/808 files -| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root +| **Contractiles** | `Mustfile`, `Trustfile`, `Intentfile`, `Adjustfile`, +`Dustfile` and `Bustfile`, as `.a2ml` declarations with Nickel (`.ncl`) +evaluation under `.machine_readable/contractiles/`. See +`.machine_readable/contractiles/INDEX.a2ml`. *Not* at the repository root — an +earlier revision of this table said they were -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ +| **Machine Readable** | `.machine_readable/6a2/` holds the seven A2ML L1 specs +(`STATE`, `META`, `ECOSYSTEM`, `AGENTIC`, `PLAYBOOK`, `NEUROSYM`, +`0-AI-MANIFEST`), plus `anchors/`, `bot_directives/`, `contractiles/`, +`self-validating/` and `svc/` -| **CI/CD** | GitHub Actions workflows in .github/workflows/ +| **CI/CD** | GitHub Actions workflows in `.github/workflows/`, SHA-pinned, with +`actions.lock` verified by `lock-sync-gate.yml` + +| **Docs** | AsciiDoc for prose; every relative link must resolve +(`tests/doc-links-gate.sh`); the retired query-language misnomer for VCL is +banned from all docs (`tests/doc-consonance-gate.sh` fails the build on it). VCL +is the VeriSim *Consonance* Language |=== @@ -138,25 +332,51 @@ This repository adheres to hyperpolymath estate-wide policies: As the project grows, this governance model may evolve: -* **Adding Co-Maintainers**: When contribution volume warrants it -* **Forming a Team**: For complex multi-maintainer projects -* **Adopting TPCF**: For large, multi-repository projects (see rhodium-standard-repositories) +* **Adding Co-Maintainers**: When contribution volume warrants it. A co-owner is + added as a link:CODEOWNERS-POLICY.adoc[`CODEOWNERS-POLICY.adoc`] Rule 2 path + line scoped to *them*, never a catch-all self-ping. +* **Forming a Team**: For complex multi-maintainer projects. +* **Widening the P1 carve-out, or narrowing it**: the carve-out in + <<_contribution_perimeter_tpcf>> is a review-discipline boundary, not a fixed + list. De-escalating a path group back to plain P3 once its gate is proven is + the expected direction of travel. + +TPCF is *adopted*, not prospective: the perimeter ruling is recorded above. This +bullet previously listed "Adopting TPCF" as a future possibility, which was +superseded by v2.0.0. -Changes to this document require the same process as Significant Changes above. +Changes to this document require the same process as Significant Changes above +(<<_discussion_windows>>, including the 72-hour minimum). A change to the +perimeter ruling itself, or to the succession clause, is a *Structural Decision* +and takes the one-week window. == See Also -* link:MAINTAINERS.adoc[Maintainers] -* link:CODE_OF_CONDUCT.md[Code of Conduct] +* link:MAINTAINERS.adoc[Maintainers] — who holds the roles described here +* link:CODE_OF_CONDUCT.adoc[Code of Conduct] * link:CONTRIBUTING.adoc[Contributing Guide] -* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] -* link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] +* link:CODEOWNERS-POLICY.adoc[CODEOWNERS Policy] — this repository's conformance + record, including why `CODEOWNERS` is comment-only +* link:SECURITY.adoc[Security Policy] and + link:SECURITY-ADVISORIES.adoc[the advisory triage log] +* link:ARCHITECTURE.adoc[Architecture Index] +* link:https://github.com/hyperpolymath/standards/blob/main/0-canon/GOVERNANCE.adoc[Estate governance canon] +* link:https://github.com/hyperpolymath/standards/blob/main/rhodium-standard-repositories/satellites/palimpsest-license/standards/TPCF.adoc[Tri-Perimeter Contribution Framework] +* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate Licence Policy] == Changelog -[cols="1,1,1"] +[cols="1,1,3,1"] |=== -| Date | Change | By +| Date | Version | Change | By + +| 2026-06-07 | 1.0.0 | Initial governance model established | @hyperpolymath -| 2026-06-07 | Initial governance model established | @hyperpolymath +| 2026-09-27 | 2.0.0 | TPCF perimeter ruling added (P3 with a named P1 +carve-out on CI/pinning, the `formal/` proof core, and release signing); +succession and bus-factor clause added; the 72-hour and one-week windows +confirmed as real commitments with an honest qualification about sole-maintainer +repos; broken `CODE_OF_CONDUCT.md` link fixed; cross-references added to +`MAINTAINERS.adoc`, `CODEOWNERS-POLICY.adoc` and the architecture index. Closes +the governance item of issue #204. | @hyperpolymath |=== diff --git a/README.adoc b/README.adoc index 806a3b25..6bd40313 100644 --- a/README.adoc +++ b/README.adoc @@ -482,16 +482,16 @@ WARNING: The HTTP API has **no built-in authentication**. In development this is [source,bash] ---- -cargo test # Rust: 510+ tests +cargo test # Rust: 694 tests (437 #[test] + 257 #[tokio::test]) cd elixir-orchestration -mix test # Elixir: 160+ tests (VCL, consensus, telemetry, federation, hypatia) +mix test # Elixir: 680 tests (VCL, consensus, telemetry, federation, hypatia) ---- === CI & Coverage * `cargo-llvm-cov` (Rust) + `excoveralls` (Elixir) wired into CI, LCOV/JSON uploaded to Codecov. * `elixir-orchestration` coverage floor is currently `40` (`coveralls.json` → `coverage_options.minimum_coverage`). Actual coverage settled near 42.6 % once federation adapters grew live-service-only branches; this is a threshold mismatch, not a regression. -* Staged ramp back to `60` is documented with target dates in link:elixir-orchestration/coveralls-coverage-targets.md[`elixir-orchestration/coveralls-coverage-targets.md`] (Phase 1: 50 by 2026-07-15; Phase 2: 60 by 2026-09-01). +* Staged ramp back to `60` is documented with target dates in link:elixir-orchestration/coveralls-coverage-targets.adoc[`elixir-orchestration/coveralls-coverage-targets.md`] (Phase 1: 50 by 2026-07-15; Phase 2: 60 by 2026-09-01). === Container @@ -567,10 +567,10 @@ grpcurl -plaintext -d '{"id": "entity-001"}' \ ---- verisimdb/ -├── rust-core/ # Rust modality stores (pure Rust, no C++) +├── rust-core/ # Rust modality stores (pure Rust, no C++ linker) │ ├── verisim-graph/ # Graph (SimpleGraphStore default, Oxigraph optional) │ ├── verisim-vector/ # Vector (HNSW similarity search) -│ ├── verisim-tensor/ # Tensor (ndarray/Burn) +│ ├── verisim-tensor/ # Tensor (ndarray) │ ├── verisim-semantic/ # Semantic (CBOR proof blobs) │ ├── verisim-document/ # Document (Tantivy full-text search) │ ├── verisim-temporal/ # Temporal (version history) @@ -579,25 +579,56 @@ verisimdb/ │ ├── verisim-octad/ # Unified octad entity │ ├── verisim-drift/ # Drift detection │ ├── verisim-normalizer/ # Self-normalisation +│ ├── verisim-planner/ # Cost-based query planner +│ ├── verisim-repl/ # Interactive VCL REPL +│ ├── verisim-storage/ # Pluggable storage backend abstraction +│ ├── verisim-nif/ # Rustler NIF bridge (scaffold; see issue #61) │ ├── verisim-wal/ # Write-ahead log │ └── verisim-api/ # HTTP/gRPC/GraphQL API ├── elixir-orchestration/ # Elixir/OTP coordination layer │ ├── lib/verisim/ │ │ ├── drift/ # DriftMonitor GenServer │ │ ├── entity/ # EntityServer (per-entity GenServer) -│ │ ├── query/ # VCL parser, executor, bridge +│ │ ├── query/ # VCL bridge, executor, type checker, VCLTGate +│ │ ├── federation/ # Peer adapters (MongoDB, Redis, Neo4j, …) │ │ └── rust_client.ex # HTTP client for Rust core +│ ├── bench/ # Benchee benchmark scripts │ └── test/ -├── demos/ -│ └── drift-detection/ # Drift detection demo script +├── src/ # AffineScript + Idris2 sources +│ ├── vcl/ # VCL parser + bidirectional type checker (11 modules) +│ ├── registry/ # Federation registry + KRaft metadata log +│ └── abi/ # Idris2 ABI definitions (Foreign, Layout, Types) +├── lib/ # Auxiliary Elixir modules (planner config, query +│ # cache, circuit breaker, error recovery) +├── connectors/ +│ ├── clients/ # SDKs: rust, elixir, rescript, julia, zig +│ ├── shared/ # openapi/, proto/, json-schema/ contracts +│ └── test-infra/ # Federation adapter test stack +├── formal/ # Coq proofs (9 modules) + CROSS-REPO-MAP.adoc +├── debugger/ # In-tree crate: TUI debugger + ABI/FFI visualisation +├── ffi/zig/ # Zig FFI implementation +├── benches/ # Criterion benchmarks +├── fuzz/ # libFuzzer targets (also rust-core/fuzz/) +├── playground/ # VCL playground web UI +├── container/ # Containerfile, stapeln/svalinn config +├── demos/drift-detection/ # Drift detection demo script ├── docs/ # Specifications and design documents +│ ├── INDEX.adoc # Documentation tree index — start here +│ ├── VCL-SPEC.adoc # Normative VCL specification │ ├── vcl-grammar.ebnf # VCL formal grammar -│ ├── vcl-formal-semantics.adoc -│ └── vcl-type-system.adoc -├── registry/ # ReScript federation registry -└── .machine_readable/ # STATE.scm, META.scm, ECOSYSTEM.scm +│ ├── architecture/ # topology, abi-ffi, snifs-bridge +│ ├── decisions/ # ADR-style decision records +│ └── proof-debt.adoc # Trusted-base ledger for the Coq development +├── scripts/ # Gate and demo scripts +├── tests/ # doc-consonance, doc-links and assail gates +├── audits/ # assail-classifications.a2ml finding registry +└── .machine_readable/ # STATE.a2ml, META.a2ml, ECOSYSTEM.a2ml (+ 4 more) ---- +For the full component map, the architecture decision register (AD-001…AD-007) +and a "read this next, by question" index, see +link:ARCHITECTURE.adoc[ARCHITECTURE.adoc]. + == Use Cases === Data Quality at Scale @@ -614,15 +645,15 @@ ZKP proofs and dependent types enable tamper-evident knowledge exchange. VCL-tot == Documentation -See link:docs/INDEX.md[docs/INDEX.md] for the complete documentation tree. +See link:docs/INDEX.adoc[docs/INDEX.md] for the complete documentation tree. Quick links: -* link:ROADMAP.md[Roadmap] — criticality-ordered work plan (Phase 1–8) +* link:ROADMAP.adoc[Roadmap] — criticality-ordered work plan (Phase 1–8) * link:CHANGELOG.adoc[Changelog] — versioned history of all notable changes -* link:TESTING.md[Testing & Benchmarking Standards] — CI gates, property tests, fuzz corpus -* link:KNOWN-ISSUES.adoc[Known Issues] — honest-gaps audit (25/25 resolved) -* link:SECURITY.md[Security Policy] — threat model and disclosure process +* link:TESTING.adoc[Testing & Benchmarking Standards] — CI gates, property tests, fuzz corpus +* link:KNOWN-ISSUES.adoc[Known Issues] — honest-gaps audit (31 catalogued, 28 resolved, 3 open) +* link:SECURITY.adoc[Security Policy] — threat model and disclosure process * link:AUDIT.adoc[Audit Index] — RSR audit-trail index VCL language (file paths retain the historical `vcl-` / `VCL-` names; the in-repo file rename is a separate, tracked cleanup): @@ -637,28 +668,28 @@ VCL language (file paths retain the historical `vcl-` / `VCL-` names; the in-rep Deployment & operations: * link:docs/deployment/deployment.adoc[Deployment Guide] — Podman, selur-compose, Containerfile -* link:docs/deployment/void-setup.md[Void Linux Dev Setup] +* link:docs/deployment/void-setup.adoc[Void Linux Dev Setup] * link:docs/deployment-modes.adoc[Deployment Modes] — standalone, federated, hybrid * link:docs/safety-and-fault-tolerance.adoc[Safety & Fault Tolerance] * link:docs/drift-handling.adoc[Drift Handling] — detection, repair, federation drift Architecture & decisions: -* link:docs/architecture/topology.md[Process Topology] -* link:docs/architecture/abi-ffi.md[ABI/FFI Contract] +* link:docs/architecture/topology.adoc[Process Topology] +* link:docs/architecture/abi-ffi.adoc[ABI/FFI Contract] * link:docs/decisions/rust-spark-stance.adoc[Why Rust] (decision record) * link:docs/decisions/kraft-comparison.adoc[Why KRaft] (decision record) -* link:docs/decisions/proven-coherence.md[Proven Library Integration] +* link:docs/decisions/proven-coherence.adoc[Proven Library Integration] Papers: -* link:docs/papers/whitepaper.md[VeriSimDB Whitepaper] (Markdown source) +* link:docs/papers/whitepaper.adoc[VeriSimDB Whitepaper] (Markdown source) * link:docs/papers/whitepaper.pdf[Whitepaper PDF] * link:docs/papers/arcvix-octad-data-model.tex[ARCVIX Octad Data-Model Paper] Releases: -* link:docs/releases/v0.1.0-alpha.md[v0.1.0-alpha Release Notes] +* link:docs/releases/v0.1.0-alpha.adoc[v0.1.0-alpha Release Notes] == License @@ -666,4 +697,4 @@ MPL-2.0 == Contributing -See link:CONTRIBUTING.md[CONTRIBUTING.md] for guidelines. +See link:CONTRIBUTING.adoc[CONTRIBUTING.adoc] for guidelines. diff --git a/SECURITY-ADVISORIES.adoc b/SECURITY-ADVISORIES.adoc new file mode 100644 index 00000000..cc1c28c7 --- /dev/null +++ b/SECURITY-ADVISORIES.adoc @@ -0,0 +1,247 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Security advisories — triage log +:toc: left +:toclevels: 3 +:icons: font + +[.lead] +Triaged record of open, deferred and closed security advisories against +`hyperpolymath/verisimdb`. Updated whenever an advisory is resolved or a +deferral is re-evaluated. +Modelled on the estate register at +https://github.com/hyperpolymath/standards/blob/main/3-practice/SECURITY-ADVISORIES.adoc[`standards/3-practice/SECURITY-ADVISORIES.adoc`]. + +This file records *dispositions*, not alerts. The reporting process, threat +model, scope and safe-harbour terms are in link:SECURITY.adoc[`SECURITY.adoc`]; +the scanner findings that are not dependency advisories are tracked in issue +#203 with their registry at +link:audits/assail-classifications.a2ml[`audits/assail-classifications.a2ml`]. + +[cols="1,1"] +|=== +|Last triage |2026-09-27, against HEAD `681d635` +|Live (unresolved, unmitigated) |*0* +|Deferred with reason |*2* (one upstream blocker, both non-default features) +|Closed |*8* (1 GHSA + 5 RUSTSEC + 2 superseded) +|=== + +== Deferred (with reason) + +Both live in `deny.toml`'s `[advisories] ignore` list, which carries the same +rationale. They are recorded here because a suppression in a config file is not +a triage: the config says *what* was ignored, this says *why that is acceptable* +and *what would change the answer*. + +=== RUSTSEC-2026-0194 + RUSTSEC-2026-0195 — `quick-xml` 0.37.5 (DoS, triaged 2026-07-21, re-verified 2026-09-27) + +*Advisories:* `RUSTSEC-2026-0194` is a quadratic duplicate-attribute check; +`RUSTSEC-2026-0195` is an unbounded namespace-declaration allocation. Both are +denial-of-service on XML parsing. Both are fixed upstream in `quick-xml` 0.41.0. + +*Why it cannot be fixed here:* `quick-xml` is reached *only* through +`oxigraph 0.5.9` → `{oxrdfxml, sparesults}`. `oxigraph` 0.5.9 is the latest +published release and still requires `quick-xml ^0.37`, so *there is no +resolution of this dependency tree that avoids it*. This is not a decision to +postpone an upgrade; it is an upstream blocker with no workaround. + +*Exposure assessment:* + +[cols="1,3"] +|=== +|Build configuration |Exposed? + +|Stock build (`cargo build`) +|*No.* `verisim-graph`'s `oxigraph-backend` feature is not in `default` +(`rust-core/verisim-graph/Cargo.toml` → `default = []`), so a stock build does +not link `quick-xml` at all. The default graph backend is pure-Rust redb +(AD-003). + +|CI (`rust-ci.yml`) +|*No.* No workflow enables `oxigraph-backend`; verified by grepping every +`*.yml` for the feature name. + +|Opt-in build with `--features oxigraph-backend` +|*Yes, conditionally.* Only RDF/XML and SPARQL-XML parsing of *untrusted* input +is affected. An opt-in build parsing trusted RDF is not exposed to a DoS that +requires attacker-controlled XML. +|=== + +*Severity rationale:* DoS-only, non-default feature, no CI exposure, and the +affected parsers are not on any untrusted-input path in the default +configuration. Consistent with a deferral rather than an emergency. + +*Re-evaluate trigger:* **when `oxigraph` publishes a release requiring +`quick-xml >= 0.41`.** At that point the ignore entries must be removed and the +tree re-resolved — not left to rot. A secondary trigger: if `oxigraph-backend` +is ever promoted into `default`, this deferral becomes invalid immediately and +both advisories become live. + +*Cross-reference:* the same rationale is duplicated in `.cargo/audit.toml:22` +and `deny.toml:35`. That duplication is deliberate (two tools read two configs) +but it does mean a future re-triage has to update three places. Worth +consolidating when the deferral is next touched. + +== Closed + +=== GHSA-4w2j-m93h-cj5j — `quinn-proto`, high, remote memory exhaustion (closed 2026-09-27) + +*Advisory:* remote memory exhaustion in `quinn-proto`, the QUIC protocol +implementation behind `quinn`. Severity high. At the time of issue #203's +measurement (2026-07-28) this was the repository's *sole live High finding*, with +2 alert instances. + +*Closed by:* **removal of the dependency chain, not by a version bump.** The +path was: + +---- +burn 0.20 → cubecl-cpu → tracel-llvm-bundler (build dep) → reqwest 0.12 → quinn → quinn-proto +---- + +`burn` was the ML stack behind the tensor modality's optional backend. It was +removed from the workspace entirely in 0.2.0 ("`burn = "0.21"` removed from +workspace — unused after Tier 2 test work removed the only consumer"). + +*Verification at HEAD `681d635` (2026-09-27):* + +[cols="2,3"] +|=== +|Check |Result + +|`burn` in `Cargo.lock` +|*absent* — 0 burn crates, as `deny.toml` records + +|`quinn` / `quinn-proto` in `Cargo.lock` +|*absent* + +|`cubecl*` / `tracel-llvm-bundler` in `Cargo.lock` +|*absent* + +|`reqwest` version +|*0.13.2* — the direct-dependency bump mentioned in the old note + +|`grep -ril quinn` over the whole tree +|one hit: the stale `Cargo.toml` comment (removed by this change) +|=== + +*Residual defect found while closing this:* `Cargo.toml:126–129` still carried a +NOTE reading "Waiting for burn 0.21 stable release", directly contradicting +`deny.toml`'s "the `burn` ML stack is no longer a dependency at all". A stale +comment that contradicts an adjacent authoritative file is worse than no comment, +because it sends the next maintainer to wait for a release that will never be +needed. *Removed.* + +*Note on measurement method:* the Dependabot alerts API returns +`403 Resource not accessible by integration` for the token used to write this, so +the closure is established from the lockfile and the manifests rather than from +the alerts feed. That is stronger evidence in this case: the lockfile shows *why* +the chain is gone, whereas a cleared alert only shows that it is. + +=== Five burn-era RUSTSEC entries (closed 2026-07-21) + +`RUSTSEC-2024-0436` (`paste`), `RUSTSEC-2025-0134` (`rustls-pemfile`), +`RUSTSEC-2025-0141` (`bincode`), `RUSTSEC-2026-0002` (`lru`), +`RUSTSEC-2026-0105` (`core2`). + +*Closed by:* the same `burn` removal as above. Recorded in `deny.toml`: all five +were reported by `cargo-deny` as `advisory-not-detected`, meaning *they were +suppressing nothing* — they were dead config left over from a dependency that had +already gone. Removing them was cleanup, not a security decision. + +This is worth stating plainly because an `ignore` list that grows monotonically +is a common failure mode: entries outlive the vulnerabilities they were written +for and quietly widen the surface where a real future advisory could hide. + +=== `bincode` (closed, dependency removed) + +`Cargo.toml` records: "bincode removed — not used in codebase. Use postcard or +ciborium for future serialization needs." `RUSTSEC-2025-0141` was one of the +five above; the underlying exposure closed with the removal. + +=== `oxrocksdb-sys` C++ dependency (closed, AD-003) + +Not a CVE but a supply-chain exposure: a C++ linker requirement and a large +native attack surface in the default build. Closed by making redb the pure-Rust +default and feature-flagging Oxigraph. This is *the reason* the two deferred +`quick-xml` advisories are non-exposing in a stock build — the deferral and the +architectural decision are coupled, and promoting `oxigraph-backend` to default +would undo that coupling. + +→ `KNOWN-ISSUES.adoc` #24, AD-003 in +link:.machine_readable/6a2/META.a2ml[`.machine_readable/6a2/META.a2ml`] + +=== `protoc` build-time binary requirement (closed) + +A build-time toolchain dependency that no longer applies. +→ `KNOWN-ISSUES.adoc` #25 + +=== Two superseded suppressions in the `assail` registry + +`audits/assail-classifications.a2ml` carries 2 *Critical*-severity +`HardcodedSecret` suppressions. Issue #203 asked that these be re-read at source +rather than trusted, on the grounds that they are the only two Criticals in the +repository. *Re-read 2026-09-27; both rationales hold.* + +[cols="2,3",options="header"] +|=== +|File |Finding and verification + +|`elixir-orchestration/lib/verisim/federation/adapters/object_storage.ex` +|Lines 25–50, inside `@moduledoc`. MinIO/S3 configuration *examples*. +`minioadmin` is MinIO's published default credential and matches +`connectors/test-infra/`; the `AKIA…` string is a literal ellipsis placeholder, +not a truncated real key. No credential present. + +|`connectors/clients/elixir/lib/verisim_client/federation.ex` +|Line 21, inside `@moduledoc`. A usage example reading +`api_key: "example-peer-key-123"` — an `example-` prefixed placeholder. No +credential present. +|=== + +Both remain classified. Neither is a live secret. + +== Researcher credits + +*There are none yet.* No external researcher has reported a vulnerability to +this project, so there is nobody to credit. This section is stated explicitly +rather than omitted, because an absent acknowledgements section is ambiguous +between "nobody has helped" and "we forgot to record it", and the second reading +is the one that discourages the first reporter. + +`SECURITY.adoc` commits to crediting reporters in the published advisory and in +release notes unless they prefer anonymity. When the first advisory is published, +the reporter is credited here and in +`SECURITY.adoc`'s Hall of Fame. Note that `SECURITY.adoc` currently links its +Hall of Fame to a `SECURITY-ACKNOWLEDGMENTS.md` that does not exist; until that +file is written, this section is the acknowledgements record. + +== How this register is maintained + +* An advisory is *Closed* only when the exposure is gone, and the entry names + *what* removed it — a version bump, a feature flag, or a dependency deletion. + "The alert cleared" is not a closure reason. +* An advisory is *Deferred* only with a named upstream blocker and an explicit + *re-evaluate trigger*. A deferral without a trigger is an ignore entry. +* Severity is recorded as upstream assigns it; *exposure* is assessed separately + and may be materially lower. Both are stated, because collapsing them is how a + high-severity non-exposed finding gets treated as an emergency and a + low-severity exposed one gets ignored. +* The `deny.toml` `[advisories]` block warns that a local `cargo deny` run + against an unpopulated advisory database reports "advisories ok" having checked + *nothing*. CI clones a fresh database every run and is the authority. Any + triage recorded here should be reproducible from CI, not from a local run. +* `cargo-deny`'s detection is sensitive to feature resolution: default features + do *not* surface the `quick-xml` advisories above, while `--all-features` and + the CI container both do. Triage against the stricter resolution. + +== See also + +* link:SECURITY.adoc[`SECURITY.adoc`] — reporting, threat model, scope, safe + harbour, response timeline +* link:audits/assail-classifications.a2ml[`audits/assail-classifications.a2ml`] — + the panic-attack finding registry, with per-finding audit trails +* link:deny.toml[`deny.toml`] — advisory, licence, ban and source policy +* `.github/workflows/security-scan.yml` — the weekly `panic-attack` scan +* `.github/workflows/secret-scanner.yml`, `.github/workflows/codeql.yml`, + `.github/workflows/scorecard.yml` — the other supply-chain gates +* Issue #203 — the panic-attack category sweep this register complements diff --git a/SECURITY.adoc b/SECURITY.adoc index aaebc241..377050f0 100644 --- a/SECURITY.adoc +++ b/SECURITY.adoc @@ -300,9 +300,20 @@ We believe in recognising security researchers who help us improve. ==== Hall of Fame -Researchers who report valid vulnerabilities will be acknowledged in our -link:SECURITY-ACKNOWLEDGMENTS.md[Security Acknowledgments] (unless they -prefer anonymity). +Researchers who report valid vulnerabilities will be acknowledged in the +researcher-credits section of +link:SECURITY-ADVISORIES.adoc[SECURITY-ADVISORIES.adoc] (unless they prefer +anonymity). + +[NOTE] +==== +This section previously pointed at a `SECURITY-ACKNOWLEDGMENTS.md` that was never +written. The advisory triage log is the acknowledgements record now, so there is +one place to update rather than two. As of 2026-09-27 there are no external +researcher credits: nobody has reported a vulnerability to this project. That is +stated explicitly rather than left implied, because an empty acknowledgements +file is indistinguishable from a forgotten one. +==== Recognition includes: @@ -343,7 +354,7 @@ To stay informed about security updates: * *GitHub Security Advisories*: Published at https://github.com/hyperpolymath/verisimdb/security/advisories[Security Advisories] -* *Release notes*: Security fixes noted in link:CHANGELOG.md[CHANGELOG] +* *Release notes*: Security fixes noted in link:CHANGELOG.adoc[CHANGELOG] ==== Update Policy @@ -394,8 +405,8 @@ When using VeriSimDB, we recommend: * https://github.com/hyperpolymath/verisimdb/security/advisories[Security Advisories] -* link:CHANGELOG.md[Changelog] -* link:CONTRIBUTING.md[Contributing Guidelines] +* link:CHANGELOG.adoc[Changelog] +* link:CONTRIBUTING.adoc[Contributing Guidelines] * https://cve.mitre.org/[CVE Database] * https://www.first.org/cvss/calculator/3.1[CVSS Calculator] @@ -414,7 +425,7 @@ via GitHub] or j.d.a.jewell@open.ac.uk |https://github.com/hyperpolymath/verisimdb/discussions[GitHub Discussions] -|*Other enquiries* |See link:README.md[README] for contact information +|*Other enquiries* |See link:README.adoc[README] for contact information |=== ''''' diff --git a/ULTRAPLAN-2026-09-27.adoc b/ULTRAPLAN-2026-09-27.adoc new file mode 100644 index 00000000..4bc28d24 --- /dev/null +++ b/ULTRAPLAN-2026-09-27.adoc @@ -0,0 +1,759 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += ULTRAPLAN 2026-09-27 — the seven open issues, re-measured, and what actually gets done +Jonathan D.A. Jewell +v1.0.0, 2026-09-27 +:toc: left +:toclevels: 2 +:icons: font + +[NOTE] +==== +Status: *parts 1–6 executed on branch `arena/01a0e211-verisimdb`*; part 8 is the +ranked forward plan for work that this sandbox cannot verify. Every number below +was measured on 2026-09-27 against HEAD `681d635` with the commands in +<>, and re-measured after the edits landed — the post-edit +figures are in <>. Where this document contradicts an issue +body, the issue body is the stale artefact and the measurement is authoritative +— the reason is in <>. + +*Execution outcome, 2026-09-27.* All documentation and gate work landed and is +verified by gates that ran here. One code change +(`elixir-orchestration/lib/verisim/query/vclt_gate.ex`, part 4) is *written but +not compiled* — no Elixir toolchain is installable in this environment, and the +blocker is recorded in part 8 rather than worked around. Issue #79's +test-expansion scope stopped at re-measurement for the same reason; #86 landed +as a design document with a scope verdict, not as code. +==== + +== 0. TL;DR + +* Seven issues are open: *#204, #203, #113, #86, #84, #79, #78*. They were + measured on four different dates between 2026-06-01 and 2026-08-24. The + repository has moved substantially since every one of those dates. +* *The single most important finding is that most of the blocking work in #113 + and #203 is already done on `main`, and nobody closed the issues.* Of #113's + five REUSE items, all five are resolved (`reuse lint` is green at *800/800*). + Of #203's three P1 items, all three are resolved. Of #203's P2 items, the + `flake.nix` supply-chain finding is gone *and* `guix.scm` now exists — the + packaging-policy contradiction resolved itself in the opposite direction to the + one #203 predicted. +* *#204 is the only issue that is still substantially open*, and it is the only + one that is fully actionable without a Rust/Elixir/Coq toolchain. Six of its + eight files are still missing. Those six are landed by this plan. +* *A defect class no issue tracks:* the documentation tree has *66 broken + relative links*, of which 43 are `.md`→`.adoc` renames that were never + propagated. `README.adoc` still carries the `.machine_readable/` + `STATE.scm`/`META.scm` filename bug that #113 filed against + `.claude/CLAUDE.md` (CLAUDE.md was fixed; README and `AUDIT.adoc` were not). + `README.adoc` advertises "honest-gaps audit (25/25 resolved)" while + `KNOWN-ISSUES.adoc` carries *31* items, *3 of them OPEN*. This plan adds a + fail-closed link gate so the class cannot recur silently. +* *Owner rulings obtained 2026-09-27* unblock all four of #204's + decision-gated files: TPCF perimeter *P3 with a P1 carve-out*; `security.txt` + `Expires: 2027-09-27T00:00:00Z` with the GitHub private-advisory contact; + `ai.txt` on a *plain MPL-2.0 / CC-BY-SA-4.0 stance* following `standards`' own + live file rather than the MIT+Palimpsest template. +* *Hard constraint:* this sandbox has network egress only to `pypi.org`, + `github.com` and `api.github.com`. `static.crates.io`, `forge.rust-lang.org`, + `hex.pm`, `erlang.org`, `opam.ocaml.org` and `deb.debian.org` are all + unreachable and the shell is unprivileged, so *no Rust, Elixir or Coq + toolchain can be installed*. #79, #78, #86 and the Coq half of #113 are + therefore specified, re-measured and ranked — not guessed at. Shipping + uncompiled Rust into a repo whose `main` gate has 21 required checks would be + a regression dressed as progress. + +[#sec-recon] +== 1. State of the house (census, 2026-09-27) + +[cols="3,2,4",options="header"] +|=== +|Measure |Value |Note + +|HEAD +|`681d635` +|`chore(deps): bump exqlite from 0.40.0 to 0.41.0 (#288)` + +|Tracked files +|807 +|`git ls-files \| wc -l` + +|REUSE compliance +|*800 / 800 green* +|`reuse lint` (REUSE 6.2.0); 7 files excluded by `.gitignore`/`.reuse` + +|Open issues +|7 +|#204 #203 #113 #86 #84 #79 #78 + +|`doc-consonance-gate.sh` +|PASS +|no `VeriSim Query Language` misnomer in docs + +|`assail-classifications-gate.sh` +|PASS +|12 file/category keys resolve + positive control fires + +|Broken relative links in `*.adoc` +|*66* +|43 auto-fixable extension swaps, 23 genuinely absent targets + +|Rust tests +|694 +|437 `#[test]` + 257 `#[tokio::test]` + +|Criterion benches +|28 +|*down* from the 30 #79 recorded + +|`proptest!` blocks +|5 +|unchanged since #79; target was 60 + +|libFuzzer targets +|4 +|up from 3 + +|Elixir tests +|680 +|up from the 615 #79 recorded + +|Insta snapshots +|3 +|unchanged +|=== + +[#sec-drift] +== 2. Issue-by-issue re-measurement + +The discipline #204 itself demands — *"part of why this needed re-measuring +rather than trusting the issue text"* — applied to all seven. + +=== #204 — docs: the 8 files (OPEN, 6 still missing) + +[cols="3,2,4",options="header"] +|=== +|File |Status at HEAD |Note + +|`ARCHITECTURE.adoc` +|❌ absent +|Landed by this plan (part 3.1) + +|`FAQ.adoc` +|❌ absent +|Landed (part 3.2). `docs/business/pr/faq.adoc` already exists — root file is a +harvest/index, not a second 500-line FAQ + +|`SECURITY-ADVISORIES.adoc` +|❌ absent +|Landed (part 3.3) + +|`.well-known/humans.txt` +|❌ absent +|Landed (part 3.4). *Correction to #204:* there is no root `.well-known/`; the +existing `void.rdf`/`void.ttl` live at `docs/.well-known/` and +`www/.well-known/`. The estate gate tests the *repo root*, so root it is + +|`GOVERNANCE.adoc` +|⚠️ exists (v1, 2026-06-07) +|Amended to v2 (part 3.5): TPCF perimeter + succession clause added + +|`CODEOWNERS-POLICY.adoc` +|✅ *done* +|Present, and `.github/CODEOWNERS` was actually fixed to a comment-only header + +|`.well-known/security.txt` +|❌ absent +|Landed (part 3.4) + +|`.well-known/ai.txt` +|❌ absent +|Landed (part 3.4) +|=== + +#204's claim that `.well-known/` "already exists" is *wrong at the path the gate +checks*. `governance-reusable.yml` lines 1110–1146 test `-f ".well-known/security.txt"` +at the repository root. Before this change that test found nothing and the job +emitted two `::warning::` lines and passed. After it, the `Expires:` branch arms. +That is by design and is documented inline in the file. + +=== #203 — security: panic-attack sweep (3/3 P1 items already resolved) + +[cols="3,2,4",options="header"] +|=== +|Finding |#203 said |Measured at HEAD + +|`CommandInjection` ×2 +|P1, "needs someone to actually look" +|✅ *Resolved and classified.* `vcl_bridge.ex:282` uses +`Port.open({:spawn_executable, runtime}, [args: [script]])` — an argv vector, no +shell. `vclt_gate.ex:108` used `sh -c` with `shell_quote`; hardened this plan to +remove the shell *and* the temp file entirely (part 4.1). Both already carry +registry entries at `assail-classifications.a2ml:65–71` + +|`PathTraversal` ×1 +|"Genuine and trivially fixable" +|✅ *Already fixed.* `scripts/two-node-test.sh:18` reads +`WORK_DIR=$(mktemp -d "${TMPDIR:-/tmp}/verisimdb-two-node.XXXXXX")` with a +`trap cleanup EXIT`. No hardcoded path remains + +|`DynamicCodeExecution` ×1 +|"Fine if compile-time constants" +|✅ *Classification, not a fix.* `postgresql.ex:347` is +`postgrex_mod = Module.concat([Postgrex])` — a literal — and both `apply/3` +calls pass the literal atoms `:start_link` / `:query`. Nothing is reachable from +federation config. Registry entry at line 75 + +|`SupplyChain` ×1 +|"`flake.nix` declares inputs with no narHash" +|✅ *Gone.* No `flake.nix` and no `flake.lock` in the tree; `guix.scm` exists. +#203 flagged that this repo "has never had a `guix.scm`" — it has one now + +|The sole live High +|`quinn-proto` GHSA-4w2j-m93h-cj5j +|✅ *Resolved by dependency removal.* `burn` left the workspace entirely +(CHANGELOG 0.2.0; `deny.toml` records "0 burn crates in Cargo.lock"). No `quinn`, +`quinn-proto`, `cubecl` or `tracel-llvm-bundler` in `Cargo.lock`; `reqwest` is +0.13.2. The advisory chain no longer exists. *But* `Cargo.toml:126–129` still +carries a NOTE saying "Waiting for burn 0.21 stable release" — stale and +self-contradictory with `deny.toml`. Fixed in part 4.2 + +|Recurrence guard +|"Add a check that every `(file …)` key resolves" +|✅ *Already built and wired.* `scripts/validate-assail-classifications.sh` +(existence + traversal + duplicate-key checks) and +`tests/assail-classifications-gate.sh` (planted-mutant positive control), run by +`.github/workflows/dogfood-gate.yml:61` + +|`ProofDrift` ×5 +|Coq axioms + Julia type-only tests +|⏸ *Open.* Coq half is toolchain-blocked. Julia half confirmed: 29 bare +`isa` assertions in `connectors/clients/julia/test/runtests.jl`, unclaimed + +|`HardcodedSecret` ×2 +|"Re-read the rationales" +|✅ *Re-read at source; both rationales hold.* See part 4.3 + +|`MutationGap` 49 + `InsecureProtocol` 29 +|"Sample a dozen of each" +|⏸ *Open.* Scanner-blocked: `panic-attack` is not installable here. A blanket +disposition *policy* is recorded in part 4.4 rather than 74 invented rationales + +|"`vclt_gate.ex` is called from nowhere in production" +|open question +|❌ *Stale and false.* `vcl_executor.ex:801` calls `VCLTGate.check/1` inside +`execute_string/2`. Corrected on the issue +|=== + +=== #113 — checkpoint 2026-06-05 (all five REUSE items closed) + +[cols="2,4",options="header"] +|=== +|Item |Status at HEAD + +|P1 `LICENSES/MPL-2.0.txt` + `CC-BY-SA-4.0.txt` +|✅ Both present. `reuse lint` green 800/800 + +|P2 json-schema `$comment` SPDX +|✅ Fixed by a `precedence = "override"` block at the end of `REUSE.toml` + +|P3 `playground/package.json` AGPL-3.0 +|✅ No AGPL anywhere; `reuse lint` reports used licences = CC-BY-SA-4.0, MPL-2.0 + +|P4 SPDX headers on ~12 docs +|✅ 800/800 files carry copyright and licence info + +|P5 `docs/security-lessons.lgt` double-stamp +|✅ Covered by the `**/*.lgt` aggregate in `REUSE.toml` + +|Coq proof-debt (Q1 axiom + refinement link) +|⏸ *Open, toolchain-blocked.* `formal/` holds 9 modules and `coq-build.yml`'s +per-module assumptions whitelist is intact. Cannot run `coqc` here + +|`STATE.a2ml` `overall-completion 0` +|✅ Fixed — reads `0.78`, with a proof-status block calibrated to +`Print Assumptions` and an explicit pointer to #113 + +|`.claude/CLAUDE.md` says `.scm` +|✅ Fixed in CLAUDE.md — *but the same bug survives in two other files.* +`README.adoc:598` and `AUDIT.adoc` both still say +`STATE.scm, META.scm, ECOSYSTEM.scm`. Fixed in part 5.2 + +|`machine_readable` gap-fill +|⚠️ Partial. `anchors/`, `bot_directives/`, `contractiles/` (incl. `dust/`), +`self-validating/` and `svc/` all now exist; the k9→self-validating rename is +done. `ai/`, `agent_instructions/`, `compliance/`, `configs/`, `policies/`, +`scripts/` do not + +|Drop throwaway `TEST_CI_VERIFY` +|❌ *Not done — renamed instead.* `TEST_CI_VERIFY.adoc` is at the root, still +reading "Delete after verification", and its licence header is malformed: both +header lines start with `==`, which AsciiDoc parses as level-2 *section headings* +rather than comments, so the file never carried a valid in-file header at all and +was compliant only via the `REUSE.toml` aggregate. Deleted in part 5.1. Quoting +the malformed header verbatim is itself a trap — it breaks `reuse lint` in the +quoting document unless wrapped in `REUSE-Ignore`, which part 5.1 demonstrates + +|Supersede PR #107 / drop redundant branches +|⏸ Cannot assess: the clone is shallow (`git rev-parse --is-shallow-repository` +→ `true`) with a single visible commit, and the agent token cannot write issues +|=== + +=== #86, #84 — cross-language bridge and cross-repo synthesis + +*#86:* `docs/architecture/snifs-bridge.adoc` still does not exist; the only +references to SNIFs are three prose mentions in `connectors/README.adoc:59`, +`connectors/clients/zig/README.adoc:13` and `docs/INDEX.adoc:254`. Step 1 of the +issue is an owner decision (Option A vs B) that has not been taken, and steps +2–5 need `wasm32-*` targets that cannot be installed here. *Landed:* the design +doc, with the Option A/B trade-off stated and a spike plan (part 6). + +*#84:* the VQL→VCL rename is *further along than the issue records*. `src/vql/` +no longer exists — it is `src/vcl/`, and the 11 modules are `.affine` +(AffineScript), not `.res` (ReScript). So the issue's "11 ReScript modules in +`src/vql/` named `VQL*.res` (4,974 LOC)" describes a tree that is gone. +88 files still match `vql` case-insensitively, against 200 matching `vcl`: +the residue is `vql-bridge/`, `rust-core/verisim-api/src/vql.rs`, +`verisim-planner/src/vql_bridge.rs`, `verisim-repl/src/vql_fmt.rs` and the +user-facing route `/api/v1/vql/execute`. `formal/CROSS-REPO-MAP.adoc` (12,984 +bytes) already exists and carries the synthesis. + +*Consequence for `docs/VCL-SPEC.adoc`:* its "Implementation Files" table still +lists `src/vql/VQLParser.res` (1154 lines), `src/vql/VQLTypes.res`, +`src/vql/VQLBidir.res`, `src/vql/VQLError.res`, `src/vql/VQLExplain.res` — +five paths that do not exist. Fixed in part 5.3. + +=== #79, #78 — test expansion and DB-theory gaps + +#79's *density* table is remarkably durable; its *headline* counts are not. + +[cols="3,1,1,1,3",options="header"] +|=== +|Crate |#79 tests/kLOC |Measured |#79 LOC |Measured LOC + +|verisim-spatial |42.3 |*42.3* |— |922 +|verisim-provenance |32.2 |*32.2* |— |963 +|verisim-repl |— |25.5 |— |2,624 +|verisim-temporal |— |22.8 |— |967 +|verisim-storage |— |22.2 |— |1,851 +|verisim-document |— |20.8 |— |385 +|verisim-wal |— |19.6 |— |1,985 +|verisim-planner |17.6 |18.1 |6,888 |7,060 +|verisim-semantic |16.3 |*16.3* |3,308 |3,316 +|verisim-normalizer |15.2 |*15.2* |3,891 |3,890 +|verisim-octad |— |15.0 |— |4,469 +|verisim-graph |12.1 |*12.1* |— |1,236 +|verisim-tensor |12.1 |*12.1* |— |494 +|verisim-vector |9.9 |*9.9* |— |1,215 +|verisim-drift |8.8 |8.9 |— |1,241 +|verisim-api |5.9 |6.9 |8,969 |*12,254* +|verisim-nif |0 |*0* |204 |135 +|=== + +Six of the densities match to the decimal. Two facts changed materially: + +* *`verisim-api` grew 37%* (8,969 → 12,254 LOC) while its density rose only + 5.9 → 6.9. It remains the largest and worst-served crate by absolute gap, and + now more so than when #79 was filed. +* *Criterion benches went backwards*, 30 → 28, in a period where every other + count rose. #79's bench target (30 → 90) is now 28 → 90. + +The priority order #79 gives is therefore *confirmed, not stale*: `verisim-nif` +(0 tests / 135 LOC) and `verisim-api` (6.9 / 12,254) are still the two +worst-served, and `verisim-spatial` + `verisim-provenance` are still the +templates to copy. + +#78 is a research gap-analysis, not a defect list. Its five "fastest wins" are +all code changes in crates that cannot be compiled here, so they are ranked in +part 5 of the forward plan against #79's rather than started blind. + +== 3. What this plan lands — #204 (all six missing files) + +. *`ARCHITECTURE.adoc`* — an index, per #204's explicit instruction ("not a + re-telling"). Points at `docs/architecture/abi-ffi.adoc`, + `docs/architecture/topology.adoc`, `docs/vcl-architecture.adoc`, + `docs/VCL-SPEC.adoc`, the deployment/drift/normalisation docs, and + `formal/CROSS-REPO-MAP.adoc`. Transcribes *AD-001…AD-007* from + `.machine_readable/6a2/META.a2ml` as a table and cites the a2ml as canonical. + Note #204 gives the extension as `abi-ffi.md`; the file is `.adoc` — the + issue text is itself a victim of the rename drift this plan fixes. +. *`FAQ.adoc`* — harvested, not re-answered. Each answer carries a `link:` to + its existing canonical source (`EXPLAINME.adoc`, README "How It Compares", + `docs/vcl-vs-sql.adoc`, `KNOWN-ISSUES.adoc`, `docs/business/pr/faq.adoc`). + Where a source is itself stale, the FAQ states the *current* behaviour and + names the stale doc — it does not launder the drift. +. *`SECURITY-ADVISORIES.adoc`* — modelled on + `standards/3-practice/SECURITY-ADVISORIES.adoc`: Closed / Deferred-with-reason + sections, per-advisory exposure assessment, explicit re-evaluate trigger. + Records the `quinn-proto` chain as *Closed by dependency removal* with the + evidence. States plainly that there are no researcher credits yet, as #204 + instructs, rather than omitting the section. +. *`.well-known/{humans.txt, security.txt, ai.txt}`* — at the *repository root*, + which is the path the estate gate tests. `security.txt` carries + `Expires: 2027-09-27T00:00:00Z` and an inline comment explaining that the + eventual red is by design. `ai.txt` follows `standards`' own live + `www/.well-known/ai.txt` (identical licence shape: MPL-2.0 code, CC-BY-SA-4.0 + prose), *not* the `templates/.well-known/ai.txt.template` whose + `License: MIT AND Palimpsest-0.8` would contradict META.a2ml AD-006. +. *`GOVERNANCE.adoc` v2* — amended, not rewritten: adds the TPCF perimeter + ruling (*P3 Community Sandbox*, with a *P1 carve-out* for signing and + proof-core paths), a succession/bus-factor clause, and a reference to the + existing `MAINTAINERS.adoc` rather than a restatement of it. The 72h / 1-week + windows are kept and explicitly confirmed as real commitments. +. *`docs/INDEX.adoc`* — updated to list the three new root documents, since an + index that omits them is the defect #204 was filed about. + +== 4. What this plan lands — #203 + +. *`vclt_gate.ex`: remove the shell.* Replaces + `System.cmd("sh", ["-c", "#{quoted_path} < #{quoted_tmp}"])` with + `System.cmd(path, [], input: payload)`. This deletes the last `sh -c` on the + VCL execution path, and with it `write_secure_payload!/2`, `shell_quote/1`, + the temp-file lifecycle and its `File.rm` — roughly 45 lines of + security-sensitive machinery that existed only to work around a shell + redirection. `:input` is available in Elixir ~> 1.17, which `mix.exs:11` + requires. *Flagged as needing Elixir CI verification* — see part 7. +. *`Cargo.toml`: delete the stale `quinn-proto` NOTE* (lines 126–129). It tells + the next maintainer to wait for `burn` 0.21 when `burn` is no longer a + dependency at all and `deny.toml` says so. A stale comment that contradicts an + adjacent authoritative file is worse than no comment. +. *`HardcodedSecret` ×2 re-read at source*, as #203 asks rather than trusting + the suppression. Both rationales hold: `object_storage.ex`'s `minioadmin` is + MinIO's published default and matches `connectors/test-infra/`; the `AKIA…` + string is a literal ellipsis placeholder in an `@moduledoc`. + `federation.ex`'s `example-peer-key-123` is an `example-` prefixed + placeholder in a usage example. No live credential. *Both remain Critical-severity + suppressions and both remain correct.* +. *Bulk disposition policy for `MutationGap` 49 + `InsecureProtocol` 29.* Not + 74 invented rationales. `MutationGap` is a *test-quality* signal, not a + vulnerability: it belongs to #79's cargo-mutants campaign and is recorded as + such. `InsecureProtocol` needs the scanner's own output to disposition + honestly, and `panic-attack` cannot be installed here. Both are handed to the + forward plan with the reason stated. + +== 5. What this plan lands — doc integrity (no issue tracks this) + +. *Delete `TEST_CI_VERIFY.adoc`* — the last item of #113 that is unambiguously + actionable. It says "Delete after verification" and was renamed `.md`→`.adoc` + instead of deleted. Its licence header is malformed, and quoting that + malformed header here breaks `reuse lint` unless the quotation is wrapped — so + the wrap below is not decoration, it is the same `REUSE-Ignore` technique #113 + prescribed for double-stamped code examples: ++ +// REUSE-IgnoreStart +[source] +---- +== SPDX-License-Identifier: MPL-2.0 +== Copyright (c) Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk +---- +// REUSE-IgnoreEnd ++ +Those are AsciiDoc *level-2 headings*, not comments, so the file never carried a +valid header and was only compliant via the `REUSE.toml` `**/*.adoc` aggregate. +. *A fail-closed relative-link gate*: `scripts/check-doc-links.sh` plus + `tests/doc-links-gate.sh` as its planted-mutant positive control, wired into + `doc-consonance.yml`. Modelled on the existing + `assail-classifications-gate.sh` pattern so it is idiomatic for this repo. +. *Fix the 43 `.md`→`.adoc` extension swaps* across `README.adoc`, + `AUDIT.adoc`, `EXPLAINME.adoc`, `GOVERNANCE.adoc`, `SECURITY.adoc`, + `connectors/README.adoc`, `docs/INDEX.adoc` and the `docs/challenges-*` and + `docs/vcl-*` families. +. *Fix the factual drift*, each one verified against its authoritative source: + * `README.adoc:598` + `AUDIT.adoc`: `STATE.scm, META.scm, ECOSYSTEM.scm` → + the real `.a2ml` filenames (#113's bug, surviving in two more files). + * `README.adoc:624`: "honest-gaps audit (25/25 resolved)" → 31 catalogued, + 28 resolved, 3 open. The old text was an *overclaim in the honesty document*. + * `AUDIT.adoc`: "As of 2026-05-25 all 25 catalogued issues are resolved" → + same correction. + * `docs/vcl-vs-sql.adoc:11`: "a 6-core multimodal database" → eight + modalities. The 2026-07-07 CHANGELOG entry claims this file was corrected; + the opening line was missed. + * `docs/vcl-vs-sql.adoc`: the "VCL is read-only / no mutations / no GROUP BY / + no ORDER BY" claims. `docs/VCL-SPEC.adoc:2783–2789` already lists these as + known inconsistencies and resolves them "in favour of the implemented grammar + and source code" — the spec recorded the defect and nobody propagated it. + * `docs/VCL-SPEC.adoc` implementation-files table: the five `src/vql/*.res` + paths → the real `src/vcl/*.affine` paths. + * `.machine_readable/6a2/README.adoc`: "6 core A2ML files" → 7, adding the + omitted `0-AI-MANIFEST.a2ml`; and the `standards/tree/main/a2ml` link, which + moved to `1-formats/a2ml` in the estate reorganisation. + * `docs/INDEX.adoc`: drop the `v-api-gateway/` (V-language API gateway) row — + no such directory exists. +. *Triage the 23 genuinely-absent link targets* individually: fix the ones with + a real target elsewhere (`WHITEPAPER.md`→`WHITEPAPER.pdf`, + `adaptive_learner.ex`→`../../lib/verisim/adaptive_learner.ex`, + `kraft-comparison.adoc`'s doubled `docs/` prefix), and convert the ones with no + target into plain text or an explicit "not yet written" marker rather than a + link that 404s. Cross-repo links to `typeql-experimental` and `typell` become + absolute GitHub URLs, which resolve whether or not the sibling is cloned. + +== 6. What this plan lands — #86 + +`docs/architecture/snifs-bridge.adoc`: the design doc step 6 of the issue asks +for. States the Option A / Option B trade-off with a recommendation and the +reason, draws the API-surface boundary the issue calls architectural +(OctadStore, DriftCalculator, Normalizer through WASM; planner/optimizer and +async federation native), and gives a costed spike plan. It does *not* pretend +to be an implementation — the owner decision at step 1 has not been taken and no +`wasm32-*` target can be installed here. + +[[sec-verify]] +== 7. Verification actually performed + +Every claim of correctness in parts 3–6 is backed by a gate that ran in this +sandbox: + +[cols="3,2,4",options="header"] +|=== +|Gate |Result |Command + +|REUSE 3.3 compliance +|*809 / 809 green* (was 810 before `TEST_CI_VERIFY.adoc` was deleted; +808 when part 7 was first drafted) +|`reuse lint` (REUSE 6.2.0, installed from PyPI) + +|Doc consonance +|PASS +|`bash tests/doc-consonance-gate.sh` + +|Assail classification registry +|PASS, 12 file/category keys resolve + positive control fires +|`bash tests/assail-classifications-gate.sh` + +|Relative-link integrity +|*PASS — 364 links resolve across 101 documents, 0 exempt* +|`bash scripts/check-doc-links.sh` (new) + +|Relative-link positive control +|PASS, 4/4 assertions +|`bash tests/doc-links-gate.sh` (new) + +|A2ML validation +|*32 / 32 files, 0 errors, 0 warnings* (the one pre-existing warning — +`6a2/0-AI-MANIFEST.a2ml` missing an SPDX header — was fixed, not suppressed) +|`INPUT_PATH=.machine_readable bash .githooks/validate-a2ml.sh` + +|Shell syntax +|PASS +|`bash -n` on every touched `.sh` + +|Workflow YAML validity +|*inspected, not machine-validated* — no `yaml` module is importable in this +environment and PyPI is blocked, so `yaml.safe_load` could not be run. +`doc-consonance.yml` was checked by hand for tabs and indentation, and adds no +new action, so `.github/workflows/actions.lock` needs no change. CI is the first +real parser of this file. +|n/a + +|Elixir compile / `mix test` / `mix format --check-formatted` +|*NOT RUN — no toolchain* +|`vclt_gate.ex` and its test are unverified; see the risk note below + +|`cargo test` / `cargo build` / `cargo clippy` +|*NOT RUN — no toolchain* +|no Rust source change is made by this plan; `Cargo.toml` and `debugger/Cargo.toml` +comment/metadata edits are not compiled here + +|`coqc` / `Print Assumptions` +|*NOT RUN — no toolchain* +|no `formal/*.v` change is made by this plan +|=== + +Two self-inflicted regressions were caught by the gates during execution and are +worth recording, because both are the same failure mode — *writing a literal +marker into prose makes a text-level gate believe the prose is data*: + +. Quoting an SPDX tag inside `ULTRAPLAN-2026-09-27.adoc` prose made `reuse lint` +parse it as a declaration. Fixed by describing the tag without spelling it, and +by wrapping the illustrative malformed-header listing in +`REUSE-IgnoreStart`/`REUSE-IgnoreEnd`. +. Writing the literal `link:` macro form with square brackets inside the +`CHANGELOG.adoc` entry *describing* the doc-links gate made that gate report a +broken link in the file announcing it. Fixed by naming the macro without the +bracket. The gate was right to fail; it had been in place for about four minutes. + +[WARNING] +==== +*The one unverified code change.* `elixir-orchestration/lib/verisim/query/vclt_gate.ex` +is edited without an Elixir compiler available. The change is small and the API +is documented (`System.cmd/3` `:input` since Elixir 1.13; `mix.exs` requires +`~> 1.17`), and `elixir-orchestration/test/verisim/query/vclt_gate_test.exs` +already exercises the admit / reject / gate-failed protocol, so CI will settle +it immediately. It is called out here rather than buried, and it is the only +file in this plan whose correctness rests on documentation rather than on a gate +that ran. If you would rather not carry an uncompiled change, revert that one +file and the rest of the plan stands on its own — the `CommandInjection` +finding is already classified either way. +==== + +== 8. Forward plan — ranked, with the blocker named + +Work this plan deliberately does *not* do, in the order it should be picked up. +Each row names the thing that actually blocks it, because "needs a toolchain" and +"needs an owner ruling" have very different next actions. + +[cols="1,3,2,3",options="header"] +|=== +|# |Work |Blocker |Why this rank + +|1 +|*Discharge the Q1 `optimize_is_permutation` axiom* (`formal/Planner.v`, +`formal/PlannerSemantic.v`) +|`coqc` + `opam` +|#113 and #203 both name it; #84 says tropical-resource-typing closes Q1 "for +free" via `Tropical_Kleene.thy::floyd_warshall`, and #203 says it is +dischargeable via `Coq.Sorting.Mergesort`'s axiom-free `Permuted_sort`. Two +independent routes to the same axiom. It is the only *crux* axiom left + +|2 +|*Coq-model ↔ Rust-impl refinement link* +|`coqc` + judgement +|#113's second owed item and the deeper of the two: without it the proofs are +"structural over uninterpreted operations", which `STATE.a2ml` already states +honestly. This is what turns 9 compiled modules into evidence about *this* +binary + +|3 +|*`verisim-nif`: 0 tests / 135 LOC* +|`cargo` +|#79's worst density, unchanged since filing, and it is the FFI surface — the +place a defect crosses a language boundary. Small crate, so ~100 tests is +tractable in one pass + +|4 +|*`verisim-api`: 6.9 tests/kLOC over 12,254 LOC* +|`cargo` +|Largest crate, grew 37% since #79, 0 integration files, 0 proptests. #79's +item 6 (`http_contract_tests.rs`, table-driven across ~30 handlers) is the +highest-leverage single file in the repo + +|5 +|*VCL Pratt-precedence differential tests* +|`cargo` + node +|#79's items 1–3 (`prop_and_left_associative`, +`prop_or_lower_precedence_than_and`, `prop_not_unary_binds_tighter_than_and`) +plus the Rust↔AffineScript differential. Three parsers in lockstep is a +divergence waiting to happen, and the ReScript→AffineScript migration is recent +enough that nobody has differential-tested across it + +|6 +|*Criterion benches 28 → 90, with p99* +|`cargo` +|The only metric that went *backwards*. #79 notes the existing benches report +mean throughput only; `sample_size(500)` plus p99 is the difference between a +number and a regression gate + +|7 +|*Julia `runtests.jl`: 29 type-only assertions* +|`julia` +|#203's unclaimed `ProofDrift` half. `@test x isa Y` passes on a wrong value. +Mechanical to fix, and it is the only ProofDrift finding not blocked on Coq + +|8 +|*`MutationGap` 49 — cargo-mutants campaign* +|`cargo` + `panic-attack` +|#79 already specifies the three adversarial scenarios (drift near-threshold +`τ ± ε`, RBAC path matcher, normalizer schedule determinism). Promote +`cargo mutants --in-diff origin/main` to a required check afterwards + +|9 +|*`InsecureProtocol` 29 — blanket disposition* +|`panic-attack` +|Needs the scanner's own JSON. #203 is right that this is one decision, not 29 +threads — but the decision needs the findings in front of it + +|10 +|*SNIFs bridge: Option A vs B ruling, then the spike* +|*owner ruling* +|#86 step 1. Unblockable in one reply. The design doc landed by this plan states +the trade-off so the ruling is informed rather than cold + +|11 +|*Bitemporal `Version`* (#78 fastest win 1) +|`cargo` + judgement +|SQL:2011 alignment, "hours of work, decades of literature". Ranked below the +test work because #78's own framing is that these are *missing features*, while +items 3–6 are *unverified existing code* — and `KNOWN-ISSUES` #31 shows +`at_time` already returns partial data, which bitemporal modelling would have to +confront anyway + +|12 +|*`machine_readable` gap-fill* (`ai/`, `agent_instructions/`, `compliance/`, +`configs/`, `policies/`, `scripts/`) +|judgement +|#113's last open structural item. Five of the eleven directories it named now +exist. Gap-filling to "estate-canonical" needs the estate's current canonical +shape, which was reorganised (`0-canon`/`1-formats`/`2-protocols`/`3-practice`) +after #113 was filed + +|13 +|*Remaining VQL→VCL call-sites* (88 files) +|`cargo` + node + judgement +|#84's staged rename. The parser layer is done; what remains is +`verisim-api/src/vql.rs`, the `/api/v1/vql/execute` route (user-facing, so it +needs a deprecation window, not a rename), and `vql-bridge/`. `doc-consonance-gate.sh` +deliberately scopes these out so the gate stays green meanwhile — that design is +correct and should be preserved +|=== + +[#app-a] +[appendix] +== Appendix A — measurement commands + +[source,bash] +---- +# Census +git rev-parse HEAD; git ls-files | wc -l +git rev-parse --is-shallow-repository # -> true + +# REUSE (installed from PyPI; system pip is PEP-668 blocked) +python3 -m venv /tmp/reuseenv +/tmp/reuseenv/bin/pip install "reuse[charset-normalizer]" +/tmp/reuseenv/bin/reuse lint # -> 800/800, compliant with 3.3 + +# Repo gates +bash tests/doc-consonance-gate.sh # -> PASS +bash tests/assail-classifications-gate.sh # -> PASS + positive control +bash scripts/validate-assail-classifications.sh + +# Broken relative links (66 before the fix; see part 5) +# python3 walk over **/*.adoc, extract the AsciiDoc link macro targets with a +# regex, resolve each relative to its own file's directory, and skip +# http/mailto/fragment-only targets. Now a permanent gate: +bash scripts/check-doc-links.sh +bash tests/doc-links-gate.sh + +# #79 re-measurement +git grep -c '#\[test\]' -- '*.rs' # 437 +git grep -c '#\[tokio::test\]' -- '*.rs' # 257 +git grep -c '#\[cfg(test)\]' -- '*.rs' # 75 +git grep -c 'bench_function' -- '*.rs' # 28 +git grep -c 'proptest!' -- '*.rs' # 5 +git grep -c 'prop_assert' -- '*.rs' # 46 +git grep -cE '^\s*test ' -- '*.exs' # 680 +find . -name '*.snap' -not -path './.git/*' | wc -l # 3 + +# Toolchain reachability (all 000 = blocked) +for h in static.crates.io forge.rust-lang.org hex.pm erlang.org \ + opam.ocaml.org deb.debian.org objects.githubusercontent.com; do + curl -sS -o /dev/null -w "%{http_code}\n" "https://$h/" +done +---- + +== Appendix B — estate sources consulted + +* `hyperpolymath/standards` → `3-practice/SECURITY-ADVISORIES.adoc` (the + Closed / Deferred-with-reason model), `0-canon/GOVERNANCE.adoc` v2.0.0, + `PALIMPSEST.adoc`, `ULTRAPLAN-2026-09-24.adoc` (house format), + `www/.well-known/{ai.txt,humans.txt}`, + `rhodium-standard-repositories/.well-known/security.txt`, + `rhodium-standard-repositories/satellites/palimpsest-license/standards/TPCF.adoc` + (perimeter definitions), + `rhodium-standard-repositories/templates/.well-known/ai.txt.template` (the + template *not* copied), `.github/workflows/governance-reusable.yml` (the + `wellknown` job, lines 1091–1155), `scripts/check-docs-presence.sh`. +* The Dependabot alerts API returns `403 Resource not accessible by integration` + for this token, so advisory status is taken from `Cargo.lock`, `Cargo.toml`, + `deny.toml` and `CHANGELOG.adoc` — which is stronger evidence than the alerts + feed anyway, because it shows *why* the chain is gone rather than just that + the alert cleared. diff --git a/connectors/README.adoc b/connectors/README.adoc index b0169018..dd5150da 100644 --- a/connectors/README.adoc +++ b/connectors/README.adoc @@ -301,7 +301,7 @@ across REST, gRPC, and SDK code generation. == Related Documentation * link:../README.adoc[VeriSimDB README] -- project overview and quick start -* link:../WHITEPAPER.md[Whitepaper] -- formal description of the octad model +* link:../WHITEPAPER.pdf[Whitepaper] -- formal description of the octad model * link:../docs/[docs/] -- design documents and architecture decisions * link:../rust-core/verisim-api/src/federation.rs[federation.rs] -- Rust federation implementation * link:../rust-core/verisim-octad/src/lib.rs[octad lib.rs] -- canonical Octad type definitions diff --git a/debugger/Cargo.toml b/debugger/Cargo.toml index f41e0690..824b0ea8 100644 --- a/debugger/Cargo.toml +++ b/debugger/Cargo.toml @@ -7,7 +7,12 @@ edition = "2024" authors = ["Jonathan D.A. Jewell "] license = "MPL-2.0" description = "Interactive debugger and visualization tool for VeriSimDB" -repository = "https://github.com/hyperpolymath/verisimdb-debugger" +# This crate lives in-tree at `debugger/` inside the verisimdb repository. The +# previous value pointed at `hyperpolymath/verisimdb-debugger`, which does not +# exist (HTTP 404, verified 2026-09-27) — a crate publishing with an unreachable +# `repository` URL sends every reader somewhere that is not there. +repository = "https://github.com/hyperpolymath/verisimdb" +homepage = "https://github.com/hyperpolymath/verisimdb/tree/main/debugger" keywords = ["database", "debugger", "tui", "multimodal", "zkp"] categories = ["command-line-utilities", "development-tools::debugging"] diff --git a/debugger/docs/CITATIONS.adoc b/debugger/docs/CITATIONS.adoc index 37fdb0f0..50017c97 100644 --- a/debugger/docs/CITATIONS.adoc +++ b/debugger/docs/CITATIONS.adoc @@ -1,36 +1,81 @@ -= RSR-template-repo - Citation Guide -:toc: +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += verisimdb-debugger — Citation Guide +:toc: left +:toclevels: 2 + +[NOTE] +==== +This file was generated unmodified from the RSR template and cited +`RSR-template-repo` under the placeholder author "Polymath, Hyper". It has been +corrected to cite this crate. Name, version, author, licence and description are +taken from `debugger/Cargo.toml`. + +The debugger is an *in-tree crate* at `debugger/` inside the `verisimdb` +repository. `debugger/Cargo.toml` previously declared +`repository = "https://github.com/hyperpolymath/verisimdb-debugger"`, which +returns *404* — no such repository exists. That field has been corrected to point +at this repository, since a crate that publishes with an unreachable `repository` +URL sends every reader somewhere that does not exist. +==== == BibTeX [source,bibtex] ---- -@software{rsr-template-repo_2025, - author = {Polymath, Hyper}, - title = {RSR-template-repo}, - year = {2025}, - url = {https://github.com/hyperpolymath/RSR-template-repo}, - license = {MPL-2.0} +@software{verisimdb_debugger_2026, + author = {Jewell, Jonathan D. A.}, + title = {verisimdb-debugger: Interactive Debugger and Visualization + Tool for VeriSimDB}, + year = {2026}, + version = {0.1.0}, + url = {https://github.com/hyperpolymath/verisimdb/tree/main/debugger}, + license = {MPL-2.0}, + note = {In-tree crate of the VeriSimDB repository. TUI debugger and + ABI/FFI visualisation for the octad modality stores.} } ---- +Cite the *parent* system as +link:../../docs/CITATIONS.adoc[`docs/CITATIONS.adoc`] describes; cite this crate +only when the debugger itself is the subject. + == Harvard Style -Polymath, H. (2025) _RSR-template-repo_ [Computer software]. Available at: https://github.com/hyperpolymath/RSR-template-repo +Jewell, J.D.A. (2026) _verisimdb-debugger: Interactive Debugger and Visualization +Tool for VeriSimDB_ (version 0.1.0) [Computer software]. Available at: +https://github.com/hyperpolymath/verisimdb/tree/main/debugger == OSCOLA -Hyper Polymath, 'RSR-template-repo' (2025) +Jonathan D.A. Jewell, 'verisimdb-debugger' (2026) + == MLA -Polymath, Hyper. "RSR-template-repo." 2025, github.com/hyperpolymath/RSR-template-repo. +Jewell, Jonathan D.A. _verisimdb-debugger: Interactive Debugger and Visualization +Tool for VeriSimDB_. Version 0.1.0, 2026, +github.com/hyperpolymath/verisimdb/tree/main/debugger. == APA 7 -Polymath, H. (2025). _RSR-template-repo_ [Computer software]. GitHub. https://github.com/hyperpolymath/RSR-template-repo +Jewell, J. D. A. (2026). _verisimdb-debugger: Interactive debugger and +visualization tool for VeriSimDB_ (Version 0.1.0) [Computer software]. GitHub. +https://github.com/hyperpolymath/verisimdb/tree/main/debugger + +== Machine-readable citation metadata + +*Not present.* This section previously linked to `../CITATION.cff` and +`../codemeta.json`; neither file exists at the repository root or in `debugger/`. + +If citation metadata is added, it belongs at the *repository* root, not here, so +that the parent system and this crate share one record. See +link:../../docs/CITATIONS.adoc[`docs/CITATIONS.adoc`] for the parent citation and +for the `CITATION.cff` / `codemeta.json` rationale. -== See Also +== Licence of this document -* link:../CITATION.cff[CITATION.cff] -* link:../codemeta.json[codemeta.json] +CC-BY-SA-4.0, per the estate policy that prose carries CC-BY-SA-4.0 and code +carries MPL-2.0 (AD-006 in +link:../../.machine_readable/6a2/META.a2ml[`.machine_readable/6a2/META.a2ml`]). +The *crate* being cited is MPL-2.0. diff --git a/docs/CITATIONS.adoc b/docs/CITATIONS.adoc index 37fdb0f0..7496b85a 100644 --- a/docs/CITATIONS.adoc +++ b/docs/CITATIONS.adoc @@ -1,36 +1,114 @@ -= RSR-template-repo - Citation Guide -:toc: +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += VeriSimDB — Citation Guide +:toc: left +:toclevels: 2 + +[NOTE] +==== +This file was generated unmodified from the RSR template and cited +`RSR-template-repo` under the placeholder author "Polymath, Hyper". It has been +corrected to cite this project. Author, title, licence and URL are taken from +`Cargo.toml` (`authors`, `license`, `homepage`), `MAINTAINERS.adoc` and the +per-file SPDX headers; the version and date are from `CHANGELOG.adoc`. + +If you are citing a *specific* release, substitute its version and date from +link:../CHANGELOG.adoc[CHANGELOG.adoc] for the `0.2.0` / 2026 used below. The +`main` branch moves, so a citation to it should carry a commit SHA or an access +date. +==== == BibTeX [source,bibtex] ---- -@software{rsr-template-repo_2025, - author = {Polymath, Hyper}, - title = {RSR-template-repo}, - year = {2025}, - url = {https://github.com/hyperpolymath/RSR-template-repo}, - license = {MPL-2.0} +@software{verisimdb_2026, + author = {Jewell, Jonathan D. A.}, + title = {VeriSimDB: The Veridical Simulacrum Database}, + year = {2026}, + version = {0.2.0}, + url = {https://github.com/hyperpolymath/verisimdb}, + license = {MPL-2.0}, + note = {A federated identity-consonance engine: each entity is + maintained across up to eight modal witnesses (the octad) with + continuous cross-modal drift detection and self-normalisation. + Documentation licensed CC-BY-SA-4.0.} } ---- +If you are citing the *formal development* rather than the software, the Coq +modules under `formal/` are the artefact, and +link:proof-debt.adoc[`docs/proof-debt.adoc`] states the strength of each result — +including which are closed, which are closed only modulo standard primitives, +which are structural over uninterpreted operations, and which rest on an axiom. +Citing the proofs without that distinction would overstate them. + == Harvard Style -Polymath, H. (2025) _RSR-template-repo_ [Computer software]. Available at: https://github.com/hyperpolymath/RSR-template-repo +Jewell, J.D.A. (2026) _VeriSimDB: The Veridical Simulacrum Database_ (version +0.2.0) [Computer software]. Available at: +https://github.com/hyperpolymath/verisimdb == OSCOLA -Hyper Polymath, 'RSR-template-repo' (2025) +Jonathan D.A. Jewell, 'VeriSimDB: The Veridical Simulacrum Database' (2026) + == MLA -Polymath, Hyper. "RSR-template-repo." 2025, github.com/hyperpolymath/RSR-template-repo. +Jewell, Jonathan D.A. _VeriSimDB: The Veridical Simulacrum Database_. Version +0.2.0, 2026, github.com/hyperpolymath/verisimdb. == APA 7 -Polymath, H. (2025). _RSR-template-repo_ [Computer software]. GitHub. https://github.com/hyperpolymath/RSR-template-repo +Jewell, J. D. A. (2026). _VeriSimDB: The Veridical Simulacrum Database_ (Version +0.2.0) [Computer software]. GitHub. https://github.com/hyperpolymath/verisimdb + +== Related artefacts worth citing separately + +[cols="2,3"] +|=== +|Artefact |Cite when + +|link:papers/whitepaper.adoc[`docs/papers/whitepaper.adoc`] (also +`WHITEPAPER.pdf` at the repository root) |you are citing the design argument +rather than the implementation + +|link:papers/arcvix-octad-data-model.tex[`docs/papers/arcvix-octad-data-model.tex`] +|you are citing the octad data model specifically + +|link:papers/references.bib[`docs/papers/references.bib`] |you need the prior +work this system builds on (Codd, Stonebraker, Malkov & Yashunin for HNSW, +Shapiro et al. for CRDTs, Pierce for the type theory) + +|link:../formal/CROSS-REPO-MAP.adoc[`formal/CROSS-REPO-MAP.adoc`] |you are +citing the cross-repository proof obligations shared with `vcl-ut`, +`echo-types`, `tropical-resource-typing` and `kategoria` + +|link:VCL-SPEC.adoc[`docs/VCL-SPEC.adoc`] |you are citing the VeriSim +Consonance Language itself +|=== + +== Machine-readable citation metadata + +*Not present.* This section previously linked to `CITATION.cff` and +`codemeta.json` at the repository root; neither file was ever written, and a link +to a file that does not exist is worse than a statement that it does not. + +Both are worth adding, and both are mechanical once the metadata above is agreed: + +* https://citation-file-format.github.io/[`CITATION.cff`] — read by GitHub, which + renders a "Cite this repository" button. +* https://codemeta.github.io/[`codemeta.json`] — the CodeMeta crosswalk, read by + Zenodo and other archives. + +They should be generated from the same facts as this file, not written +independently, or the two will drift apart in the way this file drifted from the +project it described. Until they exist, cite from this document. -== See Also +== Licence of this document -* link:../CITATION.cff[CITATION.cff] -* link:../codemeta.json[codemeta.json] +CC-BY-SA-4.0, per the estate policy that prose carries CC-BY-SA-4.0 and code +carries MPL-2.0 (AD-006 in +link:../.machine_readable/6a2/META.a2ml[`.machine_readable/6a2/META.a2ml`]). Note +that the *software* being cited is MPL-2.0; this citation guide is not. diff --git a/docs/INDEX.adoc b/docs/INDEX.adoc index 804a4aa1..8d2036f0 100644 --- a/docs/INDEX.adoc +++ b/docs/INDEX.adoc @@ -1,7 +1,7 @@ == VeriSimDB Documentation Index ____ -Last updated: 2026-05-25. This file is the table of contents for +Last updated: 2026-09-27. This file is the table of contents for everything under `+docs/+` and the top-level project documents. ____ @@ -16,13 +16,13 @@ readers, plus the artefacts the RSR template requires. |link:../README.adoc[README.adoc] |Project entry point — what VeriSimDB is, how to install/run, where to look next -|link:../ROADMAP.md[ROADMAP.md] |Criticality-ordered work plan (Phase +|link:../ROADMAP.adoc[ROADMAP.adoc] |Criticality-ordered work plan (Phase 1–8) |link:../CHANGELOG.adoc[CHANGELOG.adoc] |Versioned history of all notable changes -|link:../TESTING.md[TESTING.md] |Testing & benchmarking standards (hard +|link:../TESTING.adoc[TESTING.adoc] |Testing & benchmarking standards (hard CI gates per language, property-test patterns, fuzz corpus location) |link:../KNOWN-ISSUES.adoc[KNOWN-ISSUES.adoc] |Honest-gaps audit trail — @@ -31,15 +31,15 @@ all 25 catalogued issues with resolution status |link:../AUDIT.adoc[AUDIT.adoc] |RSR audit-index pointing to KNOWN-ISSUES, TESTING, SECURITY, CHANGELOG -|link:../SECURITY.md[SECURITY.md] |Threat model, disclosure process, +|link:../SECURITY.adoc[SECURITY.adoc] |Threat model, disclosure process, supported versions -|link:../CONTRIBUTING.md[CONTRIBUTING.md] |How to propose changes, run +|link:../CONTRIBUTING.adoc[CONTRIBUTING.adoc] |How to propose changes, run gates locally |link:../MAINTAINERS.adoc[MAINTAINERS.adoc] |Active maintainers -|link:../CODE_OF_CONDUCT.md[CODE_OF_CONDUCT.md] |Community standards +|link:../CODE_OF_CONDUCT.adoc[CODE_OF_CONDUCT.adoc] |Community standards |link:../LICENSE[LICENSE] |MPL-2.0 @@ -47,16 +47,44 @@ gates locally project |link:../justfile[justfile] |Task definitions for the `+just+` runner + +|link:../EXPLAINME.adoc[EXPLAINME.adoc] |*Orientation — read this first.* The +conceptual model: consonance subjects, modal witnesses, the identity lifecycle + +|link:../ARCHITECTURE.adoc[ARCHITECTURE.adoc] |Architecture *index*: component +map, the AD-001…AD-007 decision register, and "read this next, by question" + +|link:../FAQ.adoc[FAQ.adoc] |Short answers with pointers to the long ones; +harvested, not re-answered + +|link:../GOVERNANCE.adoc[GOVERNANCE.adoc] |Governance model, TPCF contribution +perimeter, succession and bus factor + +|link:../MAINTAINERS.adoc[MAINTAINERS.adoc] |Who holds the roles GOVERNANCE +describes + +|link:../CODEOWNERS-POLICY.adoc[CODEOWNERS-POLICY.adoc] |This repo's CODEOWNERS +conformance record, and why `.github/CODEOWNERS` is comment-only + +|link:../SECURITY-ADVISORIES.adoc[SECURITY-ADVISORIES.adoc] |Advisory triage log: +open / deferred-with-reason / closed, with re-evaluate triggers + +|link:../ULTRAPLAN-2026-09-27.adoc[ULTRAPLAN-2026-09-27.adoc] |Dated working +plan with its measurement evidence — the house convention for a census plus a +ranked forward plan |=== === docs/ tree ==== Architecture -* link:architecture/abi-ffi.md[docs/architecture/abi-ffi.md] — ABI/FFI -contract for cross-language calls (Rust ↔ Elixir ↔ Idris2) -* link:architecture/topology.md[docs/architecture/topology.md] — Process +* link:architecture/topology.adoc[docs/architecture/topology.adoc] — Process topology and deployment shapes +* link:architecture/abi-ffi.adoc[docs/architecture/abi-ffi.adoc] — ABI/FFI +contract for cross-language calls (Rust ↔ Elixir ↔ Idris2 ↔ Zig) +* link:architecture/snifs-bridge.adoc[docs/architecture/snifs-bridge.adoc] — +SNIFs WASM bridge: the single cross-language boundary for BEAM-side access, with +the scope analysis that decides what may cross it (issue #86) ==== Decisions (ADR-style) @@ -64,31 +92,31 @@ topology and deployment shapes — Why Rust over alternatives for the core * link:decisions/kraft-comparison.adoc[docs/decisions/kraft-comparison.adoc] — Why KRaft for the consensus layer -* link:decisions/proven-coherence.md[docs/decisions/proven-coherence.md] +* link:decisions/proven-coherence.adoc[docs/decisions/proven-coherence.md] — Notes on the proven library integration ==== Deployment * link:deployment/deployment.adoc[docs/deployment/deployment.adoc] — Full deployment guide (Podman, selur-compose, Containerfile) -* link:deployment/void-setup.md[docs/deployment/void-setup.md] — Void +* link:deployment/void-setup.adoc[docs/deployment/void-setup.md] — Void Linux dev environment setup ==== Status & implementation tracking -* link:status/planner.md[docs/status/planner.md] — verisim-planner +* link:status/planner.adoc[docs/status/planner.md] — verisim-planner implementation status * link:status/implementation-plan.adoc[docs/status/implementation-plan.adoc] — Original timeline-based execution plan (V1–V5) ==== Releases -* link:releases/v0.1.0-alpha.md[docs/releases/v0.1.0-alpha.md] — +* link:releases/v0.1.0-alpha.adoc[docs/releases/v0.1.0-alpha.md] — Narrative release announcement for v0.1.0-alpha (2026-02-04) ==== Papers & whitepaper -* link:papers/whitepaper.md[docs/papers/whitepaper.md] — VeriSimDB +* link:papers/whitepaper.adoc[docs/papers/whitepaper.md] — VeriSimDB whitepaper (Markdown source) * link:papers/whitepaper.pdf[docs/papers/whitepaper.pdf] — Whitepaper PDF artefact @@ -121,10 +149,10 @@ materials ==== Design notes (dated, point-in-time) -* link:design/DESIGN-2026-02-27-level-data-model.md[docs/design/DESIGN-2026-02-27-level-data-model.md] +* link:design/DESIGN-2026-02-27-level-data-model.adoc[docs/design/DESIGN-2026-02-27-level-data-model.md] * link:design/DESIGN-2026-02-27-strategic-improvements.adoc[docs/design/DESIGN-2026-02-27-strategic-improvements.adoc] * link:design/DESIGN-2026-02-27-vcl-dt-assessment.adoc[docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc] -* link:design/DESIGN-2026-02-28-panll-interop-telemetry.md[docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md] +* link:design/DESIGN-2026-02-28-panll-interop-telemetry.adoc[docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md] ==== VCL language @@ -209,9 +237,24 @@ the project Under link:../.machine_readable/[`+.machine_readable/+`]: -* `+STATE.scm+` — current project state and progress -* `+META.scm+` — architecture decisions and development practices -* `+ECOSYSTEM.scm+` — position in the ecosystem and related projects +These are A2ML (`.a2ml`) artefacts, not Scheme (`.scm`) ones — an earlier +revision of this index named three `.scm` files that have never existed here. +Seven L1 specs live under `+6a2/+`: + +* `+6a2/STATE.a2ml+` — current project state, component status, proof status +* `+6a2/META.a2ml+` — architecture decisions (AD-001…AD-007), development +practices, design rationale. *Canonical for the decision register*, which +link:../ARCHITECTURE.adoc[ARCHITECTURE.adoc] transcribes +* `+6a2/ECOSYSTEM.a2ml+` — position in the ecosystem and related projects +* `+6a2/AGENTIC.a2ml+` — AI-agent operational gating and safety controls +* `+6a2/PLAYBOOK.a2ml+` — executable plans and operational runbooks +* `+6a2/NEUROSYM.a2ml+` — symbolic semantics and composition algebra +* `+6a2/0-AI-MANIFEST.a2ml+` — AI manifest + +Alongside `+6a2/+`: `+anchors/+` (estate exception anchors), `+bot_directives/+` +(per-bot policy, including cross-thread quarantine), `+contractiles/+` +(Nickel-evaluated Mustfile / Trustfile / Intentfile / Adjustfile / Dustfile / +Bustfile), `+self-validating/+` and `+svc/+`, plus `+ENSAID_CONFIG.a2ml+`. === Workflow & CI @@ -257,8 +300,6 @@ Erlang) access via the SNIFs WASM bridge — see `+hyperpolymath/snifs+`. |`+ffi/zig/+` |Zig |Zig FFI -|`+v-api-gateway/+` |V |V-language API gateway - |`+fuzz/+`, `+rust-core/fuzz/+` |Rust |Fuzz harnesses (libFuzzer via cargo-fuzz) diff --git a/docs/VCL-SPEC.adoc b/docs/VCL-SPEC.adoc index dad77eb8..c1ae976c 100644 --- a/docs/VCL-SPEC.adoc +++ b/docs/VCL-SPEC.adoc @@ -118,11 +118,11 @@ Both modes use the same parser and produce the same AST. They diverge at the **q └───────────────────┬──────────────────────────────┘ │ ┌─────▼──────┐ - │ Parser │ (ReScript / Elixir fallback) + │ Parser │ (AffineScript / Elixir fallback) └─────┬──────┘ │ AST ┌─────▼──────┐ - │ Type Check │ (VQLBidir.res) + │ Type Check │ (VCLBidir.affine) └─────┬──────┘ │ ┌──────────┴──────────┐ @@ -152,7 +152,7 @@ Both modes use the same parser and produce the same AST. They diverge at the **q ---- `[.implemented]` Parser, basic type checking, query routing, store dispatch. + -`[.partial]` Bidirectional type inference (implemented in ReScript, not wired to runtime Lean checker). + +`[.partial]` Bidirectional type inference (implemented in AffineScript, not wired to runtime Lean checker). + `[.planned]` ZKP proof generation via `proven-library` / `sanctify`. === Conformance Levels @@ -422,7 +422,7 @@ VCL's type system operates over these primitive types: [cols="1,2,2"] |=== -| Type | Description | ReScript Representation +| Type | Description | AffineScript Representation | `Int` | Arbitrary-precision integer @@ -514,7 +514,7 @@ In slipstream mode, the type checker validates: 3. **Operator compatibility** — Comparison operators match operand types 4. **Aggregate validity** — Aggregate functions operate on appropriate types (e.g., `SUM` requires numeric) -.ReScript type representation +.AffineScript type representation [source,rescript] ---- type rec vclType = @@ -531,7 +531,7 @@ type rec vclType = | NeverType ---- -`[.implemented]` All simple type checking in `VQLBidir.res`. +`[.implemented]` All simple type checking in `VCLBidir.affine`. === Dependent Types (VCL-DT Path) @@ -607,7 +607,7 @@ The subtyping relation stem:[\tau_1 <: \tau_2] governs when a value of type stem \end{aligned} ++++ -`[.implemented]` Structural subtyping in `VQLBidir.res`. +`[.implemented]` Structural subtyping in `VCLBidir.affine`. === Type Inference (Bidirectional) @@ -616,7 +616,7 @@ VCL uses **bidirectional type checking** with two modes: * **Synthesis** (stem:[\Gamma \vdash e \Rightarrow \tau]) — Infer the type of an expression from its structure. * **Checking** (stem:[\Gamma \vdash e \Leftarrow \tau]) — Verify that an expression has an expected type. -The `synthesizeQuery` function in `VQLBidir.res` walks the query AST through nine phases: +The `synthesizeQuery` function in `VCLBidir.affine` walks the query AST through nine phases: 1. Resolve modalities from SELECT clause 2. Check source (HEXAD/FEDERATION/STORE) typing @@ -639,7 +639,7 @@ The `synthesizeQuery` function in `VQLBidir.res` walks the query AST through nin \frac{\Gamma \vdash q : \text{Query}[M] \quad \Gamma \vdash p : \text{ProofSpec}[\phi]}{\Gamma \vdash q\ \text{PROOF}\ p \Rightarrow \Sigma r : \text{QueryResult}[M]. \text{Proof}[\phi(r)]} \quad \text{(T-ProvedQuery)} ++++ -`[.implemented]` Bidirectional type inference in `VQLBidir.res` (841 lines, 9-phase pipeline). +`[.implemented]` Bidirectional type inference in `VCLBidir.affine` (841 lines, 9-phase pipeline). === Refinement Types @@ -1622,17 +1622,17 @@ Certificates are independently verifiable — any party with the verification ke The execution pipeline flows through three layers: -1. **ReScript Core** — Parsing, type checking, query plan generation +1. **AffineScript Core** — Parsing, type checking, query plan generation 2. **Elixir Orchestrator** — Query routing, federation fan-out, drift handling 3. **Rust Modality Stores** — Per-modality query execution .Execution pipeline ---- VCL String - → Parser (ReScript VQLParser.res / Elixir vcl_bridge.ex fallback) + → Parser (AffineScript VCLParser.affine / Elixir vcl_bridge.ex fallback) → AST - → Type Checker (VQLBidir.res) - → Query Plan Generator (VQLExplain.res) + → Type Checker (VCLBidir.affine) + → Query Plan Generator (VCLExplain.affine) → Condition Classifier (pushdown vs cross-modal) → Elixir QueryRouter GenServer → Route to stores by modality: @@ -1712,7 +1712,7 @@ Optimization hints: - VECTOR + DOCUMENT queries can execute in parallel ---- -.Per-modality base costs (from VQLExplain.res) +.Per-modality base costs (from VCLExplain.affine) [cols="1,1"] |=== | Modality | Base Cost @@ -1842,7 +1842,7 @@ VCL provides structured error responses with error codes, messages, and recovery | Suspicious inconsistencies suggesting Byzantine behaviour |=== -`[.implemented]` All error types defined in `VQLError.res` (447 lines). Structured JSON error responses. +`[.implemented]` All error types defined in `VCLError.affine` (447 lines). Structured JSON error responses. // ============================================================================ @@ -1859,7 +1859,7 @@ This section provides an honest assessment of what is implemented, partially imp |=== | Feature | Version | Notes -| VCL Parser (ReScript) +| VCL Parser (AffineScript) | 2.0 | 1154 lines, monadic parser combinators. Handles all grammar productions. @@ -1869,19 +1869,19 @@ This section provides an honest assessment of what is implemented, partially imp | Bidirectional Type Checker | 2.0 -| `VQLBidir.res` (841 lines). 9-phase pipeline. Cross-modal checking, mutation checking. +| `VCLBidir.affine` (841 lines). 9-phase pipeline. Cross-modal checking, mutation checking. | Type System | 2.0 -| `VQLTypes.res` (296 lines). Pi types, Sigma types, proof types, structural equality. +| `VCLTypes.affine` (296 lines). Pi types, Sigma types, proof types, structural equality. | Error System | 2.0 -| `VQLError.res` (447 lines). 5 error categories, 40+ error kinds, JSON serialization. +| `VCLError.affine` (447 lines). 5 error categories, 40+ error kinds, JSON serialization. | EXPLAIN Plans | 2.0 -| `VQLExplain.res` (427 lines). Per-modality cost estimation, performance hints. +| `VCLExplain.affine` (427 lines). Per-modality cost estimation, performance hints. | Query Executor | 2.0 @@ -1943,7 +1943,7 @@ This section provides an honest assessment of what is implemented, partially imp | Cross-modal write atomicity | INSERT/UPDATE/DELETE execute but atomic cross-modal writes (all modalities or none) are not guaranteed. -| VCL Bridge (Elixir ↔ ReScript) +| VCL Bridge (Elixir ↔ AffineScript) | Port-based communication works. Falls back to built-in Elixir parser when Deno/Node unavailable. |=== @@ -2736,7 +2736,7 @@ This specification is the authoritative reference for VCL language behaviour. Th | 63 comprehensive examples covering all VCL constructs, both execution paths, error cases, and advanced use cases. 1078 lines. | link:vcl-architecture.adoc[`vcl-architecture.adoc`] -| Dual-path routing architecture, ReScript/Elixir/Rust stack, metadata storage, audit trail, drift detection, API endpoint, performance comparison. 708 lines. +| Dual-path routing architecture, AffineScript/Elixir/Rust stack, metadata storage, audit trail, drift detection, API endpoint, performance comparison. 708 lines. | link:vcl-vs-vcl-dt.adoc[`vcl-vs-vcl-dt.adoc`] | Detailed comparison of Slipstream vs VCL-DT execution paths, six proof types, performance implications, honest implementation status. 282 lines. @@ -2751,42 +2751,73 @@ This specification is the authoritative reference for VCL language behaviour. Th |=== | File | Role -| `src/vql/VQLParser.res` -| ReScript parser (1154 lines). Monadic combinator library + grammar. +| `src/vcl/VCLParser.affine` +| AffineScript parser (1201 lines). Monadic combinator library + grammar, +including the three mutation parsers. -| `src/vql/VQLTypes.res` -| Core type definitions (296 lines). Modality, primitive, VCL, and proof types. +| `src/vcl/VCLTypes.affine` +| Core type definitions (311 lines). Modality, primitive, VCL, and proof types. -| `src/vql/VQLBidir.res` -| Bidirectional type inference engine (841 lines). 9-phase synthesis pipeline. +| `src/vcl/VCLBidir.affine` +| Bidirectional type inference engine (858 lines). 9-phase synthesis pipeline, +including `synthesizeMutation`. -| `src/vql/VQLError.res` -| Structured error types (447 lines). 5 categories, 40+ error kinds. +| `src/vcl/VCLError.affine` +| Structured error types (464 lines). 5 categories, 40+ error kinds. -| `src/vql/VQLExplain.res` -| EXPLAIN plan generation (427 lines). Cost estimation and hints. +| `src/vcl/VCLExplain.affine` +| EXPLAIN plan generation (442 lines). Cost estimation and hints. + +| `src/vcl/VCLTypeChecker.affine` +| Type-checker entry points and mode selection (407 lines). + +| `src/vcl/VCLSubtyping.affine` +| Structural subtyping relations (253 lines). + +| `src/vcl/VCLContext.affine` +| Typing context: bindings, modality scope, proof environment (253 lines). + +| `src/vcl/VCLProofObligation.affine` +| Proof-obligation generation for `PROOF`-carrying statements (257 lines). + +| `src/vcl/VCLCircuit.affine` +| Circuit-breaker hooks on the query path (77 lines). + +| `src/vcl/VCLParser_test.affine` +| Parser test suite, co-located with the module (564 lines). | `elixir-orchestration/lib/verisim/query/query_router.ex` -| Elixir query router GenServer (187 lines). Routes by modality. +| Elixir query router GenServer (189 lines). Routes by modality. | `elixir-orchestration/lib/verisim/query/vcl_bridge.ex` -| Elixir ↔ ReScript bridge (672 lines). Built-in fallback parser. +| Elixir ↔ AffineScript bridge (801 lines). Built-in fallback parser. | `elixir-orchestration/lib/verisim/query/vcl_executor.ex` -| Full VCL executor (1162 lines). Parse → type check → plan → route → aggregate. +| Full VCL executor (2310 lines). Parse → type check → plan → route → aggregate. |=== +[NOTE] +==== +The paths and line counts above were re-measured against HEAD `681d635` on +2026-09-27. An earlier revision of this table named `src/vql/VQL{Parser,Types, +Bidir,Error,Explain}.res` — files that do not exist. That was residue from two +completed migrations: the `vql` → `vcl` rename, and ReScript → AffineScript +(zero `.res` files remain in the tree; 32 `.affine` files do). The counts had +also drifted materially, most notably `vcl_executor.ex` at 1162 claimed versus +2310 actual. Six modules present in `src/vcl/` were not listed at all. +==== + === Known Inconsistencies in Existing Documents For transparency, these inconsistencies exist between the pre-v2.0 documents: -1. **`vcl-vs-sql.adoc`** states VCL lacks GROUP BY, ORDER BY, aggregates, and mutations. This was true for v1.0 but is incorrect for v2.0. The grammar, parser, and executor all support these features. +1. *[closed 2026-09-27]* **`vcl-vs-sql.adoc`** stated VCL lacks GROUP BY, ORDER BY, aggregates, and mutations. That was true for v1.0 but incorrect for v2.0: the grammar, parser, and executor all support these features. The page has now been corrected in place, so this is no longer a live divergence. -2. **`vcl-vs-vcl-dt.adoc`** lists six proof types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION) which differ from the grammar's six (EXISTENCE, CITATION, ACCESS, INTEGRITY, PROVENANCE, CUSTOM). This specification follows the grammar and implementation. +2. *[open — owner decision required]* **`vcl-vs-vcl-dt.adoc`** lists six proof types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION) which differ from the grammar's six (EXISTENCE, CITATION, ACCESS, INTEGRITY, PROVENANCE, CUSTOM). This specification follows the grammar and implementation. The divergent page now carries a prominent WARNING block naming the mismatch; its six normative subsections were *not* rewritten, because doing so in either direction would silently decide whether the grammar or that page is the target. -3. **`vcl-vs-sql.adoc`** describes VCL as "read-only" which is no longer accurate after v2.0 mutations. +3. *[closed 2026-09-27]* **`vcl-vs-sql.adoc`** described VCL as "read-only", which is no longer accurate after v2.0 mutations. The page now states that the Octad API is the *preferred* write path while recording that the grammar and parser do implement `INSERT`/`UPDATE`/`DELETE` as retained legacy forms. -This specification resolves all three inconsistencies in favour of the implemented grammar and source code. +Items 1 and 3 are resolved in the source documents themselves. Item 2 remains open pending an owner decision, and is flagged at the point of divergence rather than resolved unilaterally. // ============================================================================ // APPENDIX E: VCL-dt++ EXTENSIONS (TYPELL INTEGRATION) @@ -2797,7 +2828,16 @@ This specification resolves all three inconsistencies in favour of the implement VCL-dt++ extends VCL v3.0 with six optional clauses that provide maximal type-theoretic strictness. These extensions are consumed by the **Typell verification kernel** (the formal verification substrate for PanLL) and are specified normatively in the grammar delta file: -* link:../../typeql-experimental/docs/vcl-dtpp-grammar.ebnf[`vcl-dtpp-grammar.ebnf`] — EBNF grammar delta (199 lines) +* `vcl-dtpp-grammar.ebnf` — EBNF grammar delta (199 lines). *Not reachable.* + This document cited it at the relative path + `../../typeql-experimental/docs/vcl-dtpp-grammar.ebnf`, which assumed the + sibling repository was checked out alongside this one. That link was dead in + any standalone clone, and `hyperpolymath/typeql-experimental` itself returns + HTTP 404 as of 2026-09-27, so the file cannot be resolved even with the + sibling present. Cross-repository references in this document are given as + absolute URLs for exactly this reason; this one has no URL to give. The + grammar delta needs re-homing — see issue #84, whose cross-repo synthesis + track covers the VCL-dt++ / Typell boundary. All six clauses are optional and composable in any combination. They append after the standard query structure with no keyword conflicts against VCL v3.0's 60+ reserved keywords. @@ -2983,7 +3023,7 @@ Idris2 ABI mapping: `BoundedResource : (n : Nat) -> Type`. Generalises linear ty ==== Combined: Maximal Strictness -All six clauses composed together (see also link:../../typell/docs/design/DESIGN-2026-03-01-typell-vision.md[Typell Vision Document]): +All six clauses composed together (see also link:https://github.com/hyperpolymath/typell/blob/main/docs/design/DESIGN-2026-03-01-typell-vision.adoc[Typell Vision Document]): [source,sql] ---- @@ -3006,7 +3046,7 @@ VCL-dt++ queries are verified by the Typell kernel via JSON-RPC: typell.check(query, "vcl-dt++") → TypeResult ---- -The kernel returns: types, proof obligations, linear tracking, session protocol compliance, effect analysis, modal scope verification, and proof certificates. See the link:../../typell/docs/design/DESIGN-2026-03-01-typell-vision.md[Typell Vision Document] for the full verification protocol specification. +The kernel returns: types, proof obligations, linear tracking, session protocol compliance, effect analysis, modal scope verification, and proof certificates. See the link:https://github.com/hyperpolymath/typell/blob/main/docs/design/DESIGN-2026-03-01-typell-vision.adoc[Typell Vision Document] for the full verification protocol specification. === Status diff --git a/docs/architecture/abi-ffi.adoc b/docs/architecture/abi-ffi.adoc index 8f72de5b..e215f906 100644 --- a/docs/architecture/abi-ffi.adoc +++ b/docs/architecture/abi-ffi.adoc @@ -1,8 +1,15 @@ -\{\{~ Aditionally delete this line and fill out the template below ~}} +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += VeriSimDB ABI/FFI Documentation +:toc: left +:toclevels: 2 -== VERISIMDB ABI/FFI Documentation +// This file was generated from the RSR ABI/FFI template and carried the +// template's own placeholder line as its first line until 2026-09-27. That line +// instructed the reader to delete it; it has been deleted, and the document +// promoted from a level-2 heading to a proper level-1 title. -=== Overview +== Overview This library follows the *Hyperpolymath RSR Standard* for ABI and FFI design: @@ -14,7 +21,7 @@ compatibility * *Generated C headers* bridge Idris2 ABI to Zig FFI * *Any language* can call through standard C ABI -=== Architecture +== Architecture .... ┌─────────────────────────────────────────────┐ @@ -50,7 +57,7 @@ compatibility └─────────────────────────────────────────────┘ .... -=== Directory Structure +== Directory Structure .... {{project}}/ @@ -82,9 +89,9 @@ compatibility └── julia/ .... -=== Why Idris2 for ABI? +== Why Idris2 for ABI? -==== 1. *Formal Verification* +=== 1. *Formal Verification* Idris2’s dependent types allow proving properties about the ABI at compile-time: @@ -104,7 +111,7 @@ public export abiCompatible : Compatible (ABI 1) (ABI 2) ---- -==== 2. *Type Safety* +=== 2. *Type Safety* Encode invariants that C/Zig cannot express: @@ -119,7 +126,7 @@ data Buffer : (n : Nat) -> Type where MkBuffer : Vect n Byte -> Buffer n ---- -==== 3. *Platform Abstraction* +=== 3. *Platform Abstraction* Platform-specific types with compile-time selection: @@ -134,7 +141,7 @@ CSize Linux = Bits64 CSize Windows = Bits64 ---- -==== 4. *Safe Evolution* +=== 4. *Safe Evolution* Prove that new ABI versions are backward-compatible: @@ -150,9 +157,9 @@ abiUpgrade old = MkABI2 { } ---- -=== Why Zig for FFI? +== Why Zig for FFI? -==== 1. *C ABI Compatibility* +=== 1. *C ABI Compatibility* Zig exports C-compatible functions naturally: @@ -163,7 +170,7 @@ export fn library_function(param: i32) i32 { } ---- -==== 2. *Memory Safety* +=== 2. *Memory Safety* Compile-time safety without runtime overhead: @@ -174,7 +181,7 @@ const handle = init() orelse return error.InitFailed; defer free(handle); ---- -==== 3. *Cross-Compilation* +=== 3. *Cross-Compilation* Built-in cross-compilation to any platform: @@ -185,7 +192,7 @@ zig build -Dtarget=aarch64-macos zig build -Dtarget=x86_64-windows ---- -==== 4. *Zero Dependencies* +=== 4. *Zero Dependencies* No runtime, no libc required (unless explicitly needed): @@ -196,9 +203,9 @@ pub const lib = @import("std"); // Only includes what you use ---- -=== Building +== Building -==== Build FFI Library +=== Build FFI Library [source,bash] ---- @@ -208,7 +215,7 @@ zig build -Doptimize=ReleaseFast # Build optimized zig build test # Run tests ---- -==== Generate C Header from Idris2 ABI +=== Generate C Header from Idris2 ABI [source,bash] ---- @@ -216,7 +223,7 @@ cd src/abi idris2 --cg c-header Types.idr -o ../../generated/abi/{{project}}.h ---- -==== Cross-Compile +=== Cross-Compile [source,bash] ---- @@ -232,9 +239,9 @@ zig build -Dtarget=aarch64-macos zig build -Dtarget=x86_64-windows ---- -=== Usage +== Usage -==== From C +=== From C [source,c] ---- @@ -262,7 +269,7 @@ Compile with: gcc -o example example.c -l{{project}} -L./zig-out/lib ---- -==== From Idris2 +=== From Idris2 [source,idris] ---- @@ -280,7 +287,7 @@ main = do putStrLn "Success" ---- -==== From Rust +=== From Rust [source,rust] ---- @@ -304,7 +311,7 @@ fn main() { } ---- -==== From Julia +=== From Julia [source,julia] ---- @@ -335,9 +342,9 @@ finally end ---- -=== Testing +== Testing -==== Unit Tests (Zig) +=== Unit Tests (Zig) [source,bash] ---- @@ -345,7 +352,7 @@ cd ffi/zig zig build test ---- -==== Integration Tests +=== Integration Tests [source,bash] ---- @@ -353,7 +360,7 @@ cd ffi/zig zig build test-integration ---- -==== ABI Verification (Idris2) +=== ABI Verification (Idris2) [source,idris] ---- @@ -368,7 +375,7 @@ main = do putStrLn "ABI verification passed" ---- -=== Contributing +== Contributing When modifying the ABI/FFI: @@ -395,15 +402,32 @@ idris2 --cg c-header src/abi/Types.idr -o generated/abi/{{project}}.h * Usage examples * Migration guide (if breaking changes) -=== License +== License MPL-2.0 -=== See Also +== See Also * https://idris2.readthedocs.io[Idris2 Documentation] * https://ziglang.org/documentation/master/[Zig Documentation] * https://github.com/hyperpolymath/rhodium-standard-repositories[Rhodium Standard Repositories] -* link:../ffi-migration-guide.md[FFI Migration Guide] -* link:../abi-migration-guide.md[ABI Migration Guide] + +[NOTE] +==== +This section previously linked to an *FFI Migration Guide* and an *ABI Migration +Guide* under `docs/`. Neither document was ever written, and both links were dead. +They are recorded here as plain text rather than left as links that 404, because a +"See Also" entry pointing at nothing is a promise the documentation does not keep. + +If the Zig FFI or the Idris2 ABI is changed in a breaking way, that guide is what +should be written — and it should be written as part of the change, not +afterwards, since the ABI is the contract every cross-language caller depends on. +Until then the migration path is `CHANGELOG.adoc` plus this document. +==== + +* link:../../ARCHITECTURE.adoc[Architecture Index] — the component map and the +architecture decision register +* link:../vcl-architecture.adoc[VCL Architecture] — the dual-path query router +* link:../../debugger/docs/CITATIONS.adoc[debugger citations] — the ABI/FFI +debugger lives at `debugger/` diff --git a/docs/architecture/snifs-bridge.adoc b/docs/architecture/snifs-bridge.adoc new file mode 100644 index 00000000..1822dcbc --- /dev/null +++ b/docs/architecture/snifs-bridge.adoc @@ -0,0 +1,351 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += SNIFs WASM Bridge — design and boundary analysis +:toc: left +:toclevels: 3 +:icons: font + +[NOTE] +==== +*Status: design, not implementation.* This is step 6 of issue #86, written so the +step-1 owner decision can be taken against evidence rather than against the +sketch in the issue. No `verisim.wasm` artefact exists and no SNIF wrapper has +been spiked. + +*The headline finding is that issue #86's two options are both mis-specified +against what SNIFs actually is.* Read <> before <>. The +short version: SNIFs has *no WASI and no filesystem*, and *no BEAM terms cross +its boundary* — only `i32/i64/f32/f64` and byte-buffers. That rules out Option B +outright and rules most of Option A's proposed surface out with it. What survives +is a narrower and more defensible bridge: *pure-compute kernels, not stores*. +==== + +== What this bridge is for + +Architectural position agreed 2026-06-01: BEAM-side cross-language access to +VeriSimDB flows through *one* boundary rather than through a per-language SDK. +The question "do we ship a Gleam SDK?" is answered once, with a principled no — +ship a SNIF-compatible WASM module that any BEAM language can call, and Gleam, +Erlang, LFE, Hamler and Akula all get access through it. + +That decision is *sound and is not revisited here*. The Gleam SDK was retired in +PR #85 on exactly this basis, and the SDK matrix dropped from six first-class +clients to five (Rust, Elixir, ReScript, Julia, Zig). What this document revises +is the *shape* of the boundary, because the shape proposed in #86 does not fit +the upstream project's stated scope. + +[#sec-scope] +== What SNIFs actually is, and what that constrains + +https://github.com/hyperpolymath/snifs[SNIFs] — *Safer (sandboxed) NIFs* — keeps +the NIF *interface* and replaces its *implementation*: the guest compiles to +WebAssembly and runs in a `wasmtime` sandbox via `wasmex`, so a guest fault +becomes a catchable `{:error, reason}` tuple and the calling BEAM process +survives. A normal NIF runs native code inside the VM's address space, so any +fault in it kills the entire VM. + +The scope statement in its README is precise, and the precision is the part that +matters here: + +[cols="2,4",options="header"] +|=== +|Property |Consequence for VeriSimDB + +|*Like-for-like replacement for pure native computation over numbers and +byte-buffers* — crypto, compression, parsing, DSP, math kernels +|The drift scorer, the planner's cost algebra, vector distance kernels and proof +verification are all in this class. The stores are not. + +|*Only `i32/i64/f32/f64` and bytes cross the boundary.* A normal NIF receives +actual BEAM terms and reads binaries zero-copy; a SNIF sees only what you +marshal into linear memory +|Every `Octad`, `DriftReport` or proof witness must be serialised by the caller +and deserialised by the guest. #86 attributed this cost to Option B alone; it is +a property of *SNIFs*, and therefore applies to Option A identically. + +|*No I/O of any kind.* The guest is `wasm32-freestanding` with *no WASI* +(upstream ADR-002) +|*Decisive.* No filesystem, no sockets. `verisim-storage` (redb), +`verisim-document` (tantivy), `verisim-graph` (Oxigraph), `verisim-wal` and the +whole HTTP/gRPC surface require I/O and *cannot* run in the guest. + +|*The result is fallible:* `{:ok, values} \| {:error, reason}` +|Aligns exactly with the principle `rust-core/verisim-nif/src/lib.rs` already +encodes: "an unimplemented operation MUST fail loudly, never fake success". A +scaffold that returned canned success JSON once turned a write into *silent data +loss reported as success*. SNIFs' interface makes that class of bug inexpressible. + +|*Out of scope:* BEAM-term manipulation, `enif_make_resource`, monitors, +message-sending, dirty scheduling, zero-copy binaries +|No long-lived guest-side handle to a store. A SNIF call is stateless compute; +state stays in the host. + +|*Scope ceiling by design:* graduated integration, capability negotiation and +transaction-gating are deliberately *not* SNIF features — upstream routes them to +the *cleave* and *groove* projects +|Do not plan VeriSimDB features that require the bridge to negotiate +capabilities or gate transactions. That is asking SNIFs to be something it has +explicitly decided not to be. +|=== + +=== Measured overhead + +From upstream's in-BEAM benchmark (OTP 25, `fibonacci(20)`, n=2000): + +[cols="3,1,1,1,3",options="header"] +|=== +|Case |mean µs |p50 µs |p99 µs |Note + +|Per-call (compile every call) |3978 |3571 |10594 |the naive path — *do not do this* +|*Pooled* (compile once) |70 |*29* |500 |56× faster than per-call +|Buffer round-trip (`sum_f32`) |20 |15 |71 |the data-marshalling case +|Port (OS process, isolated) |1617 |1445 |4483 |the *other* isolated option +|=== + +Three numbers drive the design: + +* *~29 µs fixed dispatch per call.* This dominates tiny, high-frequency calls and + amortises to nothing once a call does real work. A drift score for one entity is + not "real work" at this granularity — *batch it*. +* *Pooled SNIF is ~23× cheaper than a Port* for the same crash isolation. Since + VeriSimDB's current BEAM↔Rust paths are HTTP (`VERISIM_TRANSPORT=http`) and a + parser Port (`VCLBridge`), the bridge is a genuine improvement over the Port, + not merely over nothing. +* *Compute is ~1.1–1.5× native* (upstream's estimate, not yet measured for its + kernels). This is the only *unamortisable* tax, so it bounds the benefit for + long calls: a kernel that is 1.4× slower but crash-isolated may still be worth + it, and the arithmetic should be done per kernel rather than assumed. + +*Critical invariant:* Zig guests must be compiled `-OReleaseSafe`. `ReleaseFast` +removes bounds checks and turns the same faults into *silent wrong answers* — +empirically verified upstream, and used there as the negative control. For a +database whose entire purpose is detecting silent divergence, shipping a +`ReleaseFast` bridge would be self-refuting. + +[#sec-options] +== Option A, Option B, and the option that actually works + +#86 offers two delivery options and recommends "A long-term, B as the v0 if it +ships faster". Measured against the scope above, neither survives as written. + +=== Option B — `verisim-api` as the WASM target: *not viable* + +#86 describes compiling the HTTP/JSON API gateway to WASM and having SNIFs wrap +it and "serve it locally". Serving anything locally requires sockets. SNIFs +permits *no I/O at all* (ADR-002, no WASI). This is not a performance trade-off +or an invasive refactor — it is a capability the guest does not have. + +There is a nearby shape that *does* work, and it is worth naming because it is +probably what Option B was reaching for: the host performs all I/O and the guest +is a pure *request handler* over byte-buffers — bytes in, bytes out, no sockets. +But that is not "the API gateway compiled to WASM"; it is a serialised +compute kernel with an HTTP-shaped input format, and it inherits all of Option A's +marshalling costs while adding a JSON encode/decode hop on top. It is strictly +worse than picking the right kernels directly. + +*Recommendation: drop Option B.* + +=== Option A — `verisim-core` compiled to WASM: *viable only for part of the surface* + +#86 proposes carving out the rust-core API surface that does not need tokio, and +names `OctadStore`, `DriftCalculator` and `Normalizer` as likely candidates while +excluding the planner/optimizer and async federation. + +The tokio test is necessary but *not sufficient*. Removing async gets you a +crate that compiles for `wasm32-unknown-unknown`; it does not get you a crate +that can run without a filesystem. + +[cols="2,2,2,4",options="header"] +|=== +|Candidate |#86 said |Verdict |Why + +|`OctadStore` (`verisim-octad`, `verisim-storage`) +|through WASM +|*❌ No* +|Persists through redb / tantivy / Oxigraph. All three need a filesystem. No WASI. + +|`Normalizer` (`verisim-normalizer`) +|through WASM +|*❌ No* +|Repair *writes*. Reads and writes both need the stores, which need I/O. + +|`DriftCalculator` (`verisim-drift`) +|through WASM +|*✅ Yes* +|Computes a scalar severity over modal views. Pure numeric compute — SNIFs' +stated sweet spot. Needs the views marshalled in, but produces a small result. + +|Planner / optimizer (`verisim-planner`) +|*excluded* by #86 +|*✅ Yes — and #84 strengthens the case* +|Issue #84 observes the planner is *already secretly tropical*: `parallel` takes +`max` (tropical addition) and `sequential` sums `time_ms` (tropical +multiplication). That is pure arithmetic over a plan DAG. It is a better bridge +candidate than several things #86 included, and excluding it looks like an error +rather than a judgement. + +|Vector distance kernels (`verisim-vector`) +|not considered +|*✅ Yes — best-measured case* +|Cosine / Euclidean over `f32` buffers is precisely the shape of upstream's own +`sum_f32` buffer-round-trip benchmark (p50 15 µs, p99 71 µs). The only candidate +with a directly comparable published measurement. + +|Proof verification (`verisim-semantic`, CBOR + `sha2`) +|not considered +|*⚠️ Conditional* +|"Crypto, parsing" is explicitly inside SNIFs' scope, but witnesses are +byte-buffers that must be marshalled both ways, and the ZKP surface is +partly `NotImplemented` today. Worth spiking *after* drift and cost. + +|`verisim-wal`, `verisim-api`, federation +|excluded +|*❌ Correctly excluded* +|Filesystem and sockets respectively. #86 got these right. +|=== + +=== Option C — the recommendation: *pure-compute kernels, host keeps all I/O* + +State the boundary as a rule rather than a list, so the next crate can be +classified without re-litigating this document: + +[IMPORTANT] +==== +*A VeriSimDB function may cross the SNIF boundary if and only if it is total +over marshalled numeric/byte input, produces marshalled numeric/byte output, and +performs no I/O.* Stores, WAL, API and federation stay host-side. Kernels cross. +==== + +Concretely, the v0 bridge surface is four kernels: + +. *drift scoring* — `verisim-drift`: modal views in, severity + drift type out +. *plan costing* — `verisim-planner`: plan DAG in, tropical cost estimate out +. *vector distance* — `verisim-vector`: `f32` buffers in, distances out +. *octad checksum* — `verisim-octad`'s identity/consonance hash, which is pure + over serialised modal data and is the cheapest useful thing to prove the + plumbing with + +Everything else stays native. This is a *smaller* bridge than #86 proposed, and +it is smaller for a reason that will still be true in a year: the constraint is +upstream's ADR-002, not VeriSimDB's ambition. + +=== Where the bridge sits relative to `verisim-nif` + +`rust-core/verisim-nif` is a Rustler NIF scaffold — an honest stub returning +`{:error, :not_implemented}` for every operation, tracked in issue #61, and the +only crate in the workspace with zero tests. The Elixir transport selector is: + +---- +VERISIM_TRANSPORT=http # default: HTTP to the verisim-api server +VERISIM_TRANSPORT=nif # demand NIF: surfaces {:error, :not_implemented} loudly +VERISIM_TRANSPORT=auto # NIF only if OPERATIONAL, else HTTP — today always HTTP +---- + +The SNIF bridge is a *fourth* transport, not a replacement for the NIF crate: + +---- +VERISIM_TRANSPORT=snif # crash-isolated WASM kernels; host retains all I/O +---- + +Two consequences worth stating now: + +* A Rustler NIF runs native code *inside* the VM's address space, so a fault in + it kills the BEAM. A SNIF does not. If both eventually exist, `snif` is the + safer default for the kernels it covers and `nif` remains the path for anything + needing BEAM terms or resources. +* `verisim-nif` being untested and `verisim-snif` being unbuilt are the same gap + viewed from two directions: *the in-process transport has never been exercised*. + Issue #79 ranks `verisim-nif` as the worst test-density crate in the workspace + (0 tests / 135 LOC). Whatever gets built here should not repeat that. + +== Sequence + +Revised from #86's six steps. The revision is that step 3 is *answered by this +document* rather than left open, and that step 1's decision is reframed. + +[cols="1,3,2,3",options="header"] +|=== +|# |Step |Owner |Note + +|1 +|Ratify Option C (kernels, not stores) and record why A and B do not survive +contact with SNIFs' scope +|*owner ruling* +|This document is the briefing. It is one decision, and it unblocks everything +below + +|2 +|Spike: one kernel end-to-end. *Recommended: vector distance*, because upstream +publishes a directly comparable `sum_f32` buffer-round-trip measurement to check +the result against +|1–2 days +|Success criterion is a p50 near upstream's 15 µs and a caller that survives a +deliberately trapping guest + +|3 +|Define the marshalling codec for the four v0 kernels +|architectural +|#84 step 4 proposes wiring the vcl-ut wire-codec in for query-shaped calls. For +*these* kernels that is over-engineering: they carry fixed-width numeric arrays, +not queries. Use a flat binary layout and reserve the wire codec for VCL-shaped +calls if they ever cross + +|4 +|Second kernel: drift scoring. Third: plan costing +|— +|Drift is the differentiating feature and the one whose correctness matters most; +costing is the one #84 has a theorem waiting for + +|5 +|Publish `verisim.wasm` per release; publish the SNIF wrapper as a hex package +|— +|Must be built `-OReleaseSafe` (or the Rust equivalent with overflow and bounds +checks *on*). A `ReleaseFast` artefact would be a silent-wrong-answer generator +in a drift-detection database + +|6 +|Add `VERISIM_TRANSPORT=snif` and *test it* +|— +|Include a crash-isolation test in the style upstream uses: force a guest trap +and assert the calling process survives. `verisim-nif`'s zero-test record is the +counter-example +|=== + +== Open questions this document does not answer + +* *Does the ~29 µs dispatch floor change any current call pattern?* VeriSimDB's + drift monitor scores entities on a schedule; if it scores one entity per call, + the floor dominates and batching is mandatory rather than optional. That needs + a measurement of the current call granularity, which needs a running system. +* *Rust or Zig for the guest?* SNIFs supports both at parity. VeriSimDB's kernels + are Rust, so Rust avoids a rewrite; but Zig is where upstream's five crash-mode + test surface lives, and `-OReleaseSafe` is a Zig flag with no exact Rust + analogue (the Rust equivalent is keeping `overflow-checks` and bounds checks on + in a release profile, which this repo currently *disables* — `Cargo.toml` sets + `panic = "abort"`, `lto = true`, `codegen-units = 1`). That profile + interaction needs checking before a Rust guest is assumed safe. +* *Is crash isolation the right reason?* For a database whose value proposition + is *detecting* divergence, a kernel that silently returns a wrong drift score + is worse than one that crashes. SNIFs converts crashes into errors, which is the + right direction — but only if the guest keeps its checks. This is the same + question as the previous bullet and it is the one that matters most. + +== Related + +* Issue #86 — this document is its step 6 +* Issue #84 — cross-repo synthesis; the tropical-planner observation used above, + and the vcl-ut wire-codec proposal +* Issue #79 — test expansion; `verisim-nif` at 0 tests / 135 LOC is the + worst-served crate in the workspace +* https://github.com/hyperpolymath/snifs[`hyperpolymath/snifs`] — upstream: + README (scope and benchmarks), ADR-002 (no WASI), `demo/` (wasmex loader + + ExUnit suite), `verification/proofs/agda/SnifIsolation.agda` (the SEC-1 + crash-isolation theorem) +* link:abi-ffi.adoc[`docs/architecture/abi-ffi.adoc`] — the Idris2/Zig ABI + contract, which is a *different* cross-language boundary and should not be + conflated with this one +* link:topology.adoc[`docs/architecture/topology.adoc`] — process topology +* link:../../ARCHITECTURE.adoc[`ARCHITECTURE.adoc`] — component map and decision + register +* `rust-core/verisim-nif/src/lib.rs` — the honest-stub rationale and the + transport selector diff --git a/docs/architecture/topology.adoc b/docs/architecture/topology.adoc index 2f3a752f..b6ff189d 100644 --- a/docs/architecture/topology.adoc +++ b/docs/architecture/topology.adoc @@ -1,6 +1,16 @@ -== TOPOLOGY.md — VeriSimDB +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += Process Topology — VeriSimDB +:toc: left +:toclevels: 2 -=== System Architecture +// Titled "TOPOLOGY.md" until 2026-09-27, in a file that is .adoc, as a +// level-2 heading with level-3 sections beneath it. Both were template +// artefacts; the title now names the document, not a filename that does not +// exist. + + +== System Architecture .... ┌─────────────────────────────────────┐ @@ -53,7 +63,7 @@ panic-attack → verisimdb-data (flat-file) → hypatia (rules) → gitbot-fleet (fixes) .... -=== Completion Dashboard +== Completion Dashboard [cols=",,",options="header",] |=== @@ -82,7 +92,7 @@ |*Overall* |`+██████░░░░+` *65%* | |=== -=== Key Dependencies +== Key Dependencies .... verisimdb diff --git a/docs/backwards-compatibility.adoc b/docs/backwards-compatibility.adoc index e9e5f0a9..fb126eaa 100644 --- a/docs/backwards-compatibility.adoc +++ b/docs/backwards-compatibility.adoc @@ -96,7 +96,7 @@ LIMIT 10; **Octad schema changes:** ```scheme -;; STATE.scm tracks schema version +;; STATE.a2ml tracks schema version (metadata (schema-version "1.2.0") ; Current Octad schema (min-compatible-version "1.0.0")) ; Oldest readable format diff --git a/docs/challenges-federated.adoc b/docs/challenges-federated.adoc index 9bad8643..42039a30 100644 --- a/docs/challenges-federated.adoc +++ b/docs/challenges-federated.adoc @@ -923,4 +923,4 @@ For simpler use cases, **standalone** or **hybrid** modes are recommended. - link:challenges-hybrid.adoc[Challenges: Hybrid Mode] - link:technical-specification-kraft-metadata-log.adoc[KRaft Metadata Log Specification] - link:zkp-and-sanctify-integration.adoc[Zero-Trust Security with ZKP] -- link:../WHITEPAPER.md[VeriSimDB White Paper] +- link:../WHITEPAPER.pdf[VeriSimDB White Paper] diff --git a/docs/challenges-hybrid.adoc b/docs/challenges-hybrid.adoc index 3f8ebd5e..37457a60 100644 --- a/docs/challenges-hybrid.adoc +++ b/docs/challenges-hybrid.adoc @@ -779,4 +779,4 @@ For simpler deployments, **standalone** may be better. For full-scale federation - link:deployment-modes.adoc[Deployment Modes Overview] - link:challenges-standalone.adoc[Challenges: Standalone Mode] - link:challenges-federated.adoc[Challenges: Federated Mode] -- link:../WHITEPAPER.md[VeriSimDB White Paper] +- link:../WHITEPAPER.pdf[VeriSimDB White Paper] diff --git a/docs/challenges-standalone.adoc b/docs/challenges-standalone.adoc index 1e9b24b4..671bbd05 100644 --- a/docs/challenges-standalone.adoc +++ b/docs/challenges-standalone.adoc @@ -446,4 +446,4 @@ For larger deployments, consider **hybrid** or **federated** mode to mitigate th - link:deployment-modes.adoc[Deployment Modes Overview] - link:challenges-hybrid.adoc[Challenges: Hybrid Mode] - link:challenges-federated.adoc[Challenges: Federated Mode] -- link:../WHITEPAPER.md[VeriSimDB White Paper] +- link:../WHITEPAPER.pdf[VeriSimDB White Paper] diff --git a/docs/decisions/kraft-comparison.adoc b/docs/decisions/kraft-comparison.adoc index dfb69b36..be742c06 100644 --- a/docs/decisions/kraft-comparison.adoc +++ b/docs/decisions/kraft-comparison.adoc @@ -65,5 +65,5 @@ VeriSimDB's federated registry could potentially: == References -- link:docs/technical-specification-kraft-metadata-log.adoc[VeriSimDB KRaft Integration Spec] +- link:../technical-specification-kraft-metadata-log.adoc[VeriSimDB KRaft Integration Spec] - https://cwiki.apache.org/confluence/display/KAFKA/KIP-500%3A+Replace+ZooKeeper+with+a+Self-Managed+Metadata+Quorum[KIP-500: Replace ZooKeeper with a Self-Managed Metadata Quorum] diff --git a/docs/error-handling-strategy.adoc b/docs/error-handling-strategy.adoc index 0f6d034c..a16247e9 100644 --- a/docs/error-handling-strategy.adoc +++ b/docs/error-handling-strategy.adoc @@ -1255,5 +1255,5 @@ Parse Error at 1:8: Expected 'GRAPH', 'VECTOR', ..., found 'GRPH' - link:vcl-architecture.adoc[VCL Architecture] - link:caching-strategy.adoc[Caching Strategy] - link:reversibility-design.adoc[Reversibility Design] -- link:../src/vql/VQLError.res[VCL Error Types] +- link:../src/vcl/VCLError.affine[VCL Error Types] - link:../lib/verisim/error_recovery.ex[Error Recovery Implementation] diff --git a/docs/minikanren-integration-v3.adoc b/docs/minikanren-integration-v3.adoc index 9c2f63b8..61c2aaaa 100644 --- a/docs/minikanren-integration-v3.adoc +++ b/docs/minikanren-integration-v3.adoc @@ -221,7 +221,7 @@ let solveQueryPlan = (queryAst: string): array => { === Option C: Scheme miniKanren (via Guile) -**Use existing STATE.scm infrastructure:** +**Use existing STATE.a2ml infrastructure:** ```scheme ;; lib/verisim_minikanren.scm diff --git a/docs/normalization-cascade.adoc b/docs/normalization-cascade.adoc index 8c7acb73..9038278b 100644 --- a/docs/normalization-cascade.adoc +++ b/docs/normalization-cascade.adoc @@ -756,7 +756,7 @@ In v3, miniKanren can **synthesize normalization rules** from examples: - link:drift-handling.adoc[Drift Handling Documentation] - link:backwards-compatibility.adoc[Backwards Compatibility Strategy] -- link:adaptive_learner.ex[Adaptive Learner Implementation] +- link:../lib/verisim/adaptive_learner.ex[Adaptive Learner Implementation] - link:minikanren-integration-v3.adoc[miniKanren Integration (v3)] - Helland, P. (2007). *Life beyond Distributed Transactions: an Apostate's Opinion*. CIDR. - Bailis, P. et al. (2013). *Eventual Consistency Today: Limitations, Extensions, and Beyond*. ACM Queue. diff --git a/docs/query-optimization-overview.adoc b/docs/query-optimization-overview.adoc index 0d739df3..8867a9c2 100644 --- a/docs/query-optimization-overview.adoc +++ b/docs/query-optimization-overview.adoc @@ -480,4 +480,4 @@ LIMIT 10 - link:reversibility-design.adoc[Reversibility Design] - Full technical specification - link:../lib/verisim/query_planner_config.ex[Query Planner Config] - Source code - link:../lib/verisim/query_planner_bidirectional.ex[Bidirectional Optimization] - Source code -- link:../src/vql/VQLExplain.res[EXPLAIN Implementation] - Source code +- link:../src/vcl/VCLExplain.affine[EXPLAIN Implementation] - Source code diff --git a/docs/reversibility-design.adoc b/docs/reversibility-design.adoc index ce88f27f..ee1deb4a 100644 --- a/docs/reversibility-design.adoc +++ b/docs/reversibility-design.adoc @@ -410,7 +410,7 @@ end == References -- link:../WHITEPAPER.md[VeriSimDB White Paper] - Temporal modality design +- link:../WHITEPAPER.pdf[VeriSimDB White Paper] - Temporal modality design - link:technical-specification-kraft-metadata-log.adoc[KRaft Log] - Append-only log - link:vcl-architecture.adoc[VCL Architecture] - Query execution - https://martin.kleppmann.com/2015/05/27/logs-for-data-infrastructure.html[Designing Data-Intensive Applications] diff --git a/docs/safety-and-fault-tolerance.adoc b/docs/safety-and-fault-tolerance.adoc index fcd4894b..85c63a42 100644 --- a/docs/safety-and-fault-tolerance.adoc +++ b/docs/safety-and-fault-tolerance.adoc @@ -1156,6 +1156,6 @@ Invariant: - link:error-handling-strategy.adoc[Error Handling Strategy] - link:reversibility-design.adoc[Reversibility Design] - link:vcl-architecture.adoc[VCL Architecture] -- link:../lib/verisim/supervisor.ex[Supervisor Tree Implementation] +- link:../elixir-orchestration/lib/verisim/application.ex[Supervisor Tree Implementation] - https://www.erlang.org/doc/design_principles/des_princ.html[OTP Design Principles] - https://doc.rust-lang.org/book/ch04-01-what-is-ownership.html[Rust Ownership System] diff --git a/docs/vcl-architecture.adoc b/docs/vcl-architecture.adoc index 7d294895..be92b4ec 100644 --- a/docs/vcl-architecture.adoc +++ b/docs/vcl-architecture.adoc @@ -7,7 +7,7 @@ == Overview -This document describes the **corrected** VCL (VeriSim Consonance Language) architecture, aligned with link:../design-decisions.adoc[Architecture Design Decisions] and the link:../WHITEPAPER.md[VeriSimDB White Paper]. +This document describes the **corrected** VCL (VeriSim Consonance Language) architecture, aligned with link:../ARCHITECTURE.adoc[the architecture decision register] and the link:../WHITEPAPER.pdf[VeriSimDB White Paper]. **Key Corrections from Initial Design:** @@ -625,8 +625,8 @@ let searchPapers = async () => { - link:vcl-grammar.ebnf[VCL Grammar (EBNF)] - link:vcl-examples.adoc[VCL Examples] -- link:../WHITEPAPER.md[VeriSimDB White Paper] -- link:../design-decisions.adoc[Architecture Design Decisions] +- link:../WHITEPAPER.pdf[VeriSimDB White Paper] +- link:../ARCHITECTURE.adoc[Architecture Index] — the component map and the AD-001…AD-007 decision register - link:technical-specification-kraft-metadata-log.adoc[KRaft Metadata Log] - link:challenges-federated.adoc[Federated Deployment Challenges] @@ -637,11 +637,11 @@ let searchPapers = async () => { | CockroachDB for metadata | ReScript + Raft -| Simpler, sufficient for <20 nodes (link:../design-decisions.adoc:247[]) +| Simpler, sufficient for <20 nodes | Fluree for audit trails | verisim-temporal (Merkle trees) -| Lighter weight, no blockchain overhead (link:../design-decisions.adoc:140[]) +| Lighter weight, no blockchain overhead | No drift integration | DriftMonitor checks @@ -653,7 +653,7 @@ let searchPapers = async () => { | CockroachDB geo-partitioning | Raft quorum -| Only migrate to CockroachDB if >20 nodes (link:../design-decisions.adoc:224[]) +| Only migrate to CockroachDB if >20 nodes |=== == Appendix B: Technology Stack diff --git a/docs/vcl-examples.adoc b/docs/vcl-examples.adoc index 88175ce4..6fce67cd 100644 --- a/docs/vcl-examples.adoc +++ b/docs/vcl-examples.adoc @@ -1072,6 +1072,6 @@ ensures the deletion is recorded in the audit chain. - link:vcl-grammar.ebnf[VCL Grammar (EBNF)] - link:backwards-compatibility.adoc[Backwards Compatibility Strategy] - link:drift-handling.adoc[Drift Handling Documentation] -- link:../WHITEPAPER.md[VeriSimDB White Paper] +- link:../WHITEPAPER.pdf[VeriSimDB White Paper] - link:technical-specification-kraft-metadata-log.adoc[KRaft Metadata Log Specification] -- link:../design-decisions.adoc[Architecture Design Decisions] +- link:../ARCHITECTURE.adoc[Architecture Index] — the component map and the AD-001…AD-007 decision register diff --git a/docs/vcl-grammar.ebnf b/docs/vcl-grammar.ebnf index 0142a336..ccf7c950 100644 --- a/docs/vcl-grammar.ebnf +++ b/docs/vcl-grammar.ebnf @@ -4,6 +4,17 @@ (* Version: 3.0 — Octad (8 modalities), provenance conditions, spatial conditions *) (* Date: 2026-02-27 *) +(* ------------------------------------------------------------------------ + DUPLICATE-GRAMMAR NOTICE (added 2026-09-27) + This file is a near-duplicate of spec/grammar.ebnf, which is treated as + canonical (it carries the @taxonomy tag and the copyright line, and is the + copy cited by README.adoc, EXPLAINME.adoc, 0-AI-MANIFEST.a2ml and + spec/system-specs.adoc). The two were identical in substance. + Any edit to the grammar MUST be applied to both files, or this duplicate + retired. Consolidation is an owner decision; see + ULTRAPLAN-2026-09-27.adoc. + ------------------------------------------------------------------------ *) + (* ============================================================================ 1. TOP-LEVEL STRUCTURE ============================================================================ *) diff --git a/docs/vcl-vs-sql.adoc b/docs/vcl-vs-sql.adoc index fd6f19f0..de34392e 100644 --- a/docs/vcl-vs-sql.adoc +++ b/docs/vcl-vs-sql.adoc @@ -8,9 +8,11 @@ == Introduction -VCL (VeriSim Consonance Language) is the query language for VeriSimDB, a 6-core multimodal database. While VCL borrows familiar keywords from SQL (`SELECT`, `FROM`, `WHERE`, `LIMIT`, `OFFSET`), it serves a fundamentally different purpose. +VCL (VeriSim Consonance Language) is the query language for VeriSimDB, an eight-modality database. While VCL borrows familiar keywords from SQL (`SELECT`, `FROM`, `WHERE`, `LIMIT`, `OFFSET`), it serves a fundamentally different purpose. -VCL is **read-only**. It does not support `INSERT`, `UPDATE`, or `DELETE` statements. All mutations go through the Octad API (Rust core or Elixir orchestration layer). This is a deliberate design choice: VeriSimDB treats writes as coordinated multi-modal operations that must maintain consistency across all eight modality stores (Graph, Vector, Tensor, Semantic, Document, Temporal, Provenance, Spatial). A simple `INSERT` statement cannot express the cross-modal invariants that a Octad write requires. +VCL's **preferred** write path is the Octad API (Rust core or Elixir orchestration layer), not the language. VeriSimDB treats writes as coordinated multi-modal operations that must maintain consistency across all eight modality stores (Graph, Vector, Tensor, Semantic, Document, Temporal, Provenance, Spatial), and a bare `INSERT` cannot by itself express the cross-modal invariants an octad write requires. + +That said, VCL is **not** read-only. An earlier revision of this page said it was; the normative grammar and the implemented parser disagree, and `link:VCL-SPEC.adoc[VCL-SPEC.adoc]` lists the "read-only" description as a known inconsistency resolved in favour of the implementation. `spec/grammar.ebnf` v3.0 defines `statement = query | mutation ;` with `INSERT HEXAD`, `UPDATE HEXAD … SET …` and `DELETE HEXAD …`, each accepting an optional `PROOF` clause; `src/vcl/VCLParser.affine` implements all three and `src/vcl/VCLBidir.affine` type-checks them. These SQL-shaped mutation forms are retained for backward compatibility. For verified cross-modal writes, use the Octad API or attach a `PROOF` clause. VCL is **multimodal**. Where SQL selects columns from relational tables, VCL selects _modalities_ from _octad stores_ or _federations_. A single VCL query can retrieve graph edges, vector embeddings, tensor slices, semantic annotations, document text, and temporal versions in one pass. @@ -27,7 +29,7 @@ VCL is **federation-aware**. Queries can target a local `STORE`, a specific `HEX |`SELECT` with _column names_ or `*` for all columns. |**Data Source** -|`FROM STORE `, `FROM HEXAD `, or `FROM FEDERATION `. A STORE is a collection of octad entities. A HEXAD is a single entity addressed by UUID. A FEDERATION spans multiple VeriSimDB instances. +|`FROM STORE `, `FROM HEXAD `, or `FROM FEDERATION `. A STORE is a collection of octad entities. `HEXAD` names a single octad entity addressed by UUID — it is the *legacy* keyword for the octad source, retained for backward compatibility from when the entity had six modalities rather than eight. A FEDERATION spans multiple VeriSimDB instances. |`FROM ` or `FROM
AS `. Tables are flat relational structures. |**Filtering** @@ -39,11 +41,11 @@ VCL is **federation-aware**. Queries can target a local `STORE`, a specific `HEX |`JOIN`, `LEFT JOIN`, `RIGHT JOIN`, `FULL OUTER JOIN`, `CROSS JOIN` with `ON` conditions. |**Mutations** -|**None.** VCL is strictly read-only. All writes go through the Octad API: `POST /api/octads` (create), `PUT /api/octads/:id` (update), `DELETE /api/octads/:id` (delete). This ensures cross-modal consistency. +|Legacy SQL-shaped forms exist (`INSERT HEXAD WITH …`, `UPDATE HEXAD SET …`, `DELETE HEXAD `), each with an optional `PROOF` clause. The *preferred* path is the Octad API: `POST /api/octads` (create), `PUT /api/octads/:id` (update), `DELETE /api/octads/:id` (delete). This ensures cross-modal consistency. |`INSERT INTO`, `UPDATE ... SET`, `DELETE FROM`, `MERGE`, `TRUNCATE`. |**Verification** -|`PROOF ()` clause requests a verifiable guarantee about the result. Six proof types: `EXISTENCE`, `INTEGRITY`, `CONSISTENCY`, `PROVENANCE`, `FRESHNESS`, `AUTHORIZATION`. No SQL equivalent exists. +|`PROOF ()` clause requests a verifiable guarantee about the result. Six proof types, as defined by `spec/grammar.ebnf`: `EXISTENCE`, `CITATION`, `ACCESS`, `INTEGRITY`, `PROVENANCE`, `CUSTOM`. No SQL equivalent exists. |No equivalent. SQL has no mechanism for cryptographic or type-theoretic verification of query results. |**Pagination** @@ -51,22 +53,28 @@ VCL is **federation-aware**. Queries can target a local `STORE`, a specific `HEX |`LIMIT n` and `OFFSET n` (or vendor-specific: `TOP`, `FETCH FIRST`). |=== -== What VCL Lacks That SQL Has +== SQL Features: What VCL Has and Lacks + +VCL is intentionally minimal. The table below records the actual status of each +SQL feature against `spec/grammar.ebnf` v3.0. -VCL is intentionally minimal. The following SQL features have no VCL equivalent: +NOTE: Four rows in this table — `GROUP BY`, `ORDER BY`, aggregate functions and +`HAVING` — previously read "Not supported". They are supported: the grammar +defines `group_by_clause`, `order_by_clause`, `having_clause` and +`aggregate_func = 'COUNT' | 'SUM' | 'AVG' | 'MIN' | 'MAX'`. Those claims were +correct for VCL v1.0 and were left behind when v2.0 added them; the correction +closes item 1 of the known-inconsistencies list in link:VCL-SPEC.adoc[VCL-SPEC.adoc]. +The remaining rows are genuinely absent from the grammar. [cols="2,3",options="header"] |=== |SQL Feature |VCL Status -|`GROUP BY` -|Not supported. Aggregation is performed application-side or through the Elixir orchestration layer. +|*Supported* (`group_by_clause`). See link:VCL-SPEC.adoc[VCL-SPEC.adoc] §Aggregation. -|`ORDER BY` -|Not supported. Result ordering is determined by the modality store (e.g., vector similarity ranking, graph traversal order, temporal chronological order). +|*Supported* (`order_by_clause`, with `ASC`/`DESC`). In its absence, ordering falls back to the modality store — vector similarity ranking, graph traversal order, or temporal chronological order. -|Aggregate functions (`COUNT`, `SUM`, `AVG`, `MIN`, `MAX`) -|Not supported. VCL returns raw data; aggregation is a consumer responsibility. +|*Supported* (`aggregate_expr = count_all | aggregate_field`; `aggregate_func = 'COUNT' | 'SUM' | 'AVG' | 'MIN' | 'MAX'`). |Subqueries |Not supported. Queries are flat. Compose results in application code or use the Elixir query router for multi-step workflows. @@ -74,14 +82,13 @@ VCL is intentionally minimal. The following SQL features have no VCL equivalent: |`DISTINCT` |Not supported. Octad entities are inherently unique (UUID-addressed), so deduplication is rarely needed. -|`HAVING` -|Not supported (requires `GROUP BY`). +|*Supported* (`having_clause = 'HAVING', condition ;`), used with `GROUP BY`. |`UNION` / `INTERSECT` / `EXCEPT` |Not supported. Use multiple queries and combine results application-side. |`CREATE TABLE` / DDL -|Not supported. Schema is managed through the ReScript registry and Elixir `SchemaRegistry`. +|Not supported. Schema is managed through the AffineScript registry (`src/registry/`) and the Elixir `SchemaRegistry`. |Window functions (`ROW_NUMBER`, `RANK`, `OVER`) |Not supported. @@ -97,7 +104,7 @@ VCL is intentionally minimal. The following SQL features have no VCL equivalent: |VCL Feature |Description |`PROOF` clause -|Requests a verifiable proof certificate alongside query results. Six proof types cover existence, integrity, consistency, provenance, freshness, and authorization guarantees. Enables dependent-type verification via the VCL-DT path. +|Requests a verifiable proof certificate alongside query results. Six proof types (`EXISTENCE`, `CITATION`, `ACCESS`, `INTEGRITY`, `PROVENANCE`, `CUSTOM`) cover entity presence, citation-chain validity, access rights, tamper-evidence, verifiable lineage, and custom ZKP contracts. Enables dependent-type verification via the VCL-DT path. |Multimodal `SELECT` |Select specific modalities (`GRAPH`, `VECTOR`, `TENSOR`, `SEMANTIC`, `DOCUMENT`, `TEMPORAL`) or all (`*`). No SQL equivalent for querying fundamentally different data representations of the same entity. @@ -224,17 +231,17 @@ This returns the octad data _plus_ a cryptographic proof certificate asserting d |Relational queries |Yes |No |Multimodal queries |No |Yes -|Mutations (INSERT/UPDATE/DELETE) |Yes |No (API only) +|Mutations (INSERT/UPDATE/DELETE) |Yes |Legacy forms; Octad API preferred |JOINs |Yes |No (graph modality) -|Aggregation (GROUP BY, COUNT, SUM) |Yes |No +|Aggregation (GROUP BY, COUNT, SUM) |Yes |Yes |Subqueries |Yes |No |PROOF verification |No |Yes |Federation with drift policies |No |Yes |Graph traversal |No (or extensions) |Yes (native) |Vector similarity |No (or extensions) |Yes (native) |Full-text search |Extensions |Yes (native) -|Ordering (ORDER BY) |Yes |No +|Ordering (ORDER BY) |Yes |Yes |Pagination (LIMIT/OFFSET) |Yes |Yes |=== -VCL is not a replacement for SQL. It is a purpose-built query language for a multimodal database that treats entities as six simultaneous representations rather than rows in flat tables. Use SQL when you need relational algebra. Use VCL when you need to query across modalities with optional formal verification. +VCL is not a replacement for SQL. It is a purpose-built query language for a multimodal database that treats entities as eight simultaneous modal representations (an *octad*) rather than rows in flat tables. Use SQL when you need relational algebra. Use VCL when you need to query across modalities with optional formal verification. diff --git a/docs/vcl-vs-vcl-dt.adoc b/docs/vcl-vs-vcl-dt.adoc index dc526be8..0c76bd58 100644 --- a/docs/vcl-vs-vcl-dt.adoc +++ b/docs/vcl-vs-vcl-dt.adoc @@ -120,6 +120,31 @@ generated. At L10, the proof certificate is assembled and attached to the result == The Six PROOF Types +[WARNING] +==== +*The six types enumerated below do not match the normative grammar, and this +page has deliberately not been rewritten to make them match.* + +`spec/grammar.ebnf` v3.0 and `src/vcl/VCLParser.affine` define: + + proof_type = 'EXISTENCE' | 'CITATION' | 'ACCESS' | 'INTEGRITY' + | 'PROVENANCE' | 'CUSTOM' ; + +Three subsections below instead name `CONSISTENCY`, `FRESHNESS` and +`AUTHORIZATION`, which are not grammar terminals; and the grammar's `CITATION`, +`ACCESS` and `CUSTOM` have no subsection here. `link:VCL-SPEC.adoc[VCL-SPEC.adoc]` +records this as known inconsistency #2 and rules that the specification follows +the grammar and implementation. + +Which side is the target is an *open owner decision*, not a documentation edit: +either the grammar is right and these three subsections describe proof types that +were never implemented, or this page describes an intended v-next proof set and +the grammar is behind. Rewriting six normative subsections in either direction +would silently pick a winner, so the divergence is flagged rather than resolved. +Until that decision lands, treat the grammar as authoritative for what a VCL +statement will actually accept today. +==== + Every `PROOF` clause takes the form `PROOF ()`: === EXISTENCE diff --git a/spec/grammar.ebnf b/spec/grammar.ebnf index 625d3dd1..da5c47e0 100644 --- a/spec/grammar.ebnf +++ b/spec/grammar.ebnf @@ -6,6 +6,24 @@ (* Version: 3.0 — Octad (8 modalities), provenance conditions, spatial conditions *) (* Date: 2026-02-27 *) +(* ------------------------------------------------------------------------ + DUPLICATE-GRAMMAR NOTICE (added 2026-09-27) + Two copies of this normative grammar are committed: + * spec/grammar.ebnf <- THIS FILE, treated as canonical + * docs/vcl-grammar.ebnf <- near-duplicate in the docs tree + They were byte-identical in substance; the only differences were this + file's @taxonomy and copyright lines and a stale "VQL" wording in the + case-insensitivity comment below (now corrected to "VCL"). + This file is treated as canonical because it carries the @taxonomy tag, + carries the copyright line, and is the copy cited by README.adoc, + EXPLAINME.adoc, 0-AI-MANIFEST.a2ml and spec/system-specs.adoc. + Maintaining two normative grammars is a drift hazard, not a feature: + any future edit MUST be applied to both, or the duplicate retired. + Consolidating them (deleting one and leaving a pointer) is an owner + decision, because deleting a normative artefact is not a documentation + edit. Tracked in ULTRAPLAN-2026-09-27.adoc. + ------------------------------------------------------------------------ *) + (* ============================================================================ 1. TOP-LEVEL STRUCTURE ============================================================================ *) @@ -294,7 +312,7 @@ comment = '--', { ? any character except newline ? }, '\n' (* Line comment *) (* ============================================================================ 12. RESERVED KEYWORDS ============================================================================ *) -(* Keywords are case-insensitive in VQL *) +(* Keywords are case-insensitive in VCL *) keywords = 'SELECT' | 'FROM' | 'WHERE' | 'PROOF' | 'LIMIT' | 'OFFSET' | 'GRAPH' | 'VECTOR' | 'TENSOR' | 'SEMANTIC' | 'DOCUMENT' | 'TEMPORAL' | 'PROVENANCE' | 'SPATIAL' | 'HEXAD' | 'FEDERATION' | 'STORE' From d997490b021acb96fc43164692e3ed115945d156 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 27 Sep 2026 09:55:10 +0000 Subject: [PATCH 3/4] ci(#204): add a fail-closed relative-link gate, with a positive control that proves it can fail A gate that passes on a tree with zero broken links is indistinguishable from a gate that does nothing. So this lands as a pair. scripts/check-doc-links.sh resolves every relative link: macro target in *.adoc (and [text](target) in *.md) against the working tree. Handles AsciiDoc passthrough quoting, and skips in-document anchors and absolute URLs, which are not filesystem claims. scripts/doc-links-allowlist.txt exemptions, with a required reason. Currently empty: nothing is exempt. Putting suppressions in a separate file means silencing a link is a visible, reviewable diff rather than an inline comment nobody reads. tests/doc-links-gate.sh positive control, modelled on the existing assail-classifications-gate.sh pattern so it is idiomatic here. Plants a broken link in a scratch copy and asserts four things: the real tree resolves, the planted link is rejected, the rejection names the planted target AND its resolved path, and a resolving sibling in the same file is not flagged. Current state: 364 relative links resolve across 101 documents, 0 exempt. Both are wired into .github/workflows/doc-consonance.yml, renamed "Documentation Gates". The positive control runs after the real gate so a genuine break is reported first. No new actions are introduced, so .github/workflows/actions.lock needs no change -- which matters, because SHA-pinning workflows sits inside the P1 carve-out of the TPCF perimeter and is not this branch's to touch. check-doc-links.sh walks the filesystem, so it sees new documents immediately. tests/doc-consonance-gate.sh is amended in the same commit because it does NOT: it runs `git grep`, which searches the index. Every document added by this branch was untracked while being written, so that gate reported PASS throughout and then failed the moment the files were committed -- on FAQ.adoc and on ULTRAPLAN-2026-09-27.adoc. Two earlier PASS results were measured against a tree that excluded the very files being added. A gate blind to new files is silent precisely when new prose appears, which is when it is most needed; recorded as a follow-up in the ULTRAPLAN rather than fixed here, since changing its traversal is a gate-semantics decision. The two failures it caught were resolved differently, on purpose: * ULTRAPLAN-2026-09-27.adoc quoted the misnomer in a results table describing the gate in the gate's own words. That added nothing, so it was reworded. * FAQ.adoc quotes it to explain that the name is *Consonance* and not *Query*. Naming the thing being retired is the substance of that answer, which is the exact case the gate's ALLOW list exists for -- this file, CHANGELOG and the cross-thread quarantine directive are already exempt for the same reason. FAQ.adoc was added to ALLOW with the reasoning inline. The exemption is file-scoped, not line-scoped, so it would also permit the misnomer elsewhere in FAQ.adoc. That coarseness is pre-existing in the gate's design and is accepted here because the term now appears exactly once in that file, inside the IMPORTANT block explaining its retirement. A positive control confirms the widened exemption is still narrow: a misnomer planted in a non-exempt file is caught. FAQ.adoc's gate list is also corrected -- it credited tests/doc-links-gate.sh with failing the build on a broken link, when that is scripts/check-doc-links.sh and the test file is its positive control. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/doc-consonance.yml | 19 ++- FAQ.adoc | 11 +- ULTRAPLAN-2026-09-27.adoc | 28 +++- scripts/check-doc-links.sh | 216 +++++++++++++++++++++++++++ scripts/doc-links-allowlist.txt | 0 tests/doc-consonance-gate.sh | 15 +- tests/doc-links-gate.sh | 93 ++++++++++++ 7 files changed, 375 insertions(+), 7 deletions(-) create mode 100755 scripts/check-doc-links.sh create mode 100644 scripts/doc-links-allowlist.txt create mode 100755 tests/doc-links-gate.sh diff --git a/.github/workflows/doc-consonance.yml b/.github/workflows/doc-consonance.yml index 3696a132..089a8547 100644 --- a/.github/workflows/doc-consonance.yml +++ b/.github/workflows/doc-consonance.yml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: MPL-2.0 # This workflow is managed by gh actions-lock. # This workflow is managed by gh actions-lock. -name: Doc Consonance Gate +name: Documentation Gates on: push: @@ -18,5 +18,22 @@ jobs: timeout-minutes: 10 steps: - uses: actions/checkout@v7.0.1 + - name: Doc-consonance gate (no query-language misnomer in docs) run: bash tests/doc-consonance-gate.sh + + # Added 2026-09-27 for issue #204. Every relative link:…[] target in the + # documentation set must resolve against the working tree. Exemptions go + # in scripts/doc-links-allowlist.txt (currently empty — nothing is + # exempt), so a suppression is a visible, reviewable edit rather than an + # inline comment. + - name: Doc-links gate (every relative link resolves) + run: bash scripts/check-doc-links.sh + + # The gate above passes on a tree with zero broken links, which is also + # what a no-op gate would do. This positive control proves the gate can + # actually fail: it plants a broken link in a scratch copy and asserts the + # gate rejects it, names the right target, and does not flag a resolving + # sibling. Runs after the real gate so a genuine break is reported first. + - name: Doc-links gate positive control + run: bash tests/doc-links-gate.sh diff --git a/FAQ.adoc b/FAQ.adoc index ff8651f2..e85f65fc 100644 --- a/FAQ.adoc +++ b/FAQ.adoc @@ -331,10 +331,13 @@ link:CONTRIBUTING.adoc[`CONTRIBUTING.adoc`] The gates that actually block: * *`reuse lint`* — every file needs copyright and licence information. -* *`tests/doc-consonance-gate.sh`* — the string "VeriSim Query Language" in any - doc fails the build. -* *`tests/doc-links-gate.sh`* — a broken relative link in any `*.adoc` fails the - build. +* *`tests/doc-consonance-gate.sh`* — the retired query-language misnomer, in any + tracked `*.adoc`, `*.md` or `*.a2ml`, fails the build. See the note above for + the small list of files exempted because they have to name it in order to + explain its retirement. +* *`scripts/check-doc-links.sh`* — a relative link whose target does not resolve + fails the build. `tests/doc-links-gate.sh` is its positive control: it plants a + broken link in a scratch copy to prove the gate can actually fail. * *`coq-build.yml`* — per-module `Print Assumptions` whitelists; an unexpected axiom fails. * *`tests/assail-classifications-gate.sh`* — every `(file …)` key in diff --git a/ULTRAPLAN-2026-09-27.adoc b/ULTRAPLAN-2026-09-27.adoc index 4bc28d24..c2994800 100644 --- a/ULTRAPLAN-2026-09-27.adoc +++ b/ULTRAPLAN-2026-09-27.adoc @@ -88,7 +88,7 @@ as a design document with a scope verdict, not as code. |`doc-consonance-gate.sh` |PASS -|no `VeriSim Query Language` misnomer in docs +|no retired query-language misnomer in any tracked `*.adoc` / `*.md` / `*.a2ml` |`assail-classifications-gate.sh` |PASS @@ -559,6 +559,25 @@ comment/metadata edits are not compiled here |no `formal/*.v` change is made by this plan |=== +[WARNING] +==== +*`doc-consonance-gate.sh` cannot see untracked files.* It runs `git grep`, which +searches the index, not the working tree. Every new document in this plan was +untracked while it was being written, so the gate reported PASS throughout — and +then failed the moment those files were committed, on `FAQ.adoc` and on this +document. Two of the PASS results recorded in the table above were therefore +measured against a tree that *excluded the very files this plan added*. + +This is a real weakness, not a curiosity: a gate that goes blind to new files is +silent exactly when new prose is being introduced, which is when it is most +needed. The failure was caught here only because the sweep was re-run after +committing. Fixing it means either committing before verifying, or switching the +gate to walk the working tree. Tracked as a follow-up in part 8. + +Note that `scripts/check-doc-links.sh` does *not* share this defect — it walks +the filesystem, so it saw the new documents immediately. +==== + Two self-inflicted regressions were caught by the gates during execution and are worth recording, because both are the same failure mode — *writing a literal marker into prose makes a text-level gate believe the prose is data*: @@ -571,6 +590,13 @@ by wrapping the illustrative malformed-header listing in `CHANGELOG.adoc` entry *describing* the doc-links gate made that gate report a broken link in the file announcing it. Fixed by naming the macro without the bracket. The gate was right to fail; it had been in place for about four minutes. +. `FAQ.adoc` and this document both quoted the retired query-language misnomer — +`FAQ.adoc` because explaining a retirement means naming the retired thing, this +document because a results table described the gate in the gate's own words. The +first is the legitimate case the gate's `ALLOW` list exists for, so `FAQ.adoc` +was added to it with the reasoning recorded inline; the second added nothing and +was simply reworded. A positive control confirmed the widened exemption is still +narrow: a misnomer planted in a non-exempt file is caught. [WARNING] ==== diff --git a/scripts/check-doc-links.sh b/scripts/check-doc-links.sh new file mode 100755 index 00000000..b235f7da --- /dev/null +++ b/scripts/check-doc-links.sh @@ -0,0 +1,216 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-doc-links.sh — fail-closed guard against broken relative links in docs. +# +# WHY THIS EXISTS +# On 2026-09-27 the tree carried 66 broken relative links across *.adoc, 43 of +# them `.md` -> `.adoc` renames that were never propagated to the documents +# pointing at them. Nothing caught this: doc-consonance-gate.sh checks for a +# banned *string*, and the estate governance `docs` job checks only that +# README / LICENSE / CONTRIBUTING *exist*. A link to a file that was renamed is +# invisible to both. This is the same failure shape as the assail +# classification registry drift (issue #203): a rename silently invalidates a +# reference, and the reference outlives the thing it pointed at. +# +# SCOPE +# AsciiDoc `link:TARGET[...]` macros and Markdown `[text](TARGET)` links in +# *.adoc and *.md tracked by git. Relative filesystem targets only. +# +# Deliberately NOT checked: +# * http/https/mailto — external, and a network probe in CI would make this +# gate flaky and slow for no local benefit. +# * in-document anchors (`link:#section`, `link:++#section++`, `xref:`) — +# resolving an AsciiDoc section id to its generated anchor requires an +# AsciiDoc processor, and a wrong answer here would be worse than no +# answer. Fragment-only targets are skipped; a target with both a path and +# a fragment has its *path* checked, which is the part that rots. +# * `include::` directives — separate concern, separate gate. +# +# ALLOWLIST +# Targets listed in scripts/doc-links-allowlist.txt are exempt. Each line needs +# a `#` reason, because an unexplained exemption is how a gate stops meaning +# anything. Blank lines and whole-line comments are ignored. +# +# USAGE +# scripts/check-doc-links.sh # check the working tree +# scripts/check-doc-links.sh # check an alternate root (for tests) +# +# EXIT +# 0 — every relative link resolves (or is exempt with a reason) +# 1 — at least one broken link; the full list is printed + +set -euo pipefail + +REPO_ROOT=$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd) +SCAN_ROOT=${1:-$REPO_ROOT} +ALLOWLIST="$REPO_ROOT/scripts/doc-links-allowlist.txt" + +if [[ ! -d "$SCAN_ROOT" ]]; then + echo "ERROR: scan root does not exist: $SCAN_ROOT" >&2 + exit 2 +fi + +if ! command -v python3 >/dev/null 2>&1; then + # Fail closed. A missing interpreter must not read as a clean pass; that is + # the same trap deny.toml warns about with an unpopulated advisory database. + echo "ERROR: python3 missing on runner — cannot check doc links" >&2 + exit 2 +fi + +SCAN_ROOT="$SCAN_ROOT" ALLOWLIST="$ALLOWLIST" python3 - <<'PY' +import os +import re +import sys + +root = os.environ["SCAN_ROOT"] +allowlist_path = os.environ.get("ALLOWLIST", "") + +# AsciiDoc link macro: link:TARGET[text] (TARGET cannot contain [ ] or whitespace) +ADOC_LINK = re.compile(r"(?", str(exc))) + continue + + base = os.path.dirname(path) + patterns = (ADOC_LINK,) if path.endswith(".adoc") else (MD_LINK,) + for pattern in patterns: + for match in pattern.finditer(text): + raw_target = match.group(1) + if raw_target.startswith(EXTERNAL): + continue + if is_fragment_only(raw_target): + continue + target = normalise(raw_target) + if not target: + continue + line_no = text.count("\n", 0, match.start()) + 1 + + if target in allowed: + exempt += 1 + continue + + resolved = os.path.normpath(os.path.join(base, target)) + checked += 1 + if os.path.exists(resolved): + continue + + # A rename is the overwhelmingly common cause, so name the likely + # fix rather than just reporting the miss. + stem, ext = os.path.splitext(resolved) + suggestion = "" + for alt in (".adoc", ".md", ".pdf", ".html", ".txt", ".ttl", ".rdf", ""): + if alt == ext: + continue + if os.path.exists(stem + alt): + suggestion = f" (did you mean `{os.path.relpath(stem + alt, root)}`?)" + break + broken.append( + ( + os.path.relpath(path, root), + f"{line_no}: link:{raw_target}", + f"missing {os.path.relpath(resolved, root)}{suggestion}", + ) + ) + +if allowed.get("__malformed__"): + print("ERROR: allowlist is malformed; refusing to treat it as authoritative", file=sys.stderr) + sys.exit(2) + +if broken: + print(f"FAIL doc-links: {len(broken)} broken relative link(s) in {len(doc_paths)} documents") + for path, where, why in broken: + print(f" {path} {where} -> {why}") + print() + print("Fix the target, or add it to scripts/doc-links-allowlist.txt WITH a reason.") + print("An exemption without a reason is how a gate stops meaning anything.") + sys.exit(1) + +print( + f"PASS doc-links: {checked} relative link(s) resolve across {len(doc_paths)} documents" + f" ({exempt} exempt with reason)" +) +PY diff --git a/scripts/doc-links-allowlist.txt b/scripts/doc-links-allowlist.txt new file mode 100644 index 00000000..e69de29b diff --git a/tests/doc-consonance-gate.sh b/tests/doc-consonance-gate.sh index fa7dbf02..1f08fcfd 100755 --- a/tests/doc-consonance-gate.sh +++ b/tests/doc-consonance-gate.sh @@ -21,7 +21,20 @@ GREEN='\033[0;32m'; RED='\033[0;31m'; NC='\033[0m' # Files that legitimately name the legacy term: this gate, the changelog # history, and the cross-thread quarantine directive (which explains it). -ALLOW='tests/doc-consonance-gate.sh|CHANGELOG|cross-thread-quarantine' +# +# FAQ.adoc was added 2026-09-27. Its "What is VCL?" entry has to quote the +# retired expansion in order to tell a reader that the name is *Consonance* and +# not *Query* -- naming the thing being retired is the substance of that answer, +# not an accident of prose. That is the same reason this file and the quarantine +# directive are exempt. +# +# Honest caveat: the exemption is file-scoped, not line-scoped, so it would also +# permit the misnomer to creep into FAQ.adoc elsewhere. That coarseness is +# pre-existing in this gate's design (CHANGELOG is exempt the same way) and is +# accepted here because the term appears exactly once in FAQ.adoc, inside the +# IMPORTANT block that explains its retirement. A per-line exemption marker would +# be strictly better and is noted in ULTRAPLAN-2026-09-27.adoc as a follow-up. +ALLOW='tests/doc-consonance-gate.sh|CHANGELOG|cross-thread-quarantine|FAQ\.adoc' hits=$(git grep -n 'VeriSim Query Language' -- '*.adoc' '*.md' '*.a2ml' 2>/dev/null | grep -vE "$ALLOW" || true) diff --git a/tests/doc-links-gate.sh b/tests/doc-links-gate.sh new file mode 100755 index 00000000..8ed58235 --- /dev/null +++ b/tests/doc-links-gate.sh @@ -0,0 +1,93 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# doc-links-gate.sh — positive-control test for the relative-link gate. +# +# Same shape as tests/assail-classifications-gate.sh: run the real gate first, +# then plant a known-bad fixture in a scratch tree and assert the gate (a) fails +# and (b) fails for the RIGHT reason. A gate that rejects everything would pass +# test (a) alone; the reason-match is what makes this a positive control rather +# than a smoke test. +# +# WHY: on 2026-09-27 the tree carried 66 broken relative links, 43 of them +# `.md` -> `.adoc` renames that were never propagated. Nothing caught them. +# This test exists so that the thing which now catches them is itself caught if +# it stops working. + +set -euo pipefail + +REPO_ROOT=$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd) +CHECKER="$REPO_ROOT/scripts/check-doc-links.sh" +FIXTURE_DIR=$(mktemp -d "${TMPDIR:-/tmp}/verisimdb-doc-links.XXXXXX") +trap 'rm -rf -- "$FIXTURE_DIR"' EXIT + +if [[ ! -x "$CHECKER" ]]; then + echo "ERROR: checker is not executable: $CHECKER" >&2 + exit 1 +fi + +# --- 1. The real tree must pass ------------------------------------------------ +echo "[1/4] checking the working tree..." +"$CHECKER" "$REPO_ROOT" + +# --- 2. Plant a broken link in a scratch tree --------------------------------- +echo "[2/4] planting a known-broken relative link..." +mkdir -p "$FIXTURE_DIR/docs" +cat > "$FIXTURE_DIR/docs/planted.adoc" <<'EOF' += Planted fixture +:toc: left + +A link that resolves, and one that does not. + +* link:real-target.adoc[this one exists] +* link:RENAMED-AWAY.md[this one does not] +EOF +cat > "$FIXTURE_DIR/docs/real-target.adoc" <<'EOF' += Real target +EOF + +# --- 3. Assert it FAILS ------------------------------------------------------- +echo "[3/4] asserting the gate rejects it..." +set +e +output=$("$CHECKER" "$FIXTURE_DIR" 2>&1) +result=$? +set -e + +if (( result == 0 )); then + echo "ERROR: link gate accepted a planted broken link" >&2 + echo " A gate that passes this is not checking anything." >&2 + exit 1 +fi + +# --- 4. Assert it fails for the RIGHT reason ---------------------------------- +echo "[4/4] asserting it failed for the right reason..." +if [[ "$output" != *"link:RENAMED-AWAY.md"* ]]; then + echo "ERROR: gate failed but did not name the planted target" >&2 + echo " (it may be failing on something unrelated, which is not a pass)" >&2 + echo "--- gate output ---" >&2 + echo "$output" >&2 + exit 1 +fi + +if [[ "$output" != *"docs/RENAMED-AWAY.md"* ]]; then + echo "ERROR: gate did not report the resolved missing path" >&2 + echo "--- gate output ---" >&2 + echo "$output" >&2 + exit 1 +fi + +# The sibling link must NOT be reported: a checker that flags everything is not a +# checker, and this is the assertion that distinguishes the two. +if [[ "$output" == *"real-target.adoc"* ]]; then + echo "ERROR: gate flagged a link that DOES resolve — it is over-reporting" >&2 + echo "--- gate output ---" >&2 + echo "$output" >&2 + exit 1 +fi + +echo "positive control passed:" +echo " - the working tree resolves" +echo " - a planted broken link is rejected" +echo " - the rejection names the planted target and its resolved path" +echo " - a resolving sibling link in the same file is NOT flagged" From 689a704998d6cd93c3d29e70ca610e1828114499 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 27 Sep 2026 12:26:08 +0000 Subject: [PATCH 4/4] docs(#204,#113): correct CONTRIBUTING.adoc, which had drifted further than README Found while checking this repo's PR conventions, so it was not in the original census. CONTRIBUTING.adoc carries its own copy of the repository-structure tree, and that copy had drifted further than the README block corrected in ff22d14: * "14 workspace members" -- Cargo.toml `members` declares 18: seventeen rust-core/verisim-* crates plus `benches`. * verisim-provenance, verisim-spatial and verisim-nif were missing entirely, which is how 17 became 14. * verisim-tensor described as "(Burn)". Burn was removed from the workspace in 0.2.0; it is ndarray only. This is the same stale claim corrected in .machine_readable/6a2/STATE.a2ml and Cargo.toml. * verisim-octad described as a "Unified 6-modal entity". It is an octad -- eight modalities. The modality-count drift the 2026-07-07 pass swept out of nine other documents had simply never reached this one. * A root `contractiles/` directory that does not exist. The contractiles live under `.machine_readable/contractiles/`. * `.machine_readable/` described as "SCM checkpoint files". It holds A2ML. The allowed-languages table listed *ReScript* as accepted for the VCL parser and playground, while the "Not Accepted" list directly below told contributors to use AffineScript instead of TypeScript. Both halves are now consistent with the tree: zero .res files remain, 32 .affine do. ReScript is recorded as retired, naming the two directory paths (connectors/clients/rescript/, playground/src/) that were deliberately not renamed because renaming a client-SDK directory is a consumer-visible break rather than a documentation edit. Idris2, Coq and Zig were also missing from the accepted-languages table despite all three being in active use under src/abi/, formal/ and ffi/zig/. A NOTE block records what was wrong and why, so the next reader does not have to re-derive it. Verified: reuse lint 809/809, doc-consonance PASS, doc-links PASS (364 links / 101 documents, 0 exempt) plus positive control, validate-a2ml.sh 32/32 with 0 warnings. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- CHANGELOG.adoc | 1 + CONTRIBUTING.adoc | 47 +++++++++++++++++++++++++++++++++++++---------- 2 files changed, 38 insertions(+), 10 deletions(-) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 67a5d57e..fdd0a91c 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -52,6 +52,7 @@ Issue #113 and the residue left by the 2026-07-07 docs-hygiene pass. - *`.machine_readable/6a2/README.adoc`*: "6 core A2ML files" → 7, listed the seventh, and corrected the standards-repo URL to its real `1-formats/a2ml` path. - *`Cargo.toml`*: the `quinn-proto` suppression note still described an open transitive chain. Replaced with the accurate closure (burn removed in 0.2.0, chain gone; `quinn` is absent from `Cargo.lock`). - Eight link *labels* whose targets had been fixed but whose display text still named the old file (`link:SECURITY.adoc[SECURITY.md]`) were synced. +- *`CONTRIBUTING.adoc`*: its repository-structure block claimed "14 workspace members" where `Cargo.toml` declares 18 (17 `rust-core/verisim-*` crates plus `benches`), and omitted `verisim-provenance`, `verisim-spatial` and `verisim-nif`. It described `verisim-tensor` as Burn-backed (Burn was removed in 0.2.0), called the octad a "6-modal entity" when it has eight, listed a root `contractiles/` directory that does not exist (they live under `.machine_readable/contractiles/`), and described `.machine_readable/` as holding "SCM checkpoint files". Its allowed-languages table listed *ReScript* while the adjacent "Not Accepted" list told contributors to use AffineScript instead — both are now correct, and ReScript is recorded as retired with the two historical directory names that were deliberately not renamed. === Removed diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index cd1a4529..ba118bfd 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -37,30 +37,49 @@ mix test .... verisimdb/ -├── rust-core/ # Rust crates (14 workspace members) +├── rust-core/ # Rust crates (17 of the 18 workspace members) │ ├── verisim-api/ # HTTP/gRPC API server -│ ├── verisim-graph/ # Graph modality (RDF/Property Graph) +│ ├── verisim-graph/ # Graph modality (SimpleGraphStore default, Oxigraph optional) │ ├── verisim-vector/ # Vector modality (HNSW) -│ ├── verisim-tensor/ # Tensor modality (Burn) +│ ├── verisim-tensor/ # Tensor modality (ndarray) │ ├── verisim-semantic/ # Semantic modality (CBOR proofs) │ ├── verisim-document/ # Document modality (Tantivy) │ ├── verisim-temporal/ # Temporal modality (versioning) -│ ├── verisim-octad/ # Unified 6-modal entity +│ ├── verisim-provenance/ # Provenance modality (hash-chain lineage) +│ ├── verisim-spatial/ # Spatial modality (R-tree geospatial) +│ ├── verisim-octad/ # Unified 8-modal entity (the octad) │ ├── verisim-drift/ # Drift detection │ ├── verisim-normalizer/ # Self-normalization │ ├── verisim-planner/ # Cost-based query planner │ ├── verisim-repl/ # Interactive VCL REPL │ ├── verisim-wal/ # Write-ahead log -│ └── verisim-storage/ # Storage backend abstraction +│ ├── verisim-storage/ # Storage backend abstraction +│ └── verisim-nif/ # Rustler NIF bridge (scaffold; see issue #61) +├── benches/ # Criterion benchmarks (the 18th workspace member) ├── elixir-orchestration/ # Elixir/OTP coordination layer -├── playground/ # VCL Playground PWA (ReScript) +├── src/ # AffineScript sources (VCL parser, registry, ABI) +├── playground/ # VCL Playground PWA (AffineScript) ├── container/ # Containerfile for Podman builds ├── docs/ # Architecture and design documents -├── contractiles/ # Trust, security, and policy contracts -├── .machine_readable/ # SCM checkpoint files +├── formal/ # Coq proofs (9 modules) +├── debugger/ # In-tree TUI debugger + ABI/FFI visualisation +├── .machine_readable/ # A2ML specs (6a2/, anchors/, contractiles/, …) └── .github/workflows/ # CI/CD pipelines .... +[NOTE] +==== +The 18th workspace member is `benches/`, not a crate; `Cargo.toml` `members` +lists 17 `rust-core/verisim-*` crates plus `benches`. An earlier revision of this +tree said "14 workspace members", omitted `verisim-provenance`, +`verisim-spatial` and `verisim-nif`, described `verisim-tensor` as Burn-backed +(Burn was removed from the workspace in 0.2.0 — it is ndarray only), called the +octad a "6-modal entity" when it has eight modalities, and listed a root +`contractiles/` directory that does not exist (the contractiles live under +`.machine_readable/contractiles/`). `.machine_readable/` holds A2ML artefacts, +not Scheme checkpoint files. +==== + ''''' === How to Contribute @@ -165,13 +184,21 @@ cargo fmt --check |Language |Use Case |*Rust* |Core database engine, modality stores, CLI tools |*Elixir* |OTP orchestration, distributed coordination -|*ReScript* |VCL parser, playground PWA -|*VCL* |VeriSim Consonance Language (query interface) +|*AffineScript* |VCL parser and type checker (`src/vcl/`), federation registry +(`src/registry/`), playground PWA +|*Idris2* |VCL-DT type checker / proof bridge; ABI definitions (`src/abi/`) +|*Coq* |Formal proofs (`formal/`, 9 modules) +|*Zig* |FFI implementation (`ffi/zig/`), SNIFs guest code +|*VCL* |VeriSim Consonance Language (the query interface itself) |=== ==== Not Accepted * TypeScript (use AffineScript instead) +* ReScript — retired in favour of AffineScript. Zero `.res` files remain in the + tree; 32 `.affine` files do. Two directory names are still historical + (`connectors/clients/rescript/`, `playground/src/`) and were deliberately not + renamed, because renaming a client-SDK directory is a consumer-visible break * Python (use Rust or Julia instead) * Go (use Rust instead) * Node.js/npm/bun (use Deno if JS runtime needed)