= Valence Shell (vsh) image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssourcesecurity[OpenSSF Best Practices,link=“https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/valence-shell”]

image:https://img.shields.io/badge/License-MPL–2.0-blue[License: MPL-2.0,link=“https://www.mozilla.org/MPL/2.0/”] // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell

:toc: macro :toclevels: 3 :icons: font :source-highlighter: rouge

image:https://img.shields.io/badge/RSR-PLATINUM-blueviolet[RSR Compliance] image:https://img.shields.io/badge/Proofs-478%20candidates-brightgreen[Formal Proofs] image:https://img.shields.io/badge/Systems-6%20proof%20assistants-orange[Proof Systems]

Research shell exploring formally specified reversible operations and the MAA (Mutually Assured Accountability) Framework.

Selected abstract filesystem properties have machine-checked proofs. The Rust implementation is connected to those models by tests, not by a mechanised refinement proof; neither the proofs nor the deletion command establish legal or deployment-wide GDPR compliance.

[IMPORTANT]

Current Status: v0.9.0 — Advanced Research Prototype + NOT production-ready. Functional shell with formally proven reversibility, but POSIX compliance is incomplete and Lean→Rust correspondence is testing-based (~85% confidence), not mechanized. + Progress: ~78% of full roadmap complete, 794 tests passing (0 failures, 14 ignored) + See <<_verification_status>> and link:CHANGELOG.adoc[CHANGELOG] for details. ====

toc::[]

== Overview

Valence Shell is a formally verified shell with proven reversibility guarantees. Unlike traditional shells where “undo” is a best-effort feature, vsh provides mathematical proofs that operations can be reversed.

=== Key Features

= Features

== Formal Verification * [x] Formally Proven Reversibility: rmdir(mkdir(p, fs)) = fs * [x] Polyglot Verification: 6 proof systems (Coq, Lean 4, Agda, Isabelle, Mizar, Z3) * [x] ~478 Theorem Candidates: Proven across different logical foundations (0 real gaps; 1 justified axiom + 1 structural axiom remain — see docs/PROOF_HOLES_AUDIT.md) * [x] Content Operations: File read/write with proven reversibility * [x] MAA Framework: Mutually Assured Accountability with audit trails

== Shell Features (v0.9.0) * [x] Unix Pipelines: Multi-stage pipelines (cmd1 | cmd2 | cmd3) * [x] I/O Redirections: All POSIX redirections (>, >>, <, 2>, 2>>, &>, 2>&1) * [x] Process Substitution: <(cmd) and >(cmd) with FIFO implementation * [x] Arithmetic Expansion: $expr with full operator support * [x] Here Documents: <<DELIMITER, <←DELIMITER, <<<word * [x] Job Control: Background jobs, fg, bg, kill, job specifications * [x] Shell Variables: $VAR, export, assignment, expansion * [~] RMO: obliterate implements best-effort 3-pass file overwrite + unlink + an unsigned audit residue; CoW filesystems, SSD remapping, snapshots, replicas, crash timing, and legal compliance remain outside that guarantee. Audit-log HMAC chaining is available when a key is supplied, but RMO does not yet provision one. See link:docs/RMO-DURABILITY-BOUNDARY.adoc[the exact boundary]. * [x] Syntax Highlighting: Real-time color-coded REPL * [x] Command Correction: Intelligent typo suggestions * [x] Friendly Errors: fish-style helpful error messages * [x] Smart Pager: Auto-paging for long output * [x] 3-Tier Help: Quick/verbose/man page documentation * [x] 794 Tests Passing: Unit, correspondence, integration, property, security, doctests (0 failures, 14 ignored)

== Implementation * [x] Advanced-prototype Rust CLI: 95% feature-complete shell (NOT production-ready — see <<_verification_status>>) * [x] Offline-First: All proofs verifiable air-gapped * [x] Fuzzing: 7 fuzz targets with cargo-fuzz integration (parser, arith, job-spec, signal-parse, path-ops, glob-expansion, state-machine)

=== What Makes This Different?

[cols=“1,2,2”] |=== |Feature |Traditional Shells |Valence Shell

