Add support for const in exec_spec macro

[zouyonghao]

Previously, if we do:

exec_spec! {
    pub const TEST_CONST: u32 = 0x00000010;
    spec fn is_test_const(x: u32) -> bool {
        x == TEST_CONST
    }
}

fn sanity_check(test_value: u32) {
    if exec_is_test_const(test_value) {
        assert(test_value == TEST_CONST);
    }
}

We got

error: unsupported item
  --> /home/zyh/verus/source/target/debug/test_inputs/exec_spec-e50f36aebaecab9e-test_exec_spec_const/test.rs:18:5
   |
18 |     pub const TEST_CONST: u32 = 0x00000010;
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Or, if we do

pub const TEST_CONST: u32 = 0x00000010;
exec_spec! {
    spec fn is_test_const(x: u32) -> bool {
        x == TEST_CONST
    }
}

fn sanity_check(test_value: u32) {
    if exec_is_test_const(test_value) {
        assert(test_value == TEST_CONST);
    }
}

We got

error[E0425]: cannot find value `ExecTEST_CONST` in this scope
  --> /home/zyh/verus/source/target/debug/test_inputs/exec_spec-e50f36aebaecab9e-test_exec_spec_const2/test.rs:20:14
   |
17 | pub const TEST_CONST: u32 = 0x00000010;
   | --------------------------------------- similarly named constant `TEST_CONST` defined here
...
20 |         x == TEST_CONST
   |              ^^^^^^^^^^ help: a constant with a similar name exists: `TEST_CONST`

This PR simply generates the Exec #const_name for the exec_spec macro.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.