val lemma_reverse_bytes_quad32_zero (_:unit) : Lemma
  (let z = Mkfour 0 0 0 0 in
   reverse_bytes_quad32 z == z)
let lemma_reverse_bytes_quad32_zero (_:unit) : Lemma
  (let z = Mkfour 0 0 0 0 in
   reverse_bytes_quad32 z == z)
  =
  let z = Mkfour 0 0 0 0 in
  calc (==) {
    reverse_bytes_quad32 z;
    == { reveal_reverse_bytes_quad32 z }
    four_reverse (four_map reverse_bytes_nat32 z);
    == { lemma_reverse_bytes_nat32() }
    z;
  };
  ()
val lemma_reverse_bytes_quad32_zero (_:unit) : Lemma
  (let z = Mkfour 0 0 0 0 in
   reverse_bytes_quad32 z == z)
let lemma_reverse_bytes_quad32_zero (_: unit)
    : Lemma
    (let z = Mkfour 0 0 0 0 in
      reverse_bytes_quad32 z == z) =
let z = Mkfour 0 0 0 0 in
calc ( == ) {
  reverse_bytes_quad32 z;
  ( == ) { reveal_reverse_bytes_quad32 z }
  four_reverse (four_map reverse_bytes_nat32 z);
  ( == ) { lemma_reverse_bytes_nat32 () }
  z;
};
()
Vale.Arch.Types.fst.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.Arch.Types.fst
Prims.unit FStar.Calc.calc_finish Vale.Def.Types_s.quad32 Prims.eq2 Vale.Def.Types_s.reverse_bytes_quad32 Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Vale.Def.Words.Four_s.four_reverse Vale.Def.Types_s.nat32 Vale.Def.Words.Four_s.four_map Vale.Def.Types_s.reverse_bytes_nat32 FStar.Calc.calc_init FStar.Calc.calc_pack Vale.Def.Types_s.reveal_reverse_bytes_quad32 Prims.squash Vale.Arch.Types.lemma_reverse_bytes_nat32 Vale.Def.Words_s.four Vale.Def.Words_s.nat32 Vale.Def.Words_s.Mkfour Prims.l_True FStar.Pervasives.pattern
module Vale.Arch.Types

open FStar.Mul
open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Arch.TypesNative
open Vale.Lib.Seqs
open Vale.Def.Words_s
open Vale.Def.Words.Two
open FStar.Calc

let lemma_nat_to_two32 () =
  assert_norm (forall (x:nat64).{:pattern (nat_to_two 32 x)}
    nat_to_two 32 x == Mktwo (x % 0x100000000) (x / 0x100000000))

let lemma_BitwiseXorCommutative x y =
  lemma_ixor_nth_all 32;
  lemma_equal_nth 32 (x *^ y) (y *^ x)

let lemma_BitwiseXorWithZero n =
  lemma_ixor_nth_all 32;
  lemma_zero_nth 32;
  lemma_equal_nth 32 (n *^ 0) n

let lemma_BitwiseXorCancel n =
  lemma_ixor_nth_all 32;
  lemma_zero_nth 32;
  lemma_equal_nth 32 (n *^ n) 0

let lemma_BitwiseXorCancel64 (n:nat64) =
  lemma_ixor_nth_all 64;
  lemma_zero_nth 64;
  lemma_equal_nth 64 (ixor n n) 0

let lemma_BitwiseXorAssociative x y z =
  lemma_ixor_nth_all 32;
  lemma_equal_nth 32 (x *^ (y *^ z)) ((x *^ y) *^ z)

let xor_lemmas () =
  FStar.Classical.forall_intro_2 lemma_BitwiseXorCommutative;
  FStar.Classical.forall_intro lemma_BitwiseXorWithZero;
  FStar.Classical.forall_intro lemma_BitwiseXorCancel;
  FStar.Classical.forall_intro lemma_BitwiseXorCancel64;
  FStar.Classical.forall_intro_3 lemma_BitwiseXorAssociative;
  ()

#push-options "--max_fuel 3 --initial_fuel 3 --max_ifuel 3 --initial_ifuel 3"  // REVIEW: Why do we need this?
let lemma_quad32_xor () =
  quad32_xor_reveal ();
  reverse_bytes_nat32_reveal ();
  xor_lemmas()
  (*
  let helper (q:quad32) : Lemma (quad32_xor q q == Mkfour 0 0 0 0) =
    let q' = quad32_xor q q in
    quad32_xor_reveal ();
    reverse_bytes_nat32_reveal ();
    // REVIEW: Why are these necessary?
    assert (q'.lo0 == nat32_xor q.lo0 q.lo0);
    assert (q'.lo1 == nat32_xor q.lo1 q.lo1);
    assert (q'.hi2 == nat32_xor q.hi2 q.hi2);
    assert (q'.hi3 == nat32_xor q.hi3 q.hi3);
    xor_lemmas()
  in
  FStar.Classical.forall_intro helper
  *)
#pop-options

let lemma_reverse_reverse_bytes_nat32 (n:nat32) :
  Lemma (reverse_bytes_nat32 (reverse_bytes_nat32 n) == n)
  =
  reverse_bytes_nat32_reveal ();
  let r = reverse_seq (nat32_to_be_bytes n) in
  be_bytes_to_nat32_to_be_bytes r;
  ()

#push-options "--max_fuel 3 --initial_fuel 3 --max_ifuel 3 --initial_ifuel 3"  // REVIEW: Why do we need this?
let lemma_reverse_bytes_quad32 (q:quad32) =
  quad32_xor_reveal ();
  reverse_bytes_nat32_reveal ();
  reveal_reverse_bytes_quad32 q;
  reveal_reverse_bytes_quad32 (reverse_bytes_quad32 q);
  ()
#pop-options

let lemma_reverse_bytes_nat32 (_:unit) : Lemma
  (reverse_bytes_nat32 0 == 0)
  =
  reverse_bytes_nat32_reveal ();
  assert_norm (nat_to_four 8 0 == Mkfour 0 0 0 0);
  ()

let lemma_reverse_bytes_quad32_zero (_:unit) : Lemma
  (let z = Mkfour 0 0 0 0 in
val lemma_reverse_bytes_quad32_zero (_:unit) : Lemma
  (let z = Mkfour 0 0 0 0 in
   reverse_bytes_quad32 z == z)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      (let z = Vale.Def.Words_s.Mkfour 0 0 0 0 in
        Vale.Def.Types_s.reverse_bytes_quad32 z == z))