val log_expressions_computation_maintains_unstarted_threads_have_empty_write_buffers
      (actor: tid_t)
      (logs_clauses: list expression_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        ThreadStatusRunning? (s.threads actor).status /\
        unstarted_threads_have_empty_write_buffers s)
      (ensures
        (match log_expressions_computation actor logs_clauses s with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> unstarted_threads_have_empty_write_buffers s'))
      (decreases logs_clauses)
val log_expressions_computation_maintains_unstarted_threads_have_empty_write_buffers
      (actor: tid_t)
      (logs_clauses: list expression_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        ThreadStatusRunning? (s.threads actor).status /\
        unstarted_threads_have_empty_write_buffers s)
      (ensures
        (match log_expressions_computation actor logs_clauses s with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> unstarted_threads_have_empty_write_buffers s'))
      (decreases logs_clauses)
let rec log_expressions_computation_maintains_unstarted_threads_have_empty_write_buffers
  (actor: tid_t)
  (logs_clauses: list expression_t)
  (s: Armada.State.t)
  : Lemma (requires   ThreadStatusRunning? (s.threads actor).status
                    /\ unstarted_threads_have_empty_write_buffers s)
          (ensures  (match log_expressions_computation actor logs_clauses s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> unstarted_threads_have_empty_write_buffers s'))
          (decreases logs_clauses) =
  match logs_clauses with
  | [] -> ()
  | first_logs_clause :: remaining_logs_clauses ->
      (match rvalue_computation first_logs_clause actor s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces event ->
           let trace' = s.trace $:: event in
           let s' = { s with trace = trace' } in
           log_expressions_computation_maintains_unstarted_threads_have_empty_write_buffers actor
             remaining_logs_clauses s')
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')
  | _ -> ()

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

let update_expression_maintains_unstarted_threads_have_empty_write_buffers
  (exp: expression_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_expression exp 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_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
              new_value s in
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else
    ()

let rec update_expressions_maintains_unstarted_threads_have_empty_write_buffers
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s: Armada.State.t)
  : Lemma (requires   ThreadStatusRunning? (s.threads actor).status
                    /\ unstarted_threads_have_empty_write_buffers s)
          (ensures  (match update_expressions exps actor writer_pc writer_expression_number bypassing_write_buffer
                             new_values s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' ->
                           ThreadStatusRunning? (s'.threads actor).status
                         /\ unstarted_threads_have_empty_write_buffers s'))
          (decreases exps) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_maintains_unstarted_threads_have_empty_write_buffers first_exp actor writer_pc
        writer_expression_number bypassing_write_buffer first_new_value s;
      (match update_expression first_exp actor writer_pc writer_expression_number
               bypassing_write_buffer first_new_value s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           update_expressions_maintains_unstarted_threads_have_empty_write_buffers remaining_exps actor writer_pc
             (writer_expression_number + 1) bypassing_write_buffer remaining_new_values s')
  | _ -> ()

let rec external_method_take_snapshot_maintains_unstarted_threads_have_empty_write_buffers
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (reads_clauses: list (var_id_t * expression_t))
  (s: Armada.State.t)
  : Lemma (requires   ThreadStatusRunning? (s.threads actor).status
                    /\ unstarted_threads_have_empty_write_buffers s)
          (ensures  (match external_method_take_snapshot_of_reads_clauses_computation actor writer_pc
                             writer_expression_number bypassing_write_buffer reads_clauses s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> unstarted_threads_have_empty_write_buffers s'))
          (decreases reads_clauses) =
  match reads_clauses with
  | [] -> ()
  | (first_var_id, first_reads_expression) :: remaining_reads_clauses ->
      (match rvalue_computation first_reads_expression actor s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces first_value ->
           let td = expression_to_td first_reads_expression in
           let local_var = ExpressionLocalVariable td first_var_id in
           update_expression_maintains_unstarted_threads_have_empty_write_buffers local_var actor writer_pc
             writer_expression_number bypassing_write_buffer first_value s;
           (match update_expression local_var actor writer_pc writer_expression_number bypassing_write_buffer
                    first_value s with
            | ComputationImpossible | ComputationUndefined -> ()
            | ComputationProduces s' ->
                external_method_take_snapshot_maintains_unstarted_threads_have_empty_write_buffers
                  actor writer_pc (writer_expression_number + 1) bypassing_write_buffer remaining_reads_clauses 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

    actor: Armada.Base.tid_t ->
    logs_clauses: Prims.list Armada.Expression.expression_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.Statement.log_expressions_computation actor logs_clauses s with
            | Armada.Computation.ComputationImpossible #_ -> Prims.l_True
            | Armada.Computation.ComputationUndefined #_ -> Prims.l_True
            | Armada.Computation.ComputationProduces #_ s' ->
              Strategies.ArmadaInvariant.UnstartedThreads.unstarted_threads_have_empty_write_buffers
                s')
          <:
          Type0))
      (decreases logs_clauses)
Armada.Base.tid_t Prims.list Armada.Expression.expression_t Armada.State.t Armada.Expression.rvalue_computation Armada.Type.valid_object_value_t Armada.Expression.expression_to_td Strategies.ArmadaInvariant.UnstartedThreads.log_expressions_computation_maintains_unstarted_threads_have_empty_write_buffers Armada.State.Mkt Armada.State.__proj__Mkt__item__initial_tid Armada.State.__proj__Mkt__item__uniqs_used Armada.State.__proj__Mkt__item__mem Armada.State.__proj__Mkt__item__threads Armada.State.__proj__Mkt__item__stop_reason FStar.Sequence.Base.seq Armada.State.trace_entry FStar.Sequence.Base.op_Dollar_Colon_Colon Armada.State.__proj__Mkt__item__trace Prims.unit Prims.l_and Prims.b2t Armada.Thread.uu___is_ThreadStatusRunning Armada.Thread.__proj__Mkt__item__status Strategies.ArmadaInvariant.UnstartedThreads.unstarted_threads_have_empty_write_buffers Prims.squash Armada.Statement.log_expressions_computation Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec log_expressions_computation_maintains_unstarted_threads_have_empty_write_buffers
      (actor: tid_t)
      (logs_clauses: list expression_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        ThreadStatusRunning? (s.threads actor).status /\
        unstarted_threads_have_empty_write_buffers s)
      (ensures
        (match log_expressions_computation actor logs_clauses s with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> unstarted_threads_have_empty_write_buffers s'))
      (decreases logs_clauses) =
  
match logs_clauses with
| [] -> ()
| first_logs_clause :: remaining_logs_clauses ->
  (match rvalue_computation first_logs_clause actor s with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces event ->
      let trace' = s.trace $:: event in
      let s' = { s with trace = trace' } in
      log_expressions_computation_maintains_unstarted_threads_have_empty_write_buffers actor
        remaining_logs_clauses
        s')