|Undo |Best-effort, manual |Mathematically proven correct

|Verification |Testing only |Formal proofs in 6 systems

|Accountability |Logs (can be tampered) |Optional HMAC-chained audit log; external anchoring remains future work

|Trust |“Hope it works” |Explicitly scoped model-level guarantees |===

== Quick Start

=== Prerequisites

Minimum (to run demonstrations): [source,bash] —- # One of: OCaml 5.0+ Elixir 1.15+ Bash 4.0+ —-

Full Development (to modify proofs): [source,bash] —- Coq 8.18+ Lean 4.3+ Agda 2.6.4+ Isabelle/HOL 2024 Z3 4.12+ Just (command runner) Nix (recommended) —-

=== Installation

==== Run the shell (Rust CLI) — the primary deliverable

The interactive shell lives in impl/rust-cli/ and only needs a Rust toolchain (1.88+). The proof systems below are optional — they are needed only to re-check the formal proofs, not to build or run the shell.

[source,bash]

git clone https://github.com/Hyperpolymath/valence-shell.git cd valence-shell/impl/rust-cli

cargo build –release # builds the vsh binary cargo run # start the interactive shell ./target/release/vsh –version # or run the release binary directly cargo test # run the test suite (766 passing) —-

==== With Nix (proof systems)

[source,bash]

Clone repository

git clone https://github.com/Hyperpolymath/valence-shell.git cd valence-shell

Enter development environment

nix develop

Build all proof systems

just build-all

Run comprehensive demonstration

just demo

==== With Containers

[source,bash]

Build container

podman build -t valence-shell .

Run verification

podman run valence-shell just verify-proofs

Interactive shell

podman run -it valence-shell bash

==== Manual Setup

[source,bash]

Install proof assistants (per their documentation)

Then:

git clone https://github.com/Hyperpolymath/valence-shell.git cd valence-shell

Build Coq proofs

just build-coq

Build Lean 4 proofs

just build-lean4

Run tests

just test-all

=== Basic Usage

[source,bash]

Verify all proofs compile

just verify-proofs

Run demonstration showing all proven theorems

./scripts/demo_verified_operations.sh

Build specific proof system

just build-coq # Coq proofs just build-lean4 # Lean 4 proofs just build-agda # Agda proofs just build-isabelle # Isabelle proofs

Show available commands

just –list

== What’s Proven?

=== Core Theorems (All 5 Manual Proof Systems)

[source,coq]

Theorem mkdir_rmdir_reversible : forall p fs, mkdir_precondition p fs -> rmdir p (mkdir p fs) = fs.

Theorem create_delete_file_reversible : forall p fs, create_file_precondition p fs -> delete_file p (create_file p fs) = fs.

Theorem write_file_reversible : forall p fs old_content new_content, write_file_precondition p fs -> read_file p fs = Some old_content -> write_file p old_content (write_file p new_content fs) = fs. —-

=== Composition (Proven in 5 Systems)

[source,coq]

Theorem operation_sequence_reversible : forall ops fs, all_reversible ops fs -> apply_sequence (reverse_sequence ops) (apply_sequence ops fs) = fs. —-

=== Equivalence (Proven in 4 Systems)

[source,coq]

Theorem cno_identity_element : forall op fs, reversible op fs -> apply_op (reverse_op op) (apply_op op fs) ≈ fs. —-

[TIP]

CNO = Certified Null Operation: A reversible operation followed by its reverse provably does nothing (identity element).

This connects to Absolute Zero’s composition theory.

== Architecture

=== Proof Systems

Valence Shell uses polyglot verification across 6 proof systems:

[cols=“2,2,3”] |=== |System |Foundation |Lines

|Coq |Calculus of Inductive Constructions |~1,200

|Lean 4 |Dependent Type Theory |~900

|Agda |Intensional Type Theory |~700

|Isabelle/HOL |Higher-Order Logic |~650

|Mizar |Tarski-Grothendieck Set Theory |~400

|Z3 SMT |First-Order Logic + Theories |~150 |===

Why 6 systems?

=== Trust Boundaries

[source]

