Skip to content

Commit 3b75ecf

Browse files
hyperpolymathclaude
andcommitted
feat(tropical-bridge): wire KnotTheory.jl RII into TangleGraph v0.2
- `_rii_neighbors` now calls `Main.KnotTheory.r2_simplify` via `from_dt` → `r2_simplify` → `to_dowker` pipeline; wrapped in try/catch for arc-renumbering gaps (known KnotTheory.jl v1.0.1 limit) - `_riii_neighbors` documented as intentional no-op: `r3_simplify` is topology-preserving and returns the diagram unchanged in v1.0.1 - KnotTheory + AcceleratorGate added to Project.toml as dev deps - `import KnotTheory` added to krladapter_integration.jl example; Case 5 pipeline verification added to demo_consonance() - TROPICAL-BRIDGE.adoc gap table updated: RI+RII live, RIII pending - STATE.a2ml updated for session; Intentfile/Mustfile corrected (were Burble copy-paste; now correct nextgen-databases content) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent fefeab0 commit 3b75ecf

11 files changed

Lines changed: 278 additions & 392 deletions

File tree

.machine_readable/6a2/STATE.a2ml

Lines changed: 26 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,35 @@
11
# SPDX-License-Identifier: PMPL-1.0-or-later
22
# STATE.a2ml — Project state checkpoint
33
# Converted from STATE.scm on 2026-03-15
4-
# Updated: 2026-04-04CRG C blitz
4+
# Updated: 2026-04-11Tropical matrix + KRL integration (Phase 3+4+5)
55

66
[metadata]
77
project = "nextgen-databases"
88
version = "0.1.0"
9-
last-updated = "2026-04-04"
9+
last-updated = "2026-04-11"
1010
status = "active"
1111

1212
[project-context]
1313
name = "nextgen-databases"
14-
completion-percentage = 35
15-
phase = "CRG CTesting & Benchmarking blitz"
14+
completion-percentage = 45
15+
phase = "Phase 5Tropical Consonance + KRL Integration"
1616

1717
[current-position]
18-
milestone = "CRG C test coverage"
19-
last-session = "2026-04-04"
20-
last-action = "Added E2E, P2P property, security, concurrency tests and throughput benchmarks"
18+
milestone = "verisim-modular-experiment tropical bridge v0.2"
19+
last-session = "2026-04-11"
20+
last-action = "Wired KnotTheory.jl RII (r2_simplify) into TangleGraph._rii_neighbors; ProofConsonance VCL clause live; TROPICAL-BRIDGE.adoc updated; contractiles corrected"
21+
22+
[tropical-bridge]
23+
status = "v0.2 — RI + RII live, RIII stub (KnotTheory.jl r3_simplify is no-op)"
24+
isabelle-sorry-tropical-matrices = "1 remaining (bellman_ford in Tropical_Matrices_Full.thy)"
25+
isabelle-sorry-other = "cycle_shortcutting CLOSED; floyd_warshall CLOSED; tropm_mat_pow_eq_sum_walks CLOSED"
26+
julia-mirror = "TropicalMatrix.jl + TangleGraph.jl (verisim-modular-experiment/impl/tropical/)"
27+
vcl-clauses = "ProofIntegrity, ProofConsistency, ProofFreshness, ProofConsonance — all live"
28+
29+
[pending-tropical]
30+
1 = "Close bellman_ford sorry in Tropical_Matrices_Full.thy (min-plus version)"
31+
2 = "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause"
32+
3 = "Wire _riii_neighbors when KnotTheory.jl gains live r3_simplify"
2133

2234
[test-coverage]
2335
unit-tests = "~40 (Elixir consensus + federation adapters)"
@@ -43,14 +55,14 @@ gleam-smoke = "Written; requires compiled lith_nif.so to run connection/lifecycl
4355
- "modality_benchmarks.rs uses old API — does not compile (pre-existing)"
4456

4557
[route-to-mvp]
46-
next = "Fix VQLTypeChecker binary_to_existing_atom crash (P1 hardening)"
58+
next = "Close bellman_ford sorry (Tropical_Matrices_Full.thy) — upgrades ProofConsonance to machine-checked"
59+
then = "Add Tropical_Determinants.thy + ProofOptimalAssignment"
60+
then = "Fix VQLTypeChecker binary_to_existing_atom crash (P1 hardening)"
4761
then = "Fix null-byte entity ID sanitisation in VQL parser"
4862
then = "Update integration_test.rs to current API"
49-
then = "Add real fuzz harness (replace placeholder.txt)"
50-
then = "Complete remaining E2E scenarios (federation, node failure/recovery)"
5163

