module Spec.Chacha20_vec1.Lemmas

open FStar.HyperStack.All

module ST = FStar.HyperStack.ST

open FStar.Mul
open FStar.Seq
open FStar.UInt32
open FStar.Endianness
open Spec.Lib

open Seq.Create
open Spec.Chacha20
open Spec.Chacha20_vec

module S = Spec.Chacha20
module V = Spec.Chacha20_vec

let state = S.state
let vec_state = V.state


#set-options "--max_fuel 0 --z3rlimit 100"


let state_to_vec_state (s:state) : Tot vec_state =
  let s0 = slice s 0  4  in
  let s1 = slice s 4  8  in
  let s2 = slice s 8  12 in
  let s3 = slice s 12 16 in
  create_4 s0 s1 s2 s3


let vec_state_to_state (s:vec_state) : Tot state =
  let s0 = index s 0 in
  let s1 = index s 1 in
  let s2 = index s 2 in
  let s3 = index s 3 in
  s0 @| s1 @| s2 @| s3


val lemma_state (s:state) : Lemma (vec_state_to_state (state_to_vec_state s) == s)
let lemma_state s =
  let s0 = slice s 0  4  in
  let s1 = slice s 4  8  in
  let s2 = slice s 8  12 in
  let s3 = slice s 12 16 in
  lemma_eq_intro (s0 @| s1 @| s2 @| s3) s


val lemma_vec_state (s:vec_state) : Lemma (state_to_vec_state (vec_state_to_state s) == s)
let lemma_vec_state s =
  let s0 = index s 0 in
  let s1 = index s 1 in
  let s2 = index s 2 in
  let s3 = index s 3 in
  let s' = s0 @| s1 @| s2 @| s3 in
  lemma_eq_intro (slice s' 0   4) s0;
  lemma_eq_intro (slice s' 4   8) s1;
  lemma_eq_intro (slice s' 8  12) s2;
  lemma_eq_intro (slice s' 12 16) s3;
  lemma_eq_intro (create_4 s0 s1 s2 s3) (s)


unfold let eq_states' (s:state) (s':vec_state) : GTot Type0 =
   let s0' = index (index s' 0) 0 in   let s1' = index (index s' 0) 1 in
   let s2' = index (index s' 0) 2 in   let s3' = index (index s' 0) 3 in
   let s4' = index (index s' 1) 0 in   let s5' = index (index s' 1) 1 in
   let s6' = index (index s' 1) 2 in   let s7' = index (index s' 1) 3 in
   let s8' = index (index s' 2) 0 in   let s9' = index (index s' 2) 1 in
   let s10' = index (index s' 2) 2 in  let s11' = index (index s' 2) 3 in
   let s12' = index (index s' 3) 0 in  let s13' = index (index s' 3) 1 in
   let s14' = index (index s' 3) 2 in  let s15' = index (index s' 3) 3 in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   s0' == s0 /\ s1' == s1 /\ s2' == s2 /\ s3' == s3
   /\ s4' == s4 /\ s5' == s5 /\ s6' == s6 /\ s7' == s7
   /\ s8' == s8 /\ s9' == s9 /\ s10' == s10 /\ s11' == s11
   /\ s12' == s12 /\ s13' == s13 /\ s14' == s14 /\ s15' == s15


let eq_states (s:state) (s':vec_state) : GTot Type0 =
  vec_state_to_state s' == s


val lemma_eq_states_intro: s:state -> s':vec_state -> Lemma
  (requires (eq_states' s s'))
  (ensures (eq_states s s'))
let lemma_eq_states_intro s s' =
  lemma_eq_intro (vec_state_to_state s') s


let quarter_round_vec (s:vec_state) : Tot vec_state =
  let s = V.line 0 1 3 16ul s in
  let s = V.line 2 3 1 12ul s in
  let s = V.line 0 1 3 8ul  s in
  let s = V.line 2 3 1 7ul  s in
  s


let lined (a:t) (b:t) (c:t) (d:t) (a1:t) (b1:t) (c1:t) (d1:t) : GTot Type0 =
  let open FStar.UInt32 in
  let a' = a +%^ b in
  let d' = Spec.Lib.rotate_left (d ^^ a') 16ul in
  let c' = c +%^ d' in
  let b' = Spec.Lib.rotate_left (b ^^ c') 12ul in
  let a'' = a' +%^ b' in
  let d'' = Spec.Lib.rotate_left (d' ^^ a'') 8ul in
  let c'' = c' +%^ d'' in
  let b'' = Spec.Lib.rotate_left (b' ^^ c'') 7ul in
  a1 == a'' /\ b1 == b'' /\ c1 == c'' /\ d1 == d''


val line_: a:S.idx -> b:S.idx -> d:S.idx -> ss:UInt32.t {v ss > 0 /\ v ss < 32} -> s:state -> Tot (s':state{s' == S.line a b d ss s})
let line_ a b d s m =
  let open FStar.UInt32 in
  let m = upd m a (index m a +%^ index m b) in
  let m = upd m d (Spec.Lib.rotate_left (index m d ^^  index m a) s) in
  m


#reset-options "--max_fuel 0 --z3rlimit 500"

let new_line (s:state) (a:S.idx) (b:S.idx) (d:S.idx{a <> b /\ a <> d /\ b <> d}) (ss:UInt32.t{v ss > 0 /\ v ss < 32}) : Tot (s':state{
  let sa = index s a in let sb = index s b in let sd = index s d in
  let sa' = index s' a in let sb' = index s' b in let sd' = index s' d in
  let open FStar.UInt32 in
  let a' = sa +%^ sb in
  let d' = Spec.Lib.rotate_left (sd ^^ a') ss in
  sa' == a' /\ sd' == d'
  /\ (forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> a /\ i <> d) ==> index s' i == index s i)
  })
  = line_ a b d ss s


let quarter_round_standard
  (s:state) (a:S.idx) (b:S.idx) (c:S.idx) (d:S.idx{a <> b /\ a <> c /\ a <> d /\ b <> c /\ b <> d /\ c <> d}) :
  Tot (s':state{s' == S.quarter_round a b c d s}) =
  let s = new_line s a b d 16ul in
  let s = new_line s c d b 12ul in
  let s = new_line s a b d 8ul  in
  let s = new_line s c d b 7ul  in
  s


#reset-options "--max_fuel 0 --z3rlimit 500"

let lemma_quarter_round_standard
  (s:state) (a:S.idx) (b:S.idx) (c:S.idx) (d:S.idx{a <> b /\ a <> c /\ a <> d /\ b <> c /\ b <> d /\ c <> d}) :
  Lemma
  (let s' = quarter_round_standard s a b c d in
   let sa = index s a in let sb = index s b in let sc = index s c in let sd = index s d in
   let sa' = index s' a in let sb' = index s' b in let sc' = index s' c in let sd' = index s' d in
   lined sa sb sc sd sa' sb' sc' sd'
   /\ (forall (i:nat). {:pattern (Seq.index s' i)} (i < 16 /\ i <> a /\ i <> b /\ i <> c /\ i <> d
     ==> index s' i == index s i)))
   = ()


#reset-options "--max_fuel 0 --z3rlimit 1000"

let lemma_quarter_round_vectorized (s:vec_state) : Lemma
  (let s' = quarter_round_vec s in
   let s0 = index (index s 0) 0 in   let s1 = index (index s 0) 1 in
   let s2 = index (index s 0) 2 in   let s3 = index (index s 0) 3 in
   let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
   let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
   let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
   let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
   let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
   let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
   let s0' = index (index s' 0) 0 in   let s1' = index (index s' 0) 1 in
   let s2' = index (index s' 0) 2 in   let s3' = index (index s' 0) 3 in
   let s4' = index (index s' 1) 0 in   let s5' = index (index s' 1) 1 in
   let s6' = index (index s' 1) 2 in   let s7' = index (index s' 1) 3 in
   let s8' = index (index s' 2) 0 in   let s9' = index (index s' 2) 1 in
   let s10' = index (index s' 2) 2 in  let s11' = index (index s' 2) 3 in
   let s12' = index (index s' 3) 0 in  let s13' = index (index s' 3) 1 in
   let s14' = index (index s' 3) 2 in  let s15' = index (index s' 3) 3 in
   lined s0 s4 s8 s12 s0' s4' s8' s12'
   /\ lined s1 s5 s9 s13 s1' s5' s9' s13'
   /\ lined s2 s6 s10 s14 s2' s6' s10' s14'
   /\ lined s3 s7 s11 s15 s3' s7' s11' s15')
   = ()


