diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index b80728d..c53e41e 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -11,6 +11,10 @@ on: push: branches: [main, master] +concurrency: + group: rust-ci-${{ github.ref }} + cancel-in-progress: true + permissions: contents: read diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index c32021a..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,27 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/README.adoc b/README.adoc index d1b3683..ca3eddb 100644 --- a/README.adoc +++ b/README.adoc @@ -7,12 +7,19 @@ Jonathan D.A. Jewell :icons: font :source-highlighter: rouge +== Related repos + +* https://github.com/hyperpolymath/verisimdb-data[`verisimdb-data`] — + flat-file store for scan results and drift snapshots, and the dogfood + site for the hyperpolymath Idris2 + Zig ABI shared with `proven`, + `burble`, `gossamer`. Verisimiser does not require it. + == What Is This? VeriSimiser augments existing databases with capabilities from -https://github.com/hyperpolymath/nextgen-databases[VeriSimDB]'s octad model — -specifically the capabilities that work as genuine piggybacks without requiring -you to replace your database. +https://github.com/hyperpolymath/nextgen-databases[VeriSimDB]'s **octad +model** — eight concerns layered over any backend without forcing a +schema migration. **Honest framing**: this is not a pure bolt-on like the language -isers. Language -isers generate a separate wrapper alongside your code — one-way @@ -20,11 +27,13 @@ dependency, your code untouched. Database augmentation is fundamentally different because it interacts with shared mutable state. VeriSimiser is therefore split into two tiers: -* **Tier 1 (true piggyback)** — capabilities that sit alongside or in front - of your database, never touching its storage engine. These are safe bolt-ons. -* **Tier 2 (augmentation layer)** — capabilities that require additional - storage alongside your database. These are honest about being "VeriSimDB - with your database as one backend" rather than pretending to be invisible. +* **Tier 1 (true piggyback)** — concerns that sit alongside or in front + of your database, writing only to a sidecar and never touching your + storage engine. Safe bolt-ons. +* **Tier 2 (augmentation layer)** — modality overlays (graph, vector, + tensor, semantic, document, spatial) that require additional storage + alongside your database. Honest about being "VeriSimDB with your + database as one backend" rather than pretending to be invisible. == VeriSimDB's Octad: Eight Concerns @@ -49,40 +58,19 @@ identity; see "Tier 2" below.) | **Simulation** | "What if we changed this?" — sandbox branches that do not touch the main data. | Tier 2 |=== +The codebase commits to this ontology in +`src/abi/mod.rs::OctadDimension`, `src/manifest/mod.rs::OctadConfig`, +and the codegen tables. See `docs/decisions/ADR-0001-octad-ontology.adoc` +for why "concerns" was chosen over the alternative "modalities" framing. + == Tier 1: True Piggybacks These work like PostGIS — they add capability without replacing anything. -=== Cross-Modal Drift Detection - -The jewel of VeriSimDB. Drift detection monitors whether representations -of the same entity stay consistent across modalities. VeriSimiser can -overlay drift detection onto any database: - -* Your database stores the primary data (unchanged) -* VeriSimiser maintains a lightweight **drift index** alongside it -* Queries pass through to your database normally -* VeriSimiser intercepts results and checks for cross-modal inconsistencies -* Alerts when representations drift apart - -This is a **read-path augmentation** — it observes query results, it doesn't -modify them. Safe to add, safe to remove, no data dependency. - -VeriSimDB detects eight categories of cross-modal drift: - -1. Structural drift — schema changes not reflected across modalities -2. Semantic drift — meaning divergence between representations -3. Temporal drift — version skew between modalities -4. Statistical drift — distribution shift in vector/tensor spaces -5. Referential drift — broken links between graph and document modalities -6. Provenance drift — transformation chain inconsistencies -7. Spatial drift — coordinates inconsistent with other modalities -8. Embedding drift — vector embeddings stale relative to source documents - === Provenance Tracking Hash-chain verified origin tracking for every piece of data. VeriSimiser -can add provenance to any database as a sidecar: +adds provenance to any database as a sidecar: * Every write is intercepted and a provenance record created * SHA-256 hash chain links provenance records in order @@ -95,7 +83,7 @@ change what happened. The provenance chain is stored in a separate sidecar === Temporal Versioning -Automatic version history for entities. VeriSimiser can maintain a temporal +Automatic version history for entities. VeriSimiser maintains a temporal sidecar that records every state change: * Point-in-time queries: "what did this entity look like at time T?" @@ -103,67 +91,95 @@ sidecar that records every state change: * Rollback capability: restore any entity to a previous state * Retention policies: auto-prune history older than N days -This piggybacks onto write events (triggers, CDC, or application-level hooks) -and stores version history in a separate sidecar. +This piggybacks onto write events (triggers, CDC, or application-level +hooks) and stores version history in a separate sidecar. + +=== Constraints & Drift Detection + +The Constraints concern enforces cross-dimensional invariants and +observes *drift* — places where Data, Metadata, and any active Tier 2 +overlays disagree. Drift detection is a **read-path observer**: it +inspects query results, never modifies them. + +VeriSimiser tracks eight symptomatic categories (mapped onto the +Constraints concern): + +. **Structural drift** — schema changes not reflected across active overlays +. **Semantic drift** — meaning divergence between overlays +. **Temporal drift** — version skew between overlays +. **Statistical drift** — distribution shift in vector/tensor overlays +. **Referential drift** — broken links between the graph overlay and Data +. **Provenance drift** — transformation-chain inconsistencies +. **Spatial drift** — coordinates inconsistent with other overlays +. **Embedding drift** — vector embeddings stale relative to source documents + +(Each category needs a computable definition before it can be detected; +this is on the roadmap, not implemented yet.) + +=== Lineage + +Directed-edge graph of data derivation: which entity was derived from +which other entity, and by what transformation. Intended as a DAG (cycle +prevention enforcement is a future ADR). + +=== Access Control + +Row-level and column-level policies evaluated at query time. Independent +of any backend-native role system; verisimiser interprets policies and +filters/redacts results. == Tier 2: Augmentation Layer These capabilities require additional storage alongside your database. -They're honest about being "VeriSimDB modalities with your database as the -document/primary store." This is still valuable — it's how you get octad -capabilities incrementally — but it's not a bolt-on. +They are honest about being "VeriSimDB modalities with your database as +the document/primary store." This is still valuable — it's how you get +extra modality projections incrementally — but it's not invisible. -* **Graph overlay**: Add RDF triples and property graph edges to entities +* **Graph overlay**: Add RDF triples and property-graph edges to entities in your relational database. Stored in a separate graph index. -* **Vector overlay**: Add embeddings for similarity search. Stored in HNSW - index alongside your database. +* **Vector overlay**: Add embeddings for similarity search. Stored in + HNSW index alongside your database. * **Tensor overlay**: Add multi-dimensional numeric data. Stored in ndarray-backed sidecar. * **Semantic overlay**: Add type annotations and proof blobs. Stored in CBOR sidecar. +* **Document overlay**: Add full-text search over text columns. + Stored in a Tantivy index. * **Spatial overlay**: Add geospatial coordinates. Stored in R-tree sidecar. +* **Simulation**: Branched copies of data for what-if analysis. Stored + in `verisimdb_simulation_branches` + `_deltas`. -Each Tier 2 modality has its own storage and can be enabled independently. -Your primary database remains the source of truth for its native data. +Each Tier 2 overlay has its own storage and can be enabled +independently. Your primary database remains the source of truth for +its native data. == The Manifest [source,toml] ---- -[verisimiser] +[project] name = "my-augmented-db" +version = "0.1.0" [database] -target-db = "postgresql" -connection-string = "postgres://localhost/mydb" - -# Tier 1: true piggybacks (no additional storage in your database) -[tier1] -drift-detection = true # cross-modal drift monitoring -provenance = true # SHA-256 hash-chain audit trail -temporal-versioning = true # automatic version history - -[tier1.provenance] -sidecar = "sqlite" # sqlite | file | verisim -sidecar-path = ".verisimiser/provenance.db" - -[tier1.temporal] -sidecar = "sqlite" -retention-days = 90 - -# Tier 2: augmentation layer (additional storage alongside your database) -[tier2] -graph = false # RDF/property graph overlay -vector = false # embedding similarity search -tensor = false # multi-dimensional numeric -semantic = false # type annotations + proof blobs -spatial = false # geospatial coordinates - -[tier2.vector] -# model = "sentence-transformers/all-MiniLM-L6-v2" -# dimensions = 384 +backend = "sqlite" # sqlite | postgresql | mongodb +connection-string-env = "DATABASE_URL" # env var; never the literal secret +schema-source = "schema.sql" # optional; SQL DDL describing target schema + +[octad] +enable-provenance = true +enable-lineage = true +enable-temporal = true +enable-access-control = true +enable-simulation = false # Tier 2: branching/sandboxing + +[sidecar] +storage = "sqlite" # sqlite (default) | json +path = ".verisim/sidecar.db" ---- +Run `verisimiser init --database sqlite` to generate a starter manifest. + == Architecture [source] @@ -172,52 +188,73 @@ Your Application │ ├──── writes ────► Your Database (unchanged) │ │ - │ VeriSimiser intercepts + │ VeriSimiser intercepts (write-path observer) │ │ │ ┌─────────────┼──────────────┐ │ │ │ │ - │ Drift Index Provenance Temporal - │ (Tier 1) Sidecar Sidecar - │ (Tier 1) (Tier 1) + │ Provenance Temporal Lineage / AccessControl / + │ sidecar sidecar Constraints sidecars (Tier 1) │ - └──── optional ──► Tier 2 Sidecars - (Graph, Vector, Tensor, - Semantic, Spatial) + └──── optional ──► Tier 2 modality overlays + (Graph, Vector, Tensor, Semantic, + Document, Spatial, Simulation) ---- -**Interception methods** (configurable per database): +**Interception methods** (configurable per database — most are still +roadmap items, see `ROADMAP.adoc`): * **PostgreSQL**: logical replication / `pg_notify` / triggers * **SQLite**: `sqlite3_update_hook` / WAL monitoring * **MongoDB**: change streams * **Application-level**: middleware / ORM hooks +== ABI + +The Application Binary Interface for the augmentation layer is declared +in two languages: + +* `src/interface/abi/` — Idris2 type definitions + (`Types.idr`, `Layout.idr`, `Foreign.idr`). These are the canonical + shapes; formal proofs of correctness against them are future work + (see `docs/decisions/ADR-0002-verification-tree.adoc`). +* `src/interface/ffi/` — Zig C-compatible FFI implementing the Idris2 + ABI for use from native code. + +The Rust `src/abi/mod.rs` mirrors the Idris2 types as plain structs +used directly by the CLI and codegen. + == Relationship to VeriSimDB VeriSimiser is NOT a replacement for VeriSimDB. It's a gateway drug. -* **VeriSimiser Tier 1** gives you drift detection, provenance, and temporal - versioning on your existing database. Zero commitment. -* **VeriSimiser Tier 2** gives you individual octad modalities as sidecars. - Incremental adoption. -* **Full VeriSimDB** gives you the complete octad with native cross-modal - querying, VCL, and built-in drift normalisation. Full commitment. +* **VeriSimiser Tier 1** gives you provenance, temporal, lineage, + access control, and constraints/drift detection on your existing + database. Zero commitment. +* **VeriSimiser Tier 2** gives you individual modality overlays + (graph/vector/tensor/semantic/document/spatial) and simulation as + sidecars. Incremental adoption. +* **Full VeriSimDB** gives you the complete model with native + cross-modal querying, VCL, and built-in drift normalisation. Full + commitment. -The migration path is: Tier 1 → Tier 2 → full VeriSimDB (if you want it). -Most users will be happy at Tier 1 or Tier 2. +The migration path is: Tier 1 → Tier 2 → full VeriSimDB (if you want +it). Most users will be happy at Tier 1 or Tier 2. == Integration with TypedQLiser -VeriSimiser works alongside https://github.com/hyperpolymath/typedqliser[TypedQLiser]: +VeriSimiser works alongside +https://github.com/hyperpolymath/typedqliser[TypedQLiser]: * TypedQLiser type-checks your queries (compile-time, no runtime cost) -* VeriSimiser augments your database with octad capabilities (runtime) +* VeriSimiser augments your database with octad concerns (runtime) * Together: formally verified queries against an augmented database == Status -**Pre-alpha.** Architecture defined, tier system designed. Tier 1 (drift -detection, provenance, temporal versioning) is the priority implementation. +**Pre-alpha.** Architecture defined, octad ontology pinned (ADR-0001), +codegen scaffolding in place. The next implementation milestone is V-L1-C1: +end-to-end SQLite Tier 1 piggyback (`sqlite3_update_hook` → +`verisimdb_provenance_log` sidecar). See `ROADMAP.adoc`. Part of the https://github.com/hyperpolymath/iseriser[-iser family]. **#3 priority** (after TypedQLiser and Chapeliser). diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 7f0565f..92748b8 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -4,35 +4,78 @@ :toc: :icons: font +The phases below are stated in terms of the *concerns* octad +(Data, Metadata, Provenance, Lineage, Constraints, AccessControl, +Temporal, Simulation) per `docs/decisions/ADR-0001-octad-ontology.adoc`. +Tier 2 *modalities* (graph, vector, tensor, semantic, document, spatial) +are independent overlay representations layered on top. + == Phase 0: Scaffold (COMPLETE) -* [x] RSR template with full CI/CD (17 workflows) -* [x] CLI with subcommands (init, start, drift, provenance, history, status, octad) -* [x] Manifest parser (verisimiser.toml with tier1/tier2 config) -* [x] Tier 1 data types (DriftReport, ProvenanceRecord, TemporalVersion) -* [x] ABI module stubs (Idris2 + Zig FFI) -* [x] README with two-tier architecture and honest framing - -== Phase 1: PostgreSQL Tier 1 MVP + +* [x] RSR template with full CI/CD +* [x] CLI with subcommands (init, generate, start, drift, provenance, + history, status, octad) +* [x] Manifest parser (`verisimiser.toml` with `[octad]` toggles + + legacy `tier1`/`tier2` back-compat) +* [x] ABI types in Rust (`src/abi/mod.rs`) + Idris2 declarations + (`src/interface/abi/`) + Zig FFI stubs (`src/interface/ffi/`) +* [x] Codegen for sidecar overlay schema and query interceptor SQL +* [x] README + ADRs covering octad ontology, verification tree, + Justfile recipes + +== Phase 1: SQLite Tier 1 MVP + +The shortest end-to-end loop: SQLite target, SQLite sidecar, provenance ++ temporal concerns. Sequencing follows the bottom-up issue plan in +`docs/decisions/` (forthcoming). + +* [ ] SQLite interception via `sqlite3_update_hook` +* [ ] Provenance sidecar — write-path observer, SHA-256 hash chain + covering operation + actor + before-snapshot + transformation (not + just operation + ts) +* [ ] Temporal sidecar — version history, point-in-time read, + rollback, partial-unique-index enforcement of "exactly one current" +* [ ] Property tests for hash-chain integrity, version ordering, and + sidecar isolation (Tier 1 never writes to target) +* [ ] `verisimiser doctor` + `verisimiser validate` subcommands +* [ ] Structured logging (`tracing`), `--log-format=json|pretty` + +== Phase 2: PostgreSQL Tier 1 + * [ ] PostgreSQL logical replication interception -* [ ] Provenance sidecar (SQLite) — write-path observer -* [ ] SHA-256 hash-chain integrity for provenance records -* [ ] Temporal versioning sidecar — point-in-time queries -* [ ] Cross-modal drift detection — read-path observer -* [ ] Drift index with 8-category classification -* [ ] Idris2 ABI proofs: sidecar isolation, hash-chain integrity, version ordering -* [ ] Zig FFI bridge: database connection, overlay operations, VCL-total queries -* [ ] End-to-end test: PostgreSQL -> verisimiser overlay -> VCL-total query - -== Phase 2: Multi-Backend Support -* [ ] SQLite interception via sqlite3_update_hook / WAL monitoring +* [ ] Provenance + temporal sidecars against PG target +* [ ] Idris2 ABI proofs: sidecar isolation, hash-chain integrity, + version ordering +* [ ] Zig FFI bridge: database connection, overlay operations + +== Phase 3: Multi-Backend Support + * [ ] MongoDB interception via change streams -* [ ] Redis interception via keyspace notifications -* [ ] MySQL interception via binlog CDC * [ ] Application-level middleware / ORM hooks * [ ] Backend-agnostic interception trait abstraction * [ ] Per-backend integration tests +* [ ] MySQL (binlog CDC) / Redis (keyspace notifications) — only if + there is real demand; the manifest enum currently excludes them. + +== Phase 4: Constraints / Drift Detection + +* [ ] Per-category drift definition (one ADR per category) +* [ ] First implemented category: Temporal drift (version skew — + cheapest to define and observe) +* [ ] Drift index storage + query API +* [ ] `verisimiser drift` subcommand wired to real measurements + +== Phase 5: AccessControl + Lineage + +* [ ] AccessControl model ADR: principals, role composition, deny vs + allow precedence, view interaction +* [ ] Typed policy condition language (replace free-form SQL TEXT) +* [ ] Lineage DAG enforcement: self-edge CHECK + cycle prevention + ADR +* [ ] Lineage traversal subcommand (upstream/downstream) + +== Phase 6: Tier 2 Modality Overlays -== Phase 3: Tier 2 Overlays * [ ] Graph overlay (RDF triples / property graph edges) * [ ] Vector overlay (HNSW embedding similarity search) * [ ] Tensor overlay (ndarray multi-dimensional numeric data) @@ -41,26 +84,37 @@ * [ ] Spatial overlay (R-tree geospatial coordinates) * [ ] Independent enable/disable per overlay via manifest -== Phase 4: VCL-total Integration +== Phase 7: Simulation + +* [ ] Branching semantics ADR (isolation, merge policy, conflict + resolution) +* [ ] FK enforcement on `simulation_branches.parent_branch` +* [ ] `verisimiser simulate` subcommand + +== Phase 8: VCL-total Integration + * [ ] VCL-total type-safe query parsing -* [ ] Cross-tier queries (Tier 1 + Tier 2 in single query) +* [ ] Cross-concern queries (Tier 1 + Tier 2 in single query) * [ ] TypedQLiser integration for compile-time query validation * [ ] Query planner for multi-sidecar operations * [ ] Performance benchmarks: overhead of augmentation layer -== Phase 5: Production Hardening -* [ ] Retention policies (auto-prune temporal history) +== Phase 9: Production Hardening + +* [ ] Retention policies (`[retention]` section in manifest) * [ ] Sidecar compaction and garbage collection -* [ ] Concurrent access safety (multi-writer provenance chains) +* [ ] Concurrent access safety (multi-writer provenance chains — + per-entity serialisation + UNIQUE(entity_id, previous_hash)) * [ ] Backup and restore for sidecars * [ ] Monitoring and alerting integration * [ ] Error recovery and graceful degradation * [ ] Shell completions (bash, zsh, fish) -== Phase 6: Ecosystem -* [ ] PanLL panel for drift monitoring dashboard +== Phase 10: Ecosystem + * [ ] BoJ-server cartridge (MCP integration) -* [ ] SqueakWell integration (database recovery via cross-modal constraint propagation) -* [ ] Migration tooling: Tier 1 -> Tier 2 -> full VeriSimDB +* [ ] SqueakWell integration (database recovery via cross-concern + constraint propagation) +* [ ] Migration tooling: Tier 1 → Tier 2 → full VeriSimDB * [ ] Publish to crates.io * [ ] Chainguard container image diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index ca3ebc8..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,21 +0,0 @@ -# Security Policy - -## Supported Versions - -| Version | Supported | -|---------|-----------| -| 0.1.x | ✅ | - -## Reporting a Vulnerability - -Please report security vulnerabilities to: j.d.a.jewell@open.ac.uk - -Do NOT open a public issue for security vulnerabilities. - -## Response Time - -We aim to respond within 48 hours and provide a fix within 7 days for critical issues. - -## Scope - -This policy covers the verisimiser CLI tool and its generated artifacts. diff --git a/docs/decisions/ADR-0001-octad-ontology.adoc b/docs/decisions/ADR-0001-octad-ontology.adoc new file mode 100644 index 0000000..4d29be0 --- /dev/null +++ b/docs/decisions/ADR-0001-octad-ontology.adoc @@ -0,0 +1,102 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += ADR-0001: Canonical octad ontology — concerns, not modalities +:revdate: 2026-05-13 +:status: Accepted + +== Status + +Accepted — 2026-05-13. + +Resolves: https://github.com/hyperpolymath/verisimiser/issues/19[V-L1-A1]. + +Closes as wontfix: https://github.com/hyperpolymath/verisimiser/issues/21[V-L1-A3] (the modalities-first refactor). + +Unblocks: https://github.com/hyperpolymath/verisimiser/issues/20[V-L1-A2] (the README rewrite). + +== Context + +Two competing ontologies have lived in this repository under the same name +("octad"): + +Modalities octad (README §"VeriSimDB's Octad: Eight Modalities"):: +Graph · Vector · Tensor · Semantic · Document · Temporal · Provenance · Spatial. +These are *representations* of an entity — how the same data is stored in +different shapes. The README's eight cross-modal drift categories +(structural, semantic, temporal, statistical, referential, provenance, +spatial, embedding) presuppose this ontology. + +Concerns octad (`src/abi/mod.rs::OctadDimension`, `src/manifest/mod.rs::OctadConfig`, `src/main.rs::print_octad`):: +Data · Metadata · Provenance · Lineage · Constraints · AccessControl · +Temporal · Simulation. These are *concerns/aspects* of data — what you +want to know or enforce about it. + +The code commits to the concerns octad; the README leads with the modalities +octad. A user cannot answer "what does an octad-augmented entity look like?" +without picking one. + +== Decision + +The *concerns* octad is canonical. + +The eight dimensions of the verisimiser octad are: + +. **Data** — the original entity as stored in the target database. +. **Metadata** — schema and type information. +. **Provenance** — SHA-256 hash-chain tracking of who did what and when. +. **Lineage** — directed-edge graph of data derivation (target nameschematically a DAG; see ADR-0004 when written). +. **Constraints** — cross-dimensional invariant enforcement, including + drift detection between Data + Metadata + active overlays. +. **AccessControl** — policy-based row/column-level access permissions. +. **Temporal** — version history with point-in-time queries and rollback. +. **Simulation** — what-if branching and sandbox query execution. + +Modalities (Graph, Vector, Tensor, Semantic, Document, Spatial) are +*Tier 2 overlays* — independent representational projections that a user +can enable per-entity for similarity search, full-text search, geospatial +indexing, etc. They are not "the octad" and not co-equal with the eight +concerns. Provenance and Temporal in the modalities list collapse onto +the same-named concerns. + +The eight "cross-modal drift categories" become *symptoms observed by +the Constraints concern* when Data, Metadata, and the active overlays +disagree: + +[cols="1,2"] +|=== +| Drift category (legacy framing) | Where it lives in the concerns ontology + +| Structural | Constraints (Data vs Metadata schema agreement) +| Semantic | Constraints across overlays +| Temporal | Constraints between Temporal versions across overlays +| Statistical | Constraints over Tier 2 vector/tensor overlay drift +| Referential | Constraints between Tier 2 graph overlay and Data +| Provenance | Constraints over Provenance chain integrity +| Spatial | Constraints over Tier 2 spatial overlay +| Embedding | Constraints between Tier 2 vector overlay and source documents +|=== + +== Consequences + +. README and ROADMAP must be rewritten to drop the modalities octad table + and reframe the drift categories under Constraints. Tracked as V-L1-A2. +. The modalities-first refactor (V-L1-A3) is *not* done. Closed as wontfix. +. Tier 2 design (V-L1-F, V-L1-G, V-L1-H) continues to use modality terms + for overlays — they are just no longer presented as "the octad." +. `OctadDimension` enum and `OctadConfig` fields are stable; no source-level + rename triggered by this ADR. + +== Alternatives considered + +Modalities octad as canonical:: +Rejected. Would have required rewriting `abi`, `manifest`, `codegen`, tests, +and example manifests — a multi-week change for pre-alpha framing. The +codebase had already converged on the concerns ontology; the only cost of +keeping it is doc updates. + +"Both, with one as primary":: +Considered but rejected. Two ontologies sharing a name is the bug; +ranking them doesn't fix it. + +Renaming "octad" to something else (e.g. "octave"):: +Out of scope here. The brand survives; the contents are defined. diff --git a/docs/decisions/ADR-0002-verification-tree.adoc b/docs/decisions/ADR-0002-verification-tree.adoc new file mode 100644 index 0000000..f9bce7d --- /dev/null +++ b/docs/decisions/ADR-0002-verification-tree.adoc @@ -0,0 +1,66 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += ADR-0002: Strip the empty verification/ subtree +:revdate: 2026-05-13 +:status: Accepted + +== Status + +Accepted — 2026-05-13. + +Resolves: https://github.com/hyperpolymath/verisimiser/issues/15[V-L3-D1]. + +== Context + +The `verification/` tree contained eight subdirectories +(`benchmarks/`, `coverage/`, `fuzzing/`, `proofs/`, `safety_case/`, +`simulations/`, `tests/`, `traceability/`), each with a ~20-byte +`README.adoc` and an a2ml manifest. Zero proofs, zero benchmarks, +zero fuzzing, zero safety case. + +(The actual Idris2 ABI declarations and Zig FFI implementation live in +`src/interface/abi/{Types,Layout,Foreign}.idr` and `src/interface/ffi/` +respectively — those are real Phase 0 stubs and are unaffected by this +ADR. The README's reference to "Idris2 proofs (in `src/interface/abi/`)" +already points at the correct location for the stubs; only the proofs +themselves are still future work.) + +A reader following the README's verification/-shaped tree was misled +into thinking benchmarks, fuzzing, safety cases, and traceability +artifacts existed for this product. + +== Decision + +Strip the empty `verification/` subtree from the repository. + +Reintroduce `verification/` only when there is something to put in it. +The first content is expected to be a property-test harness landing +alongside V-L1-C1 (the Tier 1 SQLite piggyback) — at that point a +single `verification/property-tests/` directory will be added with +real content. Don't predeclare the rest of the eight subdirs until +they have artifacts. + +== Consequences + +. The empty `verification/` subtree is deleted in the same change set + that lands this ADR. +. The README's "Status" / "Architecture" copy that referenced + `verification/` is reworded to point at `src/interface/abi/` only + (where the Idris2 stubs actually live). +. Future verification artifacts (proofs, benchmarks, fuzz targets) are + added directory-by-directory as they appear, not predeclared. The + first such addition is expected alongside V-L1-C1 (Tier 1 SQLite + piggyback) as a property-test harness. + +== Alternatives considered + +Populate the subtree:: +Rejected for now. Writing eight stub READMEs costs effort and doesn't +move the product forward. The contracts the README cited (drift +correctness, chain integrity, version ordering, sidecar isolation) +become provable only once the Tier 1 implementation exists, which is +V-L1-C1. + +Leave the subtree, soften the README:: +Rejected. Empty scaffolding misleads contributors who follow the tree +looking for examples to extend. diff --git a/docs/decisions/ADR-0003-justfile-aspirational-recipes.adoc b/docs/decisions/ADR-0003-justfile-aspirational-recipes.adoc new file mode 100644 index 0000000..281eb87 --- /dev/null +++ b/docs/decisions/ADR-0003-justfile-aspirational-recipes.adoc @@ -0,0 +1,52 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += ADR-0003: Remove aspirational Justfile recipes +:revdate: 2026-05-13 +:status: Accepted + +== Status + +Accepted — 2026-05-13. + +Resolves: https://github.com/hyperpolymath/verisimiser/issues/11[V-L3-C2]. +Unblocks: https://github.com/hyperpolymath/verisimiser/issues/10[V-L3-C1] (the +mechanical fix to the broken recipe block). + +== Context + +`Justfile` carried a recipe block whose source contained literal `\n` +characters where newlines were intended. The intent was three recipes +(`augment`, `check-octad`, `migrate`) calling clap subcommands of the +same names. The clap CLI in `src/main.rs` exposes +`init / generate / start / drift / provenance / history / status / octad` +— there are no `augment`, `check-octad`, or `migrate` subcommands. + +So the Justfile advertised commands that don't exist, and did so in a +syntactically broken way that made the breakage invisible to `just --list`. + +== Decision + +Delete the three aspirational recipes from `Justfile`. + +The Justfile should only reference subcommands that exist. When new +subcommands are added (per their own design issues), recipe wrappers +can be added at the same time. + +== Consequences + +. The broken `\n`-collapsed block is removed cleanly (V-L3-C1). +. `just --list` no longer shows phantom recipes. +. Future "convenience wrapper" recipes must be added in the same change + set as the underlying subcommand. + +== Alternatives considered + +Add the missing subcommands:: +Out of scope for V-L3-C2/C1, which are ground-clearing issues. The +semantics of `augment` / `check-octad` / `migrate` aren't pinned down — +e.g. `augment DB_URL` overlaps with `generate` (overlay DDL) plus `start` +(daemon). Designing them is a separate issue, not a one-line fix. + +Keep the recipes pointing at not-yet-implemented subcommands:: +Rejected. The recipes would still fail with "Unknown subcommand"; the +broken UX would just be in a different place. diff --git a/examples/SafeDOMExample.res b/examples/SafeDOMExample.res deleted file mode 100644 index 2c1b5b3..0000000 --- a/examples/SafeDOMExample.res +++ /dev/null @@ -1,109 +0,0 @@ -// SPDX-License-Identifier: PMPL-1.0-or-later -// Example: Using SafeDOM for formally verified DOM mounting - -open SafeDOM - -// Example 1: Basic mounting with error handling -let mountApp = () => { - mountSafe( - "#app", - "

