Verify all Kani attributes in all crate items upfront

[celinval]

Description of changes:

The Kani attributes were being lazily evaluated in some cases. We have also been handling duplicated attribute inconsistently.

Instead, validate all the attributes upfront and print all the errors found. Also, for all attributes that multiple occurrences is redundant, we emit an error if user provides 2 or more.

Resolved issues:

N/A

Related RFC:

Call-outs:

Leaving this as a draft until we merge #2534

Testing:

• How is this change tested? Existing + new tests

• Is this a refactor change?

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[zhassan-aws]

Should this be marked as a resolver for #2530?