#reset-options "--max_fuel 0 --z3rlimit 5"

val lemma_forall_elim: p:(nat -> Type) ->  q:(nat -> Type) -> j:nat{p j} ->
  Lemma (requires (forall (i:nat). p i ==> q i))
        (ensures (q j))
let lemma_forall_elim p q j = ()

val lemma_column_round_standard_1: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 0 /\ i <> 4 /\ i <> 8 /\ i <> 12)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s1 == s1' /\ s2 == s2' /\ s3 == s3'
   /\ s5 == s5' /\ s6 == s6' /\ s7 == s7'
   /\ s9 == s9' /\ s10 == s10' /\ s11 == s11'
   /\ s13 == s13' /\ s14 == s14' /\ s15 == s15'))
let lemma_column_round_standard_1 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 0 /\ i <> 4 /\ i <> 8 /\ i <> 12) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 1;
  lemma_forall_elim p q 2;
  lemma_forall_elim p q 3;
  lemma_forall_elim p q 5;
  lemma_forall_elim p q 6;
  lemma_forall_elim p q 7;
  lemma_forall_elim p q 9;
  lemma_forall_elim p q 10;
  lemma_forall_elim p q 11;
  lemma_forall_elim p q 13;
  lemma_forall_elim p q 14;
  lemma_forall_elim p q 15


val column_round_standard_1: s:state -> Tot (s':state{
  (let s'' = S.quarter_round 0 4 8 12 s in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s4 s8 s12 s0' s4' s8' s12'
   /\ s'' == s'
   /\ s1 == s1' /\ s2 == s2' /\ s3 == s3'
   /\ s5 == s5' /\ s6 == s6' /\ s7 == s7'
   /\ s9 == s9' /\ s10 == s10' /\ s11 == s11'
   /\ s13 == s13' /\ s14 == s14' /\ s15 == s15')})
let column_round_standard_1 s =
  lemma_quarter_round_standard s 0 4 8 12;
  let s' = quarter_round_standard s 0 4 8 12 in
  cut (lined (index s 0) (index s 4) (index s 8) (index s 12) (index s' 0) (index s' 4) (index s' 8) (index s' 12));
  lemma_column_round_standard_1 s s';
  s'


val lemma_column_round_standard_2: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 1 /\ i <> 5 /\ i <> 9 /\ i <> 13)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s0 == s0' /\ s2 == s2' /\ s3 == s3'
   /\ s4 == s4' /\ s6 == s6' /\ s7 == s7'
   /\ s8 == s8' /\ s10 == s10' /\ s11 == s11'
   /\ s12 == s12' /\ s14 == s14' /\ s15 == s15'))
let lemma_column_round_standard_2 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 1 /\ i <> 5 /\ i <> 9 /\ i <> 13) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 0;
  lemma_forall_elim p q 2;
  lemma_forall_elim p q 3;
  lemma_forall_elim p q 4;
  lemma_forall_elim p q 6;
  lemma_forall_elim p q 7;
  lemma_forall_elim p q 8;
  lemma_forall_elim p q 10;
  lemma_forall_elim p q 11;
  lemma_forall_elim p q 12;
  lemma_forall_elim p q 14;
  lemma_forall_elim p q 15


val column_round_standard_2: s:state -> Tot (s':state{
  (let s'' = S.quarter_round 0 4 8 12 s in
   let s'' = S.quarter_round 1 5 9 13 s'' in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s4 s8 s12 s0' s4' s8' s12'
   /\ s'' == s'
   /\ lined s1 s5 s9 s13 s1' s5' s9' s13'
   /\ s2 == s2' /\ s3 == s3'
   /\ s6 == s6' /\ s7 == s7'
   /\ s10 == s10' /\ s11 == s11'
   /\ s14 == s14' /\ s15 == s15')})
let column_round_standard_2 s =
  let s' = column_round_standard_1 s in
  lemma_quarter_round_standard s' 1 5 9 13;
  let s'' = quarter_round_standard s' 1 5 9 13 in
  lemma_column_round_standard_2 s' s'';
  s''


val lemma_column_round_standard_3: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 2 /\ i <> 6 /\ i <> 10 /\ i <> 14)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s0 == s0' /\ s1 == s1' /\ s3 == s3'
   /\ s4 == s4' /\ s5 == s5' /\ s7 == s7'
   /\ s8 == s8' /\ s9 == s9' /\ s11 == s11'
   /\ s12 == s12' /\ s13 == s13' /\ s15 == s15'))
let lemma_column_round_standard_3 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 2 /\ i <> 6 /\ i <> 10 /\ i <> 14) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 0;
  lemma_forall_elim p q 1;
  lemma_forall_elim p q 3;
  lemma_forall_elim p q 4;
  lemma_forall_elim p q 5;
  lemma_forall_elim p q 7;
  lemma_forall_elim p q 8;
  lemma_forall_elim p q 9;
  lemma_forall_elim p q 11;
  lemma_forall_elim p q 12;
  lemma_forall_elim p q 13;
  lemma_forall_elim p q 15


