feat(verisim-modular-experiment): scaffold Path B research experiment

Asks: can any octad shape be entirely absent (store-level) without
making VCL consonance claims unsound? Sibling to verisimdb/ and
typeql-experimental/.

Phase 0 + Phase 1 closed this session:

- Core = {Semantic, Temporal, Provenance} (store-level required)
- Federable = {Vector, Tensor, Document, Spatial}
- Conditional = {Graph} (required iff cross-entity claims)

Grounded in arcvix-octad-data-model.tex:
- def:octad — per-octad ⊥ allowed
- def:pairwise-drift — d(⊥,·)=0 soundness convention
- inv:persist — Identity Persistence requires Temporal
- def:enrichment — write primitive writes to both P and R
- thm:attestation — attestation freshness + signatures

Phase 2 ABI draft typechecks clean in Idris2 v0.8.0:
- src/Abi/Types.idr (8 shapes + Core/Federable partition)
- src/Abi/VerisimCore.idr (identity-core ABI)
- src/Abi/FederationContract.idr (5-clause contract)

Type-level guarantee: IsFederable predicate has no Core constructors,
so the type system refuses Core-shape federation at compile time.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

verisim-modular-experiment/.gitignore

@@ -0,0 +1,3 @@
+build/
+*.ttc
+*.ttm

verisim-modular-experiment/0-AI-MANIFEST.a2ml

