val with_buffer_hide_from_weak_modifies
      (#t: Type)
      (b: B.buffer U8.t)
      (from: U32.t{U32.v from <= 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)})
      (modifies_left modifies_secret: Ghost.erased bool)
      (post:
          (
                res: t ->
                contl: Seq.lseq U8.t (U32.v from) ->
                cont: Seq.lseq U8.t (B.length b - U32.v from) ->
                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 == (B.length b - U32.v from)}
              -> HST.Stack t
                  (requires
                    (fun h ->
                        B.modifies l h0 h /\ 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.live h bl /\ B.live h bs /\
                        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 ((B.len b) `U32.sub` from)))))
                  (ensures
                    (fun h res h' ->
                        B.modifies (((Ghost.reveal lout)
                              `B.loc_union`
                              (if Ghost.reveal modifies_left then B.loc_buffer bl else B.loc_none))
                            `B.loc_union`
                            (if Ghost.reveal modifies_secret then B.loc_buffer bs else B.loc_none))
                          h
                          h' /\ post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) 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`
                  (if Ghost.reveal modifies_left
                    then B.loc_buffer (B.gsub b 0ul from)
                    else B.loc_none))
                `B.loc_union`
                (if Ghost.reveal modifies_secret
                  then B.loc_buffer (B.gsub b from ((B.len b) `U32.sub` from))
                  else B.loc_none))
              h
              h' /\
            post res
              (B.as_seq h' (B.gsub b 0ul from))
              (B.as_seq h' (B.gsub b from ((B.len b) `U32.sub` from)))
              h'))
let with_buffer_hide_from_weak_modifies
  (#t: Type)
  (b: B.buffer U8.t)
  (from: U32.t { U32.v from <= 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) })
  (modifies_left modifies_secret: Ghost.erased bool)
  (post: (res: t) ->  (contl: Seq.lseq U8.t (U32.v from)) ->  (cont: Seq.lseq U8.t (B.length b - U32.v from)) -> (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 == (B.length b - U32.v from) }) ->
    HST.Stack t
    (requires (fun h ->
      B.modifies l h0 h /\
      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.live h bl /\ B.live h bs /\
      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 (B.len b `U32.sub` from)))
    ))
    (ensures (fun h res h' ->
      B.modifies (Ghost.reveal lout `B.loc_union` (if Ghost.reveal modifies_left then B.loc_buffer bl else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_secret then B.loc_buffer bs else B.loc_none)) h h' /\
      post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) 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` (if Ghost.reveal modifies_left then B.loc_buffer (B.gsub b 0ul from) else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_secret then B.loc_buffer (B.gsub b from (B.len b `U32.sub` from)) else B.loc_none)) h h' /\
    post res (B.as_seq h' (B.gsub b 0ul from)) (B.as_seq h' (B.gsub b from (B.len b `U32.sub` from))) h'
  ))
=
  with_buffer_hide_from
    b
    from
    h0
    lin
    lout
    (if Ghost.reveal modifies_left then 0ul else 1ul) (if Ghost.reveal modifies_left then from else 0ul)
    (if Ghost.reveal modifies_secret then 0ul else 1ul) (if Ghost.reveal modifies_secret then B.len b `U32.sub` from else 0ul)
    post
    (fun l bl bs ->
      B.gsub_zero_length bl;
      B.gsub_zero_length bs;
      f l bl bs
    )
