val yy_mp_bzz3 (zz yy tmp1 yy_m_bzz3 yy_p_bzz3:felem) : Stack unit
  (requires fun h ->
    live h zz /\ live h yy /\ live h tmp1 /\
    live h yy_m_bzz3 /\ live h yy_p_bzz3 /\
    disjoint zz yy /\ disjoint zz tmp1 /\ disjoint zz yy_m_bzz3 /\
    disjoint zz yy_p_bzz3 /\ disjoint yy tmp1 /\ disjoint yy yy_m_bzz3 /\
    disjoint yy yy_p_bzz3 /\ disjoint tmp1 yy_m_bzz3 /\
    disjoint tmp1 yy_p_bzz3 /\ disjoint yy_m_bzz3 yy_p_bzz3 /\

    inv_lazy_reduced2 h zz /\ inv_lazy_reduced2 h yy)
  (ensures  fun h0 _ h1 ->
    modifies (loc tmp1 |+| loc yy_m_bzz3 |+| loc yy_p_bzz3) h0 h1 /\
    (let bzz3 = S.fmul (S.fmul 3 S.b) (feval h0 zz) in
    feval h1 yy_m_bzz3 = S.fsub (feval h0 yy) bzz3 /\
    feval h1 yy_p_bzz3 = S.fadd (feval h0 yy) bzz3 /\
    felem_fits5 (as_felem5 h1 yy_m_bzz3) (5,5,5,5,6) /\
    felem_fits5 (as_felem5 h1 yy_p_bzz3) (2,2,2,2,4)))
let yy_mp_bzz3 zz yy tmp1 yy_m_bzz3 yy_p_bzz3 =
  fmul_3b_normalize_weak tmp1 zz; //tmp1 = bzz3 = (3*b)*zz
  let h1 = ST.get () in
  // assert (felem_fits5 (as_felem5 h1 tmp1) (1,1,1,1,2));

  fsub yy_m_bzz3 yy tmp1 (u64 2); //yy_m_bzz3 = yy-bzz3
  let h2 = ST.get () in
  BL.fsub5_lemma (1,1,1,1,2) (1,1,1,1,2) (as_felem5 h1 yy) (as_felem5 h1 tmp1) (u64 2);
  // assert (felem_fits5 (as_felem5 h5 yy_m_bzz3) (5,5,5,5,6));

  fadd yy_p_bzz3 yy tmp1; //yy_p_bzz3 = yy+bzz3
  let h3 = ST.get () in
  BL.fadd5_lemma (1,1,1,1,2) (1,1,1,1,2) (as_felem5 h1 yy) (as_felem5 h1 tmp1)
val yy_mp_bzz3 (zz yy tmp1 yy_m_bzz3 yy_p_bzz3:felem) : Stack unit
  (requires fun h ->
    live h zz /\ live h yy /\ live h tmp1 /\
    live h yy_m_bzz3 /\ live h yy_p_bzz3 /\
    disjoint zz yy /\ disjoint zz tmp1 /\ disjoint zz yy_m_bzz3 /\
    disjoint zz yy_p_bzz3 /\ disjoint yy tmp1 /\ disjoint yy yy_m_bzz3 /\
    disjoint yy yy_p_bzz3 /\ disjoint tmp1 yy_m_bzz3 /\
    disjoint tmp1 yy_p_bzz3 /\ disjoint yy_m_bzz3 yy_p_bzz3 /\

    inv_lazy_reduced2 h zz /\ inv_lazy_reduced2 h yy)
  (ensures  fun h0 _ h1 ->
    modifies (loc tmp1 |+| loc yy_m_bzz3 |+| loc yy_p_bzz3) h0 h1 /\
    (let bzz3 = S.fmul (S.fmul 3 S.b) (feval h0 zz) in
    feval h1 yy_m_bzz3 = S.fsub (feval h0 yy) bzz3 /\
    feval h1 yy_p_bzz3 = S.fadd (feval h0 yy) bzz3 /\
    felem_fits5 (as_felem5 h1 yy_m_bzz3) (5,5,5,5,6) /\
    felem_fits5 (as_felem5 h1 yy_p_bzz3) (2,2,2,2,4)))
