val make_push_stack_variables_premium_conditional_negative
      (pred: actor_state_predicate)
      (initializer_cond:
          (initializer_t -> GTot bool)
            { (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
                  (initializer_cond initializer \/
                    (match
                        push_stack_variable actor
                          writer_pc
                          writer_expression_number
                          method_id
                          frame_uniq
                          initializer
                          s
                      with
                      | ComputationProduces s' -> pred actor s s'
                      | _ -> True))) /\ actor_state_predicate_reflexive pred /\
              actor_state_predicate_transitive pred })
    : GTot
    (
          actor: tid_t ->
          writer_pc: _ ->
          writer_expression_number: _ ->
          method_id: _ ->
          frame_uniq: _ ->
          initializers: _ ->
          s: _
        -> GTot
          (result:
            conditional_computation_t Armada.State.t
              { result ==
                push_stack_variables actor
                  writer_pc
                  writer_expression_number
                  method_id
                  frame_uniq
                  initializers
                  s /\
                (exists_ghost initializer_cond initializers \/
                  (match result with
                    | ComputationProduces s' -> pred actor s s'
                    | _ -> True)) }))
val make_push_stack_variables_premium_conditional_negative
      (pred: actor_state_predicate)
      (initializer_cond:
          (initializer_t -> GTot bool)
            { (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
                  (initializer_cond initializer \/
                    (match
                        push_stack_variable actor
                          writer_pc
                          writer_expression_number
                          method_id
                          frame_uniq
                          initializer
                          s
                      with
                      | ComputationProduces s' -> pred actor s s'
                      | _ -> True))) /\ actor_state_predicate_reflexive pred /\
              actor_state_predicate_transitive pred })
    : GTot
    (
          actor: tid_t ->
          writer_pc: _ ->
          writer_expression_number: _ ->
          method_id: _ ->
          frame_uniq: _ ->
          initializers: _ ->
          s: _
        -> GTot
          (result:
            conditional_computation_t Armada.State.t
              { result ==
                push_stack_variables actor
                  writer_pc
                  writer_expression_number
                  method_id
                  frame_uniq
                  initializers
                  s /\
                (exists_ghost initializer_cond initializers \/
                  (match result with
                    | ComputationProduces s' -> pred actor s s'
                    | _ -> True)) }))
let make_push_stack_variables_premium_conditional_negative
  (pred: actor_state_predicate)
  (initializer_cond: (initializer_t -> GTot bool){
       (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
          (initializer_cond initializer \/
           (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                    initializer s with
            | ComputationProduces s' -> pred actor s s'
            | _ -> True)))
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : GTot (actor: tid_t -> writer_pc: _ -> writer_expression_number: _ -> method_id: _ ->
          frame_uniq: _ -> initializers: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
                  result == push_stack_variables actor writer_pc writer_expression_number method_id
                              frame_uniq initializers s
                /\ (exists_ghost initializer_cond initializers \/
                   (match result with | ComputationProduces s' -> pred actor s s' | _ -> True))})) =
  make_push_stack_variables_premium_conditional pred
    (fun initializer -> not (initializer_cond initializer))
module Strategies.ArmadaStatement

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open Spec.List
open Spec.Logic
open Spec.Ubool
open Util.List

let actor_state_predicate = tid_t -> Armada.State.t -> Armada.State.t -> Type0

let actor_state_predicate_transitive (pred: actor_state_predicate) =
  forall actor x1 x2 x3. (pred actor x1 x2 /\ pred actor x2 x3) ==> (pred actor x1 x3)

let actor_state_predicate_reflexive (pred: actor_state_predicate) =
  forall actor x. pred actor x x

let actor_memory_predicate = tid_t -> Armada.Memory.t -> Armada.Memory.t -> Type0

let actor_memory_predicate_transitive (pred: actor_memory_predicate) =
  forall actor x1 x2 x3. (pred actor x1 x2 /\ pred actor x2 x3) ==> (pred actor x1 x3)

let actor_memory_predicate_reflexive (pred: actor_memory_predicate) =
  forall actor x. pred actor x x

