val lemma_seq_scale_carry1 (a: natN 1) (bs: seq (natN 1)) (d: natN 1) (i: nat)
    : Lemma (requires i <= length bs + 1)
      (ensures (seq_add_c (seq_scale_lo a bs) (seq_scale_hi a bs d) 0 i == 0))
let rec lemma_seq_scale_carry1 (a:natN 1) (bs:seq (natN 1)) (d:natN 1) (i:nat) : Lemma
  (requires i <= length bs + 1)
  (ensures (
    seq_add_c (seq_scale_lo a bs) (seq_scale_hi a bs d) 0 i == 0
  ))
  =
  reveal_add_hi_all ();
  if i > 0 then lemma_seq_scale_carry1 a bs d (i - 1)
val lemma_seq_scale_carry1 (a: natN 1) (bs: seq (natN 1)) (d: natN 1) (i: nat)
    : Lemma (requires i <= length bs + 1)
      (ensures (seq_add_c (seq_scale_lo a bs) (seq_scale_hi a bs d) 0 i == 0))
let rec lemma_seq_scale_carry1 (a: natN 1) (bs: seq (natN 1)) (d: natN 1) (i: nat)
    : Lemma (requires i <= length bs + 1)
      (ensures (seq_add_c (seq_scale_lo a bs) (seq_scale_hi a bs d) 0 i == 0)) =
reveal_add_hi_all ();
if i > 0 then lemma_seq_scale_carry1 a bs d (i - 1)
Vale.Bignum.Lemmas.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Calc.fsti.checked
Vale.Bignum.Lemmas.fst
Vale.Def.Words_s.natN FStar.Seq.Base.seq Prims.nat Prims.op_GreaterThan Vale.Bignum.Lemmas.lemma_seq_scale_carry1 Prims.op_Subtraction Prims.bool Prims.unit Vale.Bignum.Defs.reveal_add_hi_all Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition FStar.Seq.Base.length Prims.squash Prims.eq2 Prims.int Vale.Bignum.Lemmas.seq_add_c Vale.Bignum.Lemmas.seq_scale_lo Vale.Bignum.Lemmas.seq_scale_hi Prims.Nil FStar.Pervasives.pattern
module Vale.Bignum.Lemmas
open FStar.Mul

let rec lemma_sum_seq_left_right_rec (s:seq int) (i j k:nat) : Lemma
  (requires i <= j /\ j <= k /\ k <= length s)
  (ensures sum_seq_left s i j + sum_seq_right s j k == sum_seq_right s i k)
  (decreases j)
  =
  if i < j then lemma_sum_seq_left_right_rec s i (j - 1) k

let lemma_sum_seq_left_right s i j =
  lemma_sum_seq_left_right_rec s i j j

let rec lemma_pow_nat a b =
  if b > 0 then (
    lemma_pow_nat a (b - 1);
    FStar.Math.Lemmas.nat_times_nat_is_nat a (pow_int a (b - 1))
  )

