val rounds:
    #w:lanes
  -> st:state w ->
  Stack unit
    (requires (fun h -> live h st))
    (ensures (fun h0 _ h1 -> modifies (loc st) h0 h1 /\
      as_seq h1 st == Spec.rounds (as_seq h0 st)))
let rounds #w st =
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st;
  double_round st
val rounds:
    #w:lanes
  -> st:state w ->
  Stack unit
    (requires (fun h -> live h st))
    (ensures (fun h0 _ h1 -> modifies (loc st) h0 h1 /\
      as_seq h1 st == Spec.rounds (as_seq h0 st)))
let rounds #w st =
double_round st;
double_round st;
double_round st;
double_round st;
double_round st;
double_round st;
double_round st;
double_round st;
double_round st;
double_round st
Hacl.Impl.Chacha20.Vec.fst.checked
Spec.Chacha20.fst.checked prims.fst.checked Meta.Attribute.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Chacha20.Vec.fst.checked Hacl.Spec.Chacha20.Equiv.fst.checked Hacl.Impl.Chacha20.Core32xN.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Chacha20.Vec.fst
Hacl.Impl.Chacha20.Core32xN.lanes Hacl.Impl.Chacha20.Core32xN.state Hacl.Impl.Chacha20.Core32xN.double_round Prims.unit
module Hacl.Impl.Chacha20.Vec

module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
open Lib.IntVector

open Hacl.Impl.Chacha20.Core32xN
module Spec = Hacl.Spec.Chacha20.Vec
module Chacha20Equiv = Hacl.Spec.Chacha20.Equiv
module Loop = Lib.LoopCombinators


#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 200 --record_options"
//#set-options "--debug Hacl.Impl.Chacha20.Vec --debug_level ExtractNorm"

noextract
val rounds:
    #w:lanes
  -> st:state w ->
  Stack unit
    (requires (fun h -> live h st))
    (ensures (fun h0 _ h1 -> modifies (loc st) h0 h1 /\
      as_seq h1 st == Spec.rounds (as_seq h0 st)))
[@ Meta.Attribute.inline_ ]
val rounds:
    #w:lanes
  -> st:state w ->
  Stack unit
    (requires (fun h -> live h st))
    (ensures (fun h0 _ h1 -> modifies (loc st) h0 h1 /\
      as_seq h1 st == Spec.rounds (as_seq h0 st)))
st: Hacl.Impl.Chacha20.Core32xN.state w -> FStar.HyperStack.ST.Stack Prims.unit