val with_buffer_hide_from_weak_modifies
      (#t: Type)
      (b: B.buffer U8.t)
      (from: U32.t{U32.v from <= 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)})
      (modifies_left modifies_secret: Ghost.erased bool)
      (post:
          (
                res: t ->
                contl: Seq.lseq U8.t (U32.v from) ->
                cont: Seq.lseq U8.t (B.length b - U32.v from) ->
                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 == (B.length b - U32.v from)}
              -> HST.Stack t
                  (requires
                    (fun h ->
                        B.modifies l h0 h /\ 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.live h bl /\ B.live h bs /\
                        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 ((B.len b) `U32.sub` from)))))
                  (ensures
                    (fun h res h' ->
                        B.modifies (((Ghost.reveal lout)
                              `B.loc_union`
                              (if Ghost.reveal modifies_left then B.loc_buffer bl else B.loc_none))
                            `B.loc_union`
                            (if Ghost.reveal modifies_secret then B.loc_buffer bs else B.loc_none))
                          h
                          h' /\ post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) 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`
                  (if Ghost.reveal modifies_left
                    then B.loc_buffer (B.gsub b 0ul from)
                    else B.loc_none))
                `B.loc_union`
                (if Ghost.reveal modifies_secret
                  then B.loc_buffer (B.gsub b from ((B.len b) `U32.sub` from))
                  else B.loc_none))
              h
              h' /\
            post res
              (B.as_seq h' (B.gsub b 0ul from))
              (B.as_seq h' (B.gsub b from ((B.len b) `U32.sub` from)))
              h'))
let with_buffer_hide_from_weak_modifies
      (#t: Type)
      (b: B.buffer U8.t)
      (from: U32.t{U32.v from <= 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)})
      (modifies_left modifies_secret: Ghost.erased bool)
      (post:
          (
                res: t ->
                contl: Seq.lseq U8.t (U32.v from) ->
                cont: Seq.lseq U8.t (B.length b - U32.v from) ->
                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 == (B.length b - U32.v from)}
              -> HST.Stack t
                  (requires
                    (fun h ->
                        B.modifies l h0 h /\ 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.live h bl /\ B.live h bs /\
                        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 ((B.len b) `U32.sub` from)))))
                  (ensures
                    (fun h res h' ->
                        B.modifies (((Ghost.reveal lout)
                              `B.loc_union`
                              (if Ghost.reveal modifies_left then B.loc_buffer bl else B.loc_none))
                            `B.loc_union`
                            (if Ghost.reveal modifies_secret then B.loc_buffer bs else B.loc_none))
                          h
                          h' /\ post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) 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`
                  (if Ghost.reveal modifies_left
                    then B.loc_buffer (B.gsub b 0ul from)
                    else B.loc_none))
                `B.loc_union`
                (if Ghost.reveal modifies_secret
                  then B.loc_buffer (B.gsub b from ((B.len b) `U32.sub` from))
                  else B.loc_none))
              h
              h' /\
            post res
              (B.as_seq h' (B.gsub b 0ul from))
              (B.as_seq h' (B.gsub b from ((B.len b) `U32.sub` from)))
              h')) =
with_buffer_hide_from b from h0 lin lout (if Ghost.reveal modifies_left then 0ul else 1ul)
  (if Ghost.reveal modifies_left then from else 0ul)
  (if Ghost.reveal modifies_secret then 0ul else 1ul)
  (if Ghost.reveal modifies_secret then (B.len b) `U32.sub` from else 0ul) post
  (fun l bl bs ->
      B.gsub_zero_length bl;
      B.gsub_zero_length bs;
      f l bl bs)
QUIC.Secret.Buffer.fsti.checked
QUIC.Secret.Seq.fsti.checked QUIC.Secret.Int.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
QUIC.Secret.Buffer.fsti
LowStar.Buffer.buffer FStar.UInt8.t FStar.UInt32.t 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 Prims.bool 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 Prims.l_and 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 Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC QUIC.Secret.Seq.seq_hide FStar.UInt32.sub LowStar.Monotonic.Buffer.len LowStar.Monotonic.Buffer.loc_none QUIC.Secret.Seq.seq_reveal QUIC.Secret.Buffer.with_buffer_hide_from FStar.Ghost.hide Prims.unit LowStar.Monotonic.Buffer.gsub_zero_length
module QUIC.Secret.Buffer

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

module U32 = FStar.UInt32

#set-options "--z3rlimit 32"

let loc_buffer_from_to_if
  (#t: Type)
  (b: B.buffer t)
  (from to: U32.t)
: GTot B.loc
= if U32.v to < U32.v from || U32.v to > B.length b
  then B.loc_none
  else B.loc_buffer (B.gsub b from (to `U32.sub` from))

inline_for_extraction
noextract
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'
  ))

inline_for_extraction
noextract
let with_buffer_hide_weak_modifies
  (#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) })
  (modifies_left modifies_secret modifies_right: Ghost.erased bool)
  (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` (if Ghost.reveal modifies_left then B.loc_buffer bl else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_secret then B.loc_buffer bs else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_right then B.loc_buffer br else B.loc_none)) 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` (if Ghost.reveal modifies_left then B.loc_buffer (B.gsub b 0ul from) else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_secret then B.loc_buffer (B.gsub b from (to `U32.sub` from)) else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_right then B.loc_buffer (B.gsub b to (B.len b `U32.sub` to)) else B.loc_none)) 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'
  ))
=
  with_buffer_hide
    b
    from
    to
    h0
    lin
    lout
    (if Ghost.reveal modifies_left then 0ul else 1ul) (if Ghost.reveal modifies_left then from else 0ul)
    (if Ghost.reveal modifies_secret then 0ul else 1ul) (if Ghost.reveal modifies_secret then (to `U32.sub` from) else 0ul)
    (if Ghost.reveal modifies_right then 0ul else 1ul) (if Ghost.reveal modifies_right then (B.len b `U32.sub` to) else 0ul)
    post
    (fun l bl bs br ->
      B.gsub_zero_length bl;
      B.gsub_zero_length bs;
      B.gsub_zero_length br;
      f l bl bs br
    )

(* NOTE: this CANNOT be derived from with_buffer_hide, because `to` should be the length, which is ghost *)

inline_for_extraction
noextract
val with_buffer_hide_from
  (#t: Type)
  (b: B.buffer U8.t)
  (from: U32.t { U32.v from <= 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: Ghost.erased U32.t)
  (post: (res: t) ->  (contl: Seq.lseq U8.t (U32.v from)) ->  (cont: Seq.lseq U8.t (B.length b - U32.v from)) -> (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 == (B.length b - U32.v from) }) ->
    HST.Stack t
    (requires (fun h ->
      B.modifies l h0 h /\
      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.live h bl /\ B.live h bs /\
      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 (B.len b `U32.sub` from)))
    ))
    (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) h h' /\
      post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) 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 (B.len b `U32.sub` from)) x3 x4) h h' /\
    post res (B.as_seq h' (B.gsub b 0ul from)) (B.as_seq h' (B.gsub b from (B.len b `U32.sub` from))) h'
  ))

