Experimental Surfaces

Experimental Surfaces

Two boundaries in this repository are pre-production: the Zig C-ABI FFI (ffi/zig/) and the Agda proofs (proofs/). Both compile and are checked in CI, so neither can silently rot — but neither backs the claims their names might suggest. This page states, honestly, exactly what each one does today, what it does not do, and where the open targets are tracked.

The canonical one-line summary lives in the == Experimental surfaces section of README.adoc; this page expands it. The positioning was set deliberately in the "experimental reframe" work order (PR #48, docs: reframe FFI + formal-proofs surfaces as experimental (W2-4)), and the wording here mirrors that framing.

From README.adoc:

• FFI (ffi/zig/) — Experimental. Compiles and is CI-tested, but the exported entry points are placeholders not yet backed by the Julia core; the Idris2 ABI layer is design-only (src/abi/ does not exist in this repo).
• Proofs (proofs/) — Experimental. Small ℕ-level lemmas type-checked by agda --safe in CI; the statistical theorems over ℝ remain open targets.

Neither boundary weakens the Julia statistical core, which is tested and reference-validated (see Testing-and-Validation).

What is not claimed: Statistikles is not "formally verified" for its statistics, and no number the LLM emits is proven correct by Agda. The real guarantee — no number is ever produced by the LLM — is a code-structure property enforced at the src/tools/executor.jl execute_tool() boundary and audited by the guardrail (see Testing-and-Validation), not an Agda-proven one.

---

Zig FFI (ffi/zig/)

What is real and CI-checked

The FFI locks a C ABI so downstream consumers can bind against a stable surface, and it is built + tested on every change to ffi/zig/** by .github/workflows/zig.yml against Zig 0.13.0:

- name: Build + test FFI
  working-directory: ffi/zig
  run: zig build test --summary all

build.zig produces a shared library (.so/.dylib/.dll) and a static library (.a), both linking libC, and wires zig build test to run both the in-source unit tests and the test/integration_test.zig integration tests:

cd ffi/zig
zig build                         # debug build
zig build -Doptimize=ReleaseFast  # optimized
zig build test                    # unit + integration tests

Twelve C-ABI entry points are exported from src/main.zig, and what they do implement correctly is memory safety, not statistics:

Exported function	Role
statistikles_init / statistikles_free	Lifecycle; allocate/destroy an opaque Handle
statistikles_is_initialized	Liveness query
statistikles_process / statistikles_process_array	Placeholder data ops
statistikles_get_string / statistikles_free_string	Placeholder string result + its free
statistikles_register_callback	Placeholder callback registration
statistikles_last_error	Thread-local last-error (static storage, borrowed pointer)
statistikles_version / statistikles_abi_version / statistikles_build_info	Version metadata

The handle carries a liveness magic cookie (0x57A7_1C1E) that is poisoned (0xDEAD_F8EE) on free, so a double-free or an operation on a dangling pointer returns an error code instead of undefined behaviour. That safety behaviour is what the tests actually assert — 7 unit tests in src/main.zig and 17 integration tests in test/integration_test.zig:

test "double free is a safe error, not UB" {
    const handle = statistikles_init() orelse return error.InitFailed;
    try std.testing.expectEqual(Result.ok, statistikles_free(handle));
    // Second free must be rejected, not a second destroy().
    try std.testing.expectEqual(Result.invalid_param, statistikles_free(handle));
}

What is placeholder / design-only

Directly from the build.zig and main.zig headers:

STATUS — EXPERIMENTAL: this FFI locks the C ABI and is CI-checked so it cannot silently break, but the exported operations are PLACEHOLDERS. They validate their arguments and enforce handle liveness, yet they are NOT backed by the Julia statistical core, and there is (deliberately) no Idris2 ABI wired up.

So:

• statistikles_process, statistikles_process_array, statistikles_get_string, and statistikles_register_callback check the handle and arguments, then discard the input (_ = input;) — they perform no real statistics and call no Julia code.

• The Idris2 ABI layer is design-only. ABI-FFI-README.md describes an intended pipeline (Idris2 src/abi/*.idr → generated C header → Zig FFI), but its status banner states plainly:

  src/abi/ does not exist in this repo (the template scaffolding that once lived there was removed — see PROOF-NEEDS.md, "Template ABI Cleanup"). Everything in this document past this notice describes the intended design, not the current state.

  Per PROOF-NEEDS.md, the template Types.idr / Layout.idr / Foreign.idr files were removed on 2026-03-29 because they "were creating a false impression of formal verification" — they held only RSR template scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs. generated/abi/ and bindings/ likewise do not exist; only ffi/zig/ is real.

Making the FFI ops call the real Julia core, and building any ABI proof layer, are explicitly out of scope and deferred (work order W2-4).

---

Agda proofs (proofs/)

What type-checks and is CI-checked

The proofs/ tree is an Agda library (statistikles-proofs.agda-lib, depending on standard-library) with three modules that type-check under agda --safe — no postulates, no holes:

agda --safe Statistikles/TropicalSemiring.agda
agda --safe Statistikles/RankIdentities.agda
agda --safe Statistikles/Inequalities.agda

.github/workflows/agda.yml runs exactly this on every proofs/**/*.agda module and enforces three things:

• every module must pass agda --safe (no weakening of --safe);
• no postulate is permitted anywhere under proofs/ (the lemmas are constructive) — this is also re-checked by the Aspect — Safety + SPDX job in e2e.yml;
• a new .agda file that is not registered in the workflow's module list fails the job, so a proof can't be added and left unchecked.

The honest gap: ℕ, not ℝ

This is the critical caveat, stated verbatim in proofs/README.adoc:

These modules type-check under agda --safe with no postulates and no holes — but they are not yet proofs of the statistical theorems Statistikles relies on. Every lemma below is stated and proven over the natural numbers (ℕ). The runtime computes over Float64 (IEEE-754 doubles), so each entry is a discrete proxy for — not a proof of — the statistical target.

Read "Proven (ℕ)" as "this discrete lemma type-checks", not as "the statistic is verified". The gap between the ℕ lemma and the ℝ/Float64 statement the statistic actually needs is real, and every row's right-hand target is marked pending:

#	Lemma actually proven (over ℕ)	File	Statistical target (pending, over ℝ)
1	min-assoc — min is associative	TropicalSemiring.agda	Associativity of tropical ⊕ = min
2	min-comm — min is commutative	TropicalSemiring.agda	Commutativity of tropical ⊕
3	+-distrib-min — + distributes over min	TropicalSemiring.agda	Tropical ⊗ = + distributes over ⊕
4	min-idem — min a a ≡ a	TropicalSemiring.agda	Idempotence of tropical ⊕
5	tropical-mul-identity — 0 is left identity of +	TropicalSemiring.agda	0 is the tropical ⊗-identity
6	df-identity / df-nonneg — truncated subtraction on ℕ	RankIdentities.agda	χ² df = (categories − 1) is well-defined & ≥ 0
7	sum-to recursion (sum-to 100 ≡ 5050) + sum-to-mono	RankIdentities.agda	Rank-sum identity Σᵢ i = n(n+1)/2
8	elem-le-sum — an element ≤ the list sum	Inequalities.agda	Bonferroni P(⋃ Aᵢ) ≤ Σ P(Aᵢ)
9	sq-mono — squaring is monotone	Inequalities.agda	Monotonicity of the tie-correction term Σ(tᵢ³ − tᵢ)
10	mean-ordering-transitive — transitivity of ≤	Inequalities.agda	Transitivity of power-mean ordering M_p ≤ M_q ≤ M_r ⇒ M_p ≤ M_r

All ten lemmas are Proven (ℕ); all ten statistical targets remain pending. The lemma signatures above are the exact ones in the source, e.g.:

min-assoc : ∀ (a b c : ℕ) → min a (min b c) ≡ min (min a b) c
df-identity : ∀ (k : ℕ) → suc k ∸ 1 ≡ k
elem-le-sum : ∀ (x : ℕ) (xs : List ℕ) → x ≤ x + list-sum xs
mean-ordering-transitive : ∀ {a b c : ℕ} → a ≤ b → b ≤ c → a ≤ c

Building the proofs requires Agda 2.6.4+ and agda-stdlib 2.x.

ECHIDNA integration is aspirational

proofs/README.adoc and PROOF-NEEDS.md both flag that the intended wiring — these proofs backing the StatProofObligation entries in src/bridge/echidna_adapter.jl, with ECHIDNA dispatching constructive obligations to Agda and arithmetic ones to Z3 — is not yet in place. The echidna_adapter.jl module header was itself reworded in the reframe to describe "EXPERIMENTAL / design-only proof-dispatch scaffolding" whose identities are proof targets, not currently-verified statements. Open targets are catalogued in PROOF-NEEDS.md.

---

Summary

Surface	Compiles?	CI-checked?	What it actually guarantees today	What it does not do
Zig FFI (ffi/zig/)	Yes (Zig 0.13.0)	Yes (zig build test)	A stable, memory-safe C ABI (handle liveness, safe double-free)	Compute any statistics; call the Julia core; provide an Idris2 ABI (src/abi/ absent)
Agda proofs (proofs/)	Yes (Agda 2.6.4+)	Yes (agda --safe, no postulates)	10 constructive ℕ-level lemmas type-check	Prove the ℝ/Float64 statistical theorems; back ECHIDNA dispatch (unwired)

Neither surface weakens the Julia statistical core, which is independently tested and reference-validated — see Testing-and-Validation.

See also

• Testing-and-Validation — the tested-and-reference-validated Julia core, and the guardrail that enforces the neural/symbolic boundary.
• Home
• Repo docs: README.adoc (§ Experimental surfaces), ABI-FFI-README.md, proofs/README.adoc, PROOF-NEEDS.md.