val lemma_add128 (a b:poly) : Lemma
  (requires degree a <= 127 /\ degree b <= 127)
  (ensures to_quad32 (a +. b) == quad32_xor (to_quad32 a) (to_quad32 b))
let lemma_add128 a b =
  let Mkfour a0 a1 a2 a3 = to_quad32 a in
  let Mkfour b0 b1 b2 b3 = to_quad32 b in
  let pxor m n = of_nat32 m +. of_nat32 n in
  calc (==) {
    to_quad32 (a +. b);
    == {
      lemma_quad32_to_nat32s a;
      lemma_quad32_to_nat32s b;
      lemma_bitwise_all ();
      lemma_equal (a +. b) (poly128_of_poly32s (pxor a0 b0) (pxor a1 b1) (pxor a2 b2) (pxor a3 b3))
    }
    to_quad32 (poly128_of_poly32s (pxor a0 b0) (pxor a1 b1) (pxor a2 b2) (pxor a3 b3));
    == {of_nat32_xor a0 b0; of_nat32_xor a1 b1; of_nat32_xor a2 b2; of_nat32_xor a3 b3}
    to_quad32 (poly128_of_nat32s (ixor a0 b0) (ixor a1 b1) (ixor a2 b2) (ixor a3 b3));
    == {lemma_quad32_of_nat32s (ixor a0 b0) (ixor a1 b1) (ixor a2 b2) (ixor a3 b3)}
    Mkfour (ixor a0 b0) (ixor a1 b1) (ixor a2 b2) (ixor a3 b3);
    == {quad32_xor_reveal ()}
    quad32_xor (to_quad32 a) (to_quad32 b);
  }
val lemma_add128 (a b:poly) : Lemma
  (requires degree a <= 127 /\ degree b <= 127)
  (ensures to_quad32 (a +. b) == quad32_xor (to_quad32 a) (to_quad32 b))
let lemma_add128 a b =
let Mkfour a0 a1 a2 a3 = to_quad32 a in
let Mkfour b0 b1 b2 b3 = to_quad32 b in
let pxor m n = of_nat32 m +. of_nat32 n in
calc ( == ) {
  to_quad32 (a +. b);
  ( == ) { (lemma_quad32_to_nat32s a;
    lemma_quad32_to_nat32s b;
    lemma_bitwise_all ();
    lemma_equal (a +. b) (poly128_of_poly32s (pxor a0 b0) (pxor a1 b1) (pxor a2 b2) (pxor a3 b3))) }
  to_quad32 (poly128_of_poly32s (pxor a0 b0) (pxor a1 b1) (pxor a2 b2) (pxor a3 b3));
  ( == ) { (of_nat32_xor a0 b0;
    of_nat32_xor a1 b1;
    of_nat32_xor a2 b2;
    of_nat32_xor a3 b3) }
  to_quad32 (poly128_of_nat32s (ixor a0 b0) (ixor a1 b1) (ixor a2 b2) (ixor a3 b3));
  ( == ) { lemma_quad32_of_nat32s (ixor a0 b0) (ixor a1 b1) (ixor a2 b2) (ixor a3 b3) }
  Mkfour (ixor a0 b0) (ixor a1 b1) (ixor a2 b2) (ixor a3 b3);
  ( == ) { quad32_xor_reveal () }
  quad32_xor (to_quad32 a) (to_quad32 b);
}
Vale.Math.Poly2.Words.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.Math.Poly2.Words.fst
Vale.Math.Poly2_s.poly Vale.Def.Types_s.nat32 FStar.Calc.calc_finish Vale.Def.Types_s.quad32 Prims.eq2 Vale.Math.Poly2.Bits_s.to_quad32 Vale.Math.Poly2.op_Plus_Dot Vale.Def.Types_s.quad32_xor Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Vale.Def.Words_s.Mkfour Vale.Def.Types_s.ixor Vale.Def.Words_s.pow2_32 Vale.Math.Poly2.Bits.poly128_of_nat32s Vale.Math.Poly2.Bits.poly128_of_poly32s FStar.Calc.calc_init FStar.Calc.calc_pack Vale.Math.Poly2.lemma_equal Vale.Math.Poly2.Lemmas.lemma_bitwise_all Vale.Math.Poly2.Bits.lemma_quad32_to_nat32s Prims.squash Vale.Math.Poly2.Bits.of_nat32_xor Vale.Math.Poly2.Bits.lemma_quad32_of_nat32s Vale.Def.Types_s.quad32_xor_reveal Vale.Def.Words_s.nat32 Vale.Math.Poly2.Bits.of_nat32
module Vale.Math.Poly2.Words
open FStar.Mul

let lemma_quad32_zero () =
  lemma_bitwise_all ();
  lemma_equal zero (poly128_of_nat32s 0 0 0 0);
  lemma_quad32_of_nat32s 0 0 0 0;
  lemma_of_to_quad32 zero;
  ()

let lemma_quad32_ones () =
  let n = 0xffffffff in
  lemma_bitwise_all ();
  lemma_equal (ones 128) (poly128_of_nat32s n n n n);
  lemma_quad32_of_nat32s n n n n;
  lemma_of_to_quad32 (ones 128);
  ()
val lemma_add128 (a b:poly) : Lemma
  (requires degree a <= 127 /\ degree b <= 127)
  (ensures to_quad32 (a +. b) == quad32_xor (to_quad32 a) (to_quad32 b))
a: Vale.Math.Poly2_s.poly -> b: Vale.Math.Poly2_s.poly
  -> FStar.Pervasives.Lemma
      (requires Vale.Math.Poly2_s.degree a <= 127 /\ Vale.Math.Poly2_s.degree b <= 127)
      (ensures
        Vale.Math.Poly2.Bits_s.to_quad32 (a +. b) ==
        Vale.Def.Types_s.quad32_xor (Vale.Math.Poly2.Bits_s.to_quad32 a)
          (Vale.Math.Poly2.Bits_s.to_quad32 b))