proofs(coq): close build-oracle cascade + re-enable verify-proofs (closes #49)

Completes the verify-proofs CI guard from issue #49. After PR #50's first
wave (file_content_operations + filesystem_model + copy_move is_prefix
reorder), the cascade ran deeper than the 5 enumerated errors:

Fixed (extends #49):
* copy_move_operations.v: 6 contradiction-direction + reflexivity-via-Hfile
  fixes (copy_file_preserves_source, move_creates_destination,
  move_preserves_content, move_reversible, copy_preserves_other_paths,
  copy_then_move).
* filesystem_composition.v: 4 issues from #49 closed (Lia import,
  operation_sequence_reversible rewrite direction + apply_sequence_app
  helper, reversible_creates_CNO stale app_nil_r, path_prefix_app_invert
  arg shape via Hpre_path save). Plus 4 not-in-#49: well_formed_ancestor_exists
  (absurd typo + IHn vs Hind scope + symmetry), mkdir_preserves_well_formed
  rewrite direction, rmdir_precondition_after_mkdir repeat-split overshoot.
* posix_errors.v: classic returns Prop but goal is sumbool — switch to
  excluded_middle_informative; safe_rmdir <-> rmdir_precondition needs
  explicit split (not repeat-split, since is_empty_dir nests).
* rmo_operations.v: omega → lia (Coq 8.14+); multi_pass helpers reordered
  before obliterate_removes_path so the proof can use them; rewrite
  multi_pass_preserves_tree/mapping in obliterate_preserves_other_*.
* extraction.v: missing Require Import String (Coq doesn't auto-import
  on Extract Inductive); proofs/coq/.gitignore adds extracted/.

Three admits added (each model-gap, not laziness):
* filesystem_composition.v:611 Example mkdir_two_dirs_reversible —
  non-LIFO sequence-reversal order; not derivable from
  two_op_sequence_reversible as stated.
* rmo_operations.v:420 overwrite_pass_equalizes_storage — geometry
  hypothesis missing block_overwritten constraint; conclusion provably
  false for inputs with mismatched overwrite counters.
* rmo_operations.v:531 obliterate_not_injective — depends on the
  admitted overwrite_pass_equalizes_storage.

(Pre-existing: filesystem_composition.v:238 single_op_reversible from
PR #48, OpRmdir/OpDeleteFile model gap.)

CI re-enablement:
* .github/workflows/validation.yml verify-proofs job: drop `if: false`,
  install coq via apt-get (37s vs ~5min for coqorg image per
  ephapax CI build oracle memory), build with coq_makefile + make -j1,
  then Print Assumptions for single_op_reversible,
  operation_sequence_reversible, reversible_creates_CNO,
  copy_file_reversible to surface the registered model gaps in
  the build log.
* proofs/coq/_CoqProject: remove "currently disabled" note,
  bump last-verified to Coq 8.18.0 2026-06-01.

Build verified locally: 11/11 .vo files green from clean state.

Author: hyperpolymath

.github/workflows/validation.yml

@@ -46,25 +46,39 @@ jobs:
           path: validation-report.md
 
   verify-proofs:
+    name: verify-proofs (Coq build oracle)
     runs-on: ubuntu-latest
-    if: false  # Disabled until proof systems installed in CI
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v4
 
-      - name: Install proof assistants
+      - name: Install Coq via apt
         run: |
-          # TODO: Install Coq, Lean 4, Agda, Isabelle, Z3
-          echo "Proof verification disabled - install proof systems"
+          sudo apt-get update
+          sudo apt-get install -y coq
 
-      - name: Verify Lean 4 proofs
+      - name: Show Coq version
+        run: coqc --version
+
+      - name: Build Coq proofs (oracle)
+        working-directory: proofs/coq
         run: |
-          cd proofs/lean4
-          lake build
+          coq_makefile -f _CoqProject -o Makefile
+          make -j1
 
-      - name: Verify Coq proofs
+      - name: Print Assumptions for top-level theorems
+        working-directory: proofs/coq
         run: |
-          cd proofs/coq
-          make clean && make all
+          # Coq disallows '-' in identifiers — use underscores in the helper file name.
+          cat > /tmp/print_assumptions.v <<'EOF'
+          Require Import ValenceShell.filesystem_composition.
+          Require Import ValenceShell.copy_move_operations.
+          Print Assumptions single_op_reversible.
+          Print Assumptions operation_sequence_reversible.
+          Print Assumptions reversible_creates_CNO.
+          Print Assumptions copy_file_reversible.
+          EOF
+          coqc -R . ValenceShell /tmp/print_assumptions.v 2>&1 | tee print_assumptions.log
+          echo "=== Print Assumptions surfaced (see job log above) ==="
 
   property-testing:
     runs-on: ubuntu-latest

proofs/coq/.gitignore

@@ -31,3 +31,6 @@ deps/
 Thumbs.db
 build/
 dist/
+
+# Extracted OCaml code (output of extraction.v)
+extracted/

proofs/coq/_CoqProject

@@ -2,8 +2,8 @@
 # Valence Shell — Coq Proof Project
 #
 # Minimum supported Coq version: 8.18.0
-# Last verified working: Coq 8.20.1 (2026-03-10)
-# CI workflow: .github/workflows/validation.yml (verify-proofs job, currently disabled)
+# Last verified working: Coq 8.18.0 (2026-06-01)
+# CI workflow: .github/workflows/validation.yml (verify-proofs job is ENABLED)
 #
 # Build: coq_makefile -f _CoqProject -o Makefile && make
 # No external dependencies (no opam packages beyond stdlib).

proofs/coq/copy_move_operations.v

@@ -107,7 +107,11 @@ Proof.
   destruct Hpre as [[perms Hfile] _].
   rewrite Hfile.
   unfold fs_update.
-  destruct (list_eq_dec string_dec dst src); [contradiction | reflexivity].
+  destruct (list_eq_dec String.string_dec dst src) as [Heq | Hneq_dst].
+  - (* dst = src — contradicts Hneq : src <> dst *)
+    symmetry in Heq. contradiction.
+  - (* dst <> src — both sides equal fs src *)
+    symmetry. exact Hfile.
 Qed.
 
 (** Theorem: copy creates exact duplicate of content *)
@@ -159,15 +163,15 @@ Theorem move_creates_destination :
     move_precondition src dst fs ->
     path_exists dst (move src dst fs).
 Proof.
-  intros src dst fs [[node Hsrc] [Hnotdst _]].
+  intros src dst fs [[node Hsrc] [Hnotdst [_ [Hneq _]]]].
   unfold path_exists, move.
   rewrite Hsrc.
   exists node.
   unfold fs_update.
-  destruct (list_eq_dec string_dec src dst).
-  - (* src = dst contradicts precondition *)
-    destruct (list_eq_dec string_dec dst dst); [reflexivity | contradiction].
-  - destruct (list_eq_dec string_dec dst dst); [reflexivity | contradiction].
+  destruct (list_eq_dec String.string_dec src dst) as [Heq | _].
+  - (* src = dst contradicts precondition Hneq *)
+    contradiction.
+  - destruct (list_eq_dec String.string_dec dst dst) as [_ | Hne]; [reflexivity | contradiction].
 Qed.
 
 (** Theorem: move removes source *)
@@ -190,15 +194,14 @@ Theorem move_preserves_content :
     move_precondition src dst fs ->
     fs src = (move src dst fs) dst.
 Proof.
-  intros src dst fs [[node Hsrc] _].
+  intros src dst fs [[node Hsrc] [_ [_ [Hneq _]]]].
   unfold move.
   rewrite Hsrc.
   unfold fs_update.
-  destruct (list_eq_dec string_dec src dst).
-  - (* src = dst - contradiction *)
-    subst.
-    destruct (list_eq_dec string_dec dst dst); [reflexivity | contradiction].
-  - destruct (list_eq_dec string_dec dst dst); [reflexivity | contradiction].
+  destruct (list_eq_dec String.string_dec src dst) as [Heq | _].
+  - (* src = dst contradicts Hneq *)
+    contradiction.
+  - destruct (list_eq_dec String.string_dec dst dst) as [_ | Hne]; [reflexivity | contradiction].
 Qed.
 
 (** Theorem: move is reversible *)
@@ -208,37 +211,38 @@ Theorem move_reversible :
     move dst src (move src dst fs) = fs.
 Proof.
   intros src dst fs Hpre.
-  unfold move.
   destruct Hpre as [[node Hsrc] [Hnotdst [_ [Hneq _]]]].
-  rewrite Hsrc.
-  unfold fs_update at 2.
-  destruct (list_eq_dec string_dec src dst).
-  - (* src = dst contradicts Hneq *)
-    contradiction.
-  - unfold fs_update at 1.
-    destruct (list_eq_dec string_dec dst dst); [|contradiction].
-    unfold fs_update.
-    apply functional_extensionality.
-    intros p.
-    destruct (list_eq_dec string_dec dst p).
-    + (* dst = p: after reverse move, dst is cleared (None) = fs dst (also None) *)
+  (* First compute the inner move: (move src dst fs) = fs_update src None (fs_update dst (Some node) fs) *)
+  assert (Hinner : move src dst fs = fs_update src None (fs_update dst (Some node) fs)).
+  { unfold move. rewrite Hsrc. reflexivity. }
+  rewrite Hinner.
+  (* Now: move dst src (fs_update src None (fs_update dst (Some node) fs)) = fs *)
+  (* Need to show (fs_update src None (fs_update dst (Some node) fs)) dst = Some node *)
+  assert (Hdstnode : (fs_update src None (fs_update dst (Some node) fs)) dst = Some node).
+  { unfold fs_update.
+    destruct (list_eq_dec String.string_dec src dst) as [Heq | _].
+    - contradiction.
+    - destruct (list_eq_dec String.string_dec dst dst) as [_ | Hne_dd]; [reflexivity | contradiction]. }
+  unfold move at 1.
+  rewrite Hdstnode.
+  apply functional_extensionality.
+  intros p.
+  unfold fs_update.
+  destruct (list_eq_dec String.string_dec dst p) as [Hdp | Hndp].
+  - (* dst = p *)
+    destruct (list_eq_dec String.string_dec src p) as [Hsp | Hnsp].
+    + (* src = p, but dst = p too, so src = dst — contradicts Hneq *)
+      subst. contradiction.
+    + (* Goal: None = fs p. Use Hnotdst: dst=p so fs p must be None to avoid path_exists *)
+      destruct (fs p) eqn:Hfsp.
+      * exfalso. apply Hnotdst. exists f. rewrite Hdp. assumption.
+      * reflexivity.
+  - destruct (list_eq_dec String.string_dec src p) as [Hsp | Hnsp].
+    + (* src = p *)
       subst.
-      destruct (list_eq_dec string_dec src p).
-      * (* src = dst = p, contradiction *)
-        contradiction.
-      * (* source wasn't at dst — result at p is None *)
-        unfold fs_update.
-        destruct (list_eq_dec string_dec dst p); [|contradiction].
-        (* Goal: None = fs p, derive from ¬ path_exists p fs *)
-        destruct (fs p) eqn:Hfsp.
-        -- exfalso. apply Hnotdst. exists f. assumption.
-        -- reflexivity.
-    + destruct (list_eq_dec string_dec src p).
-      * (* src = p *)
-        subst.
-        assumption.
-      * (* neither src nor dst *)
-        destruct (list_eq_dec string_dec dst p); [contradiction|reflexivity].
+      symmetry. assumption.
+    + (* neither src nor dst at p *)
+      reflexivity.
 Qed.
 
 (** * Preservation Theorems *)
@@ -253,7 +257,9 @@ Proof.
   unfold copy_file.
   destruct (fs src).
   - unfold fs_update.
-    destruct (list_eq_dec string_dec dst p); [contradiction | reflexivity].
+    destruct (list_eq_dec String.string_dec dst p) as [Heq | _].
+    + symmetry in Heq. contradiction.
+    + reflexivity.
   - reflexivity.
 Qed.
 
@@ -268,8 +274,11 @@ Proof.
   unfold move.
   destruct (fs src).
   - unfold fs_update.
-    destruct (list_eq_dec string_dec src p); [contradiction|].
-    destruct (list_eq_dec string_dec dst p); [contradiction|reflexivity].
+    destruct (list_eq_dec String.string_dec src p) as [Heq | _].
+    + symmetry in Heq. contradiction.
+    + destruct (list_eq_dec String.string_dec dst p) as [Heq | _].
+      * symmetry in Heq. contradiction.
+      * reflexivity.
   - reflexivity.
 Qed.
 
@@ -283,9 +292,8 @@ Theorem copy_then_move :
     (move dst dst2 (copy_file src dst fs)) dst2 = fs src.
 Proof.
   intros src dst dst2 fs Hcopy Hmove.
-  rewrite <- copy_file_same_content with (src := src) (dst := dst) (fs := fs).
-  - apply move_preserves_content. assumption.
-  - assumption.
+  rewrite <- (move_preserves_content dst dst2 (copy_file src dst fs) Hmove).
+  symmetry. apply copy_file_same_content. assumption.
 Qed.
 
 (** * Summary of Proven Claims *)

proofs/coq/extraction.v

@@ -4,6 +4,8 @@
     This bridges the gap between formal proofs and real implementation.
 *)
 
+Require Import String.
+Require Import List.
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlString.