val make_update_expression_lemma:
    pred:
      actor_state_predicate
        { (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
              match
                update_expression exp
                  actor
                  writer_pc
                  writer_expression_number
                  bypassing_write_buffer
                  new_value
                  s
              with
              | ComputationProduces s' -> pred actor s s'
              | _ -> True) } ->
    unit
  -> Lemma
    (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
        match
          update_expression exp
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            new_value
            s
        with
        | ComputationProduces s' -> pred actor s s'
        | _ -> True)
val make_update_expression_lemma:
    pred:
      actor_state_predicate
        { (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
              match
                update_expression exp
                  actor
                  writer_pc
                  writer_expression_number
                  bypassing_write_buffer
                  new_value
                  s
              with
              | ComputationProduces s' -> pred actor s s'
              | _ -> True) } ->
    unit
  -> Lemma
    (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
        match
          update_expression exp
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            new_value
            s
        with
        | ComputationProduces s' -> pred actor s s'
        | _ -> True)
let make_update_expression_lemma
  (pred: actor_state_predicate{
       (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
          match update_expression exp actor writer_pc writer_expression_number
                  bypassing_write_buffer new_value s with
          | ComputationProduces s' -> pred actor s s'
          | _ -> True)})
  : unit -> Lemma
      (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
         match update_expression exp actor writer_pc writer_expression_number
                 bypassing_write_buffer new_value s with
         | ComputationProduces s' -> pred actor s s'
         | _ -> True) =
  fun _ -> ()
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
  ()

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

let make_pop_stack_variables_premium
  (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})
  : GTot (actor: _ -> method_id: _ -> frame_uniq: _ -> var_ids: _ -> mem: _ ->
          GTot (result: conditional_computation_t Armada.Memory.t{
                  result == pop_stack_variables actor method_id frame_uniq var_ids mem
                /\ (match result with | ComputationProduces mem' -> pred actor mem mem' | _ -> True)})) =
  let f actor method_id frame_uniq var_ids mem
    : GTot (result: conditional_computation_t Armada.Memory.t{
              result == pop_stack_variables actor method_id frame_uniq var_ids mem
            /\ (match result with | ComputationProduces mem' -> pred actor mem mem' | _ -> True)}) =
    make_pop_stack_variables_lemma pred ();
    pop_stack_variables actor method_id frame_uniq var_ids mem
  in
  f

let make_push_stack_parameters_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 var_ids parameters s.
         {:pattern push_stack_parameters actor writer_pc writer_expression_number
                     method_id frame_uniq var_ids parameters s}
         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) =
  make_push_stack_parameters_lemma_conditional pred (fun _ -> true)

let make_push_stack_parameters_premium_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})
  : GTot (actor: _ -> writer_pc: _ -> writer_expression_number: _ -> method_id: _ -> frame_uniq: _ ->
          var_ids: _ -> parameters: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
                   result == push_stack_parameters actor writer_pc writer_expression_number
                               method_id frame_uniq var_ids parameters s
                 /\ (for_all_ghost parameter_cond parameters ==>
                    (match result with | ComputationProduces s' -> pred actor s s' | _ -> True))})) =
  make_push_stack_parameters_lemma_conditional pred parameter_cond ();
  let f actor writer_pc writer_expression_number method_id frame_uniq var_ids parameters s
    : GTot (result: conditional_computation_t Armada.State.t{
              result == push_stack_parameters actor writer_pc writer_expression_number method_id
                          frame_uniq var_ids parameters s
              /\ (for_all_ghost parameter_cond parameters ==>
                 (match result with | ComputationProduces s' -> pred actor s s' | _ -> True))}) =
    push_stack_parameters actor writer_pc writer_expression_number method_id frame_uniq var_ids
      parameters s
  in
  f

let make_push_stack_parameters_premium
  (pred: actor_state_predicate{
       (forall actor writer_pc writer_expression_number method_id frame_uniq var_ids s.
          match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                  var_ids 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: _ ->
          var_ids: _ -> parameters: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
                   result == push_stack_parameters actor writer_pc writer_expression_number
                               method_id frame_uniq var_ids parameters s
                 /\ (match result with | ComputationProduces s' -> pred actor s s' | _ -> True)})) =
  make_push_stack_parameters_premium_conditional pred (fun _ -> true)

let make_push_stack_parameters_premium_conditional_negative
  (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})
  : GTot (actor: _ -> writer_pc: _ -> writer_expression_number: _ -> method_id: _ -> frame_uniq: _ ->
          var_ids: _ -> parameters: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
                   result == push_stack_parameters actor writer_pc writer_expression_number
                               method_id frame_uniq var_ids parameters s
                 /\ (exists_ghost parameter_cond parameters \/
                     (match result with | ComputationProduces s' -> pred actor s s' | _ -> True))})) =
  make_push_stack_parameters_premium_conditional pred (fun parameter -> not (parameter_cond parameter))
/
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 (exp: Armada.Expression.expression_t)
            (actor: Armada.Base.tid_t)
            (writer_pc: Armada.Base.pc_t)
            (writer_expression_number: Prims.nat)
            (bypassing_write_buffer: Prims.bool)
            (new_value: Armada.Type.object_value_t)
            (s: Armada.State.t).
            (match
                Armada.Expression.update_expression exp
                  actor
                  writer_pc
                  writer_expression_number
                  bypassing_write_buffer
                  new_value
                  s
              with
              | Armada.Computation.ComputationProduces #_ s' -> pred actor s s'
              | _ -> Prims.l_True)
            <:
            Type0 } ->
    _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      forall (exp: Armada.Expression.expression_t)
        (actor: Armada.Base.tid_t)
        (writer_pc: Armada.Base.pc_t)
        (writer_expression_number: Prims.nat)
        (bypassing_write_buffer: Prims.bool)
        (new_value: Armada.Type.object_value_t)
        (s: Armada.State.t).
        (match
            Armada.Expression.update_expression exp
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | Armada.Computation.ComputationProduces #_ s' -> pred actor s s'
          | _ -> Prims.l_True)
        <:
        Type0)
Strategies.ArmadaStatement.actor_state_predicate Prims.l_Forall Armada.Expression.expression_t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Armada.Type.object_value_t Armada.State.t Armada.Expression.update_expression Armada.Computation.conditional_computation_t Prims.l_True Prims.unit Prims.squash Prims.Nil FStar.Pervasives.pattern
let make_update_expression_lemma
      (pred:
          actor_state_predicate
            { (forall exp
                  actor
                  writer_pc
                  writer_expression_number
                  bypassing_write_buffer
                  new_value
                  s.
                  match
                    update_expression exp
                      actor
                      writer_pc
                      writer_expression_number
                      bypassing_write_buffer
                      new_value
                      s
                  with
                  | ComputationProduces s' -> pred actor s s'
                  | _ -> True) })
    :  unit
      -> Lemma
        (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
            match
              update_expression exp
                actor
                writer_pc
                writer_expression_number
                bypassing_write_buffer
                new_value
                s
            with
            | ComputationProduces s' -> pred actor s s'
            | _ -> True) =
  
fun _ -> ()