Invalid logic in s2n tls proof

[sauclovian-g]

handshake_io_lowlevel.saw in the s2n tls proofs contains the following:

// Ghost state that represents the number of times the connection write socket
// has been corked/uncorked. 
corked <- crucible_declare_ghost_state "corked";
crucible_ghost_value corked {{ 0 : [2] }};

This is invalid because crucible_ghost_value is an action in the LLVMSetup monad and it's being attempted in the TopLevel monad.

This was silently accepted and ignored by SAW until now (see #2162); it now generates a warning. This will eventually become an error, and it will need to be fixed because (in addition to being generic tech debt) it will break the CI runs.

(There also might be other similar issues later in the build.)

This is a blocker for #2167.