val uds_len : hashable_len
val uds_len : hashable_len
let uds_len = 1ul
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
/
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
DICE.Engine.Definitions.hashable_len
FStar.UInt32.__uint_to_t
let uds_len =
  
1ul