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

* proofs(coq): partial closure of build-oracle cascade (refs #49)

Fixes the first wave of errors uncovered while attempting to re-enable
the verify-proofs CI oracle. Issue #49 catalogued 5 errors; this PR
closes those + several deeper cascading failures in the same modules.

Closed:
- file_content_operations.v:133 redundant rewrite of Hntype after eqn:
  destruct already substituted
- file_content_operations.v:137,140 exact (Hcontra eq_refl) replaced
  with destruct (False has no constructors)
- file_content_operations.v:178 destruct (node_type node) missing eqn:
  (no substitution into RHS match)
- file_content_operations.v:272 injection on un-reduced match — restructured
  with assert + destruct
- filesystem_model.v added has_read_permission (referenced by
  copy_move_operations:38, never defined)
- copy_move_operations.v reordered is_prefix definition before its use
  at line 62

Verified locally: filesystem_model.v, file_operations.v,
file_content_operations.v compile against coqc 8.18.0. Remaining
errors past line ~110 of copy_move_operations.v and downstream
in filesystem_composition.v are tracked as continuation of #49.

The verify-proofs CI job will be re-enabled in a follow-up PR once the
full module set compiles end-to-end.

Refs #49, #47.

* 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.

* ci(verify-proofs): mkdir extracted/ before make (gitignored output dir)

extraction.v's [Extraction "extracted/filesystem.ml" ...] writes into the
gitignored directory, which doesn't exist on a fresh CI clone. Add a one-
line mkdir before the make step.

Local fresh clone reproduces the issue without this fix.

Author: hyperpolymath

.github/workflows/validation.yml

@@ -46,25 +46,41 @@ 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
+          # extraction.v writes to extracted/filesystem.ml; the dir is gitignored, so create it.
+          mkdir -p extracted
+          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

@@ -48,6 +48,10 @@ Definition copy_file (src dst : Path) (fs : Filesystem) : Filesystem :=
 
 (** * Move Operation *)
 
+(** Helper: check if path is prefix of another *)
+Definition is_prefix (p1 p2 : Path) : Prop :=
+  exists suffix, p2 = p1 ++ suffix.
+
 (** Precondition for move/rename *)
 Definition move_precondition (src dst : Path) (fs : Filesystem) : Prop :=
   (* Source must exist *)
@@ -65,10 +69,6 @@ Definition move_precondition (src dst : Path) (fs : Filesystem) : Prop :=
   (* Must have write permission on destination parent *)
   has_write_permission (parent_path dst) fs.
 
-(** Helper: check if path is prefix of another *)
-Definition is_prefix (p1 p2 : Path) : Prop :=
-  exists suffix, p2 = p1 ++ suffix.
-
 (** Move operation *)
 Definition move (src dst : Path) (fs : Filesystem) : Filesystem :=
   match fs src with
@@ -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.
 

proofs/coq/file_content_operations.v

@@ -130,16 +130,11 @@ Proof.
     unfold read_file in Hold.
     destruct (fs p) as [n|] eqn:Hfs; [|discriminate].
     destruct (node_type n) eqn:Hntype; [|discriminate].
-    rewrite Hntype in Hold. simpl in Hold.
+    simpl in Hold.
     destruct (node_content n) as [c|] eqn:Hcontent; [|discriminate].
     injection Hold as Heq. subst c.
-    (* Both (list_eq_dec p p) branches are trivially left/right *)
-    destruct (list_eq_dec String.string_dec p p) as [_|Hcontra]; [|exact (Hcontra eq_refl)].
-    rewrite Hfs. rewrite Hntype.
-    (* After inner write: result is Some {|...; node_content := Some new_content|} *)
-    destruct (list_eq_dec String.string_dec p p) as [_|Hcontra]; [|exact (Hcontra eq_refl)].
-    rewrite Hfs. rewrite Hntype. simpl.
-    (* node_type of the intermediate node is File, so outer write applies old_content *)
+    destruct (list_eq_dec String.string_dec p p) as [_|Hcontra]; [|destruct (Hcontra eq_refl)].
+    destruct (list_eq_dec String.string_dec p p) as [_|Hcontra]; [|destruct (Hcontra eq_refl)].
     destruct n as [nt perms cont]; simpl in *.
     subst nt. subst cont.
     reflexivity.
@@ -180,7 +175,7 @@ Proof.
     unfold write_file.
     destruct (list_eq_dec String.string_dec p p) as [_|Hcontra].
     + destruct (fs p) as [node|] eqn:Hfs.
-      * simpl. destruct (node_type node); reflexivity.
+      * destruct (node_type node) eqn:Hnt; cbn; try rewrite Hnt; reflexivity.
       * simpl. reflexivity.
     + contradiction.
   - reflexivity.
@@ -271,15 +266,12 @@ Proof.
       subst p'.
       unfold read_file in Hread.
       destruct Hpre as [node [Hnode [Htype [perms [Hperms Hwrite]]]]].
-      rewrite Hnode in Hread.
-      rewrite Htype in Hread.
-      simpl in Hread.
-      injection Hread as Heq.
+      assert (Hc : node_content node = Some content).
+      { rewrite Hnode in Hread. cbn in Hread.
+        rewrite Htype in Hread. exact Hread. }
       rewrite Hnode.
-      rewrite Htype.
-      destruct node; simpl in *.
-      subst node_type0.
-      subst node_content0.
+      destruct node as [nt nperms ncont]; simpl in *.
+      subst nt. subst ncont.
       reflexivity.
     + (* p <> p' *)
       reflexivity.