// Low-level specifications (model functions) of parts of tls/s2n_handshake_io.c.
// The main function is s2n_advance_message, and we prove it's equivalence to its
// counterpart in s2n_handshake_io.c

module s2n_handshake_io where

// This function models the update of the s2n_connection struct by the
// s2n_conn_set_handshake_type function in s2n.
conn_set_handshake_type : connection -> connection
conn_set_handshake_type conn =
  if IS_TLS13_HANDSHAKE conn
  then conn_set_tls13_handshake_type conn
  else conn_set_pre_tls13_handshake_type conn

// This function models the update of the s2n_connection struct by the
// s2n_conn_set_handshake_type function in s2n. This only models the
// pre-TLS 1.3 code path; see conn_set_tls13_handshake_type for a model of the
// TLS 1.3 code path.
conn_set_pre_tls13_handshake_type : connection -> connection
conn_set_pre_tls13_handshake_type conn = conn'
  where conn' = {handshake = handshake'
                ,mode = conn.mode
                ,corked_io = conn.corked_io
                ,corked = conn.corked
                ,is_caching_enabled = conn.is_caching_enabled
                ,resume_from_cache = conn.resume_from_cache
                ,server_can_send_ocsp = conn.server_can_send_ocsp
                ,key_exchange_eph = conn.key_exchange_eph
                ,client_auth_flag = conn.client_auth_flag
                ,actual_protocol_version = conn.actual_protocol_version
                ,no_client_cert = conn.no_client_cert
                ,early_data_state = conn.early_data_state
                ,chosen_psk_null = conn.chosen_psk_null
                ,quic_enabled = conn.quic_enabled
                ,npn_negotiated = conn.npn_negotiated
                }
        (handshake' : handshake) = {handshake_type = handshake_type'
                                   ,message_number = conn.handshake.message_number
                                   }
        handshake_type' = NEGOTIATED || full_handshake ||  with_npn ||
                            (if (full_handshake != 0) then
                              perfect_forward_secrecy || ocsp_status || client_auth
                              else zero)
        with_npn = if conn.npn_negotiated
                   then WITH_NPN
                   else zero
        full_handshake  = if (conn.is_caching_enabled /\ ~conn.resume_from_cache)
                          then zero
                          else FULL_HANDSHAKE
        perfect_forward_secrecy = if conn.key_exchange_eph
                                  then PERFECT_FORWARD_SECRECY
                                  else zero
        ocsp_status = if conn.server_can_send_ocsp
                      then OCSP_STATUS
                      else zero
        client_auth = if conn.client_auth_flag
                      then CLIENT_AUTH
                      else zero

// This function models the update of the s2n_connection struct by the
// s2n_conn_set_tls13_handshake_type function in s2n.
conn_set_tls13_handshake_type : connection -> connection
conn_set_tls13_handshake_type conn = conn'
  where conn' = {handshake = handshake'
                ,mode = conn.mode
                ,corked_io = conn.corked_io
                ,corked = conn.corked
                ,is_caching_enabled = conn.is_caching_enabled
                ,resume_from_cache = conn.resume_from_cache
                ,server_can_send_ocsp = conn.server_can_send_ocsp
                ,key_exchange_eph = conn.key_exchange_eph
                ,client_auth_flag = conn.client_auth_flag
                ,actual_protocol_version = conn.actual_protocol_version
                ,no_client_cert = conn.no_client_cert
                ,early_data_state = conn.early_data_state
                ,chosen_psk_null = conn.chosen_psk_null
                ,quic_enabled = conn.quic_enabled
                ,npn_negotiated = conn.npn_negotiated
                }
        (handshake' : handshake) = {handshake_type = handshake_type'
                                   ,message_number = conn.handshake.message_number
                                   }
        handshake_type'  = (conn.handshake.handshake_type && (HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS))
                           || NEGOTIATED || full_handshake || with_early_data || client_auth || middlebox_compat
        full_handshake   = if conn.chosen_psk_null
                           then FULL_HANDSHAKE
                           else zero
        with_early_data  = if conn.early_data_state == S2N_EARLY_DATA_ACCEPTED
                           then WITH_EARLY_DATA
                           else zero
        client_auth      = if conn.client_auth_flag /\ (full_handshake != 0)
                           then CLIENT_AUTH
                           else zero
        middlebox_compat = if conn.quic_enabled
                           then zero
                           else MIDDLEBOX_COMPAT

