val transposewxw_f: #w:width -> #t:v_inttype -> n:nat{pow2 n == w} -> i:nat{i < n} -> lseq (vec_t t w) w -> lseq (vec_t t w) w
let transposewxw_f #w #t n i vs =
  createi w (transposewxw_f_l #w n i vs)
val transposewxw_f: #w:width -> #t:v_inttype -> n:nat{pow2 n == w} -> i:nat{i < n} -> lseq (vec_t t w) w -> lseq (vec_t t w) w
let transposewxw_f #w #t n i vs =
createi w (transposewxw_f_l #w n i vs)
Lib.IntVector.Transpose.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Lib.IntVector.Transpose.fst
Lib.IntVector.width Lib.IntVector.v_inttype Prims.nat Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThan Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Lib.IntTypes.max_size_t Prims.pow2 Prims.op_LessThan Lib.Sequence.lseq Lib.IntVector.vec_t Lib.Sequence.createi Lib.IntVector.Transpose.transposewxw_f_l
module Lib.IntVector.Transpose

module Loops = Lib.LoopCombinators


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

///
///  transpose4x4
///

inline_for_extraction
val transpose4x4_0: #t:v_inttype -> vec_t4 t -> vec_t4 t
let transpose4x4_0 #t (v0,v1,v2,v3) =
  let v0' = vec_interleave_low v0 v1 in
  let v1' = vec_interleave_high v0 v1 in
  let v2' = vec_interleave_low v2 v3 in
  let v3' = vec_interleave_high v2 v3 in

  let v0'' = vec_interleave_low_n 2 v0' v2' in
  let v1'' = vec_interleave_high_n 2 v0' v2' in
  let v2'' = vec_interleave_low_n 2 v1' v3' in
  let v3'' = vec_interleave_high_n 2 v1' v3' in
  (v0'',v2'',v1'',v3'')


inline_for_extraction
val transpose4x4_uint32: #t:v_inttype{t == U32} -> vec_t4 t -> vec_t4 t
let transpose4x4_uint32 #t vs =
  let (v0'',v2'',v1'',v3'') = transpose4x4_0 #t vs in
  (v0'',v1'',v2'',v3'')


inline_for_extraction
val transpose4x4_uint64: #t:v_inttype{t == U64} -> vec_t4 t -> vec_t4 t
let transpose4x4_uint64 #t vs = transpose4x4_0 #t vs


let transpose4x4 #t vs =
  match t with
  | U32 -> transpose4x4_uint32 #t vs
  | U64 -> transpose4x4_uint64 #t vs

///
///   transpose8x8
///

inline_for_extraction
val transpose8x8_0: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_0 #t (v0,v1,v2,v3,v4,v5,v6,v7) =
  let v0' = vec_interleave_low v0 v1 in
  let v1' = vec_interleave_high v0 v1 in
  let v2' = vec_interleave_low v2 v3 in
  let v3' = vec_interleave_high v2 v3 in
  let v4' = vec_interleave_low v4 v5 in
  let v5' = vec_interleave_high v4 v5 in
  let v6' = vec_interleave_low v6 v7 in
  let v7' = vec_interleave_high v6 v7 in
  (v0',v1',v2',v3',v4',v5',v6',v7')


inline_for_extraction
val transpose8x8_1: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_1 #t (v0,v1,v2,v3,v4,v5,v6,v7) =
  let v0' = vec_interleave_low_n 2 v0 v2 in
  let v2' = vec_interleave_high_n 2 v0 v2 in
  let v1' = vec_interleave_low_n 2 v1 v3 in
  let v3' = vec_interleave_high_n 2 v1 v3 in
  let v4' = vec_interleave_low_n 2 v4 v6 in
  let v6' = vec_interleave_high_n 2 v4 v6 in
  let v5' = vec_interleave_low_n 2 v5 v7 in
  let v7' = vec_interleave_high_n 2 v5 v7 in
  (v0',v1',v2',v3',v4',v5',v6',v7')


inline_for_extraction
val transpose8x8_2: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_2 #t (v0,v1,v2,v3,v4,v5,v6,v7) =
  let v0' = vec_interleave_low_n 4 v0 v4 in
  let v4' = vec_interleave_high_n 4 v0 v4 in
  let v1' = vec_interleave_low_n 4 v1 v5 in
  let v5' = vec_interleave_high_n 4 v1 v5 in
  let v2' = vec_interleave_low_n 4 v2 v6 in
  let v6' = vec_interleave_high_n 4 v2 v6 in
  let v3' = vec_interleave_low_n 4 v3 v7 in
  let v7' = vec_interleave_high_n 4 v3 v7 in
  (v0',v1',v2',v3',v4',v5',v6',v7')


inline_for_extraction
val transpose8x8_012: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_012 #t vs0 =
  let (v0,v1,v2,v3,v4,v5,v6,v7) = vs0 in
  let (v0',v1',v2',v3',v4',v5',v6',v7') = transpose8x8_0 #t (v0,v1,v2,v3,v4,v5,v6,v7) in
  let (v0',v1',v2',v3',v4',v5',v6',v7') = transpose8x8_1 #t (v0',v1',v2',v3',v4',v5',v6',v7') in
  let (v0',v1',v2',v3',v4',v5',v6',v7') = transpose8x8_2 #t (v0',v1',v2',v3',v4',v5',v6',v7') in
  (v0',v1',v2',v3',v4',v5',v6',v7')


inline_for_extraction
val transpose8x8_uint32: #t:v_inttype{t == U32} -> vec_t8 t -> vec_t8 t
let transpose8x8_uint32 #t vs0 =
  let (v0',v1',v2',v3',v4',v5',v6',v7') = transpose8x8_012 #t vs0 in
  (v0',v2',v1',v3',v4',v6',v5',v7')


let transpose8x8 #t vs =
  match t with
  | U32 -> transpose8x8_uint32 #t vs

///
///  generic transpose
///

val lemma_l_plus_pow2i_lt: #w:pos -> n:nat{pow2 n == w} -> i:nat{i < n} -> l:nat{l < w} -> Lemma
  (requires l % (2 * pow2 i) < pow2 i)
  (ensures  l + pow2 i < w)

let lemma_l_plus_pow2i_lt #w n i l =
  let pow2i1 = pow2 (i + 1) in

  calc (<) {
    l + pow2 i;
    (==) { Math.Lemmas.euclidean_division_definition l pow2i1 }
    l / pow2i1 * pow2i1 + l % pow2i1 + pow2 i;
    (==) { Math.Lemmas.pow2_plus 1 i }
    l / pow2i1 * pow2i1 + l % (2 * pow2 i) + pow2 i;
    (<) { assert (l % (2 * pow2 i) < pow2 i) }
    l / pow2i1 * pow2i1 + pow2 i + pow2 i;
    (==) { Math.Lemmas.pow2_double_sum i }
    l / pow2i1 * pow2i1 + pow2i1;
    (==) { Math.Lemmas.distributivity_add_left (l / pow2i1) 1 pow2i1 }
    (l / pow2i1 + 1) * pow2i1;
    (<=) { Math.Lemmas.lemma_div_lt_nat l n (i + 1) }
    pow2 (n - i - 1) * pow2 (i + 1);
    (==) { Math.Lemmas.pow2_plus (n - i - 1) (i + 1) }
    pow2 n;
  }


inline_for_extraction
val transposewxw_f_l:
    #w:width
  -> #t:v_inttype
  -> n:nat{pow2 n == w}
  -> i:nat{i < n}
  -> lseq (vec_t t w) w
  -> l:nat{l < w} ->
  vec_t t w

let transposewxw_f_l #w #t n i vs l =
  Math.Lemmas.pow2_multiplication_modulo_lemma_1 1 i n;
  if l % (2 * pow2 i) < pow2 i
  then begin
    lemma_l_plus_pow2i_lt #w n i l;
    vec_interleave_low_n (pow2 i) vs.[l] vs.[l + pow2 i] end
  else
    vec_interleave_high_n (pow2 i) vs.[l - pow2 i] vs.[l]


inline_for_extraction
val transposewxw_f: #w:width -> #t:v_inttype -> n:nat{pow2 n == w} -> i:nat{i < n} -> lseq (vec_t t w) w -> lseq (vec_t t w) w
val transposewxw_f: #w:width -> #t:v_inttype -> n:nat{pow2 n == w} -> i:nat{i < n} -> lseq (vec_t t w) w -> lseq (vec_t t w) w

    n: Prims.nat{Prims.pow2 n == w} ->
    i: Prims.nat{i < n} ->
    vs: Lib.Sequence.lseq (Lib.IntVector.vec_t t w) w
  -> Lib.Sequence.lseq (Lib.IntVector.vec_t t w) w