val 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)
val 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)
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
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 ]
/
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
img: HWState.l0_image_t -> FStar.HyperStack.ST.Stack Prims.unit
HWState.l0_image_t LowStar.Monotonic.Buffer.recall DICE.Engine.Definitions.byte_sec LowStar.Buffer.trivial_preorder HWState.__proj__Mkl0_image_t__item__l0_image_auth_pubkey 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 FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and Prims.eq2 LowStar.Monotonic.Buffer.live
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