Update crates documentation with info. on #[safety_constraint(...)]…

… attribute for structs (model-checking#3405)

This PR updates the crates documentation we already had for the
`#[safety_constraint(...)]` attribute to account for the changes in
model-checking#3270.

The proposal includes notes/guidelines on where to use the attribute
(i.e., the struct or its fields) depending on the type safety condition
to be specified. Also, it removes the `rs` annotations on the code
blocks that appear in the documentation because they don't seem to have
the intended effect (the blocks are not being highlighted at all).

The current version of this documentation can be found
[here](https://model-checking.github.io/kani/crates/doc/kani/derive.Arbitrary.html)
and
[here](https://model-checking.github.io/kani/crates/doc/kani/derive.Invariant.html).

Related model-checking#3095

library/kani_macros/src/lib.rs

@@ -103,16 +103,19 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// Allow users to auto generate `Arbitrary` implementations by using
 /// `#[derive(Arbitrary)]` macro.
 ///
-/// When using `#[derive(Arbitrary)]` on a struct, the `#[safety_constraint(<cond>)]`
-/// attribute can be added to its fields to indicate a type safety invariant
-/// condition `<cond>`. Since `kani::any()` is always expected to produce
-/// type-safe values, **adding `#[safety_constraint(...)]` to any fields will further
-/// constrain the objects generated with `kani::any()`**.
+/// ## Type safety specification with the `#[safety_constraint(...)]` attribute
+///
+/// When using `#[derive(Arbitrary)]` on a struct, the
+/// `#[safety_constraint(<cond>)]` attribute can be added to either the struct
+/// or its fields (but not both) to indicate a type safety invariant condition
+/// `<cond>`. Since `kani::any()` is always expected to produce type-safe
+/// values, **adding `#[safety_constraint(...)]` to the struct or any of its
+/// fields will further constrain the objects generated with `kani::any()`**.
 ///
 /// For example, the `check_positive` harness in this code is expected to
 /// pass:
 ///
-/// ```rs
+/// ```rust
 /// #[derive(kani::Arbitrary)]
 /// struct AlwaysPositive {
 /// #[safety_constraint(*inner >= 0)]
@@ -126,11 +129,11 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// }
 /// ```
 ///
-/// Therefore, using the `#[safety_constraint(...)]` attribute can lead to vacuous
+/// But using the `#[safety_constraint(...)]` attribute can lead to vacuous
 /// results when the values are over-constrained. For example, in this code
 /// the `check_positive` harness will pass too:
 ///
-/// ```rs
+/// ```rust
 /// #[derive(kani::Arbitrary)]
 /// struct AlwaysPositive {
 /// #[safety_constraint(*inner >= 0 && *inner < i32::MIN)]
@@ -158,6 +161,45 @@ pub fn unstable_feature(attr: TokenStream, item: TokenStream) -> TokenStream {
 /// As usual, we recommend users to defend against these behaviors by using
 /// `kani::cover!(...)` checks and watching out for unreachable assertions in
 /// their project's code.
+///
+/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields
+///
+/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added
+/// to either the struct or its fields, but not to both. Adding the
+/// `#[safety_constraint(...)]` attribute to both the struct and its fields will
+/// result in an error.
+///
+/// In practice, only one type of specification is need. If the condition for
+/// the type safety invariant involves a relation between two or more struct
+/// fields, the struct-level attribute should be used. Otherwise, using the
+/// `#[safety_constraint(...)]` on field(s) is recommended since it helps with readability.
+///
+/// For example, if we were defining a custom vector `MyVector` and wanted to
+/// specify that the inner vector's length is always less than or equal to its
+/// capacity, we should do it as follows:
+///
+/// ```rust
+/// #[derive(Arbitrary)]
+/// #[safety_constraint(vector.len() <= *capacity)]
+/// struct MyVector<T> {
+/// vector: Vec<T>,
+/// capacity: usize,
+/// }
+/// ```
+///
+/// However, if we were defining a struct whose fields are not related in any
+/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its
+/// fields:
+///
+/// ```rust
+/// #[derive(Arbitrary)]
+/// struct PositivePoint {
+/// #[safety_constraint(*x >= 0)]
+/// x: i32,
+/// #[safety_constraint(*y >= 0)]
+/// y: i32,
+/// }
+/// ```
 #[proc_macro_error]
 #[proc_macro_derive(Arbitrary, attributes(safety_constraint))]
 pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
@@ -167,15 +209,19 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
 /// Allow users to auto generate `Invariant` implementations by using
 /// `#[derive(Invariant)]` macro.
 ///
-/// When using `#[derive(Invariant)]` on a struct, the `#[safety_constraint(<cond>)]`
-/// attribute can be added to its fields to indicate a type safety invariant
-/// condition `<cond>`. This will ensure that the gets additionally checked when
-/// using the `is_safe()` method generated by the `#[derive(Invariant)]` macro.
+/// ## Type safety specification with the `#[safety_constraint(...)]` attribute
+///
+/// When using `#[derive(Invariant)]` on a struct, the
+/// `#[safety_constraint(<cond>)]` attribute can be added to either the struct
+/// or its fields (but not both) to indicate a type safety invariant condition
+/// `<cond>`. This will ensure that the type-safety condition gets additionally
+/// checked when using the `is_safe()` method automatically generated by the
+/// `#[derive(Invariant)]` macro.
 ///
 /// For example, the `check_positive` harness in this code is expected to
 /// fail:
 ///
-/// ```rs
+/// ```rust
 /// #[derive(kani::Invariant)]
 /// struct AlwaysPositive {
 /// #[safety_constraint(*inner >= 0)]
@@ -200,7 +246,7 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
 /// For example, for the `AlwaysPositive` struct from above, we will generate
 /// the following implementation:
 ///
-/// ```rs
+/// ```rust
 /// impl kani::Invariant for AlwaysPositive {
 /// fn is_safe(&self) -> bool {
 /// let obj = self;
@@ -212,6 +258,45 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream {
 ///
 /// Note: the assignments to `obj` and `inner` are made so that we can treat the
 /// fields as if they were references.
+///
+/// ### Adding `#[safety_constraint(...)]` to the struct as opposed to its fields
+///
+/// As mentioned earlier, the `#[safety_constraint(...)]` attribute can be added
+/// to either the struct or its fields, but not to both. Adding the
+/// `#[safety_constraint(...)]` attribute to both the struct and its fields will
+/// result in an error.
+///
+/// In practice, only one type of specification is need. If the condition for
+/// the type safety invariant involves a relation between two or more struct
+/// fields, the struct-level attribute should be used. Otherwise, using the
+/// `#[safety_constraint(...)]` is recommended since it helps with readability.
+///
+/// For example, if we were defining a custom vector `MyVector` and wanted to
+/// specify that the inner vector's length is always less than or equal to its
+/// capacity, we should do it as follows:
+///
+/// ```rust
+/// #[derive(Invariant)]
+/// #[safety_constraint(vector.len() <= *capacity)]
+/// struct MyVector<T> {
+/// vector: Vec<T>,
+/// capacity: usize,
+/// }
+/// ```
+///
+/// However, if we were defining a struct whose fields are not related in any
+/// way, we would prefer using the `#[safety_constraint(...)]` attribute on its
+/// fields:
+///
+/// ```rust
+/// #[derive(Invariant)]
+/// struct PositivePoint {
+/// #[safety_constraint(*x >= 0)]
+/// x: i32,
+/// #[safety_constraint(*y >= 0)]
+/// y: i32,
+/// }
+/// ```
 #[proc_macro_error]
 #[proc_macro_derive(Invariant, attributes(safety_constraint))]
 pub fn derive_invariant(item: TokenStream) -> TokenStream {