docs: distinguish modality profiles from fixed Octad schema

CHANGELOG.adoc

@@ -13,6 +13,13 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 ==== Changed
 
+* *Modality profiles distinguished from the fixed Octad schema* (vcl-ut#118):
+  adopted `modality profile` for versioned, implementation-specific modality
+  selections and `modality set` for membership alone. Clarified that VCL-UT's
+  `OctadSchema` and `VCLS` v1 remain fixed at eight modality slots; empty or
+  omitted schema fields do not signal profile membership or witness presence.
+  No type, JSON contract, or wire format changed. See
+  `docs/standards/MODALITY-PROFILES.adoc` and ADR-0007.
 * *Licensing and REUSE policy normalized*: software and package metadata use
   MPL-2.0; human-readable documentation uses CC-BY-SA-4.0. Removed the unused
   AGPL license text, corrected invalid PMPL SPDX declarations, and clarified

README.adoc

@@ -132,6 +132,18 @@ it. Simple statements short-circuit at the early safety levels; proof-bearing
 statements and high-risk lifecycle transitions go through the deeper proof,
 effect, resource, and cross-cutting checks (L9-L10).
 
+[NOTE]
+====
+Keep a deployment's **modality profile** (which modalities it supports or
+enables) separate from the **Octad** and VCL-UT's `OctadSchema`. The Octad is
+the fixed eight-modality model; a subject may have data in only some of its
+slots. `OctadSchema` still has all eight schema slots, even when a slot has no
+field definitions. The current `VCLS` v1 wire format is fixed-arity and does
+not carry a modality profile. See
+link:docs/standards/MODALITY-PROFILES.adoc[the terminology and compatibility
+contract].
+====
+
 [source]
 ----
 User / system writes VCL
@@ -170,6 +182,8 @@ routine VCL safe.
 
 Prefer: consonance language, statement, transition, identity claim, consonance
 subject, modal witness, proof-bearing statement, verified transition, octad.
+When discussing implementation/deployment modality support, use *modality
+profile*; reserve `OctadSchema` for the fixed eight-slot schema.
 
 Avoid or qualify: query language, query, record, CRUD, delete, proof-carrying
 query, 6-modal engine, passive store. Use "query" only for a read-only syntactic

ROADMAP.adoc

@@ -74,9 +74,12 @@ These are ordered by value, not by version number.
 . *Discharge the two disclosed L10 residuals.* Transitive `ENTAILS`-cycle
   detection and proposition well-typedness, both recorded as owed in
   `verification/proofs/VERIFICATION-STANCE.adoc`.
-. *Retire the `HEXAD` keyword* once VeriSimDB's default modality context
-  carries all eight witnesses. The parser accepts both `OCTAD` and `HEXAD`
-  today for compatibility.
+. *Optional syntax cleanup: retire the legacy `HEXAD` spelling* when all
+  supported frontends can do so compatibly. The current Rust parser accepts
+  both `OCTAD` and `HEXAD` as the same `Source::Octad`; this is a source-name
+  alias, not a six-modality profile. Its deprecation is independent of which
+  modalities a deployment enables or which witnesses a subject populates.
+  See link:docs/standards/MODALITY-PROFILES.adoc[the profile/Octad contract].
 
 == Milestones
 

container/README.adoc

@@ -155,7 +155,7 @@ For k9-svc managed deployments:
 [source,bash]
 ----
 # Validate the deployment component
-nickel typecheck container/deploy.k9.ncl
+k9-svc validate container/deploy.k9.ncl
 
 # Deploy (requires Hunt-level authorisation)
 k9-svc deploy container/deploy.k9.ncl --env production

container/deploy.k9.ncl

@@ -1,3 +1,4 @@
+K9!
 # SPDX-License-Identifier: MPL-2.0
 # deploy.k9.ncl — VCL-total deployment component (Hunt level)
 #
@@ -8,65 +9,9 @@
 # It requires explicit authorisation via the Leash system.
 #
 # Usage:
-#   nickel typecheck container/deploy.k9.ncl
 #   k9-svc validate container/deploy.k9.ncl
 #   k9-svc deploy container/deploy.k9.ncl --env production
 
-# The component's pedigree (self-description across five layers)
-let component_pedigree = {
-  # ─────────────────────────────────────────────────────────────
-  # L1: The Snout — Identity
-  # ─────────────────────────────────────────────────────────────
-  metadata = {
-    name = "vcl-total-deploy",
-    version = "0.1.0",
-    breed = "application/vnd.k9+nickel",
-    magic_number = "K9!",
-    description = "VCL-total deployment component (Hunt level)",
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L2: The Scent — Target Environment
-  # ─────────────────────────────────────────────────────────────
-  target = {
-    os = 'Linux,
-    is_edge = false,
-    requires_podman = true,
-    min_memory_mb = 256,
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L3: The Leash — Security
-  # ─────────────────────────────────────────────────────────────
-  security = {
-    trust_level = 'Hunt,
-    allow_network = true,
-    allow_filesystem_write = true,
-    allow_subprocess = true,
-    # In production, replace with a real Ed25519 signature.
-    signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT",
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L4: The Gut — Self-Validation
-  # ─────────────────────────────────────────────────────────────
-  validation = {
-    checksum = "sha256:placeholder",
-    pedigree_version = "1.0.0",
-    hunt_authorized = false,  # Must be set true after handshake
-  },
-
-  # ─────────────────────────────────────────────────────────────
-  # L5: The Muscle — Deployment Recipes
-  # ─────────────────────────────────────────────────────────────
-  recipes = {
-    install = "just container-build",
-    validate = "just container-verify",
-    deploy = "just container-up",
-    migrate = "just container-build && just container-up",
-  },
-} in
-
 # Deployment configuration
 let deployment = {
   # Target environments (dev / staging / production)
@@ -143,7 +88,61 @@ echo "K9: Rollback complete."
 
 # Export the component
 {
-  pedigree = component_pedigree,
+  # The component's pedigree (self-description across five layers)
+  pedigree = {
+    # ─────────────────────────────────────────────────────────────
+    # L1: The Snout — Identity
+    # ─────────────────────────────────────────────────────────────
+    metadata = {
+      name = "vcl-total-deploy",
+      version = "0.1.0",
+      breed = "application/vnd.k9+nickel",
+      magic_number = "K9!",
+      description = "VCL-total deployment component (Hunt level)",
+    },
+
+    # ─────────────────────────────────────────────────────────────
+    # L2: The Scent — Target Environment
+    # ─────────────────────────────────────────────────────────────
+    target = {
+      os = 'Linux,
+      is_edge = false,
+      requires_podman = true,
+      min_memory_mb = 256,
+    },
+
+    # ─────────────────────────────────────────────────────────────
+    # L3: The Leash — Security
+    # ─────────────────────────────────────────────────────────────
+    security = {
+      leash = 'Hunt,
+      trust_level = 'Hunt,
+      allow_network = true,
+      allow_filesystem_write = true,
+      allow_subprocess = true,
+      # In production, replace with a real Ed25519 signature.
+      signature = "PLACEHOLDER-SIGNATURE-REQUIRED-FOR-HUNT",
+    },
+
+    # ─────────────────────────────────────────────────────────────
+    # L4: The Gut — Self-Validation
+    # ─────────────────────────────────────────────────────────────
+    validation = {
+      checksum = "sha256:placeholder",
+      pedigree_version = "1.0.0",
+      hunt_authorized = false,  # Must be set true after handshake
+    },
+
+    # ─────────────────────────────────────────────────────────────
+    # L5: The Muscle — Deployment Recipes
+    # ─────────────────────────────────────────────────────────────
+    recipes = {
+      install = "just container-build",
+      validate = "just container-verify",
+      deploy = "just container-up",
+      migrate = "just container-build && just container-up",
+    },
+  },
   deployment = deployment,
   scripts = scripts,
 

docs/2026-07-21-workup-consonance-and-verisim.adoc

@@ -435,9 +435,15 @@ named `HexadType` throughout (`VCLTypes.res:50`, `:206`, `:270`,
 `VCLSubtyping.res:101`). The hexad-to-octad migration reached the variants and
 stopped before the defaults and the names.
 
-Note the same legacy is visible here: the parser still accepts `HEXAD`
-alongside `OCTAD`. That is deliberate compatibility, and it should be retired
-once VeriSimDB's default context carries all eight — not before.
+Terminology correction (2026-10-05): the six-entry `availableModalities`
+value is an implementation-specific modality set; if a versioned profile is
+introduced, it can describe that selection. It does not change the fixed
+eight-slot Octad model or VCL-UT's `OctadSchema`. In this repository's current
+Rust parser, `OCTAD` and `HEXAD` both map to the same `Source::Octad`, with
+`HEXAD` retained as a legacy source spelling. Alias removal is a separate
+cross-frontend compatibility decision; it is not gated on the default context
+listing all eight modalities. Other frontends must be checked independently.
+See link:standards/MODALITY-PROFILES.adoc[the profile/Octad contract].
 
 === The seam is unwired
 
@@ -480,8 +486,9 @@ Ordered by value delivered per unit of risk. Items 1-2 are in this repository;
 | 5
 | *Converge the checkers.* Once (4) is live, retire the ReScript checker's
   independent verdict in favour of the gate's, keeping the ReScript surface
-  parser and diagnostics. Then rename `HexadType` and retire the `HEXAD`
-  keyword together.
+  parser and diagnostics. Treat `HexadType` renaming and `HEXAD` alias removal
+  as separate compatibility cleanups; neither is implied by changing the
+  default modality set.
 | both
 
 | 6

docs/QUICKSTART.adoc

@@ -120,7 +120,7 @@ Create a file called `my-query.vcltotal`:
 ----
 -- A query that exercises 6 of the 10 safety levels
 SELECT GRAPH, DOCUMENT
-FROM HEXAD 550e8400-e29b-41d4-a716-446655440000
+FROM OCTAD 550e8400-e29b-41d4-a716-446655440000
 WHERE FULLTEXT CONTAINS $searchTerm
 CONSUME AFTER 1 USE
 WITH SESSION ReadOnlyProtocol
@@ -260,7 +260,7 @@ Every function is total (`%default total`), every proof is real (zero
 
 Start with:
 
-- `Core.idr` — Foundation types (modalities, hexad references)
+- `Core.idr` — Foundation types (modalities, Octad source references)
 - `Linear.idr` — Simplest safety level (QTT linearity)
 - `Proofs.idr` — Cross-cutting invariants (see how levels compose)
 

docs/WHAT-IS-VERISIMDB.adoc

@@ -68,8 +68,12 @@ them in one system, with _automatic consistency guarantees_.
 
 === The Octad: One Entity, Eight Views
 
-Every piece of data in VeriSimDB is stored as an **octad** -- a single entity
-with up to eight simultaneous representations:
+VeriSimDB's **Octad** is a single-entity model with exactly eight named
+modality slots. A particular subject may have actual witness data in only a
+subset of those slots; “up to eight populated representations” describes
+runtime population, not a variable-length Octad schema. A deployment's
+modality profile, when defined by that implementation, is a separate statement
+about supported or enabled modalities:
 
 ----
 ┌─────────────────────────────────────────────────────────────┐
@@ -114,6 +118,15 @@ with up to eight simultaneous representations:
 | Geospatial coordinates and geometries -- where this entity is in the world
 |===
 
+These are the eight named Octad slots, not a promise that every subject has
+data in all eight. Keep four questions distinct: which modalities the model
+names, which a deployment supports (its *modality profile*), which fields the
+safety schema declares, and which witnesses are populated for a particular
+subject. VCL-UT's `OctadSchema` has a fixed slot for every modality; an empty
+slot in the schema input does not encode a deployment profile or runtime
+absence. See
+link:standards/MODALITY-PROFILES.adoc[the VCL-UT profile/Octad contract].
+
 === Why This Matters
 
 Suppose you have a customer record. In a traditional setup:
@@ -129,13 +142,15 @@ That is six copies of the same customer, in six different systems, with six
 different update mechanisms. When the customer changes their address, you have
 to update _all six_ -- and if any update fails or is delayed, your data drifts.
 
-In VeriSimDB, there is one octad for that customer. All eight views are
-maintained automatically. When the document modality updates, VeriSimDB detects
-that the vector embedding, graph relationships, and search index may have
-drifted, and triggers automatic re-normalisation.
+In VeriSimDB, that customer is modeled by one Octad with eight named slots.
+Which witnesses are supported by a deployment and which are populated for
+that subject are implementation/runtime matters; the fixed eight-slot model
+is independent of those choices. When document and vector witnesses are both
+present, for example, the engine can detect that the vector embedding may have
+drifted from the document and trigger re-normalisation.
 
-**You do not have to choose between MongoDB and Neo4j and Redis. You get all
-of them, and they stay in sync.**
+**The Octad supplies one identity model across modalities; it is not a promise
+that every deployment or subject has every witness populated.**
 
 === Drift Detection
 
@@ -150,7 +165,7 @@ When drift exceeds a configurable threshold, VeriSimDB:
 
 1. Identifies the most authoritative modality
 2. Regenerates the drifted modalities from it
-3. Validates consistency across all eight views
+3. Validates consistency across the applicable, populated witnesses (within the fixed Octad model)
 4. Updates everything atomically (all at once, or not at all)
 
 == The Three Query Paths
@@ -313,12 +328,13 @@ A proof technique discovered for VCL-total can be applied to PanLL, and vice ver
 | Concept | One-Sentence Summary
 
 | **VeriSimDB**
-| A database where every entity exists in 8 views simultaneously, with automatic
-  drift detection and repair.
+| A multi-modal engine whose Octad model has eight fixed modality slots; which
+  witnesses are supported or populated can vary by implementation and subject.
 
 | **Octad**
-| The 8 simultaneous representations of a single entity (graph, vector, tensor,
-  semantic, document, temporal, provenance, spatial).
+| The fixed eight-slot model for graph, vector, tensor, semantic, document,
+  temporal, provenance, and spatial witnesses; a subject need not populate all
+  eight slots.
 
 | **VCL**
 | The fast, unverified query language for VeriSimDB.

docs/WHY-TYPE-SAFETY-MATTERS.adoc

@@ -168,10 +168,13 @@ FETCH orders.order_total WHERE orders.status = "completed"
 
 ==== Why It Matters for Databases
 
-In VeriSimDB, data exists across 8 modalities simultaneously (the octad). A
-typo in a modality reference could silently query the wrong view of your data.
-Schema binding ensures that every reference is checked against the live schema
-before the query runs.
+VeriSimDB's Octad names eight fixed modality slots, although a subject may
+have witness data in only a subset. A deployment's modality profile (which
+modalities it supports or enables) is a separate concept from both that fixed
+Octad and VCL-UT's `OctadSchema`. A typo in a modality reference could silently
+query the wrong view of your data; schema binding checks field references
+against the supplied schema. See
+link:standards/MODALITY-PROFILES.adoc[the profile/Octad contract].
 
 ---
 
@@ -436,10 +439,12 @@ FETCH OPTIONAL users WHERE users.email = ?email
 
 ==== Why It Matters for Databases
 
-In VeriSimDB, an entity's octad has exactly 8 modality slots but any subset
-might be populated. Cardinality safety ensures you know at compile time whether
-a modality query will return data or might be empty, eliminating an entire
-class of "expected data that was not there" bugs.
+In VeriSimDB, the Octad has exactly eight named modality slots, but any subset
+may have witness data for a particular entity. A modality profile can describe
+what an implementation supports; it does not prove that a subject has data in
+a supported modality. Cardinality safety concerns the possible result count,
+not the profile's modality count, and helps catch assumptions that a modality
+will necessarily return data when it might be empty.
 
 ---
 

docs/architecture/DECISIONS.adoc

@@ -45,6 +45,11 @@ toc::[]
 |Epistemic types via S5 modal logic
 |Accepted
 |2026-04-10
+
+|ADR-0007
+|Separate modality profiles from the fixed Octad schema (see link:../decisions/0007-modality-profiles-vs-octad-schema.adoc[record])
+|Accepted
+|2026-10-05
 |===
 
 ---