proofs(coq): assert single_op_reversible model gap (Qed → Admitted) (#48)

`proofs/coq/filesystem_composition.v::single_op_reversible` ended with
`Qed.` despite containing a mid-proof `admit.` in the OpRmdir branch.
Modern Coq (8.10+) treats this as an incomplete proof and refuses to
discharge it — meaning the file did not compile under `coqc` (the
`verify-proofs` job in `.github/workflows/validation.yml` is currently
disabled per `_CoqProject`).

Switching to `Admitted.` registers the missing branches as
Axiom-equivalents, so `Print Assumptions` on any downstream theorem now
correctly surfaces `single_op_reversible` as a dependency rather than
silently treating it as a closed fact.

While writing the docstring, also found that the OpDeleteFile branch
invoked `apply create_delete_file_reversible. assumption.`, which proves
the *forward* direction `delete_file (create_file fs) = fs`. The branch
needs the *reverse* `create_file (delete_file fs) = fs`, which is the
same model gap as OpRmdir (both rely on `default_perms` matching the
original). Now also explicitly `admit`.

Three closure paths documented in the docstring + in
`docs/PROOF-NARRATIVE.adoc § Assumption Registry`:

  (A) strengthen `reversible` to require default_perms on the original
  (B) add `OpMkdirWithPerms` / `OpCreateFileWithPerms` variants whose
      `reverse_op` carries the perm snapshot
  (C) `Filesystem × UndoLog` model

This PR does *not* attempt the closure — that requires the local Coq
build oracle to be working end-to-end. The composition.v file has
additional cascading proof-script errors at:

  * line 271 — `operation_sequence_reversible`: stale rewrite direction
  * line 327 — `reversible_creates_CNO`: `rewrite app_nil_r` targets a
                                          subterm that simpl already
                                          eliminated
  * line 407 — `path_prefix_app_invert`: argument-shape mismatch
  * line 365 — missing `Require Import Lia.` for the `lia` tactic
  * file_content_operations.v:133 — `rewrite Hntype` fails to find
                                     a matching subterm

These will need a coordinated proof-debt sweep with the build oracle
running locally. Filed at docs/PROOF-OPEN-FRONTIER.adoc § Tier S F-2.

Refs #42 (proof inventory).

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/coq/filesystem_composition.v

@@ -180,7 +180,44 @@ Proof.
   assumption.
 Qed.
 
-(** Generic single operation reversibility *)
+(** Generic single operation reversibility.
+
+    PROOF STATUS: Admitted — see [docs/PROOF-NARRATIVE.adoc] § Assumption
+    Registry. The OpRmdir and OpDeleteFile branches both depend on the
+    same model gap: [mkdir] / [create_file] write [default_perms], but
+    the original entry may have had non-default permissions, so
+    [mkdir(rmdir(fs))] ≠ [fs] and [create_file(delete_file(fs))] ≠ [fs]
+    when the original perms were not default.
+
+    Three closure paths on file: (A) strengthen [reversible (OpRmdir p) fs]
+    and [reversible (OpDeleteFile p) fs] to additionally require
+    [fs p = Some (mkFSNode _ default_perms)]; (B) add [OpMkdirWithPerms]
+    and [OpCreateFileWithPerms] variants whose [reverse_op] carries the
+    original perm snapshot; (C) move to a [Filesystem × UndoLog] model
+    where the inverse operation reads the snapshot from the log.
+
+    Two pre-existing bugs were uncovered while writing this docstring:
+
+    (1) The original form ended [Qed.] after a mid-proof [admit.] in
+        the OpRmdir branch. Modern Coq treats this as an incomplete
+        proof and refuses — meaning the file did not previously
+        compile under [coqc] (CI status: verify-proofs job is disabled
+        per [_CoqProject]). Switching to [Admitted.] registers the
+        missing branches as Axiom-equivalents.
+
+    (2) The original OpDeleteFile branch invoked
+        [apply create_delete_file_reversible. assumption.], which
+        proves [delete_file p (create_file p fs) = fs] — the *forward*
+        direction. The OpDeleteFile branch of [single_op_reversible]
+        needs the *reverse* direction
+        [create_file p (delete_file p fs) = fs], which is unprovable
+        under the same model gap. Now also explicitly [admit].
+
+    Downstream theorems ([operation_sequence_reversible],
+    [two_op_sequence_reversible], [three_op_sequence_reversible],
+    [reversible_creates_CNO]) keep their proof scripts; they now show
+    [single_op_reversible] in their [Print Assumptions] output, which
+    is the correct behaviour for an unproven leaf. *)
 Theorem single_op_reversible :
   forall op fs,
     reversible op fs ->
@@ -191,20 +228,14 @@ Proof.
   - (* OpMkdir *)
     apply single_mkdir_reversible.
     assumption.
-  - (* OpRmdir *)
-    (* MODEL GAP (pre-existing): mkdir restores with default_perms, but the original
-       directory may have had different permissions, so mkdir(rmdir(fs)) ≠ fs in general.
-       Full reversibility requires the undo stack to preserve original node data.
-       This is a known limitation of the current Filesystem = Path -> option FSNode model. *)
-    simpl in *. admit.
+  - (* OpRmdir — model gap, see header docstring *)
+    admit.
   - (* OpCreateFile *)
     apply single_create_file_reversible.
     assumption.
-  - (* OpDeleteFile *)
-    simpl in *.
-    apply create_delete_file_reversible.
-    assumption.
-Qed.
+  - (* OpDeleteFile — model gap, see header docstring *)
+    admit.
+Admitted.
 
 (** * Composition Theorems *)