Skip to content

rust-spark-stance.adoc

Latest commit

 

History

History
122 lines (98 loc) · 4.84 KB

rust-spark-stance.adoc

File metadata and controls

122 lines (98 loc) · 4.84 KB
Raw

Rust/SPARK Stance — verisimdb

Summary

VeriSimDB is a safety-critical cross-modal entity engine ("octad model": each entity exists across 8 modalities). Its application logic is written in Rust (workspace crates under rust-core/ — verisim-octad, verisim-graph, verisim-planner, verisim-drift, verisim-nif, etc.). Per the estate language policy (standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc §Terminology), "Rust" means "Rust/SPARK": Rust is the primary implementation language now, but the project is designed to admit SPARK/Ada verification modules across a stable, Idris2-typed boundary, with Zig as the FFI layer. Rust here is never the ABI/API/FFI layer.

This document is the project’s compliance stance against that policy. Prior to this audit (2026-05-18) the seam (src/abi/.idr + ffi/zig/) was present but carried *no stance doc — a silent-regress risk flagged by the estate audit (status was "DESIGNED-ONLY"). This document records the seam honestly and brings the project to documented structural compliance.

What is correctness-critical here

VeriSimDB is a database/verisimilitude engine, not a ledger. The correctness-critical surface is the cross-modal entity store, its drift detection, and the C ABI that exposes it to consumers.

Critical surface Where

Result-code round-trip (no FFI status corruption)

src/abi/Types.idr — vresultToInt / vresultFromInt, DecEq VResult

Entity lifecycle / modality read-write safety

src/abi/Foreign.idr — entityCreate, entityGet, entityDelete, modalityWrite, modalityRead

C ABI struct layout fidelity

src/abi/Layout.idr — field offsets / sizes vs the Rust #[repr©] structs

Octad cross-modal consistency, drift thresholds

Rust workspace: rust-core/verisim-octad, verisim-drift, verisim-graph

The seam

File Role

src/abi/Types.idr

Idris2 boundary types — total models of VResult, EntityId, EntityHandle, modality masks. %default total. Constructor and integer-code order is ABI-significant and matches the Rust enums; vresultFromInt . vresultToInt is the round-trip obligation and DecEq VResult is discharged.

src/abi/Layout.idr

C-ABI struct layout — offsets/sizes that must match the Rust #[repr©] definitions consumed via libverisimdb.

src/abi/Foreign.idr

Zig/C-FFI boundary: every %foreign "C:verisimdb_*, libverisimdb" entry point, with safe Idris2 wrappers that decode raw Bits32 returns back into VResult (defaulting to VError on out-of-range, i.e. fail-closed).

All three modules carry %default total and contain zero proof escapes (no believe_me, assert_total, postulate, idris_crash). They are checkable in principle with idris2 --check src/abi/Types.idr etc. The Idris2 toolchain is not yet wired into CI; wiring it is the primary tracked follow-up.

debugger/src/abi/ carries a parallel copy of the same three modules for the debugger component; the same total/no-escape property holds there.

SPARK/Ada admission path

The boundary is the Idris2 seam above. A future SPARK/Ada re-implementation of any correctness-critical store/drift component sits on the far side of the Foreign C-ABI contract without changing it: it must honour the VResult code discipline and the Layout struct contract. No SPARK code exists yet; the seam exists so it can be added without redesign, which is exactly what §Terminology requires of a "designed to admit SPARK/Ada" Rust project.

Honest gaps

  • The Idris2 seam states the FFI shape contract (result-code round-trip, layout, total wrappers). It does not yet carry type-level statements of the deeper octad-consistency or drift-threshold invariants enforced (only) in the Rust workspace; those are owed, not proven.

  • ffi/zig/src/main.zig still contains unfilled {{PROJECT}} RSR template placeholders — the Zig implementation layer is scaffolding, not a finished faithful implementation of the Foreign.idr contract. This is a real gap on the FFI side, not merely a missing proof.

  • Idris2 is not in CI (.tool-versions carries no idris2 entry), so the seam’s totality is asserted, not gate-enforced.

  • The companion data repo verisimdb-data deliberately removed its template ABI Idris2 files (see its PROOF-NEEDS.md) to avoid a false formal-verification impression; that repo is data, not verified code, and makes no verification claims.

References

  • standards/rhodium-standard-repositories/spec/LANGUAGE-POLICY.adoc §Terminology, §"Rust is never the ABI"

  • Estate exemplar stance: proof-of-work/RUST-SPARK-STANCE.adoc

  • This repo’s seam: src/abi/{Types,Layout,Foreign}.idr

  • Tracking: hyperpolymath/standards#124