Skip to content

Commit d26a219

Browse files
docs+ffi: fill rsr-template placeholders left from template instantiation (#59)
The repo was scaffolded from rsr-template-repo but several files still carried unfilled `{{project}}`, `{{PROJECT}}`, `{{BUILD_CMD}}`, `{{TEST_CMD}}`, `{{LANG_STACK}}`, `{{MUST_INVARIANTS}}`, `{{PACKAGE_NAME}}`, `{{DEPS}}`, and `{{BUILD_OUTPUT_PATH}}` placeholders. The repo's own `.machine_readable/agent_instructions/methodology.a2ml` lists `{{PROJECT}}` and `rsr-template-repo` in its `reject-if-contains` policy, so these were also active policy violations. Substitutions: * `ABI-FFI-README.md`, `ffi/zig/build.zig`, `ffi/zig/test/integration_test.zig` — `{{project}}` → `valence_shell` (matches the symbol prefix already exported from `ffi/zig/src/main.zig`); `{{PROJECT}}` → `ValenceShell` (PascalCase Idris module path). Directory-tree root label fixed to the actual hyphenated repo name. * `alkahest-shell-transmuter/*` — same substitutions but scoped to `alkahest` / `Alkahest` since that subtree is its own subproject. * `QUICKSTART-DEV.adoc` — populated tech stack, build/test commands (cross-referenced against the top-level `Justfile` recipes), and inlined the key MUST invariants from `.machine_readable/MUST.contractile` rather than leaving a placeholder. * `QUICKSTART-MAINTAINER.adoc` — populated runtime deps (glibc, optional Lean/Erlang runtimes), build output paths (`vsh` binary + `libvalence_shell.{so,a}` + generated header), and substituted `{{PACKAGE_NAME}}` → `valence-shell` throughout install/config paths. Also: * Removed `tests/fuzz/placeholder.txt`, a scorecard placeholder inherited from rsr-template-repo. Real fuzz infra lives at `impl/rust-cli/fuzz/fuzz_targets/` (cargo-fuzz) and `.clusterfuzzlite/`, so the placeholder served only to misrepresent fuzz coverage. * Updated `TEST-NEEDS.md` FAKE-FUZZ ALERT section accordingly. * Stripped the leading `{{~ Aditionally delete this line ... ~}}` template comment from both `ABI-FFI-README.md` files. The only remaining `{{...}}` strings in the repo are: the legitimate inline-prose reference to forbidden placeholders inside QUICKSTART-DEV's invariants list, the `reject-if-contains` policy entry in `methodology.a2ml` itself, and just-recipe variable references in `impl/ocaml/Justfile` (which are runtime variables, not template placeholders).
1 parent 18e3e3c commit d26a219

13 files changed

Lines changed: 236 additions & 213 deletions

File tree

ABI-FFI-README.md

Lines changed: 26 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,4 @@
1-
{{~ Aditionally delete this line and fill out the template below ~}}
2-
3-
# {{PROJECT}} ABI/FFI Documentation
1+
# ValenceShell ABI/FFI Documentation
42

53
## Overview
64

@@ -26,7 +24,7 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
2624
2725
┌─────────────────────────────────────────────┐
2826
│ C Headers (auto-generated) │
29-
│ generated/abi/{{project}}.h │
27+
│ generated/abi/valence_shell.h │
3028
└─────────────────┬───────────────────────────┘
3129
3230
│ imported by
@@ -39,7 +37,7 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
3937
│ - Memory-safe by default │
4038
└─────────────────┬───────────────────────────┘
4139
42-
│ compiled to lib{{project}}.so/.a
40+
│ compiled to libvalence_shell.so/.a
4341
4442
┌─────────────────────────────────────────────┐
4543
│ Any Language via C ABI │
@@ -50,7 +48,7 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
5048
## Directory Structure
5149

5250
```
53-
{{project}}/
51+
valence-shell/
5452
├── src/
5553
│ ├── abi/ # ABI definitions (Idris2)
5654
│ │ ├── Types.idr # Core type definitions with proofs
@@ -67,11 +65,11 @@ This library follows the **Hyperpolymath RSR Standard** for ABI and FFI design:
6765
│ ├── test/
6866
│ │ └── integration_test.zig
6967
│ └── include/
70-
│ └── {{project}}.h # C header (optional, can be generated)
68+
│ └── valence_shell.h # C header (optional, can be generated)
7169
7270
├── generated/ # Auto-generated files
7371
│ └── abi/
74-
│ └── {{project}}.h # Generated from Idris2 ABI
72+
│ └── valence_shell.h # Generated from Idris2 ABI
7573
7674
└── bindings/ # Language-specific wrappers (optional)
7775
├── rust/
@@ -199,7 +197,7 @@ zig build test # Run tests
199197

200198
```bash
201199
cd src/abi
202-
idris2 --cg c-header Types.idr -o ../../generated/abi/{{project}}.h
200+
idris2 --cg c-header Types.idr -o ../../generated/abi/valence_shell.h
203201
```
204202

205203
### Cross-Compile
@@ -222,32 +220,32 @@ zig build -Dtarget=x86_64-windows
222220
### From C
223221

224222
```c
225-
#include "{{project}}.h"
223+
#include "valence_shell.h"
226224

227225
int main() {
228-
void* handle = {{project}}_init();
226+
void* handle = valence_shell_init();
229227
if (!handle) return 1;
230228

231-
int result = {{project}}_process(handle, 42);
229+
int result = valence_shell_process(handle, 42);
232230
if (result != 0) {
233-
const char* err = {{project}}_last_error();
231+
const char* err = valence_shell_last_error();
234232
fprintf(stderr, "Error: %s\n", err);
235233
}
236234

237-
{{project}}_free(handle);
235+
valence_shell_free(handle);
238236
return 0;
239237
}
240238
```
241239

242240
Compile with:
243241
```bash
244-
gcc -o example example.c -l{{project}} -L./zig-out/lib
242+
gcc -o example example.c -lvalence_shell -L./zig-out/lib
245243
```
246244

247245
### From Idris2
248246

249247
```idris
250-
import {{PROJECT}}.ABI.Foreign
248+
import ValenceShell.ABI.Foreign
251249
252250
main : IO ()
253251
main = do
@@ -264,44 +262,44 @@ main = do
264262
### From Rust
265263

266264
```rust
267-
#[link(name = "{{project}}")]
265+
#[link(name = "valence_shell")]
268266
extern "C" {
269-
fn {{project}}_init() -> *mut std::ffi::c_void;
270-
fn {{project}}_free(handle: *mut std::ffi::c_void);
271-
fn {{project}}_process(handle: *mut std::ffi::c_void, input: u32) -> i32;
267+
fn valence_shell_init() -> *mut std::ffi::c_void;
268+
fn valence_shell_free(handle: *mut std::ffi::c_void);
269+
fn valence_shell_process(handle: *mut std::ffi::c_void, input: u32) -> i32;
272270
}
273271

274272
fn main() {
275273
unsafe {
276-
let handle = {{project}}_init();
274+
let handle = valence_shell_init();
277275
assert!(!handle.is_null());
278276

279-
let result = {{project}}_process(handle, 42);
277+
let result = valence_shell_process(handle, 42);
280278
assert_eq!(result, 0);
281279

282-
{{project}}_free(handle);
280+
valence_shell_free(handle);
283281
}
284282
}
285283
```
286284

287285
### From Julia
288286

289287
```julia
290-
const lib{{project}} = "lib{{project}}"
288+
const libvalence_shell = "libvalence_shell"
291289

292290
function init()
293-
handle = ccall((:{{project}}_init, lib{{project}}), Ptr{Cvoid}, ())
291+
handle = ccall((:valence_shell_init, libvalence_shell), Ptr{Cvoid}, ())
294292
handle == C_NULL && error("Failed to initialize")
295293
handle
296294
end
297295

298296
function process(handle, input)
299-
result = ccall((:{{project}}_process, lib{{project}}), Cint, (Ptr{Cvoid}, UInt32), handle, input)
297+
result = ccall((:valence_shell_process, libvalence_shell), Cint, (Ptr{Cvoid}, UInt32), handle, input)
300298
result
301299
end
302300

303301
function cleanup(handle)
304-
ccall((:{{project}}_free, lib{{project}}), Cvoid, (Ptr{Cvoid},), handle)
302+
ccall((:valence_shell_free, libvalence_shell), Cvoid, (Ptr{Cvoid},), handle)
305303
end
306304

307305
# Usage
@@ -355,7 +353,7 @@ When modifying the ABI/FFI:
355353

356354
2. **Generate C header**
357355
```bash
358-
idris2 --cg c-header src/abi/Types.idr -o generated/abi/{{project}}.h
356+
idris2 --cg c-header src/abi/Types.idr -o generated/abi/valence_shell.h
359357
```
360358

361359
3. **Update FFI implementation** (`ffi/zig/src/main.zig`)

QUICKSTART-DEV.adoc

Lines changed: 24 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,16 @@
11
// SPDX-License-Identifier: MPL-2.0
2-
// Template: QUICKSTART-DEV.adoc — clone → build → test → PR
3-
// Replace valence-shell, {{BUILD_CMD}}, {{TEST_CMD}}, {{LANG_STACK}} with actuals
42
= valence-shell — Quick Start for Developers
53
:toc:
64
:toclevels: 2
75

86
== Tech Stack
97

10-
{{LANG_STACK}}
8+
* **Rust** — CLI implementation (`impl/rust-cli/`), Cargo crate `vsh`
9+
* **Idris2** — ABI definitions with formal proofs (`src/abi/`, `proofs/idris2/`)
10+
* **Zig** — C-compatible FFI layer (`ffi/zig/`, exports `valence_shell_*`)
11+
* **Coq / Lean4 / Agda / Isabelle / Mizar** — 6-system polyglot proofs (`proofs/`)
12+
* **Elixir** — NIF daemon + MCP server (`impl/elixir/`)
13+
* **OCaml** — Lean-extraction FFI wrapper (`impl/ocaml/`)
1114

1215
== Set Up Development Environment
1316

@@ -38,14 +41,23 @@ just setup-dev
3841

3942
[source,bash]
4043
----
41-
{{BUILD_CMD}}
44+
just build-everything # Build proofs + FFI + CLI + Elixir + MCP
45+
# or one layer at a time:
46+
just build-coq # Coq proofs
47+
just build-lean4 # Lean4 proofs
48+
just build-cli # Rust CLI (vsh)
49+
just build-ffi # Zig + OCaml FFI
4250
----
4351

4452
== Test
4553

4654
[source,bash]
4755
----
48-
{{TEST_CMD}}
56+
just verify-all # Verify all proof systems
57+
just test-cli # Cargo test for impl/rust-cli/
58+
just test-ffi-zig # Zig FFI integration tests
59+
just test-ffi-ocaml # OCaml FFI tests
60+
just test-elixir # Elixir NIF tests
4961
----
5062

5163
== Project Structure
@@ -91,7 +103,13 @@ just panic-scan # No new security issues
91103
Read `.machine_readable/MUST.contractile` before making changes.
92104
Key invariants that must never be violated:
93105

94-
{{MUST_INVARIANTS}}
106+
* No hardcoded absolute paths (`/home/*`, `/mnt/*`); use env vars, XDG dirs, or relative references
107+
* No new TypeScript / Python / Go files; no npm/bun/yarn/pnpm dependencies (Deno only)
108+
* No `believe_me` or `assert_total` (Idris2); no new `Admitted.` (Coq); no `sorry` (Lean); no `unsafeCoerce` (Haskell); no `Obj.magic` (OCaml)
109+
* No `unsafe {}` blocks without an inline safety comment (Rust)
110+
* No template placeholders (`{{...}}`, `<...>`) in shipped files — see `.machine_readable/agent_instructions/methodology.a2ml`
111+
* All commits MUST be GPG-signed
112+
* Full machine-checked list lives at `.machine_readable/MUST.contractile`; K9 validators in `contractiles/k9/` enforce it on every PR
95113

96114
== LLM/AI Agent Development
97115

QUICKSTART-MAINTAINER.adoc

Lines changed: 21 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,4 @@
11
// SPDX-License-Identifier: MPL-2.0
2-
// Template: QUICKSTART-MAINTAINER.adoc — packaging, deploying, and maintaining
3-
// Replace valence-shell, {{PACKAGE_NAME}}, {{DEPS}} with actuals
42
= valence-shell — Quick Start for Platform Maintainers
53
:toc:
64
:toclevels: 2
@@ -12,7 +10,15 @@ distribution on your platform.
1210

1311
== Runtime Dependencies
1412

15-
{{DEPS}}
13+
* `glibc` >= 2.34 (or `musl` >= 1.2 for static builds)
14+
* Optional: `libleanshared.so` (Lean 4 runtime; required only when the Lean-extraction FFI feature is enabled — see `impl/rust-cli/docs/LEAN_EXTRACTION_BUILD_GUIDE.md`)
15+
* Optional: Erlang/OTP >= 26 (required only for the Elixir NIF daemon + MCP server features)
16+
17+
Build-time dependencies (not required at runtime):
18+
19+
* Rust >= 1.75 (CLI build)
20+
* Zig >= 0.13 (FFI library build)
21+
* Coq 8.18, Lean 4, Agda 2.6, Isabelle 2024, Mizar (proof verification; not required for release packaging if proofs are pre-verified in CI)
1622

1723
== Build from Source
1824

@@ -23,7 +29,11 @@ cd valence-shell
2329
just build-release
2430
----
2531

26-
Output: `{{BUILD_OUTPUT_PATH}}`
32+
Output:
33+
34+
* `impl/rust-cli/target/release/vsh` — the `vsh` CLI binary
35+
* `ffi/zig/zig-out/lib/libvalence_shell.{so,a}` — shared and static FFI libraries
36+
* `ffi/zig/zig-out/include/valence_shell.h` — generated C header
2737

2838
== Packaging
2939

@@ -65,10 +75,10 @@ Files installed:
6575
| `$PREFIX/bin/`
6676
| Executables
6777

68-
| `$PREFIX/share/{{PACKAGE_NAME}}/`
78+
| `$PREFIX/share/valence-shell/`
6979
| Data files, assets
7080

71-
| `$PREFIX/share/doc/{{PACKAGE_NAME}}/`
81+
| `$PREFIX/share/doc/valence-shell/`
7282
| Documentation
7383

7484
| `$PREFIX/share/applications/`
@@ -80,9 +90,9 @@ Files installed:
8090

8191
== Configuration
8292

83-
Default config location: `$XDG_CONFIG_HOME/{{PACKAGE_NAME}}/config.toml`
93+
Default config location: `$XDG_CONFIG_HOME/valence-shell/config.toml`
8494

85-
Fallback: `$HOME/.config/{{PACKAGE_NAME}}/config.toml`
95+
Fallback: `$HOME/.config/valence-shell/config.toml`
8696

8797
== Health Checks
8898

@@ -102,7 +112,7 @@ just build-release
102112
just install --prefix=/usr/local
103113
----
104114

105-
Or via OPSM: `opsm update {{PACKAGE_NAME}}`
115+
Or via OPSM: `opsm update valence-shell`
106116

107117
== Security Notes
108118

@@ -117,8 +127,8 @@ For deploying multiple instances (e.g., different users or tenants):
117127

118128
[source,bash]
119129
----
120-
just install --prefix=/opt/{{PACKAGE_NAME}}-instance1 --config=/etc/{{PACKAGE_NAME}}/instance1.toml
121-
just install --prefix=/opt/{{PACKAGE_NAME}}-instance2 --config=/etc/{{PACKAGE_NAME}}/instance2.toml
130+
just install --prefix=/opt/valence-shell-instance1 --config=/etc/valence-shell/instance1.toml
131+
just install --prefix=/opt/valence-shell-instance2 --config=/etc/valence-shell/instance2.toml
122132
----
123133

124134
Each instance has isolated config, data, and logs.

TEST-NEEDS.md

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -70,8 +70,8 @@
7070
- Elixir tests: ✅ **+6** (NIF-specific behavior)
7171
- **Total test coverage increase: ~60 new tests/benchmarks**
7272

73-
## FAKE-FUZZ ALERT
73+
## Fuzz coverage
7474

75-
- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
76-
- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
77-
- Priority: P2 — creates false impression of fuzz coverage
75+
- Real fuzz harnesses live at `impl/rust-cli/fuzz/fuzz_targets/` (cargo-fuzz) and `.clusterfuzzlite/` (ClusterFuzzLite CI integration).
76+
- The legacy `tests/fuzz/placeholder.txt` scorecard-placeholder was removed on 2026-06-01; the real harnesses now satisfy the fuzz-coverage scorecard signal.
77+
- Missing fuzz targets per #43 (quotes, redirection, here_docs, command_sub, process_sub) tracked separately.

0 commit comments

Comments
 (0)