val is_safe (#ip: ipkg) (i: ip.Pkg.t{ip.Pkg.registered i})
    : ST bool
      (requires fun h0 -> True)
      (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i))
val is_safe (#ip: ipkg) (i: ip.Pkg.t{ip.Pkg.registered i})
    : ST bool
      (requires fun h0 -> True)
      (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i))
let is_safe (#ip:ipkg) (i:ip.Pkg.t{ip.Pkg.registered i}): ST bool
  (requires fun h0 -> True)
  (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i))
  =
  let b = ip.Pkg.get_honesty i in
  ideal && b
(* Idealizing derived authentication tokens; independent of TLS, used for TLS 1.2 Finished message payloads. *)
module MiTLS.Token.UF1CMA
open MiTLS

//TODO use this file instead of TLSPRF

open FStar.Bytes
open MiTLS.Mem

// this file is adapted from HMAC.UFCMA but simpler, and yield
// probabilistic security: the advantage of an adversary guessing the
// random token is just 1/#tokens. (Do we need to enforce a single
// verification attempt?)

let ipkg = Pkg.ipkg
let model = Flags.model
let ideal = Flags.ideal_HMAC
// secret idealization flag for the UF1CMA assumption
//TODO use a separate flag

type safe (#ip:ipkg) (i:ip.Pkg.t) = b2t ideal /\ ip.Pkg.honest i
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked MiTLS.Flags.fst.checked Hacl.Hash.Definitions.fst.checked FStar.Tactics.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Token.UF1CMA.fsti
i: Idx?.t ip {Idx?.registered ip i} -> FStar.HyperStack.ST.ST Prims.bool
MiTLS.Token.UF1CMA.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Pkg.__proj__Idx__item__registered Prims.op_AmpAmp MiTLS.Token.UF1CMA.ideal Prims.bool MiTLS.Pkg.__proj__Idx__item__get_honesty FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and FStar.HyperStack.ST.modifies_none Prims.l_iff Prims.b2t MiTLS.Token.UF1CMA.safe
let is_safe (#ip: ipkg) (i: ip.Pkg.t{ip.Pkg.registered i})
    : ST bool
      (requires fun h0 -> True)
      (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i)) =
  
let b = ip.Pkg.get_honesty i in
ideal && b