clean up the proof script
@@ -31,15 +31,12 @@ let fresh_ptr ty = do {
};
// conn->corked_io
-//let conn_corked_io pconn = crucible_elem pconn 7;
let conn_corked_io pconn = crucible_field pconn "corked_io";
//conn->mode
-//let conn_mode pconn = crucible_elem pconn 8;
let conn_mode pconn = crucible_field pconn "mode";
//conn->secure.cipher_suite->key_exchange_alg->flags
-//let conn_secure_cipher_suite pconn = (crucible_elem (crucible_elem pconn 23) 11);
let conn_secure_cipher_suite pconn = (crucible_field (crucible_field pconn "secure") "cipher_suite");
//let key_exchange_algorithm csuite = crucible_elem csuite 3;
@@ -49,7 +46,6 @@ let key_exchange_algorithm csuite = crucible_field csuite "key_exchange_alg";
let kea_flags kea = crucible_field kea "flags";
//conn->status_type
-//let conn_status_type pconn = crucible_elem pconn 49;
let conn_status_type pconn = crucible_field pconn "status_type";
//let conn_config pconn = crucible_elem pconn 0;
@@ -59,23 +55,18 @@ let conn_config pconn = crucible_field pconn "config";
let cert_key_pairs config = (crucible_field config "cert_and_key_pairs");
//conn->config->cert_and_key_pairs->ocsp_status.size
-//let ocsp_status_size cert_and_key = crucible_elem (crucible_elem (cert_and_key) 3) 1;
let ocsp_status_size cert_and_key = crucible_field (crucible_field (cert_and_key) "ocsp_status") "size";
//conn->client_cert_auth_type
-//let cca_type pconn = crucible_elem pconn 19 ;
let cca_type pconn = crucible_field pconn "client_cert_auth_type";
//conn->handshake.handshake_type
-//let conn_handshake_handshake_type pconn = crucible_elem (crucible_elem pconn 40) 9;
let conn_handshake_handshake_type pconn = crucible_field (crucible_field pconn "handshake") "handshake_type";
//conn->handshake.message_number
-//let conn_handshake_message_number pconn = crucible_elem (crucible_elem pconn 40) 10;
let conn_handshake_message_number pconn = crucible_field (crucible_field pconn "handshake") "message_number";
corked <- crucible_declare_ghost_state "corked";
-// assume the socket is initially uncorked
crucible_ghost_value corked {{ 0 : [1] }};
// setup_handshake de-serializes parts of the s2n_handshake and
