val update_pointed_to_value_maintains_unstarted_threads_have_empty_write_buffers
      (p: Armada.Pointer.t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        ThreadStatusRunning? (s.threads actor).status /\
        unstarted_threads_have_empty_write_buffers s)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' ->
            ThreadStatusRunning? (s'.threads actor).status /\
            unstarted_threads_have_empty_write_buffers s'))
val update_pointed_to_value_maintains_unstarted_threads_have_empty_write_buffers
      (p: Armada.Pointer.t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        ThreadStatusRunning? (s.threads actor).status /\
        unstarted_threads_have_empty_write_buffers s)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' ->
            ThreadStatusRunning? (s'.threads actor).status /\
            unstarted_threads_have_empty_write_buffers s'))
let update_pointed_to_value_maintains_unstarted_threads_have_empty_write_buffers
  (p: Armada.Pointer.t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s: Armada.State.t)
  : Lemma (requires   ThreadStatusRunning? (s.threads actor).status
                    /\ unstarted_threads_have_empty_write_buffers s)
          (ensures  (match update_pointed_to_value p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' ->
                           ThreadStatusRunning? (s'.threads actor).status
                         /\ unstarted_threads_have_empty_write_buffers s')) =
  let cs' = update_pointed_to_value p actor writer_pc writer_expression_number bypassing_write_buffer
              new_value s in
  ()
module Strategies.ArmadaInvariant.UnstartedThreads

open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Type
open FStar.Sequence.Base
open Spec.Ubool
open Strategies.ArmadaStatement

let init_implies_unstarted_threads_have_empty_write_buffers (program: Armada.Program.t) (s: Armada.State.t)
  : Lemma (requires init_program program s)
          (ensures  unstarted_threads_have_empty_write_buffers s) =
  ()

#push-options "--z3rlimit 10"

let push_stack_variable_maintains_unstarted_threads_have_empty_write_buffers
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializer: initializer_t)
  (s: Armada.State.t)
  : Lemma (requires   ThreadStatusRunning? (s.threads actor).status
                    /\ unstarted_threads_have_empty_write_buffers s)
          (ensures  (match push_stack_variable actor writer_pc writer_expression_number method_id
                             frame_uniq initializer s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' ->
                           (forall tid. ThreadStatusRunning? (s.threads tid).status ==>
                                   ThreadStatusRunning? (s'.threads tid).status)
                         /\ unstarted_threads_have_empty_write_buffers s')) =
  ()

#pop-options

let rec push_stack_variables_maintains_unstarted_threads_have_empty_write_buffers
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializers: list initializer_t)
  (s: Armada.State.t)
  : Lemma (requires   ThreadStatusRunning? (s.threads actor).status
                    /\ unstarted_threads_have_empty_write_buffers s)
          (ensures  (match push_stack_variables actor writer_pc writer_expression_number method_id
                             frame_uniq initializers s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' ->
                           (forall tid. ThreadStatusRunning? (s.threads tid).status ==>
                                   ThreadStatusRunning? (s'.threads tid).status)
                         /\ unstarted_threads_have_empty_write_buffers s'))
          (decreases initializers) =
  match initializers with
  | [] -> ()
  | first_initializer :: remaining_initializers ->
      push_stack_variable_maintains_unstarted_threads_have_empty_write_buffers actor writer_pc
        writer_expression_number method_id frame_uniq first_initializer s;
      (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq first_initializer s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           push_stack_variables_maintains_unstarted_threads_have_empty_write_buffers actor writer_pc
             (writer_expression_number + 1) method_id frame_uniq remaining_initializers s')

let rec push_stack_parameters_maintains_unstarted_threads_have_empty_write_buffers
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (var_ids: list var_id_t)
  (parameters: list object_value_t)
  (s: Armada.State.t)
  : Lemma (requires   ThreadStatusRunning? (s.threads actor).status
                    /\ unstarted_threads_have_empty_write_buffers s)
          (ensures  (match push_stack_parameters actor writer_pc writer_expression_number method_id frame_uniq
                             var_ids parameters s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' ->
                           (forall tid. ThreadStatusRunning? (s.threads tid).status ==>
                                   ThreadStatusRunning? (s'.threads tid).status)
                         /\ unstarted_threads_have_empty_write_buffers s'))
          (decreases parameters) =
  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
      push_stack_variable_maintains_unstarted_threads_have_empty_write_buffers actor writer_pc
        writer_expression_number method_id frame_uniq first_initializer s;
      (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq first_initializer s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           push_stack_parameters_maintains_unstarted_threads_have_empty_write_buffers actor writer_pc
             (writer_expression_number + 1) method_id frame_uniq remaining_var_ids remaining_parameters s')
  | _ -> ()
/
Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.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
Strategies.ArmadaInvariant.UnstartedThreads.fst

    p: Armada.Pointer.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
  -> FStar.Pervasives.Lemma
      (requires
        ThreadStatusRunning? (Mkt?.status (Mkt?.threads s actor)) /\
        Strategies.ArmadaInvariant.UnstartedThreads.unstarted_threads_have_empty_write_buffers s)
      (ensures
        ((match
              Armada.Expression.update_pointed_to_value p
                actor
                writer_pc
                writer_expression_number
                bypassing_write_buffer
                new_value
                s
            with
            | Armada.Computation.ComputationImpossible #_ -> Prims.l_True
            | Armada.Computation.ComputationUndefined #_ -> Prims.l_True
            | Armada.Computation.ComputationProduces #_ s' ->
              ThreadStatusRunning? (Mkt?.status (Mkt?.threads s' actor)) /\
              Strategies.ArmadaInvariant.UnstartedThreads.unstarted_threads_have_empty_write_buffers
                s')
          <:
          Type0))
Armada.Pointer.t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Armada.Type.object_value_t Armada.State.t Armada.Computation.conditional_computation_t Armada.Expression.update_pointed_to_value Prims.unit Prims.l_and Prims.b2t Armada.Thread.uu___is_ThreadStatusRunning Armada.Thread.__proj__Mkt__item__status Armada.State.__proj__Mkt__item__threads Strategies.ArmadaInvariant.UnstartedThreads.unstarted_threads_have_empty_write_buffers Prims.squash Prims.l_True Prims.Nil FStar.Pervasives.pattern
let update_pointed_to_value_maintains_unstarted_threads_have_empty_write_buffers
      (p: Armada.Pointer.t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        ThreadStatusRunning? (s.threads actor).status /\
        unstarted_threads_have_empty_write_buffers s)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' ->
            ThreadStatusRunning? (s'.threads actor).status /\
            unstarted_threads_have_empty_write_buffers s')) =
  
let cs' =
  update_pointed_to_value p
    actor
    writer_pc
    writer_expression_number
    bypassing_write_buffer
    new_value
    s
in
()