Generating documentation with fsdoc comments - FStarLang/FStar GitHub Wiki

let initiator_send_msg_1 a b =

  print_string ("initiator "^a^" sending first message to "^b^"\n");
  let si = new_session_number #tls13 a in
  let (|t0,x|) = rand_gen #tls13 (readers [V a si 0]) (dh_usage "TLS13.dh_key") in
  let gx = dh_pk #tls13_global_usage #t0 #(readers [V a si 0]) x in
  let ev = initiate a b gx in
  trigger_event #tls13 a ev;
  let t1 = global_timestamp () in
  let new_ss_st = InitiatorSentMsg1 b x in
  let new_ss = serialize_valid_session_st t1 a si 0 new_ss_st in
  new_session #(tls13) #t1 a si 0 new_ss;
  let t2 = global_timestamp () in
  let msg1 = Msg1 gx in
  let w_msg1 = serialize_msg t2 msg1 in
  let i = send #tls13 #t2 a b w_msg1 in
  i,si