[hermes] Fix more integration tests

tools/hermes/examples/const_generics.rs

@@ -1,4 +1,15 @@
-/// ```lean, hermes, spec
+/// ```hermes
+/// isValid self := N > 0
+/// ```
+pub struct ConstGen<const N: usize>;
+
+/// ```hermes
+/// isSafe : N > 0
+/// ```
+pub unsafe trait ConstTrait<const N: usize> {}
+
+/// ```hermes
+/// ensures: if N.val = 0 then ret.val = 0 else True
 /// ```
 pub fn use_const<const N: usize>(arr: [u8; N]) -> u8 {
     if N > 0 { arr[0] } else { 0 }

tools/hermes/tests/fixtures/associated_types/hermes.toml

@@ -4,6 +4,8 @@ Behavior: Compiles a Rust source featuring a trait with an associated type (`T::
 """
 
 [test]
+# FIXME(#3089): Update to use valid syntax in `lib.rs`; coalesce with
+# `test_4_6_assoc_types`.
+expected_status = "known_bug"
 stderr_file = "expected.stderr"
-expected_status = "failure"
 args = ["verify", "--allow-sorry"]

tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml

@@ -4,6 +4,6 @@ Behavior: Declares a single function with two consecutive `/// ```lean, hermes`
 """
 
 [test]
+expected_status = "failure"
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
-expected_status = "failure"

tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml

@@ -4,5 +4,7 @@ Behavior: In an `isValid` boundary condition, queries the default instantiation
 """
 
 [test]
-expected_status = "failure"
+# FIXME(#3089): Update the syntax in `lib.rs` to be valid Lean, and get this
+# passing.
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]

tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs

@@ -3,7 +3,7 @@ pub trait Iter {
     type Item: Default;
 }
 
-/// ```lean, hermes
+/// ```hermes
 /// proof (h_progress):
 ///   sorry
 /// proof context:
@@ -13,8 +13,9 @@ pub fn check_item<T: Iter>(x: T::Item) -> T::Item {
     x
 }
 
-/// @spec
+/// ```hermes
 /// isValid self := self.val == T::Item::default()
+/// ```
 pub struct Wrapper<T: Iter> where T::Item: PartialEq {
     pub val: T::Item,
 }

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

@@ -4,5 +4,5 @@ Behavior: Uses Rust keywords natively (`r#match`, `r#type`). Confirms Charon saf
 """
 
 [test]
-expected_status = "failure"
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry"]

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

@@ -4,5 +4,5 @@ Behavior: Uses parameters such as `&&u32`, `&mut &u32`, and `&&mut u32`. Validat
 """
 
 [test]
-expected_status = "failure"
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry"]

tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml

@@ -4,6 +4,6 @@ Behavior: Introduces missing colons, invalid names, and Lean keywords as named b
 """
 
 [test]
+expected_status = "failure"
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
-expected_status = "failure"

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

@@ -2,7 +2,6 @@
 /// We test both validation errors (rust-level parsing and validation)
 /// and verification errors (Lean-level theorem failures).
 
-
 /// 3. Mismatched proof name
 /// ```lean, hermes, spec
 /// ensures (h_ensures):
@@ -15,7 +14,6 @@ fn fail_mismatched_proof_name(x: u32) -> u32 {
     x
 }
 
-
 /// 9. Reserved name collision (requires)
 /// ```lean, hermes, spec
 /// requires (h_x_is_valid):
@@ -30,7 +28,6 @@ unsafe fn fail_reserved_name_collision_requires(x: u32) -> u32 {
     x
 }
 
-
 /// 10. Reserved name collision (ensures)
 /// ```lean, hermes, spec
 /// ensures (h_ret_is_valid):
@@ -43,7 +40,6 @@ fn fail_reserved_name_collision_ensures(x: u32) -> u32 {
     x
 }
 
-
 /// 26. Proof targets a requires clause instead of an ensures clause
 /// ```lean, hermes, spec
 /// requires (h_req):

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

@@ -79,42 +79,6 @@
  47 │     A(u32),
     ╰────
 
-  ⚠ union `MyUnion` is never used
-    ╭─[[PROJECT_ROOT]/src/lib.rs:51:7]
- 50 │ 
- 51 │ union MyUnion {
-    ·       ───┬───
-    ·          ╰── 
- 52 │     f1: u32,
-    ╰────
-
-  ⚠ struct `UnionWrapper` is never constructed
-    ╭─[[PROJECT_ROOT]/src/lib.rs:59:8]
- 58 │ /// ```
- 59 │ struct UnionWrapper(MyUnion);
-    ·        ──────┬─────
-    ·              ╰── 
-    ╰────
-
-Error: Aeneas failed for package 'type_features' with status: exit status: 2
-stderr:
-Applied prepasses:  [----------------------------------------------------] 0/1 ⠋Applied prepasses:  [####################################################] 1/1 ⠋Applied prepasses:  [####################################################] 1/1 ✔️
-Uncaught exception:
-
-  (Failure
-    "unions are not supported\
-   \nSource: 'src/lib.rs', lines 51:0-54:1\
-   \nCompiler source: llbc/TypesAnalysis.ml, line 503")
-
-Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 120, characters 4-23
-Called from Aeneas__Errors.craise in file "Errors.ml" (inlined), line 126, characters 2-43
-Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 503, characters 19-74
-Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
-Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 554-556, characters 6-23
-Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62
-Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
-Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66
-Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71
-Called from Dune__exe__Main in file "Main.ml", lines 726-727, characters 8-37
-
+[External Error] generated/TypeFeaturesTypeFeatures<HASH>/TypeFeaturesTypeFeatures<HASH>.lean: type expected, got
+  (UsesAssoc Self : Type → Type)
+Error: Lean verification failed

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

@@ -1,11 +1,11 @@
 /// ```hermes
-/// isValid self := {N} > 0
+/// isValid self := N > 0
 /// ```
 struct ConstGen<const N: usize>;
 
 /// ```hermes
 /// isSafe :
-///   {N} > 0
+///   N > 0
 /// ```
 unsafe trait ConstTrait<const N: usize> {}
 
@@ -47,13 +47,3 @@ enum ValidatedEnum {
     A(u32),
     B { x: u32 },
 }
-
-union MyUnion {
-    f1: u32,
-    f2: f32,
-}
-
-/// ```hermes
-/// isValid self := True
-/// ```
-struct UnionWrapper(MyUnion);

tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml

@@ -4,6 +4,6 @@ Behavior: Triggers a `panic!("Boom")` immediately in `build.rs`. Confirms Hermes
 """
 
 [test]
+expected_status = "failure"
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
-expected_status = "failure"

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

@@ -1,3 +1,3 @@
-/// ```lean, hermes
+/// ```hermes
 /// ```
 pub fn foo() {}