Skip to content

Commit 9ecad26

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
README batch 1/4: add 5 subtree READMEs (audit item 3 first batch)
Closes the first 5 of 16 missing per-directory READMEs flagged by CRG-AUDIT-2026-04-18 ("Per-directory README coverage 23% → ~90%" was the single biggest unaddressed C-blocker). Files added (all .adoc, all SPDX-headed): * impl/README.adoc — top-level orientation across the 5 implementations (rust-cli primary; elixir/ocaml/mcp/zig with honest status notes per CLAUDE.md). * impl/rust-cli/src/README.adoc — file-by-file map of the ~32 Rust source files, grouped by concern (entry points, parsing, execution, state+reversibility, REPL+UX, verification, job control). References the .expect("TODO") sweep closure. * impl/rust-cli/tests/README.adoc — 13-suite breakdown with the audit-recorded #[test] counts, run commands, and the API notes for adding tests (ShellState::new takes &str, undo/redo are free functions, history is a public field, etc.). * ffi/rust/README.adoc — Rust FFI crate (vsh-ffi) overview, citing the consolidation commit f43cfb5 (impl/rust-ffi/ deleted as duplicate). Per-file LOC + role table. * proofs/lean4/README.adoc — Lean 4 as primary source of truth; file-by-file role table for the 9 .lean modules + Lake build manifest; cites the verify-proofs CI gate (audit item 6, still open). Coverage move: 5/22 (~23%) → 10/22 (~45%) of non-hidden subtrees. Remaining 11 subtrees in the audit list (not yet addressed): proofs/{coq,agda,isabelle,mizar,z3}, impl/{elixir,ocaml,mcp}, ffi/zig, src/{abi,_root}, scripts/, examples/, hooks/, benches/, docs/. Plus tests/ at repo root if present. All files are read-only docs; no source/build effects. Pattern established for follow-up batches: file inventory + concern grouping + cross-refs to neighbouring trees, audit, and STATE. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent dd35630 commit 9ecad26

5 files changed

Lines changed: 442 additions & 0 deletions

File tree

‎ffi/rust/README.adoc‎

Lines changed: 67 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,67 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= ffi/rust/ — Rust FFI Library (`vsh-ffi`)
3+
4+
Standalone Rust crate (`vsh-ffi`, library `vsh_ffi`) that exposes
5+
verified POSIX operations with precondition checking. Bridges the
6+
Coq/Lean filesystem proofs in `../../proofs/` to real POSIX syscalls.
7+
8+
This is the **canonical** Rust FFI tree. The previous `impl/rust-ffi/`
9+
duplicate was deleted on 2026-04-19 in commit `f43cfb5` after
10+
verification that 6 of 7 sibling files were byte-identical and that
11+
this tree is the superset (carries `verification.rs` plus richer
12+
doc-comments referencing the six-system proof stack). See the
13+
governance audit
14+
`../../docs/governance/CRG-AUDIT-2026-04-18.adoc` for the consolidation
15+
trail.
16+
17+
== Files
18+
19+
[cols="2,1,4"]
20+
|===
21+
| File | LOC | Role
22+
23+
| `src/lib.rs` | 443 | Crate root; re-exports + `FfiContext`
24+
entry point for ABI consumers.
25+
| `src/operations.rs` | 509 | Filesystem ops (`mkdir`, `rmdir`,
26+
`create_file`, `delete_file`,
27+
`atomic_write`, `directory_size`, ...).
28+
| `src/preconditions.rs` | 452 | Per-op precondition checks aligned
29+
with the Coq theorems.
30+
| `src/rmo.rs` | 411 | Remove-Match-Obliterate primitives
31+
(secure-delete with declared passes;
32+
GDPR-relevant).
33+
| `src/audit.rs` | 294 | Append-only audit log; integrity
34+
check via SHA-256 chain.
35+
| `src/sandbox.rs` | 273 | Sandbox-root resolution; clamps `..`
36+
traversal.
37+
| `src/errors.rs` | 206 | Typed error hierarchy via `thiserror`.
38+
| `src/verification.rs` | 462 | Runtime verification suite tying
39+
invocations to proof references.
40+
|===
41+
42+
== Build + test
43+
44+
```bash
45+
cd ffi/rust
46+
cargo build # library build
47+
cargo test # 24 tests (last verified post .expect sweep)
48+
cargo build --features paranoid # extra security checks
49+
cargo build --features audit # detailed audit logging
50+
```
51+
52+
== Conventions
53+
54+
* `#[cfg(test)]` modules at the bottom of each source file; mass
55+
`.unwrap()` is conventional in test scaffolding.
56+
* No `Dockerfile` (use `Containerfile` per repo policy); no banned
57+
languages.
58+
* SPDX header on every file; `PMPL-1.0-or-later`.
59+
* The crate is currently unconsumed by `impl/rust-cli/`; intended for
60+
external linkage from non-Rust callers via the C ABI.
61+
62+
== See also
63+
64+
* `../../impl/rust-cli/` — the primary Rust shell (does NOT depend
65+
on this crate; built separately)
66+
* `../../proofs/coq/` — Coq specs that the operations satisfy
67+
* `../../proofs/lean4/` — Lean 4 specs (cross-validated)

