ensures/requires on traits and impls: better ergonomics

[W95Psp]

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.