Revision 0f7967bd30c718d4290fc4ff7d67c09a4ec3b497 authored by Dzomo the everest Yak on 22 April 2020, 08:20:07 UTC, committed by Dzomo the everest Yak on 22 April 2020, 08:20:07 UTC
1 parent 0bcd4ea
Hacl.Poly1305_256.fsti
module Hacl.Poly1305_256
open FStar.HyperStack
open FStar.HyperStack.All
open Lib.IntTypes
open Lib.Buffer
open Hacl.Impl.Poly1305.Fields
open Hacl.Impl.Poly1305
let blocklen = 16ul
type poly1305_ctx = lbuffer (Lib.IntVector.vec_t U64 4) 25ul
val poly1305_init: poly1305_init_st M256
val poly1305_update1: poly1305_update1_st M256
val poly1305_update: poly1305_update_st M256
val poly1305_finish: poly1305_finish_st M256
val poly1305_mac: poly1305_mac_st M256
Computing file changes ...
