val bn_add1:
    #t:limb_t
  -> aLen:size_t{0 < v aLen}
  -> a:lbignum t aLen
  -> b1:limb t
  -> res:lbignum t aLen ->
  Stack (carry t)
  (requires fun h ->
    live h a /\ live h res /\ eq_or_disjoint a res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1 /\
    (let c, r = S.bn_add1 (as_seq h0 a) b1 in
    c_out == c /\ as_seq h1 res == r))
let bn_add1 #t aLen a b1 res =
  Hacl.Bignum.Addition.bn_add1 aLen a b1 res
val bn_add1:
    #t:limb_t
  -> aLen:size_t{0 < v aLen}
  -> a:lbignum t aLen
  -> b1:limb t
  -> res:lbignum t aLen ->
  Stack (carry t)
  (requires fun h ->
    live h a /\ live h res /\ eq_or_disjoint a res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1 /\
    (let c, r = S.bn_add1 (as_seq h0 a) b1 in
    c_out == c /\ as_seq h1 res == r))
let bn_add1 #t aLen a b1 res =
Hacl.Bignum.Addition.bn_add1 aLen a b1 res
Hacl.Bignum.fst.checked
prims.fst.checked LowStar.Ignore.fsti.checked Lib.ByteBuffer.fsti.checked Hacl.Spec.Bignum.fst.checked Hacl.Bignum.Multiplication.fst.checked Hacl.Bignum.Lib.fst.checked Hacl.Bignum.Karatsuba.fst.checked Hacl.Bignum.Convert.fst.checked Hacl.Bignum.Comparison.fst.checked Hacl.Bignum.Addition.fst.checked FStar.UInt32.fsti.checked FStar.ST.fst.checked FStar.Pervasives.fsti.checked
Hacl.Bignum.fst
Hacl.Bignum.Definitions.limb_t Lib.IntTypes.size_t Prims.b2t Prims.op_LessThan Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Bignum.Definitions.lbignum Hacl.Bignum.Definitions.limb Hacl.Bignum.Addition.bn_add1 Hacl.Spec.Bignum.Base.carry
module Hacl.Bignum

friend Hacl.Spec.Bignum

#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val bn_add1:
    #t:limb_t
  -> aLen:size_t{0 < v aLen}
  -> a:lbignum t aLen
  -> b1:limb t
  -> res:lbignum t aLen ->
  Stack (carry t)
  (requires fun h ->
    live h a /\ live h res /\ eq_or_disjoint a res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1 /\
    (let c, r = S.bn_add1 (as_seq h0 a) b1 in
    c_out == c /\ as_seq h1 res == r))

    aLen: Lib.IntTypes.size_t{0 < Lib.IntTypes.v aLen} ->
    a: Hacl.Bignum.Definitions.lbignum t aLen ->
    b1: Hacl.Bignum.Definitions.limb t ->
    res: Hacl.Bignum.Definitions.lbignum t aLen
  -> FStar.HyperStack.ST.Stack (Hacl.Spec.Bignum.Base.carry t)