val make_pop_stack_variables_lemma:
    pred:
      actor_memory_predicate
        { (forall actor method_id frame_uniq var_id mem.
              (match pop_stack_variable actor method_id frame_uniq var_id mem with
                | ComputationProduces mem' -> pred actor mem mem'
                | _ -> True)) /\ actor_memory_predicate_reflexive pred /\
          actor_memory_predicate_transitive pred } ->
    unit
  -> Lemma
    (forall actor method_id frame_uniq var_ids mem.
        {:pattern pop_stack_variables actor method_id frame_uniq var_ids mem}
        match pop_stack_variables actor method_id frame_uniq var_ids mem with
        | ComputationProduces mem' -> pred actor mem mem'
        | _ -> True)
val make_pop_stack_variables_lemma:
    pred:
      actor_memory_predicate
        { (forall actor method_id frame_uniq var_id mem.
              (match pop_stack_variable actor method_id frame_uniq var_id mem with
                | ComputationProduces mem' -> pred actor mem mem'
                | _ -> True)) /\ actor_memory_predicate_reflexive pred /\
          actor_memory_predicate_transitive pred } ->
    unit
  -> Lemma
    (forall actor method_id frame_uniq var_ids mem.
        {:pattern pop_stack_variables actor method_id frame_uniq var_ids mem}
        match pop_stack_variables actor method_id frame_uniq var_ids mem with
        | ComputationProduces mem' -> pred actor mem mem'
        | _ -> True)
let make_pop_stack_variables_lemma
  (pred: actor_memory_predicate{
       (forall actor method_id frame_uniq var_id mem.
          (match pop_stack_variable actor method_id frame_uniq var_id mem with
           | ComputationProduces mem' -> pred actor mem mem'
           | _ -> True))
     /\ actor_memory_predicate_reflexive pred
     /\ actor_memory_predicate_transitive pred})
  : unit -> Lemma
      (forall actor method_id frame_uniq var_ids mem.
         {:pattern pop_stack_variables actor method_id frame_uniq var_ids mem}
         match pop_stack_variables actor method_id frame_uniq var_ids mem with
         | ComputationProduces mem' -> pred actor mem mem'
         | _ -> True) =
  fun _ ->
  let rec internal_lem actor method_id frame_uniq var_ids mem
    : Lemma (ensures (match pop_stack_variables actor method_id frame_uniq var_ids mem with
                      | ComputationProduces mem' -> pred actor mem mem'
                      | _ -> True))
            (decreases var_ids)
            [SMTPat (pop_stack_variables actor method_id frame_uniq var_ids mem)] =
    match pop_stack_variables actor method_id frame_uniq var_ids mem with
    | ComputationProduces mem' ->
        (match var_ids with
         | [] -> ()
         | first_var_id :: remaining_var_ids ->
             (match pop_stack_variable actor method_id frame_uniq first_var_id mem with
              | ComputationProduces mem2 ->
                  internal_lem actor method_id frame_uniq remaining_var_ids mem2
              | _ -> ()))
    | _ -> ()
  in
  ()
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)

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))

