Skip to content

ROADMAP.adoc

Latest commit

 

History

History
139 lines (115 loc) · 6.5 KB

ROADMAP.adoc

File metadata and controls

139 lines (115 loc) · 6.5 KB
Raw

Valence Shell Roadmap

Table of Contents

Current Status

v0.9.0 (advanced research prototype, ~74% complete per .machine_readable/6a2/STATE.a2ml).

The Rust CLI in impl/rust-cli/ is a functional interactive shell with reversible filesystem operations, transaction grouping, and proof-annotated dry runs. It is NOT production-ready and NOT a drop-in replacement for bash/zsh.

For the full honest status see CLAUDE.md; for caveats per claim see EXPLAINME.adoc; for proof-debt see docs/PROOF_HOLES_AUDIT.md.

Last refreshed: 2026-06-02 (post-merge sweep: PRs #105 #106 #108 #109 — closes #60 / #61 / #70 / #89; PR #107 dropped codeql.yml).

v0.9.x — Stabilisation (D → C per CRG v2.0)

Tracked against docs/governance/CRG-AUDIT-2026-04-18.adoc. Goal: green CI on rust-cli.yml, dogfood evidence, structural compliance.

  • ❏ Revert the remaining .expect("TODO: handle error") sites in impl/rust-cli/src/. Batches 1-3 cleared 136 of ~530 (commits 712e3a1, 962da88, f045ced). Remaining concentrated in parser.rs (116), commands.rs (66), arith.rs (55), state.rs (35) — each warrants its own session. Tracked under #41 (seam walk).

  • ✓ Resolved 2026-06-01 (#55, PR #55): The Coq admit. in proofs/coq/filesystem_composition.v single_op_reversible was closed; verify-proofs CI job re-enabled with Print Assumptions wiring. Three new admits surfaced and were filed as #56/#57/#58.

  • ❏ Turn rust-cli.yml green after the .expect sweep completes.

  • ✓ Resolved 2026-06-01 (#49, PR #55): validation.yml verify-proofs re-enabled; build oracle now red-on-real-failure rather than silently disabled. Five cascading Coq build errors fixed in the same PR.

  • ❏ Per-directory README coverage 23% → ~90% (17 subtrees missing, enumerated in the audit).

  • ❏ Add [dogfooding-status] to STATE.a2ml with concrete daily-use entries.

  • ❏ Add 3+ ADRs to META.a2ml (six-system proof stack, Rust as primary implementation, property-testing as correspondence-gap mitigation) and populate [development-practices].

  • ✓ Resolved 2026-04-19: impl/rust-ffi/ deleted; ffi/rust/ is canonical (superset, includes verification.rs, matches CLAUDE.md ABI/FFI standard ffi/<lang>/). 7 sibling files were byte-identical; lib.rs differed only by the pub mod verification; export and richer doc-comment proof references. No build consumers.

  • ❏ Complete contractile six-verb layout: create intend/ (absorbs former lust/, already removed in commit a48a1dc), adjust/; relocate k9 out of contractiles/ per ADR-001 (k9 is svc, not a contractile).

  • [~] Close docs/reports/audit/audit-2026-04-04.md residuals:

    • ❏ Re-author 47 spoofed git commits (Test <test@example.com> → canonical attribution). Requires history rewrite + force-push; needs explicit human authorization before execution.

    • ❏ Wire Echidna CI integration for automated property-based verification.

    • ✓ Remove dead code (lean_ffi.rs, daemon_client.rs) — closed 2026-02-12 in commit 5802dc9 (predates the 2026-04-18 audit; the audit’s residual claim was stale). Phase 4C design docs under impl/rust-cli/docs/ carry archival banners noting the removal.

v0.9.x — Closed-issue housekeeping (2026-06-01)

The following Phase-0 / housekeeping issues closed on 2026-06-01; their remediation work is rolled into the historical record above.

  • ✓ #33 — security: 8 Critical/High panic-attack findings (Track C). Resolved by PR #52 (panic-attack triage); see audits/assail-classifications.a2ml for retained suppressions.

  • ✓ #44 — Docs max-out vs standards. Resolved by PR #53; INTENT.contractile + methodology.a2ml placeholders filled.

  • ✓ #46 — CI/CD reds on main (6 distinct workflows). Resolved by PR #54; 8 governance workflow fixes landed.

  • ✓ #49 — Re-enable verify-proofs CI job + 5 Coq build errors. Resolved by PR #55; 22 Coq errors closed and Print Assumptions wired.

Open follow-ups: #41 (seam walk: panics + TODOs), #42 (proof inventory), #43 (test+bench expansion), #45 (filesystem-theory gap), #51 (L3 echo integration), #56/#57/#58 (the three admits surfaced by #55).

v0.10.x — POSIX Coverage

Most critical missing POSIX features, ranked by impact (per CLAUDE.md and docs/POSIX_COMPLIANCE.md):

  1. Shell functions (func() { …​ } syntax) — blocks modular scripts.

  2. Shell script execution (.sh files, shebang handling).

  3. Word splitting ($IFS) — unquoted variable expansions are not split.

  4. Tilde expansion beyond ~/ in cd.

  5. trap — cannot handle signals in scripts.

  6. alias — no command aliases.

  7. SIGCHLD / Ctrl+Z — job control incomplete.

docs/POSIX_COMPLIANCE.md carries the full M1-M11 milestone tracker; M1-M9 complete, M10-M11 partial.

v1.0.0 — Production Readiness Gate

Hard requirements before any v1.0 claim:

  • ❏ Mechanized Lean → Rust correspondence (currently property testing only, ~85% confidence).

  • ✓ Close all real gaps in docs/PROOF_HOLES_AUDIT.md — DONE (re-verified 2026-07-16 under Coq 8.18.0): 0 real gaps; 1 justified axiom (is_empty_dir_dec) + 1 structural (funext) remain.

  • ❏ CRG v2.0 grade B: 6+ diverse external targets, issues fed back. See audit === External validation section for the proposed diverse-6 shape.

  • [~] RMO (Remove-Match-Obliterate): file-level obliterate implemented and wired (best-effort 3-pass overwrite + unlink + append-only audit residue). Remaining for full GDPR: hardware erase for CoW/SSD, audit HMAC signing, recursive-dir hardening. Tracked under #41.

  • ❏ Echidna integration for automated property-based verification.

v2.0 — Idris2 Extraction Path

Begin the Idris2 extraction path (per CLAUDE.md "This Month" plan).

  • ❏ Populate src/abi/ Idris2 ABI definitions beyond the current 3-file stubs (Types.idr, Layout.idr, Foreign.idr).

  • ❏ Wire Zig FFI: ffi/zig/ builds but is not integrated with the Rust CLI; impl/zig/ targets ~5ms cold start.

  • ❏ BEAM daemon implementation (planned, not built; Elixir NIF build currently broken, low priority).

Operating Notes

  • This roadmap supersedes the prior rsr-template stub. Authoritative next-step detail lives here; CLAUDE.md retains the honest-status narrative.

  • All milestone items are grep-verifiable against on-disk artefacts.

  • Cadence: edit ends with an Agda/Coq/Lean compile or cargo build
    cargo test; outcomes captured in commit messages.