From d3ff7eeb006b1d94f97756f8758e2d653e58644d Mon Sep 17 00:00:00 2001
From: Joshua Liebow-Feeser <joshlf@google.com>
Date: Wed, 4 Feb 2026 04:13:19 +0000
Subject: [PATCH] [WIP] --start-with

gherrit-pr-id: Gbeca6e8c6a2f4e776c00719d86c9eabf4f63fe2e
---
 .../tests/cases/success/repro_box_anyhow.rs   | 25 +++++++++++++++++++
 .../tests/cases/success/repro_box_branch.rs   | 20 +++++++++++++++
 .../tests/cases/success/repro_dyn_trait.rs    | 16 ++++++++++++
 3 files changed, 61 insertions(+)
 create mode 100644 tools/hermes/tests/cases/success/repro_box_anyhow.rs
 create mode 100644 tools/hermes/tests/cases/success/repro_box_branch.rs
 create mode 100644 tools/hermes/tests/cases/success/repro_dyn_trait.rs

diff --git a/tools/hermes/tests/cases/success/repro_box_anyhow.rs b/tools/hermes/tests/cases/success/repro_box_anyhow.rs
new file mode 100644
index 0000000000..edc2d6a6b9
--- /dev/null
+++ b/tools/hermes/tests/cases/success/repro_box_anyhow.rs
@@ -0,0 +1,25 @@
+
+///@ lean spec foo(x : U32)
+///@ ensures |ret| ret.val = x.val
+///@ proof
+///@   simp [foo]
+pub fn foo(x: u32) -> u32 {
+    x
+}
+
+pub fn trigger_box_error(fail: bool) -> Result<(), Box<dyn std::fmt::Debug>> {
+    let e = if fail {
+        Box::new("failed")
+    } else {
+        Box::new("succeeded")
+    };
+    if fail {
+        return Err(e);
+    }
+    Ok(())
+}
+
+fn main() {
+    let _ = foo(42);
+    let _ = trigger_box_error(true);
+}
diff --git a/tools/hermes/tests/cases/success/repro_box_branch.rs b/tools/hermes/tests/cases/success/repro_box_branch.rs
new file mode 100644
index 0000000000..4d94d5be83
--- /dev/null
+++ b/tools/hermes/tests/cases/success/repro_box_branch.rs
@@ -0,0 +1,20 @@
+///@ lean spec foo(x : U32)
+///@ ensures |ret| ret.val = x.val
+///@ proof
+///@   simp [foo]
+pub fn foo(x: u32) -> u32 {
+    x
+}
+
+pub fn trigger_branch_box(cond: bool) -> Box<u32> {
+    if cond {
+        Box::new(1)
+    } else {
+        Box::new(2)
+    }
+}
+
+fn main() {
+    foo(42);
+    trigger_branch_box(true);
+}
diff --git a/tools/hermes/tests/cases/success/repro_dyn_trait.rs b/tools/hermes/tests/cases/success/repro_dyn_trait.rs
new file mode 100644
index 0000000000..2987fb1902
--- /dev/null
+++ b/tools/hermes/tests/cases/success/repro_dyn_trait.rs
@@ -0,0 +1,16 @@
+///@ lean spec foo(x : U32)
+///@ ensures |ret| ret.val = x.val
+///@ proof
+///@   simp [foo]
+pub fn foo(x: u32) -> u32 {
+    x
+}
+
+pub fn trigger_dyn_trait() {
+    let _x: Box<dyn std::fmt::Debug> = Box::new(42);
+}
+
+fn main() {
+    foo(42);
+    trigger_dyn_trait();
+}