val unsafe_hide_buffer: i:id -> #l:plainLen -> b:lbuffer l -> Tot (plainBuffer i l)
val unsafe_hide_buffer: i:id -> #l:plainLen -> b:lbuffer l -> Tot (plainBuffer i l)
let unsafe_hide_buffer i #l b = b
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 

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

let plain (i:id) (l:plainLen) = lbytes l

// ghost
let as_bytes #i #l p = p

// restricted
let repr #i #l p = p

let make #i l b = b


(*
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 = ()
*)

let slice #i #l p s j = Seq.slice p s j


let plainBuffer (i:id) (l:plainLen) = b:lbuffer l

//usage?

// ghost (was named bufferT; no need to be live)
let as_buffer #i #l pb = pb
/
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.fst
i: MiTLS.Crypto.Indexing.id -> b: MiTLS.Crypto.Symmetric.Bytes.lbuffer l
  -> MiTLS.Crypto.Plain.plainBuffer i l
MiTLS.Crypto.Indexing.id MiTLS.Crypto.Plain.plainLen MiTLS.Crypto.Symmetric.Bytes.lbuffer MiTLS.Crypto.Plain.plainBuffer
let unsafe_hide_buffer i #l b =
  
b