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.

Author: hyperpolymath

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

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.

proofs/coq/filesystem_model.v

@@ -99,6 +99,10 @@ Definition parent_exists (p : Path) (fs : Filesystem) : Prop :=
 Definition has_write_permission (p : Path) (fs : Filesystem) : Prop :=
   exists node, fs p = Some node /\ writable (permissions node) = true.
 
+(** Path has read permission *)
+Definition has_read_permission (p : Path) (fs : Filesystem) : Prop :=
+  exists node, fs p = Some node /\ readable (permissions node) = true.
+
 (** Directory is empty (has no children) *)
 Definition is_empty_dir (p : Path) (fs : Filesystem) : Prop :=
   is_directory p fs /\