val lemma_BitwiseXorWithZero64 (n:nat64) : Lemma (ixor n 0 == n)
let lemma_BitwiseXorWithZero64 n =
  lemma_ixor_nth_all 64;
  lemma_zero_nth 64;
  lemma_equal_nth 64 (ixor n 0) n
val lemma_BitwiseXorWithZero64 (n:nat64) : Lemma (ixor n 0 == n)
let lemma_BitwiseXorWithZero64 n =
lemma_ixor_nth_all 64;
lemma_zero_nth 64;
lemma_equal_nth 64 (ixor n 0) n
Vale.AES.Types_helpers.fst.checked
Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Vale.AES.Types_helpers.fst
Vale.Def.Types_s.nat64 Vale.Arch.TypesNative.lemma_equal_nth Vale.Def.Types_s.ixor Vale.Def.Words_s.pow2_64 Prims.unit Vale.Arch.TypesNative.lemma_zero_nth Vale.Arch.TypesNative.lemma_ixor_nth_all
module Vale.AES.Types_helpers

open Vale.Def.Words.Seq_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.Arch.Types
open FStar.Seq
open Vale.Arch.TypesNative

let lemma_slices_le_quad32_to_bytes (q:quad32) : Lemma
  (ensures (
    let s = le_quad32_to_bytes q in
    q.lo0 == four_to_nat 8 (seq_to_four_LE (slice s 0 4)) /\
    q.lo1 == four_to_nat 8 (seq_to_four_LE (slice s 4 8)) /\
    q.hi2 == four_to_nat 8 (seq_to_four_LE (slice s 8 12)) /\
    q.hi3 == four_to_nat 8 (seq_to_four_LE (slice s 12 16))
  ))
  =
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
  reveal_opaque (`%le_quad32_to_bytes) le_quad32_to_bytes;
  ()

let lemma_slices_be_quad32_to_bytes (q:quad32) : Lemma
  (ensures (
    let s = be_quad32_to_bytes q in
    q.hi3 == four_to_nat 8 (seq_to_four_BE (slice s 0 4)) /\
    q.hi2 == four_to_nat 8 (seq_to_four_BE (slice s 4 8)) /\
    q.lo1 == four_to_nat 8 (seq_to_four_BE (slice s 8 12)) /\
    q.lo0 == four_to_nat 8 (seq_to_four_BE (slice s 12 16))
  ))
  =
  reveal_opaque (`%seq_four_to_seq_BE) (seq_four_to_seq_BE #nat8);
  reveal_opaque (`%be_quad32_to_bytes) be_quad32_to_bytes;
  ()
val lemma_BitwiseXorWithZero64 (n:nat64) : Lemma (ixor n 0 == n)
n: Vale.Def.Types_s.nat64 -> FStar.Pervasives.Lemma (ensures Vale.Def.Types_s.ixor n 0 == n)