https://github.com/project-everest/hacl-star
Raw File
Tip revision: 37b8a39e2ffd970444f7864cc1b32da48ac8111c authored by Tahina Ramananandro on 14 June 2018, 22:31:20 UTC
Remove all proof annotations about modifies
Tip revision: 37b8a39
Hacl.Salsa20.fst
module Hacl.Salsa20

open Hacl.Impl.Salsa20
open Hacl.Impl.HSalsa20

#reset-options "--max_fuel 0 --z3rlimit 20"

let salsa20 output plain len k n ctr = salsa20 output plain len k n ctr

let hsalsa20 output key nonce =
  crypto_core_hsalsa20 output nonce key
back to top