proofs/close-coq-admit-triumvirate-56-57-58#140
Merged
Conversation
hyperpolymath
commented
Jun 5, 2026
hyperpolymath
commented
Owner
- proofs(coq): close admit triumvirate (proofs(coq): restate mkdir_two_dirs_reversible as LIFO sequence (admit #1 of 3 from #55) #56 / proofs(coq): strengthen Hgeom or weaken overwrite_pass_equalizes_storage (admit #2 of 3 from #55) #57 / proofs(coq): reconnect obliterate_not_injective after #57 closes (admit #3 of 3 from #55) #58)
- docs(proof-needs): reclassify 3 RMO 'Cat-D' holes as Cat-A non-theorems
Three closures land the Coq layer at zero `Admitted` markers: * `mkdir_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`. Closes #56. Only standard funext. * `overwrite_pass_equalizes_storage` (rmo_operations.v) — closure path (A) per issue #57: `Hgeom` strengthened with `block_overwritten blk1 = block_overwritten blk2`. Proof case-splits 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` and the `Hother` hypothesis. `one_pass_storage_agrees` re-signed to match. Closes #57. Zero axioms. * `obliterate_not_injective` (rmo_operations.v) — threads the strengthened hypothesis through `one_pass_storage_agrees` and `multi_pass_same_start_same_result`, then reassembles the `mkStorageFS` via `cbn [sfs_tree sfs_storage sfs_mapping]` + `f_equal` + `functional_extensionality`. The strengthened hypothesis is trivially satisfied for the canonical first-time obliteration use case (block_overwritten = 0 on both sides), so the MAA/GDPR marketing claim is unchanged. Closes #58. Only standard funext. PROOF-NEEDS.md reconciled: * Idris2 hole tally corrected 22 -> 16 (equivSymProof and appendOnlyAuditLogProof were closed silently during the morning sweep but the inventory text was not updated). * Assumption Registry table updated: 3 Coq admits removed, axiom inventory now lists only is_empty_dir_dec + funext. * "What Needs Proving" rewritten as a 7-tier prioritised attack-list (P1 closeable now; P2 blocked on primitive-eq groundwork; P3-P7 research / frontier / marginal / tooling). Verified locally: * `coqc -R . ValenceShell` clean on all 11 .v files * `Print Assumptions` for each closed theorem: only funext (or zero for #57) * `idris2 --build valence-shell.ipkg` exit 0 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Closer reading of every remaining Idris2 hole on the P1/P2 attack-list reveals the original triage (and the P1 paragraph from earlier this commit-series) was over-optimistic. The 3 RMO holes I'd labelled Cat-D axiomatic placeholders are actually provably false as stated: * overwriteIrreversibleProof (RMO.idr:130) — conclusion `recovery randomData = Nothing` is refuted by `recovery = Just`. * hardwareEraseIrreversibleProof (RMO.idr:215) — type signature is refuted by any non-empty `Unit -> Filesystem`. * auditTrailCompletenessProof (RMO.idr:270) — conclusion is refuted by `entries = []`. These need theorem-shape redesign (per the #60 / #61 precedent), not believe_me markers. Recorded as follow-up — recommend filing as #119 sub-issues with the explicit refutations. Additionally: * DecEq Path does NOT unblock the primitive-eq batch because it transitively depends on DecEq String. Earlier claim that decEq gives a free path-eq reflexivity lemma was wrong. * Three closure paths for the primitive-eq blocker documented (axioms via believe_me / Nat-interned paths / decEq-style reformulation), each requiring owner sign-off. * Frozen-hole list made explicit. No source changes; documentation honesty only. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
force-pushed
the
proofs/close-coq-admit-triumvirate-56-57-58
branch
from
June 5, 2026 03:04
824b84f to
f40c0ab
Compare
🔍 Hypatia Security ScanFindings: 154 issues detected
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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.