Skip to content

CHANGELOG.adoc

Latest commit

 

History

History
610 lines (502 loc) · 26.2 KB

CHANGELOG.adoc

File metadata and controls

610 lines (502 loc) · 26.2 KB
Raw

Changelog

All notable changes to Valence Shell will be documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).

Note: Versions 0.x.x are pre-release. Breaking changes may occur between minor versions.

[Unreleased]

Planned

  • Glob expansion (.txt, ?.rs, [a-z])

  • Quote processing (proper escaping, single/double quotes)

  • Full POSIX shell compliance (subset)

  • RMO (Remove-Match-Obliterate) proofs for GDPR compliance

Added — 2026-07-17

RMO / secure deletion (runtime)

  • obliterate is now wired into the shell and reachable from the REPL and scripts. It was previously implemented in commands/secure_deletion.rs but never dispatched (no Command variant, parser case, or executor arm), so it was unreachable dead code. Added Command::Obliterate { path, force, .. }, the "obliterate" parser case (with --force/-f), and the executor arm routing to secure_deletion::obliterate_path (file/dir dispatch). Proof reference: OBLITERATE_IRREVERSIBLE.

  • Audit residue: obliterate now appends an append-only record to <sandbox-root>/.vsh-audit.log — the MAA attestation that survives the data destruction (GDPR Article 17 evidence). Data is destroyed; proof-of-deletion persists.

  • Tests: impl/rust-cli/tests/obliterate_rmo_tests.rs (6 tests) — dispatch wiring, missing-operand error, end-to-end destruction, audit residue, irreversibility (undo cannot resurrect), and no-old-plaintext-remains. Full suite green; verified through the real binary in script mode.

  • Honest scope: best-effort 3-pass overwrite (random/0x00/0xFF + fsync) on in-place filesystems only. CoW (btrfs/ZFS/APFS)/SSD FTL defeat overwrite (use secure_erase for hardware NIST SP 800-88 Purge); audit-log HMAC signing is still pending. NOT a complete GDPR compliance framework. Status docs reconciled from "RMO stubs only" accordingly.

Correspondence (mechanized differential oracle)

  • proofs/lean4/ModelOracle.lean + lean_exe model_oracle — compiles the proven Lean model definitions (mkdir/rmdir/createFile/deleteFile/ fsUpdate) into a standalone oracle that reports the node type at probe paths.

  • impl/rust-cli/tests/model_oracle_correspondence.rs — differential test that generates precondition-respecting operation sequences, applies them to the real Rust ShellState, runs the same sequence through the compiled Lean model, and asserts they agree at every touched path. 1218 probes agree across 200 sequences. This makes the proof artifact itself the test oracle (stronger than hand-transcribed property tests); it remains differential testing, not a full refinement proof — the latter is still the v1.0 blocker. The test skips cleanly when the oracle is not built.

  • just build-model-oracle / just test-correspondence-model; wired into lean-verification.yml CI.

  • docs/LEAN4_RUST_CORRESPONDENCE.md documents the harness, why the Coq extraction is not executable (function-typed filesystem + classical axioms; needs FMaps.t FSNode migration), and the roadmap to full mechanization.

Launcher (E-Grade Launcher Standard)

  • launch.sh — a standard-conformant launcher implementing the Hyperpolymath E-Grade Launcher Standard mode surface: --auto (default), --start, --stop, --status, --browser/--web, --integ, --disinteg, --help, --version. Version output matches the required vsh <version> (<sha>) [<platform>] format. Desktop integration (Linux first-class) is idempotent, copies rather than symlinks, sets Terminal=true, writes the .desktop at 0444, and --disinteg preserves config and logs. Sources keepopen.sh/soft-attach.sh/gui-error.sh via the published resolution ladder with graceful no-op degradation when the desktop-tools are absent. PID/log paths use XDG dirs (never /tmp). Server-oriented clauses (nohup daemon, wait_for_server URL polling, browser launch) are honestly declared deferred in the a2ml-metadata-block header, since vsh is a foreground terminal shell with no HTTP server. See docs/LAUNCHER.md.

  • scripts/run.sh — the canonical startup command the standard searches for ({repo-dir}/scripts/run.sh); builds the release binary on first use and execs the shell.

  • just run / just launch now delegate to ./launch.sh --auto.

