Skip to content

Commit 0afe7ca

Browse files
committed
docs(abi/ffi): add C header + boundary decision record; correct FFI mislabels
Item 4A (document-and-align, non-breaking) of the ABI/FFI consolidation. No code paths change; this records the boundary and completes the documented spine. - Add ffi/zig/include/valence_shell.h — the C ABI header that was documented but missing. Hand-written to match the 11 `export fn valence_shell_*` in ffi/zig/src/main.zig and the `%foreign` decls in src/abi/Foreign.idr. Verified: compiles warning-clean as C11 and C++, and a consumer TU using all 11 symbols type-checks (gcc -fsyntax-only). - Add docs/ABI-FFI-BOUNDARY.md — records the canonical spine (Idris2 src/abi -> Zig ffi/zig -> C header), the three sanctioned exceptions with rationale (C Erlang NIF, C OCaml/Lean wrapper, ReScript MCP), the two-Zig-tree status, and that impl/rust-cli does not yet link the FFI. The code-level rewrite (port ffi/rust to Zig, wire the CLI, collapse impl/zig) is explicitly deferred to a separate owner-approved pass. - Relabel ffi/rust as a Rust *library* (calls libc/POSIX), not a C-ABI FFI — it exposes no #[no_mangle]/extern "C"; the C-ABI-provider role is ffi/zig's. - Correct ABI-FFI-README.md: the header is hand-maintained; the `idris2 --cg c-header` step it described is aspirational (Idris2 has no such codegen). Launcher: deliberately not attempted — no launcher spec exists in this repo or the reference sibling; the standard lives in the external hyperpolymath/standards. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU
1 parent dd4da3e commit 0afe7ca

5 files changed

Lines changed: 207 additions & 10 deletions

File tree

