val sha256_8
  (dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 : lbuffer uint8 32ul)
  (input_len:size_t) (input0 input1 input2 input3 input4 input5 input6 input7 : lbuffer uint8 input_len) :
  Stack unit
  (requires fun h0 -> v input_len `less_than_max_input_length` SHA2_256 /\
    live8 h0 input0 input1 input2 input3 input4 input5 input6 input7 /\
    live8 h0 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 /\
    internally_disjoint8 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7)
  (ensures  fun h0 _ h1 ->
    modifies (loc dst0 |+| (loc dst1 |+| (loc dst2 |+| (loc dst3 |+| (loc dst4 |+| (loc dst5 |+| (loc dst6 |+| loc dst7))))))) h0 h1 /\
    as_seq h1 dst0 == Spec.hash SHA2_256 (as_seq h0 input0) /\
    as_seq h1 dst1 == Spec.hash SHA2_256 (as_seq h0 input1) /\
    as_seq h1 dst2 == Spec.hash SHA2_256 (as_seq h0 input2) /\
    as_seq h1 dst3 == Spec.hash SHA2_256 (as_seq h0 input3) /\
    as_seq h1 dst4 == Spec.hash SHA2_256 (as_seq h0 input4) /\
    as_seq h1 dst5 == Spec.hash SHA2_256 (as_seq h0 input5) /\
    as_seq h1 dst6 == Spec.hash SHA2_256 (as_seq h0 input6) /\
    as_seq h1 dst7 == Spec.hash SHA2_256 (as_seq h0 input7))
let sha256_8 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 input_len input0 input1 input2 input3 input4 input5 input6 input7 =
  let ib = ntup8 (input0,(input1,(input2,(input3,(input4,(input5,(input6,input7))))))) in
  let rb = ntup8 (dst0,(dst1,(dst2,(dst3,(dst4,(dst5,(dst6,dst7))))))) in
  let h0 = ST.get() in
  assert (live_multi h0 ib);
  assert (live_multi h0 rb);
  assert (internally_disjoint rb);
  loc_multi8 rb;
  hash #SHA2_256 #M256 sha256_init8 sha256_update_nblocks8 sha256_update_last8 sha256_finish8 rb input_len ib;
  let h1 = ST.get() in
  Hacl.Spec.SHA2.Equiv.hash_agile_lemma #SHA2_256 #M256 (v input_len) (as_seq_multi h0 ib);
  assert ((as_seq_multi h1 rb).(|0|) == as_seq h1 dst0);
  assert ((as_seq_multi h1 rb).(|1|) == as_seq h1 dst1);
  assert ((as_seq_multi h1 rb).(|2|) == as_seq h1 dst2);
  assert ((as_seq_multi h1 rb).(|3|) == as_seq h1 dst3);
  assert ((as_seq_multi h1 rb).(|4|) == as_seq h1 dst4);
  assert ((as_seq_multi h1 rb).(|5|) == as_seq h1 dst5);
  assert ((as_seq_multi h1 rb).(|6|) == as_seq h1 dst6);
  assert ((as_seq_multi h1 rb).(|7|) == as_seq h1 dst7)
val sha256_8
  (dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 : lbuffer uint8 32ul)
  (input_len:size_t) (input0 input1 input2 input3 input4 input5 input6 input7 : lbuffer uint8 input_len) :
  Stack unit
  (requires fun h0 -> v input_len `less_than_max_input_length` SHA2_256 /\
    live8 h0 input0 input1 input2 input3 input4 input5 input6 input7 /\
    live8 h0 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 /\
    internally_disjoint8 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7)
  (ensures  fun h0 _ h1 ->
    modifies (loc dst0 |+| (loc dst1 |+| (loc dst2 |+| (loc dst3 |+| (loc dst4 |+| (loc dst5 |+| (loc dst6 |+| loc dst7))))))) h0 h1 /\
    as_seq h1 dst0 == Spec.hash SHA2_256 (as_seq h0 input0) /\
    as_seq h1 dst1 == Spec.hash SHA2_256 (as_seq h0 input1) /\
    as_seq h1 dst2 == Spec.hash SHA2_256 (as_seq h0 input2) /\
    as_seq h1 dst3 == Spec.hash SHA2_256 (as_seq h0 input3) /\
    as_seq h1 dst4 == Spec.hash SHA2_256 (as_seq h0 input4) /\
    as_seq h1 dst5 == Spec.hash SHA2_256 (as_seq h0 input5) /\
    as_seq h1 dst6 == Spec.hash SHA2_256 (as_seq h0 input6) /\
    as_seq h1 dst7 == Spec.hash SHA2_256 (as_seq h0 input7))
