let load_felem5 ((s0,s1,s2,s3): felem4) : felem5 =
  let f0 = s0 &. mask52 in
  let f1 = (s0 >>. 52ul) |. ((s1 &. u64 0xffffffffff) <<. 12ul) in
  let f2 = (s1 >>. 40ul) |. ((s2 &. u64 0xfffffff) <<. 24ul) in
  let f3 = (s2 >>. 28ul) |. ((s3 &. u64 0xffff) <<. 36ul) in
  let f4 = s3 >>. 16ul in
  (f0,f1,f2,f3,f4)
let load_felem5 (s0, s1, s2, s3: felem4) : felem5 =
let f0 = s0 &. mask52 in
let f1 = (s0 >>. 52ul) |. ((s1 &. u64 0xffffffffff) <<. 12ul) in
let f2 = (s1 >>. 40ul) |. ((s2 &. u64 0xfffffff) <<. 24ul) in
let f3 = (s2 >>. 28ul) |. ((s3 &. u64 0xffff) <<. 36ul) in
let f4 = s3 >>. 16ul in
(f0, f1, f2, f3, f4)
Hacl.Spec.K256.Field52.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.RawIntTypes.fsti.checked Lib.IntTypes.fsti.checked Hacl.Spec.K256.Field52.Definitions.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Hacl.Spec.K256.Field52.fst
Hacl.Spec.K256.Field52.Definitions.felem4 Lib.IntTypes.uint64 FStar.Pervasives.Native.Mktuple5 Lib.IntTypes.int_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.IntTypes.op_Greater_Greater_Dot FStar.UInt32.__uint_to_t Lib.IntTypes.op_Bar_Dot Lib.IntTypes.op_Less_Less_Dot Lib.IntTypes.op_Amp_Dot Lib.IntTypes.u64 Hacl.Spec.K256.Field52.Definitions.mask52 Hacl.Spec.K256.Field52.Definitions.felem5
module Hacl.Spec.K256.Field52

open FStar.Mul
open Lib.IntTypes

module S = Spec.K256

include Hacl.Spec.K256.Field52.Definitions

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val load_felem5 : _: Hacl.Spec.K256.Field52.Definitions.felem4 -> Hacl.Spec.K256.Field52.Definitions.felem5
_: Hacl.Spec.K256.Field52.Definitions.felem4 -> Hacl.Spec.K256.Field52.Definitions.felem5