Ensuring that MIR constants are marked as static consts

[vonaka]

This is an attempt to resolve #3905

Currently, we rely on the mutability of the Allocation when marking constants. However, my understanding is that for various internal reasons the compiler may use mutable allocations even for constants. Instead, we should probably track whether a variable is constant ourselves.

Currently, some tests are failing. Specifically, tests/expected/function-contract/valid_ptr.rs fails because, while checking pre_condition::harness_invalid_ptr, the output doesn't include

Failed Checks: assertion failed: unsafe { read_ptr(ptr) } == -20

Instead, the assertion is UNREACHABLE, which honestly makes perfect sense to me (since the precondition doesn't hold for any input, we'll never get a chance to actually verify this assertion).

tests/kani-fixme/FunctionContracts/modify_slice_elem_fixme.rs also fails, which hopefully indicates that this also resolves #4029 (though the relation between the issue and the PR is not obvious to me).

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