Skip to content

Commit f7fc0e4

Browse files
hyperpolymathclaude
andcommitted
feat(verisim-modular-experiment): Phase 3 runtime validation of Path B
Phase 3 decision gate PASSED. 70/70 assertions green across 3 suites. Federated aggregate-drift numerically equals monolithic aggregate-drift for the same octad data over a {Semantic,Vector} federation. Path B is runtime-confirmed: a non-trivial VerisimCore exists. Julia reference impl (impl/): - VerisimCore.jl — Store, enrich!, attest, verify_attest, inv:persist - FederationManager.jl — DriftWeights, renormalise, aggregate_drift, PeerAttestation, runtime IsFederable validation (Core shapes rejected) - drift/Metrics.jl — cosine_distance, hash_embedding, d_SV, dispatcher - peers/VectorPeer.jl — DriftProjector + CoherenceProjector + LWWAcceptor - Crypto.jl — Ed25519 wrapper over libsodium (wiring in progress) Test suites (test/): - test_verisim_core.jl (25 assertions): enrichment atomicity, Identity Persistence, hash-chain integrity, attestation round-trip, freshness - test_federation_parity.jl (24 assertions): parity vs monolithic, multi-octad parity, reduced-scope drift, Clause 1/5 behaviours - test_seams.jl (21 assertions): register_peer! rejects Core shapes, PeerAttestation struct matches Idris2 record, classification constants Seam audit (docs/SEAMS.adoc): ABI↔impl alignment post-Phase 3. Fixed: PeerAttestation struct, is_fresh signature, runtime Core rejection. Documented: driftAgainst transport abstraction, enrich payload, naming. Documentation (human + machine): - EXPLAINME.adoc — plain-language repo overview - docs/SHAPES.adoc — central mapping (TeX letters ↔ Idris2 ↔ Julia) - docs/PHASE-3-IMPLEMENTATION-PLAN.adoc — scope + defaults rationale - .machine_readable/6a2/{STATE,META,ECOSYSTEM}.a2ml — structured metadata - LICENSE pointer, PLAN.adoc updated with Phase 3 outcome - PROOF-NEEDS.md updated with discharged obligations - src/Abi/FederationContract.idr — driftAgainst transport docstring Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 4c74d07 commit f7fc0e4

22 files changed

