val with_buffer_hide
  (#t: Type)
  (b: B.buffer U8.t)
  (from: U32.t)
  (to: U32.t { U32.v from <= U32.v to /\ U32.v to <= B.length b })
  (h0: HS.mem)
  (lin: Ghost.erased B.loc { B.loc_disjoint (Ghost.reveal lin) (B.loc_buffer b) })
  (lout: Ghost.erased B.loc { B.loc_disjoint (Ghost.reveal lout) (B.loc_buffer b) })
  (x1 x2 x3 x4 x5 x6: Ghost.erased U32.t)
  (post: (res: t) ->  (contl: Seq.lseq U8.t (U32.v from)) ->  (cont: Seq.lseq U8.t (U32.v to - U32.v from)) ->  (contr: Seq.lseq U8.t (B.length b - U32.v to)) -> (h: HS.mem) -> GTot Type0)
  (f: (
    (l: Ghost.erased B.loc) ->
    (bl: B.buffer U8.t { B.length bl == (U32.v from) }) ->
    (bs: B.buffer Secret.uint8 { B.length bs == (U32.v to - U32.v from) }) ->
    (br: B.buffer U8.t { B.length br == (B.length b - U32.v to) }) ->
    HST.Stack t
    (requires (fun h ->
      B.modifies l h0 h /\
      B.loc_disjoint (B.loc_buffer bl `B.loc_union` B.loc_buffer bs) (B.loc_buffer br) /\
      B.loc_disjoint (B.loc_buffer bl) (B.loc_buffer bs) /\
      B.loc_disjoint (Ghost.reveal lin `B.loc_union` Ghost.reveal lout) (Ghost.reveal l `B.loc_union` B.loc_buffer bl `B.loc_union` B.loc_buffer bs `B.loc_union` B.loc_buffer br) /\
      B.live h bl /\ B.live h bs /\ B.live h br /\
      B.as_seq h bl == B.as_seq h0 (B.gsub b 0ul from) /\
      B.as_seq h bs == Seq.seq_hide #Secret.U8 (B.as_seq h0 (B.gsub b from (to `U32.sub` from))) /\
      B.as_seq h br == B.as_seq h0 (B.gsub b to (B.len b `U32.sub` to))
    ))
    (ensures (fun h res h' ->
      B.modifies (Ghost.reveal lout `B.loc_union` loc_buffer_from_to_if bl x1 x2 `B.loc_union` loc_buffer_from_to_if bs x3 x4 `B.loc_union` loc_buffer_from_to_if br x5 x6) h h' /\
      post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) (B.as_seq h' br) h'
    ))
  ))
: HST.Stack t
  (requires (fun h ->
    B.live h b /\
    h0 == h
  ))
  (ensures (fun h res h' ->
    B.modifies (Ghost.reveal lout `B.loc_union` loc_buffer_from_to_if (B.gsub b 0ul from) x1 x2 `B.loc_union` loc_buffer_from_to_if (B.gsub b from (to `U32.sub` from)) x3 x4 `B.loc_union` loc_buffer_from_to_if (B.gsub b to (B.len b `U32.sub` to)) x5 x6) h h' /\
    post res (B.as_seq h' (B.gsub b 0ul from)) (B.as_seq h' (B.gsub b from (to `U32.sub` from))) (B.as_seq h' (B.gsub b to (B.len b `U32.sub` to))) h'
  ))
let with_buffer_hide #t b from to h0 lin lout x1 x2 x3 x4 x5 x6 post f =
  let bl = B.sub b 0ul from in
  let bs = B.sub b from (to `U32.sub` from) in
  let br = B.offset b to in
  f (Ghost.hide (B.loc_buffer b)) bl bs br
val with_buffer_hide
  (#t: Type)
  (b: B.buffer U8.t)
  (from: U32.t)
  (to: U32.t { U32.v from <= U32.v to /\ U32.v to <= B.length b })
  (h0: HS.mem)
  (lin: Ghost.erased B.loc { B.loc_disjoint (Ghost.reveal lin) (B.loc_buffer b) })
  (lout: Ghost.erased B.loc { B.loc_disjoint (Ghost.reveal lout) (B.loc_buffer b) })
  (x1 x2 x3 x4 x5 x6: Ghost.erased U32.t)
  (post: (res: t) ->  (contl: Seq.lseq U8.t (U32.v from)) ->  (cont: Seq.lseq U8.t (U32.v to - U32.v from)) ->  (contr: Seq.lseq U8.t (B.length b - U32.v to)) -> (h: HS.mem) -> GTot Type0)
  (f: (
    (l: Ghost.erased B.loc) ->
    (bl: B.buffer U8.t { B.length bl == (U32.v from) }) ->
    (bs: B.buffer Secret.uint8 { B.length bs == (U32.v to - U32.v from) }) ->
    (br: B.buffer U8.t { B.length br == (B.length b - U32.v to) }) ->
    HST.Stack t
    (requires (fun h ->
      B.modifies l h0 h /\
      B.loc_disjoint (B.loc_buffer bl `B.loc_union` B.loc_buffer bs) (B.loc_buffer br) /\
      B.loc_disjoint (B.loc_buffer bl) (B.loc_buffer bs) /\
      B.loc_disjoint (Ghost.reveal lin `B.loc_union` Ghost.reveal lout) (Ghost.reveal l `B.loc_union` B.loc_buffer bl `B.loc_union` B.loc_buffer bs `B.loc_union` B.loc_buffer br) /\
      B.live h bl /\ B.live h bs /\ B.live h br /\
      B.as_seq h bl == B.as_seq h0 (B.gsub b 0ul from) /\
      B.as_seq h bs == Seq.seq_hide #Secret.U8 (B.as_seq h0 (B.gsub b from (to `U32.sub` from))) /\
      B.as_seq h br == B.as_seq h0 (B.gsub b to (B.len b `U32.sub` to))
    ))
    (ensures (fun h res h' ->
      B.modifies (Ghost.reveal lout `B.loc_union` loc_buffer_from_to_if bl x1 x2 `B.loc_union` loc_buffer_from_to_if bs x3 x4 `B.loc_union` loc_buffer_from_to_if br x5 x6) h h' /\
      post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) (B.as_seq h' br) h'
    ))
  ))
