anchor.diff:      | sid ->
           SessionDB.insert sDB sinfo.sessionID (sinfo, ms, role)
   
  +// FIXME: Seems we can skip this function with the new state machine *)
  +(*
   let goToIdle state =
       let init_sessionInfo = null_sessionInfo state.poptions.minVer in
       match state.pstate with
  
positive.code:    (* by convention, the parameters are named si, cv, cr', sr', ms, log *)
     | ServerWritingCCS     of SessionInfo * StatefulAEAD.writer * bytes (* outgoing after CCS; this and next state shared only for full HS *)
     | ServerWritingFinished
     | ServerWritingCCSRes  of SessionInfo * crand * srand * masterSecret * log
     | ClientCCSResume      of SessionInfo * crand * srand * masterSecret * log  
     | ClientFinishedResume of SessionInfo * masterSecret * log 
     | ServerIdle   
     (* the ProtocolVersion is the highest TLS version proposed by the client *)
  
  
negative.code: let makeCCSFragment ki b = makeFragment ki b
  
  let next_fragment ci state =
      match state.hs_outgoing with
      | [||] ->
          match state.pstate with
          | PSClient(cstate) ->
              match cstate with
              | 
  
  
      (* Assumptions: The buffers have been filled in the following order:
         1) hs_outgoing; 2) ccs_outgoing; 3) hs_outgoing_after_ccs
         We check 2) and 3) only if we are in a {C,S}WaitingToWrite state.
  