5264
[critical-next-actions]
53-
1 = "Run full mix test suite to confirm 6-failure baseline is stable"
54-
2 = "Fix VQLTypeChecker to use String.to_existing_atom with rescue guard (P1)"
55-
3 = "Add null-byte sanitisation in VQLBridge built-in parser (P1)"
56-
4 = "Update integration_test.rs to use ConcreteOctadStore from verisim-api"
65+
1 = "Close bellman_ford OFFICIAL SORRY 2 (min-plus Bellman-Ford optimality)"
66+
2 = "Tropical_Determinants.thy new file — permanent = optimal assignment"
67+
3 = "Fix VQLTypeChecker to use String.to_existing_atom with rescue guard (P1)"
68+
4 = "Add null-byte sanitisation in VQLBridge built-in parser (P1)"

.machine_readable/contractiles/intend/Intentfile.a2ml

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,32 @@
33
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
44

55
@abstract:
6-
Declared intent and purpose for Burble.
6+
Declared intent and purpose for nextgen-databases.
77
@end
88

99
## Purpose
1010

11-
Burble — // SPDX-License-Identifier: PMPL-1.0-or-later
11+
Nextgen Databases is a monorepo containing VeriSimDB (identity-persistent
12+
octad store with VCL proof clauses and tropical matrix consonance checking),
13+
QuandleDB (quandle-based knot invariant store), and Lithoglyph (graph-based
14+
storage). It is the primary dogfood target for KRLAdapter.jl and the
15+
verisim-modular-experiment proof-of-concept.
16+
17+
Tropical proof work (Isabelle/HOL ↔ Julia mirror) lives in
18+
`tropical-resource-typing/` and is bridged to the VCL layer via
19+
`verisim-modular-experiment/impl/tropical/`.
1220

1321
## Anti-Purpose
1422

1523
This project is NOT:
16-
- A fork or wrapper around another tool
17-
- A monorepo (unless explicitly structured as one)
24+
- A standalone database engine (sits above storage primitives)
25+
- A replacement for existing relational or document databases
26+
- A general-purpose time-series or event-sourcing store
27+
- A programming language implementation
1828

1929
## If In Doubt
2030

2131
If you are unsure whether a change is in scope, ask.
22-
Sensitive areas: ABI definitions, license headers, CI workflows.
32+
Sensitive areas: VCL proof semantics, Isabelle/Julia tropical bridge,
33+
KnotTheory.jl integration boundary (KRLAdapter.jl / TangleGraph.jl only —
34+
never modify KnotTheory.jl directly).
Lines changed: 21 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,14 @@
11
# SPDX-License-Identifier: PMPL-1.0-or-later
2-
# Mustfile — Physical state contract for Burble
2+
# Mustfile — Physical state contract for nextgen-databases
33
# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
44
#
55
# What MUST be true about this repository. Hard requirements.
66
# Run with: must check
77
# Fix with: must fix (where deterministic fix exists)
88

99
@abstract:
10-
Physical state invariants for the Burble voice platform.
10+
Physical state invariants for the nextgen-databases monorepo (VeriSimDB,
11+
QuandleDB, Lithoglyph).
1112
These are hard requirements — CI and pre-commit hooks fail if any check fails.
1213
@end
1314

@@ -35,59 +36,19 @@ These are hard requirements — CI and pre-commit hooks fail if any check fails.
3536

3637
### contributing
3738
- description: CONTRIBUTING guide must exist
38-
- run: test -f CONTRIBUTING.adoc || test -f .github/CONTRIBUTING.md
39+
- run: test -f CONTRIBUTING.md || test -f CONTRIBUTING.adoc
3940
- severity: warning
4041

4142
### editorconfig
4243
- description: .editorconfig must exist
4344
- run: test -f .editorconfig
4445
- severity: warning
4546

46-
## Elixir Server
47-
48-
### mix-exs-present
49-
- description: Elixir mix.exs must exist in server/
50-
- run: test -f server/mix.exs
51-
- severity: critical
52-
53-
### elixir-compiles
54-
- description: Elixir server compiles without errors
55-
- run: test -f server/mix.exs
56-
- severity: critical
57-
- notes: Full compile check via CI (mix compile), file presence check here
58-
59-
### ecto-migrations-exist
60-
- description: Database migrations directory exists
61-
- run: test -d server/priv/repo/migrations
62-
- severity: critical
63-
64-
### config-files-present
65-
- description: All config files exist
66-
- run: test -f server/config/config.exs && test -f server/config/dev.exs && test -f server/config/prod.exs && test -f server/config/runtime.exs
67-
- severity: critical
68-
69-
## Web Client
70-
71-
### rescript-json-present
72-
- description: ReScript config exists for web client
73-
- run: test -f client/web/rescript.json
74-
- severity: warning
75-
76-
### web-entry-point
77-
- description: Web client entry point exists
78-
- run: test -f server/priv/static/index.html || test -f client/web/index.html
79-
- severity: warning
80-
8147
## SPDX Compliance
8248