┌─────────────────────────────────────┐ │ Formal Proofs (HIGH TRUST) │ ← Mathematical guarantees │ ~478 candidates, ~4,280 lines │ └─────────────┬───────────────────────┘ │ Extraction (GAP) ⚠️ ┌─────────────▼───────────────────────┐ │ OCaml Implementation (MEDIUM TRUST) │ ← Type safe, memory safe │ FFI to POSIX, audit logging │ └─────────────┬───────────────────────┘ │ FFI (GAP) ⚠️ ┌─────────────▼───────────────────────┐ │ POSIX Syscalls (LOW TRUST) │ ← Kernel guarantees only │ mkdir, rmdir, open, read, write │ └──────────────────────────────────────┘ —-

[WARNING]

Verification Gap: The formal proofs operate on abstract models. The implementation (OCaml FFI + POSIX) is not formally connected to the proofs.

This means:

To reach production: Close extraction gap (Coq → OCaml verification).

== Bridge to Echo Types + Ochrance

Valence Shell sits inside a three-layer architecture; the other two layers are upstream theory repositories:

[cols=“1,2”] |=== | Layer | Role

Valence Shell (this repo)
Executes commands; tracks operation history; exposes explain/checkpoint/diff/replay; proves reversible-operation properties across the proof stack.
hyperpolymath/echo-types
Semantic theory of structured loss. Interprets shell operations as maps f : Pre -> Post with proof-relevant residues Echo f y := Σ (x : A) , (f x ≡ y). Names what is recoverable, constrained, observationally equivalent, or genuinely lost.
hyperpolymath/ochrance
Receipt + attestation substrate (A2ML manifests, Merkle-backed state commitments, repair witnesses).

|===

Status: the bridge is documentation-and-orientation-only — not a mechanised dependency. Read link:docs/ECHO-TYPES-OCHRANCE-BRIDGE.adoc[the bridge doc] before claiming production-readiness, mechanised Lean-to-Rust correspondence, RMO/GDPR beyond stubs, or Ochrance cryptographic integrity. Machine-readable companion at link:.machine_readable/ECHO_TYPES_OCHRANCE_BRIDGE.a2ml[ECHO_TYPES_OCHRANCE_BRIDGE.a2ml].

== Verification Status

=== ✅ What IS Guaranteed (by proofs)

=== ❌ What Is NOT Guaranteed

== MAA Framework

Mutually Assured Accountability: Every action has a provable audit trail.

=== RMR (Remove-Match-Reverse)

Status: ✅ Proven for directories and files

[source,coq]

RMR primitives: - mkdir/rmdir (proven reversible) - create_file/delete_file (proven reversible) - write_file (proven reversible) —-

Use Case: Safe operations with guaranteed rollback

=== RMO (Remove-Match-Obliterate)

Status: ⚠️ Experimental file-level implementation

obliterate overwrites and unlinks regular files and records a best-effort audit residue. It does not guarantee removal from CoW extents, flash translation layers, snapshots, journals, replicas, backups, or remote storage, and its abstract Z3 model is not a proof of the Rust implementation or a GDPR compliance determination. See link:docs/RMO-DURABILITY-BOUNDARY.adoc[RMO durability and assurance boundary].

== Contributing

We welcome contributions across three perimeters:

=== 🔴 Perimeter 1: Core (Maintainers Only)

=== 🟡 Perimeter 2: Extensions (Trusted Contributors)

=== 🟢 Perimeter 3: Community (Open to All)

See link:CONTRIBUTING.md[CONTRIBUTING.md] for details.

== Documentation

[cols=“2,3”] |=== |File |Description

|link:CLAUDE.md[CLAUDE.md] |START HERE - Comprehensive AI assistant context

|link:proofs/README.md[proofs/README.md] |Proof documentation, how to read proofs

|link:SECURITY.md[SECURITY.md] |Security policy, vulnerability reporting

|link:CONTRIBUTING.md[CONTRIBUTING.md] |Contribution guidelines, TPCF framework

|link:CODE_OF_CONDUCT.md[CODE_OF_CONDUCT.md] |Community standards, emotional safety