// This function models the update of the s2n_connection struct by the
// s2n_advance_message function in s2n.
advance_message : connection -> connection
advance_message conn = conn2
  where conn2 = {handshake = handshake2
                ,mode = conn.mode
                ,corked_io = conn.corked_io
                ,corked = cork2
                ,is_caching_enabled = conn.is_caching_enabled
                ,resume_from_cache = conn.resume_from_cache
                ,server_can_send_ocsp = conn.server_can_send_ocsp
                ,key_exchange_eph = conn.key_exchange_eph
                ,client_auth_flag = conn.client_auth_flag
                ,actual_protocol_version = conn.actual_protocol_version
                ,no_client_cert = conn.no_client_cert
                ,early_data_state = conn.early_data_state
                ,chosen_psk_null = conn.chosen_psk_null
                ,quic_enabled = conn.quic_enabled
                ,npn_negotiated = conn.npn_negotiated
                }
        (handshake2 : handshake) = { handshake_type = conn.handshake.handshake_type,
                                     message_number = message_number2 }
        cork2 = if (ACTIVE_STATE conn2).writer != (ACTIVE_STATE conn).writer
                then if (ACTIVE_STATE conn2).writer == mode_writer conn2.mode
                     then s2n_cork conn else s2n_uncork conn
                else conn.corked
        message_number2 = conn.handshake.message_number + ( if skip_message then 2 else 1)
        skip_message = (IS_TLS13_HANDSHAKE conn2) /\ ((mode_writer conn2.mode) != (next_state conn).writer)
                           /\ ((next_state conn).record_type == TLS_CHANGE_CIPHER_SPEC)

// This function models the update of the s2n_connection struct by the 
// s2n_conn_set_handshake_no_client_cert function in s2n.
conn_set_handshake_no_client_cert : connection -> connection
conn_set_handshake_no_client_cert conn = conn2
  where conn2 = {handshake = handshake'
                ,mode = conn.mode
                ,corked_io = conn.corked_io
                ,corked = conn.corked
                ,is_caching_enabled = conn.is_caching_enabled
                ,resume_from_cache = conn.resume_from_cache
                ,server_can_send_ocsp = conn.server_can_send_ocsp
                ,key_exchange_eph = conn.key_exchange_eph
                ,client_auth_flag = conn.client_auth_flag
                ,actual_protocol_version = conn.actual_protocol_version
                ,no_client_cert = conn.no_client_cert
                ,early_data_state = conn.early_data_state
                ,chosen_psk_null = conn.chosen_psk_null
                ,quic_enabled = conn.quic_enabled
                ,npn_negotiated = conn.npn_negotiated
                }
        (handshake' : handshake) = {handshake_type = handshake_type'
                                   ,message_number = conn.handshake.message_number
                                   }
        handshake_type' = if conn.client_auth_flag
                          then conn.handshake.handshake_type || NO_CLIENT_CERT
                          else conn.handshake.handshake_type

// for a given initial connection struct generate the
// sequence of handshake_action's
traceS2N : {n} (fin n) => connection -> [n]handshake_action
traceS2N conn = normalizeAfterData (take (map ACTIVE_STATE (iterate s2nTrans conn)))

traceS2N2 : {n} (fin n) => connection -> [n][32]
traceS2N2 conn = take (map ACTIVE_MESSAGE (iterate s2nTrans conn))

//Make sure all the messages after the first APPLICATION_DATA are also APPLICATION_DATA
normalizeAfterData : {n} (fin n) => [n]handshake_action -> [n]handshake_action
normalizeAfterData hsas = map snd (tail (scanl f (False, dataMsg) hsas))
    where f (found, acc) hsa = if hsa == dataMsg \/ found then (True, dataMsg)
                               else (found, hsa)
          dataMsg = mkAct TLS_APPLICATION_DATA 0 'B'

