val repr: #i:id {~(safeId i)} -> #l:plainLen -> p:plain i l -> Tot (b:lbytes l {b = as_bytes p })
val repr: #i:id {~(safeId i)} -> #l:plainLen -> p:plain i l -> Tot (b:lbytes l {b = as_bytes p })
let repr #i #l p = p
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
/
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
p: MiTLS.Crypto.Plain.plain i l
  -> b: MiTLS.Crypto.Symmetric.Bytes.lbytes l {b = MiTLS.Crypto.Plain.as_bytes p}
MiTLS.Crypto.Indexing.id Prims.l_not Prims.b2t MiTLS.Flag.safeId MiTLS.Crypto.Plain.plainLen MiTLS.Crypto.Plain.plain MiTLS.Crypto.Symmetric.Bytes.lbytes Prims.op_Equality MiTLS.Crypto.Plain.as_bytes
let repr #i #l p =
  
p