val uds_bytes : s:G.erased bytes_sec{Seq.length (G.reveal s) == v uds_len}
val uds_bytes : s:G.erased bytes_sec{Seq.length (G.reveal s) == v uds_len}
let uds_bytes = G.hide (Seq.create (v uds_len) (I.u8 0))
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
/
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
s:
FStar.Ghost.erased DICE.Engine.Definitions.bytes_sec
  {FStar.Seq.Base.length (FStar.Ghost.reveal s) == FStar.Integers.v HWAbstraction.uds_len}
FStar.Ghost.hide DICE.Engine.Definitions.bytes_sec FStar.Seq.Base.create Lib.IntTypes.uint8 FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 HWAbstraction.uds_len Lib.IntTypes.u8
let uds_bytes =
  
G.hide (Seq.create (v uds_len) (I.u8 0))