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.

[RyanGlScott]

For reference, here is the corresponding part of the s2n code.

If I understand correctly, the fact that the s2n proof currently succeeds means that we can just remove the crucible_ghost_value corked {{ 0 : [2] }}; and things will continue to work? That would match my understanding, given that all of the relevant specifications are careful to initialize the corked ghost value anyway (e.g., here).

[sauclovian-g]

Yes. (The only other thing this might in principle do is constrain the ghost variable's type, but we don't check those statically so it has no effect that way either.)