val init_as_list:list uint32
let init_as_list : list uint32 = [
  u32 0x67452301;
  u32 0xefcdab89;
  u32 0x98badcfe;
  u32 0x10325476;
  u32 0xc3d2e1f0;
]
val init_as_list:list uint32
let init_as_list:list uint32 =
[u32 0x67452301; u32 0xefcdab89; u32 0x98badcfe; u32 0x10325476; u32 0xc3d2e1f0]
Spec.SHA1.fst.checked
Spec.Loops.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Spec.SHA1.fst
Prims.Cons Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.u32 Prims.Nil
module Spec.SHA1

open Lib.IntTypes
module H = Spec.Hash.Definitions
module Seq = FStar.Seq

open Spec.Hash.Definitions
(* Source: https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf *)

(* Section 5.3.1 *)
val init_as_list:list uint32
Prims.list (Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC)