Skip to content

Commit 03705b5

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
README batch 3/4: 5 implementation/FFI/ABI READMEs (audit item 3)
Continues per-directory README coverage. Covers the three secondary implementation trees, the canonical Zig FFI scaffolding, and the Idris2 ABI declarations. Files added (all .adoc, all SPDX-headed, all reference CLAUDE.md + audit): * impl/elixir/README.adoc — reference impl with broken NIF (per CLAUDE.md "Elixir NIF build broken (low priority)"); enumerates mix manifest, lib/, c_src NIF, native dir, test/, Justfile. * impl/ocaml/README.adoc — extraction target for Coq proofs (design surface only); 4 files (filesystem_ffi, lean_wrapper, valence_lean, Justfile); flags the Lean-extraction residual context (Phase 4C Rust endpoint removed in 5802dc9; OCaml endpoint same residual). * impl/mcp/README.adoc — Deno + ReScript MCP server; cites the 2026-04-04 audit's "hyperpolymath-policy-clean MCP reference" finding; lists Main.res / Server.res / State.res / bindings/. * ffi/zig/README.adoc — ABI/FFI Universal Standard scaffolding; distinguishes from the parallel impl/zig/ daily-driver (different contract); references the global standard + sibling Rust FFI. * src/abi/README.adoc — Idris2 ABI declarations (Types/Layout/Foreign); cites the audit's "minimal stubs" finding honestly; flags absent generated/abi/ header emission as still-TODO. Cumulative coverage move: 15/22 (~68%) → 20/22 (~91%) of non-hidden subtrees in the audit's missing-README list. **Item 3 effectively closed for the source/spec layers; one remaining batch covers utility dirs** (docs, scripts, examples, hooks, benches), most of which may warrant short "intentionally minimal" notes rather than full docs. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent cb0f0b8 commit 03705b5

5 files changed

Lines changed: 249 additions & 0 deletions

File tree

‎ffi/zig/README.adoc‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= ffi/zig/ — Zig FFI (ABI/FFI Universal Standard scaffolding)
3+
4+
Zig FFI implementation matching the **CLAUDE.md ABI/FFI Universal
5+
Standard** layout: Idris2 ABI declarations live in `../../src/abi/`,
6+
the Zig-side concrete implementation lives here, and C-compatible
7+
headers consume the bridge.
8+
9+
Per the 2026-04-18 audit (`../../docs/governance/CRG-AUDIT-2026-04-18.adoc`):
10+
"`ffi/zig/` is ABI-FFI-standard scaffolding". Builds cleanly; not yet
11+
integrated with `../../impl/rust-cli/` (separate, more mature
12+
implementation lives at `../../impl/zig/` targeting ~5ms cold start).
13+
14+
== Files
15+
16+
[cols="2,4"]
17+
|===
18+
| File | Role
19+
20+
| `build.zig` | Zig build manifest.
21+
| `src/main.zig` | FFI surface entry; ABI-conformant exports.
22+
| `test/integration_test.zig` | Integration test for the FFI surface.
23+
|===
24+
25+
== Build + test
26+
27+
```bash
28+
cd ffi/zig
29+
zig build # library build
30+
zig build test # run integration tests
31+
```
32+
33+
== Relationship to `../../impl/zig/`
34+
35+
Two Zig trees serve distinct roles:
36+
37+
* `ffi/zig/` (this tree) — minimal ABI/FFI scaffolding matching the
38+
hyperpolymath universal standard. Use when wiring the formal
39+
Idris2 ABI (`../../src/abi/`) to C-callable Zig.
40+
41+
* `../../impl/zig/` — daily-driver Zig implementation; carries its own
42+
README, targets ~5ms cold start; richer feature surface.
43+
44+
The audit treated these as cooperating, not duplicating; each has a
45+
distinct contract.
46+
47+
== See also
48+
49+
* `../../src/abi/README.adoc` (this batch) — Idris2 ABI declarations
50+
this implementation conforms to
51+
* `../rust/README.adoc` — sibling Rust FFI tree
52+
* `../../impl/zig/` — parallel daily-driver Zig implementation
53+
* `../../CLAUDE.md` — global ABI/FFI Universal Standard layout