Hello, World!

Mounted safely with proofs.

", - ~onSuccess=el => { - Console.log("✓ App mounted successfully!") - Console.log("Element:", el) - }, - ~onError=err => { - Console.error("✗ Mount failed:", err) - } - ) -} - -// Example 2: Wait for DOM ready before mounting -let mountWhenDOMReady = () => { - mountWhenReady( - "#app", - "

App Title

", - ~onSuccess=_ => Console.log("✓ Mounted after DOM ready"), - ~onError=err => Console.error("✗ Failed:", err) - ) -} - -// Example 3: Batch mounting (atomic - all or nothing) -let mountMultiple = () => { - let specs = [ - {selector: "#header", html: "

Site Title

"}, - {selector: "#nav", html: ""}, - {selector: "#main", html: "

Content here

"}, - {selector: "#footer", html: "
© 2026
"} - ] - - switch mountBatch(specs) { - | Ok(elements) => { - Console.log(`✓ Successfully mounted ${Array.length(elements)} elements`) - elements->Array.forEach(el => Console.log(" -", el)) - } - | Error(err) => { - Console.error("✗ Batch mount failed:", err) - Console.error(" (None were mounted - atomic operation)") - } - } -} - -// Example 4: Explicit validation before mounting -let mountWithValidation = () => { - // Validate selector first - switch ProvenSelector.validate("#my-app") { - | Error(e) => Console.error(`Invalid selector: ${e}`) - | Ok(validSelector) => { - // Validate HTML - switch ProvenHTML.validate("
Content
") { - | Error(e) => Console.error(`Invalid HTML: ${e}`) - | Ok(validHtml) => { - // Now mount with proven safety - switch mount(validSelector, validHtml) { - | Mounted(el) => Console.log("✓ Mounted with validated inputs:", el) - | MountPointNotFound(s) => Console.error(`✗ Element not found: ${s}`) - | InvalidSelector(_) => Console.error("Impossible - already validated") - | InvalidHTML(_) => Console.error("Impossible - already validated") - } - } - } - } -} - -// Example 5: Integration with TEA -module MyApp = { - type model = {message: string} - type msg = NoOp - - let init = () => {message: "Hello from TEA"} - let update = (model, _msg) => model - let view = model => `