‎impl/README.adoc‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= impl/ — Implementation Layer
3+
4+
Five concrete implementations of the valence-shell semantics, each
5+
serving a distinct role in the polyglot verification stack.
6+
7+
== Subtrees
8+
9+
[cols="1,4"]
10+
|===
11+
| Path | Role
12+
13+
| `rust-cli/`
14+
| **PRIMARY** — the interactive Rust shell. Daily-driver development
15+
target (v0.9.0; see `../CLAUDE.md` for honest status). The other four
16+
trees are reference, extraction target, or known-broken.
17+
18+
| `elixir/`
19+
| Reference implementation in Elixir. The NIF build is currently
20+
broken (declared low-priority in `CLAUDE.md`); the planned BEAM
21+
daemon is not yet built.
22+
23+
| `ocaml/`
24+
| Extraction target for the Coq proofs in `../proofs/coq/`. Three
25+
files (`valence_lean.ml`, `lean_wrapper.c`, `filesystem_ffi.ml`);
26+
design-surface only, not wired into a binary.
27+
28+
| `mcp/`
29+
| ReScript-based MCP (Model Context Protocol) bindings. Uses Deno
30+
+ ReScript per the hyperpolymath language policy in `CLAUDE.md`.
31+
See `mcp/src/bindings/Mcp.res`.
32+
33+
| `zig/`
34+
| Zig FFI implementation targeting ~5ms cold start. Builds cleanly
35+
but is not yet integrated with the Rust CLI. See
36+
`zig/README.adoc` (when present) or `zig/build.zig`.
37+
|===
38+
39+
== Why multiple implementations
40+
41+
Polyglot implementations cross-validate the formal Lean 4 / Coq specs
42+
in `../proofs/`: the Rust CLI is the "is" (running code), the OCaml
43+
extraction is one "ought" path (extracted from Coq), the Elixir / Zig
44+
variants test portability of the same operational semantics.
45+
46+
The audit report `../docs/governance/CRG-AUDIT-2026-04-18.adoc` is the
47+
authoritative cross-implementation status snapshot.
48+
49+
== See also
50+
51+
* `../proofs/` — formal specs the implementations satisfy
52+
* `../ffi/rust/` — Rust FFI library (separate from the CLI; see
53+
its own `README.adoc`)
54+
* `../CLAUDE.md` — honest status per implementation, with explicit
55+
"What Does NOT Work" list