let rec lemma_sum_pow_seq_bound_rec (#n:nat) (s:seq (natN n)) (i:nat{i <= length s}) : Lemma
  (ensures 0 <= sum_pow_seq_left s i /\ sum_pow_seq_left s i < pow_int n i)
  =
  let open FStar.Math.Lemmas in
  if i > 0 then (
    calc (<=) {
      0;
      <= {lemma_sum_pow_seq_bound_rec s (i - 1)}
      sum_pow_seq_left s (i - 1);
      <= {lemma_pow_nat n (i - 1); nat_times_nat_is_nat s.[i - 1] (pow_int n (i - 1))}
      s.[i - 1] * pow_int n (i - 1) + sum_seq_left (pow_seq s) 0 (i - 1);
      == {}
      sum_pow_seq_left s i;
    };
    calc (<=) {
      sum_pow_seq_left s i + 1;
      == {}
      s.[i - 1] * pow_int n (i - 1) + sum_seq_left (pow_seq s) 0 (i - 1) + 1;
      <= {lemma_sum_pow_seq_bound_rec s (i - 1)}
      s.[i - 1] * pow_int n (i - 1) + pow_int n (i - 1);
      <= {lemma_pow_nat n (i - 1); lemma_mult_le_right (pow_int n (i - 1)) s.[i - 1] (n - 1)}
      (n - 1) * pow_int n (i - 1) + pow_int n (i - 1);
      == {}
      pow_int n i;
    }
  )

let lemma_sum_pow_seq_bound #n s =
  lemma_sum_pow_seq_bound_rec s (length s)

let lemma_seq_add_is_norm #n as0 bs c0 i =
  ()

#push-options "--z3cliopt smt.arith.nl=true"
#restart-solver
let lemma_last_carry_mul a b c =
  ()
#pop-options

#push-options "--z3cliopt smt.arith.nl=true"
#restart-solver
let lemma_add_lo_mul_right #n a b c m =
  reveal_add_lo_all ()
#pop-options

let rec lemma_seq_add_rec (#n:nat) (as0 bs:seq (natN n)) (c0:nat1) (i:nat) : Lemma
  (requires i <= length as0 /\ length bs == length as0)
  (ensures (
    let xs = fst (seq_add as0 bs c0) in
    let ci = seq_add_c as0 bs c0 i in
    sum_pow_seq_left xs i + last_carry n i ci == sum_pow_seq_left as0 i + sum_pow_seq_left bs i + c0
  ))
  (decreases i)
  =
  if (i > 0) then (
    let xs = fst (seq_add as0 bs c0) in
    let ci = seq_add_c as0 bs c0 i in
    let i' = i - 1 in
    let ci' = seq_add_c as0 bs c0 i' in
    calc (==) {
      sum_pow_seq_left xs i + last_carry n i ci;
      == {}
      xs.[i'] * pow_int n i' + sum_pow_seq_left xs i' + last_carry n i ci;
      == {lemma_seq_add_rec as0 bs c0 i'}
      xs.[i'] * pow_int n i' + sum_pow_seq_left as0 i' + sum_pow_seq_left bs i' + c0 - last_carry n i' ci' + last_carry n i ci;
      == {
        reveal_add_hi_all ();
        lemma_last_carry_mul n i' ci';
        lemma_add_lo_mul_right as0.[i'] bs.[i'] ci' (pow_int n i')
      }
      sum_pow_seq_left as0 i + sum_pow_seq_left bs i + c0;
    }
  )

let lemma_seq_add #n as0 bs c0 =
  lemma_seq_add_rec as0 bs c0 (length as0)

#push-options "--z3rlimit 100 --z3cliopt smt.arith.nl=true --max_ifuel 0"
#restart-solver
let rec lemma_seq_scale_rec (#n:nat) (a:natN n) (bs:seq (natN n)) (d:natN n) (i:nat) : Lemma
  (requires i <= length bs)
  (ensures (
    a * sum_pow_seq_left bs i + d ==
      sum_pow_seq_left (seq_scale_lo a bs) i + sum_pow_seq_left (seq_scale_hi a bs d) (i + 1)
  ))
  (decreases i)
  =
  reveal_mul_lo_all ();
  reveal_mul_hi_all ();
  if i = 0 then (
    assert (sum_pow_seq_left (seq_scale_hi a bs d) 0 == 0);
    assert (sum_pow_seq_left (seq_scale_hi a bs d) 1 == d)
  ) else (
    lemma_seq_scale_rec a bs d (i - 1)
  )
#pop-options

let rec lemma_seq_scale_carry1 (a:natN 1) (bs:seq (natN 1)) (d:natN 1) (i:nat) : Lemma
  (requires i <= length bs + 1)
  (ensures (
    seq_add_c (seq_scale_lo a bs) (seq_scale_hi a bs d) 0 i == 0
  ))
val lemma_seq_scale_carry1 (a: natN 1) (bs: seq (natN 1)) (d: natN 1) (i: nat)
    : Lemma (requires i <= length bs + 1)
      (ensures (seq_add_c (seq_scale_lo a bs) (seq_scale_hi a bs d) 0 i == 0))

    a: Vale.Def.Words_s.natN 1 ->
    bs: FStar.Seq.Base.seq (Vale.Def.Words_s.natN 1) ->
    d: Vale.Def.Words_s.natN 1 ->
    i: Prims.nat
  -> FStar.Pervasives.Lemma (requires i <= FStar.Seq.Base.length bs + 1)
      (ensures
        Vale.Bignum.Lemmas.seq_add_c (Vale.Bignum.Lemmas.seq_scale_lo a bs)
          (Vale.Bignum.Lemmas.seq_scale_hi a bs d)
          0
          i ==
        0)