Added — 2026-07-16

Launcher

  • just run (alias just launch) — the user-facing launcher for the vsh shell, previously missing. Builds and starts the interactive REPL; passes extra arguments through to the binary (just run --version, just run script.vsh). Verified end-to-end: --version prints vsh 0.9.0 (exit 0), the REPL banner starts interactively, and script execution runs and exits 0.

  • QUICKSTART-USER.adoc rewritten from the unfilled RSR template to the real, working flow — it no longer references non-existent recipes (just setup, just uninstall, just stapeln-run, just install --portable); every just command it now cites is a real recipe (verified via just --show). Uninstall documents the honest cargo uninstall vsh path.

Verified — 2026-07-16

Proofs

  • Coq proof-debt re-verified to 0 admits / 0 real gaps under Coq 8.18.0. The full _CoqProject (11 files) compiles with no admit/Admitted/Axiom markers. Print Assumptions on the load-bearing theorems: obliterate_overwrites_all_blocks and overwrite_pass_equalizes_storage are Closed under the global context (zero axioms); single_op_reversible, operation_sequence_reversible, copy_file_reversible, mkdir_two_dirs_reversible, obliterate_not_injective depend only on the standard functional_extensionality_dep. The historically-tracked "1 real gap" (obliterate_overwrites_all_blocks) and the three 2026-06-02 admits (#56/#57/#58) are all closed. Remaining assumptions are standard/justified: Coq functional_extensionality (stdlib)
    is_empty_dir_dec (justified classical), Agda funext (structural). Docs reconciled: PROOF_HOLES_AUDIT.md, README.adoc, FAQ.adoc, CLAUDE.md, docs/wiki/, ROADMAP*.{adoc,md}, .machine_readable/6a2/STATE.a2ml, bot_directives/methodology.a2ml.

Fixed — 2026-07-16

Build / tooling

  • just build-coq and scripts/verify-proofs.sh now succeed from a clean checkout. Both previously compiled an incomplete file subset (missing filesystem_composition.v and others), so posix_errors.v failed with "Cannot find a physical path bound to logical path filesystem_composition"; both now compile the full _CoqProject chain in dependency order and mkdir -p extracted before extraction.v (the gitignored output dir), matching the CI oracle in validation.yml.

  • scripts/verify-proofs.sh: fixed two latent set -e bugs that aborted the script before any test ran — VAR++ counters (post-increment returns the pre-value, so the first bump from 0 yields exit status 1) replaced with assignment form; and per-test cd side effects that leaked between tests are now isolated by running each test command in a subshell.

Added — 2026-06-02

Implementation

  • O_NOATIME discipline for pure-read theorems (#94 Gap 9). New src/fs_pure.rs module exposes open_pure / read_to_end / read_to_string helpers that set libc::O_NOATIME on Linux (via OpenOptionsExt::custom_flags) with a graceful EPERM fallback to vanilla File::open when the calling process is not the file owner and lacks CAP_FOWNER. Eight call sites converted: script load (main.rs), source command (executable.rs), audit-log replay (audit_log.rs), state load (state.rs), input redirection (redirection.rs + external.rs), truncate-redirection backup read (redirection.rs), pre-deletion undo backup (commands.rs). Reads from character-special / sysfs paths (e.g. /dev/urandom, /sys/block/…​/rotational) are intentionally untouched — atime is not tracked there and O_NOATIME may be rejected by those subsystems. macOS / non-Linux paths transparently fall through to File::open and rely on mount-level noatime/relatime. Six new unit tests cover round-trip (Vec<u8> + String), open-position, large-file (200 KB), missing-file, and EPERM-fallback parity. Test total: 757 → 764 (+7 incl. doctest).

Proof work

  • Idris2: RMO theorem-shape redesigns landed via PR #105 — secureDeleteNotInjective (mirrors Coq obliterate_not_injective, closes #60) + gdprDeletionCompliant structural redesign (closes #61). New removeEntryDeterminedByFilter + keepIfNotP helpers in Filesystem.Model. Drive-by DecEq Path fix + equivRefl hole unblock the build past Model.

  • Idris2: 8 remaining partial markers in Composition.idr cleared via PR #109 — applyOp now calls underlying addEntry/removeEntry/updateEntry primitives directly. Theorem-shape fixes for All import, Maybe-monadic undo-redo chain, LTE length predicate, and reverseConcat hole. Closes #89.

  • Idris2: 2 misleading partial markers in RMO.idr (secureDelete + gdprDelete IO computations) dropped via PR #108 — IO does not introduce partiality.

  • Total Idris2 partial count is now zero, down from 10 at the start of the session. Hole count 21 + 8 partial → 22 + 0 partial.

  • Idris2 0.8.0 parse fixes — AuditEntry.proof reserved-token clash renamed to obliterated (PR #112); hardwareEraseIrreversible multi-line signature converted to single-line via Unit (PR #113).

  • reverseConcat hole closed via Data.List.revAppend from base stdlib (PR #115). One fewer Composition.idr hole.

CI/CD hardening

  • Idris2 build oracle merged via PR #106 — idris-verification.yml workflow + Justfile recipes (build-idris2, verify-idris2). Non-blocking initially (pre-existing build issues at hardwareEraseIrreversible — resolved same day by PR #113). Closes #70.

Doc + housekeeping

  • Stale sweep: 4 claude/issue-* branches deleted post-merge (#105/#106/#108/#109 squash-merge cleanup) + 1 orphan claude/safedom-res-stale-sweep branch removed (PR #34 merged 2026-05-27; 3 subsequent campaign commits were superseded). Salvaged .github/copilot/coding-agent.yml decision filed as #111.

  • PROOF-NEEDS.md + proofs/idris2/README.md + ROADMAP.adoc refreshed to reflect zero partial count + 3-admit Coq state.

  • State refresh after the 2026-06-02 post-merge sweep (PR #114).

  • Doc followup gathering PRs #112 / #113 / #115 into a single coherent note (PR #116).

CI follow-ups (later in the day)

  • Inherited governance reds cleared on 4 open PRs (PR #110).

  • RMO.idr overwriteIrreversible + auditTrailCompleteness type fixes (PR #117).

  • Idris2 build oracle flipped to strict (PR #118, closes #70 follow-up).

  • Implementation: O_NOATIME discipline landed via PR #120 (merge of the #94 Gap 9 work cited above).

  • Idris2 Category A non-theorem redesigns (PR #121, closes #119A).

  • CI: idris-verification install chez symlink for Ubuntu’s chezscheme (PR #122).

  • Proof: equivSym closed via Data.Bool.andCommutative (PR #123, 1/5 Cat B).

  • 4 admits annotated in rmo_operations.v with explicit obligations; Idris2 keyword/parse fixes accompany.

Added — 2026-06-01

Proof work

  • Coq: single_op_reversible Qed-closed via OpMkdirWithPerms + OpCreateFileWithPerms constructor-variant approach; zero new axioms (PR #67)

  • Lean 4: crash_atomic_within_op_mkdir keystone theorem + 280-line docs/THEORY-CRASH-CONSISTENCY.adoc design doc (PR #62, closes #45 keystone)

  • Idris2: Filesystem/Model.idr typecheck fixed via Data.Maybe import + Eq Path + Eq FSEntry instances (PR #69)

  • Idris2: RMO theorem-shape redesigns closing #60 + #61. secureDeleteIrreversible (non-theorem: recovery fs = fs → Void refuted by recovery = id) → secureDeleteNotInjective mirroring Coq’s obliterate_not_injective; gdprDeletionCompliant (non-theorem: recovery = id refuted by recovery = const empty) → structural witness mirroring Coq’s obliterate_leaves_no_trace. New removeEntryDeterminedByFilter + keepIfNotP helpers in Filesystem.Model. Drive-by Model.idr fixes (DecEq Path impossible-pattern + equivRefl hole) unblock the Idris2 build past Model.

  • Cross-system witness matrix + open-frontier docs (PRs #47/#62)

Implementation

  • Real secure_delete (3-pass overwrite with /dev/urandom/zeros/0xFF + fsync + unlink) replacing the stub (PR #72)

  • Real audit_log (XDG_STATE_HOME, JSON-lines, append-only) replacing the stub (PR #72)

  • 6 unreachable! in commands.rs converted to typed CommandError variants (PR #72)

  • 20 new property-correspondence tests bringing total to 757 passing / 0 failing (PR #72)

CI/CD hardening

  • Clippy -D warnings sweep: 86 errors → 0 across 34 files in impl/rust-cli/ (PR #74)

  • cargo fmt sweep across impl/rust-cli/ (PR #73)

  • SHA-pin standards/governance-reusable.yml from floating @main (PR #103)

  • 5 GH Action SHA bumps (checkout → 1cce339, cache → 27d5ce7, upload-artifact → 043fb46, rust-cache → 8ba370a, scorecard-action → af76153) + 30 cargo dep bumps (PR #68)

  • Add Idris2 build oracle: Justfile recipes + idris-verification.yml workflow + README docs (PR #106 — closes #70)

  • Drop codeql.yml: the JS/TS leg failed under newer codeql-action SHAs (empty-source rejection) and the repo is Rust-primary; Hypatia Neurosymbolic Analysis covers semantic analysis (closes #71)

Licensing

  • LICENSE: drop Palimpsest preamble + FALLBACK framing → plain MPL-2.0 (PR #101)

  • SPDX-FileCopyrightText sweep across the codebase: 267 files in 7 language-batched PRs (PRs #95-#100, #102):

    • 105 Markdown · 70 Rust · 44 AsciiDoc · 22 Zig+C+H · 11 Elixir · 10 Idris2 + LICENSE + anchor taxonomy

Documentation

  • RSR-template gap fill: 188 {{project}} / valence-shell / BUILD_CMD placeholders replaced across 10 files (PR #59)

  • Anchor taxonomy migration: .machine_readable/anchors/ANCHOR.a2ml → .machine_readable/6a2/anchor/ANCHOR.a2ml + 0-AI-MANIFEST.a2ml + README.adoc (PR #102)

  • ROADMAP refreshed with landed-PR cross-refs (M2 + M3 + M4 sweep, PR #68)

  • Wiki bootstrapped (Home + Session-Log-2026-06-01)

Fixed

  • Remove accidentally-tracked runtime artifacts impl/rust-cli/$FILE + .vsh_state.json from PR #73’s test session; add both to .gitignore (PR #75)

Issues filed (PR-sized work units)

  • #60, #61 — RMO.idr theorem-shape redesigns CLOSED via PR #105 (Idris2 ?holes were non-theorems by type signature; signatures redesigned to mirror Coq)

  • #63-#66 — 4 crash-consistency sub-frontiers (POSIX 2024 edges / concurrency-multi-process / Idris2-via-typed-WASM / hardware barriers)

  • #70 — Idris2 build oracle infra CLOSED via PR #106 (Justfile target + CI job + README docs)

  • #71 — CodeQL JS/TS regression CLOSED (workflow dropped — Hypatia covers semantic analysis)

  • #76-#94 — 17 sub-issues under #41/#42/#43/#45 for Option-2 full-closure work

[0.14.0] - 2026-01-29

Added

  • Phase 6 M7-M10: Advanced Shell Features

  • Process substitution (<(cmd) and >(cmd)) with FIFO-based implementation

  • Arithmetic expansion ($expr with +, -, , /, %, * operators)

  • Here documents (<<DELIMITER with expansion, <←DELIMITER with tab stripping)

  • Here strings (<<<word for single-line input)

  • Full job control implementation:

  • Background execution with & operator

  • Job table with specifications (%1, %+, %-, %name, %?pattern)

  • fg command with terminal control (tcsetpgrp)

  • bg command with SIGCONT for resuming stopped jobs

  • kill command with signal parsing (numbers and names)

  • Process group management for job control

  • Job signal handling (SIGTERM, SIGKILL, SIGCONT)

  • Phase 6 M11: Shell Variables (Discovered Complete)

  • Variable storage in ShellState (HashMap, export tracking, positional params)

  • Variable tokenization ($VAR, ${VAR}, special params)

  • Variable expansion with environment fallback

  • Assignment parsing and execution (VAR=value)

  • Export command (export VAR=value)

  • Integration with commands, arithmetic, command/process substitution

  • Fuzzing Infrastructure

  • Comprehensive fuzzing with cargo-fuzz

  • 4 fuzz targets: parser, arithmetic, job specs, signal parsing

  • FUZZING.md documentation guide

  • CI-ready fuzzing configuration

  • Phase 4: Rust-Lean Correspondence

  • Created correspondence design document (PHASE4_CORRESPONDENCE_DESIGN.md, 400+ lines)

  • Created detailed correspondence mapping (PHASE4_CORRESPONDENCE.md, 600+ lines)

  • 15 correspondence tests covering Lean theorems

  • State, operation, precondition, effect, and reversibility correspondence

  • 85% confidence in Rust-Lean equivalence (informal argument + tests)

Testing

  • All tests passing (177 total: 131 unit + 27 integration + 19 property)

  • Added 17 job control tests

  • Added 15 correspondence tests

  • Background job execution verified

  • Signal handling verified

Statistics

  • Phase 6 progress: 11/14 milestones complete (78%)

  • Overall completion: 82%

  • Rust CLI: 95% feature-complete (advanced research prototype — NOT production-ready; extraction gap not formally closed)

Documentation

  • PHASE6_M10_DESIGN.md (job control)

  • PHASE6_M11_DESIGN.md (variables)

  • PHASE6_M11_COMPLETE.md (variable completion report)

  • PHASE4_CORRESPONDENCE_DESIGN.md (verification approach)

  • PHASE4_CORRESPONDENCE.md (detailed mapping)

  • FUZZING.md (fuzzing guide)

[0.7.3] - 2026-01-28

Added

  • Phase 6 M3: Unix Pipelines

  • Pipeline operator (|)

  • Multi-stage pipeline execution (cmd1 | cmd2 | cmd3)

  • Stdio chaining via Stdio::piped()

  • Exit code from last stage (POSIX behavior)

  • Pipeline error handling with undo support

  • SIGINT handling for entire pipeline

  • Final redirections tracked for undo

  • 7 pipeline integration tests

Statistics

  • All tests passing (104/104: 58 unit + 27 integration + 19 property)

Documentation

  • Updated GETTING_STARTED.md with Pipelines section

  • Pipeline examples in documentation

[0.7.2] - 2026-01-28

Added

  • Phase 0: Sealing (Foundation Hardening)

  • SIGINT handling (Ctrl+C interrupts commands, not shell)

  • Error recovery (no silent state persistence failures)

  • Transaction rollback error reporting

  • Test fixtures migration (modern test_sandbox)

  • Getting Started guide and examples

  • GitHub Actions CI pipeline

  • Comprehensive API documentation (rustdoc)

Infrastructure

  • GitHub Actions CI/CD pipeline operational

  • All documentation builds without warnings

  • Rust documentation (rustdoc) complete

[0.7.1] - 2026-01-28

Added

  • Phase 6 M2: I/O Redirections

  • Output redirection (>)

  • Input redirection (<)

  • Append redirection (>>)

  • Error redirection (2>, 2>>)

  • Combined redirection (&>, 2>&1)

  • Redirection undo support (file modifications reversible)

  • Redirection parser with proper precedence

  • File truncate/append tracking for undo

Statistics

  • All tests passing (90/90: 44 unit + 27 integration + 19 property)

Documentation

  • PHASE6_M2_COMPLETE.md

[0.7.0] - 2026-01-28

Added

  • Phase 6 M1: Simple Command Execution

  • Parser extension for external commands

  • External command execution via std::process::Command

  • PATH lookup and executable discovery

  • Exit code tracking in ShellState

  • stdio inheritance (stdin/stdout/stderr)

  • Updated REPL with new parser and external execution

  • Architecture Documentation

  • LEAN4_RUST_CORRESPONDENCE.md

  • ECHIDNA_INTEGRATION.md

  • ARCHITECTURE.md

  • POSIX_COMPLIANCE.md with 14-milestone roadmap

  • OCaml Extraction Pipeline

  • Designed Lean 4 → C → OCaml/Zig extraction pipeline

  • Created proofs/lean4/Extraction.lean (270 lines)

  • Created impl/ocaml/lean_wrapper.c (300 lines)

  • Created impl/ocaml/valence_lean.ml (200 lines)

  • Created impl/zig/src/lean_bindings.zig (400 lines)

  • Architecture: Lean 4 → C → liblean_vsh.so → OCaml/Zig FFI

  • 2,820 lines of code + 1,400 lines of documentation

  • Design 85% complete (C wrapper marshaling TODO)

Statistics

  • All tests passing (27/27: 13 unit + 14 integration)

  • Manual testing successful (ls, echo, pwd working)

Documentation

  • PHASE6_M1_DESIGN.md

  • EXTRACTION_SUMMARY.md (500 lines)

  • docs/OCAML_EXTRACTION.md (600 lines)

  • docs/ZIG_LEAN_EXTRACTION.md (700 lines)

[0.6.0] - 2025-12-01

Added

  • Phase 3 Extended: Advanced File Operations

  • File copy/move operations

  • Symbolic link support

  • Content composition theorems

  • Isabelle and Mizar content operations

Changed

  • Extended proof coverage for file operations

  • Completed all Phase 3 planned features

[0.5.0] - 2025-11-22

Added

  • Phase 3 Initial: File Content Operations

  • File content read/write operations in Coq (~330 lines)

  • File content operations in Lean 4 (~210 lines)

  • File content operations in Agda (~180 lines)

  • Proven reversibility: write(old, write(new, fs)) = fs

  • Proven independence: operations on different paths don’t interfere

  • State capture/restore for undo/redo

  • FileModificationRecord for MAA audit trail

  • Equivalence Theory Completion

  • Mizar equivalence proofs (~190 lines)

  • All 5 manual proof assistants now have complete equivalence theory

  • CNO = identity element proven in 5 systems

Statistics

  • Proof files: 23 → 27

  • Proof lines: ~3,180 → ~4,280

  • Total theorems: ~217 → ~256

  • Systems with equivalence: 4/5 → 5/5 ✅

  • Systems with content ops: 0 → 3

Documentation

  • docs/PHASE3_INITIAL_REPORT.md (comprehensive phase report)

[0.4.0] - 2025-11-22

Added

  • Phase 2: Composition & Equivalence Theory

  • Composition theorems in Coq, Lean 4, Agda, Isabelle

  • Equivalence relations in Coq

  • Z3 SMT encoding for automated verification

  • CNO (Certified Null Operations) connection

  • Mizar composition framework

  • Infrastructure

  • Containerfile for reproducible builds

  • Complete Justfile with 25+ recipes

  • scripts/verify-proofs.sh multi-prover orchestration

Fixed

  • Agda composition admitted lemmas completed

  • Isabelle composition sorry statements resolved

Statistics

  • Proof files: 19 → 23 (+4)

  • Proof lines: ~2,280 → ~3,180 (+900)

  • Total proofs: ~130 → ~217 (+87)

Documentation

  • docs/PHASE2_REPORT.md

  • SESSION_COMPLETE.md

  • INTEGRATION_SUMMARY.md

[0.3.0] - 2025-11-22 (Early)

Added

  • Isabelle/HOL and Mizar Support

  • Filesystem model in Isabelle/HOL

  • File operations in Isabelle/HOL

  • Filesystem model in Mizar

  • File operations in Mizar

  • Cross-validation across 5 proof systems

Changed

  • Expanded to 5 proof assistants (was 3)

  • Polyglot verification now includes different logical foundations

[0.2.0] - 2025-11-21

Added

  • Lean 4 and Agda Support

  • Complete filesystem model in Lean 4

  • Complete file operations in Lean 4

  • Complete filesystem model in Agda

  • Complete file operations in Agda

  • Cross-validation between dependent type theories

Changed

  • Proofs now in 3 systems: Coq, Lean 4, Agda

  • Improved proof modularity

Documentation

  • Added proof system comparison documentation

[0.1.0] - 2025-11-20

Added

  • Initial Coq Proofs

  • Filesystem model with paths, nodes, permissions

  • mkdir/rmdir operations with reversibility proof

  • create_file/delete_file operations with reversibility proof

  • POSIX error modeling (EEXIST, ENOENT, EACCES, etc.)

  • Extraction framework to OCaml

  • OCaml Implementation

  • FFI to POSIX syscalls

  • Audit logging hooks for MAA

  • Path resolution and sandboxing

  • Elixir Reference Implementation

  • Matches Coq specification

  • POSIX error handling

  • Reversible operations (RMR primitives)

  • Core Theorems (Coq only)

  • mkdir_rmdir_reversible

  • create_delete_file_reversible

  • operation_independence

  • path_preservation

  • Error code correctness

Documentation

  • CLAUDE.md (AI assistant context)

  • docs/PROGRESS_REPORT.md

  • docs/ARCHITECTURE.adoc

  • proofs/README.md

Infrastructure

  • Justfile build automation

  • scripts/demo_verified_operations.sh

  • Nix flake for reproducible builds

  • GitLab CI/CD configuration

[0.0.1] - 2025-11-19

Added

  • Initial project structure

  • Basic MAA framework concepts

  • RMO/RMR primitive definitions (abstract lists only)

  • Repository setup (GitLab primary, GitHub mirror)

Documentation

  • Initial README

  • Vision and goals document

Version Numbering

Current status: Pre-1.0 (Research Prototype)

  • 0.x.x: Research and development

  • Breaking changes allowed

  • Formal proofs stable

  • Implementation unstable

  • 1.0.0: Production-grade target (future — not yet attempted)

  • Extraction gap closed

  • FFI verified

  • Security audit complete

  • Breaking changes follow semver

Upgrade Notes

0.4.0 → 0.5.0

New capabilities: - File content operations available - Can now read/write file contents with proven reversibility

Breaking changes: - None (additive only)

Migration: - No migration needed - New features are opt-in

0.3.0 → 0.4.0

New capabilities: - Operation sequences - Equivalence relations - CNO = identity element

Breaking changes: - None (proof additions only)

Future Releases

Planned for 0.15.0

  • ❏ Glob expansion (.txt, ?.rs, [a-z])

  • ❏ Quote processing (proper escaping, single/double quotes)

  • ❏ Variables in redirections (edge case fix)

  • ❏ Expanded correspondence tests (15 → 25+ property tests)

Planned for 0.16.0

  • ❏ Echidna validation pipeline integration

  • ❏ Property-based build validation

  • ❏ Continuous fuzzing in CI/CD

Planned for 0.17.0

  • ❏ RMO (obliterative deletion) proofs

  • ❏ GDPR compliance primitives

  • ❏ Secure overwrite guarantees

Planned for 0.18.0

  • ❏ Access control modeling

  • ❏ Capability-based security

  • ❏ Enhanced MAA framework

Planned for 1.0.0 (Production Ready)

  • ❏ Extraction gap closed (Lean → Rust formal verification)

  • ❏ Full verification stack

  • ❏ Verify FFI layer

  • ❏ Security audit complete

  • ❏ Performance optimization

  • ❏ Complete POSIX compliance (subset)

  • ❏ Fuzzing campaign complete

Contributing

See [CONTRIBUTING.md](CONTRIBUTING.md) for how to contribute to future releases.

Maintained by: See [MAINTAINERS.adoc](MAINTAINERS.adoc) License: Palimpsest-MPL 1.0 or later (see LICENSE)