Lines changed: 2335 additions & 11 deletions
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
build/
22
*.ttc
33
*.ttm
4+
Manifest.toml
Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
;; SPDX-License-Identifier: PMPL-1.0-or-later
2+
(ecosystem
3+
(version "1.0.0")
4+
(last-updated "2026-04-05")
5+
6+
(name "verisim-modular-experiment")
7+
(type "research-experiment")
8+
(purpose "Test whether a non-trivial VerisimCore (identity-core subset of the octad)
9+
exists such that VCL consonance claims compose soundly over federations
10+
that omit non-core shapes entirely at store level.")
11+
12+
(position-in-ecosystem
13+
(parent "nextgen-databases"
14+
(relationship "sub-project")
15+
(description "Lives within the nextgen-databases monorepo; no own .git."))
16+
(siblings
17+
(sibling "verisimdb"
18+
(relationship "parent-architecture")
19+
(description "Canonical paved-road octad. Experiment is read-only w.r.t. its sources.
20+
Foldback items (doc drift, soundness remarks) track in docs/FOLDBACK.adoc."))
21+
(sibling "typeql-experimental"
22+
(relationship "sibling-experiment")
23+
(description "Experimental sister project exploring VCL type-theoretic extensions.
24+
Same experiment-repo pattern (deno.json / ipkg / machine_readable).")))
25+
(description "Opens an architectural question neither verisimdb nor typeql-experimental
26+
asks: the presence axis for modality shapes. Independent falsifier."))
27+
28+
(related-projects
29+
(project "verisimdb"
30+
(relationship "reference")
31+
(description "Authoritative formal data model (arcvix-octad-data-model.tex)
32+
and 8-shape octad implementation in rust-core/.")
33+
(artefacts-used "arcvix-octad-data-model.tex"
34+
"rust-core/verisim-octad/src/query_octad.rs"
35+
"docs/federation-readiness.adoc"
36+
"docs/deployment-modes.adoc"
37+
"CLAUDE.md (octad modality list)"))
38+
39+
(project "krladapter-jl"
40+
(relationship "intended-phase-4-dogfood")
41+
(description "Julia package earmarked as first dogfood client for VerisimCore.
42+
Current upstream keeps a VeriSim interface slot open (per vcl-rename
43+
memory). Phase 4 wires KRLAdapter.jl against VerisimCore + federation.")
44+
(artefacts-used "(planned: KRLAdapter.jl VeriSim interface slot)"))
45+
46+
(project "idris2-ecosystem"
47+
(relationship "abi-toolchain")
48+
(description "Idris2 v0.8.0 used for ABI specification per hyperpolymath standard.")
49+
(artefacts-used "idris2 compiler")))
50+
51+
(standards-followed
52+
(standard "hyperpolymath-abi-ffi-standard"
53+
(description "Idris2 ABI + (intended) Zig FFI per ~/Documents/hyperpolymath-repos/rsr-template-repo")
54+
(conformance "partial — Idris2 ABI done, Zig FFI deferred past Phase 4"))
55+
(standard "a2ml-machine-readable"
56+
(description "This .machine_readable/6a2/*.a2ml directory")
57+
(conformance "complete — STATE, META, ECOSYSTEM all present"))
58+
(standard "pmpl-1.0-license"
59+
(description "All original code uses SPDX-License-Identifier: PMPL-1.0-or-later")
60+
(conformance "complete — all files headered")))
61+
62+
(deliverables
63+
(deliverable "idris2-abi"
64+
(description "3-module typechecked ABI: Types, VerisimCore, FederationContract")
65+
(status "complete"))
66+
(deliverable "julia-reference-impl"
67+
(description "Core + Vector peer + federation manager; 70 test assertions green")
68+
(status "complete"))
69+
(deliverable "path-b-validation"
70+
(description "Runtime-confirmed: Core={S,T,R} admits sound federation with
71+
one Federable peer (Vector) on the parity test")
72+
(status "complete"))
73+
(deliverable "full-nondivisibility-decision"
74+
(description "Multi-peer N≥2 non-interference + formal proof + VCL surface")
75+
(status "pending (Phase 3 follow-ups + Phase 4)"))))
Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
;; SPDX-License-Identifier: PMPL-1.0-or-later
2+
(meta
3+
(version "1.0.0")
4+
(last-updated "2026-04-05")
5+
6+
(architecture-decisions
7+
(decision "shape-absence-as-novel-axis"
8+
(status accepted)
9+
(date "2026-04-05")
10+
(context "Existing verisimdb federation architecture treats all 8 shapes as
11+
present-but-located-variably. User raised question: what if shapes
12+
can be entirely absent (not just remote)?")
13+
(decision "Open 'presence axis' as orthogonal to existing 'location axis'.
14+
Store-level absence is the novel axis this experiment explores.")
15+
(rationale "Existing axis: where does each shape live (standalone/federated/hybrid).
16+
New axis: which shapes exist at all. Per-octad absence already handled
17+
(def:octad allows φ(m)=⊥). Store-level absence is new."))
18+
19+
(decision "core-identity-set"
20+
(status accepted)
21+
(date "2026-04-05")
22+
(context "Phase 1 closure test per shape against formal data model.")
23+
(decision "Core={Semantic, Temporal, Provenance}. Federable={Vector, Tensor,
24+
Document, Spatial}. Conditional={Graph}.")
25+
(rationale "Semantic=VCL proof substrate. Temporal=inv:persist+def:enrichment+
26+
LWW-total-order+attestation-freshness. Provenance=def:enrichment+
27+
federation-trust-substrate. Others admit absence via d(⊥,·)=0.
28+
Graph required iff cross-entity consonance claims in scope."))
29+
30+
(decision "idris2-abi-plus-julia-impl"
31+
(status accepted)
32+
(date "2026-04-05")
33+
(context "Hyperpolymath standard: Idris2 ABI + Zig FFI. Phase 3 needs a
34+
runnable reference implementation.")
35+
(decision "Keep Idris2 ABI per standard. Write Phase 3 prototype in Julia
36+
(not Zig). Zig FFI port deferred to Phase 5+ if Path B validates.")
37+
(rationale "Julia aligns with Phase 4 dogfood client (KRLAdapter.jl).
38+
Research prototype pays for iteration speed over runtime speed.
39+
ABI remains canonical; Julia is one valid implementation."))
40+
41+
(decision "single-shape-phase-3-scope"
42+
(status accepted)
43+
(date "2026-04-05")
44+
(context "Phase 3 scope: reference impl + parity test. Choice of which
45+
Federable shape to federate first.")
46+
(decision "Vector first (per Phase 3 plan). Vector-Document drift is first
47+
pairwise metric in TeX §4.3; HNSW has clean algebraic drift.")
48+
(rationale "PLAN.adoc originally named Temporal — corrected (Temporal is Core,
49+
cannot be federated). Vector is natural first Federable peer."))
50+
51+
(decision "federated-parity-as-decision-gate"
52+
(status accepted)
53+
(date "2026-04-05")
54+
(context "Phase 3 decision gate needs a concrete falsifier.")
55+
(decision "Decision gate = aggregate_drift over {Core + peers} numerically
56+
equals aggregate_drift over monolithic store with same data.
57+
If parity fails, revisit Phase 1 classification.")
58+
(rationale "Parity at drift level is stronger than VCL-surface-level parity
59+
— if drift computation is identical, any VCL claim evaluating
60+
via drift is preserved.")
61+
(outcome "PASSED — 24/24 parity assertions green.")))
62+
63+
(development-practices
64+
(practice "tex-grounded"
65+
(description "Every classification verdict traceable to a TeX definition or
66+
theorem in verisimdb/arcvix-octad-data-model.tex.")
67+
(enforcement "docs/CORE-CANDIDATES.adoc cites each def/inv/thm."))
68+
(practice "seam-audit-every-phase"
69+
(description "After each phase, audit ABI↔impl seams and document in SEAMS.adoc.")
70+
(enforcement "docs/SEAMS.adoc updated 2026-04-05 after Phase 3."))
71+
(practice "typecheck-before-commit"
72+
(description "idris2 --build must pass. Julia test suites must pass.")
73+
(enforcement "Pre-commit verification noted in session log.")))
74+
75+
(design-rationale
76+
(why-not-subset-of-verisimdb "verisimdb/ is the paved-road canonical octad.
77+
Fragmenting its code is not the goal; opening the presence axis is. Experiment
78+
stays read-only w.r.t. main verisimdb sources.")
79+
(why-not-zig-phase-3 "Zig FFI is the hyperpolymath production standard but
80+
carries a porting cost premature for a falsifier experiment. Julia is sufficient
81+
to test the central hypothesis.")
82+
(why-path-b-over-path-a "Path A (formalise existing federation) is high-probability
83+
low-payoff. Path B (shape-absence) is lower-probability higher-payoff. Path B
84+
turned out to be live — non-trivial Core exists.")))
Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
;; SPDX-License-Identifier: PMPL-1.0-or-later
2+
(state
3+
(metadata
4+
(version "0.1.0")
5+
(last-updated "2026-04-05")
6+
(status active))
7+
8+
(project-context
9+
(name "verisim-modular-experiment")
10+
(purpose "Research experiment: can any octad shape be entirely absent (store-level)
11+
without making VCL consonance claims unsound?")
12+
(type "research-prototype")
13+
(completion-percentage 55))
14+
15+
(current-position
16+
(phase "phase-3-complete-seams-sorted")
17+
(summary "Phase 0-3 complete. Core={Semantic,Temporal,Provenance}, Federable={V,T,D,X},
18+
Graph conditional. Idris2 ABI typechecks in v0.8.0. Julia reference impl
19+
runs 70/70 assertions green across three suites. Federated aggregate-drift
20+
numerically equals monolithic aggregate-drift for same data. Path B
21+
runtime-confirmed. Seam audit completed and fixes applied."))
22+
23+
(phases
24+
(phase "phase-0-octad-archaeology"
25+
(status complete)
26+
(artefact "docs/OCTAD-SHAPES.adoc"))
27+
(phase "phase-1-core-identification"
28+
(status complete)
29+
(decision-gate "passed")
30+
(result "Core={S,T,R} Federable={V,T,D,X} Conditional={G}")
31+
(artefact "docs/CORE-CANDIDATES.adoc"))
32+
(phase "phase-2-federation-contract"
33+
(status complete)
34+
(artefact "src/Abi/FederationContract.idr" "spec/federation-contract.adoc")
35+
(verified "idris2 --build"))
36+
(phase "phase-3-reference-impl"
37+
(status complete)
38+
(decision-gate "passed")
39+
(result "70/70 assertions green, federated=monolithic parity confirmed")
40+
(language "julia")
41+
(federated-shape "vector")
42+
(deferred "ed25519" "multi-peer-noninterference" "vcl-parser"))
43+
(phase "phase-4-krladapter-dogfood"
44+
(status pending))
45+
(phase "phase-5-findings-writeup"
46+
(status pending)))
47+
48+
(components
49+
(component "idris2-abi"
50+
(status complete)
51+
(description "3 modules: Types, VerisimCore, FederationContract. Typechecks clean.")
52+
(completion 100))
53+
(component "julia-core"
54+
(status complete)
55+
(description "VerisimCore.jl: enrich!, attest, verify_attest, Identity Persistence.")
56+
(completion 100))
57+
(component "julia-federation"
58+
(status complete)
59+
(description "FederationManager.jl: renormalise, aggregate_drift, PeerAttestation.")
60+
(completion 100))
61+
(component "julia-vector-peer"
62+
(status complete)
63+
(description "First Federable peer: DriftProjector, CoherenceProjector, LWWAcceptor.")
64+
(completion 100))
65+
(component "julia-crypto-ed25519"
66+
(status in-progress)
67+
(description "Replacing placeholder SHA-256 with real Ed25519 via libsodium.")
68+
(completion 50))
69+
(component "documentation"
70+
(status complete)
71+
(description "README, PLAN, PROOF-NEEDS, DESIGN, OCTAD-SHAPES, CORE-CANDIDATES,
72+
FOLDBACK, SEAMS, PHASE-3-IMPL-PLAN, federation-contract spec, AI manifest.")
73+
(completion 90)))
74+
75+
(verified-results
76+
(result "idris2-typecheck"
77+
(command "idris2 --build verisim-modular-experiment.ipkg")
78+
(status pass))
79+
(result "verisim-core-tests"
80+
(command "julia --project=. test/test_verisim_core.jl")
81+
(status pass)
82+
(assertions 25))
83+
(result "federation-parity-tests"
84+
(command "julia --project=. test/test_federation_parity.jl")
85+
(status pass)
86+
(assertions 24))
87+
(result "seam-tests"
88+
(command "julia --project=. test/test_seams.jl")
89+
(status pass)
90+
(assertions 21)))
91+
92+
(foldback-to-main-verisimdb
93+
(applied
94+
(item "docs/deployment-modes.adoc: 6→8 modalities")
95+
(item "docs/federation-readiness.adoc: 6→8 modalities + normalizer strategies")
96+
(item "arcvix-octad-data-model.tex: rem:agg-drift-renorm added to §4.2"))
97+
(pending
98+
(item "Normalizer regeneration stub-status doc update (documented in FOLDBACK.adoc)")))
99+
100+
(critical-next-actions
101+
(action "Finish Ed25519 wiring (impl/Crypto.jl written, needs VerisimCore/VectorPeer update)")
102+
(action "Add second Federable peer (Document) for multi-peer non-interference test")
103+
(action "Write minimal VCL parser/evaluator exercising FROM FEDERATION syntax")
104+
(action "Update this STATE.a2ml after each"))
105+
106+
(session-history
107+
(session "2026-04-05"
108+
(focus "Full experiment scaffold → Phase 3 runtime validation")
109+
(phases-closed "0" "1" "2" "3")
110+
(highlight "Path B confirmed: non-trivial Core exists"))))

0 commit comments

Comments
 (0)