@@ -0,0 +1,42 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# 0-AI-MANIFEST.a2ml — verisim-modular-experiment
+# Universal entry point for AI agents (Claude, Gemini, OpenAI, etc.)
+
+repository:
+  name: verisim-modular-experiment
+  status: experimental
+  purpose: |
+    Research experiment asking whether VeriSimDB's octad can be decomposed
+    into a slim identity core + federation contract protocol without
+    weakening VCL's consonance guarantees. NOT a replacement for VeriSimDB.
+  parent-monorepo: nextgen-databases
+  siblings:
+    - verisimdb (canonical, paved-road)
+    - typeql-experimental (sibling experiment)
+
+critical-invariants:
+  - "Main verisimdb/ is read-only from this experiment's perspective."
+  - "Do NOT weaken VCL's consonance guarantees in pursuit of modularity —
+     either preserve them via federation contract, or document the
+     degradation honestly."
+  - "A negative result (octad is indivisible) is an acceptable outcome."
+  - "Follow hyperpolymath standards: Idris2 ABI, Zig FFI, PMPL-1.0-or-later."
+
+canonical-locations:
+  design-docs: docs/
+  spec: spec/
+  proof-obligations: PROOF-NEEDS.md
+
+lifecycle:
+  on-enter:
+    - Read README.adoc
+    - Read docs/DESIGN-2026-04-05-core-and-federation.adoc
+    - Read PROOF-NEEDS.md
+  on-exit:
+    - Update DESIGN log if conclusions changed
+    - Update PROOF-NEEDS.md if obligations discharged or added
+
+references:
+  - memory: vcl-rename.md (user's modularity thought, 2026-04-05)
+  - memory: feedback_verisimdb_policy.md (maximise-first philosophy)
+  - conversation: 2026-04-05 Claude Code session

verisim-modular-experiment/PLAN.adoc

@@ -0,0 +1,230 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= Plan — verisim-modular-experiment
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:toc:
+:sectnums:
+
+*Type:* research plan (not feature plan). Phases have decision gates that
+can terminate the experiment with a positive or negative result. A
+negative result (octad-is-indivisible) is an acceptable outcome and
+strengthens the main verisimdb documentation.
+
+*Cadence:* light. User has many other active projects. Run in background
+between higher-priority work. No ship deadline.
+
+== Scope boundaries
+
+[cols="1,3",options="header"]
+|===
+|In scope |Out of scope
+
+|Articulating the identity core vs. federable shapes |Refactoring main `verisimdb/`
+|Federation contract Idris2 ABI design |Production implementation
+|One reference federated shape + one dogfood client |Full parity with octad
+|Honest degradation documentation |Maintaining both monolith + modular long-term
+|VCL consonance-preservation proofs |New VCL features
+|===
+
+== Phases and decision gates
+
+=== Phase 0 — Octad archaeology
+
+*Goal:* inventory the octad's shapes and their current VCL-visible contracts.
+No code written.
+
+*Activities:*
+
+* Read main `verisimdb/` sources to enumerate the eight shapes
+* For each shape, document:
+  - What invariants does VeriSim *enforce* about it?
+  - What does VeriSim merely *expose* about it to VCL?
+  - Which VCL constraints cross this shape's boundary?
+
+*Artifact:* `docs/OCTAD-SHAPES.adoc` — inventory with per-shape contract surface.
+
+*Decision gate:* none. This phase is descriptive.
+
+*Dependency:* needs read access to main verisimdb sources (already have).
+
+---
+
+=== Phase 1 — Core identification
+
+*Goal:* produce a candidate `Core ⊆ Octad` split with justifications.
+
+*Activities:*
+
+* Apply the _closure test_ per shape: is this invariant VeriSim-enforced
+  (core candidate) or can it be externally honoured + checked (federable
+  candidate)?
+* For each federable candidate, sketch the degradation story (what
+  VCL claims weaken if this shape is omitted from a federation?)
+* Stress-test with adversarial cases: can VCL compose claims across the
+  proposed `Core/Federable` boundary?
+
+*Artifact:* `docs/CORE-CANDIDATES.adoc` — split with justification per
+shape + degradation table.
+
+*Decision gates:*
+
+* **Trivial core (|Core| ≤ 1)** → experiment collapses to "VeriSim is an
+  audit wrapper". *Negative result, stop.*
+* **Full octad (|Core| = 8)** → octad is indivisible. *Negative result,
+  stop and write up.*
+* **Non-trivial split (2 ≤ |Core| ≤ 6)** → proceed to Phase 2.
+
+---
+
+=== Phase 2 — Federation contract design
+
+*Goal:* state the typed contract a federable shape must honour, in Idris2,
+such that VCL's consonance claims over a federation are sound.
+
+*Activities:*
+
+* Draft `src/abi/FederationContract.idr` — the ABI honoured by any
+  federated shape
+* Prove contract composability: federating shape A + shape B under the
+  contract does not weaken claims about A or B or Core (non-interference)
+* Document the reduced-guarantee story formally
+
+*Artifacts:*
+
+* `src/abi/FederationContract.idr`
+* `spec/federation-contract.adoc` — prose + type-level statement
+* `PROOF-NEEDS.md` updated with discharged obligations
+
+*Decision gate:*
+
+* **Contract unstateable in Idris2 without losing guarantees** →
+  indivisibility confirmed by a different route. *Negative result, stop.*
+* **Contract states cleanly + non-interference proved** → proceed to
+  Phase 3.
+
+---
+
+=== Phase 3 — Reference core + one federated shape
+
+*Goal:* working reference implementation of VerisimCore with exactly one
+shape federated through the contract.
+
+*Choice of federated shape:* probably *temporal* — well-understood ordering
+semantics, easy to expose invariants externally, common in real systems.
+
+*Activities:*
+
+* Implement minimal VerisimCore (identity + provenance + VCL runtime +
+  consonance prover)
+* Implement federation adapter for temporal shape via Zig FFI
+* Write VCL test cases that exercise claims crossing Core/temporal boundary
+* Verify consonance is preserved vs. equivalent full-octad run
+
+*Artifacts:*
+
+* Reference implementation (language TBD — Julia for Core? Zig for FFI?
+  Decide in Phase 2 as contract crystallises)
+* Integration tests
+* Benchmark comparison vs. full octad for shared claims
+
+*Decision gate:*
+
+* **VCL composes correctly across boundary, tests pass** → proceed to
+  Phase 4.
+* **VCL claims fail to compose, or require weakening** → revisit Phase 1/2
+  split or declare indivisibility.
+
+---
+
+=== Phase 4 — Dogfood on KRLAdapter.jl
+
+*Goal:* validate that a real client can be satisfied by VerisimCore +
+federation, not by the full octad.
+
+*Activities:*
+
+* Wire `KRLAdapter.jl` against VerisimCore (already earmarked for this per
+  `vcl-rename.md` memory)
+* Verify it can do what it needs with only identity + provenance (+
+  temporal via federation?)
+* Document what it *cannot* do that the full octad would enable
+* Decide: is the reduced capability acceptable for this client?
+
+*Artifacts:*
+
+* Working `KRLAdapter.jl` ↔ VerisimCore integration
+* Degradation report for this client
+
+*Decision gate:*
+
+* **KRLAdapter.jl satisfied** → positive result, proceed to Phase 5.
+* **KRLAdapter.jl needs more than Core provides** → either revisit the
+  Core split (maybe too slim) or declare "this client needs the octad"
+  (useful finding either way).
+
+---
+
+=== Phase 5 — Write-up
+
+*Goal:* capture findings so the work isn't lost.
+
+*If positive result:*
+
+* Publish federation contract spec
+* Write adoption guide: "when to use VerisimCore vs. full octad"
+* Propose whether modular VerisimCore ships as a real product, stays
+  experimental, or informs a refactor of main verisimdb
+
+*If negative result:*
+
+* Formal indivisibility argument → fold into main `verisimdb/` docs as
+  justification for the octad
+* Document which shapes are most "federation-resistant" and why
+
+*Artifact:* `docs/FINDINGS.adoc` with conclusions + recommendations.
+
+== Risks and off-ramps
+
+[cols="2,3",options="header"]
+|===
+|Risk |Mitigation
+
+|Scope creep into reimplementing VeriSim
+|Phase gates. Minimum viable Core only. Zero production concerns.
+
+|VCL's internal structure makes the split impossible to state
+|That *is* the result. Negative results are acceptable outcomes.
+
+|Federation contract requires bidirectional trust we can't provide
+|Document as a constraint on which external DBs can federate.
+
+|Competes for attention with higher-priority work
+|Light cadence. No deadline. Park between phases if needed.
+
+|Findings don't translate back to main verisimdb
+|Phase 5 has explicit fold-back artifact for negative case.
+|===
+
+== Dependencies
+
+* *Main `verisimdb/`* — read-only reference for Phase 0–1. No modifications.
+* *VCL spec* — need current spec for Phase 1 (check `verisimdb/` + memory files).
+* *KRLAdapter.jl* — Phase 4 client. Kept at Verisim-interface-slot per memory.
+* *Idris2 toolchain* — Phase 2 onward.
+* *Zig toolchain* — Phase 3 onward.
+* *Dedicated VeriSimDB instance* — if experiment needs one, allocate a new
+  port (8097 is next free per `feedback_verisimdb_policy.md`). Decide in
+  Phase 3.
+
+== Working conventions
+
+* Each phase gets a dated session log in `docs/sessions/`
+* Decision gates are recorded in `PROOF-NEEDS.md` as discharged or refuted
+  obligations
+* Folded-back findings to main verisimdb are tracked in `docs/FOLDBACK.adoc`
+* VCL is the current name (not VQL)
+* No fragmenting main verisimdb until after Phase 5
+
+== Next action
+
+Phase 0, activity 1: read main `verisimdb/` sources and enumerate the
+octad's eight shapes.

verisim-modular-experiment/PROOF-NEEDS.md

@@ -0,0 +1,41 @@
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+# Proof Needs — verisim-modular-experiment
+
+## Central obligation
+
+**Claim:** There exists a subset `Core ⊆ Octad` and a federation contract
+`F` such that, for every federation `S = Core ⊎ {external shapes honouring F}`,
+VCL's consonance judgements on `S` are sound — i.e. no weaker than on
+`Core` alone, and equivalent to the full octad for claims that stay within
+shapes present in `S`.
+
+**Or the negation:** No such `Core` and `F` exist, and the octad is
+indivisible w.r.t. VCL's consonance guarantees.
+
+Either resolution is acceptable. The experiment succeeds by *deciding*
+which holds.
+
+## Subordinate obligations
+
+1. **Core closure.** Consonance claims purely over `Core` are verifiable
+   without appeal to federated shapes.
+
+2. **Federation soundness.** If external shape `E` honours contract `F`,
+   then VCL claims crossing the `Core`/`E` boundary are sound relative to
+   `E`'s externally-verified invariants.
+
+3. **Degradation honesty.** For every shape omitted from a federation, the
+   guarantees weakened by that omission are enumerated and documented.
+
+4. **Non-interference.** Federating shape `E1` does not silently weaken
+   claims about shape `E2` or about `Core`.
+
+## Proof stack (intended)
+
+- Idris2 for the federation contract ABI (per hyperpolymath standard)
+- VCL's existing proof apparatus for consonance claims
+- Zig FFI at the external-shape boundary
+
+## Status
+
+Empty. No obligations discharged yet — this is a research scaffold.

verisim-modular-experiment/README.adoc

@@ -0,0 +1,66 @@
+// SPDX-License-Identifier: PMPL-1.0-or-later
+= verisim-modular-experiment
+Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+:toc:
+:sectnums:
+
+*Status:* experimental — research repo, NOT a replacement for VeriSimDB.
+
+== The question
+
+VeriSimDB's value is _consonance_: VCL (formerly VQL) states and verifies
+constraints across the octad as an integrated substrate. The octad works well
+as a monolith for hyperpolymath's own use, but may be too heavy for external
+adopters who already have existing databases and only need some of what
+VeriSim provides.
+
+This experiment asks:
+
+[quote]
+What is the minimum set of shapes and invariants such that VCL can still
+state and verify consonance claims about a federation that swaps out
+non-core shapes for external databases?
+
+== Hypothesis
+
+A slim *VerisimCore* (identity + provenance + VCL runtime + consonance
+prover) can be extracted from the octad, with the remaining shapes exposed
+via a *federation contract protocol* that preserves VCL's type/constraint
+guarantees across typed boundaries.
+
+== Non-goals
+
+* *Not* a replacement for VeriSimDB. Canonical octad stays the paved road.
+* *Not* a "verisim-lite" audit wrapper. If the experiment collapses to that,
+  we learn the octad is indivisible (a valuable negative result).
+* *Not* shipping to production — this is a research artefact.
+
+== Research questions
+
+. Which of the octad's eight shapes are load-bearing for consonance, and
+  which are storage-flavoured concerns that could be federated out?
+. What contracts must a federated shape honour for VCL to type-check across
+  the boundary?
+. Can VCL's constraint composition be stated over a federation without
+  weakening the consonance guarantees of the core?
+. What is the reduced-guarantee story for federations that omit shapes the
+  core would normally require?
+
+== First client (dogfood)
+
+`KRLAdapter.jl` — per existing memory, already earmarked as a slim-core
+candidate. Needs identity + provenance, does not need the full octad. Good
+fit for exercising the minimal core and the federation contract.
+
+== Relationship to main VeriSimDB
+
+* Main `verisimdb/` remains canonical, maximal, octad-as-unit. No
+  fragmentation of the existing code.
+* This experiment is read-only with respect to main verisimdb's sources.
+* Findings that strengthen the monolith (e.g. clearer articulation of why
+  each shape is load-bearing) should be folded back into main verisimdb's
+  documentation regardless of whether the modular version ships.
+
+== License
+
+PMPL-1.0-or-later.