83-
### spdx-elixir
84-
- description: All Elixir files have SPDX header
85-
- run: test -z "$(find server/lib -name '*.ex' -exec head -1 {} \; 2>/dev/null | grep -cv 'SPDX' | grep -v '^0$')"
86-
- severity: warning
87-
8849
### no-agpl
8950
- description: No AGPL-3.0 references (replaced by PMPL)
90-
- run: test -z "$(grep -rl 'AGPL-3.0' LICENSE .editorconfig .gitattributes 2>/dev/null)"
51+
- run: test -z "$(grep -rl 'AGPL-3.0' LICENSE 2>/dev/null)"
9152
- severity: critical
9253

9354
## Dangerous Patterns
@@ -128,17 +89,24 @@ These are hard requirements — CI and pre-commit hooks fail if any check fails.
12889

12990
## Security
13091

131-
### no-secrets-in-config
132-
- description: No hardcoded secrets in Elixir config
133-
- run: test -z "$(grep -rE '(secret_key_base|password).*=\"[A-Za-z0-9+/]{32,}\"' server/config/ 2>/dev/null | grep -v 'dev_only\|test_only')"
134-
- severity: critical
135-
136-
### beam-cookie-absent
137-
- description: No Erlang cookie in repository
138-
- run: test -z "$(find . -name '.erlang.cookie' 2>/dev/null)"
92+
### no-hardcoded-paths
93+
- description: No hardcoded developer paths in source files
94+
- run: "! grep -rn '/home/hyper\|/mnt/eclipse' --include='*.rs' --include='*.res' --include='*.ex' --include='*.gleam' --include='*.zig' --include='*.sh' . 2>/dev/null | grep -v '.git/' | head -1"
13995
- severity: critical
14096

14197
### env-files-absent
14298
- description: No .env files committed
143-
- run: test ! -f .env && test ! -f server/.env && test ! -f .env.local && test ! -f .env.production
99+
- run: test ! -f .env && test ! -f .env.local && test ! -f .env.production
100+
- severity: critical
101+
102+
## VeriSimDB / KRL Integration
103+
104+
### state-in-machine-readable
105+
- description: STATE files only in .machine_readable/ (never root)
106+
- run: test ! -f STATE.scm && test ! -f STATE.a2ml
107+
- severity: critical
108+
109+
### no-knottheory-modifications
110+
- description: KnotTheory.jl is READ-ONLY — never modify its source
111+
- notes: KRLAdapter integration goes in TangleGraph.jl only; KnotTheory.jl is a community library
144112
- severity: critical

contractiles/intend/Intentfile.a2ml

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,20 @@ Declared intent and purpose for Nextgen Databases.
88

99
## Purpose
1010

11-
Nextgen Databases — // SPDX-License-Identifier: PMPL-1.0-or-later
11+
Nextgen Databases is a monorepo containing VeriSimDB (identity-persistent
12+
octad store with VCL proof clauses), QuandleDB (quandle-based knot
13+
invariant store), and Lithoglyph (graph-based storage). It is the
14+
primary dogfood target for KRLAdapter.jl and the verisim-modular-experiment.
1215

1316
## Anti-Purpose
1417

1518
This project is NOT:
16-
- A fork or wrapper around another tool
17-
- A monorepo (unless explicitly structured as one)
19+
- A standalone database engine (sits above storage primitives)
20+
- A replacement for existing relational or document databases
21+
- A general-purpose time-series or event-sourcing store
1822

1923
## If In Doubt
2024

2125
If you are unsure whether a change is in scope, ask.
22-
Sensitive areas: ABI definitions, license headers, CI workflows.
26+
Sensitive areas: VCL proof semantics, Isabelle/Julia tropical bridge,
27+
KnotTheory.jl integration boundary (KRLAdapter only — never modify KnotTheory directly).
Lines changed: 18 additions & 71 deletions
Original file line numberDiff line numberDiff line change
@@ -1,75 +1,22 @@
1-
;; SPDX-License-Identifier: PMPL-1.0-or-later
2-
(ecosystem
3-
(version "1.0.0")
4-
(last-updated "2026-04-05")
1+
# SPDX-License-Identifier: PMPL-1.0-or-later
2+
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
#
4+
# ECOSYSTEM.a2ml — Verisim Modular Experiment ecosystem position
5+
[metadata]
6+
version = "1.0.0"
7+
last-updated = "2026-04-05"
58

6-
(name "verisim-modular-experiment")
7-
(type "research-experiment")
8-
(purpose "Test whether a non-trivial VerisimCore (identity-core subset of the octad)
9+
[project]
10+
name = "Verisim Modular Experiment"
11+
purpose = "Test whether a non-trivial VerisimCore (identity-core subset of the octad)
912
exists such that VCL consonance claims compose soundly over federations
10-
that omit non-core shapes entirely at store level.")
13+
that omit non-core shapes entirely at store level."
14+
role = "research-experiment"
1115

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."))
16+
[position-in-ecosystem]
17+
category = ""
2718

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)"))))
19+
[related-projects]
20+
projects = [
21+
# No related projects recorded
22+
]

0 commit comments

Comments
 (0)