proofs(coq): assert single_op_reversible model gap (Qed → Admitted)

[hyperpolymath]

Summary

Convert the silently-broken proofs/coq/filesystem_composition.v::single_op_reversible (Qed. after mid-proof admit.) into an explicit Admitted. so the assumption is registered for Print Assumptions.

The original form ended with Qed. after a mid-proof admit. in the OpRmdir branch — modern Coq treats this as an incomplete proof and refuses to discharge it. Confirmed locally with coqc 8.18.0. The verify-proofs job in .github/workflows/validation.yml is disabled per _CoqProject, so this never surfaced in CI.

Also found and made-explicit: the OpDeleteFile branch invoked apply create_delete_file_reversible. assumption., which proves the forward direction delete_file (create_file fs) = fs. The branch needs the reversecreate_file (delete_file fs) = fs — same model gap as OpRmdir (both rely on default_perms matching the original).

Why this matters

Per the 2026-06-01 directive ("make sure we start asserting the assumptions"):

• Silent admit.+Qed. looks like a proven theorem to downstream readers, but is rejected by Coq.
• Explicit Admitted. registers the theorem as an axiom-equivalent; Print Assumptions on any downstream theorem now correctly surfaces single_op_reversible as a dependency.

This is the smallest principled change toward honesty in the proof layer. Three closure paths are documented in the new docstring + in docs/PROOF-NARRATIVE.adoc § Assumption Registry (PR #47):

(A) strengthen reversible to require default_perms on the original
(B) add OpMkdirWithPerms / OpCreateFileWithPerms variants whose reverse_op carries the perm snapshot
(C) Filesystem × UndoLog model

Scope

This PR does not attempt the closure. The composition.v file has additional cascading proof-script errors at:

Line	Issue
filesystem_composition.v:271	operation_sequence_reversible — stale rewrite direction; rewrite <- (IH ...) expands fs on RHS instead of folding the apply_sequence on LHS
filesystem_composition.v:327	reversible_creates_CNO — rewrite app_nil_r targets a subterm simpl already eliminated
filesystem_composition.v:407	path_prefix_app_invert — argument-shape mismatch
filesystem_composition.v:365	missing Require Import Lia. for the lia tactic
file_content_operations.v:133	rewrite Hntype fails to find a matching subterm

These need a coordinated proof-debt sweep with the build oracle running locally. Catalogued in docs/PROOF-OPEN-FRONTIER.adoc § Tier S F-2 (PR #47).

Test plan

• coqc filesystem_model.v succeeds
• coqc file_operations.v succeeds
• Local build of filesystem_composition.vup to the cascading-error line (271) — this PR doesn't make compilation worse; it makes the single specific bug explicit.
• CI: governance / link-check / SPDX should pass (no doc files modified; pure proof script).

Refs #42 (proof inventory).

[github-actions]

🔍 Hypatia Security Scan

Findings: 132 issues detected

Severity	Count
🔴 Critical	9
🟠 High	21
🟡 Medium	102

⚠️Action Required: Critical security issues found!

View findings

[
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action dtolnay/rust-toolchain@nightly needs attention",
"type": "unpinned_action",
"file": "validation.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
"type": "download_then_run",
"file": "lean-verification.yml",
"action": "verify_download_integrity",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
"type": "download_then_run",
"file": "rust-cli.yml",
"action": "verify_download_integrity",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in boj-build.yml",
"type": "missing_timeout_minutes",
"file": "boj-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in cflite_batch.yml",
"type": "missing_timeout_minutes",
"file": "cflite_batch.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in cflite_pr.yml",
"type": "missing_timeout_minutes",
"file": "cflite_pr.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 132 issues detected

Severity	Count
🔴 Critical	9
🟠 High	21
🟡 Medium	102

⚠️Action Required: Critical security issues found!

View findings

[
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action dtolnay/rust-toolchain@nightly needs attention",
"type": "unpinned_action",
"file": "validation.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
"type": "download_then_run",
"file": "lean-verification.yml",
"action": "verify_download_integrity",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
"type": "download_then_run",
"file": "rust-cli.yml",
"action": "verify_download_integrity",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in boj-build.yml",
"type": "missing_timeout_minutes",
"file": "boj-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in cflite_batch.yml",
"type": "missing_timeout_minutes",
"file": "cflite_batch.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in cflite_pr.yml",
"type": "missing_timeout_minutes",
"file": "cflite_pr.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence