val read_uds (uds_out:B.lbuffer byte_sec (v uds_len))
  : Stack unit
      (requires fun h ->
        uds_is_enabled h /\
        B.live h uds_out /\
        HS.is_stack_region (B.frameOf uds_out))
      (ensures fun h0 _ h1 ->
        B.(modifies (loc_buffer uds_out) h0 h1) /\
        B.as_seq h1 uds_out == G.reveal uds_bytes)
val read_uds (uds_out:B.lbuffer byte_sec (v uds_len))
  : Stack unit
      (requires fun h ->
        uds_is_enabled h /\
        B.live h uds_out /\
        HS.is_stack_region (B.frameOf uds_out))
      (ensures fun h0 _ h1 ->
        B.(modifies (loc_buffer uds_out) h0 h1) /\
        B.as_seq h1 uds_out == G.reveal uds_bytes)
let read_uds uds_out =
  B.recall uds;
  IB.recall_value uds uds_bytes;
  B.blit uds 0ul uds_out 0ul uds_len
module HWAbstraction

module G = FStar.Ghost

module HS = FStar.HyperStack

open FStar.HyperStack.ST

module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer

module I = Lib.IntTypes

open FStar.Integers

open DICE.Engine.Definitions

friend HWState

let uds_len = 1ul

let uds_bytes = G.hide (Seq.create (v uds_len) (I.u8 0))

let uds : b:IB.ibuffer byte_sec{
  IB.frameOf b == HS.root /\
  IB.recallable b /\
  IB.length b == (v uds_len) /\
  IB.value_is b uds_bytes} =

  let uds = IB.igcmalloc HS.root (I.u8 0) uds_len in
  IB.witness_value uds;
  uds


let st_var : state =
  let l0_image_header_size = 1ul in
  let l0_binary_size = 1ul in
  let ghost_state = B.mgcmalloc HS.root (G.hide (true, true)) 1ul in
  let cdi = B.gcmalloc HS.root (I.u8 0) digest_len in
  let l0_image_header = B.gcmalloc HS.root (I.u8 0) l0_image_header_size in
  let l0_image_header_sig = B.gcmalloc HS.root (I.u8 0) 64ul in
  let l0_binary = B.gcmalloc HS.root (I.u8 0) l0_binary_size in
  let l0_binary_hash = B.gcmalloc HS.root (I.u8 0) digest_len in
  let l0_image_auth_pubkey = B.gcmalloc HS.root (I.u8 0) 32ul in

  let l0 = {
    l0_image_header_size = l0_image_header_size;
    l0_image_header = l0_image_header;
    l0_image_header_sig = l0_image_header_sig;
    l0_binary_size = l0_binary_size;
    l0_binary = l0_binary;
    l0_binary_hash = l0_binary_hash;
    l0_image_auth_pubkey = l0_image_auth_pubkey } in

  { ghost_state = ghost_state;
    cdi = cdi;
    l0 = l0 }

let st _ = st_var

let uds_is_enabled h = b2t (fst (B.get h st_var.ghost_state 0))

let stack_is_erased h = b2t (snd (B.get h st_var.ghost_state 0))

let frame_ghost_state _ _ _ = ()
/
prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked HWState.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked DICE.Engine.Definitions.fst.checked
HWAbstraction.fst

    uds_out:
      LowStar.Buffer.lbuffer DICE.Engine.Definitions.byte_sec
        (FStar.Integers.v HWAbstraction.uds_len)
  -> FStar.HyperStack.ST.Stack Prims.unit
LowStar.Buffer.lbuffer DICE.Engine.Definitions.byte_sec FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 HWAbstraction.uds_len LowStar.Monotonic.Buffer.blit LowStar.ImmutableBuffer.immutable_preorder LowStar.Buffer.trivial_preorder HWAbstraction.uds FStar.UInt32.__uint_to_t Prims.unit LowStar.ImmutableBuffer.recall_value HWAbstraction.uds_bytes LowStar.Monotonic.Buffer.recall
let read_uds uds_out =
  
B.recall uds;
IB.recall_value uds uds_bytes;
B.blit uds 0ul uds_out 0ul uds_len