// match actions, but drop any with an 'A' writer from the second trace
tracesMatchExcludingWaits: {n} (fin n, width n>=1) => [n]handshake_action -> [n]handshake_action -> Bit
tracesMatchExcludingWaits xs ys = go 0 0 where
  go: [width n] -> [width n] -> Bit
  go i j = if i >= `n then True
            | j >= `n then True
            else (xs@i == ys@j /\ go (i+1) (j+1))

// returns the first element of an array that satisfies a given
// predicate. If none found, a provided default value is returned.
find : {n, x} (fin n) => (x -> Bool) -> x -> [n]x -> x
find p def xs = snd (foldl f (False, def) xs)
  where f (found, y) next = if ~found /\ p next then (True, next) else (found, y)

head : {n, x} [n+1]x -> x
head (([a] : [1]x) # _) = a

lookupDefault : {a, b, n} (fin n, Cmp a) => [n](a, b) -> b -> a -> b
lookupDefault dict def key = fst (foldl f (def, False) dict)
  where f (value, found) (key', value') =
          if found then (value, found)
          else if key == key' then (value', True)
                else (value, found)

fst (a, b) = a
snd (a, b) = b

// s2n state transition that incorporates both s2n_advance_message and
// s2n_conn_set_handshake_type
s2nTrans : connection -> connection
s2nTrans conn = conn3
          where conn2 = if helloState then conn_set_handshake_type conn 
                        else if noCertAuthState then conn_set_handshake_no_client_cert conn
                        else conn
                conn3 = advance_message conn2
                helloState = ACTIVE_MESSAGE conn == CLIENT_HELLO \/ ACTIVE_MESSAGE conn == SERVER_HELLO
                // currently nocertAuthState is only set for TLS 1.3. Issue to fix: https://github.com/awslabs/s2n/issues/1786
                noCertAuthState = ACTIVE_MESSAGE conn == CLIENT_CERT /\ conn.no_client_cert /\ conn.actual_protocol_version == S2N_TLS13

// Part of the s2n_connection struct that s2n_advance_message
// uses. The names of the fields are the same as in C.
type connection = {handshake : handshake
                  ,mode : [32]
                  ,corked_io : Bit
                  ,corked : [2]
                  ,is_caching_enabled : Bit
                  ,resume_from_cache : Bit
                  ,server_can_send_ocsp : Bit
                  ,key_exchange_eph : Bit
                  ,client_auth_flag : Bit //whether the server will request client cert
                  ,actual_protocol_version : [8]
                  ,no_client_cert : Bit
                  ,early_data_state : [32]
                  ,chosen_psk_null : Bit
                  ,quic_enabled : Bit
                  ,npn_negotiated : Bit
                  }

type handshake = {handshake_type : [32]
                 ,message_number : [32]
                 }

type S2N_HANDSHAKES_COUNT = 256
type S2N_MAX_HANDSHAKE_LENGTH = 32

// functions model the corresponding macros in C

IS_TLS13_HANDSHAKE : connection -> Bit
IS_TLS13_HANDSHAKE conn = conn.actual_protocol_version == S2N_TLS13

ACTIVE_STATE_MACHINE : connection -> [TOTAL_HANDSHAKE_ACTIONS]handshake_action
ACTIVE_STATE_MACHINE conn = if IS_TLS13_HANDSHAKE conn then tls13_state_machine else state_machine # zero

ACTIVE_HANDSHAKES : connection -> [S2N_HANDSHAKES_COUNT][S2N_MAX_HANDSHAKE_LENGTH][32]
ACTIVE_HANDSHAKES conn = if IS_TLS13_HANDSHAKE conn then tls13_handshakes else handshakes

ACTIVE_MESSAGE : connection -> [32]
ACTIVE_MESSAGE conn = ((ACTIVE_HANDSHAKES conn) @ (conn.handshake.handshake_type))
                                                @ (conn.handshake.message_number)

ACTIVE_STATE : connection -> handshake_action
ACTIVE_STATE conn = (ACTIVE_STATE_MACHINE conn) @ (ACTIVE_MESSAGE conn)

next_message : connection -> [32]
next_message conn = ((ACTIVE_HANDSHAKES conn) @ (conn.handshake.handshake_type))
                                              @ (conn.handshake.message_number + 1)
                                              
next_state : connection -> handshake_action
next_state conn = (ACTIVE_STATE_MACHINE conn) @ (next_message conn)

// Helper function that gives the value of the 'writer' field of the
// current handshake state (handshake action) that would correspond to
// the connection mode  (S2N_SERVER or S2N_CLIENT)
mode_writer : [32] -> [8]
mode_writer m = if m == S2N_CLIENT then 'C' else 'S'

s2n_cork : connection -> [2]
s2n_cork c = c.corked + 1

s2n_uncork : connection -> [2]
s2n_uncork c = c.corked - 1

// this models the handshake_action struct (part of the handshake
// state), but without the handler functions
type handshake_action = {record_type : [8]
                        ,message_type : [8]
                        ,writer : [8]
                        }

mkAct : [8] -> [8] -> [8] -> handshake_action
mkAct r m w = {record_type = r, message_type = m, writer = w}

// A model of the tls1.3 handshake states (array state_machine in C)
tls13_state_machine : [TOTAL_HANDSHAKE_ACTIONS]handshake_action
tls13_state_machine = [tls13_state_machine_fn m | m <- [0..(TOTAL_HANDSHAKE_ACTIONS-1)]]

// Function that tells a handshake_action for a given tls1.3 state
tls13_state_machine_fn : [5] -> handshake_action
tls13_state_machine_fn m =
  if      m == CLIENT_HELLO then mkAct TLS_HANDSHAKE TLS_CLIENT_HELLO 'C'
  else if m == SERVER_HELLO then mkAct TLS_HANDSHAKE TLS_SERVER_HELLO 'S'
  else if m == HELLO_RETRY_MSG then mkAct TLS_HANDSHAKE TLS_SERVER_HELLO 'S'
  else if m == ENCRYPTED_EXTENSIONS then mkAct TLS_HANDSHAKE TLS_ENCRYPTED_EXTENSIONS 'S'
  else if m == SERVER_CERT_REQ then mkAct TLS_HANDSHAKE TLS_CERTIFICATE_REQ 'S'
  else if m == SERVER_CERT then mkAct TLS_HANDSHAKE TLS_CERTIFICATE 'S'
  else if m == SERVER_CERT_VERIFY then mkAct TLS_HANDSHAKE TLS_CERT_VERIFY 'S'
  else if m == SERVER_FINISHED then mkAct TLS_HANDSHAKE TLS_FINISHED 'S'
  else if m == CLIENT_CERT then mkAct TLS_HANDSHAKE TLS_CERTIFICATE 'C'
  else if m == CLIENT_CERT_VERIFY then mkAct TLS_HANDSHAKE TLS_CERT_VERIFY 'C'
  else if m == CLIENT_FINISHED then mkAct TLS_HANDSHAKE TLS_FINISHED 'C'
  else if m == END_OF_EARLY_DATA then mkAct TLS_HANDSHAKE TLS_END_OF_EARLY_DATA 'C'
  else if m == CLIENT_CHANGE_CIPHER_SPEC then mkAct TLS_CHANGE_CIPHER_SPEC 0 'C'
  else if m == SERVER_CHANGE_CIPHER_SPEC then mkAct TLS_CHANGE_CIPHER_SPEC 0 'S'
  else if m == APPLICATION_DATA then mkAct TLS_APPLICATION_DATA 0 'B'
  else zero

// A model of the handshake states (array state_machine in C)
state_machine : [TOTAL_HANDSHAKE_ACTIONS]handshake_action
state_machine = [state_machine_fn m | m <- [0..(TOTAL_HANDSHAKE_ACTIONS-1)]]

