let equiv_states (s1 s2:va_state) = equiv_states s1 s2
let equiv_states (s1 s2: va_state) =
equiv_states s1 s2
Vale.Transformers.Transform.fsti.checked
Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Transformers.Common.fsti.checked Vale.Def.PossiblyMonad.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked
Vale.Transformers.Transform.fsti
Vale.X64.Decls.va_state Vale.Transformers.Common.equiv_states Prims.logical
(**

   This module exposes user-friendly transformers and lemmas for them.

   Each transformation takes 1 or more [va_code] object(s) and
   produces a [va_code] object, along with additional data. The lemma
   guarantees that the produced [va_code] object is semantically
   identical to the (first, if more than one) provided [va_code]
   object.

   The additional data that is generated is always a [pbool] which is
   [ttrue] if the transformation succeeded, and otherwise is a [ffalse
   reason].  Under both circumstances, the lemma mentioned above is
   held, and in particular, a failed transformation is still safe to
   use (since in that case, the code returned is exactly the same as
   the first [va_code] object). The additional data is provided only
   for debugging, since we expect that after debugging and fixing
   things, all transformations will succeed.

*)
module Vale.Transformers.Transform

open Vale.X64.Machine_s
open Vale.Def.PossiblyMonad
open Vale.X64.Decls
open Vale.Transformers.Common
val equiv_states : s1: Vale.X64.Decls.va_state -> s2: Vale.X64.Decls.va_state -> Prims.logical
s1: Vale.X64.Decls.va_state -> s2: Vale.X64.Decls.va_state -> Prims.logical