let rotate_idx = rotval U32
let rotate_idx =
rotval U32
Spec.MD5.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
Spec.MD5.fst
Lib.IntTypes.rotval Lib.IntTypes.U32
module Spec.MD5

(* Source: https://tools.ietf.org/html/rfc1321 *)

open Lib.IntTypes
open Spec.Hash.Definitions

(* Section 3.3 *)

inline_for_extraction
let init_as_list : list uint32 = [
  u32 0x67452301;
  u32 0xefcdab89;
  u32 0x98badcfe;
  u32 0x10325476;
]

let init : words_state MD5 = Seq.seq_of_list init_as_list

(* Section 3.4 *)

inline_for_extraction
let f (x y z: uint32) : Tot uint32 =
  (x &. y) |. ((~. x) &. z)

inline_for_extraction
let g (x y z: uint32) : Tot uint32 =
  (x &. z) |. (y &. (~. z))

inline_for_extraction
let h (x y z: uint32) : Tot uint32 =
  x ^. y ^. z

inline_for_extraction
let i (x y z: uint32) : Tot uint32 =
  y ^. (x |. ~. z)

(* Table T: specified in 3.4, defined in Appendix A.3, function MD5Transform *)

inline_for_extraction
let t_as_list : list uint32 = [
  u32 0xd76aa478;
  u32 0xe8c7b756;
  u32 0x242070db;
  u32 0xc1bdceee;
  u32 0xf57c0faf;
  u32 0x4787c62a;
  u32 0xa8304613;
  u32 0xfd469501;
  u32 0x698098d8;
  u32 0x8b44f7af;
  u32 0xffff5bb1;
  u32 0x895cd7be;
  u32 0x6b901122;
  u32 0xfd987193;
  u32 0xa679438e;
  u32 0x49b40821;

  u32 0xf61e2562;
  u32 0xc040b340;
  u32 0x265e5a51;
  u32 0xe9b6c7aa;
  u32 0xd62f105d;
  u32 0x02441453;
  u32 0xd8a1e681;
  u32 0xe7d3fbc8;
  u32 0x21e1cde6;
  u32 0xc33707d6;
  u32 0xf4d50d87;
  u32 0x455a14ed;
  u32 0xa9e3e905;
  u32 0xfcefa3f8;
  u32 0x676f02d9;
  u32 0x8d2a4c8a;

  u32 0xfffa3942;
  u32 0x8771f681;
  u32 0x6d9d6122;
  u32 0xfde5380c;
  u32 0xa4beea44;
  u32 0x4bdecfa9;
  u32 0xf6bb4b60;
  u32 0xbebfbc70;
  u32 0x289b7ec6;
  u32 0xeaa127fa;
  u32 0xd4ef3085;
  u32 0x4881d05;
  u32 0xd9d4d039;
  u32 0xe6db99e5;
  u32 0x1fa27cf8;
  u32 0xc4ac5665;

  u32 0xf4292244;
  u32 0x432aff97;
  u32 0xab9423a7;
  u32 0xfc93a039;
  u32 0x655b59c3;
  u32 0x8f0ccc92;
  u32 0xffeff47d;
  u32 0x85845dd1;
  u32 0x6fa87e4f;
  u32 0xfe2ce6e0;
  u32 0xa3014314;
  u32 0x4e0811a1;
  u32 0xf7537e82;
  u32 0xbd3af235;
  u32 0x2ad7d2bb;
  u32 0xeb86d391;
]

module L = FStar.List.Tot

let t : Seq.lseq uint32 64 =
  assert_norm (L.length t_as_list == 64);
  Seq.seq_of_list t_as_list

let abcd_idx = (n: nat { n < 4 } )

let abcd_t = Seq.lseq uint32 4

let x_idx = (n: nat { n < 16 } )
let x_t = Seq.lseq uint32 16

let t_idx = (n: nat { 1 <= n /\ n <= 64 } )
val rotate_idx : Type0
Type0