inline_for_extraction
noextract
let with_buffer_hide_from_weak_modifies
  (#t: Type)
  (b: B.buffer U8.t)
  (from: U32.t { U32.v from <= 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) })
  (modifies_left modifies_secret: Ghost.erased bool)
  (post: (res: t) ->  (contl: Seq.lseq U8.t (U32.v from)) ->  (cont: Seq.lseq U8.t (B.length b - U32.v from)) -> (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 == (B.length b - U32.v from) }) ->
    HST.Stack t
    (requires (fun h ->
      B.modifies l h0 h /\
      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.live h bl /\ B.live h bs /\
      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 (B.len b `U32.sub` from)))
    ))
    (ensures (fun h res h' ->
      B.modifies (Ghost.reveal lout `B.loc_union` (if Ghost.reveal modifies_left then B.loc_buffer bl else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_secret then B.loc_buffer bs else B.loc_none)) h h' /\
      post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) 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` (if Ghost.reveal modifies_left then B.loc_buffer (B.gsub b 0ul from) else B.loc_none) `B.loc_union` (if Ghost.reveal modifies_secret then B.loc_buffer (B.gsub b from (B.len b `U32.sub` from)) else B.loc_none)) h h' /\
    post res (B.as_seq h' (B.gsub b 0ul from)) (B.as_seq h' (B.gsub b from (B.len b `U32.sub` from))) h'
  ))
val with_buffer_hide_from_weak_modifies
      (#t: Type)
      (b: B.buffer U8.t)
      (from: U32.t{U32.v from <= 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)})
      (modifies_left modifies_secret: Ghost.erased bool)
      (post:
          (
                res: t ->
                contl: Seq.lseq U8.t (U32.v from) ->
                cont: Seq.lseq U8.t (B.length b - U32.v from) ->
                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 == (B.length b - U32.v from)}
              -> HST.Stack t
                  (requires
                    (fun h ->
                        B.modifies l h0 h /\ 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.live h bl /\ B.live h bs /\
                        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 ((B.len b) `U32.sub` from)))))
                  (ensures
                    (fun h res h' ->
                        B.modifies (((Ghost.reveal lout)
                              `B.loc_union`
                              (if Ghost.reveal modifies_left then B.loc_buffer bl else B.loc_none))
                            `B.loc_union`
                            (if Ghost.reveal modifies_secret then B.loc_buffer bs else B.loc_none))
                          h
                          h' /\ post res (B.as_seq h' bl) (Seq.seq_reveal (B.as_seq h' bs)) 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`
                  (if Ghost.reveal modifies_left
                    then B.loc_buffer (B.gsub b 0ul from)
                    else B.loc_none))
                `B.loc_union`
                (if Ghost.reveal modifies_secret
                  then B.loc_buffer (B.gsub b from ((B.len b) `U32.sub` from))
                  else B.loc_none))
              h
              h' /\
            post res
              (B.as_seq h' (B.gsub b 0ul from))
              (B.as_seq h' (B.gsub b from ((B.len b) `U32.sub` from)))
              h'))

    b: LowStar.Buffer.buffer FStar.UInt8.t ->
    from: FStar.UInt32.t{FStar.UInt32.v from <= 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) } ->
    modifies_left: FStar.Ghost.erased Prims.bool ->
    modifies_secret: FStar.Ghost.erased Prims.bool ->
    post:
      (
            res: t ->
            contl: FStar.Seq.Properties.lseq FStar.UInt8.t (FStar.UInt32.v from) ->
            cont:
              FStar.Seq.Properties.lseq FStar.UInt8.t
                (LowStar.Monotonic.Buffer.length b - FStar.UInt32.v from) ->
            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 ==
                  LowStar.Monotonic.Buffer.length b - FStar.UInt32.v from }
          -> FStar.HyperStack.ST.Stack t)
  -> FStar.HyperStack.ST.Stack t