val 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)
val 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)
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)
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
  ()
/
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
        { (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).
              (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)
              <:
              Type0) /\ Strategies.ArmadaStatement.actor_state_predicate_reflexive pred /\
          Strategies.ArmadaStatement.actor_state_predicate_transitive pred } ->
    _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      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)
        (initializers: Prims.list Armada.Init.initializer_t)
        (s: Armada.State.t).
        {:pattern

          Armada.Init.push_stack_variables actor
            writer_pc
            writer_expression_number
            method_id
            frame_uniq
            initializers
            s}
        (match
            Armada.Init.push_stack_variables actor
              writer_pc
              writer_expression_number
              method_id
              frame_uniq
              initializers
              s
          with
          | Armada.Computation.ComputationProduces #_ s' -> pred actor s s'
          | _ -> Prims.l_True)
        <:
        Type0)
Strategies.ArmadaStatement.actor_state_predicate 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.Init.initializer_t Armada.State.t Armada.Init.push_stack_variable Armada.Computation.conditional_computation_t Prims.l_True Strategies.ArmadaStatement.actor_state_predicate_reflexive Strategies.ArmadaStatement.actor_state_predicate_transitive Strategies.ArmadaStatement.make_push_stack_variables_lemma_conditional Prims.bool Prims.unit Prims.squash Prims.list Armada.Init.push_stack_variables Prims.Nil FStar.Pervasives.pattern
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)