let make_push_stack_variables_lemma_conditional
  (pred: actor_state_predicate)
  (initializer_cond: (initializer_t -> GTot bool){
       (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
          initializer_cond initializer ==>
          (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                   initializer s with
           | ComputationProduces s' -> pred actor s s'
           | _ -> True))
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : unit -> Lemma
      (forall actor writer_pc writer_expression_number method_id frame_uniq initializers s.
         {:pattern push_stack_variables actor writer_pc writer_expression_number method_id
                     frame_uniq initializers s}
         for_all_ghost initializer_cond initializers ==>
         (match push_stack_variables actor writer_pc writer_expression_number method_id
                  frame_uniq initializers s with
          | ComputationProduces s' -> pred actor s s'
          | _ -> True)) =
  fun _ ->
  let rec internal_lem actor writer_pc writer_expression_number method_id frame_uniq initializers s
    : Lemma (requires for_all_ghost initializer_cond initializers)
            (ensures (match push_stack_variables actor writer_pc writer_expression_number method_id
                              frame_uniq initializers s with
                      | ComputationProduces s' -> pred actor s s'
                      | _ -> True))
            (decreases initializers)
            [SMTPat (push_stack_variables actor writer_pc writer_expression_number method_id
                       frame_uniq initializers s)] =
    match initializers with
    | [] -> ()
    | first_initializer :: remaining_initializers ->
        (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                 first_initializer s with
         | ComputationProduces s' ->
             (match push_stack_variables actor writer_pc (writer_expression_number + 1) method_id
                      frame_uniq remaining_initializers s' with
              | ComputationProduces s'' ->
                  internal_lem actor writer_pc (writer_expression_number + 1) method_id frame_uniq
                    remaining_initializers s'
              | _ -> ())
         | _ -> ())
  in
  ()

let make_push_stack_variables_lemma
  (pred: actor_state_predicate{
       (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
           match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                   initializer s with
           | ComputationProduces s' -> pred actor s s'
           | _ -> True)
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : unit -> Lemma
      (forall actor writer_pc writer_expression_number method_id frame_uniq initializers s.
         {:pattern push_stack_variables actor writer_pc writer_expression_number method_id
                     frame_uniq initializers s}
         match push_stack_variables actor writer_pc writer_expression_number method_id
                 frame_uniq initializers s with
         | ComputationProduces s' -> pred actor s s'
         | _ -> True) =
  make_push_stack_variables_lemma_conditional pred (fun _ -> true)

let make_push_stack_variables_premium_conditional
  (pred: actor_state_predicate)
  (initializer_cond: initializer_t -> GTot bool{
       (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
          initializer_cond initializer ==>
          (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                   initializer s with
           | ComputationProduces s' -> pred actor s s'
           | _ -> True))
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : GTot (actor: _ -> writer_pc: _ -> writer_expression_number: _ -> method_id: _ -> frame_uniq: _ ->
          initializers: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
                  result == push_stack_variables actor writer_pc writer_expression_number method_id
                              frame_uniq initializers s
                /\ (for_all_ghost initializer_cond initializers ==>
                   (match result with | ComputationProduces s' -> pred actor s s' | _ -> True))})) =
  make_push_stack_variables_lemma_conditional pred initializer_cond ();
  let f actor writer_pc writer_expression_number method_id frame_uniq initializers s
    : GTot (result: conditional_computation_t Armada.State.t{
                result == push_stack_variables actor writer_pc writer_expression_number method_id
                            frame_uniq initializers s
              /\ (for_all_ghost initializer_cond initializers ==>
                 (match result with | ComputationProduces s' -> pred actor s s' | _ -> True))}) =
    push_stack_variables actor writer_pc writer_expression_number method_id frame_uniq initializers
      s
  in
  f

let make_push_stack_variables_premium
  (pred: actor_state_predicate{
       (forall actor writer_pc writer_expression_number method_id frame_uniq initializers s.
          match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                  initializers s with
          | ComputationProduces s' -> pred actor s s'
          | _ -> True)
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : GTot (actor: tid_t -> writer_pc: _ -> writer_expression_number: _ -> method_id: _ ->
          frame_uniq: _ -> initializers: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
                  result == push_stack_variables actor writer_pc writer_expression_number method_id
                              frame_uniq initializers s
                /\ (match result with | ComputationProduces s' -> pred actor s s' | _ -> True)})) =
  make_push_stack_variables_premium_conditional pred (fun _ -> true)
/
Util.List.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.ArmadaStatement.fst

    pred: Strategies.ArmadaStatement.actor_state_predicate ->
    initializer_cond:
      (_: Armada.Init.initializer_t -> Prims.GTot Prims.bool)
        { (forall (actor: Armada.Base.tid_t)
              (writer_pc: Armada.Base.pc_t)
              (writer_expression_number: Prims.nat)
              (method_id: Armada.Base.method_id_t)
              (frame_uniq: Armada.Base.root_id_uniquifier_t)
              (initializer: Armada.Init.initializer_t)
              (s: Armada.State.t).
              initializer_cond initializer \/
              (match
                  Armada.Init.push_stack_variable actor
                    writer_pc
                    writer_expression_number
                    method_id
                    frame_uniq
                    initializer
                    s
                with
                | Armada.Computation.ComputationProduces #_ s' -> pred actor s s'
                | _ -> Prims.l_True)) /\
          Strategies.ArmadaStatement.actor_state_predicate_reflexive pred /\
          Strategies.ArmadaStatement.actor_state_predicate_transitive pred }
  -> Prims.GTot
    (
          actor: Armada.Base.tid_t ->
          writer_pc: Armada.Base.pc_t ->
          writer_expression_number: Prims.nat ->
          method_id: Armada.Base.method_id_t ->
          frame_uniq: Armada.Base.root_id_uniquifier_t ->
          initializers: Prims.list Armada.Init.initializer_t ->
          s: Armada.State.t
        -> Prims.GTot
          (result:
            Armada.Computation.conditional_computation_t Armada.State.t
              { result ==
                Armada.Init.push_stack_variables actor
                  writer_pc
                  writer_expression_number
                  method_id
                  frame_uniq
                  initializers
                  s /\
                (Util.List.exists_ghost initializer_cond initializers \/
                  (match result with
                    | Armada.Computation.ComputationProduces #_ s' -> pred actor s s'
                    | _ -> Prims.l_True)) }))
Strategies.ArmadaStatement.actor_state_predicate Armada.Init.initializer_t Prims.bool Prims.l_and Prims.l_Forall Armada.Base.tid_t Armada.Base.pc_t Prims.nat Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Armada.State.t Prims.l_or Prims.b2t Armada.Init.push_stack_variable Armada.Computation.conditional_computation_t Prims.l_True Prims.logical Strategies.ArmadaStatement.actor_state_predicate_reflexive Strategies.ArmadaStatement.actor_state_predicate_transitive Strategies.ArmadaStatement.make_push_stack_variables_premium_conditional Prims.op_Negation Prims.list Prims.eq2 Armada.Init.push_stack_variables Util.List.exists_ghost
let make_push_stack_variables_premium_conditional_negative
      (pred: actor_state_predicate)
      (initializer_cond:
          (initializer_t -> GTot bool)
            { (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
                  (initializer_cond initializer \/
                    (match
                        push_stack_variable actor
                          writer_pc
                          writer_expression_number
                          method_id
                          frame_uniq
                          initializer
                          s
                      with
                      | ComputationProduces s' -> pred actor s s'
                      | _ -> True))) /\ actor_state_predicate_reflexive pred /\
              actor_state_predicate_transitive pred })
    : GTot
    (
          actor: tid_t ->
          writer_pc: _ ->
          writer_expression_number: _ ->
          method_id: _ ->
          frame_uniq: _ ->
          initializers: _ ->
          s: _
        -> GTot
          (result:
            conditional_computation_t Armada.State.t
              { result ==
                push_stack_variables actor
                  writer_pc
                  writer_expression_number
                  method_id
                  frame_uniq
                  initializers
                  s /\
                (exists_ghost initializer_cond initializers \/
                  (match result with
                    | ComputationProduces s' -> pred actor s s'
                    | _ -> True)) })) =
  
make_push_stack_variables_premium_conditional pred
  (fun initializer -> not (initializer_cond initializer))