diff --git a/tools/hermes/tests/fixtures/design_doc/expected.stderr b/tools/hermes/tests/fixtures/design_doc/expected.stderr deleted file mode 100644 index 58ed8cd441..0000000000 --- a/tools/hermes/tests/fixtures/design_doc/expected.stderr +++ /dev/null @@ -1,16 +0,0 @@ - -=== Hermes Verification Failed === - -[Hermes Error] hermes::doc_block - - × Documentation block error: `requires` sections are only permitted on - │ `unsafe` functions. - ╭─[[PROJECT_ROOT]/src/lib.rs:62:1] - 61 │ /// ```lean, hermes - 62 │ /// requires: stack.len > 0 - · ─────────────┬───────────── - · ╰── problematic block - 63 │ /// ensures: - ╰──── - -Error: Aborting due to 1 previous errors. diff --git a/tools/hermes/tests/fixtures/design_doc/hermes.toml b/tools/hermes/tests/fixtures/design_doc/hermes.toml deleted file mode 100644 index d95580f54b..0000000000 --- a/tools/hermes/tests/fixtures/design_doc/hermes.toml +++ /dev/null @@ -1,9 +0,0 @@ -description = """ -Purpose: Tests the Hermes code generation using the exact examples from the design doc. -Behavior: Exercises the 'isSafe', 'isValid' and 'spec' attribute mapping against functions and structs. -""" - -[test] -stderr_file = "expected.stderr" -expected_status = "failure" -args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"] diff --git a/tools/hermes/tests/fixtures/design_doc/source/Cargo.toml b/tools/hermes/tests/fixtures/design_doc/source/Cargo.toml deleted file mode 100644 index a027d7deeb..0000000000 --- a/tools/hermes/tests/fixtures/design_doc/source/Cargo.toml +++ /dev/null @@ -1,8 +0,0 @@ -[package] -name = "design_doc" -version = "0.1.0" -edition = "2021" - -[dependencies] - -[workspace] diff --git a/tools/hermes/tests/fixtures/design_doc/source/src/lib.rs b/tools/hermes/tests/fixtures/design_doc/source/src/lib.rs deleted file mode 100644 index 3b7c3c1ef4..0000000000 --- a/tools/hermes/tests/fixtures/design_doc/source/src/lib.rs +++ /dev/null @@ -1,73 +0,0 @@ -/// ```lean, hermes, unsafe(axiom) -/// requires: b.val > 0 -/// ensures: -/// /// /// ret.val = a.val / b.val -/// ``` -#[allow(unused_unsafe)] -pub unsafe fn safe_div(a: u32, b: u32) -> u32 { - unsafe { a / b } -} - -/// ```lean, hermes, spec -/// ensures: -/// /// /// ret.val = a.val -/// proof context: -/// proof: -/// rw [wrapper] -/// obtain ⟨ret_val, h_eq⟩ := safe_div_spec a 1#u32 (by decide) -/// simp_all [Nat.div_one] -/// omega -/// ``` -pub fn wrapper(a: u32) -> u32 { - unsafe { safe_div(a, 1) } -} - -/// ```lean, hermes -/// isValid self := 2 | self.x.val -/// ``` -pub struct Even { - #[allow(dead_code)] - x: usize, -} - -/// ```lean, hermes -/// isSafe : -/// ... -/// ``` -pub unsafe trait FromBytes {} - -/// ```lean, hermes, spec -/// ensures: -/// /// /// ret.val = x.val -/// proof context: -/// proof: -/// -- We will use sorry here for unproven things to allow verification to proceed -/// sorry -/// ``` -pub fn read_val(x: &u32) -> u32 { - *x -} - -/// ```lean, hermes, spec -/// ensures: -/// /// /// x'.val = x.val + add.val -/// proof context: -/// have h_foo : True := True.intro -/// ``` -pub fn add_in_place(x: &mut u32, add: u32) { - *x += add; -} - -/// ```lean, hermes -/// requires: stack.len > 0 -/// ensures: -/// /// /// stack'.len = stack.len - 1 -/// ensures (h_second): -/// /// /// ret = stack[stack.len - 1] -/// proof context: -/// have h_foo : True := True.intro -/// ``` -pub fn pop(stack: &mut Vec) -> u32 { - stack.pop().unwrap() -} - diff --git a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml index d20c2131d8..e7cd6e5f5d 100644 --- a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml index 610251cdae..0ef4e1db20 100644 --- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs b/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs index bd902c3321..d4cbe3620f 100644 --- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs +++ b/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() -> () {} diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/hermes.toml deleted file mode 100644 index 7d611de900..0000000000 --- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/hermes.toml +++ /dev/null @@ -1,8 +0,0 @@ -description = """ -Purpose: Exercises bounded parameters and non-instantiated markers. -Behavior: Tests generic bounds and unused generic instantiations utilizing `PhantomData`. Verifies standard typing constraints pass into Lean via `variable (T : Type)`. -""" - -[test] -expected_status = "failure" -args = ["verify", "--allow-sorry"] diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/Cargo.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/Cargo.toml deleted file mode 100644 index 65aea2bde9..0000000000 --- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/Cargo.toml +++ /dev/null @@ -1,9 +0,0 @@ - -[package] -name = "test_2_9_generic_bounds" -version = "0.1.0" -edition = "2021" - -[dependencies] - -[workspace] diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/src/lib.rs b/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/src/lib.rs deleted file mode 100644 index cdc715d440..0000000000 --- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/src/lib.rs +++ /dev/null @@ -1,13 +0,0 @@ -pub struct Phantom { - _marker: std::marker::PhantomData, -} - -/// ```lean, hermes -/// proof (h_progress): -/// sorry -/// proof context: -/// have h_foo : True := True.intro -/// ``` -pub fn unused(x: u32) -> u32 { - x -} diff --git a/tools/hermes/tests/fixtures/is_valid_verification/hermes.toml b/tools/hermes/tests/fixtures/is_valid_verification/hermes.toml index 4b37a866d8..6fbb325ff8 100644 --- a/tools/hermes/tests/fixtures/is_valid_verification/hermes.toml +++ b/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] diff --git a/tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml b/tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml index 8328ee7ffc..bb2e935bee 100644 --- a/tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/multiple_errors/hermes.toml b/tools/hermes/tests/fixtures/multiple_errors/hermes.toml index 0666d29f6b..c5fd43c18c 100644 --- a/tools/hermes/tests/fixtures/multiple_errors/hermes.toml +++ b/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" diff --git a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr b/tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr index c9d51f37e5..82065badd8 100644 --- a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr +++ b/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. diff --git a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml b/tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml index 2f3d0ebe97..d7d394065c 100644 --- a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs b/tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs index 22090081ce..ebf9994f1f 100644 --- a/tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs +++ b/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() {} diff --git a/tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml b/tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml index 5974a9dd90..0e50ea9bf4 100644 --- a/tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml +++ b/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"]