‎impl/rust-cli/src/README.adoc‎

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= impl/rust-cli/src/ — Primary Rust Shell Source
3+
4+
Source tree for the Rust valence-shell binary `vsh` (v0.9.0). Roughly
5+
32 source files; entry points, REPL machinery, parser, executor, state
6+
machine, and verification glue.
7+
8+
Tests live in `../tests/`; the FFI library lives in `../../../ffi/rust/`
9+
(separate crate, not linked from here).
10+
11+
== Files by concern
12+
13+
=== Entry points
14+
15+
[cols="1,3"]
16+
|===
17+
| File | Purpose
18+
| `main.rs` | Binary entry; argument handling; spawns the REPL.
19+
| `lib.rs` | Library root; module declarations + public API.
20+
|===
21+
22+
=== Parsing
23+
24+
[cols="1,3"]
25+
|===
26+
| File | Purpose
27+
| `parser.rs` | Tokeniser + command parser; variable expansion;
28+
parameter expansion (`${VAR:-...}`, etc.); heredoc
29+
extraction; control-flow recognition.
30+
| `quotes.rs` | Quote-aware segmentation (single, double,
31+
backslash); feeds the parser.
32+
| `glob.rs` | POSIX glob expansion (literal-leading-dot
33+
discipline) + brace expansion.
34+
| `arith.rs` | `$((expr))` arithmetic parser + evaluator;
35+
precedence, bitwise, comparison, logical.
36+
| `quotes.rs` | Quote-aware tokenisation.
37+
|===
38+
39+
=== Execution
40+
41+
[cols="1,3"]
42+
|===
43+
| File | Purpose
44+
| `commands.rs` | Built-in command dispatch (mkdir, rmdir, undo,
45+
redo, checkpoint, restore, fg/bg, kill, etc.).
46+
| `commands/` | Module subtree for larger built-ins
47+
(`secure_deletion.rs`, ...).
48+
| `executable.rs` | External-command launch; PATH lookup; shell
49+
function dispatch.
50+
| `external.rs` | External-command pipeline construction;
51+
stdio + redirect wiring.
52+
| `functions.rs` | Shell function table + frame stack.
53+
| `redirection.rs` | I/O redirection setup (`>`, `>>`, `<`, `2>`,
54+
`&>`, `2>&1`).
55+
| `process_sub.rs` | Process substitution `<(cmd)` / `>(cmd)` via
56+
FIFO.
57+
| `posix_builtins.rs` | POSIX-defined builtins (echo, read, source,
58+
eval, set, unset, true, false, ...).
59+
| `test_command.rs` | `test` / `[` / `[[ ]]` conditionals.
60+
|===
61+
62+
=== State + reversibility
63+
64+
[cols="1,3"]
65+
|===
66+
| File | Purpose
67+
| `state.rs` | `ShellState`; operation history; undo/redo
68+
stacks; tracked variables.
69+
| `history.rs` | Command-history persistence (interactive
70+
REPL).
71+
| `audit_log.rs` | Append-only audit log for filesystem ops
72+
(JSON-line format, integrity check).
73+
| `secure_erase.rs` | RMO (Remove-Match-Obliterate) primitives;
74+
currently stubs per `CLAUDE.md`.
75+
|===
76+
77+
=== REPL + UX
78+
79+
[cols="1,3"]
80+
|===
81+
| File | Purpose
82+
| `repl.rs` | Interactive REPL loop.
83+
| `enhanced_repl.rs` | reedline-backed REPL with history search.
84+
| `highlighter.rs` | Syntax highlighting for the REPL.
85+
| `pager.rs` | Output pagination (height-threshold gated).
86+
| `help.rs` | `help` builtin; per-command documentation.
87+
| `correction.rs` | zsh-style "Did you mean?" Levenshtein
88+
suggestions.
89+
| `friendly_errors.rs` | Human-readable error formatting.
90+
| `confirmation.rs` | Y/N prompts for destructive ops.
91+
| `signals.rs` | Signal handling (SIGINT, SIGCHLD).
92+
|===
93+
94+
=== Verification + correspondence
95+
96+
[cols="1,3"]
97+
|===
98+
| File | Purpose
99+
| `proof_refs.rs` | References from runtime ops to formal
100+
proof artefacts in `../../proofs/`.
101+
| `verification.rs` | Runtime precondition checks.
102+
| `echidna_integration.rs` | Property-test registry feeding the
103+
Echidna validator (workflow gated).
104+
|===
105+
106+
=== Job control
107+
108+
[cols="1,3"]
109+
|===
110+
| File | Purpose
111+
| `job.rs` | `JobTable`; bash-style %N / %+ / %- / %prefix specs.
112+
|===
113+
114+
== Conventions used here
115+
116+
* `--safe` Rust: every public function is panic-free at the contract
117+
layer. The `.expect("TODO: handle error")` anti-pattern was swept
118+
out in commits `712e3a1..b5cc0cc` (2026-04-19); `cargo audit` and
119+
`cargo clippy` should remain clean post-sweep.
120+
* SPDX header on every source file (`PMPL-1.0-or-later`).
121+
* Tests live in `../tests/`; doctests inline.
122+
123+
== See also
124+
125+
* `../tests/README.adoc` — test-suite breakdown
126+
* `../../../proofs/` — formal specs
127+
* `../../../docs/PROOF_HOLES_AUDIT.md` — proof-debt status

