val lemma_sub3
      (a:nat) (a0 a1 a2:nat64)
      (b:nat) (b0 b1 b2:nat64)
      (s1 s2 s3:nat64) (c:bit) : Lemma
  (requires a = pow2_three a0 a1 a2 /\
            b = pow2_three b0 b1 b2 /\
           (let s1', c1 = sub_carry a0 b0 0 in
            let s2', c2 = sub_carry a1 b1 c1 in
            let s3', c3 = sub_carry a2 b2 c2 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            c  == c3))
  (ensures a - b == pow2_three s1 s2 s3 - c * pow2_192)
let lemma_sub3
      (a:nat) (a0 a1 a2:nat64)
      (b:nat) (b0 b1 b2:nat64)
      (s1 s2 s3:nat64) (c:bit) : Lemma
  (requires a = pow2_three a0 a1 a2 /\
            b = pow2_three b0 b1 b2 /\
           (let s1', c1 = sub_carry a0 b0 0 in
            let s2', c2 = sub_carry a1 b1 c1 in
            let s3', c3 = sub_carry a2 b2 c2 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            c  == c3))
  (ensures a - b == pow2_three s1 s2 s3 - c * pow2_192)
  =
  assert_by_tactic (a - b == pow2int_three (a0 - b0) (a1 - b1) (a2 - b2)) int_canon;
  lemma_pow2_int_23 (a0 - b0) (a1 - b1) (a2 - b2);
  let a_two = pow2_two a0 a1 in
  let b_two = pow2_two b0 b1 in
  let a_minus_b_two = a_two - b_two in
  assert_by_tactic (a_minus_b_two == pow2int_two (a0 - b0) (a1 - b1)) int_canon;
  let s1', c1 = sub_carry a0 b0 0 in
  let s2', c2 = sub_carry a1 b1 c1 in
  let s3', c3 = sub_carry a2 b2 c2 in
  lemma_sub2 a_two a0 a1
             b_two b0 b1
             s1 s2 c2;
  assert_by_tactic ((a2 - b2 - c2) * pow2_128 == s3 * pow2_128 - c * pow2_192) int_canon;
  assert_by_tactic (pow2_two s1 s2 + s3 * pow2_128 == pow2_three s1 s2 s3) int_canon;
  ()
val lemma_sub3
      (a:nat) (a0 a1 a2:nat64)
      (b:nat) (b0 b1 b2:nat64)
      (s1 s2 s3:nat64) (c:bit) : Lemma
  (requires a = pow2_three a0 a1 a2 /\
            b = pow2_three b0 b1 b2 /\
           (let s1', c1 = sub_carry a0 b0 0 in
            let s2', c2 = sub_carry a1 b1 c1 in
            let s3', c3 = sub_carry a2 b2 c2 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            c  == c3))
  (ensures a - b == pow2_three s1 s2 s3 - c * pow2_192)
let lemma_sub3 (a: nat) (a0 a1 a2: nat64) (b: nat) (b0 b1 b2 s1 s2 s3: nat64) (c: bit)
    : Lemma
      (requires
        a = pow2_three a0 a1 a2 /\ b = pow2_three b0 b1 b2 /\
        (let s1', c1 = sub_carry a0 b0 0 in
          let s2', c2 = sub_carry a1 b1 c1 in
          let s3', c3 = sub_carry a2 b2 c2 in
          s1 == s1' /\ s2 == s2' /\ s3 == s3' /\ c == c3))
      (ensures a - b == pow2_three s1 s2 s3 - c * pow2_192) =
assert_by_tactic (a - b == pow2int_three (a0 - b0) (a1 - b1) (a2 - b2)) int_canon;
lemma_pow2_int_23 (a0 - b0) (a1 - b1) (a2 - b2);
let a_two = pow2_two a0 a1 in
let b_two = pow2_two b0 b1 in
let a_minus_b_two = a_two - b_two in
assert_by_tactic (a_minus_b_two == pow2int_two (a0 - b0) (a1 - b1)) int_canon;
let s1', c1 = sub_carry a0 b0 0 in
let s2', c2 = sub_carry a1 b1 c1 in
let s3', c3 = sub_carry a2 b2 c2 in
lemma_sub2 a_two a0 a1 b_two b0 b1 s1 s2 c2;
assert_by_tactic ((a2 - b2 - c2) * pow2_128 == s3 * pow2_128 - c * pow2_192) int_canon;
assert_by_tactic (pow2_two s1 s2 + s3 * pow2_128 == pow2_three s1 s2 s3) int_canon;
()
Vale.Curve25519.FastUtil_helpers.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.Fast_lemmas_internal.fsti.checked Vale.Curve25519.Fast_defs.fst.checked prims.fst.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Curve25519.FastUtil_helpers.fst
Prims.nat Vale.Def.Types_s.nat64 Vale.Curve25519.Fast_defs.bit Prims.unit FStar.Tactics.Effect.assert_by_tactic Prims.eq2 Prims.int Prims.op_Addition Vale.Curve25519.Fast_defs.pow2_two FStar.Mul.op_Star Vale.Def.Words_s.pow2_128 Vale.Curve25519.Fast_defs.pow2_three Vale.Curve25519.FastUtil_helpers.int_canon Prims.op_Subtraction Vale.Curve25519.Fast_defs.pow2_192 Vale.Curve25519.FastUtil_helpers.lemma_sub2 FStar.Pervasives.Native.tuple2 Vale.Def.Words_s.nat64 Vale.Curve25519.FastUtil_helpers.sub_carry Vale.Curve25519.FastUtil_helpers.pow2int_two Vale.Curve25519.FastUtil_helpers.lemma_pow2_int_23 Vale.Curve25519.FastUtil_helpers.pow2int_three Prims.l_and Prims.b2t Prims.op_Equality Prims.logical Prims.squash Prims.Nil FStar.Pervasives.pattern
module Vale.Curve25519.FastUtil_helpers

open Vale.Def.Words_s
open Vale.Def.Types_s
open FStar.Mul
open FStar.Tactics
open FStar.Tactics.CanonCommSemiring
open Vale.Curve25519.Fast_defs
open Vale.Curve25519.Fast_lemmas_internal

(*
let lemma_sub_carry_equiv (x y:nat64) (c:bit) :
  Lemma (let v, c' = sub_carry x y c in
         v == (x - (y + c)) % pow2_64 /\
         c' == bool_bit (x - (y+c) < 0))
  =
  ()

let lemma_sub_carry_equiv_forall () :
  Lemma (forall x y c . {:pattern (sub_carry x y c)}
         let v, c' = sub_carry x y c in
         v == (x - (y + c)) % pow2_64 /\
         c' == bool_bit (x - (y+c) < 0))
  =
  ()
*)

#reset-options "--using_facts_from '* -FStar.Tactics -FStar.Reflection' \
  --max_fuel 0 --max_ifuel 0 --z3rlimit 50"
let lemma_sub2
      (a:nat) (a0 a1:nat64)
      (b:nat) (b0 b1:nat64)
      (s1 s2:nat64) (c:bit) : Lemma
  (requires a = pow2_two a0 a1 /\
            b = pow2_two b0 b1 /\
           (let s1', c1 = sub_carry a0 b0 0 in
            let s2', c2 = sub_carry a1 b1 c1 in
            s1 == s1' /\
            s2 == s2' /\
            c  == c2))
  (ensures a - b == pow2_two s1 s2 - c * pow2_128)
  =
  ()

// Unclear why lemma_sub2 passes, lemma_sub3 sometimes passed, sometimes ran forever (before we added explicit help), but lemma_sub4 fails without explicit help

let pow2int_two (c0 c1:int) : int = c0 + c1 * pow2_64
let pow2int_three (c0 c1 c2:int) : int = c0 + c1 * pow2_64 + c2 * pow2_128
let pow2int_four (c0 c1 c2 c3:int) : int = c0 + c1 * pow2_64 + c2 * pow2_128 + c3 * pow2_192

let lemma_pow2_int_23 (c0 c1 c2:int) :
  Lemma (pow2int_three c0 c1 c2 == pow2int_two c0 c1 + c2 * pow2_128)
  =
  ()

let lemma_pow2_int_34 (c0 c1 c2 c3:int) :
  Lemma (pow2int_four c0 c1 c2 c3 == pow2int_three c0 c1 c2 + c3 * pow2_192)
  =
  ()

#reset-options "--z3rlimit 30 --max_fuel 0 --max_ifuel 0"
// Passes
let lemma_sub3
      (a:nat) (a0 a1 a2:nat64)
      (b:nat) (b0 b1 b2:nat64)
      (s1 s2 s3:nat64) (c:bit) : Lemma
  (requires a = pow2_three a0 a1 a2 /\
            b = pow2_three b0 b1 b2 /\
           (let s1', c1 = sub_carry a0 b0 0 in
            let s2', c2 = sub_carry a1 b1 c1 in
            let s3', c3 = sub_carry a2 b2 c2 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            c  == c3))
  (ensures a - b == pow2_three s1 s2 s3 - c * pow2_192)
val lemma_sub3
      (a:nat) (a0 a1 a2:nat64)
      (b:nat) (b0 b1 b2:nat64)
      (s1 s2 s3:nat64) (c:bit) : Lemma
  (requires a = pow2_three a0 a1 a2 /\
            b = pow2_three b0 b1 b2 /\
           (let s1', c1 = sub_carry a0 b0 0 in
            let s2', c2 = sub_carry a1 b1 c1 in
            let s3', c3 = sub_carry a2 b2 c2 in
            s1 == s1' /\
            s2 == s2' /\
            s3 == s3' /\
            c  == c3))
  (ensures a - b == pow2_three s1 s2 s3 - c * pow2_192)

    a: Prims.nat ->
    a0: Vale.Def.Types_s.nat64 ->
    a1: Vale.Def.Types_s.nat64 ->
    a2: Vale.Def.Types_s.nat64 ->
    b: Prims.nat ->
    b0: Vale.Def.Types_s.nat64 ->
    b1: Vale.Def.Types_s.nat64 ->
    b2: Vale.Def.Types_s.nat64 ->
    s1: Vale.Def.Types_s.nat64 ->
    s2: Vale.Def.Types_s.nat64 ->
    s3: Vale.Def.Types_s.nat64 ->
    c: Vale.Curve25519.Fast_defs.bit
  -> FStar.Pervasives.Lemma
      (requires
        a = Vale.Curve25519.Fast_defs.pow2_three a0 a1 a2 /\
        b = Vale.Curve25519.Fast_defs.pow2_three b0 b1 b2 /\
        (let _ = Vale.Curve25519.FastUtil_helpers.sub_carry a0 b0 0 in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ s1' c1 = _ in
            let _ = Vale.Curve25519.FastUtil_helpers.sub_carry a1 b1 c1 in
            (let FStar.Pervasives.Native.Mktuple2 #_ #_ s2' c2 = _ in
              let _ = Vale.Curve25519.FastUtil_helpers.sub_carry a2 b2 c2 in
              (let FStar.Pervasives.Native.Mktuple2 #_ #_ s3' c3 = _ in
                s1 == s1' /\ s2 == s2' /\ s3 == s3' /\ c == c3)
              <:
              Prims.logical)
            <:
            Prims.logical)
          <:
          Prims.logical))
      (ensures
        a - b ==
        Vale.Curve25519.Fast_defs.pow2_three s1 s2 s3 - c * Vale.Curve25519.Fast_defs.pow2_192)