feat(verisim-modular-experiment): Ed25519, multi-peer, VCL subset

All three deferred Phase-3 follow-ups complete. 126/126 assertions
green across 5 test suites.

Ed25519 (task 7):
- impl/Crypto.jl wraps Sodium.jl libsodium bindings
- VerisimCore.Store holds Ed25519KeyPair; Signature.key_id now carries
  32-byte pubkey; ed25519_sign/ed25519_verify replace SHA-256 placeholders
- VectorPeer and DocumentPeer hold their own independent keypairs
- test_seams.jl +7 assertions: crypto round-trip, tampered-signature
  rejection, hash-chain integrity under real Ed25519

Multi-peer non-interference (task 8):
- impl/peers/DocumentPeer.jl — second Federable shape
- drift/Metrics.jl: added d_VD (TeX §4.3) and d_SD; dispatcher
  canonicalises {semantic, vector, document} pair ordering
- test_noninterference.jl: 15 assertions — 3-way parity over (S,V),
  (S,D), (V,D); adding Document peer leaves (S,V) drift unchanged;
  Document LWW writes don't affect Vector state; independent Ed25519
  keypairs per peer

VCL subset (task 9):
- impl/vcl/Query.jl — AST: ProofIntegrity, ProofConsistency, ProofFreshness
- impl/vcl/Prover.jl — routes clauses to VerisimCore + FederationManager
- impl/vcl/Parser.jl — hand-written tokeniser + recursive descent for
  PROOF INTEGRITY/CONSISTENCY/FRESHNESS syntax
- test_vcl.jl: 32 assertions — parse+prove round-trips, tampered-chain
  detection, renormalisation over absent shapes, error cases

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

Author: hyperpolymath

verisim-modular-experiment/.machine_readable/6a2/STATE.a2ml

