val f (x y z: uint32) : Tot uint32
let f (x y z: uint32) : Tot uint32 =
  (x &. y) |. ((~. x) &. z)
val f (x y z: uint32) : Tot uint32
let f (x y z: uint32) : Tot uint32 =
(x &. y) |. ((~.x) &. z)
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.uint32 Lib.IntTypes.op_Bar_Dot Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.op_Amp_Dot Lib.IntTypes.op_Tilde_Dot
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
val f (x y z: uint32) : Tot uint32
x: Lib.IntTypes.uint32 -> y: Lib.IntTypes.uint32 -> z: Lib.IntTypes.uint32 -> Lib.IntTypes.uint32