val mods_contains (allowed found: mods_t) : bool
let rec mods_contains (allowed:mods_t) (found:mods_t) : bool =
  match found with
  | [] -> true
  | h::t -> mods_contains1 allowed h && mods_contains allowed t
val mods_contains (allowed found: mods_t) : bool
let rec mods_contains (allowed found: mods_t) : bool =
match found with
| [] -> true
| h :: t -> mods_contains1 allowed h && mods_contains allowed t
Vale.PPC64LE.QuickCodes.fsti.checked
Vale.PPC64LE.Vecs.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.Stack_i.fsti.checked Vale.PPC64LE.Regs.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.Decls.fsti.checked Vale.Def.Prop_s.fst.checked Vale.Arch.HeapImpl.fsti.checked prims.fst.checked FStar.Range.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Monotonic.Pure.fst.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked
Vale.PPC64LE.QuickCodes.fsti
Vale.PPC64LE.QuickCode.mods_t Vale.PPC64LE.QuickCode.mod_t Prims.list Prims.op_AmpAmp Vale.PPC64LE.QuickCodes.mods_contains1 Vale.PPC64LE.QuickCodes.mods_contains Prims.bool
module Vale.PPC64LE.QuickCodes
// Optimized weakest precondition generation for 'quick' procedures
open FStar.Mul
open FStar.Range
open Vale.Def.Prop_s
open Vale.Arch.HeapImpl
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.PPC64LE.Stack_i
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.QuickCode

unfold let code = va_code
unfold let codes = va_codes
unfold let fuel = va_fuel
unfold let eval = eval_code

[@va_qattr "opaque_to_smt"]
let labeled_wrap (r:range) (msg:string) (p:Type0) : GTot Type0 = labeled r msg p

// REVIEW: when used inside a function definition, 'labeled' can show up in an SMT query
// as an uninterpreted function.  Make a wrapper around labeled that is interpreted:
[@va_qattr "opaque_to_smt"]
let label (r:range) (msg:string) (p:Type0) : Ghost Type (requires True) (ensures fun q -> q <==> p) =
  assert_norm (labeled_wrap r msg p <==> p);
  labeled_wrap r msg p

val lemma_label_bool (r:range) (msg:string) (b:bool) : Lemma
  (requires label r msg b)
  (ensures b)
  [SMTPat (label r msg b)]

// wrap "precedes" and LexCons to avoid issues with label (precedes ...)
let precedes_wrap (#a:Type) (x y:a) : GTot Type0 = precedes x y

[@va_qattr]
let rec mods_contains1 (allowed:mods_t) (found:mod_t) : bool =
  match allowed with
  | [] -> mod_eq Mod_None found
  | h::t -> mod_eq h found || mods_contains1 t found

[@va_qattr]
val mods_contains (allowed found: mods_t) : bool
allowed: Vale.PPC64LE.QuickCode.mods_t -> found: Vale.PPC64LE.QuickCode.mods_t -> Prims.bool