let test_column_round () =
  let expected_l = List.Tot.map u32_from_UInt32 [
    0x10090288ul; 0x00000000ul; 0x00000000ul; 0x00000000ul;
    0x00000101ul; 0x00000000ul; 0x00000000ul; 0x00000000ul;
    0x00020401ul; 0x00000000ul; 0x00000000ul; 0x00000000ul;
    0x40a04001ul; 0x00000000ul; 0x00000000ul; 0x00000000ul] in
  assert_norm (List.Tot.length expected_l = 16);
  let expected : lseq uint32 16 = of_list expected_l in

  let st = create 16 (u32 0) in
  let st = upd st 0 (u32 1) in
  let st = upd st 4 (u32 1) in
  let st = upd st 8 (u32 1) in
  let st = upd st 12 (u32 1) in
  let st = column_round st in
  for_all2 (fun a b -> uint_to_nat #U32 a = uint_to_nat #U32 b) st expected
let test_column_round () =
let expected_l =
  List.Tot.map u32_from_UInt32
    [
      0x10090288ul; 0x00000000ul; 0x00000000ul; 0x00000000ul; 0x00000101ul; 0x00000000ul;
      0x00000000ul; 0x00000000ul; 0x00020401ul; 0x00000000ul; 0x00000000ul; 0x00000000ul;
      0x40a04001ul; 0x00000000ul; 0x00000000ul; 0x00000000ul
    ]
in
assert_norm (List.Tot.length expected_l = 16);
let expected:lseq uint32 16 = of_list expected_l in
let st = create 16 (u32 0) in
let st = upd st 0 (u32 1) in
let st = upd st 4 (u32 1) in
let st = upd st 8 (u32 1) in
let st = upd st 12 (u32 1) in
let st = column_round st in
for_all2 (fun a b -> uint_to_nat #U32 a = uint_to_nat #U32 b) st expected
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 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 Prims.bool Spec.Salsa20.state Spec.Salsa20.column_round Lib.Sequence.lseq Lib.IntTypes.int_t Prims.l_and Prims.eq2 FStar.Seq.Base.seq Lib.Sequence.to_seq FStar.Seq.Base.upd Lib.IntTypes.mk_int Lib.Sequence.index Prims.l_Forall Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.l_imp Prims.op_LessThan Prims.op_disEquality FStar.Seq.Base.index Lib.Sequence.upd Lib.IntTypes.uint32 Lib.IntTypes.u32 FStar.Seq.Base.create 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"

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_row_round () =
  let expected_l = List.Tot.map u32_from_UInt32 [
    0x08008145ul; 0x00000080ul; 0x00010200ul; 0x20500000ul;
    0x20100001ul; 0x00048044ul; 0x00000080ul; 0x00010000ul;
    0x00000001ul; 0x00002000ul; 0x80040000ul; 0x00000000ul;
    0x00000001ul; 0x00000200ul; 0x00402000ul; 0x88000100ul ] in
  assert_norm (List.Tot.length expected_l = 16);
  let expected : lseq uint32 16 = of_list expected_l in

  let st = create 16 (u32 0) in
  let st = upd st 0 (u32 1) in
  let st = upd st 4 (u32 1) in
  let st = upd st 8 (u32 1) in
  let st = upd st 12 (u32 1) in
  let st = row_round st in
  for_all2 (fun a b -> uint_to_nat #U32 a = uint_to_nat #U32 b) st expected
val test_column_round : _: Prims.unit -> Prims.bool
_: Prims.unit -> Prims.bool