val transpose_ws4_lemma_ij:
    #a:sha2_alg
  -> #m:m_spec{lanes a m == 4} // lanes a m * lanes a m = 16
  -> ws:ws_spec a m
  -> j:nat{j < lanes a m}
  -> i:nat{i < 16} ->
  Lemma
   (let l = lanes a m in
    (vec_v (transpose_ws4 ws).[i]).[j] == (vec_v ws.[i / l * l + j]).[i % l])
let transpose_ws4_lemma_ij #a #m ws j i =
  let l = lanes a m in
  let i_sub = i / l in
  let j_sub = i % l in
  assert (i_sub * l + j_sub == i);

  let vs = sub ws (i_sub * l) l in
  eq_intro (sub (transpose_ws4 ws) (i_sub * l) l) (transpose4x4_lseq vs);
  //assert ((transpose_ws4 ws).[i] == (sub (transpose_ws4 ws) (i_sub * l) l).[j_sub]);
  //assert ((transpose_ws4 ws).[i] == (transpose4x4_lseq vs).[j_sub]);
  assert ((vec_v (transpose_ws4 ws).[i]).[j] == (vec_v (transpose4x4_lseq vs).[j_sub]).[j]);
  transpose4x4_lemma vs;
  assert ((vec_v (transpose_ws4 ws).[i]).[j] == (vec_v vs.[j]).[j_sub]);
  assert ((vec_v (transpose_ws4 ws).[i]).[j] == (vec_v ws.[i_sub * l + j]).[j_sub])
val transpose_ws4_lemma_ij:
    #a:sha2_alg
  -> #m:m_spec{lanes a m == 4} // lanes a m * lanes a m = 16
  -> ws:ws_spec a m
  -> j:nat{j < lanes a m}
  -> i:nat{i < 16} ->
  Lemma
   (let l = lanes a m in
    (vec_v (transpose_ws4 ws).[i]).[j] == (vec_v ws.[i / l * l + j]).[i % l])
let transpose_ws4_lemma_ij #a #m ws j i =
let l = lanes a m in
let i_sub = i / l in
let j_sub = i % l in
assert (i_sub * l + j_sub == i);
let vs = sub ws (i_sub * l) l in
eq_intro (sub (transpose_ws4 ws) (i_sub * l) l) (transpose4x4_lseq vs);
assert ((vec_v (transpose_ws4 ws).[ i ]).[ j ] == (vec_v (transpose4x4_lseq vs).[ j_sub ]).[ j ]);
transpose4x4_lemma vs;
assert ((vec_v (transpose_ws4 ws).[ i ]).[ j ] == (vec_v vs.[ j ]).[ j_sub ]);
assert ((vec_v (transpose_ws4 ws).[ i ]).[ j ] == (vec_v ws.[ i_sub * l + j ]).[ j_sub ])
Hacl.Spec.SHA2.Lemmas.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.Transpose.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.SHA2.Vec.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.SHA2.Lemmas.fst
Spec.Hash.Definitions.sha2_alg Hacl.Spec.SHA2.Vec.m_spec Prims.eq2 Prims.int Hacl.Spec.SHA2.Vec.lanes Hacl.Spec.SHA2.Vec.ws_spec Prims.nat Prims.b2t Prims.op_LessThan Prims._assert Lib.IntTypes.uint_t Spec.Hash.Definitions.word_t Lib.IntTypes.SEC Prims.l_or FStar.Seq.Base.index Lib.Sequence.to_seq Lib.IntVector.vec_v Lib.Sequence.op_String_Access Hacl.Spec.SHA2.Vec.element_t Prims.op_Addition FStar.Mul.op_Star Hacl.Spec.SHA2.Vec.transpose_ws4 Prims.unit Lib.IntVector.Transpose.transpose4x4_lemma Lib.IntVector.vec_t Lib.IntVector.Transpose.transpose4x4_lseq Lib.Sequence.eq_intro Lib.Sequence.sub Lib.Sequence.lseq Prims.l_and FStar.Seq.Base.seq FStar.Seq.Base.slice Prims.op_Multiply Prims.l_Forall Lib.Sequence.index Prims.op_Modulus Prims.op_Division Hacl.Spec.SHA2.Vec.lanes_t
module Hacl.Spec.SHA2.Lemmas

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

open Spec.Hash.Definitions
open Hacl.Spec.SHA2.Vec


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

val transpose_ws4_lemma_ij:
    #a:sha2_alg
  -> #m:m_spec{lanes a m == 4} // lanes a m * lanes a m = 16
  -> ws:ws_spec a m
  -> j:nat{j < lanes a m}
  -> i:nat{i < 16} ->
  Lemma
   (let l = lanes a m in
    (vec_v (transpose_ws4 ws).[i]).[j] == (vec_v ws.[i / l * l + j]).[i % l])
val transpose_ws4_lemma_ij:
    #a:sha2_alg
  -> #m:m_spec{lanes a m == 4} // lanes a m * lanes a m = 16
  -> ws:ws_spec a m
  -> j:nat{j < lanes a m}
  -> i:nat{i < 16} ->
  Lemma
   (let l = lanes a m in
    (vec_v (transpose_ws4 ws).[i]).[j] == (vec_v ws.[i / l * l + j]).[i % l])

    ws: Hacl.Spec.SHA2.Vec.ws_spec a m ->
    j: Prims.nat{j < Hacl.Spec.SHA2.Vec.lanes a m} ->
    i: Prims.nat{i < 16}
  -> FStar.Pervasives.Lemma
    (ensures
      (let l = Hacl.Spec.SHA2.Vec.lanes a m in
        (Lib.IntVector.vec_v (Hacl.Spec.SHA2.Vec.transpose_ws4 ws).[ i ]).[ j ] ==
        (Lib.IntVector.vec_v ws.[ (i / l) * l + j ]).[ i % l ]))