let wp_Seq_t (a:Type0) = va_state -> a -> Type0
let wp_Seq_t (a: Type0) =
va_state -> a -> Type0
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.Decls.va_state
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]
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

[@va_qattr]
let if_code (b:bool) (c1:code) (c2:code) : code = if b then c1 else c2

open FStar.Monotonic.Pure

noeq type quickCodes (a:Type0) : codes -> Type =
| QEmpty: a -> quickCodes a []
| QSeq: #b:Type -> #c:code -> #cs:codes -> r:range -> msg:string ->
    quickCode b c -> quickCodes a cs -> quickCodes a (c::cs)
| QBind: #b:Type -> #c:code -> #cs:codes -> r:range -> msg:string ->
    quickCode b c -> (va_state -> b -> GTot (quickCodes a cs)) -> quickCodes a (c::cs)
| QGetState: #cs:codes -> (va_state -> GTot (quickCodes a cs)) -> quickCodes a ((Block [])::cs)
| QPURE: #cs:codes -> r:range -> msg:string -> pre:((unit -> GTot Type0) -> GTot Type0){is_monotonic pre} ->
    (unit -> PURE unit (as_pure_wp pre)) -> quickCodes a cs -> quickCodes a cs
//| QBindPURE: #cs:codes -> b:Type -> r:range -> msg:string -> pre:((b -> GTot Type0) -> GTot Type0) ->
//    (unit -> PURE b pre) -> (va_state -> b -> GTot (quickCodes a cs)) -> quickCodes a ((Block [])::cs)
| QLemma: #cs:codes -> r:range -> msg:string -> pre:Type0 -> post:(squash pre -> Type0) ->
    (unit -> Lemma (requires pre) (ensures post ())) -> quickCodes a cs -> quickCodes a cs
| QGhost: #cs:codes -> b:Type -> r:range -> msg:string -> pre:Type0 -> post:(b -> Type0) ->
    (unit -> Ghost b (requires pre) (ensures post)) -> (b -> GTot (quickCodes a cs)) -> quickCodes a ((Block [])::cs)
| QAssertBy: #cs:codes -> r:range -> msg:string -> p:Type0 ->
    quickCodes unit [] -> quickCodes a cs -> quickCodes a cs

[@va_qattr] unfold let va_QBind (#a:Type0) (#b:Type) (#c:code) (#cs:codes) (r:range) (msg:string) (qc:quickCode b c) (qcs:va_state -> b -> GTot (quickCodes a cs)) : quickCodes a (c::cs) = QBind r msg qc qcs
[@va_qattr] unfold let va_QEmpty (#a:Type0) (v:a) : quickCodes a [] = QEmpty v
[@va_qattr] unfold let va_QLemma (#a:Type0) (#cs:codes) (r:range) (msg:string) (pre:Type0) (post:(squash pre -> Type0)) (l:unit -> Lemma (requires pre) (ensures post ())) (qcs:quickCodes a cs) : quickCodes a cs = QLemma r msg pre post l qcs
[@va_qattr] unfold let va_QSeq (#a:Type0) (#b:Type) (#c:code) (#cs:codes) (r:range) (msg:string) (qc:quickCode b c) (qcs:quickCodes a cs) : quickCodes a (c::cs) = QSeq r msg qc qcs

[@va_qattr]
let va_qPURE
    (#cs:codes) (#pre:((unit -> GTot Type0) -> GTot Type0){is_monotonic pre}) (#a:Type0) (r:range) (msg:string)
    ($l:unit -> PURE unit (intro_pure_wp_monotonicity pre; pre)) (qcs:quickCodes a cs)
  : quickCodes a cs =
  QPURE r msg pre l qcs

(* REVIEW: this might be useful, but inference of pre doesn't work as well as for va_qPURE
  (need to provide pre explicitly; as a result, no need to put $ on l)
[@va_qattr]
let va_qBindPURE
    (#a #b:Type0) (#cs:codes) (pre:(b -> GTot Type0) -> GTot Type0) (r:range) (msg:string)
    (l:unit -> PURE b pre) (qcs:va_state -> b -> GTot (quickCodes a cs))
  : quickCodes a ((Block [])::cs) =
  QBindPURE b r msg pre l qcs
*)

[@va_qattr]
let wp_proc (#a:Type0) (c:code) (qc:quickCode a c) (s0:va_state) (k:va_state -> a -> Type0) : Type0 =
  match qc with
  | QProc _ _ wp _ -> wp s0 k
val wp_Seq_t : a: Type0 -> Type
a: Type0 -> Type