‎impl/elixir/README.adoc‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= impl/elixir/ — Elixir Reference Implementation (NIF build broken)
3+
4+
Elixir reference implementation of the valence-shell semantics, intended
5+
to demonstrate portability of the Lean 4 / Coq operational specs to a
6+
BEAM-target language with Rust NIF backing.
7+
8+
Per `../../CLAUDE.md` "What Does NOT Work": the NIF build is currently
9+
broken (declared low priority); the planned BEAM daemon is not yet
10+
implemented. Treat this tree as design-surface, not as a runnable
11+
alternative to `../rust-cli/`.
12+
13+
== Files
14+
15+
[cols="2,4"]
16+
|===
17+
| Path | Role
18+
19+
| `mix.exs` / `mix.lock` | Mix project manifest + locked deps.
20+
| `lib/vsh.ex` | Top-level Elixir module (entry surface).
21+
| `lib/vsh/` | Elixir submodule subtree.
22+
| `lib/mix/` | Mix tasks (project-specific).
23+
| `c_src/valence_nif.c` | C NIF source (the broken layer).
24+
| `native/vsh_nif/` | Rustler-style native subdirectory.
25+
| `test/vsh_test.exs` | ExUnit test entry.
26+
| `test/test_helper.exs` | Test helper bootstrap.
27+
| `Justfile` | Project-local recipes.
28+
|===
29+
30+
== Build (currently broken)
31+
32+
```bash
33+
cd impl/elixir
34+
mix deps.get
35+
mix compile # NIF link step is the failing point per CLAUDE.md
36+
mix test # ExUnit suite, NIF-dependent
37+
```
38+
39+
== Status + intent
40+
41+
* **Current**: NIF build broken; not on the v0.9.x stabilisation track.
42+
* **Planned**: BEAM daemon (separate process) for long-running shell
43+
sessions. Tracked in the repo `ROADMAP.adoc` v2.0 section.
44+
45+
== See also
46+
47+
* `../README.adoc` — implementation-layer overview
48+
* `../../CLAUDE.md` — honest status (declares this tree broken)
49+
* `../../proofs/lean4/README.adoc` — primary spec the implementation
50+
targets

‎impl/mcp/README.adoc‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= impl/mcp/ — MCP Server (Deno + ReScript)
3+
4+
MCP (Model Context Protocol) server exposing valence-shell capabilities
5+
to AI agents. Implemented in ReScript on Deno per the hyperpolymath
6+
language policy in `../../CLAUDE.md` (no Node.js, no TypeScript, no
7+
package.json for runtime deps).
8+
9+
== Files
10+
11+
[cols="2,4"]
12+
|===
13+
| File | Role
14+
15+
| `deno.json` | Deno manifest; import map; tasks.
16+
| `deno.lock` | Locked dependency tree.
17+
| `rescript.json` | ReScript v11+ build config.
18+
| `src/Main.res` | Server entry point.
19+
| `src/Server.res` | MCP server protocol handler (request/response).
20+
| `src/State.res` | Server-side state.
21+
| `src/bindings/` | ReScript-to-JS FFI bindings (e.g. `Mcp.res`).
22+
|===
23+
24+
== Build + run
25+
26+
```bash
27+
cd impl/mcp
28+
deno task build # ReScript → JS via rescript.json
29+
deno task start # runs the MCP server (Deno runtime)
30+
```
31+
32+
== Conventions
33+
34+
* **Language policy compliance** (per CLAUDE.md): zero TypeScript, zero
35+
Node.js, zero npm. Deno + ReScript only. The 2026-04-04 audit
36+
explicitly cited this tree as the hyperpolymath-policy-clean MCP
37+
reference.
38+
* `bindings/Mcp.res` is the protocol-glue layer. Per the 2026-04-04
39+
audit all 24 prior `Obj.magic` uses were eliminated; one remains
40+
documented for the MCP JSON cast.
41+
42+
== See also
43+
44+
* `../README.adoc` — implementation-layer overview
45+
* `../../CLAUDE.md` — language policy (Deno + ReScript, no Node)
46+
* `../../docs/governance/CRG-AUDIT-2026-04-18.adoc` — audit cites this
47+
tree as banned-language-clean