val column_round_standard_3: s:state -> Tot (s':state{
  (let s'' = S.quarter_round 0 4 8 12 s in
   let s'' = S.quarter_round 1 5 9 13 s'' in
   let s'' = S.quarter_round 2 6 10 14 s'' in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s4 s8 s12 s0' s4' s8' s12'
   /\ lined s1 s5 s9 s13 s1' s5' s9' s13'
   /\ lined s2 s6 s10 s14 s2' s6' s10' s14'
   /\ s'' == s'
   /\ s3 == s3'
   /\ s7 == s7'
   /\ s11 == s11'
   /\ s15 == s15')})
let column_round_standard_3 s =
  let s'' = column_round_standard_2 s in
  lemma_quarter_round_standard s'' 2 6 10 14;
  let s''' = quarter_round_standard s'' 2 6 10 14 in
  lemma_column_round_standard_3 s'' s''';
  s'''


val lemma_column_round_standard_4: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 3 /\ i <> 7 /\ i <> 11 /\ i <> 15)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s0 == s0' /\ s1 == s1' /\ s2 == s2'
   /\ s4 == s4' /\ s5 == s5' /\ s6 == s6'
   /\ s8 == s8' /\ s9 == s9' /\ s10 == s10'
   /\ s12 == s12' /\ s13 == s13' /\ s14 == s14'))
let lemma_column_round_standard_4 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 3 /\ i <> 7 /\ i <> 11 /\ i <> 15) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 0;
  lemma_forall_elim p q 1;
  lemma_forall_elim p q 2;
  lemma_forall_elim p q 4;
  lemma_forall_elim p q 5;
  lemma_forall_elim p q 6;
  lemma_forall_elim p q 8;
  lemma_forall_elim p q 9;
  lemma_forall_elim p q 10;
  lemma_forall_elim p q 12;
  lemma_forall_elim p q 13;
  lemma_forall_elim p q 14


#reset-options "--max_fuel 0"

val lemma_column_round_def: s:state -> Lemma
  (let s' = S.quarter_round 0 4 8 12 s in
   let s' = S.quarter_round 1 5 9 13 s' in
   let s' = S.quarter_round 2 6 10 14 s' in
   let s' = S.quarter_round 3 7 11 15 s' in
   s' == S.column_round s)
let lemma_column_round_def s = ()

val column_round_standard: s:state -> Tot (s':state{
  (s' == S.column_round s
   /\ (let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s4 s8 s12 s0' s4' s8' s12'
   /\ lined s1 s5 s9 s13 s1' s5' s9' s13'
   /\ lined s2 s6 s10 s14 s2' s6' s10' s14'
   /\ lined s3 s7 s11 s15 s3' s7' s11' s15'))})
let column_round_standard s =
  let s''' = column_round_standard_3 s in
  lemma_quarter_round_standard s''' 3 7 11 15;
  let s'''' = quarter_round_standard s''' 3 7 11 15 in
  lemma_column_round_standard_4 s''' s'''';
  lemma_column_round_def s;
  s''''


#reset-options "--max_fuel 0 --z3rlimit 100"

val shuffle_right: x:vec -> n:V.idx -> Tot (x':vec{
  index x' 0 == index x (n % 4)
  /\ index x' 1 == index x ((n+1) % 4)
  /\ index x' 2 == index x ((n+2) % 4)
  /\ index x' 3 == index x ((n+3) % 4)})
let shuffle_right x n =
  V.shuffle_right x n


#reset-options "--max_fuel 0 --z3rlimit 100"

val shuffle_rous_1: s:vec_state -> Tot (s':vec_state{
   let s0' = index (index s' 0) 0 in   let s1' = index (index s' 0) 1 in
   let s2' = index (index s' 0) 2 in   let s3' = index (index s' 0) 3 in
   let s4' = index (index s' 1) 0 in   let s5' = index (index s' 1) 1 in
   let s6' = index (index s' 1) 2 in   let s7' = index (index s' 1) 3 in
   let s8' = index (index s' 2) 0 in   let s9' = index (index s' 2) 1 in
   let s10' = index (index s' 2) 2 in  let s11' = index (index s' 2) 3 in
   let s12' = index (index s' 3) 0 in  let s13' = index (index s' 3) 1 in
   let s14' = index (index s' 3) 2 in  let s15' = index (index s' 3) 3 in
   let s0 = index (index s 0) 0 in   let s1 = index (index s 0) 1 in
   let s2 = index (index s 0) 2 in   let s3 = index (index s 0) 3 in
   let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
   let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
   let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
   let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
   let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
   let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
   s0 == s0' /\ s1 == s1' /\ s2 == s2' /\ s3 == s3'
   /\ s4' == s5 /\ s5' == s6 /\ s6' == s7 /\ s7' == s4
   /\ s8' == s10 /\ s9' == s11 /\ s10' == s8 /\ s11' == s9
   /\ s12' == s15 /\ s13' == s12 /\ s14' == s13 /\ s15' == s14
   /\ (let s'' = V.shuffle_row 1 1 s in
     let s'' = V.shuffle_row 2 2 s'' in
     let s'' = V.shuffle_row 3 3 s'' in
     s'' == s')
   })
let shuffle_rous_1 s =
  let s' = shuffle_row 1 1 s in
  lemma_eq_intro (shuffle_right (index s 1) 1) (index s' 1);
  lemma_eq_intro (index s 0) (index s' 0);
  lemma_eq_intro (index s 2) (index s' 2);
  lemma_eq_intro (index s 3) (index s' 3);
  let s'' = shuffle_row 2 2 s' in
  lemma_eq_intro (shuffle_right (index s' 2) 2) (index s'' 2);
  lemma_eq_intro (index s' 0) (index s'' 0);
  lemma_eq_intro (index s' 1) (index s'' 1);
  lemma_eq_intro (index s' 3) (index s'' 3);
  let s''' = shuffle_row 3 3 s'' in
  lemma_eq_intro (shuffle_right (index s'' 3) 3) (index s''' 3);
  lemma_eq_intro (index s'' 0) (index s''' 0);
  lemma_eq_intro (index s'' 1) (index s''' 1);
  lemma_eq_intro (index s'' 2) (index s''' 2);
  s'''


val shuffle_rous_2: s:vec_state -> Tot (s':vec_state{
   let s0' = index (index s' 0) 0 in   let s1' = index (index s' 0) 1 in
   let s2' = index (index s' 0) 2 in   let s3' = index (index s' 0) 3 in
   let s4' = index (index s' 1) 0 in   let s5' = index (index s' 1) 1 in
   let s6' = index (index s' 1) 2 in   let s7' = index (index s' 1) 3 in
   let s8' = index (index s' 2) 0 in   let s9' = index (index s' 2) 1 in
   let s10' = index (index s' 2) 2 in  let s11' = index (index s' 2) 3 in
   let s12' = index (index s' 3) 0 in  let s13' = index (index s' 3) 1 in
   let s14' = index (index s' 3) 2 in  let s15' = index (index s' 3) 3 in
   let s0 = index (index s 0) 0 in   let s1 = index (index s 0) 1 in
   let s2 = index (index s 0) 2 in   let s3 = index (index s 0) 3 in
   let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
   let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
   let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
   let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
   let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
   let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
   s0 == s0' /\ s1 == s1' /\ s2 == s2' /\ s3 == s3'
   /\ s4' == s7 /\ s5' == s4 /\ s6' == s5 /\ s7' == s6
   /\ s8' == s10 /\ s9' == s11 /\ s10' == s8 /\ s11' == s9
   /\ s12' == s13 /\ s13' == s14 /\ s14' == s15 /\ s15' == s12
   /\ (let s'' = V.shuffle_row 1 3 s in
     let s'' = V.shuffle_row 2 2 s'' in
     let s'' = V.shuffle_row 3 1 s'' in
     s'' == s')
   })
let shuffle_rous_2 s =
  let s' = shuffle_row 1 3 s in
  lemma_eq_intro (shuffle_right (index s 1) 3) (index s' 1);
  lemma_eq_intro (index s 0) (index s' 0);
  lemma_eq_intro (index s 2) (index s' 2);
  lemma_eq_intro (index s 3) (index s' 3);
  let s'' = shuffle_row 2 2 s' in
  lemma_eq_intro (shuffle_right (index s' 2) 2) (index s'' 2);
  lemma_eq_intro (index s' 0) (index s'' 0);
  lemma_eq_intro (index s' 1) (index s'' 1);
  lemma_eq_intro (index s' 3) (index s'' 3);
  let s''' = shuffle_row 3 1 s'' in
  lemma_eq_intro (shuffle_right (index s'' 3) 1) (index s''' 3);
  lemma_eq_intro (index s'' 0) (index s''' 0);
  lemma_eq_intro (index s'' 1) (index s''' 1);
  lemma_eq_intro (index s'' 2) (index s''' 2);
  s'''


#reset-options "--max_fuel 0 --z3rlimit 5"

val lemma_diagonal_round_standard_1: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 0 /\ i <> 5 /\ i <> 10 /\ i <> 15)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s1 == s1' /\ s2 == s2' /\ s3 == s3'
   /\ s4 == s4' /\ s6 == s6' /\ s7 == s7'
   /\ s9 == s9' /\ s8 == s8' /\ s11 == s11'
   /\ s13 == s13' /\ s14 == s14' /\ s12 == s12'))
let lemma_diagonal_round_standard_1 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 0 /\ i <> 5 /\ i <> 10 /\ i <> 15) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 1;
  lemma_forall_elim p q 2;
  lemma_forall_elim p q 3;
  lemma_forall_elim p q 4;
  lemma_forall_elim p q 6;
  lemma_forall_elim p q 7;
  lemma_forall_elim p q 9;
  lemma_forall_elim p q 8;
  lemma_forall_elim p q 11;
  lemma_forall_elim p q 13;
  lemma_forall_elim p q 14;
  lemma_forall_elim p q 12


val diagonal_round_standard_1: s:state -> Tot (s':state{
  (let s'' = S.quarter_round 0 5 10 15 s in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s5 s10 s15 s0' s5' s10' s15'
   /\ s'' == s'
   /\ s1 == s1' /\ s2 == s2' /\ s3 == s3'
   /\ s4 == s4' /\ s6 == s6' /\ s7 == s7'
   /\ s9 == s9' /\ s8 == s8' /\ s11 == s11'
   /\ s13 == s13' /\ s14 == s14' /\ s12 == s12')})
let diagonal_round_standard_1 s =
  lemma_quarter_round_standard s 0 5 10 15;
  let s' = quarter_round_standard s 0 5 10 15 in
  cut (lined (index s 0) (index s 5) (index s 10) (index s 15) (index s' 0) (index s' 5) (index s' 10) (index s' 15));
  lemma_diagonal_round_standard_1 s s';
  s'


val lemma_diagonal_round_standard_2: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 1 /\ i <> 6 /\ i <> 11 /\ i <> 12)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s0 == s0' /\ s2 == s2' /\ s3 == s3'
   /\ s4 == s4' /\ s5 == s5' /\ s7 == s7'
   /\ s8 == s8' /\ s10 == s10' /\ s9 == s9'
   /\ s13 == s13' /\ s14 == s14' /\ s15 == s15'))
let lemma_diagonal_round_standard_2 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 1 /\ i <> 6 /\ i <> 11 /\ i <> 12) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 0;
  lemma_forall_elim p q 2;
  lemma_forall_elim p q 3;
  lemma_forall_elim p q 4;
  lemma_forall_elim p q 5;
  lemma_forall_elim p q 7;
  lemma_forall_elim p q 8;
  lemma_forall_elim p q 10;
  lemma_forall_elim p q 9;
  lemma_forall_elim p q 13;
  lemma_forall_elim p q 14;
  lemma_forall_elim p q 15


val diagonal_round_standard_2: s:state -> Tot (s':state{
  (let s'' = S.quarter_round 0 5 10 15 s in
   let s'' = S.quarter_round 1 6 11 12 s'' in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s5 s10 s15 s0' s5' s10' s15'
   /\ s'' == s'
   /\ lined s1 s6 s11 s12 s1' s6' s11' s12'
   /\ s2 == s2' /\ s3 == s3'
   /\ s4 == s4' /\ s7 == s7'
   /\ s8 == s8' /\ s9 == s9'
   /\ s14 == s14' /\ s13 == s13')})
let diagonal_round_standard_2 s =
  let s' = diagonal_round_standard_1 s in
  lemma_quarter_round_standard s' 1 6 11 12;
  let s'' = quarter_round_standard s' 1 6 11 12 in
  lemma_diagonal_round_standard_2 s' s'';
  s''


val lemma_diagonal_round_standard_3: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 2 /\ i <> 7 /\ i <> 8 /\ i <> 13)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s0 == s0' /\ s1 == s1' /\ s3 == s3'
   /\ s4 == s4' /\ s5 == s5' /\ s6 == s6'
   /\ s10 == s10' /\ s9 == s9' /\ s11 == s11'
   /\ s12 == s12' /\ s14 == s14' /\ s15 == s15'))
let lemma_diagonal_round_standard_3 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 2 /\ i <> 7 /\ i <> 8 /\ i <> 13) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 0;
  lemma_forall_elim p q 1;
  lemma_forall_elim p q 3;
  lemma_forall_elim p q 4;
  lemma_forall_elim p q 5;
  lemma_forall_elim p q 6;
  lemma_forall_elim p q 10;
  lemma_forall_elim p q 9;
  lemma_forall_elim p q 11;
  lemma_forall_elim p q 12;
  lemma_forall_elim p q 14;
  lemma_forall_elim p q 15


val diagonal_round_standard_3: s:state -> Tot (s':state{
  (let s'' = S.quarter_round 0 5 10 15 s in
   let s'' = S.quarter_round 1 6 11 12 s'' in
   let s'' = S.quarter_round 2 7  8 13 s'' in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s5 s10 s15 s0' s5' s10' s15'
   /\ lined s1 s6 s11 s12 s1' s6' s11' s12'
   /\ lined s2 s7 s8 s13 s2' s7' s8' s13'
   /\ s'' == s'
   /\ s3 == s3'
   /\ s4 == s4'
   /\ s9 == s9'
   /\ s14 == s14')})
let diagonal_round_standard_3 s =
  let s'' = diagonal_round_standard_2 s in
  lemma_quarter_round_standard s'' 2 7 8 13;
  let s''' = quarter_round_standard s'' 2 7 8 13 in
  lemma_diagonal_round_standard_3 s'' s''';
  s'''


val lemma_diagonal_round_standard_4: s:state -> s':state -> Lemma
  (requires ((forall (i:nat). {:pattern (index s' i)} (i < 16 /\ i <> 3 /\ i <> 4 /\ i <> 9 /\ i <> 14)  ==> index s' i == index s i)))
  (ensures (
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   s0 == s0' /\ s1 == s1' /\ s2 == s2'
   /\ s6 == s6' /\ s5 == s5' /\ s7 == s7'
   /\ s8 == s8' /\ s11 == s11' /\ s10 == s10'
   /\ s12 == s12' /\ s13 == s13' /\ s15 == s15'))
let lemma_diagonal_round_standard_4 s s' =
  let p = fun (i:nat) -> (i < 16 /\ i <> 3 /\ i <> 4 /\ i <> 9 /\ i <> 14) in
  let q = fun (i:nat) -> (i < 16 /\ index s' i == index s i) in
  lemma_forall_elim p q 0;
  lemma_forall_elim p q 1;
  lemma_forall_elim p q 2;
  lemma_forall_elim p q 7;
  lemma_forall_elim p q 5;
  lemma_forall_elim p q 6;
  lemma_forall_elim p q 8;
  lemma_forall_elim p q 11;
  lemma_forall_elim p q 10;
  lemma_forall_elim p q 12;
  lemma_forall_elim p q 13;
  lemma_forall_elim p q 15


#reset-options "--max_fuel 0 --z3rlimit 10"

val lemma_diagonal_round_def: s:state -> Lemma
  (let s' = S.quarter_round 0 5 10 15 s in
   let s' = S.quarter_round 1 6 11 12 s' in
   let s' = S.quarter_round 2 7 8  13 s' in
   let s' = S.quarter_round 3 4 9  14 s' in
   s' == S.diagonal_round s)
let lemma_diagonal_round_def s = ()

val diagonal_round_standard: s:state -> Tot (s':state{
  (s' == S.diagonal_round s
   /\ (let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   let s0' = index s' 0 in   let s1' = index s' 1 in
   let s2' = index s' 2 in   let s3' = index s' 3 in
   let s4' = index s' 4 in   let s5' = index s' 5 in
   let s6' = index s' 6 in   let s7' = index s' 7 in
   let s8' = index s' 8 in   let s9' = index s' 9 in
   let s10' = index s' 10 in  let s11' = index s' 11 in
   let s12' = index s' 12 in  let s13' = index s' 13 in
   let s14' = index s' 14 in  let s15' = index s' 15 in
   lined s0 s5 s10 s15 s0' s5' s10' s15'
   /\ lined s1 s6 s11 s12 s1' s6' s11' s12'
   /\ lined s2 s7 s8 s13 s2' s7' s8' s13'
   /\ lined s3 s4 s9 s14 s3' s4' s9' s14'))})
let diagonal_round_standard s =
  let s''' = diagonal_round_standard_3 s in
  lemma_quarter_round_standard s''' 3 4 9 14;
  let s'''' = quarter_round_standard s''' 3 4 9 14 in
  lemma_diagonal_round_standard_4 s''' s'''';
  lemma_diagonal_round_def s;
  s''''


val diagonal_round_vectorized: s:vec_state -> Tot (s':vec_state{
  (let s0 = index (index s 0) 0 in   let s1 = index (index s 0) 1 in
   let s2 = index (index s 0) 2 in   let s3 = index (index s 0) 3 in
   let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
   let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
   let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
   let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
   let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
   let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
   let s0' = index (index s' 0) 0 in   let s1' = index (index s' 0) 1 in
   let s2' = index (index s' 0) 2 in   let s3' = index (index s' 0) 3 in
   let s4' = index (index s' 1) 0 in   let s5' = index (index s' 1) 1 in
   let s6' = index (index s' 1) 2 in   let s7' = index (index s' 1) 3 in
   let s8' = index (index s' 2) 0 in   let s9' = index (index s' 2) 1 in
   let s10' = index (index s' 2) 2 in  let s11' = index (index s' 2) 3 in
   let s12' = index (index s' 3) 0 in  let s13' = index (index s' 3) 1 in
   let s14' = index (index s' 3) 2 in  let s15' = index (index s' 3) 3 in
   lined s0 s5 s10 s15 s0' s5' s10' s15'
   /\ lined s1 s6 s11 s12 s1' s6' s11' s12'
   /\ lined s2 s7 s8 s13 s2' s7' s8' s13'
   /\ lined s3 s4 s9 s14 s3' s4' s9' s14')})
let diagonal_round_vectorized s =
  let s' = shuffle_rous_1 s in
  lemma_quarter_round_vectorized s';
  let s'' = quarter_round_vec s' in
  let s''' = shuffle_rous_2 s'' in
  s'''


#reset-options "--max_fuel 0 --z3rlimit 100"


val lemma_quarter_round: s:vec_state -> Lemma
  (quarter_round_vec s == V.round s)
let lemma_quarter_round s = ()

val lemma_column_round: s:vec_state -> Lemma
  (quarter_round_vec s == V.column_round s)
let lemma_column_round s = ()

val lemma_shuffle_rows_1: s:vec_state -> Lemma
  (shuffle_rous_1 s == V.shuffle_rows_0123 s)
let lemma_shuffle_rows_1 s = ()

val lemma_shuffle_rows_2: s:vec_state -> Lemma
  (shuffle_rous_2 s == V.shuffle_rows_0321 s)
let lemma_shuffle_rows_2 s = ()

val lemma_diagonal_round_vec: s:vec_state -> Lemma
  (diagonal_round_vectorized s == V.diagonal_round s)
let lemma_diagonal_round_vec s =
  lemma_shuffle_rows_1 s;
  let s' = shuffle_rous_1 s in
  lemma_quarter_round s';
  let s'' = quarter_round_vec s' in
  lemma_shuffle_rows_2 s''

val double_round_vec: s:vec_state -> Tot vec_state
let double_round_vec s =
  let s' = quarter_round_vec s in
  let s'' = diagonal_round_vectorized s' in
  s''

val lemma_double_round_def: s:vec_state -> Lemma
  (double_round_vec s == V.double_round s)
let lemma_double_round_def s =
  lemma_column_round s;
  let s = quarter_round_vec s in
  lemma_diagonal_round_vec s

(* #reset-options "--initial_fuel 1 --max_fuel 1 --z3rlimit 100" *)

(* // TODO: move somewhere else *)
(* private val lemma_seq_of_list: (#a:Type) -> (l:list a) -> Lemma *)
(*   (forall (i:nat). {:pattern (Seq.index (Seq.seq_of_list l) i)} i < List.Tot.length l *)
(*              ==> Seq.index (Seq.seq_of_list l) i == List.Tot.index l i) *)
(* let rec lemma_seq_of_list #a l = *)
(*   match l with *)
(*   | [] -> Seq.lemma_eq_intro (Seq.seq_of_list l) Seq.createEmpty *)
(*   | hd::tl -> ( *)
(*     lemma_seq_of_list #a tl; *)
(*     Seq.lemma_eq_intro (Seq.seq_of_list l) (Seq.cons hd (Seq.seq_of_list tl)) *)
(*   ) *)

#reset-options "--max_fuel 0 --z3rlimit 100"

val lemma_setup_standard_1: k:S.key -> n:S.nonce -> c:S.counter -> Lemma
  (let s = S.setup k n c in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   s0 == 0x61707865ul /\ s1 == 0x3320646eul /\ s2 == 0x79622d32ul /\ s3 == 0x6b206574ul)
let lemma_setup_standard_1 k n c = ()

val lemma_setup_standard_2: k:S.key -> n:S.nonce -> c:S.counter -> Lemma
  (let s = S.setup k n c in
   let k = uint32s_from_le 8 k in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   s4 == index k 0 /\ s5 == index k 1 /\ s6 == index k 2 /\ s7 == index k 3
   /\ s8 == index k 4 /\ s9 == index k 5 /\ s10 == index k 6 /\ s11 == index k 7)
let lemma_setup_standard_2 k n c =
  lemma_eq_intro (slice (S.setup k n c) 4 12) (uint32s_from_le 8 k)


val lemma_setup_standard_3: k:S.key -> n:S.nonce -> c:S.counter -> Lemma
  (let s = S.setup k n c in
   let n = uint32s_from_le 3 n in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   s12 == UInt32.uint_to_t c /\ s13 == index n 0 /\ s14 == index n 1 /\ s15 == index n 2)
let lemma_setup_standard_3 k n c =
  lemma_eq_intro (slice (S.setup k n c) 12 13) (singleton (UInt32.uint_to_t c));
  lemma_eq_intro (slice (S.setup k n c) 13 16) (uint32s_from_le 3 n)


val lemma_setup_standard: k:S.key -> n:S.nonce -> c:S.counter -> Lemma
  (let s = S.setup k n c in
   let k = uint32s_from_le 8 k in
   let n = uint32s_from_le 3 n in
   let s0 = index s 0 in   let s1 = index s 1 in
   let s2 = index s 2 in   let s3 = index s 3 in
   let s4 = index s 4 in   let s5 = index s 5 in
   let s6 = index s 6 in   let s7 = index s 7 in
   let s8 = index s 8 in   let s9 = index s 9 in
   let s10 = index s 10 in  let s11 = index s 11 in
   let s12 = index s 12 in  let s13 = index s 13 in
   let s14 = index s 14 in  let s15 = index s 15 in
   s0 == 0x61707865ul /\ s1 == 0x3320646eul /\ s2 == 0x79622d32ul /\ s3 == 0x6b206574ul
   /\ s4 == index k 0 /\ s5 == index k 1 /\ s6 == index k 2 /\ s7 == index k 3
   /\ s8 == index k 4 /\ s9 == index k 5 /\ s10 == index k 6 /\ s11 == index k 7
   /\ s12 == UInt32.uint_to_t c /\ s13 == index n 0 /\ s14 == index n 1 /\ s15 == index n 2)
let lemma_setup_standard k n c =
  lemma_setup_standard_1 k n c;
  lemma_setup_standard_2 k n c;
  lemma_setup_standard_3 k n c


val lemma_setup_vec_1: k:V.key -> n:V.nonce -> c:V.counter -> Lemma
  (let s = V.setup k n c in
   let s0 = index (index s 0) 0 in   let s1 = index (index s 0) 1 in
   let s2 = index (index s 0) 2 in   let s3 = index (index s 0) 3 in
   let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
   let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
   let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
   let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
   let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
   let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
   s0 == 0x61707865ul /\ s1 == 0x3320646eul /\ s2 == 0x79622d32ul /\ s3 == 0x6b206574ul)
let lemma_setup_vec_1 k n c = ()


val lemma_setup_vec_2: k:S.key -> n:S.nonce -> c:S.counter -> Lemma
  (let s = V.setup k n c in
   let k = uint32s_from_le 8 k in
   let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
   let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
   let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
   let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
   s4 == index k 0 /\ s5 == index k 1 /\ s6 == index k 2 /\ s7 == index k 3
   /\ s8 == index k 4 /\ s9 == index k 5 /\ s10 == index k 6 /\ s11 == index k 7)
let lemma_setup_vec_2 k n c =
  lemma_uint32s_from_le_slice 8 k 4;
  let key_part_1:vec = uint32s_from_le 4 (Seq.slice k 0 16)  in
  let key_part_2:vec = uint32s_from_le 4 (Seq.slice k 16 32) in
  lemma_eq_intro (key_part_1 @| key_part_2) (uint32s_from_le 8 k);
  let nonce    :vec = Seq.cons (UInt32.uint_to_t c) (uint32s_from_le 3 n) in
  lemma_eq_intro (index (V.setup k n c) 1) (uint32s_from_le 4 (slice k 0 16));
  lemma_eq_intro (index (V.setup k n c) 2) (uint32s_from_le 4 (slice k 16 32))


val lemma_setup_vec_3: k:V.key -> n:V.nonce -> c:V.counter -> Lemma
  (let s = V.setup k n c in
   let n = uint32s_from_le 3 n in
   let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
   let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
   s12 == UInt32.uint_to_t c /\ s13 == index n 0 /\ s14 == index n 1 /\ s15 == index n 2)
let lemma_setup_vec_3 k n c =
  let nonce    :vec = Seq.cons (UInt32.uint_to_t c) (uint32s_from_le 3 n) in
  lemma_eq_intro (slice nonce 1 4) (uint32s_from_le 3 n)


val lemma_setup_vec: k:V.key -> n:V.nonce -> c:V.counter -> Lemma
  (let s = V.setup k n c in
   let k = uint32s_from_le 8 k in
   let n = uint32s_from_le 3 n in
   let s0 = index (index s 0) 0 in   let s1 = index (index s 0) 1 in
   let s2 = index (index s 0) 2 in   let s3 = index (index s 0) 3 in
   let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
   let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
   let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
   let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
   let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
   let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
   s0 == 0x61707865ul /\ s1 == 0x3320646eul /\ s2 == 0x79622d32ul /\ s3 == 0x6b206574ul
   /\ s4 == index k 0 /\ s5 == index k 1 /\ s6 == index k 2 /\ s7 == index k 3
   /\ s8 == index k 4 /\ s9 == index k 5 /\ s10 == index k 6 /\ s11 == index k 7
   /\ s12 == UInt32.uint_to_t c /\ s13 == index n 0 /\ s14 == index n 1 /\ s15 == index n 2)
let lemma_setup_vec k n c =
  lemma_setup_vec_1 k n c;
  lemma_setup_vec_2 k n c;
  lemma_setup_vec_3 k n c


val lemma_setup: k:S.key -> n:S.nonce -> c:S.counter -> Lemma
  (let sv = V.setup k n c in let s = S.setup k n c in
   eq_states' s sv)
let lemma_setup k n c =
  lemma_setup_standard k n c; lemma_setup_vec k n c


val lemma_iter_state: s:state -> sv:vec_state{eq_states' s sv} ->
  f:(state -> Tot state) -> fv:(vec_state -> Tot vec_state)  -> n:nat -> Lemma
  (requires (forall (s:state) (sv:vec_state). eq_states' s sv ==> eq_states' (f s) (fv sv)))
  (ensures (eq_states' (iter n f s) (iter n fv sv)))
  (decreases n)
#reset-options "--initial_fuel 1 --max_fuel 1 --z3rlimit 100"
let rec lemma_iter_state s sv f fv n =
  if n = 0 then ()
  else (
    lemma_iter_state (f s) (fv sv) f fv (n-1)
  )


#reset-options "--max_fuel 0 --z3rlimit 10"

val lemma_column_round_eq : s:state -> sv:vec_state{eq_states' s sv} -> Lemma
  (let s = S.column_round s in let sv = V.column_round sv in eq_states' s sv)
let lemma_column_round_eq s sv =
  cut (eq_states' s sv);
  let s' = column_round_standard s in
  lemma_column_round sv;
  let sv' = quarter_round_vec sv in
  let s0 = index s 0 in   let s1 = index s 1 in
  let s2 = index s 2 in   let s3 = index s 3 in
  let s4 = index s 4 in   let s5 = index s 5 in
  let s6 = index s 6 in   let s7 = index s 7 in
  let s8 = index s 8 in   let s9 = index s 9 in
  let s10 = index s 10 in  let s11 = index s 11 in
  let s12 = index s 12 in  let s13 = index s 13 in
  let s14 = index s 14 in  let s15 = index s 15 in
  let sv0 = index (index sv 0) 0 in   let sv1 = index (index sv 0) 1 in
  let sv2 = index (index sv 0) 2 in   let sv3 = index (index sv 0) 3 in
  let sv4 = index (index sv 1) 0 in   let sv5 = index (index sv 1) 1 in
  let sv6 = index (index sv 1) 2 in   let sv7 = index (index sv 1) 3 in
  let sv8 = index (index sv 2) 0 in   let sv9 = index (index sv 2) 1 in
  let sv10 = index (index sv 2) 2 in  let sv11 = index (index sv 2) 3 in
  let sv12 = index (index sv 3) 0 in  let sv13 = index (index sv 3) 1 in
  let sv14 = index (index sv 3) 2 in  let sv15 = index (index sv 3) 3 in
  cut (sv0 == s0); cut (sv1 == s1); cut (sv2 == s2); cut (sv3 == s3);
  cut (sv4 == s4); cut (sv5 == s5); cut (sv6 == s6); cut (sv7 == s7);
  cut (sv8 == s8); cut (sv9 == s9); cut (sv10 == s10); cut (sv11 == s11);
  cut (sv12 == s12); cut (sv13 == s13); cut (sv14 == s14); cut (sv15 == s15);
  let s0' = index s' 0 in   let s1' = index s' 1 in
  let s2' = index s' 2 in   let s3' = index s' 3 in
  let s4' = index s' 4 in   let s5' = index s' 5 in
  let s6' = index s' 6 in   let s7' = index s' 7 in
  let s8' = index s' 8 in   let s9' = index s' 9 in
  let s10' = index s' 10 in  let s11' = index s' 11 in
  let s12' = index s' 12 in  let s13' = index s' 13 in
  let s14' = index s' 14 in  let s15' = index s' 15 in
  let sv0' = index (index sv' 0) 0 in   let sv1' = index (index sv' 0) 1 in
  let sv2' = index (index sv' 0) 2 in   let sv3' = index (index sv' 0) 3 in
  let sv4' = index (index sv' 1) 0 in   let sv5' = index (index sv' 1) 1 in
  let sv6' = index (index sv' 1) 2 in   let sv7' = index (index sv' 1) 3 in
  let sv8' = index (index sv' 2) 0 in   let sv9' = index (index sv' 2) 1 in
  let sv10' = index (index sv' 2) 2 in  let sv11' = index (index sv' 2) 3 in
  let sv12' = index (index sv' 3) 0 in  let sv13' = index (index sv' 3) 1 in
  let sv14' = index (index sv' 3) 2 in  let sv15' = index (index sv' 3) 3 in
  cut (lined s0 s4 s8 s12 s0' s4' s8' s12');
  cut (lined s1 s5 s9 s13 s1' s5' s9' s13');
  cut (lined s2 s6 s10 s14 s2' s6' s10' s14');
  cut (lined s3 s7 s11 s15 s3' s7' s11' s15');
  lemma_quarter_round_vectorized sv;
  cut (lined sv0 sv4 sv8 sv12 sv0' sv4' sv8' sv12');
  cut (lined sv1 sv5 sv9 sv13 sv1' sv5' sv9' sv13');
  cut (lined sv2 sv6 sv10 sv14 sv2' sv6' sv10' sv14');
  cut (lined sv3 sv7 sv11 sv15 sv3' sv7' sv11' sv15');
  cut (sv' == V.column_round sv);
  cut (s' == S.column_round s)


val lemma_diagonal_round_eq : s:state -> sv:vec_state{eq_states' s sv} -> Lemma
  (let s = S.diagonal_round s in let sv = V.diagonal_round sv in eq_states' s sv)
let lemma_diagonal_round_eq s sv =
  cut (eq_states' s sv);
  let s' = diagonal_round_standard s in
  lemma_diagonal_round_vec sv;
  let sv' = diagonal_round_vectorized sv in
  let s0 = index s 0 in   let s1 = index s 1 in
  let s2 = index s 2 in   let s3 = index s 3 in
  let s4 = index s 4 in   let s5 = index s 5 in
  let s6 = index s 6 in   let s7 = index s 7 in
  let s8 = index s 8 in   let s9 = index s 9 in
  let s10 = index s 10 in  let s11 = index s 11 in
  let s12 = index s 12 in  let s13 = index s 13 in
  let s14 = index s 14 in  let s15 = index s 15 in
  let sv0 = index (index sv 0) 0 in   let sv1 = index (index sv 0) 1 in
  let sv2 = index (index sv 0) 2 in   let sv3 = index (index sv 0) 3 in
  let sv4 = index (index sv 1) 0 in   let sv5 = index (index sv 1) 1 in
  let sv6 = index (index sv 1) 2 in   let sv7 = index (index sv 1) 3 in
  let sv8 = index (index sv 2) 0 in   let sv9 = index (index sv 2) 1 in
  let sv10 = index (index sv 2) 2 in  let sv11 = index (index sv 2) 3 in
  let sv12 = index (index sv 3) 0 in  let sv13 = index (index sv 3) 1 in
  let sv14 = index (index sv 3) 2 in  let sv15 = index (index sv 3) 3 in
  cut (sv0 == s0); cut (sv1 == s1); cut (sv2 == s2); cut (sv3 == s3);
  cut (sv4 == s4); cut (sv5 == s5); cut (sv6 == s6); cut (sv7 == s7);
  cut (sv8 == s8); cut (sv9 == s9); cut (sv10 == s10); cut (sv11 == s11);
  cut (sv12 == s12); cut (sv13 == s13); cut (sv14 == s14); cut (sv15 == s15);
  let s0' = index s' 0 in   let s1' = index s' 1 in
  let s2' = index s' 2 in   let s3' = index s' 3 in
  let s4' = index s' 4 in   let s5' = index s' 5 in
  let s6' = index s' 6 in   let s7' = index s' 7 in
  let s8' = index s' 8 in   let s9' = index s' 9 in
  let s10' = index s' 10 in  let s11' = index s' 11 in
  let s12' = index s' 12 in  let s13' = index s' 13 in
  let s14' = index s' 14 in  let s15' = index s' 15 in
  let sv0' = index (index sv' 0) 0 in   let sv1' = index (index sv' 0) 1 in
  let sv2' = index (index sv' 0) 2 in   let sv3' = index (index sv' 0) 3 in
  let sv4' = index (index sv' 1) 0 in   let sv5' = index (index sv' 1) 1 in
  let sv6' = index (index sv' 1) 2 in   let sv7' = index (index sv' 1) 3 in
  let sv8' = index (index sv' 2) 0 in   let sv9' = index (index sv' 2) 1 in
  let sv10' = index (index sv' 2) 2 in  let sv11' = index (index sv' 2) 3 in
  let sv12' = index (index sv' 3) 0 in  let sv13' = index (index sv' 3) 1 in
  let sv14' = index (index sv' 3) 2 in  let sv15' = index (index sv' 3) 3 in
  cut (lined s0 s5 s10 s15 s0' s5' s10' s15');
  cut (lined s1 s6 s11 s12 s1' s6' s11' s12');
  cut (lined s2 s7 s8 s13 s2' s7' s8' s13');
  cut (lined s3 s4 s9 s14 s3' s4' s9' s14');
  cut (lined sv0 sv5 sv10 sv15 sv0' sv5' sv10' sv15');
  cut (lined sv1 sv6 sv11 sv12 sv1' sv6' sv11' sv12');
  cut (lined sv2 sv7 sv8 sv13 sv2' sv7' sv8' sv13');
  cut (lined sv3 sv4 sv9 sv14 sv3' sv4' sv9' sv14');
  cut (sv' == V.diagonal_round sv);
  cut (s' == S.diagonal_round s)


val lemma_double_round_eq: s:state -> sv:vec_state{eq_states' s sv} -> Lemma
  (let s = S.double_round s in let sv = V.double_round sv in eq_states' s sv)
let lemma_double_round_eq s sv =
  let s' = S.column_round s in
  let s'' = S.diagonal_round s' in
  cut (s'' == S.double_round s);
  let sv' = V.column_round sv in
  let sv'' = V.diagonal_round sv' in
  cut (sv'' == V.double_round sv);
  lemma_column_round_eq s sv;
  cut (eq_states' s' sv');
  lemma_diagonal_round_eq s' sv'


val lemma_double_round_eq_: s:state -> sv:vec_state -> Lemma
  (requires (eq_states' s sv))
  (ensures (let s = S.double_round s in let sv = V.double_round sv in eq_states' s sv))
let lemma_double_round_eq_ s sv = lemma_double_round_eq s sv

val lemma_double_round_eq': s:state -> sv:vec_state -> Lemma
  (eq_states' s sv ==> (let s = S.double_round s in let sv = V.double_round sv in eq_states' s sv))
let lemma_double_round_eq' s sv =
  Classical.move_requires (lemma_double_round_eq_ s) sv

val lemma_double_round_eq_forall_1: s:state -> Lemma
  (forall sv. eq_states' s sv ==> eq_states' (S.double_round s) (V.double_round sv))
let lemma_double_round_eq_forall_1 s =
  let post (sv:vec_state) =
    eq_states' s sv ==> eq_states' (S.double_round s) (V.double_round sv) in
  FStar.Classical.forall_intro #_ #post (lemma_double_round_eq' s)

val lemma_double_round_eq_forall: unit -> Lemma
  (forall s sv. eq_states' s sv ==> eq_states' (S.double_round s) (V.double_round sv))
let lemma_double_round_eq_forall () =
  let post (s:state) =
    (forall sv. eq_states' s sv ==> eq_states' (S.double_round s) (V.double_round sv)) in
  FStar.Classical.forall_intro #_ #post lemma_double_round_eq_forall_1

#reset-options "--max_fuel 0 --z3rlimit 5"

val lemma_chacha_rounds_vec: s:state -> sv:vec_state{eq_states' s sv} -> Lemma
  (let s' = S.rounds s in let sv' = V.rounds sv in
   eq_states' s' sv')
let lemma_chacha_rounds_vec s sv =
  lemma_double_round_eq_forall ();
  lemma_iter_state s sv S.double_round V.double_round 10;
  cut (eq_states' (iter 10 S.double_round s) (iter 10 V.double_round sv));
  cut (S.rounds s == iter 10 S.double_round s);
  cut (V.rounds sv == iter 10 V.double_round sv)


val lemma_chacha_core_std: s:state -> s':state -> Lemma
  (let s'' = Spec.Loops.seq_map2 FStar.UInt32.op_Plus_Percent_Hat s' s in
  let s0 = index s 0 in   let s1 = index s 1 in
  let s2 = index s 2 in   let s3 = index s 3 in
  let s4 = index s 4 in   let s5 = index s 5 in
  let s6 = index s 6 in   let s7 = index s 7 in
  let s8 = index s 8 in   let s9 = index s 9 in
  let s10 = index s 10 in  let s11 = index s 11 in
  let s12 = index s 12 in  let s13 = index s 13 in
  let s14 = index s 14 in  let s15 = index s 15 in
  let s0' = index s' 0 in   let s1' = index s' 1 in
  let s2' = index s' 2 in   let s3' = index s' 3 in
  let s4' = index s' 4 in   let s5' = index s' 5 in
  let s6' = index s' 6 in   let s7' = index s' 7 in
  let s8' = index s' 8 in   let s9' = index s' 9 in
  let s10' = index s' 10 in  let s11' = index s' 11 in
  let s12' = index s' 12 in  let s13' = index s' 13 in
  let s14' = index s' 14 in  let s15' = index s' 15 in
  let s0'' = index s'' 0 in   let s1'' = index s'' 1 in
  let s2'' = index s'' 2 in   let s3'' = index s'' 3 in
  let s4'' = index s'' 4 in   let s5'' = index s'' 5 in
  let s6'' = index s'' 6 in   let s7'' = index s'' 7 in
  let s8'' = index s'' 8 in   let s9'' = index s'' 9 in
  let s10'' = index s'' 10 in  let s11'' = index s'' 11 in
  let s12'' = index s'' 12 in  let s13'' = index s'' 13 in
  let s14'' = index s'' 14 in  let s15'' = index s'' 15 in
  FStar.UInt32.(
  s0'' == s0' +%^ s0
  /\ s1'' == s1' +%^ s1
  /\ s2'' == s2' +%^ s2
  /\ s3'' == s3' +%^ s3
  /\ s4'' == s4' +%^ s4
  /\ s5'' == s5' +%^ s5
  /\ s6'' == s6' +%^ s6
  /\ s7'' == s7' +%^ s7
  /\ s8'' == s8' +%^ s8
  /\ s9'' == s9' +%^ s9
  /\ s10'' == s10' +%^ s10
  /\ s11'' == s11' +%^ s11
  /\ s12'' == s12' +%^ s12
  /\ s13'' == s13' +%^ s13
  /\ s14'' == s14' +%^ s14
  /\ s15'' == s15' +%^ s15))
#reset-options "--max_fuel 0 --z3rlimit 100"
let lemma_chacha_core_std s s' = ()

val lemma_chacha_core_vec: s:vec_state -> s':vec_state -> Lemma
  (let s'' = Spec.Loops.seq_map2 V.op_Plus_Percent_Hat s' s in
  let s0 = index (index s 0) 0 in   let s1 = index (index s 0) 1 in
  let s2 = index (index s 0) 2 in   let s3 = index (index s 0) 3 in
  let s4 = index (index s 1) 0 in   let s5 = index (index s 1) 1 in
  let s6 = index (index s 1) 2 in   let s7 = index (index s 1) 3 in
  let s8 = index (index s 2) 0 in   let s9 = index (index s 2) 1 in
  let s10 = index (index s 2) 2 in  let s11 = index (index s 2) 3 in
  let s12 = index (index s 3) 0 in  let s13 = index (index s 3) 1 in
  let s14 = index (index s 3) 2 in  let s15 = index (index s 3) 3 in
  let s0' = index (index s' 0) 0 in   let s1' = index (index s' 0) 1 in
  let s2' = index (index s' 0) 2 in   let s3' = index (index s' 0) 3 in
  let s4' = index (index s' 1) 0 in   let s5' = index (index s' 1) 1 in
  let s6' = index (index s' 1) 2 in   let s7' = index (index s' 1) 3 in
  let s8' = index (index s' 2) 0 in   let s9' = index (index s' 2) 1 in
  let s10' = index (index s' 2) 2 in  let s11' = index (index s' 2) 3 in
  let s12' = index (index s' 3) 0 in  let s13' = index (index s' 3) 1 in
  let s14' = index (index s' 3) 2 in  let s15' = index (index s' 3) 3 in
  let s0'' = index (index s'' 0) 0 in   let s1'' = index (index s'' 0) 1 in
  let s2'' = index (index s'' 0) 2 in   let s3'' = index (index s'' 0) 3 in
  let s4'' = index (index s'' 1) 0 in   let s5'' = index (index s'' 1) 1 in
  let s6'' = index (index s'' 1) 2 in   let s7'' = index (index s'' 1) 3 in
  let s8'' = index (index s'' 2) 0 in   let s9'' = index (index s'' 2) 1 in
  let s10'' = index (index s'' 2) 2 in  let s11'' = index (index s'' 2) 3 in
  let s12'' = index (index s'' 3) 0 in  let s13'' = index (index s'' 3) 1 in
  let s14'' = index (index s'' 3) 2 in  let s15'' = index (index s'' 3) 3 in
  FStar.UInt32.(
  s0'' == s0' +%^ s0
  /\ s1'' == s1' +%^ s1
  /\ s2'' == s2' +%^ s2
  /\ s3'' == s3' +%^ s3
  /\ s4'' == s4' +%^ s4
  /\ s5'' == s5' +%^ s5
  /\ s6'' == s6' +%^ s6
  /\ s7'' == s7' +%^ s7
  /\ s8'' == s8' +%^ s8
  /\ s9'' == s9' +%^ s9
  /\ s10'' == s10' +%^ s10
  /\ s11'' == s11' +%^ s11
  /\ s12'' == s12' +%^ s12
  /\ s13'' == s13' +%^ s13
  /\ s14'' == s14' +%^ s14
  /\ s15'' == s15' +%^ s15))
#reset-options "--max_fuel 0 --z3rlimit 100"
let lemma_chacha_core_vec s s' = ()

val lemma_chacha_core: s:state -> sv:vec_state{eq_states' s sv} -> Lemma
  (let s = S.chacha20_core s in let sv = V.chacha20_core sv in
   eq_states' s sv)
let lemma_chacha_core s sv =
  lemma_chacha_rounds_vec s sv;
  let s' = S.rounds s in
  let sv' = V.rounds sv in
  lemma_chacha_core_std s s'; lemma_chacha_core_vec sv sv'


private let lemma_append_assoc (#a:Type) (x:seq a) (y:seq a) (z:seq a) : Lemma
  (x @| (y @| z) == (x @| y) @| z) = lemma_eq_intro ((x @| y) @| z) (x @| (y @| z))


val lemma_chacha_block_slice: s:state -> Lemma
  (uint32s_to_le 16 s == uint32s_to_le 4 (slice s 0 4)
                         @| uint32s_to_le 4 (slice s 4  8)
                         @| uint32s_to_le 4 (slice s 8  12)
                         @| uint32s_to_le 4 (slice s 12 16))
#reset-options "--max_fuel 0 --z3rlimit 100"
let lemma_chacha_block_slice b =
  lemma_uint32s_to_le_slice 16 b 8;
  let b0 = slice b 0 8 in
  let b1 = slice b 8 16 in
  cut (uint32s_to_le 16 b == uint32s_to_le 8 b0 @| uint32s_to_le 8 b1);
  lemma_uint32s_to_le_slice 8 b0 4;
  lemma_uint32s_to_le_slice 8 b1 4;
  cut (uint32s_to_le 8 b0 == uint32s_to_le 4 (slice b0 0 4) @| uint32s_to_le 4 (slice b0 4 8));
  cut (uint32s_to_le 8 b1 == uint32s_to_le 4 (slice b1 0 4) @| uint32s_to_le 4 (slice b1 4 8));
  lemma_eq_intro (slice b0 0 4) (slice b 0 4);
  lemma_eq_intro (slice b0 4 8) (slice b 4 8);
  lemma_eq_intro (slice b1 0 4) (slice b 8 12);
  lemma_eq_intro (slice b1 4 8) (slice b 12 16);
  cut (uint32s_to_le 8 b0 == uint32s_to_le 4 (slice b 0 4) @| uint32s_to_le 4 (slice b 4 8));
  cut (uint32s_to_le 8 b1 == uint32s_to_le 4 (slice b 8 12) @| uint32s_to_le 4 (slice b 12 16));
  cut (uint32s_to_le 16 b == (uint32s_to_le 4 (slice b 0 4) @| uint32s_to_le 4 (slice b 4 8))
                             @| (uint32s_to_le 4 (slice b 8 12) @| uint32s_to_le 4 (slice b 12 16)));
  lemma_append_assoc (uint32s_to_le 4 (slice b 0 4) @| uint32s_to_le 4 (slice b 4 8))
                     (uint32s_to_le 4 (slice b 8 12)) (uint32s_to_le 4 (slice b 12 16));
  lemma_append_assoc (uint32s_to_le 4 (slice b 0 4)) (uint32s_to_le 4 (slice b 4 8))
                     (uint32s_to_le 4 (slice b 8 12) @| uint32s_to_le 4 (slice b 12 16))


val lemma_chacha20_block: k:key -> n:nonce -> c:counter ->
  Lemma (let b = S.chacha20_block k n c in let b' = V.chacha20_block k n c in  b == b')
let lemma_chacha20_block k n c =
  lemma_setup k n c;
  let s = S.setup k n c in
  let sv = V.setup k n c in
  cut (eq_states' s sv);
  lemma_chacha_core s sv;
  let s' = S.chacha20_core s in
  let sv' = V.chacha20_core sv in
  lemma_chacha_block_slice s';
  lemma_eq_states_intro s' sv';
  lemma_eq_intro (index sv' 0) (slice s' 0 4);
  lemma_eq_intro (index sv' 1) (slice s' 4 8);
  lemma_eq_intro (index sv' 2) (slice s' 8 12);
  lemma_eq_intro (index sv' 3) (slice s' 12 16);
  lemma_eq_intro (uint32s_to_le 4 (index sv' 0) @|  uint32s_to_le 4 (index sv' 1) @|  uint32s_to_le 4 (index sv' 2) @|  uint32s_to_le 4 (index sv' 3)) (uint32s_to_le 16 s')


val lemma_chacha20_counter_mode_blocks: k:key -> n:nonce -> c:counter -> m:bytes{c + 1 * (length m / 64) < pow2 32 /\
    length m % (64 * 1) = 0} -> Lemma
  (requires (True))
  (ensures (Spec.CTR.counter_mode_blocks S.chacha20_ctx S.chacha20_cipher k n c m ==
            Spec.CTR.counter_mode_blocks V.chacha20_ctx V.chacha20_cipher k n c m))
  (decreases (length m))
#reset-options "--initial_fuel 1 --max_fuel 1 --z3rlimit 50"
let rec lemma_chacha20_counter_mode_blocks k n c m =
  if length m = 0 then ()
  else (
    let len = length m in
    let len' = len / (64 * 1) in
    Math.Lemmas.lemma_div_mod len (64 * 1);
    let prefix, block = split m (len - 64 * 1) in    
      (* TODO: move to a single lemma for clarify *)
      Math.Lemmas.lemma_mod_plus (length prefix) 1 (64 * 1);
      Math.Lemmas.lemma_div_le (length prefix) len 64;
      Spec.CTR.Lemmas.lemma_div len (64 * 1);
      (* End TODO *)
    lemma_chacha20_counter_mode_blocks k n c prefix;
    lemma_chacha20_block k n ((c + (len / 64 - 1)) * 1)
  )
  

val lemma_chacha20_encrypt_bytes: k:key -> n:nonce -> c:counter -> m:bytes{c + length m / 64 < pow2 32} -> Lemma
  (requires (True))
  (ensures (V.chacha20_encrypt_bytes k n c m == S.chacha20_encrypt_bytes k n c m))
  (decreases (length m))
#reset-options "--max_fuel 0 --z3rlimit 100"
let rec lemma_chacha20_encrypt_bytes k n c m =
  let len = length m in
  let blocks_len = (1 * 64) * (len / (64 * 1)) in
  let part_len   = len % (64 * 1) in
  Math.Lemmas.lemma_div_mod len (64 * 1);
  Math.Lemmas.multiple_modulo_lemma (len / (64 * 1)) (64 * 1);
  Math.Lemmas.lemma_div_le (blocks_len) len 64;
  let blocks, last_block = split m blocks_len in
  lemma_chacha20_counter_mode_blocks k n c blocks;
  if part_len > 0
  then
    lemma_chacha20_block k n (c+1*(length m / 64))
  else ()