let test_quarter_round () =
  let expected1_l =
    List.Tot.map u32_from_UInt32 [0ul; 0ul; 0ul; 0ul] in
  let expected2_l =
    List.Tot.map u32_from_UInt32 [0x08008145ul; 0x80ul; 0x010200ul; 0x20500000ul] in
  assert_norm (List.Tot.length expected1_l = 4);
  assert_norm (List.Tot.length expected2_l = 4);
  let expected1 : lseq uint32 4 = of_list expected1_l in
  let expected2 : lseq uint32 4 = of_list expected2_l in

  let st = create 16 (u32 0) in
  let st1 = quarter_round 0 1 2 3 st in
  let st2 = quarter_round 0 1 2 3 (upd st 0 (u32 1)) in
  let computed1: lseq uint32 4 = slice st1 0 4 in
  let computed2: lseq uint32 4 = slice st2 0 4 in
  let res1 = for_all2 (fun a b -> uint_to_nat #U32 a = uint_to_nat #U32 b) computed1 expected1 in
  let res2 = for_all2 (fun a b -> uint_to_nat #U32 a = uint_to_nat #U32 b) computed2 expected2 in
  res1 && res2
let test_quarter_round () =
let expected1_l = List.Tot.map u32_from_UInt32 [0ul; 0ul; 0ul; 0ul] in
let expected2_l = List.Tot.map u32_from_UInt32 [0x08008145ul; 0x80ul; 0x010200ul; 0x20500000ul] in
assert_norm (List.Tot.length expected1_l = 4);
assert_norm (List.Tot.length expected2_l = 4);
let expected1:lseq uint32 4 = of_list expected1_l in
let expected2:lseq uint32 4 = of_list expected2_l in
let st = create 16 (u32 0) in
let st1 = quarter_round 0 1 2 3 st in
let st2 = quarter_round 0 1 2 3 (upd st 0 (u32 1)) in
let computed1:lseq uint32 4 = slice st1 0 4 in
let computed2:lseq uint32 4 = slice st2 0 4 in
let res1 = for_all2 (fun a b -> uint_to_nat #U32 a = uint_to_nat #U32 b) computed1 expected1 in
let res2 = for_all2 (fun a b -> uint_to_nat #U32 a = uint_to_nat #U32 b) computed2 expected2 in
res1 && res2
Spec.Salsa20.Test.fst.checked
Spec.Salsa20.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.IO.fst.checked
Spec.Salsa20.Test.fst
Prims.unit Prims.op_AmpAmp Prims.bool Lib.Sequence.for_all2 Lib.IntTypes.uint_t Lib.IntTypes.U32 Lib.IntTypes.SEC Prims.op_Equality Prims.nat Prims.l_or Prims.b2t Prims.int Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.IntTypes.uint_v Lib.RawIntTypes.uint_to_nat Lib.Sequence.lseq Lib.IntTypes.int_t Lib.Sequence.slice Lib.IntTypes.uint32 Spec.Salsa20.state Spec.Salsa20.quarter_round Lib.Sequence.upd Lib.IntTypes.u32 Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.create Lib.IntTypes.mk_int Prims.l_Forall Prims.l_imp Prims.op_LessThan Lib.Sequence.index Lib.Sequence.create Lib.Sequence.of_list FStar.Pervasives.assert_norm FStar.List.Tot.Base.length Prims.list FStar.List.Tot.Base.map FStar.UInt32.t Lib.RawIntTypes.u32_from_UInt32 Prims.Cons FStar.UInt32.__uint_to_t Prims.Nil
module Spec.Salsa20.Test

open FStar.Mul
open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Salsa20

///  TESTS: https://cr.yp.to/snuffle/spec.pdf

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val test_quarter_round : _: Prims.unit -> Prims.bool
_: Prims.unit -> Prims.bool