val lemma_hmac_preconditions: Prims.unit
  -> Lemma
    (Spec.Agile.HMAC.keysized alg (v digest_len) /\
      v digest_len + S.block_length alg <= (Some?.v (S.max_input_length alg)))
val lemma_hmac_preconditions: Prims.unit
  -> Lemma
    (Spec.Agile.HMAC.keysized alg (v digest_len) /\
      v digest_len + S.block_length alg <= (Some?.v (S.max_input_length alg)))
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)))
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
/
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
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.Agile.HMAC.keysized DICE.Engine.Definitions.alg
        (Lib.IntTypes.v DICE.Engine.Definitions.digest_len) /\
      Lib.IntTypes.v DICE.Engine.Definitions.digest_len +
      Spec.Hash.Definitions.block_length DICE.Engine.Definitions.alg <=
      Some?.v (Spec.Hash.Definitions.max_input_length DICE.Engine.Definitions.alg))
Prims.unit FStar.Pervasives.assert_norm Prims.l_and Spec.Agile.HMAC.keysized DICE.Engine.Definitions.alg Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB DICE.Engine.Definitions.digest_len Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Spec.Hash.Definitions.block_length FStar.Pervasives.Native.__proj__Some__item__v Prims.pos Spec.Hash.Definitions.max_input_length Prims.l_True Prims.squash Prims.Nil FStar.Pervasives.pattern
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)))