let yy_mp_bzz3 zz yy tmp1 yy_m_bzz3 yy_p_bzz3 =
fmul_3b_normalize_weak tmp1 zz;
let h1 = ST.get () in
fsub yy_m_bzz3 yy tmp1 (u64 2);
let h2 = ST.get () in
BL.fsub5_lemma (1, 1, 1, 1, 2) (1, 1, 1, 1, 2) (as_felem5 h1 yy) (as_felem5 h1 tmp1) (u64 2);
fadd yy_p_bzz3 yy tmp1;
let h3 = ST.get () in
BL.fadd5_lemma (1, 1, 1, 1, 2) (1, 1, 1, 1, 2) (as_felem5 h1 yy) (as_felem5 h1 tmp1)
Hacl.Impl.K256.PointAdd.fst.checked
Spec.K256.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.K256.Field52.Lemmas.fsti.checked Hacl.K256.Field.fsti.checked Hacl.Impl.K256.Point.fsti.checked FStar.UInt32.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.Impl.K256.PointAdd.fst
Hacl.K256.Field.felem Hacl.Spec.K256.Field52.Lemmas.fadd5_lemma FStar.Pervasives.Native.Mktuple5 Prims.nat Hacl.K256.Field.as_felem5 Prims.unit FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.K256.Field.fadd Hacl.Spec.K256.Field52.Lemmas.fsub5_lemma Lib.IntTypes.u64 Hacl.K256.Field.fsub Hacl.K256.Field.fmul_3b_normalize_weak
module Hacl.Impl.K256.PointAdd

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

open Lib.IntTypes
open Lib.Buffer

module ST = FStar.HyperStack.ST

module S = Spec.K256
module BL = Hacl.Spec.K256.Field52.Lemmas

open Hacl.K256.Field
open Hacl.Impl.K256.Point

#set-options "--z3rlimit 100 --fuel 0 --ifuel 0"

inline_for_extraction noextract
val point_add_xy_pairs (x1 y1 x2 y2 xx yy tmp xy_pairs:felem) : Stack unit
  (requires fun h ->
    live h x1 /\ live h y1 /\ live h x2 /\ live h y2 /\
    live h xx /\ live h yy /\ live h tmp /\ live h xy_pairs /\
    eq_or_disjoint x1 y1 /\ eq_or_disjoint x2 y2 /\ eq_or_disjoint xx yy /\
    disjoint x1 xy_pairs /\ disjoint y1 xy_pairs /\ disjoint x2 xy_pairs /\ disjoint y2 xy_pairs /\
    disjoint x1 tmp /\ disjoint y1 tmp /\ disjoint x2 tmp /\ disjoint y2 tmp /\
    disjoint xx xy_pairs /\ disjoint yy xy_pairs /\ disjoint xx tmp /\ disjoint yy tmp /\
    disjoint xy_pairs tmp /\

    inv_lazy_reduced2 h x1 /\ inv_lazy_reduced2 h y1 /\ inv_lazy_reduced2 h x2 /\ inv_lazy_reduced2 h y2 /\
    inv_lazy_reduced2 h xx /\ inv_lazy_reduced2 h yy)
  (ensures  fun h0 _ h1 -> modifies (loc xy_pairs |+| loc tmp) h0 h1 /\
    feval h1 xy_pairs =
      S.fsub
	(S.fmul (S.fadd (feval h0 x1) (feval h0 y1)) (S.fadd (feval h0 x2) (feval h0 y2)))
	(S.fadd (feval h0 xx) (feval h0 yy)) /\
    felem_fits5 (as_felem5 h1 xy_pairs) (9,9,9,9,10))