: HST.Stack t
  (requires (fun h ->
    B.live h b /\
    h0 == h
  ))
  (ensures (fun h res h' ->
    B.modifies (Ghost.reveal lout `B.loc_union` loc_buffer_from_to_if (B.gsub b 0ul from) x1 x2 `B.loc_union` loc_buffer_from_to_if (B.gsub b from (to `U32.sub` from)) x3 x4 `B.loc_union` loc_buffer_from_to_if (B.gsub b to (B.len b `U32.sub` to)) x5 x6) h h' /\
    post res (B.as_seq h' (B.gsub b 0ul from)) (B.as_seq h' (B.gsub b from (to `U32.sub` from))) (B.as_seq h' (B.gsub b to (B.len b `U32.sub` to))) h'
  ))
let with_buffer_hide #t b from to h0 lin lout x1 x2 x3 x4 x5 x6 post f =
let bl = B.sub b 0ul from in
let bs = B.sub b from (to `U32.sub` from) in
let br = B.offset b to in
f (Ghost.hide (B.loc_buffer b)) bl bs br
QUIC.Secret.Buffer.fst.checked
QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowStar.Endianness.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
QUIC.Secret.Buffer.fst
LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder FStar.Monotonic.HyperStack.mem FStar.Ghost.erased LowStar.Monotonic.Buffer.loc LowStar.Monotonic.Buffer.loc_disjoint FStar.Ghost.reveal LowStar.Monotonic.Buffer.loc_buffer FStar.Seq.Properties.lseq Prims.op_Subtraction Prims.eq2 Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n Lib.IntTypes.uint8 LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_union LowStar.Monotonic.Buffer.live FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.gsub FStar.UInt32.__uint_to_t QUIC.Secret.Seq.seq_hide Lib.IntTypes.U8 FStar.UInt32.sub LowStar.Monotonic.Buffer.len QUIC.Secret.Buffer.loc_buffer_from_to_if QUIC.Secret.Seq.seq_reveal Lib.IntTypes.SEC FStar.Ghost.hide LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.offset LowStar.Buffer.sub
module QUIC.Secret.Buffer

friend Lib.IntTypes

module Secret = QUIC.Secret.Int
module B = LowStar.Buffer
module U8 = FStar.UInt8
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module Seq = QUIC.Secret.Seq
module Ghost = FStar.Ghost

#set-options "--z3rlimit 64" // --query_stats"

#restart-solver

