val st_liveness (st: state) (h: HS.mem) : Type0
val st_liveness (st: state) (h: HS.mem) : Type0
let st_liveness (st:state) (h:HS.mem) : Type0 =
  B.all_live h [
    B.buf st.ghost_state;
    B.buf st.cdi;
    B.buf st.l0.l0_image_header;
    B.buf st.l0.l0_image_header_sig;
    B.buf st.l0.l0_binary;
    B.buf st.l0.l0_binary_hash;
    B.buf st.l0.l0_image_auth_pubkey ]
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

open HWState

val uds_len : hashable_len

val uds_bytes : s:G.erased bytes_sec{Seq.length (G.reveal s) == v uds_len}

val st (_:unit) : state
/
prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked HWState.fsti.checked FStar.Seq.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.fsti
st: HWState.state -> h: FStar.Monotonic.HyperStack.mem -> Type0
HWState.state FStar.Monotonic.HyperStack.mem LowStar.Monotonic.Buffer.all_live Prims.Cons LowStar.Monotonic.Buffer.buf_t LowStar.Monotonic.Buffer.buf FStar.Ghost.erased HWState.t HWState.t_rel HWState.__proj__Mkstate__item__ghost_state DICE.Engine.Definitions.byte_sec LowStar.Buffer.trivial_preorder HWState.__proj__Mkstate__item__cdi HWState.__proj__Mkl0_image_t__item__l0_image_header HWState.__proj__Mkstate__item__l0 HWState.__proj__Mkl0_image_t__item__l0_image_header_sig HWState.__proj__Mkl0_image_t__item__l0_binary HWState.__proj__Mkl0_image_t__item__l0_binary_hash HWState.__proj__Mkl0_image_t__item__l0_image_auth_pubkey Prims.Nil
let st_liveness (st: state) (h: HS.mem) : Type0 =
  
B.all_live h
  [
    B.buf st.ghost_state;
    B.buf st.cdi;
    B.buf st.l0.l0_image_header;
    B.buf st.l0.l0_image_header_sig;
    B.buf st.l0.l0_binary;
    B.buf st.l0.l0_binary_hash;
    B.buf st.l0.l0_image_auth_pubkey
  ]