Background
PR #55 introduced 3 documented admits. This is the LOAD-BEARING one — the keystone for the RMO/obliterate proof chain.
Admit
proofs/coq/rmo_operations.v:420 — overwrite_pass_equalizes_storage
Status
Geometry hypothesis (Hgeom) is missing the block_overwritten constraint; conclusion is provably false when overwrite counters differ. This means the theorem as stated has a counterexample — the current proof would be unsound.
Closure paths
Two options:
(A) Strengthen Hgeom. Add block_overwritten p sfs ≥ N (or similar) to the hypothesis so the conclusion follows. Requires tracking per-path overwrite counters in StorageFS if not already present.
(B) Weaken the conclusion. Restate to something true: e.g. obliterate p sfs1 patterns ≈ obliterate p sfs2 patterns (observational equivalence at storage level) rather than literal equality, OR storage_after_pass p N sfs1 = storage_after_pass p N sfs2 ∨ ¬reachable_distinct sfs1 sfs2 p (disjunction with the bad case).
Echo-types alignment
Per issue #51 (echo-types integration audit), this theorem is the L3 loss-taxonomy shape. EchoLossTaxonomy.const-fibre-↔-domain could ground a weaker version directly. Worth checking whether option (B) can lift to a downstream consequence of echo-types' CONST case.
Blocks
Refs
🤖 Filed from PR #55 closure
Background
PR #55 introduced 3 documented admits. This is the LOAD-BEARING one — the keystone for the RMO/obliterate proof chain.
Admit
proofs/coq/rmo_operations.v:420—overwrite_pass_equalizes_storageStatus
Geometry hypothesis (
Hgeom) is missing theblock_overwrittenconstraint; conclusion is provably false when overwrite counters differ. This means the theorem as stated has a counterexample — the current proof would be unsound.Closure paths
Two options:
(A) Strengthen
Hgeom. Addblock_overwritten p sfs ≥ N(or similar) to the hypothesis so the conclusion follows. Requires tracking per-path overwrite counters inStorageFSif not already present.(B) Weaken the conclusion. Restate to something true: e.g.
obliterate p sfs1 patterns ≈ obliterate p sfs2 patterns(observational equivalence at storage level) rather than literal equality, ORstorage_after_pass p N sfs1 = storage_after_pass p N sfs2 ∨ ¬reachable_distinct sfs1 sfs2 p(disjunction with the bad case).Echo-types alignment
Per issue #51 (echo-types integration audit), this theorem is the L3 loss-taxonomy shape.
EchoLossTaxonomy.const-fibre-↔-domaincould ground a weaker version directly. Worth checking whether option (B) can lift to a downstream consequence of echo-types' CONST case.Blocks
obliterate_not_injectiveatrmo_operations.v:531) depends transitively on this.Refs
proofs/coq/rmo_operations.v:420🤖 Filed from PR #55 closure