Compilation fails with errors in `ring`

[acoglio]

When I run cargo kani in (any of) the top-level directories of the open-source repositories

https://github.com/ProvableHQ/snarkVM
https://github.com/ProvableHQ/snarkOS

I get errors in the ring crate (similar to the ones reported in #3109):

error[E0080]: evaluation of constant value failed
  --> /Users/ac/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ring-0.17.14/src/cpu/arm/darwin.rs:44:5
   |
44 |     assert!((CAPS_STATIC & MIN_STATIC_FEATURES) == MIN_STATIC_FEATURES);
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: (CAPS_STATIC & MIN_STATIC_FEATURES) == MIN_STATIC_FEATURES

error[E0080]: evaluation of constant value failed
  --> /Users/ac/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ring-0.17.14/src/cpu/arm/darwin.rs:51:5
   |
51 |     assert!(CAPS_STATIC == MIN_STATIC_FEATURES);
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: CAPS_STATIC == MIN_STATIC_FEATURES

error[E0080]: evaluation of constant value failed
  --> /Users/ac/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ring-0.17.14/src/cpu/arm/darwin.rs:78:39
   |
78 |     const _ASSERT_NEON_DETECTED: () = assert!((CAPS_STATIC & Neon::mask()) == Neon::mask());
   |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: (CAPS_STATIC & Neon::mask()) == Neon::mask()

error[E0080]: evaluation of constant value failed
   --> /Users/ac/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/ring-0.17.14/src/cpu/arm.rs:189:31
    |
189 |   const _AARCH64_HAS_NEON: () = assert!(
    |  _______________________________^
190 | |     ((CAPS_STATIC & Neon::mask()) == Neon::mask())
191 | |         || !cfg!(all(target_arch = "aarch64", target_endian = "little"))
192 | | );
    | |_^ evaluation panicked: assertion failed: ((CAPS_STATIC & Neon::mask()) == Neon::mask()) ||
    !cfg!(all(target_arch = "aarch64", target_endian = "little"))

There are no Kani annotations yet in those two repositories, but when I run cargo kani in smaller projects without Kani annotations I don't get a failure.

[zhassan-aws]

Thanks for creating this issue @acoglio. The errors can be reproduced on the ring crate directly:

$ git clone https://github.com/briansmith/ring
$ cd ring
$ cargo kani
Kani Rust Verifier 0.62.0 (cargo plugin)
   Compiling shlex v1.3.0
   Compiling libc v0.2.172
   Compiling cfg-if v1.0.0
   Compiling untrusted v0.9.0
   Compiling cc v1.2.25
   Compiling getrandom v0.2.16
   Compiling ring v0.17.14 (/home/ubuntu/git/ring)
error[E0080]: evaluation of constant value failed
  --> src/cpu/intel.rs:31:9
   |
31 |         assert!(cfg!(target_feature = "sse") && cfg!(target_feature = "sse2"));
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: cfg!(target_feature = "sse") && cfg!(target_feature = "sse2")

error[E0080]: evaluation of constant value failed
   --> src/cpu/intel.rs:234:31
    |
234 |     const _SSE_REQUIRED: () = assert!(cfg!(target_feature = "sse"));
    |                               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: cfg!(target_feature = "sse")

error[E0080]: evaluation of constant value failed
   --> src/cpu/intel.rs:235:32
    |
235 |     const _SSE2_REQUIRED: () = assert!(cfg!(target_feature = "sse2"));
    |                                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: cfg!(target_feature = "sse2")

error[E0080]: evaluation of constant value failed
   --> src/cpu/intel.rs:264:39
    |
264 |     const _SSE2_REQUIRED_X86_64: () = assert!(cfg!(target_feature = "sse2"));
    |                                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: cfg!(target_feature = "sse2")

error[E0080]: evaluation of constant value failed
   --> src/cpu/intel.rs:266:38
    |
266 |     const _SSE_REQUIRED_X86_64: () = assert!(cfg!(target_feature = "sse2"));
    |                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation panicked: assertion failed: cfg!(target_feature = "sse2")

For more information about this error, try `rustc --explain E0080`.
error: could not compile `ring` (lib) due to 5 previous errors
error: Failed to execute cargo (exit status: 101). Found 5 compilation errors.

@thanhnguyen-aws This seems related to the sse/sse2 fix that you added recently. Can you check?