val 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))
val 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))
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
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
/
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
img: HWState.l0_image_t -> FStar.HyperStack.ST.Stack Prims.bool
HWState.l0_image_t DICE.Engine.Core.verify_l0_image_hash Prims.bool Hacl.Ed25519.verify HWState.__proj__Mkl0_image_t__item__l0_image_auth_pubkey HWState.__proj__Mkl0_image_t__item__l0_image_header_size HWState.__proj__Mkl0_image_t__item__l0_image_header HWState.__proj__Mkl0_image_t__item__l0_image_header_sig Prims.unit HWAbstraction.recall_image_liveness FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none Prims.l_iff Prims.b2t DICE.Engine.Core.l0_image_is_valid
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 img.l0_image_auth_pubkey
    img.l0_image_header_size
    img.l0_image_header
    img.l0_image_header_sig
in
if valid_header_sig then verify_l0_image_hash img else false