val make_update_expressions_lemma_conditional:
    pred: actor_state_predicate ->
    exp_value_pred:
      (expression_t -> object_value_t -> bool)
        { (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
              exp_value_pred exp new_value ==>
              (match
                  update_expression exp
                    actor
                    writer_pc
                    writer_expression_number
                    bypassing_write_buffer
                    new_value
                    s
                with
                | ComputationProduces s' -> pred actor s s'
                | _ -> True)) /\ actor_state_predicate_reflexive pred /\
          actor_state_predicate_transitive pred } ->
    unit
  -> Lemma
    (forall exps actor writer_pc writer_expression_number bypassing_write_buffer new_values s.
        lists_correspond exp_value_pred exps new_values ==>
        (match
            update_expressions exps
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_values
              s
          with
          | ComputationProduces s' -> pred actor s s'
          | _ -> True))
val make_update_expressions_lemma_conditional:
    pred: actor_state_predicate ->
    exp_value_pred:
      (expression_t -> object_value_t -> bool)
        { (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
              exp_value_pred exp new_value ==>
              (match
                  update_expression exp
                    actor
                    writer_pc
                    writer_expression_number
                    bypassing_write_buffer
                    new_value
                    s
                with
                | ComputationProduces s' -> pred actor s s'
                | _ -> True)) /\ actor_state_predicate_reflexive pred /\
          actor_state_predicate_transitive pred } ->
    unit
  -> Lemma
    (forall exps actor writer_pc writer_expression_number bypassing_write_buffer new_values s.
        lists_correspond exp_value_pred exps new_values ==>
        (match
            update_expressions exps
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_values
              s
          with
          | ComputationProduces s' -> pred actor s s'
          | _ -> True))
let make_update_expressions_lemma_conditional
  (pred: actor_state_predicate)
  (exp_value_pred: expression_t -> object_value_t -> bool{
       (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
          exp_value_pred exp new_value ==>
          (match update_expression exp actor writer_pc writer_expression_number
                   bypassing_write_buffer new_value s with
           | ComputationProduces s' -> pred actor s s'
           | _ -> True))
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : unit -> Lemma
      (forall exps actor writer_pc writer_expression_number bypassing_write_buffer new_values s.
         lists_correspond exp_value_pred exps new_values ==>
         (match update_expressions exps actor writer_pc writer_expression_number
                  bypassing_write_buffer new_values s with
          | ComputationProduces s' -> pred actor s s'
          | _ -> True)) =
  fun _ ->
  let rec internal_lem exps actor writer_pc writer_expression_number bypassing_write_buffer
                         new_values s
    : Lemma (requires lists_correspond exp_value_pred exps new_values)
            (ensures (match update_expressions exps actor writer_pc writer_expression_number
                              bypassing_write_buffer new_values s with
                      | ComputationProduces s' -> pred actor s s'
                      | _ -> True))
            (decreases exps)
            [SMTPat (update_expressions exps actor writer_pc writer_expression_number
                              bypassing_write_buffer new_values s)] =
    match exps, new_values with
    | [], [] -> ()
    | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
        (match update_expression first_exp actor writer_pc writer_expression_number
                 bypassing_write_buffer first_new_value s with
         | ComputationProduces s' ->
             internal_lem remaining_exps actor writer_pc (writer_expression_number + 1)
                            bypassing_write_buffer remaining_new_values s'
         | _ -> ())
    | _ -> ()
  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
  ()

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

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

let make_update_expression_premium_conditional
  (pred: actor_state_predicate)
  (exp_value_pred: expression_t -> object_value_t -> bool{
       (forall exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s.
          exp_value_pred exp new_value ==>
          (match update_expression exp actor writer_pc writer_expression_number
                   bypassing_write_buffer new_value s with
           | ComputationProduces s' -> pred actor s s'
           | _ -> True))
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : GTot (exp: _ -> actor: _ -> writer_pc: _ -> writer_expression_number: _ ->
          bypassing_write_buffer: _ -> new_value: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
            result == update_expression exp actor writer_pc writer_expression_number
                        bypassing_write_buffer new_value s
          /\ (exp_value_pred exp new_value ==>
              (match result with
               | ComputationProduces s' -> pred actor s s'
               | _ -> True))})) =
  let f exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s
    : GTot (result: conditional_computation_t Armada.State.t{
              result == update_expression exp actor writer_pc writer_expression_number
                          bypassing_write_buffer new_value s
              /\ (exp_value_pred exp new_value ==>
                 (match result with
                  | ComputationProduces s' -> pred actor s s'
                  | _ -> True))}) =
    update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
      new_value s
  in
  f

let make_update_expression_premium
  (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)
     /\ actor_state_predicate_reflexive pred
     /\ actor_state_predicate_transitive pred})
  : GTot (exp: _ -> actor: _ -> writer_pc: _ -> writer_expression_number: _ ->
          bypassing_write_buffer: _ -> new_value: _ -> s: _ ->
          GTot (result: conditional_computation_t Armada.State.t{
            result == update_expression exp actor writer_pc writer_expression_number
                        bypassing_write_buffer new_value s
          /\ (match result with | ComputationProduces s' -> pred actor s s' | _ -> True)})) =
  let f exp actor writer_pc writer_expression_number bypassing_write_buffer new_value s
    : GTot (result: conditional_computation_t Armada.State.t{
              result == update_expression exp actor writer_pc writer_expression_number
                          bypassing_write_buffer new_value s
              /\ (match result with | ComputationProduces s' -> pred actor s s' | _ -> True)}) =
    update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
      new_value s
  in
  f
