val pow2_61:_: unit{pow2 61 == 2305843009213693952}
let pow2_61 : _:unit{pow2 61 == 2305843009213693952} = assert_norm(pow2 61 == 2305843009213693952)
val pow2_61:_: unit{pow2 61 == 2305843009213693952}
let pow2_61:_: unit{pow2 61 == 2305843009213693952} =
assert_norm (pow2 61 == 2305843009213693952)
Spec.Agile.HPKE.fst.checked
Spec.P256.fst.checked Spec.Loops.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.DH.fst.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Spec.Agile.HPKE.fst
FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.pow2
module Spec.Agile.HPKE

open FStar.Mul
open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence

module DH = Spec.Agile.DH
module AEAD = Spec.Agile.AEAD
module Hash = Spec.Agile.Hash
module HKDF = Spec.Agile.HKDF
val pow2_61:_: unit{pow2 61 == 2305843009213693952}
_: Prims.unit{Prims.pow2 61 == 2305843009213693952}