`ensures`/`requires` on traits and impls: better ergonomics

[W95Psp]

trafficstars

We can right ensures and requires on methods in impls and traits, but that requires putting a #[hax_lib::attributes] on the impl or trait block.

That is fine, but when the user forgets to put that #[hax_lib::attributes], we should output a nice error message with hints (the hint being: add hax_lib::attribtue).

[karthikbhargavan]

Here is an actual bug: when I write

        #[ensures(|out| fstar!("v $LEN < pow2 32 ==> $out == Spec.Utils.map_array (Spec.Utils.v_PRF $LEN) $input"))]
        fn PRFxN<const LEN: usize>(input: &[[u8; 33]; K]) -> [[u8; LEN]; K] {
            PRFxN::<K, LEN>(input)
        }

I get an ugly error:

Fatal error: exception ("Map.of_alist_exn: duplicate key" ((name K) (id (Cnst 0))))
Raised at Base__Error.raise in file "src/error.ml" (inlined), line 9, characters 14-30
Called from Base__Map.Tree0.Of_foldable.of_foldable_exn in file "src/map.ml", line 1451, characters 8-113
Called from Base__Map.Using_comparator.of_alist_exn in file "src/map.ml", line 2800, characters 25-63
Called from Base__Map.of_alist_exn in file "src/map.ml" (inlined), line 2954, characters 23-84
Called from Hax_engine__Attr_payloads.Make.WithItems.associated_expr_rebinding in file "lib/attr_payloads.ml", line 291, characters 8-95
Called from Hax_engine__Phase_traits_specs.Make.ditems.f'.f in file "lib/phases/phase_traits_specs.ml", line 134, characters 34-146
Called from Base__List.concat_map.aux in file "src/list.ml", line 726, characters 34-40
Called from Hax_engine__Phase_traits_specs.Make.ditems.f' in file "lib/phases/phase_traits_specs.ml", line 144, characters 18-74
Called from Base__List.count_map in file "src/list.ml", line 500, characters 13-17

This only appears when we use an ensures on a method that uses a new const parameter K in the return value.

---

Repro at the time: https://hax-playground.cryspen.com/#fstar/2a17a0beef/gist=3b834700dd378dd3648ade9a7a319141 This is fixed in main: https://hax-playground.cryspen.com/#fstar/latest-main/gist=e89a287ee67581769bc1a71a11010514

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Would still be useful

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

Let's keep open, related to https://github.com/cryspen/hax-evit/issues/11