let sha256_8
      dst0
      dst1
      dst2
      dst3
      dst4
      dst5
      dst6
      dst7
      input_len
      input0
      input1
      input2
      input3
      input4
      input5
      input6
      input7
     =
let ib = ntup8 (input0, (input1, (input2, (input3, (input4, (input5, (input6, input7))))))) in
let rb = ntup8 (dst0, (dst1, (dst2, (dst3, (dst4, (dst5, (dst6, dst7))))))) in
let h0 = ST.get () in
assert (live_multi h0 ib);
assert (live_multi h0 rb);
assert (internally_disjoint rb);
loc_multi8 rb;
hash #SHA2_256
  #M256
  sha256_init8
  sha256_update_nblocks8
  sha256_update_last8
  sha256_finish8
  rb
  input_len
  ib;
let h1 = ST.get () in
Hacl.Spec.SHA2.Equiv.hash_agile_lemma #SHA2_256 #M256 (v input_len) (as_seq_multi h0 ib);
assert ((as_seq_multi h1 rb).(| 0 |) == as_seq h1 dst0);
assert ((as_seq_multi h1 rb).(| 1 |) == as_seq h1 dst1);
assert ((as_seq_multi h1 rb).(| 2 |) == as_seq h1 dst2);
assert ((as_seq_multi h1 rb).(| 3 |) == as_seq h1 dst3);
assert ((as_seq_multi h1 rb).(| 4 |) == as_seq h1 dst4);
assert ((as_seq_multi h1 rb).(| 5 |) == as_seq h1 dst5);
assert ((as_seq_multi h1 rb).(| 6 |) == as_seq h1 dst6);
assert ((as_seq_multi h1 rb).(| 7 |) == as_seq h1 dst7)
Hacl.SHA2.Vec256.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.NTuple.fsti.checked Lib.MultiBuffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.SHA2.Vec.fst.checked Hacl.Spec.SHA2.Equiv.fst.checked Hacl.Impl.SHA2.Generic.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.SHA2.Vec256.fst
Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.size_t Prims._assert Prims.eq2 FStar.Seq.Base.seq Prims.l_or Prims.nat FStar.Seq.Base.length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Hash.Definitions.hash_len Spec.Hash.Definitions.SHA2_256 Lib.MultiBuffer.op_Lens_Access FStar.Seq.Properties.lseq Hacl.Spec.SHA2.Vec.lanes Hacl.Spec.SHA2.Vec.M256 Lib.MultiBuffer.as_seq_multi Lib.Buffer.as_seq Lib.Buffer.MUT Prims.unit Hacl.Spec.SHA2.Equiv.hash_agile_lemma FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Impl.SHA2.Generic.hash Hacl.SHA2.Vec256.sha256_init8 Hacl.SHA2.Vec256.sha256_update_nblocks8 Hacl.SHA2.Vec256.sha256_update_last8 Hacl.SHA2.Vec256.sha256_finish8 Lib.MultiBuffer.loc_multi8 Lib.MultiBuffer.internally_disjoint Lib.MultiBuffer.live_multi Lib.NTuple.ntuple Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.NTuple.ntup8 FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple2
module Hacl.SHA2.Vec256

