val disable_uds (_:unit)
  : Stack unit
      (requires fun h -> uds_is_enabled h)
      (ensures fun h0 _ h1 ->
        (~ (uds_is_enabled h1)) /\
        B.(modifies (loc_buffer (st ()).ghost_state) h0 h1))
val disable_uds (_:unit)
  : Stack unit
      (requires fun h -> uds_is_enabled h)
      (ensures fun h0 _ h1 ->
        (~ (uds_is_enabled h1)) /\
        B.(modifies (loc_buffer (st ()).ghost_state) h0 h1))
let disable_uds () =
  B.recall st_var.ghost_state;
  let old_val = B.index st_var.ghost_state 0ul in
  let new_val : (G.erased (bool & bool)) =
    let (b1, b2) = G.reveal old_val in
    G.hide (false, b2) in
  B.upd st_var.ghost_state 0ul new_val
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 _ _ _ = ()

let read_uds uds_out =
  B.recall uds;
  IB.recall_value uds uds_bytes;
  B.blit uds 0ul uds_out 0ul uds_len
/
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
_: Prims.unit -> FStar.HyperStack.ST.Stack Prims.unit
Prims.unit LowStar.Monotonic.Buffer.upd FStar.Ghost.erased HWState.t HWState.t_rel HWState.__proj__Mkstate__item__ghost_state HWAbstraction.st_var FStar.UInt32.__uint_to_t FStar.Pervasives.Native.tuple2 Prims.bool FStar.Ghost.hide FStar.Pervasives.Native.Mktuple2 FStar.Ghost.reveal LowStar.Monotonic.Buffer.index LowStar.Monotonic.Buffer.recall
let disable_uds () =
  
B.recall st_var.ghost_state;
let old_val = B.index st_var.ghost_state 0ul in
let new_val:(G.erased (bool & bool)) =
  let b1, b2 = G.reveal old_val in
  G.hide (false, b2)
in
B.upd st_var.ghost_state 0ul new_val