proofs(coq): close single_op_reversible OpRmdir branch via OpMkdirWithPerms variant (#67)

Closes the long-standing [admit.] in [single_op_reversible] (OpRmdir
and OpDeleteFile branches) by taking closure path #2 from the
documented design note: the [Operation] inductive now carries
[OpMkdirWithPerms : Path -> Permissions -> Operation] and
[OpCreateFileWithPerms : Path -> Permissions -> Operation]
constructors, and [reverse_op] is threaded with the pre-state so the
inverse of [OpRmdir]/[OpDeleteFile] can capture the original node's
permissions exactly.

Changes:

  * filesystem_composition.v
    - Operation: +2 constructors (OpMkdirWithPerms, OpCreateFileWithPerms).
    - mkdir_with / create_file_with: write a node at a path with the
      supplied permissions (instead of default_perms).
    - apply_op: handle the two new constructors.
    - reverse_op: now [Operation -> Filesystem -> Operation]; for
      OpRmdir/OpDeleteFile, look up the node and route to the
      ...WithPerms variant.
    - reverse_sequence: now stateful; LIFO threading of pre-states.
    - reverse_sequence_app / _singleton: re-proved under the new signature.
    - op_precondition / reversible: extended to the new constructors.
    - single_op_reversible: now closed with Qed (no admits).  All 6
      cases discharged from [reversible op fs] alone.
    - operation_sequence_reversible / two_op_ / three_op_ /
      reversible_creates_CNO: re-stated under the new reverse_sequence
      threading; proofs adjusted.
    - Print Assumptions at end-of-file: 3 lines, each showing only
      [functional_extensionality_dep] — the same axiom already used by
      [mkdir_rmdir_reversible] in the base model.  No new axioms.

  * filesystem_equivalence.v
    - apply_op_preserves_equiv: +2 branches for the new constructors.
    - mkdir_with_preserves_equiv / create_file_with_preserves_equiv:
      added (same shape as their default-perms cousins).
    - reversible_creates_equiv / sequence_reversible_equiv /
      cno_identity_element / sequence_cno_identity: re-stated under
      the threaded [reverse_op]/[reverse_sequence] signatures.

Out of scope (pre-existing admit unchanged):

  - [mkdir_two_dirs_reversible] is still [Admitted.] — it documents a
    non-LIFO sequence-reversal that is independent of the model-gap
    closed here.

Refs #41 (Phase 1)
Refs #42 (proof inventory)

Closure path #2 ("OpMkdirWithPerms variant") chosen — the directive
called this the cleanest.  Path #1 would have required strengthening
[reversible] with a [fs p = Some (mkFSNode _ default_perms)] side
condition; path #3 (UndoLog) is heavier-weight.

Echo-types audit: not relevant — this is L1 (region-mode) shape, not
L3 (echo).  Recorded per [feedback_proofs_must_check_and_cross_doc_echo_types].

Local build oracle (mandatory per [feedback_proof_pr_build_oracle_is_only_truth]):
  coq_makefile -f _CoqProject -o build.mk && make -f build.mk
GREEN on Coq 8.18.0.

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

Author: hyperpolymath