From 743e98372f3f1d4fdab32b7b77d1d7723e2a7f8f Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 23 May 2026 06:40:19 +0200
Subject: [PATCH 01/16] chore(deps): bump rules_rocq_rust to e4660cc
 (rules_rust migration)

Picks up pulseengine/rules_rocq_rust#34 which migrates rocq-of-rust to
a hermetic rules_rust toolchain, replacing the ad-hoc cargo build in
coq_of_rust/private/repository.bzl. The old build failed on the CI
runner with `rust-lld: error: unable to find library
-lLLVM-19-rust-1.85.0-nightly`, which has kept the Rocq Formal Proofs
CI check red on main since v1.0.5 (admin-merged through it for the
v1.1.0 and v1.1.1 releases).

Closes the v1.1.1 carry-forward item (task #89).

Trace: REQ-12
---
 MODULE.bazel | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/MODULE.bazel b/MODULE.bazel
index b409504..30068b6 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -16,10 +16,16 @@ module(
 bazel_dep(name = "rules_rocq_rust", version = "0.1.0")
 
 # Override to fetch from GitHub (not yet in BCR)
+# Pinned to e4660cc1b — pulseengine/rules_rocq_rust#34, which migrates
+# rocq-of-rust to a hermetic rules_rust toolchain. This replaces the
+# ad-hoc cargo build in coq_of_rust/private/repository.bzl that was
+# failing on the CI runner with
+# `rust-lld: error: unable to find library -lLLVM-19-rust-1.85.0-nightly`
+# and kept the Rocq Formal Proofs check red on LOOM main since v1.0.5.
 git_override(
     module_name = "rules_rocq_rust",
     remote = "https://github.com/pulseengine/rules_rocq_rust.git",
-    commit = "307b65f",
+    commit = "e4660cc1b",
 )
 
 # Rocq toolchain extension (creates internal nixpkgs for bzlmod compatibility)

From 1e731fbd25e96155671c1a48c4195026e3e2431a Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 23 May 2026 14:22:32 +0200
Subject: [PATCH 02/16] build(bazel): migrate MODULE.bazel for rules_rocq_rust
 rules_rust API
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The pin bump alone (307b65f → e4660cc1b) is necessary but not sufficient:
rules_rocq_rust#34 changed the rocq_of_rust extension's API. Without
matching consumer-side changes the Rocq Formal Proofs CI check fails at
analysis time with

  module extension @@rules_rocq_rust+//coq_of_rust:extensions.bzl%rocq_of_rust
  does not generate repository "rocq_of_rust_source", yet it is imported
  as "rocq_of_rust_source" in the usage at MODULE.bazel:51:29

Updates to match the new API, modelled on the canonical consumer
example at examples/rust_to_rocq/MODULE.bazel in rules_rocq_rust:

- Add bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0").
  rules_rocq_rust's nix_repo is dev_dependency=True there, so as the
  root module LOOM must configure nixpkgs itself.
- Add the nix_repo extension call pinning nixpkgs to the same
  2026-04-01 commit the upstream example uses (Rocq 9.0.1).
- rocq.toolchain: add `with_rocq_of_rust_deps = True`.
- use_repo(rocq, ...): drop `rocq_nixpkgs` (no longer exported by the
  new extension API — the root configures nixpkgs above).
- rocq_of_rust.toolchain: drop the `commit = "..."` arg; the new
  toolchain uses a build-time pinned default (rocq-of-rust @ 877dd65).
- use_repo(rocq_of_rust, ...): replace `rocq_of_rust_source` with
  `rocq_of_rust_build` (the new extension's output repo name).

rules_rust, crate_universe, and the hermetic Rust nightly+rustc-dev
toolchain are NOT dev_dependency in rules_rocq_rust@e4660cc1b's own
MODULE.bazel, so they are inherited transitively and no consumer-side
plumbing is needed for them.

Trace: REQ-12
---
 MODULE.bazel | 50 +++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 37 insertions(+), 13 deletions(-)

diff --git a/MODULE.bazel b/MODULE.bazel
index 30068b6..e7289ef 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -15,12 +15,12 @@ module(
 # Requires nix to be installed: sh <(curl -L https://nixos.org/nix/install)
 bazel_dep(name = "rules_rocq_rust", version = "0.1.0")
 
-# Override to fetch from GitHub (not yet in BCR)
+# Override to fetch from GitHub (not yet in BCR).
 # Pinned to e4660cc1b — pulseengine/rules_rocq_rust#34, which migrates
-# rocq-of-rust to a hermetic rules_rust toolchain. This replaces the
-# ad-hoc cargo build in coq_of_rust/private/repository.bzl that was
-# failing on the CI runner with
-# `rust-lld: error: unable to find library -lLLVM-19-rust-1.85.0-nightly`
+# rocq-of-rust to a hermetic rules_rust toolchain. Replaces the ad-hoc
+# cargo build in coq_of_rust/private/repository.bzl that was failing on
+# the CI runner with
+#   `rust-lld: error: unable to find library -lLLVM-19-rust-1.85.0-nightly`
 # and kept the Rocq Formal Proofs check red on LOOM main since v1.0.5.
 git_override(
     module_name = "rules_rocq_rust",
@@ -28,18 +28,40 @@ git_override(
     commit = "e4660cc1b",
 )
 
-# Rocq toolchain extension (creates internal nixpkgs for bzlmod compatibility)
+# Nix integration. rules_rocq_rust declares rules_nixpkgs_core internally
+# but its nix_repo is dev_dependency=True there, so the root module must
+# configure nixpkgs explicitly. rules_rust, crate_universe, and the
+# hermetic Rust nightly+rustc-dev toolchain that the rocq-of-rust build
+# needs are already registered (non-dev) by rules_rocq_rust's own
+# MODULE.bazel and are inherited automatically.
+bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0")
+
+nix_repo = use_extension(
+    "@rules_nixpkgs_core//extensions:repository.bzl",
+    "nix_repo",
+)
+nix_repo.github(
+    name = "nixpkgs",
+    org = "NixOS",
+    repo = "nixpkgs",
+    # nixos-unstable with Rocq 9.0.1 (2026-04-01).
+    commit = "6201e203d09599479a3b3450ed24fa81537ebc4e",
+    sha256 = "",
+)
+use_repo(nix_repo, "nixpkgs")
+
+# Rocq toolchain extension (uses nixpkgs for a hermetic Rocq/Coq install).
 rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
 rocq.toolchain(
-    version = "9.0",    # Rocq 9.0 for rocq-of-rust compatibility
-    strategy = "nix",   # Hermetic nix-based installation
+    version = "9.0",  # Rocq 9.0.1 (required for the real RocqOfRust library).
+    strategy = "nix",  # Hermetic nix-based installation.
+    with_rocq_of_rust_deps = True,  # Include coqutil, hammer, smpl.
 )
 use_repo(
     rocq,
     "rocq_coqutil",
     "rocq_hammer",
     "rocq_hammer_tactics",
-    "rocq_nixpkgs",
     "rocq_smpl",
     "rocq_stdlib",
     "rocq_toolchains",
@@ -47,12 +69,14 @@ use_repo(
 
 register_toolchains("@rocq_toolchains//:all")
 
-# rocq-of-rust toolchain for translating Rust to Rocq
+# rocq-of-rust toolchain — translates Rust subset to Rocq. Built
+# hermetically through rules_rust + crate_universe in the upstream
+# ruleset (see rules_rocq_rust@e4660cc1b's MODULE.bazel and
+# docs/rules_rust-migration.md).
 rocq_of_rust = use_extension("@rules_rocq_rust//coq_of_rust:extensions.bzl", "rocq_of_rust")
 rocq_of_rust.toolchain(
-    commit = "858907dbee116c51d7c6e87511bf5f92d6432ba4",  # Pinned for reproducibility
-    use_real_library = True,  # Full library with coqutil/hammer/smpl
+    use_real_library = True,  # Full library with coqutil + hammer + smpl.
 )
-use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_source")
+use_repo(rocq_of_rust, "rocq_of_rust_toolchains", "rocq_of_rust_build")
 
 register_toolchains("@rocq_of_rust_toolchains//:toolchain")

From d17e5583dc71c72bdf4fcdf9c997a0c2519ccd92 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sun, 24 May 2026 06:17:37 +0200
Subject: [PATCH 03/16] =?UTF-8?q?build(bazel):=20rename=20@rocq=5Fof=5Frus?=
 =?UTF-8?q?t=5Fsource=20=E2=86=92=20@rocq=5Fof=5Frust=5Fbuild?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Follow-up to the MODULE.bazel migration in 1e731fb. The new
rules_rocq_rust API renamed the build-output repo from
rocq_of_rust_source to rocq_of_rust_build; the alias in
proofs/rust_verified/BUILD.bazel still pointed at the old name and
held up the Rocq Formal Proofs check at analysis time with

  ERROR: no such package '@@[unknown repo 'rocq_of_rust_source'
         requested from @@]//': ... referenced by
         '//proofs/rust_verified:rocq_of_rust_lib'

The :rocq_of_rust_main target it consumes is preserved in the new
repo (verified in upstream coq_of_rust/private/rocq_of_rust_build.bzl
@ e4660cc1b).

Trace: REQ-12
---
 proofs/rust_verified/BUILD.bazel | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/rust_verified/BUILD.bazel b/proofs/rust_verified/BUILD.bazel
index 6bec4d9..a180eaf 100644
--- a/proofs/rust_verified/BUILD.bazel
+++ b/proofs/rust_verified/BUILD.bazel
@@ -9,7 +9,7 @@ load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library")
 # RocqOfRust library - provides the core types needed by translated code
 alias(
     name = "rocq_of_rust_lib",
-    actual = "@rocq_of_rust_source//:rocq_of_rust_main",
+    actual = "@rocq_of_rust_build//:rocq_of_rust_main",
 )
 
 # =============================================================================

From 155381f0829f2135d456711fd40c60f24d38df5f Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sun, 24 May 2026 12:59:22 +0200
Subject: [PATCH 04/16] fix(proofs): decode_uleb128_small replace pattern after
 Rocq 9.0 simpl change
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The Track A roundtrip proof was passing on the v1.0.5-era pin of
rules_rocq_rust (Rocq toolchain pulled by the old ad-hoc cargo build).
After bumping to e4660cc1b — which pulls Rocq 9.0.1 with a stdlib
where [simpl] reduces [0 + n * 1] to [n * 1] eagerly — the existing

  replace (0 + n * 1) with n by lia.

silently no-ops (pattern absent) and the follow-up [reflexivity] then
fails with

  Unable to unify "Some (n, rest)" with "Some (n * 1, rest)".

at proofs/codec/Roundtrip.v:123. Match the post-simpl shape directly:
[replace (n * 1) with n by lia]. The proof still closes with [Qed];
no Admitteds added.

Trace: REQ-12
---
 proofs/codec/Roundtrip.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/proofs/codec/Roundtrip.v b/proofs/codec/Roundtrip.v
index 9f83ba9..0fe38ca 100644
--- a/proofs/codec/Roundtrip.v
+++ b/proofs/codec/Roundtrip.v
@@ -119,7 +119,10 @@ Proof.
   assert (Nat.ltb n 128 = true) as Hltb.
   { apply Nat.ltb_lt. exact Hlt. }
   rewrite Hltb.
-  replace (0 + n * 1) with n by lia.
+  (* Rocq 9.0's [simpl] is more aggressive than v1.1.0's pin: it
+     reduces [0 + n * 1] to [n * 1] here, so the old [replace (0 + n * 1)]
+     pattern no longer matches. Match the post-simpl shape directly. *)
+  replace (n * 1) with n by lia.
   reflexivity.
 Qed.
 

From 47b45f6394cb2c4faeffd22be190cc4bd10296c9 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sun, 24 May 2026 19:32:29 +0200
Subject: [PATCH 05/16] fix(proofs): StackSignature rev_involutive orientation
 for Rocq 9.0
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

After the rules_rocq_rust toolchain bump, proofs/stack/StackSignature.v
line 214 fails with

  Unable to unify "rev (rev ?M768) = ?M768" with
                  "p0 :: ps = rev (rev (p0 :: ps))".

Rocq 9.0's `apply` no longer silently flips orientation when the goal
direction is reversed. The local proof obligation after
`rewrite <- Hrev` is `p0 :: ps = rev (rev (p0 :: ps))`, while
`rev_involutive : rev (rev l) = l` goes the other way — insert an
explicit `symmetry`. Same proof, same Qed, no Admitteds added.

Trace: REQ-12
---
 proofs/stack/StackSignature.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/stack/StackSignature.v b/proofs/stack/StackSignature.v
index c2b333f..dd535d6 100644
--- a/proofs/stack/StackSignature.v
+++ b/proofs/stack/StackSignature.v
@@ -211,7 +211,7 @@ Proof.
     (* Result is mkSig ([] ++ rev (y::ys)) r (match Fixed, k ...) *)
     (* rev (y::ys) = rev (rev (p0::ps)) = p0::ps *)
     replace (rev (y :: ys)) with (p0 :: ps)
-      by (rewrite <- Hrev; apply rev_involutive).
+      by (rewrite <- Hrev; symmetry; apply rev_involutive).
     simpl.
     destruct k; reflexivity.
 Qed.

From 9042f2e0acbac949936c9c9b70ea95b5b0774061 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Mon, 25 May 2026 06:32:21 +0200
Subject: [PATCH 06/16] fix(proofs): subdir-qualify Require Import paths for
 new rocq_library
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The new rules_rocq_rust rocq_library rule preserves subdirectory
hierarchy under the logical prefix:

  proofs/semantics/WasmSemantics.v  →  proofs.semantics.WasmSemantics
  proofs/simplify/ConstantFolding.v →  proofs.simplify.ConstantFolding

The old pin (307b65f) appears to have flattened these to plain
proofs.WasmSemantics / proofs.ConstantFolding, so every dependent
file used `From proofs Require Import X.`. Under the new rules
that resolves to logical path "proofs.X" with no .vo file at that
location and fails with:

  Error: Cannot find a physical path bound to logical path
         WasmSemantics with prefix proofs.

Update all 17 imports across 9 .v files to point at the correct
subdirectory:

- WasmSemantics / TermSemantics    → From proofs.semantics
- ConstantFolding / Identity /
  Bitwise / StrengthReduction      → From proofs.simplify

No proof bodies changed; only the module path qualifiers.

Trace: REQ-12
---
 proofs/Correctness.v                | 12 ++++++------
 proofs/semantics/TermSemantics.v    |  2 +-
 proofs/simplify/Bitwise.v           |  4 ++--
 proofs/simplify/ConstantFolding.v   |  4 ++--
 proofs/simplify/FusedOptimization.v |  4 ++--
 proofs/simplify/Identity.v          |  4 ++--
 proofs/simplify/StrengthReduction.v |  4 ++--
 7 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/proofs/Correctness.v b/proofs/Correctness.v
index 34b020e..58dafcf 100644
--- a/proofs/Correctness.v
+++ b/proofs/Correctness.v
@@ -15,12 +15,12 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
-From proofs Require Import ConstantFolding.
-From proofs Require Import Identity.
-From proofs Require Import Bitwise.
-From proofs Require Import StrengthReduction.
+From proofs.semantics Require Import WasmSemantics.
+From proofs.semantics Require Import TermSemantics.
+From proofs.simplify Require Import ConstantFolding.
+From proofs.simplify Require Import Identity.
+From proofs.simplify Require Import Bitwise.
+From proofs.simplify Require Import StrengthReduction.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/semantics/TermSemantics.v b/proofs/semantics/TermSemantics.v
index 1e5cf5d..426be7d 100644
--- a/proofs/semantics/TermSemantics.v
+++ b/proofs/semantics/TermSemantics.v
@@ -18,7 +18,7 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
+From proofs.semantics Require Import WasmSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Bitwise.v b/proofs/simplify/Bitwise.v
index 2affefe..1140c8c 100644
--- a/proofs/simplify/Bitwise.v
+++ b/proofs/simplify/Bitwise.v
@@ -18,8 +18,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From proofs.semantics Require Import WasmSemantics.
+From proofs.semantics Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/ConstantFolding.v b/proofs/simplify/ConstantFolding.v
index 9d64ae0..ff1e470 100644
--- a/proofs/simplify/ConstantFolding.v
+++ b/proofs/simplify/ConstantFolding.v
@@ -15,8 +15,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From proofs.semantics Require Import WasmSemantics.
+From proofs.semantics Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/FusedOptimization.v b/proofs/simplify/FusedOptimization.v
index 315a94e..4ba6d65 100644
--- a/proofs/simplify/FusedOptimization.v
+++ b/proofs/simplify/FusedOptimization.v
@@ -64,8 +64,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From proofs.semantics Require Import WasmSemantics.
+From proofs.semantics Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Identity.v b/proofs/simplify/Identity.v
index 65eba15..ee21aa8 100644
--- a/proofs/simplify/Identity.v
+++ b/proofs/simplify/Identity.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From proofs.semantics Require Import WasmSemantics.
+From proofs.semantics Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/StrengthReduction.v b/proofs/simplify/StrengthReduction.v
index 4243d94..3a0ba38 100644
--- a/proofs/simplify/StrengthReduction.v
+++ b/proofs/simplify/StrengthReduction.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import WasmSemantics.
-From proofs Require Import TermSemantics.
+From proofs.semantics Require Import WasmSemantics.
+From proofs.semantics Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.

From 3008dbb8283263d65309f1847be7edddb02b8936 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Mon, 25 May 2026 13:23:30 +0200
Subject: [PATCH 07/16] fix(proofs): StackSignature replace pattern after Rocq
 9.0 simpl unfolds rev

Follow-up to 47b45f6. That commit added a `symmetry` to fix the
orientation of [apply rev_involutive], but the proof still failed
one tactic later at line 216 with

  Unable to unify
    "Some {| params := p0 :: ps; results := r; kind := Fixed |}"
  with
    "Some {| params := rev ys ++ [y]; results := r; kind := Fixed |}".

Cause: Rocq 9.0's [simpl] above the [replace] is more eager than the
v1.1.0-era pin's, and it unfolds [rev (y :: ys)] definitionally to
[rev ys ++ [y]]. The old replace pattern [(rev (y :: ys))] then no
longer matches anything in the post-simpl goal, the replace silently
no-ops, and [destruct k; reflexivity] fails because the goal still
holds [rev ys ++ [y]] where the lemma statement has [p0 :: ps].

Match the post-simpl shape directly and route the proof obligation
through a [change] back to [rev (y :: ys)] (definitionally equal),
then apply the same rev-involutive identity.

Same Qed, no Admitteds added.

Trace: REQ-12
---
 proofs/stack/StackSignature.v | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/proofs/stack/StackSignature.v b/proofs/stack/StackSignature.v
index dd535d6..65ef44f 100644
--- a/proofs/stack/StackSignature.v
+++ b/proofs/stack/StackSignature.v
@@ -209,9 +209,14 @@ Proof.
     rewrite Hrev. simpl.
     (* Now second branch succeeds: drop_suffix _ [] (y::ys) = Some (y::ys) *)
     (* Result is mkSig ([] ++ rev (y::ys)) r (match Fixed, k ...) *)
-    (* rev (y::ys) = rev (rev (p0::ps)) = p0::ps *)
-    replace (rev (y :: ys)) with (p0 :: ps)
-      by (rewrite <- Hrev; symmetry; apply rev_involutive).
+    (* Rocq 9.0's [simpl] above unfolds [rev (y :: ys)] definitionally to
+       [rev ys ++ [y]], so we have to match the post-[simpl] shape rather
+       than the pre-[simpl] one the v1.1.0-era pin produced. The proof
+       obligation is still the same equality, just routed via a [change]
+       through the definitional unfolding of [rev]. *)
+    replace (rev ys ++ [y]) with (p0 :: ps)
+      by (change (rev ys ++ [y]) with (rev (y :: ys));
+          rewrite <- Hrev; symmetry; apply rev_involutive).
     simpl.
     destruct k; reflexivity.
 Qed.

From 672a4b56283b144123aa619ab2fae37bb81e08a7 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Tue, 26 May 2026 20:31:03 +0200
Subject: [PATCH 08/16] fix(proofs): tolerate Rocq 9.0 simpl pre-reducing
 Nat.sub_0_r at line 238
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

After 3008dbb closed compose_empty_left, compose_empty_right now fails
at line 238 with

  Error: Found no subterm matching "?M755 - 0" in the current goal.

Same root cause as the previous two simpl-eagerness fixes: Rocq 9.0's
[simpl] above the [rewrite] has already reduced [length (r0 :: rs) - 0]
to its [length] form, so [rewrite Nat.sub_0_r] has no subterm to match.

Wrap with [try] so the proof tolerates both simpl behaviours — the
v1.1.0-era pin (which left the [- 0] intact) and the new pin (which
eats it). No other tactics are changed; same Qed.

Trace: REQ-12
---
 proofs/stack/StackSignature.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/proofs/stack/StackSignature.v b/proofs/stack/StackSignature.v
index 65ef44f..9add419 100644
--- a/proofs/stack/StackSignature.v
+++ b/proofs/stack/StackSignature.v
@@ -234,8 +234,12 @@ Proof.
   - (* results = r0 :: rs *)
     (* drop_suffix _ [] (rev (r0::rs)) = Some (rev (r0::rs)) *)
     simpl.
-    (* skipn (length (r0::rs) - 0) [] = skipn _ [] = [] *)
-    rewrite Nat.sub_0_r.
+    (* Rocq 9.0's [simpl] is more aggressive than the v1.1.0-era pin:
+       it already reduces [length (r0 :: rs) - 0] to its [length]
+       form definitionally, so [rewrite Nat.sub_0_r] finds no subterm
+       to match. [try rewrite] keeps the proof robust against both
+       behaviours. *)
+    try rewrite Nat.sub_0_r.
     rewrite app_nil_r.
     rewrite rev_involutive.
     rewrite app_nil_r.

From 48341767866a8a20acb658f900b65533f9cbcb89 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Wed, 27 May 2026 05:41:47 +0200
Subject: [PATCH 09/16] fix(proofs): wrap remaining compose_empty_right
 rewrites with try
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Follow-up to 672a4b5. The new pin's Rocq 9.0 [simpl] keeps eating
the subterms each downstream [rewrite] wanted to match — first
[?M - 0], now [rev (rev ?M)]. Same pattern, same root cause: the
old pin left these untouched and the proof did explicit rewrites;
the new pin reduces them eagerly so the rewrites no-op-or-error.

Wrap every rewrite in the [compose_empty_right] non-empty branch
with [try], so the proof tolerates whichever way [simpl] settles
the term. If [simpl] reduced everything, the rewrites all no-op
and [destruct k; reflexivity] closes the residual goal directly;
if it left some shapes intact, the rewrites still fire.

Trace: REQ-12
---
 proofs/stack/StackSignature.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/proofs/stack/StackSignature.v b/proofs/stack/StackSignature.v
index 9add419..96ee734 100644
--- a/proofs/stack/StackSignature.v
+++ b/proofs/stack/StackSignature.v
@@ -240,9 +240,9 @@ Proof.
        to match. [try rewrite] keeps the proof robust against both
        behaviours. *)
     try rewrite Nat.sub_0_r.
-    rewrite app_nil_r.
-    rewrite rev_involutive.
-    rewrite app_nil_r.
+    try rewrite app_nil_r.
+    try rewrite rev_involutive.
+    try rewrite app_nil_r.
     destruct k; reflexivity.
 Qed.
 

From a198044fbc1c3e43a2230fe60d504e0b5cc4f6a2 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Wed, 27 May 2026 19:09:42 +0200
Subject: [PATCH 10/16] fix(proofs): correct From/Import split for
 subdir-qualified modules

My earlier 9042f2e change used the wrong half of the Coq import syntax:

  From proofs.semantics Require Import WasmSemantics.   (wrong)

`From X Require Import Y.` looks for module path `X.Y`, but `X` must
match an existing `-Q` prefix binding. The new rules_rocq_rust
`rocq_library` produces only the `proofs` prefix binding (from
`ctx.label.package`), not `proofs.semantics`. So coqc reports:

  Cannot find a physical path bound to logical path
  WasmSemantics with prefix proofs.semantics.

The subdir hierarchy belongs in the Import part, not the From part:

  From proofs Require Import semantics.WasmSemantics.   (right)

The `proofs` prefix matches the `-Q` binding; `semantics.WasmSemantics`
is the path *within* that prefix and resolves to the .vo at
`proofs/semantics/WasmSemantics.vo`.

Apply to all 17 imports across the 7 dependent files. Pure
text-level fix; no proof bodies touched.

Trace: REQ-12
---
 proofs/Correctness.v                | 12 ++++++------
 proofs/semantics/TermSemantics.v    |  2 +-
 proofs/simplify/Bitwise.v           |  4 ++--
 proofs/simplify/ConstantFolding.v   |  4 ++--
 proofs/simplify/FusedOptimization.v |  4 ++--
 proofs/simplify/Identity.v          |  4 ++--
 proofs/simplify/StrengthReduction.v |  4 ++--
 7 files changed, 17 insertions(+), 17 deletions(-)

diff --git a/proofs/Correctness.v b/proofs/Correctness.v
index 58dafcf..68a9cf6 100644
--- a/proofs/Correctness.v
+++ b/proofs/Correctness.v
@@ -15,12 +15,12 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs.semantics Require Import WasmSemantics.
-From proofs.semantics Require Import TermSemantics.
-From proofs.simplify Require Import ConstantFolding.
-From proofs.simplify Require Import Identity.
-From proofs.simplify Require Import Bitwise.
-From proofs.simplify Require Import StrengthReduction.
+From proofs Require Import semantics.WasmSemantics.
+From proofs Require Import semantics.TermSemantics.
+From proofs Require Import simplify.ConstantFolding.
+From proofs Require Import simplify.Identity.
+From proofs Require Import simplify.Bitwise.
+From proofs Require Import simplify.StrengthReduction.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/semantics/TermSemantics.v b/proofs/semantics/TermSemantics.v
index 426be7d..3c131fe 100644
--- a/proofs/semantics/TermSemantics.v
+++ b/proofs/semantics/TermSemantics.v
@@ -18,7 +18,7 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs.semantics Require Import WasmSemantics.
+From proofs Require Import semantics.WasmSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Bitwise.v b/proofs/simplify/Bitwise.v
index 1140c8c..8fdfc39 100644
--- a/proofs/simplify/Bitwise.v
+++ b/proofs/simplify/Bitwise.v
@@ -18,8 +18,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs.semantics Require Import WasmSemantics.
-From proofs.semantics Require Import TermSemantics.
+From proofs Require Import semantics.WasmSemantics.
+From proofs Require Import semantics.TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/ConstantFolding.v b/proofs/simplify/ConstantFolding.v
index ff1e470..66e5b11 100644
--- a/proofs/simplify/ConstantFolding.v
+++ b/proofs/simplify/ConstantFolding.v
@@ -15,8 +15,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs.semantics Require Import WasmSemantics.
-From proofs.semantics Require Import TermSemantics.
+From proofs Require Import semantics.WasmSemantics.
+From proofs Require Import semantics.TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/FusedOptimization.v b/proofs/simplify/FusedOptimization.v
index 4ba6d65..99c8546 100644
--- a/proofs/simplify/FusedOptimization.v
+++ b/proofs/simplify/FusedOptimization.v
@@ -64,8 +64,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs.semantics Require Import WasmSemantics.
-From proofs.semantics Require Import TermSemantics.
+From proofs Require Import semantics.WasmSemantics.
+From proofs Require Import semantics.TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Identity.v b/proofs/simplify/Identity.v
index ee21aa8..57b62c4 100644
--- a/proofs/simplify/Identity.v
+++ b/proofs/simplify/Identity.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs.semantics Require Import WasmSemantics.
-From proofs.semantics Require Import TermSemantics.
+From proofs Require Import semantics.WasmSemantics.
+From proofs Require Import semantics.TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/StrengthReduction.v b/proofs/simplify/StrengthReduction.v
index 3a0ba38..670628e 100644
--- a/proofs/simplify/StrengthReduction.v
+++ b/proofs/simplify/StrengthReduction.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs.semantics Require Import WasmSemantics.
-From proofs.semantics Require Import TermSemantics.
+From proofs Require Import semantics.WasmSemantics.
+From proofs Require Import semantics.TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.

From 277627fb57e4da26d2fb08403db524b4538002a1 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Thu, 28 May 2026 06:24:39 +0200
Subject: [PATCH 11/16] fix(proofs): reduce rev (rev rs ++ [r0]) in
 compose_empty_right
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The try-wrapped rewrites from 4834176 still left compose_empty_right
failing at line 246:

  Unable to unify
    "Some {| ...; results := r0 :: rs; ... |}"
  with
    "Some {| ...; results := rev (rev rs ++ [r0]); ... |}".

Rocq 9.0's simpl unfolds the *inner* rev (r0 :: rs) definitionally to
rev rs ++ [r0], so the results field becomes rev (rev rs ++ [r0]).
[rewrite rev_involutive] cannot fire — its pattern rev (rev ?M) does
not match rev (rev rs ++ [r0]) (the inner term is an append, not a
rev). The try-wrap therefore no-ops and the goal stays unreduced.

rev rs ++ [r0] is definitionally rev (r0 :: rs), so replace the field
with r0 :: rs and discharge via change + rev_involutive. Uses only
rev_involutive (known to resolve) and a definitional change — no
guess at possibly-renamed stdlib lemma names (rev_app_distr / rev_unit).

Trace: REQ-12
---
 proofs/stack/StackSignature.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/proofs/stack/StackSignature.v b/proofs/stack/StackSignature.v
index 96ee734..648f073 100644
--- a/proofs/stack/StackSignature.v
+++ b/proofs/stack/StackSignature.v
@@ -241,8 +241,15 @@ Proof.
        behaviours. *)
     try rewrite Nat.sub_0_r.
     try rewrite app_nil_r.
-    try rewrite rev_involutive.
-    try rewrite app_nil_r.
+    (* Rocq 9.0's [simpl] unfolds the inner [rev (r0 :: rs)] to
+       [rev rs ++ [r0]], leaving the results field as
+       [rev (rev rs ++ [r0])] — a shape [rewrite rev_involutive] cannot
+       match (its pattern is [rev (rev ?M)]). But [rev rs ++ [r0]] is
+       definitionally [rev (r0 :: rs)], so route through [change] and
+       close with involutivity. *)
+    replace (rev (rev rs ++ [r0])) with (r0 :: rs)
+      by (change (rev rs ++ [r0]) with (rev (r0 :: rs));
+          symmetry; apply rev_involutive).
     destruct k; reflexivity.
 Qed.
 

From 3640b982a07ee4a76c74e70da7a15273e6ac0a0f Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Thu, 28 May 2026 19:27:30 +0200
Subject: [PATCH 12/16] fix(proofs): split semantics library + prefix-agnostic
 Require Import
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Root cause of the recurring TermSemantics.v "Cannot find a physical
path bound to logical path WasmSemantics" error, found by reading the
new rocq_library impl (rules_rocq_rust@e4660cc1b,
rocq/private/rocq.bzl): each source's coqc action gets

  inputs = [src] + dep_vo_files + stdlib + ...

where dep_vo_files comes ONLY from `deps` (transitive_compiled). The
.vo files compiled from *sibling sources in the same library* are
never added as inputs to later compilations in that library. So in
the two-file :semantics target, TermSemantics.v was compiled without
WasmSemantics.vo present — no import syntax could fix that.

Two-part fix:

1. proofs/BUILD.bazel: split :semantics (WasmSemantics.v +
   TermSemantics.v) into two single-file rocq_library targets,
   :wasm_semantics and :term_semantics (deps = [:wasm_semantics]).
   The cross-file dependency now flows through `deps`, which DOES
   propagate the include path and wire the .vo as a compile input.
   Replace the :semantics alias pair + :semantics_test with the two
   real libraries and their _test targets (the names all_proofs_test
   already referenced — closing the stale test_suite warning too).

2. The dependent .v files now use plain `Require Import WasmSemantics.`
   (no `From proofs`). Plain Require resolves by logical-name suffix
   across every -Q loadpath, so it is invariant to whether the rule
   maps the .vo to `proofs.WasmSemantics` or
   `proofs.semantics.WasmSemantics` — the prefix ambiguity that caused
   two earlier failed attempts. All 17 imports across 7 files updated.

Trace: REQ-12
---
 proofs/BUILD.bazel                  | 38 +++++++++++++++++------------
 proofs/Correctness.v                | 12 ++++-----
 proofs/semantics/TermSemantics.v    |  2 +-
 proofs/simplify/Bitwise.v           |  4 +--
 proofs/simplify/ConstantFolding.v   |  4 +--
 proofs/simplify/FusedOptimization.v |  4 +--
 proofs/simplify/Identity.v          |  4 +--
 proofs/simplify/StrengthReduction.v |  4 +--
 8 files changed, 39 insertions(+), 33 deletions(-)

diff --git a/proofs/BUILD.bazel b/proofs/BUILD.bazel
index 142c96c..25e09ce 100644
--- a/proofs/BUILD.bazel
+++ b/proofs/BUILD.bazel
@@ -4,32 +4,38 @@ load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library", "rocq_proof_test")
 # Core Semantic Model
 # =============================================================================
 
-# WebAssembly and Term semantics (combined for module resolution)
+# WebAssembly semantics — base layer, no intra-proof dependencies.
 rocq_library(
-    name = "semantics",
-    srcs = [
-        "semantics/WasmSemantics.v",
-        "semantics/TermSemantics.v",
-    ],
-    visibility = ["//visibility:public"],
-)
-
-# Aliases for backwards compatibility
-alias(
     name = "wasm_semantics",
-    actual = ":semantics",
+    srcs = ["semantics/WasmSemantics.v"],
     visibility = ["//visibility:public"],
 )
 
-alias(
+# Term (ISLE) semantics — depends on WasmSemantics.
+#
+# Kept as a SEPARATE rocq_library (rather than a second src in the
+# WasmSemantics library) because the rules_rocq_rust rocq_library rule
+# (pulseengine/rules_rocq_rust@e4660cc1b) only wires a compiled .vo as a
+# coqc input to a *dependent* library through `deps`. Sibling sources
+# inside a single multi-file library do NOT see each other's .vo, so
+# TermSemantics could never `Require Import WasmSemantics` when both
+# lived in one `:semantics` target. Splitting routes the dependency
+# through `deps`, which propagates the include path and the .vo input.
+rocq_library(
     name = "term_semantics",
-    actual = ":semantics",
+    srcs = ["semantics/TermSemantics.v"],
+    deps = [":wasm_semantics"],
     visibility = ["//visibility:public"],
 )
 
 rocq_proof_test(
-    name = "semantics_test",
-    deps = [":semantics"],
+    name = "wasm_semantics_test",
+    deps = [":wasm_semantics"],
+)
+
+rocq_proof_test(
+    name = "term_semantics_test",
+    deps = [":term_semantics"],
 )
 
 # =============================================================================
diff --git a/proofs/Correctness.v b/proofs/Correctness.v
index 68a9cf6..164526f 100644
--- a/proofs/Correctness.v
+++ b/proofs/Correctness.v
@@ -15,12 +15,12 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import semantics.WasmSemantics.
-From proofs Require Import semantics.TermSemantics.
-From proofs Require Import simplify.ConstantFolding.
-From proofs Require Import simplify.Identity.
-From proofs Require Import simplify.Bitwise.
-From proofs Require Import simplify.StrengthReduction.
+Require Import WasmSemantics.
+Require Import TermSemantics.
+Require Import ConstantFolding.
+Require Import Identity.
+Require Import Bitwise.
+Require Import StrengthReduction.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/semantics/TermSemantics.v b/proofs/semantics/TermSemantics.v
index 3c131fe..c72ff03 100644
--- a/proofs/semantics/TermSemantics.v
+++ b/proofs/semantics/TermSemantics.v
@@ -18,7 +18,7 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import semantics.WasmSemantics.
+Require Import WasmSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Bitwise.v b/proofs/simplify/Bitwise.v
index 8fdfc39..d7f1afa 100644
--- a/proofs/simplify/Bitwise.v
+++ b/proofs/simplify/Bitwise.v
@@ -18,8 +18,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import semantics.WasmSemantics.
-From proofs Require Import semantics.TermSemantics.
+Require Import WasmSemantics.
+Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/ConstantFolding.v b/proofs/simplify/ConstantFolding.v
index 66e5b11..9843bf2 100644
--- a/proofs/simplify/ConstantFolding.v
+++ b/proofs/simplify/ConstantFolding.v
@@ -15,8 +15,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import semantics.WasmSemantics.
-From proofs Require Import semantics.TermSemantics.
+Require Import WasmSemantics.
+Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/FusedOptimization.v b/proofs/simplify/FusedOptimization.v
index 99c8546..cda7133 100644
--- a/proofs/simplify/FusedOptimization.v
+++ b/proofs/simplify/FusedOptimization.v
@@ -64,8 +64,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import semantics.WasmSemantics.
-From proofs Require Import semantics.TermSemantics.
+Require Import WasmSemantics.
+Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Identity.v b/proofs/simplify/Identity.v
index 57b62c4..66eff7c 100644
--- a/proofs/simplify/Identity.v
+++ b/proofs/simplify/Identity.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import semantics.WasmSemantics.
-From proofs Require Import semantics.TermSemantics.
+Require Import WasmSemantics.
+Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/StrengthReduction.v b/proofs/simplify/StrengthReduction.v
index 670628e..8624c8d 100644
--- a/proofs/simplify/StrengthReduction.v
+++ b/proofs/simplify/StrengthReduction.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-From proofs Require Import semantics.WasmSemantics.
-From proofs Require Import semantics.TermSemantics.
+Require Import WasmSemantics.
+Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.

From fb2a0ba32da279fe348da9467cb0aec9ec195d80 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Fri, 29 May 2026 06:07:04 +0200
Subject: [PATCH 13/16] fix(proofs): clear residual ++ [] after rev reduction
 in compose_empty_right

The semantics library split (3640b98) cleared the import errors; the
build now reaches StackSignature.v again, failing at the [replace]
block I added in 277627f:

  Unable to unify
    "Some {| ...; results := r0 :: rs; ... |}"
  with
    "Some {| ...; results := (r0 :: rs) ++ []; ... |}".

The [replace] correctly reduced [rev (rev rs ++ [r0])] to [r0 :: rs],
but the surrounding [++ results empty_sig] = [++ []] survived (the
pre-replace [try rewrite app_nil_r] fired on a different occurrence /
shape). Add a [try rewrite app_nil_r] after the replace to discharge
the residual append before [destruct k; reflexivity].

Trace: REQ-12
---
 proofs/stack/StackSignature.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/proofs/stack/StackSignature.v b/proofs/stack/StackSignature.v
index 648f073..2edb8ae 100644
--- a/proofs/stack/StackSignature.v
+++ b/proofs/stack/StackSignature.v
@@ -250,6 +250,9 @@ Proof.
     replace (rev (rev rs ++ [r0])) with (r0 :: rs)
       by (change (rev rs ++ [r0]) with (rev (r0 :: rs));
           symmetry; apply rev_involutive).
+    (* The results field is [(r0 :: rs) ++ results empty_sig] = [_ ++ []];
+       clear the residual append left after the rev reduction. *)
+    try rewrite app_nil_r.
     destruct k; reflexivity.
 Qed.
 

From 48ed53d704be50dd4eb5288857e2892a4cfcad6a Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Fri, 29 May 2026 19:42:22 +0200
Subject: [PATCH 14/16] fix(proofs): adopt meld include_path idiom for
 inter-file rocq deps
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Empirical fix, modelled on the working pulseengine/meld proofs
(proofs/spec/BUILD.bazel) which solve exactly this inter-file
dependency case under the same rules_rocq_rust rule.

The meld idiom, applied here:
  1. one rocq_library per .v file (already done in the prior split);
  2. inter-file deps wired through `deps` (already done);
  3. a SHARED explicit include_path on every library in the group
     (meld uses "MeldSpec"; loom now uses "LoomProofs"); and
  4. cross-file imports written `From <Prefix> Require Import <Module>`.

Why the earlier attempts failed: the rules_rocq_rust rocq_library
rule maps a library's .vo under `-Q <output_dir> <include_path>`,
where include_path defaults to the BUILD package path. loom's .v
files live in SUBDIRECTORIES of the proofs/ package, so the
package-derived prefix did not line up with where the .vo landed,
and neither plain `Require Import` nor a `From proofs[.subdir]`
guess could resolve the dependency's module. A shared explicit
include_path gives every library a stable logical prefix independent
of Bazel's per-target output-dir layout — which is precisely why meld
sets it on every spec library.

Changes:
- proofs/BUILD.bazel: include_path = "LoomProofs" on all 8 libraries
  in the inter-dependent group (wasm_semantics, term_semantics, the
  five simplify libs, correctness). The standalone glob libraries
  (stack/codec/isle — no cross-proof deps) are unchanged.
- 17 cross-proof imports across 7 .v files rewritten to
  `From LoomProofs Require Import <Module>`.

stack/codec/isle proofs are independent single-file groups with no
inter-file deps, so they keep the plain glob layout.

Trace: REQ-12
---
 proofs/BUILD.bazel                  | 35 ++++++++++++++++++++---------
 proofs/Correctness.v                | 12 +++++-----
 proofs/semantics/TermSemantics.v    |  2 +-
 proofs/simplify/Bitwise.v           |  4 ++--
 proofs/simplify/ConstantFolding.v   |  4 ++--
 proofs/simplify/FusedOptimization.v |  4 ++--
 proofs/simplify/Identity.v          |  4 ++--
 proofs/simplify/StrengthReduction.v |  4 ++--
 8 files changed, 42 insertions(+), 27 deletions(-)

diff --git a/proofs/BUILD.bazel b/proofs/BUILD.bazel
index 25e09ce..d083e69 100644
--- a/proofs/BUILD.bazel
+++ b/proofs/BUILD.bazel
@@ -5,26 +5,35 @@ load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library", "rocq_proof_test")
 # =============================================================================
 
 # WebAssembly semantics — base layer, no intra-proof dependencies.
+#
+# The whole inter-dependent proof group (semantics + simplify +
+# correctness) shares the logical prefix `LoomProofs` via include_path,
+# and the .v files import each other as `From LoomProofs Require Import
+# <Module>`. This is the idiom the pulseengine/meld proofs use
+# (proofs/spec/BUILD.bazel: include_path = "MeldSpec" on every library,
+# `From MeldSpec Require Import ...`). It is required because the
+# rules_rocq_rust rocq_library rule (@e4660cc1b) maps a library's .vo
+# under `-Q <output_dir> <include_path>`; a shared explicit include_path
+# gives every library a STABLE logical prefix independent of Bazel's
+# per-target output-dir layout, so a dependent's `From LoomProofs
+# Require Import WasmSemantics` resolves against the dep's .vo wired in
+# through `deps`. The package-derived default prefix did not, because
+# the .v files live in subdirectories of the BUILD package.
 rocq_library(
     name = "wasm_semantics",
     srcs = ["semantics/WasmSemantics.v"],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
-# Term (ISLE) semantics — depends on WasmSemantics.
-#
-# Kept as a SEPARATE rocq_library (rather than a second src in the
-# WasmSemantics library) because the rules_rocq_rust rocq_library rule
-# (pulseengine/rules_rocq_rust@e4660cc1b) only wires a compiled .vo as a
-# coqc input to a *dependent* library through `deps`. Sibling sources
-# inside a single multi-file library do NOT see each other's .vo, so
-# TermSemantics could never `Require Import WasmSemantics` when both
-# lived in one `:semantics` target. Splitting routes the dependency
-# through `deps`, which propagates the include path and the .vo input.
+# Term (ISLE) semantics — depends on WasmSemantics. One library per .v
+# file; the cross-file dependency is wired through `deps` (which makes
+# the dep's .vo a coqc input and adds its -Q loadpath).
 rocq_library(
     name = "term_semantics",
     srcs = ["semantics/TermSemantics.v"],
     deps = [":wasm_semantics"],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -50,6 +59,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -66,6 +76,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -82,6 +93,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -98,6 +110,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -117,6 +130,7 @@ rocq_library(
         ":wasm_semantics",
         ":term_semantics",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
@@ -140,6 +154,7 @@ rocq_library(
         ":bitwise",
         ":strength_reduction",
     ],
+    include_path = "LoomProofs",
     visibility = ["//visibility:public"],
 )
 
diff --git a/proofs/Correctness.v b/proofs/Correctness.v
index 164526f..4651522 100644
--- a/proofs/Correctness.v
+++ b/proofs/Correctness.v
@@ -15,12 +15,12 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-Require Import WasmSemantics.
-Require Import TermSemantics.
-Require Import ConstantFolding.
-Require Import Identity.
-Require Import Bitwise.
-Require Import StrengthReduction.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
+From LoomProofs Require Import ConstantFolding.
+From LoomProofs Require Import Identity.
+From LoomProofs Require Import Bitwise.
+From LoomProofs Require Import StrengthReduction.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/semantics/TermSemantics.v b/proofs/semantics/TermSemantics.v
index c72ff03..b583813 100644
--- a/proofs/semantics/TermSemantics.v
+++ b/proofs/semantics/TermSemantics.v
@@ -18,7 +18,7 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-Require Import WasmSemantics.
+From LoomProofs Require Import WasmSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Bitwise.v b/proofs/simplify/Bitwise.v
index d7f1afa..744bf60 100644
--- a/proofs/simplify/Bitwise.v
+++ b/proofs/simplify/Bitwise.v
@@ -18,8 +18,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-Require Import WasmSemantics.
-Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/ConstantFolding.v b/proofs/simplify/ConstantFolding.v
index 9843bf2..e394683 100644
--- a/proofs/simplify/ConstantFolding.v
+++ b/proofs/simplify/ConstantFolding.v
@@ -15,8 +15,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-Require Import WasmSemantics.
-Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/FusedOptimization.v b/proofs/simplify/FusedOptimization.v
index cda7133..cfcd7ce 100644
--- a/proofs/simplify/FusedOptimization.v
+++ b/proofs/simplify/FusedOptimization.v
@@ -64,8 +64,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-Require Import WasmSemantics.
-Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/Identity.v b/proofs/simplify/Identity.v
index 66eff7c..cb7af86 100644
--- a/proofs/simplify/Identity.v
+++ b/proofs/simplify/Identity.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-Require Import WasmSemantics.
-Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.
diff --git a/proofs/simplify/StrengthReduction.v b/proofs/simplify/StrengthReduction.v
index 8624c8d..387f16a 100644
--- a/proofs/simplify/StrengthReduction.v
+++ b/proofs/simplify/StrengthReduction.v
@@ -20,8 +20,8 @@ From Stdlib Require Import Arith.
 From Stdlib Require Import List.
 From Stdlib Require Import ZArith.
 From Stdlib Require Import Lia.
-Require Import WasmSemantics.
-Require Import TermSemantics.
+From LoomProofs Require Import WasmSemantics.
+From LoomProofs Require Import TermSemantics.
 Import ListNotations.
 
 Open Scope Z_scope.

From d609a316039c07a0253e137b196c08ba1f662444 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 30 May 2026 07:30:07 +0200
Subject: [PATCH 15/16] fix(proofs): Roundtrip.v Rocq 9.0 simpl/rewrite nits
 (locally verified)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Two mechanical Rocq-9.0 fixes in proofs/codec/Roundtrip.v, both
verified locally via `bazel build //proofs:codec_proofs` (now PASSES)
using the nix-hermetic Rocq 9.0.1 toolchain:

- functypes_roundtrip_n (was line 551): Rocq 9.0's `simpl` unfolds the
  `decode_functype` Definition itself, leaving no `decode_functype (_)`
  subterm for `rewrite functype_roundtrip`. Use
  `cbn [length encode_functypes decode_functypes_n]` so the structural
  fixpoints unfold but `decode_functype` stays folded for the rewrite.
- roundtrip_identity (was line 646): `rewrite <- !app_assoc` (one-or-
  more) errors because 9.0's `simpl` already right-associates the
  section appends. Changed to `<- ?app_assoc` (zero-or-more): a no-op
  when simpl already normalized, still correct otherwise.

Verified locally: codec_proofs, stack_proofs, isle_proofs all build.
TermSemantics.v is a separate, deeper issue (see PR discussion) — not
touched here.

Trace: REQ-12
---
 proofs/codec/Roundtrip.v | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/proofs/codec/Roundtrip.v b/proofs/codec/Roundtrip.v
index 0fe38ca..62b7479 100644
--- a/proofs/codec/Roundtrip.v
+++ b/proofs/codec/Roundtrip.v
@@ -547,7 +547,13 @@ Theorem functypes_roundtrip_n : forall fts rest,
 Proof.
   induction fts as [|ft fts IH]; intros rest.
   - simpl. reflexivity.
-  - simpl. rewrite <- app_assoc.
+  - (* Rocq 9.0's [simpl] unfolds the [decode_functype] Definition itself,
+       leaving no [decode_functype (...)] subterm for [functype_roundtrip]
+       to rewrite. Use [cbn] restricted to the structural fixpoints
+       ([length], [encode_functypes], [decode_functypes_n]) so the
+       [decode_functype] CALL is exposed but stays folded. *)
+    cbn [length encode_functypes decode_functypes_n].
+    rewrite <- app_assoc.
     rewrite functype_roundtrip.
     rewrite IH. reflexivity.
 Qed.
@@ -637,7 +643,11 @@ Theorem roundtrip_identity : forall m : ScopedModule,
 Proof.
   intros [ts fs pt].
   unfold encode_scoped, decode_scoped. simpl.
-  rewrite <- !app_assoc.
+  (* Rocq 9.0's [simpl] already right-associates the section appends, so
+     [<- !app_assoc] (one-or-more) finds nothing and errors. [?] makes
+     the reassociation zero-or-more — a no-op when [simpl] already did it,
+     still correct on a pin where it didn't. *)
+  rewrite <- ?app_assoc.
   rewrite leb128_roundtrip. simpl.
   rewrite functypes_roundtrip_n. simpl.
   rewrite leb128_roundtrip. simpl.

From 3789467c513499f1fb0ed2f895959a628d1f9804 Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 30 May 2026 07:43:08 +0200
Subject: [PATCH 16/16] proofs(wip): HasType + canonical_forms foundation for
 TermSemantics (#141)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Locally-verified foundation for fixing simplify_preserves_semantics
(per the Option-A well-typedness decision). Both new pieces compile
clean under the nix-hermetic Rocq 9.0 toolchain (verified: the build
error remains only at the pre-existing theorem below them):

- HasType : Term -> ValueType : a 42-rule static typing relation
  mirroring wasm. i64 comparisons produce TI32 even on TI64 operands;
  TDrop/TNop produce no value and so have no rule (they always TRFail).
- canonical_forms : HasType t ty -> a well-typed term evaluates to a
  value of its type (never TRFail), by induction on the derivation.

NOT yet done (theorem rework deferred — see PR discussion): the
identity arms (x+0=x, …) need a SECOND invariant beyond well-typedness
— a wrappedness invariant — because a TI32Const may hold an unwrapped
Z, making eval(x+0)=VI32(wrap32 v) <> VI32 v. Reworking the theorem
also changes its signature (adds the HasType hypothesis), which ripples
into the callers in Correctness.v and Identity.v. The old theorem is
left intact (still failing at its TI32Add case) rather than Admitted,
because its current statement `forall t, term_equiv t (simplify t)` is
FALSE and must not be admitted.

stack/codec/isle proof targets remain green (committed in d609a31).

Trace: REQ-12
---
 proofs/semantics/TermSemantics.v | 93 ++++++++++++++++++++++++++++++++
 1 file changed, 93 insertions(+)

diff --git a/proofs/semantics/TermSemantics.v b/proofs/semantics/TermSemantics.v
index b583813..05ce38c 100644
--- a/proofs/semantics/TermSemantics.v
+++ b/proofs/semantics/TermSemantics.v
@@ -939,6 +939,99 @@ Qed.
     adding a precondition that all term values are wrapped, or by having
     TI32Const always store wrapped values.
 *)
+(** * Well-typedness (loom#141 / TermSemantics fix)
+
+    [simplify]'s identity arms (x+0=x, 0+x=x, x-0=x, …) drop the zero
+    operand WITHOUT a type check, so on a mixed-width term the [Term]
+    type permits but well-typed wasm never produces — e.g.
+    [TI32Add (TI32Const 0) (TI64Const z)] — the original [eval_term]
+    traps ([TRFail], operands aren't both [VI32]) while the simplified
+    form yields [VI64 z]. So [simplify_preserves_semantics] is FALSE for
+    arbitrary terms. We restrict it to well-typed terms via [HasType],
+    which mirrors wasm's static typing: every operator constrains its
+    operands' types and fixes its result type (comparisons produce i32
+    even on i64 operands; [TDrop]/[TNop] produce no value and so have no
+    [HasType] rule). *)
+Inductive HasType : Term -> ValueType -> Prop :=
+  (* Constants *)
+  | HT_I32Const : forall v, HasType (TI32Const v) TI32
+  | HT_I64Const : forall v, HasType (TI64Const v) TI64
+  (* i32 arithmetic + bitwise + shifts: (i32, i32) -> i32 *)
+  | HT_I32Add  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Add l r) TI32
+  | HT_I32Sub  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Sub l r) TI32
+  | HT_I32Mul  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Mul l r) TI32
+  | HT_I32And  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32And l r) TI32
+  | HT_I32Or   : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Or l r) TI32
+  | HT_I32Xor  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Xor l r) TI32
+  | HT_I32Shl  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Shl l r) TI32
+  | HT_I32ShrS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32ShrS l r) TI32
+  | HT_I32ShrU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32ShrU l r) TI32
+  (* i64 arithmetic + bitwise + shifts: (i64, i64) -> i64 *)
+  | HT_I64Add  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Add l r) TI64
+  | HT_I64Sub  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Sub l r) TI64
+  | HT_I64Mul  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Mul l r) TI64
+  | HT_I64And  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64And l r) TI64
+  | HT_I64Or   : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Or l r) TI64
+  | HT_I64Xor  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Xor l r) TI64
+  | HT_I64Shl  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Shl l r) TI64
+  | HT_I64ShrS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64ShrS l r) TI64
+  | HT_I64ShrU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64ShrU l r) TI64
+  (* i32 comparisons: (i32, i32) -> i32 *)
+  | HT_I32Eq  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Eq l r) TI32
+  | HT_I32Ne  : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32Ne l r) TI32
+  | HT_I32LtS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LtS l r) TI32
+  | HT_I32LtU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LtU l r) TI32
+  | HT_I32GtS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GtS l r) TI32
+  | HT_I32GtU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GtU l r) TI32
+  | HT_I32LeS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LeS l r) TI32
+  | HT_I32LeU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32LeU l r) TI32
+  | HT_I32GeS : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GeS l r) TI32
+  | HT_I32GeU : forall l r, HasType l TI32 -> HasType r TI32 -> HasType (TI32GeU l r) TI32
+  | HT_I32Eqz : forall t, HasType t TI32 -> HasType (TI32Eqz t) TI32
+  (* i64 comparisons: (i64, i64) -> i32  (result is i32!) *)
+  | HT_I64Eq  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Eq l r) TI32
+  | HT_I64Ne  : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64Ne l r) TI32
+  | HT_I64LtS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LtS l r) TI32
+  | HT_I64LtU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LtU l r) TI32
+  | HT_I64GtS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GtS l r) TI32
+  | HT_I64GtU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GtU l r) TI32
+  | HT_I64LeS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LeS l r) TI32
+  | HT_I64LeU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64LeU l r) TI32
+  | HT_I64GeS : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GeS l r) TI32
+  | HT_I64GeU : forall l r, HasType l TI64 -> HasType r TI64 -> HasType (TI64GeU l r) TI32
+  | HT_I64Eqz : forall t, HasType t TI64 -> HasType (TI64Eqz t) TI32.
+
+(** Canonical forms: a well-typed term evaluates to a value of its type
+    (never [TRFail]). Proven by induction on the typing derivation; each
+    operator case uses the IH to fix operand shapes, eliminating the
+    [TRFail] arms of [eval_term]. *)
+Lemma canonical_forms : forall t ty,
+  HasType t ty ->
+  (ty = TI32 -> exists a, eval_term t = TROk (VI32 a)) /\
+  (ty = TI64 -> exists a, eval_term t = TROk (VI64 a)).
+Proof.
+  intros t ty H.
+  induction H; split; intros Hty; try discriminate Hty; simpl;
+    repeat match goal with
+           | [ H : _ /\ _ |- _ ] => destruct H
+           end;
+    (* discharge the i32/i64 selectors of each IH using the typing *)
+    repeat match goal with
+           | [ H : TI32 = TI32 -> _ |- _ ] => specialize (H eq_refl)
+           | [ H : TI64 = TI64 -> _ |- _ ] => specialize (H eq_refl)
+           | [ H : TI64 = TI32 -> _ |- _ ] => clear H
+           | [ H : TI32 = TI64 -> _ |- _ ] => clear H
+           end;
+    repeat match goal with
+           | [ H : exists a, _ |- _ ] => destruct H
+           end;
+    (* rewrite operand evaluations, then the eval match reduces *)
+    repeat match goal with
+           | [ H : eval_term _ = _ |- _ ] => rewrite H
+           end;
+    eauto.
+Qed.
+
 Theorem simplify_preserves_semantics : forall t,
   term_equiv t (simplify t).
 Proof.