val add_carry_u64: add_carry_st U64
let add_carry_u64 cin x y r =
  let res = to_u128 x +. to_u128 cin +. to_u128 y in
  let c = to_u64 (res >>. 64ul) in
  r.(0ul) <- to_u64 res;
  c
val add_carry_u64: add_carry_st U64
let add_carry_u64 cin x y r =
let res = to_u128 x +. to_u128 cin +. to_u128 y in
let c = to_u64 (res >>. 64ul) in
r.(0ul) <- to_u64 res;
c
Hacl.IntTypes.Intrinsics_128.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.IntTypes.Intrinsics.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked
Hacl.IntTypes.Intrinsics_128.fst
Lib.IntTypes.uint_t Lib.IntTypes.U64 Lib.IntTypes.SEC Lib.Buffer.lbuffer Lib.IntTypes.size Prims.unit Lib.Buffer.op_Array_Assignment FStar.UInt32.__uint_to_t Lib.IntTypes.to_u64 Lib.IntTypes.U128 Lib.IntTypes.int_t Lib.IntTypes.op_Greater_Greater_Dot Lib.IntTypes.op_Plus_Dot Lib.IntTypes.to_u128
module Hacl.IntTypes.Intrinsics_128

open Hacl.IntTypes.Intrinsics

open Lib.IntTypes
open Lib.Buffer

(* Versions of add_carry_u64 and sub_borrow_u64 that rely on uint128 *)

#set-options "--fuel 0 --ifuel 0 --z3rlimit 200"
val add_carry_u64: add_carry_st U64
Hacl.IntTypes.Intrinsics.add_carry_st Lib.IntTypes.U64