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-11 — Tropical matrix + KRL integration (Phase 3+4+5)
4+ # Updated: 2026-04-11 — bellman_ford sorry CLOSED; all Isabelle sorries gone
55
66[metadata]
77project = "nextgen-databases"
@@ -11,25 +11,24 @@ status = "active"
1111
1212[project-context]
1313name = "nextgen-databases"
14- completion-percentage = 45
14+ completion-percentage = 50
1515phase = "Phase 5 — Tropical Consonance + KRL Integration"
1616
1717[current-position]
18- milestone = "verisim-modular-experiment tropical bridge v0.2"
18+ milestone = "verisim-modular-experiment tropical bridge v0.2 + bellman_ford proved "
1919last-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 "
20+ last-action = "Closed bellman_ford OFFICIAL SORRY 2 — full min-plus Bellman-Ford proof in Tropical_Matrices_Full.thy. All Isabelle sorries gone (0 remaining). "
2121
2222[tropical-bridge]
2323status = "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 )"
24+ isabelle-sorry-tropical-matrices = "NONE — all closed (bellman_ford CLOSED 2026-04-11 )"
2525isabelle-sorry-other = "cycle_shortcutting CLOSED; floyd_warshall CLOSED; tropm_mat_pow_eq_sum_walks CLOSED"
2626julia-mirror = "TropicalMatrix.jl + TangleGraph.jl (verisim-modular-experiment/impl/tropical/)"
2727vcl-clauses = "ProofIntegrity, ProofConsistency, ProofFreshness, ProofConsonance — all live"
2828
2929[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"
30+ 1 = "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause"
31+ 2 = "Wire _riii_neighbors when KnotTheory.jl gains live r3_simplify"
3332
3433[test-coverage]
3534unit-tests = "~40 (Elixir consensus + federation adapters)"
@@ -55,14 +54,12 @@ gleam-smoke = "Written; requires compiled lith_nif.so to run connection/lifecycl
5554- "modality_benchmarks.rs uses old API — does not compile (pre-existing)"
5655
5756[route-to-mvp]
58- next = "Close bellman_ford sorry (Tropical_Matrices_Full.thy) — upgrades ProofConsonance to machine-checked"
59- then = "Add Tropical_Determinants.thy + ProofOptimalAssignment"
57+ next = "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause"
6058then = "Fix VQLTypeChecker binary_to_existing_atom crash (P1 hardening)"
6159then = "Fix null-byte entity ID sanitisation in VQL parser"
6260then = "Update integration_test.rs to current API"
6361
6462[critical-next-actions]
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)"
63+ 1 = "Tropical_Determinants.thy new file — permanent = optimal assignment"
64+ 2 = "Fix VQLTypeChecker to use String.to_existing_atom with rescue guard (P1)"
65+ 3 = "Add null-byte sanitisation in VQLBridge built-in parser (P1)"
0 commit comments