‎impl/ocaml/README.adoc‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= impl/ocaml/ — OCaml Extraction Target (design surface)
3+
4+
OCaml is the extraction target for the Coq proofs in `../../proofs/coq/`
5+
(see `../../proofs/coq/extraction.v`). This tree is intentionally
6+
design-surface only: the Coq verifier emits OCaml that conceptually
7+
matches the in-tree files; nothing here is wired into a runnable binary
8+
in the repo.
9+
10+
== Files
11+
12+
[cols="2,4"]
13+
|===
14+
| File | Role
15+
16+
| `valence_lean.ml` | OCaml-side wrapper around Lean-extracted code.
17+
| `lean_wrapper.c` | C wrapper bridging Lean 4 extracted C to OCaml.
18+
| `filesystem_ffi.ml` | OCaml FFI surface for filesystem operations.
19+
| `Justfile` | Project-local recipes (build / verify).
20+
|===
21+
22+
== Build (design-only)
23+
24+
```bash
25+
cd impl/ocaml
26+
just build # via Justfile (recipe currently a stub for an
27+
# unbuilt target — see CLAUDE.md "What Does NOT Work")
28+
```
29+
30+
The `lean_wrapper.c` companion would have linked extracted Lean 4 C
31+
into OCaml at runtime; the corresponding Rust endpoint
32+
(`impl/rust-cli/src/lean_ffi.rs`) was removed as dead code in commit
33+
`5802dc9` because the underlying extracted-C library was never produced.
34+
The OCaml side carries the same residual design.
35+
36+
== See also
37+
38+
* `../README.adoc` — implementation-layer overview
39+
* `../../proofs/coq/README.adoc` — extraction source (`extraction.v`)
40+
* `../rust-cli/docs/PHASE4C_LEAN_EXTRACTION.md` — archived Lean-extraction
41+
pipeline design (notes the Rust endpoint removal; same context applies
42+
to the OCaml endpoint here)

‎src/abi/README.adoc‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= src/abi/ — Idris2 ABI Declarations (formal interface contracts)
3+
4+
Idris2 dependent-type-checked ABI declarations for the valence-shell
5+
foreign-function interface. Per the **CLAUDE.md ABI/FFI Universal
6+
Standard**:
7+
8+
> Idris2 for ABI: Dependent types prove interface correctness at
9+
> compile-time; formal verification of memory layout; platform-specific
10+
> ABIs with compile-time selection; provable backward compatibility.
11+
12+
This tree provides the formal contract that `../../ffi/zig/` (and any
13+
future per-language FFI binding) must satisfy.
14+
15+
Per the 2026-04-18 audit (`../../docs/governance/CRG-AUDIT-2026-04-18.adoc`):
16+
"minimal stubs; primary proof work is in proofs/{coq,lean4,...} not in
17+
the Idris2 ABI layer". The three-file shape below is the
18+
template-required minimum; deeper proofs live in the `proofs/` tree.
19+
20+
== Files
21+
22+
[cols="2,4"]
23+
|===
24+
| File | Role
25+
26+
| `Types.idr` | Type-level encoding of the FFI value domain
27+
(file descriptors, paths, error codes, etc.).
28+
| `Layout.idr` | Memory-layout proofs (alignment, size, padding) —
29+
the dependent-type guarantee that Zig structs match
30+
the Idris2 contract.
31+
| `Foreign.idr` | `%foreign` declarations: the actual function
32+
signatures exposed across the ABI boundary.
33+
|===
34+
35+
== Build / typecheck
36+
37+
```bash
38+
cd src/abi
39+
idris2 --check Types.idr # single module
40+
idris2 --check Foreign.idr # transitive (imports Types + Layout)
41+
```
42+
43+
== Generated headers
44+
45+
C headers derived from these declarations would be emitted under
46+
`../generated/abi/` per the standard layout (currently absent — this
47+
tree is at the stub stage; the audit's "minimal stubs" finding stands).
48+
49+
== See also
50+
51+
* `../../ffi/zig/README.adoc` — Zig implementation that conforms to
52+
these contracts
53+
* `../../ffi/rust/README.adoc` — Rust FFI library (separate; does not
54+
currently consume these Idris2 declarations)
55+
* `../../CLAUDE.md` — global ABI/FFI Universal Standard
56+
* `../../alkahest-shell-transmuter/src/abi/` — sibling sub-project
57+
carrying its own (also-stub) ABI tree

0 commit comments

Comments
 (0)