|
30 | 30 | ; ── End Definitions ────────────────────────────────────────────── |
31 | 31 |
|
32 | 32 | (intent-contractile |
33 | | - (version "1.0.0") |
| 33 | + (version "1.1.0") |
34 | 34 | (repo "valence-shell") |
35 | 35 |
|
36 | 36 | ; === Purpose (what this repo IS) === |
37 | 37 | (purpose |
38 | | - "{{ONE_PARAGRAPH_PURPOSE}}" |
| 38 | + "valence-shell (vsh) is a formally verified Unix-style shell whose every \ |
| 39 | + filesystem-touching operation is backed by a machine-checkable proof of \ |
| 40 | + reversibility. It implements the MAA (Mutually Assured Accountability) \ |
| 41 | + framework: the model-layer operations (mkdir/rmdir, create/delete/write, \ |
| 42 | + cp/mv/ln -s, chmod/chown) are proven reversible across 6 independent \ |
| 43 | + proof systems (Coq, Lean 4, Agda, Isabelle/HOL, Mizar, Z3) so that \ |
| 44 | + cross-validation catches errors a single foundation would miss. The \ |
| 45 | + primary deliverable is a working interactive Rust CLI (impl/rust-cli/) \ |
| 46 | + that mirrors those proven operations and provides undo/redo, named \ |
| 47 | + checkpoints, transaction grouping, and proof-annotated dry-runs — \ |
| 48 | + plus enough POSIX shell surface (pipelines, redirections, here-docs, \ |
| 49 | + job control, variables, control structures, glob, quoting) to be \ |
| 50 | + actually usable. The long-term motivation is GDPR-grade auditable \ |
| 51 | + deletion: every act on the filesystem should be either reversible \ |
| 52 | + (RMR) or attestably irreversible (RMO), with the choice and the proof \ |
| 53 | + observable to a third party." |
39 | 54 | ) |
40 | 55 |
|
41 | 56 | ; === Anti-Purpose (what this repo is NOT — prevents scope creep) === |
42 | 57 | (anti-purpose |
43 | | - "{{ONE_PARAGRAPH_ANTI_PURPOSE}}" |
| 58 | + "valence-shell is NOT a drop-in bash/zsh replacement: it is \ |
| 59 | + verification-first, not POSIX-first. POSIX compliance is a means to \ |
| 60 | + the end of running real shell scripts against proven operations, not \ |
| 61 | + the goal itself — features that cannot be modelled and proven \ |
| 62 | + reversible (or attestably irreversible) are out of scope for the \ |
| 63 | + core. It is NOT a research vehicle for shell language design: \ |
| 64 | + syntactic innovation goes to other shells. It is NOT a production \ |
| 65 | + shell as of v0.9.0 — the extraction gap (Lean → Rust → POSIX \ |
| 66 | + syscalls) is not formally closed; the Rust CLI matches the proven \ |
| 67 | + model via property tests at roughly 85% confidence, not via a \ |
| 68 | + mechanised correspondence theorem. It is NOT a general-purpose \ |
| 69 | + filesystem library: external consumers should not depend on \ |
| 70 | + impl/rust-cli/ internals; the stable surface is the proofs and \ |
| 71 | + (eventually) an extracted, verified runtime. It is NOT a place for \ |
| 72 | + unverified 'convenience features' — every command must have a \ |
| 73 | + proof story or an explicit, documented gap." |
44 | 74 | ; Examples: |
45 | 75 | ; "This is NOT a general-purpose database — it solves one specific problem." |
46 | 76 | ; "This is NOT a framework — it is a library with a focused API." |
|
49 | 79 |
|
50 | 80 | ; === Key Architectural Decisions That Must Not Be Reversed === |
51 | 81 | (architectural-invariants |
52 | | - ; *REMINDER: List the foundational decisions* |
53 | | - ; ("Idris2 for ABI definitions — dependent types prove interface correctness") |
54 | | - ; ("Zig for FFI — zero-cost C ABI compatibility") |
55 | | - ; ("Elixir for supervision — OTP fault tolerance") |
| 82 | + ("Polyglot verification — 6 proof systems (Coq, Lean 4, Agda, Isabelle/HOL, Mizar, Z3) prove the SAME core theorems across DIFFERENT logical foundations; do not collapse to a single prover") |
| 83 | + ("Lean 4 is the primary spec — when proofs disagree, Lean is the canonical statement; other systems cross-validate") |
| 84 | + ("Coq is the extraction path — proofs in coq/ must remain extractable to OCaml/Rust; do not introduce non-computational axioms beyond the documented set (funext, well-formedness, decidability of is_empty_dir)") |
| 85 | + ("Rust is the primary runtime — impl/rust-cli/ is the only production-tracked implementation; OCaml/Elixir/Zig live in impl/ but are reference/FFI artefacts only") |
| 86 | + ("MAA framework split — RMR (Remove-Match-Reverse) operations MUST be proven reversible; RMO (Remove-Match-Obliterate) operations MUST be proven non-injective (information-loss) — never collapse the two") |
| 87 | + ("Honest-status discipline — every claim in README/CLAUDE.md/contractiles must have a counterpart caveat; the EXPLAINME.adoc per-claim caveat pattern is load-bearing") |
| 88 | + ("Reversibility predicate is conditional — theorems are of the form `precondition p fs -> reverse(op(p, fs)) = fs`; never weaken to unconditional reversibility") |
| 89 | + ("Proof-hole audit is authoritative — `docs/PROOF_HOLES_AUDIT.md` is the single source of truth for remaining gaps; CLAUDE.md and README MUST be kept in sync with it") |
| 90 | + ("Six-tool boundary policy is in force — Zig for APIs/FFIs, Idris2 for ABIs, SNIFs for BEAM↔native, typed-wasm for compile targets, Groove Protocol for cross-system service discovery; bash/POSIX is the user surface, not an internal interop layer") |
56 | 91 | ) |
57 | 92 |
|
58 | 93 | ; === Sensitive Areas (if in doubt, ask) === |
59 | 94 | (ask-before-touching |
60 | | - ; *REMINDER: List areas where LLMs should check before modifying* |
61 | | - ; "src/abi/ — formal proofs, changes require re-verification" |
62 | | - ; "ffi/zig/ — C ABI boundary, changes affect all language bindings" |
63 | | - ; ".machine_readable/ — checkpoint files, format is specified" |
| 95 | + "proofs/coq/ proofs/lean4/ proofs/agda/ proofs/isabelle/ proofs/mizar/ proofs/z3/ — every change requires re-verification across affected systems" |
| 96 | + "proofs/idris2/ — ABI carriers; changes here ripple to FFI surface" |
| 97 | + "docs/PROOF_HOLES_AUDIT.md — single-source-of-truth for proof debt; any change must be reflected in CLAUDE.md and README counts the same commit" |
| 98 | + ".machine_readable/ — contractile family (MUST/TRUST/DUST/INTENT/ADJUST) + a2ml agent state; format is specified by the agentic-a2ml ADRs" |
| 99 | + "impl/rust-cli/src/state.rs — operation history, undo/redo, checkpoints; this is the runtime correspondence to the proven model" |
| 100 | + "impl/rust-cli/src/commands/secure_deletion.rs and proofs/idris2/RMO.idr — RMO/GDPR claims; the entire compliance story rides on these" |
| 101 | + "EXPLAINME.adoc — the per-claim-caveat scaffold; do not delete or 'simplify' without owner sign-off" |
| 102 | + "LICENSE + LICENSES/ — REUSE-format SPDX; the project migrated PMPL-1.0 → MPL-2.0 in commit 990b147 and must not regress" |
64 | 103 | ) |
65 | 104 |
|
66 | 105 | ; === Ecosystem Position === |
67 | 106 | (ecosystem |
68 | | - (belongs-to "{{MONOREPO_OR_STANDALONE}}") |
69 | | - (depends-on ("{{DEP1}}" "{{DEP2}}")) |
70 | | - (depended-on-by ("{{CONSUMER1}}" "{{CONSUMER2}}")) |
| 107 | + (belongs-to "STANDALONE") |
| 108 | + ; The proof systems, the Rust CLI, the ABI carriers, and the supporting |
| 109 | + ; reference implementations (OCaml/Elixir/Zig) all live in this single repo. |
| 110 | + ; valence-shell is NOT a sub-project of a larger monorepo. |
| 111 | + |
| 112 | + (depends-on |
| 113 | + "Coq 8.18+ — Calculus of Inductive Constructions, extraction to OCaml" |
| 114 | + "Lean 4.3+ — primary specification language (dependent type theory)" |
| 115 | + "Agda 2.6.4+ — intensional type theory, cross-validation" |
| 116 | + "Isabelle/HOL 2024 — higher-order logic, cross-validation" |
| 117 | + "Mizar — Tarski-Grothendieck set theory, cross-validation" |
| 118 | + "Z3 4.12+ — SMT solver, automated decision procedures" |
| 119 | + "Rust toolchain (stable, edition 2021) — impl/rust-cli/ primary implementation" |
| 120 | + "cargo-fuzz — fuzz harness (7 targets in impl/rust-cli/fuzz/fuzz_targets/)" |
| 121 | + "reedline — interactive REPL backend" |
| 122 | + "Just (command runner) — top-level build orchestration" |
| 123 | + "Nix (recommended) — pinned multi-prover toolchain via flake.nix" |
| 124 | + ) |
| 125 | + |
| 126 | + (depended-on-by |
| 127 | + ; valence-shell has no known production downstream consumers at v0.9.0. |
| 128 | + ; It is a standalone research prototype. Treat any future consumer |
| 129 | + ; relationship as a hard architectural decision requiring INTENT update. |
| 130 | + "NONE_AT_V0_9_0 — no known downstream consumers; this is a standalone research prototype" |
| 131 | + ; Conceptual / aspirational relationships (NOT current code dependencies): |
| 132 | + "absolute-zero (conceptual ancestor) — CNO composition theory predates this project; vsh implements it for filesystem ops" |
| 133 | + ) |
71 | 134 | ) |
72 | 135 | ) |
0 commit comments