Skip to content

Commit fc3313b

Browse files
hyperpolymathclaude
andcommitted
Docs hygiene: anchor version, alkahest email, populate ROADMAP
Closes three of the small drift findings from CRG-AUDIT-2026-04-18: * `.machine_readable/anchors/ANCHOR.a2ml` — version bumped from the Sonnet-era "1.0.0" relic to the actual "0.9.0" matching STATE.a2ml. The anchor is the canonical-authority file; carrying the inflated version was the same drift the 2026-02-12 Opus audit cleaned in README/main.rs but missed here. * `alkahest-shell-transmuter/README.adoc` — author email `hyperpolymath@example.com` placeholder replaced with `j.d.a.jewell@open.ac.uk` (canonical attribution per the project author rules: noreply for git metadata, real email for docs). * `ROADMAP.adoc` — replaces the 22-line rsr-template stub with a substantive roadmap ported from CLAUDE.md. Sections: v0.9.x Stabilisation (D→C closure list against the 2026-04-18 audit), v0.10.x POSIX coverage, v1.0.0 production gate, v2.0 Idris2 extraction path. All milestone items grep-verifiable against on-disk artefacts. References the audit, PROOF_HOLES_AUDIT, POSIX_COMPLIANCE.md, and the audit-2026-04-04 residuals list. Two related items deliberately not bundled here: * `lust/` rename: already done in commits a48a1dc + 8b0a56a (the audit was stale on this point — neither root `contractiles/` nor `.machine_readable/contractiles/` carries `lust/` any more). Completing the six-verb layout (creating `intend/`, `adjust/`, relocating k9 to svc/) is a separate larger restructure. * `.expect("TODO: handle error")` sweep: tracked in batches 1-3 (commits 712e3a1, 962da88, f045ced); 136/~530 cleared. Continues in subsequent commits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent f045ced commit fc3313b

3 files changed

Lines changed: 92 additions & 14 deletions

File tree

.machine_readable/anchors/ANCHOR.a2ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
# This is the canonical authority for the valence-shell repository.
33

44
id: "org.hyperpolymath.valence-shell"
5-
version: "1.0.0"
5+
version: "0.9.0"
66
clade: "unknown"
77
status: "active"
88

ROADMAP.adoc

Lines changed: 90 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,100 @@
11
// SPDX-License-Identifier: PMPL-1.0-or-later
22
= Valence Shell Roadmap
3+
:toc:
34

45
== Current Status
56

6-
Initial development phase.
7+
v0.9.0 (advanced research prototype, ~74% complete per
8+
`.machine_readable/6a2/STATE.a2ml`).
79

8-
== Milestones
10+
The Rust CLI in `impl/rust-cli/` is a functional interactive shell with
11+
reversible filesystem operations, transaction grouping, and
12+
proof-annotated dry runs. It is NOT production-ready and NOT a drop-in
13+
replacement for bash/zsh.
914

10-
=== v0.1.0 - Foundation
11-
* [ ] Core functionality
12-
* [ ] Basic documentation
13-
* [ ] CI/CD pipeline
15+
For the full honest status see `CLAUDE.md`; for caveats per claim see
16+
`EXPLAINME.adoc`; for proof-debt see `docs/PROOF_HOLES_AUDIT.md`.
1417

15-
=== v1.0.0 - Stable Release
16-
* [ ] Full feature set
17-
* [ ] Comprehensive tests
18-
* [ ] Production ready
18+
== v0.9.x — Stabilisation (D → C per CRG v2.0)
1919

20-
== Future Directions
20+
Tracked against `docs/governance/CRG-AUDIT-2026-04-18.adoc`. Goal: green
21+
CI on `rust-cli.yml`, dogfood evidence, structural compliance.
2122

