[hermes] Update some integration tests

Delete some obsolete tests. Mark some tests as `FIXME`.

gherrit-pr-id: Gftcay6e46fu54jc6ytsszqb3b4rah7dj

Author: joshlf

tools/hermes/tests/fixtures/design_doc/expected.stderr

@@ -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/design_doc/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/design_doc/source/Cargo.toml

@@ -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() -> () {}