val pow2int_four (c0 c1 c2 c3: int) : int
let pow2int_four (c0 c1 c2 c3:int) : int = c0 + c1 * pow2_64 + c2 * pow2_128 + c3 * pow2_192
val pow2int_four (c0 c1 c2 c3: int) : int
let pow2int_four (c0 c1 c2 c3: int) : int =
c0 + c1 * pow2_64 + c2 * pow2_128 + c3 * pow2_192
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.int Prims.op_Addition FStar.Mul.op_Star Vale.Def.Words_s.pow2_64 Vale.Def.Words_s.pow2_128 Vale.Curve25519.Fast_defs.pow2_192
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
val pow2int_four (c0 c1 c2 c3: int) : int
c0: Prims.int -> c1: Prims.int -> c2: Prims.int -> c3: Prims.int -> Prims.int