22-
_To be determined based on community feedback._
23+
* [ ] Revert the remaining `.expect("TODO: handle error")` sites in
24+
`impl/rust-cli/src/`. Batches 1-3 cleared 136 of ~530 (commits
25+
`712e3a1`, `962da88`, `f045ced`). Remaining concentrated in
26+
`parser.rs` (116), `commands.rs` (66), `arith.rs` (55), `state.rs`
27+
(35) — each warrants its own session.
28+
* [ ] Close the Coq `admit.` in `proofs/coq/filesystem_composition.v:199`
29+
(`single_op_reversible` `OpRmdir` branch) or update
30+
`[coq-proof-status] admitted = 1` with full justification.
31+
* [ ] Turn `rust-cli.yml` green after the `.expect` sweep completes.
32+
* [ ] Enable `validation.yml verify-proofs` job (currently `if: false`);
33+
start with Lean 4 via `lake build`, then phase in Coq/Agda/Isabelle/Z3.
34+
* [ ] Per-directory README coverage 23% → ~90% (17 subtrees missing,
35+
enumerated in the audit).
36+
* [ ] Add `[dogfooding-status]` to STATE.a2ml with concrete daily-use
37+
entries.
38+
* [ ] Add 3+ ADRs to META.a2ml (six-system proof stack, Rust as primary
39+
implementation, property-testing as correspondence-gap mitigation) and
40+
populate `[development-practices]`.
41+
* [ ] Resolve `impl/rust-ffi/` ↔ `ffi/rust/` duplicate tree (~50
42+
`.expect("TODO")` sites in each); decide which is canonical.
43+
* [ ] Complete contractile six-verb layout: create `intend/` (absorbs
44+
former `lust/`, already removed in commit `a48a1dc`), `adjust/`;
45+
relocate `k9` out of `contractiles/` per ADR-001 (k9 is svc, not a
46+
contractile).
47+
* [ ] Close `docs/reports/audit/audit-2026-04-04.md` residuals: re-author
48+
47 spoofed git commits, wire Echidna CI, remove dead code
49+
(`lean_ffi.rs`, `daemon_client.rs`).
50+
51+
== v0.10.x — POSIX Coverage
52+
53+
Most critical missing POSIX features, ranked by impact (per CLAUDE.md
54+
and `docs/POSIX_COMPLIANCE.md`):
55+
56+
. Shell functions (`func() { ... }` syntax) — blocks modular scripts.
57+
. Shell script execution (`.sh` files, shebang handling).
58+
. Word splitting (`$IFS`) — unquoted variable expansions are not split.
59+
. Tilde expansion beyond `~/` in `cd`.
60+
. `trap` — cannot handle signals in scripts.
61+
. `alias` — no command aliases.
62+
. SIGCHLD / Ctrl+Z — job control incomplete.
63+
64+
`docs/POSIX_COMPLIANCE.md` carries the full M1-M11 milestone tracker;
65+
M1-M9 complete, M10-M11 partial.
66+
67+
== v1.0.0 — Production Readiness Gate
68+
69+
Hard requirements before any v1.0 claim:
70+
71+
* [ ] Mechanized Lean → Rust correspondence (currently property testing
72+
only, ~85% confidence).
73+
* [ ] Close all real gaps in `docs/PROOF_HOLES_AUDIT.md` (post-2026-04
74+
sweep: 1 real gap, 1 justified axiom, 1 structural).
75+
* [ ] CRG v2.0 grade B: 6+ diverse external targets, issues fed back.
76+
See audit `=== External validation` section for the proposed diverse-6
77+
shape.
78+
* [ ] Complete RMO (Remove-Match-Obliterate) implementation for GDPR
79+
compliance — currently stubs only.
80+
* [ ] Echidna integration for automated property-based verification.
81+
82+
== v2.0 — Idris2 Extraction Path
83+
84+
Begin the Idris2 extraction path (per CLAUDE.md "This Month" plan).
85+
86+
* [ ] Populate `src/abi/` Idris2 ABI definitions beyond the current
87+
3-file stubs (`Types.idr`, `Layout.idr`, `Foreign.idr`).
88+
* [ ] Wire Zig FFI: `ffi/zig/` builds but is not integrated with the
89+
Rust CLI; `impl/zig/` targets ~5ms cold start.
90+
* [ ] BEAM daemon implementation (planned, not built; Elixir NIF build
91+
currently broken, low priority).
92+
93+
== Operating Notes
94+
95+
* This roadmap supersedes the prior rsr-template stub. Authoritative
96+
next-step detail lives here; CLAUDE.md retains the honest-status
97+
narrative.
98+
* All milestone items are grep-verifiable against on-disk artefacts.
99+
* Cadence: edit ends with an Agda/Coq/Lean compile or `cargo build` +
100+
`cargo test`; outcomes captured in commit messages.

alkahest-shell-transmuter/README.adoc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ image:https://img.shields.io/badge/License-PMPL--1.0-blue.svg[License: PMPL-1.0,
55

66

77

8-
Jonathan D.A. Jewell <hyperpolymath@example.com>
8+
Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
99
v0.1.0-alpha, 2025-12-19
1010
:toc: left
1111
:sectnums:

0 commit comments

Comments
 (0)