‎impl/rust-cli/tests/README.adoc‎

Lines changed: 106 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,106 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= impl/rust-cli/tests/ — Test Suite
3+
4+
Cargo integration-test directory for the `vsh` Rust shell. Counts below
5+
are as-of the 2026-04-18 audit (`../../../docs/governance/CRG-AUDIT-2026-04-18.adoc`)
6+
and may have shifted slightly; current totals are visible from
7+
`cargo test`.
8+
9+
== Files
10+
11+
[cols="2,1,4"]
12+
|===
13+
| File | #[test] | Role
14+
15+
| `correspondence_tests.rs`
16+
| 35
17+
| Validates the Lean 4 → Rust correspondence (declared 28 in CLAUDE.md;
18+
35 found). Calls `vsh::commands::undo`/`redo` and walks operation
19+
history.
20+
21+
| `extended_test_tests.rs`
22+
| 55
23+
| Advanced feature coverage (heredocs, here strings, process sub,
24+
`&&`/`||` short-circuit, etc.).
25+
26+
| `integration_test.rs`
27+
| 35
28+
| End-to-end shell behaviour (glob expansion via `vsh::glob::expand_glob`,
29+
multi-stage pipelines, redirection chains).
30+
31+
| `integration_tests.rs`
32+
| 10
33+
| Edge-case integration scenarios.
34+
35+
| `lean4_proptest_correspondence.rs`
36+
| 16
37+
| Property-based Lean validation (proptest-driven).
38+
39+
| `parameter_expansion_tests.rs`
40+
| 67
41+
| `$VAR` / `${VAR:-default}` / `${VAR:?msg}` / `${#VAR}` /
42+
`${VAR:offset:length}` expansion coverage.
43+
44+
| `property_correspondence_tests.rs`
45+
| 19
46+
| Property-based Lean validation (declared 15; 19 found).
47+
48+
| `property_tests.rs`
49+
| 28
50+
| General property tests (proptest crate).
51+
52+
| `security_tests.rs`
53+
| 15
54+
| Injection prevention, path traversal, sandbox-clamp validation.
55+
56+
| `stress_tests.rs`
57+
| 11 (ignored)
58+
| Run manually with `cargo test --test stress_tests -- --ignored`.
59+
60+
| `function_and_script_tests.rs`
61+
| 24
62+
| `func() { ... }` definition + invocation.
63+
64+
| `function_control_flow_tests.rs`
65+
| 8
66+
| Control flow inside functions.
67+
68+
| `e2e_script_execution.rs`
69+
| 25
70+
| End-to-end `.sh`-style script execution.
71+
|===
72+
73+
Plus:
74+
75+
* `fixtures/` — fixture data referenced by integration tests.
76+
* `manual_redirect_test.sh`, `manual_sigint_test.sh` — interactive
77+
manual scripts (not driven by `cargo test`; kept for human regression
78+
checks of TTY-bound behaviour).
79+
80+
== Running
81+
82+
```bash
83+
cd impl/rust-cli
84+
cargo test # full suite (lib + integration + doctests)
85+
cargo test --lib # library unit tests only (~310)
86+
cargo test --test integration_test # one suite
87+
cargo test --test stress_tests -- --ignored # manually-gated stress
88+
```
89+
90+
Last full run captured this commit lineage: 703 passed / 0 failed /
91+
14 ignored (post-`.expect("TODO")` sweep, commits
92+
`712e3a1..b5cc0cc`).
93+
94+
== API notes for adding tests
95+
96+
`ShellState::new(...)` takes `&str`, not `&Path`. `undo`/`redo` are
97+
free functions in `vsh::commands`, not methods on state. `state.history`
98+
is a public field (not a method). For glob testing, call
99+
`vsh::glob::expand_glob(pattern, base_dir)` directly rather than
100+
shelling out to `ls`.
101+
102+
== See also
103+
104+
* `../src/README.adoc` — source-file map
105+
* `../../../docs/PROPERTY_TESTING.md` — proptest discipline
106+
* `../../../docs/LEAN4_RUST_CORRESPONDENCE.md` — correspondence design

0 commit comments

Comments
 (0)