Skip to content

Commit 2c028a4

Browse files
infra: ABI/FFI docs + header (4A), scorecard perms (3), fuzz build fix (2) (#156)
Three cohesive infra items from the audit follow-up (items **4A, 3, 2**), as separate commits. Item **1** (audience docs + wiki) will be its own PR. ## 4A — ABI/FFI document-and-align (non-breaking) — `0afe7ca` No code paths change; this records the boundary and completes the documented spine. - **New `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`). - **New `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` doesn't 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"`. - **Correct `ABI-FFI-README.md`**: the header is hand-maintained; `idris2 --cg c-header` is aspirational (Idris2 has no such codegen). - **Launcher: deliberately not attempted** — no launcher spec exists in this repo or the reference sibling; it lives in the external `hyperpolymath/standards`. ## 3 — scorecard.yml least-privilege job permissions — `c2b7e81` The OSSF Scorecard reusable-workflow wrapper job had no job-level permissions and leaned on a broad workflow-level `read-all` (Hypatia `scorecard_wrapper_missing_job_permissions`). Granted the documented least-privilege set on the job (`contents`/`actions` read; `security-events`/`id-token` write) and narrowed the workflow-level grant to `contents: read`. ## 2 — fuzz build fix (`pr_fuzzing`) — `fa00b1c` `.clusterfuzzlite/build.sh` ran `cargo install cargo-fuzz --force`, which rebuilt cargo-fuzz + its proc-macro dep `thiserror_impl` under the OSS-Fuzz image's sanitizer `RUSTFLAGS` — failing with `error[E0463]: can't find crate for thiserror_impl` **before any project code compiled**. The `base-builder-rust` image already ships cargo-fuzz, so use it; only fall back to a clean (`RUSTFLAGS`-cleared) install if genuinely missing. > ⚠️ This one is **not locally reproducible** without the OSS-Fuzz container — the `pr_fuzzing` CI checks on this PR are the verification. ## Verification ``` gcc -fsyntax-only -std=c11 ffi/zig/include/valence_shell.h # clean cd ffi/rust && cargo build # ok (doc-only change) bash -n .clusterfuzzlite/build.sh # ok python3 -c "import yaml,glob; [yaml.safe_load(open(f)) for f in glob.glob('.github/workflows/*.yml')]" # all parse ``` 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU --- _Generated by [Claude Code](https://claude.ai/code/session_01KfgJznd6jzSeDYsSXGAXkU)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent dd4da3e commit 2c028a4

11 files changed

Lines changed: 242 additions & 20 deletions

File tree

.clusterfuzzlite/build.sh

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,20 @@ set -euo pipefail
66

77
cd "$SRC"/valence-shell/impl/rust-cli
88

9-
# Install cargo-fuzz if not present
10-
cargo install cargo-fuzz --force
9+
# The OSS-Fuzz base-builder-rust image already ships cargo-fuzz. Reinstalling it
10+
# with `cargo install --force` rebuilds cargo-fuzz and its dependencies —
11+
# including the proc-macro crate `thiserror_impl` — under the image's sanitizer
12+
# RUSTFLAGS, which breaks the host build with:
13+
# error[E0463]: can't find crate for `thiserror_impl`
14+
# So prefer the pre-installed cargo-fuzz, and only fall back to a clean install
15+
# (RUSTFLAGS cleared) if it is genuinely missing.
16+
if ! command -v cargo-fuzz >/dev/null 2>&1; then
17+
RUSTFLAGS="" cargo install cargo-fuzz --locked
18+
fi
1119

12-
# Build all fuzz targets
13-
cargo +nightly fuzz build
20+
# Build all fuzz targets. cargo-fuzz only supports the address sanitizer for
21+
# Rust; honour $SANITIZER when set (OSS-Fuzz exports it) but default to address.
22+
cargo +nightly fuzz build --sanitizer "${SANITIZER:-address}"
1423

1524
# Copy fuzz targets to $OUT
1625
for target in fuzz/target/*/release/fuzz_*; do

.clusterfuzzlite/project.yaml

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,13 @@ primary_contact: "jonathan.jewell@open.ac.uk"
77
auto_ccs:
88
- "jonathan.jewell@open.ac.uk"
99

10+
# Rust fuzz targets are built by cargo-fuzz, which hard-codes AddressSanitizer
11+
# and ignores $SANITIZER. Advertising `undefined`/`memory` makes OSS-Fuzz's
12+
# bad_build_check fail ("UBSan build ... seems to be compiled with ASan"),
13+
# because the produced binary is always ASan. ASan already covers Rust's
14+
# relevant memory-safety classes here, so `address` is the supported set.
1015
sanitizers:
1116
- address
12-
- undefined
13-
- memory
1417

1518
fuzzing_engines:
1619
- libfuzzer

.github/workflows/cflite_batch.yml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,9 @@ jobs:
2424
strategy:
2525
fail-fast: false
2626
matrix:
27-
sanitizer: [address, undefined, memory]
27+
# cargo-fuzz hard-codes ASan for Rust, so only `address` yields a valid
28+
# build (see .clusterfuzzlite/project.yaml for the full rationale).
29+
sanitizer: [address]
2830
steps:
2931
- name: Checkout code
3032
uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4

.github/workflows/cflite_pr.yml

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,9 @@ jobs:
2323
strategy:
2424
fail-fast: false
2525
matrix:
26-
sanitizer: [address, undefined]
26+
# cargo-fuzz hard-codes ASan for Rust, so only `address` yields a valid
27+
# build (see .clusterfuzzlite/project.yaml for the full rationale).
28+
sanitizer: [address]
2729
steps:
2830
- name: Checkout code
2931
uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4

.github/workflows/scorecard.yml

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,18 @@ on:
88
push:
99
branches: [main]
1010

11-
permissions: read-all
11+
permissions:
12+
contents: read
1213

1314
jobs:
1415
analysis:
16+
# Explicit least-privilege permissions for the OSSF Scorecard reusable
17+
# workflow (the documented set), instead of relying on a broad
18+
# workflow-level `read-all`:
19+
permissions:
20+
contents: read # read the repository
21+
actions: read # inspect workflow runs (Token-Permissions, etc.)
22+
security-events: write # upload results to the code-scanning dashboard
23+
id-token: write # OIDC, to publish results / badge
1524
uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e
1625
secrets: inherit

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)