Repair TLS 1.3 proofs after c096a55

Unfortunately, #3031 landed before it had a chance to be tested against
c096a55, which alters the logic used to check whether QUIC is enabled
`s2n_connection_is_quic_enabled`. This updates the corresponding SAW
specification to take the new definition of
`s2n_connection_is_quic_enabled` into account. This requires inspecting
one more bitfield in `s2n_connection` to accomplish.

While I was in town, I took the time to tidy up the various pieces of the
SAW specification that involve bitfields. It's still not as pretty as it
could be, but it's a sit better than it was before.

tests/saw/spec/handshake/handshake_io_lowlevel.saw

@@ -35,9 +35,6 @@ print "Loaded bitcode via Crucible";
 // definitions by this SAW script.
 ////////////////////////////////////////////////////////////////
 
-//conn->corked_io
-let conn_corked_io pconn = crucible_field pconn "corked_io";
-
 //conn->mode
 let conn_mode pconn = crucible_field pconn "mode";
 
@@ -54,7 +51,7 @@ let kea_is_ephemeral kea = crucible_elem kea 0;
 //conn->status_type
 let conn_status_type pconn = crucible_field pconn "status_type";
 
-//let conn_config pconn = crucible_elem pconn 0;
+//conn->config
 let conn_config pconn = crucible_field pconn "config";
 
 //conn->config -> client_cert_auth_type
@@ -64,21 +61,61 @@ let config_cca_type config = (crucible_field config "client_cert_auth_type");
 let ocsp_status_size cert_and_key =
     crucible_field (crucible_field (cert_and_key) "ocsp_status") "size";
 
-// conn->config->use_tickets and conn->config->quic_enabled are the fields we
-// care about, but they are in a bitfield. We currently handle this by
-// initializing the entire bitfield with a symbolic value and imposing a
-// precondition that bit 3 (i.e., use_tickets) must be equal to 0.
-// Bit 9 (i.e., quic_enabled), on the other hand, is allowed to be either
-// 0 or 1.
+// At the moment, we care about the following fields that are located in
+// bitfields:
+//
+// * conn->corked_io
+// * conn->client_session_resumed
+// * conn->quic_enabled
+// * conn->config->use_tickets
+// * conn->config->quic_enabled
+//
+// We currently handle this by initializing the entirety of each bitfield with
+// a symbolic value and imposing appropriate preconditions on them. See the
+// comments in setup_connection_common next to conn_bitfield and
+// config_bitfield for more details about these preconditions.
 
-// It's also noteworthy that we use the crucible_elem here, which will
+// It's also noteworthy that we use crucible_elem here, which will
 // cause problems if the fields are reordered. This is reasonably unlikely
 // because it makes sense to have the bitfield at the start, but it is a bit
 // fragile nonetheless. If https://github.com/GaloisInc/saw-script/issues/1461
 // were implemented, we could reference the names of bitfields instead of their
 // offsets, which would avoid this issue.
+let conn_bitfield pconn = (crucible_elem pconn 0);
 let config_bitfield config = (crucible_elem config 0);
 
+// These represent the amount of memory that LLVM will use to represent the
+// bitfields in s2n_connection and s2n_config, respectively. The size is
+// determined by counting the number of fields in the bitfield and rounding
+// up to the nearest power of 2.
+let conn_bitfield_size = 32;
+let config_bitfield_size = 16;
+
+let {{
+// The position (0-indexed) of each field of interest in
+// s2n_connection's bitfield.
+conn_corked_io_index : [conn_bitfield_size]
+conn_corked_io_index = 0
+
+conn_client_session_resumed_index : [conn_bitfield_size]
+conn_client_session_resumed_index = 1
+
+conn_quic_enabled_index : [conn_bitfield_size]
+conn_quic_enabled_index = 16
+
+// The position (0-indexed) of each field of interest in
+// s2n_config's bitfield.
+config_use_tickets_index : [config_bitfield_size]
+config_use_tickets_index = 2
+
+config_quic_enabled_index : [config_bitfield_size]
+config_quic_enabled_index = 8
+
+// Check if a field at a particular index in a bitfield is set.
+bitfield_is_set : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
+bitfield_is_set bitfield field_index = (bitfield && (1 << field_index)) != zero
+}};
+
 //conn->session_ticket_status
 let conn_session_ticket_status pconn = (crucible_field pconn "session_ticket_status");
 
