Skip to content

Commit 84004cb

Browse files
chore: audit-remediation batch — panic/unsafe, CI test-gating + coverage, doc drift (#154)
## What & why Closes the short list of low-risk fixes surfaced by the repo audit. Everything Rust-side is **verified locally**: `cargo build` + `cargo clippy` clean on the touched files (modulo one pre-existing `parser.rs` `let_and_return` lint that only the newest clippy flags — not in this diff), **766 tests pass** in `impl/rust-cli` + **24** in `ffi/rust`, **0 failures**. ### 1. Panic-safety & `unsafe` (`impl/rust-cli/src`, `ffi/rust/src`) - Removed the **3 startup panics**: `enhanced_repl.rs` (history file, Ctrl-C handler) and `repl.rs` (Ctrl-C handler) now **degrade gracefully** — warn + fall back to in-memory history / default Ctrl-C behaviour — instead of `.expect()`-aborting the shell on a degraded environment (e.g. read-only `$HOME`). - Added `// SAFETY:` comments to the **4 previously-undocumented `unsafe` libc blocks** (`audit.rs` `getuid`; `operations.rs` + `commands.rs` ×2 `chown`). Also clears the matching Hypatia `code_safety` findings. ### 2. CI (`rust-cli.yml`) - **Gate the full suite**: the `test` job previously ran only 3 of ~18 suites (`--lib`, one integration suite, `property_tests`). Now runs `cargo test` (all suites + doctests) plus a dedicated `ffi/rust` step — so every test that passes locally is enforced on push. - **New `coverage` job** using `cargo-llvm-cov` (self-contained; all actions SHA-pinned to the versions already used in the repo). Runs the suite under instrumentation, writes the summary to the job summary, and uploads `lcov.info`. **Measured/reported, not a hard gate** — closes the "coverage is unmeasured" gap without a brittle threshold. ### 3. Docs / metadata drift - `security.txt`: fixed the **RFC 9116 §2.5.3 `Canonical`** URL — was a non-served `github.com/.../.well-known/...` blob path; now the served `raw.githubusercontent.com` location (Pages only publishes the README, so `.well-known` isn't served there). - `README.adoc`: added a **"Run the shell (Rust CLI)"** section as the *first* install step — the front door previously only documented compiling the six proof systems, not how to `cargo build`/run the actual shell. - `0-AI-MANIFEST.a2ml` + `6a2/STATE.a2ml`: **reconciled counts to measured reality** — `idris2-holes 22 → 0` (closed in #152), `tests-passing 757 → 766`, source files `32 → 33`, LoC `21331 → 22574`, `last-updated → 2026-07-01`. The manifest had been contradicting its own authoritative `docs/PROOF_HOLES_AUDIT.md`. ## Verification ``` cd impl/rust-cli && cargo build && cargo test # 766 pass / 0 fail / 14 ignored cd ffi/rust && cargo test # 24 pass / 0 fail python3 -c "import glob,yaml; [yaml.safe_load(open(f)) for f in glob.glob('.github/workflows/*.yml')]" # all parse ``` ## Not included (deliberately out of scope) The larger audit items — missing marketer/journalist + lay-person docs and a real audience-segmented wiki, the ABI/FFI consolidation (C NIF / Rust `ffi/rust` / ReScript MCP not being Zig), the absent launcher, and the RSR template/`RSR_COMPLIANCE.md` inflation — are each their own scoped pass, not smuggled into this hygiene batch. 🤖 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 9b11d08 commit 84004cb

10 files changed

Lines changed: 123 additions & 31 deletions

File tree

.github/workflows/rust-cli.yml

Lines changed: 46 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -42,17 +42,13 @@ jobs:
4242
working-directory: impl/rust-cli
4343
run: cargo clippy --all-targets --all-features -- -D warnings
4444

45-
- name: Run unit tests
45+
- name: Run all tests (unit + every integration suite + doctests)
4646
working-directory: impl/rust-cli
47-
run: cargo test --lib --verbose
47+
run: cargo test --verbose
4848

49-
- name: Run integration tests
50-
working-directory: impl/rust-cli
51-
run: cargo test --test integration_test --verbose
52-
53-
- name: Run property tests
54-
working-directory: impl/rust-cli
55-
run: cargo test --test property_tests --verbose
49+
- name: Run ffi/rust tests
50+
working-directory: ffi/rust
51+
run: cargo test --verbose
5652

5753
- name: Build release binary
5854
working-directory: impl/rust-cli
@@ -98,3 +94,44 @@ jobs:
9894
SORRY_COUNT=$(grep -r "sorry" *.lean | wc -l || echo "0")
9995
echo "Found $SORRY_COUNT sorry placeholders in proofs"
10096
# Note: Some sorry placeholders are expected during development
97+
98+
coverage:
99+
name: Code coverage (llvm-cov)
100+
runs-on: ubuntu-latest
101+
timeout-minutes: 30
102+
steps:
103+
- name: Checkout code
104+
uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v4
105+
106+
- name: Install Rust toolchain
107+
uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b # stable
108+
with:
109+
components: llvm-tools-preview
110+
111+
- name: Cache Rust dependencies
112+
uses: Swatinem/rust-cache@baf1a810e98b6a3001d0d7234864ed75a17c42fb # v2
113+
with:
114+
workspaces: impl/rust-cli
115+
116+
- name: Install cargo-llvm-cov
117+
run: cargo install cargo-llvm-cov --locked
118+
119+
- name: Measure coverage (impl/rust-cli)
120+
working-directory: impl/rust-cli
121+
run: |
122+
# Run the full suite once under instrumentation, then emit reports.
123+
# Measured and surfaced as a regression signal — not a hard gate.
124+
cargo llvm-cov --no-report
125+
cargo llvm-cov report --lcov --output-path lcov.info
126+
{
127+
echo '### Coverage — impl/rust-cli'
128+
echo '```'
129+
cargo llvm-cov report --summary-only
130+
echo '```'
131+
} >> "$GITHUB_STEP_SUMMARY"
132+
133+
- name: Upload coverage (lcov)
134+
uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7
135+
with:
136+
name: coverage-lcov
137+
path: impl/rust-cli/lcov.info

.machine_readable/6a2/STATE.a2ml

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
[metadata]
77
project = "valence-shell"
88
version = "0.9.0"
9-
last-updated = "2026-06-02"
9+
last-updated = "2026-07-01"
1010
status = "active"
1111

1212
[project-context]
@@ -17,6 +17,23 @@ bridge-status = "documentation-and-orientation-only (echo-types + ochrance; NOT
1717
bridge-doc = "docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc"
1818
bridge-a2ml = ".machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml"
1919

20+
[recent-work-2026-07-01]
21+
session = "2026-07-01 — Idris2 proof-hole closure at the root + CI hardening + drift reconcile"
22+
focus = "Close all Idris2 ABI proof holes; harden CI workflows; reconcile machine-readable counts to measured reality"
23+
prs-merged-2026-07-01 = [
24+
"#152 proofs(idris2): close ALL proof holes — 17 -> 0, zero new axioms, builds under --total (root of #151)",
25+
"#153 ci: workflow hardening — timeout caps, pinned+SHA256-verified elan, CodeQL js/ts -> actions, presence-gate instant-sync dispatch"
26+
]
27+
idris2-holes = 0
28+
idris2-axioms = 2
29+
tests-passing = 766
30+
tests-ignored = 14
31+
tests-failing = 0
32+
ffi-rust-tests = 24
33+
rust-source-files = 33
34+
rust-loc = 22574
35+
note = "idris2-holes 22 -> 0 (via #152) supersedes the 2026-06-02 tallies below; older dated test totals (703/757/764) are historical snapshots, not current claims."
36+
2037
[recent-work-2026-06-02]
2138
session = "2026-06-02 morning + afternoon sweep — inbox cleanup + root-cause main fixes"
2239
focus = "Clear governance reds inherited by 4 open PRs; LICENSE SPDX prepend; annotate 4 admits in rmo_operations.v; Idris2 0.8.0 keyword/parse fixes"

.well-known/security.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,5 +5,5 @@
55
Contact: mailto:j.d.a.jewell@open.ac.uk
66
Expires: 2027-03-08T23:59:59.000Z
77
Preferred-Languages: en
8-
Canonical: https://github.com/hyperpolymath/valence-shell/.well-known/security.txt
8+
Canonical: https://raw.githubusercontent.com/hyperpolymath/valence-shell/main/.well-known/security.txt
99
Policy: https://github.com/hyperpolymath/valence-shell/blob/main/SECURITY.md

0-AI-MANIFEST.a2ml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ project = "valence-shell"
1010
version = "0.9.0"
1111
status = "Advanced research prototype — NOT production-ready"
1212
license = "MPL-2.0"
13-
last-updated = "2026-06-02"
13+
last-updated = "2026-07-01"
1414

1515
# What this project IS — one-line summary; for the full statement read
1616
# .machine_readable/INTENT.contractile (the load-bearing artefact).
@@ -38,16 +38,16 @@ deep-audit-log-dir = "docs/audits/"
3838
latest-deep-audit = "docs/audits/2026-06-01-deep-audit.adoc"
3939

4040
[counts-as-of-last-audit]
41-
# Per docs/audits/2026-06-01-deep-audit.adoc + issue #42 + 2026-06-02 sweep.
41+
# Per docs/audits/2026-06-01-deep-audit.adoc + issue #42 + measured 2026-07-01.
4242
theorem-candidates = 478
4343
proof-systems = 6
4444
coq-admits-remaining = 3 # #56 + #57 + #58 (3 surfaced post-#55)
4545
coq-axioms-justified = 1 # is_empty_dir_dec
46-
idris2-holes-remaining = 22 # was 21 + 8 partial; now 22 holes + 0 partial post-PRs #105/#108/#109/#115
46+
idris2-holes-remaining = 0 # all closed 2026-07-01 (#152); builds under --total, 2 registered primitive-eq axioms
4747
idris2-partial-markers = 0 # cleared 2026-06-02
48-
rust-source-files = 32
49-
rust-loc = 21331
50-
tests-passing = 757 # +21 via PR #72 (2026-06-01)
48+
rust-source-files = 33 # measured 2026-07-01 (impl/rust-cli/src)
49+
rust-loc = 22574 # measured 2026-07-01 (impl/rust-cli/src)
50+
tests-passing = 766 # measured 2026-07-01 (impl/rust-cli); +24 in ffi/rust
5151
tests-ignored = 14
5252
tests-failing = 0
5353
fuzz-targets = 7

README.adoc

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,24 @@ Nix (recommended)
117117

118118
=== Installation
119119

120-
==== With Nix (Recommended)
120+
==== Run the shell (Rust CLI) — the primary deliverable
121+
122+
The interactive shell lives in `impl/rust-cli/` and only needs a Rust toolchain
123+
(1.88+). The proof systems below are optional — they are needed only to
124+
re-check the formal proofs, not to build or run the shell.
125+
126+
[source,bash]
127+
----
128+
git clone https://github.com/Hyperpolymath/valence-shell.git
129+
cd valence-shell/impl/rust-cli
130+
131+
cargo build --release # builds the `vsh` binary
132+
cargo run # start the interactive shell
133+
./target/release/vsh --version # or run the release binary directly
134+
cargo test # run the test suite (766 passing)
135+
----
136+
137+
==== With Nix (proof systems)
121138

122139
[source,bash]
123140
----

ffi/rust/src/audit.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,8 @@ impl AuditLog {
134134
hash: String::new(),
135135
pid: std::process::id(),
136136
#[cfg(unix)]
137+
// SAFETY: `getuid` takes no arguments, cannot fail, and only reads
138+
// the calling process's real UID — no pointers or invariants.
137139
uid: unsafe { libc::getuid() },
138140
result,
139141
proof_ref: proof_ref.map(String::from),

ffi/rust/src/operations.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -271,6 +271,10 @@ pub fn chown(path: &Path, uid: Option<u32>, gid: Option<u32>) -> FfiResult<()> {
271271
let uid = uid.map(|u| u as libc::uid_t).unwrap_or(u32::MAX as libc::uid_t);
272272
let gid = gid.map(|g| g as libc::gid_t).unwrap_or(u32::MAX as libc::gid_t);
273273

274+
// SAFETY: `path_cstr` is a valid, NUL-terminated `CString` that outlives
275+
// this call, so `as_ptr()` is a live pointer for the call's duration;
276+
// `uid`/`gid` are plain integers. `chown` only borrows the pointer and
277+
// returns a status code we check below.
274278
let result = unsafe { libc::chown(path_cstr.as_ptr(), uid, gid) };
275279

276280
if result != 0 {

impl/rust-cli/src/commands.rs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1000,6 +1000,10 @@ pub fn undo(state: &mut ShellState, count: usize, verbose: bool) -> Result<()> {
10001000
let gid: u32 = parts[1].parse().context("Invalid gid")?;
10011001
let c_path = std::ffi::CString::new(path.to_str().context("Invalid path")?)
10021002
.context("Path contains null bytes")?;
1003+
// SAFETY: `c_path` is a valid, NUL-terminated `CString` that
1004+
// outlives the call, so `as_ptr()` is live; `uid`/`gid` are
1005+
// plain integers. `chown` only borrows the pointer and
1006+
// returns a status code we check below.
10031007
let ret = unsafe { libc::chown(c_path.as_ptr(), uid, gid) };
10041008
if ret != 0 {
10051009
let err = std::io::Error::last_os_error();
@@ -1523,6 +1527,11 @@ pub fn rollback_transaction(state: &mut ShellState) -> Result<()> {
15231527
let gid: u32 = parts[1].parse().context("Invalid gid")?;
15241528
let c_path = std::ffi::CString::new(path.to_str().unwrap_or(""))
15251529
.context("Path contains null bytes")?;
1530+
// SAFETY: `c_path` is a valid, NUL-terminated
1531+
// `CString` that outlives the call, so `as_ptr()`
1532+
// is live; `uid`/`gid` are plain integers. `chown`
1533+
// only borrows the pointer and returns a status
1534+
// code we check below.
15261535
let ret = unsafe { libc::chown(c_path.as_ptr(), uid, gid) };
15271536
if ret != 0 {
15281537
Err(anyhow::anyhow!(

impl/rust-cli/src/enhanced_repl.rs

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -246,10 +246,6 @@ pub fn run(state: &mut ShellState) -> Result<()> {
246246
.unwrap_or_else(|| PathBuf::from("/tmp"))
247247
.join(".vsh_history");
248248

249-
let history = Box::new(
250-
FileBackedHistory::with_file(1000, history_file).expect("Failed to initialize history"),
251-
);
252-
253249
// Set up completion menu
254250
let completion_menu = Box::new(ColumnarMenu::default().with_name("completion_menu"));
255251

@@ -268,7 +264,6 @@ pub fn run(state: &mut ShellState) -> Result<()> {
268264

269265
// Create reedline instance
270266
let mut line_editor = Reedline::create()
271-
.with_history(history)
272267
.with_completer(Box::new(VshCompleter))
273268
.with_highlighter(Box::new(VshHighlighter::new()))
274269
.with_hinter(Box::new(
@@ -278,11 +273,20 @@ pub fn run(state: &mut ShellState) -> Result<()> {
278273
.with_edit_mode(edit_mode)
279274
.with_menu(ReedlineMenu::EngineCompleter(completion_menu));
280275

281-
// Install SIGINT handler
282-
ctrlc::set_handler(move || {
276+
// Attach a file-backed history if it opens; otherwise fall back to
277+
// reedline's in-memory history instead of aborting the shell.
278+
match FileBackedHistory::with_file(1000, history_file) {
279+
Ok(h) => line_editor = line_editor.with_history(Box::new(h)),
280+
Err(e) => eprintln!("vsh: warning: history disabled ({e}); using in-memory history"),
281+
}
282+
283+
// Install SIGINT handler; a failure only means Ctrl-C keeps its default
284+
// behaviour, so warn and continue rather than panicking.
285+
if let Err(e) = ctrlc::set_handler(move || {
283286
signals::request_interrupt();
284-
})
285-
.expect("Error setting Ctrl-C handler");
287+
}) {
288+
eprintln!("vsh: warning: could not install Ctrl-C handler ({e})");
289+
}
286290

287291
let mut accumulated_input = String::new();
288292

impl/rust-cli/src/repl.rs

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -43,11 +43,13 @@ use crate::state::ShellState;
4343
/// # Ok::<(), anyhow::Error>(())
4444
/// ```
4545
pub fn run(state: &mut ShellState) -> Result<()> {
46-
// Install SIGINT handler for graceful Ctrl+C handling
47-
ctrlc::set_handler(move || {
46+
// Install SIGINT handler for graceful Ctrl+C handling; a failure only
47+
// means Ctrl-C keeps its default behaviour, so warn and continue.
48+
if let Err(e) = ctrlc::set_handler(move || {
4849
signals::request_interrupt();
49-
})
50-
.expect("Error setting Ctrl-C handler");
50+
}) {
51+
eprintln!("vsh: warning: could not install Ctrl-C handler ({e})");
52+
}
5153

5254
let stdin = io::stdin();
5355
let mut stdout = io::stdout();

0 commit comments

Comments
 (0)