Skip to content

Commit cb0f0b8

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
README batch 2/4: 5 proofs/* subtree READMEs (audit item 3)
Continues per-directory README coverage (CRG-AUDIT-2026-04-18 item 3). Completes the proofs/ tree — every cross-validating proof system now carries an orientation file alongside the existing parent proofs/README.md. Files added (all .adoc, all SPDX-headed, all reference the audit + STATE proof-debt status): * proofs/coq/README.adoc — CIC foundation; OCaml extraction target; cites the active admit. at filesystem_composition.v:199 and the justified is_empty_dir_dec axiom; flags the Makefile.conf auto-emission as RSR-acceptable; records the 2026-04-12 -Q→-R fix and the .gitignore for build artefacts. * proofs/agda/README.adoc — intensional type theory; --safe --without-K discipline (matches the echo-types proof suite); valence-shell.agda-lib manifest. * proofs/isabelle/README.adoc — classical HOL; ROOT session declaration; notes the RMO_Operations.thy underscore-naming divergence from sibling systems (Isabelle convention). * proofs/mizar/README.adoc — Tarski-Grothendieck set-theory grounding; foundational diversity (vs the type-theoretic and HOL systems); MML-anchored articles. * proofs/z3/README.adoc — automated SMT-LIB v2 verification; combined filesystem_operations.smt2 (Z3 doesn't need the per-module split the interactive systems use); unsat = theorem-holds discipline. All five reference the parent ../README.md, the primary-source-of-truth ../lean4/README.adoc, and the unified proof-debt audit. Cumulative coverage move: 10/22 (~45%) → 15/22 (~68%) of non-hidden subtrees in the audit's missing-README list. Remaining 7: impl/elixir, impl/ocaml, impl/mcp, ffi/zig, src/abi, scripts, examples, hooks, benches (some likely empty / RSR-template scaffold and may need "intentionally minimal" notes rather than full docs). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 9ecad26 commit cb0f0b8

5 files changed

Lines changed: 306 additions & 0 deletions

File tree

‎proofs/agda/README.adoc‎

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= proofs/agda/ — Agda Filesystem Proofs (Intensional Type Theory)
3+
4+
Agda (intensional dependent type theory) cross-validates the
5+
filesystem reversibility theorems against the primary Lean 4 source
6+
of truth (`../lean4/`). Agda's intensional treatment of equality
7+
provides a different lens than Lean's HoTT-flavoured framework.
8+
9+
== Files
10+
11+
[cols="2,4"]
12+
|===
13+
| File | Role
14+
15+
| `FilesystemModel.agda` | Core `Filesystem` model + structural lemmas.
16+
| `FilesystemComposition.agda` | Composition theorems.
17+
| `FilesystemEquivalence.agda` | State-equivalence relations.
18+
| `FileOperations.agda` | Per-op specs (mkdir, rmdir, touch, rm).
19+
| `FileContentOperations.agda` | Read/write/append + size lemmas.
20+
| `CopyMoveOperations.agda` | `cp`/`mv` reversibility.
21+
| `PermissionOperations.agda` | chmod/chown bit-preservation.
22+
| `SymlinkOperations.agda` | Symlink creation + traversal.
23+
| `RMOOperations.agda` | Remove-Match-Obliterate (GDPR-relevant).
24+
|===
25+
26+
Manifest:
27+
28+
* `valence-shell.agda-lib` — Agda library file declaring this
29+
directory as the `valence-shell` library.
30+
31+
== Build
32+
33+
```bash
34+
cd proofs/agda
35+
agda --safe --without-K FilesystemModel.agda # single module
36+
agda --safe --without-K -i . CopyMoveOperations.agda # transitive
37+
```
38+
39+
== Conventions
40+
41+
* `--safe --without-K` discipline (no axiom K, no postulates) — same
42+
flags as the `echo-types` proof suite the author maintains in the
43+
hyperpolymath repo.
44+
* PascalCase module names; one module per file.
45+
* No `.agdai` interface artefacts in tree (cached locally, not
46+
committed).
47+
48+
== See also
49+
50+
* `../README.md` — overall proof-stack design
51+
* `../lean4/README.adoc` — primary source of truth
52+
* `../../docs/PROOF_HOLES_AUDIT.md` — proof-debt status across all
53+
systems

‎proofs/coq/README.adoc‎

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,81 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= proofs/coq/ — Coq Filesystem Proofs (CIC Foundation)
3+
4+
Coq (Calculus of Inductive Constructions) provides the CIC foundation
5+
for the valence-shell formal specs and serves as the OCaml extraction
6+
target. The primary source of truth is Lean 4 (`../lean4/`); Coq
7+
cross-validates and feeds extraction.
8+
9+
== Files
10+
11+
[cols="2,4"]
12+
|===
13+
| File | Role
14+
15+
| `filesystem_model.v`
16+
| Core `Filesystem = Path -> option FSNode` model + structural lemmas.
17+
Note: this finite-domain model is the source of the
18+
`is_empty_dir_dec` axiom (justified per `STATE.a2ml
19+
[coq-proof-status] axiom-detail`).
20+
21+
| `filesystem_composition.v`
22+
| Composition theorems. Carries one declared `admit.` at line ~199
23+
(`single_op_reversible` OpRmdir branch — pre-existing model gap;
24+
see `STATE.a2ml [coq-proof-status] admitted-detail`).
25+
26+
| `filesystem_equivalence.v`
27+
| State-equivalence relations.
28+
29+
| `file_operations.v` | Per-op specs for mkdir, rmdir, touch, rm.
30+
| `file_content_operations.v`| Read/write/append; size lemmas.
31+
| `copy_move_operations.v` | `cp`/`mv` reversibility.
32+
| `permission_operations.v` | chmod/chown bit-preservation.
33+
| `symlink_operations.v` | Symlink creation + traversal.
34+
| `rmo_operations.v` | Remove-Match-Obliterate (GDPR-relevant).
35+
| `posix_errors.v` | POSIX error classification + 5/6
36+
constructively-proved decision procedures
37+
(was 3 Axiom; full rewrite 2026-04-12,
38+
commit `1ef841c`).
39+
40+
| `extraction.v`
41+
| OCaml extraction declarations; targets `../../impl/ocaml/`.
42+
|===
43+
44+
Manifests + build:
45+
46+
* `_CoqProject` — uses `-R` recursive logical-path mapping (was `-Q`,
47+
fixed 2026-04-12 to handle subdir imports correctly).
48+
* `Justfile` — Coq-specific recipes (preferred entry point).
49+
* `Makefile.conf` — auto-emitted by `coq_makefile`; standard for the
50+
Coq toolchain. Per the 2026-04-18 audit this is acceptable under the
51+
RSR R-020 root-Makefile rule (proof-system carve-out).
52+
53+
Build artefacts (`.glob`, `.vo`, `.vos`, `.vok`) are present in the
54+
tree but should be `.gitignore`'d (gitignore added 2026-04-12; legacy
55+
commits seeded these files pre-ignore).
56+
57+
== Build
58+
59+
```bash
60+
cd proofs/coq
61+
just build # via Justfile (preferred)
62+
make all # via auto-emitted Makefile
63+
```
64+
65+
== Proof-debt status
66+
67+
* `admitted = 1` — `single_op_reversible` OpRmdir branch
68+
(`filesystem_composition.v:199`).
69+
* `axioms-justified = 1` — `is_empty_dir_dec` (infinite-domain
70+
decidability; migration path: switch to `FMaps.t FSNode`).
71+
* All other proofs constructively closed.
72+
73+
Authoritative status in `../../.machine_readable/6a2/STATE.a2ml`
74+
under `[coq-proof-status]`.
75+
76+
== See also
77+
78+
* `../README.md` — overall proof-stack design
79+
* `../lean4/README.adoc` — primary source of truth
80+
* `../../docs/PROOF_HOLES_AUDIT.md` — full proof-debt history
81+
* `../../impl/ocaml/` — extraction target

‎proofs/isabelle/README.adoc‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= proofs/isabelle/ — Isabelle/HOL Filesystem Proofs
3+
4+
Isabelle/HOL (higher-order logic) cross-validates the filesystem
5+
reversibility theorems against the primary Lean 4 source of truth
6+
(`../lean4/`). Isabelle's classical HOL setting and Sledgehammer
7+
automation provide an independent verification path.
8+
9+
== Files
10+
11+
[cols="2,4"]
12+
|===
13+
| Theory | Role
14+
15+
| `FilesystemModel.thy` | Core `Filesystem` model + structural lemmas.
16+
| `FilesystemComposition.thy` | Composition theorems.
17+
| `FilesystemEquivalence.thy` | State-equivalence relations.
18+
| `FileOperations.thy` | Per-op specs (mkdir, rmdir, touch, rm).
19+
| `FileContentOperations.thy` | Read/write/append + size lemmas.
20+
| `CopyMoveOperations.thy` | `cp`/`mv` reversibility.
21+
| `PermissionOperations.thy` | chmod/chown bit-preservation.
22+
| `SymlinkOperations.thy` | Symlink creation + traversal.
23+
| `RMO_Operations.thy` | Remove-Match-Obliterate (GDPR-relevant).
24+
Note underscore vs other systems'
25+
RMOOperations — Isabelle convention.
26+
|===
27+
28+
Manifest:
29+
30+
* `ROOT` — Isabelle session declaration; lists theories + base session.
31+
32+
== Build
33+
34+
```bash
35+
cd proofs/isabelle
36+
isabelle build -d . valence-shell # full session
37+
isabelle jedit -d . FilesystemModel.thy # interactive
38+
```
39+
40+
== Conventions
41+
42+
* PascalCase theory names matching the file basename.
43+
* Classical HOL; uses Sledgehammer for proof discovery where helpful.
44+
* No build artefacts in tree (Isabelle keeps caches under `~/.isabelle/`).
45+
46+
== See also
47+
48+
* `../README.md` — overall proof-stack design
49+
* `../lean4/README.adoc` — primary source of truth
50+
* `../../docs/PROOF_HOLES_AUDIT.md` — proof-debt status

‎proofs/mizar/README.adoc‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= proofs/mizar/ — Mizar Filesystem Proofs (Tarski-Grothendieck Set Theory)
3+
4+
Mizar grounds the valence-shell filesystem theorems in
5+
Tarski-Grothendieck set theory — a foundationally distinct lens from
6+
the type-theoretic systems (Lean 4 / Coq / Agda) and the higher-order
7+
logic system (Isabelle). Mizar's MML cross-checks the same composition
8+
identities under classical first-order logic.
9+
10+
== Files
11+
12+
[cols="2,4"]
13+
|===
14+
| Article | Role
15+
16+
| `filesystem_model.miz` | Core `Filesystem` model + structural lemmas.
17+
| `filesystem_composition.miz` | Composition theorems.
18+
| `filesystem_equivalence.miz` | State-equivalence relations.
19+
| `file_operations.miz` | Per-op specs (mkdir, rmdir, touch, rm).
20+
| `file_content_operations.miz` | Read/write/append + size lemmas.
21+
| `copy_move_operations.miz` | `cp`/`mv` reversibility.
22+
| `permission_operations.miz` | chmod/chown bit-preservation.
23+
| `symlink_operations.miz` | Symlink creation + traversal.
24+
| `rmo_operations.miz` | Remove-Match-Obliterate (GDPR-relevant).
25+
|===
26+
27+
== Build
28+
29+
Mizar verification typically runs against an installed MML (Mizar
30+
Mathematical Library). With the standard MML environment configured:
31+
32+
```bash
33+
cd proofs/mizar
34+
mizf filesystem_model.miz # single article
35+
verifier filesystem_model.miz # core verifier
36+
```
37+
38+
== Conventions
39+
40+
* snake_case article names (Mizar convention).
41+
* Each `.miz` file is a self-contained article importing from the MML.
42+
* No build artefacts in tree.
43+
44+
== Status
45+
46+
Mizar's value here is foundation-diversity rather than driving the
47+
implementation. Tracked alongside the other systems in the unified
48+
proof-debt audit; per the 2026-04-12 sweep no Mizar-specific debts are
49+
outstanding.
50+
51+
== See also
52+
53+
* `../README.md` — overall proof-stack design + the 5-system
54+
reversibility theorem
55+
* `../lean4/README.adoc` — primary source of truth
56+
* `../../docs/PROOF_HOLES_AUDIT.md` — proof-debt status across all
57+
systems

‎proofs/z3/README.adoc‎

Lines changed: 65 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,65 @@
1+
// SPDX-License-Identifier: PMPL-1.0-or-later
2+
= proofs/z3/ — Z3 SMT Filesystem Proofs (Automated Verification)
3+
4+
Z3 (SMT-LIB v2 scripts) provides automated verification for the
5+
filesystem operation invariants. Unlike the interactive proof systems
6+
(Lean 4 / Coq / Agda / Isabelle) and the structural foundation (Mizar),
7+
Z3 discharges decidable fragments via SAT-modulo-theories solving.
8+
9+
== Files
10+
11+
[cols="2,4"]
12+
|===
13+
| Script | Role
14+
15+
| `filesystem_operations.smt2`
16+
| Combined filesystem-model + composition + equivalence in one
17+
SMT-LIB session (Z3 doesn't need the per-module split that the
18+
type-theoretic systems use). Carries the core
19+
reversibility-as-equality assertions.
20+
21+
| `copy_move_operations.smt2`
22+
| `cp`/`mv` reversibility properties as SMT assertions.
23+
24+
| `permission_operations.smt2`
25+
| chmod/chown bit-preservation properties.
26+
27+
| `symlink_operations.smt2`
28+
| Symlink creation + traversal properties.
29+
30+
| `rmo_operations.smt2`
31+
| Remove-Match-Obliterate properties (GDPR-relevant).
32+
|===
33+
34+
== Build / verify
35+
36+
```bash
37+
cd proofs/z3
38+
z3 filesystem_operations.smt2 # single script
39+
z3 -smt2 copy_move_operations.smt2 # explicit SMT-LIB v2 mode
40+
```
41+
42+
A `(check-sat)` returning `unsat` for a negated property is the
43+
"theorem holds" outcome; `sat` indicates a counterexample (model
44+
extractable via `(get-model)`).
45+
46+
== Conventions
47+
48+
* SMT-LIB v2 syntax; one script per concern.
49+
* snake_case filenames matching the underlying-system naming.
50+
* Theorems quoted from the Lean 4 / Coq sources are referenced in
51+
comments at the top of each script.
52+
53+
== Status
54+
55+
Z3's role is decidability of low-level fragments + counterexample
56+
generation. Tracked alongside the other systems in the unified
57+
proof-debt audit; no Z3-specific debts outstanding per the 2026-04-12
58+
sweep.
59+
60+
== See also
61+
62+
* `../README.md` — overall proof-stack design
63+
* `../lean4/README.adoc` — primary source of truth (interactive)
64+
* `../coq/README.adoc` — interactive CIC foundation
65+
* `../../docs/PROOF_HOLES_AUDIT.md` — proof-debt status

0 commit comments

Comments
 (0)