Tests towards replacing Old.Handshake.recv_fragment

[nikswamy]

All of this is with respect to the dev branch, unless otherwise made explicit.

Please see Old.Handshake.recv_fragment in the dev branch.
https://github.com/project-everest/mitls-fstar/blob/dev/src/tls/Old.Handshake.fst#L1196

It currently provides a bytes-oriented interface to the rest of the handshake.

val recv_fragment: s:hs -> #i:TLSInfo.id -> rg:Range.frange i -> f:Range.rbytes rg -> ST incoming (* incoming transitions for our state machine *)
      (requires (hs_inv s))
        (ensures (recv_ensures s))

For the foreseeable future, we will continue to provide this bytes-oriented interface to avoid breaking the rest of the handshake.

However, internally, we want to revise the implementation of recv_fragement so that it calls HSL.Receive and HSL.Transcript, the new low-level code.

Towards that end, we want tests that exercise a few representative cases of the implementation of recv_fragment. These tests will guide the eventual rewriting of Old.Handshake, which will be done by @fournet and @adl.

Cedric proposes test code implemented in a separate file that comes in two parts:

I propose we write our new receive _fragment based on TLS.Handshake.Machine (adapting that module if need be) independently of Old.Handshake. I started, for now at the end of that file. It lax typechecks, with lots of gaps, but it should be more precise than the outlines below.

1. A function with the following (partial) signature

     val recv_fragment: 
       ts: Transcript.state (* todo: add ghost transcript *) -> 
       rs:rcv_state (* machine state for now in rs.flt *) -> 
       new_rcv_to: UInt32.t (* the new fragment is in rs.rcv.[rs.recv_to..new_rcv_to] *) -> 
         ST (Transcript.state (* todo: add new ghost transcript *) * rcv_state * incoming)

A definition for rcv_state is presented in experiments/TLS.Handshake.Machine.fst
https://github.com/project-everest/mitls-fstar/blob/dev/src/tls/experiments/TLS.Handshake.Machine.fst#L58

For defining rcv_state and its auxiliary functions,. do we extend HSL.Receive.fsti or write an intermediate TLS.Handshake.Receive as a counterpart for my new TLS.Handshake.Send ?.

Internally, it should support transitions from the following states as seen on Old.Handshake:

   - C13_wait_Finished1 (3 cases)
   - C_wait_ServerHello (1 case)
   - S_Idle (1 case)

However, these three states are now renamed in HSL.Receive.fsti to easily identified counterparts.

I don't understand this remark. See the explicit linking of Handshake and Flight state in TLS.Handshake.Machine.

Relevant to this task are existing test that are available from @R1kM in https://github.com/project-everest/mitls-fstar/blob/afromher_dev/src/tls/Test.TLS.Send.fst#L310
- It (almost) uses Cedric's TLS.Handshake.Machine receiving state
- The invariant https://github.com/project-everest/mitls-fstar/blob/afromher_dev/src/tls/Test.TLS.Send.fst#L332 allows to easily change receiving states after completely parsing one message thanks to Aseem's interface
- The postcondition is not complete yet, it might require more interleaving of the receiving part and the handling part, but I would like to discuss this tomorrow

Similarly I'd prefer to rebase this example on TLS.Handshake.Machine instead of Old.Handshake.

2. An adapter function to call recv_fragment with bytes:

val buffer_recv_fragment: 
  rs: recv_state -> 
  f: bytes -> 
  ST recv_state 
  (requires fun h0 -> inv rs h0)
  (ensures fun h0 rs h1 -> 
    modifies h0 h1 rs.rcv /\ 
    inv rs h1) 

This function should fill in the bytes f into the recv_state's input buffer at the current writing offset.

See also buffer_received_fragment at the end of TLS.Handshake.Machine; I hope we can simplify the calling convention.

3. A composite function that combines buffer_recv_fragment and recv_fragment to provide:

     val recv_fragment_bytes: 
       ts: Transcript.state (* todo: add ghost transcript *) -> 
       rs:rcv_state (* machine state for now in rs.flt *) -> 
       f:bytes -> 
         ST (Transcript.state (* todo: add new ghost transcript *) * rcv_state * incoming)

We need to keep recv_fragment unchanged, as it is part of the stable Handshake API. So let's name our new (1) function e.g. receive_fragment.

[aseemr]

See this for a wrapper over HSL.Receive as expected by TLS.Handshake.Machine: https://github.com/project-everest/mitls-fstar/blob/dev/src/tls/experiments/HSL.Receive.Wrapper.fst.

It also contains an implementation of buffer_received_fragment. The way the invariant of this wrapper is structured, I think it should be simple to call HSL.Receive.receive functions. Trying one out is the next step.