val live' : h: FStar.Monotonic.HyperStack.mem -> p: MiTLS.Crypto.Plain.plainBuffer i l -> Type0
let live' #i #l = live #i #l
module MiTLS.Crypto.Plain
open MiTLS

module ST = FStar.HyperStack.ST

open FStar.HyperStack.All

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.UInt32
open FStar.Ghost
open MiTLS.Buffer.Utils
open MiTLS.Crypto.Symmetric.Bytes

// Abstraction for secret plaintexts (heap- and stack-based)

// For now we assume public lengths and no padding
// For TLS, we will pass around instead 
// - a public maximal length
// - a private actual length
// - a buffer of maximal length (possibly + 1 for TLS CT)
// The need to pass two lengths is a small price to pay for length hiding. 
// It is yet unclear whether to use buffers or bytes values. 

// Type abstraction protects against aliasing inasmuch
// as it is enforced from allocation.

open MiTLS.Crypto.Indexing
open MiTLS.Flag 

// -----------------------------------------------------------------------------

type plainLen = nat // we'll need a tigher bound

val plain (i:id) (l:plainLen) : Type0

// ghost
noextract val as_bytes: #i:id -> #l:plainLen -> p:plain i l -> GTot (lbytes l)

// restricted
val repr: #i:id {~(safeId i)} -> #l:plainLen -> p:plain i l -> Tot (b:lbytes l {b = as_bytes p })

val make: #i:id {~(safeId i)}-> l:plainLen -> b:lbytes l -> Tot (p:plain i l {b = as_bytes p})


(*
val reveal: #i:id -> #l:plainLen -> p:plain i l -> GTot (lbytes l)
let reveal #i #l p = p

val repr_injective : i:id -> l:plainLen -> p:plain i l -> Lemma
  (requires True)
  (ensures (make #i l (as_bytes p) == p))
  [SMTPat (as_bytes p)]
let repr_injective i l p = ()
*)

noextract val slice: #i:id -> #l:plainLen -> p:plain i l -> s:nat -> j:nat{s <= j && j <= l} -> 
  Tot (q:plain i (j - s) {as_bytes q = Seq.slice (as_bytes p) s j})


val plainBuffer (i:id) (l:plainLen) : Type0

//usage?

// ghost (was named bufferT; no need to be live)
val as_buffer: #i:id -> #l:plainLen -> pb: plainBuffer i l -> GTot(lbuffer l)

// for tests
val unsafe_hide_buffer: i:id -> #l:plainLen -> b:lbuffer l -> Tot (plainBuffer i l)

// usage?
val hide_buffer: i:id -> #l:plainLen -> b:lbuffer l -> GTot (plainBuffer i l)

val as_buffer_injective : i:id -> l:plainLen -> p:plainBuffer i l -> Lemma
  (requires True)
  (ensures (hide_buffer i (as_buffer p) == p))
  [SMTPat (as_buffer p)]
/
prims.fst.checked MiTLS.Flag.fst.checked MiTLS.Crypto.Symmetric.Bytes.fst.checked MiTLS.Crypto.Indexing.fst.checked MiTLS.Buffer.Utils.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Buffer.fst.checked
MiTLS.Crypto.Plain.fsti
h: FStar.Monotonic.HyperStack.mem -> p: MiTLS.Crypto.Plain.plainBuffer i l -> Type0
MiTLS.Crypto.Indexing.id MiTLS.Crypto.Plain.plainLen MiTLS.Crypto.Plain.live FStar.Monotonic.HyperStack.mem MiTLS.Crypto.Plain.plainBuffer
let live' #i #l =
  
live #i #l