// Function that tells a handshake_action for a given state
state_machine_fn : [5] -> handshake_action
state_machine_fn m =
  if      m == CLIENT_HELLO then mkAct TLS_HANDSHAKE TLS_CLIENT_HELLO 'C'
  else if m == SERVER_HELLO then mkAct TLS_HANDSHAKE TLS_SERVER_HELLO 'S'
  else if m == SERVER_NEW_SESSION_TICKET then mkAct TLS_HANDSHAKE TLS_SERVER_NEW_SESSION_TICKET 'S'
  else if m == SERVER_CERT then mkAct TLS_HANDSHAKE TLS_CERTIFICATE 'S'
  else if m == SERVER_CERT_STATUS then mkAct TLS_HANDSHAKE TLS_CERTIFICATE_STATUS 'S'
  else if m == SERVER_KEY then mkAct TLS_HANDSHAKE TLS_SERVER_KEY 'S'
  else if m == SERVER_CERT_REQ then mkAct TLS_HANDSHAKE TLS_CERTIFICATE_REQ 'S'
  else if m == SERVER_HELLO_DONE then mkAct TLS_HANDSHAKE TLS_SERVER_HELLO_DONE 'S'
  else if m == CLIENT_CERT then mkAct TLS_HANDSHAKE TLS_CERTIFICATE 'C'
  else if m == CLIENT_KEY then mkAct TLS_HANDSHAKE TLS_CLIENT_KEY 'C'
  else if m == CLIENT_CERT_VERIFY then mkAct TLS_HANDSHAKE TLS_CERT_VERIFY 'C'
  else if m == CLIENT_CHANGE_CIPHER_SPEC then mkAct TLS_CHANGE_CIPHER_SPEC 0 'C'
  else if m == CLIENT_NPN then mkAct TLS_HANDSHAKE TLS_NPN 'C'
  else if m == CLIENT_FINISHED then mkAct TLS_HANDSHAKE TLS_FINISHED 'C'
  else if m == SERVER_CHANGE_CIPHER_SPEC then mkAct TLS_CHANGE_CIPHER_SPEC 0 'S'
  else if m == SERVER_FINISHED then mkAct TLS_HANDSHAKE TLS_FINISHED 'S'
  else if m == APPLICATION_DATA then mkAct TLS_APPLICATION_DATA 0 'B'
  else zero

// A model of the tls1.3 handshake state machine (array handshakes in C)
tls13_handshakes : [S2N_HANDSHAKES_COUNT][S2N_MAX_HANDSHAKE_LENGTH][32]
tls13_handshakes = [tls13_handshakes_fn h | h <- [0..255]]

// A function that gives the tls1.3 handshake sequence for each valid handshake_type.
tls13_handshakes_fn: [32] -> [32][32]
tls13_handshakes_fn handshk =
  if handshk == INITIAL
    then [ CLIENT_HELLO,
           SERVER_HELLO
         ] # zero else
  if handshk == (INITIAL || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           SERVER_HELLO
         ] # zero else
  if handshk == (INITIAL || HELLO_RETRY_REQUEST)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG
         ] # zero else
  if handshk == (INITIAL || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           HELLO_RETRY_MSG
         ] # zero else
  if handshk == NEGOTIATED
    then [ CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || WITH_EARLY_DATA)
    then [ CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           END_OF_EARLY_DATA, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT || WITH_EARLY_DATA)
    then [ CLIENT_HELLO,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           CLIENT_CHANGE_CIPHER_SPEC, END_OF_EARLY_DATA, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS || WITH_EARLY_DATA)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           END_OF_EARLY_DATA, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || HELLO_RETRY_REQUEST)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE)
    then [ CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || NO_CLIENT_CERT)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || HELLO_RETRY_REQUEST || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           HELLO_RETRY_MSG, SERVER_CHANGE_CIPHER_SPEC,
           CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH)
    then [ CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_CERT_VERIFY, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || NO_CLIENT_CERT)
    then [ CLIENT_HELLO,
           SERVER_HELLO, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT)
    then [ CLIENT_HELLO,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CHANGE_CIPHER_SPEC, CLIENT_CERT, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || NO_CLIENT_CERT || MIDDLEBOX_COMPAT || EARLY_CLIENT_CCS)
    then [ CLIENT_HELLO, CLIENT_CHANGE_CIPHER_SPEC,
           SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC, ENCRYPTED_EXTENSIONS, SERVER_CERT_REQ, SERVER_CERT, SERVER_CERT_VERIFY, SERVER_FINISHED,
           CLIENT_CERT, CLIENT_FINISHED,
           APPLICATION_DATA
         ] # zero else
  zero