ABI-FFI-README.md

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -197,12 +197,14 @@ zig build -Doptimize=ReleaseFast # Build optimized
197197
zig build test # Run tests
198198
```
199199

200-
### Generate C Header from Idris2 ABI
200+
### C Header
201201

202-
```bash
203-
cd src/abi
204-
idris2 --cg c-header Types.idr -o ../../generated/abi/valence_shell.h
205-
```
202+
The C header lives at **`ffi/zig/include/valence_shell.h`** and is
203+
**hand-maintained** to match the `export fn` signatures in
204+
`ffi/zig/src/main.zig`. Idris2 ships no `c-header` codegen (only
205+
chez/node/racket/refc), so the older `idris2 --cg c-header` step is aspirational
206+
— update the header by hand in the same commit as any FFI signature change.
207+
See [`docs/ABI-FFI-BOUNDARY.md`](docs/ABI-FFI-BOUNDARY.md).
206208

207209
### Cross-Compile
208210

@@ -355,10 +357,8 @@ When modifying the ABI/FFI:
355357
- Update proofs
356358
- Ensure backward compatibility
357359

358-
2. **Generate C header**
359-
```bash
360-
idris2 --cg c-header src/abi/Types.idr -o generated/abi/valence_shell.h
361-
```
360+
2. **Update the C header by hand** (`ffi/zig/include/valence_shell.h`) to match
361+
the new/changed `export fn` signatures — Idris2 has no `c-header` codegen.
362362

363363
3. **Update FFI implementation** (`ffi/zig/src/main.zig`)
364364
- Implement new functions
@@ -380,6 +380,7 @@ MPL-2.0
380380

381381
## See Also
382382

383+
- [ABI/FFI boundary decision record](docs/ABI-FFI-BOUNDARY.md)
383384
- [Idris2 Documentation](https://idris2.readthedocs.io)
384385
- [Zig Documentation](https://ziglang.org/documentation/master/)
385386
- [Rhodium Standard Repositories](https://github.com/hyperpolymath/rhodium-standard-repositories)

docs/ABI-FFI-BOUNDARY.md

Lines changed: 83 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,83 @@
1+
<!--
2+
SPDX-License-Identifier: CC-BY-SA-4.0
3+
Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
-->
5+
# ABI / FFI boundary — decision record
6+
7+
**Status:** documented (2026-07-01). Non-breaking — this records the current
8+
boundary and the accepted exceptions; it does **not** rewrite any code. The
9+
code-level consolidation (see "Deferred" below) needs a separate, owner-approved
10+
pass.
11+
12+
## Context
13+
14+
The estate convention is **"Idris2 = ABIs, Zig = APIs + FFIs."** An audit found
15+
the convention is *documented and partially scaffolded* but not uniformly
16+
upheld: several non-Zig FFI/API surfaces exist, the Zig spine was unintegrated
17+
(no C header on disk), and the primary Rust CLI doesn't consume the ABI at all.
18+
This record names the canonical spine, sanctions the real exceptions with
19+
rationale, and clarifies each surface's role — without a risky rewrite.
20+
21+
## The canonical ABI/FFI spine (conformant)
22+
23+
```
24+
src/abi/*.idr Idris2 ABI declarations (%foreign)
25+
26+
27+
ffi/zig/src/main.zig Zig FFI implementation (export fn) → libvalence_shell.{so,a}
28+
29+
30+
ffi/zig/include/valence_shell.h C header (any language via C ABI)
31+
```
32+
33+
- `src/abi/Foreign.idr`'s `%foreign "C:valence_shell_*, libvalence_shell"`
34+
declarations correspond 1:1 to `ffi/zig/src/main.zig`'s `export fn
35+
valence_shell_*` symbols (11 functions).
36+
- The C header **`ffi/zig/include/valence_shell.h`** is now present and
37+
**hand-maintained** to match those exports. (Older docs describe an `idris2
38+
--cg c-header` step, but Idris2 ships no such codegen — only chez/node/racket/
39+
refc — so the header is authored by hand and updated in the same commit as any
40+
`export fn` change.)
41+
42+
## Named exceptions — surfaces that are *not* on the Zig C-ABI spine
43+
44+
These are accepted deviations from "all FFIs are Zig", each for a concrete
45+
reason. They are sanctioned, not stray.
46+
47+
| Surface | Language | Why not Zig | Status |
48+
|---|---|---|---|
49+
| `impl/elixir/c_src/valence_nif.c` | C | The BEAM NIF ABI is fixed by `erl_nif.h`; the glue is C by necessity. It *calls* the Zig fast-path lib. | Sanctioned exception |
50+
| `impl/ocaml/lean_wrapper.c` | C | Marshaling Lean-4-extracted objects into OCaml uses the OCaml/Lean C runtime ABI. | Sanctioned exception |
51+
| `impl/mcp/**/*.res` | ReScript/Deno | MCP is a *protocol* API (JSON-RPC over stdio/HTTP), not a C ABI; ReScript per estate language policy. | Sanctioned (API, not a C-ABI FFI) |
52+
53+
## Clarifications (role of each Rust/Zig surface)
54+
55+
- **`ffi/rust/` is a Rust *library*, not a C-ABI FFI.** It consumes POSIX/libc
56+
(a "foreign function interface" only in the *calls-libc* sense) with
57+
precondition checking; it exposes **no** `#[no_mangle]`/`extern "C"` symbols
58+
and is not something other languages link against. The C-ABI-*provider* role
59+
belongs to `ffi/zig`. Its docs have been relabeled to say so.
60+
- **Two Zig trees.** `ffi/zig/` is the **canonical**, spine-conformant FFI
61+
(11 exports, wired to the Idris2 ABI declarations). `impl/zig/` is an
62+
experimental fast-path lib plus a Lean-runtime wrapper, gated on the
63+
not-yet-built BEAM daemon. Collapsing the two is future work.
64+
- **The primary Rust CLI (`impl/rust-cli/`) does not link the FFI.** Its
65+
`build.rs` is intentionally a no-op; `vsh` is a self-contained pure-Rust
66+
shell today. Wiring it to the Zig FFI is future work.
67+
68+
## Deferred (code-level consolidation — needs owner sign-off)
69+
70+
Out of scope for this documentation pass because each can destabilize the
71+
shipping shell:
72+
73+
1. Port `ffi/rust` to Zig, or fold it behind the Zig FFI.
74+
2. Wire `impl/rust-cli` to the Zig FFI (replace the no-op `build.rs`).
75+
3. Collapse `impl/zig` into `ffi/zig`.
76+
77+
Until then, the spine above is the documented contract, and the three
78+
exceptions are the sanctioned deviations.
79+
80+
## See also
81+
82+
- `ABI-FFI-README.md` — architecture overview and per-language usage.
83+
- `src/abi/README.adoc`, `ffi/zig/README.adoc` — the two ends of the spine.

ffi/rust/README.adoc

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,12 @@ Standalone Rust crate (`vsh-ffi`, library `vsh_ffi`) that exposes
66
verified POSIX operations with precondition checking. Bridges the
77
Coq/Lean filesystem proofs in `../../proofs/` to real POSIX syscalls.
88

