val xor_lemmas (_:unit) : Lemma
  (ensures
    (forall (x y:nat32).{:pattern (x *^ y)} x *^ y == y *^ x) /\
    (forall (n:nat32).{:pattern (n *^ 0)} n *^ 0 == n) /\
    (forall (n:nat32).{:pattern (n *^ n)} n *^ n == 0) /\
    (forall (n:nat64).{:pattern (ixor n n)} ixor n n == 0) /\
    (forall (x y z:nat32).{:pattern (x *^ (y *^ z))} 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;
  ()
val xor_lemmas (_:unit) : Lemma
  (ensures
    (forall (x y:nat32).{:pattern (x *^ y)} x *^ y == y *^ x) /\
    (forall (n:nat32).{:pattern (n *^ 0)} n *^ 0 == n) /\
    (forall (n:nat32).{:pattern (n *^ n)} n *^ n == 0) /\
    (forall (n:nat64).{:pattern (ixor n n)} ixor n n == 0) /\
    (forall (x y z:nat32).{:pattern (x *^ (y *^ z))} 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;
()
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.Classical.forall_intro_3 Vale.Def.Words_s.nat32 Prims.eq2 Vale.Def.Types_s.nat32 Vale.Arch.Types.op_Star_Hat Vale.Arch.Types.lemma_BitwiseXorAssociative FStar.Classical.forall_intro Vale.Def.Words_s.nat64 Prims.int Vale.Def.Types_s.ixor Vale.Def.Words_s.pow2_64 Vale.Arch.Types.lemma_BitwiseXorCancel64 Vale.Arch.Types.lemma_BitwiseXorCancel Vale.Arch.Types.lemma_BitwiseXorWithZero FStar.Classical.forall_intro_2 Vale.Arch.Types.lemma_BitwiseXorCommutative
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)
val xor_lemmas (_:unit) : Lemma
  (ensures
    (forall (x y:nat32).{:pattern (x *^ y)} x *^ y == y *^ x) /\
    (forall (n:nat32).{:pattern (n *^ 0)} n *^ 0 == n) /\
    (forall (n:nat32).{:pattern (n *^ n)} n *^ n == 0) /\
    (forall (n:nat64).{:pattern (ixor n n)} ixor n n == 0) /\
    (forall (x y z:nat32).{:pattern (x *^ (y *^ z))} x *^ (y *^ z) == (x *^ y) *^ z)
  )
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      (forall (x: Vale.Def.Words_s.nat32) (y: Vale.Def.Words_s.nat32). {:pattern (x *^ y)}
          x *^ y == y *^ x) /\ (forall (n: Vale.Def.Words_s.nat32). {:pattern (n *^ 0)} n *^ 0 == n) /\
      (forall (n: Vale.Def.Words_s.nat32). {:pattern (n *^ n)} n *^ n == 0) /\
      (forall (n: Vale.Def.Words_s.nat64). {:pattern Vale.Def.Types_s.ixor n n}
          Vale.Def.Types_s.ixor n n == 0) /\
      (forall (x: Vale.Def.Words_s.nat32) (y: Vale.Def.Words_s.nat32) (z: Vale.Def.Words_s.nat32).
          {:pattern (x *^ (y *^ z))}
          x *^ (y *^ z) == x *^ y *^ z))