open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.NTuple
open Lib.Buffer
open Lib.MultiBuffer

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

module ST = FStar.HyperStack.ST
module Spec = Spec.Agile.Hash
module SpecVec = Hacl.Spec.SHA2.Vec

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

[@CInline] private let sha224_init8 = init #SHA2_224 #M256
[@CInline] private let sha224_update8 = update #SHA2_224 #M256
[@CInline] private let sha224_update_nblocks8 = update_nblocks #SHA2_224 #M256 sha224_update8
[@CInline] private let sha224_update_last8 = update_last #SHA2_224 #M256 sha224_update8
[@CInline] private let sha224_finish8 = finish #SHA2_224 #M256


val sha224_8
  (dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 : lbuffer uint8 28ul)
  (input_len:size_t) (input0 input1 input2 input3 input4 input5 input6 input7 : lbuffer uint8 input_len) :
  Stack unit
  (requires fun h0 -> v input_len `less_than_max_input_length` SHA2_224 /\
    live8 h0 input0 input1 input2 input3 input4 input5 input6 input7 /\
    live8 h0 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 /\
    internally_disjoint8 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7)
  (ensures  fun h0 _ h1 ->
    modifies (loc dst0 |+| (loc dst1 |+| (loc dst2 |+| (loc dst3 |+| (loc dst4 |+| (loc dst5 |+| (loc dst6 |+| loc dst7))))))) h0 h1 /\
    as_seq h1 dst0 == Spec.hash SHA2_224 (as_seq h0 input0) /\
    as_seq h1 dst1 == Spec.hash SHA2_224 (as_seq h0 input1) /\
    as_seq h1 dst2 == Spec.hash SHA2_224 (as_seq h0 input2) /\
    as_seq h1 dst3 == Spec.hash SHA2_224 (as_seq h0 input3) /\
    as_seq h1 dst4 == Spec.hash SHA2_224 (as_seq h0 input4) /\
    as_seq h1 dst5 == Spec.hash SHA2_224 (as_seq h0 input5) /\
    as_seq h1 dst6 == Spec.hash SHA2_224 (as_seq h0 input6) /\
    as_seq h1 dst7 == Spec.hash SHA2_224 (as_seq h0 input7))

let sha224_8 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 input_len input0 input1 input2 input3 input4 input5 input6 input7 =
  let ib = ntup8 (input0,(input1,(input2,(input3,(input4,(input5,(input6,input7))))))) in
  let rb = ntup8 (dst0,(dst1,(dst2,(dst3,(dst4,(dst5,(dst6,dst7))))))) in
  let h0 = ST.get() in
  assert (live_multi h0 ib);
  assert (live_multi h0 rb);
  assert (internally_disjoint rb);
  loc_multi8 rb;
  hash #SHA2_224 #M256 sha224_init8 sha224_update_nblocks8 sha224_update_last8 sha224_finish8 rb input_len ib;
  let h1 = ST.get() in
  Hacl.Spec.SHA2.Equiv.hash_agile_lemma #SHA2_224 #M256 (v input_len) (as_seq_multi h0 ib);
  assert ((as_seq_multi h1 rb).(|0|) == as_seq h1 dst0);
  assert ((as_seq_multi h1 rb).(|1|) == as_seq h1 dst1);
  assert ((as_seq_multi h1 rb).(|2|) == as_seq h1 dst2);
  assert ((as_seq_multi h1 rb).(|3|) == as_seq h1 dst3);
  assert ((as_seq_multi h1 rb).(|4|) == as_seq h1 dst4);
  assert ((as_seq_multi h1 rb).(|5|) == as_seq h1 dst5);
  assert ((as_seq_multi h1 rb).(|6|) == as_seq h1 dst6);
  assert ((as_seq_multi h1 rb).(|7|) == as_seq h1 dst7)



