[hermes] Update some integration tests

tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml

@@ -4,5 +4,6 @@ Behavior: Asserts that `fn theorem()`, `fn match()`, etc. are strictly escaped i
 """
 
 [test]
-expected_status = "failure"
+# FIXME(#3089): This should succeed
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry"]

tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml

@@ -4,5 +4,6 @@ Behavior: Utilizes explicit zero-sized structs and the common `()` unit type to
 """
 
 [test]
-expected_status = "failure"
-args = ["verify", "--allow-sorry"]
+# FIXME(#3089): This should succeed.
+expected_status = "known_bug"
+args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]

tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs

@@ -1,16 +1,21 @@
-
+/// ```hermes
+/// isValid self := True
+/// ```
 pub struct Empty {}
 
+/// ```hermes
+/// isValid self := True
+/// ```
 pub struct WrapUnit {
     pub f: (),
 }
 
-/// ```lean, hermes
-/// proof (h_progress):
-///   sorry
-/// proof context:
-///   have h_foo : True := True.intro
+/// ```hermes
+/// ensures: True
 /// ```
 pub fn unit_arg(_: ()) {}
 
+/// ```hermes
+/// ensures: True
+/// ```
 pub fn unit_ret() -> () {}

tools/hermes/tests/fixtures/is_valid_verification/hermes.toml

@@ -1,6 +1,6 @@
 description = """
 Purpose: Exercises end-to-end Lean verification integration evaluating `isValid` invariants.
-Behavior: Uses `--verify` to trigger Lean analysis on the extracted logic. Confirms that purposefully faulty initialization states correctly drive Lean to trip the `Decidable` invariant logic, reporting "failed to synthesize" through Hermes.
+Behavior: Confirms that purposefully faulty initialization states correctly drive Lean to trip the `Decidable` invariant logic, reporting "failed to synthesize" through Hermes.
 """
 
 [test]

tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml

@@ -3,6 +3,10 @@ Purpose: Validates diagnostics resolution pointing to canonicalized symlinks.
 Behavior: Provides Charon errors mapped to an original `untransformed.rs` target spanning behind a symlink. Ensures Hermes resolves and prints the logical/canonical code appropriately.
 """
 
+# FIXME(#3089): It looks like this test *originally* correctly exercised symlink
+# logic, but it doesn't anymore. We should fix this to ensure it actualy
+# uses symlinks.
+
 [test]
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]

tools/hermes/tests/fixtures/multiple_errors/hermes.toml

@@ -1,7 +1,4 @@
-description = """
-Purpose: Checks aggregation for widespread compilation failures.
-Behavior: Embeds syntax issues in two independent files (`a.rs`, `b.rs`). Exercises the diagnostic collector to aggregate and uniformly render the batch of distinct parsing errors.
-"""
+description = "Tests that syntax errors across multiple files are all reported"
 
 [test]
 stderr_file = "expected.stderr"

tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr

@@ -7,7 +7,7 @@
   │ `unsafe` functions.
    ╭─[[PROJECT_ROOT]/src/lib.rs:2:1]
  1 │ /// ```hermes
- 2 │ /// requires: true
+ 2 │ /// requires: True
    · ─────────┬────────
    ·          ╰── problematic block
  3 │ /// ```
@@ -40,4 +40,17 @@
  14 │ /// ```
     ╰────
 
-Error: Aborting due to 3 previous errors.
+
+[Hermes Error] hermes::doc_block
+
+  × Documentation block error: `requires` sections are only permitted on
+  │ `unsafe` functions.
+    ╭─[[PROJECT_ROOT]/src/lib.rs:18:1]
+ 17 │ /// ```hermes
+ 18 │ /// requires(h_true): True
+    · ─────────────┬────────────
+    ·              ╰── problematic block
+ 19 │ /// ```
+    ╰────
+
+Error: Aborting due to 4 previous errors.

tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml

@@ -1,7 +1,4 @@
-description = """
-Purpose: Verify that `requires` blocks are strictly rejected on safe functions.
-Behavior: Hermes parses the file, encounters `requires` on safe functions, and errors out pointing to the specific spans.
-"""
+description = "Verify that `requires` blocks are rejected on safe functions."
 
 [test]
 args = ["verify"]

tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs

@@ -1,5 +1,5 @@
 /// ```hermes
-/// requires: true
+/// requires: True
 /// ```
 pub fn safe_with_requires() {}
 
@@ -13,3 +13,8 @@ pub fn multiple_requires_safe(x: u32, y: u32) {}
 /// requires:
 /// ```
 pub fn empty_requires_safe() {}
+
+/// ```hermes
+/// requires(h_true): True
+/// ```
+pub fn named_requires_safe() {}

tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml

@@ -3,6 +3,9 @@ Purpose: Tests UI robustness handling invalid JSON interlacing from build script
 Behavior: Prints invalid JSON payloads before emitting a valid `compiler-artifact` blob. Ensures Hermes' diagnostic collector discards garbage outputs without panicking.
 """
 
+# FIXME(#3089): Hermes doesn't panic, but it also doesn't seem to interpret the
+# JSON payload, instead passing it to stderr verbatim.
+
 [test]
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]