let sub_borrow_st (t:inttype{t = U32 \/ t = U64}) =
    cin:uint_t t SEC
  -> x:uint_t t SEC
  -> y:uint_t t SEC
  -> r:lbuffer (uint_t t SEC) (size 1) ->
  Stack (uint_t t SEC)
  (requires fun h -> live h r /\ v cin <= 1)
  (ensures  fun h0 c h1 ->
    modifies1 r h0 h1 /\ v c <= 1 /\
    (let r = Seq.index (as_seq h1 r) 0 in
    v r - v c * pow2 (bits t) == v x - v y - v cin))
let sub_borrow_st (t: inttype{t = U32 \/ t = U64}) =
cin: uint_t t SEC -> x: uint_t t SEC -> y: uint_t t SEC -> r: lbuffer (uint_t t SEC) (size 1)
  -> Stack (uint_t t SEC)
      (requires fun h -> live h r /\ v cin <= 1)
      (ensures
        fun h0 c h1 ->
          modifies1 r h0 h1 /\ v c <= 1 /\
          (let r = Seq.index (as_seq h1 r) 0 in
            v r - v c * pow2 (bits t) == v x - v y - v cin))
Hacl.IntTypes.Intrinsics.fst.checked
prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.IntTypes.Intrinsics.fst
Lib.IntTypes.inttype Prims.l_or Prims.b2t Prims.op_Equality Lib.IntTypes.U32 Lib.IntTypes.U64 Lib.IntTypes.uint_t Lib.IntTypes.SEC Lib.Buffer.lbuffer Lib.IntTypes.size FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.Buffer.modifies1 Prims.eq2 Prims.int Prims.op_Subtraction FStar.Mul.op_Star Prims.pow2 Lib.IntTypes.bits Lib.IntTypes.int_t FStar.Seq.Base.index Lib.Buffer.as_seq
module Hacl.IntTypes.Intrinsics

open FStar.HyperStack.All
open FStar.HyperStack
module ST = FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer

open FStar.Mul

#set-options "--fuel 0 --ifuel 0 --z3rlimit 100"

inline_for_extraction noextract
let add_carry_st (t:inttype{t = U32 \/ t = U64}) =
    cin:uint_t t SEC
  -> x:uint_t t SEC
  -> y:uint_t t SEC
  -> r:lbuffer (uint_t t SEC) (size 1) ->
  Stack (uint_t t SEC)
  (requires fun h -> live h r /\ v cin <= 1)
  (ensures  fun h0 c h1 ->
    modifies1 r h0 h1 /\ v c <= 1 /\
    (let r = Seq.index (as_seq h1 r) 0 in
    v r + v c * pow2 (bits t) == v x + v y + v cin))

val add_carry_u32: add_carry_st U32
let add_carry_u32 cin x y r =
  let res = to_u64 x +. to_u64 cin +. to_u64 y in
  let c = to_u32 (res >>. 32ul) in
  r.(0ul) <- to_u32 res;
  c

inline_for_extraction noextract
val sub_borrow_st : t: Lib.IntTypes.inttype{t = Lib.IntTypes.U32 \/ t = Lib.IntTypes.U64} -> Type0
t: Lib.IntTypes.inttype{t = Lib.IntTypes.U32 \/ t = Lib.IntTypes.U64} -> Type0