[@CInline] private let sha256_init8 = init #SHA2_256 #M256
[@CInline] private let sha256_update8 = update #SHA2_256 #M256
[@CInline] private let sha256_update_nblocks8 = update_nblocks #SHA2_256 #M256 sha256_update8
[@CInline] private let sha256_update_last8 = update_last #SHA2_256 #M256 sha256_update8
[@CInline] private let sha256_finish8 = finish #SHA2_256 #M256


val sha256_8
  (dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 : lbuffer uint8 32ul)
  (input_len:size_t) (input0 input1 input2 input3 input4 input5 input6 input7 : lbuffer uint8 input_len) :
  Stack unit
  (requires fun h0 -> v input_len `less_than_max_input_length` SHA2_256 /\
    live8 h0 input0 input1 input2 input3 input4 input5 input6 input7 /\
    live8 h0 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 /\
    internally_disjoint8 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7)
  (ensures  fun h0 _ h1 ->
    modifies (loc dst0 |+| (loc dst1 |+| (loc dst2 |+| (loc dst3 |+| (loc dst4 |+| (loc dst5 |+| (loc dst6 |+| loc dst7))))))) h0 h1 /\
    as_seq h1 dst0 == Spec.hash SHA2_256 (as_seq h0 input0) /\
    as_seq h1 dst1 == Spec.hash SHA2_256 (as_seq h0 input1) /\
    as_seq h1 dst2 == Spec.hash SHA2_256 (as_seq h0 input2) /\
    as_seq h1 dst3 == Spec.hash SHA2_256 (as_seq h0 input3) /\
    as_seq h1 dst4 == Spec.hash SHA2_256 (as_seq h0 input4) /\
    as_seq h1 dst5 == Spec.hash SHA2_256 (as_seq h0 input5) /\
    as_seq h1 dst6 == Spec.hash SHA2_256 (as_seq h0 input6) /\
    as_seq h1 dst7 == Spec.hash SHA2_256 (as_seq h0 input7))
val sha256_8
  (dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 : lbuffer uint8 32ul)
  (input_len:size_t) (input0 input1 input2 input3 input4 input5 input6 input7 : lbuffer uint8 input_len) :
  Stack unit
  (requires fun h0 -> v input_len `less_than_max_input_length` SHA2_256 /\
    live8 h0 input0 input1 input2 input3 input4 input5 input6 input7 /\
    live8 h0 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7 /\
    internally_disjoint8 dst0 dst1 dst2 dst3 dst4 dst5 dst6 dst7)
  (ensures  fun h0 _ h1 ->
    modifies (loc dst0 |+| (loc dst1 |+| (loc dst2 |+| (loc dst3 |+| (loc dst4 |+| (loc dst5 |+| (loc dst6 |+| loc dst7))))))) h0 h1 /\
    as_seq h1 dst0 == Spec.hash SHA2_256 (as_seq h0 input0) /\
    as_seq h1 dst1 == Spec.hash SHA2_256 (as_seq h0 input1) /\
    as_seq h1 dst2 == Spec.hash SHA2_256 (as_seq h0 input2) /\
    as_seq h1 dst3 == Spec.hash SHA2_256 (as_seq h0 input3) /\
    as_seq h1 dst4 == Spec.hash SHA2_256 (as_seq h0 input4) /\
    as_seq h1 dst5 == Spec.hash SHA2_256 (as_seq h0 input5) /\
    as_seq h1 dst6 == Spec.hash SHA2_256 (as_seq h0 input6) /\
    as_seq h1 dst7 == Spec.hash SHA2_256 (as_seq h0 input7))

    dst0: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    dst1: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    dst2: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    dst3: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    dst4: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    dst5: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    dst6: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    dst7: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    input_len: Lib.IntTypes.size_t ->
    input0: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input1: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input2: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input3: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input4: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input5: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input6: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len ->
    input7: Lib.Buffer.lbuffer Lib.IntTypes.uint8 input_len
  -> FStar.HyperStack.ST.Stack Prims.unit