/
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 ->
    exp_value_pred:
      (_: Armada.Expression.expression_t -> _: Armada.Type.object_value_t -> Prims.bool)
        { (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).
              exp_value_pred exp new_value ==>
              (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)) /\
          Strategies.ArmadaStatement.actor_state_predicate_reflexive pred /\
          Strategies.ArmadaStatement.actor_state_predicate_transitive pred } ->
    _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures
      forall (exps: Prims.list 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_values: Prims.list Armada.Type.object_value_t)
        (s: Armada.State.t).
        Util.List.lists_correspond exp_value_pred exps new_values ==>
        (match
            Armada.Expression.update_expressions exps
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_values
              s
          with
          | Armada.Computation.ComputationProduces #_ s' -> pred actor s s'
          | _ -> Prims.l_True))
Strategies.ArmadaStatement.actor_state_predicate Armada.Expression.expression_t Armada.Type.object_value_t Prims.bool Prims.l_and Prims.l_Forall Armada.Base.tid_t Armada.Base.pc_t Prims.nat Armada.State.t Prims.l_imp Prims.b2t Armada.Expression.update_expression Armada.Computation.conditional_computation_t Prims.l_True Prims.logical Strategies.ArmadaStatement.actor_state_predicate_reflexive Strategies.ArmadaStatement.actor_state_predicate_transitive Prims.unit Prims.list Util.List.lists_correspond Prims.squash Armada.Expression.update_expressions Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil FStar.Pervasives.Native.Mktuple2 Prims.op_Addition FStar.Pervasives.Native.tuple2
let make_update_expressions_lemma_conditional
      (pred: actor_state_predicate)
      (exp_value_pred:
          (expression_t -> object_value_t -> bool)
            { (forall exp
                  actor
                  writer_pc
                  writer_expression_number
                  bypassing_write_buffer
                  new_value
                  s.
                  exp_value_pred exp new_value ==>
                  (match
                      update_expression exp
                        actor
                        writer_pc
                        writer_expression_number
                        bypassing_write_buffer
                        new_value
                        s
                    with
                    | ComputationProduces s' -> pred actor s s'
                    | _ -> True)) /\ actor_state_predicate_reflexive pred /\
              actor_state_predicate_transitive pred })
    :  unit
      -> Lemma
        (forall exps actor writer_pc writer_expression_number bypassing_write_buffer new_values s.
            lists_correspond exp_value_pred exps new_values ==>
            (match
                update_expressions exps
                  actor
                  writer_pc
                  writer_expression_number
                  bypassing_write_buffer
                  new_values
                  s
              with
              | ComputationProduces s' -> pred actor s s'
              | _ -> True)) =
  
fun _ ->
  let rec internal_lem
        exps
        actor
        writer_pc
        writer_expression_number
        bypassing_write_buffer
        new_values
        s
      : Lemma (requires lists_correspond exp_value_pred exps new_values)
        (ensures
          (match
              update_expressions exps
                actor
                writer_pc
                writer_expression_number
                bypassing_write_buffer
                new_values
                s
            with
            | ComputationProduces s' -> pred actor s s'
            | _ -> True))
        (decreases exps)
        [
          SMTPat
          (update_expressions exps
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_values
              s)
        ] =
    match exps, new_values with
    | [], [] -> ()
    | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      (match
          update_expression first_exp
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            first_new_value
            s
        with
        | ComputationProduces s' ->
          internal_lem remaining_exps
            actor
            writer_pc
            (writer_expression_number + 1)
            bypassing_write_buffer
            remaining_new_values
            s'
        | _ -> ())
    | _ -> ()
  in
  ()