val as_header (h: QUIC.Impl.header) (packet_number: PN.packet_number_t)
    : Stack QUIC.Spec.header
      (requires fun h0 -> QUIC.Impl.header_live h h0)
      (ensures fun h0 r h1 -> h0 == h1 /\ r == QUIC.Impl.g_header h h0 packet_number)
val as_header (h: QUIC.Impl.header) (packet_number: PN.packet_number_t)
    : Stack QUIC.Spec.header
      (requires fun h0 -> QUIC.Impl.header_live h h0)
      (ensures fun h0 r h1 -> h0 == h1 /\ r == QUIC.Impl.g_header h h0 packet_number)
let as_header (h: QUIC.Impl.header) (packet_number: PN.packet_number_t) : Stack QUIC.Spec.header
  (requires fun h0 ->
    QUIC.Impl.header_live h h0)
  (ensures fun h0 r h1 ->
    h0 == h1 /\
    r == QUIC.Impl.g_header h h0 packet_number)
=
  let _ = allow_inversion QImplBase.header in
  let _ = allow_inversion QImplBase.long_header_specifics in

  let x = packet_number in
  let open QUIC.Impl in
  let open QUIC.Spec.Header.Base in
  let packet_number = x in
  match h with
  | BShort rb spin phase cid cid_len packet_number_length ->
    // Insane type errors if I don't put everything in A-normal form.
    let bar: S.seq UInt8.t = as_seq cid cid_len in
    let foo: vlbytes 0 20 = fstar_bytes_of_seq bar in
    MShort
      (reveal_bitfield rb)
      spin
      (nat_of_u8 phase = 1)
      foo
      packet_number_length packet_number
  | BLong version dcid dcil scid scil spec ->
    let dcid' = as_seq dcid dcil in
    let scid' = as_seq scid scil in
    [@inline_let]
    let f = MLong version (LowParse.SLow.Base.bytes_of_seq dcid') (LowParse.SLow.Base.bytes_of_seq scid') in
    begin match spec with
      | BInitial rb payload_length packet_number_length token token_length ->
        let token' = as_seq token token_length in
        f (MInitial (reveal_bitfield rb) (LowParse.SLow.Base.bytes_of_seq token') payload_length packet_number_length packet_number)
      | BZeroRTT rb payload_length packet_number_length ->
        f (MZeroRTT (reveal_bitfield rb) payload_length packet_number_length packet_number)
      | BHandshake rb payload_length packet_number_length ->
        f (MHandshake (reveal_bitfield rb) payload_length packet_number_length packet_number)
      | BRetry unused odcid odcil ->
        let odcid' = as_seq odcid odcil in
        f (MRetry (reveal_bitfield unused) (LowParse.SLow.Base.bytes_of_seq odcid'))
    end
module QUIC

module QSpec = QUIC.Spec
module QImpl = QUIC.State
module QImplBase = QUIC.Impl.Header.Base
module QModel = Model.QUIC

module I = Model.Indexing
module G = FStar.Ghost
module B = LowStar.Buffer
module S = FStar.Seq
module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST

module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U8 = FStar.UInt8

open FStar.HyperStack
open FStar.HyperStack.ST

open EverCrypt.Helpers
open EverCrypt.Error

// The switch only makes sense in the non-ideal case. (Unsurprisingly: if we
// replace data by random values, functional correctness no longer holds!)
let index =
  if I.model then i:QModel.id { QModel.unsafe i } else QImpl.index

let mid (i:index{I.model}) = i <: QModel.id
let iid (i:index{not I.model}) = i <: QImpl.index

let alg (i:index) =
  if I.model then I.ae_id_ginfo (dfst (mid i))
  else (iid i).QImpl.aead_alg

let halg (i:index) =
  if I.model then I.ae_id_ghash (dfst (mid i))
  else (iid i).QImpl.hash_alg

let itraffic_secret (i:QModel.id) =
  Spec.Hash.Definitions.bytes_hash (I.ae_id_ghash (dfst i))

module MH = Model.Helpers

let derived (#i:QModel.id) (#w:QModel.stream_writer i) (r:QModel.stream_reader w) (ts:itraffic_secret i) =
  if I.model && QModel.unsafe i then
    let ha = I.ae_id_hash (dfst i) in
    let ea = I.ae_id_info (dfst i) in
    let (k1, k2) = QModel.reader_leak r in
    MH.hide (QModel.writer_static_iv w) ==
      QSpec.derive_secret ha ts QSpec.label_iv 12 /\
    MH.hide k1 == QSpec.derive_secret ha ts
        QSpec.label_key (QSpec.cipher_keysize ea) /\
    MH.hide k2 == QUIC.Spec.derive_secret ha ts
        QUIC.Spec.label_hp (QSpec.cipher_keysize ea)
  else True

noeq type mstate_t i =
| Ideal:
  writer: QModel.stream_writer i ->
  reader: QModel.stream_reader writer ->
  ts: itraffic_secret i{derived reader ts} -> // FIXME erased
  mstate_t i

let istate_t i = QImpl.state i

noeq
type raise (i: index { not I.model }): Type u#1 = | Raise: s:istate_t i -> raise i

let state i =
  if I.model then mstate_t (mid i)
  else raise (iid i)

let mstate (#i:index{I.model}) (s:state i) = s <: mstate_t (mid i)
let istate (#i:index{not I.model}) (s:state i) = (s <: raise (iid i)).s

let footprint #i h s =
  if I.model then
    QModel.rfootprint (mstate s).reader `B.loc_union` QModel.footprint (mstate s).writer
  else QImpl.footprint h (istate s)

let invariant #i h s =
  if I.model then
    let Ideal writer reader _ = mstate s in
    QModel.invariant writer h /\ QModel.rinvariant reader h /\
    B.loc_disjoint (QModel.rfootprint (mstate s).reader) (QModel.footprint (mstate s).writer)
  else QImpl.invariant h (istate s)

let g_traffic_secret #i s h =
  if I.model then (mstate s).ts
  else
    QImpl.g_traffic_secret (B.deref h (istate s))

let g_initial_packet_number #i s h =
  assert_norm (pow2 62 - 1 < pow2 64);
  if I.model then
    Lib.IntTypes.u64 (QModel.writer_offset #(mid i) (mstate s).writer)
  else
    QImpl.g_initial_packet_number (B.deref h (istate s))

let g_last_packet_number #i s h =
  assert_norm (pow2 62 - 1 < pow2 64);
  if I.model then
    Lib.IntTypes.u64 (QModel.expected_pnT #(mid i) (mstate s).reader h)
  else
    QImpl.g_last_packet_number (B.deref h (istate s)) h

let g_next_packet_number #i s h =
  assert_norm (pow2 62 - 1 < pow2 64);
  if I.model then
    Lib.IntTypes.u64 (QModel.wctrT #(mid i) (mstate s).writer h)
  else
    QImpl.g_last_packet_number (B.deref h (istate s)) h

// TODO: reveal in the interface (just for good measure)
let frame_invariant #i l s h0 h1 =
  if I.model then
    let Ideal w r _ = mstate #(mid i) s in
    QModel.frame_invariant w h0 l h1;
    QModel.rframe_invariant r h0 l h1
  else
    QImpl.frame_invariant #(iid i) l s h0 h1

/// Ingredients we need for the mythical switch

/// First, a stateful equivalent of as_seq. Implementation doesn't need to be
/// efficient.

let rec as_seq #a (b: B.buffer a) (l: UInt32.t { l == B.len b }): Stack (S.seq a)
  (requires fun h0 ->
    B.live h0 b)
  (ensures fun h0 r h1 ->
    h0 == h1 /\
    B.as_seq h0 b `S.equal` r)
=
  let h0 = ST.get () in
  if l = 0ul then
    S.empty
  else
    let hd = B.index b 0ul in
    let l = l `U32.sub` 1ul in
    let b = B.sub b 1ul l in
    S.cons hd (as_seq b l)

let rec from_seq #a (dst: B.buffer a) (s: S.seq a): Stack unit
  (requires fun h0 ->
    B.live h0 dst /\
    B.length dst == S.length s)
  (ensures fun h0 _ h1 ->
    B.modifies (B.loc_buffer dst) h0 h1 /\
    B.as_seq h1 dst `S.equal` s)
=
  if S.length s = 0 then
    ()
  else begin
    let hd = B.sub dst 0ul 1ul in
    let tl = B.sub dst 1ul (UInt32.uint_to_t (S.length s - 1)) in
    B.upd hd 0ul (S.index s 0);
    from_seq tl (S.slice s 1 (S.length s));
    let h1 = ST.get () in
    calc (S.equal) {
      B.as_seq h1 dst;
    (S.equal) { }
      S.append (S.slice (B.as_seq h1 hd) 0 1) (S.slice (B.as_seq h1 dst) 1 (S.length s));
    (S.equal) { }
      S.append (S.create 1 (S.index s 0)) (S.slice (B.as_seq h1 dst) 1 (S.length s));
    (S.equal) { }
      S.append (S.create 1 (S.index s 0)) (S.slice s 1 (S.length s));
    (S.equal) { }
      s;
    }
  end

#set-options "--fuel 0 --ifuel 0 --z3rlimit 200 --using_facts_from '*,-LowStar.Monotonic.Buffer.unused_in_not_unused_in_disjoint_2'"

let nat_of_u8 (x: Lib.IntTypes.uint8) =
  UInt8.v (Lib.RawIntTypes.u8_to_UInt8 x)

let reveal_bitfield #n (x: QUIC.Spec.secret_bitfield n): QUIC.Spec.bitfield n =
  Lib.RawIntTypes.u8_to_UInt8 x

let fstar_bytes_of_seq (s: S.seq UInt8.t):
  Pure FStar.Bytes.bytes
    (requires S.length s < pow2 32)
    (ensures fun b -> FStar.Bytes.reveal b `S.equal` s)
=
  assert_norm (pow2 32 = 4294967296);
  LowParse.SLow.Base.bytes_of_seq s
/
Spec.Hash.Definitions.fst.checked Spec.Agile.AEAD.fsti.checked QUIC.State.fsti.checked QUIC.Spec.Header.Base.fst.checked QUIC.Spec.fsti.checked QUIC.Secret.Seq.fsti.checked QUIC.Impl.Header.Base.fst.checked QUIC.Impl.fsti.checked prims.fst.checked Model.QUIC.fsti.checked Model.Indexing.fsti.checked Model.Helpers.fsti.checked Model.AEAD.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked LowParse.SLow.Base.fst.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked FStar.Bytes.fsti.checked EverCrypt.Helpers.fsti.checked EverCrypt.Error.fsti.checked
QUIC.fst
h: QUIC.Impl.Header.Base.header -> packet_number: QUIC.Spec.PacketNumber.Base.packet_number_t
  -> FStar.HyperStack.ST.Stack QUIC.Spec.Header.Base.header
QUIC.Impl.Header.Base.header QUIC.Spec.PacketNumber.Base.packet_number_t QUIC.Spec.Base.secret_bitfield Prims.bool LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t Prims.l_and Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Prims.op_LessThanOrEqual FStar.UInt.uint_t FStar.UInt32.v QUIC.Spec.PacketNumber.Base.packet_number_length_t QUIC.Spec.Header.Base.MShort QUIC.reveal_bitfield Prims.op_Equality QUIC.nat_of_u8 QUIC.Spec.Base.vlbytes QUIC.fstar_bytes_of_seq QUIC.Spec.Header.Base.header FStar.Seq.Base.seq QUIC.as_seq QUIC.Impl.Header.Base.long_header_specifics QUIC.Spec.Base.payload_and_pn_length_t QUIC.Spec.Base.token_max_len QUIC.Spec.Header.Base.MInitial LowParse.SLow.Base.bytes_of_seq QUIC.Spec.Header.Base.MZeroRTT QUIC.Spec.Header.Base.MHandshake QUIC.Spec.Header.Base.MRetry QUIC.Spec.Header.Base.long_header_specifics QUIC.Spec.Header.Base.MLong Prims.unit FStar.Pervasives.allow_inversion FStar.Monotonic.HyperStack.mem QUIC.Impl.Header.Base.header_live QUIC.Impl.Header.Base.g_header
let as_header (h: QUIC.Impl.header) (packet_number: PN.packet_number_t)
    : Stack QUIC.Spec.header
      (requires fun h0 -> QUIC.Impl.header_live h h0)
      (ensures fun h0 r h1 -> h0 == h1 /\ r == QUIC.Impl.g_header h h0 packet_number) =
  
let _ = allow_inversion QImplBase.header in
let _ = allow_inversion QImplBase.long_header_specifics in
let x = packet_number in
let open QUIC.Impl in
let open QUIC.Spec.Header.Base in
let packet_number = x in
match h with
| BShort rb spin phase cid cid_len packet_number_length ->
  let bar:S.seq UInt8.t = as_seq cid cid_len in
  let foo:vlbytes 0 20 = fstar_bytes_of_seq bar in
  MShort (reveal_bitfield rb) spin (nat_of_u8 phase = 1) foo packet_number_length packet_number
| BLong version dcid dcil scid scil spec ->
  let dcid' = as_seq dcid dcil in
  let scid' = as_seq scid scil in
  [@@ inline_let ]let f =
    MLong version (LowParse.SLow.Base.bytes_of_seq dcid') (LowParse.SLow.Base.bytes_of_seq scid')
  in
  match spec with
  | BInitial rb payload_length packet_number_length token token_length ->
    let token' = as_seq token token_length in
    f (MInitial (reveal_bitfield rb)
          (LowParse.SLow.Base.bytes_of_seq token')
          payload_length
          packet_number_length
          packet_number)
  | BZeroRTT rb payload_length packet_number_length ->
    f (MZeroRTT (reveal_bitfield rb) payload_length packet_number_length packet_number)
  | BHandshake rb payload_length packet_number_length ->
    f (MHandshake (reveal_bitfield rb) payload_length packet_number_length packet_number)
  | BRetry unused odcid odcil ->
    let odcid' = as_seq odcid odcil in
    f (MRetry (reveal_bitfield unused) (LowParse.SLow.Base.bytes_of_seq odcid'))