let spec_l (a: keccak_alg)
  (len:size_nat{len < block_length a})
  (inp:Lib.Sequence.lseq uint8 len)
  (s:Lib.Sequence.lseq uint64 25) = s
let spec_l
      (a: keccak_alg)
      (len: size_nat{len < block_length a})
      (inp: Lib.Sequence.lseq uint8 len)
      (s: Lib.Sequence.lseq uint64 25)
     =
s
Hacl.Hash.SHA3.fst.checked
Spec.SHA3.fst.checked Spec.Hash.Incremental.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.SHA3.fst.checked Hacl.Impl.SHA3.fst.checked Hacl.Hash.PadFinish.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked
Hacl.Hash.SHA3.fst
Spec.Hash.Definitions.keccak_alg Lib.IntTypes.size_nat Prims.b2t Prims.op_LessThan Spec.Hash.Definitions.block_length Lib.Sequence.lseq Lib.IntTypes.uint8 Lib.IntTypes.uint64 Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC
module Hacl.Hash.SHA3

open Spec.Hash.Definitions
open Hacl.Hash.Definitions
open FStar.Mul

module B = LowStar.Buffer
module S = FStar.Seq
module ST = FStar.HyperStack.ST
open Lib.IntTypes

module LB = Lib.Buffer

friend Spec.Agile.Hash

#push-options "--fuel 0 --ifuel 0 --z3rlimit 20"

/// We name this function used in Lib.Sequence spec combinators to avoid Z3 reasoning on anonymous functions
inline_for_extraction noextract
let spec_l (a: keccak_alg)
  (len:size_nat{len < block_length a})
val spec_l : a: Spec.Hash.Definitions.keccak_alg ->
    len: Lib.IntTypes.size_nat{len < Spec.Hash.Definitions.block_length a} ->
    inp: Lib.Sequence.lseq Lib.IntTypes.uint8 len ->
    s: Lib.Sequence.lseq Lib.IntTypes.uint64 25
  -> Lib.Sequence.lseq (Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC) 25

    a: Spec.Hash.Definitions.keccak_alg ->
    len: Lib.IntTypes.size_nat{len < Spec.Hash.Definitions.block_length a} ->
    inp: Lib.Sequence.lseq Lib.IntTypes.uint8 len ->
    s: Lib.Sequence.lseq Lib.IntTypes.uint64 25
  -> Lib.Sequence.lseq (Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC) 25