Skip to content

proofs(coq): re-enable verify-proofs CI job (oracle); fix 5 cascading build errors #49

Description

@hyperpolymath

Background

The audit on 2026-06-01 (PRs #47, #48) discovered that `proofs/coq/filesystem_composition.v` has 5 pre-existing build errors that `coqc 8.18.0` rejects but CI does not surface — `.github/workflows/validation.yml::verify-proofs` is currently disabled per `proofs/coq/_CoqProject`.

Without this guard, the proof layer can silently drift. Specifically: `single_op_reversible` was Qed-after-admit (would error in modern Coq) for months without anyone noticing.

Errors uncovered

File:Line Error
`filesystem_composition.v:271` `operation_sequence_reversible` — `rewrite <- (IH ...)` expands `fs` on RHS instead of folding the `apply_sequence` on LHS. `apply single_op_reversible` fails to unify.
`filesystem_composition.v:327` `reversible_creates_CNO` — `rewrite app_nil_r` targets a `_ ++ []` subterm that `simpl` already eliminated.
`filesystem_composition.v:407` `path_prefix_app_invert` — `Hpre` provided where shape `path_prefix (ct ++ [ch]) p = true` expected.
`filesystem_composition.v:365` Missing `Require Import Lia.` — the `lia` tactic is used at lines 365/376/378/387/407/437/451 but the import is absent. Trivial fix.
`file_content_operations.v:133` `rewrite Hntype` fails to find a matching subterm ("`node_type n`" not in `Hold`).

Work breakdown

  1. Trivial: Add `Require Import Lia.` to `filesystem_composition.v`.
  2. Small: Re-derive the `reversible_creates_CNO` proof; the underlying claim is true. Replace the stale `rewrite app_nil_r` script with a direct argument.
  3. Medium: Fix `operation_sequence_reversible` rewrite direction. The right script is roughly:
    ```coq
    rewrite reverse_sequence_app. (* split off the last op )
    rewrite apply_sequence_app. (
    split apply over append — need helper lemma )
    rewrite (IH (apply_op op fs) Hrev_rest). (
    fold inner sequence *)
    apply single_op_reversible. assumption.
    ```
  4. Medium: Fix `path_prefix_app_invert` argument shape.
  5. Medium: Fix `file_content_operations.v:133` rewrite target.
  6. Then: Re-enable the `verify-proofs` CI job in `.github/workflows/validation.yml`. Update `_CoqProject` to remove the disabled-note comment.

Acceptance criteria

  • `coq_makefile -f _CoqProject -o Makefile && make` succeeds end-to-end against `coqc 8.18.0`.
  • CI `verify-proofs` job is enabled and green on `main`.
  • `Print Assumptions single_op_reversible.` is captured in the build output for the assumption-registry audit trail.

Note on closure of the underlying model gap

This issue is the build-oracle portion. The semantic content (model gap in `single_op_reversible` OpRmdir/OpDeleteFile branches) is tracked in `docs/PROOF-OPEN-FRONTIER.adoc § Tier S F-2` with three closure paths (strengthen `reversible`, OpMkdirWithPerms variant, or UndoLog model). They are independent fixes.

Refs #42, PR #47, PR #48.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions