val all_heap_buffers_except_cdi_and_ghost_state_remain_same : h0: FStar.Monotonic.HyperStack.mem -> h1: FStar.Monotonic.HyperStack.mem -> Prims.logical
let all_heap_buffers_except_cdi_and_ghost_state_remain_same (h0 h1:HS.mem) =
  let s = st () in
  forall (a:Type0) (b:B.buffer a).
    (ST.is_eternal_region (B.frameOf b) /\
     B.disjoint b s.ghost_state /\
     B.disjoint b s.cdi /\
     B.live h0 b) ==> (B.as_seq h0 b == B.as_seq h1 b /\ B.live h1 b)
module DICE.Engine.Core

open LowStar.Comment

module Fail = LowStar.Failure
module B = LowStar.Buffer
module HS  = FStar.HyperStack
module HST = FStar.HyperStack.ST

open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.ByteBuffer

module S = Spec.Hash.Definitions
module Ed25519 = Hacl.Ed25519

module HW = HWAbstraction

open DICE.Engine.Definitions

module HSeq = Lib.Sequence

module G = FStar.Ghost

open HWAbstraction

open HWState

let l0_image_is_valid (img:l0_image_t) (h:HS.mem) =
  Spec.Ed25519.verify
    (B.as_seq h img.l0_image_auth_pubkey)
    (B.as_seq h img.l0_image_header)
    (B.as_seq h img.l0_image_header_sig) /\

  Spec.Agile.Hash.hash alg (B.as_seq h img.l0_binary) ==
  B.as_seq h img.l0_binary_hash

inline_for_extraction noextract
let verify_l0_image_hash (img:l0_image_t)
  : Stack bool
      (requires fun _ -> True)
      (ensures fun h0 b h1 ->
        B.(modifies loc_none h0 h1) /\
        (b <==> Spec.Agile.Hash.hash alg (B.as_seq h1 img.l0_binary) == B.as_seq h1 img.l0_binary_hash))
  = recall_image_liveness img;

    HST.push_frame ();

    let hash_buf = B.alloca (u8 0x00) digest_len in
    dice_hash alg
      (* dst *) hash_buf
      (* msg *) img.l0_binary img.l0_binary_size;
    let b = lbytes_eq #digest_len img.l0_binary_hash hash_buf in

    HST.pop_frame ();

    b

let authenticate_l0_image (img:l0_image_t)
  : Stack bool
      (requires fun _ -> True)
      (ensures fun h0 b h1 ->
        B.modifies B.loc_none h0 h1 /\
        (b <==> l0_image_is_valid img h1))
  = recall_image_liveness img;
    
    let valid_header_sig = Ed25519.verify
                           (* pub *) img.l0_image_auth_pubkey
                           (* msg *) img.l0_image_header_size img.l0_image_header
                           (* sig *) img.l0_image_header_sig in
    if valid_header_sig then verify_l0_image_hash img else false

let lemma_hmac_preconditions ()
  : Lemma
      (Spec.Agile.HMAC.keysized alg (v digest_len) /\
       v digest_len + S.block_length alg <= (Some?.v (S.max_input_length alg)))
  = assert_norm (Spec.Agile.HMAC.keysized alg (v digest_len) /\
               v digest_len + S.block_length alg <= (Some?.v (S.max_input_length alg)))


let cdi_functional_correctness (st:state) (h:HS.mem) =
  lemma_hmac_preconditions ();

  B.as_seq h st.cdi ==
  Spec.Agile.HMAC.hmac alg
    (Spec.Agile.Hash.hash alg uds_bytes)
    (Spec.Agile.Hash.hash alg (B.as_seq h st.l0.l0_binary))

#push-options "--z3rlimit 40 --fuel 0 --ifuel 0"
inline_for_extraction noextract
let compute_cdi (st:state)
  : Stack unit
      (requires fun h ->
        st == HW.st () /\
        uds_is_enabled h)
      (ensures fun h0 _ h1 ->
        B.(modifies (loc_buffer st.cdi) h0 h1) /\
        cdi_functional_correctness st h1)
  = recall_st_liveness st;

    let h0 = get () in
    HST.push_frame ();

    let uds = B.alloca (u8 0x00) HW.uds_len in

    let h1 = get () in
    frame_ghost_state B.loc_none h0 h1;

    read_uds uds;

    let uds_digest = B.alloca (u8 0x00) digest_len in
    let l0_digest = B.alloca (u8 0x00) digest_len in
    
    dice_hash alg uds_digest uds uds_len;
    dice_hash alg l0_digest st.l0.l0_binary st.l0.l0_binary_size;
    
    (* Prf *) lemma_hmac_preconditions ();

    dice_hmac alg
      (* dst *) st.cdi
      (* key *) uds_digest digest_len
      (* msg *) l0_digest digest_len;

    zeroize uds_len uds;

    HST.pop_frame ()
#pop-options

type dice_return_code = | DICE_SUCCESS | DICE_ERROR

module ST = FStar.HyperStack.ST
/
Spec.Hash.Definitions.fst.checked Spec.Ed25519.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked LowStar.Failure.fsti.checked LowStar.Comment.fsti.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked HWState.fsti.checked HWAbstraction.fsti.checked Hacl.Ed25519.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked DICE.Engine.Definitions.fst.checked
DICE.Engine.Core.fst
h0: FStar.Monotonic.HyperStack.mem -> h1: FStar.Monotonic.HyperStack.mem -> Prims.logical
FStar.Monotonic.HyperStack.mem Prims.l_Forall LowStar.Buffer.buffer Prims.l_imp Prims.l_and FStar.HyperStack.ST.is_eternal_region LowStar.Monotonic.Buffer.frameOf LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.disjoint FStar.Ghost.erased HWState.t HWState.t_rel HWState.__proj__Mkstate__item__ghost_state DICE.Engine.Definitions.byte_sec HWState.__proj__Mkstate__item__cdi LowStar.Monotonic.Buffer.live Prims.eq2 FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq HWState.state HWAbstraction.st Prims.logical
let all_heap_buffers_except_cdi_and_ghost_state_remain_same (h0 h1: HS.mem) =
  
let s = st () in
forall (a: Type0) (b: B.buffer a).
  (ST.is_eternal_region (B.frameOf b) /\ B.disjoint b s.ghost_state /\ B.disjoint b s.cdi /\
    B.live h0 b) ==>
  (B.as_seq h0 b == B.as_seq h1 b /\ B.live h1 b)