9-
This is the **canonical** Rust FFI tree. The previous `impl/rust-ffi/`
9+
NOTE: "FFI" here means this crate _calls_ foreign functions (libc/POSIX). It is
10+
an internal Rust library — it exposes no `#[no_mangle]` / `extern "C"` C ABI and
11+
is not linked by other languages. The C-ABI boundary that other languages call
12+
is the Zig FFI in `../zig/`; see `../../docs/ABI-FFI-BOUNDARY.md`.
13+
14+
This is the **canonical** Rust tree (among Rust helper trees). The previous `impl/rust-ffi/`
1015
duplicate was deleted on 2026-04-19 in commit `f43cfb5` after
1116
verification that 6 of 7 sibling files were byte-identical and that
1217
this tree is the superset (carries `verification.rs` plus richer

ffi/rust/src/lib.rs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,12 @@
55
//! This crate provides the FFI (Foreign Function Interface) layer that bridges
66
//! Coq-verified operations to real POSIX syscalls.
77
//!
8+
//! > **Boundary note:** "FFI" here means this crate *calls* foreign functions
9+
//! > (libc/POSIX). It is an internal Rust library and does **not** export a C
10+
//! > ABI (`#[no_mangle]`/`extern "C"`), so it is not the C-ABI boundary that
11+
//! > other languages link against — that role belongs to the Zig FFI in
12+
//! > `ffi/zig/`. See `docs/ABI-FFI-BOUNDARY.md`.
13+
//!
814
//! # Trust Boundaries
915
//!
1016
//! ```text

ffi/zig/include/valence_shell.h

Lines changed: 102 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,102 @@
1+
/* SPDX-License-Identifier: MPL-2.0
2+
* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
*
4+
* C ABI for libvalence_shell — the stable boundary that any language may call.
5+
*
6+
* This header is the C projection of the ABI/FFI spine:
7+
*
8+
* src/abi — Idris2 ABI declarations (%foreign)
9+
* │
10+
* ▼
11+
* ffi/zig/src/main.zig — Zig FFI implementation (`export fn`)
12+
* │ compiled to libvalence_shell.{so,a}
13+
* ▼
14+
* THIS HEADER → C, Rust, ReScript, Julia, …
15+
*
16+
* NOTE ON PROVENANCE: this file is HAND-MAINTAINED to match the `export fn`
17+
* signatures in ffi/zig/src/main.zig and the `%foreign` declarations in
18+
* src/abi/Foreign.idr. Older docs describe an `idris2 --cg c-header` step, but
19+
* Idris2 ships no such codegen (only chez/node/racket/refc), so the header is
20+
* authored by hand. When you add or change a Zig `export fn`, update this
21+
* header in the same commit. See docs/ABI-FFI-BOUNDARY.md.
22+
*/
23+
24+
#ifndef VALENCE_SHELL_H
25+
#define VALENCE_SHELL_H
26+
27+
#include <stdint.h>
28+
29+
#ifdef __cplusplus
30+
extern "C" {
31+
#endif
32+
33+
/* Opaque library handle. Its layout is private to the Zig implementation;
34+
* C consumers only ever hold a pointer to it. (Matches `?*Handle`.) */
35+
typedef struct ValenceShellHandle ValenceShellHandle;
36+
37+
/* Result codes. Backed by `c_int` to match `enum(c_int)` in main.zig and the
38+
* Idris2 `Result` type in src/abi/Types.idr. */
39+
typedef enum ValenceShellResult {
40+
VALENCE_SHELL_OK = 0,
41+
VALENCE_SHELL_ERROR = 1,
42+
VALENCE_SHELL_INVALID_PARAM = 2,
43+
VALENCE_SHELL_OUT_OF_MEMORY = 3,
44+
VALENCE_SHELL_NULL_POINTER = 4
45+
} ValenceShellResult;
46+
47+
/* Callback invoked by the library. Matches
48+
* `*const fn (u64, u32) callconv(.C) u32`. */
49+
typedef uint32_t (*ValenceShellCallback)(uint64_t context, uint32_t value);
50+
51+
/* --- Lifecycle -------------------------------------------------------------- */
52+
53+
/* Initialize the library. Returns a handle, or NULL on failure. */
54+
ValenceShellHandle *valence_shell_init(void);
55+
56+
/* Release a handle previously returned by valence_shell_init. */
57+
void valence_shell_free(ValenceShellHandle *handle);
58+
59+
/* Non-zero if `handle` refers to an initialized library instance. */
60+
uint32_t valence_shell_is_initialized(ValenceShellHandle *handle);
61+
62+
/* --- Operations ------------------------------------------------------------- */
63+
64+
/* Process a single 32-bit input. */
65+
ValenceShellResult valence_shell_process(ValenceShellHandle *handle,
66+
uint32_t input);
67+
68+
/* Process `len` bytes at `buffer`. */
69+
ValenceShellResult valence_shell_process_array(ValenceShellHandle *handle,
70+
const uint8_t *buffer,
71+
uint32_t len);
72+
73+
/* Register a C callback. */
74+
ValenceShellResult valence_shell_register_callback(ValenceShellHandle *handle,
75+
ValenceShellCallback callback);
76+
77+
/* --- Strings ---------------------------------------------------------------- */
78+
79+
/* Borrow the handle's current result string, or NULL. The returned pointer is
80+
* owned by the library; free it with valence_shell_free_string. */
81+
const char *valence_shell_get_string(ValenceShellHandle *handle);
82+
83+
/* Free a string previously returned by the library. */
84+
void valence_shell_free_string(const char *str);
85+
86+
/* --- Diagnostics ------------------------------------------------------------ */
87+
88+
/* Last error message for the calling thread, or NULL if none. Owned by the
89+
* library; do not free. */
90+
const char *valence_shell_last_error(void);
91+
92+
/* Library version string (never NULL). Owned by the library; do not free. */
93+
const char *valence_shell_version(void);
94+
95+
/* Build-info string (never NULL). Owned by the library; do not free. */
96+
const char *valence_shell_build_info(void);
97+
98+
#ifdef __cplusplus
99+
} /* extern "C" */
100+
#endif
101+
102+
#endif /* VALENCE_SHELL_H */

0 commit comments

Comments
 (0)