Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .github/SUPPORT.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,12 @@ 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

This is a solo-maintained project. Response times vary but issues are reviewed regularly.

## Contributing

See [CONTRIBUTING.md](../CONTRIBUTING.md) for contribution guidelines.
See [CONTRIBUTING.adoc](../CONTRIBUTING.adoc) for contribution guidelines.
19 changes: 18 additions & 1 deletion .github/workflows/doc-consonance.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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
12 changes: 12 additions & 0 deletions .machine_readable/6a2/0-AI-MANIFEST.a2ml
Original file line number Diff line number Diff line change
@@ -1,3 +1,15 @@
;; SPDX-License-Identifier: MPL-2.0
;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
;;
;; 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
Expand Down
5 changes: 3 additions & 2 deletions .machine_readable/6a2/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
# 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

Expand All @@ -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

25 changes: 20 additions & 5 deletions .machine_readable/6a2/STATE.a2ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"))

Expand All @@ -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
Expand All @@ -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"))
Expand Down Expand Up @@ -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")))

Expand Down
82 changes: 82 additions & 0 deletions .well-known/ai.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
# SPDX-License-Identifier: MPL-2.0
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
#
# 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
96 changes: 96 additions & 0 deletions .well-known/humans.txt
Original file line number Diff line number Diff line change
@@ -0,0 +1,96 @@
# SPDX-License-Identifier: MPL-2.0
# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
#
# 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
Loading