// A model of the handshake state machine (array handshakes in C)
handshakes : [S2N_HANDSHAKES_COUNT][S2N_MAX_HANDSHAKE_LENGTH][32]
handshakes = [handshakes_fn h | h <- [0..255]]

// A function that gives the handshake sequence for each valid handshake_type.
// This is a sparse encoding of the handshakes array (which is sparse too).
handshakes_fn : [32] -> [32][32]
handshakes_fn handshk =
  if handshk == INITIAL then [CLIENT_HELLO, SERVER_HELLO] # zero else
  if handshk == (NEGOTIATED) 
    then  [ CLIENT_HELLO, SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC 
          , SERVER_FINISHED, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
          , APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || WITH_NPN) 
    then  [ CLIENT_HELLO, SERVER_HELLO, SERVER_CHANGE_CIPHER_SPEC 
          , SERVER_FINISHED, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN
          , CLIENT_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || WITH_SESSION_TICKET) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || WITH_SESSION_TICKET || WITH_NPN) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_HELLO_DONE
         , CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || WITH_NPN) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_HELLO_DONE
         , CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN
         , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || WITH_SESSION_TICKET) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_HELLO_DONE
         , CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || WITH_SESSION_TICKET
                || WITH_NPN) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_HELLO_DONE
         , CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN
         , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == ( NEGOTIATED || FULL_HANDSHAKE 
                || PERFECT_FORWARD_SECRECY || WITH_SESSION_TICKET)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == ( NEGOTIATED || FULL_HANDSHAKE 
                || PERFECT_FORWARD_SECRECY || WITH_SESSION_TICKET
                || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || WITH_NPN) 
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (  NEGOTIATED || OCSP_STATUS || FULL_HANDSHAKE 
                || WITH_SESSION_TICKET)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (  NEGOTIATED || OCSP_STATUS || FULL_HANDSHAKE 
                || WITH_SESSION_TICKET || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_HELLO_DONE, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_HELLO_DONE, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_HELLO_DONE, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || WITH_SESSION_TICKET)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_HELLO_DONE, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || WITH_SESSION_TICKET || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_HELLO_DONE, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
         , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY, CLIENT_CERT_VERIFY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY, CLIENT_CERT_VERIFY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH
                || NO_CLIENT_CERT)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH
                || NO_CLIENT_CERT || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH
                || WITH_SESSION_TICKET)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
         , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH
                || WITH_SESSION_TICKET || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
         , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH
                || NO_CLIENT_CERT || WITH_SESSION_TICKET)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
         , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || CLIENT_AUTH
                || NO_CLIENT_CERT || WITH_SESSION_TICKET || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_REQ
         , SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
         , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
         , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || CLIENT_AUTH)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT
          , CLIENT_KEY, CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
          , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
          , APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || CLIENT_AUTH || WITH_NPN)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT
          , CLIENT_KEY, CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
          , CLIENT_NPN, CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC
          , SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk ==  (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                 || CLIENT_AUTH || WITH_SESSION_TICKET)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
          , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
          , SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk ==  (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                 || CLIENT_AUTH || WITH_SESSION_TICKET || WITH_NPN)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN
          , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
          , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || CLIENT_AUTH || NO_CLIENT_CERT)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
          , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || CLIENT_AUTH || NO_CLIENT_CERT || WITH_NPN)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
          , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || CLIENT_AUTH || NO_CLIENT_CERT || WITH_SESSION_TICKET)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
          , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
          , SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || CLIENT_AUTH || NO_CLIENT_CERT || WITH_SESSION_TICKET
                || WITH_NPN)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_KEY
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN, CLIENT_FINISHED
          , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
          , SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
          , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH
                || WITH_NPN)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN
          , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
          , APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH
                || NO_CLIENT_CERT)
    then [  CLIENT_HELLO, SERVER_HELLO, SERVER_CERT
         , SERVER_CERT_STATUS, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH
                || NO_CLIENT_CERT || WITH_NPN)
    then [  CLIENT_HELLO, SERVER_HELLO, SERVER_CERT
         , SERVER_CERT_STATUS, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH
                || WITH_SESSION_TICKET)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_FINISHED
          , SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
          , SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH
                || WITH_SESSION_TICKET || WITH_NPN)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
          , SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT, CLIENT_KEY
          , CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC, CLIENT_NPN
          , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
          , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH
                || NO_CLIENT_CERT || WITH_SESSION_TICKET)
    then [  CLIENT_HELLO, SERVER_HELLO, SERVER_CERT
         , SERVER_CERT_STATUS, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || OCSP_STATUS || CLIENT_AUTH
                || NO_CLIENT_CERT || WITH_SESSION_TICKET || WITH_NPN)
    then [  CLIENT_HELLO, SERVER_HELLO, SERVER_CERT
         , SERVER_CERT_STATUS, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
          , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT
          , CLIENT_KEY, CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
          , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
          , APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH || WITH_NPN)
     then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
          , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT
          , CLIENT_KEY, CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
          , CLIENT_NPN, CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC
          , SERVER_FINISHED, APPLICATION_DATA
          ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH || WITH_SESSION_TICKET)
     then [CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT
         , CLIENT_KEY, CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH || WITH_SESSION_TICKET
                || WITH_NPN)
     then [CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE, CLIENT_CERT
         , CLIENT_KEY, CLIENT_CERT_VERIFY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH || NO_CLIENT_CERT)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED
         , APPLICATION_DATA 
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH || NO_CLIENT_CERT || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH || NO_CLIENT_CERT
                || WITH_SESSION_TICKET)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET, SERVER_CHANGE_CIPHER_SPEC
         , SERVER_FINISHED, APPLICATION_DATA
         ] # zero else
  if handshk == (NEGOTIATED || FULL_HANDSHAKE || PERFECT_FORWARD_SECRECY
                || OCSP_STATUS || CLIENT_AUTH || NO_CLIENT_CERT
                || WITH_SESSION_TICKET || WITH_NPN)
    then [ CLIENT_HELLO, SERVER_HELLO, SERVER_CERT, SERVER_CERT_STATUS
         , SERVER_KEY, SERVER_CERT_REQ, SERVER_HELLO_DONE
         , CLIENT_CERT, CLIENT_KEY, CLIENT_CHANGE_CIPHER_SPEC
         , CLIENT_NPN, CLIENT_FINISHED, SERVER_NEW_SESSION_TICKET
         , SERVER_CHANGE_CIPHER_SPEC, SERVER_FINISHED, APPLICATION_DATA
         ] # zero
  else zero