let point_add_xy_pairs x1 y1 x2 y2 xx yy tmp xy_pairs =
  let h0 = ST.get () in
  BL.fadd5_lemma (1,1,1,1,2) (1,1,1,1,2) (as_felem5 h0 x1) (as_felem5 h0 y1);
  BL.fadd5_lemma (1,1,1,1,2) (1,1,1,1,2) (as_felem5 h0 x2) (as_felem5 h0 y2);
  fadd xy_pairs x1 y1;
  fadd tmp x2 y2;
  let h1 = ST.get () in
  assert (felem_fits5 (as_felem5 h1 xy_pairs) (2,2,2,2,4));
  assert (felem_fits5 (as_felem5 h1 tmp) (2,2,2,2,4));
  fmul xy_pairs xy_pairs tmp;
  let h2 = ST.get () in
  assert (felem_fits5 (as_felem5 h2 xy_pairs) (1,1,1,1,2));
  BL.fadd5_lemma (1,1,1,1,2) (1,1,1,1,2) (as_felem5 h2 xx) (as_felem5 h2 yy);
  fadd tmp xx yy;
  let h3 = ST.get () in
  assert (felem_fits5 (as_felem5 h3 tmp) (2,2,2,2,4));

  fsub xy_pairs xy_pairs tmp (u64 4);
  let h4 = ST.get () in
  BL.fsub5_lemma (1,1,1,1,2) (2,2,2,2,4) (as_felem5 h3 xy_pairs) (as_felem5 h3 tmp) (u64 4);
  assert (felem_fits5 (as_felem5 h4 xy_pairs) (9,9,9,9,10))


inline_for_extraction noextract
val ab_plus_cd (a b c d tmp:felem) : Stack unit
  (requires fun h ->
    live h a /\ live h b /\ live h c /\ live h d /\ live h tmp /\
    disjoint a b /\ disjoint c d /\ eq_or_disjoint a b /\ eq_or_disjoint a d /\
    disjoint a tmp /\ disjoint b tmp /\ disjoint c tmp /\ disjoint d tmp /\

    felem_fits5 (as_felem5 h a) (9,9,9,9,10) /\
    felem_fits5 (as_felem5 h b) (5,5,5,5,6) /\
    felem_fits5 (as_felem5 h c) (3,3,3,3,6) /\
    felem_fits5 (as_felem5 h d) (9,9,9,9,10))
  (ensures fun h0 _ h1 -> modifies (loc c |+| loc tmp) h0 h1 /\
    feval h1 c ==
      S.fadd
	(S.fmul (feval h0 a) (feval h0 b))
	(S.fmul (feval h0 c) (feval h0 d)) /\
    inv_lazy_reduced2 h1 c)

let ab_plus_cd a b c d tmp =
  fmul tmp a b;
  fmul c c d;
  let h1 = ST.get () in
  assert (inv_lazy_reduced2 h1 tmp);
  assert (inv_lazy_reduced2 h1 c);
  BL.fadd5_lemma (1,1,1,1,2) (1,1,1,1,2) (as_felem5 h1 tmp) (as_felem5 h1 c);
  fadd c tmp c;
  let h2 = ST.get () in
  assert (felem_fits5 (as_felem5 h2 c) (2,2,2,2,4));
  fnormalize_weak c c;
  BL.normalize_weak5_lemma (2,2,2,2,4) (as_felem5 h2 c)


inline_for_extraction noextract
val ab_minus_cd (a b c d tmp:felem) : Stack unit
  (requires fun h ->
    live h a /\ live h b /\ live h c /\ live h d /\ live h tmp /\
    disjoint a b /\ disjoint c d /\ eq_or_disjoint a b /\ eq_or_disjoint a d /\
    disjoint a tmp /\ disjoint b tmp /\ disjoint c tmp /\ disjoint d tmp /\

    felem_fits5 (as_felem5 h a) (9,9,9,9,10) /\
    felem_fits5 (as_felem5 h b) (5,5,5,5,6) /\
    felem_fits5 (as_felem5 h c) (1,1,1,1,2) /\
    felem_fits5 (as_felem5 h d) (9,9,9,9,10))
  (ensures fun h0 _ h1 -> modifies (loc c |+| loc tmp) h0 h1 /\
    feval h1 c ==
      S.fsub
	(S.fmul (feval h0 a) (feval h0 b))
	(S.fmul (feval h0 c) (feval h0 d)) /\
    inv_lazy_reduced2 h1 c)

