add missing ST function declarations (cf. FStarLang/FStar#1055)

src/tls/HSL.Receive.fst

@@ -183,7 +183,24 @@ private let err_or_insufficient_data
 ///   and then either return an error or the flight flt
 
 inline_for_extraction noextract
-let check_end_index_and_return (#a:Type) (st:hsl_state) (pos f_end:uint_32) (flt:a) =
+let check_end_index_and_return
+  (#a:Type)
+  (st:hsl_state)
+  (pos f_end:uint_32)
+  (flt:a)
+: Stack (TLSError.result (option a))
+  (requires (fun h -> B.live h st.inc_st))
+  (ensures (fun h0 res h1 ->
+    B.modifies (footprint st) h0 h1 /\ (
+    if pos <> f_end
+    then
+      E.Error? res /\ B.as_seq h1 st.inc_st == B.as_seq h0 st.inc_st
+    else
+      res == E.Correct (Some flt) /\
+      parsed_bytes st h1 == Seq.empty /\
+      in_progress_flt st h1 == F_none
+  )))
+=
   if pos <> f_end then E.Error bytes_remain_error
   else begin
     reset_incremental_state st;

src/tls/IdNonce.fst

@@ -24,7 +24,23 @@ let nonce_id_table : MDM.t tls_tables_region random n_id (fun x -> True) =
 
 let id_of_nonce (n:random) (i:n_id n) = HST.witnessed (MDM.contains nonce_id_table n i)
 
-let insert n i =
+val insert:
+  n: random ->
+  i: n_id n ->
+  ST unit
+  (requires (fun h ->
+    ~ (MDM.defined nonce_id_table n h)
+  ))
+  (ensures (fun h0 _ h1 ->
+    let cur = HS.sel h0 nonce_id_table in
+    HS.contains h1 nonce_id_table /\
+    HS.modifies (Set.singleton tls_tables_region) h0 h1 /\
+    HS.modifies_ref tls_tables_region (Set.singleton (HS.as_addr nonce_id_table)) h0 h1 /\
+    HS.sel h1 nonce_id_table == MDM.upd cur n i /\
+    witnessed (MDM.contains nonce_id_table n i)
+  ))
+
+let insert n i=
   HST.recall nonce_id_table;
   MDM.extend nonce_id_table n i
 

src/tls/Transport.fst

@@ -46,6 +46,19 @@ noeq type t = {
 
 let callbacks v send recv: t = { ptr = v; snd = send; rcv = recv }
 
+val send:
+  t ->
+  buffer: FStar.Buffer.buffer UInt8.t ->
+  len: size_t ->
+  ST Int32.t
+  (requires fun h0 -> 
+    Buffer.live h0 buffer /\ 
+    UInt32.v len = Buffer.length buffer)
+  (ensures fun h0 r h1 -> 
+    let v = Int32.v r in
+    modifies_none h0 h1 /\
+    (v = -1 \/ (0 <= v /\ v <= UInt32.v len)))
+
 // following the indirection
 let send t buffer len = t.snd t.ptr buffer len