let seq_hide_eq
  (#t: Secret.inttype { Secret.unsigned t })
  (x: Seq.seq (Secret.uint_t t Secret.PUB))
: Lemma
  (Seq.seq_hide x `Seq.equal` x)
  [SMTPat (Seq.seq_hide x)]
= ()

let seq_reveal_eq
  (#t: Secret.inttype { Secret.unsigned t })
  (#sec: Secret.secrecy_level)
  (x: Seq.seq (Secret.uint_t t sec))
: Lemma
  (Seq.seq_reveal x `Seq.equal` x)
  [SMTPat (Seq.seq_reveal x)]
= ()
val with_buffer_hide
  (#t: Type)
  (b: B.buffer U8.t)
  (from: U32.t)
  (to: U32.t { U32.v from <= U32.v to /\ U32.v to <= B.length b })
  (h0: HS.mem)
  (lin: Ghost.erased B.loc { B.loc_disjoint (Ghost.reveal lin) (B.loc_buffer b) })
  (lout: Ghost.erased B.loc { B.loc_disjoint (Ghost.reveal lout) (B.loc_buffer b) })
  (x1 x2 x3 x4 x5 x6: Ghost.erased U32.t)
  (post: (res: t) ->  (contl: Seq.lseq U8.t (U32.v from)) ->  (cont: Seq.lseq U8.t (U32.v to - U32.v from)) ->  (contr: Seq.lseq U8.t (B.length b - U32.v to)) -> (h: HS.mem) -> GTot Type0)
  (f: (
    (l: Ghost.erased B.loc) ->
    (bl: B.buffer U8.t { B.length bl == (U32.v from) }) ->
    (bs: B.buffer Secret.uint8 { B.length bs == (U32.v to - U32.v from) }) ->
    (br: B.buffer U8.t { B.length br == (B.length b - U32.v to) }) ->
    HST.Stack t
    (requires (fun h ->
      B.modifies l h0 h /\
      B.loc_disjoint (B.loc_buffer bl `B.loc_union` B.loc_buffer bs) (B.loc_buffer br) /\
      B.loc_disjoint (B.loc_buffer bl) (B.loc_buffer bs) /\
      B.loc_disjoint (Ghost.reveal lin `B.loc_union` Ghost.reveal lout) (Ghost.reveal l `B.loc_union` B.loc_buffer bl `B.loc_union` B.loc_buffer bs `B.loc_union` B.loc_buffer br) /\
      B.live h bl /\ B.live h bs /\ B.live h br /\
      B.as_seq h bl == B.as_seq h0 (B.gsub b 0ul from) /\
      B.as_seq h bs == Seq.seq_hide #Secret.U8 (B.as_seq h0 (B.gsub b from (to `U32.sub` from))) /\
      B.as_seq h br == B.as_seq h0 (B.gsub b to (B.len b `U32.sub` to))
    ))
    (ensures (fun h res h' ->
      B.modifies (Ghost.reveal lout `B.loc_union` loc_buffer_from_to_if bl x1 x2 `B.loc_union` loc_buffer_from_to_if bs x3 x4 `B.loc_union` loc_buffer_from_to_if br x5 x6) h h' /\
      post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) (B.as_seq h' br) h'
    ))
  ))
: HST.Stack t
  (requires (fun h ->
    B.live h b /\
    h0 == h
  ))
  (ensures (fun h res h' ->
    B.modifies (Ghost.reveal lout `B.loc_union` loc_buffer_from_to_if (B.gsub b 0ul from) x1 x2 `B.loc_union` loc_buffer_from_to_if (B.gsub b from (to `U32.sub` from)) x3 x4 `B.loc_union` loc_buffer_from_to_if (B.gsub b to (B.len b `U32.sub` to)) x5 x6) h h' /\
    post res (B.as_seq h' (B.gsub b 0ul from)) (B.as_seq h' (B.gsub b from (to `U32.sub` from))) (B.as_seq h' (B.gsub b to (B.len b `U32.sub` to))) h'
  ))

    b: LowStar.Buffer.buffer FStar.UInt8.t ->
    from: FStar.UInt32.t ->
    to:
      FStar.UInt32.t
        { FStar.UInt32.v from <= FStar.UInt32.v to /\
          FStar.UInt32.v to <= LowStar.Monotonic.Buffer.length b } ->
    h0: FStar.Monotonic.HyperStack.mem ->
    lin:
      FStar.Ghost.erased LowStar.Monotonic.Buffer.loc
        { LowStar.Monotonic.Buffer.loc_disjoint (FStar.Ghost.reveal lin)
            (LowStar.Monotonic.Buffer.loc_buffer b) } ->
    lout:
      FStar.Ghost.erased LowStar.Monotonic.Buffer.loc
        { LowStar.Monotonic.Buffer.loc_disjoint (FStar.Ghost.reveal lout)
            (LowStar.Monotonic.Buffer.loc_buffer b) } ->
    x1: FStar.Ghost.erased FStar.UInt32.t ->
    x2: FStar.Ghost.erased FStar.UInt32.t ->
    x3: FStar.Ghost.erased FStar.UInt32.t ->
    x4: FStar.Ghost.erased FStar.UInt32.t ->
    x5: FStar.Ghost.erased FStar.UInt32.t ->
    x6: FStar.Ghost.erased FStar.UInt32.t ->
    post:
      (
            res: t ->
            contl: FStar.Seq.Properties.lseq FStar.UInt8.t (FStar.UInt32.v from) ->
            cont: FStar.Seq.Properties.lseq FStar.UInt8.t (FStar.UInt32.v to - FStar.UInt32.v from) ->
            contr:
              FStar.Seq.Properties.lseq FStar.UInt8.t
                (LowStar.Monotonic.Buffer.length b - FStar.UInt32.v to) ->
            h: FStar.Monotonic.HyperStack.mem
          -> Prims.GTot Type0) ->
    f:
      (
            l: FStar.Ghost.erased LowStar.Monotonic.Buffer.loc ->
            bl:
              LowStar.Buffer.buffer FStar.UInt8.t
                {LowStar.Monotonic.Buffer.length bl == FStar.UInt32.v from} ->
            bs:
              LowStar.Buffer.buffer Lib.IntTypes.uint8
                {LowStar.Monotonic.Buffer.length bs == FStar.UInt32.v to - FStar.UInt32.v from} ->
            br:
              LowStar.Buffer.buffer FStar.UInt8.t
                { LowStar.Monotonic.Buffer.length br ==
                  LowStar.Monotonic.Buffer.length b - FStar.UInt32.v to }
          -> FStar.HyperStack.ST.Stack t)
  -> FStar.HyperStack.ST.Stack t