module Hacl.SecureAPI.Chacha20

module ST = FStar.HyperStack.ST

open FStar.HyperStack.All


open FStar.Mul
open FStar.HyperStack
open FStar.Buffer
open Hacl.Lib.LoadStore32
open Hacl.Impl.Chacha20


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

[@ Substitute]
val setup:
  st:state ->
  k:uint8_p{length k = 32 /\ disjoint st k} ->
  n:uint8_p{length n = 12 /\ disjoint st n} ->
  c:UInt32.t ->
  Stack unit
    (requires (fun h -> live h st /\ live h k /\ live h n))
    (ensures (fun h0 _ h1 -> live h0 k /\ live h0 n /\ live h1 st /\ modifies_1 st h0 h1))
[@ Substitute]
let setup st k n c = setup st k n c

[@ Substitute]
val chacha20_core:
  k:state ->
  st:state{disjoint st k} ->
  Stack unit
    (requires (fun h -> live h k /\ live h st))
    (ensures  (fun h0 updated_log h1 -> live h0 st /\ live h0 k
      /\ live h1 k /\ live h1 st /\ modifies_1 k h0 h1))
[@ Substitute]
let chacha20_core k st =
  copy_state k st;
  rounds k;
  sum_states k st


[@ Substitute]
val chacha20_stream:
  stream_block:uint8_p{length stream_block = 64} ->
  st:state{disjoint st stream_block} ->
  Stack unit
    (requires (fun h -> live h stream_block /\ live h st))
    (ensures  (fun h0 updated_log h1 -> live h1 stream_block /\ live h0 st
      /\ live h1 st /\ live h0 stream_block /\ modifies_1 stream_block h0 h1))
[@ Substitute]
let chacha20_stream stream_block st =
  push_frame();
  let h_0 = ST.get() in
  let st' = Buffer.create (Hacl.Cast.uint32_to_sint32 0ul) 16ul in
  let log' = chacha20_core st' st in
  uint32s_to_le_bytes stream_block st' 16ul;
  let h = ST.get() in
  cut (modifies_2_1 stream_block h_0 h);
  pop_frame()


[@ Substitute]
val chacha20_stream_finish:
  stream_block:uint8_p ->
  len:UInt32.t{UInt32.v len <= 64 /\ length stream_block = UInt32.v len} ->
  st:state{disjoint st stream_block} ->
  Stack unit
    (requires (fun h -> live h stream_block /\ live h st))
    (ensures  (fun h0 updated_log h1 -> live h1 stream_block /\ live h0 st
      /\ live h1 st /\ live h0 stream_block /\ modifies_1 stream_block h0 h1))
[@ Substitute]
let chacha20_stream_finish stream_block len st =
  push_frame();
  let b = create (Hacl.Cast.uint8_to_sint8 0uy) 64ul in
  chacha20_stream b st;
  blit b 0ul stream_block 0ul len;
  pop_frame()