Lib.IntTypes.Intrinsics.fsti
module Lib.IntTypes.Intrinsics
open FStar.HyperStack
open FStar.HyperStack.All
open Lib.IntTypes
open Lib.Buffer
open FStar.Mul
noextract
val add_carry_u64: cin:uint64 -> x:uint64 -> y:uint64 -> r:lbuffer uint64 (size 1) ->
Stack uint64
(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 64 == v x + v y + v cin))
noextract
val sub_borrow_u64: cin:uint64 -> x:uint64 -> y:uint64 -> r:lbuffer uint64 (size 1) ->
Stack uint64
(requires fun h -> live h r /\ v cin <= 1)
(ensures fun h0 c h1 ->
modifies1 r h0 h1 /\
(let r = Seq.index (as_seq h1 r) 0 in
v r - v c * pow2 64 == v x - v y - v cin))