val transpose4_lemma: k:state 4 -> i:nat{i < 16 * 4} ->
  Lemma ((vec_v (transpose4 k).[i / 4]).[i % 4] == ((transpose_state k).[i / 16]).[i % 16])
let transpose4_lemma st i =
  let r0 = transpose4x4_lseq (sub st 0 4) in
  transpose4x4_lemma (sub st 0 4);
  let r1 = transpose4x4_lseq (sub st 4 4) in
  transpose4x4_lemma (sub st 4 4);
  let r2 = transpose4x4_lseq (sub st 8 4) in
  transpose4x4_lemma (sub st 8 4);
  let r3 = transpose4x4_lseq (sub st 12 4) in
  transpose4x4_lemma (sub st 12 4)
val transpose4_lemma: k:state 4 -> i:nat{i < 16 * 4} ->
  Lemma ((vec_v (transpose4 k).[i / 4]).[i % 4] == ((transpose_state k).[i / 16]).[i % 16])
let transpose4_lemma st i =
let r0 = transpose4x4_lseq (sub st 0 4) in
transpose4x4_lemma (sub st 0 4);
let r1 = transpose4x4_lseq (sub st 4 4) in
transpose4x4_lemma (sub st 4 4);
let r2 = transpose4x4_lseq (sub st 8 4) in
transpose4x4_lemma (sub st 8 4);
let r3 = transpose4x4_lseq (sub st 12 4) in
transpose4x4_lemma (sub st 12 4)
Hacl.Spec.Chacha20.Lemmas.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.Transpose.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.Chacha20.Vec.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.Chacha20.Lemmas.fst
Hacl.Spec.Chacha20.Vec.state Prims.nat Prims.b2t Prims.op_LessThan FStar.Mul.op_Star Lib.IntVector.Transpose.transpose4x4_lemma Lib.IntTypes.U32 Lib.Sequence.sub Hacl.Spec.Chacha20.Vec.uint32xN Lib.Sequence.lseq Lib.IntVector.vec_t Lib.IntVector.Transpose.transpose4x4_lseq Prims.unit
module Hacl.Spec.Chacha20.Lemmas

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.IntVector
open Lib.IntVector.Transpose

open Hacl.Spec.Chacha20.Vec

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"

/// (vec_v (transpose #w k).[i / w]).[i % w] == ((transpose_state k).[i / 16]).[i % 16]

val transpose4_lemma: k:state 4 -> i:nat{i < 16 * 4} ->
val transpose4_lemma: k:state 4 -> i:nat{i < 16 * 4} ->
  Lemma ((vec_v (transpose4 k).[i / 4]).[i % 4] == ((transpose_state k).[i / 16]).[i % 16])
k: Hacl.Spec.Chacha20.Vec.state 4 -> i: Prims.nat{i < 16 * 4}
  -> FStar.Pervasives.Lemma
    (ensures
      (Lib.IntVector.vec_v (Hacl.Spec.Chacha20.Vec.transpose4 k).[ i / 4 ]).[ i % 4 ] ==
      (Hacl.Spec.Chacha20.Vec.transpose_state k).[ i / 16 ].[ i % 16 ])