|link:CHANGELOG.adoc[CHANGELOG.adoc] |Version history, what’s changed

|link:RSR_COMPLIANCE.md[RSR_COMPLIANCE.md] |RSR Framework compliance report (PLATINUM)

|link:docs/PROGRESS_REPORT.md[PROGRESS_REPORT.md] |Phase 1 detailed report

|link:docs/PHASE2_REPORT.md[PHASE2_REPORT.md] |Composition & equivalence theory

|link:docs/PHASE3_INITIAL_REPORT.md[PHASE3_INITIAL_REPORT.md] |File content operations |===

== Roadmap

=== Version 0.15.0 (Next Release)

=== Version 0.16.0

=== Version 0.17.0

=== Version 1.0.0 (Production Ready)

== Licensing

License: Palimpsest-MPL 1.0 or later (SPDX: MPL-2.0)

See link:LICENSE[LICENSE] for full text and usage rights. Third-party notices: link:THIRD_PARTY_NOTICES.md[THIRD_PARTY_NOTICES.md].

== RSR Compliance

image:https://img.shields.io/badge/RSR-PLATINUM-blueviolet[RSR PLATINUM]

Valence Shell achieves PLATINUM-level Rhodium Standard Repository (RSR) compliance (105/100):

See link:RSR_COMPLIANCE.md[RSR_COMPLIANCE.md] for full report.

== Community

== FAQ

=== Why 6 proof systems?

Different logical foundations increase confidence. If all 6 systems prove the same theorem, it’s highly unlikely all have the same bug.

=== Is this ready to put in production?

No. Version 0.9.0 is an advanced research prototype with a working shell (~78% complete), but the extraction gap (Lean → Rust → POSIX) is not formally verified. The Rust CLI is functional and extensively tested (794 tests passing, 0 failures), but lacks a mechanised proof of correspondence to the Lean theorems (~85% confidence via property testing). Use for research, education, and experimentation only.

=== Can I use this in my project?

For research/education: Yes! + For production: Not yet (wait for v1.0.0) + License: Palimpsest-MPL 1.0 or later (MPL-2.0)

=== How do I verify the proofs?

[source,bash]

Install proof assistants (via Nix or manually)

nix develop # if using Nix

Verify all proofs compile

just verify-proofs

This compiles ~4,280 lines of proofs and checks:

- Coq: generates .vo certificate files

- Lean 4: compiles to executable

- Agda: type-checks and generates interface files

- Isabelle: builds heap image

# - Z3: checks SMT assertions

=== What’s the difference between algorithmic and thermodynamic reversibility?

Algorithmic (what we have): F⁻¹(F(s)) = s - operations can be undone, information preserved

Thermodynamic (what we DON’T have): Energy → 0 (Landauer limit), Bennett’s reversible computing

We prove the former, not the latter.

=== How does this relate to Absolute Zero?

Absolute Zero provided the CNO (Certified Null Operation) theory showing that reversible operations create identity elements. Valence Shell implements this theory for filesystem operations.

== Citation

If you use Valence Shell in academic work:

[source,bibtex]

@software{valence_shell_2026, title = {Valence Shell: Formally Verified Shell with MAA Framework}, author = {{Valence Shell Contributors}}, year = {2026}, url = {https://github.com/Hyperpolymath/valence-shell}, note = {Polyglot verification across 6 proof systems}, version = {0.9.0} } —-

== Acknowledgments

See link:.well-known/humans.txt[humans.txt] for complete attribution.

== License

Copyright (c) 2025 Valence Shell Contributors

Licensed under Palimpsest-MPL 1.0 or later (SPDX: MPL-2.0). See link:LICENSE[LICENSE] for full text.

Made with ❤️ by humans and AI, for humans who value formal correctness.

Status: Advanced Research Prototype (v0.9.0) | RSR: PLATINUM (105/100) | Proofs: ~478 theorem candidates (0 real gaps; 2 justified axioms) | Tests: 791 passing

[.text-center] “Every operation reversible. Every claim proven. Every contributor valued.”

== Architecture

See link:TOPOLOGY.md[TOPOLOGY.md] for a visual architecture map and completion dashboard.