From e755dc7a0db7e6b7dbc19ea2d547375d936b8d18 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 2 May 2026 08:25:41 +0200
Subject: [PATCH] chore(proofs): wire FusedOptimization.v into BUILD.bazel
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Closes audit D1: proofs/simplify/FusedOptimization.v was orphaned
from the Bazel build (not in any rocq_library / rocq_proof_test
target), so CI never compiled or checked it. The file backs the
fused/meld optimization pipeline with 7 axioms + 8+ theorems
covering same-memory adapter collapse, adapter devirtualization,
trivial-call elimination, and type/import dedup.

Wires it in as:
- new rocq_library "fused_optimization" depending on wasm_semantics
  and term_semantics
- new rocq_proof_test "fused_optimization_test"
- added to the all_proofs_test test_suite

The 7 axioms remain unchanged in this PR (they are stated assumptions,
not Admitteds — they typecheck and CI accepts them as load-bearing
trust). Future work: discharge them with real proofs against the
operational semantics in WasmSemantics.v.

This is the BUILD.bazel patch authored by a parallel agent that
hit a watchdog timeout before pushing — the diff was clean and is
shipped as-is.

Note on Rocq CI: the Rocq Formal Proofs job in ci.yml is currently
continue-on-error: true due to a known rules_rocq_rust toolchain
linker error (LLVM-19-rust-1.85.0-nightly missing). That is infra,
not a proof failure. Once the toolchain is fixed, FusedOptimization.v
will be checked alongside the other proofs.

Trace: REQ-7
---
 proofs/BUILD.bazel | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/proofs/BUILD.bazel b/proofs/BUILD.bazel
index 437f084..142c96c 100644
--- a/proofs/BUILD.bazel
+++ b/proofs/BUILD.bazel
@@ -100,6 +100,25 @@ rocq_proof_test(
     deps = [":strength_reduction"],
 )
 
+# Fused/meld optimization proofs
+# Covers the optimization passes specific to WebAssembly modules produced by
+# component fusion: same-memory adapter collapse, adapter devirtualization,
+# trivial call elimination, type/import dedup, dead function elimination.
+rocq_library(
+    name = "fused_optimization",
+    srcs = ["simplify/FusedOptimization.v"],
+    deps = [
+        ":wasm_semantics",
+        ":term_semantics",
+    ],
+    visibility = ["//visibility:public"],
+)
+
+rocq_proof_test(
+    name = "fused_optimization_test",
+    deps = [":fused_optimization"],
+)
+
 # =============================================================================
 # Master Correctness Theorem
 # =============================================================================
@@ -175,6 +194,7 @@ filegroup(
         ":identity",
         ":bitwise",
         ":strength_reduction",
+        ":fused_optimization",
     ],
     visibility = ["//visibility:public"],
 )
@@ -200,6 +220,7 @@ filegroup(
         ":identity",
         ":bitwise",
         ":strength_reduction",
+        ":fused_optimization",
         ":correctness",
         # Existing proofs
         ":stack_proofs",
@@ -226,6 +247,7 @@ test_suite(
         ":identity_test",
         ":bitwise_test",
         ":strength_reduction_test",
+        ":fused_optimization_test",
         ":correctness_test",
         ":stack_proofs_test",
         ":codec_proofs_test",