val 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 }
val 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 : 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
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))
/
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
b:
LowStar.ImmutableBuffer.ibuffer DICE.Engine.Definitions.byte_sec
  { LowStar.Monotonic.Buffer.frameOf b == FStar.Monotonic.HyperHeap.root /\
    LowStar.Monotonic.Buffer.recallable b /\
    LowStar.Monotonic.Buffer.length b == FStar.UInt32.v HWAbstraction.uds_len /\
    LowStar.ImmutableBuffer.value_is b HWAbstraction.uds_bytes }
LowStar.ImmutableBuffer.ibuffer DICE.Engine.Definitions.byte_sec Prims.l_and Prims.eq2 FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.ImmutableBuffer.immutable_preorder FStar.Monotonic.HyperHeap.root LowStar.Monotonic.Buffer.recallable Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual FStar.Pervasives.norm Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.iota FStar.Pervasives.delta_attr Prims.string Prims.Nil FStar.Pervasives.Native.Mktuple2 FStar.Integers.signed_width FStar.Pervasives.Native.option FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.nat_of_width FStar.Integers.width_of_sw FStar.Integers.width Prims.l_True FStar.Int.size FStar.Integers.fixed_width FStar.UInt.size LowStar.Monotonic.Buffer.length FStar.UInt32.v HWAbstraction.uds_len LowStar.ImmutableBuffer.value_is HWAbstraction.uds_bytes Prims.unit LowStar.ImmutableBuffer.witness_value LowStar.Monotonic.Buffer.mbuffer Prims.nat Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Monotonic.Buffer.witnessed LowStar.ImmutableBuffer.cpred FStar.Seq.Base.create Lib.IntTypes.mk_int Lib.IntTypes.U8 Lib.IntTypes.SEC LowStar.ImmutableBuffer.igcmalloc Lib.IntTypes.u8 LowStar.ImmutableBuffer.libuffer
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