val recall_st_liveness (st: state)
    : Stack unit (requires fun _ -> True) (ensures fun h0 _ h1 -> h0 == h1 /\ st_liveness st h1)
val recall_st_liveness (st: state)
    : Stack unit (requires fun _ -> True) (ensures fun h0 _ h1 -> h0 == h1 /\ st_liveness st h1)
let recall_st_liveness (st:state)
  : Stack unit
      (requires fun _ -> True)
      (ensures fun h0 _ h1 ->
        h0 == h1 /\
        st_liveness st h1)
  = B.recall st.ghost_state;
    B.recall st.cdi;
    B.recall st.l0.l0_image_header;
    B.recall st.l0.l0_image_header_sig;
    B.recall st.l0.l0_binary;
    B.recall st.l0.l0_binary_hash;
    B.recall 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

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 ]

inline_for_extraction noextract
let recall_image_liveness (img:l0_image_t)
  : Stack unit
      (requires fun _ -> True)
      (ensures fun h0 _ h1 ->
        h0 == h1 /\
        B.live h1 img.l0_image_header /\
        B.live h1 img.l0_image_header_sig /\
        B.live h1 img.l0_binary /\
        B.live h1 img.l0_binary_hash /\
        B.live h1 img.l0_image_auth_pubkey)
  = B.recall img.l0_image_header;
    B.recall img.l0_image_header_sig;
    B.recall img.l0_binary;
    B.recall img.l0_binary_hash;
    B.recall img.l0_image_auth_pubkey
/
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 -> FStar.HyperStack.ST.Stack Prims.unit
HWState.state LowStar.Monotonic.Buffer.recall DICE.Engine.Definitions.byte_sec LowStar.Buffer.trivial_preorder HWState.__proj__Mkl0_image_t__item__l0_image_auth_pubkey HWState.__proj__Mkstate__item__l0 Prims.unit HWState.__proj__Mkl0_image_t__item__l0_binary_hash HWState.__proj__Mkl0_image_t__item__l0_binary HWState.__proj__Mkl0_image_t__item__l0_image_header_sig HWState.__proj__Mkl0_image_t__item__l0_image_header HWState.__proj__Mkstate__item__cdi FStar.Ghost.erased HWState.t HWState.t_rel HWState.__proj__Mkstate__item__ghost_state FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and Prims.eq2 HWAbstraction.st_liveness
let recall_st_liveness (st: state)
    : Stack unit (requires fun _ -> True) (ensures fun h0 _ h1 -> h0 == h1 /\ st_liveness st h1) =
  
B.recall st.ghost_state;
B.recall st.cdi;
B.recall st.l0.l0_image_header;
B.recall st.l0.l0_image_header_sig;
B.recall st.l0.l0_binary;
B.recall st.l0.l0_binary_hash;
B.recall st.l0.l0_image_auth_pubkey