let bn_sub_st (t:limb_t) =
    aLen:size_t
  -> a:lbignum t aLen
  -> bLen:size_t{v bLen <= v aLen}
  -> b:lbignum t bLen
  -> res:lbignum t aLen ->
  Stack (carry t)
  (requires fun h ->
    live h a /\ live h b /\ live h res /\
    disjoint a b /\ eq_or_disjoint a res /\ disjoint b res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1 /\
   (c_out, as_seq h1 res) == S.bn_sub (as_seq h0 a) (as_seq h0 b))
let bn_sub_st (t: limb_t) =

    aLen: size_t ->
    a: lbignum t aLen ->
    bLen: size_t{v bLen <= v aLen} ->
    b: lbignum t bLen ->
    res: lbignum t aLen
  -> Stack (carry t)
      (requires
        fun h ->
          live h a /\ live h b /\ live h res /\ disjoint a b /\ eq_or_disjoint a res /\
          disjoint b res)
      (ensures
        fun h0 c_out h1 ->
          modifies (loc res) h0 h1 /\ (c_out, as_seq h1 res) == S.bn_sub (as_seq h0 a) (as_seq h0 b)
      )
Hacl.Bignum.fsti.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.Bignum.fsti.checked Hacl.Bignum.Definitions.fst.checked Hacl.Bignum.Base.fst.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.Bignum.fsti
Hacl.Bignum.Definitions.limb_t Lib.IntTypes.size_t Hacl.Bignum.Definitions.lbignum Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Spec.Bignum.Base.carry FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Hacl.Bignum.Definitions.limb Lib.Buffer.disjoint Lib.Buffer.eq_or_disjoint Lib.Buffer.modifies Lib.Buffer.loc Prims.eq2 FStar.Pervasives.Native.tuple2 Hacl.Spec.Bignum.Definitions.lbignum FStar.Pervasives.Native.Mktuple2 Lib.Buffer.as_seq Hacl.Spec.Bignum.bn_sub
module Hacl.Bignum

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer

open Hacl.Bignum.Base
open Hacl.Bignum.Definitions

module S = Hacl.Spec.Bignum
module ST = FStar.HyperStack.ST
module Loops = Lib.LoopCombinators


#reset-options "--z3rlimit 50 --fuel 0 --ifuel 0"

inline_for_extraction noextract
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))


inline_for_extraction noextract
val bn_sub1:
    #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_sub1 (as_seq h0 a) b1 in
    c_out == c /\ as_seq h1 res == r))


inline_for_extraction noextract
let bn_add_eq_len_st (t:limb_t) (len:size_t) =
     a:lbignum t len
  -> b:lbignum t len
  -> res:lbignum t len ->
  Stack (carry t)
  (requires fun h ->
    live h a /\ live h b /\ live h res /\
    eq_or_disjoint a b /\ eq_or_disjoint a res /\ eq_or_disjoint b res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1 /\
    (c_out, as_seq h1 res) == S.bn_add (as_seq h0 a) (as_seq h0 b))


inline_for_extraction noextract
val bn_add_eq_len: #t:limb_t -> len:size_t -> bn_add_eq_len_st t len


inline_for_extraction noextract
let bn_sub_eq_len_st (t:limb_t) (len:size_t) =
     a:lbignum t len
  -> b:lbignum t len
  -> res:lbignum t len ->
  Stack (carry t)
  (requires fun h ->
    live h a /\ live h b /\ live h res /\
    eq_or_disjoint a b /\ eq_or_disjoint a res /\ eq_or_disjoint b res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1 /\
   (c_out, as_seq h1 res) == S.bn_sub (as_seq h0 a) (as_seq h0 b))


inline_for_extraction noextract
val bn_sub_eq_len: #t:limb_t -> len:size_t -> bn_sub_eq_len_st t len


inline_for_extraction noextract
let bn_add_st (t:limb_t) =
    aLen:size_t
  -> a:lbignum t aLen
  -> bLen:size_t{v bLen <= v aLen}
  -> b:lbignum t bLen
  -> res:lbignum t aLen ->
  Stack (carry t)
  (requires fun h ->
    live h a /\ live h b /\ live h res /\
    disjoint a b /\ eq_or_disjoint a res /\ disjoint b res)
  (ensures  fun h0 c_out h1 -> modifies (loc res) h0 h1 /\
    (c_out, as_seq h1 res) == S.bn_add (as_seq h0 a) (as_seq h0 b))


inline_for_extraction noextract
val bn_add: #t:limb_t -> bn_add_st t


inline_for_extraction noextract
val bn_sub_st : t: Hacl.Bignum.Definitions.limb_t -> Type0
t: Hacl.Bignum.Definitions.limb_t -> Type0