${model.message}

` -} - -let mountTEAApp = () => { - let model = MyApp.init() - let html = MyApp.view(model) - - mountWhenReady( - "#tea-app", - html, - ~onSuccess=el => { - Console.log("✓ TEA app mounted") - // Set up event handlers, subscriptions here - }, - ~onError=err => Console.error(`✗ TEA mount failed: ${err}`) - ) -} - -// Entry point -let main = () => { - Console.log("SafeDOM Examples") - Console.log("================\n") - - // Choose which example to run - mountWhenDOMReady() // Run on DOM ready -} - -// Auto-execute when module loads -main() diff --git a/examples/web-project-deno.json b/examples/web-project-deno.json deleted file mode 100644 index 5ddd3bd..0000000 --- a/examples/web-project-deno.json +++ /dev/null @@ -1,20 +0,0 @@ -{ - "// NOTE": "Example deno.json for ReScript web projects", - "tasks": { - "build": "deno run -A npm:rescript", - "clean": "deno run -A npm:rescript clean", - "watch": "deno run -A npm:rescript -w", - "serve": "deno run -A jsr:@std/http/file-server .", - "test": "deno test --allow-all" - }, - "imports": { - "rescript": "^12.0.0", - "@rescript/core": "npm:@rescript/core@^1.6.0", - "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/rescript-dom-mounter/main/src/", - "proven/": "../proven/bindings/rescript/src/" - }, - "compilerOptions": { - "allowJs": true, - "checkJs": false - } -} diff --git a/tests/integration_test.rs b/tests/integration_test.rs index f5bd100..09019c2 100644 --- a/tests/integration_test.rs +++ b/tests/integration_test.rs @@ -83,23 +83,23 @@ fn test_full_pipeline_blog_schema() { // Verify all expected sidecar tables are present. assert!( - overlay_ddl.contains("verisim_metadata"), + overlay_ddl.contains("verisimdb_metadata"), "Should contain metadata table" ); assert!( - overlay_ddl.contains("verisim_provenance_log"), + overlay_ddl.contains("verisimdb_provenance_log"), "Should contain provenance table" ); assert!( - overlay_ddl.contains("verisim_lineage_graph"), + overlay_ddl.contains("verisimdb_lineage_graph"), "Should contain lineage table" ); assert!( - overlay_ddl.contains("verisim_temporal_versions"), + overlay_ddl.contains("verisimdb_temporal_versions"), "Should contain temporal table" ); assert!( - overlay_ddl.contains("verisim_access_policies"), + overlay_ddl.contains("verisimdb_access_policies"), "Should contain access policies table" ); @@ -151,9 +151,9 @@ fn test_full_pipeline_blog_schema() { // Step 4: Render interceptors to SQL and verify output. let rendered = query::render_interceptors(&interceptors); - assert!(rendered.contains("verisim_users_with_provenance")); - assert!(rendered.contains("verisim_posts_with_temporal")); - assert!(rendered.contains("verisim_comments_with_provenance")); + assert!(rendered.contains("verisimdb_users_with_provenance")); + assert!(rendered.contains("verisimdb_posts_with_temporal")); + assert!(rendered.contains("verisimdb_comments_with_provenance")); } // --------------------------------------------------------------------------- @@ -436,7 +436,9 @@ fn test_end_to_end_file_workflow() { .unwrap(); } - // Write a manifest file. + // Write a manifest file. Note: on Windows, schema_path uses backslashes + // which are escape characters in TOML basic strings — emit the path as a + // TOML literal string (single-quoted) to dodge escape interpretation. let manifest_path = dir.path().join("verisimiser.toml"); { let mut f = std::fs::File::create(&manifest_path).unwrap(); @@ -449,7 +451,7 @@ name = "test-articles" [database] backend = "sqlite" connection-string-env = "TEST_DB" -schema-source = "{}" +schema-source = '{}' [octad] enable-provenance = true @@ -483,11 +485,11 @@ path = ".verisim/test.db" assert!(overlay_ddl.contains("verisim_provenance_log")); assert!(overlay_ddl.contains("verisim_temporal_versions")); assert!( - !overlay_ddl.contains("verisim_lineage_graph"), + !overlay_ddl.contains("verisimdb_lineage_graph"), "Lineage is disabled" ); assert!( - !overlay_ddl.contains("verisim_access_policies"), + !overlay_ddl.contains("verisimdb_access_policies"), "Access control is disabled" ); diff --git a/verification/0.1-AI-MANIFEST.a2ml b/verification/0.1-AI-MANIFEST.a2ml deleted file mode 100644 index 39b370f..0000000 --- a/verification/0.1-AI-MANIFEST.a2ml +++ /dev/null @@ -1,27 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-pillar" -level: 1 -parent: "../0-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Primary verification pillar. Contains evidence for correctness, - performance, formal proofs, randomized testing, and aerospace-grade - high-assurance metrics (MC/DC coverage, traceability, safety cases). - -canonical_locations: - tests: "tests/" - benchmarks: "benchmarks/" - proofs: "proofs/" - fuzzing: "fuzzing/" - simulations: "simulations/" - coverage: "coverage/" - traceability: "traceability/" - safety_case: "safety_case/" - -invariants: - - "Evidence MUST be reproducible and documented" - - "High-assurance deployments MUST satisfy traceability and safety_case requirements" diff --git a/verification/README.adoc b/verification/README.adoc deleted file mode 100644 index f07e7f3..0000000 --- a/verification/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Verification Pillar diff --git a/verification/benchmarks/0.2-AI-MANIFEST.a2ml b/verification/benchmarks/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 6416309..0000000 --- a/verification/benchmarks/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "benches-pillar" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Benches pillar. diff --git a/verification/benchmarks/README.adoc b/verification/benchmarks/README.adoc deleted file mode 100644 index 5db7648..0000000 --- a/verification/benchmarks/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Benchmarks Unit diff --git a/verification/coverage/0.2-AI-MANIFEST.a2ml b/verification/coverage/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index fc15bd3..0000000 --- a/verification/coverage/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,12 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-coverage" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - High-assurance verification unit for coverage. - Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/coverage/README.adoc b/verification/coverage/README.adoc deleted file mode 100644 index 2566956..0000000 --- a/verification/coverage/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Coverage Unit diff --git a/verification/fuzzing/0.2-AI-MANIFEST.a2ml b/verification/fuzzing/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 79c4fef..0000000 --- a/verification/fuzzing/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "fuzzing-unit" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Fuzzing unit for high-rigor verification. diff --git a/verification/fuzzing/README.adoc b/verification/fuzzing/README.adoc deleted file mode 100644 index edeb179..0000000 --- a/verification/fuzzing/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Fuzzing Unit diff --git a/verification/proofs/0.2-AI-MANIFEST.a2ml b/verification/proofs/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 0e5666f..0000000 --- a/verification/proofs/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-proofs" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Sub-unit focusing on proofs. diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc deleted file mode 100644 index 1ae324d..0000000 --- a/verification/proofs/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Proofs Unit diff --git a/verification/safety_case/0.2-AI-MANIFEST.a2ml b/verification/safety_case/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 818fba4..0000000 --- a/verification/safety_case/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,12 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-safety_case" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - High-assurance verification unit for safety case. - Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/safety_case/README.adoc b/verification/safety_case/README.adoc deleted file mode 100644 index 47c8e36..0000000 --- a/verification/safety_case/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Safety case Unit diff --git a/verification/simulations/0.2-AI-MANIFEST.a2ml b/verification/simulations/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index f40fc1c..0000000 --- a/verification/simulations/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "simulations-unit" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Simulations unit for high-rigor verification. diff --git a/verification/simulations/README.adoc b/verification/simulations/README.adoc deleted file mode 100644 index 8e1b13a..0000000 --- a/verification/simulations/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Simulations Unit diff --git a/verification/tests/0.2-AI-MANIFEST.a2ml b/verification/tests/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 0008fcf..0000000 --- a/verification/tests/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1 +0,0 @@ -# AI Manifest - Level 1: tests diff --git a/verification/tests/README.adoc b/verification/tests/README.adoc deleted file mode 100644 index 344bf86..0000000 --- a/verification/tests/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Tests Unit diff --git a/verification/traceability/0.2-AI-MANIFEST.a2ml b/verification/traceability/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index defa125..0000000 --- a/verification/traceability/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,12 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-traceability" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - High-assurance verification unit for traceability. - Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/traceability/README.adoc b/verification/traceability/README.adoc deleted file mode 100644 index ff23dd7..0000000 --- a/verification/traceability/README.adoc +++ /dev/null @@ -1 +0,0 @@ -= Traceability Unit