proofs(coq): close admit triumvirate (#56 / #57 / #58) — Coq layer at zero Admitted

[hyperpolymath]

Summary

Closes the 3 Coq Admitted markers introduced in PR #55 (build-oracle cascade), bringing the Coq layer to zero Admitted markers — only the justified Axiom is_empty_dir_dec remains.

• proofs(coq): restate mkdir_two_dirs_reversible as LIFO sequence (admit #1 of 3 from #55) #56mkdir_two_dirs_reversible (filesystem_composition.v) — restated to LIFO order so it discharges via two_op_sequence_reversible + rmdir_precondition_after_mkdir + mkdir_preserves_well_formed. Only standard funext.
• proofs(coq): strengthen Hgeom or weaken overwrite_pass_equalizes_storage (admit #2 of 3 from #55) #57overwrite_pass_equalizes_storage (rmo_operations.v) — closure path (A): Hgeom strengthened with block_overwritten blk1 = block_overwritten blk2. Case-split on In bid (sfs_mapping sfs1 p); mapped branch uses In_existsb_Nat_eqb + f_equal on the mkBlock constructor; un-mapped branch uses overwrite_path_blocks_non_mapped_preserved. one_pass_storage_agrees re-signed to match. Zero axioms.
• proofs(coq): reconnect obliterate_not_injective after #57 closes (admit #3 of 3 from #55) #58obliterate_not_injective (rmo_operations.v) — threads the strengthened hypothesis through one_pass_storage_agrees and multi_pass_same_start_same_result, then reassembles mkStorageFS via cbn [sfs_tree sfs_storage sfs_mapping] + f_equal + functional_extensionality. The strengthened hypothesis is trivially satisfied for first-time obliteration (block_overwritten = 0 on both sides), so the MAA/GDPR marketing claim is unchanged. Only standard funext.

Also reconciles PROOF-NEEDS.md:

• Idris2 hole tally corrected 22 → 16 (equivSymProof and appendOnlyAuditLogProof were closed silently in the morning sweep but the inventory text was not updated).
• Assumption Registry table updated.
• "What Needs Proving" rewritten as a 7-tier prioritised attack-list (P1 closeable now; P2 blocked on primitive-eq groundwork; P3 research; P4–P7 Tier-A/B/C/D from frontier).

Test plan

• coqc -R . ValenceShell clean on all 11 .v files
• Print Assumptions mkdir_two_dirs_reversible → functional_extensionality_dep only
• Print Assumptions overwrite_pass_equalizes_storage → "Closed under the global context" (zero axioms)
• Print Assumptions obliterate_not_injective → functional_extensionality_dep only
• idris2 --build valence-shell.ipkg exit 0 (no Idris2-side regression)
• grep -c '^Admitted' across proofs/coq/*.v = 0
• CI idris-verification.yml green
• CI Coq build oracle green (if wired)

Closes#56.
Closes#57.
Closes#58.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 136 issues detected

Severity	Count
🔴 Critical	8
🟠 High	36
🟡 Medium	92

⚠️Action Required: Critical security issues found!

View findings

[
{
"reason": "Issue in codeql.yml",
"type": "missing_workflow",
"file": "codeql.yml",
"action": "create",
"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": "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 bridge-forbidden-phrases.yml",
"type": "missing_timeout_minutes",
"file": "bridge-forbidden-phrases.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 compilation_tests.yml",
"type": "missing_timeout_minutes",
"file": "compilation_tests.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[github-actions]

🔍 Hypatia Security Scan

Findings: 136 issues detected

Severity	Count
🔴 Critical	8
🟠 High	36
🟡 Medium	92

⚠️Action Required: Critical security issues found!

View findings

[
{
"reason": "Issue in codeql.yml",
"type": "missing_workflow",
"file": "codeql.yml",
"action": "create",
"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": "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 bridge-forbidden-phrases.yml",
"type": "missing_timeout_minutes",
"file": "bridge-forbidden-phrases.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 compilation_tests.yml",
"type": "missing_timeout_minutes",
"file": "compilation_tests.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence