From 926857ab278de78543936283200d73c15d82aeed Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 17:50:47 +0000 Subject: [PATCH 01/10] proofs(octad): mechanise octad modality algebra (O-series + R1-R3) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit New formal/Octad.v mechanises the Modality Algebra of docs/papers/arcvix-octad-data-model.tex (sec:modality-algebra): - Merge Commutativity: the paper's one pen-and-paper proposition, now machine-checked (merge_commutative), plus R2/R3 companions (merge_associative, merge_idempotent). The CRDT laws are stated as implications from resolve's algebra — the honest resolution of #77's "R1-R3 likely false as written": octad merge inherits exactly the algebra of its conflict kernel. - O2 modality_cardinality + modality_exhaustive (fixed 8-element basis, mirroring ModalityStatus). - O10 complete_iff_no_missing (is_complete vs missing cross-method check). - Projection pi_M: idempotent + composition-as-meet (project_compose). - Enrichment enrich_* (inv:persist; sets target, preserves others). Closes on mval, ident, functional_extensionality_dep only; Print Assumptions confirms zero axiom slippage. Wired into formal/Justfile (octad + check-octad), coq-build.yml, and CROSS-REPO-MAP.adoc. Verified with coqc 8.18.0: all 9 modules compile, all 9 assumption guards pass. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- .github/workflows/coq-build.yml | 25 +++ formal/CROSS-REPO-MAP.adoc | 49 ++++- formal/Justfile | 17 +- formal/Octad.v | 368 ++++++++++++++++++++++++++++++++ 4 files changed, 453 insertions(+), 6 deletions(-) create mode 100644 formal/Octad.v diff --git a/.github/workflows/coq-build.yml b/.github/workflows/coq-build.yml index d6cd8e7..0c73717 100644 --- a/.github/workflows/coq-build.yml +++ b/.github/workflows/coq-build.yml @@ -90,6 +90,12 @@ jobs: set -euo pipefail coqc -q PlannerSemantic.v | tee PlannerSemantic.out + - name: Compile Octad.v + working-directory: formal + run: | + set -euo pipefail + coqc -q Octad.v | tee Octad.out + - name: Verify Provenance assumptions whitelist working-directory: formal run: | @@ -220,3 +226,22 @@ jobs: exit 1 fi echo "OK(PlannerSemantic): Q1-full semantic equivalence + membership" + + - name: Verify Octad assumptions whitelist + working-directory: formal + run: | + set -euo pipefail + # Whitelist: 2 Parameters (mval, ident) + functional_extensionality_dep + # (Coq stdlib). modality is inductive; resolve is an operation + # argument — neither is an axiom. + UNEXPECTED=$(awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Octad.out \ + | sort -u \ + | grep -vE '^(mval|ident|functional_extensionality_dep)$' || true) + if [ -n "$UNEXPECTED" ]; then + echo "ERROR(Octad): unexpected axiom(s) in Print Assumptions:" + echo "$UNEXPECTED" + echo "---" + cat Octad.out + exit 1 + fi + echo "OK(Octad): O-series + R1-R3 modality algebra whitelisted" diff --git a/formal/CROSS-REPO-MAP.adoc b/formal/CROSS-REPO-MAP.adoc index 8756d90..6cebf5e 100644 --- a/formal/CROSS-REPO-MAP.adoc +++ b/formal/CROSS-REPO-MAP.adoc @@ -79,6 +79,31 @@ Concretely: | `EchoGradedComonadInterface.agda` (existing) — graded comonad for "well-typed at type τ" | Type-preservation under reduction is the comonad ε ∘ δ = id property in the graded comonad of "well-typed terms at type τ". Reduction is the comonad action. The V2 mechanisation here is the MINIMUM-VIABLE core (booleans + opaque proof terms + conditional), closing #92 blockers 1 (big-step → small-step) and 2 (proof terms as values, no β-reduction). Full VCL extends mechanically per added expression form. Progress bundled as the type-soundness companion. +| O2 `modality_cardinality` + `modality_exhaustive` +| `formal/Octad.v` +| **Direct inductive — no echo-types lift needed** (finite-basis cardinality is structural, like C2) +| The 8-element `modality` enum mirrors `ModalityStatus`'s eight booleans. Cardinality (= 8) and exhaustiveness are structural facts over a finite inductive; same deliberate non-port rationale as the Transaction.v 3-state automaton. + +| O10 `complete_iff_no_missing` +| `formal/Octad.v` +| `EchoCharacteristic.agda` (existing) — collapse / echo-true / echo-false +| `present` partitions modalities into `Echo true` (a value) and `Echo false` (bot). `is_complete` (all present) iff `missing` (the false-fibre) is empty — the same true/false-fibre disjointness as D2. Doubles as a cross-method consistency check between `ModalityStatus::is_complete` and `ModalityStatus::missing`. + +| Projection `project_full` + `project_idempotent` + `project_compose` +| `formal/Octad.v` +| `EchoTruncation.agda` (existing) — same module N2 cites +| `pi_M` truncates the modality section `phi` to a mask. `project_compose` (`pi_M . pi_N = pi_{M /\ N}`) is the meet-semilattice law — projections form a bounded meet-semilattice under composition, the "structural modularity" of octads. Direct lift of `EchoTruncation`'s decoupling lemma, restricted to a Boolean modality mask. + +| R1-R3 `merge_commutative` + `merge_associative` + `merge_idempotent` +| `formal/Octad.v` +| Candidate NEW abstraction — join-semilattice of partial sections (to be established in echo-types per standing directive) +| The paper's `arcvix-octad-data-model.tex` Proposition "Merge Commutativity" had a one-line pen-and-paper proof; `merge_commutative` is it MECHANISED. Octad merge `(+)` inherits exactly the algebra of its conflict kernel `resolve`: `(+)` is commutative/associative/idempotent iff `resolve` is (R1/R2/R3 stated as implications). This is the honest resolution of verisimdb#77's "R1-R3 likely false as written": a CRDT-shaped `resolve` (join on a semilattice) instantiates all three; AutoMerge does not. Echo-types has no join-semilattice-of-sections module yet — companion issue to file per the standing directive. + +| Enrichment `enrich_sets_target` + `enrich_preserves_others` + `enrich_present` +| `formal/Octad.v` +| `EchoProvenance.agda` (existing) — for the audit-trail clause, via Provenance.v +| `enrich_m` is the fundamental write primitive: sets modality `m`, preserves the rest, preserves `id` (`inv:persist`). The `def:enrichment` clause "every enrichment appends to phi(P) and phi(R)" (audit trail) is the hash-chain append already mechanised in `Provenance.v` (`append_preserves_verified`, mapping to `EchoProvenance.agda` above) — not re-modelled here. + | Future: D7 `temporal_drift_zero_iff_monotone_unique` | _todo_ | `EchoLossTaxonomy.agda` + `EchoEntropy.agda` @@ -104,22 +129,38 @@ Concretely: . The verisimdb Coq module's docstring **MUST** name the corresponding echo-types module (or "no direct echo-types analogue, deliberate" with rationale). . Update `MEMORY.md` `[[verisimdb-proof-programme-started]]` cross-ref. -== Status (2026-06-01) +== Status (2026-06-03) -**Foundation pack COMPLETE — 8 of 8 closed.** +**Foundation pack COMPLETE — 10 of 10 closed** (P2, P3, P4, D1, D2, C2, C7, N2, Q1-lite, Q1-full, V2). * P2, P3 → `formal/Provenance.v` (PR #87) * D1, C2 → `formal/Drift.v`, `formal/Transaction.v` (PR #90) * D2, Q1-lite → `formal/Drift.v`, `formal/Planner.v` (PR #93) * C7 → `formal/WAL.v` (PR #94, closed #89) * N2 → `formal/Normalizer.v` (PR #95, closed #91) -* **V2 → `formal/VCL.v` (PR #96, closed #92)** +* V2 → `formal/VCL.v` (PR #96, closed #92) +* Q1-full → `formal/PlannerSemantic.v` (PR #97) +* P4 → `formal/Provenance.v` (PR #103) + +**Post-foundation — first module landed:** + +* **O-series + R1-R3 → `formal/Octad.v`** — the Modality Algebra of + `docs/papers/arcvix-octad-data-model.tex` (`sec:modality-algebra`) + mechanised: O2 (modality cardinality + exhaustiveness), O10 + (present-totality / `is_complete` ↔ `missing`), Projection (`pi_M` + idempotent + composition-as-meet), the paper's **Merge Commutativity** + proposition (`merge_commutative`) plus its R2/R3 companions, and + Enrichment (`enrich_*`, `inv:persist`). Closes on `mval`, `ident` and + `functional_extensionality_dep` only — Print Assumptions confirms no + slippage. Cross-doc to echo-types established by this file. Future work: +* File the echo-types companion issue for the merge join-semilattice + abstraction (R1-R3 row above) per the standing directive. * Port `WAL.v` + `Normalizer.v` + `VCL.v` to Agda within echo-types (refactor on top of `EchoResidue`, `EchoSearchExample`, `EchoGradedComonadInterface`). * Extend `VCL.v` from the 4-rule core to full VCL: filter expressions, projections, modality quantifiers, multi-proof composition. Each form adds one congruence step rule + one preservation case. * Add a CI check: every new `formal/*.v` module must reference an echo-types module name in its docstring (or `no-echo-types-analogue` with reason). -* Tackle the post-foundation theorems (D3-D8, C1-C11, F1-F6, Q2-Q9, V1-V8, P1, P4, P5) per the #77 inventory. +* Tackle the remaining post-foundation theorems (O1/O3-O9, D3-D8, C1/C3-C6/C8-C11, F1-F6, Q2-Q9, V1/V3-V8, P1, P5) per the #77 inventory. diff --git a/formal/Justfile b/formal/Justfile index eb5631d..9876c55 100644 --- a/formal/Justfile +++ b/formal/Justfile @@ -12,7 +12,7 @@ COQC := "coqc" # Compile every proof module. -all: provenance drift transaction planner wal normalizer vcl planner-semantic +all: provenance drift transaction planner wal normalizer vcl planner-semantic octad # --- Per-module compile recipes ------------------------------------------- @@ -40,11 +40,14 @@ vcl: planner-semantic: {{COQC}} -q PlannerSemantic.v | tee PlannerSemantic.out +octad: + {{COQC}} -q Octad.v | tee Octad.out + # --- Whitelist guards ----------------------------------------------------- # Each module declares its own set of Parameters/Axioms; the guard greps # Print Assumptions output for any name outside that module's whitelist. -check-assumptions: check-provenance check-drift check-transaction check-planner check-wal check-normalizer check-vcl check-planner-semantic +check-assumptions: check-provenance check-drift check-transaction check-planner check-wal check-normalizer check-vcl check-planner-semantic check-octad check-provenance: provenance @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Provenance.out \ @@ -124,6 +127,16 @@ check-planner-semantic: planner-semantic echo "OK(PlannerSemantic): Q1-full semantic equivalence + membership"; \ fi; } +check-octad: octad + @awk '/^[A-Za-z_][A-Za-z0-9_]* :/ {print $1}' Octad.out \ + | sort -u \ + | grep -vE '^(mval|ident|functional_extensionality_dep)$' \ + | { if read -r line; then \ + echo "ERROR(Octad): unexpected axiom: $line"; cat; exit 1; \ + else \ + echo "OK(Octad): O-series (cardinality, present-totality, projection) + R1-R3 merge algebra"; \ + fi; } + # Remove all build artefacts. clean: rm -f *.vo *.vos *.vok *.glob .*.aux *.out diff --git a/formal/Octad.v b/formal/Octad.v new file mode 100644 index 0000000..594081f --- /dev/null +++ b/formal/Octad.v @@ -0,0 +1,368 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* Copyright (c) Jonathan D.A. Jewell *) + +(** * VeriSimDB Octad Modality Algebra (O-series + R1-R3) + + Mechanises the OCTAD DATA MODEL and its MODALITY ALGEBRA as written + (on paper) in [docs/papers/arcvix-octad-data-model.tex], section + [sec:octad] "The Octad Data Model": + + - [def:modset] Modality Set — the fixed eight-element basis. + - [def:octad] Octad — (id, phi), phi : M -> Sigma_m u {bot}. + - [inv:persist] Identity Persistence — id is immutable under mutation. + - [def:projection] Projection pi_M. + - [def:merge] Merge (+) with conflict resolver [resolve]. + - Proposition Merge Commutativity (the paper's one proven claim). + - [def:enrichment] Enrichment enrich_m — the fundamental write primitive. + + ** Why this module exists + + The paper's "Modality Algebra" subsection [sec:modality-algebra] is + the octad-modularity experiment. Its sole stated proof — the + Proposition "Merge Commutativity" — is a one-line pen-and-paper + argument ("follows directly from the symmetry of the case analysis in + [def:merge] and the commutativity assumption on resolve"). + [merge_commutative] below is that proposition MECHANISED. The + associativity and idempotence companions ([merge_associative], + [merge_idempotent]) close the conditional CRDT-shape laws R1-R3 from + the verisimdb#77 inventory. + + ** On verisimdb#77's "honest uncertainty" about R1-R3 + + Issue #77 flags R1/R2/R3 ("CRDT-shaped octad merge") as "likely false + as currently written", because the concrete AutoMerge heuristic in + [verisim-normalizer/src/conflict.rs] is not unconditionally + commutative. The honest resolution, mechanised here, is the paper's: + the octad merge (+) inherits EXACTLY the algebra of its + conflict-resolution kernel [resolve]. (+) is commutative / associative + / idempotent precisely WHEN [resolve] is. The laws are therefore + stated as implications from [resolve]'s properties — the faithful + form. A CRDT-shaped [resolve] (e.g. a join on a semilattice) + instantiates all three; AutoMerge does not, and the implication makes + that explicit rather than over-claiming. + + ** Faithfulness to the Rust source + + The eight-constructor [modality] enumeration mirrors the eight boolean + fields of [ModalityStatus] in [rust-core/verisim-octad/src/lib.rs] + (graph, vector, tensor, semantic, document, temporal, provenance, + spatial). [is_complete] / [missing] mirror [ModalityStatus::is_complete] + and [ModalityStatus::missing]; [complete_iff_no_missing] is the + cross-method consistency check between those two independent Rust + functions (edit one without the other and this theorem breaks). + [resolve] abstracts [RegenerationStrategy] in + [rust-core/verisim-normalizer/src/regeneration.rs]. + + The [def:enrichment] clause "every enrichment appends a record to + phi'(P) and phi'(R)" (the audit-trail invariant) is the hash-chain + append modelled separately in [formal/Provenance.v] + ([append_preserves_verified]); it is intentionally NOT re-modelled + here. This module proves the structural part of enrichment: it sets + the target modality and leaves the others untouched. + + ** Abstraction note + + Per-modality value spaces Sigma_m are unified into one opaque [mval] + (the algebra laws are parametric in the value type, exactly as + [Drift.v] abstracts the score type). The dependently-typed layout + phi : forall m, Sigma_m u {bot} specialises this by a sigma-type; + that refinement is orthogonal to the algebraic laws proved here. + + ** Cross-doc: echo-types + + Projection pi_M is a TRUNCATION of the modality section phi — the same + shape as [EchoTruncation.agda], already cited by N2 in + [formal/CROSS-REPO-MAP.adoc]. Merge (+) under a semilattice [resolve] + is a JOIN; the conditional CRDT laws (R1-R3) are a candidate NEW + echo-types abstraction (join-semilattice of partial sections), flagged + for cross-documentation per the standing directive. See CROSS-REPO-MAP. + + Declared parameters: [mval], [ident]. Declared axioms: + [functional_extensionality_dep] (Coq stdlib, for octad/function + equality — the same whitelist entry as WAL.v and Normalizer.v). + + Build oracle: [just -f formal/Justfile octad]. CI: coq-build.yml. + + Tracking issue: hyperpolymath/verisimdb#77 (O-series + R1-R3). +*) + +Require Import Coq.Lists.List. +Require Import Coq.Bool.Bool. +Require Import Coq.Logic.FunctionalExtensionality. +Import ListNotations. + +(** ** [def:modset] — Modality Set + + The fixed eight-element basis M = {G,V,T,S,D,P,R,X}. Mirrors the eight + boolean fields of [ModalityStatus]. *) +Inductive modality : Type := +| Graph | Vector | Tensor | Semantic +| Document | Temporal | Provenance | Spatial. + +Definition all_modalities : list modality := + [Graph; Vector; Tensor; Semantic; Document; Temporal; Provenance; Spatial]. + +(** O2 — modality cardinality: an octad has exactly eight modalities. *) +Theorem modality_cardinality : length all_modalities = 8. +Proof. reflexivity. Qed. + +(** O2 — exhaustiveness: every modality is one of the eight. The CI + tripwire for a ninth modality being added without updating the + octad model. *) +Theorem modality_exhaustive : forall m, In m all_modalities. +Proof. intros m; destruct m; simpl; tauto. Qed. + +(** Decidable equality on the finite modality enumeration. Proved by + [decide equality]; introduces no axiom. *) +Definition modality_eq_dec (a b : modality) : {a = b} + {a <> b}. +Proof. decide equality. Defined. + +(** ** [def:octad] — Octad: identity + modality function *) + +(** Opaque per-modality value. Unifies the paper's Sigma_m; [None] models + the paper's bot (absence of a representation in that modality). *) +Parameter mval : Type. + +(** Opaque identifier (the paper's UUID). *) +Parameter ident : Type. + +(** An octad: an identifier together with a modality function + phi : modality -> option mval, where [None] = bot. *) +Record octad : Type := mk_octad { + oid : ident; + ophi : modality -> option mval; +}. + +(** Extensional octad equality: equal identifiers and equal modality + functions imply equal octads. *) +Lemma octad_ext : + forall o1 o2, + oid o1 = oid o2 -> + ophi o1 = ophi o2 -> + o1 = o2. +Proof. + intros [i1 p1] [i2 p2] Hid Hphi; simpl in *; subst; reflexivity. +Qed. + +(** ** Presence, completeness, and the missing-set (O10) *) + +Definition present (o : octad) (m : modality) : bool := + match ophi o m with Some _ => true | None => false end. + +(** Mirrors [ModalityStatus::is_complete]: all eight modalities present. *) +Definition is_complete (o : octad) : bool := + forallb (present o) all_modalities. + +(** Mirrors [ModalityStatus::missing]: the modalities that are bot. *) +Definition missing (o : octad) : list modality := + filter (fun m => negb (present o m)) all_modalities. + +(** General bridge: a list is [forallb p]-true iff filtering by [negb . p] + leaves nothing. *) +Lemma forallb_iff_filter_negb_nil : + forall (A : Type) (p : A -> bool) (l : list A), + forallb p l = true <-> filter (fun x => negb (p x)) l = []. +Proof. + induction l as [|x xs IH]; simpl. + - split; reflexivity. + - destruct (p x); simpl. + + exact IH. + + split; intro H; discriminate H. +Qed. + +(** O10 — present-totality: an octad is complete iff nothing is missing. + Cross-checks [ModalityStatus::is_complete] against + [ModalityStatus::missing]. *) +Theorem complete_iff_no_missing : + forall o, is_complete o = true <-> missing o = []. +Proof. + intros o. unfold is_complete, missing. + apply forallb_iff_filter_negb_nil. +Qed. + +(** ** [def:projection] — Projection pi_M + + Restrict the modality function to a mask [M : modality -> bool] (the + paper's subset M of modality), sending masked-out modalities to bot. *) +Definition project (M : modality -> bool) (o : octad) : octad := + mk_octad (oid o) (fun m => if M m then ophi o m else None). + +(** [inv:persist] for projection — identity is preserved. *) +Theorem project_preserves_id : + forall M o, oid (project M o) = oid o. +Proof. reflexivity. Qed. + +(** Projecting onto every modality is the identity. *) +Theorem project_full : + forall o, project (fun _ => true) o = o. +Proof. + intros o. apply octad_ext; [reflexivity|]. + apply functional_extensionality; intro m; reflexivity. +Qed. + +(** Projection is idempotent. *) +Theorem project_idempotent : + forall M o, project M (project M o) = project M o. +Proof. + intros M o. apply octad_ext; [reflexivity|]. + apply functional_extensionality; intro m; simpl. + destruct (M m); reflexivity. +Qed. + +(** Projection composes as mask intersection: pi_M . pi_N = pi_{M /\ N}. + The meet-semilattice law — the structural "modularity" of + projections. *) +Theorem project_compose : + forall M N o, + project M (project N o) = project (fun m => andb (M m) (N m)) o. +Proof. + intros M N o. apply octad_ext; [reflexivity|]. + apply functional_extensionality; intro m; simpl. + destruct (M m), (N m); reflexivity. +Qed. + +(** ** [def:merge] — Merge (+) + + [mcombine] is the per-modality merge kernel: + bot (+) bot = bot; v (+) bot = v; bot (+) v = v; + v1 (+) v2 = resolve v1 v2. + [resolve] is the policy-dependent conflict resolver (the paper's + [resolve]; [RegenerationStrategy] in the Rust source). It is an + ARGUMENT of the operation, not a global axiom — the algebra laws below + are implications from its properties. *) +Definition mcombine (resolve : mval -> mval -> mval) + (x y : option mval) : option mval := + match x, y with + | None, None => None + | Some a, None => Some a + | None, Some b => Some b + | Some a, Some b => Some (resolve a b) + end. + +(** Merge of two same-identifier octads. The result inherits the left + operand's identifier; under the paper's precondition [oid o1 = oid o2] + the choice of side is immaterial. *) +Definition merge (resolve : mval -> mval -> mval) (o1 o2 : octad) : octad := + mk_octad (oid o1) (fun m => mcombine resolve (ophi o1 m) (ophi o2 m)). + +(** Merge preserves the (shared) identifier — [inv:persist]. *) +Theorem merge_preserves_id : + forall resolve o1 o2, oid (merge resolve o1 o2) = oid o1. +Proof. reflexivity. Qed. + +(** ** Proposition (Merge Commutativity) — MECHANISED + + The paper: "If resolve is commutative, then (+) is commutative." + Its proof was one line; this is that proposition fully mechanised. + The same-identifier hypothesis [oid o1 = oid o2] is the paper's + "sharing the same identifier" precondition. *) +Theorem merge_commutative : + forall resolve o1 o2, + oid o1 = oid o2 -> + (forall a b, resolve a b = resolve b a) -> + merge resolve o1 o2 = merge resolve o2 o1. +Proof. + intros resolve o1 o2 Hid Hcomm. + apply octad_ext. + - simpl. exact Hid. + - apply functional_extensionality; intro m; simpl. + destruct (ophi o1 m) as [a|], (ophi o2 m) as [b|]; simpl; + try reflexivity. + rewrite Hcomm. reflexivity. +Qed. + +(** ** R2 — Merge associativity, under associative [resolve]. + + The left-identifier convention makes (+) associative with NO identifier + precondition: both nestings inherit [oid o1]. *) +Lemma mcombine_assoc : + forall resolve, + (forall a b c, resolve a (resolve b c) = resolve (resolve a b) c) -> + forall x y z, + mcombine resolve (mcombine resolve x y) z + = mcombine resolve x (mcombine resolve y z). +Proof. + intros resolve Hassoc x y z. + destruct x as [a|], y as [b|], z as [c|]; simpl; try reflexivity. + rewrite Hassoc. reflexivity. +Qed. + +Theorem merge_associative : + forall resolve o1 o2 o3, + (forall a b c, resolve a (resolve b c) = resolve (resolve a b) c) -> + merge resolve (merge resolve o1 o2) o3 + = merge resolve o1 (merge resolve o2 o3). +Proof. + intros resolve o1 o2 o3 Hassoc. + apply octad_ext; [reflexivity|]. + apply functional_extensionality; intro m; simpl. + apply mcombine_assoc. exact Hassoc. +Qed. + +(** ** R3 — Merge idempotence, under idempotent [resolve]. *) +Theorem merge_idempotent : + forall resolve o, + (forall a, resolve a a = a) -> + merge resolve o o = o. +Proof. + intros resolve o Hidem. + apply octad_ext; [reflexivity|]. + apply functional_extensionality; intro m; simpl. + destruct (ophi o m) as [a|]; simpl; [rewrite Hidem|]; reflexivity. +Qed. + +(** ** [def:enrichment] — Enrichment + + [enrich m v o] sets modality [m] to [v] and leaves all others + untouched (the paper's fundamental write primitive). *) +Definition enrich (m : modality) (v : mval) (o : octad) : octad := + mk_octad (oid o) + (fun m' => if modality_eq_dec m' m then Some v else ophi o m'). + +(** [inv:persist]: enrichment never changes the identifier. *) +Theorem enrich_preserves_id : + forall m v o, oid (enrich m v o) = oid o. +Proof. reflexivity. Qed. + +(** Enrichment writes the target modality. *) +Theorem enrich_sets_target : + forall m v o, ophi (enrich m v o) m = Some v. +Proof. + intros m v o; simpl. + destruct (modality_eq_dec m m); [reflexivity | congruence]. +Qed. + +(** Enrichment leaves every other modality untouched. *) +Theorem enrich_preserves_others : + forall m v o m', m' <> m -> ophi (enrich m v o) m' = ophi o m'. +Proof. + intros m v o m' Hneq; simpl. + destruct (modality_eq_dec m' m); [congruence | reflexivity]. +Qed. + +(** After enrichment the target modality is present (not bot) — a local + present-totality fact. *) +Theorem enrich_present : + forall m v o, present (enrich m v o) m = true. +Proof. + intros m v o. unfold present. rewrite enrich_sets_target. reflexivity. +Qed. + +(** ** Print Assumptions guard + + Allowed: [mval], [ident] (Parameters) and [functional_extensionality_dep] + (Coq stdlib). [modality] is inductive and [resolve] is an operation + argument — neither is an axiom. Any other name fails the CI guard. *) + +Print Assumptions modality_cardinality. +Print Assumptions modality_exhaustive. +Print Assumptions complete_iff_no_missing. +Print Assumptions project_full. +Print Assumptions project_idempotent. +Print Assumptions project_compose. +Print Assumptions merge_commutative. +Print Assumptions merge_associative. +Print Assumptions merge_idempotent. +Print Assumptions enrich_sets_target. +Print Assumptions enrich_preserves_others. +Print Assumptions enrich_present. From 4e4c698a6f2ea9c180cc84255ab93666d3c31db0 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 21:32:53 +0000 Subject: [PATCH 02/10] ci: green the governance + fuzz gate at root Three pre-existing gate failures on this repo, fixed at source (none were introduced by the Octad proofs in this branch): - governance / Licence consistency: LICENSE carried the MPL-2.0 body but no SPDX-License-Identifier line the estate check greps for. Add it (machine-readable identifier only; terms unchanged, Cargo.toml already declares MPL-2.0). - governance / Trusted-base reduction: enumerate all 13 Coq Axioms (0 Admitted/admit.) in docs/proof-debt.md per the standards policy, so the formal trusted base is documented and CI can no longer flag an undocumented escape hatch. Octad.v adds Parameters only, no axioms. - pr-fuzzing (address): ClusterFuzzLite's OSS-Fuzz image ships rustc 1.91-nightly, but burn / cubecl-zspace (transitive via verisim-tensor) require 1.92, so the CFLite fuzz build failed while the native "fuzz targets compile" job (newer rustc) passed. Two contained fixes: drop the unused verisim-octad dependency from fuzz/Cargo.toml (fuzz_octad_id only fuzzes UUID parsing, eliminating its burn chain), and pin a burn-compatible nightly with rust-src in .clusterfuzzlite/build.sh for the verisim-api-based fuzz_vql_parser. Both changes touch only the fuzz path; no other job's toolchain or dependency set changes. All previously-green jobs (Coq proofs, cargo test/clippy/deny/doc, Elixir, CodeQL, the rest of governance) are untouched. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- .clusterfuzzlite/build.sh | 13 ++++++ LICENSE | 2 + docs/proof-debt.md | 86 +++++++++++++++++++++++++++++++++++++++ fuzz/Cargo.toml | 7 ++-- 4 files changed, 105 insertions(+), 3 deletions(-) create mode 100644 docs/proof-debt.md diff --git a/.clusterfuzzlite/build.sh b/.clusterfuzzlite/build.sh index 6399b28..45a41de 100755 --- a/.clusterfuzzlite/build.sh +++ b/.clusterfuzzlite/build.sh @@ -12,6 +12,19 @@ set -euo pipefail +# ── Toolchain floor ────────────────────────────────────────────────────── +# The OSS-Fuzz base-builder-rust image pins an older nightly (rustc 1.91 at +# time of writing), but part of the dependency graph — burn / cubecl-zspace, +# pulled transitively via verisim-tensor (rust-core/fuzz -> verisim-api) — +# declares rust-version = 1.92. cargo-fuzz rebuilds the standard library with +# -Zbuild-std, so all we need is a new-enough nightly with rust-src present. +# Install one and force it for the whole script via RUSTUP_TOOLCHAIN. This is +# contained to the fuzz job: it never touches the main workspace toolchain or +# any other CI job. +rustup toolchain install nightly --profile minimal \ + --component rust-src --component llvm-tools-preview +export RUSTUP_TOOLCHAIN=nightly + # cargo-fuzz drives libfuzzer; install it if missing. if ! command -v cargo-fuzz &>/dev/null; then cargo install cargo-fuzz --locked diff --git a/LICENSE b/LICENSE index d0a1fa1..a06bf12 100644 --- a/LICENSE +++ b/LICENSE @@ -1,3 +1,5 @@ +SPDX-License-Identifier: MPL-2.0 + Mozilla Public License Version 2.0 ================================== diff --git a/docs/proof-debt.md b/docs/proof-debt.md new file mode 100644 index 0000000..8ce1d7b --- /dev/null +++ b/docs/proof-debt.md @@ -0,0 +1,86 @@ + +# Proof Debt — Trusted Base of the VeriSimDB Formal Development + +This document is the authoritative catalogue of **soundness-relevant escape +hatches** in VeriSimDB's machine-checked proofs, per the estate +[Trusted-Base Reduction Policy](https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc). +Every Coq `Axiom` (and any `Admitted` / `admit.`, of which there are currently +**none**) is enumerated here by `file:line`, with its justification. + +The Coq corpus lives in [`formal/`](../formal/). Each module is compiled by +`coqc` and its `Print Assumptions` output is grepped against a per-module +whitelist in [`formal/Justfile`](../formal/Justfile) and +[`.github/workflows/coq-build.yml`](../.github/workflows/coq-build.yml), so an +axiom that is **not** in this ledger cannot silently enter a theorem's trusted +base — CI fails on any unlisted assumption ("axiom slippage"). + +## Summary + +| Count | Kind | Status | +|------:|------|--------| +| 13 | Coq `Axiom` | Documented below; whitelisted; non-`Admitted` | +| 0 | `Admitted` / `admit.` | None — every theorem closes with `Qed` | +| 0 | Rust `unsafePerformIO` / `unsafeCoerce` | N/A (Rust core uses neither) | + +`formal/Octad.v` (the octad modality algebra) contributes **zero** axioms: it +closes on two `Parameter`s (`mval`, `ident`) plus the Coq stdlib +`functional_extensionality_dep`. `Parameter`s are interface points (opaque +carriers), not soundness escape hatches, and are tracked by the same +`Print Assumptions` guard. + +## Catalogue + +### `formal/Drift.v` — drift-score order laws (6 axioms) + +Minimal axiomatisation of the abstract `score` order (the Rust source is +`f64`). These are standard total-order / clamp laws, not domain assumptions. + +- `formal/Drift.v:46` — `le_refl` — reflexivity of the score order (`x <= x`). +- `formal/Drift.v:47` — `clamp_lower` — `clamp lo hi x` is `>= lo`. Mirrors `f64::clamp`. +- `formal/Drift.v:48` — `clamp_upper` — `clamp lo hi x` is `<= hi`. Mirrors `f64::clamp`. +- `formal/Drift.v:157` — `le_or_gt` — totality of the order (`s <= t` or `s > t`); faithful to the `f64` total order modulo NaN, which the clamp rules out. +- `formal/Drift.v:161` — `le_gt_exclusive` — `<=` and `>` are mutually exclusive. +- `formal/Drift.v:167` — `detector_iff_threshold` — the detector signals iff `score > threshold` (the `if score > threshold` guard at `verisim-drift/src/lib.rs`). + +### `formal/Provenance.v` — cryptographic assumption (1 axiom) + +- `formal/Provenance.v:59` — `sha256_collision_resistant` — injectivity of SHA-256 on `(content, parent_hash)`. Standard cryptographic assumption; **declared but unused** by the current P2/P3/P4 theorems (reserved for later uniqueness work). `Print Assumptions` confirms it is not in their trusted base. + +### `formal/WAL.v` — decidable equality (1 axiom) + +- `formal/WAL.v:57` — `eq_entity_dec` — decidable equality on `entity_id`. True for `String` in the Rust source (`store.rs`); axiomatised because the carrier is opaque. + +### `formal/Normalizer.v` — normalize spec contract (2 axioms) + +Encode the remediated N2 spec (see issue #91): the authoritative source is +never a drifted modality, and winner selection ignores drifted data. + +- `formal/Normalizer.v:73` — `winner_excludes_drifted` — the normalize winner is never a drifted modality ("never copy FROM corrupt sources"). +- `formal/Normalizer.v:80` — `winner_stable_off_drifted` — winner selection depends only on non-drifted modalities ("frozen rank, not `Utc::now()`"). + +### `formal/Planner.v` / `formal/PlannerSemantic.v` — optimizer contract (3 axioms) + +Structural contracts on `Planner::optimize` (a `stable_sort_by`): it permutes +plan nodes, and per-node filters commute at the set level. + +- `formal/Planner.v:63` — `optimize_is_permutation` — the optimizer reorders nodes without adding or dropping any (Q1-lite). +- `formal/PlannerSemantic.v:94` — `optimize_is_permutation` — same contract, restated for the Q1-full semantic-equivalence development. +- `formal/PlannerSemantic.v:78` — `exec_node_comm` — per-node set-restrictions commute (filter intersection is order-independent across operator types). + +## Discharge paths (future work) + +These are deliberate, mathematically-standard assumptions, not gaps in +reasoning. Where the estate wishes to shrink the trusted base further: + +- The `Drift.v` order laws and `WAL.v` `eq_entity_dec` discharge automatically + if the abstract carriers are instantiated to concrete Coq types + (`R`/`Q`/`bool`-decidable strings) — they exist only because the carriers are + kept opaque to mirror the Rust generics. +- `sha256_collision_resistant` is a genuine cryptographic axiom; it can be + re-homed to a CryptHOL/Isabelle development per the issue #77 tool-selection + table, but stays an assumption in any first-order model. +- `optimize_is_permutation` / `exec_node_comm` are checkable by a Rust property + test over `Planner::optimize`; that test is the intended runtime corroboration. + +See `formal/CROSS-REPO-MAP.adoc` for the echo-types correspondence of each +theorem these axioms support. diff --git a/fuzz/Cargo.toml b/fuzz/Cargo.toml index a6b35d5..ff29670 100644 --- a/fuzz/Cargo.toml +++ b/fuzz/Cargo.toml @@ -11,9 +11,10 @@ cargo-fuzz = true [dependencies] libfuzzer-sys = "0.4" uuid = "1.23" - -[dependencies.verisim-octad] -path = "../rust-core/verisim-octad" +# NOTE: this harness fuzzes UUID parsing only (see fuzz_targets/fuzz_octad_id.rs); +# it deliberately does NOT depend on verisim-octad. Pulling verisim-octad would +# drag in verisim-tensor -> burn (rust-version 1.92), which the OSS-Fuzz image's +# older nightly cannot build. Keep this crate's dependency surface minimal. # Prevent this from interfering with workspaces [workspace] From 7eaec69db534dab7e203d86f4d32fe86b3a4bd71 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 21:41:39 +0000 Subject: [PATCH 03/10] =?UTF-8?q?ci(fuzz):=20build=20fuzz=5Fvql=5Fparser?= =?UTF-8?q?=20=E2=80=94=20distinct=20package=20name=20+=20robust=20copy?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The toolchain pin + dropping verisim-octad from the top-level fuzz crate fixed fuzz_octad_id (now builds in ~3s), which unmasked a second, latent failure in the rust-core fuzz crate: `cargo fuzz build` there finished in 0.01s producing no binary, so the copy step failed with "cannot stat target/*/release/fuzz_vql_parser". Root cause: BOTH fuzz crates declared the same package name `verisimdb-fuzz`. ClusterFuzzLite builds both in one OSS-Fuzz project over a shared cargo target directory, so the second root package collided with the first's build fingerprint and was treated as up to date — a silent no-op. Fixes: - Rename the rust-core fuzz package to `verisimdb-rustcore-fuzz` so the two crates no longer collide. - Rewrite .clusterfuzzlite/build.sh to build each target *by name*, locate the produced binary via `find` (not a brittle glob), and fail loudly with a clear message if a target produces nothing. burn (pulled via verisim-api) is CPU-only here — the native "fuzz targets compile" job builds it in ~80s — so the ASan + build-std build is tractable under the nightly installed by the toolchain floor above. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- .clusterfuzzlite/build.sh | 32 ++++++++++++++++++++++++-------- rust-core/fuzz/Cargo.toml | 7 ++++++- 2 files changed, 30 insertions(+), 9 deletions(-) diff --git a/.clusterfuzzlite/build.sh b/.clusterfuzzlite/build.sh index 45a41de..04d23f9 100755 --- a/.clusterfuzzlite/build.sh +++ b/.clusterfuzzlite/build.sh @@ -30,15 +30,31 @@ if ! command -v cargo-fuzz &>/dev/null; then cargo install cargo-fuzz --locked fi -# ── fuzz_octad_id — top-level fuzz crate ───────────────────────────────── -cd "${SRC}/verisimdb/fuzz" -cargo fuzz build --release --sanitizer="${SANITIZER:-address}" -cp target/*/release/fuzz_octad_id "${OUT}/" +# Build one named fuzz target in a given crate directory and copy the binary +# to $OUT. We build the target *by name* and then locate the produced binary +# wherever cargo-fuzz placed it (instead of a brittle glob), failing loudly if +# nothing was produced. Combined with the two fuzz crates carrying distinct +# package names, this is robust against the shared-target-dir collision that +# previously turned the second build into a silent 0.01s no-op. +build_target() { + local crate_dir="$1" target="$2" + echo "── building fuzz target '${target}' in ${crate_dir} ──" + ( + cd "${crate_dir}" + cargo fuzz build --release --sanitizer="${SANITIZER:-address}" "${target}" + local bin + bin="$(find . -type f -name "${target}" -path '*/release/*' -print -quit)" + if [[ -z "${bin}" ]]; then + echo "ERROR: no '${target}' binary produced under ${crate_dir}" >&2 + exit 1 + fi + cp "${bin}" "${OUT}/${target}" + echo "── copied ${bin} -> ${OUT}/${target} ──" + ) +} -# ── fuzz_vql_parser — rust-core fuzz crate ─────────────────────────────── -cd "${SRC}/verisimdb/rust-core/fuzz" -cargo fuzz build --release --sanitizer="${SANITIZER:-address}" -cp target/*/release/fuzz_vql_parser "${OUT}/" +build_target "${SRC}/verisimdb/fuzz" fuzz_octad_id +build_target "${SRC}/verisimdb/rust-core/fuzz" fuzz_vql_parser # Optional seed corpora — empty for now, will populate as we discover # interesting inputs. Comment in once corpora exist: diff --git a/rust-core/fuzz/Cargo.toml b/rust-core/fuzz/Cargo.toml index 69cc0c0..1d69bcf 100644 --- a/rust-core/fuzz/Cargo.toml +++ b/rust-core/fuzz/Cargo.toml @@ -1,7 +1,12 @@ # SPDX-License-Identifier: MPL-2.0 +# NOTE: package name MUST differ from the top-level fuzz crate (verisimdb-fuzz). +# ClusterFuzzLite builds both fuzz crates in one OSS-Fuzz project; two root +# packages sharing a name collide in the shared cargo target directory, which +# silently no-ops the second build (it "Finished in 0.01s" and produces no +# binary). Distinct names keep their build fingerprints separate. [package] -name = "verisimdb-fuzz" +name = "verisimdb-rustcore-fuzz" version = "0.0.0" publish = false edition = "2021" From 771b7e95ae021f25e15d535d464eeb619ac4165d Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 21:44:01 +0000 Subject: [PATCH 04/10] =?UTF-8?q?docs(readme):=20add=20"Conceptual=20Model?= =?UTF-8?q?=20=E2=80=94=20Continuous=20Identity,=20Not=20Passive=20Storage?= =?UTF-8?q?"?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Inserts the consonance/identity-transition framing at the top of the README (owner-provided copy), led by the non-negotiable anchor: VeriSimDB maintains identity consonance across modal witnesses and federation boundaries; VCL expresses propositions and epistemic requests; VCL-total validates whether proposed identity transitions are admissible. Adds the lifecycle states, the core-terms table, and the VCL vs VCL-total distinction. Partial by design: this is the conceptual-model insert only. The full terminology sweep (query language -> consonance language, HEXAD/6-modal -> octad, the VQL section reframe, deletion -> retract/tombstone/expunge), EXPLAINME.adoc, and the matching vcl-ut docs are the follow-up pass, held pending owner review before wider propagation. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- README.adoc | 91 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 90 insertions(+), 1 deletion(-) diff --git a/README.adoc b/README.adoc index c7171f8..4fd3020 100644 --- a/README.adoc +++ b/README.adoc @@ -4,10 +4,99 @@ :toc: :toc-placement!: -**Cross-system data consistency that catches drift before it causes damage.** +[.lead] +**VeriSimDB does not merely store records. It maintains identity consonance across modal witnesses and federation boundaries. VCL expresses propositions and epistemic requests over that consonance state. VCL-total validates whether proposed identity transitions are admissible.** + +_Cross-modal consonance that catches identity drift before it causes damage._ toc::[] +== Conceptual Model: Continuous Identity, Not Passive Storage + +VeriSimDB is not primarily a database of records. It is a federated consonance engine for continuously maintained identity claims. + +A VeriSimDB "entity" is best understood as a **consonance subject**: an identity under active maintenance across multiple modal witnesses. Those witnesses may include graph structure, vector embeddings, tensor data, semantic annotations, documents, temporal history, provenance chains, and spatial references. Together they form the octad view of an identity. + +The central problem VeriSimDB solves is not merely storing these views. The central problem is deciding whether they still refer to the same identity, whether they have drifted, whether a repair or normalisation is justified, whether a federated claim should be accepted, and whether an identity claim should be strengthened, weakened, merged, split, retracted, tombstoned, or expunged under policy. + +This means VeriSimDB should be read as a lifecycle system for identity claims: + +---- +Candidate + -> Declared + -> Asserted + -> Consonant + -> Drifting + -> Normalised + -> Merged / Split + -> Retracted + -> Tombstoned + -> Expunged only under explicit policy +---- + +A modality failure is not automatically an identity failure. For example: + +---- +document changed, vector stale -> modal drift +hash chain broken -> provenance/integrity failure +remote node asserts incompatible type -> federation conflict +all live witnesses retracted -> inactive or tombstoned identity +---- + +These states have different proof obligations and different repair paths. + +=== Core Terms + +[cols="1,2"] +|=== +|Term |Meaning + +|Consonance Subject +|The lifecycle-managed identity under consideration. + +|Identity Claim +|A claim that some subject exists, has a property, has a relation, or survives a transition. + +|Modality Witness +|One modal presentation of a subject: graph, vector, tensor, semantic, document, temporal, provenance, or spatial. + +|Drift Report +|Evidence that one or more modal witnesses no longer cohere. + +|Transition +|A proposed identity event: declare, assert, retract, normalise, merge, split, federate, tombstone. + +|Proof Obligation +|What must be shown before a transition is admissible. + +|Federation Attestation +|A remote or local authority claim about identity, provenance, validity, or trust. + +|Tombstone +|A durable marker that an identity claim is no longer live, without pretending it never existed. +|=== + +=== VCL and VCL-total + +VCL is the production consonance language used to propose and inspect identity transitions. VCL statements are not simply queries against a passive store. They are propositions or epistemic requests directed at a consonance engine. + +VCL-total / VCL-UT is the proof-bearing safety substrate behind VCL. It validates whether a proposed transition is admissible under the relevant schema, modality, provenance, authority, freshness, resource, effect, federation, and proof constraints. + +In short: + +---- +VeriSimDB stores and maintains identity consonance. +VCL expresses identity propositions and epistemic requests. +VCL-total checks whether those transitions are safe and admissible. +---- + +The proof goal is not "prove the whole database correct". The proof goal is narrower and more useful: + +---- +prove that this identity transition is admissible, +traceable, authorised, and consonant enough to affect live state. +---- + == The Problem: Silent Data Drift Your data lives in multiple systems — graphs, vector stores, document indexes, time-series databases. When one system's view of an entity silently diverges from the others, you get **data drift**: stale embeddings, broken provenance chains, graph edges referencing deleted documents, spatial coordinates that no longer match textual descriptions. From 05118e1fd6514efe037e46778fc333fb9edd0098 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 21:51:47 +0000 Subject: [PATCH 05/10] ci(fuzz): host both fuzz targets in the single cargo-fuzz crate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Earlier attempts mis-diagnosed the rust-core fuzz failure (toolchain, then package-name collision). The real cause, from the build log: cargo-fuzz resolves exactly ONE fuzz directory per project — it walks up from the cwd to the nearest `fuzz/`, which is always the top-level /fuzz — so the `rust-core/fuzz` crate is unreachable via `cargo fuzz` and silently resolves back to the top-level manifest: cd /src/verisimdb/rust-core/fuzz cargo fuzz build ... fuzz_vql_parser error: no bin target named `fuzz_vql_parser` available bin targets: fuzz_octad_id ... "cargo" "build" "--manifest-path" "/src/verisimdb/fuzz/Cargo.toml" ... Fix (convention-aligned): host fuzz_vql_parser in the top-level fuzz/ crate alongside fuzz_octad_id (add the verisim-api dep + the target source), and build both from fuzz/ in .clusterfuzzlite/build.sh. rust-core/fuzz is reverted to pristine and retained only for the native `cargo check` matrix leg in rust-ci.yml, so no currently-green check changes. The toolchain floor (nightly + rust-src) still satisfies burn's rust-version 1.92 for the verisim-api-backed parser fuzzer. Verified locally: build.sh passes `bash -n`; `cargo metadata` parses fuzz/Cargo.toml with both [[bin]] targets and the verisim-api path dep. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- .clusterfuzzlite/build.sh | 17 ++++++++--------- fuzz/Cargo.toml | 20 ++++++++++++++++---- fuzz/fuzz_targets/fuzz_vql_parser.rs | 25 +++++++++++++++++++++++++ rust-core/fuzz/Cargo.toml | 10 ++++------ 4 files changed, 53 insertions(+), 19 deletions(-) create mode 100644 fuzz/fuzz_targets/fuzz_vql_parser.rs diff --git a/.clusterfuzzlite/build.sh b/.clusterfuzzlite/build.sh index 04d23f9..35dd119 100755 --- a/.clusterfuzzlite/build.sh +++ b/.clusterfuzzlite/build.sh @@ -15,7 +15,7 @@ set -euo pipefail # ── Toolchain floor ────────────────────────────────────────────────────── # The OSS-Fuzz base-builder-rust image pins an older nightly (rustc 1.91 at # time of writing), but part of the dependency graph — burn / cubecl-zspace, -# pulled transitively via verisim-tensor (rust-core/fuzz -> verisim-api) — +# pulled transitively via verisim-tensor (fuzz -> verisim-api) — # declares rust-version = 1.92. cargo-fuzz rebuilds the standard library with # -Zbuild-std, so all we need is a new-enough nightly with rust-src present. # Install one and force it for the whole script via RUSTUP_TOOLCHAIN. This is @@ -30,12 +30,11 @@ if ! command -v cargo-fuzz &>/dev/null; then cargo install cargo-fuzz --locked fi -# Build one named fuzz target in a given crate directory and copy the binary -# to $OUT. We build the target *by name* and then locate the produced binary -# wherever cargo-fuzz placed it (instead of a brittle glob), failing loudly if -# nothing was produced. Combined with the two fuzz crates carrying distinct -# package names, this is robust against the shared-target-dir collision that -# previously turned the second build into a silent 0.01s no-op. +# Build one named fuzz target from the project's single cargo-fuzz crate +# (fuzz/) and copy the binary to $OUT. cargo-fuzz resolves ONE fuzz directory +# per project, so both targets are hosted in fuzz/; building each by name is +# reliable. We then locate the produced binary wherever cargo-fuzz placed it +# (not a brittle glob), failing loudly if nothing was produced. build_target() { local crate_dir="$1" target="$2" echo "── building fuzz target '${target}' in ${crate_dir} ──" @@ -53,8 +52,8 @@ build_target() { ) } -build_target "${SRC}/verisimdb/fuzz" fuzz_octad_id -build_target "${SRC}/verisimdb/rust-core/fuzz" fuzz_vql_parser +build_target "${SRC}/verisimdb/fuzz" fuzz_octad_id +build_target "${SRC}/verisimdb/fuzz" fuzz_vql_parser # Optional seed corpora — empty for now, will populate as we discover # interesting inputs. Comment in once corpora exist: diff --git a/fuzz/Cargo.toml b/fuzz/Cargo.toml index ff29670..2e8beaf 100644 --- a/fuzz/Cargo.toml +++ b/fuzz/Cargo.toml @@ -8,13 +8,19 @@ edition = "2021" [package.metadata] cargo-fuzz = true +# This is the project's single cargo-fuzz crate. cargo-fuzz resolves ONE fuzz +# directory per project (it walks up from the cwd to the nearest `fuzz/`, which +# is always this one), so EVERY target ClusterFuzzLite builds must live here — +# a target in rust-core/fuzz is unreachable via `cargo fuzz` and silently +# resolves back to this manifest. fuzz_vql_parser therefore lives here too. +# rust-core/fuzz is retained only for the native `cargo check` matrix leg in +# rust-ci.yml; the canonical fuzz harnesses are these. [dependencies] libfuzzer-sys = "0.4" uuid = "1.23" -# NOTE: this harness fuzzes UUID parsing only (see fuzz_targets/fuzz_octad_id.rs); -# it deliberately does NOT depend on verisim-octad. Pulling verisim-octad would -# drag in verisim-tensor -> burn (rust-version 1.92), which the OSS-Fuzz image's -# older nightly cannot build. Keep this crate's dependency surface minimal. + +[dependencies.verisim-api] +path = "../rust-core/verisim-api" # Prevent this from interfering with workspaces [workspace] @@ -26,5 +32,11 @@ path = "fuzz_targets/fuzz_octad_id.rs" test = false doc = false +[[bin]] +name = "fuzz_vql_parser" +path = "fuzz_targets/fuzz_vql_parser.rs" +test = false +doc = false + [profile.release] debug = 1 diff --git a/fuzz/fuzz_targets/fuzz_vql_parser.rs b/fuzz/fuzz_targets/fuzz_vql_parser.rs new file mode 100644 index 0000000..624cddc --- /dev/null +++ b/fuzz/fuzz_targets/fuzz_vql_parser.rs @@ -0,0 +1,25 @@ +// SPDX-License-Identifier: MPL-2.0 +// +// Fuzz target for the VQL parser. +// Run with: cargo +nightly fuzz run fuzz_vql_parser +// +// This fuzzer feeds arbitrary byte strings to the VQL parser to find +// panics, hangs, or memory safety issues. The parser should gracefully +// reject invalid input without crashing. + +#![no_main] + +use libfuzzer_sys::fuzz_target; + +fuzz_target!(|data: &[u8]| { + // Only attempt to parse valid UTF-8 strings — the VQL parser + // operates on &str, not raw bytes. + if let Ok(input) = std::str::from_utf8(data) { + // Limit input size to prevent timeouts on extremely long strings + if input.len() <= 4096 { + // The parser should never panic on any valid UTF-8 input. + // We don't care about the result — only that it doesn't crash. + let _ = verisim_api::vql::tokenize(input); + } + } +}); diff --git a/rust-core/fuzz/Cargo.toml b/rust-core/fuzz/Cargo.toml index 1d69bcf..977c204 100644 --- a/rust-core/fuzz/Cargo.toml +++ b/rust-core/fuzz/Cargo.toml @@ -1,12 +1,10 @@ # SPDX-License-Identifier: MPL-2.0 -# NOTE: package name MUST differ from the top-level fuzz crate (verisimdb-fuzz). -# ClusterFuzzLite builds both fuzz crates in one OSS-Fuzz project; two root -# packages sharing a name collide in the shared cargo target directory, which -# silently no-ops the second build (it "Finished in 0.01s" and produces no -# binary). Distinct names keep their build fingerprints separate. +# Retained for the native `cargo check` matrix leg in rust-ci.yml. The +# ClusterFuzzLite build uses the top-level fuzz/ crate (cargo-fuzz resolves a +# single fuzz dir per project), where fuzz_vql_parser is canonically hosted. [package] -name = "verisimdb-rustcore-fuzz" +name = "verisimdb-fuzz" version = "0.0.0" publish = false edition = "2021" From d9a3c3c24f9922c2dc02b1d34fbd08cf44ef3d90 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 23:01:48 +0000 Subject: [PATCH 06/10] ci(security): SHA-pin all GitHub Actions (clears Hypatia workflow_audit) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pin every third-party action to its exact commit SHA (resolved via `git ls-remote`, peeled to the commit for annotated tags) with a `# version` comment, across the four workflows that still used floating tags: build-validation.yml, elixir-ci.yml, rust-ci.yml, fuzz.yml. 54 `uses:` lines pinned; zero floating refs remain repo-wide. Each SHA is exactly what the floating tag resolved to, so runtime behaviour is unchanged — this only removes the moved-tag supply-chain hazard and clears the Hypatia scan's unpinned_action findings. Pins (action @ sha # tag): actions/checkout 9f698171… # v6.0.3 dtolnay/rust-toolchain 29eef336… # stable Swatinem/rust-cache 42dc69e1… # v2 erlef/setup-beam 8251c486… # v1 actions/cache 27d5ce7f… # v5 codecov/codecov-action e79a6962… # v6 rustsec/audit-check 69366f33… # v2.0.0 EmbarkStudios/cargo-deny-action 8f84122a… # v2 taiki-e/install-action 28ba36d3… # cargo-llvm-cov / 25435dc8… # v2 actions/upload-artifact 043fb46d… # v7 Note (separate, untouched): coq-build.yml / codeql.yml pin actions/checkout@df4cb1c… but comment it "# v6.0.3" in one place and "# v4" in another; df4cb1c is v4. The new pins use the correct v6.0.3 SHA. Harmonising the older pins is a follow-up cleanup. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- .github/workflows/build-validation.yml | 10 ++--- .github/workflows/elixir-ci.yml | 24 +++++----- .github/workflows/fuzz.yml | 12 ++--- .github/workflows/rust-ci.yml | 62 +++++++++++++------------- 4 files changed, 54 insertions(+), 54 deletions(-) diff --git a/.github/workflows/build-validation.yml b/.github/workflows/build-validation.yml index 24907ed..3439fef 100644 --- a/.github/workflows/build-validation.yml +++ b/.github/workflows/build-validation.yml @@ -15,9 +15,9 @@ jobs: name: Rust build validation runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - run: cargo check --workspace validate-elixir: @@ -27,8 +27,8 @@ jobs: run: working-directory: elixir-orchestration steps: - - uses: actions/checkout@v6.0.3 - - uses: erlef/setup-beam@v1 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 with: elixir-version: "1.17" otp-version: "27" diff --git a/.github/workflows/elixir-ci.yml b/.github/workflows/elixir-ci.yml index 1a5235f..c10f500 100644 --- a/.github/workflows/elixir-ci.yml +++ b/.github/workflows/elixir-ci.yml @@ -38,12 +38,12 @@ jobs: - elixir: "1.17" otp: "27" steps: - - uses: actions/checkout@v6.0.3 - - uses: erlef/setup-beam@v1 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 with: elixir-version: ${{ matrix.elixir }} otp-version: ${{ matrix.otp }} - - uses: actions/cache@v5 + - uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5 with: path: | elixir-orchestration/deps @@ -63,12 +63,12 @@ jobs: run: working-directory: elixir-orchestration steps: - - uses: actions/checkout@v6.0.3 - - uses: erlef/setup-beam@v1 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 with: elixir-version: "1.17" otp-version: "27" - - uses: actions/cache@v5 + - uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5 with: path: | elixir-orchestration/deps @@ -76,7 +76,7 @@ jobs: key: ${{ runner.os }}-mix-coverage-${{ hashFiles('elixir-orchestration/mix.lock') }} - run: mix deps.get - run: mix coveralls.json - - uses: codecov/codecov-action@v6 + - uses: codecov/codecov-action@e79a6962e0d4c0c17b229090214935d2e33f8354 # v6 with: files: elixir-orchestration/cover/excoveralls.json flags: elixir @@ -90,12 +90,12 @@ jobs: run: working-directory: elixir-orchestration steps: - - uses: actions/checkout@v6.0.3 - - uses: erlef/setup-beam@v1 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 with: elixir-version: "1.17" otp-version: "27" - - uses: actions/cache@v5 + - uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5 with: path: | elixir-orchestration/deps @@ -116,9 +116,9 @@ jobs: run: working-directory: elixir-orchestration steps: - - uses: actions/checkout@v6.0.3 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 - - uses: erlef/setup-beam@v1 + - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 with: elixir-version: "1.17" otp-version: "27" diff --git a/.github/workflows/fuzz.yml b/.github/workflows/fuzz.yml index bdf64f5..870a9d2 100644 --- a/.github/workflows/fuzz.yml +++ b/.github/workflows/fuzz.yml @@ -25,9 +25,9 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - name: Run core fuzz compile check run: | cd rust-core/fuzz @@ -40,9 +40,9 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - name: Run debugger fuzz compile check run: | cd debugger/fuzz diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index f1ee480..02e1390 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -28,8 +28,8 @@ jobs: name: rustfmt runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable with: components: rustfmt - run: cargo fmt --all -- --check @@ -38,20 +38,20 @@ jobs: name: clippy (all-targets) runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable with: components: clippy - - uses: Swatinem/rust-cache@v2 + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - run: cargo clippy --workspace --all-targets --no-deps -- -D warnings test: name: cargo test runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - run: cargo test --workspace --no-fail-fast doc: @@ -60,17 +60,17 @@ jobs: env: RUSTDOCFLAGS: "-D warnings" steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - run: cargo doc --workspace --no-deps audit: name: cargo audit runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: rustsec/audit-check@v2.0.0 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: rustsec/audit-check@69366f33c96575abad1ee0dba8212993eecbe998 # v2.0.0 with: token: ${{ secrets.GITHUB_TOKEN }} @@ -78,8 +78,8 @@ jobs: name: cargo deny runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: EmbarkStudios/cargo-deny-action@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: EmbarkStudios/cargo-deny-action@8f84122a46a358a27cb0625d85ad60ab436a1b87 # v2 with: command: check advisories bans licenses sources @@ -87,24 +87,24 @@ jobs: name: benchmarks compile runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - run: cargo bench --no-run coverage: name: cargo-llvm-cov (≥60%) runs-on: ubuntu-latest steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable with: components: llvm-tools-preview - - uses: Swatinem/rust-cache@v2 - - uses: taiki-e/install-action@cargo-llvm-cov + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 + - uses: taiki-e/install-action@28ba36d36bfc4814f98a469ff9f76b2a41e9aa8a # cargo-llvm-cov - name: Generate lcov report run: cargo llvm-cov --workspace --lcov --output-path lcov.info - - uses: codecov/codecov-action@v6 + - uses: codecov/codecov-action@e79a6962e0d4c0c17b229090214935d2e33f8354 # v6 with: files: lcov.info flags: rust @@ -122,10 +122,10 @@ jobs: runs-on: ubuntu-latest if: github.event_name == 'workflow_dispatch' || github.event_name == 'schedule' steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 - - uses: taiki-e/install-action@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 + - uses: taiki-e/install-action@25435dc8dd3baed7417e0c96d3fe89013a5b2e09 # v2 with: tool: cargo-mutants - name: Run mutation tests on core invariant crates @@ -140,7 +140,7 @@ jobs: --no-shuffle \ --output mutants-out/ continue-on-error: true - - uses: actions/upload-artifact@v7 + - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7 if: always() with: name: mutants-report @@ -155,7 +155,7 @@ jobs: - fuzz/Cargo.toml - rust-core/fuzz/Cargo.toml steps: - - uses: actions/checkout@v6.0.3 - - uses: dtolnay/rust-toolchain@stable - - uses: Swatinem/rust-cache@v2 + - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: dtolnay/rust-toolchain@29eef336d9b2848a0b548edc03f92a220660cdb8 # stable + - uses: Swatinem/rust-cache@42dc69e1aa15d09112580998cf2ef0119e2e91ae # v2 - run: cargo check --manifest-path ${{ matrix.manifest }} From a039900b28bf8a09411538e6704e2e9a079cc63b Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 23:18:15 +0000 Subject: [PATCH 07/10] test(elixir): exclude :integration by default so CI suite is green MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit elixir-ci.yml runs `mix test` / `mix coveralls.json` on a plain runner with no databases, but test/test_helper.exs only called ExUnit.start() — so the 7 @moduletag :integration federation-adapter test files ran, hit their skip_if_unavailable/1 guard, and produced 90 hard failures (the guard flunks rather than skipping). That failed both `compile + test` and `ExCoveralls`. Add ExUnit.configure(exclude: [:integration]) so the integration suite is opt-in, matching the documented convention (CLAUDE.md: run with `mix test --include integration` once the test-infra stack is up). All unit tests — including the 10 adapter *_test.exs files — still run, so coverage stays above the enforced gate (coveralls.json minimum_coverage = 40; current 42.2%, integration tests contribute ~1% so the margin holds). These failures were pre-existing; they only surfaced on this PR because SHA-pinning elixir-ci.yml's actions added that file to its changed-paths trigger. The pins are retained. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- elixir-orchestration/test/test_helper.exs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/elixir-orchestration/test/test_helper.exs b/elixir-orchestration/test/test_helper.exs index bfa2917..ecc8abc 100644 --- a/elixir-orchestration/test/test_helper.exs +++ b/elixir-orchestration/test/test_helper.exs @@ -1,3 +1,14 @@ # SPDX-License-Identifier: MPL-2.0 ExUnit.start() + +# Federation-adapter integration tests are tagged `@moduletag :integration` and +# require the live test-infra database stack (MongoDB, Redis, Neo4j, ClickHouse, +# SurrealDB, InfluxDB, object storage). They cannot run on a plain CI runner, so +# they are EXCLUDED by default; their `skip_if_unavailable/1` guard otherwise +# turns "DB not reachable" into a hard failure rather than a skip. +# +# Run them with the stack up via: mix test --include integration +# (see CLAUDE.md "Federation Adapter Integration Tests"). +ExUnit.configure(exclude: [:integration]) + From c466f4dece9fe017ce410f185e80505d5bb505f5 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 3 Jun 2026 23:20:04 +0000 Subject: [PATCH 08/10] style(elixir): drop trailing blank line in test_helper.exs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit mix format --check-formatted (elixir-ci compile+test step, which runs before the test step) rejected a trailing blank line left by the previous commit. Logic unchanged — the :integration exclusion is intact; this only satisfies the formatter so the suite can proceed. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- elixir-orchestration/test/test_helper.exs | 1 - 1 file changed, 1 deletion(-) diff --git a/elixir-orchestration/test/test_helper.exs b/elixir-orchestration/test/test_helper.exs index ecc8abc..e956728 100644 --- a/elixir-orchestration/test/test_helper.exs +++ b/elixir-orchestration/test/test_helper.exs @@ -11,4 +11,3 @@ ExUnit.start() # Run them with the stack up via: mix test --include integration # (see CLAUDE.md "Federation Adapter Integration Tests"). ExUnit.configure(exclude: [:integration]) - From 250da66fe26ee58f4c202b3186e638d0b1c1ca0d Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 4 Jun 2026 09:39:42 +0000 Subject: [PATCH 09/10] revert(ci): decouple Elixir CI from #109 (track separately) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Restore .github/workflows/elixir-ci.yml and elixir-orchestration/test/test_helper.exs to their main versions, so this PR no longer touches elixir-orchestration/** or elixir-ci.yml — that workflow's paths filter then leaves it dormant on #109. Why: SHA-pinning elixir-ci.yml's actions added that file to its own changed-paths trigger, running the (previously dormant) Elixir workflow on this proofs/hardening PR and exposing deep pre-existing Elixir-suite debt unrelated to #109: - 7 @moduletag :integration adapter suites need the live test-infra DBs; - 10 genuine consensus/Raft (KRaft*) unit failures — stale assertions plus timing-flaky GenServer.call timeouts; - unit coverage 39.4% vs the 40% gate once integration is excluded. That remediation needs local `mix` iteration and is tracked separately. #109 retains the Octad proofs, the governance + fuzz root fixes, and the SHA-pins on build-validation.yml, rust-ci.yml and fuzz.yml. Refs hyperpolymath/verisimdb#77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- .github/workflows/elixir-ci.yml | 24 +++++++++++------------ elixir-orchestration/test/test_helper.exs | 10 ---------- 2 files changed, 12 insertions(+), 22 deletions(-) diff --git a/.github/workflows/elixir-ci.yml b/.github/workflows/elixir-ci.yml index c10f500..1a5235f 100644 --- a/.github/workflows/elixir-ci.yml +++ b/.github/workflows/elixir-ci.yml @@ -38,12 +38,12 @@ jobs: - elixir: "1.17" otp: "27" steps: - - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 - - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 + - uses: actions/checkout@v6.0.3 + - uses: erlef/setup-beam@v1 with: elixir-version: ${{ matrix.elixir }} otp-version: ${{ matrix.otp }} - - uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5 + - uses: actions/cache@v5 with: path: | elixir-orchestration/deps @@ -63,12 +63,12 @@ jobs: run: working-directory: elixir-orchestration steps: - - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 - - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 + - uses: actions/checkout@v6.0.3 + - uses: erlef/setup-beam@v1 with: elixir-version: "1.17" otp-version: "27" - - uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5 + - uses: actions/cache@v5 with: path: | elixir-orchestration/deps @@ -76,7 +76,7 @@ jobs: key: ${{ runner.os }}-mix-coverage-${{ hashFiles('elixir-orchestration/mix.lock') }} - run: mix deps.get - run: mix coveralls.json - - uses: codecov/codecov-action@e79a6962e0d4c0c17b229090214935d2e33f8354 # v6 + - uses: codecov/codecov-action@v6 with: files: elixir-orchestration/cover/excoveralls.json flags: elixir @@ -90,12 +90,12 @@ jobs: run: working-directory: elixir-orchestration steps: - - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 - - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 + - uses: actions/checkout@v6.0.3 + - uses: erlef/setup-beam@v1 with: elixir-version: "1.17" otp-version: "27" - - uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5 + - uses: actions/cache@v5 with: path: | elixir-orchestration/deps @@ -116,9 +116,9 @@ jobs: run: working-directory: elixir-orchestration steps: - - uses: actions/checkout@9f698171ed81b15d1823a05fc7211befd50c8ae0 # v6.0.3 + - uses: actions/checkout@v6.0.3 - - uses: erlef/setup-beam@8251c48667b97e88a0a24ec512f5b72a039fcea7 # v1 + - uses: erlef/setup-beam@v1 with: elixir-version: "1.17" otp-version: "27" diff --git a/elixir-orchestration/test/test_helper.exs b/elixir-orchestration/test/test_helper.exs index e956728..bfa2917 100644 --- a/elixir-orchestration/test/test_helper.exs +++ b/elixir-orchestration/test/test_helper.exs @@ -1,13 +1,3 @@ # SPDX-License-Identifier: MPL-2.0 ExUnit.start() - -# Federation-adapter integration tests are tagged `@moduletag :integration` and -# require the live test-infra database stack (MongoDB, Redis, Neo4j, ClickHouse, -# SurrealDB, InfluxDB, object storage). They cannot run on a plain CI runner, so -# they are EXCLUDED by default; their `skip_if_unavailable/1` guard otherwise -# turns "DB not reachable" into a hard failure rather than a skip. -# -# Run them with the stack up via: mix test --include integration -# (see CLAUDE.md "Federation Adapter Integration Tests"). -ExUnit.configure(exclude: [:integration]) From 7f712025ae98605609da731be285f82c3759d5f7 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 4 Jun 2026 12:25:31 +0000 Subject: [PATCH 10/10] docs(readme,explainme): consonance / identity-transition terminology pass Completes the reframing begun in 771b7e9 (Conceptual Model section + the non-negotiable anchor). README.adoc: - "What VeriSimDB Does": "cross-modal consistency engine" -> "federated consonance engine"; entities -> consonance subjects / modal witnesses. - Comparison table: "Query language / VQL" -> "Consonance language / VCL"; "Formal verification / VQL-DT" -> "Proof-bearing transitions / VCL-total". - "VQL: VeriSim Query Language" -> "VCL: VeriSim Consonance Language": leads with the consonance operations (DECLARE/ASSERT/RETRACT/INSPECT/VERIFY/ MERGE/SPLIT/NORMALISE) as the semantic model, with an honest NOTE that the current in-repo grammar (spec/grammar.ebnf v3.0) is a read-style SQL-shaped convenience (HEXAD = legacy octad-source keyword) superseded by VCL-total. SELECT/PROOF examples retained (they reflect the real grammar) but reframed as epistemic inspection of consonance state. - VQL-DT -> VCL-total; doc-link labels VQL -> VCL (file paths kept; the vql-*/VQL-* file rename is a separate tracked cleanup). EXPLAINME.adoc (new): human-readable orientation embedding the anchor, the identity lifecycle, "modality failure != identity failure", core terms (matching README), the VCL/VCL-total/VeriSimDB split, "retraction != deletion", and an honest implemented-vs-design-intent section. Docs/terminology only; no runtime changes. Machine-readable + cross-agent propagation deliberately untouched (held per owner direction). Refs #77. https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME --- EXPLAINME.adoc | 130 +++++++++++++++++++++++++++++++++++++++++++++++++ README.adoc | 76 +++++++++++++++++++---------- 2 files changed, 179 insertions(+), 27 deletions(-) create mode 100644 EXPLAINME.adoc diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc new file mode 100644 index 0000000..e2a94e3 --- /dev/null +++ b/EXPLAINME.adoc @@ -0,0 +1,130 @@ +// SPDX-License-Identifier: MPL-2.0 += EXPLAINME — VeriSimDB Orientation +:toc: +:toc-placement!: + +[.lead] +**VeriSimDB does not merely store records. It maintains identity consonance across modal witnesses and federation boundaries. VCL expresses propositions and epistemic requests over that consonance state. VCL-total validates whether proposed identity transitions are admissible.** + +This is the human-readable orientation. For the feature/benefit framing see +link:README.adoc[README.adoc]; for the normative VCL grammar see +link:docs/VQL-SPEC.adoc[the VCL specification] (file still historically named +`VQL-SPEC.adoc`). + +toc::[] + +== The one idea to hold onto + +If you take away a single thing: a VeriSimDB "entity" is **not a row**. It is a +**consonance subject** — an identity under continuous maintenance across up to +eight *modal witnesses* (the octad: graph, vector, tensor, semantic, document, +temporal, provenance, spatial). The system's job is not storage; it is deciding, +continuously, whether those witnesses still cohere as one identity — and what to +do when they do not. + +So the verbs are not CRUD. They are **lifecycle transitions** on identity claims: +declare, assert, inspect, verify, transform, retract, merge, split, normalise, +tombstone. + +== Why "consonance", not "consistency" + +Classic databases enforce *consistency* up front (transactions, locks) and treat +divergence as an error to prevent. VeriSimDB instead expects modal witnesses to +drift — a document is edited before its embedding is recomputed; a spatial +coordinate is refined independently of the text — and treats that drift as a +**first-class, typed condition** to be measured, classified, and repaired. The +maintained property is *consonance*: the witnesses still refer to the same +identity, within policy. + +A modality failure is therefore **not** automatically an identity failure. These +are distinct states with distinct proof obligations and repair paths: + +[cols="1,1"] +|=== +|Observation |State + +|document changed, vector stale |modal drift (repairable by normalisation) +|hash chain broken |provenance / integrity failure +|remote node asserts an incompatible type |federation conflict (needs arbitration) +|all live witnesses retracted |inactive / tombstoned identity +|=== + +== The identity lifecycle + +---- +Candidate + -> Declared + -> Asserted + -> Consonant + -> Drifting + -> Normalised + -> Merged / Split + -> Retracted + -> Tombstoned + -> Expunged (only under explicit policy) +---- + +**Retraction is not deletion.** A retracted claim usually stays visible to +provenance, audit, federation, and proof systems — it is no longer *live*. +Tombstoning durably retires an identity or claim without pretending it never +existed. Expungement is a separate, policy-governed operation. + +== Core terms + +[cols="1,2"] +|=== +|Term |Meaning + +|Consonance Subject |The lifecycle-managed identity under consideration. +|Identity Claim |A claim that some subject exists, has a property, has a relation, or survives a transition. +|Modality Witness |One modal presentation of a subject: graph, vector, tensor, semantic, document, temporal, provenance, or spatial. +|Drift Report |Evidence that one or more modal witnesses no longer cohere. +|Transition |A proposed identity event: declare, assert, retract, normalise, merge, split, federate, tombstone. +|Proof Obligation |What must be shown before a transition is admissible. +|Federation Attestation |A remote or local authority claim about identity, provenance, validity, or trust. +|Tombstone |A durable marker that an identity claim is no longer live, without pretending it never existed. +|=== + +== VCL, VCL-total, and VeriSimDB + +[cols="1,3"] +|=== +|Layer |Role + +|**VeriSimDB** |The federated consonance engine. Stores and maintains identity consonance across the octad of modal witnesses; detects drift; repairs under policy. +|**VCL** |The production consonance language. Statements are *propositions* (`DECLARE`, `ASSERT`, `RETRACT`) or *epistemic requests* (`INSPECT`, `VERIFY`), plus `MERGE` / `SPLIT` / `NORMALISE` — directed at the engine, not queries against a passive store. +|**VCL-total** |The proof-bearing safety substrate behind VCL (repo: https://github.com/hyperpolymath/vcl-ut[vcl-ut]). It decides whether a proposed identity transition is *admissible* under schema, modality, provenance, authority, freshness, resource, effect, federation, and proof constraints. +|=== + +The proof goal is deliberately narrow and useful — **not** "prove the whole +database correct", but: + +---- +prove that THIS identity transition is admissible, +traceable, authorised, and consonant enough to affect live state. +---- + +== What is implemented vs design intent (honest) + +* **Implemented today:** the octad stores (graph, vector, tensor, semantic, + document, temporal, provenance hash-chain, spatial R-tree); cross-modal drift + detection + self-normalisation; the federation coordinator; and a VCL surface + whose *current* in-repo grammar (`spec/grammar.ebnf` v3.0) is a read-style, + SQL-shaped convenience (`SELECT … FROM HEXAD …`, with `HEXAD` the legacy + keyword for the octad source) plus `PROOF`-carrying statements. +* **The model / direction:** the lifecycle/consonance verbs (`DECLARE` … + `NORMALISE`) and full proof-bearing admissibility are the semantic target, + carried by **VCL-total** (vcl-ut). Read the SQL-ish read-path as *epistemic + inspection of consonance state*, not row retrieval. +* **Formal core:** invariants are mechanised in Coq under `formal/` (octad + modality algebra, provenance hash-chain, drift bounds, planner equivalence, + WAL/normaliser idempotence, VCL preservation) — see + link:formal/CROSS-REPO-MAP.adoc[the cross-repo map] and + link:docs/proof-debt.md[the trusted-base ledger]. + +== Where to go next + +* link:README.adoc[README.adoc] — capabilities, comparisons, quick start. +* link:docs/VQL-SPEC.adoc[VCL specification] — normative grammar (historically `VQL-SPEC.adoc`). +* https://github.com/hyperpolymath/vcl-ut[vcl-ut] — VCL-total, the proof-bearing substrate. +* link:KNOWN-ISSUES.adoc[KNOWN-ISSUES.adoc] — honest-gaps audit. diff --git a/README.adoc b/README.adoc index 4fd3020..6b1d5b7 100644 --- a/README.adoc +++ b/README.adoc @@ -105,7 +105,7 @@ Traditional tools detect drift _after_ it causes downstream failures. VeriSimDB == What VeriSimDB Does -VeriSimDB is a **cross-modal consistency engine**. Each entity exists simultaneously across up to 8 representations (the **octad**) with automatic drift detection and self-normalisation: +VeriSimDB is a **federated consonance engine**. Each consonance subject is maintained across up to 8 modal witnesses (the **octad**), with continuous drift detection and self-normalisation: ---- ┌─────────────────────────────────────────────────────────────┐ @@ -192,15 +192,15 @@ Sample output: |Partial |**Hash-chain verified** -|Query language +|Consonance language |No (Python API) |No (UI) -|**VQL (with dependent types)** +|**VCL (propositions + epistemic requests)** -|Formal verification +|Proof-bearing transitions |No |No -|**VQL-DT (proof certificates)** +|**VCL-total (admissibility proofs)** |=== == The Octad: Eight Modalities @@ -330,34 +330,56 @@ VeriSimDB can also operate as a **federation coordinator** over existing databas └────────────────────────────────────────────────────────────────┘ ---- -== VQL: VeriSim Query Language +== VCL: VeriSim Consonance Language -VQL provides unified querying across all eight modalities with two execution paths: +VCL statements are **propositions and epistemic requests to a consonance engine**, not queries against a passive store. They propose, inspect, verify, transform, retract, merge, split, and normalise identity claims across the eight modal witnesses (see the Conceptual Model section above). The proof-bearing safety substrate behind VCL is **VCL-total** (https://github.com/hyperpolymath/vcl-ut[vcl-ut]), which decides whether a proposed identity transition is _admissible_. -=== Slipstream (Fast, No Proofs) +The consonance operations: + +[cols="1,3"] +|=== +|Operation |Meaning + +|`DECLARE` |introduce a candidate identity claim +|`ASSERT` |strengthen or add evidence to an identity claim +|`RETRACT` |revoke, weaken, or retire a live claim (not erasure — see below) +|`INSPECT` |observe consonance, drift, provenance, or federation state +|`VERIFY` |request proof-bearing validation of a claim or transition +|`MERGE` |join identities when consonance evidence supports it +|`SPLIT` |separate an over-coalesced identity +|`NORMALISE` |repair drift when a justified repair path exists +|=== + +NOTE: The lifecycle/consonance verbs above are the **semantic model**, carried fully by VCL-total. The current in-repo surface grammar (`spec/grammar.ebnf` v3.0) still exposes a read-style, SQL-shaped convenience (`SELECT … FROM …`, plus legacy `INSERT`/`UPDATE`/`DELETE` mutation forms) and uses `HEXAD` as the legacy keyword for the octad source (8 modal witnesses, retained for backward compatibility). Read the read-path below as **epistemic inspection of consonance state**, not row retrieval from a passive store. + +=== Inspection surface — Slipstream (fast, no proofs) + +A read-only convenience for inspecting consonance state. `HEXAD ` names the octad source; `DRIFT(...)` inspects cross-modal divergence: [source,sql] ---- --- Query across modalities +-- Inspect across modal witnesses SELECT GRAPH.*, DOCUMENT.*, VECTOR.* FROM HEXAD 'entity-001' --- Cross-modal drift detection in WHERE clause +-- Cross-modal drift inspection SELECT * FROM HEXAD 'entity-001' WHERE DRIFT(VECTOR, DOCUMENT) > 0.3 --- Modality existence checks +-- Modality-witness presence checks SELECT * FROM HEXAD 'entity-001' WHERE PROVENANCE EXISTS AND TENSOR NOT EXISTS --- Federation queries +-- Federated inspection SELECT * FROM FEDERATION /* WITH DRIFT STRICT ---- -=== VQL-DT (Dependent Types with Proof Certificates) +=== Proof-bearing statements — VCL-total (dependent types + proof certificates) + +A `PROOF` clause makes a statement proof-bearing: VCL-total must discharge the attached obligation before the result is admissible. [source,sql] ---- --- Query with existence proof +-- Statement carrying an existence proof obligation SELECT GRAPH.* FROM HEXAD 'entity-001' PROOF EXISTENCE(entity-001) @@ -365,12 +387,12 @@ SELECT GRAPH.* FROM HEXAD 'entity-001' SELECT * FROM HEXAD 'entity-001' PROOF EXISTENCE(entity-001) AND PROVENANCE(entity-001) --- Integrity verification with contract +-- Integrity verification against a contract SELECT GRAPH.* FROM HEXAD 'entity-001' PROOF INTEGRITY(my_contract) ---- -VQL-DT queries return a `ProvedResult` with data AND a proof certificate: +VCL-total proof-bearing statements return a `ProvedResult` with data AND a proof certificate: [source,elixir] ---- @@ -424,7 +446,7 @@ iex -S mix ---- cargo test # Rust: 510+ tests cd elixir-orchestration -mix test # Elixir: 160+ tests (VQL, consensus, telemetry, federation, hypatia) +mix test # Elixir: 160+ tests (VCL, consensus, telemetry, federation, hypatia) ---- === CI & Coverage @@ -494,7 +516,7 @@ grpcurl -plaintext localhost:50051 list # Health check grpcurl -plaintext localhost:50051 verisimdb.VeriSimService/Health -# Execute a VQL query +# Submit a VCL statement grpcurl -plaintext -d '{"query": "SELECT * FROM octads LIMIT 10"}' \ localhost:50051 verisimdb.VeriSimService/Query @@ -525,13 +547,13 @@ verisimdb/ │ ├── lib/verisim/ │ │ ├── drift/ # DriftMonitor GenServer │ │ ├── entity/ # EntityServer (per-entity GenServer) -│ │ ├── query/ # VQL parser, executor, bridge +│ │ ├── query/ # VCL parser, executor, bridge │ │ └── rust_client.ex # HTTP client for Rust core │ └── test/ ├── demos/ │ └── drift-detection/ # Drift detection demo script ├── docs/ # Specifications and design documents -│ ├── vql-grammar.ebnf # VQL formal grammar +│ ├── vql-grammar.ebnf # VCL formal grammar │ ├── vql-formal-semantics.adoc │ └── vql-type-system.adoc ├── registry/ # ReScript federation registry @@ -550,7 +572,7 @@ Universities and research institutions federate their archives while maintaining Vector embeddings and symbolic graphs coexist in the same namespace. AI systems query both modalities without ETL, with formal proof certificates guaranteeing query correctness. === Verifiable Data Exchange -ZKP proofs and dependent types enable tamper-evident knowledge exchange. VQL-DT queries return data with cryptographic proof certificates — you can verify the result without trusting the source. +ZKP proofs and dependent types enable tamper-evident knowledge exchange. VCL-total proof-bearing statements return data with cryptographic proof certificates — you can verify the result without trusting the source. == Documentation @@ -565,14 +587,14 @@ Quick links: * link:SECURITY.md[Security Policy] — threat model and disclosure process * link:AUDIT.adoc[Audit Index] — RSR audit-trail index -VQL language: +VCL language (file paths retain the historical `vql-` / `VQL-` names; the in-repo file rename is a separate, tracked cleanup): * link:docs/getting-started.adoc[Getting Started] — step-by-step setup guide -* link:docs/VQL-SPEC.adoc[VQL Specification] — normative language spec -* link:docs/vql-grammar.ebnf[VQL Grammar] — formal EBNF -* link:docs/vql-formal-semantics.adoc[VQL Formal Semantics] — operational semantics -* link:docs/vql-type-system.adoc[VQL Type System] — dependent types + bidirectional checking -* link:docs/vql-examples.adoc[VQL Examples] — worked examples +* link:docs/VQL-SPEC.adoc[VCL Specification] — normative language spec +* link:docs/vql-grammar.ebnf[VCL Grammar] — formal EBNF +* link:docs/vql-formal-semantics.adoc[VCL Formal Semantics] — operational semantics +* link:docs/vql-type-system.adoc[VCL Type System] — dependent types + bidirectional checking +* link:docs/vql-examples.adoc[VCL Examples] — worked examples Deployment & operations: