val put32_128_aux1 (x: quad32) : Lemma (get32_128 (put32_128 x) == x)
let put32_128_aux1 (x: quad32): Lemma (get32_128 (put32_128 x) == x) =
  put32_128_reveal ();
  get32_128_reveal ();
  ()
val put32_128_aux1 (x: quad32) : Lemma (get32_128 (put32_128 x) == x)
let put32_128_aux1 (x: quad32) : Lemma (get32_128 (put32_128 x) == x) =
put32_128_reveal ();
get32_128_reveal ();
()
Vale.Interop.Views.fst.checked
Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.Interop.Views.fst
Vale.Def.Types_s.quad32 Prims.unit Vale.Interop.Views.get32_128_reveal Vale.Interop.Views.put32_128_reveal Prims.l_True Prims.squash Prims.eq2 Vale.Interop.Views.get32_128 Vale.Interop.Views.put32_128 Prims.Nil FStar.Pervasives.pattern
module Vale.Interop.Views
open FStar.Mul

let inverses8 (u:unit) =
  get8_reveal ();
  put8_reveal ();
  let aux (x:Seq.lseq U8.t 1) : Lemma (put8 (get8 x) == x) =
    assert (Seq.equal x (put8 (get8 x)))
  in Classical.forall_intro aux

let inverses16 (u:unit) =
  get16_reveal ();
  put16_reveal ();
  let aux (x:Seq.lseq U8.t 2) : Lemma (put16 (get16 x) == x) =
    assert (Seq.equal x (put16 (get16 x)))
  in Classical.forall_intro aux

#set-options "--z3rlimit 40"

let inverses32 (u:unit) =
  get32_reveal ();
  put32_reveal ();
  Classical.forall_intro (four_to_seq_to_four_LE #nat8);
  Classical.forall_intro (seq_to_four_to_seq_LE #nat8)

#reset-options "--z3rlimit 20"
let inverses64 (u:unit) =
  get64_reveal ();
  put64_reveal ();
  Classical.forall_intro Vale.Arch.Types.le_nat64_to_bytes_to_nat64;
  Classical.forall_intro Vale.Arch.Types.le_bytes_to_nat64_to_bytes

let inverses128 (u:unit) =
  get128_reveal ();
  put128_reveal ();
  Classical.forall_intro Vale.Arch.Types.le_quad32_to_bytes_to_quad32;
  Classical.forall_intro Vale.Arch.Types.le_bytes_to_quad32_to_bytes

let get32_128_aux1 (x: Seq.lseq U32.t 4): Lemma (put32_128 (get32_128 x) == x) =
  put32_128_reveal ();
  get32_128_reveal ();
  let vg = get32_128 x in
  let vp = put32_128 vg in
  assert (Seq.equal x vp)
val put32_128_aux1 (x: quad32) : Lemma (get32_128 (put32_128 x) == x)
x: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
    (ensures Vale.Interop.Views.get32_128 (Vale.Interop.Views.put32_128 x) == x)