let make_push_stack_parameters_lemma_conditional
  (pred: actor_state_predicate)
  (parameter_cond: object_value_t -> GTot bool{
       (forall actor writer_pc writer_expression_number method_id frame_uniq initializer s.
            InitializerSpecific? initializer.iv
          /\ parameter_cond (InitializerSpecific?.value initializer.iv) ==>
          (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 var_ids parameters s.
         {:pattern push_stack_parameters actor writer_pc writer_expression_number
                     method_id frame_uniq var_ids parameters s}
         for_all_ghost parameter_cond parameters ==>
         (match push_stack_parameters actor writer_pc writer_expression_number
                  method_id frame_uniq var_ids parameters s with
          | ComputationProduces s' -> pred actor s s'
          | _ -> True)) =
  fun _ ->
  let rec internal_lem actor writer_pc writer_expression_number method_id frame_uniq var_ids
                         parameters s
    : Lemma (requires for_all_ghost parameter_cond parameters)
            (ensures (match push_stack_parameters actor writer_pc writer_expression_number
                              method_id frame_uniq var_ids parameters s with
                      | ComputationProduces s' -> pred actor s s'
                      | _ -> True))
            (decreases parameters)
            [SMTPat (push_stack_parameters actor writer_pc writer_expression_number
                       method_id frame_uniq var_ids parameters s)] =
    match parameters, var_ids with
    | [], [] -> ()
    | first_parameter :: remaining_parameters, first_var_id :: remaining_var_ids ->
        let first_initializer = { var_id = first_var_id; iv = InitializerSpecific first_parameter;
                                  weakly_consistent = false } in
        (match push_stack_variable actor writer_pc writer_expression_number method_id
                             frame_uniq first_initializer s with
         | ComputationProduces s' ->
             (match push_stack_parameters actor writer_pc (writer_expression_number + 1) method_id
                      frame_uniq remaining_var_ids remaining_parameters s' with
              | ComputationProduces s'' ->
                  internal_lem actor writer_pc (writer_expression_number + 1) method_id frame_uniq
                    remaining_var_ids remaining_parameters s'
              | _ -> ())
         | _ -> ())
    | _ -> ()
  in
  ()
/
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_memory_predicate
        { (forall (actor: Armada.Base.tid_t)
              (method_id: Armada.Base.method_id_t)
              (frame_uniq: Armada.Base.root_id_uniquifier_t)
              (var_id: Armada.Base.var_id_t)
              (mem: Armada.Memory.t).
              (match Armada.Memory.pop_stack_variable actor method_id frame_uniq var_id mem with
                | Armada.Computation.ComputationProduces #_ mem' -> pred actor mem mem'
                | _ -> Prims.l_True)
              <:
              Type0) /\ Strategies.ArmadaStatement.actor_memory_predicate_reflexive pred /\
          Strategies.ArmadaStatement.actor_memory_predicate_transitive pred } ->
    _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      forall (actor: Armada.Base.tid_t)
        (method_id: Armada.Base.method_id_t)
        (frame_uniq: Armada.Base.root_id_uniquifier_t)
        (var_ids: Prims.list Armada.Base.var_id_t)
        (mem: Armada.Memory.t).
        {:pattern Armada.Memory.pop_stack_variables actor method_id frame_uniq var_ids mem}
        (match Armada.Memory.pop_stack_variables actor method_id frame_uniq var_ids mem with
          | Armada.Computation.ComputationProduces #_ mem' -> pred actor mem mem'
          | _ -> Prims.l_True)
        <:
        Type0)
Strategies.ArmadaStatement.actor_memory_predicate Prims.l_and Prims.l_Forall Armada.Base.tid_t Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Armada.Base.var_id_t Armada.Memory.t Armada.Memory.pop_stack_variable Armada.Computation.conditional_computation_t Prims.l_True Strategies.ArmadaStatement.actor_memory_predicate_reflexive Strategies.ArmadaStatement.actor_memory_predicate_transitive Prims.unit Prims.list Prims.squash Armada.Memory.pop_stack_variables Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let make_pop_stack_variables_lemma
      (pred:
          actor_memory_predicate
            { (forall actor method_id frame_uniq var_id mem.
                  (match pop_stack_variable actor method_id frame_uniq var_id mem with
                    | ComputationProduces mem' -> pred actor mem mem'
                    | _ -> True)) /\ actor_memory_predicate_reflexive pred /\
              actor_memory_predicate_transitive pred })
    :  unit
      -> Lemma
        (forall actor method_id frame_uniq var_ids mem.
            {:pattern pop_stack_variables actor method_id frame_uniq var_ids mem}
            match pop_stack_variables actor method_id frame_uniq var_ids mem with
            | ComputationProduces mem' -> pred actor mem mem'
            | _ -> True) =
  
fun _ ->
  let rec internal_lem actor method_id frame_uniq var_ids mem
      : Lemma
        (ensures
          (match pop_stack_variables actor method_id frame_uniq var_ids mem with
            | ComputationProduces mem' -> pred actor mem mem'
            | _ -> True))
        (decreases var_ids)
        [SMTPat (pop_stack_variables actor method_id frame_uniq var_ids mem)] =
    match pop_stack_variables actor method_id frame_uniq var_ids mem with
    | ComputationProduces mem' ->
      (match var_ids with
        | [] -> ()
        | first_var_id :: remaining_var_ids ->
          (match pop_stack_variable actor method_id frame_uniq first_var_id mem with
            | ComputationProduces mem2 ->
              internal_lem actor method_id frame_uniq remaining_var_ids mem2
            | _ -> ()))
    | _ -> ()
  in
  ()