let ab_minus_cd a b c d tmp =
  fmul tmp a b;
  fmul c c d;
  let h1 = ST.get () in
  assert (inv_lazy_reduced2 h1 tmp);
  assert (inv_lazy_reduced2 h1 c);
  BL.fsub5_lemma (1,1,1,1,2) (1,1,1,1,2) (as_felem5 h1 tmp) (as_felem5 h1 c) (u64 2);
  fsub c tmp c (u64 2);
  let h2 = ST.get () in
  assert (felem_fits5 (as_felem5 h2 c) (5,5,5,5,6));
  fnormalize_weak c c;
  BL.normalize_weak5_lemma (5,5,5,5,6) (as_felem5 h2 c)


inline_for_extraction noextract
val yy_mp_bzz3 (zz yy tmp1 yy_m_bzz3 yy_p_bzz3:felem) : Stack unit
  (requires fun h ->
    live h zz /\ live h yy /\ live h tmp1 /\
    live h yy_m_bzz3 /\ live h yy_p_bzz3 /\
    disjoint zz yy /\ disjoint zz tmp1 /\ disjoint zz yy_m_bzz3 /\
    disjoint zz yy_p_bzz3 /\ disjoint yy tmp1 /\ disjoint yy yy_m_bzz3 /\
    disjoint yy yy_p_bzz3 /\ disjoint tmp1 yy_m_bzz3 /\
    disjoint tmp1 yy_p_bzz3 /\ disjoint yy_m_bzz3 yy_p_bzz3 /\

    inv_lazy_reduced2 h zz /\ inv_lazy_reduced2 h yy)
  (ensures  fun h0 _ h1 ->
    modifies (loc tmp1 |+| loc yy_m_bzz3 |+| loc yy_p_bzz3) h0 h1 /\
    (let bzz3 = S.fmul (S.fmul 3 S.b) (feval h0 zz) in
    feval h1 yy_m_bzz3 = S.fsub (feval h0 yy) bzz3 /\
    feval h1 yy_p_bzz3 = S.fadd (feval h0 yy) bzz3 /\
    felem_fits5 (as_felem5 h1 yy_m_bzz3) (5,5,5,5,6) /\
    felem_fits5 (as_felem5 h1 yy_p_bzz3) (2,2,2,2,4)))
val yy_mp_bzz3 (zz yy tmp1 yy_m_bzz3 yy_p_bzz3:felem) : Stack unit
  (requires fun h ->
    live h zz /\ live h yy /\ live h tmp1 /\
    live h yy_m_bzz3 /\ live h yy_p_bzz3 /\
    disjoint zz yy /\ disjoint zz tmp1 /\ disjoint zz yy_m_bzz3 /\
    disjoint zz yy_p_bzz3 /\ disjoint yy tmp1 /\ disjoint yy yy_m_bzz3 /\
    disjoint yy yy_p_bzz3 /\ disjoint tmp1 yy_m_bzz3 /\
    disjoint tmp1 yy_p_bzz3 /\ disjoint yy_m_bzz3 yy_p_bzz3 /\

    inv_lazy_reduced2 h zz /\ inv_lazy_reduced2 h yy)
  (ensures  fun h0 _ h1 ->
    modifies (loc tmp1 |+| loc yy_m_bzz3 |+| loc yy_p_bzz3) h0 h1 /\
    (let bzz3 = S.fmul (S.fmul 3 S.b) (feval h0 zz) in
    feval h1 yy_m_bzz3 = S.fsub (feval h0 yy) bzz3 /\
    feval h1 yy_p_bzz3 = S.fadd (feval h0 yy) bzz3 /\
    felem_fits5 (as_felem5 h1 yy_m_bzz3) (5,5,5,5,6) /\
    felem_fits5 (as_felem5 h1 yy_p_bzz3) (2,2,2,2,4)))

    zz: Hacl.K256.Field.felem ->
    yy: Hacl.K256.Field.felem ->
    tmp1: Hacl.K256.Field.felem ->
    yy_m_bzz3: Hacl.K256.Field.felem ->
    yy_p_bzz3: Hacl.K256.Field.felem
  -> FStar.HyperStack.ST.Stack Prims.unit