// A predicate to tell whether a given handshake struct is valid
// (i.e. the fields are indexing into a valid state of the handshake
// state machine)
valid_handshake : handshake -> Bit
valid_handshake hs = handshakefn != zero /\
                     (hs.message_number < length handshakefn - 1) /\
                     ((hs.message_number > 0) ==> (handshakefn@(hs.message_number + 1) != 0)) where
                     handshakefn = (handshakes_fn hs.handshake_type)

valid_connection : connection -> Bit
valid_connection conn = valid_handshake (conn.handshake)

// Tells if the connection struct is in a valid initial state
initial_connection : connection -> Bit
initial_connection conn =
       conn.handshake.handshake_type < `(S2N_HANDSHAKES_COUNT)
    /\ conn.handshake.message_number == 0
    /\ (conn.corked == 0 \/ conn.corked == 1)

       // The assumptions below specifically pertain to TLS 1.3 handshakes.
       // Some of the logic that decides which TLS 1.3 handshake types are
       // reachable has moved out of the functions that we're verifying, so
       // we use the preconditions below instead. Issue
       // https://github.com/aws/s2n-tls/issues/3047 is about consolidating
       // this logic into the `s2n_conn_set_tls13_handshake_type` function
       // instead.

       // If using early data, a full handshake (i.e., chosen_psk being null)
       // cannot happen
    /\ ((conn.early_data_state == S2N_EARLY_DATA_ACCEPTED) ==> ~conn.chosen_psk_null)

       // HelloRetryRequest and EarlyData cannot both happen simultaneously
    /\ ~(((conn.handshake.handshake_type && HELLO_RETRY_REQUEST) != zero)
            /\ (conn.early_data_state == S2N_EARLY_DATA_ACCEPTED))

       // EarlyClientCCS implies MiddleboxCompat
    /\ (((conn.handshake.handshake_type && EARLY_CLIENT_CCS) != zero) ==>
         ((conn.handshake.handshake_type && MIDDLEBOX_COMPAT) != zero))

// Logical implication
implies : Bit -> Bit -> Bit
implies l r = if r then True else ~l

// values of similarly named C macros and enum values
INITIAL : [32]
INITIAL =  zero # 0x00 
NEGOTIATED : [32]
NEGOTIATED = zero #  0x01
RESUME : [32]
RESUME = zero # 0x01
FULL_HANDSHAKE : [32]
FULL_HANDSHAKE = zero # 0x02
CLIENT_AUTH : [32]
CLIENT_AUTH = zero # 0x04
NO_CLIENT_CERT : [32]
NO_CLIENT_CERT = zero # 0x08

PERFECT_FORWARD_SECRECY : [32]
PERFECT_FORWARD_SECRECY= zero # 0x10
OCSP_STATUS : [32]
OCSP_STATUS = zero # 0x20
WITH_SESSION_TICKET : [32]
WITH_SESSION_TICKET = zero # 0x40
WITH_NPN : [32]
WITH_NPN = zero # 0x80

HELLO_RETRY_REQUEST : [32]
HELLO_RETRY_REQUEST = zero # 0x10
MIDDLEBOX_COMPAT : [32]
MIDDLEBOX_COMPAT = zero # 0x20
WITH_EARLY_DATA : [32]
WITH_EARLY_DATA = zero # 0x40
EARLY_CLIENT_CCS : [32]
EARLY_CLIENT_CCS = zero # 0x80

S2N_UNKNOWN_PROTOCOL_VERSION : [8]
S2N_UNKNOWN_PROTOCOL_VERSION = 0
S2N_TLS12 : [8]
S2N_TLS12 = 33
S2N_TLS13 : [8]
S2N_TLS13 = 34

CLIENT_HELLO = 0
SERVER_HELLO = 1
SERVER_CERT = 2
SERVER_NEW_SESSION_TICKET = 3
SERVER_CERT_STATUS = 4
SERVER_KEY = 5
SERVER_CERT_REQ = 6
SERVER_HELLO_DONE = 7
CLIENT_CERT = 8
CLIENT_KEY = 9
CLIENT_CERT_VERIFY = 10
CLIENT_CHANGE_CIPHER_SPEC = 11
CLIENT_NPN = 12
CLIENT_FINISHED = 13
SERVER_CHANGE_CIPHER_SPEC = 14
SERVER_FINISHED = 15
ENCRYPTED_EXTENSIONS = 16
SERVER_CERT_VERIFY = 17
HELLO_RETRY_MSG = 18
END_OF_EARLY_DATA = 19
APPLICATION_DATA = 20
type TOTAL_HANDSHAKE_ACTIONS = 21

//TLS record type
TLS_CHANGE_CIPHER_SPEC = 20
TLS_ALERT = 21
TLS_HANDSHAKE = 22
TLS_APPLICATION_DATA = 23

//TLS handshake message types
TLS_HELLO_REQUEST             = 0
TLS_CLIENT_HELLO              = 1
TLS_SERVER_HELLO              = 2
TLS_END_OF_EARLY_DATA         = 5
TLS_SERVER_NEW_SESSION_TICKET = 4
TLS_ENCRYPTED_EXTENSIONS      = 8
TLS_CERTIFICATE               = 11
TLS_SERVER_KEY                = 12
TLS_CERTIFICATE_REQ           = 13
TLS_SERVER_HELLO_DONE         = 14
TLS_CERT_VERIFY               = 15
TLS_CLIENT_KEY                = 16
TLS_FINISHED                  = 20
TLS_CERTIFICATE_STATUS        = 22
TLS_NPN                       = 67

S2N_SERVER = 0
S2N_CLIENT = 1

//S2N cert auth types
S2N_CERT_AUTH_NONE = 0
S2N_CERT_AUTH_REQUIRED = 1

//S2N early data states
S2N_EARLY_DATA_ACCEPTED = 3