@@ -10,7 +10,7 @@
     (purpose "Research experiment: can any octad shape be entirely absent (store-level)
               without making VCL consonance claims unsound?")
     (type "research-prototype")
-    (completion-percentage 55))
+    (completion-percentage 78))
 
   (current-position
     (phase "phase-3-complete-seams-sorted")
@@ -63,9 +63,21 @@
       (description "First Federable peer: DriftProjector, CoherenceProjector, LWWAcceptor.")
       (completion 100))
     (component "julia-crypto-ed25519"
-      (status in-progress)
-      (description "Replacing placeholder SHA-256 with real Ed25519 via libsodium.")
-      (completion 50))
+      (status complete)
+      (description "Real Ed25519 via Sodium.jl/libsodium. Signatures over provenance
+                    entries and attestations. 7 round-trip assertions in test_seams.jl.")
+      (completion 100))
+    (component "document-peer"
+      (status complete)
+      (description "Second Federable peer. Exercises multi-peer non-interference:
+                    drift pairs (S,V), (S,D), (V,D); independent Ed25519 keys.")
+      (completion 100))
+    (component "vcl-subset"
+      (status complete)
+      (description "VCLQuery AST, VCLProver evaluator, VCLParser string parser.
+                    Supports PROOF INTEGRITY, CONSISTENCY with DRIFT < θ, FRESHNESS.
+                    32 assertions in test_vcl.jl.")
+      (completion 100))
     (component "documentation"
       (status complete)
       (description "README, PLAN, PROOF-NEEDS, DESIGN, OCTAD-SHAPES, CORE-CANDIDATES,
@@ -87,7 +99,17 @@
     (result "seam-tests"
       (command "julia --project=. test/test_seams.jl")
       (status pass)
-      (assertions 21)))
+      (assertions 30))
+    (result "non-interference-tests"
+      (command "julia --project=. test/test_noninterference.jl")
+      (status pass)
+      (assertions 15))
+    (result "vcl-tests"
+      (command "julia --project=. test/test_vcl.jl")
+      (status pass)
+      (assertions 32)))
+
+  (total-assertions 126)
 
   (foldback-to-main-verisimdb
     (applied
@@ -98,10 +120,10 @@
       (item "Normalizer regeneration stub-status doc update (documented in FOLDBACK.adoc)")))
 
   (critical-next-actions
-    (action "Finish Ed25519 wiring (impl/Crypto.jl written, needs VerisimCore/VectorPeer update)")
-    (action "Add second Federable peer (Document) for multi-peer non-interference test")
-    (action "Write minimal VCL parser/evaluator exercising FROM FEDERATION syntax")
-    (action "Update this STATE.a2ml after each"))
+    (action "Phase 4 dogfood: wire KRLAdapter.jl against VerisimCore+FederationManager")
+    (action "Phase 5 writeup: document findings, adoption guide, foldback to main verisimdb")
+    (action "Optional: add Tensor and Spatial Federable peers for 4-peer parity coverage")
+    (action "Optional: Zig FFI port of VerisimCore for production readiness"))
 
   (session-history
     (session "2026-04-05"

verisim-modular-experiment/EXPLAINME.adoc

@@ -111,9 +111,22 @@ See `spec/federation-contract.adoc` for details.
 
 == What's deferred past Phase 3?
 
-* **Ed25519 placeholder → real** — code in `impl/Crypto.jl`, wiring into VerisimCore in progress.
-* **Multi-peer non-interference** — Phase 3 tested one peer; need N≥2.
-* **VCL parser/evaluator surface** — parity was proved at the drift layer; syntax layer is convenience.
+All three immediate follow-ups now complete:
+
+* ✓ **Ed25519** — real Ed25519 via libsodium (Sodium.jl). `impl/Crypto.jl` +
+  VerisimCore/VectorPeer/DocumentPeer all signed with real keypairs.
+* ✓ **Multi-peer non-interference** — `impl/peers/DocumentPeer.jl` registered
+  alongside VectorPeer. 15 assertions confirm drift pairs (S,V), (S,D), (V,D)
+  compose; each peer has an independent Ed25519 keypair.
+* ✓ **VCL parser/evaluator** — `impl/vcl/{Query,Prover,Parser}.jl`. Supports
+  PROOF INTEGRITY, PROOF CONSISTENCY WITH DRIFT < θ (with OVER scope),
+  PROOF FRESHNESS. 32 assertions.
+
+Remaining:
+
+* **Phase 4 dogfood** — wire `KRLAdapter.jl` against this VerisimCore.
+* **Phase 5 writeup** — findings document, adoption guide, main-verisimdb foldback.
+* **Optional Zig FFI port** — production readiness if Path B ships.
 
 == What if the result had been negative?
 

verisim-modular-experiment/docs/sessions/2026-04-05-blitz.adoc

@@ -11,8 +11,13 @@ absent?") and blitz pace.
 * **Phase 0 — Octad archaeology:** COMPLETED.
 * **Phase 1 — Core identification:** COMPLETED.
 * **Phase 2 — Federation contract (Idris2 ABI):** COMPLETED — typechecks clean in Idris2 0.8.0.
-* **Phase 3 — Reference core + Vector federation (Julia):** decision gate PASSED — 70/70 assertions green. Deferred: Ed25519, multi-peer non-interference, VCL parser.
+* **Phase 3 — Reference core + Vector federation (Julia):** decision gate PASSED — 70/70 assertions green.
 * **Seam audit:** COMPLETED — `docs/SEAMS.adoc`. High+medium priority seams fixed; low-priority documented as language-idiom.
+* **Ed25519 wiring:** COMPLETED — real libsodium-backed signing via `impl/Crypto.jl`. Store and peers hold Ed25519 keypairs; signatures verified end-to-end.
+* **Multi-peer non-interference:** COMPLETED — `impl/peers/DocumentPeer.jl` as second Federable peer. 15 assertions confirm drift pairs (S,V), (S,D), (V,D) compose, independent keys, LWW isolation.
+* **VCL subset:** COMPLETED — `impl/vcl/{Query,Prover,Parser}.jl`. 32 assertions covering PROOF INTEGRITY, CONSISTENCY with DRIFT, FRESHNESS, parser round-trips, tamper detection.
+
+**Grand total: 126 assertions green across 5 test suites.**
 
 == Key findings
 

verisim-modular-experiment/impl/FederationManager.jl

@@ -199,10 +199,12 @@ end
 # Duck-typed peer value retrieval. Each peer type provides a `_peer_value`
 # specialisation at the call site via method dispatch or via this path.
 function _peer_value(peer, octad_id)
-    # Try method-based lookup; fall back to Dict access on .embeddings
-    # for VectorPeer compatibility.
+    # Duck-typed peer storage access. Each peer type carries its shape's
+    # values in a named Dict field; we check the known ones.
     if hasfield(typeof(peer), :embeddings)
         return get(peer.embeddings, octad_id, nothing)
+    elseif hasfield(typeof(peer), :documents)
+        return get(peer.documents, octad_id, nothing)
     end
     error("FederationManager: don't know how to extract value from peer type $(typeof(peer))")
 end

verisim-modular-experiment/impl/VerisimCore.jl

@@ -15,10 +15,14 @@ module VerisimCore
 
 using SHA
 
+# Crypto module is loaded by the including script before VerisimCore
+# (flat-include scaffold). Reached via Main namespace.
+
 export OctadId, Timestamp, Signature, SemanticBlob,
        ProvenanceEntry, ProvenanceChain, TemporalHistory,
        CoreOctad, Store,
-       get_core, enrich!, attest, verify_attest, now_ts
+       get_core, enrich!, attest, verify_attest, now_ts,
+       ed25519_sign, ed25519_verify
 
 # -----------------------------------------------------------------------
 # Primitive types (mirror Idris2 ABI)
@@ -52,12 +56,14 @@ Base.:(==)(a::Timestamp, b::Timestamp) = a.epoch_nanos == b.epoch_nanos
 now_ts() = Timestamp(Int64(time_ns()))
 
 """
-Signature placeholder. TODO(Phase 3 defaults validation): replace with
-Ed25519 via Nettle.jl or similar. For scaffold, using SHA-256 as a
-stand-in 'signature' (signer_id || payload). This is NOT cryptographic
-signing — it is a placeholder so the ABI shapes compile and test paths
-work. Cryptographic fidelity is not required for Phase 3's correctness
-experiment; it IS required before any production consideration.
+Ed25519 detached signature. Matches Idris2 ABI
+`Signature { keyId, sigBytes }`. In this implementation `key_id` holds
+the signer's Ed25519 **public key** (32 bytes); pubkeys are both
+compact and self-identifying, so no separate key_id registry is
+needed.
+
+- `key_id`   : 32 bytes (Ed25519 public key)
+- `sig_bytes`: 64 bytes (Ed25519 detached signature)
 """
 struct Signature
     key_id::Vector{UInt8}
@@ -108,18 +114,18 @@ end
 # Store
 # -----------------------------------------------------------------------
 
-"In-memory ephemeral Core store. Dict-backed, no persistence."
+"In-memory ephemeral Core store. Dict-backed, no persistence. Holds
+a fresh Ed25519 keypair for signing attestations and provenance entries."
 struct Store
     octads::Dict{OctadId, CoreOctad}
-    # For placeholder signing — real impl would hold an Ed25519 keypair
-    signing_key_id::Vector{UInt8}
+    keypair::Any                     # Main.Crypto.Ed25519KeyPair (duck-typed to avoid load order)
     # Attestation freshness window, in nanoseconds (default: 60s)
     freshness_window_ns::Int64
 end
 
 Store(; freshness_window_ns::Int64 = Int64(60_000_000_000)) = Store(
     Dict{OctadId, CoreOctad}(),
-    collect(codeunits("verisim-core-test-key")),
+    Main.Crypto.generate_keypair(),
     freshness_window_ns,
 )
 
@@ -196,8 +202,8 @@ function enrich!(store::Store,
     )
     this_hash = sha256(to_hash)
 
-    # Placeholder signature — see Signature docstring.
-    sig = placeholder_sign(store.signing_key_id, this_hash)
+    # Real Ed25519 signature over this_hash.
+    sig = ed25519_sign(store.keypair, this_hash)
 
     push!(octad.provenance.entries, ProvenanceEntry(
         prev, this_hash, actor, t, sig,
@@ -215,27 +221,25 @@ function bytes2hex_summary(blob::SemanticBlob)::Vector{UInt8}
 end
 
 """
-    placeholder_sign(key_id, payload) -> Signature
+    ed25519_sign(keypair, payload) -> Signature
 
-Placeholder for Ed25519 signing. Current impl: SHA-256 of
-(key_id || payload). NOT cryptographically sound. See Signature docstring.
+Produce an Ed25519 detached signature over `payload`. Returns a
+Signature whose `key_id` field carries the public key (32 bytes) and
+`sig_bytes` carries the 64-byte signature.
 """
-function placeholder_sign(key_id::Vector{UInt8},
-                          payload::Vector{UInt8})::Signature
-    sig = sha256(vcat(key_id, payload))
-    Signature(key_id, sig)
+function ed25519_sign(keypair, payload::Vector{UInt8})::Signature
+    sig_bytes = Main.Crypto.sign_detached(keypair, payload)
+    Signature(copy(keypair.pk), sig_bytes)
 end
 
 """
-    placeholder_verify(sig, payload) -> Bool
+    ed25519_verify(sig, payload) -> Bool
 
-Placeholder verification matching placeholder_sign. Recomputes the
-expected SHA-256 and compares. This provides the ABI shape; real
-Ed25519 verification is a Phase 4+ task.
+Verify an Ed25519 signature. Uses `sig.key_id` as the public key.
+Returns true iff the signature is valid for the given payload.
 """
-function placeholder_verify(sig::Signature, payload::Vector{UInt8})::Bool
-    expected = sha256(vcat(sig.key_id, payload))
-    expected == sig.sig_bytes
+function ed25519_verify(sig::Signature, payload::Vector{UInt8})::Bool
+    Main.Crypto.verify_detached(sig.key_id, sig.sig_bytes, payload)
 end
 
 # -----------------------------------------------------------------------
@@ -256,7 +260,7 @@ function attest(store::Store, id::OctadId)
     # Sign a digest of (id || t || semantic summary).
     sem_summary = octad.semantic === nothing ? UInt8[] : bytes2hex_summary(octad.semantic)
     payload = vcat(octad.id.bytes, reinterpret(UInt8, [t.epoch_nanos]), sem_summary)
-    sig = placeholder_sign(store.signing_key_id, payload)
+    sig = ed25519_sign(store.keypair, payload)
     (octad, sig, t)
 end
 
@@ -280,7 +284,7 @@ function verify_attest(store::Store,
     # Recompute expected payload and verify.
     sem_summary = octad.semantic === nothing ? UInt8[] : bytes2hex_summary(octad.semantic)
     payload = vcat(octad.id.bytes, reinterpret(UInt8, [t.epoch_nanos]), sem_summary)
-    placeholder_verify(sig, payload)
+    ed25519_verify(sig, payload)
 end
 
 end # module

verisim-modular-experiment/impl/drift/Metrics.jl

@@ -14,7 +14,7 @@ module Metrics
 
 using SHA
 
-export cosine_distance, hash_embedding, d_SV, drift
+export cosine_distance, hash_embedding, d_SV, d_VD, d_SD, drift
 
 # -----------------------------------------------------------------------
 # Primitive drift functions
@@ -97,6 +97,49 @@ function d_SV(type_uris::Vector{String},
     cosine_distance(ref, vector_embedding)
 end
 
+# -----------------------------------------------------------------------
+# Pairwise drift — Vector × Document (d_VD, TeX §4.3)
+# -----------------------------------------------------------------------
+
+"""
+    d_VD(vector_embedding, document_bytes) -> Float64
+
+Vector-Document drift (TeX §4.3, d_{V,D}): cosine distance between
+stored embedding and the embedding that *would* be computed from the
+current document content. A drift value near 0 indicates the embedding
+is fresh; near 1 indicates the document has changed since the
+embedding was computed.
+"""
+function d_VD(vector_embedding::Vector{Float32},
+              document_bytes::Vector{UInt8})::Float64
+    ref = hash_embedding(document_bytes, length(vector_embedding))
+    cosine_distance(ref, vector_embedding)
+end
+
+# -----------------------------------------------------------------------
+# Pairwise drift — Semantic × Document (d_SD)
+# -----------------------------------------------------------------------
+
+"""
+    d_SD(semantic_type_uris, semantic_proof, document_bytes) -> Float64
+
+Semantic-Document drift. Research-prototype definition: cosine distance
+between hash-derived embeddings of the Semantic blob and the Document
+bytes. Plays the role TeX §4.3 leaves implicit for this pair.
+"""
+function d_SD(type_uris::Vector{String},
+              proof_bytes::Vector{UInt8},
+              document_bytes::Vector{UInt8})::Float64
+    semantic_bytes = vcat(
+        collect(codeunits(join(type_uris, ","))),
+        proof_bytes,
+    )
+    dim = 384
+    s_ref = hash_embedding(semantic_bytes, dim)
+    d_ref = hash_embedding(document_bytes, dim)
+    cosine_distance(s_ref, d_ref)
+end
+
 # -----------------------------------------------------------------------
 # Drift dispatcher — absent-pair convention
 # -----------------------------------------------------------------------
@@ -117,20 +160,26 @@ function drift(shape1::Symbol, val1,
     # Absent-pair convention: d(⊥, ·) = d(·, ⊥) = 0.
     (val1 === nothing || val2 === nothing) && return 0.0
 
-    # Normalise pair order so (A,B) and (B,A) dispatch the same way.
-    if (shape1, shape2) == (:vector, :semantic)
-        shape1, shape2 = :semantic, :vector
-        val1, val2 = val2, val1
+    # Normalise pair order — canonicalise so (A,B) and (B,A) dispatch the
+    # same way. Priority order: :semantic < :vector < :document.
+    canonical_order = Dict(:semantic => 1, :vector => 2, :document => 3)
+    if haskey(canonical_order, shape1) && haskey(canonical_order, shape2)
+        if canonical_order[shape1] > canonical_order[shape2]
+            shape1, shape2 = shape2, shape1
+            val1, val2 = val2, val1
+        end
     end
 
     if shape1 == :semantic && shape2 == :vector
-        # val1 is a SemanticBlob-like (has .type_uris, .proof_bytes fields
-        # via duck-typing); val2 is a Vector{Float32}.
         return d_SV(val1.type_uris, val1.proof_bytes, val2)
+    elseif shape1 == :vector && shape2 == :document
+        return d_VD(val1, val2)
+    elseif shape1 == :semantic && shape2 == :document
+        return d_SD(val1.type_uris, val1.proof_bytes, val2)
     end
 
-    error("drift: pair ($shape1, $shape2) not implemented in Phase 3 " *
-          "(only :semantic × :vector is wired). Add it to drift/Metrics.jl.")
+    error("drift: pair ($shape1, $shape2) not implemented. " *
+          "Wired pairs: (S,V), (V,D), (S,D). Add to drift/Metrics.jl.")
 end
 
 end # module