val lemma_and_quad32 (a b:quad32) : Lemma
  (ensures poly_and (of_quad32 a) (of_quad32 b) == of_quad32 (four_map2 (fun di si -> iand di si) a b))
let lemma_and_quad32 a b =
  calc (==) {
    poly_and (of_quad32 a) (of_quad32 b);
    == {lemma_of_to_quad32 (poly_and (of_quad32 a) (of_quad32 b))}
    of_quad32 (to_quad32 (poly_and (of_quad32 a) (of_quad32 b)));
    == {lemma_and128 (of_quad32 a) (of_quad32 b)}
    of_quad32 (four_map2 (fun di si -> iand di si) a b);
  }
val lemma_and_quad32 (a b:quad32) : Lemma
  (ensures poly_and (of_quad32 a) (of_quad32 b) == of_quad32 (four_map2 (fun di si -> iand di si) a b))
let lemma_and_quad32 a b =
calc ( == ) {
  poly_and (of_quad32 a) (of_quad32 b);
  ( == ) { lemma_of_to_quad32 (poly_and (of_quad32 a) (of_quad32 b)) }
  of_quad32 (to_quad32 (poly_and (of_quad32 a) (of_quad32 b)));
  ( == ) { lemma_and128 (of_quad32 a) (of_quad32 b) }
  of_quad32 (four_map2 (fun di si -> iand di si) a 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.Def.Types_s.quad32 FStar.Calc.calc_finish Vale.Math.Poly2_s.poly Prims.eq2 Vale.Math.Poly2.poly_and Vale.Math.Poly2.Bits_s.of_quad32 Vale.Def.Words.Four_s.four_map2 Vale.Def.Words_s.natN Vale.Def.Words_s.pow2_32 Vale.Def.Types_s.iand Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Vale.Math.Poly2.Bits_s.to_quad32 FStar.Calc.calc_init FStar.Calc.calc_pack Vale.Math.Poly2.Bits.lemma_of_to_quad32 Prims.squash Vale.Math.Poly2.Words.lemma_and128
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);
  ()

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);
  }

let lemma_add_quad32 a b =
  calc (==) {
    of_quad32 a +. of_quad32 b;
    == {lemma_of_to_quad32 (of_quad32 a +. of_quad32 b)}
    of_quad32 (to_quad32 (of_quad32 a +. of_quad32 b));
    == {lemma_add128 (of_quad32 a) (of_quad32 b)}
    of_quad32 (quad32_xor a b);
  }

let lemma_and128 a b =
  let Mkfour a0 a1 a2 a3 = to_quad32 a in
  let Mkfour b0 b1 b2 b3 = to_quad32 b in
  let pand m n = poly_and (of_nat32 m) (of_nat32 n) in
  calc (==) {
    to_quad32 (poly_and a b);
    == {
      lemma_quad32_to_nat32s a;
      lemma_quad32_to_nat32s b;
      lemma_bitwise_all ();
      lemma_equal (poly_and a b) (poly128_of_poly32s (pand a0 b0) (pand a1 b1) (pand a2 b2) (pand a3 b3))
    }
    to_quad32 (poly128_of_poly32s (pand a0 b0) (pand a1 b1) (pand a2 b2) (pand a3 b3));
    == {of_nat32_and a0 b0; of_nat32_and a1 b1; of_nat32_and a2 b2; of_nat32_and a3 b3}
    to_quad32 (poly128_of_nat32s (iand a0 b0) (iand a1 b1) (iand a2 b2) (iand a3 b3));
    == {lemma_quad32_of_nat32s (iand a0 b0) (iand a1 b1) (iand a2 b2) (iand a3 b3)}
    Mkfour (iand a0 b0) (iand a1 b1) (iand a2 b2) (iand a3 b3);
  }
val lemma_and_quad32 (a b:quad32) : Lemma
  (ensures poly_and (of_quad32 a) (of_quad32 b) == of_quad32 (four_map2 (fun di si -> iand di si) a b))
a: Vale.Def.Types_s.quad32 -> b: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
    (ensures
      Vale.Math.Poly2.poly_and (Vale.Math.Poly2.Bits_s.of_quad32 a)
        (Vale.Math.Poly2.Bits_s.of_quad32 b) ==
      Vale.Math.Poly2.Bits_s.of_quad32 (Vale.Def.Words.Four_s.four_map2 (fun di si ->
                Vale.Def.Types_s.iand di si)
            a
            b))