module Hacl.Chacha20
module ST = FStar.HyperStack.ST
open FStar.HyperStack.All
open FStar.Buffer
open FStar.UInt32
open Hacl.Spec.Endianness
open Spec.Chacha20
#reset-options "--max_fuel 0 --z3rlimit 100"
let uint8_p = buffer Hacl.UInt8.t
let uint32_t = t
private let op_String_Access (h:HyperStack.mem) (m:uint8_p{live h m}) = reveal_sbytes (as_seq h m)
val chacha20_key_block:
block:uint8_p{length block = 64} ->
k:uint8_p{length k = 32 /\ disjoint block k} ->
n:uint8_p{length n = 12 /\ disjoint block n} ->
ctr:uint32_t ->
Stack unit
(requires (fun h -> live h block /\ live h k /\ live h n))
(ensures (fun h0 _ h1 -> live h1 block /\ modifies_1 block h0 h1 /\ live h0 k /\ live h0 n /\
h1.[block] == Spec.Chacha20.chacha20_block h0.[k] h0.[n] (v ctr)))
(** @summary This function implements Chacha20
@type
*)
val chacha20:
output:uint8_p ->
plain:uint8_p{disjoint output plain} ->
len:uint32_t{v len = length output /\ v len = length plain} ->
key:uint8_p{length key = 32} ->
nonce:uint8_p{length nonce = 12} ->
ctr:uint32_t{v ctr + (length plain / 64) < pow2 32} ->
Stack unit
(requires (fun h -> live h output /\ live h plain /\ live h nonce /\ live h key))
(ensures (fun h0 _ h1 -> live h1 output /\ live h0 plain /\ modifies_1 output h0 h1
/\ live h0 nonce /\ live h0 key /\
h1.[output] == chacha20_encrypt_bytes h0.[key] h0.[nonce] (v ctr) h0.[plain]))