@@ -125,10 +162,6 @@ crucible_ghost_value corked {{ 0 : [2] }};
 let setup_connection_common chosen_psk_null = do {
    pconn <- crucible_alloc (llvm_struct "struct.s2n_connection");
 
-   // we assume that corking/uncorking is managed by s2n
-   let corked_io = {{1 : [8]}};
-   crucible_points_to (conn_corked_io pconn) (crucible_term corked_io); 
-
    version <- crucible_fresh_var "version" (llvm_int 8);
    crucible_precond {{ version != S2N_UNKNOWN_PROTOCOL_VERSION /\ version <= S2N_TLS13 }};
    crucible_points_to (crucible_field pconn "actual_protocol_version") (crucible_term version);
@@ -175,16 +208,37 @@ let setup_connection_common chosen_psk_null = do {
    crucible_points_to (ocsp_status_size cak) (crucible_term status_size);
    crucible_equal (crucible_term status_size) (crucible_term {{zero : [32]}});
 
-   config_bitfield_value <- crucible_fresh_var "config_bitfield" (llvm_int 16);
-   crucible_points_to (config_bitfield config) (crucible_term config_bitfield_value);
-   // We currently require that the use_tickets bit is zero. Because
-   // use_tickets is the third field in a bitfield, we force it to be zero by
-   // requiring that bit 3 in the bitfield (corresponding to a bitmask of
-   // 2^(3 - 1) = 4) be set to zero.
-   crucible_equal (crucible_term {{ config_bitfield_value && 4 }}) (crucible_term {{ zero : [16] }});
-   // quic_enabled is bit 9 in the bitfield, corresponding to a bitmask of
-   // 2^(9 - 1) = 256.
-   let quic_enabled_bit = {{ (config_bitfield_value && 256) != zero }};
+   // Here, we initialize two bitfields: one in s2n_connection (conn_bitfield)
+   // and the other in s2n_config (config_bitfield). We start by initializing
+   // the entirety of each bitfield with a symbolic value of the appropriate
+   // size...
+   conn_bitfield_value <- crucible_fresh_var "conn_bitfield" (llvm_int conn_bitfield_size);
+   crucible_points_to_untyped (conn_bitfield pconn) (crucible_term conn_bitfield_value);
+   config_bitfield_value <- crucible_fresh_var "config_bitfield" (llvm_int config_bitfield_size);
+   crucible_points_to_untyped (config_bitfield config) (crucible_term config_bitfield_value);
+
+   // ...next, we impose preconditions on these symbolic values as appropriate.
+   //
+   // We assume that corking/uncorking is managed by s2n, so set the corked_io
+   // bit in s2n_connection to one...
+   let corked_io = {{ bitfield_is_set conn_bitfield_value conn_corked_io_index : Bit }};
+   crucible_precond corked_io;
+
+   // ...we assume that the client_session_resumed bit in s2n_connection must
+   // be zero...
+   crucible_precond {{ ~(bitfield_is_set conn_bitfield_value conn_client_session_resumed_index) }};
+
+   // ...we currently require that the use_tickets bit in s2n_config must be
+   // zero...
+   crucible_precond {{ ~(bitfield_is_set config_bitfield_value config_use_tickets_index) }};
+
+   // ...on the other hand, the quic_enabled bits in both s2n_connection and
+   // s2n_config are allowed to be either 0 or 1. As such, we don't need to
+   // impose any direct constraints on them. We simply query which values
+   // they have taken on during simulation and remember them for later.
+   let quic_enabled_bit = {{    bitfield_is_set conn_bitfield_value conn_quic_enabled_index
+                             \/ bitfield_is_set config_bitfield_value config_quic_enabled_index
+                          }};
 
    session_ticket_status <- crucible_fresh_var "session_ticket_status" (llvm_int 32);
    crucible_points_to (conn_session_ticket_status pconn) (crucible_term session_ticket_status);
@@ -343,7 +397,9 @@ let s2n_advance_message_spec = do {
     // of the post-state of the s2n_connection struct.
     let conn' = {{ advance_message conn }};
     crucible_ghost_value corked {{ conn'.corked }};
-    crucible_points_to (conn_corked_io pconn) (crucible_term {{ conn'.corked_io }});
+    conn_bitfield_post <- crucible_fresh_var "conn_bitfield_post" (llvm_int conn_bitfield_size);
+    crucible_points_to_untyped (conn_bitfield pconn) (crucible_term conn_bitfield_post);
+    crucible_postcond {{ bitfield_is_set conn_bitfield_post conn_corked_io_index == conn'.corked_io }};
     crucible_points_to (conn_mode pconn) (crucible_term {{ conn'.mode }});
     crucible_points_to (conn_handshake_handshake_type pconn) (crucible_term {{ conn'.handshake.handshake_type }});
     crucible_points_to (conn_handshake_message_number pconn) (crucible_term {{ conn'.handshake.message_number }});

tests/saw/spec/handshake/rfc_handshake_tls13.cry

@@ -341,7 +341,7 @@ testConnection = {
             handshake = {handshake_type = 0x00000000,
                 message_number = 0x00000000},
             mode = 0x00000000,
-            corked_io = '\NUL',
+            corked_io = False,
             corked = zero,
             is_caching_enabled = False,
             resume_from_cache = False,

tests/saw/spec/handshake/s2n_handshake_io.cry

@@ -203,7 +203,7 @@ s2nTrans conn = conn3
 // uses. The names of the fields are the same as in C.
 type connection = {handshake : handshake
                   ,mode : [32]
-                  ,corked_io : [8]
+                  ,corked_io : Bit
                   ,corked : [2]
                   ,is_caching_enabled : Bit
                   ,resume_from_cache : Bit