Integrate Coq/OCaml extraction into Bazel

[avrabe]

Goal

Build Coq proofs and OCaml extraction in Bazel pipeline.

Tasks

• Add rules_ocaml to MODULE.bazel
• Create BUILD files for coq/theories/
• Add Coq compilation targets
• Add OCaml extraction targets
• Build extracted OCaml code
• Create FFI layer: Rust ↔ OCaml
• Integrate into compilation pipeline

Coq Theories

• WASM/, ARM/, Synth/, Common/, Extraction/

Acceptance Criteria

• ✅ Coq proofs compile in Bazel
• ✅ OCaml extraction happens automatically
• ✅ Rust can call extracted OCaml (or vice versa)
• ✅ End-to-end verified compilation works

Dependencies

• Requires: Issue Split backend crate into logical components #11 (Rust BUILD files)

[avrabe]

Completed. Rocq proofs are now fully integrated into Bazel via rules_rocq_rust. The coq/BUILD.bazel defines 15 fine-grained rocq_library targets with proper dependency chains, and rocq_proof_test validates all proofs. Run bazel test //coq:verify_proofs to build and verify all proofs.