diff --git a/tools/hermes/examples/const_generics.rs b/tools/hermes/examples/const_generics.rs index 8240b359f8..ff2e8cf2bc 100644 --- a/tools/hermes/examples/const_generics.rs +++ b/tools/hermes/examples/const_generics.rs @@ -1,4 +1,15 @@ -/// ```lean, hermes, spec +/// ```hermes +/// isValid self := N > 0 +/// ``` +pub struct ConstGen; + +/// ```hermes +/// isSafe : N > 0 +/// ``` +pub unsafe trait ConstTrait {} + +/// ```hermes +/// ensures: if N.val = 0 then ret.val = 0 else True /// ``` pub fn use_const(arr: [u8; N]) -> u8 { if N > 0 { arr[0] } else { 0 } diff --git a/tools/hermes/tests/fixtures/associated_types/hermes.toml b/tools/hermes/tests/fixtures/associated_types/hermes.toml index 37a83639ce..2027a39260 100644 --- a/tools/hermes/tests/fixtures/associated_types/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml b/tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml index cfeec1bd66..37cb609d46 100644 --- a/tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml +++ b/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" diff --git a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml index 32c4af6892..6ab9e06772 100644 --- a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs b/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs index 32eb3ba1d8..9abcb4a866 100644 --- a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs +++ b/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(x: T::Item) -> T::Item { x } -/// @spec +/// ```hermes /// isValid self := self.val == T::Item::default() +/// ``` pub struct Wrapper where T::Item: PartialEq { pub val: T::Item, } diff --git a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/hermes.toml index 8e56d84d9b..0c6dd38316 100644 --- a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/hermes.toml index 9348e7ee10..e770de59b5 100644 --- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/hermes.toml +++ b/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"] diff --git a/tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml b/tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml index c641c3a7cf..64ba649d22 100644 --- a/tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml +++ b/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" diff --git a/tools/hermes/tests/fixtures/named_bounds_validation_failures/source/src/lib.rs b/tools/hermes/tests/fixtures/named_bounds_validation_failures/source/src/lib.rs index 12bbd8f1d9..acd5c6bef0 100644 --- a/tools/hermes/tests/fixtures/named_bounds_validation_failures/source/src/lib.rs +++ b/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): diff --git a/tools/hermes/tests/fixtures/type_features/expected.stderr b/tools/hermes/tests/fixtures/type_features/expected.stderr index e807a7a9e9..e3700cad00 100644 --- a/tools/hermes/tests/fixtures/type_features/expected.stderr +++ b/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/TypeFeaturesTypeFeatures.lean: type expected, got + (UsesAssoc Self : Type → Type) +Error: Lean verification failed diff --git a/tools/hermes/tests/fixtures/type_features/source/src/lib.rs b/tools/hermes/tests/fixtures/type_features/source/src/lib.rs index d726bff9cd..57d3fdf3a0 100644 --- a/tools/hermes/tests/fixtures/type_features/source/src/lib.rs +++ b/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; /// ```hermes /// isSafe : -/// {N} > 0 +/// N > 0 /// ``` unsafe trait ConstTrait {} @@ -47,13 +47,3 @@ enum ValidatedEnum { A(u32), B { x: u32 }, } - -union MyUnion { - f1: u32, - f2: f32, -} - -/// ```hermes -/// isValid self := True -/// ``` -struct UnionWrapper(MyUnion); diff --git a/tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml b/tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml index b3b6b35037..c99d500be7 100644 --- a/tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml +++ b/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" diff --git a/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs b/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs index 8afbc86ed9..ca243b427c 100644 --- a/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs +++ b/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs @@ -1,3 +1,3 @@ -/// ```lean, hermes +/// ```hermes /// ``` pub fn foo() {}