val inverses128 (u:unit) : Lemma (DV.inverses get128 put128)
val inverses128 (u:unit) : Lemma (DV.inverses get128 put128)
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
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
/
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
u80: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures LowStar.BufferView.Down.inverses Vale.Interop.Views.get128 Vale.Interop.Views.put128)
Prims.unit FStar.Classical.forall_intro Vale.Def.Types_s.quad32 Prims.eq2 Vale.Def.Types_s.le_bytes_to_quad32 Vale.Def.Types_s.le_quad32_to_bytes Vale.Arch.Types.le_bytes_to_quad32_to_bytes FStar.Seq.Base.seq Vale.Def.Words_s.nat8 Prims.int FStar.Seq.Base.length Vale.Arch.Types.le_quad32_to_bytes_to_quad32 Vale.Interop.Views.put128_reveal Vale.Interop.Views.get128_reveal
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